Fix zookeeper controller bug caused by optional storageClassName (#327)

Signed-off-by: Xudong Sun <[email protected]>
anvil-verifier · Oct 2, 2023 · e6b6074 · e6b6074
1 parent b787aee
commit e6b6074
Show file tree

Hide file tree

Showing 9 changed files with 26 additions and 12 deletions.
diff --git a/deploy/zookeeper/crd.yaml b/deploy/zookeeper/crd.yaml
@@ -571,7 +571,6 @@ spec:
                         - rule: "self == oldSelf"
                           message: changing persistence.enabled is not supported
                     storageClassName:
-                      nullable: true
                       type: string
                       x-kubernetes-validations:
                         - rule: "self == oldSelf"
@@ -584,6 +583,7 @@ spec:
                           message: changing persistence.storageSize is not supported
                   required:
                     - enabled
+                    - storageClassName
                     - storageSize
                   type: object
                 ports:

diff --git a/deploy/zookeeper/zookeeper.yaml b/deploy/zookeeper/zookeeper.yaml
@@ -31,3 +31,4 @@ spec:
   persistence:
     enabled: true
     storageSize: 20Gi
+    storageClassName: standard
diff --git a/e2e/src/zookeeper_e2e.rs b/e2e/src/zookeeper_e2e.rs
@@ -57,6 +57,7 @@ pub fn zookeeper_cluster() -> String {
       persistence:
         enabled: true
         storageSize: 20Gi
+        storageClassName: standard
     "
     .to_string()
 }
@@ -96,6 +97,7 @@ pub fn zookeeper_cluster_ephemeral() -> String {
       persistence:
         enabled: false
         storageSize: 20Gi
+        storageClassName: standard
     "
     .to_string()
 }

diff --git a/src/controller_examples/zookeeper_controller/exec/reconciler.rs b/src/controller_examples/zookeeper_controller/exec/reconciler.rs
@@ -1341,7 +1341,7 @@ fn make_stateful_set(zk: &ZookeeperCluster, rv: &String) -> (stateful_set: State
                             });
                             resources
                         });
-                        pvc_spec.overwrite_storage_class_name(zk.spec().persistence().storage_class_name());
+                        pvc_spec.set_storage_class_name(zk.spec().persistence().storage_class_name());
                         pvc_spec
                     });
                     pvc

diff --git a/src/controller_examples/zookeeper_controller/exec/types.rs b/src/controller_examples/zookeeper_controller/exec/types.rs
@@ -467,15 +467,11 @@ impl ZookeeperPersistence {
     }
 
     #[verifier(external_body)]
-    pub fn storage_class_name(&self) -> (storage_class_name: Option<String>)
+    pub fn storage_class_name(&self) -> (storage_class_name: String)
         ensures
-            self@.storage_class_name.is_Some() == storage_class_name.is_Some(),
-            storage_class_name.is_Some() ==> storage_class_name.get_Some_0()@ == self@.storage_class_name.get_Some_0(),
+            self@.storage_class_name == storage_class_name@,
     {
-        match &self.inner.storage_class_name {
-            Some(s) => Some(String::from_rust_string(s.clone())),
-            None => None,
-        }
+        String::from_rust_string(self.inner.storage_class_name.clone())
     }
 }
 

diff --git a/src/controller_examples/zookeeper_controller/spec/reconciler.rs b/src/controller_examples/zookeeper_controller/spec/reconciler.rs
@@ -1139,7 +1139,7 @@ pub open spec fn make_stateful_set(zk: ZookeeperClusterView, rv: StringView) ->
                                 .insert(new_strlit("storage")@, zk.spec.persistence.storage_size)
                             )
                         )
-                        .overwrite_storage_class_name(zk.spec.persistence.storage_class_name)
+                        .set_storage_class_name(zk.spec.persistence.storage_class_name)
                     )
                 ]
             } else {

diff --git a/src/controller_examples/zookeeper_controller/spec/types.rs b/src/controller_examples/zookeeper_controller/spec/types.rs
@@ -186,7 +186,7 @@ pub struct ZookeeperConfigView {
 pub struct ZookeeperPersistenceView {
     pub enabled: bool,
     pub storage_size: StringView,
-    pub storage_class_name: Option<StringView>,
+    pub storage_class_name: StringView,
 }
 
 pub struct ZookeeperClusterStatusView {

diff --git a/src/deps_hack/src/lib.rs b/src/deps_hack/src/lib.rs
@@ -115,7 +115,7 @@ pub struct ZookeeperPersistence {
     #[serde(rename = "storageSize")]
     pub storage_size: k8s_openapi::apimachinery::pkg::api::resource::Quantity,
     #[serde(rename = "storageClassName")]
-    pub storage_class_name: Option<String>,
+    pub storage_class_name: String,
 }
 
 #[derive(

diff --git a/src/kubernetes_api_objects/persistent_volume_claim.rs b/src/kubernetes_api_objects/persistent_volume_claim.rs
@@ -157,6 +157,14 @@ impl PersistentVolumeClaimSpec {
         self.inner.resources = Some(resources.into_kube());
     }
 
+    #[verifier(external_body)]
+    pub fn set_storage_class_name(&mut self, storage_class_name: String)
+        ensures
+            self@ == old(self)@.set_storage_class_name(storage_class_name@),
+    {
+        self.inner.storage_class_name = Some(storage_class_name.into_rust_string());
+    }
+
     #[verifier(external_body)]
     pub fn overwrite_storage_class_name(&mut self, storage_class_name: Option<String>)
         ensures
@@ -341,6 +349,13 @@ impl PersistentVolumeClaimSpecView {
         }
     }
 
+    pub open spec fn set_storage_class_name(self, storage_class_name: StringView) -> PersistentVolumeClaimSpecView {
+        PersistentVolumeClaimSpecView {
+            storage_class_name: Some(storage_class_name),
+            ..self
+        }
+    }
+
     pub open spec fn overwrite_storage_class_name(self, storage_class_name: Option<StringView>) -> PersistentVolumeClaimSpecView {
         PersistentVolumeClaimSpecView {
             storage_class_name: storage_class_name,