Rename cluster_state_machine.rs to cluster.rs (#543)

Signed-off-by: Xudong Sun <[email protected]>
anvil-verifier · Sep 28, 2024 · 9f6a0ff · 9f6a0ff
1 parent bec4f3c
commit 9f6a0ff
Show file tree

Hide file tree

Showing 21 changed files with 22 additions and 24 deletions.
diff --git a/src/v2/controllers/vreplicaset_controller/install.rs b/src/v2/controllers/vreplicaset_controller/install.rs
@@ -4,7 +4,7 @@ use crate::external_api::spec::EmptyTypeView;
 use crate::kubernetes_api_objects::{error::*, spec::prelude::*};
 use crate::kubernetes_cluster::spec::{
     api_server::types::InstalledType,
-    cluster_state_machine::ControllerModel,
+    cluster::ControllerModel,
     controller::types::{ReconcileModel, RequestContent, ResponseContent},
     install_helpers::*,
 };

diff --git a/src/v2/controllers/vreplicaset_controller/trusted/liveness_theorem.rs b/src/v2/controllers/vreplicaset_controller/trusted/liveness_theorem.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: MIT
 #![allow(unused_imports)]
 use crate::kubernetes_api_objects::spec::prelude::*;
-use crate::kubernetes_cluster::spec::{cluster_state_machine::*, message::*};
+use crate::kubernetes_cluster::spec::{cluster::*, message::*};
 use crate::temporal_logic::defs::*;
 use crate::vreplicaset_controller::trusted::{spec_types::*, step::*};
 use crate::vstd_ext::string_view::int_to_string_view;

diff --git a/src/v2/controllers/vreplicaset_controller/trusted/spec_types.rs b/src/v2/controllers/vreplicaset_controller/trusted/spec_types.rs
@@ -5,7 +5,7 @@ use crate::kubernetes_api_objects::error::*;
 use crate::kubernetes_api_objects::spec::{
     api_resource::*, label_selector::*, pod_template_spec::*, prelude::*,
 };
-use crate::kubernetes_cluster::spec::{cluster_state_machine::*, message::*};
+use crate::kubernetes_cluster::spec::{cluster::*, message::*};
 use crate::vreplicaset_controller::trusted::step::*;
 use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;

diff --git a/src/v2/kubernetes_cluster/proof/cluster.rs b/src/v2/kubernetes_cluster/proof/cluster.rs
@@ -3,7 +3,7 @@
 #![allow(unused_imports)]
 use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::temporal_logic::{defs::*, rules::*};
-use crate::kubernetes_cluster::spec::{cluster_state_machine::*, message::*};
+use crate::kubernetes_cluster::spec::{cluster::*, message::*};
 use vstd::prelude::*;
 
 verus! {

diff --git a/src/v2/kubernetes_cluster/proof/compositionality.rs b/src/v2/kubernetes_cluster/proof/compositionality.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: MIT
 #![allow(unused_imports)]
 use crate::kubernetes_cluster::spec::{
-    cluster_state_machine::*, controller::state_machine::controller,
+    cluster::*, controller::state_machine::controller,
 };
 use crate::temporal_logic::defs::*;
 use vstd::prelude::*;

diff --git a/src/v2/kubernetes_cluster/proof/controller_runtime_liveness.rs b/src/v2/kubernetes_cluster/proof/controller_runtime_liveness.rs
@@ -5,7 +5,7 @@ use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::temporal_logic::{defs::*, rules::*};
 use crate::kubernetes_cluster::spec::{
     api_server::{state_machine::transition_by_etcd, types::*},
-    cluster_state_machine::*,
+    cluster::*,
     controller::types::*,
     external::{state_machine::*, types::*},
     message::*,

diff --git a/src/v2/kubernetes_cluster/proof/controller_runtime_safety.rs b/src/v2/kubernetes_cluster/proof/controller_runtime_safety.rs
@@ -5,7 +5,7 @@ use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::temporal_logic::{defs::*, rules::*};
 use crate::kubernetes_cluster::spec::{
     api_server::{state_machine::transition_by_etcd, types::*},
-    cluster_state_machine::*,
+    cluster::*,
     controller::types::*,
     external::{state_machine::*, types::*},
     message::*,

diff --git a/src/v2/kubernetes_cluster/proof/failures_liveness.rs b/src/v2/kubernetes_cluster/proof/failures_liveness.rs
@@ -3,7 +3,7 @@
 #![allow(unused_imports)]
 use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::temporal_logic::{defs::*, rules::*};
-use crate::kubernetes_cluster::spec::{cluster_state_machine::*, message::*};
+use crate::kubernetes_cluster::spec::{cluster::*, message::*};
 use vstd::prelude::*;
 
 verus! {

diff --git a/src/v2/kubernetes_cluster/proof/garbage_collector.rs b/src/v2/kubernetes_cluster/proof/garbage_collector.rs
@@ -5,7 +5,7 @@ use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::temporal_logic::{defs::*, rules::*};
 use crate::kubernetes_cluster::spec::{
     api_server::types::*, builtin_controllers::garbage_collector::run_garbage_collector,
-    builtin_controllers::types::*, cluster_state_machine::*, message::*,
+    builtin_controllers::types::*, cluster::*, message::*,
 };
 use crate::vstd_ext::string_view::StringView;
 use vstd::prelude::*;

diff --git a/src/v2/kubernetes_cluster/proof/network.rs b/src/v2/kubernetes_cluster/proof/network.rs
@@ -4,7 +4,7 @@
 use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::temporal_logic::{defs::*, rules::*};
 use crate::kubernetes_cluster::spec::{
-    api_server::state_machine::transition_by_etcd, cluster_state_machine::*, message::*,
+    api_server::state_machine::transition_by_etcd, cluster::*, message::*,
 };
 use vstd::prelude::*;
 

diff --git a/src/v2/kubernetes_cluster/proof/network_liveness.rs b/src/v2/kubernetes_cluster/proof/network_liveness.rs
@@ -4,7 +4,7 @@
 use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::temporal_logic::{defs::*, rules::*};
 use crate::kubernetes_cluster::spec::{
-    api_server::types::*, cluster_state_machine::*, message::*,
+    api_server::types::*, cluster::*, message::*,
 };
 use crate::vstd_ext::multiset_lib::*;
 use vstd::assert_multisets_equal;

diff --git a/src/v2/kubernetes_cluster/proof/objects_in_reconcile.rs b/src/v2/kubernetes_cluster/proof/objects_in_reconcile.rs
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: MIT
 #![allow(unused_imports)]
 use crate::kubernetes_api_objects::spec::prelude::*;
+use crate::kubernetes_cluster::spec::{cluster::*, message::*};
 use crate::temporal_logic::{defs::*, rules::*};
-use crate::kubernetes_cluster::spec::{cluster_state_machine::*, message::*};
 use crate::vstd_ext::string_view::StringView;
 use vstd::prelude::*;
 

diff --git a/src/v2/kubernetes_cluster/proof/objects_in_store.rs b/src/v2/kubernetes_cluster/proof/objects_in_store.rs
@@ -2,13 +2,13 @@
 // SPDX-License-Identifier: MIT
 #![allow(unused_imports)]
 use crate::kubernetes_api_objects::spec::prelude::*;
-use crate::temporal_logic::{defs::*, rules::*};
 use crate::kubernetes_cluster::spec::{
     api_server::state_machine::{deletion_timestamp, unmarshallable_object, valid_object},
-    cluster_state_machine::*,
+    cluster::*,
     install_helpers::*,
     message::*,
 };
+use crate::temporal_logic::{defs::*, rules::*};
 use crate::vstd_ext::string_view::StringView;
 use vstd::prelude::*;
 

diff --git a/src/v2/kubernetes_cluster/proof/req_resp.rs b/src/v2/kubernetes_cluster/proof/req_resp.rs
@@ -2,14 +2,14 @@
 // SPDX-License-Identifier: MIT
 #![allow(unused_imports)]
 use crate::kubernetes_api_objects::spec::prelude::*;
-use crate::temporal_logic::{defs::*, rules::*};
 use crate::kubernetes_cluster::spec::{
     api_server::state_machine::{
         handle_create_request_msg, handle_get_request_msg, handle_update_request_msg,
     },
-    cluster_state_machine::*,
+    cluster::*,
     message::*,
 };
+use crate::temporal_logic::{defs::*, rules::*};
 use vstd::prelude::*;
 
 verus! {

diff --git a/src/v2/kubernetes_cluster/proof/retentive_cluster.rs b/src/v2/kubernetes_cluster/proof/retentive_cluster.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: MIT
 #![allow(unused_imports)]
 use crate::kubernetes_api_objects::spec::prelude::*;
-use crate::kubernetes_cluster::spec::{cluster_state_machine::*, retentive_cluster::*};
+use crate::kubernetes_cluster::spec::{cluster::*, retentive_cluster::*};
 use crate::temporal_logic::{defs::*, rules::*};
 use vstd::prelude::*;
 

diff --git a/src/v2/kubernetes_cluster/proof/stability.rs b/src/v2/kubernetes_cluster/proof/stability.rs
@@ -3,7 +3,7 @@
 #![allow(unused_imports)]
 use crate::state_machine::{action::*, state_machine::*};
 use crate::temporal_logic::{defs::*, rules::*};
-use crate::kubernetes_cluster::spec::cluster_state_machine::*;
+use crate::kubernetes_cluster::spec::cluster::*;
 use vstd::prelude::*;
 
 verus! {

diff --git a/src/v2/kubernetes_cluster/proof/transition_validation.rs b/src/v2/kubernetes_cluster/proof/transition_validation.rs
@@ -5,7 +5,7 @@ use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::temporal_logic::{defs::*, rules::*};
 use crate::kubernetes_cluster::spec::{
     api_server::state_machine::{deletion_timestamp, unmarshallable_object, valid_object},
-    cluster_state_machine::*,
+    cluster::*,
     message::*,
 };
 use crate::vstd_ext::string_view::StringView;

diff --git a/src/v2/kubernetes_cluster/proof/wf1_helpers.rs b/src/v2/kubernetes_cluster/proof/wf1_helpers.rs
@@ -9,7 +9,7 @@ use crate::kubernetes_cluster::spec::{
     api_server::types::*,
     builtin_controllers::state_machine::builtin_controllers,
     builtin_controllers::types::*,
-    cluster_state_machine::*,
+    cluster::*,
     controller::state_machine::{controller, init_controller_state},
     controller::types::*,
     external::state_machine::external,

diff --git a/...tes_cluster/spec/cluster_state_machine.rs → src/v2/kubernetes_cluster/spec/cluster.rs b/...tes_cluster/spec/cluster_state_machine.rs → src/v2/kubernetes_cluster/spec/cluster.rs
diff --git a/src/v2/kubernetes_cluster/spec/mod.rs b/src/v2/kubernetes_cluster/spec/mod.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: MIT
 pub mod api_server;
 pub mod builtin_controllers;
-pub mod cluster_state_machine;
+pub mod cluster;
 pub mod controller;
 pub mod external;
 pub mod install_helpers;

diff --git a/src/v2/kubernetes_cluster/spec/retentive_cluster.rs b/src/v2/kubernetes_cluster/spec/retentive_cluster.rs
@@ -3,9 +3,7 @@
 #![allow(unused_imports)]
 use crate::kubernetes_api_objects::error::*;
 use crate::kubernetes_api_objects::spec::prelude::*;
-use crate::kubernetes_cluster::spec::{
-    api_server::types::InstalledTypes, cluster_state_machine::*,
-};
+use crate::kubernetes_cluster::spec::{api_server::types::InstalledTypes, cluster::*};
 use crate::state_machine::{action::*, state_machine::*};
 use crate::temporal_logic::defs::*;
 use vstd::{multiset::*, prelude::*};