From f50326c8727111e13d6e776746cace719c7a1c54 Mon Sep 17 00:00:00 2001
From: Xudong Sun <xudongs3@illinois.edu>
Date: Mon, 7 Oct 2024 12:20:52 -0500
Subject: [PATCH] Clean up imports

Signed-off-by: Xudong Sun <xudongs3@illinois.edu>
---
 src/kubernetes_api_objects/error.rs                |  1 -
 src/kubernetes_api_objects/exec/affinity.rs        |  6 +-----
 src/kubernetes_api_objects/exec/api_method.rs      |  9 +++------
 src/kubernetes_api_objects/exec/api_resource.rs    |  2 +-
 src/kubernetes_api_objects/exec/common.rs          |  2 --
 src/kubernetes_api_objects/exec/config_map.rs      |  2 +-
 src/kubernetes_api_objects/exec/container.rs       |  9 +++------
 src/kubernetes_api_objects/exec/daemon_set.rs      |  3 +--
 src/kubernetes_api_objects/exec/dynamic.rs         |  6 ++----
 src/kubernetes_api_objects/exec/label_selector.rs  |  5 ++---
 src/kubernetes_api_objects/exec/object_meta.rs     |  3 +--
 src/kubernetes_api_objects/exec/owner_reference.rs |  4 +---
 .../exec/persistent_volume_claim.rs                |  2 --
 src/kubernetes_api_objects/exec/pod.rs             |  6 ++----
 .../exec/pod_template_spec.rs                      |  8 +-------
 src/kubernetes_api_objects/exec/preconditions.rs   |  3 +--
 .../exec/resource_requirements.rs                  |  4 +---
 src/kubernetes_api_objects/exec/role.rs            |  3 +--
 src/kubernetes_api_objects/exec/role_binding.rs    |  4 ----
 src/kubernetes_api_objects/exec/secret.rs          |  1 -
 src/kubernetes_api_objects/exec/service.rs         |  2 --
 src/kubernetes_api_objects/exec/service_account.rs |  2 --
 src/kubernetes_api_objects/exec/stateful_set.rs    |  4 ----
 src/kubernetes_api_objects/exec/toleration.rs      |  7 +------
 src/kubernetes_api_objects/exec/volume.rs          |  7 +------
 .../exec/volume_resource_requirements.rs           |  4 +---
 src/kubernetes_api_objects/spec/api_method.rs      |  3 +--
 src/kubernetes_api_objects/spec/common.rs          |  1 -
 src/kubernetes_api_objects/spec/config_map.rs      |  2 +-
 src/kubernetes_api_objects/spec/container.rs       |  6 ++----
 src/kubernetes_api_objects/spec/daemon_set.rs      |  4 ----
 src/kubernetes_api_objects/spec/dynamic.rs         |  4 +---
 src/kubernetes_api_objects/spec/label_selector.rs  |  4 ----
 src/kubernetes_api_objects/spec/object_meta.rs     |  5 +----
 src/kubernetes_api_objects/spec/owner_reference.rs |  5 +----
 .../spec/persistent_volume_claim.rs                |  1 -
 src/kubernetes_api_objects/spec/pod.rs             |  8 +++-----
 .../spec/pod_template_spec.rs                      |  8 +-------
 .../spec/resource_requirements.rs                  |  2 --
 src/kubernetes_api_objects/spec/role.rs            |  2 --
 src/kubernetes_api_objects/spec/role_binding.rs    |  3 ---
 src/kubernetes_api_objects/spec/secret.rs          |  1 -
 src/kubernetes_api_objects/spec/service.rs         |  2 --
 src/kubernetes_api_objects/spec/service_account.rs |  2 --
 src/kubernetes_api_objects/spec/stateful_set.rs    |  3 ---
 src/kubernetes_api_objects/spec/toleration.rs      |  4 ----
 src/kubernetes_api_objects/spec/volume.rs          |  4 ----
 .../spec/volume_resource_requirements.rs           |  2 --
 .../vreplicaset_controller/exec/reconciler.rs      |  4 ++--
 .../vreplicaset_controller/model/reconciler.rs     |  2 +-
 .../vreplicaset_controller/trusted/exec_types.rs   |  3 +--
 .../trusted/liveness_theorem.rs                    |  3 +--
 .../vreplicaset_controller/trusted/spec_types.rs   |  7 +------
 src/v2/kubernetes_cluster/proof/cluster.rs         |  3 +--
 .../proof/controller_runtime_safety.rs             |  7 ++-----
 .../kubernetes_cluster/proof/failures_liveness.rs  |  3 +--
 .../kubernetes_cluster/proof/network_liveness.rs   |  7 +------
 .../proof/objects_in_reconcile.rs                  |  3 +--
 .../kubernetes_cluster/proof/objects_in_store.rs   |  5 +----
 .../kubernetes_cluster/proof/retentive_cluster.rs  |  3 +--
 src/v2/kubernetes_cluster/proof/stability.rs       |  4 ++--
 .../proof/transition_validation.rs                 |  7 +------
 src/v2/kubernetes_cluster/proof/wf1_helpers.rs     |  8 ++------
 .../spec/api_server/state_machine.rs               |  1 -
 src/v2/kubernetes_cluster/spec/api_server/types.rs |  1 -
 .../spec/builtin_controllers/garbage_collector.rs  |  5 +----
 .../spec/builtin_controllers/state_machine.rs      | 10 ++--------
 .../spec/builtin_controllers/types.rs              |  2 +-
 src/v2/kubernetes_cluster/spec/cluster.rs          |  2 +-
 .../spec/controller/state_machine.rs               |  1 -
 src/v2/kubernetes_cluster/spec/external/types.rs   |  2 --
 .../spec/network/state_machine.rs                  |  1 -
 src/v2/kubernetes_cluster/spec/network/types.rs    |  3 ---
 .../spec/pod_monkey/state_machine.rs               |  1 -
 src/v2/kubernetes_cluster/spec/pod_monkey/types.rs |  4 ++--
 .../kubernetes_cluster/spec/retentive_cluster.rs   |  5 +----
 src/v2/reconciler/exec/io.rs                       |  2 +-
 src/v2/reconciler/exec/reconciler.rs               |  2 +-
 src/v2/reconciler/exec/resource_builder.rs         |  6 +-----
 src/v2/reconciler/spec/io.rs                       |  3 +--
 src/v2/reconciler/spec/reconciler.rs               |  5 ++---
 src/v2/reconciler/spec/resource_builder.rs         |  4 ----
 src/v2/shim_layer/controller_runtime.rs            | 14 ++++++--------
 src/v2/shim_layer/fault_injection.rs               |  7 +------
 src/vstd_ext/string_map.rs                         |  1 -
 src/vstd_ext/string_view.rs                        |  1 -
 86 files changed, 76 insertions(+), 261 deletions(-)

diff --git a/src/kubernetes_api_objects/error.rs b/src/kubernetes_api_objects/error.rs
index 3d952925c..3d5eb71d7 100644
--- a/src/kubernetes_api_objects/error.rs
+++ b/src/kubernetes_api_objects/error.rs
@@ -1,6 +1,5 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use deps_hack::kube;
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/kubernetes_api_objects/exec/affinity.rs b/src/kubernetes_api_objects/exec/affinity.rs
index f8406c49e..5eed3259e 100644
--- a/src/kubernetes_api_objects/exec/affinity.rs
+++ b/src/kubernetes_api_objects/exec/affinity.rs
@@ -1,11 +1,7 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::error::UnmarshalError;
-use crate::kubernetes_api_objects::exec::{
-    api_resource::*, dynamic::*, object_meta::*, resource::*,
-};
+use crate::kubernetes_api_objects::exec::resource::*;
 use crate::kubernetes_api_objects::spec::affinity::*;
-use crate::vstd_ext::{string_map::*, string_view::*};
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/kubernetes_api_objects/exec/api_method.rs b/src/kubernetes_api_objects/exec/api_method.rs
index d440a47f7..e5d1e0a77 100644
--- a/src/kubernetes_api_objects/exec/api_method.rs
+++ b/src/kubernetes_api_objects/exec/api_method.rs
@@ -2,12 +2,9 @@
 // SPDX-License-Identifier: MIT
 use crate::kubernetes_api_objects::error::*;
 use crate::kubernetes_api_objects::exec::{api_resource::*, dynamic::*, preconditions::*};
