From dfb8a6f8905c957393cb5b879f4fab643aa439c6 Mon Sep 17 00:00:00 2001 From: Xudong Sun Date: Tue, 14 Nov 2023 13:36:19 -0600 Subject: [PATCH] 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(rabbitmq: RabbitmqClusterView) -> TempPred { always(lift_state(desired_state_is(rabbitmq))).leads_to(always(lift_state(current_state_matches::(rabbitmq)))) } ... pub open spec fn current_state_matches(rabbitmq: RabbitmqClusterView) -> StatePred { |s: RMQCluster| { forall |sub_resource: SubResource| #[trigger] resource_state_matches::(sub_resource, rabbitmq, s.resources()) } } pub open spec fn resource_state_matches(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::(), { ... } ``` `Maker` trait is defined inside `trusted` and `RabbitmqMaker` (which implements `Maker`) is not in `trusted`. --------- Signed-off-by: Xudong Sun --- .../fluentbit/exec/reconciler.rs | 5 +- .../fluentbit_config/exec/reconciler.rs | 5 +- .../rabbitmq_controller/exec/mod.rs | 1 - .../rabbitmq_controller/exec/reconciler.rs | 45 ++++---- .../exec/resource/common.rs | 16 +-- .../exec/resource/config_map.rs | 18 +-- .../exec/resource/default_user_secret.rs | 18 +-- .../exec/resource/erlang_cookie.rs | 27 ++--- .../exec/resource/headless_service.rs | 18 +-- .../exec/resource/rabbitmq_plugins.rs | 16 +-- .../rabbitmq_controller/exec/resource/role.rs | 32 +++--- .../exec/resource/role_binding.rs | 22 ++-- .../exec/resource/service.rs | 18 +-- .../exec/resource/service_account.rs | 16 +-- .../exec/resource/stateful_set.rs | 50 ++++----- .../rabbitmq_controller/mod.rs | 4 +- .../{spec => model}/mod.rs | 1 - .../{spec => model}/reconciler.rs | 73 ++++++++++++- .../{spec => model}/resource/common.rs | 4 +- .../{spec => model}/resource/config_map.rs | 6 +- .../resource/default_user_secret.rs | 6 +- .../{spec => model}/resource/erlang_cookie.rs | 8 +- .../resource/headless_service.rs | 6 +- .../{spec => model}/resource/mod.rs | 0 .../resource/rabbitmq_plugins.rs | 6 +- .../{spec => model}/resource/role.rs | 6 +- .../{spec => model}/resource/role_binding.rs | 6 +- .../{spec => model}/resource/service.rs | 6 +- .../resource/service_account.rs | 6 +- .../{spec => model}/resource/stateful_set.rs | 6 +- .../proof/helper_invariants/owner_ref.rs | 4 +- .../proof/helper_invariants/predicate.rs | 4 +- .../proof/helper_invariants/proof.rs | 7 +- .../proof/helper_invariants/unchangeable.rs | 4 +- .../proof/helper_invariants/validation.rs | 4 +- .../proof/liveness/proof.rs | 33 +++--- .../proof/liveness/resource_match.rs | 8 +- .../proof/liveness/spec.rs | 8 +- .../proof/liveness/stateful_set_match.rs | 5 +- .../proof/liveness/terminate.rs | 4 +- .../rabbitmq_controller/proof/mod.rs | 2 - .../rabbitmq_controller/proof/predicate.rs | 10 +- .../rabbitmq_controller/proof/resource.rs | 8 +- .../rabbitmq_controller/proof/safety/proof.rs | 20 ++-- .../{exec/types.rs => trusted/exec_types.rs} | 75 +++++-------- .../{proof => trusted}/liveness_theorem.rs | 103 +++++++++--------- .../rabbitmq_controller/trusted/maker.rs | 36 ++++++ .../rabbitmq_controller/trusted/mod.rs | 8 ++ .../{proof => trusted}/safety_theorem.rs | 19 ++-- .../{spec/types.rs => trusted/spec_types.rs} | 4 +- .../{common/mod.rs => trusted/step.rs} | 0 .../zookeeper_controller/exec/reconciler.rs | 5 +- src/rabbitmq_controller.rs | 2 +- src/reconciler/exec/reconciler.rs | 4 +- 54 files changed, 458 insertions(+), 370 deletions(-) rename src/controller_examples/rabbitmq_controller/{spec => model}/mod.rs (87%) rename src/controller_examples/rabbitmq_controller/{spec => model}/reconciler.rs (79%) rename src/controller_examples/rabbitmq_controller/{spec => model}/resource/common.rs (96%) rename src/controller_examples/rabbitmq_controller/{spec => model}/resource/config_map.rs (97%) rename src/controller_examples/rabbitmq_controller/{spec => model}/resource/default_user_secret.rs (96%) rename src/controller_examples/rabbitmq_controller/{spec => model}/resource/erlang_cookie.rs (94%) rename src/controller_examples/rabbitmq_controller/{spec => model}/resource/headless_service.rs (96%) rename src/controller_examples/rabbitmq_controller/{spec => model}/resource/mod.rs (100%) rename src/controller_examples/rabbitmq_controller/{spec => model}/resource/rabbitmq_plugins.rs (96%) rename src/controller_examples/rabbitmq_controller/{spec => model}/resource/role.rs (96%) rename src/controller_examples/rabbitmq_controller/{spec => model}/resource/role_binding.rs (96%) rename src/controller_examples/rabbitmq_controller/{spec => model}/resource/service.rs (96%) rename src/controller_examples/rabbitmq_controller/{spec => model}/resource/service_account.rs (96%) rename src/controller_examples/rabbitmq_controller/{spec => model}/resource/stateful_set.rs (98%) rename src/controller_examples/rabbitmq_controller/{exec/types.rs => trusted/exec_types.rs} (85%) rename src/controller_examples/rabbitmq_controller/{proof => trusted}/liveness_theorem.rs (51%) create mode 100644 src/controller_examples/rabbitmq_controller/trusted/maker.rs create mode 100644 src/controller_examples/rabbitmq_controller/trusted/mod.rs rename src/controller_examples/rabbitmq_controller/{proof => trusted}/safety_theorem.rs (75%) rename src/controller_examples/rabbitmq_controller/{spec/types.rs => trusted/spec_types.rs} (98%) rename src/controller_examples/rabbitmq_controller/{common/mod.rs => trusted/step.rs} (100%) diff --git a/src/controller_examples/fluent_controller/fluentbit/exec/reconciler.rs b/src/controller_examples/fluent_controller/fluentbit/exec/reconciler.rs index 118bcb6db..b83086955 100644 --- 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 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 index 7f5515541..3e44583f3 100644 --- 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 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 index 45860e477..701491013 100644 --- 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 index e66c3bbea..a938153d6 100644 --- 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::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 for RabbitmqReconciler { + open spec fn well_formed(rabbitmq: &RabbitmqCluster) -> bool { + rabbitmq@.well_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>, state: RabbitmqReconcileState) -> (res: (RabbitmqReconcileState, Option>)) requires rabbitmq@.well_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 { match resource { - SubResource::HeadlessService => reconcile_helper::(rabbitmq, resp_o, state), - SubResource::Service => reconcile_helper::(rabbitmq, resp_o, state), - SubResource::ErlangCookieSecret => reconcile_helper::(rabbitmq, resp_o, state), - SubResource::DefaultUserSecret => reconcile_helper::(rabbitmq, resp_o, state), - SubResource::PluginsConfigMap => reconcile_helper::(rabbitmq, resp_o, state), - SubResource::ServerConfigMap => reconcile_helper::(rabbitmq, resp_o, state), - SubResource::ServiceAccount => reconcile_helper::(rabbitmq, resp_o, state), - SubResource::Role => reconcile_helper::(rabbitmq, resp_o, state), - SubResource::RoleBinding => reconcile_helper::(rabbitmq, resp_o, state), - SubResource::StatefulSet => reconcile_helper::(rabbitmq, resp_o, state), + SubResource::HeadlessService => reconcile_helper::(rabbitmq, resp_o, state), + SubResource::Service => reconcile_helper::(rabbitmq, resp_o, state), + SubResource::ErlangCookieSecret => reconcile_helper::(rabbitmq, resp_o, state), + SubResource::DefaultUserSecret => reconcile_helper::(rabbitmq, resp_o, state), + SubResource::PluginsConfigMap => reconcile_helper::(rabbitmq, resp_o, state), + SubResource::ServerConfigMap => reconcile_helper::(rabbitmq, resp_o, state), + SubResource::ServiceAccount => reconcile_helper::(rabbitmq, resp_o, state), + SubResource::Role => reconcile_helper::(rabbitmq, resp_o, state), + SubResource::RoleBinding => reconcile_helper::(rabbitmq, resp_o, state), + SubResource::StatefulSet => reconcile_helper::(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::(rabbitmq@, opt_response_to_view(&resp_o), state@), + (res.0@, opt_request_to_view(&res.1)) == model_reconciler::reconcile_helper::(rabbitmq@, opt_response_to_view(&resp_o), state@), { let step = state.reconcile_step.clone(); match step { diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/common.rs b/src/controller_examples/rabbitmq_controller/exec/resource/common.rs index 2e4776171..ce5d73bec 100644 --- 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::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 rabbitmq@.metadata.name.is_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 rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - owner_references@.map_values(|or: OwnerReference| or@) == spec_resource::make_owner_references(rabbitmq@), + owner_references@.map_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!( owner_references@.map_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) -> rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_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 for ServerConfigMapBuilder { +impl ResourceBuilder 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 rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_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) rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_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 rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_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) rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - s@ == spec_resource::default_rbmq_config(rabbitmq@), + s@ == model_resource::default_rbmq_config(rabbitmq@), { new_strlit( "queue_master_locator = min-masters\n\ 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 index d2adec16e..e38fbd7f7 100644 --- 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::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 for DefaultUserSecretBuilder { +impl ResourceBuilder 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 rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_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 rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_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 rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_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) rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_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)) } diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/erlang_cookie.rs b/src/controller_examples/rabbitmq_controller/exec/resource/erlang_cookie.rs index fdbd87111..064ba3ffc 100644 --- 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::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 ErlangCookieBuilder {} -impl ResourceBuilder for ErlangCookieBuilder { +impl ResourceBuilder for ErlangCookieBuilder { open spec fn requirements(rabbitmq: RabbitmqClusterView) -> bool { &&& rabbitmq.metadata.name.is_Some() &&& rabbitmq.metadata.namespace.is_Some() @@ -85,7 +85,7 @@ pub fn update_erlang_secret(rabbitmq: &RabbitmqCluster, found_erlang_secret: Sec rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - secret@ == spec_resource::update_erlang_secret(rabbitmq@, found_erlang_secret@), + secret@ == model_resource::update_erlang_secret(rabbitmq@, found_erlang_secret@), { let mut erlang_secret = found_erlang_secret.clone(); let made_secret = make_erlang_secret(rabbitmq); @@ -96,7 +96,7 @@ pub fn update_erlang_secret(rabbitmq: &RabbitmqCluster, found_erlang_secret: Sec proof { assert_seqs_equal!( owner_references@.map_values(|owner_ref: OwnerReference| owner_ref@), - spec_resource::update_erlang_secret(rabbitmq@, found_erlang_secret@).metadata.owner_references.get_Some_0() + model_resource::update_erlang_secret(rabbitmq@, found_erlang_secret@).metadata.owner_references.get_Some_0() ); } metadata.set_owner_references(make_owner_references(rabbitmq)); @@ -113,7 +113,7 @@ pub fn make_erlang_secret_name(rabbitmq: &RabbitmqCluster) -> (name: String) rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - name@ == spec_resource::make_erlang_secret_name(rabbitmq@), + name@ == model_resource::make_erlang_secret_name(rabbitmq@), { rabbitmq.metadata().name().unwrap().concat(new_strlit("-erlang-cookie")) } @@ -123,7 +123,7 @@ pub fn make_erlang_secret(rabbitmq: &RabbitmqCluster) -> (secret: Secret) rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - secret@ == spec_resource::make_erlang_secret(rabbitmq@) + secret@ == model_resource::make_erlang_secret(rabbitmq@) { let mut data = StringMap::empty(); let cookie = random_encoded_string(24); @@ -131,13 +131,4 @@ pub fn make_erlang_secret(rabbitmq: &RabbitmqCluster) -> (secret: Secret) make_secret(rabbitmq, make_erlang_secret_name(rabbitmq), data) } -#[verifier(external_body)] -pub fn random_encoded_string(data_len: usize) -> (cookie: String) - ensures - cookie@ == spec_resource::random_encoded_string(data_len), -{ - let random_bytes: std::vec::Vec = (0..data_len).map(|_| deps_hack::rand::random::()).collect(); - String::from_rust_string(deps_hack::base64::encode(random_bytes)) -} - } diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/headless_service.rs b/src/controller_examples/rabbitmq_controller/exec/resource/headless_service.rs index 983435528..d5c4a5323 100644 --- 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::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 HeadlessServiceBuilder {} -impl ResourceBuilder for HeadlessServiceBuilder { +impl ResourceBuilder for HeadlessServiceBuilder { open spec fn requirements(rabbitmq: RabbitmqClusterView) -> bool { &&& rabbitmq.metadata.name.is_Some() &&& rabbitmq.metadata.namespace.is_Some() @@ -88,7 +88,7 @@ pub fn update_headless_service(rabbitmq: &RabbitmqCluster, found_headless_servic rabbitmq@.metadata.namespace.is_Some(), found_headless_service@.spec.is_Some(), ensures - service@ == spec_resource::update_headless_service(rabbitmq@, found_headless_service@), + service@ == model_resource::update_headless_service(rabbitmq@, found_headless_service@), { let made_service = make_headless_service(rabbitmq); @@ -118,7 +118,7 @@ pub fn make_headless_service_name(rabbitmq: &RabbitmqCluster) -> (name: String) rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - name@ == spec_resource::make_headless_service_name(rabbitmq@), + name@ == model_resource::make_headless_service_name(rabbitmq@), { rabbitmq.metadata().name().unwrap().concat(new_strlit("-nodes")) } @@ -128,7 +128,7 @@ pub fn make_headless_service(rabbitmq: &RabbitmqCluster) -> (service: Service) rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - service@ == spec_resource::make_headless_service(rabbitmq@), + service@ == model_resource::make_headless_service(rabbitmq@), { let mut ports = Vec::new(); ports.push(ServicePort::new_with(new_strlit("epmd").to_string(), 4369)); @@ -136,7 +136,7 @@ pub fn make_headless_service(rabbitmq: &RabbitmqCluster) -> (service: Service) proof { assert_seqs_equal!( ports@.map_values(|port: ServicePort| port@), - spec_resource::make_headless_service(rabbitmq@).spec.get_Some_0().ports.get_Some_0() + model_resource::make_headless_service(rabbitmq@).spec.get_Some_0().ports.get_Some_0() ); } make_service(rabbitmq, make_headless_service_name(rabbitmq), ports, false) diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/rabbitmq_plugins.rs b/src/controller_examples/rabbitmq_controller/exec/resource/rabbitmq_plugins.rs index 48e2aba30..aad1c7017 100644 --- 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::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 PluginsConfigMapBuilder {} -impl ResourceBuilder for PluginsConfigMapBuilder { +impl ResourceBuilder for PluginsConfigMapBuilder { open spec fn requirements(rabbitmq: RabbitmqClusterView) -> bool { &&& rabbitmq.metadata.name.is_Some() &&& rabbitmq.metadata.namespace.is_Some() @@ -85,7 +85,7 @@ pub fn update_plugins_config_map(rabbitmq: &RabbitmqCluster, found_config_map: C rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - config_map@ == spec_resource::update_plugins_config_map(rabbitmq@, found_config_map@), + config_map@ == model_resource::update_plugins_config_map(rabbitmq@, found_config_map@), { let mut config_map = found_config_map.clone(); let made_config_map = make_plugins_config_map(rabbitmq); @@ -106,7 +106,7 @@ pub fn make_plugins_config_map_name(rabbitmq: &RabbitmqCluster) -> (name: String rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - name@ == spec_resource::make_plugins_config_map_name(rabbitmq@), + name@ == model_resource::make_plugins_config_map_name(rabbitmq@), { rabbitmq.metadata().name().unwrap().concat(new_strlit("-plugins-conf")) } @@ -116,7 +116,7 @@ pub fn make_plugins_config_map(rabbitmq: &RabbitmqCluster) -> (config_map: Confi rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - config_map@ == spec_resource::make_plugins_config_map(rabbitmq@), + config_map@ == model_resource::make_plugins_config_map(rabbitmq@), { let mut config_map = ConfigMap::default(); config_map.set_metadata({ diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/role.rs b/src/controller_examples/rabbitmq_controller/exec/resource/role.rs index 9df688bec..3e493abb5 100644 --- 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::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 RoleBuilder {} -impl ResourceBuilder for RoleBuilder { +impl ResourceBuilder for RoleBuilder { open spec fn requirements(rabbitmq: RabbitmqClusterView) -> bool { &&& rabbitmq.metadata.name.is_Some() &&& rabbitmq.metadata.namespace.is_Some() @@ -85,7 +85,7 @@ pub fn update_role(rabbitmq: &RabbitmqCluster, found_role: Role) -> (role: Role) rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - role@ == spec_resource::update_role(rabbitmq@, found_role@), + role@ == model_resource::update_role(rabbitmq@, found_role@), { let mut role = found_role.clone(); let made_role = make_role(rabbitmq); @@ -106,7 +106,7 @@ pub fn make_role_name(rabbitmq: &RabbitmqCluster) -> (name: String) rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - name@ == spec_resource::make_role_name(rabbitmq@), + name@ == model_resource::make_role_name(rabbitmq@), { rabbitmq.metadata().name().unwrap().concat(new_strlit("-peer-discovery")) } @@ -116,7 +116,7 @@ pub fn make_policy_rules(rabbitmq: &RabbitmqCluster) -> (rules: Vec) rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - rules@.map_values(|r: PolicyRule| r@) == spec_resource::make_role(rabbitmq@).policy_rules.get_Some_0(), + rules@.map_values(|r: PolicyRule| r@) == model_resource::make_role(rabbitmq@).policy_rules.get_Some_0(), { let mut rules = Vec::new(); rules.push({ @@ -127,7 +127,7 @@ pub fn make_policy_rules(rabbitmq: &RabbitmqCluster) -> (rules: Vec) proof{ assert_seqs_equal!( api_groups@.map_values(|p: String| p@), - spec_resource::make_role(rabbitmq@).policy_rules.get_Some_0()[0].api_groups.get_Some_0() + model_resource::make_role(rabbitmq@).policy_rules.get_Some_0()[0].api_groups.get_Some_0() ); } api_groups @@ -138,7 +138,7 @@ pub fn make_policy_rules(rabbitmq: &RabbitmqCluster) -> (rules: Vec) proof{ assert_seqs_equal!( resources@.map_values(|p: String| p@), - spec_resource::make_role(rabbitmq@).policy_rules.get_Some_0()[0].resources.get_Some_0() + model_resource::make_role(rabbitmq@).policy_rules.get_Some_0()[0].resources.get_Some_0() ); } resources @@ -149,7 +149,7 @@ pub fn make_policy_rules(rabbitmq: &RabbitmqCluster) -> (rules: Vec) proof{ assert_seqs_equal!( verbs@.map_values(|p: String| p@), - spec_resource::make_role(rabbitmq@).policy_rules.get_Some_0()[0].verbs + model_resource::make_role(rabbitmq@).policy_rules.get_Some_0()[0].verbs ); } verbs @@ -164,7 +164,7 @@ pub fn make_policy_rules(rabbitmq: &RabbitmqCluster) -> (rules: Vec) proof{ assert_seqs_equal!( api_groups@.map_values(|p: String| p@), - spec_resource::make_role(rabbitmq@).policy_rules.get_Some_0()[1].api_groups.get_Some_0() + model_resource::make_role(rabbitmq@).policy_rules.get_Some_0()[1].api_groups.get_Some_0() ); } api_groups @@ -175,7 +175,7 @@ pub fn make_policy_rules(rabbitmq: &RabbitmqCluster) -> (rules: Vec) proof{ assert_seqs_equal!( resources@.map_values(|p: String| p@), - spec_resource::make_role(rabbitmq@).policy_rules.get_Some_0()[1].resources.get_Some_0() + model_resource::make_role(rabbitmq@).policy_rules.get_Some_0()[1].resources.get_Some_0() ); } resources @@ -186,7 +186,7 @@ pub fn make_policy_rules(rabbitmq: &RabbitmqCluster) -> (rules: Vec) proof{ assert_seqs_equal!( verbs@.map_values(|p: String| p@), - spec_resource::make_role(rabbitmq@).policy_rules.get_Some_0()[1].verbs + model_resource::make_role(rabbitmq@).policy_rules.get_Some_0()[1].verbs ); } verbs @@ -196,7 +196,7 @@ pub fn make_policy_rules(rabbitmq: &RabbitmqCluster) -> (rules: Vec) proof{ assert_seqs_equal!( rules@.map_values(|p: PolicyRule| p@), - spec_resource::make_role(rabbitmq@).policy_rules.get_Some_0() + model_resource::make_role(rabbitmq@).policy_rules.get_Some_0() ); } rules @@ -207,7 +207,7 @@ pub fn make_role(rabbitmq: &RabbitmqCluster) -> (role: Role) rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - role@ == spec_resource::make_role(rabbitmq@), + role@ == model_resource::make_role(rabbitmq@), { let mut role = Role::default(); role.set_metadata({ diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/role_binding.rs b/src/controller_examples/rabbitmq_controller/exec/resource/role_binding.rs index e9ccecff3..3424ec0bf 100644 --- 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::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 RoleBindingBuilder {} -impl ResourceBuilder for RoleBindingBuilder { +impl ResourceBuilder for RoleBindingBuilder { open spec fn requirements(rabbitmq: RabbitmqClusterView) -> bool { &&& rabbitmq.metadata.name.is_Some() &&& rabbitmq.metadata.namespace.is_Some() @@ -85,7 +85,7 @@ pub fn update_role_binding(rabbitmq: &RabbitmqCluster, found_role_binding: RoleB rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - role_binding@ == spec_resource::update_role_binding(rabbitmq@, found_role_binding@), + role_binding@ == model_resource::update_role_binding(rabbitmq@, found_role_binding@), { let mut role_binding = found_role_binding.clone(); let made_role_binding = make_role_binding(rabbitmq); @@ -106,7 +106,7 @@ pub fn make_role_binding_name(rabbitmq: &RabbitmqCluster) -> (name: String) rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - name@ == spec_resource::make_role_binding_name(rabbitmq@), + name@ == model_resource::make_role_binding_name(rabbitmq@), { rabbitmq.metadata().name().unwrap().concat(new_strlit("-server")) } @@ -115,7 +115,7 @@ pub fn make_role_ref(rabbitmq: &RabbitmqCluster) -> (role_ref: RoleRef) requires rabbitmq@.metadata.name.is_Some(), ensures - role_ref@ == spec_resource::make_role_binding(rabbitmq@).role_ref + role_ref@ == model_resource::make_role_binding(rabbitmq@).role_ref { let mut role_ref = RoleRef::default(); role_ref.set_api_group(new_strlit("rbac.authorization.k8s.io").to_string()); @@ -129,7 +129,7 @@ pub fn make_subjects(rabbitmq: &RabbitmqCluster) -> (subjects: Vec) rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - subjects@.map_values(|s: Subject| s@) == spec_resource::make_role_binding(rabbitmq@).subjects.get_Some_0(), + subjects@.map_values(|s: Subject| s@) == model_resource::make_role_binding(rabbitmq@).subjects.get_Some_0(), { let mut subjects = Vec::new(); subjects.push({ @@ -142,7 +142,7 @@ pub fn make_subjects(rabbitmq: &RabbitmqCluster) -> (subjects: Vec) proof{ assert_seqs_equal!( subjects@.map_values(|p: Subject| p@), - spec_resource::make_role_binding(rabbitmq@).subjects.get_Some_0() + model_resource::make_role_binding(rabbitmq@).subjects.get_Some_0() ); } subjects @@ -153,7 +153,7 @@ pub fn make_role_binding(rabbitmq: &RabbitmqCluster) -> (role_binding: RoleBindi rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - role_binding@ == spec_resource::make_role_binding(rabbitmq@), + role_binding@ == model_resource::make_role_binding(rabbitmq@), { let mut role_binding = RoleBinding::default(); role_binding.set_metadata({ diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/service.rs b/src/controller_examples/rabbitmq_controller/exec/resource/service.rs index aec291ebf..974c782ed 100644 --- 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::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 ServiceBuilder {} -impl ResourceBuilder for ServiceBuilder { +impl ResourceBuilder for ServiceBuilder { open spec fn requirements(rabbitmq: RabbitmqClusterView) -> bool { &&& rabbitmq.metadata.name.is_Some() &&& rabbitmq.metadata.namespace.is_Some() @@ -88,7 +88,7 @@ pub fn update_main_service(rabbitmq: &RabbitmqCluster, found_main_service: Servi rabbitmq@.metadata.namespace.is_Some(), found_main_service@.spec.is_Some(), ensures - service@ == spec_resource::update_main_service(rabbitmq@, found_main_service@), + service@ == model_resource::update_main_service(rabbitmq@, found_main_service@), { let mut main_service = found_main_service.clone(); let made_service = make_main_service(rabbitmq); @@ -120,7 +120,7 @@ pub fn make_main_service_name(rabbitmq: &RabbitmqCluster) -> (name: String) rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - name@ == spec_resource::make_main_service_name(rabbitmq@), + name@ == model_resource::make_main_service_name(rabbitmq@), { rabbitmq.metadata().name().unwrap().concat(new_strlit("-client")) } @@ -130,7 +130,7 @@ pub fn make_main_service(rabbitmq: &RabbitmqCluster) -> (service: Service) rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - service@ == spec_resource::make_main_service(rabbitmq@) + service@ == model_resource::make_main_service(rabbitmq@) { let mut ports = Vec::new(); // TODO: check whether the protocols are set to TCP @@ -152,7 +152,7 @@ pub fn make_main_service(rabbitmq: &RabbitmqCluster) -> (service: Service) proof { assert_seqs_equal!( ports@.map_values(|port: ServicePort| port@), - spec_resource::make_main_service(rabbitmq@).spec.get_Some_0().ports.get_Some_0() + model_resource::make_main_service(rabbitmq@).spec.get_Some_0().ports.get_Some_0() ); } make_service(rabbitmq, make_main_service_name(rabbitmq), ports, true) diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/service_account.rs b/src/controller_examples/rabbitmq_controller/exec/resource/service_account.rs index 9097cbc46..266874248 100644 --- 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::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 ServiceAccountBuilder {} -impl ResourceBuilder for ServiceAccountBuilder { +impl ResourceBuilder for ServiceAccountBuilder { open spec fn requirements(rabbitmq: RabbitmqClusterView) -> bool { &&& rabbitmq.metadata.name.is_Some() &&& rabbitmq.metadata.namespace.is_Some() @@ -85,7 +85,7 @@ pub fn update_service_account(rabbitmq: &RabbitmqCluster, found_service_account: rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - service_account@ == spec_resource::update_service_account(rabbitmq@, found_service_account@), + service_account@ == model_resource::update_service_account(rabbitmq@, found_service_account@), { let mut service_account = found_service_account.clone(); let made_service_account = make_service_account(rabbitmq); @@ -105,7 +105,7 @@ pub fn make_service_account_name(rabbitmq: &RabbitmqCluster) -> (name: String) rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - name@ == spec_resource::make_service_account_name(rabbitmq@), + name@ == model_resource::make_service_account_name(rabbitmq@), { rabbitmq.metadata().name().unwrap().concat(new_strlit("-server")) } @@ -115,7 +115,7 @@ pub fn make_service_account(rabbitmq: &RabbitmqCluster) -> (service_account: Ser rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - service_account@ == spec_resource::make_service_account(rabbitmq@), + service_account@ == model_resource::make_service_account(rabbitmq@), { let mut service_account = ServiceAccount::default(); service_account.set_metadata({ diff --git a/src/controller_examples/rabbitmq_controller/exec/resource/stateful_set.rs b/src/controller_examples/rabbitmq_controller/exec/resource/stateful_set.rs index 008dc1383..4e19313a2 100644 --- 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::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::*; @@ -23,7 +23,7 @@ verus! { pub struct StatefulSetBuilder {} -impl ResourceBuilder for StatefulSetBuilder { +impl ResourceBuilder for StatefulSetBuilder { open spec fn requirements(rabbitmq: RabbitmqClusterView) -> bool { &&& rabbitmq.metadata.name.is_Some() &&& rabbitmq.metadata.namespace.is_Some() @@ -97,7 +97,7 @@ pub fn update_stateful_set(rabbitmq: &RabbitmqCluster, found_stateful_set: State rabbitmq@.metadata.namespace.is_Some(), found_stateful_set@.spec.is_Some(), ensures - stateful_set@ == spec_resource::update_stateful_set(rabbitmq@, found_stateful_set@, config_map_rv@), + stateful_set@ == model_resource::update_stateful_set(rabbitmq@, found_stateful_set@, config_map_rv@), { let made_sts = make_stateful_set(rabbitmq, config_map_rv); @@ -128,7 +128,7 @@ pub fn update_stateful_set(rabbitmq: &RabbitmqCluster, found_stateful_set: State pub fn sts_restart_annotation() -> (anno: String) ensures - anno@ == spec_resource::sts_restart_annotation(), + anno@ == model_resource::sts_restart_annotation(), { new_strlit("anvil.dev/lastRestartAt").to_string() } @@ -138,7 +138,7 @@ pub fn make_stateful_set_name(rabbitmq: &RabbitmqCluster) -> (name: String) rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - name@ == spec_resource::make_stateful_set_name(rabbitmq@), + name@ == model_resource::make_stateful_set_name(rabbitmq@), { rabbitmq.metadata().name().unwrap().concat(new_strlit("-server")) } @@ -148,7 +148,7 @@ pub fn make_stateful_set(rabbitmq: &RabbitmqCluster, config_map_rv: &String) -> rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - stateful_set@ == spec_resource::make_stateful_set(rabbitmq@, config_map_rv@), + stateful_set@ == model_resource::make_stateful_set(rabbitmq@, config_map_rv@), { let mut stateful_set = StatefulSet::default(); stateful_set.set_metadata({ @@ -183,7 +183,7 @@ pub fn make_stateful_set(rabbitmq: &RabbitmqCluster, config_map_rv: &String) -> proof { assert_seqs_equal!( empty_pvc@.map_values(|pvc: PersistentVolumeClaim| pvc@), - spec_resource::make_stateful_set(rabbitmq@, config_map_rv@).spec.get_Some_0().volume_claim_templates.get_Some_0() + model_resource::make_stateful_set(rabbitmq@, config_map_rv@).spec.get_Some_0().volume_claim_templates.get_Some_0() ); } empty_pvc @@ -210,7 +210,7 @@ pub fn make_stateful_set(rabbitmq: &RabbitmqCluster, config_map_rv: &String) -> proof { assert_seqs_equal!( access_modes@.map_values(|mode: String| mode@), - spec_resource::make_stateful_set(rabbitmq@, config_map_rv@) + model_resource::make_stateful_set(rabbitmq@, config_map_rv@) .spec.get_Some_0().volume_claim_templates.get_Some_0()[0] .spec.get_Some_0().access_modes.get_Some_0() ); @@ -235,7 +235,7 @@ pub fn make_stateful_set(rabbitmq: &RabbitmqCluster, config_map_rv: &String) -> proof { assert_seqs_equal!( volume_claim_templates@.map_values(|pvc: PersistentVolumeClaim| pvc@), - spec_resource::make_stateful_set(rabbitmq@, config_map_rv@).spec.get_Some_0().volume_claim_templates.get_Some_0() + model_resource::make_stateful_set(rabbitmq@, config_map_rv@).spec.get_Some_0().volume_claim_templates.get_Some_0() ); } volume_claim_templates @@ -273,7 +273,7 @@ pub fn make_rabbitmq_pod_spec(rabbitmq: &RabbitmqCluster) -> (pod_spec: PodSpec) rabbitmq@.metadata.name.is_Some(), rabbitmq@.metadata.namespace.is_Some(), ensures - pod_spec@ == spec_resource::make_rabbitmq_pod_spec(rabbitmq@), + pod_spec@ == model_resource::make_rabbitmq_pod_spec(rabbitmq@), { let mut volumes = Vec::new(); volumes.push({ @@ -315,7 +315,7 @@ pub fn make_rabbitmq_pod_spec(rabbitmq: &RabbitmqCluster) -> (pod_spec: PodSpec) proof { assert_seqs_equal!( items@.map_values(|item: KeyToPath| item@), - spec_resource::make_rabbitmq_pod_spec(rabbitmq@).volumes.get_Some_0()[1].projected.get_Some_0() + model_resource::make_rabbitmq_pod_spec(rabbitmq@).volumes.get_Some_0()[1].projected.get_Some_0() .sources.get_Some_0()[0].config_map.get_Some_0().items.get_Some_0() ); } @@ -341,7 +341,7 @@ pub fn make_rabbitmq_pod_spec(rabbitmq: &RabbitmqCluster) -> (pod_spec: PodSpec) proof { assert_seqs_equal!( items@.map_values(|item: KeyToPath| item@), - spec_resource::make_rabbitmq_pod_spec(rabbitmq@).volumes.get_Some_0()[1].projected.get_Some_0() + model_resource::make_rabbitmq_pod_spec(rabbitmq@).volumes.get_Some_0()[1].projected.get_Some_0() .sources.get_Some_0()[1].secret.get_Some_0().items.get_Some_0() ); } @@ -354,7 +354,7 @@ pub fn make_rabbitmq_pod_spec(rabbitmq: &RabbitmqCluster) -> (pod_spec: PodSpec) proof { assert_seqs_equal!( sources@.map_values(|source: VolumeProjection| source@), - spec_resource::make_rabbitmq_pod_spec(rabbitmq@).volumes.get_Some_0()[1].projected.get_Some_0() + model_resource::make_rabbitmq_pod_spec(rabbitmq@).volumes.get_Some_0()[1].projected.get_Some_0() .sources.get_Some_0() ); } @@ -406,7 +406,7 @@ pub fn make_rabbitmq_pod_spec(rabbitmq: &RabbitmqCluster) -> (pod_spec: PodSpec) proof { assert_seqs_equal!( items@.map_values(|item: DownwardAPIVolumeFile| item@), - spec_resource::make_rabbitmq_pod_spec(rabbitmq@).volumes.get_Some_0()[5].downward_api.get_Some_0().items.get_Some_0() + model_resource::make_rabbitmq_pod_spec(rabbitmq@).volumes.get_Some_0()[5].downward_api.get_Some_0().items.get_Some_0() ); } items @@ -426,7 +426,7 @@ pub fn make_rabbitmq_pod_spec(rabbitmq: &RabbitmqCluster) -> (pod_spec: PodSpec) proof { assert_seqs_equal!( volumes@.map_values(|vol: Volume| vol@), - spec_resource::make_rabbitmq_pod_spec(rabbitmq@).volumes.get_Some_0() + model_resource::make_rabbitmq_pod_spec(rabbitmq@).volumes.get_Some_0() ); } let mut pod_spec = PodSpec::default(); @@ -519,7 +519,7 @@ pub fn make_rabbitmq_pod_spec(rabbitmq: &RabbitmqCluster) -> (pod_spec: PodSpec) proof { assert_seqs_equal!( volume_mounts@.map_values(|volume_mount: VolumeMount| volume_mount@), - spec_resource::make_rabbitmq_pod_spec(rabbitmq@).init_containers.unwrap()[0].volume_mounts.get_Some_0() + model_resource::make_rabbitmq_pod_spec(rabbitmq@).init_containers.unwrap()[0].volume_mounts.get_Some_0() ); } volume_mounts @@ -529,7 +529,7 @@ pub fn make_rabbitmq_pod_spec(rabbitmq: &RabbitmqCluster) -> (pod_spec: PodSpec) proof { assert_seqs_equal!( containers@.map_values(|container: Container| container@), - spec_resource::make_rabbitmq_pod_spec(rabbitmq@).init_containers.unwrap() + model_resource::make_rabbitmq_pod_spec(rabbitmq@).init_containers.unwrap() ); } containers @@ -592,7 +592,7 @@ pub fn make_rabbitmq_pod_spec(rabbitmq: &RabbitmqCluster) -> (pod_spec: PodSpec) proof { assert_seqs_equal!( volume_mounts@.map_values(|volume_mount: VolumeMount| volume_mount@), - spec_resource::make_rabbitmq_pod_spec(rabbitmq@).containers[0].volume_mounts.get_Some_0() + model_resource::make_rabbitmq_pod_spec(rabbitmq@).containers[0].volume_mounts.get_Some_0() ); } volume_mounts @@ -606,7 +606,7 @@ pub fn make_rabbitmq_pod_spec(rabbitmq: &RabbitmqCluster) -> (pod_spec: PodSpec) proof { assert_seqs_equal!( ports@.map_values(|port: ContainerPort| port@), - spec_resource::make_rabbitmq_pod_spec(rabbitmq@).containers[0].ports.get_Some_0() + model_resource::make_rabbitmq_pod_spec(rabbitmq@).containers[0].ports.get_Some_0() ); } @@ -631,7 +631,7 @@ pub fn make_rabbitmq_pod_spec(rabbitmq: &RabbitmqCluster) -> (pod_spec: PodSpec) proof { assert_seqs_equal!( containers@.map_values(|container: Container| container@), - spec_resource::make_rabbitmq_pod_spec(rabbitmq@).containers + model_resource::make_rabbitmq_pod_spec(rabbitmq@).containers ); } containers @@ -646,7 +646,7 @@ pub fn make_env_vars(rabbitmq: &RabbitmqCluster) -> (env_vars: Vec) requires rabbitmq@.metadata.name.is_Some(), ensures - env_vars@.map_values(|v: EnvVar| v@) == spec_resource::make_env_vars(rabbitmq@) + env_vars@.map_values(|v: EnvVar| v@) == model_resource::make_env_vars(rabbitmq@) { let mut env_vars = Vec::new(); env_vars.push(EnvVar::new_with( @@ -677,7 +677,7 @@ pub fn make_env_vars(rabbitmq: &RabbitmqCluster) -> (env_vars: Vec) proof { assert_seqs_equal!( env_vars@.map_values(|v: EnvVar| v@), - spec_resource::make_env_vars(rabbitmq@) + model_resource::make_env_vars(rabbitmq@) ); } env_vars diff --git a/src/controller_examples/rabbitmq_controller/mod.rs b/src/controller_examples/rabbitmq_controller/mod.rs index ace54d2d1..ab69eb2d9 100644 --- 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 model; pub mod proof; -pub mod spec; +pub mod trusted; diff --git a/src/controller_examples/rabbitmq_controller/spec/mod.rs b/src/controller_examples/rabbitmq_controller/model/mod.rs similarity index 87% rename from src/controller_examples/rabbitmq_controller/spec/mod.rs rename to src/controller_examples/rabbitmq_controller/model/mod.rs index 45860e477..701491013 100644 --- a/src/controller_examples/rabbitmq_controller/spec/mod.rs +++ b/src/controller_examples/rabbitmq_controller/model/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/spec/reconciler.rs b/src/controller_examples/rabbitmq_controller/model/reconciler.rs similarity index 79% rename from src/controller_examples/rabbitmq_controller/spec/reconciler.rs rename to src/controller_examples/rabbitmq_controller/model/reconciler.rs index 48f11420c..7bb2eef73 100644 --- a/src/controller_examples/rabbitmq_controller/spec/reconciler.rs +++ b/src/controller_examples/rabbitmq_controller/model/reconciler.rs @@ -7,9 +7,10 @@ use crate::kubernetes_api_objects::{ volume::*, }; use crate::kubernetes_cluster::spec::message::*; -use crate::rabbitmq_controller::common::*; -use crate::rabbitmq_controller::spec::resource::*; -use crate::rabbitmq_controller::spec::types::*; +use crate::rabbitmq_controller::model::resource::*; +use crate::rabbitmq_controller::trusted::maker::*; +use crate::rabbitmq_controller::trusted::spec_types::*; +use crate::rabbitmq_controller::trusted::step::*; use crate::reconciler::spec::{io::*, reconciler::*, resource_builder::*}; use crate::state_machine::{action::*, state_machine::*}; use crate::temporal_logic::defs::*; @@ -251,4 +252,70 @@ pub open spec fn reconcile_helper ObjectRef { + make_headless_service_key(rabbitmq) + } + open spec fn make_main_service_key(rabbitmq: RabbitmqClusterView) -> ObjectRef { + make_main_service_key(rabbitmq) + } + open spec fn make_erlang_secret_key(rabbitmq: RabbitmqClusterView) -> ObjectRef { + make_erlang_secret_key(rabbitmq) + } + open spec fn make_default_user_secret_key(rabbitmq: RabbitmqClusterView) -> ObjectRef { + make_default_user_secret_key(rabbitmq) + } + open spec fn make_plugins_config_map_key(rabbitmq: RabbitmqClusterView) -> ObjectRef { + make_plugins_config_map_key(rabbitmq) + } + open spec fn make_server_config_map_key(rabbitmq: RabbitmqClusterView) -> ObjectRef { + make_server_config_map_key(rabbitmq) + } + open spec fn make_service_account_key(rabbitmq: RabbitmqClusterView) -> ObjectRef { + make_service_account_key(rabbitmq) + } + open spec fn make_role_key(rabbitmq: RabbitmqClusterView) -> ObjectRef { + make_role_key(rabbitmq) + } + open spec fn make_role_binding_key(rabbitmq: RabbitmqClusterView) -> ObjectRef { + make_role_binding_key(rabbitmq) + } + open spec fn make_stateful_set_key(rabbitmq: RabbitmqClusterView) -> ObjectRef { + make_stateful_set_key(rabbitmq) + } + + open spec fn make_headless_service(rabbitmq: RabbitmqClusterView) -> ServiceView { + make_headless_service(rabbitmq) + } + open spec fn make_main_service(rabbitmq: RabbitmqClusterView) -> ServiceView { + make_main_service(rabbitmq) + } + open spec fn make_erlang_secret(rabbitmq: RabbitmqClusterView) -> SecretView { + make_erlang_secret(rabbitmq) + } + open spec fn make_default_user_secret(rabbitmq: RabbitmqClusterView) -> SecretView { + make_default_user_secret(rabbitmq) + } + open spec fn make_plugins_config_map(rabbitmq: RabbitmqClusterView) -> ConfigMapView { + make_plugins_config_map(rabbitmq) + } + open spec fn make_server_config_map(rabbitmq: RabbitmqClusterView) -> ConfigMapView { + make_server_config_map(rabbitmq) + } + open spec fn make_service_account(rabbitmq: RabbitmqClusterView) -> ServiceAccountView { + make_service_account(rabbitmq) + } + open spec fn make_role(rabbitmq: RabbitmqClusterView) -> RoleView { + make_role(rabbitmq) + } + open spec fn make_role_binding(rabbitmq: RabbitmqClusterView) -> RoleBindingView { + make_role_binding(rabbitmq) + } + open spec fn make_stateful_set(rabbitmq: RabbitmqClusterView, config_map_rv: StringView) -> StatefulSetView { + make_stateful_set(rabbitmq, config_map_rv) + } +} + } diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/common.rs b/src/controller_examples/rabbitmq_controller/model/resource/common.rs similarity index 96% rename from src/controller_examples/rabbitmq_controller/spec/resource/common.rs rename to src/controller_examples/rabbitmq_controller/model/resource/common.rs index 6c1c4007c..910b55e66 100644 --- a/src/controller_examples/rabbitmq_controller/spec/resource/common.rs +++ b/src/controller_examples/rabbitmq_controller/model/resource/common.rs @@ -6,8 +6,8 @@ use crate::kubernetes_api_objects::{ volume::*, }; use crate::kubernetes_cluster::spec::message::*; -use crate::rabbitmq_controller::common::*; -use crate::rabbitmq_controller::spec::types::*; +use crate::rabbitmq_controller::trusted::spec_types::*; +use crate::rabbitmq_controller::trusted::step::*; use crate::reconciler::spec::{io::*, reconciler::*}; use crate::state_machine::{action::*, state_machine::*}; use crate::temporal_logic::defs::*; diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/config_map.rs b/src/controller_examples/rabbitmq_controller/model/resource/config_map.rs similarity index 97% rename from src/controller_examples/rabbitmq_controller/spec/resource/config_map.rs rename to src/controller_examples/rabbitmq_controller/model/resource/config_map.rs index 7fc06fec5..bd0e1ec20 100644 --- a/src/controller_examples/rabbitmq_controller/spec/resource/config_map.rs +++ b/src/controller_examples/rabbitmq_controller/model/resource/config_map.rs @@ -8,9 +8,9 @@ use crate::kubernetes_api_objects::{ volume::*, }; use crate::kubernetes_cluster::spec::message::*; -use crate::rabbitmq_controller::common::*; -use crate::rabbitmq_controller::spec::resource::ServiceAccountBuilder; -use crate::rabbitmq_controller::spec::types::*; +use crate::rabbitmq_controller::model::resource::ServiceAccountBuilder; +use crate::rabbitmq_controller::trusted::spec_types::*; +use crate::rabbitmq_controller::trusted::step::*; use crate::reconciler::spec::{io::*, reconciler::*, resource_builder::*}; use crate::state_machine::{action::*, state_machine::*}; use crate::temporal_logic::defs::*; diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/default_user_secret.rs b/src/controller_examples/rabbitmq_controller/model/resource/default_user_secret.rs similarity index 96% rename from src/controller_examples/rabbitmq_controller/spec/resource/default_user_secret.rs rename to src/controller_examples/rabbitmq_controller/model/resource/default_user_secret.rs index 50ce68668..7e0468d84 100644 --- a/src/controller_examples/rabbitmq_controller/spec/resource/default_user_secret.rs +++ b/src/controller_examples/rabbitmq_controller/model/resource/default_user_secret.rs @@ -8,9 +8,9 @@ use crate::kubernetes_api_objects::{ volume::*, }; use crate::kubernetes_cluster::spec::message::*; -use crate::rabbitmq_controller::common::*; -use crate::rabbitmq_controller::spec::resource::rabbitmq_plugins::PluginsConfigMapBuilder; -use crate::rabbitmq_controller::spec::types::*; +use crate::rabbitmq_controller::model::resource::rabbitmq_plugins::PluginsConfigMapBuilder; +use crate::rabbitmq_controller::trusted::spec_types::*; +use crate::rabbitmq_controller::trusted::step::*; use crate::reconciler::spec::{io::*, reconciler::*, resource_builder::*}; use crate::state_machine::{action::*, state_machine::*}; use crate::temporal_logic::defs::*; diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/erlang_cookie.rs b/src/controller_examples/rabbitmq_controller/model/resource/erlang_cookie.rs similarity index 94% rename from src/controller_examples/rabbitmq_controller/spec/resource/erlang_cookie.rs rename to src/controller_examples/rabbitmq_controller/model/resource/erlang_cookie.rs index af73e15f8..4a2f39e9e 100644 --- a/src/controller_examples/rabbitmq_controller/spec/resource/erlang_cookie.rs +++ b/src/controller_examples/rabbitmq_controller/model/resource/erlang_cookie.rs @@ -8,9 +8,9 @@ use crate::kubernetes_api_objects::{ volume::*, }; use crate::kubernetes_cluster::spec::message::*; -use crate::rabbitmq_controller::common::*; -use crate::rabbitmq_controller::spec::resource::default_user_secret::DefaultUserSecretBuilder; -use crate::rabbitmq_controller::spec::types::*; +use crate::rabbitmq_controller::model::resource::default_user_secret::DefaultUserSecretBuilder; +use crate::rabbitmq_controller::trusted::spec_types::*; +use crate::rabbitmq_controller::trusted::step::*; use crate::reconciler::spec::{io::*, reconciler::*, resource_builder::*}; use crate::state_machine::{action::*, state_machine::*}; use crate::temporal_logic::defs::*; @@ -117,6 +117,4 @@ pub open spec fn make_erlang_secret(rabbitmq: RabbitmqClusterView) -> SecretView make_secret(rabbitmq, make_erlang_secret_name(rabbitmq), data) } -pub closed spec fn random_encoded_string(length: usize) -> StringView; - } diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/headless_service.rs b/src/controller_examples/rabbitmq_controller/model/resource/headless_service.rs similarity index 96% rename from src/controller_examples/rabbitmq_controller/spec/resource/headless_service.rs rename to src/controller_examples/rabbitmq_controller/model/resource/headless_service.rs index 4157742d3..a2b988e64 100644 --- a/src/controller_examples/rabbitmq_controller/spec/resource/headless_service.rs +++ b/src/controller_examples/rabbitmq_controller/model/resource/headless_service.rs @@ -8,9 +8,9 @@ use crate::kubernetes_api_objects::{ volume::*, }; use crate::kubernetes_cluster::spec::message::*; -use crate::rabbitmq_controller::common::*; -use crate::rabbitmq_controller::spec::resource::service::ServiceBuilder; -use crate::rabbitmq_controller::spec::types::*; +use crate::rabbitmq_controller::model::resource::service::ServiceBuilder; +use crate::rabbitmq_controller::trusted::spec_types::*; +use crate::rabbitmq_controller::trusted::step::*; use crate::reconciler::spec::{io::*, reconciler::*, resource_builder::*}; use crate::state_machine::{action::*, state_machine::*}; use crate::temporal_logic::defs::*; diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/mod.rs b/src/controller_examples/rabbitmq_controller/model/resource/mod.rs similarity index 100% rename from src/controller_examples/rabbitmq_controller/spec/resource/mod.rs rename to src/controller_examples/rabbitmq_controller/model/resource/mod.rs diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/rabbitmq_plugins.rs b/src/controller_examples/rabbitmq_controller/model/resource/rabbitmq_plugins.rs similarity index 96% rename from src/controller_examples/rabbitmq_controller/spec/resource/rabbitmq_plugins.rs rename to src/controller_examples/rabbitmq_controller/model/resource/rabbitmq_plugins.rs index 040eb160f..c6453aa3d 100644 --- a/src/controller_examples/rabbitmq_controller/spec/resource/rabbitmq_plugins.rs +++ b/src/controller_examples/rabbitmq_controller/model/resource/rabbitmq_plugins.rs @@ -8,9 +8,9 @@ use crate::kubernetes_api_objects::{ volume::*, }; use crate::kubernetes_cluster::spec::message::*; -use crate::rabbitmq_controller::common::*; -use crate::rabbitmq_controller::spec::resource::config_map::ServerConfigMapBuilder; -use crate::rabbitmq_controller::spec::types::*; +use crate::rabbitmq_controller::model::resource::config_map::ServerConfigMapBuilder; +use crate::rabbitmq_controller::trusted::spec_types::*; +use crate::rabbitmq_controller::trusted::step::*; use crate::reconciler::spec::{io::*, reconciler::*, resource_builder::*}; use crate::state_machine::{action::*, state_machine::*}; use crate::temporal_logic::defs::*; diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/role.rs b/src/controller_examples/rabbitmq_controller/model/resource/role.rs similarity index 96% rename from src/controller_examples/rabbitmq_controller/spec/resource/role.rs rename to src/controller_examples/rabbitmq_controller/model/resource/role.rs index 6ab8a9556..9c14e2c70 100644 --- a/src/controller_examples/rabbitmq_controller/spec/resource/role.rs +++ b/src/controller_examples/rabbitmq_controller/model/resource/role.rs @@ -8,9 +8,9 @@ use crate::kubernetes_api_objects::{ volume::*, }; use crate::kubernetes_cluster::spec::message::*; -use crate::rabbitmq_controller::common::*; -use crate::rabbitmq_controller::spec::resource::role_binding::RoleBindingBuilder; -use crate::rabbitmq_controller::spec::types::*; +use crate::rabbitmq_controller::model::resource::role_binding::RoleBindingBuilder; +use crate::rabbitmq_controller::trusted::spec_types::*; +use crate::rabbitmq_controller::trusted::step::*; use crate::reconciler::spec::{io::*, reconciler::*, resource_builder::*}; use crate::state_machine::{action::*, state_machine::*}; use crate::temporal_logic::defs::*; diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/role_binding.rs b/src/controller_examples/rabbitmq_controller/model/resource/role_binding.rs similarity index 96% rename from src/controller_examples/rabbitmq_controller/spec/resource/role_binding.rs rename to src/controller_examples/rabbitmq_controller/model/resource/role_binding.rs index 693011886..edaeab471 100644 --- a/src/controller_examples/rabbitmq_controller/spec/resource/role_binding.rs +++ b/src/controller_examples/rabbitmq_controller/model/resource/role_binding.rs @@ -8,9 +8,9 @@ use crate::kubernetes_api_objects::{ volume::*, }; use crate::kubernetes_cluster::spec::message::*; -use crate::rabbitmq_controller::common::*; -use crate::rabbitmq_controller::spec::resource::StatefulSetBuilder; -use crate::rabbitmq_controller::spec::types::*; +use crate::rabbitmq_controller::model::resource::StatefulSetBuilder; +use crate::rabbitmq_controller::trusted::spec_types::*; +use crate::rabbitmq_controller::trusted::step::*; use crate::reconciler::spec::{io::*, reconciler::*, resource_builder::*}; use crate::state_machine::{action::*, state_machine::*}; use crate::temporal_logic::defs::*; diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/service.rs b/src/controller_examples/rabbitmq_controller/model/resource/service.rs similarity index 96% rename from src/controller_examples/rabbitmq_controller/spec/resource/service.rs rename to src/controller_examples/rabbitmq_controller/model/resource/service.rs index 62702ff99..512442088 100644 --- a/src/controller_examples/rabbitmq_controller/spec/resource/service.rs +++ b/src/controller_examples/rabbitmq_controller/model/resource/service.rs @@ -8,9 +8,9 @@ use crate::kubernetes_api_objects::{ volume::*, }; use crate::kubernetes_cluster::spec::message::*; -use crate::rabbitmq_controller::common::*; -use crate::rabbitmq_controller::spec::resource::erlang_cookie::ErlangCookieBuilder; -use crate::rabbitmq_controller::spec::types::*; +use crate::rabbitmq_controller::model::resource::erlang_cookie::ErlangCookieBuilder; +use crate::rabbitmq_controller::trusted::spec_types::*; +use crate::rabbitmq_controller::trusted::step::*; use crate::reconciler::spec::{io::*, reconciler::*, resource_builder::*}; use crate::state_machine::{action::*, state_machine::*}; use crate::temporal_logic::defs::*; diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/service_account.rs b/src/controller_examples/rabbitmq_controller/model/resource/service_account.rs similarity index 96% rename from src/controller_examples/rabbitmq_controller/spec/resource/service_account.rs rename to src/controller_examples/rabbitmq_controller/model/resource/service_account.rs index 017887586..5aff38b4a 100644 --- a/src/controller_examples/rabbitmq_controller/spec/resource/service_account.rs +++ b/src/controller_examples/rabbitmq_controller/model/resource/service_account.rs @@ -8,9 +8,9 @@ use crate::kubernetes_api_objects::{ volume::*, }; use crate::kubernetes_cluster::spec::message::*; -use crate::rabbitmq_controller::common::*; -use crate::rabbitmq_controller::spec::resource::role::RoleBuilder; -use crate::rabbitmq_controller::spec::types::*; +use crate::rabbitmq_controller::model::resource::role::RoleBuilder; +use crate::rabbitmq_controller::trusted::spec_types::*; +use crate::rabbitmq_controller::trusted::step::*; use crate::reconciler::spec::{io::*, reconciler::*, resource_builder::*}; use crate::state_machine::{action::*, state_machine::*}; use crate::temporal_logic::defs::*; diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/stateful_set.rs b/src/controller_examples/rabbitmq_controller/model/resource/stateful_set.rs similarity index 98% rename from src/controller_examples/rabbitmq_controller/spec/resource/stateful_set.rs rename to src/controller_examples/rabbitmq_controller/model/resource/stateful_set.rs index 345f26e30..6d5db19d7 100644 --- a/src/controller_examples/rabbitmq_controller/spec/resource/stateful_set.rs +++ b/src/controller_examples/rabbitmq_controller/model/resource/stateful_set.rs @@ -8,9 +8,9 @@ use crate::kubernetes_api_objects::{ volume::*, }; use crate::kubernetes_cluster::spec::message::*; -use crate::rabbitmq_controller::common::*; -use crate::rabbitmq_controller::spec::resource::config_map::make_server_config_map_key; -use crate::rabbitmq_controller::spec::types::*; +use crate::rabbitmq_controller::model::resource::config_map::make_server_config_map_key; +use crate::rabbitmq_controller::trusted::spec_types::*; +use crate::rabbitmq_controller::trusted::step::*; use crate::reconciler::spec::{io::*, reconciler::*, resource_builder::*}; use crate::state_machine::{action::*, state_machine::*}; use crate::temporal_logic::defs::*; 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 index ff7f0aff4..187c93088 100644 --- 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::*, + model::reconciler::*, proof::{ helper_invariants::{predicate::*, proof::*}, predicate::*, resource::*, }, - spec::{reconciler::*, types::*}, + 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 index 03e2806fe..2c1984c85 100644 --- 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::*, + model::reconciler::*, proof::{predicate::*, resource::*}, - spec::{reconciler::*, types::*}, + 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 index 16f17aad5..43787e554 100644 --- 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::*, + model::resource::make_stateful_set, 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::*}, + 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 index b2e3e8ae3..38c29e35f 100644 --- 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::*, + model::{reconciler::*, resource::*}, proof::{ helper_invariants::{owner_ref::*, predicate::*, proof::*, validation::*}, predicate::*, resource::*, }, - spec::{reconciler::*, resource::*, types::*}, + 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 index 602d646f3..4099249b0 100644 --- 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::*, + model::{reconciler::*, resource::*}, proof::{ helper_invariants::{owner_ref::*, predicate::*, proof::*}, predicate::*, resource::*, }, - spec::{reconciler::*, resource::*, types::*}, + 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/liveness/proof.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/proof.rs index 862df01e5..89e267fee 100644 --- a/src/controller_examples/rabbitmq_controller/proof/liveness/proof.rs +++ b/src/controller_examples/rabbitmq_controller/proof/liveness/proof.rs @@ -13,7 +13,7 @@ use crate::kubernetes_cluster::spec::{ message::*, }; use crate::rabbitmq_controller::{ - common::*, + model::{reconciler::*, resource::*}, proof::{ helper_invariants, liveness::{ @@ -25,11 +25,10 @@ use crate::rabbitmq_controller::{ }, terminate, }, - liveness_theorem::*, predicate::*, resource::*, }, - spec::{reconciler::*, resource::*, types::*}, + trusted::{liveness_theorem::*, spec_types::*, step::*}, }; use crate::temporal_logic::{defs::*, rules::*}; use crate::vstd_ext::{map_lib::*, string_view::*}; @@ -40,17 +39,17 @@ verus! { // We prove init /\ []next /\ []wf |= []RMQCluster::desired_state_is(rabbitmq) ~> []current_state_matches(rabbitmq) holds for each rabbitmq. proof fn liveness_proof_forall_rabbitmq() ensures - liveness_theorem(), + liveness_theorem::(), { - assert forall |rabbitmq: RabbitmqClusterView| #[trigger] cluster_spec().entails(liveness(rabbitmq)) by { + assert forall |rabbitmq: RabbitmqClusterView| #[trigger] cluster_spec().entails(liveness::(rabbitmq)) by { liveness_proof(rabbitmq); }; - spec_entails_tla_forall(cluster_spec(), |rabbitmq: RabbitmqClusterView| liveness(rabbitmq)); + spec_entails_tla_forall(cluster_spec(), |rabbitmq: RabbitmqClusterView| liveness::(rabbitmq)); } proof fn liveness_proof(rabbitmq: RabbitmqClusterView) ensures - cluster_spec().entails(liveness(rabbitmq)), + cluster_spec().entails(liveness::(rabbitmq)), { assumption_and_invariants_of_all_phases_is_stable(rabbitmq); lemma_true_leads_to_always_current_state_matches(rabbitmq); @@ -64,12 +63,12 @@ proof fn liveness_proof(rabbitmq: RabbitmqClusterView) spec_before_phase_n_entails_true_leads_to_current_state_matches(1, rabbitmq); let assumption = always(lift_state(RMQCluster::desired_state_is(rabbitmq))); - unpack_conditions_from_spec(invariants(rabbitmq), assumption, true_pred(), always(lift_state(current_state_matches(rabbitmq)))); + unpack_conditions_from_spec(invariants(rabbitmq), assumption, true_pred(), always(lift_state(current_state_matches::(rabbitmq)))); temp_pred_equality(true_pred().and(assumption), assumption); valid_implies_trans( cluster_spec().and(derived_invariants_since_beginning(rabbitmq)), invariants(rabbitmq), - always(lift_state(RMQCluster::desired_state_is(rabbitmq))).leads_to(always(lift_state(current_state_matches(rabbitmq)))) + always(lift_state(RMQCluster::desired_state_is(rabbitmq))).leads_to(always(lift_state(current_state_matches::(rabbitmq)))) ); sm_spec_entails_all_invariants(rabbitmq); simplify_predicate(cluster_spec(), derived_invariants_since_beginning(rabbitmq)); @@ -79,38 +78,38 @@ proof fn spec_before_phase_n_entails_true_leads_to_current_state_matches(i: nat, requires 1 <= i <= 7, valid(stable(spec_before_phase_n(i, rabbitmq))), - spec_before_phase_n(i + 1, rabbitmq).entails(true_pred().leads_to(always(lift_state(current_state_matches(rabbitmq))))) + spec_before_phase_n(i + 1, rabbitmq).entails(true_pred().leads_to(always(lift_state(current_state_matches::(rabbitmq))))) ensures - spec_before_phase_n(i, rabbitmq).entails(true_pred().leads_to(always(lift_state(current_state_matches(rabbitmq))))), + spec_before_phase_n(i, rabbitmq).entails(true_pred().leads_to(always(lift_state(current_state_matches::(rabbitmq))))), { reveal_with_fuel(spec_before_phase_n, 8); temp_pred_equality(spec_before_phase_n(i + 1, rabbitmq), spec_before_phase_n(i, rabbitmq).and(invariants_since_phase_n(i, rabbitmq))); spec_of_previous_phases_entails_eventually_new_invariants(i, rabbitmq); - unpack_conditions_from_spec(spec_before_phase_n(i, rabbitmq), invariants_since_phase_n(i, rabbitmq), true_pred(), always(lift_state(current_state_matches(rabbitmq)))); + unpack_conditions_from_spec(spec_before_phase_n(i, rabbitmq), invariants_since_phase_n(i, rabbitmq), true_pred(), always(lift_state(current_state_matches::(rabbitmq)))); temp_pred_equality(true_pred().and(invariants_since_phase_n(i, rabbitmq)), invariants_since_phase_n(i, rabbitmq)); - leads_to_trans_temp(spec_before_phase_n(i, rabbitmq), true_pred(), invariants_since_phase_n(i, rabbitmq), always(lift_state(current_state_matches(rabbitmq)))); + leads_to_trans_temp(spec_before_phase_n(i, rabbitmq), true_pred(), invariants_since_phase_n(i, rabbitmq), always(lift_state(current_state_matches::(rabbitmq)))); } proof fn lemma_true_leads_to_always_current_state_matches(rabbitmq: RabbitmqClusterView) ensures assumption_and_invariants_of_all_phases(rabbitmq) .entails( - true_pred().leads_to(always(lift_state(current_state_matches(rabbitmq)))) + true_pred().leads_to(always(lift_state(current_state_matches::(rabbitmq)))) ), { let spec = assumption_and_invariants_of_all_phases(rabbitmq); lemma_true_leads_to_always_state_matches_for_all_resources(rabbitmq); let a_to_p = |res: SubResource| lift_state(sub_resource_state_matches(res, rabbitmq)); helper_invariants::leads_to_always_tla_forall_subresource(spec, true_pred(), a_to_p); - assert forall |ex| #[trigger] tla_forall(a_to_p).satisfied_by(ex) implies lift_state(current_state_matches(rabbitmq)).satisfied_by(ex) by { + assert forall |ex| #[trigger] tla_forall(a_to_p).satisfied_by(ex) implies lift_state(current_state_matches::(rabbitmq)).satisfied_by(ex) by { let s = ex.head(); - assert forall |res: SubResource| #[trigger] resource_state_matches(res, rabbitmq, s.resources()) by { + assert forall |res: SubResource| #[trigger] resource_state_matches::(res, rabbitmq, s.resources()) by { tla_forall_apply(a_to_p, res); assert(a_to_p(res).satisfied_by(ex)); assert(sub_resource_state_matches(res, rabbitmq)(s)); } } - temp_pred_equality(tla_forall(|res: SubResource| lift_state(sub_resource_state_matches(res, rabbitmq))), lift_state(current_state_matches(rabbitmq))); + temp_pred_equality(tla_forall(|res: SubResource| lift_state(sub_resource_state_matches(res, rabbitmq))), lift_state(current_state_matches::(rabbitmq))); } proof fn lemma_true_leads_to_always_state_matches_for_all_resources(rabbitmq: RabbitmqClusterView) diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs index 36d15f397..c3907e578 100644 --- a/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs +++ b/src/controller_examples/rabbitmq_controller/proof/liveness/resource_match.rs @@ -13,12 +13,12 @@ use crate::kubernetes_cluster::spec::{ message::*, }; use crate::rabbitmq_controller::{ - common::*, + model::{reconciler::*, resource::*}, proof::{ - helper_invariants, liveness::spec::assumption_and_invariants_of_all_phases, - liveness_theorem::*, predicate::*, resource::*, + helper_invariants, liveness::spec::assumption_and_invariants_of_all_phases, predicate::*, + resource::*, }, - spec::{reconciler::*, resource::*, types::*}, + trusted::{liveness_theorem::*, spec_types::*, step::*}, }; use crate::temporal_logic::{defs::*, rules::*}; use crate::vstd_ext::{map_lib::*, string_view::*}; diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness/spec.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/spec.rs index ada09e743..8ee329071 100644 --- a/src/controller_examples/rabbitmq_controller/proof/liveness/spec.rs +++ b/src/controller_examples/rabbitmq_controller/proof/liveness/spec.rs @@ -14,11 +14,9 @@ use crate::kubernetes_cluster::spec::{ message::*, }; use crate::rabbitmq_controller::{ - common::*, - proof::{ - helper_invariants, liveness::terminate, liveness_theorem::*, predicate::*, resource::*, - }, - spec::{reconciler::*, types::*}, + model::reconciler::*, + proof::{helper_invariants, liveness::terminate, predicate::*, resource::*}, + trusted::{liveness_theorem::*, spec_types::*, step::*}, }; use crate::temporal_logic::{defs::*, rules::*}; use vstd::prelude::*; diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness/stateful_set_match.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/stateful_set_match.rs index f0decf23d..b1439e247 100644 --- a/src/controller_examples/rabbitmq_controller/proof/liveness/stateful_set_match.rs +++ b/src/controller_examples/rabbitmq_controller/proof/liveness/stateful_set_match.rs @@ -13,15 +13,14 @@ use crate::kubernetes_cluster::spec::{ message::*, }; use crate::rabbitmq_controller::{ - common::*, + model::{reconciler::*, resource::*}, proof::{ helper_invariants, liveness::{resource_match::*, spec::assumption_and_invariants_of_all_phases}, - liveness_theorem::*, predicate::*, resource::*, }, - spec::{reconciler::*, resource::*, types::*}, + trusted::{liveness_theorem::*, spec_types::*, step::*}, }; use crate::temporal_logic::{defs::*, rules::*}; use crate::vstd_ext::{map_lib::*, string_view::*}; diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness/terminate.rs b/src/controller_examples/rabbitmq_controller/proof/liveness/terminate.rs index 366b3cfcd..d210523d7 100644 --- a/src/controller_examples/rabbitmq_controller/proof/liveness/terminate.rs +++ b/src/controller_examples/rabbitmq_controller/proof/liveness/terminate.rs @@ -11,9 +11,9 @@ use crate::kubernetes_cluster::spec::{ message::*, }; use crate::rabbitmq_controller::{ - common::*, + model::reconciler::*, proof::predicate::*, - spec::{reconciler::*, types::*}, + trusted::{spec_types::*, step::*}, }; use crate::reconciler::spec::reconciler::*; use crate::temporal_logic::{defs::*, rules::*}; diff --git a/src/controller_examples/rabbitmq_controller/proof/mod.rs b/src/controller_examples/rabbitmq_controller/proof/mod.rs index 31c38b5ce..8b79179df 100644 --- a/src/controller_examples/rabbitmq_controller/proof/mod.rs +++ b/src/controller_examples/rabbitmq_controller/proof/mod.rs @@ -2,8 +2,6 @@ // SPDX-License-Identifier: MIT pub mod helper_invariants; pub mod liveness; -pub mod liveness_theorem; pub mod predicate; pub mod resource; pub mod safety; -pub mod safety_theorem; diff --git a/src/controller_examples/rabbitmq_controller/proof/predicate.rs b/src/controller_examples/rabbitmq_controller/proof/predicate.rs index e4067f841..b515ed52f 100644 --- a/src/controller_examples/rabbitmq_controller/proof/predicate.rs +++ b/src/controller_examples/rabbitmq_controller/proof/predicate.rs @@ -11,9 +11,11 @@ use crate::kubernetes_cluster::spec::{ controller::common::{ControllerActionInput, ControllerStep}, message::*, }; -use crate::rabbitmq_controller::common::*; -use crate::rabbitmq_controller::proof::{liveness_theorem::resource_state_matches, resource::*}; -use crate::rabbitmq_controller::spec::{reconciler::*, resource::*, types::*}; +use crate::rabbitmq_controller::model::{reconciler::*, resource::*}; +use crate::rabbitmq_controller::proof::resource::*; +use crate::rabbitmq_controller::trusted::{ + liveness_theorem::resource_state_matches, spec_types::*, step::*, +}; use crate::temporal_logic::defs::*; use vstd::prelude::*; @@ -21,7 +23,7 @@ verus! { pub open spec fn sub_resource_state_matches(sub_resource: SubResource, rabbitmq: RabbitmqClusterView) -> StatePred { |s: RMQCluster| { - resource_state_matches(sub_resource, rabbitmq, s.resources()) + resource_state_matches::(sub_resource, rabbitmq, s.resources()) } } diff --git a/src/controller_examples/rabbitmq_controller/proof/resource.rs b/src/controller_examples/rabbitmq_controller/proof/resource.rs index 1c4a60a88..bd6797005 100644 --- a/src/controller_examples/rabbitmq_controller/proof/resource.rs +++ b/src/controller_examples/rabbitmq_controller/proof/resource.rs @@ -7,9 +7,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::spec::resource::*; -use crate::rabbitmq_controller::spec::types::{RabbitmqClusterView, RabbitmqReconcileState}; +use crate::rabbitmq_controller::model::resource::*; +use crate::rabbitmq_controller::trusted::spec_types::{ + RabbitmqClusterView, RabbitmqReconcileState, +}; +use crate::rabbitmq_controller::trusted::step::*; use crate::reconciler::spec::resource_builder::*; use crate::vstd_ext::string_map::StringMap; use crate::vstd_ext::string_view::*; diff --git a/src/controller_examples/rabbitmq_controller/proof/safety/proof.rs b/src/controller_examples/rabbitmq_controller/proof/safety/proof.rs index 60164e811..214514e49 100644 --- a/src/controller_examples/rabbitmq_controller/proof/safety/proof.rs +++ b/src/controller_examples/rabbitmq_controller/proof/safety/proof.rs @@ -12,9 +12,9 @@ use crate::kubernetes_cluster::spec::{ message::*, }; use crate::rabbitmq_controller::{ - common::*, - proof::{helper_invariants::*, predicate::*, resource::*, safety_theorem::*}, - spec::{reconciler::*, resource::*, types::*}, + model::{reconciler::*, resource::*}, + proof::{helper_invariants::*, predicate::*, resource::*}, + trusted::{safety_theorem::*, spec_types::*, step::*}, }; use crate::temporal_logic::{defs::*, rules::*}; use vstd::prelude::*; @@ -23,17 +23,17 @@ verus! { proof fn safety_proof_forall_rabbitmq() ensures - safety_theorem(), + safety_theorem::(), { - assert forall |rabbitmq: RabbitmqClusterView| #[trigger] cluster_spec_without_wf().entails(safety(rabbitmq)) by { + assert forall |rabbitmq: RabbitmqClusterView| #[trigger] cluster_spec_without_wf().entails(safety::(rabbitmq)) by { safety_proof(rabbitmq); }; - spec_entails_tla_forall(cluster_spec_without_wf(), |rabbitmq: RabbitmqClusterView| safety(rabbitmq)); + spec_entails_tla_forall(cluster_spec_without_wf(), |rabbitmq: RabbitmqClusterView| safety::(rabbitmq)); } proof fn safety_proof(rabbitmq: RabbitmqClusterView) ensures - cluster_spec_without_wf().entails(safety(rabbitmq)), + cluster_spec_without_wf().entails(safety::(rabbitmq)), { lemma_stateful_set_never_scaled_down_for_rabbitmq(cluster_spec_without_wf(), rabbitmq); } @@ -48,9 +48,9 @@ proof fn lemma_stateful_set_never_scaled_down_for_rabbitmq(spec: TempPred(rabbitmq)))), { - let inv = stateful_set_not_scaled_down(rabbitmq); + let inv = stateful_set_not_scaled_down::(rabbitmq); let next = |s, s_prime| { &&& RMQCluster::next()(s, s_prime) &&& replicas_of_stateful_set_update_request_msg_is_no_smaller_than_etcd(rabbitmq)(s) @@ -62,7 +62,7 @@ proof fn lemma_stateful_set_never_scaled_down_for_rabbitmq(spec: TempPred(rabbitmq)(s, s_prime) by { let sts_key = make_stateful_set_key(rabbitmq); if s.resources().contains_key(sts_key) && s_prime.resources().contains_key(sts_key) { if s.resources()[sts_key].spec != s_prime.resources()[sts_key].spec { diff --git a/src/controller_examples/rabbitmq_controller/exec/types.rs b/src/controller_examples/rabbitmq_controller/trusted/exec_types.rs similarity index 85% rename from src/controller_examples/rabbitmq_controller/exec/types.rs rename to src/controller_examples/rabbitmq_controller/trusted/exec_types.rs index 02d6f2b9d..b006f1936 100644 --- a/src/controller_examples/rabbitmq_controller/exec/types.rs +++ b/src/controller_examples/rabbitmq_controller/trusted/exec_types.rs @@ -5,8 +5,7 @@ use crate::kubernetes_api_objects::{ affinity::*, api_resource::*, common::*, dynamic::*, marshal::*, object_meta::*, owner_reference::*, resource::*, resource_requirements::*, stateful_set::*, toleration::*, }; -use crate::rabbitmq_controller::common::*; -use crate::rabbitmq_controller::spec::types as spec_types; +use crate::rabbitmq_controller::trusted::{spec_types, step::*}; use crate::vstd_ext::{string_map::*, string_view::*}; use deps_hack::kube::Resource; use vstd::prelude::*; @@ -67,54 +66,43 @@ impl View for RabbitmqCluster { impl RabbitmqCluster { #[verifier(external_body)] pub fn metadata(&self) -> (metadata: ObjectMeta) - ensures - metadata@ == self@.metadata, + ensures metadata@ == self@.metadata, { ObjectMeta::from_kube(self.inner.metadata.clone()) } #[verifier(external_body)] pub fn spec(&self) -> (spec: RabbitmqClusterSpec) - ensures - spec@ == self@.spec, + ensures spec@ == self@.spec, { RabbitmqClusterSpec { inner: self.inner.spec.clone() } } #[verifier(external)] - pub fn into_kube(self) -> deps_hack::RabbitmqCluster { - self.inner - } + pub fn into_kube(self) -> deps_hack::RabbitmqCluster { self.inner } #[verifier(external_body)] pub fn api_resource() -> (res: ApiResource) - ensures - res@.kind == spec_types::RabbitmqClusterView::kind(), + ensures res@.kind == spec_types::RabbitmqClusterView::kind(), { ApiResource::from_kube(deps_hack::kube::api::ApiResource::erase::(&())) } #[verifier(external_body)] pub fn controller_owner_ref(&self) -> (owner_reference: OwnerReference) - ensures - owner_reference@ == self@.controller_owner_ref(), + ensures owner_reference@ == self@.controller_owner_ref(), { - OwnerReference::from_kube( - // We can safely unwrap here because the trait method implementation always returns a Some(...) - self.inner.controller_owner_ref(&()).unwrap() - ) + // We can safely unwrap here because the trait method implementation always returns a Some(...) + OwnerReference::from_kube(self.inner.controller_owner_ref(&()).unwrap()) } // NOTE: This function assumes serde_json::to_string won't fail! #[verifier(external_body)] pub fn marshal(self) -> (obj: DynamicObject) - ensures - obj@ == self@.marshal(), + ensures obj@ == self@.marshal(), { // TODO: this might be unnecessarily slow - DynamicObject::from_kube( - deps_hack::k8s_openapi::serde_json::from_str(&deps_hack::k8s_openapi::serde_json::to_string(&self.inner).unwrap()).unwrap() - ) + DynamicObject::from_kube(deps_hack::k8s_openapi::serde_json::from_str(&deps_hack::k8s_openapi::serde_json::to_string(&self.inner).unwrap()).unwrap()) } #[verifier(external_body)] @@ -135,16 +123,10 @@ impl RabbitmqCluster { impl ResourceWrapper for RabbitmqCluster { #[verifier(external)] - fn from_kube(inner: deps_hack::RabbitmqCluster) -> RabbitmqCluster { - RabbitmqCluster { - inner: inner - } - } + fn from_kube(inner: deps_hack::RabbitmqCluster) -> RabbitmqCluster { RabbitmqCluster { inner: inner } } #[verifier(external)] - fn into_kube(self) -> deps_hack::RabbitmqCluster { - self.inner - } + fn into_kube(self) -> deps_hack::RabbitmqCluster { self.inner } } #[verifier(external_body)] @@ -157,16 +139,14 @@ impl RabbitmqClusterSpec { #[verifier(external_body)] pub fn replicas(&self) -> (replicas: i32) - ensures - replicas as int == self@.replicas, + ensures replicas as int == self@.replicas, { self.inner.replicas } #[verifier(external_body)] pub fn image(&self) -> (image: String) - ensures - image@ == self@.image, + ensures image@ == self@.image, { String::from_rust_string(self.inner.image.clone()) } @@ -185,8 +165,7 @@ impl RabbitmqClusterSpec { #[verifier(external_body)] pub fn persistence(&self) -> (persistence: RabbitmqClusterPersistenceSpec) - ensures - persistence@ == self@.persistence, + ensures persistence@ == self@.persistence, { RabbitmqClusterPersistenceSpec { inner: self.inner.persistence.clone() } } @@ -217,16 +196,14 @@ impl RabbitmqClusterSpec { #[verifier(external_body)] pub fn labels(&self) -> (labels: StringMap) - ensures - labels@ == self@.labels, + ensures labels@ == self@.labels, { StringMap::from_rust_map(self.inner.labels.clone()) } #[verifier(external_body)] pub fn annotations(&self) -> (annotations: StringMap) - ensures - annotations@ == self@.annotations, + ensures annotations@ == self@.annotations, { StringMap::from_rust_map(self.inner.annotations.clone()) } @@ -245,8 +222,7 @@ impl RabbitmqClusterSpec { #[verifier(external_body)] pub fn pod_management_policy(&self) -> (policy: String) - ensures - policy@ == self@.pod_management_policy, + ensures policy@ == self@.pod_management_policy, { String::from_rust_string(self.inner.pod_management_policy.clone()) } @@ -319,19 +295,26 @@ impl RabbitmqClusterPersistenceSpec { #[verifier(external_body)] pub fn storage(&self) -> (storage: String) - ensures - storage@ == self@.storage, + ensures storage@ == self@.storage, { String::from_rust_string(self.inner.storage.clone().0) } #[verifier(external_body)] pub fn storage_class_name(&self) -> (storage_class_name: String) - ensures - storage_class_name@ == self@.storage_class_name, + ensures storage_class_name@ == self@.storage_class_name, { String::from_rust_string(self.inner.storage_class_name.clone()) } } +#[verifier(external_body)] +pub fn random_encoded_string(data_len: usize) -> (cookie: String) + ensures + cookie@ == spec_types::random_encoded_string(data_len), +{ + let random_bytes: std::vec::Vec = (0..data_len).map(|_| deps_hack::rand::random::()).collect(); + String::from_rust_string(deps_hack::base64::encode(random_bytes)) +} + } diff --git a/src/controller_examples/rabbitmq_controller/proof/liveness_theorem.rs b/src/controller_examples/rabbitmq_controller/trusted/liveness_theorem.rs similarity index 51% rename from src/controller_examples/rabbitmq_controller/proof/liveness_theorem.rs rename to src/controller_examples/rabbitmq_controller/trusted/liveness_theorem.rs index 7c493083a..acdd4578c 100644 --- a/src/controller_examples/rabbitmq_controller/proof/liveness_theorem.rs +++ b/src/controller_examples/rabbitmq_controller/trusted/liveness_theorem.rs @@ -3,45 +3,42 @@ #![allow(unused_imports)] use crate::kubernetes_api_objects::prelude::*; use crate::kubernetes_cluster::spec::{cluster::*, cluster_state_machine::Step, message::*}; -use crate::rabbitmq_controller::{ - common::*, - spec::{reconciler::*, resource::*, types::*}, -}; -use crate::temporal_logic::{defs::*, rules::*}; +use crate::rabbitmq_controller::trusted::{maker::*, spec_types::*, step::*}; +use crate::temporal_logic::defs::*; use crate::vstd_ext::string_view::int_to_string_view; use vstd::prelude::*; verus! { -pub open spec fn liveness_theorem() -> bool { - cluster_spec().entails(tla_forall(|rabbitmq: RabbitmqClusterView| liveness(rabbitmq))) +pub open spec fn liveness_theorem() -> bool { + cluster_spec().entails(tla_forall(|rabbitmq: RabbitmqClusterView| liveness::(rabbitmq))) } pub open spec fn cluster_spec() -> TempPred { RMQCluster::sm_spec() } -pub open spec fn liveness(rabbitmq: RabbitmqClusterView) -> TempPred { - always(lift_state(desired_state_is(rabbitmq))).leads_to(always(lift_state(current_state_matches(rabbitmq)))) +pub open spec fn liveness(rabbitmq: RabbitmqClusterView) -> TempPred { + always(lift_state(desired_state_is(rabbitmq))).leads_to(always(lift_state(current_state_matches::(rabbitmq)))) } pub open spec fn desired_state_is(rabbitmq: RabbitmqClusterView) -> StatePred { RMQCluster::desired_state_is(rabbitmq) } -pub open spec fn current_state_matches(rabbitmq: RabbitmqClusterView) -> StatePred { +pub open spec fn current_state_matches(rabbitmq: RabbitmqClusterView) -> StatePred { |s: RMQCluster| { forall |sub_resource: SubResource| - #[trigger] resource_state_matches(sub_resource, rabbitmq, s.resources()) + #[trigger] resource_state_matches::(sub_resource, rabbitmq, s.resources()) } } -pub open spec fn resource_state_matches(sub_resource: SubResource, rabbitmq: RabbitmqClusterView, resources: StoredState) -> bool { +pub open spec fn resource_state_matches(sub_resource: SubResource, rabbitmq: RabbitmqClusterView, resources: StoredState) -> bool { match sub_resource { SubResource::HeadlessService => { - let key = make_headless_service_key(rabbitmq); + let key = M::make_headless_service_key(rabbitmq); let obj = resources[key]; - let made_spec = make_headless_service(rabbitmq).spec.get_Some_0(); + let made_spec = M::make_headless_service(rabbitmq).spec.get_Some_0(); let spec = ServiceView::unmarshal(obj).get_Ok_0().spec.get_Some_0(); &&& resources.contains_key(key) &&& ServiceView::unmarshal(obj).is_Ok() @@ -50,13 +47,13 @@ pub open spec fn resource_state_matches(sub_resource: SubResource, rabbitmq: Rab cluster_ip: made_spec.cluster_ip, ..spec } - &&& obj.metadata.labels == make_headless_service(rabbitmq).metadata.labels - &&& obj.metadata.annotations == make_headless_service(rabbitmq).metadata.annotations + &&& obj.metadata.labels == M::make_headless_service(rabbitmq).metadata.labels + &&& obj.metadata.annotations == M::make_headless_service(rabbitmq).metadata.annotations }, SubResource::Service => { - let key = make_main_service_key(rabbitmq); + let key = M::make_main_service_key(rabbitmq); let obj = resources[key]; - let made_spec = make_main_service(rabbitmq).spec.get_Some_0(); + let made_spec = M::make_main_service(rabbitmq).spec.get_Some_0(); let spec = ServiceView::unmarshal(obj).get_Ok_0().spec.get_Some_0(); &&& resources.contains_key(key) &&& ServiceView::unmarshal(obj).is_Ok() @@ -65,80 +62,80 @@ pub open spec fn resource_state_matches(sub_resource: SubResource, rabbitmq: Rab cluster_ip: made_spec.cluster_ip, ..spec } - &&& obj.metadata.labels == make_main_service(rabbitmq).metadata.labels - &&& obj.metadata.annotations == make_main_service(rabbitmq).metadata.annotations + &&& obj.metadata.labels == M::make_main_service(rabbitmq).metadata.labels + &&& obj.metadata.annotations == M::make_main_service(rabbitmq).metadata.annotations }, SubResource::ErlangCookieSecret => { - let key = make_erlang_secret_key(rabbitmq); + let key = M::make_erlang_secret_key(rabbitmq); let obj = resources[key]; &&& resources.contains_key(key) &&& SecretView::unmarshal(obj).is_Ok() - &&& SecretView::unmarshal(obj).get_Ok_0().data == make_erlang_secret(rabbitmq).data - &&& obj.metadata.labels == make_erlang_secret(rabbitmq).metadata.labels - &&& obj.metadata.annotations == make_erlang_secret(rabbitmq).metadata.annotations + &&& SecretView::unmarshal(obj).get_Ok_0().data == M::make_erlang_secret(rabbitmq).data + &&& obj.metadata.labels == M::make_erlang_secret(rabbitmq).metadata.labels + &&& obj.metadata.annotations == M::make_erlang_secret(rabbitmq).metadata.annotations }, SubResource::DefaultUserSecret => { - let key = make_default_user_secret_key(rabbitmq); + let key = M::make_default_user_secret_key(rabbitmq); let obj = resources[key]; &&& resources.contains_key(key) &&& SecretView::unmarshal(obj).is_Ok() - &&& SecretView::unmarshal(obj).get_Ok_0().data == make_default_user_secret(rabbitmq).data - &&& obj.metadata.labels == make_default_user_secret(rabbitmq).metadata.labels - &&& obj.metadata.annotations == make_default_user_secret(rabbitmq).metadata.annotations + &&& SecretView::unmarshal(obj).get_Ok_0().data == M::make_default_user_secret(rabbitmq).data + &&& obj.metadata.labels == M::make_default_user_secret(rabbitmq).metadata.labels + &&& obj.metadata.annotations == M::make_default_user_secret(rabbitmq).metadata.annotations }, SubResource::PluginsConfigMap => { - let key = make_plugins_config_map_key(rabbitmq); + let key = M::make_plugins_config_map_key(rabbitmq); let obj = resources[key]; &&& resources.contains_key(key) &&& ConfigMapView::unmarshal(obj).is_Ok() - &&& ConfigMapView::unmarshal(obj).get_Ok_0().data == make_plugins_config_map(rabbitmq).data - &&& obj.metadata.labels == make_plugins_config_map(rabbitmq).metadata.labels - &&& obj.metadata.annotations == make_plugins_config_map(rabbitmq).metadata.annotations + &&& ConfigMapView::unmarshal(obj).get_Ok_0().data == M::make_plugins_config_map(rabbitmq).data + &&& obj.metadata.labels == M::make_plugins_config_map(rabbitmq).metadata.labels + &&& obj.metadata.annotations == M::make_plugins_config_map(rabbitmq).metadata.annotations }, SubResource::ServerConfigMap => { - let key = make_server_config_map_key(rabbitmq); + let key = M::make_server_config_map_key(rabbitmq); let obj = resources[key]; &&& resources.contains_key(key) &&& ConfigMapView::unmarshal(obj).is_Ok() - &&& ConfigMapView::unmarshal(obj).get_Ok_0().data == make_server_config_map(rabbitmq).data - &&& obj.spec == ConfigMapView::marshal_spec((make_server_config_map(rabbitmq).data, ())) - &&& obj.metadata.labels == make_server_config_map(rabbitmq).metadata.labels - &&& obj.metadata.annotations == make_server_config_map(rabbitmq).metadata.annotations + &&& ConfigMapView::unmarshal(obj).get_Ok_0().data == M::make_server_config_map(rabbitmq).data + &&& obj.spec == ConfigMapView::marshal_spec((M::make_server_config_map(rabbitmq).data, ())) + &&& obj.metadata.labels == M::make_server_config_map(rabbitmq).metadata.labels + &&& obj.metadata.annotations == M::make_server_config_map(rabbitmq).metadata.annotations }, SubResource::ServiceAccount => { - let key = make_service_account_key(rabbitmq); + let key = M::make_service_account_key(rabbitmq); let obj = resources[key]; &&& resources.contains_key(key) &&& ServiceAccountView::unmarshal(obj).is_Ok() - &&& ServiceAccountView::unmarshal(obj).get_Ok_0().automount_service_account_token == make_service_account(rabbitmq).automount_service_account_token - &&& obj.metadata.labels == make_service_account(rabbitmq).metadata.labels - &&& obj.metadata.annotations == make_service_account(rabbitmq).metadata.annotations + &&& ServiceAccountView::unmarshal(obj).get_Ok_0().automount_service_account_token == M::make_service_account(rabbitmq).automount_service_account_token + &&& obj.metadata.labels == M::make_service_account(rabbitmq).metadata.labels + &&& obj.metadata.annotations == M::make_service_account(rabbitmq).metadata.annotations }, SubResource::Role => { - let key = make_role_key(rabbitmq); + let key = M::make_role_key(rabbitmq); let obj = resources[key]; &&& resources.contains_key(key) &&& RoleView::unmarshal(obj).is_Ok() - &&& RoleView::unmarshal(obj).get_Ok_0().policy_rules == make_role(rabbitmq).policy_rules - &&& obj.metadata.labels == make_role(rabbitmq).metadata.labels - &&& obj.metadata.annotations == make_role(rabbitmq).metadata.annotations + &&& RoleView::unmarshal(obj).get_Ok_0().policy_rules == M::make_role(rabbitmq).policy_rules + &&& obj.metadata.labels == M::make_role(rabbitmq).metadata.labels + &&& obj.metadata.annotations == M::make_role(rabbitmq).metadata.annotations }, SubResource::RoleBinding => { - let key = make_role_binding_key(rabbitmq); + let key = M::make_role_binding_key(rabbitmq); let obj = resources[key]; &&& resources.contains_key(key) &&& RoleBindingView::unmarshal(obj).is_Ok() - &&& RoleBindingView::unmarshal(obj).get_Ok_0().role_ref == make_role_binding(rabbitmq).role_ref - &&& RoleBindingView::unmarshal(obj).get_Ok_0().subjects == make_role_binding(rabbitmq).subjects - &&& obj.metadata.labels == make_role_binding(rabbitmq).metadata.labels - &&& obj.metadata.annotations == make_role_binding(rabbitmq).metadata.annotations + &&& RoleBindingView::unmarshal(obj).get_Ok_0().role_ref == M::make_role_binding(rabbitmq).role_ref + &&& RoleBindingView::unmarshal(obj).get_Ok_0().subjects == M::make_role_binding(rabbitmq).subjects + &&& obj.metadata.labels == M::make_role_binding(rabbitmq).metadata.labels + &&& obj.metadata.annotations == M::make_role_binding(rabbitmq).metadata.annotations }, SubResource::StatefulSet => { - let key = make_stateful_set_key(rabbitmq); + let key = M::make_stateful_set_key(rabbitmq); let obj = resources[key]; - let cm_key = make_server_config_map_key(rabbitmq); + let cm_key = M::make_server_config_map_key(rabbitmq); let cm_obj = resources[cm_key]; - let made_sts = make_stateful_set(rabbitmq, int_to_string_view(cm_obj.metadata.resource_version.get_Some_0())); + let made_sts = M::make_stateful_set(rabbitmq, int_to_string_view(cm_obj.metadata.resource_version.get_Some_0())); &&& resources.contains_key(key) &&& resources.contains_key(cm_key) &&& cm_obj.metadata.resource_version.is_Some() diff --git a/src/controller_examples/rabbitmq_controller/trusted/maker.rs b/src/controller_examples/rabbitmq_controller/trusted/maker.rs new file mode 100644 index 000000000..bd03683e3 --- /dev/null +++ b/src/controller_examples/rabbitmq_controller/trusted/maker.rs @@ -0,0 +1,36 @@ +// Copyright 2022 VMware, Inc. +// SPDX-License-Identifier: MIT +use crate::kubernetes_api_objects::error::ParseDynamicObjectError; +use crate::kubernetes_api_objects::prelude::*; +use crate::rabbitmq_controller::trusted::spec_types::RabbitmqClusterView; +use crate::vstd_ext::{string_map::*, string_view::*}; +use deps_hack::kube::Resource; +use vstd::prelude::*; + +verus! { + +pub trait Maker { + spec fn make_headless_service_key(rabbitmq: RabbitmqClusterView) -> ObjectRef; + spec fn make_main_service_key(rabbitmq: RabbitmqClusterView) -> ObjectRef; + spec fn make_erlang_secret_key(rabbitmq: RabbitmqClusterView) -> ObjectRef; + spec fn make_default_user_secret_key(rabbitmq: RabbitmqClusterView) -> ObjectRef; + spec fn make_plugins_config_map_key(rabbitmq: RabbitmqClusterView) -> ObjectRef; + spec fn make_server_config_map_key(rabbitmq: RabbitmqClusterView) -> ObjectRef; + spec fn make_service_account_key(rabbitmq: RabbitmqClusterView) -> ObjectRef; + spec fn make_role_key(rabbitmq: RabbitmqClusterView) -> ObjectRef; + spec fn make_role_binding_key(rabbitmq: RabbitmqClusterView) -> ObjectRef; + spec fn make_stateful_set_key(rabbitmq: RabbitmqClusterView) -> ObjectRef; + + spec fn make_headless_service(rabbitmq: RabbitmqClusterView) -> ServiceView; + spec fn make_main_service(rabbitmq: RabbitmqClusterView) -> ServiceView; + spec fn make_erlang_secret(rabbitmq: RabbitmqClusterView) -> SecretView; + spec fn make_default_user_secret(rabbitmq: RabbitmqClusterView) -> SecretView; + spec fn make_plugins_config_map(rabbitmq: RabbitmqClusterView) -> ConfigMapView; + spec fn make_server_config_map(rabbitmq: RabbitmqClusterView) -> ConfigMapView; + spec fn make_service_account(rabbitmq: RabbitmqClusterView) -> ServiceAccountView; + spec fn make_role(rabbitmq: RabbitmqClusterView) -> RoleView; + spec fn make_role_binding(rabbitmq: RabbitmqClusterView) -> RoleBindingView; + spec fn make_stateful_set(rabbitmq: RabbitmqClusterView, config_map_rv: StringView) -> StatefulSetView; +} + +} diff --git a/src/controller_examples/rabbitmq_controller/trusted/mod.rs b/src/controller_examples/rabbitmq_controller/trusted/mod.rs new file mode 100644 index 000000000..a94afea4a --- /dev/null +++ b/src/controller_examples/rabbitmq_controller/trusted/mod.rs @@ -0,0 +1,8 @@ +// Copyright 2022 VMware, Inc. +// SPDX-License-Identifier: MIT +pub mod exec_types; +pub mod liveness_theorem; +pub mod maker; +pub mod safety_theorem; +pub mod spec_types; +pub mod step; diff --git a/src/controller_examples/rabbitmq_controller/proof/safety_theorem.rs b/src/controller_examples/rabbitmq_controller/trusted/safety_theorem.rs similarity index 75% rename from src/controller_examples/rabbitmq_controller/proof/safety_theorem.rs rename to src/controller_examples/rabbitmq_controller/trusted/safety_theorem.rs index 9f38b6da1..23cab1939 100644 --- a/src/controller_examples/rabbitmq_controller/proof/safety_theorem.rs +++ b/src/controller_examples/rabbitmq_controller/trusted/safety_theorem.rs @@ -3,26 +3,23 @@ #![allow(unused_imports)] use crate::kubernetes_api_objects::prelude::*; use crate::kubernetes_cluster::spec::{cluster::*, cluster_state_machine::Step, message::*}; -use crate::rabbitmq_controller::{ - common::*, - spec::{reconciler::*, resource::*, types::*}, -}; -use crate::temporal_logic::{defs::*, rules::*}; +use crate::rabbitmq_controller::trusted::{maker::*, spec_types::*, step::*}; +use crate::temporal_logic::defs::*; use crate::vstd_ext::string_view::int_to_string_view; use vstd::prelude::*; verus! { -pub open spec fn safety_theorem() -> bool { - cluster_spec_without_wf().entails(tla_forall(|rabbitmq: RabbitmqClusterView| safety(rabbitmq))) +pub open spec fn safety_theorem() -> bool { + cluster_spec_without_wf().entails(tla_forall(|rabbitmq: RabbitmqClusterView| safety::(rabbitmq))) } pub open spec fn cluster_spec_without_wf() -> TempPred { lift_state(RMQCluster::init()).and(always(lift_action(RMQCluster::next()))) } -pub open spec fn safety(rabbitmq: RabbitmqClusterView) -> TempPred { - always(lift_action(stateful_set_not_scaled_down(rabbitmq))) +pub open spec fn safety(rabbitmq: RabbitmqClusterView) -> TempPred { + always(lift_action(stateful_set_not_scaled_down::(rabbitmq))) } /// To prove the safety property about stateful set, we need to first specify what the property is. @@ -32,9 +29,9 @@ pub open spec fn safety(rabbitmq: RabbitmqClusterView) -> TempPred { /// because Message is just a tool and a detail of the system. For update action, one way to circumvent using Message is /// to talk about the previous and current state: an object being updated means that it exists in both states but changes /// in current state. -pub open spec fn stateful_set_not_scaled_down(rabbitmq: RabbitmqClusterView) -> ActionPred { +pub open spec fn stateful_set_not_scaled_down(rabbitmq: RabbitmqClusterView) -> ActionPred { |s: RMQCluster, s_prime: RMQCluster| { - let sts_key = make_stateful_set_key(rabbitmq); + let sts_key = M::make_stateful_set_key(rabbitmq); s.resources().contains_key(sts_key) && s_prime.resources().contains_key(sts_key) ==> replicas_of_stateful_set(s_prime.resources()[sts_key]) >= replicas_of_stateful_set(s.resources()[sts_key]) diff --git a/src/controller_examples/rabbitmq_controller/spec/types.rs b/src/controller_examples/rabbitmq_controller/trusted/spec_types.rs similarity index 98% rename from src/controller_examples/rabbitmq_controller/spec/types.rs rename to src/controller_examples/rabbitmq_controller/trusted/spec_types.rs index c1b2b3301..11f4d607d 100644 --- a/src/controller_examples/rabbitmq_controller/spec/types.rs +++ b/src/controller_examples/rabbitmq_controller/trusted/spec_types.rs @@ -7,7 +7,7 @@ use crate::kubernetes_api_objects::{ stateful_set::*, toleration::*, }; use crate::kubernetes_cluster::spec::{cluster::*, cluster_state_machine::*, message::*}; -use crate::rabbitmq_controller::common::*; +use crate::rabbitmq_controller::trusted::step::*; use crate::vstd_ext::string_view::*; use vstd::prelude::*; @@ -185,4 +185,6 @@ pub struct RabbitmqClusterPersistenceSpecView { pub storage: StringView, } +pub closed spec fn random_encoded_string(length: usize) -> StringView; + } diff --git a/src/controller_examples/rabbitmq_controller/common/mod.rs b/src/controller_examples/rabbitmq_controller/trusted/step.rs similarity index 100% rename from src/controller_examples/rabbitmq_controller/common/mod.rs rename to src/controller_examples/rabbitmq_controller/trusted/step.rs diff --git a/src/controller_examples/zookeeper_controller/exec/reconciler.rs b/src/controller_examples/zookeeper_controller/exec/reconciler.rs index 94accd989..f02aaf85a 100644 --- a/src/controller_examples/zookeeper_controller/exec/reconciler.rs +++ b/src/controller_examples/zookeeper_controller/exec/reconciler.rs @@ -24,8 +24,11 @@ verus! { pub struct ZookeeperReconciler {} -#[verifier(external)] impl Reconciler for ZookeeperReconciler { + open spec fn well_formed(zk: &ZookeeperCluster) -> bool { + zk@.well_formed() + } + fn reconcile_init_state() -> ZookeeperReconcileState { reconcile_init_state() } diff --git a/src/rabbitmq_controller.rs b/src/rabbitmq_controller.rs index 4d8d113aa..2e0390ce5 100644 --- a/src/rabbitmq_controller.rs +++ b/src/rabbitmq_controller.rs @@ -18,7 +18,7 @@ use builtin_macros::*; use crate::external_api::exec::*; use crate::rabbitmq_controller::exec::reconciler::RabbitmqReconciler; -use crate::rabbitmq_controller::exec::types::{RabbitmqCluster, RabbitmqReconcileState}; +use crate::rabbitmq_controller::trusted::exec_types::{RabbitmqCluster, RabbitmqReconcileState}; use deps_hack::anyhow::Result; use deps_hack::kube::CustomResourceExt; use deps_hack::serde_yaml; diff --git a/src/reconciler/exec/reconciler.rs b/src/reconciler/exec/reconciler.rs index 007b5b458..a505ef9ca 100644 --- a/src/reconciler/exec/reconciler.rs +++ b/src/reconciler/exec/reconciler.rs @@ -12,8 +12,10 @@ verus! { pub trait Reconciler where ExternalAPIInput: View, ExternalAPIOutput: View, ExternalAPIType: ExternalAPIShimLayer { + spec fn well_formed(cr: &R) -> bool; fn reconcile_init_state() -> T; - fn reconcile_core(cr: &R, resp_o: Option>, state: T) -> (T, Option>); + fn reconcile_core(cr: &R, resp_o: Option>, state: T) -> (T, Option>) + requires Self::well_formed(cr); fn reconcile_done(state: &T) -> bool; fn reconcile_error(state: &T) -> bool; }