From ecd4a44f7784a93aa3f4d3fc17059039378fe065 Mon Sep 17 00:00:00 2001 From: Wenjie Ma Date: Mon, 2 Oct 2023 23:05:25 -0500 Subject: [PATCH] Add labels and annotations to desired state Signed-off-by: Wenjie Ma --- .../spec/resource/default_user_secret.rs | 2 + .../spec/resource/erlang_cookie.rs | 2 + .../spec/resource/headless_service.rs | 2 + .../spec/resource/rabbitmq_plugins.rs | 2 + .../rabbitmq_controller/spec/resource/role.rs | 2 + .../spec/resource/role_binding.rs | 2 + .../spec/resource/service.rs | 2 + .../spec/resource/service_account.rs | 2 + .../spec/resource/stateful_set.rs | 6 ++- .../proof/cluster_safety.rs | 54 ++++--------------- 10 files changed, 31 insertions(+), 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 index 2eb2114ef..ec03ea9e2 100644 --- 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 index 68addaae1..f9e9b99c1 100644 --- 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 index 35d6f8fd7..a3ea8fb39 100644 --- 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 index 84ef29a55..ce1df9544 100644 --- 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 index 17ace2e8c..f8beffc66 100644 --- 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 index 060143b18..d3f66b4cc 100644 --- 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 index 0f34b900f..cd9119e35 100644 --- 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 index efc8a871d..9699750e0 100644 --- 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 index 00bfd4447..21efd05fa 100644 --- 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 index 5cee3925c..96351f95b 100644 --- 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 { &&& 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 } } }