-use crate::kubernetes_api_objects::spec::{
-    api_method::*,
-    common::{Kind, ObjectRef},
-};
-use crate::vstd_ext::{option_lib::*, string_view::*};
-use vstd::{prelude::*, string::*, view::*};
+use crate::kubernetes_api_objects::spec::{api_method::*, common::ObjectRef};
+use crate::vstd_ext::option_lib::*;
+use vstd::prelude::*;
 
 use vstd::pervasive::unreached;
 
diff --git a/src/kubernetes_api_objects/exec/api_resource.rs b/src/kubernetes_api_objects/exec/api_resource.rs
index 7d4cda3c4..13e2ba071 100644
--- a/src/kubernetes_api_objects/exec/api_resource.rs
+++ b/src/kubernetes_api_objects/exec/api_resource.rs
@@ -1,6 +1,6 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::exec::{object_meta::*, resource::*};
+use crate::kubernetes_api_objects::exec::resource::*;
 use crate::kubernetes_api_objects::spec::api_resource::*;
 use vstd::prelude::*;
 
diff --git a/src/kubernetes_api_objects/exec/common.rs b/src/kubernetes_api_objects/exec/common.rs
index 267701940..8d0c62cd3 100644
--- a/src/kubernetes_api_objects/exec/common.rs
+++ b/src/kubernetes_api_objects/exec/common.rs
@@ -1,9 +1,7 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
 use crate::kubernetes_api_objects::spec::common::*;
-use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
-use vstd::string::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/exec/config_map.rs b/src/kubernetes_api_objects/exec/config_map.rs
index 7cfdcd04f..fdc549d92 100644
--- a/src/kubernetes_api_objects/exec/config_map.rs
+++ b/src/kubernetes_api_objects/exec/config_map.rs
@@ -5,7 +5,7 @@ use crate::kubernetes_api_objects::exec::{
     api_resource::*, dynamic::*, object_meta::*, resource::*,
 };
 use crate::kubernetes_api_objects::spec::{config_map::*, resource::*};
-use crate::vstd_ext::{string_map::*, string_view::*};
+use crate::vstd_ext::string_map::*;
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/kubernetes_api_objects/exec/container.rs b/src/kubernetes_api_objects/exec/container.rs
index 91904edfb..efbb834d2 100644
--- a/src/kubernetes_api_objects/exec/container.rs
+++ b/src/kubernetes_api_objects/exec/container.rs
@@ -1,12 +1,9 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::error::UnmarshalError;
-use crate::kubernetes_api_objects::exec::{
-    api_resource::*, dynamic::*, resource::*, resource_requirements::*, volume::*,
-};
-use crate::kubernetes_api_objects::spec::{container::*, resource::*};
+use crate::kubernetes_api_objects::exec::{resource_requirements::*, volume::*};
+use crate::kubernetes_api_objects::spec::container::*;
 use crate::vstd_ext::string_view::*;
-use vstd::{prelude::*, seq_lib::*, string::*};
+use vstd::prelude::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/exec/daemon_set.rs b/src/kubernetes_api_objects/exec/daemon_set.rs
index 74bca3a58..ce9a06ba6 100644
--- a/src/kubernetes_api_objects/exec/daemon_set.rs
+++ b/src/kubernetes_api_objects/exec/daemon_set.rs
@@ -6,8 +6,7 @@ use crate::kubernetes_api_objects::exec::{
     resource::*,
 };
 use crate::kubernetes_api_objects::spec::{daemon_set::*, resource::*};
-use crate::vstd_ext::{string_map::*, string_view::*};
-use vstd::{prelude::*, seq_lib::*, string::*};
+use vstd::prelude::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/exec/dynamic.rs b/src/kubernetes_api_objects/exec/dynamic.rs
index e8af445e3..490cd38a7 100644
--- a/src/kubernetes_api_objects/exec/dynamic.rs
+++ b/src/kubernetes_api_objects/exec/dynamic.rs
@@ -1,9 +1,7 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::error::UnmarshalError;
-use crate::kubernetes_api_objects::exec::{object_meta::*, owner_reference::*, resource::*};
-use crate::kubernetes_api_objects::spec::{common::*, dynamic::*};
-use crate::vstd_ext::string_view::*;
+use crate::kubernetes_api_objects::exec::{object_meta::*, resource::*};
+use crate::kubernetes_api_objects::spec::dynamic::*;
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/kubernetes_api_objects/exec/label_selector.rs b/src/kubernetes_api_objects/exec/label_selector.rs
index bdefedca1..41f8c7921 100644
--- a/src/kubernetes_api_objects/exec/label_selector.rs
+++ b/src/kubernetes_api_objects/exec/label_selector.rs
@@ -1,10 +1,9 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::error::UnmarshalError;
 use crate::kubernetes_api_objects::exec::resource::*;
 use crate::kubernetes_api_objects::spec::label_selector::*;
-use crate::vstd_ext::{string_map::*, string_view::*};
-use vstd::{prelude::*, string::*};
+use crate::vstd_ext::string_map::*;
+use vstd::prelude::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/exec/object_meta.rs b/src/kubernetes_api_objects/exec/object_meta.rs
index 2fea18e83..517283fab 100644
--- a/src/kubernetes_api_objects/exec/object_meta.rs
+++ b/src/kubernetes_api_objects/exec/object_meta.rs
@@ -1,10 +1,9 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::error::UnmarshalError;
 use crate::kubernetes_api_objects::exec::{owner_reference::*, resource::*};
 use crate::kubernetes_api_objects::spec::object_meta::*;
 use crate::vstd_ext::{string_map::*, string_view::*};
-use vstd::{prelude::*, string::*};
+use vstd::prelude::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/exec/owner_reference.rs b/src/kubernetes_api_objects/exec/owner_reference.rs
index b1eaeec14..300642178 100644
--- a/src/kubernetes_api_objects/exec/owner_reference.rs
+++ b/src/kubernetes_api_objects/exec/owner_reference.rs
@@ -1,10 +1,8 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::error::UnmarshalError;
 use crate::kubernetes_api_objects::exec::resource::*;
 use crate::kubernetes_api_objects::spec::owner_reference::*;
-use crate::vstd_ext::{string_map::*, string_view::*};
-use vstd::{prelude::*, string::*};
+use vstd::prelude::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/exec/persistent_volume_claim.rs b/src/kubernetes_api_objects/exec/persistent_volume_claim.rs
index 761b437cb..5684e86c9 100644
--- a/src/kubernetes_api_objects/exec/persistent_volume_claim.rs
+++ b/src/kubernetes_api_objects/exec/persistent_volume_claim.rs
@@ -5,9 +5,7 @@ use crate::kubernetes_api_objects::exec::{
     api_resource::*, dynamic::*, object_meta::*, resource::*, volume_resource_requirements::*,
 };
 use crate::kubernetes_api_objects::spec::{persistent_volume_claim::*, resource::*};
-use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
-use vstd::seq_lib::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/exec/pod.rs b/src/kubernetes_api_objects/exec/pod.rs
index dadcaad2a..b88278b8c 100644
--- a/src/kubernetes_api_objects/exec/pod.rs
+++ b/src/kubernetes_api_objects/exec/pod.rs
@@ -3,13 +3,11 @@
 use crate::kubernetes_api_objects::error::UnmarshalError;
 use crate::kubernetes_api_objects::exec::{
     affinity::*, api_resource::*, container::*, dynamic::*, object_meta::*, resource::*,
-    resource_requirements::*, toleration::*, volume::*,
+    toleration::*, volume::*,
 };
 use crate::kubernetes_api_objects::spec::{pod::*, resource::*};
-use crate::vstd_ext::{string_map::*, string_view::*};
+use crate::vstd_ext::string_map::*;
 use vstd::prelude::*;
