Require there is only one controller owner reference

Signed-off-by: Xudong Sun <[email protected]>
anvil-verifier · Aug 22, 2023 · 33620b6 · 33620b6
1 parent fa6e972
commit 33620b6
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 0 deletions.
diff --git a/src/kubernetes_api_objects/owner_reference.rs b/src/kubernetes_api_objects/owner_reference.rs
@@ -52,6 +52,13 @@ pub struct OwnerReferenceView {
     pub uid: nat,
 }
 
+impl OwnerReferenceView {
+    pub open spec fn is_controller_ref(self) -> bool {
+        self.controller.is_Some()
+        && self.controller.get_Some_0()
+    }
+}
+
 pub open spec fn owner_reference_to_object_reference(owner_reference: OwnerReferenceView, namespace: StringView) -> ObjectRef {
     ObjectRef {
         kind: owner_reference.kind,

diff --git a/src/kubernetes_cluster/spec/kubernetes_api/state_machine.rs b/src/kubernetes_cluster/spec/kubernetes_api/state_machine.rs
@@ -223,6 +223,17 @@ pub open spec fn validate_update_request(req: UpdateRequest, s: KubernetesAPISta
         // Update fails because the object has a wrong uid
         // TODO: double check the Error type
         Some(APIError::InternalError)
+    } else if req.obj.metadata.owner_references.is_Some()
+        && req.obj.metadata.owner_references.get_Some_0().len() > 1
+        && exists |i, j| #![auto] (
+            i != j
+            && 0 <= i < req.obj.metadata.owner_references.get_Some_0().len()
+            && 0 <= j < req.obj.metadata.owner_references.get_Some_0().len()
+            && req.obj.metadata.owner_references.get_Some_0()[i].is_controller_ref()
+            && req.obj.metadata.owner_references.get_Some_0()[j].is_controller_ref()
+        ) {
+        // Update fails because the object has multiple controller owner references
+        Some(APIError::Invalid)
     } else if req.obj.kind == K::kind() && !(
         K::rule(K::from_dynamic_object(req.obj).get_Ok_0())
         && K::transition_rule(K::from_dynamic_object(req.obj).get_Ok_0(), K::from_dynamic_object(s.resources[req.key]).get_Ok_0())