Prove get_step ~> current_state_matches for all subresources of rab…

…bitmq (#323) This PR also proves the stability. After proving these, the left to do is as follows: - Prove that `init ~> get_step` for all sub resources, which should be straightforward. - Combine all subresources and derive the overall `current_state_matches` state. - Put all the invariants in good order. - Prove all the invariants. --------- Signed-off-by: Wenjie Ma <[email protected]>
anvil-verifier · Oct 2, 2023 · 2627417 · 2627417
1 parent e6b6074
commit 2627417
Show file tree

Hide file tree

Showing 27 changed files with 1,323 additions and 1,918 deletions.
diff --git a/e2e/src/rabbitmq_e2e.rs b/e2e/src/rabbitmq_e2e.rs
@@ -404,7 +404,7 @@ pub async fn scaling_test(client: Client, rabbitmq_name: String) -> Result<(), E
             Ok(sts) => {
                 if sts.spec.unwrap().replicas != Some(4) {
                     println!(
-                        "Stateful set spec is not consistent with zookeeper cluster spec yet."
+                        "Stateful set spec is not consistent with rabbitmq cluster spec yet."
                     );
                     continue;
                 }

diff --git a/src/controller_examples/rabbitmq_controller/common/mod.rs b/src/controller_examples/rabbitmq_controller/common/mod.rs
@@ -62,7 +62,7 @@ impl std::marker::Copy for ActionKind {}
 impl std::clone::Clone for ActionKind {
 
     #[verifier(external_body)]
-    fn clone(&self) -> (result: Self) 
+    fn clone(&self) -> (result: Self)
         ensures result == self
     {
         *self

diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/config_map.rs b/src/controller_examples/rabbitmq_controller/exec/resource/config_map.rs
@@ -68,12 +68,7 @@ pub fn update_server_config_map(rabbitmq: &RabbitmqCluster, found_config_map: Co
     let mut config_map = found_config_map.clone();
     let made_server_cm = make_server_config_map(rabbitmq);
 
-    config_map.set_data({
-        let old_data_opt = found_config_map.data();
-        let mut old_data = if old_data_opt.is_some() { old_data_opt.unwrap() } else { StringMap::empty() };
-        old_data.extend(made_server_cm.data().unwrap());
-        old_data
-    });
+    config_map.set_data(made_server_cm.data().unwrap());
     config_map.set_metadata({
         let mut metadata = found_config_map.metadata();
         // The reason why we add these two operations is that it makes the proof easier.

diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/default_user_secret.rs b/src/controller_examples/rabbitmq_controller/exec/resource/default_user_secret.rs
@@ -73,6 +73,7 @@ pub fn update_default_user_secret(rabbitmq: &RabbitmqCluster, found_secret: Secr
         metadata.set_annotations(made_user_secret.metadata().annotations().unwrap());
         metadata
     });
+    user_secret.set_data(make_default_user_secret_data(rabbitmq));
     user_secret
 }
 
@@ -86,12 +87,12 @@ pub fn make_default_user_secret_name(rabbitmq: &RabbitmqCluster) -> (name: Strin
     rabbitmq.name().unwrap().concat(new_strlit("-default-user"))
 }
 
-pub fn make_default_user_secret(rabbitmq: &RabbitmqCluster) -> (secret: Secret)
+pub fn make_default_user_secret_data(rabbitmq: &RabbitmqCluster) -> (data: StringMap)
     requires
         rabbitmq@.metadata.name.is_Some(),
         rabbitmq@.metadata.namespace.is_Some(),
     ensures
-        secret@ == spec_resource::make_default_user_secret(rabbitmq@)
+        data@ == spec_resource::make_default_user_secret_data(rabbitmq@),
 {
     let mut data = StringMap::empty();
     data.insert(new_strlit("username").to_string(), new_strlit("user").to_string());
@@ -104,7 +105,17 @@ pub fn make_default_user_secret(rabbitmq: &RabbitmqCluster) -> (secret: Secret)
     // TODO: check \n
     data.insert(new_strlit("default_user.conf").to_string(), new_strlit("default_user = user\ndefault_pass = changeme").to_string());
     data.insert(new_strlit("port").to_string(), new_strlit("5672").to_string());
-    make_secret(rabbitmq, make_default_user_secret_name(rabbitmq), data)
+    data
+}
+
+pub fn make_default_user_secret(rabbitmq: &RabbitmqCluster) -> (secret: Secret)
+    requires
+        rabbitmq@.metadata.name.is_Some(),
+        rabbitmq@.metadata.namespace.is_Some(),
+    ensures
+        secret@ == spec_resource::make_default_user_secret(rabbitmq@),
+{
+    make_secret(rabbitmq, make_default_user_secret_name(rabbitmq), make_default_user_secret_data(rabbitmq))
 }
 
 }
diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/rabbitmq_plugins.rs b/src/controller_examples/rabbitmq_controller/exec/resource/rabbitmq_plugins.rs
@@ -64,12 +64,7 @@ pub fn update_plugins_config_map(rabbitmq: &RabbitmqCluster, found_config_map: C
 {
     let mut config_map = found_config_map.clone();
     let made_config_map = make_plugins_config_map(rabbitmq);
-    config_map.set_data({
-        let mut data = if found_config_map.data().is_some() { found_config_map.data().unwrap() } else { StringMap::empty() };
-        data.insert(new_strlit("enabled_plugins").to_string(),
-                new_strlit("[rabbitmq_peer_discovery_k8s,rabbitmq_prometheus,rabbitmq_management].").to_string());
-        data
-    });
+    config_map.set_data(made_config_map.data().unwrap());
     config_map.set_metadata({
         let mut metadata = found_config_map.metadata();
         metadata.set_owner_references(make_owner_references(rabbitmq));

diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/service.rs b/src/controller_examples/rabbitmq_controller/exec/resource/service.rs
@@ -76,6 +76,7 @@ pub fn update_main_service(rabbitmq: &RabbitmqCluster, found_main_service: Servi
         metadata.set_annotations(made_service.metadata().annotations().unwrap());
         metadata
     });
+    main_service.set_spec(made_service.spec().unwrap());
     main_service
 }
 

diff --git a/src/controller_examples/rabbitmq_controller/proof/common.rs b/src/controller_examples/rabbitmq_controller/proof/common.rs
@@ -36,76 +36,6 @@ pub open spec fn no_pending_req_at_rabbitmq_step_with_rabbitmq(rabbitmq: Rabbitm
     }
 }
 
-pub open spec fn pending_req_in_flight_at_rabbitmq_step_with_rabbitmq(
-    step: RabbitmqReconcileStep, rabbitmq: RabbitmqClusterView
-) -> StatePred<RMQCluster> {
-    |s: RMQCluster| {
-        &&& at_rabbitmq_step_with_rabbitmq(rabbitmq, step)(s)
-        &&& RMQCluster::pending_k8s_api_req_msg(s, rabbitmq.object_ref())
-        &&& s.in_flight().contains(s.ongoing_reconciles()[rabbitmq.object_ref()].pending_req_msg.get_Some_0())
-        &&& is_correct_pending_request_msg_at_rabbitmq_step(step, s.ongoing_reconciles()[rabbitmq.object_ref()].pending_req_msg.get_Some_0(), rabbitmq)
-    }
-}
-
-pub open spec fn pending_req_with_object_in_flight_at_rabbitmq_step_with_rabbitmq(
-    step: RabbitmqReconcileStep, rabbitmq: RabbitmqClusterView, object: DynamicObjectView
-) -> StatePred<RMQCluster> {
-    |s: RMQCluster| {
-        &&& at_rabbitmq_step_with_rabbitmq(rabbitmq, step)(s)
-        &&& RMQCluster::pending_k8s_api_req_msg(s, rabbitmq.object_ref())
-        &&& s.in_flight().contains(s.ongoing_reconciles()[rabbitmq.object_ref()].pending_req_msg.get_Some_0())
-        &&& is_correct_pending_request_msg_with_object_at_rabbitmq_step(step, s.ongoing_reconciles()[rabbitmq.object_ref()].pending_req_msg.get_Some_0(), rabbitmq, object)
-    }
-}
-
-pub open spec fn req_msg_is_the_in_flight_pending_req_at_rabbitmq_step_with_rabbitmq(
-    step: RabbitmqReconcileStep, rabbitmq: RabbitmqClusterView, req_msg: RMQMessage
-) -> StatePred<RMQCluster> {
-    |s: RMQCluster| {
-        &&& at_rabbitmq_step_with_rabbitmq(rabbitmq, step)(s)
-        &&& RMQCluster::pending_k8s_api_req_msg_is(s, rabbitmq.object_ref(), req_msg)
-        &&& s.in_flight().contains(req_msg)
-        &&& is_correct_pending_request_msg_at_rabbitmq_step(step, req_msg, rabbitmq)
-    }
-}
-
-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: RMQMessage, object: DynamicObjectView
-) -> StatePred<RMQCluster> {
-    |s: RMQCluster| {
-        &&& at_rabbitmq_step_with_rabbitmq(rabbitmq, step)(s)
-        &&& RMQCluster::pending_k8s_api_req_msg_is(s, rabbitmq.object_ref(), req_msg)
-        &&& s.in_flight().contains(req_msg)
-        &&& is_correct_pending_request_msg_with_object_at_rabbitmq_step(step, req_msg, rabbitmq, object)
-    }
-}
-
-pub open spec fn exists_resp_in_flight_at_rabbitmq_step_with_rabbitmq(
-    step: RabbitmqReconcileStep, rabbitmq: RabbitmqClusterView
-) -> StatePred<RMQCluster> {
-    |s: RMQCluster| {
-        &&& at_rabbitmq_step_with_rabbitmq(rabbitmq, step)(s)
-        &&& RMQCluster::pending_k8s_api_req_msg(s, rabbitmq.object_ref())
-        &&& is_correct_pending_request_msg_at_rabbitmq_step(step, s.ongoing_reconciles()[rabbitmq.object_ref()].pending_req_msg.get_Some_0(), rabbitmq)
-        &&& exists |resp_msg| {
-            &&& #[trigger] s.in_flight().contains(resp_msg)
-            &&& Message::resp_msg_matches_req_msg(resp_msg, s.ongoing_reconciles()[rabbitmq.object_ref()].pending_req_msg.get_Some_0())
-        }
-    }
-}
-
-pub open spec fn resp_msg_is_the_in_flight_resp_at_rabbitmq_step_with_rabbitmq(
-    step: RabbitmqReconcileStep, rabbitmq: RabbitmqClusterView, resp_msg: RMQMessage
-) -> StatePred<RMQCluster> {
-    |s: RMQCluster| {
-        &&& at_rabbitmq_step_with_rabbitmq(rabbitmq, step)(s)
-        &&& RMQCluster::pending_k8s_api_req_msg(s, rabbitmq.object_ref())
-        &&& is_correct_pending_request_msg_at_rabbitmq_step(step, s.ongoing_reconciles()[rabbitmq.object_ref()].pending_req_msg.get_Some_0(), rabbitmq)
-        &&& s.in_flight().contains(resp_msg)
-        &&& Message::resp_msg_matches_req_msg(resp_msg, s.ongoing_reconciles()[rabbitmq.object_ref()].pending_req_msg.get_Some_0())
-    }
-}
-
 pub open spec fn is_correct_pending_request_msg_at_rabbitmq_step(
     step: RabbitmqReconcileStep, msg: RMQMessage, rabbitmq: RabbitmqClusterView
 ) -> bool {

diff --git a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/predicate.rs b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/predicate.rs
@@ -40,77 +40,42 @@ pub open spec fn object_of_key_has_no_finalizers_or_timestamp_and_only_has_contr
     }
 }
 
-pub open spec fn resource_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 == key.namespace
-        && msg.content.get_create_request().obj.metadata.name.get_Some_0() == key.name
-        && msg.content.get_create_request().obj.kind == key.kind
-}
-
-pub open spec fn resource_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() == key
-}
-
-pub open spec fn every_resource_object_in_create_request_does_the_make_method(sub_resource: SubResource, rabbitmq: RabbitmqClusterView) -> StatePred<RMQCluster>
+pub open spec fn every_resource_create_request_implies_at_after_create_resource_step(sub_resource: SubResource, rabbitmq: RabbitmqClusterView) -> StatePred<RMQCluster>
     recommends
         rabbitmq.well_formed(),
 {
     |s: RMQCluster| {
         let key = rabbitmq.object_ref();
         let resource_key = get_request(sub_resource, rabbitmq).key;
-        let made_object = make(sub_resource, rabbitmq, s.ongoing_reconciles()[key].local_state);
         forall |msg: RMQMessage| {
             &&& #[trigger] s.network_state.in_flight.contains(msg)
             &&& resource_create_request_msg(resource_key)(msg)
         } ==> {
             &&& at_rabbitmq_step(key, RabbitmqReconcileStep::AfterKRequestStep(ActionKind::Create, sub_resource))(s)
-            &&& RMQCluster::pending_k8s_api_req_msg(s, key)
-            &&& msg == s.ongoing_reconciles()[key].pending_req_msg.get_Some_0()
-            &&& made_object.is_Ok()
-            &&& msg.content.get_create_request().obj == made_object.get_Ok_0()
+            &&& RMQCluster::pending_k8s_api_req_msg_is(s, key, msg)
+            &&& make(sub_resource, rabbitmq, s.ongoing_reconciles()[key].local_state).is_Ok()
+            &&& msg.content.get_create_request().obj == make(sub_resource, rabbitmq, s.ongoing_reconciles()[key].local_state).get_Ok_0()
         }
-            // A reminder: The last predicate implies:
-            // && msg.content.get_create_request().obj.metadata.owner_references == Some(seq![rabbitmq.controller_owner_ref()])
     }
 }
 
-/// We have to impose constraint on the resource version of update request message now instead of making no distinction
-/// to update request messages before. This is because we don't update the whole spec/data for the object now (we only update
-/// part of the fields).
-///
-/// Note that in order to prove this invariant, we should take advantage of every get response message, if with the same rv,
-/// has the same object as etcd.
-///
-/// Also, with the invariant proved, we also need to prove for every resource builder, (!!at the update step!!) the updated object
-/// (as long as the non-metadata part) matches the desired state.
-pub open spec fn every_resource_object_in_update_request_does_the_update_method(sub_resource: SubResource, rabbitmq: RabbitmqClusterView) -> StatePred<RMQCluster>
+pub open spec fn every_resource_update_request_implies_at_after_update_resource_step(sub_resource: SubResource, rabbitmq: RabbitmqClusterView) -> StatePred<RMQCluster>
     recommends
         rabbitmq.well_formed(),
 {
     |s: RMQCluster| {
         let key = rabbitmq.object_ref();
         let resource_key = get_request(sub_resource, rabbitmq).key;
-        let resources = s.resources();
-        let updated_obj = update(sub_resource, rabbitmq, s.ongoing_reconciles()[key].local_state, resources[resource_key]);
         forall |msg: RMQMessage| {
             &&& #[trigger] s.network_state.in_flight.contains(msg)
             &&& resource_update_request_msg(resource_key)(msg)
-            &&& resources.contains_key(resource_key)
-            &&& msg.content.get_update_request().obj.metadata.resource_version.get_Some_0() == resources[resource_key].metadata.resource_version.get_Some_0()
         } ==> {
             &&& at_rabbitmq_step(key, RabbitmqReconcileStep::AfterKRequestStep(ActionKind::Update, sub_resource))(s)
-            &&& RMQCluster::pending_k8s_api_req_msg(s, key)
-            &&& msg == s.ongoing_reconciles()[key].pending_req_msg.get_Some_0()
-            &&& updated_obj.is_Ok()
-            &&& msg.content.get_update_request().obj == updated_obj.get_Ok_0()
+            &&& RMQCluster::pending_k8s_api_req_msg_is(s, key, msg)
+            &&& s.resources().contains_key(resource_key)
+            &&& update(sub_resource, rabbitmq, s.ongoing_reconciles()[key].local_state, s.resources()[resource_key]).is_Ok()
+            &&& msg.content.get_update_request().obj == update(sub_resource, rabbitmq, s.ongoing_reconciles()[key].local_state, s.resources()[resource_key]).get_Ok_0()
         }
-            // A reminder: The last predicate implies:
-            // && msg.content.get_update_request().obj.metadata.owner_references == Some(seq![rabbitmq.controller_owner_ref()])
     }
 }
 
@@ -132,6 +97,17 @@ pub open spec fn no_delete_request_msg_in_flight_with_key(key: ObjectRef) -> Sta
     }
 }
 