-use vstd::seq_lib::*;
-use vstd::string::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/exec/pod_template_spec.rs b/src/kubernetes_api_objects/exec/pod_template_spec.rs
index a4495b2bb..886b79635 100644
--- a/src/kubernetes_api_objects/exec/pod_template_spec.rs
+++ b/src/kubernetes_api_objects/exec/pod_template_spec.rs
@@ -1,14 +1,8 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::error::UnmarshalError;
-use crate::kubernetes_api_objects::exec::{
-    api_resource::*, dynamic::*, object_meta::*, pod::*, resource::*,
-};
+use crate::kubernetes_api_objects::exec::{object_meta::*, pod::*, resource::*};
 use crate::kubernetes_api_objects::spec::pod_template_spec::*;
-use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
-use vstd::seq_lib::*;
-use vstd::string::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/exec/preconditions.rs b/src/kubernetes_api_objects/exec/preconditions.rs
index 5355c5d9d..591eddd3a 100644
--- a/src/kubernetes_api_objects/exec/preconditions.rs
+++ b/src/kubernetes_api_objects/exec/preconditions.rs
@@ -2,8 +2,7 @@
 // SPDX-License-Identifier: MIT
 use crate::kubernetes_api_objects::exec::{object_meta::*, resource::*};
 use crate::kubernetes_api_objects::spec::preconditions::*;
-use crate::vstd_ext::string_view::*;
-use vstd::{prelude::*, string::*, view::*};
+use vstd::prelude::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/exec/resource_requirements.rs b/src/kubernetes_api_objects/exec/resource_requirements.rs
index bbd1833cb..067c3e3dc 100644
--- a/src/kubernetes_api_objects/exec/resource_requirements.rs
+++ b/src/kubernetes_api_objects/exec/resource_requirements.rs
@@ -1,9 +1,7 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::exec::resource::*;
-use crate::kubernetes_api_objects::spec::{resource::*, resource_requirements::*};
+use crate::kubernetes_api_objects::spec::resource_requirements::*;
 use crate::vstd_ext::string_map::*;
-use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/kubernetes_api_objects/exec/role.rs b/src/kubernetes_api_objects/exec/role.rs
index 584e5495c..4a1df5c8e 100644
--- a/src/kubernetes_api_objects/exec/role.rs
+++ b/src/kubernetes_api_objects/exec/role.rs
@@ -5,8 +5,7 @@ use crate::kubernetes_api_objects::exec::{
     api_resource::*, dynamic::*, object_meta::*, resource::*,
 };
 use crate::kubernetes_api_objects::spec::{resource::*, role::*};
-use crate::vstd_ext::{string_map::StringMap, string_view::StringView};
-use vstd::{prelude::*, seq_lib::*};
+use vstd::prelude::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/exec/role_binding.rs b/src/kubernetes_api_objects/exec/role_binding.rs
index b8716af00..811e7f579 100644
--- a/src/kubernetes_api_objects/exec/role_binding.rs
+++ b/src/kubernetes_api_objects/exec/role_binding.rs
@@ -5,11 +5,7 @@ use crate::kubernetes_api_objects::exec::{
     api_resource::*, dynamic::*, object_meta::*, resource::*,
 };
 use crate::kubernetes_api_objects::spec::{resource::*, role_binding::*};
-use crate::vstd_ext::string_map::StringMap;
-use crate::vstd_ext::string_view::StringView;
 use vstd::prelude::*;
-use vstd::seq_lib::*;
-use vstd::string::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/exec/secret.rs b/src/kubernetes_api_objects/exec/secret.rs
index 86579c29b..d273ef90d 100644
--- a/src/kubernetes_api_objects/exec/secret.rs
+++ b/src/kubernetes_api_objects/exec/secret.rs
@@ -6,7 +6,6 @@ use crate::kubernetes_api_objects::exec::{
 };
 use crate::kubernetes_api_objects::spec::{resource::*, secret::*};
 use crate::vstd_ext::string_map::*;
-use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/kubernetes_api_objects/exec/service.rs b/src/kubernetes_api_objects/exec/service.rs
index 53b7ed4d0..292ca7768 100644
--- a/src/kubernetes_api_objects/exec/service.rs
+++ b/src/kubernetes_api_objects/exec/service.rs
@@ -6,9 +6,7 @@ use crate::kubernetes_api_objects::exec::{
 };
 use crate::kubernetes_api_objects::spec::{resource::*, service::*};
 use crate::vstd_ext::string_map::StringMap;
-use crate::vstd_ext::string_view::StringView;
 use vstd::prelude::*;
-use vstd::seq_lib::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/exec/service_account.rs b/src/kubernetes_api_objects/exec/service_account.rs
index 40725704d..b02c2b04b 100644
--- a/src/kubernetes_api_objects/exec/service_account.rs
+++ b/src/kubernetes_api_objects/exec/service_account.rs
@@ -5,8 +5,6 @@ use crate::kubernetes_api_objects::exec::{
     api_resource::*, dynamic::*, object_meta::*, resource::*,
 };
 use crate::kubernetes_api_objects::spec::{resource::*, service_account::*};
-use crate::vstd_ext::string_map::*;
-use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/kubernetes_api_objects/exec/stateful_set.rs b/src/kubernetes_api_objects/exec/stateful_set.rs
index 4c791943f..0937716f0 100644
--- a/src/kubernetes_api_objects/exec/stateful_set.rs
+++ b/src/kubernetes_api_objects/exec/stateful_set.rs
@@ -6,11 +6,7 @@ use crate::kubernetes_api_objects::exec::{
     pod_template_spec::*, resource::*,
 };
 use crate::kubernetes_api_objects::spec::{resource::*, stateful_set::*};
-use crate::vstd_ext::string_map::*;
-use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
-use vstd::seq_lib::*;
-use vstd::string::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/exec/toleration.rs b/src/kubernetes_api_objects/exec/toleration.rs
index 8d0ff2ff4..ed1598a06 100644
--- a/src/kubernetes_api_objects/exec/toleration.rs
+++ b/src/kubernetes_api_objects/exec/toleration.rs
@@ -1,12 +1,7 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::error::UnmarshalError;
-use crate::kubernetes_api_objects::exec::{
-    api_resource::*, dynamic::*, object_meta::*, resource::*,
-};
+use crate::kubernetes_api_objects::exec::resource::*;
 use crate::kubernetes_api_objects::spec::toleration::*;
-use crate::vstd_ext::string_map::*;
-use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/kubernetes_api_objects/exec/volume.rs b/src/kubernetes_api_objects/exec/volume.rs
index 33cc2cf51..eca9bee12 100644
--- a/src/kubernetes_api_objects/exec/volume.rs
+++ b/src/kubernetes_api_objects/exec/volume.rs
@@ -1,12 +1,7 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::error::UnmarshalError;
-use crate::kubernetes_api_objects::exec::{
-    api_resource::*, dynamic::*, object_meta::*, resource::*,
-};
 use crate::kubernetes_api_objects::spec::volume::*;
-use crate::vstd_ext::string_view::*;
-use vstd::{prelude::*, seq_lib::*, string::*};
+use vstd::prelude::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/exec/volume_resource_requirements.rs b/src/kubernetes_api_objects/exec/volume_resource_requirements.rs
index 1948243c9..30838f9b6 100644
--- a/src/kubernetes_api_objects/exec/volume_resource_requirements.rs
+++ b/src/kubernetes_api_objects/exec/volume_resource_requirements.rs
@@ -1,9 +1,7 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::exec::resource::*;
-use crate::kubernetes_api_objects::spec::{resource::*, volume_resource_requirements::*};
+use crate::kubernetes_api_objects::spec::volume_resource_requirements::*;
 use crate::vstd_ext::string_map::*;
-use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/kubernetes_api_objects/spec/api_method.rs b/src/kubernetes_api_objects/spec/api_method.rs
index 1b9bc9f2c..143553196 100644
--- a/src/kubernetes_api_objects/spec/api_method.rs
+++ b/src/kubernetes_api_objects/spec/api_method.rs
@@ -7,8 +7,7 @@ use crate::kubernetes_api_objects::spec::{
     preconditions::*,
 };
 use crate::vstd_ext::string_view::*;
-use vstd::string::*;
-use vstd::{prelude::*, view::*};
+use vstd::prelude::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/spec/common.rs b/src/kubernetes_api_objects/spec/common.rs
index 614a73e79..1dfaeb641 100644
--- a/src/kubernetes_api_objects/spec/common.rs
+++ b/src/kubernetes_api_objects/spec/common.rs
@@ -2,7 +2,6 @@
 // SPDX-License-Identifier: MIT
 use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
