Add labels and annotations to desired state

Signed-off-by: Wenjie Ma <[email protected]>
anvil-verifier · Oct 3, 2023 · ecd4a44 · ecd4a44
1 parent cbfc060
commit ecd4a44
Show file tree

Hide file tree

Showing 10 changed files with 31 additions and 45 deletions.
diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/default_user_secret.rs b/src/controller_examples/rabbitmq_controller/spec/resource/default_user_secret.rs
@@ -55,6 +55,8 @@ impl ResourceBuilder for DefaultUserSecretBuilder {
         &&& 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
     }
 
     open spec fn unchangeable(object: DynamicObjectView, rabbitmq: RabbitmqClusterView) -> bool {

diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/erlang_cookie.rs b/src/controller_examples/rabbitmq_controller/spec/resource/erlang_cookie.rs
@@ -55,6 +55,8 @@ impl ResourceBuilder for ErlangCookieBuilder {
         &&& 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
     }
 
     open spec fn unchangeable(object: DynamicObjectView, rabbitmq: RabbitmqClusterView) -> bool {

diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/headless_service.rs b/src/controller_examples/rabbitmq_controller/spec/resource/headless_service.rs
@@ -62,6 +62,8 @@ impl ResourceBuilder for HeadlessServiceBuilder {
             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
     }
 
     open spec fn unchangeable(object: DynamicObjectView, rabbitmq: RabbitmqClusterView) -> bool {

diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/rabbitmq_plugins.rs b/src/controller_examples/rabbitmq_controller/spec/resource/rabbitmq_plugins.rs
@@ -55,6 +55,8 @@ impl ResourceBuilder for PluginsConfigMapBuilder {
         &&& 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
     }
 
     open spec fn unchangeable(object: DynamicObjectView, rabbitmq: RabbitmqClusterView) -> bool {

diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/role.rs b/src/controller_examples/rabbitmq_controller/spec/resource/role.rs
@@ -55,6 +55,8 @@ impl ResourceBuilder for RoleBuilder {
         &&& 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
     }
 
     open spec fn unchangeable(object: DynamicObjectView, rabbitmq: RabbitmqClusterView) -> bool {

diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/role_binding.rs b/src/controller_examples/rabbitmq_controller/spec/resource/role_binding.rs
@@ -56,6 +56,8 @@ impl ResourceBuilder for RoleBindingBuilder {
         &&& 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
     }
 
     open spec fn unchangeable(object: DynamicObjectView, rabbitmq: RabbitmqClusterView) -> bool {

diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/service.rs b/src/controller_examples/rabbitmq_controller/spec/resource/service.rs
@@ -61,6 +61,8 @@ impl ResourceBuilder for ServiceBuilder {
             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
     }
 
     open spec fn unchangeable(object: DynamicObjectView, rabbitmq: RabbitmqClusterView) -> bool {

diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/service_account.rs b/src/controller_examples/rabbitmq_controller/spec/resource/service_account.rs
@@ -55,6 +55,8 @@ impl ResourceBuilder for ServiceAccountBuilder {
         &&& 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
     }
 
     open spec fn unchangeable(object: DynamicObjectView, rabbitmq: RabbitmqClusterView) -> bool {

diff --git a/src/controller_examples/rabbitmq_controller/spec/resource/stateful_set.rs b/src/controller_examples/rabbitmq_controller/spec/resource/stateful_set.rs
@@ -60,12 +60,14 @@ impl ResourceBuilder for StatefulSetBuilder {
         let obj = resources[key];
         let cm_key = ServerConfigMapBuilder::get_request(rabbitmq).key;
         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()));
         &&& resources.contains_key(key)
         &&& resources.contains_key(cm_key)
         &&& cm_obj.metadata.resource_version.is_Some()
         &&& StatefulSetView::unmarshal(obj).is_Ok()
-        &&& StatefulSetView::unmarshal(obj).get_Ok_0().spec
-            == (#[trigger] make_stateful_set(rabbitmq, int_to_string_view(cm_obj.metadata.resource_version.get_Some_0()))).spec
+        &&& StatefulSetView::unmarshal(obj).get_Ok_0().spec == made_sts.spec
+        &&& obj.metadata.labels == made_sts.metadata.labels
+        &&& obj.metadata.annotations == made_sts.metadata.annotations
     }
 
     open spec fn unchangeable(object: DynamicObjectView, rabbitmq: RabbitmqClusterView) -> bool {

diff --git a/src/kubernetes_cluster/proof/cluster_safety.rs b/src/kubernetes_cluster/proof/cluster_safety.rs
@@ -32,49 +32,17 @@ pub open spec fn etcd_object_is_well_formed(key: ObjectRef) -> StatePred<Self> {
         &&& s.resources()[key].metadata.resource_version.get_Some_0() < s.kubernetes_api_state.resource_version_counter
         &&& s.resources()[key].metadata.uid.get_Some_0() < s.kubernetes_api_state.uid_counter
         &&& {
-            if key.kind == ConfigMapView::kind() { 
-                &&& ConfigMapView::unmarshal(s.resources()[key]).is_Ok() 
-                &&& ConfigMapView::unmarshal(s.resources()[key]).get_Ok_0().state_validation()
-            }
-            else if key.kind == DaemonSetView::kind() { 
-                &&& DaemonSetView::unmarshal(s.resources()[key]).is_Ok() 
-                &&& DaemonSetView::unmarshal(s.resources()[key]).get_Ok_0().state_validation()
-            }
-            else if key.kind == PersistentVolumeClaimView::kind() { 
-                &&& PersistentVolumeClaimView::unmarshal(s.resources()[key]).is_Ok() 
-                &&& PersistentVolumeClaimView::unmarshal(s.resources()[key]).get_Ok_0().state_validation()
-            }
-            else if key.kind == PodView::kind() { 
-                &&& PodView::unmarshal(s.resources()[key]).is_Ok() 
-                &&& PodView::unmarshal(s.resources()[key]).get_Ok_0().state_validation()
-            }
-            else if key.kind == RoleBindingView::kind() { 
-                &&& RoleBindingView::unmarshal(s.resources()[key]).is_Ok() 
-                &&& RoleBindingView::unmarshal(s.resources()[key]).get_Ok_0().state_validation()
-            }
-            else if key.kind == RoleView::kind() { 
-                &&& RoleView::unmarshal(s.resources()[key]).is_Ok() 
-                &&& RoleView::unmarshal(s.resources()[key]).get_Ok_0().state_validation()
-            }
-            else if key.kind == SecretView::kind() { 
-                &&& SecretView::unmarshal(s.resources()[key]).is_Ok()
-                &&& SecretView::unmarshal(s.resources()[key]).get_Ok_0().state_validation()
-            }
-            else if key.kind == ServiceView::kind() { 
-                &&& ServiceView::unmarshal(s.resources()[key]).is_Ok() 
-                &&& ServiceView::unmarshal(s.resources()[key]).get_Ok_0().state_validation()
-            }
-            else if key.kind == StatefulSetView::kind() { 
-                &&& StatefulSetView::unmarshal(s.resources()[key]).is_Ok() 
-                &&& StatefulSetView::unmarshal(s.resources()[key]).get_Ok_0().state_validation()
-            }
-            else if key.kind == ServiceAccountView::kind() { 
-                &&& ServiceAccountView::unmarshal(s.resources()[key]).is_Ok() 
-                &&& ServiceAccountView::unmarshal(s.resources()[key]).get_Ok_0().state_validation()
-            }
-            else if key.kind == K::kind() { 
-                &&& K::unmarshal(s.resources()[key]).is_Ok() 
-            }
+            if key.kind == ConfigMapView::kind() { ConfigMapView::unmarshal(s.resources()[key]).is_Ok() }
+            else if key.kind == DaemonSetView::kind() { DaemonSetView::unmarshal(s.resources()[key]).is_Ok() }
+            else if key.kind == PersistentVolumeClaimView::kind() { PersistentVolumeClaimView::unmarshal(s.resources()[key]).is_Ok() }
+            else if key.kind == PodView::kind() { PodView::unmarshal(s.resources()[key]).is_Ok() }
+            else if key.kind == RoleBindingView::kind() { RoleBindingView::unmarshal(s.resources()[key]).is_Ok() }
+            else if key.kind == RoleView::kind() { RoleView::unmarshal(s.resources()[key]).is_Ok() }
+            else if key.kind == SecretView::kind() { SecretView::unmarshal(s.resources()[key]).is_Ok() }
+            else if key.kind == ServiceView::kind() { ServiceView::unmarshal(s.resources()[key]).is_Ok() }
+            else if key.kind == StatefulSetView::kind() { StatefulSetView::unmarshal(s.resources()[key]).is_Ok() }
+            else if key.kind == ServiceAccountView::kind() { ServiceAccountView::unmarshal(s.resources()[key]).is_Ok() }
+            else if key.kind == K::kind() { K::unmarshal(s.resources()[key]).is_Ok() }
             else { true }
         }
     }