Accelerate some lemmas in rabbitmq proof

.gitignore

@@ -13,3 +13,4 @@ e2e/target/
 /Cargo.lock
 src/liblib.rlib
 verifiable-controllers.code-workspace
+src/.verus-solver-log/

src/controller_examples/rabbitmq_controller/proof/helper_invariants/owner_ref.rs

@@ -87,29 +87,48 @@ 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);
-                lemma_resource_create_or_update_request_msg_implies_key_in_reconcile_equals(sub_resource, rabbitmq, s, s_prime, msg, 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) {
-                    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) {
-                    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);
 }
 
+#[verifier(spinoff_prover)]
+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> {

src/controller_examples/rabbitmq_controller/proof/helper_invariants/predicate.rs

@@ -136,6 +136,18 @@ pub open spec fn response_at_after_get_resource_step_is_resource_get_response(
     }
 }
 
+pub open spec fn request_at_after_get_request_step_is_resource_get_request(
+    sub_resource: SubResource, rabbitmq: RabbitmqClusterView
+) -> StatePred<RMQCluster> {
+    let key = rabbitmq.object_ref();
+    let resource_key = get_request(sub_resource, rabbitmq).key;
+    |s: RMQCluster| {
+        at_rabbitmq_step(key, RabbitmqReconcileStep::AfterKRequestStep(ActionKind::Get, sub_resource))(s)
+        ==> s.ongoing_reconciles()[key].pending_req_msg.is_Some()
+            && resource_get_request_msg(resource_key)(s.ongoing_reconciles()[key].pending_req_msg.get_Some_0())
+    }
+}
+
 pub open spec fn object_in_response_at_after_update_resource_step_is_same_as_etcd(
     sub_resource: SubResource, rabbitmq: RabbitmqClusterView
 ) -> StatePred<RMQCluster> {