-use vstd::string::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/spec/config_map.rs b/src/kubernetes_api_objects/spec/config_map.rs
index fa0127c03..baf42b985 100644
--- a/src/kubernetes_api_objects/spec/config_map.rs
+++ b/src/kubernetes_api_objects/spec/config_map.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: MIT
 use crate::kubernetes_api_objects::error::*;
 use crate::kubernetes_api_objects::spec::{common::*, dynamic::*, object_meta::*, resource::*};
-use crate::vstd_ext::{string_map::*, string_view::*};
+use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/kubernetes_api_objects/spec/container.rs b/src/kubernetes_api_objects/spec/container.rs
index cfcd8135f..d250161b8 100644
--- a/src/kubernetes_api_objects/spec/container.rs
+++ b/src/kubernetes_api_objects/spec/container.rs
@@ -1,10 +1,8 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::spec::{
-    common::*, dynamic::*, resource::*, resource_requirements::*, volume::*,
-};
+use crate::kubernetes_api_objects::spec::{resource_requirements::*, volume::*};
 use crate::vstd_ext::string_view::*;
-use vstd::{prelude::*, string::*};
+use vstd::prelude::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/spec/daemon_set.rs b/src/kubernetes_api_objects/spec/daemon_set.rs
index 55f5f6e54..b057ded7b 100644
--- a/src/kubernetes_api_objects/spec/daemon_set.rs
+++ b/src/kubernetes_api_objects/spec/daemon_set.rs
@@ -4,11 +4,7 @@ use crate::kubernetes_api_objects::error::*;
 use crate::kubernetes_api_objects::spec::{
     common::*, dynamic::*, label_selector::*, object_meta::*, pod_template_spec::*, resource::*,
 };
-use crate::vstd_ext::string_map::*;
-use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
-use vstd::seq_lib::*;
-use vstd::string::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/spec/dynamic.rs b/src/kubernetes_api_objects/spec/dynamic.rs
index 24d3f87fd..22e2b6f03 100644
--- a/src/kubernetes_api_objects/spec/dynamic.rs
+++ b/src/kubernetes_api_objects/spec/dynamic.rs
@@ -1,8 +1,6 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::spec::{
-    common::*, object_meta::*, owner_reference::*, resource::*,
-};
+use crate::kubernetes_api_objects::spec::{common::*, object_meta::*, resource::*};
 use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
 
diff --git a/src/kubernetes_api_objects/spec/label_selector.rs b/src/kubernetes_api_objects/spec/label_selector.rs
index 55ce8c7de..945dc8c41 100644
--- a/src/kubernetes_api_objects/spec/label_selector.rs
+++ b/src/kubernetes_api_objects/spec/label_selector.rs
@@ -1,11 +1,7 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::error::*;
-use crate::kubernetes_api_objects::spec::{common::*, resource::*};
-use crate::vstd_ext::string_map::*;
 use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
-use vstd::string::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/spec/object_meta.rs b/src/kubernetes_api_objects/spec/object_meta.rs
index af448c086..7d4d7a705 100644
--- a/src/kubernetes_api_objects/spec/object_meta.rs
+++ b/src/kubernetes_api_objects/spec/object_meta.rs
@@ -1,11 +1,8 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::error::*;
-use crate::kubernetes_api_objects::spec::{common::*, owner_reference::*, resource::*};
-use crate::vstd_ext::string_map::*;
+use crate::kubernetes_api_objects::spec::{common::*, owner_reference::*};
 use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
-use vstd::string::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/spec/owner_reference.rs b/src/kubernetes_api_objects/spec/owner_reference.rs
index 163ff93d0..afbbd11af 100644
--- a/src/kubernetes_api_objects/spec/owner_reference.rs
+++ b/src/kubernetes_api_objects/spec/owner_reference.rs
@@ -1,11 +1,8 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::error::*;
-use crate::kubernetes_api_objects::spec::{common::*, resource::*};
-use crate::vstd_ext::string_map::*;
+use crate::kubernetes_api_objects::spec::common::*;
 use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
-use vstd::string::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/spec/persistent_volume_claim.rs b/src/kubernetes_api_objects/spec/persistent_volume_claim.rs
index cdc954836..a56fb58ba 100644
--- a/src/kubernetes_api_objects/spec/persistent_volume_claim.rs
+++ b/src/kubernetes_api_objects/spec/persistent_volume_claim.rs
@@ -6,7 +6,6 @@ use crate::kubernetes_api_objects::spec::{
 };
 use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
-use vstd::seq_lib::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/spec/pod.rs b/src/kubernetes_api_objects/spec/pod.rs
index e984960fc..8e3784460 100644
--- a/src/kubernetes_api_objects/spec/pod.rs
+++ b/src/kubernetes_api_objects/spec/pod.rs
@@ -2,13 +2,11 @@
 // SPDX-License-Identifier: MIT
 use crate::kubernetes_api_objects::error::*;
 use crate::kubernetes_api_objects::spec::{
-    affinity::*, common::*, container::*, dynamic::*, object_meta::*, resource::*,
-    resource_requirements::*, toleration::*, volume::*,
+    affinity::*, common::*, container::*, dynamic::*, object_meta::*, resource::*, toleration::*,
+    volume::*,
 };
-use crate::vstd_ext::{string_map::*, string_view::*};
+use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
-use vstd::seq_lib::*;
-use vstd::string::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/spec/pod_template_spec.rs b/src/kubernetes_api_objects/spec/pod_template_spec.rs
index 81539733c..6233f98af 100644
--- a/src/kubernetes_api_objects/spec/pod_template_spec.rs
+++ b/src/kubernetes_api_objects/spec/pod_template_spec.rs
@@ -1,13 +1,7 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::error::*;
-use crate::kubernetes_api_objects::spec::{
-    common::*, dynamic::*, object_meta::*, pod::*, resource::*,
-};
-use crate::vstd_ext::string_view::*;
+use crate::kubernetes_api_objects::spec::{object_meta::*, pod::*};
 use vstd::prelude::*;
-use vstd::seq_lib::*;
-use vstd::string::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/spec/resource_requirements.rs b/src/kubernetes_api_objects/spec/resource_requirements.rs
index 8e228e7e6..4d4060404 100644
--- a/src/kubernetes_api_objects/spec/resource_requirements.rs
+++ b/src/kubernetes_api_objects/spec/resource_requirements.rs
@@ -1,7 +1,5 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::spec::resource::*;
-use crate::vstd_ext::string_map::*;
 use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
 
diff --git a/src/kubernetes_api_objects/spec/role.rs b/src/kubernetes_api_objects/spec/role.rs
index 18711328b..8c7eeca3d 100644
--- a/src/kubernetes_api_objects/spec/role.rs
+++ b/src/kubernetes_api_objects/spec/role.rs
@@ -2,10 +2,8 @@
 // SPDX-License-Identifier: MIT
 use crate::kubernetes_api_objects::error::*;
 use crate::kubernetes_api_objects::spec::{common::*, dynamic::*, object_meta::*, resource::*};
-use crate::vstd_ext::string_map::StringMap;
 use crate::vstd_ext::string_view::StringView;
 use vstd::prelude::*;
-use vstd::seq_lib::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/spec/role_binding.rs b/src/kubernetes_api_objects/spec/role_binding.rs
index bec43a431..3bb24e9e9 100644
--- a/src/kubernetes_api_objects/spec/role_binding.rs
+++ b/src/kubernetes_api_objects/spec/role_binding.rs
@@ -2,11 +2,8 @@
 // SPDX-License-Identifier: MIT
 use crate::kubernetes_api_objects::error::*;
 use crate::kubernetes_api_objects::spec::{common::*, dynamic::*, object_meta::*, resource::*};
-use crate::vstd_ext::string_map::StringMap;
 use crate::vstd_ext::string_view::StringView;
 use vstd::prelude::*;
