Break down object_in_every_resource_create_or_update_request_msg_only…

…_has_valid_owner_references_helper Signed-off-by: Wenjie Ma <[email protected]>
anvil-verifier · Oct 18, 2023 · d35b737 · d35b737
1 parent 52e3c4a
commit d35b737
Showing 1 changed file with 35 additions and 18 deletions.
diff --git a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/owner_ref.rs b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/owner_ref.rs
@@ -87,30 +87,47 @@ pub proof fn lemma_always_object_in_every_resource_create_or_update_request_msg_
         assert forall |msg| #[trigger] s_prime.in_flight().contains(msg) implies create_valid(msg, s_prime) && update_valid(msg, s_prime) by {
             assert(s.kubernetes_api_state.uid_counter <= s_prime.kubernetes_api_state.uid_counter);
             if !s.in_flight().contains(msg) {
-                let step = choose |step| RMQCluster::next_step(s, s_prime, step);
-                let input = step.get_ControllerStep_0();
-                let cr = s.ongoing_reconciles()[input.1.get_Some_0()].triggering_cr;
-                if resource_create_request_msg(resource_key)(msg) {
-                    lemma_resource_create_request_msg_implies_key_in_reconcile_equals(sub_resource, rabbitmq, s, s_prime, msg, step);
-                    let owner_refs = msg.content.get_create_request().obj.metadata.owner_references;
-                    assert(owner_refs == Some(seq![cr.controller_owner_ref()]));
-                    assert(owner_refs.is_Some());
-                    assert(owner_refs.get_Some_0().len() == 1);
-                    assert(owner_refs.get_Some_0()[0].uid < s.kubernetes_api_state.uid_counter);
-                } else if resource_update_request_msg(resource_key)(msg) {
-                    lemma_resource_update_request_msg_implies_key_in_reconcile_equals(sub_resource, rabbitmq, s, s_prime, msg, step);
-                    let owner_refs = msg.content.get_update_request().obj.metadata.owner_references;
-                    assert(owner_refs == Some(seq![cr.controller_owner_ref()]));
-                    assert(owner_refs.is_Some());
-                    assert(owner_refs.get_Some_0().len() == 1);
-                    assert(owner_refs.get_Some_0()[0].uid < s.kubernetes_api_state.uid_counter);
-                }
+                object_in_every_resource_create_or_update_request_msg_only_has_valid_owner_references_helper(s, s_prime, sub_resource, rabbitmq, msg);
             }
         }
     }
     init_invariant(spec, RMQCluster::init(), next, inv);
 }
 
+proof fn object_in_every_resource_create_or_update_request_msg_only_has_valid_owner_references_helper(
+    s: RMQCluster, s_prime: RMQCluster, sub_resource: SubResource, rabbitmq: RabbitmqClusterView, msg: RMQMessage
+)
+    requires
+        !s.in_flight().contains(msg), s_prime.in_flight().contains(msg),
+        RMQCluster::next()(s, s_prime),
+        RMQCluster::triggering_cr_has_lower_uid_than_uid_counter()(s),
+        RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s),
+    ensures
+        resource_create_request_msg(get_request(sub_resource, rabbitmq).key)(msg) ==> owner_references_is_valid(msg.content.get_create_request().obj, s_prime),
+        resource_update_request_msg(get_request(sub_resource, rabbitmq).key)(msg) ==> owner_references_is_valid(msg.content.get_update_request().obj, s_prime),
+{
+    let resource_key = get_request(sub_resource, rabbitmq).key;
+    assert(s.kubernetes_api_state.uid_counter <= s_prime.kubernetes_api_state.uid_counter);
+    let step = choose |step| RMQCluster::next_step(s, s_prime, step);
+    let input = step.get_ControllerStep_0();
+    let cr = s.ongoing_reconciles()[input.1.get_Some_0()].triggering_cr;
+    if resource_create_request_msg(resource_key)(msg) {
+        lemma_resource_create_request_msg_implies_key_in_reconcile_equals(sub_resource, rabbitmq, s, s_prime, msg, step);
+        let owner_refs = msg.content.get_create_request().obj.metadata.owner_references;
+        assert(owner_refs == Some(seq![cr.controller_owner_ref()]));
+        assert(owner_refs.is_Some());
+        assert(owner_refs.get_Some_0().len() == 1);
+        assert(owner_refs.get_Some_0()[0].uid < s.kubernetes_api_state.uid_counter);
+    } else if resource_update_request_msg(resource_key)(msg) {
+        lemma_resource_update_request_msg_implies_key_in_reconcile_equals(sub_resource, rabbitmq, s, s_prime, msg, step);
+        let owner_refs = msg.content.get_update_request().obj.metadata.owner_references;
+        assert(owner_refs == Some(seq![cr.controller_owner_ref()]));
+        assert(owner_refs.is_Some());
+        assert(owner_refs.get_Some_0().len() == 1);
+        assert(owner_refs.get_Some_0()[0].uid < s.kubernetes_api_state.uid_counter);
+    }
+}
+
 pub open spec fn every_owner_ref_of_every_object_in_etcd_has_different_uid_from_uid_counter(
     sub_resource: SubResource, rabbitmq: RabbitmqClusterView
 ) -> StatePred<RMQCluster> {