Set a boundary between trusted and verified for RabbitMQ controller (#…

…414)

After this PR our rabbitmq controller example consists of four folders:
- `trusted`: all the trusted code, including the top-level theorems and
unverified wrapper object (like vstd::Vec).
- `exec`: the executable code that is verified.
- `model`: the ghost version of the executable code. This is not
trusted.
- `proof`: the proof for liveness (and safety).

Notably, files in `trusted` only import other files from `trusted` or
Anvil's trusted specs---they don't import anything from `exec`, `model`,
or `proof`. Everything outside `trusted` is verified---they don't have
any `external` or `external_body` proof functions.

After this refactoring, the liveness theorem inside `trusted` now takes
a Maker trait as a placeholder for the sub-resource objects created by
the controller implementation:
```
pub open spec fn liveness<M: Maker>(rabbitmq: RabbitmqClusterView) -> TempPred<RMQCluster> {
    always(lift_state(desired_state_is(rabbitmq))).leads_to(always(lift_state(current_state_matches::<M>(rabbitmq))))
}

...

pub open spec fn current_state_matches<M: Maker>(rabbitmq: RabbitmqClusterView) -> StatePred<RMQCluster> {
    |s: RMQCluster| {
        forall |sub_resource: SubResource|
            #[trigger] resource_state_matches::<M>(sub_resource, rabbitmq, s.resources())
    }
}

pub open spec fn resource_state_matches<M: Maker>(sub_resource: SubResource, rabbitmq: RabbitmqClusterView, resources: StoredState) -> bool {
    match sub_resource {
        SubResource::HeadlessService => {
            ...
            &&& obj.metadata.labels == M::make_headless_service(rabbitmq).metadata.labels
            &&& obj.metadata.annotations == M::make_headless_service(rabbitmq).metadata.annotations
        },
        ...
    }
}
```
And our liveness proof inside `proof` instantiates this theorem with the
concrete maker `RabbitmqMaker` and proves it:
```
proof fn liveness_proof_forall_rabbitmq()
    ensures
        liveness_theorem::<RabbitmqMaker>(),
{ ... }
```

`Maker` trait is defined inside `trusted` and `RabbitmqMaker` (which
implements `Maker`) is not in `trusted`.

---------

Signed-off-by: Xudong Sun <[email protected]>

src/controller_examples/fluent_controller/fluentbit/exec/reconciler.rs

