Prove Delete Lemmas for ReplicaSet in V2 State Machine (#572)

Prove delete WF1 lemmas for ReplicaSet in V2 state machine. --------- Signed-off-by: Cody Rivera <[email protected]>
anvil-verifier · Nov 12, 2024 · 69690ea · 69690ea
1 parent e226ed6
commit 69690ea
Show file tree

Hide file tree

Showing 2 changed files with 476 additions and 31 deletions.
diff --git a/src/v2/controllers/vreplicaset_controller/proof/helper_invariants/predicate.rs b/src/v2/controllers/vreplicaset_controller/proof/helper_invariants/predicate.rs
@@ -209,42 +209,29 @@ pub open spec fn every_delete_matching_pod_request_implies_at_after_delete_pod_s
             &&& s.resources().contains_key(key)
             &&& owned_selector_match_is(vrs, obj)
         } ==> {
+            let content = msg.content;
+            let req = content.get_delete_request();
+            let obj = s.resources()[req.key];
             &&& exists |diff: usize| #[trigger] at_vrs_step_with_vrs(vrs, controller_id, VReplicaSetReconcileStep::AfterDeletePod(diff))(s)
             &&& Cluster::pending_req_msg_is(controller_id, s, vrs.object_ref(), msg)
+            // NOTE: We require that the resource version in etcd is
+            // equal to the one carried by the delete request to
+            // exclude the case where another reconcile working on another
+            // vrs object tries to delete the same object.
+            &&& req.preconditions.is_Some()
+            &&& req.preconditions.unwrap().resource_version.is_Some()
+            &&& obj.metadata.uid.is_None()
+            &&& obj.metadata.resource_version.is_Some()
+            &&& obj.metadata.resource_version.unwrap() == 
+                    req.preconditions.unwrap().resource_version.unwrap()
         }
     }
 }
-// //
-// // TODO: Prove this.
-// //
-// // The proof sketch for this invariant is similar to the above.
-// //
-
-// pub open spec fn each_vrs_in_reconcile_implies_filtered_pods_owned_by_vrs_if_in_etcd() -> StatePred<ClusterState> {
-//     |s: ClusterState| {
-//         forall |key: ObjectRef|
-//             #[trigger] s.ongoing_reconciles().contains_key(key)
-//             ==> {
-//                 let state = s.ongoing_reconciles()[key].local_state; 
-//                 let filtered_pods = state.filtered_pods.unwrap();
-//                 &&& s.ongoing_reconciles()[key].triggering_cr.object_ref() == key
-//                 &&& s.ongoing_reconciles()[key].triggering_cr.metadata().well_formed()
-//                 &&& state.filtered_pods.is_Some()
-//                 // Maintained across deletes, 
-//                 // maintained across creates since all new keys with generate_name
-//                 // are unique, maintained across updates since there are
-//                 // no updates.
-//                 &&& forall |i| #![auto] 0 <= i < filtered_pods.len() ==>
-//                     (
-//                         filtered_pods[i].object_ref().namespace == s.ongoing_reconciles()[key].triggering_cr.metadata.namespace.unwrap()
-//                         && (s.resources().contains_key(filtered_pods[i].object_ref()) ==>
-//                             s.resources()[filtered_pods[i].object_ref()].metadata.owner_references_contains(
-//                                 s.ongoing_reconciles()[key].triggering_cr.controller_owner_ref()
-//                             ))
-//                     )
-//             }
-//     }
-// }
+//
+// TODO: Prove this.
+//
+// The proof sketch for this invariant is similar to the above.
+//
 
 pub open spec fn at_after_delete_pod_step_implies_filtered_pods_in_matching_pod_entries(
     vrs: VReplicaSetView, controller_id: int,
@@ -257,6 +244,7 @@ pub open spec fn at_after_delete_pod_step_implies_filtered_pods_in_matching_pod_
             let filtered_pods = state.filtered_pods.unwrap();
             let filtered_pod_keys = filtered_pods.map_values(|p: PodView| p.object_ref());
             &&& s.ongoing_reconciles(controller_id).contains_key(vrs.object_ref())
+            &&& VReplicaSetReconcileState::unmarshal(s.ongoing_reconciles(controller_id)[vrs.object_ref()].local_state).is_ok()
             &&& state.filtered_pods.is_Some()
             &&& diff <= filtered_pod_keys.len()
             &&& filtered_pod_keys.no_duplicates()