From f8d89c9d4cd4c24c23806992693e705f190908c7 Mon Sep 17 00:00:00 2001 From: Wenjie Ma Date: Thu, 24 Aug 2023 23:23:13 -0500 Subject: [PATCH] Rebase main and fix some subsequent issues Add generics to the Message Type. --------- Signed-off-by: Wenjie Ma --- .../rabbitmq_controller/proof/common.rs | 30 ++++---- .../liveness/helper_invariants/invariants.rs | 72 +++++++++---------- .../proof/liveness/liveness.rs | 28 ++++---- .../rabbitmq_controller/proof/safety.rs | 37 ++++++---- .../simple_controller/proof/liveness.rs | 52 +++++++------- .../simple_controller/proof/safety.rs | 2 +- .../simple_controller/proof/shared.rs | 26 +++---- .../zookeeper_controller/proof/common.rs | 10 +-- .../proof/liveness/helper_invariants.rs | 20 +++--- .../proof/liveness/liveness_property.rs | 10 +-- .../proof/safety/deletion_safety.rs | 4 +- .../proof/builtin_controllers.rs | 10 +-- src/kubernetes_cluster/proof/cluster.rs | 6 +- .../proof/controller_runtime.rs | 10 +-- .../proof/controller_runtime_liveness.rs | 14 ++-- .../proof/controller_runtime_safety.rs | 28 ++++---- .../proof/kubernetes_api_liveness.rs | 40 +++++------ src/kubernetes_cluster/proof/message.rs | 55 +++++++------- src/kubernetes_cluster/proof/wf1_assistant.rs | 4 +- src/kubernetes_cluster/spec/cluster.rs | 4 +- .../spec/cluster_state_machine.rs | 52 +++++++------- .../spec/controller/common.rs | 6 +- .../spec/external_api/types.rs | 4 +- .../spec/kubernetes_api/state_machine.rs | 16 ++--- src/kubernetes_cluster/spec/message.rs | 2 + .../spec/network/state_machine.rs | 2 +- 26 files changed, 276 insertions(+), 268 deletions(-) diff --git a/src/controller_examples/rabbitmq_controller/proof/common.rs b/src/controller_examples/rabbitmq_controller/proof/common.rs index 2d443bc6b..d9d2352fd 100644 --- a/src/controller_examples/rabbitmq_controller/proof/common.rs +++ b/src/controller_examples/rabbitmq_controller/proof/common.rs @@ -19,10 +19,12 @@ use vstd::prelude::*; verus! { -pub type RMQStep = Step; +pub type RMQStep = Step; pub type RMQCluster = Cluster; +pub type RMQMessage = Message; + pub open spec fn cluster_spec() -> TempPred { RMQCluster::sm_spec() } @@ -81,7 +83,7 @@ pub open spec fn pending_req_with_object_in_flight_at_rabbitmq_step_with_rabbitm } pub open spec fn req_msg_is_the_in_flight_pending_req_at_rabbitmq_step_with_rabbitmq( - step: RabbitmqReconcileStep, rabbitmq: RabbitmqClusterView, req_msg: Message + step: RabbitmqReconcileStep, rabbitmq: RabbitmqClusterView, req_msg: RMQMessage ) -> StatePred { |s: RMQCluster| { &&& at_rabbitmq_step_with_rabbitmq(rabbitmq, step)(s) @@ -92,7 +94,7 @@ pub open spec fn req_msg_is_the_in_flight_pending_req_at_rabbitmq_step_with_rabb } pub open spec fn req_msg_is_the_in_flight_pending_req_with_object_at_rabbitmq_step_with_rabbitmq( - step: RabbitmqReconcileStep, rabbitmq: RabbitmqClusterView, req_msg: Message, object: DynamicObjectView + step: RabbitmqReconcileStep, rabbitmq: RabbitmqClusterView, req_msg: RMQMessage, object: DynamicObjectView ) -> StatePred { |s: RMQCluster| { &&& at_rabbitmq_step_with_rabbitmq(rabbitmq, step)(s) @@ -117,7 +119,7 @@ pub open spec fn exists_resp_in_flight_at_rabbitmq_step_with_rabbitmq( } pub open spec fn resp_msg_is_the_in_flight_resp_at_rabbitmq_step_with_rabbitmq( - step: RabbitmqReconcileStep, rabbitmq: RabbitmqClusterView, resp_msg: Message + step: RabbitmqReconcileStep, rabbitmq: RabbitmqClusterView, resp_msg: RMQMessage ) -> StatePred { |s: RMQCluster| { &&& at_rabbitmq_step_with_rabbitmq(rabbitmq, step)(s) @@ -129,7 +131,7 @@ pub open spec fn resp_msg_is_the_in_flight_resp_at_rabbitmq_step_with_rabbitmq( } pub open spec fn is_correct_pending_request_msg_at_rabbitmq_step( - step: RabbitmqReconcileStep, msg: Message, rabbitmq: RabbitmqClusterView + step: RabbitmqReconcileStep, msg: RMQMessage, rabbitmq: RabbitmqClusterView ) -> bool { &&& msg.src == HostId::CustomController &&& msg.dst == HostId::KubernetesAPI @@ -160,7 +162,7 @@ pub open spec fn is_correct_pending_request_at_rabbitmq_step( } pub open spec fn is_correct_pending_request_msg_with_object_at_rabbitmq_step( - step: RabbitmqReconcileStep, msg: Message, rabbitmq: RabbitmqClusterView, object: DynamicObjectView + step: RabbitmqReconcileStep, msg: RMQMessage, rabbitmq: RabbitmqClusterView, object: DynamicObjectView ) -> bool { &&& msg.src == HostId::CustomController &&& msg.dst == HostId::KubernetesAPI @@ -366,8 +368,8 @@ pub open spec fn at_after_get_server_config_map_step_with_rabbitmq_and_exists_no } } -pub open spec fn sts_create_request_msg(key: ObjectRef) -> FnSpec(Message) -> bool { - |msg: Message| +pub open spec fn sts_create_request_msg(key: ObjectRef) -> FnSpec(RMQMessage) -> bool { + |msg: RMQMessage| msg.dst.is_KubernetesAPI() && msg.content.is_create_request() && msg.content.get_create_request().namespace == make_stateful_set_key(key).namespace @@ -375,15 +377,15 @@ pub open spec fn sts_create_request_msg(key: ObjectRef) -> FnSpec(Message) -> bo && msg.content.get_create_request().obj.kind == make_stateful_set_key(key).kind } -pub open spec fn sts_update_request_msg(key: ObjectRef) -> FnSpec(Message) -> bool { - |msg: Message| +pub open spec fn sts_update_request_msg(key: ObjectRef) -> FnSpec(RMQMessage) -> bool { + |msg: RMQMessage| msg.dst.is_KubernetesAPI() && msg.content.is_update_request() && msg.content.get_update_request().key == make_stateful_set_key(key) } -pub open spec fn sts_get_response_msg(key: ObjectRef) -> FnSpec(Message) -> bool { - |msg: Message| +pub open spec fn sts_get_response_msg(key: ObjectRef) -> FnSpec(RMQMessage) -> bool { + |msg: RMQMessage| msg.src.is_KubernetesAPI() && msg.content.is_get_response() && ( @@ -392,8 +394,8 @@ pub open spec fn sts_get_response_msg(key: ObjectRef) -> FnSpec(Message) -> bool ) } -pub open spec fn ok_sts_get_response_msg(key: ObjectRef) -> FnSpec(Message) -> bool { - |msg: Message| +pub open spec fn ok_sts_get_response_msg(key: ObjectRef) -> FnSpec(RMQMessage) -> bool { + |msg: RMQMessage| msg.src.is_KubernetesAPI() && msg.content.is_get_response() && msg.content.get_get_response().res.is_Ok() diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness/helper_invariants/invariants.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/helper_invariants/invariants.rs index d8f684560..886d12562 100644 --- a/src/controller_examples/rabbitmq_controller/proof/liveness/helper_invariants/invariants.rs +++ b/src/controller_examples/rabbitmq_controller/proof/liveness/helper_invariants/invariants.rs @@ -28,8 +28,8 @@ verus! { // And use this assumption to write lemmas that are independent of controllers, then further decouple specific controller // from the proof logic. -pub open spec fn server_config_map_create_request_msg(key: ObjectRef) -> FnSpec(Message) -> bool { - |msg: Message| +pub open spec fn server_config_map_create_request_msg(key: ObjectRef) -> FnSpec(RMQMessage) -> bool { + |msg: RMQMessage| msg.dst.is_KubernetesAPI() && msg.content.is_create_request() && msg.content.get_create_request().namespace == make_server_config_map_key(key).namespace @@ -37,8 +37,8 @@ pub open spec fn server_config_map_create_request_msg(key: ObjectRef) -> FnSpec( && msg.content.get_create_request().obj.kind == make_server_config_map_key(key).kind } -pub open spec fn server_config_map_update_request_msg(key: ObjectRef) -> FnSpec(Message) -> bool { - |msg: Message| +pub open spec fn server_config_map_update_request_msg(key: ObjectRef) -> FnSpec(RMQMessage) -> bool { + |msg: RMQMessage| msg.dst.is_KubernetesAPI() && msg.content.is_update_request() && msg.content.get_update_request().key == make_server_config_map_key(key) @@ -56,7 +56,7 @@ spec fn make_owner_references_with_name_and_uid(name: StringView, uid: nat) -> O spec fn server_config_map_create_request_msg_is_valid(key: ObjectRef) -> StatePred { |s: RMQCluster| { - forall |msg: Message| { + forall |msg: RMQMessage| { #[trigger] s.message_in_flight(msg) && server_config_map_create_request_msg(key)(msg) ==> msg.content.get_create_request().obj.metadata.finalizers.is_None() @@ -73,7 +73,7 @@ spec fn server_config_map_create_request_msg_is_valid(key: ObjectRef) -> StatePr /// /// After the action, the controller stays at AfterCreateServerConfigMap step. proof fn lemma_server_config_map_create_request_msg_implies_key_in_reconcile_equals( - key: ObjectRef, s: RMQCluster, s_prime: RMQCluster, msg: Message, step: RMQStep + key: ObjectRef, s: RMQCluster, s_prime: RMQCluster, msg: RMQMessage, step: RMQStep ) requires key.kind.is_CustomResourceKind(), @@ -117,7 +117,7 @@ proof fn lemma_server_config_map_create_request_msg_implies_key_in_reconcile_equ /// /// After the action, the controller stays at AfterUpdateServerConfigMap step. proof fn lemma_server_config_map_update_request_msg_implies_key_in_reconcile_equals( - key: ObjectRef, s: RMQCluster, s_prime: RMQCluster, msg: Message, step: RMQStep + key: ObjectRef, s: RMQCluster, s_prime: RMQCluster, msg: RMQMessage, step: RMQStep ) requires key.kind.is_CustomResourceKind(), @@ -139,7 +139,7 @@ proof fn lemma_server_config_map_update_request_msg_implies_key_in_reconcile_equ /// /// After the action, the controller stays at AfterCreateStatefulSet step. pub proof fn lemma_stateful_set_create_request_msg_implies_key_in_reconcile_equals( - key: ObjectRef, s: RMQCluster, s_prime: RMQCluster, msg: Message, step: RMQStep + key: ObjectRef, s: RMQCluster, s_prime: RMQCluster, msg: RMQMessage, step: RMQStep ) requires key.kind.is_CustomResourceKind(), @@ -161,7 +161,7 @@ pub proof fn lemma_stateful_set_create_request_msg_implies_key_in_reconcile_equa /// /// After the action, the controller stays at AfterUpdateStatefulSet step. pub proof fn lemma_stateful_set_update_request_msg_implies_key_in_reconcile_equals( - key: ObjectRef, s: RMQCluster, s_prime: RMQCluster, msg: Message, step: RMQStep + key: ObjectRef, s: RMQCluster, s_prime: RMQCluster, msg: RMQMessage, step: RMQStep ) requires key.kind.is_CustomResourceKind(), @@ -219,7 +219,7 @@ proof fn lemma_always_server_config_map_create_request_msg_is_valid(spec: TempPr spec fn server_config_map_update_request_msg_is_valid(key: ObjectRef) -> StatePred { |s: RMQCluster| { - forall |msg: Message| { + forall |msg: RMQMessage| { #[trigger] s.message_in_flight(msg) && server_config_map_update_request_msg(key)(msg) ==> msg.content.get_update_request().obj.metadata.finalizers.is_None() @@ -270,7 +270,7 @@ proof fn lemma_always_server_config_map_update_request_msg_is_valid(spec: TempPr spec fn sts_update_request_msg_is_valid(key: ObjectRef) -> StatePred { |s: RMQCluster| { - forall |msg: Message| { + forall |msg: RMQMessage| { #[trigger] s.message_in_flight(msg) && sts_update_request_msg(key)(msg) ==> msg.content.get_update_request().obj.metadata.finalizers.is_None() @@ -321,7 +321,7 @@ proof fn lemma_always_sts_update_request_msg_is_valid(spec: TempPred spec fn sts_create_request_msg_is_valid(key: ObjectRef) -> StatePred { |s: RMQCluster| { - forall |msg: Message| { + forall |msg: RMQMessage| { #[trigger] s.message_in_flight(msg) && sts_create_request_msg(key)(msg) ==> msg.content.get_create_request().obj.metadata.finalizers.is_None() @@ -401,7 +401,7 @@ pub proof fn lemma_true_leads_to_always_create_server_cm_req_msg_in_flight_impli true_pred().leads_to(always(lift_state(create_server_cm_req_msg_in_flight_implies_at_after_create_server_cm_step(key)))) ), { - let requirements = |msg: Message, s: RMQCluster| { + let requirements = |msg: RMQMessage, s: RMQCluster| { server_config_map_create_request_msg(key)(msg) ==> { &&& at_rabbitmq_step(key, RabbitmqReconcileStep::AfterCreateServerConfigMap)(s) @@ -418,7 +418,7 @@ pub proof fn lemma_true_leads_to_always_create_server_cm_req_msg_in_flight_impli }; assert forall |s, s_prime| #[trigger] stronger_next(s, s_prime) implies RMQCluster::every_new_req_msg_if_in_flight_then_satisfies(requirements)(s, s_prime) by { - assert forall |msg: Message| (!s.message_in_flight(msg) || requirements(msg, s)) && #[trigger] s_prime.message_in_flight(msg) + assert forall |msg: RMQMessage| (!s.message_in_flight(msg) || requirements(msg, s)) && #[trigger] s_prime.message_in_flight(msg) implies requirements(msg, s_prime) by { if server_config_map_create_request_msg(key)(msg) { let pending_req = s_prime.pending_req_of(key); @@ -475,7 +475,7 @@ pub proof fn lemma_true_leads_to_always_update_server_cm_req_msg_in_flight_impli true_pred().leads_to(always(lift_state(update_server_cm_req_msg_in_flight_implies_at_after_update_server_cm_step(key)))) ), { - let requirements = |msg: Message, s: RMQCluster| { + let requirements = |msg: RMQMessage, s: RMQCluster| { server_config_map_update_request_msg(key)(msg) ==> { &&& at_rabbitmq_step(key, RabbitmqReconcileStep::AfterUpdateServerConfigMap)(s) @@ -524,7 +524,7 @@ pub open spec fn every_update_server_cm_req_does_the_same(rabbitmq: RabbitmqClus rabbitmq.well_formed(), { |s: RMQCluster| { - forall |msg: Message| { + forall |msg: RMQMessage| { &&& #[trigger] s.network_state.in_flight.contains(msg) &&& server_config_map_update_request_msg(rabbitmq.object_ref())(msg) } ==> msg.content.get_update_request().obj.spec == ConfigMapView::marshal_spec((make_server_config_map(rabbitmq).data, ())) @@ -609,7 +609,7 @@ pub proof fn lemma_true_leads_to_always_every_update_server_cm_req_does_the_same true_pred().leads_to(always(lift_state(every_update_server_cm_req_does_the_same(rabbitmq)))) ), { - let requirements = |msg: Message, s: RMQCluster| { + let requirements = |msg: RMQMessage, s: RMQCluster| { server_config_map_update_request_msg(rabbitmq.object_ref())(msg) ==> msg.content.get_update_request().obj.spec == ConfigMapView::marshal_spec((make_server_config_map(rabbitmq).data, ())) && msg.content.get_update_request().obj.metadata.owner_references == Some(seq![rabbitmq.controller_owner_ref()]) @@ -620,7 +620,7 @@ pub proof fn lemma_true_leads_to_always_every_update_server_cm_req_does_the_same &&& RMQCluster::the_object_in_reconcile_has_spec_and_uid_as(rabbitmq)(s) }; assert forall |s, s_prime| #[trigger] stronger_next(s, s_prime) implies RMQCluster::every_new_req_msg_if_in_flight_then_satisfies(requirements)(s, s_prime) by { - assert forall |msg: Message| (!s.message_in_flight(msg) || requirements(msg, s)) && #[trigger] s_prime.message_in_flight(msg) + assert forall |msg: RMQMessage| (!s.message_in_flight(msg) || requirements(msg, s)) && #[trigger] s_prime.message_in_flight(msg) && msg.dst.is_KubernetesAPI() && msg.content.is_APIRequest() implies requirements(msg, s_prime) by { if !s.message_in_flight(msg) && server_config_map_update_request_msg(rabbitmq.object_ref())(msg) { let step = choose |step| RMQCluster::next_step(s, s_prime, step); @@ -656,7 +656,7 @@ pub proof fn lemma_true_leads_to_always_no_delete_cm_req_is_in_flight(spec: Temp ), { let key = rabbitmq.object_ref(); - let requirements = |msg: Message, s: RMQCluster| !{ + let requirements = |msg: RMQMessage, s: RMQCluster| !{ &&& msg.dst.is_KubernetesAPI() &&& msg.content.is_delete_request() &&& msg.content.get_delete_request().key == make_server_config_map_key(rabbitmq.object_ref()) @@ -669,7 +669,7 @@ pub proof fn lemma_true_leads_to_always_no_delete_cm_req_is_in_flight(spec: Temp &&& RMQCluster::each_object_in_etcd_is_well_formed()(s) }; assert forall |s: RMQCluster, s_prime: RMQCluster| #[trigger] stronger_next(s, s_prime) implies RMQCluster::every_new_req_msg_if_in_flight_then_satisfies(requirements)(s, s_prime) by { - assert forall |msg: Message| (!s.message_in_flight(msg) || requirements(msg, s)) && #[trigger] s_prime.message_in_flight(msg) + assert forall |msg: RMQMessage| (!s.message_in_flight(msg) || requirements(msg, s)) && #[trigger] s_prime.message_in_flight(msg) implies requirements(msg, s_prime) by { if s.resource_key_exists(make_server_config_map_key(key)) { let owner_refs = s.resource_obj_of(make_server_config_map_key(key)).metadata.owner_references; @@ -697,7 +697,7 @@ pub open spec fn every_update_sts_req_does_the_same(rabbitmq: RabbitmqClusterVie rabbitmq.well_formed(), { |s: RMQCluster| { - forall |msg: Message| { + forall |msg: RMQMessage| { &&& #[trigger] s.network_state.in_flight.contains(msg) &&& sts_update_request_msg(rabbitmq.object_ref())(msg) } ==> msg.content.get_update_request().obj.spec == StatefulSetView::marshal_spec(make_stateful_set(rabbitmq).spec) @@ -718,7 +718,7 @@ pub proof fn lemma_true_leads_to_always_every_update_sts_req_does_the_same(spec: true_pred().leads_to(always(lift_state(every_update_sts_req_does_the_same(rabbitmq)))) ), { - let requirements = |msg: Message, s: RMQCluster| { + let requirements = |msg: RMQMessage, s: RMQCluster| { sts_update_request_msg(rabbitmq.object_ref())(msg) ==> msg.content.get_update_request().obj.spec == StatefulSetView::marshal_spec(make_stateful_set(rabbitmq).spec) && msg.content.get_update_request().obj.metadata.owner_references == Some(seq![rabbitmq.controller_owner_ref()]) @@ -729,7 +729,7 @@ pub proof fn lemma_true_leads_to_always_every_update_sts_req_does_the_same(spec: &&& RMQCluster::the_object_in_reconcile_has_spec_and_uid_as(rabbitmq)(s) }; assert forall |s, s_prime| #[trigger] stronger_next(s, s_prime) implies RMQCluster::every_new_req_msg_if_in_flight_then_satisfies(requirements)(s, s_prime) by { - assert forall |msg: Message| (!s.message_in_flight(msg) || requirements(msg, s)) && #[trigger] s_prime.message_in_flight(msg) + assert forall |msg: RMQMessage| (!s.message_in_flight(msg) || requirements(msg, s)) && #[trigger] s_prime.message_in_flight(msg) && msg.dst.is_KubernetesAPI() && msg.content.is_APIRequest() implies requirements(msg, s_prime) by { if !s.message_in_flight(msg) && sts_update_request_msg(rabbitmq.object_ref())(msg) { let step = choose |step| RMQCluster::next_step(s, s_prime, step); @@ -754,7 +754,7 @@ pub open spec fn every_create_sts_req_does_the_same(rabbitmq: RabbitmqClusterVie rabbitmq.well_formed(), { |s: RMQCluster| { - forall |msg: Message| { + forall |msg: RMQMessage| { &&& #[trigger] s.network_state.in_flight.contains(msg) &&& sts_create_request_msg(rabbitmq.object_ref())(msg) } ==> msg.content.get_create_request().obj.spec == StatefulSetView::marshal_spec(make_stateful_set(rabbitmq).spec) @@ -775,7 +775,7 @@ pub proof fn lemma_true_leads_to_always_every_create_sts_req_does_the_same(spec: true_pred().leads_to(always(lift_state(every_create_sts_req_does_the_same(rabbitmq)))) ), { - let requirements = |msg: Message, s: RMQCluster| { + let requirements = |msg: RMQMessage, s: RMQCluster| { sts_create_request_msg(rabbitmq.object_ref())(msg) ==> msg.content.get_create_request().obj.spec == StatefulSetView::marshal_spec(make_stateful_set(rabbitmq).spec) && msg.content.get_create_request().obj.metadata.owner_references == Some(seq![rabbitmq.controller_owner_ref()]) @@ -786,7 +786,7 @@ pub proof fn lemma_true_leads_to_always_every_create_sts_req_does_the_same(spec: &&& RMQCluster::the_object_in_reconcile_has_spec_and_uid_as(rabbitmq)(s) }; assert forall |s, s_prime| #[trigger] stronger_next(s, s_prime) implies RMQCluster::every_new_req_msg_if_in_flight_then_satisfies(requirements)(s, s_prime) by { - assert forall |msg: Message| (!s.message_in_flight(msg) || requirements(msg, s)) && #[trigger] s_prime.message_in_flight(msg) + assert forall |msg: RMQMessage| (!s.message_in_flight(msg) || requirements(msg, s)) && #[trigger] s_prime.message_in_flight(msg) && msg.dst.is_KubernetesAPI() && msg.content.is_APIRequest() implies requirements(msg, s_prime) by { if !s.message_in_flight(msg) && sts_create_request_msg(rabbitmq.object_ref())(msg) { let step = choose |step| RMQCluster::next_step(s, s_prime, step); @@ -811,7 +811,7 @@ pub open spec fn every_create_server_cm_req_does_the_same(rabbitmq: RabbitmqClus rabbitmq.well_formed(), { |s: RMQCluster| { - forall |msg: Message| { + forall |msg: RMQMessage| { &&& #[trigger] s.network_state.in_flight.contains(msg) &&& server_config_map_create_request_msg(rabbitmq.object_ref())(msg) } ==> msg.content.get_create_request().obj.spec == ConfigMapView::marshal_spec((make_server_config_map(rabbitmq).data, ())) @@ -833,7 +833,7 @@ pub proof fn lemma_true_leads_to_always_every_create_server_cm_req_does_the_same true_pred().leads_to(always(lift_state(every_create_server_cm_req_does_the_same(rabbitmq)))) ), { - let requirements = |msg: Message, s: RMQCluster| { + let requirements = |msg: RMQMessage, s: RMQCluster| { server_config_map_create_request_msg(rabbitmq.object_ref())(msg) ==> msg.content.get_create_request().obj.spec == ConfigMapView::marshal_spec((make_server_config_map(rabbitmq).data, ())) && && msg.content.get_create_request().obj.metadata.owner_references == Some(seq![rabbitmq.controller_owner_ref()]) @@ -844,7 +844,7 @@ pub proof fn lemma_true_leads_to_always_every_create_server_cm_req_does_the_same &&& RMQCluster::the_object_in_reconcile_has_spec_and_uid_as(rabbitmq)(s) }; assert forall |s, s_prime| #[trigger] stronger_next(s, s_prime) implies RMQCluster::every_new_req_msg_if_in_flight_then_satisfies(requirements)(s, s_prime) by { - assert forall |msg: Message| (!s.message_in_flight(msg) || requirements(msg, s)) && #[trigger] s_prime.message_in_flight(msg) + assert forall |msg: RMQMessage| (!s.message_in_flight(msg) || requirements(msg, s)) && #[trigger] s_prime.message_in_flight(msg) && msg.dst.is_KubernetesAPI() && msg.content.is_APIRequest() implies requirements(msg, s_prime) by { if !s.message_in_flight(msg) && server_config_map_create_request_msg(rabbitmq.object_ref())(msg) { let step = choose |step| RMQCluster::next_step(s, s_prime, step); @@ -895,7 +895,7 @@ pub proof fn lemma_true_leads_to_always_create_sts_req_msg_in_flight_implies_at_ true_pred().leads_to(always(lift_state(create_sts_req_msg_in_flight_implies_at_after_create_sts_step(key)))) ), { - let requirements = |msg: Message, s: RMQCluster| { + let requirements = |msg: RMQMessage, s: RMQCluster| { sts_create_request_msg(key)(msg) ==> { &&& at_rabbitmq_step(key, RabbitmqReconcileStep::AfterCreateStatefulSet)(s) @@ -912,7 +912,7 @@ pub proof fn lemma_true_leads_to_always_create_sts_req_msg_in_flight_implies_at_ }; assert forall |s, s_prime| #[trigger] stronger_next(s, s_prime) implies RMQCluster::every_new_req_msg_if_in_flight_then_satisfies(requirements)(s, s_prime) by { - assert forall |msg: Message| (!s.message_in_flight(msg) || requirements(msg, s)) && #[trigger] s_prime.message_in_flight(msg) + assert forall |msg: RMQMessage| (!s.message_in_flight(msg) || requirements(msg, s)) && #[trigger] s_prime.message_in_flight(msg) implies requirements(msg, s_prime) by { if sts_create_request_msg(key)(msg) { if !s.message_in_flight(msg) { @@ -967,7 +967,7 @@ pub proof fn lemma_true_leads_to_always_update_sts_req_msg_in_flight_implies_at_ true_pred().leads_to(always(lift_state(update_sts_req_msg_in_flight_implies_at_after_update_sts_step(key)))) ), { - let requirements = |msg: Message, s: RMQCluster| { + let requirements = |msg: RMQMessage, s: RMQCluster| { sts_update_request_msg(key)(msg) ==> { &&& at_rabbitmq_step(key, RabbitmqReconcileStep::AfterUpdateStatefulSet)(s) @@ -984,7 +984,7 @@ pub proof fn lemma_true_leads_to_always_update_sts_req_msg_in_flight_implies_at_ }; assert forall |s, s_prime| #[trigger] stronger_next(s, s_prime) implies RMQCluster::every_new_req_msg_if_in_flight_then_satisfies(requirements)(s, s_prime) by { - assert forall |msg: Message| (!s.message_in_flight(msg) || requirements(msg, s)) && #[trigger] s_prime.message_in_flight(msg) + assert forall |msg: RMQMessage| (!s.message_in_flight(msg) || requirements(msg, s)) && #[trigger] s_prime.message_in_flight(msg) implies requirements(msg, s_prime) by { if sts_update_request_msg(key)(msg) { let step = choose |step| RMQCluster::next_step(s, s_prime, step); @@ -1010,7 +1010,7 @@ pub proof fn lemma_true_leads_to_always_update_sts_req_msg_in_flight_implies_at_ pub open spec fn no_delete_request_msg_in_flight_with_key(key: ObjectRef) -> StatePred { |s: RMQCluster| { - forall |msg: Message| !{ + forall |msg: RMQMessage| !{ &&& #[trigger] s.message_in_flight(msg) &&& msg.dst.is_KubernetesAPI() &&& msg.content.is_delete_request() @@ -1060,7 +1060,7 @@ pub proof fn lemma_true_leads_to_always_no_delete_sts_req_is_in_flight(spec: Tem ), { let key = rabbitmq.object_ref(); - let requirements = |msg: Message, s: RMQCluster| !{ + let requirements = |msg: RMQMessage, s: RMQCluster| !{ &&& msg.dst.is_KubernetesAPI() &&& msg.content.is_delete_request() &&& msg.content.get_delete_request().key == make_stateful_set_key(rabbitmq.object_ref()) @@ -1073,7 +1073,7 @@ pub proof fn lemma_true_leads_to_always_no_delete_sts_req_is_in_flight(spec: Tem &&& RMQCluster::each_object_in_etcd_is_well_formed()(s) }; assert forall |s: RMQCluster, s_prime: RMQCluster| #[trigger] stronger_next(s, s_prime) implies RMQCluster::every_new_req_msg_if_in_flight_then_satisfies(requirements)(s, s_prime) by { - assert forall |msg: Message| (!s.message_in_flight(msg) || requirements(msg, s)) && #[trigger] s_prime.message_in_flight(msg) + assert forall |msg: RMQMessage| (!s.message_in_flight(msg) || requirements(msg, s)) && #[trigger] s_prime.message_in_flight(msg) implies requirements(msg, s_prime) by { if s.resource_key_exists(make_stateful_set_key(key)) { let owner_refs = s.resource_obj_of(make_stateful_set_key(key)).metadata.owner_references; diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness/liveness.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/liveness.rs index 159d5c70a..1119e06fe 100644 --- a/src/controller_examples/rabbitmq_controller/proof/liveness/liveness.rs +++ b/src/controller_examples/rabbitmq_controller/proof/liveness/liveness.rs @@ -860,7 +860,7 @@ proof fn lemma_from_pending_req_in_flight_at_some_step_to_pending_req_in_flight_ } proof fn lemma_receives_some_resp_at_rabbitmq_step_with_rabbitmq( - spec: TempPred, rabbitmq: RabbitmqClusterView, req_msg: Message, step: RabbitmqReconcileStep + spec: TempPred, rabbitmq: RabbitmqClusterView, req_msg: RMQMessage, step: RabbitmqReconcileStep ) requires spec.entails(always(lift_action(RMQCluster::next()))), @@ -912,7 +912,7 @@ proof fn lemma_receives_some_resp_at_rabbitmq_step_with_rabbitmq( // 1. There is only one possible next_step for it. // 2. When the controller enters this step, it must creates a request (which will be used to create the pending request message) proof fn lemma_from_resp_in_flight_at_some_step_to_pending_req_in_flight_at_next_step( - spec: TempPred, rabbitmq: RabbitmqClusterView, resp_msg: Message, step: RabbitmqReconcileStep, result_step: RabbitmqReconcileStep + spec: TempPred, rabbitmq: RabbitmqClusterView, resp_msg: RMQMessage, step: RabbitmqReconcileStep, result_step: RabbitmqReconcileStep ) requires spec.entails(always(lift_action(RMQCluster::next()))), @@ -1324,7 +1324,7 @@ proof fn lemma_from_after_get_stateful_set_and_key_exists_to_rabbitmq_matches(ra } proof fn lemma_receives_ok_resp_at_after_get_stateful_set_step_with_rabbitmq( - spec: TempPred, rabbitmq: RabbitmqClusterView, req_msg: Message, object: DynamicObjectView + spec: TempPred, rabbitmq: RabbitmqClusterView, req_msg: RMQMessage, object: DynamicObjectView ) requires spec.entails(always(lift_action(RMQCluster::next()))), @@ -1422,7 +1422,7 @@ proof fn lemma_receives_ok_resp_at_after_get_stateful_set_step_with_rabbitmq( } proof fn lemma_from_after_get_stateful_set_step_to_after_update_stateful_set_step( - spec: TempPred, rabbitmq: RabbitmqClusterView, resp_msg: Message, object: DynamicObjectView + spec: TempPred, rabbitmq: RabbitmqClusterView, resp_msg: RMQMessage, object: DynamicObjectView ) requires spec.entails(always(lift_action(RMQCluster::next()))), @@ -1495,7 +1495,7 @@ proof fn lemma_from_after_get_stateful_set_step_to_after_update_stateful_set_ste } proof fn lemma_sts_is_updated_at_after_update_stateful_set_step_with_rabbitmq( - spec: TempPred, rabbitmq: RabbitmqClusterView, req_msg: Message, object: DynamicObjectView + spec: TempPred, rabbitmq: RabbitmqClusterView, req_msg: RMQMessage, object: DynamicObjectView ) requires spec.entails(always(lift_action(RMQCluster::next()))), @@ -1702,7 +1702,7 @@ proof fn lemma_from_after_get_server_config_map_and_key_not_exists_to_rabbitmq_m } proof fn lemma_receives_not_found_resp_at_after_get_server_config_map_step_with_rabbitmq( - spec: TempPred, rabbitmq: RabbitmqClusterView, req_msg: Message + spec: TempPred, rabbitmq: RabbitmqClusterView, req_msg: RMQMessage ) requires spec.entails(always(lift_action(RMQCluster::next()))), @@ -1787,7 +1787,7 @@ proof fn lemma_receives_not_found_resp_at_after_get_server_config_map_step_with_ } proof fn lemma_from_after_get_server_config_map_step_to_after_create_server_config_map_step( - spec: TempPred, rabbitmq: RabbitmqClusterView, resp_msg: Message + spec: TempPred, rabbitmq: RabbitmqClusterView, resp_msg: RMQMessage ) requires spec.entails(always(lift_action(RMQCluster::next()))), @@ -1848,7 +1848,7 @@ proof fn lemma_from_after_get_server_config_map_step_to_after_create_server_conf } proof fn lemma_cm_is_created_at_after_create_server_config_map_step_with_rabbitmq( - spec: TempPred, rabbitmq: RabbitmqClusterView, req_msg: Message + spec: TempPred, rabbitmq: RabbitmqClusterView, req_msg: RMQMessage ) requires spec.entails(always(lift_action(RMQCluster::next()))), @@ -1921,7 +1921,7 @@ proof fn lemma_cm_is_created_at_after_create_server_config_map_step_with_rabbitm } proof fn lemma_receives_not_found_resp_at_after_get_stateful_set_step_with_rabbitmq( - spec: TempPred, rabbitmq: RabbitmqClusterView, req_msg: Message + spec: TempPred, rabbitmq: RabbitmqClusterView, req_msg: RMQMessage ) requires spec.entails(always(lift_action(RMQCluster::next()))), @@ -2006,7 +2006,7 @@ proof fn lemma_receives_not_found_resp_at_after_get_stateful_set_step_with_rabbi } proof fn lemma_from_after_get_stateful_set_step_to_after_create_stateful_set_step( - spec: TempPred, rabbitmq: RabbitmqClusterView, resp_msg: Message + spec: TempPred, rabbitmq: RabbitmqClusterView, resp_msg: RMQMessage ) requires spec.entails(always(lift_action(RMQCluster::next()))), @@ -2067,7 +2067,7 @@ proof fn lemma_from_after_get_stateful_set_step_to_after_create_stateful_set_ste } proof fn lemma_sts_is_created_at_after_create_stateful_set_step_with_rabbitmq( - spec: TempPred, rabbitmq: RabbitmqClusterView, req_msg: Message + spec: TempPred, rabbitmq: RabbitmqClusterView, req_msg: RMQMessage ) requires spec.entails(always(lift_action(RMQCluster::next()))), @@ -2317,7 +2317,7 @@ proof fn lemma_from_after_get_server_config_map_and_key_exists_to_rabbitmq_match } proof fn lemma_receives_ok_resp_at_after_get_server_config_map_step_with_rabbitmq( - spec: TempPred, rabbitmq: RabbitmqClusterView, req_msg: Message, object: DynamicObjectView + spec: TempPred, rabbitmq: RabbitmqClusterView, req_msg: RMQMessage, object: DynamicObjectView ) requires spec.entails(always(lift_action(RMQCluster::next()))), @@ -2409,7 +2409,7 @@ proof fn lemma_receives_ok_resp_at_after_get_server_config_map_step_with_rabbitm } proof fn lemma_cm_is_updated_at_after_update_server_config_map_step_with_rabbitmq( - spec: TempPred, rabbitmq: RabbitmqClusterView, req_msg: Message, object: DynamicObjectView + spec: TempPred, rabbitmq: RabbitmqClusterView, req_msg: RMQMessage, object: DynamicObjectView ) requires spec.entails(always(lift_action(RMQCluster::next()))), @@ -2497,7 +2497,7 @@ proof fn lemma_cm_is_updated_at_after_update_server_config_map_step_with_rabbitm } proof fn lemma_from_after_get_server_config_map_step_to_after_update_server_config_map_step( - spec: TempPred, rabbitmq: RabbitmqClusterView, resp_msg: Message, object: DynamicObjectView + spec: TempPred, rabbitmq: RabbitmqClusterView, resp_msg: RMQMessage, object: DynamicObjectView ) requires spec.entails(always(lift_action(RMQCluster::next()))), diff --git a/src/controller_examples/rabbitmq_controller/proof/safety.rs b/src/controller_examples/rabbitmq_controller/proof/safety.rs index 7e21373f1..f22374209 100644 --- a/src/controller_examples/rabbitmq_controller/proof/safety.rs +++ b/src/controller_examples/rabbitmq_controller/proof/safety.rs @@ -267,9 +267,9 @@ spec fn response_at_after_get_stateful_set_step_is_sts_get_response(rabbitmq: Ra ==> 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) && ( - forall |msg: Message| + forall |msg: RMQMessage| #[trigger] s.message_in_flight(msg) - && resp_msg_matches_req_msg(msg, s.pending_req_of(key)) + && Message::resp_msg_matches_req_msg(msg, s.pending_req_of(key)) ==> sts_get_response_msg(key)(msg) ) } @@ -312,13 +312,13 @@ proof fn lemma_always_response_at_after_get_stateful_set_step_is_sts_get_respons 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) && resp_msg_matches_req_msg(msg, s_prime.pending_req_of(key)) + 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.2.get_Some_0(); + let cr_key = input.1.get_Some_0(); if cr_key == key { assert(s.message_in_flight(msg)); assert(false); @@ -353,8 +353,15 @@ proof fn lemma_always_response_at_after_get_stateful_set_step_is_sts_get_respons 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)); + }, + _ => { + assert(sts_get_response_msg(key)(msg)); + } } } } @@ -366,7 +373,7 @@ spec fn stateful_set_in_get_response_and_update_request_have_no_larger_resource_ |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: Message| + forall |msg: RMQMessage| #[trigger] s.message_in_flight(msg) ==> ( sts_update_request_msg(rabbitmq.object_ref())(msg) @@ -391,12 +398,12 @@ proof fn lemma_always_stateful_set_in_get_response_and_update_request_have_no_la { let key = rabbitmq.object_ref(); let sts_key = make_stateful_set_key(rabbitmq.object_ref()); - let upd_rv_leq = |msg: Message, s: RMQCluster| { + let upd_rv_leq = |msg: RMQMessage, s: RMQCluster| { 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 }; - let get_rv_leq = |msg: Message, s: RMQCluster| { + 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 @@ -474,7 +481,7 @@ spec fn replicas_of_etcd_stateful_set_satisfies_order(rabbitmq: RabbitmqClusterV spec fn replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd(rabbitmq: RabbitmqClusterView) -> StatePred { |s: RMQCluster| { let sts_key = make_stateful_set_key(rabbitmq.object_ref()); - forall |msg: Message| + forall |msg: RMQMessage| #[trigger] s.message_in_flight(msg) && sts_update_request_msg(rabbitmq.object_ref())(msg) && s.resource_key_exists(sts_key) @@ -753,11 +760,11 @@ proof fn lemma_always_object_in_every_create_or_update_request_msg_only_has_vali combine_spec_entails_always_n!( spec, lift_action(next), lift_action(RMQCluster::next()), lift_state(RMQCluster::triggering_cr_has_lower_uid_than_uid_counter()) ); - let create_valid = |msg: Message, s: RMQCluster| { + let create_valid = |msg: RMQMessage, s: RMQCluster| { msg.content.is_create_request() && msg.content.get_create_request().obj.metadata.owner_references.is_Some() ==> owner_references_is_valid(msg.content.get_create_request().obj, s) }; - let update_valid = |msg: Message, s: RMQCluster| { + let update_valid = |msg: RMQMessage, s: RMQCluster| { msg.content.is_update_request() && msg.content.get_update_request().obj.metadata.owner_references.is_Some() ==> owner_references_is_valid(msg.content.get_update_request().obj, s) }; @@ -769,7 +776,7 @@ proof fn lemma_always_object_in_every_create_or_update_request_msg_only_has_vali let step = choose |step| RMQCluster::next_step(s, s_prime, step); match step { Step::ControllerStep(input) => { - let cr = s.triggering_cr_of(input.2.get_Some_0()); + let cr = s.triggering_cr_of(input.1.get_Some_0()); if msg.content.is_create_request() { let owner_refs = msg.content.get_create_request().obj.metadata.owner_references; if owner_refs.is_Some() { @@ -782,7 +789,7 @@ proof fn lemma_always_object_in_every_create_or_update_request_msg_only_has_vali } } }, - Step::ClientStep(_) => { + Step::ClientStep() => { if msg.content.is_create_request() { assert(msg.content.get_create_request().obj.kind.is_CustomResourceKind()); } else if msg.content.is_update_request() { @@ -838,7 +845,7 @@ proof fn lemma_always_every_owner_ref_of_every_object_in_etcd_has_different_uid_ spec fn replicas_of_stateful_set_update_request_msg_satisfies_order(rabbitmq: RabbitmqClusterView) -> StatePred { |s: RMQCluster| { let sts_key = make_stateful_set_key(rabbitmq.object_ref()); - forall |msg: Message| + forall |msg: RMQMessage| #[trigger] s.message_in_flight(msg) && sts_update_request_msg(rabbitmq.object_ref())(msg) ==> msg.content.get_update_request().obj.kind == Kind::StatefulSetKind @@ -850,7 +857,7 @@ spec fn replicas_of_stateful_set_update_request_msg_satisfies_order(rabbitmq: Ra spec fn replicas_of_stateful_set_create_request_msg_satisfies_order(rabbitmq: RabbitmqClusterView) -> StatePred { |s: RMQCluster| { let sts_key = make_stateful_set_key(rabbitmq.object_ref()); - forall |msg: Message| + forall |msg: RMQMessage| #[trigger] s.message_in_flight(msg) && sts_create_request_msg(rabbitmq.object_ref())(msg) ==> replicas_satisfies_order(msg.content.get_create_request().obj, rabbitmq)(s) diff --git a/src/controller_examples/simple_controller/proof/liveness.rs b/src/controller_examples/simple_controller/proof/liveness.rs index 4c32476da..5c96e8bbb 100644 --- a/src/controller_examples/simple_controller/proof/liveness.rs +++ b/src/controller_examples/simple_controller/proof/liveness.rs @@ -48,7 +48,7 @@ spec fn cr_matched(cr: SimpleCRView) -> TempPred> { /// To prove the liveness property, we need some invariants (these invariants have already contained "always" constraint). spec fn all_invariants(cr: SimpleCRView) -> TempPred> { tla_forall(|msg| always(lift_state(resp_matches_at_most_one_pending_req(msg, cr.object_ref())))) - .and(tla_forall(|resp_msg: Message| always(lift_state(at_most_one_resp_matches_req(resp_msg, cr.object_ref()))))) + .and(tla_forall(|resp_msg: SimpleMessage| always(lift_state(at_most_one_resp_matches_req(resp_msg, cr.object_ref()))))) .and(always(lift_state(reconcile_get_cr_done_implies_pending_req_in_flight_or_resp_in_flight(cr)))) .and(always(lift_state(reconciler_at_init_pc(cr)) .implies(lift_state(reconciler_init_and_no_pending_req(simple_reconciler(), cr.object_ref()))))) @@ -152,7 +152,7 @@ proof fn lemma_sm_partial_spec_is_stable_and_invariants(cr: SimpleCRView) always_p_is_stable::>( tla_forall(|msg| lift_state(resp_matches_at_most_one_pending_req(msg, cr.object_ref())))); always_p_is_stable::>( - tla_forall(|resp_msg: Message| lift_state(at_most_one_resp_matches_req(resp_msg, cr.object_ref())))); + tla_forall(|resp_msg: SimpleMessage| lift_state(at_most_one_resp_matches_req(resp_msg, cr.object_ref())))); always_p_is_stable::>( lift_state(reconciler_at_init_pc(cr)) .implies(lift_state(reconciler_init_and_no_pending_req(simple_reconciler(), cr.object_ref())))); @@ -164,11 +164,11 @@ proof fn lemma_sm_partial_spec_is_stable_and_invariants(cr: SimpleCRView) let a_to_p = |msg| lift_state(resp_matches_at_most_one_pending_req::(msg, cr.object_ref())); let a_to_always = |msg| always(lift_state( resp_matches_at_most_one_pending_req::(msg, cr.object_ref()))); - tla_forall_always_equality_variant::, Message>(a_to_always, a_to_p); + tla_forall_always_equality_variant::, SimpleMessage>(a_to_always, a_to_p); - let a_to_p_1 = |resp_msg: Message| lift_state(at_most_one_resp_matches_req(resp_msg, cr.object_ref())); - let a_to_always_1 = |resp_msg: Message| always(lift_state(at_most_one_resp_matches_req(resp_msg, cr.object_ref()))); - tla_forall_always_equality_variant::, Message>(a_to_always_1, a_to_p_1); + let a_to_p_1 = |resp_msg: SimpleMessage| lift_state(at_most_one_resp_matches_req(resp_msg, cr.object_ref())); + let a_to_always_1 = |resp_msg: SimpleMessage| always(lift_state(at_most_one_resp_matches_req(resp_msg, cr.object_ref()))); + tla_forall_always_equality_variant::, SimpleMessage>(a_to_always_1, a_to_p_1); stable_and_n!( tla_forall(|msg| always(lift_state(resp_matches_at_most_one_pending_req::(msg, cr.object_ref())))), @@ -197,7 +197,7 @@ proof fn lemma_sm_spec_entails_all_invariants(cr: SimpleCRView) entails_and_n!(sm_spec(simple_reconciler()), tla_forall(|msg| always(lift_state(resp_matches_at_most_one_pending_req(msg, cr.object_ref())))), - tla_forall(|resp_msg: Message| always(lift_state(at_most_one_resp_matches_req(resp_msg, cr.object_ref())))), + tla_forall(|resp_msg: SimpleMessage| always(lift_state(at_most_one_resp_matches_req(resp_msg, cr.object_ref())))), always(lift_state(reconcile_get_cr_done_implies_pending_req_in_flight_or_resp_in_flight(cr))), always(lift_state(reconciler_at_init_pc(cr)) .implies(lift_state(reconciler_init_and_no_pending_req(simple_reconciler(), cr.object_ref())))), @@ -342,11 +342,11 @@ proof fn lemma_after_get_cr_pc_leads_to_cm_exists(cr: SimpleCRView) assert(lift_state(reconcile_get_cr_done_implies_pending_req_in_flight_or_resp_in_flight(cr)) .satisfied_by(ex.suffix(i))); let s = ex.suffix(i).head(); - let req_msg = choose |req_msg: Message| { + let req_msg = choose |req_msg: SimpleMessage| { #[trigger] is_controller_get_cr_request_msg(req_msg, cr) && ClusterProof::pending_k8s_api_req_msg_is(s, cr.object_ref(), req_msg) && (s.message_in_flight(req_msg) - || exists |resp_msg: Message| { + || exists |resp_msg: SimpleMessage| { #[trigger] s.message_in_flight(resp_msg) && Message::resp_msg_matches_req_msg(resp_msg, req_msg) }) @@ -401,7 +401,7 @@ proof fn lemma_init_pc_and_no_pending_req_leads_to_cm_exists(cr: SimpleCRView) let req_msg = choose |msg| { &&& #[trigger] is_controller_get_cr_request_msg(msg, cr) &&& ClusterProof::pending_k8s_api_req_msg_is(s, cr.object_ref(), msg) - &&& ! exists |resp_msg: Message| { + &&& ! exists |resp_msg: SimpleMessage| { &&& #[trigger] s.message_in_flight(resp_msg) &&& Message::resp_msg_matches_req_msg(resp_msg, msg) } @@ -425,7 +425,7 @@ proof fn lemma_init_pc_and_no_pending_req_leads_to_cm_exists(cr: SimpleCRView) cm_exists(cr)); } -proof fn lemma_req_msg_sent_and_after_get_cr_pc_leads_to_cm_exists(req_msg: Message, cr: SimpleCRView) +proof fn lemma_req_msg_sent_and_after_get_cr_pc_leads_to_cm_exists(req_msg: SimpleMessage, cr: SimpleCRView) ensures partial_spec_with_invariants_and_assumptions(cr).entails( lift_state(reconciler_at_after_get_cr_pc_and_pending_req_and_req_in_flight(req_msg, cr)) @@ -434,7 +434,7 @@ proof fn lemma_req_msg_sent_and_after_get_cr_pc_leads_to_cm_exists(req_msg: Mess { let pre = reconciler_at_after_get_cr_pc_and_pending_req_and_req_in_flight(req_msg, cr); let get_cr_resp_msg_sent = |s: State| { - exists |resp_msg: Message| { + exists |resp_msg: SimpleMessage| { &&& #[trigger] s.message_in_flight(resp_msg) &&& Message::resp_msg_matches_req_msg(resp_msg, req_msg) } @@ -472,7 +472,7 @@ proof fn lemma_req_msg_sent_and_after_get_cr_pc_leads_to_cm_exists(req_msg: Mess reconciler_at_after_get_cr_pc_and_pending_req_and_exists_resp_in_flight(req_msg, cr), cm_exists(cr)); } -proof fn lemma_exists_resp_msg_sent_and_after_get_cr_pc_leads_to_cm_exists(req_msg: Message, cr: SimpleCRView) +proof fn lemma_exists_resp_msg_sent_and_after_get_cr_pc_leads_to_cm_exists(req_msg: SimpleMessage, cr: SimpleCRView) ensures partial_spec_with_invariants_and_assumptions(cr).entails( lift_state(reconciler_at_after_get_cr_pc_and_pending_req_and_exists_resp_in_flight(req_msg, cr)) @@ -482,10 +482,10 @@ proof fn lemma_exists_resp_msg_sent_and_after_get_cr_pc_leads_to_cm_exists(req_m let m_to_pre = |m: Message| lift_state(reconciler_at_after_get_cr_pc_and_pending_req_and_resp_in_flight(req_msg, m, cr)); let post = lift_state(cm_exists(cr)); let spec = partial_spec_with_invariants_and_assumptions(cr); - assert forall |msg: Message| spec.entails(#[trigger] m_to_pre(msg).leads_to(post)) by { + assert forall |msg: SimpleMessage| spec.entails(#[trigger] m_to_pre(msg).leads_to(post)) by { lemma_resp_msg_sent_and_after_get_cr_pc_leads_to_cm_exists(msg, req_msg, cr); }; - leads_to_exists_intro::, Message>(spec, m_to_pre, post); + leads_to_exists_intro::, SimpleMessage>(spec, m_to_pre, post); // This is for showing exists_m_to_pre == tla_exists(m_to_pre) let exists_m_to_pre = lift_state(reconciler_at_after_get_cr_pc_and_pending_req_and_exists_resp_in_flight(req_msg, cr)); @@ -526,7 +526,7 @@ proof fn lemma_init_pc_and_no_pending_req_leads_to_after_get_cr_pc_and_exists_pe lemma_pre_leads_to_post_by_controller(partial_spec_with_invariants_and_assumptions(cr), simple_reconciler(), input, stronger_next, continue_reconcile(simple_reconciler()), pre, post); } -proof fn lemma_after_get_cr_pc_and_pending_req_in_flight_and_no_resp_in_flight_leads_to_ok_resp_in_flight(req_msg: Message, cr: SimpleCRView) +proof fn lemma_after_get_cr_pc_and_pending_req_in_flight_and_no_resp_in_flight_leads_to_ok_resp_in_flight(req_msg: SimpleMessage, cr: SimpleCRView) ensures partial_spec_with_invariants_and_assumptions(cr).entails( lift_state(reconciler_at_after_get_cr_pc_and_pending_req_in_flight_and_no_resp_in_flight(req_msg, cr)) @@ -557,7 +557,7 @@ proof fn lemma_after_get_cr_pc_and_pending_req_in_flight_and_no_resp_in_flight_l // This lemma proves: // ideal_spec |= get_cr_pc /\ pending_req /\ ok_resp_in_flight ~> cm_exists -proof fn lemma_after_get_cr_pc_and_ok_resp_in_flight_leads_to_cm_exists(req_msg: Message, cr: SimpleCRView) +proof fn lemma_after_get_cr_pc_and_ok_resp_in_flight_leads_to_cm_exists(req_msg: SimpleMessage, cr: SimpleCRView) ensures partial_spec_with_invariants_and_assumptions(cr).entails( lift_state(reconciler_at_after_get_cr_pc_and_ok_resp_with_name_and_namespace_in_flight(req_msg, cr)) @@ -588,7 +588,7 @@ proof fn lemma_after_get_cr_pc_and_ok_resp_in_flight_leads_to_cm_exists(req_msg: assert forall |ex| #[trigger] spec.satisfied_by(ex) implies lift_state(cm_created).leads_to(lift_state(cm_exists(cr))).satisfied_by(ex) by { assert forall |i| #[trigger] lift_state(cm_created).satisfied_by(ex.suffix(i)) implies eventually(lift_state(cm_exists(cr))).satisfied_by(ex.suffix(i)) by { let s = ex.suffix(i).head(); - let req_msg = choose |msg: Message| { + let req_msg = choose |msg: SimpleMessage| { s.message_in_flight(msg) && msg.dst == HostId::KubernetesAPI && #[trigger] msg.content.is_create_request() @@ -608,7 +608,7 @@ proof fn lemma_after_get_cr_pc_and_ok_resp_in_flight_leads_to_cm_exists(req_msg: cm_created, cm_exists(cr)); } -spec fn strengthen_next_with_rep_resp_injectivity(resp_msg: Message, req_msg: Message, cr: SimpleCRView) -> ActionPred> { +spec fn strengthen_next_with_rep_resp_injectivity(resp_msg: SimpleMessage, req_msg: SimpleMessage, cr: SimpleCRView) -> ActionPred> { |s, s_prime: State| { &&& next(simple_reconciler())(s, s_prime) &&& at_most_one_resp_matches_req(resp_msg, cr.object_ref())(s) @@ -617,7 +617,7 @@ spec fn strengthen_next_with_rep_resp_injectivity(resp_msg: Message, req_msg: Message, cr: SimpleCRView) +proof fn lemma_resp_msg_sent_and_after_get_cr_pc_leads_to_cm_exists(resp_msg: SimpleMessage, req_msg: SimpleMessage, cr: SimpleCRView) ensures partial_spec_with_invariants_and_assumptions(cr).entails( lift_state(reconciler_at_after_get_cr_pc_and_pending_req_and_resp_in_flight(req_msg, resp_msg, cr)).leads_to(lift_state(cm_exists(cr))) @@ -644,7 +644,7 @@ proof fn lemma_resp_msg_sent_and_after_get_cr_pc_leads_to_cm_exists(resp_msg: Me leads_to_trans(partial_spec_with_invariants_and_assumptions(cr), pre, post, cm_exists(cr)); } -proof fn spec_entails_strengthen_next_with_rep_resp_injectivity(resp_msg: Message, req_msg: Message, cr: SimpleCRView) +proof fn spec_entails_strengthen_next_with_rep_resp_injectivity(resp_msg: SimpleMessage, req_msg: SimpleMessage, cr: SimpleCRView) ensures partial_spec_with_invariants_and_assumptions(cr).entails( always(lift_action(strengthen_next_with_rep_resp_injectivity(resp_msg, req_msg, cr))) @@ -653,10 +653,10 @@ proof fn spec_entails_strengthen_next_with_rep_resp_injectivity(resp_msg: Messag let next_and_invariant = strengthen_next_with_rep_resp_injectivity(resp_msg, req_msg, cr); let spec = partial_spec_with_invariants_and_assumptions(cr); // First, show spec |= always(inv1) - let a_to_p_1 = |resp_msg: Message| always(lift_state(at_most_one_resp_matches_req(resp_msg, cr.object_ref()))); + let a_to_p_1 = |resp_msg: SimpleMessage| always(lift_state(at_most_one_resp_matches_req(resp_msg, cr.object_ref()))); let tla_forall_pred_1 = tla_forall(a_to_p_1); assert(spec.entails(tla_forall_pred_1)); - tla_forall_apply::, Message>(a_to_p_1, resp_msg); + tla_forall_apply::, SimpleMessage>(a_to_p_1, resp_msg); entails_trans::>(spec, tla_forall_pred_1, always(lift_state(at_most_one_resp_matches_req(resp_msg, cr.object_ref())))); @@ -664,7 +664,7 @@ proof fn spec_entails_strengthen_next_with_rep_resp_injectivity(resp_msg: Messag let a_to_p_2 = |msg| always(lift_state(resp_matches_at_most_one_pending_req(msg, cr.object_ref()))); let tla_forall_pred_2 = tla_forall(a_to_p_2); assert(spec.entails(tla_forall_pred_2)); - tla_forall_apply::, Message>(a_to_p_2, resp_msg); + tla_forall_apply::, SimpleMessage>(a_to_p_2, resp_msg); entails_trans::>(spec, tla_forall_pred_2, always(lift_state(resp_matches_at_most_one_pending_req(resp_msg, cr.object_ref())))); @@ -693,11 +693,11 @@ pub proof fn next_and_not_crash_preserves_init_pc_or_reconciler_at_after_get_cr_ let req_msg = controller_req_msg(APIRequest::GetRequest(GetRequest{key: cr.object_ref()}), s.rest_id_allocator.allocate().1); assert(is_controller_get_cr_request_msg(req_msg, cr)); assert(req_msg.content.get_rest_id() == s.rest_id_allocator.rest_id_counter); - if (exists |resp_msg: Message| { + if (exists |resp_msg: SimpleMessage| { &&& #[trigger] s_prime.message_in_flight(resp_msg) &&& Message::resp_msg_matches_req_msg(resp_msg, req_msg) }) { - let resp_msg = choose |resp_msg: Message| { + let resp_msg = choose |resp_msg: SimpleMessage| { &&& #[trigger] s_prime.message_in_flight(resp_msg) &&& Message::resp_msg_matches_req_msg(resp_msg, req_msg) }; diff --git a/src/controller_examples/simple_controller/proof/safety.rs b/src/controller_examples/simple_controller/proof/safety.rs index fd42f2e44..2614624ef 100644 --- a/src/controller_examples/simple_controller/proof/safety.rs +++ b/src/controller_examples/simple_controller/proof/safety.rs @@ -56,7 +56,7 @@ pub open spec fn reconcile_get_cr_done_implies_pending_req_in_flight_or_resp_in_ #[trigger] is_controller_get_cr_request_msg(req_msg, cr) && pending_k8s_api_req_msg_is(s, cr.object_ref(), req_msg) && (s.message_in_flight(req_msg) - || exists |resp_msg: Message| { + || exists |resp_msg: SimpleMessage| { #[trigger] s.message_in_flight(resp_msg) && Message::resp_msg_matches_req_msg(resp_msg, req_msg) }) diff --git a/src/controller_examples/simple_controller/proof/shared.rs b/src/controller_examples/simple_controller/proof/shared.rs index 959d2654a..30a9c563d 100644 --- a/src/controller_examples/simple_controller/proof/shared.rs +++ b/src/controller_examples/simple_controller/proof/shared.rs @@ -18,6 +18,8 @@ use vstd::prelude::*; verus! { +pub type SimpleMessage = Message; + pub closed spec fn dummy_trigger(x: A); pub open spec fn reconciler_at_init_pc(cr: SimpleCRView) -> StatePred> { @@ -42,7 +44,7 @@ pub open spec fn reconciler_at_after_get_cr_pc(cr: SimpleCRView) -> StatePred, cr: SimpleCRView) -> StatePred> { +pub open spec fn reconciler_at_after_get_cr_pc_and_pending_req(msg: SimpleMessage, cr: SimpleCRView) -> StatePred> { |s: State| { &&& s.reconcile_state_contains(cr.object_ref()) &&& s.reconcile_state_of(cr.object_ref()).local_state.reconcile_pc == reconciler::after_get_cr_pc() @@ -51,7 +53,7 @@ pub open spec fn reconciler_at_after_get_cr_pc_and_pending_req(msg: Message, cr: SimpleCRView) -> StatePred> { +pub open spec fn reconciler_at_after_get_cr_pc_and_ok_resp_with_name_and_namespace_in_flight(req_msg: SimpleMessage, cr: SimpleCRView) -> StatePred> { |s: State| { &&& s.reconcile_state_contains(cr.object_ref()) &&& s.reconcile_state_of(cr.object_ref()).local_state.reconcile_pc == reconciler::after_get_cr_pc() @@ -70,7 +72,7 @@ pub open spec fn reconciler_at_after_get_cr_pc_and_exists_pending_req_and_req_in &&& #[trigger] is_controller_get_cr_request_msg(req_msg, cr) &&& s.message_in_flight(req_msg) &&& s.reconcile_state_of(cr.object_ref()).pending_req_msg == Some(req_msg) - &&& (! exists |resp_msg: Message| + &&& (! exists |resp_msg: SimpleMessage| #![trigger s.message_in_flight(resp_msg)] #![trigger resp_msg_matches_req_msg(resp_msg, req_msg)] s.message_in_flight(resp_msg) @@ -79,21 +81,21 @@ pub open spec fn reconciler_at_after_get_cr_pc_and_exists_pending_req_and_req_in } } -pub open spec fn reconciler_at_after_get_cr_pc_and_pending_req_in_flight_and_no_resp_in_flight(req_msg: Message, cr: SimpleCRView) -> StatePred> { +pub open spec fn reconciler_at_after_get_cr_pc_and_pending_req_in_flight_and_no_resp_in_flight(req_msg: SimpleMessage, cr: SimpleCRView) -> StatePred> { |s: State| { &&& s.reconcile_state_contains(cr.object_ref()) &&& s.reconcile_state_of(cr.object_ref()).local_state.reconcile_pc == reconciler::after_get_cr_pc() &&& s.reconcile_state_of(cr.object_ref()).pending_req_msg == Some(req_msg) &&& is_controller_get_cr_request_msg(req_msg, cr) &&& s.message_in_flight(req_msg) - &&& ! exists |resp_msg: Message| { + &&& ! exists |resp_msg: SimpleMessage| { &&& s.message_in_flight(resp_msg) &&& #[trigger] Message::resp_msg_matches_req_msg(resp_msg, req_msg) } } } -pub open spec fn reconciler_at_after_get_cr_pc_and_pending_req_and_req_in_flight(msg: Message, cr: SimpleCRView) -> StatePred> { +pub open spec fn reconciler_at_after_get_cr_pc_and_pending_req_and_req_in_flight(msg: SimpleMessage, cr: SimpleCRView) -> StatePred> { |s: State| { &&& s.reconcile_state_contains(cr.object_ref()) &&& s.reconcile_state_of(cr.object_ref()).local_state.reconcile_pc == reconciler::after_get_cr_pc() @@ -103,20 +105,20 @@ pub open spec fn reconciler_at_after_get_cr_pc_and_pending_req_and_req_in_flight } } -pub open spec fn reconciler_at_after_get_cr_pc_and_pending_req_and_exists_resp_in_flight(msg: Message, cr: SimpleCRView) -> StatePred> { +pub open spec fn reconciler_at_after_get_cr_pc_and_pending_req_and_exists_resp_in_flight(msg: SimpleMessage, cr: SimpleCRView) -> StatePred> { |s: State| { &&& s.reconcile_state_contains(cr.object_ref()) &&& s.reconcile_state_of(cr.object_ref()).local_state.reconcile_pc == reconciler::after_get_cr_pc() &&& s.reconcile_state_of(cr.object_ref()).pending_req_msg == Some(msg) &&& is_controller_get_cr_request_msg(msg, cr) - &&& exists |resp_msg: Message| { + &&& exists |resp_msg: SimpleMessage| { &&& #[trigger] s.message_in_flight(resp_msg) &&& Message::resp_msg_matches_req_msg(resp_msg, msg) } } } -pub open spec fn reconciler_at_after_get_cr_pc_and_pending_req_and_resp_in_flight(req_msg: Message, resp_msg: Message, cr: SimpleCRView) -> StatePred> { +pub open spec fn reconciler_at_after_get_cr_pc_and_pending_req_and_resp_in_flight(req_msg: SimpleMessage, resp_msg: SimpleMessage, cr: SimpleCRView) -> StatePred> { |s: State| { &&& s.reconcile_state_contains(cr.object_ref()) &&& s.reconcile_state_of(cr.object_ref()).local_state.reconcile_pc == reconciler::after_get_cr_pc() @@ -130,7 +132,7 @@ pub open spec fn reconciler_at_after_get_cr_pc_and_pending_req_and_resp_in_fligh pub open spec fn reconciler_at_after_create_cm_pc_and_req_in_flight_and_cm_created(cr: SimpleCRView) -> StatePred> { |s: State| { reconciler_at_after_create_cm_pc(cr)(s) - && exists |req_msg: Message| + && exists |req_msg: SimpleMessage| #![trigger s.message_in_flight(req_msg)] #![trigger req_msg.content.is_create_request()] s.message_in_flight(req_msg) @@ -173,14 +175,14 @@ pub open spec fn cm_exists(cr: SimpleCRView) -> StatePred| s.resource_key_exists(reconciler::make_config_map(cr).object_ref()) } -pub open spec fn is_controller_get_cr_request_msg(msg: Message, cr: SimpleCRView) -> bool { +pub open spec fn is_controller_get_cr_request_msg(msg: SimpleMessage, cr: SimpleCRView) -> bool { &&& msg.src == HostId::CustomController &&& msg.dst == HostId::KubernetesAPI &&& msg.content.is_get_request() &&& msg.content.get_get_request().key == cr.object_ref() } -pub open spec fn is_controller_create_cm_request_msg(msg: Message, cr: SimpleCRView) -> bool { +pub open spec fn is_controller_create_cm_request_msg(msg: SimpleMessage, cr: SimpleCRView) -> bool { &&& msg.src == HostId::CustomController &&& msg.dst == HostId::KubernetesAPI &&& msg.content.is_create_request() diff --git a/src/controller_examples/zookeeper_controller/proof/common.rs b/src/controller_examples/zookeeper_controller/proof/common.rs index 8ed4c5fda..5a71fdd1f 100644 --- a/src/controller_examples/zookeeper_controller/proof/common.rs +++ b/src/controller_examples/zookeeper_controller/proof/common.rs @@ -12,7 +12,7 @@ use crate::kubernetes_cluster::spec::{ }; use crate::temporal_logic::defs::*; use crate::zookeeper_controller::common::*; -use crate::zookeeper_controller::spec::zookeeper_api::ZKAPI; +use crate::zookeeper_controller::spec::zookeeper_api::*; use crate::zookeeper_controller::spec::{reconciler::*, zookeepercluster::*}; use vstd::prelude::*; @@ -20,6 +20,8 @@ verus! { pub type ZKCluster = Cluster; +pub type ZKMessage = Message; + pub open spec fn cluster_spec() -> TempPred { ZKCluster::sm_spec() } @@ -73,7 +75,7 @@ pub open spec fn pending_req_in_flight_at_zookeeper_step_with_zk( } pub open spec fn req_msg_is_the_in_flight_pending_req_at_zookeeper_step_with_zk( - step: ZookeeperReconcileStep, zk: ZookeeperClusterView, req_msg: Message, object: DynamicObjectView + step: ZookeeperReconcileStep, zk: ZookeeperClusterView, req_msg: ZKMessage, object: DynamicObjectView ) -> StatePred { |s: ZKCluster| { &&& at_zookeeper_step_with_zk(zk, step)(s) @@ -98,7 +100,7 @@ pub open spec fn exists_resp_in_flight_at_zookeeper_step_with_zk( } pub open spec fn resp_msg_is_the_in_flight_resp_at_zookeeper_step_with_zk( - step: ZookeeperReconcileStep, zk: ZookeeperClusterView, resp_msg: Message, object: DynamicObjectView + step: ZookeeperReconcileStep, zk: ZookeeperClusterView, resp_msg: ZKMessage, object: DynamicObjectView ) -> StatePred { |s: ZKCluster| { &&& at_zookeeper_step_with_zk(zk, step)(s) @@ -164,7 +166,7 @@ pub open spec fn at_after_get_stateful_set_step_with_zk_and_exists_not_found_err } pub open spec fn is_correct_pending_request_msg_at_zookeeper_step( - step: ZookeeperReconcileStep, msg: Message, zk: ZookeeperClusterView, object: DynamicObjectView + step: ZookeeperReconcileStep, msg: ZKMessage, zk: ZookeeperClusterView, object: DynamicObjectView ) -> bool { &&& msg.src == HostId::CustomController &&& msg.dst == HostId::KubernetesAPI diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/helper_invariants.rs b/src/controller_examples/zookeeper_controller/proof/liveness/helper_invariants.rs index 99af59b73..4f786dbed 100644 --- a/src/controller_examples/zookeeper_controller/proof/liveness/helper_invariants.rs +++ b/src/controller_examples/zookeeper_controller/proof/liveness/helper_invariants.rs @@ -23,7 +23,7 @@ use vstd::{multiset::*, prelude::*}; verus! { pub open spec fn sts_create_request_msg(key: ObjectRef) -> FnSpec(Message) -> bool { - |msg: Message| + |msg: ZKMessage| msg.dst.is_KubernetesAPI() && msg.content.is_create_request() && msg.content.get_create_request().namespace == make_stateful_set_key(key).namespace @@ -32,7 +32,7 @@ pub open spec fn sts_create_request_msg(key: ObjectRef) -> FnSpec(Message) -> bo } pub open spec fn sts_create_request_msg_since(key: ObjectRef, rest_id: RestId) -> FnSpec(Message) -> bool { - |msg: Message| + |msg: ZKMessage| sts_create_request_msg(key)(msg) && msg.content.get_rest_id() >= rest_id } @@ -336,14 +336,14 @@ pub proof fn lemma_always_at_most_one_create_sts_req_since_rest_id_is_in_flight( } pub open spec fn sts_update_request_msg(key: ObjectRef) -> FnSpec(Message) -> bool { - |msg: Message| + |msg: ZKMessage| msg.dst.is_KubernetesAPI() && msg.content.is_update_request() && msg.content.get_update_request().key == make_stateful_set_key(key) } pub open spec fn sts_update_request_msg_since(key: ObjectRef, rest_id: RestId) -> FnSpec(Message) -> bool { - |msg: Message| + |msg: ZKMessage| sts_update_request_msg(key)(msg) && msg.content.get_rest_id() >= rest_id } @@ -653,7 +653,7 @@ pub open spec fn every_update_sts_req_since_rest_id_does_the_same( zk.well_formed(), { |s: ZKCluster| { - forall |msg: Message| { + forall |msg: ZKMessage| { &&& #[trigger] s.network_state.in_flight.contains(msg) &&& sts_update_request_msg_since(zk.object_ref(), rest_id)(msg) } ==> msg.content.get_update_request().obj.spec == StatefulSetView::marshal_spec(make_stateful_set(zk).spec) @@ -713,7 +713,7 @@ pub proof fn lemma_always_every_update_sts_req_since_rest_id_does_the_same( assert forall |s, s_prime: ZKCluster| invariant(s) && #[trigger] stronger_next(s, s_prime) implies invariant(s_prime) by { - assert forall |msg: Message| + assert forall |msg: ZKMessage| #[trigger] s_prime.network_state.in_flight.contains(msg) && sts_update_request_msg_since(zk.object_ref(), rest_id)(msg) implies msg.content.get_update_request().obj.spec == StatefulSetView::marshal_spec(make_stateful_set(zk).spec) by { @@ -725,14 +725,14 @@ pub proof fn lemma_always_every_update_sts_req_since_rest_id_does_the_same( } pub open spec fn sts_delete_request_msg(key: ObjectRef) -> FnSpec(Message) -> bool { - |msg: Message| + |msg: ZKMessage| msg.dst.is_KubernetesAPI() && msg.content.is_delete_request() && msg.content.get_delete_request().key == make_stateful_set_key(key) } pub open spec fn sts_delete_request_msg_since(key: ObjectRef, rest_id: RestId) -> FnSpec(Message) -> bool { - |msg: Message| + |msg: ZKMessage| sts_delete_request_msg(key)(msg) && msg.content.get_rest_id() >= rest_id } @@ -744,7 +744,7 @@ pub open spec fn no_delete_sts_req_since_rest_id_is_in_flight( key.kind.is_CustomResourceKind(), { |s: ZKCluster| { - forall |msg: Message| !{ + forall |msg: ZKMessage| !{ &&& #[trigger] s.message_in_flight(msg) &&& sts_delete_request_msg_since(key, rest_id)(msg) } @@ -784,7 +784,7 @@ pub proof fn lemma_always_no_delete_sts_req_since_rest_id_is_in_flight( assert forall |s, s_prime: ZKCluster| invariant(s) && #[trigger] next(s, s_prime) implies invariant(s_prime) by { - assert forall |msg: Message| + assert forall |msg: ZKMessage| !(#[trigger] s_prime.message_in_flight(msg) && sts_delete_request_msg_since(key, rest_id)(msg)) by { if s.message_in_flight(msg) {} else {} } diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/liveness_property.rs b/src/controller_examples/zookeeper_controller/proof/liveness/liveness_property.rs index 16d507a8d..e78f44559 100644 --- a/src/controller_examples/zookeeper_controller/proof/liveness/liveness_property.rs +++ b/src/controller_examples/zookeeper_controller/proof/liveness/liveness_property.rs @@ -1162,7 +1162,7 @@ proof fn lemma_from_init_step_to_after_create_headless_service_step( // We don't care about update step here, so arbitraray() is used to show that the object parameter in // pending_req_in_flight_at_zookeeper_step_with_zk is unrelated. proof fn lemma_from_resp_in_flight_at_some_step_to_pending_req_in_flight_at_next_step( - spec: TempPred, zk: ZookeeperClusterView, resp_msg: Message, step: ZookeeperReconcileStep, result_step: ZookeeperReconcileStep + spec: TempPred, zk: ZookeeperClusterView, resp_msg: ZKMessage, step: ZookeeperReconcileStep, result_step: ZookeeperReconcileStep ) requires spec.entails(always(lift_action(ZKCluster::next()))), @@ -1241,7 +1241,7 @@ proof fn lemma_from_resp_in_flight_at_some_step_to_pending_req_in_flight_at_next } proof fn lemma_receives_some_resp_at_zookeeper_step_with_zk( - spec: TempPred, zk: ZookeeperClusterView, req_msg: Message, step: ZookeeperReconcileStep + spec: TempPred, zk: ZookeeperClusterView, req_msg: ZKMessage, step: ZookeeperReconcileStep ) requires spec.entails(always(lift_action(ZKCluster::next()))), @@ -1296,7 +1296,7 @@ proof fn lemma_receives_some_resp_at_zookeeper_step_with_zk( } proof fn lemma_receives_ok_resp_at_after_get_stateful_set_step_with_zk( - spec: TempPred, zk: ZookeeperClusterView, rest_id: nat, req_msg: Message, object: DynamicObjectView + spec: TempPred, zk: ZookeeperClusterView, rest_id: nat, req_msg: ZKMessage, object: DynamicObjectView ) requires spec.entails(always(lift_action(ZKCluster::next()))), @@ -1402,7 +1402,7 @@ proof fn lemma_receives_ok_resp_at_after_get_stateful_set_step_with_zk( } proof fn lemma_from_after_get_stateful_set_step_to_after_update_stateful_set_step( - spec: TempPred, zk: ZookeeperClusterView, rest_id: nat, resp_msg: Message, object: DynamicObjectView + spec: TempPred, zk: ZookeeperClusterView, rest_id: nat, resp_msg: ZKMessage, object: DynamicObjectView ) requires spec.entails(always(lift_action(ZKCluster::next()))), @@ -1486,7 +1486,7 @@ proof fn lemma_from_after_get_stateful_set_step_to_after_update_stateful_set_ste } proof fn lemma_sts_is_updated_at_after_update_stateful_set_step_with_zk( - spec: TempPred, zk: ZookeeperClusterView, rest_id: nat, req_msg: Message, object: DynamicObjectView + spec: TempPred, zk: ZookeeperClusterView, rest_id: nat, req_msg: ZKMessage, object: DynamicObjectView ) requires spec.entails(always(lift_action(ZKCluster::next()))), diff --git a/src/controller_examples/zookeeper_controller/proof/safety/deletion_safety.rs b/src/controller_examples/zookeeper_controller/proof/safety/deletion_safety.rs index 27d19e45a..b3c9c2b63 100644 --- a/src/controller_examples/zookeeper_controller/proof/safety/deletion_safety.rs +++ b/src/controller_examples/zookeeper_controller/proof/safety/deletion_safety.rs @@ -53,9 +53,9 @@ spec fn always_deletion_safety(req_msg: Message) -> TempPred { proof fn deletion_safety_proof_forall_msg() ensures - forall |msg: Message| cluster_spec().entails(#[trigger] always_deletion_safety(msg)), + forall |msg: ZKMessage| cluster_spec().entails(#[trigger] always_deletion_safety(msg)), { - assert forall |req_msg: Message| cluster_spec().entails(#[trigger] always_deletion_safety(req_msg)) by { + assert forall |req_msg: ZKMessage| cluster_spec().entails(#[trigger] always_deletion_safety(req_msg)) by { deletion_safety_proof(req_msg); } } diff --git a/src/kubernetes_cluster/proof/builtin_controllers.rs b/src/kubernetes_cluster/proof/builtin_controllers.rs index e39e3a6c1..b35c5c85f 100644 --- a/src/kubernetes_cluster/proof/builtin_controllers.rs +++ b/src/kubernetes_cluster/proof/builtin_controllers.rs @@ -25,7 +25,7 @@ pub open spec fn every_update_msg_sets_owner_references_as( key: ObjectRef, requirements: FnSpec(Option>) -> bool ) -> StatePred { |s: Self| { - forall |msg: Message| + forall |msg: MsgType| #[trigger] s.message_in_flight(msg) && msg.dst.is_KubernetesAPI() && msg.content.is_update_request() @@ -38,7 +38,7 @@ pub open spec fn every_create_msg_sets_owner_references_as( key: ObjectRef, requirements: FnSpec(Option>) -> bool ) -> StatePred { |s: Self| { - forall |msg: Message| + forall |msg: MsgType| #[trigger] s.message_in_flight(msg) && msg.dst.is_KubernetesAPI() && msg.content.is_create_request() @@ -70,7 +70,7 @@ pub open spec fn object_has_no_finalizers(key: ObjectRef) -> StatePred { spec fn exists_delete_request_msg_in_flight_with_key(key: ObjectRef) -> StatePred { |s: Self| { - exists |msg: Message| { + exists |msg: MsgType| { #[trigger] s.message_in_flight(msg) && msg.dst.is_KubernetesAPI() && msg.content.is_delete_request_with_key(key) @@ -227,14 +227,14 @@ proof fn lemma_delete_msg_in_flight_leads_to_owner_references_satisfies( assert_by( spec.entails(lift_state(pre).leads_to(lift_state(post))), { - let msg_to_p = |msg: Message| { + let msg_to_p = |msg: MsgType| { lift_state(|s: Self| { &&& s.message_in_flight(msg) &&& msg.dst.is_KubernetesAPI() &&& msg.content.is_delete_request_with_key(key) }) }; - assert forall |msg: Message| spec.entails((#[trigger] msg_to_p(msg)).leads_to(lift_state(post))) by { + assert forall |msg: MsgType| spec.entails((#[trigger] msg_to_p(msg)).leads_to(lift_state(post))) by { let input = Some(msg); let msg_to_p_state = |s: Self| { &&& s.message_in_flight(msg) diff --git a/src/kubernetes_cluster/proof/cluster.rs b/src/kubernetes_cluster/proof/cluster.rs index f01df9a4a..1b0718ef6 100644 --- a/src/kubernetes_cluster/proof/cluster.rs +++ b/src/kubernetes_cluster/proof/cluster.rs @@ -55,10 +55,10 @@ pub proof fn sm_partial_spec_is_stable() valid(stable(Self::sm_partial_spec())), { always_p_is_stable::(lift_action(Self::next())); - Self::tla_forall_action_weak_fairness_is_stable::>, ()>(Self::kubernetes_api_next()); + Self::tla_forall_action_weak_fairness_is_stable::>, ()>(Self::kubernetes_api_next()); Self::tla_forall_action_weak_fairness_is_stable::<(BuiltinControllerChoice, ObjectRef), ()>(Self::builtin_controllers_next()); - Self::tla_forall_action_weak_fairness_is_stable::<(Option>, Option), ()>(Self::controller_next()); - Self::tla_forall_action_weak_fairness_is_stable::>, ()>(Self::external_api_next()); + Self::tla_forall_action_weak_fairness_is_stable::<(Option>, Option), ()>(Self::controller_next()); + Self::tla_forall_action_weak_fairness_is_stable::>, ()>(Self::external_api_next()); Self::tla_forall_action_weak_fairness_is_stable::(Self::schedule_controller_reconcile()); Self::action_weak_fairness_is_stable::<()>(Self::disable_crash()); Self::action_weak_fairness_is_stable::<()>(Self::disable_busy()); diff --git a/src/kubernetes_cluster/proof/controller_runtime.rs b/src/kubernetes_cluster/proof/controller_runtime.rs index f8951ee30..4bf225aed 100644 --- a/src/kubernetes_cluster/proof/controller_runtime.rs +++ b/src/kubernetes_cluster/proof/controller_runtime.rs @@ -80,7 +80,7 @@ pub open spec fn pending_k8s_api_req_msg(s: Self, key: ObjectRef) -> bool { && s.reconcile_state_of(key).pending_req_msg.get_Some_0().content.is_APIRequest() } -pub open spec fn pending_k8s_api_req_msg_is(s: Self, key: ObjectRef, req: Message) -> bool { +pub open spec fn pending_k8s_api_req_msg_is(s: Self, key: ObjectRef, req: MsgType) -> bool { s.reconcile_state_of(key).pending_req_msg == Some(req) } @@ -100,14 +100,14 @@ pub open spec fn pending_req_in_flight_at_reconcile_state(key: ObjectRef, state: } } -pub open spec fn request_sent_by_controller(msg: Message) -> bool { +pub open spec fn request_sent_by_controller(msg: MsgType) -> bool { msg.src.is_CustomController() && msg.dst.is_KubernetesAPI() && msg.content.is_APIRequest() } pub open spec fn req_msg_is_the_in_flight_pending_req_at_reconcile_state( - key: ObjectRef, state: FnSpec(R::T) -> bool, req_msg: Message + key: ObjectRef, state: FnSpec(R::T) -> bool, req_msg: MsgType ) -> StatePred { |s: Self| { Self::at_expected_reconcile_states(key, state)(s) @@ -129,7 +129,7 @@ pub open spec fn pending_req_in_flight_or_resp_in_flight_at_reconcile_state( Self::pending_k8s_api_req_msg(s, key) && Self::request_sent_by_controller(s.pending_req_of(key)) && (s.message_in_flight(s.pending_req_of(key)) - || exists |resp_msg: Message| { + || exists |resp_msg: MsgType| { #[trigger] s.message_in_flight(resp_msg) && Message::resp_msg_matches_req_msg(resp_msg, s.pending_req_of(key)) }) @@ -171,7 +171,7 @@ pub open spec fn resp_in_flight_matches_pending_req_at_reconcile_state( Self::at_expected_reconcile_states(key, state)(s) && Self::pending_k8s_api_req_msg(s, key) && Self::request_sent_by_controller(s.pending_req_of(key)) - && exists |resp_msg: Message| { + && exists |resp_msg: MsgType| { #[trigger] s.message_in_flight(resp_msg) && Message::resp_msg_matches_req_msg(resp_msg, s.pending_req_of(key)) } diff --git a/src/kubernetes_cluster/proof/controller_runtime_liveness.rs b/src/kubernetes_cluster/proof/controller_runtime_liveness.rs index b75bfc273..797713ceb 100644 --- a/src/kubernetes_cluster/proof/controller_runtime_liveness.rs +++ b/src/kubernetes_cluster/proof/controller_runtime_liveness.rs @@ -27,7 +27,7 @@ pub open spec fn partial_spec_with_always_cr_key_exists_and_crash_disabled(cr_ke } pub proof fn lemma_pre_leads_to_post_by_controller( - spec: TempPred, input: (Option>, Option), next: ActionPred, + spec: TempPred, input: (Option>, Option), next: ActionPred, action: ControllerAction, pre: StatePred, post: StatePred ) requires @@ -40,7 +40,7 @@ pub proof fn lemma_pre_leads_to_post_by_controller( ensures spec.entails(lift_state(pre).leads_to(lift_state(post))), { - use_tla_forall::>, Option)>( + use_tla_forall::>, Option)>( spec, |i| Self::controller_next().weak_fairness(i), input ); @@ -256,7 +256,7 @@ pub proof fn lemma_from_some_state_to_arbitrary_next_state_to_reconcile_idle( && Self::pending_k8s_api_req_msg(s, cr.object_ref()) && Self::request_sent_by_controller(s.pending_req_of(cr.object_ref())) && (s.message_in_flight(s.pending_req_of(cr.object_ref())) - || exists |resp_msg: Message| { + || exists |resp_msg: MsgType| { #[trigger] s.message_in_flight(resp_msg) && Message::resp_msg_matches_req_msg(resp_msg, s.pending_req_of(cr.object_ref())) }) @@ -386,7 +386,7 @@ pub proof fn lemma_from_in_flight_resp_matches_pending_req_at_some_state_to_next && Message::resp_msg_matches_req_msg(resp, s.pending_req_of(cr.object_ref())) } ); - assert forall |msg: Message| spec.entails(#[trigger] known_resp_in_flight(msg) + assert forall |msg: MsgType| spec.entails(#[trigger] known_resp_in_flight(msg) .leads_to(lift_state(post))) by { let resp_in_flight_state = |s: Self| { Self::at_expected_reconcile_states(cr.object_ref(), state)(s) @@ -400,14 +400,14 @@ pub proof fn lemma_from_in_flight_resp_matches_pending_req_at_some_state_to_next spec, input, stronger_next, Self::continue_reconcile(), resp_in_flight_state, post ); }; - leads_to_exists_intro::>(spec, known_resp_in_flight, lift_state(post)); + leads_to_exists_intro::>(spec, known_resp_in_flight, lift_state(post)); assert_by( tla_exists(known_resp_in_flight) == lift_state(pre), { assert forall |ex| #[trigger] lift_state(pre).satisfied_by(ex) implies tla_exists(known_resp_in_flight).satisfied_by(ex) by { let s = ex.head(); - let msg = choose |resp_msg: Message| { + let msg = choose |resp_msg: MsgType| { #[trigger] s.message_in_flight(resp_msg) && Message::resp_msg_matches_req_msg(resp_msg, s.reconcile_state_of(cr.object_ref()).pending_req_msg.get_Some_0()) }; @@ -442,7 +442,7 @@ pub proof fn lemma_from_pending_req_in_flight_at_some_state_to_next_state( ), { let pre = Self::pending_req_in_flight_at_reconcile_state(cr.object_ref(), state); - assert forall |req_msg: Message| spec.entails( + assert forall |req_msg: MsgType| spec.entails( lift_state(#[trigger] Self::req_msg_is_the_in_flight_pending_req_at_reconcile_state(cr.object_ref(), state, req_msg)) .leads_to(lift_state(Self::resp_in_flight_matches_pending_req_at_reconcile_state(cr.object_ref(), state))) ) by { diff --git a/src/kubernetes_cluster/proof/controller_runtime_safety.rs b/src/kubernetes_cluster/proof/controller_runtime_safety.rs index fe3857538..12729ed2b 100644 --- a/src/kubernetes_cluster/proof/controller_runtime_safety.rs +++ b/src/kubernetes_cluster/proof/controller_runtime_safety.rs @@ -82,7 +82,7 @@ pub proof fn lemma_always_triggering_cr_has_lower_uid_than_uid_counter(spec: Tem } pub open spec fn resp_matches_at_most_one_pending_req( - resp_msg: Message, cr_key: ObjectRef + resp_msg: MsgType, cr_key: ObjectRef ) -> StatePred { |s: Self| { s.reconcile_state_contains(cr_key) @@ -99,7 +99,7 @@ pub open spec fn resp_matches_at_most_one_pending_req( } pub open spec fn resp_if_matches_pending_req_then_no_other_resp_matches( - resp_msg: Message, cr_key: ObjectRef + resp_msg: MsgType, cr_key: ObjectRef ) -> StatePred { |s: Self| { s.reconcile_state_contains(cr_key) @@ -107,14 +107,14 @@ pub open spec fn resp_if_matches_pending_req_then_no_other_resp_matches( && Self::pending_k8s_api_req_msg(s, cr_key) && Message::resp_msg_matches_req_msg(resp_msg, s.reconcile_state_of(cr_key).pending_req_msg.get_Some_0()) ==> ( - forall |other_resp: Message| other_resp != resp_msg && #[trigger] s.message_in_flight(other_resp) + forall |other_resp: MsgType| other_resp != resp_msg && #[trigger] s.message_in_flight(other_resp) ==> !Message::resp_msg_matches_req_msg(other_resp, s.reconcile_state_of(cr_key).pending_req_msg.get_Some_0()) ) } } pub proof fn lemma_always_resp_if_matches_pending_req_then_no_other_resp_matches( - spec: TempPred, resp_msg: Message, cr_key: ObjectRef + spec: TempPred, resp_msg: MsgType, cr_key: ObjectRef ) requires spec.entails(lift_state(Self::init())), @@ -143,7 +143,7 @@ pub proof fn lemma_forall_always_resp_if_matches_pending_req_then_no_other_resp_ spec.entails(always(lift_action(Self::next()))), ensures spec.entails( - tla_forall(|resp_msg: Message| always(lift_state(Self::resp_if_matches_pending_req_then_no_other_resp_matches(resp_msg, cr_key)))) + tla_forall(|resp_msg: MsgType| always(lift_state(Self::resp_if_matches_pending_req_then_no_other_resp_matches(resp_msg, cr_key)))) ), { let m_to_p = |msg| always(lift_state(Self::resp_if_matches_pending_req_then_no_other_resp_matches(msg, cr_key))); @@ -160,13 +160,13 @@ pub open spec fn each_resp_if_matches_pending_req_then_no_other_resp_matches( cr_key.kind.is_CustomResourceKind(), { |s: Self| { - forall |resp_msg: Message| + forall |resp_msg: MsgType| s.reconcile_state_contains(cr_key) && #[trigger] s.message_in_flight(resp_msg) && Self::pending_k8s_api_req_msg(s, cr_key) && Message::resp_msg_matches_req_msg(resp_msg, s.reconcile_state_of(cr_key).pending_req_msg.get_Some_0()) ==> ( - forall |other_resp: Message| other_resp != resp_msg && #[trigger] s.message_in_flight(other_resp) + forall |other_resp: MsgType| other_resp != resp_msg && #[trigger] s.message_in_flight(other_resp) ==> !Message::resp_msg_matches_req_msg(other_resp, s.reconcile_state_of(cr_key).pending_req_msg.get_Some_0()) ) } @@ -185,9 +185,9 @@ pub proof fn lemma_always_each_resp_if_matches_pending_req_then_no_other_resp_ma ), { let forall_a_to_p = lift_state(Self::each_resp_if_matches_pending_req_then_no_other_resp_matches(cr_key)); - let a_to_p = |resp_msg: Message| lift_state(Self::resp_if_matches_pending_req_then_no_other_resp_matches(resp_msg, cr_key)); - let a_to_always_p = |resp_msg: Message| always(a_to_p(resp_msg)); - assert forall |resp_msg: Message| spec.entails(#[trigger] a_to_always_p(resp_msg)) + let a_to_p = |resp_msg: MsgType| lift_state(Self::resp_if_matches_pending_req_then_no_other_resp_matches(resp_msg, cr_key)); + let a_to_always_p = |resp_msg: MsgType| always(a_to_p(resp_msg)); + assert forall |resp_msg: MsgType| spec.entails(#[trigger] a_to_always_p(resp_msg)) by { Self::lemma_always_resp_if_matches_pending_req_then_no_other_resp_matches(spec, resp_msg, cr_key); } @@ -195,13 +195,13 @@ pub proof fn lemma_always_each_resp_if_matches_pending_req_then_no_other_resp_ma tla_forall_always_equality(a_to_p); assert forall |ex| #[trigger] tla_forall(a_to_p).satisfied_by(ex) implies forall_a_to_p.satisfied_by(ex) by { - assert forall |resp_msg: Message| + assert forall |resp_msg: MsgType| ex.head().reconcile_state_contains(cr_key) && #[trigger] ex.head().message_in_flight(resp_msg) && Self::pending_k8s_api_req_msg(ex.head(), cr_key) && Message::resp_msg_matches_req_msg(resp_msg, ex.head().reconcile_state_of(cr_key).pending_req_msg.get_Some_0()) ==> ( - forall |other_resp: Message| other_resp != resp_msg && #[trigger] ex.head().message_in_flight(other_resp) + forall |other_resp: MsgType| other_resp != resp_msg && #[trigger] ex.head().message_in_flight(other_resp) ==> !Message::resp_msg_matches_req_msg(other_resp, ex.head().reconcile_state_of(cr_key).pending_req_msg.get_Some_0()) ) by { @@ -214,7 +214,7 @@ pub proof fn lemma_always_each_resp_if_matches_pending_req_then_no_other_resp_ma } pub proof fn lemma_always_resp_matches_at_most_one_pending_req( - spec: TempPred, resp_msg: Message, cr_key: ObjectRef + spec: TempPred, resp_msg: MsgType, cr_key: ObjectRef ) requires cr_key.kind.is_CustomResourceKind(), @@ -263,7 +263,7 @@ pub open spec fn each_resp_matches_at_most_one_pending_req( cr_key.kind.is_CustomResourceKind(), { |s: Self| { - forall |resp_msg: Message| + forall |resp_msg: MsgType| s.reconcile_state_contains(cr_key) && Self::pending_k8s_api_req_msg(s, cr_key) && #[trigger] Message::resp_msg_matches_req_msg(resp_msg, s.reconcile_state_of(cr_key).pending_req_msg.get_Some_0()) diff --git a/src/kubernetes_cluster/proof/kubernetes_api_liveness.rs b/src/kubernetes_cluster/proof/kubernetes_api_liveness.rs index 414c082bc..44e281b8a 100644 --- a/src/kubernetes_cluster/proof/kubernetes_api_liveness.rs +++ b/src/kubernetes_cluster/proof/kubernetes_api_liveness.rs @@ -19,7 +19,7 @@ verus! { impl > Cluster { pub proof fn lemma_pre_leads_to_post_by_kubernetes_api( - spec: TempPred, input: Option>, next: ActionPred, action: KubernetesAPIAction, + spec: TempPred, input: Option>, next: ActionPred, action: KubernetesAPIAction, pre: StatePred, post: StatePred ) requires @@ -32,7 +32,7 @@ pub proof fn lemma_pre_leads_to_post_by_kubernetes_api( ensures spec.entails(lift_state(pre).leads_to(lift_state(post))), { - use_tla_forall::>>(spec, |i| Self::kubernetes_api_next().weak_fairness(i), input); + use_tla_forall::>>(spec, |i| Self::kubernetes_api_next().weak_fairness(i), input); Self::kubernetes_api_action_pre_implies_next_pre(action, input); valid_implies_trans::( @@ -66,7 +66,7 @@ pub proof fn lemma_pre_leads_to_post_by_builtin_controllers( } pub proof fn lemma_get_req_leads_to_some_resp -(spec: TempPred, msg: Message, key: ObjectRef) +(spec: TempPred, msg: MsgType, key: ObjectRef) requires spec.entails(always(lift_action(Self::next()))), spec.entails(tla_forall(|i| Self::kubernetes_api_next().weak_fairness(i))), @@ -80,7 +80,7 @@ pub proof fn lemma_get_req_leads_to_some_resp }) .leads_to( lift_state(|s: Self| - exists |resp_msg: Message| { + exists |resp_msg: MsgType| { &&& #[trigger] s.message_in_flight(resp_msg) &&& Message::resp_msg_matches_req_msg(resp_msg, msg) } @@ -95,7 +95,7 @@ pub proof fn lemma_get_req_leads_to_some_resp &&& msg.content.is_get_request() &&& msg.content.get_get_request().key == key }; - let post = |s: Self| exists |resp_msg: Message| { + let post = |s: Self| exists |resp_msg: MsgType| { &&& #[trigger] s.message_in_flight(resp_msg) &&& Message::resp_msg_matches_req_msg(resp_msg, msg) }; @@ -148,7 +148,7 @@ pub proof fn lemma_get_req_leads_to_some_resp } pub proof fn lemma_get_req_leads_to_ok_or_err_resp -(spec: TempPred, msg: Message, key: ObjectRef) +(spec: TempPred, msg: MsgType, key: ObjectRef) requires spec.entails(always(lift_state(Self::busy_disabled()))), spec.entails(always(lift_action(Self::next()))), @@ -190,7 +190,7 @@ pub proof fn lemma_get_req_leads_to_ok_or_err_resp ); } -pub proof fn lemma_create_req_leads_to_res_exists(spec: TempPred, msg: Message) +pub proof fn lemma_create_req_leads_to_res_exists(spec: TempPred, msg: MsgType) requires spec.entails(always(lift_state(Self::busy_disabled()))), spec.entails(always(lift_action(Self::next()))), @@ -243,7 +243,7 @@ pub proof fn lemma_create_req_leads_to_res_exists(spec: TempPred, msg: Mes pub open spec fn no_req_before_rest_id_is_in_flight(rest_id: RestId) -> StatePred { |s: Self| { - forall |msg: Message| !{ + forall |msg: MsgType| !{ &&& #[trigger] s.message_in_flight(msg) &&& api_request_msg_before(rest_id)(msg) } @@ -268,9 +268,9 @@ pub open spec fn no_req_before_rest_id_is_in_flight(rest_id: RestId) -> StatePre /// (s.in_flight(msg) ==> requirements(msg, s)) ==> (s_prime.in_flight(msg) ==> requirements(msg, s_prime)) /// If we think of s.in_flight(msg) ==> requirements(msg, s) as an invariant, it is the same as the proof of invariants in previous /// proof strategy. -pub open spec fn every_new_req_msg_if_in_flight_then_satisfies(requirements: FnSpec(Message, Self) -> bool) -> ActionPred { +pub open spec fn every_new_req_msg_if_in_flight_then_satisfies(requirements: FnSpec(MsgType, Self) -> bool) -> ActionPred { |s: Self, s_prime: Self| { - forall |msg: Message| + forall |msg: MsgType| (!s.message_in_flight(msg) || requirements(msg, s)) && #[trigger] s_prime.message_in_flight(msg) && msg.dst.is_KubernetesAPI() @@ -279,9 +279,9 @@ pub open spec fn every_new_req_msg_if_in_flight_then_satisfies(requirements: FnS } } -pub open spec fn every_in_flight_req_msg_satisfies(requirements: FnSpec(Message, Self) -> bool) -> StatePred { +pub open spec fn every_in_flight_req_msg_satisfies(requirements: FnSpec(MsgType, Self) -> bool) -> StatePred { |s: Self| { - forall |msg: Message| + forall |msg: MsgType| #[trigger] s.message_in_flight(msg) && msg.dst.is_KubernetesAPI() && msg.content.is_APIRequest() @@ -297,7 +297,7 @@ pub open spec fn every_in_flight_req_msg_satisfies(requirements: FnSpec(Message< /// /// The last parameter must be equivalent to every_in_flight_req_msg_satisfies(requirements) pub proof fn lemma_true_leads_to_always_every_in_flight_req_msg_satisfies( - spec: TempPred, requirements: FnSpec(Message, Self) -> bool + spec: TempPred, requirements: FnSpec(MsgType, Self) -> bool ) requires spec.entails(always(lift_action(Self::every_new_req_msg_if_in_flight_then_satisfies(requirements)))), @@ -332,7 +332,7 @@ pub proof fn lemma_true_leads_to_always_every_in_flight_req_msg_satisfies( /// This lemma is an assistant one for the previous one without rest_id. pub proof fn lemma_some_rest_id_leads_to_always_every_in_flight_req_msg_satisfies_with_rest_id( - spec: TempPred, requirements: FnSpec(Message, Self) -> bool, rest_id: nat + spec: TempPred, requirements: FnSpec(MsgType, Self) -> bool, rest_id: nat ) requires spec.entails(always(lift_action(Self::every_new_req_msg_if_in_flight_then_satisfies(requirements)))), @@ -383,7 +383,7 @@ pub proof fn lemma_some_rest_id_leads_to_always_every_in_flight_req_msg_satisfie { Self::lemma_always_has_rest_id_counter_no_smaller_than(spec_with_rest_id, rest_id); let invariant = |s: Self| { - forall |msg: Message| #[trigger] + forall |msg: MsgType| #[trigger] s.message_in_flight(msg) && msg.content.get_rest_id() >= rest_id && msg.dst.is_KubernetesAPI() @@ -575,7 +575,7 @@ proof fn lemma_pending_requests_number_is_n_leads_to_no_pending_requests( && msg.content.get_rest_id() < rest_id) ); }; - len_is_zero_means_count_for_each_value_is_zero::>( + len_is_zero_means_count_for_each_value_is_zero::>( ex.head().network_state.in_flight.filter(api_request_msg_before(rest_id)) ); }; @@ -596,10 +596,10 @@ proof fn lemma_pending_requests_number_is_n_leads_to_no_pending_requests( s.network_state.in_flight.filter(api_request_msg_before(rest_id)).len() == (msg_num - 1) as nat }); let no_more_pending_requests = lift_state(Self::no_req_before_rest_id_is_in_flight(rest_id)); - let pending_req_in_flight = |msg: Message| lift_state(|s: Self| { + let pending_req_in_flight = |msg: MsgType| lift_state(|s: Self| { s.network_state.in_flight.filter(api_request_msg_before(rest_id)).count(msg) > 0 }); - let pending_requests_num_is_msg_num_and_pending_req_in_flight = |msg: Message| lift_state(|s: Self| { + let pending_requests_num_is_msg_num_and_pending_req_in_flight = |msg: MsgType| lift_state(|s: Self| { &&& s.network_state.in_flight.filter(api_request_msg_before(rest_id)).len() == msg_num &&& s.network_state.in_flight.filter(api_request_msg_before(rest_id)).count(msg) > 0 }); @@ -607,7 +607,7 @@ proof fn lemma_pending_requests_number_is_n_leads_to_no_pending_requests( // we need a concrete message to serve as the input of the forward action. // So here we split cases on different request messages in the network so that we have a concrete message // to reason about. - assert forall |msg: Message| spec.entails( + assert forall |msg: MsgType| spec.entails( #[trigger] pending_requests_num_is_msg_num_and_pending_req_in_flight(msg) .leads_to(pending_requests_num_is_msg_num_minus_1) ) by { @@ -639,7 +639,7 @@ proof fn lemma_pending_requests_number_is_n_leads_to_no_pending_requests( } proof fn pending_requests_num_decreases( - spec: TempPred, rest_id: RestId, msg_num: nat, msg: Message + spec: TempPred, rest_id: RestId, msg_num: nat, msg: MsgType ) requires msg_num > 0, diff --git a/src/kubernetes_cluster/proof/message.rs b/src/kubernetes_cluster/proof/message.rs index 9c106936d..99f1e8fc4 100644 --- a/src/kubernetes_cluster/proof/message.rs +++ b/src/kubernetes_cluster/proof/message.rs @@ -20,7 +20,7 @@ impl > Cluster { pub open spec fn every_in_flight_msg_has_lower_id_than_allocator() -> StatePred { |s: Self| { - forall |msg: Message| + forall |msg: MsgType| #[trigger] s.message_in_flight(msg) ==> msg.content.get_rest_id() < s.rest_id_allocator.rest_id_counter } @@ -49,7 +49,7 @@ proof fn next_preserves_every_in_flight_msg_has_lower_id_than_allocator( ensures Self::every_in_flight_msg_has_lower_id_than_allocator()(s_prime), { - assert forall |msg: Message| #[trigger] s_prime.message_in_flight(msg) implies + assert forall |msg: MsgType| #[trigger] s_prime.message_in_flight(msg) implies msg.content.get_rest_id() < s_prime.rest_id_allocator.rest_id_counter by { assert(s.rest_id_allocator.rest_id_counter <= s_prime.rest_id_allocator.rest_id_counter); if (s.message_in_flight(msg)) { @@ -61,7 +61,7 @@ proof fn next_preserves_every_in_flight_msg_has_lower_id_than_allocator( assert(s.rest_id_allocator.rest_id_counter < s_prime.rest_id_allocator.rest_id_counter) }, MessageContent::APIResponse(_, id) => { - let next_step = choose |step: Step| Self::next_step(s, s_prime, step); + let next_step = choose |step: Step>| Self::next_step(s, s_prime, step); match next_step { Step::KubernetesAPIStep(input) => { let req_msg = input.get_Some_0(); @@ -81,7 +81,7 @@ proof fn next_preserves_every_in_flight_msg_has_lower_id_than_allocator( assert(s.rest_id_allocator.rest_id_counter < s_prime.rest_id_allocator.rest_id_counter) }, MessageContent::ExternalAPIResponse(_, id) => { - let next_step = choose |step: Step| Self::next_step(s, s_prime, step); + let next_step = choose |step: Step>| Self::next_step(s, s_prime, step); match next_step { Step::ExternalAPIStep(input) => { let req_msg = input.get_Some_0(); @@ -101,7 +101,7 @@ proof fn next_preserves_every_in_flight_msg_has_lower_id_than_allocator( pub open spec fn every_in_flight_req_is_unique() -> StatePred { |s: Self| { - forall |msg: Message| + forall |msg: MsgType| (msg.content.is_APIRequest() || msg.content.is_ExternalAPIRequest()) && #[trigger] s.message_in_flight(msg) ==> s.network_state.in_flight.count(msg) == 1 @@ -128,7 +128,7 @@ pub proof fn lemma_always_every_in_flight_req_is_unique(spec: TempPred) ); assert forall |s, s_prime: Self| invariant(s) && #[trigger] stronger_next(s, s_prime) implies invariant(s_prime) by { - assert forall |msg: Message| + assert forall |msg: MsgType| (msg.content.is_APIRequest() || msg.content.is_ExternalAPIRequest()) && #[trigger] s_prime.message_in_flight(msg) implies s_prime.network_state.in_flight.count(msg) == 1 by { if (s.message_in_flight(msg)) { @@ -139,22 +139,22 @@ pub proof fn lemma_always_every_in_flight_req_is_unique(spec: TempPred) init_invariant::(spec, Self::init(), stronger_next, invariant); } -pub open spec fn in_flight_or_pending_req_message(s: Self, msg: Message) -> bool { +pub open spec fn in_flight_or_pending_req_message(s: Self, msg: MsgType) -> bool { msg.content.is_APIRequest() && (s.message_in_flight(msg) || ( - exists |key| - #[trigger] s.reconcile_state_contains(key) + exists |key| + #[trigger] s.reconcile_state_contains(key) && s.reconcile_state_of(key).pending_req_msg == Some(msg) )) } pub open spec fn every_in_flight_or_pending_req_msg_has_unique_id() -> StatePred { |s: Self| { - forall |msg: Message| - #[trigger] Self::in_flight_or_pending_req_message(s, msg) + forall |msg: MsgType| + #[trigger] Self::in_flight_or_pending_req_message(s, msg) ==> ( - forall |other_msg: Message| + forall |other_msg: MsgType| #[trigger] Self::in_flight_or_pending_req_message(s, other_msg) && msg != other_msg ==> msg.content.get_rest_id() != other_msg.content.get_rest_id() @@ -180,7 +180,7 @@ pub proof fn lemma_always_every_in_flight_or_pending_req_msg_has_unique_id(spec: Self::lemma_always_every_in_flight_msg_has_lower_id_than_allocator(spec); Self::lemma_always_pending_req_has_lower_req_id_than_allocator(spec); combine_spec_entails_always_n!( - spec, lift_action(stronger_next), + spec, lift_action(stronger_next), lift_action(Self::next()), lift_state(Self::every_in_flight_msg_has_lower_id_than_allocator()), lift_state(Self::pending_req_has_lower_req_id_than_allocator()) @@ -188,9 +188,9 @@ pub proof fn lemma_always_every_in_flight_or_pending_req_msg_has_unique_id(spec: assert forall |s, s_prime: Self| invariant(s) && #[trigger] stronger_next(s, s_prime) implies invariant(s_prime) by { assert forall |msg| #[trigger] Self::in_flight_or_pending_req_message(s_prime, msg) implies ( - forall |other_msg: Message| #[trigger] Self::in_flight_or_pending_req_message(s_prime, other_msg) && msg != other_msg + forall |other_msg: MsgType| #[trigger] Self::in_flight_or_pending_req_message(s_prime, other_msg) && msg != other_msg ==> msg.content.get_rest_id() != other_msg.content.get_rest_id()) by { - assert forall |other_msg: Message| #[trigger] Self::in_flight_or_pending_req_message(s_prime, other_msg) && msg != other_msg implies + assert forall |other_msg: MsgType| #[trigger] Self::in_flight_or_pending_req_message(s_prime, other_msg) && msg != other_msg implies msg.content.get_rest_id() != other_msg.content.get_rest_id() by { let step = choose |step| Self::next_step(s, s_prime, step); if Self::in_flight_or_pending_req_message(s, other_msg) && Self::in_flight_or_pending_req_message(s, msg) { @@ -208,10 +208,10 @@ pub proof fn lemma_always_every_in_flight_or_pending_req_msg_has_unique_id(spec: pub open spec fn every_in_flight_msg_has_unique_id() -> StatePred { |s: Self| { - forall |msg: Message| + forall |msg: MsgType| #[trigger] s.message_in_flight(msg) ==> ( - forall |other_msg: Message| + forall |other_msg: MsgType| #[trigger] s.message_in_flight(other_msg) && msg != other_msg ==> msg.content.get_rest_id() != other_msg.content.get_rest_id() @@ -237,7 +237,7 @@ pub proof fn lemma_always_every_in_flight_msg_has_unique_id(spec: TempPred Self::lemma_always_every_in_flight_msg_has_lower_id_than_allocator(spec); Self::lemma_always_every_in_flight_req_is_unique(spec); combine_spec_entails_always_n!( - spec, lift_action(stronger_next), + spec, lift_action(stronger_next), lift_action(Self::next()), lift_state(Self::every_in_flight_msg_has_lower_id_than_allocator()), lift_state(Self::every_in_flight_req_is_unique()) @@ -260,10 +260,10 @@ proof fn next_and_unique_lower_msg_id_preserves_in_flight_msg_has_unique_id( ensures Self::every_in_flight_msg_has_unique_id()(s_prime), { - assert forall |msg: Message| #[trigger] s_prime.message_in_flight(msg) implies - (forall |other_msg: Message| #[trigger] s_prime.message_in_flight(other_msg) && msg != other_msg + assert forall |msg: MsgType| #[trigger] s_prime.message_in_flight(msg) implies + (forall |other_msg: MsgType| #[trigger] s_prime.message_in_flight(other_msg) && msg != other_msg ==> msg.content.get_rest_id() != other_msg.content.get_rest_id()) by { - assert forall |other_msg: Message| #[trigger] s_prime.message_in_flight(other_msg) && msg != other_msg implies + assert forall |other_msg: MsgType| #[trigger] s_prime.message_in_flight(other_msg) && msg != other_msg implies msg.content.get_rest_id() != other_msg.content.get_rest_id() by { // At most one message will be added to the network_state.in_flight for each action. assert(s.message_in_flight(msg) || s.message_in_flight(other_msg)); @@ -281,7 +281,7 @@ proof fn next_and_unique_lower_msg_id_preserves_in_flight_msg_has_unique_id( } proof fn newly_added_msg_have_different_id_from_existing_ones( - s: Self, s_prime: Self, msg_1: Message, msg_2: Message + s: Self, s_prime: Self, msg_1: MsgType, msg_2: MsgType ) requires Self::next()(s, s_prime), @@ -296,7 +296,7 @@ proof fn newly_added_msg_have_different_id_from_existing_ones( msg_1.content.get_rest_id() != msg_2.content.get_rest_id(), { if (msg_2.content.is_APIResponse()) { - let next_step = choose |step: Step| Self::next_step(s, s_prime, step); + let next_step = choose |step: Step>| Self::next_step(s, s_prime, step); match next_step { Step::KubernetesAPIStep(input) => { let req_msg = input.get_Some_0(); @@ -311,7 +311,7 @@ proof fn newly_added_msg_have_different_id_from_existing_ones( _ => assert(false), } } else if msg_2.content.is_ExternalAPIResponse() { - let next_step = choose |step: Step| Self::next_step(s, s_prime, step); + let next_step = choose |step: Step>| Self::next_step(s, s_prime, step); match next_step { Step::ExternalAPIStep(input) => { let req_msg = input.get_Some_0(); @@ -323,13 +323,6 @@ proof fn newly_added_msg_have_different_id_from_existing_ones( } } -pub open spec fn req_in_flight_or_pending_at_controller(req_msg: Message, s: Self) -> bool { - req_msg.content.is_APIRequest() && (s.message_in_flight(req_msg) - || exists |cr_key: ObjectRef| ( - #[trigger] s.reconcile_state_contains(cr_key) - && Self::pending_k8s_api_req_msg_is(s, cr_key, req_msg) - )) -} pub open spec fn pending_req_has_lower_req_id_than_allocator() -> StatePred { |s: Self| { diff --git a/src/kubernetes_cluster/proof/wf1_assistant.rs b/src/kubernetes_cluster/proof/wf1_assistant.rs index c28ccec9a..ebd04f71e 100644 --- a/src/kubernetes_cluster/proof/wf1_assistant.rs +++ b/src/kubernetes_cluster/proof/wf1_assistant.rs @@ -26,7 +26,7 @@ verus! { impl > Cluster { pub proof fn kubernetes_api_action_pre_implies_next_pre( - action: KubernetesAPIAction, input: Option> + action: KubernetesAPIAction, input: Option> ) requires Self::kubernetes_api().actions.contains(action), @@ -57,7 +57,7 @@ pub proof fn exists_next_kubernetes_api_step( } pub proof fn controller_action_pre_implies_next_pre( - action: ControllerAction, input: (Option>, Option) + action: ControllerAction, input: (Option>, Option) ) requires Self::controller().actions.contains(action), diff --git a/src/kubernetes_cluster/spec/cluster.rs b/src/kubernetes_cluster/spec/cluster.rs index 265fbae88..8677cf886 100644 --- a/src/kubernetes_cluster/spec/cluster.rs +++ b/src/kubernetes_cluster/spec/cluster.rs @@ -40,7 +40,7 @@ pub struct Cluster> { impl> Cluster { #[verifier(inline)] - pub open spec fn message_in_flight(self, msg: Message) -> bool { + pub open spec fn message_in_flight(self, msg: MsgType) -> bool { self.network_state.in_flight.contains(msg) } @@ -79,7 +79,7 @@ impl> Cluster { } #[verifier(inline)] - pub open spec fn pending_req_of(self, key: ObjectRef) -> Message + pub open spec fn pending_req_of(self, key: ObjectRef) -> MsgType recommends self.reconcile_state_contains(key), self.reconcile_state_of(key).pending_req_msg.is_Some(), diff --git a/src/kubernetes_cluster/spec/cluster_state_machine.rs b/src/kubernetes_cluster/spec/cluster_state_machine.rs index 66b4f7c31..5b13e1b6d 100644 --- a/src/kubernetes_cluster/spec/cluster_state_machine.rs +++ b/src/kubernetes_cluster/spec/cluster_state_machine.rs @@ -24,16 +24,16 @@ use vstd::{multiset::*, prelude::*}; verus! { #[is_variant] -pub enum Step { - KubernetesAPIStep(Option>), +pub enum Step { + KubernetesAPIStep(Option), BuiltinControllersStep((BuiltinControllerChoice, ObjectRef)), - ControllerStep((Option>, Option)), + ControllerStep((Option, Option)), ClientStep(), - ExternalAPIStep(Option>), + ExternalAPIStep(Option), ScheduleControllerReconcileStep(ObjectRef), RestartController(), DisableCrash(), - KubernetesBusy(Option>), + KubernetesBusy(Option), DisableBusy(), StutterStep(), } @@ -58,8 +58,8 @@ pub open spec fn init() -> StatePred { /// Handling each create/update/delete request will potentially change the objects stored in the key-value store /// (etcd by default). /// The persistent state stored in the key-value store is modeled as a Map. -pub open spec fn kubernetes_api_next() -> Action>, ()> { - let result = |input: Option>, s: Self| { +pub open spec fn kubernetes_api_next() -> Action>, ()> { + let result = |input: Option>, s: Self| { let host_result = Self::kubernetes_api().next_result( KubernetesAPIActionInput{ recv: input }, s.kubernetes_api_state @@ -73,12 +73,12 @@ pub open spec fn kubernetes_api_next() -> Action>, s: Self| { + precondition: |input: Option>, s: Self| { &&& received_msg_destined_for(input, HostId::KubernetesAPI) &&& result(input, s).0.is_Enabled() &&& result(input, s).1.is_Enabled() }, - transition: |input: Option>, s: Self| { + transition: |input: Option>, s: Self| { let (host_result, network_result) = result(input, s); (Self { kubernetes_api_state: host_result.get_Enabled_0(), @@ -133,8 +133,8 @@ pub open spec fn builtin_controllers_next() -> Action Action>, ()> { - let result = |input: Option>, s: Self| { +pub open spec fn external_api_next() -> Action>, ()> { + let result = |input: Option>, s: Self| { let host_result = Self::external_api().next_result( ExternalAPIActionInput { recv: input, @@ -151,12 +151,12 @@ pub open spec fn external_api_next() -> Action>, s: Self| { + precondition: |input: Option>, s: Self| { &&& received_msg_destined_for(input, HostId::ExternalAPI) &&& result(input, s).0.is_Enabled() &&& result(input, s).1.is_Enabled() }, - transition: |input: Option>, s: Self| { + transition: |input: Option>, s: Self| { let (host_result, network_result) = result(input, s); (Self { external_api_state: host_result.get_Enabled_0(), @@ -167,8 +167,8 @@ pub open spec fn external_api_next() -> Action Action>, Option), ()> { - let result = |input: (Option>, Option), s: Self| { +pub open spec fn controller_next() -> Action>, Option), ()> { + let result = |input: (Option>, Option), s: Self| { let host_result = Self::controller().next_result( ControllerActionInput{recv: input.0, scheduled_cr_key: input.1, rest_id_allocator: s.rest_id_allocator}, s.controller_state @@ -182,12 +182,12 @@ pub open spec fn controller_next() -> Action>, Option), s: Self| { + precondition: |input: (Option>, Option), s: Self| { &&& received_msg_destined_for(input.0, HostId::CustomController) &&& result(input, s).0.is_Enabled() &&& result(input, s).1.is_Enabled() }, - transition: |input: (Option>, Option), s: Self| { + transition: |input: (Option>, Option), s: Self| { let (host_result, network_result) = result(input, s); (Self { controller_state: host_result.get_Enabled_0(), @@ -270,8 +270,8 @@ pub open spec fn disable_crash() -> Action { } } -pub open spec fn busy_kubernetes_api_rejects_request() -> Action>, ()> { - let network_result = |input: Option>, s: Self| { +pub open spec fn busy_kubernetes_api_rejects_request() -> Action>, ()> { + let network_result = |input: Option>, s: Self| { let req_msg = input.get_Some_0(); let resp = Message::form_matched_resp_msg(req_msg, Err(APIError::ServerTimeout)); let msg_ops = MessageOps { @@ -282,14 +282,14 @@ pub open spec fn busy_kubernetes_api_rejects_request() -> Action>, s: Self| { + precondition: |input: Option>, s: Self| { &&& s.busy_enabled &&& input.is_Some() &&& input.get_Some_0().dst.is_KubernetesAPI() &&& input.get_Some_0().content.is_APIRequest() &&& network_result(input, s).is_Enabled() }, - transition: |input: Option>, s: Self| { + transition: |input: Option>, s: Self| { (Self { network_state: network_result(input, s).get_Enabled_0(), ..s @@ -357,7 +357,7 @@ pub open spec fn stutter() -> Action { } } -pub open spec fn next_step(s: Self, s_prime: Self, step: Step) -> bool { +pub open spec fn next_step(s: Self, s_prime: Self, step: Step>) -> bool { match step { Step::KubernetesAPIStep(input) => Self::kubernetes_api_next().forward(input)(s, s_prime), Step::BuiltinControllersStep(input) => Self::builtin_controllers_next().forward(input)(s, s_prime), @@ -375,9 +375,9 @@ pub open spec fn next_step(s: Self, s_prime: Self, step: Step) -> bool { /// `next` chooses: /// * which host to take the next action (`Step`) -/// * whether to deliver a message and which message to deliver (`Option>` in `Step`) +/// * whether to deliver a message and which message to deliver (`Option>` in `Step`) pub open spec fn next() -> ActionPred { - |s: Self, s_prime: Self| exists |step: Step| Self::next_step(s, s_prime, step) + |s: Self, s_prime: Self| exists |step: Step>| Self::next_step(s, s_prime, step) } /// We install the reconciler to the Kubernetes cluster state machine spec @@ -398,7 +398,7 @@ pub open spec fn sm_partial_spec() -> TempPred { .and(Self::disable_busy().weak_fairness(())) } -pub open spec fn kubernetes_api_action_pre(action: KubernetesAPIAction, input: Option>) -> StatePred { +pub open spec fn kubernetes_api_action_pre(action: KubernetesAPIAction, input: Option>) -> StatePred { |s: Self| { let host_result = Self::kubernetes_api().next_action_result( action, @@ -439,7 +439,7 @@ pub open spec fn builtin_controllers_action_pre(action: BuiltinControllersAction } } -pub open spec fn controller_action_pre(action: ControllerAction, input: (Option>, Option)) -> StatePred { +pub open spec fn controller_action_pre(action: ControllerAction, input: (Option>, Option)) -> StatePred { |s: Self| { let host_result = Self::controller().next_action_result( action, diff --git a/src/kubernetes_cluster/spec/controller/common.rs b/src/kubernetes_cluster/spec/controller/common.rs index d5c91b958..8f5019037 100644 --- a/src/kubernetes_cluster/spec/controller/common.rs +++ b/src/kubernetes_cluster/spec/controller/common.rs @@ -20,7 +20,7 @@ pub struct OngoingReconcile pub triggering_cr: K, // pending_req_msg: the request message pending for the handling for k8s api // pending_external_api_input: the request returned by the reconcile_core which should be sent to be external api - pub pending_req_msg: Option>, + pub pending_req_msg: Option>, pub local_state: R::T, } @@ -32,13 +32,13 @@ pub enum ControllerStep { } pub struct ControllerActionInput { - pub recv: Option>, + pub recv: Option>, pub scheduled_cr_key: Option, pub rest_id_allocator: RestIdAllocator, } pub struct ControllerActionOutput { - pub send: Multiset>, + pub send: Multiset>, pub rest_id_allocator: RestIdAllocator, } diff --git a/src/kubernetes_cluster/spec/external_api/types.rs b/src/kubernetes_cluster/spec/external_api/types.rs index 5f6387652..9885fca86 100644 --- a/src/kubernetes_cluster/spec/external_api/types.rs +++ b/src/kubernetes_cluster/spec/external_api/types.rs @@ -21,12 +21,12 @@ pub enum ExternalAPIStep { } pub struct ExternalAPIActionInput { - pub recv: Option>, + pub recv: Option>, pub resources: StoredState, } pub struct ExternalAPIActionOutput { - pub send: Multiset>, + pub send: Multiset>, } pub type ExternalAPIStateMachine = StateMachine, ExternalAPIActionInput, ExternalAPIActionInput, ExternalAPIActionOutput, ExternalAPIStep>; diff --git a/src/kubernetes_cluster/spec/kubernetes_api/state_machine.rs b/src/kubernetes_cluster/spec/kubernetes_api/state_machine.rs index 192881f9b..41b7afd1e 100644 --- a/src/kubernetes_cluster/spec/kubernetes_api/state_machine.rs +++ b/src/kubernetes_cluster/spec/kubernetes_api/state_machine.rs @@ -49,7 +49,7 @@ pub open spec fn object_has_well_formed_spec(obj: DynamicObjectView) -> bool { &&& obj.kind == K::kind() ==> K::unmarshal_spec(obj.spec).is_Ok() } -pub open spec fn handle_get_request(msg: Message, s: KubernetesAPIState) -> (KubernetesAPIState, Message) +pub open spec fn handle_get_request(msg: MsgType, s: KubernetesAPIState) -> (KubernetesAPIState, MsgType) recommends msg.content.is_get_request(), { @@ -72,7 +72,7 @@ pub open spec fn list_query(list_req: ListRequest, s: KubernetesAPIState) -> Seq Seq::empty() } -pub open spec fn handle_list_request(msg: Message, s: KubernetesAPIState) -> (KubernetesAPIState, Message) +pub open spec fn handle_list_request(msg: MsgType, s: KubernetesAPIState) -> (KubernetesAPIState, MsgType) recommends msg.content.is_list_request(), { @@ -113,7 +113,7 @@ pub open spec fn validate_create_request(req: CreateRequest, s: KubernetesAPISta } } -pub open spec fn handle_create_request(msg: Message, s: KubernetesAPIState) -> (KubernetesAPIState, Message) +pub open spec fn handle_create_request(msg: MsgType, s: KubernetesAPIState) -> (KubernetesAPIState, MsgType) recommends msg.content.is_create_request(), { @@ -143,7 +143,7 @@ pub open spec fn handle_create_request(msg: Message, s: Kub pub closed spec fn deletion_timestamp() -> StringView; -pub open spec fn handle_delete_request(msg: Message, s: KubernetesAPIState) -> (KubernetesAPIState, Message) +pub open spec fn handle_delete_request(msg: MsgType, s: KubernetesAPIState) -> (KubernetesAPIState, MsgType) recommends msg.content.is_delete_request(), { @@ -167,7 +167,7 @@ pub open spec fn handle_delete_request(msg: Message, s: Kub } else { let stamped_obj_with_new_rv = stamped_obj.set_resource_version(s.resource_version_counter); let result = Ok(stamped_obj_with_new_rv); - let resp = form_delete_resp_msg(msg, result); + let resp = Message::form_delete_resp_msg(msg, result); (KubernetesAPIState { // Here we use req.key, instead of stamped_obj.object_ref(), to insert to the map. // This is intended because using stamped_obj.object_ref() will require us to use @@ -179,7 +179,7 @@ pub open spec fn handle_delete_request(msg: Message, s: Kub ..s }, resp) } - + } else { // The object can be immediately removed from the key-value store. let result = Ok(obj); @@ -277,7 +277,7 @@ pub open spec fn updated_object(req: UpdateRequest, s: KubernetesAPIState) -> Dy updated_obj } -pub open spec fn handle_update_request(msg: Message, s: KubernetesAPIState) -> (KubernetesAPIState, Message) +pub open spec fn handle_update_request(msg: MsgType, s: KubernetesAPIState) -> (KubernetesAPIState, MsgType) recommends msg.content.is_update_request(), { @@ -338,7 +338,7 @@ pub open spec fn handle_update_request(msg: Message, s: Kub } // etcd is modeled as a centralized map that handles get/list/create/delete/update -pub open spec fn transition_by_etcd(msg: Message, s: KubernetesAPIState) -> (KubernetesAPIState, Message) +pub open spec fn transition_by_etcd(msg: MsgType, s: KubernetesAPIState) -> (KubernetesAPIState, MsgType) recommends msg.content.is_APIRequest(), { diff --git a/src/kubernetes_cluster/spec/message.rs b/src/kubernetes_cluster/spec/message.rs index 713eab99e..14ba967b4 100644 --- a/src/kubernetes_cluster/spec/message.rs +++ b/src/kubernetes_cluster/spec/message.rs @@ -19,6 +19,8 @@ pub struct Message { pub content: MessageContent, } +pub type MsgType = Message<::Input, ::Output>; + #[is_variant] pub enum HostId { KubernetesAPI, diff --git a/src/kubernetes_cluster/spec/network/state_machine.rs b/src/kubernetes_cluster/spec/network/state_machine.rs index 9a419dcc5..2229629cc 100644 --- a/src/kubernetes_cluster/spec/network/state_machine.rs +++ b/src/kubernetes_cluster/spec/network/state_machine.rs @@ -38,7 +38,7 @@ pub open spec fn deliver() -> Action, MessageO pub open spec fn network() -> NetworkStateMachine, MessageOps> { NetworkStateMachine { - init: |s: NetworkState| s.in_flight == Multiset::>::empty(), + init: |s: NetworkState| s.in_flight == Multiset::>::empty(), deliver: Self::deliver(), } }