+pub open spec fn no_update_status_request_msg_in_flight_with_key(key: ObjectRef) -> StatePred<RMQCluster> {
+    |s: RMQCluster| {
+        forall |msg: RMQMessage| !{
+            &&& #[trigger] s.in_flight().contains(msg)
+            &&& msg.dst.is_KubernetesAPI()
+            &&& msg.content.is_update_status_request()
+            &&& msg.content.get_update_status_request().key() == key
+        }
+    }
+}
+
 /// We only need it for AfterGetStatefulSet, but keeping all the steps makes the invariant easier to prove.
 pub open spec fn cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(rabbitmq: RabbitmqClusterView) -> StatePred<RMQCluster> {
     |s: RMQCluster| {
@@ -144,6 +120,7 @@ pub open spec fn cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(rabbitmq: Rab
                     SubResource::ServiceAccount | SubResource::Role | SubResource::RoleBinding | SubResource::StatefulSet => {
                         let cm_key = get_request(SubResource::ServerConfigMap, rabbitmq).key;
                         &&& s.resources().contains_key(cm_key)
+                        &&& s.resources()[cm_key].metadata.resource_version.is_Some()
                         &&& local_state.latest_config_map_rv_opt == Some(int_to_string_view(s.resources()[cm_key].metadata.resource_version.get_Some_0()))
                     },
                     _ => true,
@@ -154,4 +131,21 @@ pub open spec fn cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(rabbitmq: Rab
     }
 }
 
+pub open spec fn object_in_etcd_satisfies_unchangeable(sub_resource: SubResource, rabbitmq: RabbitmqClusterView) -> StatePred<RMQCluster> {
+    |s: RMQCluster| {
+        s.resources().contains_key(get_request(sub_resource, rabbitmq).key)
+        ==> unchangeable(sub_resource, s.resources()[get_request(sub_resource, rabbitmq).key], rabbitmq)
+    }
+}
+
+pub open spec fn cm_rv_stays_unchanged(rabbitmq: RabbitmqClusterView) -> ActionPred<RMQCluster> {
+    |s: RMQCluster, s_prime: RMQCluster| {
+        let cm_key = get_request(SubResource::ServerConfigMap, rabbitmq).key;
+        &&& s.resources().contains_key(cm_key)
+        &&& s_prime.resources().contains_key(cm_key)
+        &&& s.resources()[cm_key].metadata.resource_version.is_Some()
+        &&& s.resources()[cm_key].metadata.resource_version == s_prime.resources()[cm_key].metadata.resource_version
+    }
+}
+
 }