Refine and refactor the proof and file structure

Compact some similar lemmas. Try to delete some useless functions. Move
some lemmas to common module (i.e, kubernetes_cluster::proof, not specific 
to one controller). Refactor the file structure to make it more reasonable.
Reword some comments and naming. Try to make the verification more stable.
Rename lower_rv => smaller_rv.

---------

Signed-off-by: Wenjie Ma <[email protected]>

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 {
@@ -394,12 +395,4 @@ pub open spec fn sts_get_response_msg(key: ObjectRef) -> FnSpec(RMQMessage) -> b
         )
 }
 
-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()
-        && msg.content.get_get_response().res.get_Ok_0().object_ref() == make_stateful_set_key(key)
-}
-
 }

src/controller_examples/rabbitmq_controller/proof/liveness/helper_invariants/invariants.rs → src/controller_examples/rabbitmq_controller/proof/helper_invariants/invariants.rs

@@ -1096,4 +1096,124 @@ pub proof fn lemma_true_leads_to_always_no_delete_sts_req_is_in_flight(spec: Tem
     );
 }
 
+/// This spec tells that when the reconciler is at AfterGetStatefulSet, and there is a matched response, the reponse must be
+/// sts_get_response_msg. This lemma is used to show that the response message, if is ok, has an object whose reference is
+/// stateful_set_key. resp_msg_matches_req_msg doesn't talk about the object in response should match the key in request
+/// so we need this extra spec and lemma.
+/// 
+/// If we don't have this, we have no idea of what is inside the response message.
+pub open spec fn response_at_after_get_stateful_set_step_is_sts_get_response(rabbitmq: RabbitmqClusterView) -> StatePred<RMQCluster> {
+    let key = rabbitmq.object_ref();
+    |s: RMQCluster| {
+        at_rabbitmq_step(key, RabbitmqReconcileStep::AfterGetStatefulSet)(s)
+        ==> s.reconcile_state_of(key).pending_req_msg.is_Some()
+            && is_get_stateful_set_request(s.pending_req_of(key).content.get_APIRequest_0(), rabbitmq)
+            && (
+                forall |msg: RMQMessage|
+                    #[trigger] s.message_in_flight(msg)
+                    && Message::resp_msg_matches_req_msg(msg, s.pending_req_of(key))
+                    ==> sts_get_response_msg(key)(msg)
+            )
+    }
+}
+
+pub proof fn lemma_always_response_at_after_get_stateful_set_step_is_sts_get_response(spec: TempPred<RMQCluster>, rabbitmq: RabbitmqClusterView)
+    requires
+        spec.entails(lift_state(RMQCluster::init())),
+        spec.entails(always(lift_action(RMQCluster::next()))),
+    ensures
+        spec.entails(always(lift_state(response_at_after_get_stateful_set_step_is_sts_get_response(rabbitmq)))),
+{
+    let inv = response_at_after_get_stateful_set_step_is_sts_get_response(rabbitmq);
+    let key = rabbitmq.object_ref();
+    let next = |s, s_prime| {
+        &&& RMQCluster::next()(s, s_prime)
+        &&& RMQCluster::each_object_in_etcd_is_well_formed()(s)
+        &&& RMQCluster::every_in_flight_msg_has_lower_id_than_allocator()(s)
+        &&& RMQCluster::every_in_flight_or_pending_req_msg_has_unique_id()(s)
+        &&& RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s)
+    };
+    RMQCluster::lemma_always_each_object_in_etcd_is_well_formed(spec);
+    RMQCluster::lemma_always_every_in_flight_msg_has_lower_id_than_allocator(spec);
+    RMQCluster::lemma_always_every_in_flight_or_pending_req_msg_has_unique_id(spec);
+    RMQCluster::lemma_always_each_object_in_reconcile_has_consistent_key_and_valid_metadata(spec);
+    combine_spec_entails_always_n!(
+        spec, lift_action(next), lift_action(RMQCluster::next()), lift_state(RMQCluster::each_object_in_etcd_is_well_formed()),
+        lift_state(RMQCluster::every_in_flight_msg_has_lower_id_than_allocator()),
+        lift_state(RMQCluster::every_in_flight_or_pending_req_msg_has_unique_id()),
+        lift_state(RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata())
+    );
+    assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by {
+        if at_rabbitmq_step(key, RabbitmqReconcileStep::AfterGetStatefulSet)(s_prime) {
+            if at_rabbitmq_step(key, RabbitmqReconcileStep::AfterGetStatefulSet)(s) {
+                assert(s.reconcile_state_of(key) == s_prime.reconcile_state_of(key));
+                assert(s_prime.reconcile_state_of(key).pending_req_msg.is_Some());
+                assert(is_get_stateful_set_request(s_prime.pending_req_of(key).content.get_APIRequest_0(), rabbitmq));
+            } else {
+                assert(at_rabbitmq_step(key, RabbitmqReconcileStep::AfterCreateRoleBinding)(s));
+                assert(s_prime.reconcile_state_of(key).pending_req_msg.is_Some());
+                assert(is_get_stateful_set_request(s_prime.pending_req_of(key).content.get_APIRequest_0(), rabbitmq));
+            }
+            assert forall |msg| #[trigger] s_prime.message_in_flight(msg) && Message::resp_msg_matches_req_msg(msg, s_prime.pending_req_of(key))
+            implies sts_get_response_msg(key)(msg) by {
+                let step = choose |step| RMQCluster::next_step(s, s_prime, step);
+                match step {
+                    Step::ControllerStep(input) => {
+                        assert(s.message_in_flight(msg));
+                        let cr_key = input.1.get_Some_0();
+                        if cr_key == key {
+                            assert(s.message_in_flight(msg));
+                            assert(false);
+                        } else {
+                            assert(s.pending_req_of(key) == s_prime.pending_req_of(key));
+                            assert(sts_get_response_msg(key)(msg));
+                        }
+                    },
+                    Step::KubernetesAPIStep(input) => {
+                        assert(s.reconcile_state_of(key) == s_prime.reconcile_state_of(key));
+                        if !s.message_in_flight(msg) {
+                            assert(RMQCluster::in_flight_or_pending_req_message(s, s.pending_req_of(key)));
+                            assert(RMQCluster::in_flight_or_pending_req_message(s, input.get_Some_0()));
+                            assert(is_get_stateful_set_request(s_prime.pending_req_of(key).content.get_APIRequest_0(), rabbitmq));
+                            assert(msg.content.is_get_response());
+                            assert(msg == RMQCluster::handle_get_request(s.pending_req_of(key), s.kubernetes_api_state).1);
+                            assert(msg.src.is_KubernetesAPI()
+                            && msg.content.is_get_response());
+                            if msg.content.get_get_response().res.is_Ok() {
+                                assert(s.resource_key_exists(make_stateful_set_key(key)));
+                                assert(s.resource_obj_of(make_stateful_set_key(key)).object_ref() == make_stateful_set_key(key));
+                            }
+                            assert(sts_get_response_msg(key)(msg));
+                        }
+                    },
+                    Step::KubernetesBusy(input) => {
+                        assert(s.reconcile_state_of(key) == s_prime.reconcile_state_of(key));
+                        if !s.message_in_flight(msg) {
+                            assert(RMQCluster::in_flight_or_pending_req_message(s, s.pending_req_of(key)));
+                            assert(RMQCluster::in_flight_or_pending_req_message(s, input.get_Some_0()));
+                            assert(msg.src.is_KubernetesAPI());
+                            assert(msg.content.is_get_response());
+                            assert(msg.content.get_get_response().res.is_Err());
+                        }
+                        assert(sts_get_response_msg(key)(msg));
+                    },
+                    Step::ClientStep() => {
+                        assert(s.message_in_flight(msg));
+                        assert(sts_get_response_msg(key)(msg));
+                    },
+                    Step::ExternalAPIStep(input) => {
+                        assert(input.get_Some_0() != msg);
+                        assert(s.message_in_flight(msg));
+                    },
+                    _ => {
+                        assert(s.message_in_flight(msg));
+                        assert(sts_get_response_msg(key)(msg));
+                    }
+                }
+            }
+        }
+    }
+    init_invariant(spec, RMQCluster::init(), next, inv);
+}
+
 }