From b4c5bf2306f6c7212821b671231f3ee2bcc554e1 Mon Sep 17 00:00:00 2001 From: Wenjie Ma Date: Fri, 25 Aug 2023 12:06:39 -0500 Subject: [PATCH] Move some lemmas Signed-off-by: Wenjie Ma --- .../rabbitmq_controller/proof/safety.rs | 139 +++++------------- src/kubernetes_cluster/proof/message.rs | 115 +++++++++++++++ 2 files changed, 151 insertions(+), 103 deletions(-) diff --git a/src/controller_examples/rabbitmq_controller/proof/safety.rs b/src/controller_examples/rabbitmq_controller/proof/safety.rs index e92101912..c3f71c1d3 100644 --- a/src/controller_examples/rabbitmq_controller/proof/safety.rs +++ b/src/controller_examples/rabbitmq_controller/proof/safety.rs @@ -54,12 +54,12 @@ proof fn lemma_stateful_set_never_scaled_down_for_rabbitmq(spec: TempPred= replicas_of_stateful_set(s.resource_obj_of(sts_key))); } - } + } } } invariant_n!( spec, lift_action(next), lift_action(inv), lift_action(RMQCluster::next()), lift_state(replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd(rabbitmq)), - lift_state(stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(rabbitmq)), + lift_state(object_in_sts_update_request_has_smaller_rv_than_etcd(rabbitmq)), lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), later(lift_state(RMQCluster::each_object_in_etcd_is_well_formed())) ); } @@ -373,32 +373,26 @@ proof fn lemma_always_response_at_after_get_stateful_set_step_is_sts_get_respons init_invariant(spec, RMQCluster::init(), next, inv); } -spec fn stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(rabbitmq: RabbitmqClusterView) -> StatePred { +spec fn object_in_sts_update_request_has_smaller_rv_than_etcd(rabbitmq: RabbitmqClusterView) -> StatePred { |s: RMQCluster| { let sts_key = make_stateful_set_key(rabbitmq.object_ref()); let etcd_rv = s.resource_obj_of(sts_key).metadata.resource_version.get_Some_0(); forall |msg: RMQMessage| #[trigger] s.message_in_flight(msg) - ==> ( - sts_update_request_msg(rabbitmq.object_ref())(msg) - ==> msg.content.get_update_request().obj.metadata.resource_version.is_Some() - && msg.content.get_update_request().obj.metadata.resource_version.get_Some_0() < s.kubernetes_api_state.resource_version_counter - ) && ( - ok_sts_get_response_msg(rabbitmq.object_ref())(msg) - ==> msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.is_Some() - && msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.get_Some_0() < s.kubernetes_api_state.resource_version_counter - ) + && sts_update_request_msg(rabbitmq.object_ref())(msg) + ==> msg.content.get_update_request().obj.metadata.resource_version.is_Some() + && msg.content.get_update_request().obj.metadata.resource_version.get_Some_0() < s.kubernetes_api_state.resource_version_counter } } -proof fn lemma_always_stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd( +proof fn lemma_always_object_in_sts_update_request_has_smaller_rv_than_etcd( spec: TempPred, rabbitmq: RabbitmqClusterView ) requires spec.entails(lift_state(RMQCluster::init())), spec.entails(always(lift_action(RMQCluster::next()))), ensures - spec.entails(always(lift_state(stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(rabbitmq)))), + spec.entails(always(lift_state(object_in_sts_update_request_has_smaller_rv_than_etcd(rabbitmq)))), { let key = rabbitmq.object_ref(); let sts_key = make_stateful_set_key(rabbitmq.object_ref()); @@ -407,46 +401,40 @@ proof fn lemma_always_stateful_set_in_get_response_and_update_request_have_no_la ==> msg.content.get_update_request().obj.metadata.resource_version.is_Some() && msg.content.get_update_request().obj.metadata.resource_version.get_Some_0() < s.kubernetes_api_state.resource_version_counter }; - let get_rv_leq = |msg: RMQMessage, s: RMQCluster| { - ok_sts_get_response_msg(rabbitmq.object_ref())(msg) - ==> msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.is_Some() - && msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.get_Some_0() < s.kubernetes_api_state.resource_version_counter - }; - let inv = stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(rabbitmq); + let inv = object_in_sts_update_request_has_smaller_rv_than_etcd(rabbitmq); let next = |s, s_prime| { &&& RMQCluster::next()(s, s_prime) &&& RMQCluster::each_object_in_etcd_is_well_formed()(s) &&& RMQCluster::each_object_in_etcd_is_well_formed()(s_prime) &&& response_at_after_get_stateful_set_step_is_sts_get_response(rabbitmq)(s) &&& RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s) + &&& RMQCluster::object_in_ok_get_response_has_lower_rv_than_etcd(sts_key)(s) }; RMQCluster::lemma_always_each_object_in_etcd_is_well_formed(spec); lemma_always_response_at_after_get_stateful_set_step_is_sts_get_response(spec, rabbitmq); always_to_always_later(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed())); RMQCluster::lemma_always_each_object_in_reconcile_has_consistent_key_and_valid_metadata(spec); + RMQCluster::lemma_always_object_in_ok_get_response_has_lower_rv_than_etcd(spec, sts_key); combine_spec_entails_always_n!( spec, lift_action(next), lift_action(RMQCluster::next()), lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), later(lift_state(RMQCluster::each_object_in_etcd_is_well_formed())), lift_state(response_at_after_get_stateful_set_step_is_sts_get_response(rabbitmq)), - lift_state(RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()) + lift_state(RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()), + lift_state(RMQCluster::object_in_ok_get_response_has_lower_rv_than_etcd(sts_key)) ); assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by { let etcd_rv = s.resource_obj_of(sts_key).metadata.resource_version.get_Some_0(); - assert forall |msg| #[trigger] s_prime.message_in_flight(msg) implies upd_rv_leq(msg, s_prime) && get_rv_leq(msg, s_prime) by { + assert forall |msg| #[trigger] s_prime.message_in_flight(msg) && sts_update_request_msg(rabbitmq.object_ref())(msg) implies + msg.content.get_update_request().obj.metadata.resource_version.is_Some() + && msg.content.get_update_request().obj.metadata.resource_version.get_Some_0() < s_prime.kubernetes_api_state.resource_version_counter by { let step = choose |step| RMQCluster::next_step(s, s_prime, step); if s.message_in_flight(msg) { assert(s.kubernetes_api_state.resource_version_counter <= s_prime.kubernetes_api_state.resource_version_counter); } else if sts_update_request_msg(rabbitmq.object_ref())(msg) { lemma_stateful_set_update_request_msg_implies_key_in_reconcile_equals(key, s, s_prime, msg, step); assert(at_rabbitmq_step(key, RabbitmqReconcileStep::AfterUpdateStatefulSet)(s_prime)); - } else if ok_sts_get_response_msg(rabbitmq.object_ref())(msg) { - let input = step.get_KubernetesAPIStep_0().get_Some_0(); - assert(s.resource_key_exists(input.content.get_get_request().key)); - assert(input.content.get_get_request().key == sts_key); - assert(msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.get_Some_0() == s.resource_obj_of(sts_key).metadata.resource_version.get_Some_0()); - assert(s.resource_obj_of(sts_key).metadata.resource_version.get_Some_0() < s.kubernetes_api_state.resource_version_counter); - } + } } } init_invariant(spec, RMQCluster::init(), next, inv); @@ -494,63 +482,6 @@ spec fn replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd(rabb } } -spec fn helper_3_spec_ok_get_resp(rabbitmq: RabbitmqClusterView) -> StatePred { - |s: RMQCluster| { - let key = rabbitmq.object_ref(); - let sts_key = make_stateful_set_key(key); - forall |msg| - #[trigger] s.message_in_flight(msg) - && ok_sts_get_response_msg(key)(msg) - && s.resource_key_exists(sts_key) - && s.resource_obj_of(sts_key).metadata.resource_version.get_Some_0() == msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.get_Some_0() - ==> s.resource_obj_of(sts_key) == msg.content.get_get_response().res.get_Ok_0() - } -} - -proof fn lemma_always_helper_3_spec(spec: TempPred, rabbitmq: RabbitmqClusterView) - requires - spec.entails(lift_state(RMQCluster::init())), - spec.entails(always(lift_action(RMQCluster::next()))), - ensures - spec.entails(always(lift_state(helper_3_spec_ok_get_resp(rabbitmq)))), -{ - let key = rabbitmq.object_ref(); - let sts_key = make_stateful_set_key(key); - let inv = helper_3_spec_ok_get_resp(rabbitmq); - let next = |s, s_prime| { - &&& RMQCluster::next()(s, s_prime) - &&& RMQCluster::each_object_in_etcd_is_well_formed()(s) - &&& stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(rabbitmq)(s) - }; - RMQCluster::lemma_always_each_object_in_etcd_is_well_formed(spec); - lemma_always_stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(spec, rabbitmq); - combine_spec_entails_always_n!( - spec, lift_action(next), lift_action(RMQCluster::next()), lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), - lift_state(stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(rabbitmq)) - ); - assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by { - assert forall |msg| #[trigger] s_prime.message_in_flight(msg) && ok_sts_get_response_msg(key)(msg) && s_prime.resource_key_exists(sts_key) - && s_prime.resource_obj_of(sts_key).metadata.resource_version.get_Some_0() == msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.get_Some_0() implies s_prime.resource_obj_of(sts_key) == msg.content.get_get_response().res.get_Ok_0() by { - if s.message_in_flight(msg) { - if !s.resource_key_exists(sts_key) || s.resource_obj_of(sts_key) != s_prime.resource_obj_of(sts_key) { - assert(s_prime.resource_obj_of(sts_key).metadata.resource_version.get_Some_0() != msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.get_Some_0()) - } - } else { - let step = choose |step| RMQCluster::next_step(s, s_prime, step); - assert(step.is_KubernetesAPIStep()); - let req = step.get_KubernetesAPIStep_0().get_Some_0(); - assert(msg == RMQCluster::handle_get_request(req, s.kubernetes_api_state).1); - assert(s.resource_key_exists(req.content.get_get_request().key)); - assert(msg.content.get_get_response().res.get_Ok_0() == s.resource_obj_of(req.content.get_get_request().key)); - assert(req.content.get_get_request().key == msg.content.get_get_response().res.get_Ok_0().object_ref()); - assert(s.kubernetes_api_state == s_prime.kubernetes_api_state); - assert(s_prime.resource_obj_of(sts_key) == msg.content.get_get_response().res.get_Ok_0()); - } - } - } - init_invariant(spec, RMQCluster::init(), next, inv); -} - proof fn lemma_always_replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd(spec: TempPred, rabbitmq: RabbitmqClusterView) requires spec.entails(lift_state(RMQCluster::init())), @@ -559,50 +490,52 @@ proof fn lemma_always_replicas_of_stateful_set_update_request_msg_is_no_smaller_ spec.entails(always(lift_state(replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd(rabbitmq)))), { let inv = replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd(rabbitmq); + let key = rabbitmq.object_ref(); + let sts_key = make_stateful_set_key(key); let next = |s, s_prime| { &&& RMQCluster::next()(s, s_prime) &&& RMQCluster::each_object_in_etcd_is_well_formed()(s) &&& RMQCluster::each_object_in_etcd_is_well_formed()(s_prime) &&& replicas_of_etcd_stateful_set_satisfies_order(rabbitmq)(s_prime) - &&& stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(rabbitmq)(s) + &&& object_in_sts_update_request_has_smaller_rv_than_etcd(rabbitmq)(s) &&& RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s) - &&& helper_3_spec_ok_get_resp(rabbitmq)(s) + &&& RMQCluster::object_in_ok_get_resp_is_same_as_etcd_with_same_rv(sts_key)(s) &&& response_at_after_get_stateful_set_step_is_sts_get_response(rabbitmq)(s) }; RMQCluster::lemma_always_each_object_in_etcd_is_well_formed(spec); always_to_always_later(spec, lift_state(RMQCluster::each_object_in_etcd_is_well_formed())); lemma_always_replicas_of_etcd_stateful_set_satisfies_order(spec, rabbitmq); always_to_always_later(spec, lift_state(replicas_of_etcd_stateful_set_satisfies_order(rabbitmq))); - lemma_always_stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(spec, rabbitmq); + lemma_always_object_in_sts_update_request_has_smaller_rv_than_etcd(spec, rabbitmq); RMQCluster::lemma_always_each_object_in_reconcile_has_consistent_key_and_valid_metadata(spec); - lemma_always_helper_3_spec(spec, rabbitmq); + RMQCluster::lemma_always_object_in_ok_get_resp_is_same_as_etcd_with_same_rv(spec, sts_key); lemma_always_response_at_after_get_stateful_set_step_is_sts_get_response(spec, rabbitmq); combine_spec_entails_always_n!( spec, lift_action(next), lift_action(RMQCluster::next()), lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), later(lift_state(RMQCluster::each_object_in_etcd_is_well_formed())), later(lift_state(replicas_of_etcd_stateful_set_satisfies_order(rabbitmq))), - lift_state(stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(rabbitmq)), + lift_state(object_in_sts_update_request_has_smaller_rv_than_etcd(rabbitmq)), lift_state(RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()), - lift_state(helper_3_spec_ok_get_resp(rabbitmq)), + lift_state(RMQCluster::object_in_ok_get_resp_is_same_as_etcd_with_same_rv(sts_key)), lift_state(response_at_after_get_stateful_set_step_is_sts_get_response(rabbitmq)) ); assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by { - helper_2(rabbitmq, s, s_prime); + replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd_induction(rabbitmq, s, s_prime); } init_invariant(spec, RMQCluster::init(), next, inv); } -proof fn helper_2(rabbitmq: RabbitmqClusterView, s: RMQCluster, s_prime: RMQCluster) +proof fn replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd_induction(rabbitmq: RabbitmqClusterView, s: RMQCluster, s_prime: RMQCluster) requires RMQCluster::next()(s, s_prime), RMQCluster::each_object_in_etcd_is_well_formed()(s), RMQCluster::each_object_in_etcd_is_well_formed()(s_prime), replicas_of_etcd_stateful_set_satisfies_order(rabbitmq)(s_prime), replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd(rabbitmq)(s), - stateful_set_in_get_response_and_update_request_have_no_larger_resource_version_than_etcd(rabbitmq)(s), + object_in_sts_update_request_has_smaller_rv_than_etcd(rabbitmq)(s), RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s), - helper_3_spec_ok_get_resp(rabbitmq)(s), + RMQCluster::object_in_ok_get_resp_is_same_as_etcd_with_same_rv(make_stateful_set_key(rabbitmq.object_ref()))(s), response_at_after_get_stateful_set_step_is_sts_get_response(rabbitmq)(s), ensures replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd(rabbitmq)(s_prime), @@ -663,12 +596,12 @@ proof fn lemma_always_replicas_of_etcd_stateful_set_satisfies_order(spec: TempPr lift_state(replicas_of_stateful_set_create_request_msg_satisfies_order(rabbitmq)) ); assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by { - helper_1(rabbitmq, s, s_prime); + replicas_of_etcd_stateful_set_satisfies_order_induction(rabbitmq, s, s_prime); } init_invariant(spec, RMQCluster::init(), next, inv); } -proof fn helper_1(rabbitmq: RabbitmqClusterView, s: RMQCluster, s_prime: RMQCluster) +proof fn replicas_of_etcd_stateful_set_satisfies_order_induction(rabbitmq: RabbitmqClusterView, s: RMQCluster, s_prime: RMQCluster) requires RMQCluster::next()(s, s_prime), replicas_of_etcd_stateful_set_satisfies_order(rabbitmq)(s), @@ -729,7 +662,7 @@ spec fn owner_references_is_valid(obj: DynamicObjectView, s: RMQCluster) -> bool #![auto] 0 <= i < owner_refs.len() ==> owner_refs[i].uid < s.kubernetes_api_state.uid_counter } - + } spec fn object_in_every_create_or_update_request_msg_only_has_valid_owner_references() -> StatePred { @@ -959,7 +892,7 @@ proof fn lemma_always_replicas_of_stateful_set_create_request_msg_satisfies_orde assert(replicas_satisfies_order(msg.content.get_create_request().obj, rabbitmq)(s_prime)); } } - } + } } init_invariant(spec, RMQCluster::init(), next, inv); } @@ -1065,7 +998,7 @@ proof fn lemma_always_replicas_of_stateful_set_update_request_msg_satisfies_orde assert(replicas_satisfies_order(msg.content.get_update_request().obj, rabbitmq)(s_prime)); } } - } + } } init_invariant(spec, RMQCluster::init(), next, inv); } diff --git a/src/kubernetes_cluster/proof/message.rs b/src/kubernetes_cluster/proof/message.rs index 99f1e8fc4..58c2e3b47 100644 --- a/src/kubernetes_cluster/proof/message.rs +++ b/src/kubernetes_cluster/proof/message.rs @@ -346,6 +346,121 @@ pub proof fn lemma_always_pending_req_has_lower_req_id_than_allocator(spec: Temp ); } +pub open spec fn ok_get_response_msg(key: ObjectRef) -> FnSpec(MsgType) -> bool { + |msg: MsgType| + msg.src.is_KubernetesAPI() + && msg.content.is_get_response() + && msg.content.get_get_response().res.is_Ok() + && msg.content.get_get_response().res.get_Ok_0().object_ref() == key +} + +pub open spec fn object_in_ok_get_response_has_lower_rv_than_etcd(key: ObjectRef) -> StatePred { + |s: Self| { + let etcd_rv = s.resource_obj_of(key).metadata.resource_version.get_Some_0(); + forall |msg: MsgType| + #[trigger] s.message_in_flight(msg) + && Self::ok_get_response_msg(key)(msg) + ==> msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.is_Some() + && msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.get_Some_0() < s.kubernetes_api_state.resource_version_counter + } +} + +pub proof fn lemma_always_object_in_ok_get_response_has_lower_rv_than_etcd(spec: TempPred, key: ObjectRef) + requires + spec.entails(lift_state(Self::init())), + spec.entails(always(lift_action(Self::next()))), + ensures + spec.entails(always(lift_state(Self::object_in_ok_get_response_has_lower_rv_than_etcd(key)))), +{ + let inv = Self::object_in_ok_get_response_has_lower_rv_than_etcd(key); + let next = |s, s_prime| { + &&& Self::next()(s, s_prime) + &&& Self::each_object_in_etcd_is_well_formed()(s) + &&& Self::each_object_in_etcd_is_well_formed()(s_prime) + &&& Self::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s) + }; + Self::lemma_always_each_object_in_etcd_is_well_formed(spec); + always_to_always_later(spec, lift_state(Self::each_object_in_etcd_is_well_formed())); + Self::lemma_always_each_object_in_reconcile_has_consistent_key_and_valid_metadata(spec); + combine_spec_entails_always_n!( + spec, lift_action(next), lift_action(Self::next()), + lift_state(Self::each_object_in_etcd_is_well_formed()), + later(lift_state(Self::each_object_in_etcd_is_well_formed())), + lift_state(Self::each_object_in_reconcile_has_consistent_key_and_valid_metadata()) + ); + assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by { + let etcd_rv = s.resource_obj_of(key).metadata.resource_version.get_Some_0(); + assert forall |msg| #[trigger] s_prime.message_in_flight(msg) && Self::ok_get_response_msg(key)(msg) implies + msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.is_Some() + && msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.get_Some_0() < s_prime.kubernetes_api_state.resource_version_counter by { + let step = choose |step| Self::next_step(s, s_prime, step); + if s.message_in_flight(msg) { + assert(s.kubernetes_api_state.resource_version_counter <= s_prime.kubernetes_api_state.resource_version_counter); + } else { + let input = step.get_KubernetesAPIStep_0().get_Some_0(); + assert(s.resource_key_exists(input.content.get_get_request().key)); + assert(input.content.get_get_request().key == key); + assert(msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.get_Some_0() == s.resource_obj_of(key).metadata.resource_version.get_Some_0()); + assert(s.resource_obj_of(key).metadata.resource_version.get_Some_0() < s.kubernetes_api_state.resource_version_counter); + } + } + } + init_invariant(spec, Self::init(), next, inv); +} + +pub open spec fn object_in_ok_get_resp_is_same_as_etcd_with_same_rv(key: ObjectRef) -> StatePred { + |s: Self| { + forall |msg| + #[trigger] s.message_in_flight(msg) + && Self::ok_get_response_msg(key)(msg) + && s.resource_key_exists(key) + && s.resource_obj_of(key).metadata.resource_version.get_Some_0() == msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.get_Some_0() + ==> s.resource_obj_of(key) == msg.content.get_get_response().res.get_Ok_0() + } +} + +pub proof fn lemma_always_object_in_ok_get_resp_is_same_as_etcd_with_same_rv(spec: TempPred, key: ObjectRef) + requires + spec.entails(lift_state(Self::init())), + spec.entails(always(lift_action(Self::next()))), + ensures + spec.entails(always(lift_state(Self::object_in_ok_get_resp_is_same_as_etcd_with_same_rv(key)))), +{ + let inv = Self::object_in_ok_get_resp_is_same_as_etcd_with_same_rv(key); + let next = |s, s_prime| { + &&& Self::next()(s, s_prime) + &&& Self::each_object_in_etcd_is_well_formed()(s) + &&& Self::object_in_ok_get_response_has_lower_rv_than_etcd(key)(s) + }; + Self::lemma_always_each_object_in_etcd_is_well_formed(spec); + Self::lemma_always_object_in_ok_get_response_has_lower_rv_than_etcd(spec, key); + combine_spec_entails_always_n!( + spec, lift_action(next), lift_action(Self::next()), lift_state(Self::each_object_in_etcd_is_well_formed()), + lift_state(Self::object_in_ok_get_response_has_lower_rv_than_etcd(key)) + ); + assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by { + assert forall |msg| #[trigger] s_prime.message_in_flight(msg) && Self::ok_get_response_msg(key)(msg) && s_prime.resource_key_exists(key) + && s_prime.resource_obj_of(key).metadata.resource_version.get_Some_0() == msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.get_Some_0() implies s_prime.resource_obj_of(key) == msg.content.get_get_response().res.get_Ok_0() by { + if s.message_in_flight(msg) { + if !s.resource_key_exists(key) || s.resource_obj_of(key) != s_prime.resource_obj_of(key) { + assert(s_prime.resource_obj_of(key).metadata.resource_version.get_Some_0() != msg.content.get_get_response().res.get_Ok_0().metadata.resource_version.get_Some_0()) + } + } else { + let step = choose |step| Self::next_step(s, s_prime, step); + assert(step.is_KubernetesAPIStep()); + let req = step.get_KubernetesAPIStep_0().get_Some_0(); + assert(msg == Self::handle_get_request(req, s.kubernetes_api_state).1); + assert(s.resource_key_exists(req.content.get_get_request().key)); + assert(msg.content.get_get_response().res.get_Ok_0() == s.resource_obj_of(req.content.get_get_request().key)); + assert(req.content.get_get_request().key == msg.content.get_get_response().res.get_Ok_0().object_ref()); + assert(s.kubernetes_api_state == s_prime.kubernetes_api_state); + assert(s_prime.resource_obj_of(key) == msg.content.get_get_response().res.get_Ok_0()); + } + } + } + init_invariant(spec, Self::init(), next, inv); +} + } }