Add delete precondition to V2 state machine for Verified ReplicaSet (#…

…552) Here I've added the precondition on resource versions to delete requests sent by the model (and the exec) state machines. The conformance proof still goes through. Signed-off-by: Cody Rivera <[email protected]>
anvil-verifier · Oct 2, 2024 · f3fe6d9 · f3fe6d9
1 parent b8f30ad
commit f3fe6d9
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 5 deletions.
diff --git a/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs b/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs
@@ -138,7 +138,11 @@ pub fn reconcile_core(v_replica_set: &VReplicaSet, resp_o: Option<Response<Empty
                     api_resource: Pod::api_resource(),
                     name: pod_name_or_none.unwrap(),
                     namespace: namespace,
-                    preconditions: None,
+                    preconditions: {
+                        let mut pre = Preconditions::default();
+                        pre.set_resource_version_from_object_meta(filtered_pods[diff - 1].metadata());
+                        Some(pre)
+                    },
                 });
                 let state_prime = VReplicaSetReconcileState {
                     reconcile_step: VReplicaSetReconcileStep::AfterDeletePod(diff - 1),
@@ -203,8 +207,13 @@ pub fn reconcile_core(v_replica_set: &VReplicaSet, resp_o: Option<Response<Empty
                     api_resource: Pod::api_resource(),
                     name: pod_name_or_none.unwrap(),
                     namespace: namespace,
-                    // TODO: set the resource version to be the precondition
-                    preconditions: None,
+                    preconditions: {
+                        let mut pre = Preconditions::default();
+                        pre.set_resource_version_from_object_meta(
+                            state.filtered_pods.as_ref().unwrap()[diff - 1].metadata()
+                        );
+                        Some(pre)
+                    },
                 });
                 let state_prime = VReplicaSetReconcileState {
                     reconcile_step: VReplicaSetReconcileStep::AfterDeletePod(diff - 1),

diff --git a/src/v2/controllers/vreplicaset_controller/model/reconciler.rs b/src/v2/controllers/vreplicaset_controller/model/reconciler.rs
@@ -117,7 +117,10 @@ pub open spec fn reconcile_core(
                                         name: pod_name_or_none.unwrap(),
                                         namespace: namespace,
                                     },
-                                    preconditions: None,
+                                    preconditions: Some(PreconditionsView {
+                                        uid: None,
+                                        resource_version: filtered_pods[diff - 1].metadata.resource_version
+                                    }),
                                 });
                                 let state_prime = VReplicaSetReconcileState {
                                     reconcile_step: VReplicaSetReconcileStep::AfterDeletePod((diff - 1) as usize),
@@ -184,7 +187,10 @@ pub open spec fn reconcile_core(
                                 name: pod_name_or_none.unwrap(),
                                 namespace: namespace,
                             },
-                            preconditions: None,
+                            preconditions: Some(PreconditionsView {
+                                uid: None,
+                                resource_version: state.filtered_pods.unwrap()[diff - 1].metadata.resource_version
+                            }),
                         });
                         let state_prime = VReplicaSetReconcileState {
                             reconcile_step: VReplicaSetReconcileStep::AfterDeletePod((diff - 1) as usize),

diff --git a/src/v2/controllers/vreplicaset_controller/trusted/liveness_theorem.rs b/src/v2/controllers/vreplicaset_controller/trusted/liveness_theorem.rs
@@ -30,6 +30,7 @@ pub open spec fn current_state_matches(vrs: VReplicaSetView) -> StatePred<Cluste
 
 pub open spec fn owned_selector_match_is(vrs: VReplicaSetView, obj: DynamicObjectView) -> bool {
     &&& obj.kind == PodView::kind()
+    &&& obj.metadata.namespace.is_Some()
     &&& obj.metadata.namespace == vrs.metadata.namespace
     &&& obj.metadata.owner_references_contains(vrs.controller_owner_ref())
     &&& vrs.spec.selector.matches(obj.metadata.labels.unwrap_or(Map::empty()))