-use vstd::seq_lib::*;
-use vstd::string::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/spec/secret.rs b/src/kubernetes_api_objects/spec/secret.rs
index 7aa3bc914..bd6750440 100644
--- a/src/kubernetes_api_objects/spec/secret.rs
+++ b/src/kubernetes_api_objects/spec/secret.rs
@@ -2,7 +2,6 @@
 // SPDX-License-Identifier: MIT
 use crate::kubernetes_api_objects::error::*;
 use crate::kubernetes_api_objects::spec::{common::*, dynamic::*, object_meta::*, resource::*};
-use crate::vstd_ext::string_map::*;
 use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
 
diff --git a/src/kubernetes_api_objects/spec/service.rs b/src/kubernetes_api_objects/spec/service.rs
index 8fb093cce..cbecad2fe 100644
--- a/src/kubernetes_api_objects/spec/service.rs
+++ b/src/kubernetes_api_objects/spec/service.rs
@@ -2,10 +2,8 @@
 // SPDX-License-Identifier: MIT
 use crate::kubernetes_api_objects::error::*;
 use crate::kubernetes_api_objects::spec::{common::*, dynamic::*, object_meta::*, resource::*};
-use crate::vstd_ext::string_map::StringMap;
 use crate::vstd_ext::string_view::StringView;
 use vstd::prelude::*;
-use vstd::seq_lib::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/spec/service_account.rs b/src/kubernetes_api_objects/spec/service_account.rs
index a7589a798..00d5786ac 100644
--- a/src/kubernetes_api_objects/spec/service_account.rs
+++ b/src/kubernetes_api_objects/spec/service_account.rs
@@ -2,8 +2,6 @@
 // SPDX-License-Identifier: MIT
 use crate::kubernetes_api_objects::error::*;
 use crate::kubernetes_api_objects::spec::{common::*, dynamic::*, object_meta::*, resource::*};
-use crate::vstd_ext::string_map::*;
-use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/kubernetes_api_objects/spec/stateful_set.rs b/src/kubernetes_api_objects/spec/stateful_set.rs
index 4f05da359..0a2631928 100644
--- a/src/kubernetes_api_objects/spec/stateful_set.rs
+++ b/src/kubernetes_api_objects/spec/stateful_set.rs
@@ -5,11 +5,8 @@ use crate::kubernetes_api_objects::spec::{
     common::*, dynamic::*, label_selector::*, object_meta::*, persistent_volume_claim::*,
     pod_template_spec::*, resource::*,
 };
-use crate::vstd_ext::string_map::*;
 use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
-use vstd::seq_lib::*;
-use vstd::string::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/spec/toleration.rs b/src/kubernetes_api_objects/spec/toleration.rs
index 081968780..ac96c7aa5 100644
--- a/src/kubernetes_api_objects/spec/toleration.rs
+++ b/src/kubernetes_api_objects/spec/toleration.rs
@@ -1,9 +1,5 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::error::*;
-use crate::kubernetes_api_objects::spec::{common::*, dynamic::*, object_meta::*, resource::*};
-use crate::vstd_ext::string_map::*;
-use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/kubernetes_api_objects/spec/volume.rs b/src/kubernetes_api_objects/spec/volume.rs
index c0c10d762..16f3bf9d0 100644
--- a/src/kubernetes_api_objects/spec/volume.rs
+++ b/src/kubernetes_api_objects/spec/volume.rs
@@ -1,11 +1,7 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::error::*;
-use crate::kubernetes_api_objects::spec::{common::*, dynamic::*, object_meta::*, resource::*};
 use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
