From fe5bfa33cf8c19982371d003ab2ff3cef6aaaf7c Mon Sep 17 00:00:00 2001 From: Wenjie Ma Date: Sat, 26 Aug 2023 23:51:36 -0500 Subject: [PATCH] Add a lemma about message, rename the transition_rule specs Signed-off-by: Wenjie Ma --- .../rabbitmq_controller/proof/common.rs | 7 + .../proof/helper_invariants/invariants.rs | 88 +----------- .../proof/safety/safety.rs | 10 +- src/kubernetes_cluster/proof/message.rs | 125 +++++++++++++++++- .../proof/validation_rule.rs | 58 ++++---- 5 files changed, 168 insertions(+), 120 deletions(-) diff --git a/src/controller_examples/rabbitmq_controller/proof/common.rs b/src/controller_examples/rabbitmq_controller/proof/common.rs index b45092f96..4f847049f 100644 --- a/src/controller_examples/rabbitmq_controller/proof/common.rs +++ b/src/controller_examples/rabbitmq_controller/proof/common.rs @@ -385,6 +385,13 @@ pub open spec fn sts_update_request_msg(key: ObjectRef) -> FnSpec(RMQMessage) -> && msg.content.get_update_request().obj.kind == Kind::StatefulSetKind } +pub open spec fn sts_get_request_msg(key: ObjectRef) -> FnSpec(RMQMessage) -> bool { + |msg: RMQMessage| + msg.dst.is_KubernetesAPI() + && msg.content.is_get_request() + && msg.content.get_get_request().key == make_stateful_set_key(key) +} + pub open spec fn sts_get_response_msg(key: ObjectRef) -> FnSpec(RMQMessage) -> bool { |msg: RMQMessage| msg.src.is_KubernetesAPI() diff --git a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/invariants.rs b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/invariants.rs index 80257f726..12185f277 100644 --- a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/invariants.rs +++ b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/invariants.rs @@ -1107,7 +1107,7 @@ pub open spec fn response_at_after_get_stateful_set_step_is_sts_get_response(rab |s: RMQCluster| { at_rabbitmq_step(key, RabbitmqReconcileStep::AfterGetStatefulSet)(s) ==> s.reconcile_state_of(key).pending_req_msg.is_Some() - && is_get_stateful_set_request(s.pending_req_of(key).content.get_APIRequest_0(), rabbitmq) + && sts_get_request_msg(key)(s.pending_req_of(key)) && ( forall |msg: RMQMessage| #[trigger] s.message_in_flight(msg) @@ -1128,91 +1128,17 @@ pub proof fn lemma_always_response_at_after_get_stateful_set_step_is_sts_get_res let key = rabbitmq.object_ref(); let next = |s, s_prime| { &&& RMQCluster::next()(s, s_prime) - &&& RMQCluster::each_object_in_etcd_is_well_formed()(s) - &&& RMQCluster::every_in_flight_msg_has_lower_id_than_allocator()(s) - &&& RMQCluster::every_in_flight_or_pending_req_msg_has_unique_id()(s) &&& RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s) + &&& RMQCluster::reference_of_object_in_matched_ok_get_resp_message_is_same_as_key_of_pending_req(key)(s_prime) }; - RMQCluster::lemma_always_each_object_in_etcd_is_well_formed(spec); - RMQCluster::lemma_always_every_in_flight_msg_has_lower_id_than_allocator(spec); - RMQCluster::lemma_always_every_in_flight_or_pending_req_msg_has_unique_id(spec); RMQCluster::lemma_always_each_object_in_reconcile_has_consistent_key_and_valid_metadata(spec); + RMQCluster::lemma_always_reference_of_object_in_matched_ok_get_resp_message_is_same_as_key_of_pending_req(spec, key); + always_to_always_later(spec, lift_state(RMQCluster::reference_of_object_in_matched_ok_get_resp_message_is_same_as_key_of_pending_req(key))); 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(RMQCluster::every_in_flight_msg_has_lower_id_than_allocator()), - lift_state(RMQCluster::every_in_flight_or_pending_req_msg_has_unique_id()), - lift_state(RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()) + spec, lift_action(next), lift_action(RMQCluster::next()), + lift_state(RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()), + later(lift_state(RMQCluster::reference_of_object_in_matched_ok_get_resp_message_is_same_as_key_of_pending_req(key))) ); - assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by { - if at_rabbitmq_step(key, RabbitmqReconcileStep::AfterGetStatefulSet)(s_prime) { - if at_rabbitmq_step(key, RabbitmqReconcileStep::AfterGetStatefulSet)(s) { - assert(s.reconcile_state_of(key) == s_prime.reconcile_state_of(key)); - assert(s_prime.reconcile_state_of(key).pending_req_msg.is_Some()); - assert(is_get_stateful_set_request(s_prime.pending_req_of(key).content.get_APIRequest_0(), rabbitmq)); - } else { - assert(at_rabbitmq_step(key, RabbitmqReconcileStep::AfterCreateRoleBinding)(s)); - assert(s_prime.reconcile_state_of(key).pending_req_msg.is_Some()); - assert(is_get_stateful_set_request(s_prime.pending_req_of(key).content.get_APIRequest_0(), rabbitmq)); - } - assert forall |msg| #[trigger] s_prime.message_in_flight(msg) && Message::resp_msg_matches_req_msg(msg, s_prime.pending_req_of(key)) - implies sts_get_response_msg(key)(msg) by { - let step = choose |step| RMQCluster::next_step(s, s_prime, step); - match step { - Step::ControllerStep(input) => { - assert(s.message_in_flight(msg)); - let cr_key = input.1.get_Some_0(); - if cr_key == key { - assert(s.message_in_flight(msg)); - assert(false); - } else { - assert(s.pending_req_of(key) == s_prime.pending_req_of(key)); - assert(sts_get_response_msg(key)(msg)); - } - }, - Step::KubernetesAPIStep(input) => { - assert(s.reconcile_state_of(key) == s_prime.reconcile_state_of(key)); - if !s.message_in_flight(msg) { - assert(RMQCluster::in_flight_or_pending_req_message(s, s.pending_req_of(key))); - assert(RMQCluster::in_flight_or_pending_req_message(s, input.get_Some_0())); - assert(is_get_stateful_set_request(s_prime.pending_req_of(key).content.get_APIRequest_0(), rabbitmq)); - assert(msg.content.is_get_response()); - assert(msg == RMQCluster::handle_get_request(s.pending_req_of(key), s.kubernetes_api_state).1); - assert(msg.src.is_KubernetesAPI() - && msg.content.is_get_response()); - if msg.content.get_get_response().res.is_Ok() { - assert(s.resource_key_exists(make_stateful_set_key(key))); - assert(s.resource_obj_of(make_stateful_set_key(key)).object_ref() == make_stateful_set_key(key)); - } - assert(sts_get_response_msg(key)(msg)); - } - }, - Step::KubernetesBusy(input) => { - assert(s.reconcile_state_of(key) == s_prime.reconcile_state_of(key)); - if !s.message_in_flight(msg) { - assert(RMQCluster::in_flight_or_pending_req_message(s, s.pending_req_of(key))); - assert(RMQCluster::in_flight_or_pending_req_message(s, input.get_Some_0())); - assert(msg.src.is_KubernetesAPI()); - assert(msg.content.is_get_response()); - assert(msg.content.get_get_response().res.is_Err()); - } - assert(sts_get_response_msg(key)(msg)); - }, - Step::ClientStep() => { - assert(s.message_in_flight(msg)); - assert(sts_get_response_msg(key)(msg)); - }, - Step::ExternalAPIStep(input) => { - assert(input.get_Some_0() != msg); - assert(s.message_in_flight(msg)); - }, - _ => { - assert(s.message_in_flight(msg)); - assert(sts_get_response_msg(key)(msg)); - } - } - } - } - } init_invariant(spec, RMQCluster::init(), next, inv); } diff --git a/src/controller_examples/rabbitmq_controller/proof/safety/safety.rs b/src/controller_examples/rabbitmq_controller/proof/safety/safety.rs index d1fde9e1f..c9bfe8b85 100644 --- a/src/controller_examples/rabbitmq_controller/proof/safety/safety.rs +++ b/src/controller_examples/rabbitmq_controller/proof/safety/safety.rs @@ -402,13 +402,13 @@ proof fn lemma_always_replicas_of_stateful_set_create_or_update_request_msg_sati &&& RMQCluster::each_object_in_etcd_is_well_formed()(s) &&& RMQCluster::each_object_in_etcd_is_well_formed()(s_prime) &&& RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s) - &&& RMQCluster::etcd_and_scheduled_and_triggering_cr_in_correct_order(rabbitmq)(s) + &&& RMQCluster::transition_rule_applies_to_etcd_and_scheduled_and_triggering_cr(rabbitmq)(s) &&& object_in_every_create_or_update_request_msg_only_has_valid_owner_references()(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())); RMQCluster::lemma_always_each_object_in_reconcile_has_consistent_key_and_valid_metadata(spec); - RMQCluster::lemma_always_etcd_and_scheduled_and_triggering_cr_in_correct_order(spec, rabbitmq); + RMQCluster::lemma_always_transition_rule_applies_to_etcd_and_scheduled_and_triggering_cr(spec, rabbitmq); lemma_always_object_in_every_create_or_update_request_msg_only_has_valid_owner_references(spec); combine_spec_entails_always_n!( spec, lift_action(next), @@ -416,7 +416,7 @@ proof fn lemma_always_replicas_of_stateful_set_create_or_update_request_msg_sati lift_state(RMQCluster::each_object_in_etcd_is_well_formed()), later(lift_state(RMQCluster::each_object_in_etcd_is_well_formed())), lift_state(RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()), - lift_state(RMQCluster::etcd_and_scheduled_and_triggering_cr_in_correct_order(rabbitmq)), + lift_state(RMQCluster::transition_rule_applies_to_etcd_and_scheduled_and_triggering_cr(rabbitmq)), lift_state(object_in_every_create_or_update_request_msg_only_has_valid_owner_references()) ); assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by { @@ -442,7 +442,7 @@ proof fn replicas_of_stateful_set_create_request_msg_satisfies_order_induction( RMQCluster::each_object_in_etcd_is_well_formed()(s), RMQCluster::each_object_in_etcd_is_well_formed()(s_prime), RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s), - RMQCluster::etcd_and_scheduled_and_triggering_cr_in_correct_order(rabbitmq)(s), + RMQCluster::transition_rule_applies_to_etcd_and_scheduled_and_triggering_cr(rabbitmq)(s), object_in_every_create_or_update_request_msg_only_has_valid_owner_references()(s), replicas_of_stateful_set_create_or_update_request_msg_satisfies_order(rabbitmq)(s), s_prime.message_in_flight(msg), @@ -502,7 +502,7 @@ proof fn replicas_of_stateful_set_update_request_msg_satisfies_order_induction( RMQCluster::each_object_in_etcd_is_well_formed()(s), RMQCluster::each_object_in_etcd_is_well_formed()(s_prime), RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s), - RMQCluster::etcd_and_scheduled_and_triggering_cr_in_correct_order(rabbitmq)(s), + RMQCluster::transition_rule_applies_to_etcd_and_scheduled_and_triggering_cr(rabbitmq)(s), object_in_every_create_or_update_request_msg_only_has_valid_owner_references()(s), replicas_of_stateful_set_create_or_update_request_msg_satisfies_order(rabbitmq)(s), s_prime.message_in_flight(msg), diff --git a/src/kubernetes_cluster/proof/message.rs b/src/kubernetes_cluster/proof/message.rs index 6c1c12903..6dd230e63 100644 --- a/src/kubernetes_cluster/proof/message.rs +++ b/src/kubernetes_cluster/proof/message.rs @@ -346,7 +346,14 @@ 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 { +pub open spec fn ok_get_response_msg() -> FnSpec(MsgType) -> bool { + |msg: MsgType| + msg.src.is_KubernetesAPI() + && msg.content.is_get_response() + && msg.content.get_get_response().res.is_Ok() +} + +pub open spec fn ok_get_response_msg_with_key(key: ObjectRef) -> FnSpec(MsgType) -> bool { |msg: MsgType| msg.src.is_KubernetesAPI() && msg.content.is_get_response() @@ -359,7 +366,7 @@ pub open spec fn object_in_ok_get_response_has_smaller_rv_than_etcd(key: ObjectR 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) + && Self::ok_get_response_msg_with_key(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 } @@ -390,7 +397,7 @@ pub proof fn lemma_always_object_in_ok_get_response_has_smaller_rv_than_etcd(spe ); 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 + assert forall |msg| #[trigger] s_prime.message_in_flight(msg) && Self::ok_get_response_msg_with_key(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); @@ -412,7 +419,7 @@ pub open spec fn object_in_ok_get_resp_is_same_as_etcd_with_same_rv(key: ObjectR |s: Self| { forall |msg| #[trigger] s.message_in_flight(msg) - && Self::ok_get_response_msg(key)(msg) + && Self::ok_get_response_msg_with_key(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() @@ -439,7 +446,7 @@ pub proof fn lemma_always_object_in_ok_get_resp_is_same_as_etcd_with_same_rv(spe lift_state(Self::object_in_ok_get_response_has_smaller_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) + assert forall |msg| #[trigger] s_prime.message_in_flight(msg) && Self::ok_get_response_msg_with_key(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) { @@ -461,6 +468,114 @@ pub proof fn lemma_always_object_in_ok_get_resp_is_same_as_etcd_with_same_rv(spe init_invariant(spec, Self::init(), next, inv); } +pub open spec fn reference_of_object_in_matched_ok_get_resp_message_is_same_as_key_of_pending_req(key: ObjectRef) -> StatePred + recommends + key.kind.is_CustomResourceKind(), +{ + |s: Self| { + forall |msg: MsgType| + #[trigger] s.message_in_flight(msg) + && Self::ok_get_response_msg()(msg) + && s.reconcile_state_contains(key) + && s.reconcile_state_of(key).pending_req_msg.is_Some() + && Message::resp_msg_matches_req_msg(msg, s.pending_req_of(key)) + ==> Self::ok_get_response_msg_with_key(s.pending_req_of(key).content.get_get_request().key)(msg) + } + +} + +pub proof fn lemma_always_reference_of_object_in_matched_ok_get_resp_message_is_same_as_key_of_pending_req(spec: TempPred, key: ObjectRef) + requires + key.kind.is_CustomResourceKind(), + spec.entails(lift_state(Self::init())), + spec.entails(always(lift_action(Self::next()))), + ensures + spec.entails(always(lift_state(Self::reference_of_object_in_matched_ok_get_resp_message_is_same_as_key_of_pending_req(key)))), +{ + let inv = Self::reference_of_object_in_matched_ok_get_resp_message_is_same_as_key_of_pending_req(key); + let next = |s, s_prime| { + &&& Self::next()(s, s_prime) + &&& Self::each_object_in_etcd_is_well_formed()(s) + &&& Self::every_in_flight_msg_has_lower_id_than_allocator()(s) + &&& Self::every_in_flight_or_pending_req_msg_has_unique_id()(s) + &&& Self::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s) + &&& Self::each_resp_if_matches_pending_req_then_no_other_resp_matches(key)(s) + }; + Self::lemma_always_each_object_in_etcd_is_well_formed(spec); + Self::lemma_always_every_in_flight_msg_has_lower_id_than_allocator(spec); + Self::lemma_always_every_in_flight_or_pending_req_msg_has_unique_id(spec); + Self::lemma_always_each_object_in_reconcile_has_consistent_key_and_valid_metadata(spec); + Self::lemma_always_each_resp_if_matches_pending_req_then_no_other_resp_matches(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::every_in_flight_msg_has_lower_id_than_allocator()), + lift_state(Self::every_in_flight_or_pending_req_msg_has_unique_id()), + lift_state(Self::each_object_in_reconcile_has_consistent_key_and_valid_metadata()), + lift_state(Self::each_resp_if_matches_pending_req_then_no_other_resp_matches(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()(msg) && s_prime.reconcile_state_contains(key) + && s_prime.reconcile_state_of(key).pending_req_msg.is_Some() && Message::resp_msg_matches_req_msg(msg, s_prime.pending_req_of(key)) implies + Self::ok_get_response_msg_with_key(s_prime.pending_req_of(key).content.get_get_request().key)(msg) by { + assert(s_prime.pending_req_of(key).content.is_get_request()); + let req_key = s_prime.pending_req_of(key).content.get_get_request().key; + let step = choose |step| Self::next_step(s, s_prime, step); + match step { + Step::ControllerStep(input) => { + assert(s.message_in_flight(msg)); + let cr_key = input.1.get_Some_0(); + if cr_key == key { + assert(false); + } else { + assert(s.reconcile_state_of(key) == s_prime.reconcile_state_of(key)); + assert(Self::ok_get_response_msg_with_key(req_key)(msg)); + } + }, + Step::KubernetesAPIStep(input) => { + assert(s.reconcile_state_of(key) == s_prime.reconcile_state_of(key)); + if !s.message_in_flight(msg) { + assert(Self::in_flight_or_pending_req_message(s, s.pending_req_of(key))); + assert(Self::in_flight_or_pending_req_message(s, input.get_Some_0())); + assert(msg.content.is_get_response()); + assert(msg == Self::handle_get_request(s.pending_req_of(key), s.kubernetes_api_state).1); + assert(msg.src.is_KubernetesAPI() + && msg.content.is_get_response()); + if msg.content.get_get_response().res.is_Ok() { + assert(s.resource_key_exists(req_key)); + assert(s.resource_obj_of(req_key).object_ref() == req_key); + } + assert(Self::ok_get_response_msg_with_key(req_key)(msg)); + } + }, + Step::KubernetesBusy(input) => { + assert(s.reconcile_state_of(key) == s_prime.reconcile_state_of(key)); + if !s.message_in_flight(msg) { + assert(Self::in_flight_or_pending_req_message(s, s.pending_req_of(key))); + assert(Self::in_flight_or_pending_req_message(s, input.get_Some_0())); + assert(msg.src.is_KubernetesAPI()); + assert(msg.content.is_get_response()); + assert(msg.content.get_get_response().res.is_Err()); + } + assert(Self::ok_get_response_msg_with_key(req_key)(msg)); + }, + Step::ClientStep() => { + assert(s.message_in_flight(msg)); + assert(Self::ok_get_response_msg_with_key(req_key)(msg)); + }, + Step::ExternalAPIStep(input) => { + assert(input.get_Some_0() != msg); + assert(s.message_in_flight(msg)); + }, + _ => { + assert(s.message_in_flight(msg)); + assert(Self::ok_get_response_msg_with_key(req_key)(msg)); + } + } + } + } + init_invariant(spec, Self::init(), next, inv); +} + } } diff --git a/src/kubernetes_cluster/proof/validation_rule.rs b/src/kubernetes_cluster/proof/validation_rule.rs index 75608c7d8..e02033a4e 100644 --- a/src/kubernetes_cluster/proof/validation_rule.rs +++ b/src/kubernetes_cluster/proof/validation_rule.rs @@ -35,17 +35,17 @@ pub open spec fn is_reflexive_and_transitive() -> bool { /// This spec and also this module are targeted at the relations of the three versions of custom resource object. We know that /// if cr is updated, the old and new object are subject to the transition rule (if any). Since scheduled_cr and triggering_cr /// are derived from the cr in etcd, they are either equal to or satisfy the transition rule with etcd cr. -/// +/// /// When the transition rule is transitive, we can determine a linear order of the three custom resource objects. -pub open spec fn etcd_and_scheduled_and_triggering_cr_in_correct_order(cr: K) -> StatePred { +pub open spec fn transition_rule_applies_to_etcd_and_scheduled_and_triggering_cr(cr: K) -> StatePred { |s: Self| { - Self::scheduled_cr_is_in_correct_order_with_etcd_cr(cr)(s) - && Self::triggering_cr_is_in_correct_order_with_scheduled_cr(cr)(s) - && Self::triggering_cr_is_in_correct_order_with_etcd_cr(cr)(s) + Self::transition_rule_applies_to_etcd_and_scheduled_cr(cr)(s) + && Self::transition_rule_applies_to_scheduled_and_triggering_cr(cr)(s) + && Self::transition_rule_applies_to_etcd_and_triggering_cr(cr)(s) } } -pub proof fn lemma_always_etcd_and_scheduled_and_triggering_cr_in_correct_order(spec: TempPred, cr: K) +pub proof fn lemma_always_transition_rule_applies_to_etcd_and_scheduled_and_triggering_cr(spec: TempPred, cr: K) requires K::kind() == Kind::CustomResourceKind, Self::from_dynamic_preserves_spec(), @@ -53,19 +53,19 @@ pub proof fn lemma_always_etcd_and_scheduled_and_triggering_cr_in_correct_order( spec.entails(lift_state(Self::init())), spec.entails(always(lift_action(Self::next()))), ensures - spec.entails(always(lift_state(Self::etcd_and_scheduled_and_triggering_cr_in_correct_order(cr)))), + spec.entails(always(lift_state(Self::transition_rule_applies_to_etcd_and_scheduled_and_triggering_cr(cr)))), { - Self::lemma_always_scheduled_cr_is_in_correct_order_with_etcd_cr(spec, cr); + Self::lemma_always_transition_rule_applies_to_etcd_and_scheduled_cr(spec, cr); Self::lemma_always_triggering_cr_is_in_correct_order(spec, cr); combine_spec_entails_always_n!( - spec, lift_state(Self::etcd_and_scheduled_and_triggering_cr_in_correct_order(cr)), - lift_state(Self::scheduled_cr_is_in_correct_order_with_etcd_cr(cr)), - lift_state(Self::triggering_cr_is_in_correct_order_with_scheduled_cr(cr)), - lift_state(Self::triggering_cr_is_in_correct_order_with_etcd_cr(cr)) + spec, lift_state(Self::transition_rule_applies_to_etcd_and_scheduled_and_triggering_cr(cr)), + lift_state(Self::transition_rule_applies_to_etcd_and_scheduled_cr(cr)), + lift_state(Self::transition_rule_applies_to_scheduled_and_triggering_cr(cr)), + lift_state(Self::transition_rule_applies_to_etcd_and_triggering_cr(cr)) ); } -pub open spec fn scheduled_cr_is_in_correct_order_with_etcd_cr(cr: K) -> StatePred { +pub open spec fn transition_rule_applies_to_etcd_and_scheduled_cr(cr: K) -> StatePred { |s: Self| { let key = cr.object_ref(); s.reconcile_scheduled_for(key) @@ -75,7 +75,7 @@ pub open spec fn scheduled_cr_is_in_correct_order_with_etcd_cr(cr: K) -> StatePr } } -proof fn lemma_always_scheduled_cr_is_in_correct_order_with_etcd_cr(spec: TempPred, cr: K) +proof fn lemma_always_transition_rule_applies_to_etcd_and_scheduled_cr(spec: TempPred, cr: K) requires K::kind() == Kind::CustomResourceKind, Self::is_reflexive_and_transitive(), @@ -83,9 +83,9 @@ proof fn lemma_always_scheduled_cr_is_in_correct_order_with_etcd_cr(spec: TempPr spec.entails(lift_state(Self::init())), spec.entails(always(lift_action(Self::next()))), ensures - spec.entails(always(lift_state(Self::scheduled_cr_is_in_correct_order_with_etcd_cr(cr)))), + spec.entails(always(lift_state(Self::transition_rule_applies_to_etcd_and_scheduled_cr(cr)))), { - let inv = Self::scheduled_cr_is_in_correct_order_with_etcd_cr(cr); + let inv = Self::transition_rule_applies_to_etcd_and_scheduled_cr(cr); let next = |s, s_prime| { &&& Self::next()(s, s_prime) &&& Self::each_object_in_etcd_is_well_formed()(s) @@ -143,7 +143,7 @@ proof fn lemma_always_scheduled_cr_is_in_correct_order_with_etcd_cr(spec: TempPr init_invariant(spec, Self::init(), next, inv); } -pub open spec fn triggering_cr_is_in_correct_order_with_etcd_cr(cr: K) -> StatePred { +pub open spec fn transition_rule_applies_to_etcd_and_triggering_cr(cr: K) -> StatePred { |s: Self| { let key = cr.object_ref(); s.reconcile_state_contains(key) @@ -153,7 +153,7 @@ pub open spec fn triggering_cr_is_in_correct_order_with_etcd_cr(cr: K) -> StateP } } -pub open spec fn triggering_cr_is_in_correct_order_with_scheduled_cr(cr: K) -> StatePred { +pub open spec fn transition_rule_applies_to_scheduled_and_triggering_cr(cr: K) -> StatePred { |s: Self| { let key = cr.object_ref(); s.reconcile_state_contains(key) @@ -171,30 +171,30 @@ proof fn lemma_always_triggering_cr_is_in_correct_order(spec: TempPred, cr spec.entails(lift_state(Self::init())), spec.entails(always(lift_action(Self::next()))), ensures - spec.entails(always(lift_state(Self::triggering_cr_is_in_correct_order_with_etcd_cr(cr)))), - spec.entails(always(lift_state(Self::triggering_cr_is_in_correct_order_with_scheduled_cr(cr)))), + spec.entails(always(lift_state(Self::transition_rule_applies_to_etcd_and_triggering_cr(cr)))), + spec.entails(always(lift_state(Self::transition_rule_applies_to_scheduled_and_triggering_cr(cr)))), { let inv = |s: Self| { - &&& Self::triggering_cr_is_in_correct_order_with_etcd_cr(cr)(s) - &&& Self::triggering_cr_is_in_correct_order_with_scheduled_cr(cr)(s) + &&& Self::transition_rule_applies_to_etcd_and_triggering_cr(cr)(s) + &&& Self::transition_rule_applies_to_scheduled_and_triggering_cr(cr)(s) }; 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::triggering_cr_has_lower_uid_than_uid_counter()(s) - &&& Self::scheduled_cr_is_in_correct_order_with_etcd_cr(cr)(s) + &&& Self::transition_rule_applies_to_etcd_and_scheduled_cr(cr)(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_triggering_cr_has_lower_uid_than_uid_counter(spec); - Self::lemma_always_scheduled_cr_is_in_correct_order_with_etcd_cr(spec, cr); + Self::lemma_always_transition_rule_applies_to_etcd_and_scheduled_cr(spec, cr); 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::triggering_cr_has_lower_uid_than_uid_counter()), - lift_state(Self::scheduled_cr_is_in_correct_order_with_etcd_cr(cr)) + lift_state(Self::transition_rule_applies_to_etcd_and_scheduled_cr(cr)) ); assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by { let key = cr.object_ref(); @@ -245,17 +245,17 @@ proof fn lemma_always_triggering_cr_is_in_correct_order(spec: TempPred, cr assert(K::transition_rule(s_prime.reconcile_scheduled_obj_of(key), K::from_dynamic_object(s.resource_obj_of(key)).get_Ok_0())); assert(K::transition_rule(K::from_dynamic_object(s.resource_obj_of(key)).get_Ok_0(), s.triggering_cr_of(key))); } - assert(Self::triggering_cr_is_in_correct_order_with_scheduled_cr(cr)(s_prime)); + assert(Self::transition_rule_applies_to_scheduled_and_triggering_cr(cr)(s_prime)); }, _ => { - assert(Self::triggering_cr_is_in_correct_order_with_scheduled_cr(cr)(s_prime)); + assert(Self::transition_rule_applies_to_scheduled_and_triggering_cr(cr)(s_prime)); } } } } init_invariant(spec, Self::init(), next, inv); - always_weaken(spec, inv, Self::triggering_cr_is_in_correct_order_with_etcd_cr(cr)); - always_weaken(spec, inv, Self::triggering_cr_is_in_correct_order_with_scheduled_cr(cr)); + always_weaken(spec, inv, Self::transition_rule_applies_to_etcd_and_triggering_cr(cr)); + always_weaken(spec, inv, Self::transition_rule_applies_to_scheduled_and_triggering_cr(cr)); } }