Add kind to sts_update_request_msg

Signed-off-by: Wenjie Ma <[email protected]>
anvil-verifier · Aug 25, 2023 · 0f75d88 · 0f75d88
1 parent 741cd2a
commit 0f75d88
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 9 deletions.
diff --git a/src/controller_examples/rabbitmq_controller/proof/common.rs b/src/controller_examples/rabbitmq_controller/proof/common.rs
@@ -382,6 +382,7 @@ pub open spec fn sts_update_request_msg(key: ObjectRef) -> FnSpec(RMQMessage) ->
         msg.dst.is_KubernetesAPI()
         && msg.content.is_update_request()
         && msg.content.get_update_request().key == make_stateful_set_key(key)
+        && msg.content.get_update_request().obj.kind == Kind::StatefulSetKind
 }
 
 pub open spec fn sts_get_response_msg(key: ObjectRef) -> FnSpec(RMQMessage) -> bool {

diff --git a/src/controller_examples/rabbitmq_controller/proof/safety.rs b/src/controller_examples/rabbitmq_controller/proof/safety.rs
@@ -339,6 +339,7 @@ proof fn lemma_always_response_at_after_get_stateful_set_step_is_sts_get_respons
                         assert(s.message_in_flight(msg));
                     },
                     _ => {
+                        assert(s.message_in_flight(msg));
                         assert(sts_get_response_msg(key)(msg));
                     }
                 }
@@ -760,8 +761,7 @@ spec fn replicas_of_stateful_set_update_request_msg_satisfies_order(rabbitmq: Ra
         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
-                && replicas_satisfies_order(msg.content.get_update_request().obj, rabbitmq)(s)
+            ==> replicas_satisfies_order(msg.content.get_update_request().obj, rabbitmq)(s)
     }
 }
 
@@ -909,14 +909,13 @@ proof fn lemma_always_replicas_of_stateful_set_update_request_msg_satisfies_orde
     );
     assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by {
         assert forall |msg| #[trigger] s_prime.message_in_flight(msg) && sts_update_request_msg(rabbitmq.object_ref())(msg)
-        implies msg.content.get_update_request().obj.kind == Kind::StatefulSetKind && replicas_satisfies_order(msg.content.get_update_request().obj, rabbitmq)(s_prime) by {
+        implies replicas_satisfies_order(msg.content.get_update_request().obj, rabbitmq)(s_prime) by {
             let step = choose |step| RMQCluster::next_step(s, s_prime, step);
             let key = rabbitmq.object_ref();
             let sts_key = make_stateful_set_key(key);
             match step {
                 Step::KubernetesAPIStep(input) => {
                     assert(s.message_in_flight(msg));
-                    assert(msg.content.get_update_request().obj.kind == Kind::StatefulSetKind);
                     assert(s.controller_state == s_prime.controller_state);
                     if s_prime.resource_key_exists(key) {
                         if s.resource_key_exists(key) {
@@ -944,30 +943,25 @@ proof fn lemma_always_replicas_of_stateful_set_update_request_msg_satisfies_orde
                         let cr = s.triggering_cr_of(key);
                         StatefulSetView::spec_integrity_is_preserved_by_marshal();
                         assert(replicas_of_stateful_set(msg.content.get_update_request().obj) == cr.spec.replicas);
-                        assert(msg.content.get_update_request().obj.kind == Kind::StatefulSetKind);
                     } else {
-                        assert(msg.content.get_update_request().obj.kind == Kind::StatefulSetKind);
                         assert(replicas_satisfies_order(msg.content.get_update_request().obj, rabbitmq)(s_prime));
                     }
                 },
                 Step::ScheduleControllerReconcileStep(input) => {
                     assert(s.message_in_flight(msg));
-                    assert(msg.content.get_update_request().obj.kind == Kind::StatefulSetKind);
                     assert(s.kubernetes_api_state == s_prime.kubernetes_api_state);
                     if input == key {} else {}
                     assert(replicas_satisfies_order(msg.content.get_update_request().obj, rabbitmq)(s_prime));
                 },
                 Step::RestartController() => {
                     assert(s.message_in_flight(msg));
-                    assert(msg.content.get_update_request().obj.kind == Kind::StatefulSetKind);
                     assert(s.kubernetes_api_state == s_prime.kubernetes_api_state);
                     assert(!s_prime.reconcile_state_contains(key));
                     assert(!s_prime.reconcile_scheduled_for(key));
                     assert(replicas_satisfies_order(msg.content.get_update_request().obj, rabbitmq)(s_prime));
                 },
                 _ => {
                     assert(s.message_in_flight(msg));
-                    assert(msg.content.get_update_request().obj.kind == Kind::StatefulSetKind);
                     assert(s.kubernetes_api_state == s_prime.kubernetes_api_state);
                     assert(s.controller_state == s_prime.controller_state);
                     assert(replicas_satisfies_order(msg.content.get_update_request().obj, rabbitmq)(s_prime));

diff --git a/src/kubernetes_cluster/proof/builtin_controllers.rs b/src/kubernetes_cluster/proof/builtin_controllers.rs
@@ -21,6 +21,11 @@ verus! {
 
 impl <K: ResourceView, E: ExternalAPI, R: Reconciler<K, E>> Cluster<K, E, R> {
 
+/// Everytime when we reason about update request message, we can only consider those valid ones (see validata_update_request).
+/// However, listing all requirements makes spec looks cubersome; we can only list those that we need or that may appear according
+/// to the spec of system.
+/// 
+/// For example, in some lemma we use msg.content.get_update_request().obj.kind == key.kind, so this requirement is added here.
 pub open spec fn every_update_msg_sets_owner_references_as(
     key: ObjectRef, requirements: FnSpec(Option<Seq<OwnerReferenceView>>) -> bool
 ) -> StatePred<Self> {
@@ -30,6 +35,7 @@ pub open spec fn every_update_msg_sets_owner_references_as(
             && msg.dst.is_KubernetesAPI()
             && msg.content.is_update_request()
             && msg.content.get_update_request().key == key
+            && msg.content.get_update_request().obj.kind == key.kind
             ==> requirements(msg.content.get_update_request().obj.metadata.owner_references)
     }
 }