-use vstd::seq_lib::*;
-use vstd::string::*;
 
 verus! {
 
diff --git a/src/kubernetes_api_objects/spec/volume_resource_requirements.rs b/src/kubernetes_api_objects/spec/volume_resource_requirements.rs
index 75f11ac3d..4c354dba8 100644
--- a/src/kubernetes_api_objects/spec/volume_resource_requirements.rs
+++ b/src/kubernetes_api_objects/spec/volume_resource_requirements.rs
@@ -1,7 +1,5 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::spec::resource::*;
-use crate::vstd_ext::string_map::*;
 use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
 
diff --git a/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs b/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs
index 0e0681113..31c964081 100644
--- a/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs
+++ b/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs
@@ -1,12 +1,12 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-use crate::kubernetes_api_objects::exec::{label_selector::*, pod_template_spec::*, prelude::*};
+use crate::kubernetes_api_objects::exec::prelude::*;
 use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::reconciler::exec::{io::*, reconciler::*};
 use crate::vreplicaset_controller::model::reconciler as model_reconciler;
 use crate::vreplicaset_controller::trusted::{exec_types::*, step::*};
 use crate::vstd_ext::option_lib::*;
-use crate::vstd_ext::{string_map::StringMap, string_view::*};
+use crate::vstd_ext::string_map::StringMap;
 use vstd::prelude::*;
 use vstd::seq_lib::*;
 
diff --git a/src/v2/controllers/vreplicaset_controller/model/reconciler.rs b/src/v2/controllers/vreplicaset_controller/model/reconciler.rs
index df98fffff..059be6980 100644
--- a/src/v2/controllers/vreplicaset_controller/model/reconciler.rs
+++ b/src/v2/controllers/vreplicaset_controller/model/reconciler.rs
@@ -1,7 +1,7 @@
 use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::reconciler::spec::{io::*, reconciler::*};
 use crate::vreplicaset_controller::trusted::{spec_types::*, step::*};
-use vstd::{prelude::*, string::*};
+use vstd::prelude::*;
 
 verus! {
 
diff --git a/src/v2/controllers/vreplicaset_controller/trusted/exec_types.rs b/src/v2/controllers/vreplicaset_controller/trusted/exec_types.rs
index 8aaf14a71..879f20683 100644
--- a/src/v2/controllers/vreplicaset_controller/trusted/exec_types.rs
+++ b/src/v2/controllers/vreplicaset_controller/trusted/exec_types.rs
@@ -5,8 +5,7 @@ use crate::kubernetes_api_objects::exec::{
     api_resource::*, label_selector::*, pod_template_spec::*, prelude::*,
 };
 use crate::kubernetes_api_objects::spec::resource::*;
-use crate::vreplicaset_controller::trusted::{spec_types, step::*};
-use crate::vstd_ext::{string_map::*, string_view::*};
+use crate::vreplicaset_controller::trusted::spec_types;
 use deps_hack::kube::Resource;
 use vstd::prelude::*;
 
diff --git a/src/v2/controllers/vreplicaset_controller/trusted/liveness_theorem.rs b/src/v2/controllers/vreplicaset_controller/trusted/liveness_theorem.rs
index d643746ae..13c553a46 100644
--- a/src/v2/controllers/vreplicaset_controller/trusted/liveness_theorem.rs
+++ b/src/v2/controllers/vreplicaset_controller/trusted/liveness_theorem.rs
@@ -1,8 +1,7 @@
 use crate::kubernetes_api_objects::spec::prelude::*;
 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;
+use crate::vreplicaset_controller::trusted::spec_types::*;
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/v2/controllers/vreplicaset_controller/trusted/spec_types.rs b/src/v2/controllers/vreplicaset_controller/trusted/spec_types.rs
index 919bc4dbb..0f0b2388c 100644
--- a/src/v2/controllers/vreplicaset_controller/trusted/spec_types.rs
+++ b/src/v2/controllers/vreplicaset_controller/trusted/spec_types.rs
@@ -1,12 +1,7 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
 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::*, message::*};
-use crate::vreplicaset_controller::trusted::step::*;
-use crate::vstd_ext::string_view::*;
+use crate::kubernetes_api_objects::spec::{label_selector::*, pod_template_spec::*, prelude::*};
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/v2/kubernetes_cluster/proof/cluster.rs b/src/v2/kubernetes_cluster/proof/cluster.rs
index fb25a9c40..3e437e1ce 100644
--- a/src/v2/kubernetes_cluster/proof/cluster.rs
+++ b/src/v2/kubernetes_cluster/proof/cluster.rs
@@ -1,6 +1,5 @@
-use crate::kubernetes_api_objects::spec::prelude::*;
+use crate::kubernetes_cluster::spec::cluster::*;
 use crate::temporal_logic::{defs::*, rules::*};
-use crate::kubernetes_cluster::spec::{cluster::*, message::*};
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/v2/kubernetes_cluster/proof/controller_runtime_safety.rs b/src/v2/kubernetes_cluster/proof/controller_runtime_safety.rs
index b5d80af28..b0d48ffb6 100644
--- a/src/v2/kubernetes_cluster/proof/controller_runtime_safety.rs
+++ b/src/v2/kubernetes_cluster/proof/controller_runtime_safety.rs
@@ -1,10 +1,7 @@
 use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::kubernetes_cluster::spec::{
-    api_server::{state_machine::transition_by_etcd, types::*},
-    cluster::*,
-    controller::types::*,
-    external::{state_machine::*, types::*},
-    message::*,
+    api_server::state_machine::transition_by_etcd, cluster::*, controller::types::*,
+    external::state_machine::*, message::*,
 };
 use crate::temporal_logic::{defs::*, rules::*};
 use vstd::prelude::*;
diff --git a/src/v2/kubernetes_cluster/proof/failures_liveness.rs b/src/v2/kubernetes_cluster/proof/failures_liveness.rs
index 6919a3aed..3497fff9c 100644
--- a/src/v2/kubernetes_cluster/proof/failures_liveness.rs
+++ b/src/v2/kubernetes_cluster/proof/failures_liveness.rs
@@ -1,6 +1,5 @@
-use crate::kubernetes_api_objects::spec::prelude::*;
+use crate::kubernetes_cluster::spec::cluster::*;
 use crate::temporal_logic::{defs::*, rules::*};
-use crate::kubernetes_cluster::spec::{cluster::*, message::*};
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/v2/kubernetes_cluster/proof/network_liveness.rs b/src/v2/kubernetes_cluster/proof/network_liveness.rs
index 8bc1c8895..68212c67f 100644
--- a/src/v2/kubernetes_cluster/proof/network_liveness.rs
+++ b/src/v2/kubernetes_cluster/proof/network_liveness.rs
@@ -1,10 +1,5 @@
-use crate::kubernetes_api_objects::spec::prelude::*;
+use crate::kubernetes_cluster::spec::{api_server::types::*, cluster::*, message::*};
 use crate::temporal_logic::{defs::*, rules::*};
-use crate::kubernetes_cluster::spec::{
-    api_server::types::*, cluster::*, message::*,
-};
-use crate::vstd_ext::multiset_lib::*;
-use vstd::assert_multisets_equal;
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/v2/kubernetes_cluster/proof/objects_in_reconcile.rs b/src/v2/kubernetes_cluster/proof/objects_in_reconcile.rs
index 0353e308f..1c5a4d46e 100644
--- a/src/v2/kubernetes_cluster/proof/objects_in_reconcile.rs
+++ b/src/v2/kubernetes_cluster/proof/objects_in_reconcile.rs
@@ -1,7 +1,6 @@
 use crate::kubernetes_api_objects::spec::prelude::*;
-use crate::kubernetes_cluster::spec::{cluster::*, message::*};
+use crate::kubernetes_cluster::spec::cluster::*;
 use crate::temporal_logic::{defs::*, rules::*};
-use crate::vstd_ext::string_view::StringView;
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/v2/kubernetes_cluster/proof/objects_in_store.rs b/src/v2/kubernetes_cluster/proof/objects_in_store.rs
index f218f6582..c2e8d2cb1 100644
--- a/src/v2/kubernetes_cluster/proof/objects_in_store.rs
+++ b/src/v2/kubernetes_cluster/proof/objects_in_store.rs
@@ -1,12 +1,9 @@
 use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::kubernetes_cluster::spec::{
-    api_server::state_machine::{deletion_timestamp, unmarshallable_object, valid_object},
+    api_server::state_machine::{unmarshallable_object, valid_object},
     cluster::*,
-    install_helpers::*,
-    message::*,
 };
 use crate::temporal_logic::{defs::*, rules::*};
-use crate::vstd_ext::string_view::StringView;
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/v2/kubernetes_cluster/proof/retentive_cluster.rs b/src/v2/kubernetes_cluster/proof/retentive_cluster.rs
index bfca5a5f6..5f4463390 100644
--- a/src/v2/kubernetes_cluster/proof/retentive_cluster.rs
+++ b/src/v2/kubernetes_cluster/proof/retentive_cluster.rs
@@ -1,6 +1,5 @@
-use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::kubernetes_cluster::spec::{cluster::*, retentive_cluster::*};
-use crate::temporal_logic::{defs::*, rules::*};
+use crate::temporal_logic::defs::*;
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/v2/kubernetes_cluster/proof/stability.rs b/src/v2/kubernetes_cluster/proof/stability.rs
index 034c06b36..3ee067f4e 100644
--- a/src/v2/kubernetes_cluster/proof/stability.rs
+++ b/src/v2/kubernetes_cluster/proof/stability.rs
@@ -1,6 +1,6 @@
-use crate::state_machine::{action::*, state_machine::*};
-use crate::temporal_logic::{defs::*, rules::*};
 use crate::kubernetes_cluster::spec::cluster::*;
+use crate::state_machine::action::*;
+use crate::temporal_logic::{defs::*, rules::*};
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/v2/kubernetes_cluster/proof/transition_validation.rs b/src/v2/kubernetes_cluster/proof/transition_validation.rs
index 4277ad47c..ebc433e69 100644
--- a/src/v2/kubernetes_cluster/proof/transition_validation.rs
+++ b/src/v2/kubernetes_cluster/proof/transition_validation.rs
@@ -1,11 +1,6 @@
 use crate::kubernetes_api_objects::spec::prelude::*;
+use crate::kubernetes_cluster::spec::cluster::*;
 use crate::temporal_logic::{defs::*, rules::*};
-use crate::kubernetes_cluster::spec::{
-    api_server::state_machine::{deletion_timestamp, unmarshallable_object, valid_object},
-    cluster::*,
-    message::*,
-};
-use crate::vstd_ext::string_view::StringView;
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/v2/kubernetes_cluster/proof/wf1_helpers.rs b/src/v2/kubernetes_cluster/proof/wf1_helpers.rs
index 9f4a212ff..2ddf129ae 100644
--- a/src/v2/kubernetes_cluster/proof/wf1_helpers.rs
+++ b/src/v2/kubernetes_cluster/proof/wf1_helpers.rs
@@ -1,12 +1,8 @@
 use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::kubernetes_cluster::spec::{
-    api_server::state_machine::api_server, api_server::types::*,
-    builtin_controllers::state_machine::builtin_controllers, builtin_controllers::types::*,
-    cluster::*, controller::state_machine::controller, controller::types::*,
-    external::state_machine::external, external::types::*, message::*,
-    network::state_machine::network, network::types::*,
+    api_server::types::*, builtin_controllers::types::*, cluster::*, controller::types::*,
+    external::types::*, message::*,
 };
-use crate::state_machine::{action::*, state_machine::*};
 use crate::temporal_logic::{defs::*, rules::*};
 use vstd::prelude::*;
 
diff --git a/src/v2/kubernetes_cluster/spec/api_server/state_machine.rs b/src/v2/kubernetes_cluster/spec/api_server/state_machine.rs
index d9c6b4eca..2a16ac8f6 100644
--- a/src/v2/kubernetes_cluster/spec/api_server/state_machine.rs
+++ b/src/v2/kubernetes_cluster/spec/api_server/state_machine.rs
@@ -3,7 +3,6 @@ use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::kubernetes_cluster::spec::{api_server::types::*, message::*};
 use crate::state_machine::action::*;
 use crate::state_machine::state_machine::*;
-use crate::temporal_logic::defs::*;
 use crate::vstd_ext::{map_lib::*, string_view::*};
 use vstd::{multiset::*, prelude::*};
 
diff --git a/src/v2/kubernetes_cluster/spec/api_server/types.rs b/src/v2/kubernetes_cluster/spec/api_server/types.rs
index 541fd0daf..57f76f30e 100644
--- a/src/v2/kubernetes_cluster/spec/api_server/types.rs
+++ b/src/v2/kubernetes_cluster/spec/api_server/types.rs
@@ -2,7 +2,6 @@ use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::kubernetes_cluster::spec::message::*;
 use crate::state_machine::action::*;
 use crate::state_machine::state_machine::*;
-use crate::temporal_logic::defs::*;
 use crate::vstd_ext::string_view::StringView;
 use vstd::{multiset::*, prelude::*};
 
diff --git a/src/v2/kubernetes_cluster/spec/builtin_controllers/garbage_collector.rs b/src/v2/kubernetes_cluster/spec/builtin_controllers/garbage_collector.rs
index b8036f4da..6d92a8bf1 100644
--- a/src/v2/kubernetes_cluster/spec/builtin_controllers/garbage_collector.rs
+++ b/src/v2/kubernetes_cluster/spec/builtin_controllers/garbage_collector.rs
@@ -1,9 +1,6 @@
 use crate::kubernetes_api_objects::spec::prelude::*;
-use crate::kubernetes_cluster::spec::{
-    api_server::types::APIServerState, builtin_controllers::types::*, message::*,
-};
+use crate::kubernetes_cluster::spec::{builtin_controllers::types::*, message::*};
 use crate::state_machine::action::*;
-use crate::state_machine::state_machine::*;
 use vstd::{multiset::*, prelude::*};
 
 verus! {
diff --git a/src/v2/kubernetes_cluster/spec/builtin_controllers/state_machine.rs b/src/v2/kubernetes_cluster/spec/builtin_controllers/state_machine.rs
index 7e82787d6..ae60db195 100644
--- a/src/v2/kubernetes_cluster/spec/builtin_controllers/state_machine.rs
+++ b/src/v2/kubernetes_cluster/spec/builtin_controllers/state_machine.rs
@@ -1,12 +1,6 @@
-use crate::kubernetes_api_objects::spec::prelude::*;
-use crate::kubernetes_cluster::spec::{
-    api_server::types::APIServerState,
-    builtin_controllers::{garbage_collector::*, types::*},
-    message::*,
-};
-use crate::state_machine::action::*;
+use crate::kubernetes_cluster::spec::builtin_controllers::{garbage_collector::*, types::*};
 use crate::state_machine::state_machine::*;
-use vstd::{multiset::*, prelude::*};
+use vstd::prelude::*;
 
 verus! {
 
diff --git a/src/v2/kubernetes_cluster/spec/builtin_controllers/types.rs b/src/v2/kubernetes_cluster/spec/builtin_controllers/types.rs
index f0a57e285..a0c81bf1c 100644
--- a/src/v2/kubernetes_cluster/spec/builtin_controllers/types.rs
+++ b/src/v2/kubernetes_cluster/spec/builtin_controllers/types.rs
@@ -1,5 +1,5 @@
 use crate::kubernetes_api_objects::spec::prelude::*;
-use crate::kubernetes_cluster::spec::{api_server::types::APIServerState, message::*};
+use crate::kubernetes_cluster::spec::message::*;
 use crate::state_machine::action::*;
 use crate::state_machine::state_machine::*;
 use vstd::{multiset::*, prelude::*};
diff --git a/src/v2/kubernetes_cluster/spec/cluster.rs b/src/v2/kubernetes_cluster/spec/cluster.rs
index 68cb15aaa..f6b8b9fe3 100644
--- a/src/v2/kubernetes_cluster/spec/cluster.rs
+++ b/src/v2/kubernetes_cluster/spec/cluster.rs
@@ -7,7 +7,7 @@ use crate::kubernetes_cluster::spec::{
     external::types::*, message::*, network::state_machine::network, network::types::*,
     pod_monkey::state_machine::pod_monkey, pod_monkey::types::*,
 };
-use crate::state_machine::{action::*, state_machine::*};
+use crate::state_machine::action::*;
 use crate::temporal_logic::defs::*;
 use vstd::{multiset::*, prelude::*};
 
diff --git a/src/v2/kubernetes_cluster/spec/controller/state_machine.rs b/src/v2/kubernetes_cluster/spec/controller/state_machine.rs
index 945d599d2..910a5d388 100644
--- a/src/v2/kubernetes_cluster/spec/controller/state_machine.rs
+++ b/src/v2/kubernetes_cluster/spec/controller/state_machine.rs
@@ -2,7 +2,6 @@ use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::kubernetes_cluster::spec::{controller::types::*, message::*};
 use crate::state_machine::action::*;
 use crate::state_machine::state_machine::*;
-use crate::temporal_logic::defs::*;
 use vstd::{multiset::*, prelude::*};
 
 verus! {
diff --git a/src/v2/kubernetes_cluster/spec/external/types.rs b/src/v2/kubernetes_cluster/spec/external/types.rs
index 5adaa6cdf..2d087dc4c 100644
--- a/src/v2/kubernetes_cluster/spec/external/types.rs
+++ b/src/v2/kubernetes_cluster/spec/external/types.rs
@@ -2,8 +2,6 @@ use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::kubernetes_cluster::spec::message::*;
 use crate::state_machine::action::*;
 use crate::state_machine::state_machine::*;
-
-use crate::temporal_logic::defs::*;
 use vstd::{multiset::*, prelude::*};
 
 verus! {
diff --git a/src/v2/kubernetes_cluster/spec/network/state_machine.rs b/src/v2/kubernetes_cluster/spec/network/state_machine.rs
index 36b6334f2..a3c2a6d6e 100644
--- a/src/v2/kubernetes_cluster/spec/network/state_machine.rs
+++ b/src/v2/kubernetes_cluster/spec/network/state_machine.rs
@@ -2,7 +2,6 @@ use crate::kubernetes_cluster::spec::message::*;
 use crate::kubernetes_cluster::spec::network::types::*;
 use crate::state_machine::action::*;
 use crate::state_machine::state_machine::*;
-use crate::temporal_logic::defs::*;
 use vstd::{multiset::*, prelude::*};
 
 verus! {
diff --git a/src/v2/kubernetes_cluster/spec/network/types.rs b/src/v2/kubernetes_cluster/spec/network/types.rs
index 2dd58211c..db9349f18 100644
--- a/src/v2/kubernetes_cluster/spec/network/types.rs
+++ b/src/v2/kubernetes_cluster/spec/network/types.rs
@@ -1,7 +1,4 @@
 use crate::kubernetes_cluster::spec::message::*;
-use crate::state_machine::action::*;
-use crate::state_machine::state_machine::*;
-use crate::temporal_logic::defs::*;
 use vstd::{multiset::*, prelude::*};
 
 verus! {
diff --git a/src/v2/kubernetes_cluster/spec/pod_monkey/state_machine.rs b/src/v2/kubernetes_cluster/spec/pod_monkey/state_machine.rs
index 025e15457..92833603a 100644
--- a/src/v2/kubernetes_cluster/spec/pod_monkey/state_machine.rs
+++ b/src/v2/kubernetes_cluster/spec/pod_monkey/state_machine.rs
@@ -1,7 +1,6 @@
 use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::kubernetes_cluster::spec::{message::*, pod_monkey::types::*};
 use crate::state_machine::{action::*, state_machine::*};
-use crate::temporal_logic::defs::*;
 use vstd::{multiset::*, prelude::*};
 
 verus! {
diff --git a/src/v2/kubernetes_cluster/spec/pod_monkey/types.rs b/src/v2/kubernetes_cluster/spec/pod_monkey/types.rs
index 7f5737449..41392653d 100644
--- a/src/v2/kubernetes_cluster/spec/pod_monkey/types.rs
+++ b/src/v2/kubernetes_cluster/spec/pod_monkey/types.rs
@@ -1,6 +1,6 @@
-use crate::kubernetes_api_objects::spec::{pod::*, resource::*};
-use crate::state_machine::{action::*, state_machine::*};
+use crate::kubernetes_api_objects::spec::pod::*;
 use crate::kubernetes_cluster::spec::message::*;
+use crate::state_machine::{action::*, state_machine::*};
 use vstd::{multiset::*, prelude::*};
 
 verus! {
diff --git a/src/v2/kubernetes_cluster/spec/retentive_cluster.rs b/src/v2/kubernetes_cluster/spec/retentive_cluster.rs
index 2869bce06..586eb2509 100644
--- a/src/v2/kubernetes_cluster/spec/retentive_cluster.rs
+++ b/src/v2/kubernetes_cluster/spec/retentive_cluster.rs
@@ -1,9 +1,6 @@
-use crate::kubernetes_api_objects::error::*;
-use crate::kubernetes_api_objects::spec::prelude::*;
 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::*};
+use vstd::prelude::*;
 
 verus! {
 
diff --git a/src/v2/reconciler/exec/io.rs b/src/v2/reconciler/exec/io.rs
index bde6254da..693c72a37 100644
--- a/src/v2/reconciler/exec/io.rs
+++ b/src/v2/reconciler/exec/io.rs
@@ -1,6 +1,6 @@
 use crate::kubernetes_api_objects::exec::api_method::*;
 use crate::reconciler::spec::io::*;
-use vstd::{prelude::*, view::*};
+use vstd::prelude::*;
 
 use vstd::pervasive::unreached;
 
diff --git a/src/v2/reconciler/exec/reconciler.rs b/src/v2/reconciler/exec/reconciler.rs
index 17a7c453b..b8c2efdda 100644
--- a/src/v2/reconciler/exec/reconciler.rs
+++ b/src/v2/reconciler/exec/reconciler.rs
@@ -1,6 +1,6 @@
 use crate::kubernetes_api_objects::spec::resource::{CustomResourceView, ResourceView};
 use crate::reconciler::exec::io::*;
-use crate::reconciler::spec::{io::*, reconciler::Reconciler as ModelReconciler};
+use crate::reconciler::spec::reconciler::Reconciler as ModelReconciler;
 use crate::vstd_ext::option_lib::*;
 use vstd::prelude::*;
 
diff --git a/src/v2/reconciler/exec/resource_builder.rs b/src/v2/reconciler/exec/resource_builder.rs
index 741fb3d7c..3912ccceb 100644
--- a/src/v2/reconciler/exec/resource_builder.rs
+++ b/src/v2/reconciler/exec/resource_builder.rs
@@ -1,10 +1,6 @@
-use crate::kubernetes_api_objects::exec::{api_method::*, dynamic::*, resource::*};
-use crate::reconciler::exec::{io::*, reconciler::*};
+use crate::kubernetes_api_objects::exec::{api_method::*, dynamic::*};
 use crate::reconciler::spec::resource_builder;
-use crate::vstd_ext::{string_map::StringMap, string_view::*};
 use vstd::prelude::*;
-use vstd::seq_lib::*;
-use vstd::string::*;
 
 verus! {
 
diff --git a/src/v2/reconciler/spec/io.rs b/src/v2/reconciler/spec/io.rs
index 8320f5fee..269e58ef2 100644
--- a/src/v2/reconciler/spec/io.rs
+++ b/src/v2/reconciler/spec/io.rs
@@ -1,8 +1,7 @@
 use crate::kubernetes_api_objects::{
     error::UnmarshalError,
-    spec::{api_method::*, common::*, resource::*},
+    spec::{api_method::*, resource::*},
 };
-use crate::kubernetes_cluster::spec::message::*;
 use vstd::prelude::*;
 
 verus! {
diff --git a/src/v2/reconciler/spec/reconciler.rs b/src/v2/reconciler/spec/reconciler.rs
index ad976b559..d94014ef6 100644
--- a/src/v2/reconciler/spec/reconciler.rs
+++ b/src/v2/reconciler/spec/reconciler.rs
@@ -1,5 +1,4 @@
-use crate::kubernetes_api_objects::spec::{api_method::*, common::*, dynamic::*, resource::*};
-use crate::kubernetes_cluster::spec::message::*;
+use crate::kubernetes_api_objects::spec::resource::*;
 use crate::reconciler::spec::io::*;
 use vstd::prelude::*;
 
@@ -20,7 +19,7 @@ verus! {
 // correspondingly. Since Rust doesn't support type equality constraint (see https://github.com/rust-lang/rust/issues/20041),
 // instead of stating the equality constraint, we state that the spec Reconciler is built
 // using the views of the exec Reconciler's S, K, EReq and EResp.
-pub trait Reconciler<S, K, EReq, EResp> {
+pub trait Reconciler<S, K: CustomResourceView, EReq, EResp> {
     // reconcile_init_state returns the initial local state that the reconciler starts
     // its reconcile function with.
     spec fn reconcile_init_state() -> S;
diff --git a/src/v2/reconciler/spec/resource_builder.rs b/src/v2/reconciler/spec/resource_builder.rs
index 9b4c5dca3..d9666e6e2 100644
--- a/src/v2/reconciler/spec/resource_builder.rs
+++ b/src/v2/reconciler/spec/resource_builder.rs
@@ -1,9 +1,5 @@
 use crate::kubernetes_api_objects::spec::prelude::*;
-use crate::reconciler::spec::{io::*, reconciler::*};
-use crate::temporal_logic::defs::*;
-use crate::vstd_ext::string_view::*;
 use vstd::prelude::*;
-use vstd::string::*;
 
 verus! {
 
diff --git a/src/v2/shim_layer/controller_runtime.rs b/src/v2/shim_layer/controller_runtime.rs
index 30e0c6777..b87709ef5 100644
--- a/src/v2/shim_layer/controller_runtime.rs
+++ b/src/v2/shim_layer/controller_runtime.rs
@@ -4,19 +4,17 @@ use crate::kubernetes_api_objects::exec::{api_method::*, dynamic::*, resource::*
 use crate::kubernetes_api_objects::spec::resource::*;
 use crate::reconciler::exec::{io::*, reconciler::*};
 use crate::shim_layer::fault_injection::*;
-use builtin::*;
-use builtin_macros::*;
 use core::fmt::Debug;
 use core::hash::Hash;
 use deps_hack::anyhow::Result;
-use deps_hack::futures::{Future, Stream, StreamExt, TryFuture};
+use deps_hack::futures::StreamExt;
 use deps_hack::kube::{
-    api::{Api, DeleteParams, ListParams, ObjectMeta, PostParams, Resource},
+    api::{Api, DeleteParams, ListParams, PostParams, Resource},
     runtime::{
-        controller::{self, Action, Controller},
-        reflector, watcher,
+        controller::{Action, Controller},
+        watcher,
     },
-    Client, CustomResource, CustomResourceExt,
+    Client, CustomResourceExt,
 };
 use deps_hack::kube_core::{ErrorResponse, NamespaceResourceScope};
 use deps_hack::serde::{de::DeserializeOwned, Serialize};
@@ -24,7 +22,7 @@ use deps_hack::tracing::{error, info, warn};
 use deps_hack::Error;
 use std::sync::Arc;
 use std::time::Duration;
-use vstd::{string::*, view::*};
+use vstd::string::*;
 
 // The shim layer connects the verified reconciler to the trusted kube-rs APIs.
 // The key is to implement the reconcile function (impl FnMut(Arc<K>, Arc<Ctx>) -> ReconcilerFut),
diff --git a/src/v2/shim_layer/fault_injection.rs b/src/v2/shim_layer/fault_injection.rs
index 7e8222152..4cc64cf86 100644
--- a/src/v2/shim_layer/fault_injection.rs
+++ b/src/v2/shim_layer/fault_injection.rs
@@ -1,15 +1,10 @@
-use builtin::*;
-use builtin_macros::*;
-use core::fmt::Debug;
 use deps_hack::anyhow::Result;
-use deps_hack::futures::{Future, Stream, StreamExt, TryFuture};
 use deps_hack::k8s_openapi::api::core::v1::ConfigMap;
 use deps_hack::kube::{
-    api::{Api, ObjectMeta, PostParams, Resource},
+    api::{Api, PostParams},
     Client,
 };
 use deps_hack::tracing::info;
-use deps_hack::Error;
 
 pub async fn crash_or_continue(
     client: &Client,
diff --git a/src/vstd_ext/string_map.rs b/src/vstd_ext/string_map.rs
index a45e6786e..9d1d138e7 100644
--- a/src/vstd_ext/string_map.rs
+++ b/src/vstd_ext/string_map.rs
@@ -1,5 +1,4 @@
 use vstd::prelude::*;
-use vstd::string::*;
 
 verus! {
 
diff --git a/src/vstd_ext/string_view.rs b/src/vstd_ext/string_view.rs
index ac668437c..fee6d457f 100644
--- a/src/vstd_ext/string_view.rs
+++ b/src/vstd_ext/string_view.rs
@@ -2,7 +2,6 @@
 // SPDX-License-Identifier: MIT
 
 use vstd::prelude::*;
-use vstd::string::*;
 
 verus! {