Set a boundary between trusted and verified for RabbitMQ controller

Signed-off-by: Xudong Sun <[email protected]>
anvil-verifier · Nov 13, 2023 · c143657 · c143657
1 parent 3eed7dd
commit c143657
Show file tree

Hide file tree

Showing 53 changed files with 310 additions and 196 deletions.
diff --git a/src/controller_examples/fluent_controller/fluentbit/exec/reconciler.rs b/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 {
+        fb@.well_formed()
+    }
+
     fn reconcile_init_state() -> FluentBitReconcileState {
         reconcile_init_state()
     }

diff --git a/src/controller_examples/fluent_controller/fluentbit_config/exec/reconciler.rs b/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 {
+        fbc@.well_formed()
+    }
+
     fn reconcile_init_state() -> FluentBitConfigReconcileState {
         reconcile_init_state()
     }

diff --git a/src/controller_examples/rabbitmq_controller/exec/mod.rs b/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;
diff --git a/src/controller_examples/rabbitmq_controller/exec/reconciler.rs b/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::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 {
+        rabbitmq@.well_formed()
+    }
+
     fn reconcile_init_state() -> RabbitmqReconcileState {
         reconcile_init_state()
     }

diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/common.rs b/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::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::*;

diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/config_map.rs b/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::trusted::exec_types::*;
+use crate::rabbitmq_controller::trusted::spec_types::RabbitmqClusterView;
+use crate::rabbitmq_controller::trusted::step::*;
 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::reconciler::exec::{io::*, reconciler::*, resource_builder::*};
 use crate::vstd_ext::string_map::StringMap;
 use crate::vstd_ext::string_view::*;

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
@@ -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::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::*;

diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/erlang_cookie.rs b/src/controller_examples/rabbitmq_controller/exec/resource/erlang_cookie.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::default_user_secret::DefaultUserSecretBuilder;
-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::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::*;

diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/headless_service.rs b/src/controller_examples/rabbitmq_controller/exec/resource/headless_service.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::ServiceBuilder;
-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::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::*;

diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/rabbitmq_plugins.rs b/src/controller_examples/rabbitmq_controller/exec/resource/rabbitmq_plugins.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::config_map::ServerConfigMapBuilder;
-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::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::*;

diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/role.rs b/src/controller_examples/rabbitmq_controller/exec/resource/role.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::role_binding::RoleBindingBuilder;
-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::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::*;

diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/role_binding.rs b/src/controller_examples/rabbitmq_controller/exec/resource/role_binding.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::stateful_set::StatefulSetBuilder;
-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::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::*;

diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/service.rs b/src/controller_examples/rabbitmq_controller/exec/resource/service.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::erlang_cookie::ErlangCookieBuilder;
-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::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::*;

diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/service_account.rs b/src/controller_examples/rabbitmq_controller/exec/resource/service_account.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::role::RoleBuilder;
-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::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::*;

diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/stateful_set.rs b/src/controller_examples/rabbitmq_controller/exec/resource/stateful_set.rs
@@ -8,10 +8,10 @@ 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::spec::types::RabbitmqClusterView;
+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::*;

diff --git a/src/controller_examples/rabbitmq_controller/mod.rs b/src/controller_examples/rabbitmq_controller/mod.rs
@@ -1,6 +1,6 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-pub mod common;
 pub mod exec;
 pub mod proof;
 pub mod spec;
+pub mod trusted;
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
@@ -14,13 +14,13 @@ use crate::kubernetes_cluster::spec::{
     message::*,
 };
 use crate::rabbitmq_controller::{
-    common::*,
     proof::{
         helper_invariants::{predicate::*, proof::*},
         predicate::*,
         resource::*,
     },
-    spec::{reconciler::*, types::*},
+    spec::reconciler::*,
+    trusted::{spec_types::*, step::*},
 };
 use crate::temporal_logic::{defs::*, rules::*};
 use vstd::prelude::*;

diff --git a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/predicate.rs b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/predicate.rs
@@ -13,9 +13,9 @@ use crate::kubernetes_cluster::spec::{
     message::*,
 };
 use crate::rabbitmq_controller::{
-    common::*,
     proof::{predicate::*, resource::*},
-    spec::{reconciler::*, types::*},
+    spec::reconciler::*,
+    trusted::{spec_types::*, step::*},
 };
 use crate::reconciler::spec::reconciler::*;
 use crate::temporal_logic::{defs::*, rules::*};

diff --git a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/proof.rs b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/proof.rs
@@ -12,12 +12,11 @@ use crate::kubernetes_cluster::spec::{
     message::*,
 };
 use crate::rabbitmq_controller::{
-    common::*,
     proof::{
-        helper_invariants::stateful_set_in_etcd_satisfies_unchangeable,
-        liveness_theorem::desired_state_is, predicate::*, resource::*,
+        helper_invariants::stateful_set_in_etcd_satisfies_unchangeable, predicate::*, resource::*,
     },
-    spec::{resource::make_stateful_set, types::*},
+    spec::resource::make_stateful_set,
+    trusted::{liveness_theorem::desired_state_is, spec_types::*, step::*},
 };
 use crate::temporal_logic::{defs::*, rules::*};
 use crate::vstd_ext::{multiset_lib, seq_lib, string_view::*};

diff --git a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/unchangeable.rs b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/unchangeable.rs
@@ -12,13 +12,13 @@ use crate::kubernetes_cluster::spec::{
     message::*,
 };
 use crate::rabbitmq_controller::{
-    common::*,
     proof::{
         helper_invariants::{owner_ref::*, predicate::*, proof::*, validation::*},
         predicate::*,
         resource::*,
     },
-    spec::{reconciler::*, resource::*, types::*},
+    spec::{reconciler::*, resource::*},
+    trusted::{spec_types::*, step::*},
 };
 use crate::reconciler::spec::{reconciler::*, resource_builder::*};
 use crate::temporal_logic::{defs::*, rules::*};

diff --git a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/validation.rs b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/validation.rs
@@ -13,13 +13,13 @@ use crate::kubernetes_cluster::spec::{
     message::*,
 };
 use crate::rabbitmq_controller::{
-    common::*,
     proof::{
         helper_invariants::{owner_ref::*, predicate::*, proof::*},
         predicate::*,
         resource::*,
     },
-    spec::{reconciler::*, resource::*, types::*},
+    spec::{reconciler::*, resource::*},
+    trusted::{spec_types::*, step::*},
 };
 use crate::reconciler::spec::{reconciler::*, resource_builder::*};
 use crate::temporal_logic::{defs::*, rules::*};