@@ -19,8 +19,11 @@ verus! {
 
 pub struct FluentBitReconciler {}
 
-#[verifier(external)]
 impl Reconciler<FluentBit, FluentBitReconcileState, EmptyType, EmptyType, EmptyAPIShimLayer> for FluentBitReconciler {
+    open spec fn well_formed(fb: &FluentBit) -> bool {
+        [email protected]_formed()
+    }
+
     fn reconcile_init_state() -> FluentBitReconcileState {
         reconcile_init_state()
     }

src/controller_examples/fluent_controller/fluentbit_config/exec/reconciler.rs

@@ -19,8 +19,11 @@ verus! {
 
 pub struct FluentBitConfigReconciler {}
 
-#[verifier(external)]
 impl Reconciler<FluentBitConfig, FluentBitConfigReconcileState, EmptyType, EmptyType, EmptyAPIShimLayer> for FluentBitConfigReconciler {
+    open spec fn well_formed(fbc: &FluentBitConfig) -> bool {
+        [email protected]_formed()
+    }
+
     fn reconcile_init_state() -> FluentBitConfigReconcileState {
         reconcile_init_state()
     }

src/controller_examples/rabbitmq_controller/exec/mod.rs

@@ -2,4 +2,3 @@
 // SPDX-License-Identifier: MIT
 pub mod reconciler;
 pub mod resource;
-pub mod types;

src/controller_examples/rabbitmq_controller/exec/reconciler.rs

@@ -7,12 +7,12 @@ use crate::kubernetes_api_objects::{
     container::*, label_selector::*, pod_template_spec::*, prelude::*, resource_requirements::*,
     volume::*,
 };
-use crate::rabbitmq_controller::common::*;
 use crate::rabbitmq_controller::exec::resource::*;
-use crate::rabbitmq_controller::exec::types::*;
-use crate::rabbitmq_controller::spec::reconciler as rabbitmq_spec;
-use crate::rabbitmq_controller::spec::resource as spec_resource;
-use crate::rabbitmq_controller::spec::types as spec_types;
+use crate::rabbitmq_controller::model::reconciler as model_reconciler;
+use crate::rabbitmq_controller::model::resource as model_resource;
+use crate::rabbitmq_controller::trusted::exec_types::*;
+use crate::rabbitmq_controller::trusted::spec_types;
+use crate::rabbitmq_controller::trusted::step::*;
 use crate::reconciler::exec::{io::*, reconciler::*, resource_builder::*};
 use crate::reconciler::spec::resource_builder::ResourceBuilder as SpecResourceBuilder;
 use crate::vstd_ext::{string_map::StringMap, string_view::*};
@@ -24,8 +24,11 @@ verus! {
 
 pub struct RabbitmqReconciler {}
 
-#[verifier(external)]
 impl Reconciler<RabbitmqCluster, RabbitmqReconcileState, EmptyType, EmptyType, EmptyAPIShimLayer> for RabbitmqReconciler {
+    open spec fn well_formed(rabbitmq: &RabbitmqCluster) -> bool {
+        [email protected]_formed()
+    }
+
     fn reconcile_init_state() -> RabbitmqReconcileState {
         reconcile_init_state()
     }
@@ -48,7 +51,7 @@ impl Default for RabbitmqReconciler {
 }
 
 pub fn reconcile_init_state() -> (state: RabbitmqReconcileState)
-    ensures state@ == rabbitmq_spec::reconcile_init_state(),
+    ensures state@ == model_reconciler::reconcile_init_state(),
 {
     RabbitmqReconcileState {
         reconcile_step: RabbitmqReconcileStep::Init,
@@ -57,7 +60,7 @@ pub fn reconcile_init_state() -> (state: RabbitmqReconcileState)
 }
 
 pub fn reconcile_done(state: &RabbitmqReconcileState) -> (res: bool)
-    ensures res == rabbitmq_spec::reconcile_done(state@),
+    ensures res == model_reconciler::reconcile_done(state@),
 {
     match state.reconcile_step {
         RabbitmqReconcileStep::Done => true,
@@ -66,7 +69,7 @@ pub fn reconcile_done(state: &RabbitmqReconcileState) -> (res: bool)
 }
 
 pub fn reconcile_error(state: &RabbitmqReconcileState) -> (res: bool)
-    ensures res == rabbitmq_spec::reconcile_error(state@),
+    ensures res == model_reconciler::reconcile_error(state@),
 {
     match state.reconcile_step {
         RabbitmqReconcileStep::Error => true,
@@ -76,7 +79,7 @@ pub fn reconcile_error(state: &RabbitmqReconcileState) -> (res: bool)
 
 pub fn reconcile_core(rabbitmq: &RabbitmqCluster, resp_o: Option<Response<EmptyType>>, state: RabbitmqReconcileState) -> (res: (RabbitmqReconcileState, Option<Request<EmptyType>>))
     requires [email protected]_formed(),
-    ensures (res.0@, opt_request_to_view(&res.1)) == rabbitmq_spec::reconcile_core(rabbitmq@, opt_response_to_view(&resp_o), state@),
+    ensures (res.0@, opt_request_to_view(&res.1)) == model_reconciler::reconcile_core(rabbitmq@, opt_response_to_view(&resp_o), state@),
         // resource_version_check(opt_response_to_view(&resp_o), opt_request_to_view(&res.1)),
 {
     match &state.reconcile_step {
@@ -90,16 +93,16 @@ pub fn reconcile_core(rabbitmq: &RabbitmqCluster, resp_o: Option<Response<EmptyT
         },
         RabbitmqReconcileStep::AfterKRequestStep(_, resource) => {
             match resource {
-                SubResource::HeadlessService => reconcile_helper::<spec_resource::HeadlessServiceBuilder, HeadlessServiceBuilder>(rabbitmq, resp_o, state),
-                SubResource::Service => reconcile_helper::<spec_resource::ServiceBuilder, ServiceBuilder>(rabbitmq, resp_o, state),
-                SubResource::ErlangCookieSecret => reconcile_helper::<spec_resource::ErlangCookieBuilder, ErlangCookieBuilder>(rabbitmq, resp_o, state),
-                SubResource::DefaultUserSecret => reconcile_helper::<spec_resource::DefaultUserSecretBuilder, DefaultUserSecretBuilder>(rabbitmq, resp_o, state),
-                SubResource::PluginsConfigMap => reconcile_helper::<spec_resource::PluginsConfigMapBuilder, PluginsConfigMapBuilder>(rabbitmq, resp_o, state),
-                SubResource::ServerConfigMap => reconcile_helper::<spec_resource::ServerConfigMapBuilder, ServerConfigMapBuilder>(rabbitmq, resp_o, state),
-                SubResource::ServiceAccount => reconcile_helper::<spec_resource::ServiceAccountBuilder, ServiceAccountBuilder>(rabbitmq, resp_o, state),
-                SubResource::Role => reconcile_helper::<spec_resource::RoleBuilder, RoleBuilder>(rabbitmq, resp_o, state),
-                SubResource::RoleBinding => reconcile_helper::<spec_resource::RoleBindingBuilder, RoleBindingBuilder>(rabbitmq, resp_o, state),
-                SubResource::StatefulSet => reconcile_helper::<spec_resource::StatefulSetBuilder, StatefulSetBuilder>(rabbitmq, resp_o, state),
+                SubResource::HeadlessService => reconcile_helper::<model_resource::HeadlessServiceBuilder, HeadlessServiceBuilder>(rabbitmq, resp_o, state),
+                SubResource::Service => reconcile_helper::<model_resource::ServiceBuilder, ServiceBuilder>(rabbitmq, resp_o, state),
+                SubResource::ErlangCookieSecret => reconcile_helper::<model_resource::ErlangCookieBuilder, ErlangCookieBuilder>(rabbitmq, resp_o, state),
+                SubResource::DefaultUserSecret => reconcile_helper::<model_resource::DefaultUserSecretBuilder, DefaultUserSecretBuilder>(rabbitmq, resp_o, state),
+                SubResource::PluginsConfigMap => reconcile_helper::<model_resource::PluginsConfigMapBuilder, PluginsConfigMapBuilder>(rabbitmq, resp_o, state),
+                SubResource::ServerConfigMap => reconcile_helper::<model_resource::ServerConfigMapBuilder, ServerConfigMapBuilder>(rabbitmq, resp_o, state),
+                SubResource::ServiceAccount => reconcile_helper::<model_resource::ServiceAccountBuilder, ServiceAccountBuilder>(rabbitmq, resp_o, state),
+                SubResource::Role => reconcile_helper::<model_resource::RoleBuilder, RoleBuilder>(rabbitmq, resp_o, state),
+                SubResource::RoleBinding => reconcile_helper::<model_resource::RoleBindingBuilder, RoleBindingBuilder>(rabbitmq, resp_o, state),
+                SubResource::StatefulSet => reconcile_helper::<model_resource::StatefulSetBuilder, StatefulSetBuilder>(rabbitmq, resp_o, state),
             }
         },
         _ => {
@@ -120,7 +123,7 @@ pub fn reconcile_helper<
         Builder::requirements(rabbitmq@),
         state.reconcile_step.is_AfterKRequestStep(),
     ensures
-        (res.0@, opt_request_to_view(&res.1)) == rabbitmq_spec::reconcile_helper::<SpecBuilder>(rabbitmq@, opt_response_to_view(&resp_o), state@),
+        (res.0@, opt_request_to_view(&res.1)) == model_reconciler::reconcile_helper::<SpecBuilder>(rabbitmq@, opt_response_to_view(&resp_o), state@),
 {
     let step = state.reconcile_step.clone();
     match step {

src/controller_examples/rabbitmq_controller/exec/resource/common.rs

@@ -7,9 +7,9 @@ use crate::kubernetes_api_objects::{
     container::*, label_selector::*, pod_template_spec::*, prelude::*, resource_requirements::*,
     volume::*,
 };
-use crate::rabbitmq_controller::common::*;
-use crate::rabbitmq_controller::exec::types::*;
-use crate::rabbitmq_controller::spec::resource as spec_resource;
+use crate::rabbitmq_controller::model::resource as model_resource;
+use crate::rabbitmq_controller::trusted::exec_types::*;
+use crate::rabbitmq_controller::trusted::step::*;
 use crate::reconciler::exec::{io::*, reconciler::*};
 use crate::vstd_ext::{string_map::StringMap, string_view::*};
 use vstd::prelude::*;
@@ -22,7 +22,7 @@ pub fn make_labels(rabbitmq: &RabbitmqCluster) -> (labels: StringMap)
     requires
         [email protected]_Some(),
     ensures
-        labels@ == spec_resource::make_labels(rabbitmq@),
+        labels@ == model_resource::make_labels(rabbitmq@),
 {
     let mut labels = rabbitmq.spec().labels();
     labels.insert(new_strlit("app").to_string(), rabbitmq.metadata().name().unwrap());
@@ -34,14 +34,14 @@ pub fn make_owner_references(rabbitmq: &RabbitmqCluster) -> (owner_references: V
         [email protected]_Some(),
         [email protected]_Some(),
     ensures
-        [email protected]_values(|or: OwnerReference| or@) ==  spec_resource::make_owner_references(rabbitmq@),
+        [email protected]_values(|or: OwnerReference| or@) ==  model_resource::make_owner_references(rabbitmq@),
 {
     let mut owner_references = Vec::new();
     owner_references.push(rabbitmq.controller_owner_ref());
     proof {
         assert_seqs_equal!(
             [email protected]_values(|owner_ref: OwnerReference| owner_ref@),
-            spec_resource::make_owner_references(rabbitmq@)
+            model_resource::make_owner_references(rabbitmq@)
         );
     }
     owner_references
@@ -52,7 +52,7 @@ pub fn make_secret(rabbitmq: &RabbitmqCluster, name:String , data: StringMap) ->
         [email protected]_Some(),
         [email protected]_Some(),
     ensures
-        secret@ == spec_resource::make_secret(rabbitmq@, name@, data@)
+        secret@ == model_resource::make_secret(rabbitmq@, name@, data@)
 {
     let mut secret = Secret::default();
     secret.set_metadata({
@@ -73,7 +73,7 @@ pub fn make_service(rabbitmq: &RabbitmqCluster, name:String, ports: Vec<ServiceP
         [email protected]_Some(),
         [email protected]_Some(),
     ensures
-        service@ == spec_resource::make_service(rabbitmq@, name@, [email protected]_values(|port: ServicePort| port@), cluster_ip)
+        service@ == model_resource::make_service(rabbitmq@, name@, [email protected]_values(|port: ServicePort| port@), cluster_ip)
 {
     let mut service = Service::default();
     service.set_metadata({

src/controller_examples/rabbitmq_controller/exec/resource/config_map.rs

@@ -8,11 +8,11 @@ use crate::kubernetes_api_objects::{
     container::*, label_selector::*, pod_template_spec::*, prelude::*, resource_requirements::*,
     volume::*,
 };
-use crate::rabbitmq_controller::common::*;
 use crate::rabbitmq_controller::exec::resource::service_account::ServiceAccountBuilder;
-use crate::rabbitmq_controller::exec::types::*;
-use crate::rabbitmq_controller::spec::resource as spec_resource;
-use crate::rabbitmq_controller::spec::types::RabbitmqClusterView;
+use crate::rabbitmq_controller::model::resource as model_resource;
+use crate::rabbitmq_controller::trusted::exec_types::*;
+use crate::rabbitmq_controller::trusted::spec_types::RabbitmqClusterView;
+use crate::rabbitmq_controller::trusted::step::*;
 use crate::reconciler::exec::{io::*, reconciler::*, resource_builder::*};
 use crate::vstd_ext::string_map::StringMap;
 use crate::vstd_ext::string_view::*;
@@ -24,7 +24,7 @@ verus! {
 
 pub struct ServerConfigMapBuilder {}
 
-impl ResourceBuilder<RabbitmqCluster, RabbitmqReconcileState, spec_resource::ServerConfigMapBuilder> for ServerConfigMapBuilder {
+impl ResourceBuilder<RabbitmqCluster, RabbitmqReconcileState, model_resource::ServerConfigMapBuilder> for ServerConfigMapBuilder {
     open spec fn requirements(rabbitmq: RabbitmqClusterView) -> bool {
         &&& rabbitmq.metadata.name.is_Some()
         &&& rabbitmq.metadata.namespace.is_Some()
@@ -87,7 +87,7 @@ pub fn update_server_config_map(rabbitmq: &RabbitmqCluster, found_config_map: Co
         [email protected]_Some(),
         [email protected]_Some(),
     ensures
-        config_map@ == spec_resource::update_server_config_map(rabbitmq@, found_config_map@),
+        config_map@ == model_resource::update_server_config_map(rabbitmq@, found_config_map@),
 {
     let mut config_map = found_config_map.clone();
     let made_server_cm = make_server_config_map(rabbitmq);
@@ -112,7 +112,7 @@ pub fn make_server_config_map_name(rabbitmq: &RabbitmqCluster) -> (name: String)
         [email protected]_Some(),
         [email protected]_Some(),
     ensures
-        name@ == spec_resource::make_server_config_map_name(rabbitmq@),
+        name@ == model_resource::make_server_config_map_name(rabbitmq@),
 {
     rabbitmq.metadata().name().unwrap().concat(new_strlit("-server-conf"))
 }
@@ -122,7 +122,7 @@ pub fn make_server_config_map(rabbitmq: &RabbitmqCluster) -> (config_map: Config
         [email protected]_Some(),
         [email protected]_Some(),
     ensures
-        config_map@ == spec_resource::make_server_config_map(rabbitmq@),
+        config_map@ == model_resource::make_server_config_map(rabbitmq@),
 {
     let mut config_map = ConfigMap::default();
     config_map.set_metadata({
@@ -165,7 +165,7 @@ pub fn default_rbmq_config(rabbitmq: &RabbitmqCluster) -> (s: String)
         [email protected]_Some(),
         [email protected]_Some(),
     ensures
-        s@ == spec_resource::default_rbmq_config(rabbitmq@),
+        s@ == model_resource::default_rbmq_config(rabbitmq@),
 {
     new_strlit(
         "queue_master_locator = min-masters\n\

src/controller_examples/rabbitmq_controller/exec/resource/default_user_secret.rs

@@ -8,11 +8,11 @@ use crate::kubernetes_api_objects::{
     container::*, label_selector::*, pod_template_spec::*, prelude::*, resource_requirements::*,
     volume::*,
 };
-use crate::rabbitmq_controller::common::*;
 use crate::rabbitmq_controller::exec::resource::rabbitmq_plugins::PluginsConfigMapBuilder;
-use crate::rabbitmq_controller::exec::types::*;
-use crate::rabbitmq_controller::spec::resource as spec_resource;
-use crate::rabbitmq_controller::spec::types::RabbitmqClusterView;
+use crate::rabbitmq_controller::model::resource as model_resource;
+use crate::rabbitmq_controller::trusted::exec_types::*;
+use crate::rabbitmq_controller::trusted::spec_types::RabbitmqClusterView;
+use crate::rabbitmq_controller::trusted::step::*;
 use crate::reconciler::exec::{io::*, reconciler::*, resource_builder::*};
 use crate::vstd_ext::string_map::StringMap;
 use crate::vstd_ext::string_view::*;
@@ -24,7 +24,7 @@ verus! {
 
 pub struct DefaultUserSecretBuilder {}
 
-impl ResourceBuilder<RabbitmqCluster, RabbitmqReconcileState, spec_resource::DefaultUserSecretBuilder> for DefaultUserSecretBuilder {
+impl ResourceBuilder<RabbitmqCluster, RabbitmqReconcileState, model_resource::DefaultUserSecretBuilder> for DefaultUserSecretBuilder {
     open spec fn requirements(rabbitmq: RabbitmqClusterView) -> bool {
         &&& rabbitmq.metadata.name.is_Some()
         &&& rabbitmq.metadata.namespace.is_Some()
@@ -85,7 +85,7 @@ pub fn update_default_user_secret(rabbitmq: &RabbitmqCluster, found_secret: Secr
         [email protected]_Some(),
         [email protected]_Some(),
     ensures
-        secret@ == spec_resource::update_default_user_secret(rabbitmq@, found_secret@),
+        secret@ == model_resource::update_default_user_secret(rabbitmq@, found_secret@),
 {
     let mut user_secret = found_secret.clone();
     let made_user_secret = make_default_user_secret(rabbitmq);
@@ -107,7 +107,7 @@ pub fn make_default_user_secret_name(rabbitmq: &RabbitmqCluster) -> (name: Strin
         [email protected]_Some(),
         [email protected]_Some(),
     ensures
-        name@ == spec_resource::make_default_user_secret_name(rabbitmq@),
+        name@ == model_resource::make_default_user_secret_name(rabbitmq@),
 {
     rabbitmq.metadata().name().unwrap().concat(new_strlit("-default-user"))
 }
@@ -117,7 +117,7 @@ pub fn make_default_user_secret_data(rabbitmq: &RabbitmqCluster) -> (data: Strin
         [email protected]_Some(),
         [email protected]_Some(),
     ensures
-        data@ == spec_resource::make_default_user_secret_data(rabbitmq@),
+        data@ == model_resource::make_default_user_secret_data(rabbitmq@),
 {
     let mut data = StringMap::empty();
     data.insert(new_strlit("username").to_string(), new_strlit("user").to_string());
@@ -138,7 +138,7 @@ pub fn make_default_user_secret(rabbitmq: &RabbitmqCluster) -> (secret: Secret)
         [email protected]_Some(),
         [email protected]_Some(),
     ensures
-        secret@ == spec_resource::make_default_user_secret(rabbitmq@),
+        secret@ == model_resource::make_default_user_secret(rabbitmq@),
 {
     make_secret(rabbitmq, make_default_user_secret_name(rabbitmq), make_default_user_secret_data(rabbitmq))
 }