support for deletion timestamp added, tests failed

src/v2/controllers/vreplicaset_controller/exec/reconciler.rs

@@ -99,6 +99,13 @@ pub fn reconcile_core(v_replica_set: &VReplicaSet, resp_o: Option<Response<VoidE
     let namespace = v_replica_set.metadata().namespace().unwrap();
     match &state.reconcile_step {
         VReplicaSetReconcileStep::Init => {
+            if v_replica_set.metadata().has_deletion_timestamp() {
+                let state_prime = VReplicaSetReconcileState {
+                    reconcile_step: VReplicaSetReconcileStep::Done,
+                    ..state
+                };
+                return (state_prime, None);
+            }
             let req = KubeAPIRequest::ListRequest(KubeListRequest {
                 api_resource: Pod::api_resource(),
                 namespace: namespace,

src/v2/controllers/vreplicaset_controller/model/reconciler.rs

@@ -55,15 +55,23 @@ pub open spec fn reconcile_core(v_replica_set: VReplicaSetView, resp_o: Option<R
     let namespace = v_replica_set.metadata.namespace.unwrap();
     match &state.reconcile_step {
         VReplicaSetReconcileStep::Init => {
-            let req = APIRequest::ListRequest(ListRequest {
-                kind: PodView::kind(),
-                namespace: namespace,
-            });
-            let state_prime = VReplicaSetReconcileState {
-                reconcile_step: VReplicaSetReconcileStep::AfterListPods,
-                ..state
-            };
-            (state_prime, Some(RequestView::KRequest(req)))
+            if v_replica_set.metadata.deletion_timestamp.is_some() {
+                let state_prime = VReplicaSetReconcileState {
+                    reconcile_step: VReplicaSetReconcileStep::Done,
+                    ..state
+                };
+                (state_prime, None)
+            } else {
+                let req = APIRequest::ListRequest(ListRequest {
+                    kind: PodView::kind(),
+                    namespace: namespace,
+                });
+                let state_prime = VReplicaSetReconcileState {
+                    reconcile_step: VReplicaSetReconcileStep::AfterListPods,
+                    ..state
+                };
+                (state_prime, Some(RequestView::KRequest(req)))
+            }
         },
         VReplicaSetReconcileStep::AfterListPods => {
             if !(resp_o.is_Some() && resp_o.get_Some_0().is_KResponse()

src/v2/controllers/vreplicaset_controller/proof/helper_invariants/predicate.rs

@@ -334,4 +334,12 @@ pub open spec fn every_delete_request_from_vrs_has_rv_precondition_that_is_less_
 // Every delete request must be on an object with a resource version less than the resource version counter.
 //
 
+pub open spec fn vrs_does_not_have_deletion_timestamp (
+    vrs: VReplicaSetView
+) -> StatePred<ClusterState> {
+    |s: ClusterState| {
+        let vrs_obj = s.resources()[vrs.object_ref()];
+        vrs_obj.metadata.deletion_timestamp.is_None()
+    }
+}
 }

src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs

@@ -49,6 +49,7 @@ pub proof fn lemma_from_init_step_to_send_list_pods_req(
         spec.entails(always(lift_state(helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)))),
         spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, controller_id)))),
         spec.entails(always(lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)))),
+        spec.entails(always(lift_state(helper_invariants::vrs_does_not_have_deletion_timestamp(vrs)))),
     ensures
         spec.entails(
             lift_state(
@@ -94,6 +95,7 @@ pub proof fn lemma_from_init_step_to_send_list_pods_req(
         &&& helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)(s)
         &&& helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, controller_id)(s)
         &&& helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)(s)
+        &&& helper_invariants::vrs_does_not_have_deletion_timestamp(vrs)(s)
     };
     helper_lemmas::vrs_non_interference_property_equivalent_to_lifted_vrs_non_interference_property(
         spec, cluster, controller_id
@@ -117,7 +119,8 @@ pub proof fn lemma_from_init_step_to_send_list_pods_req(
         lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()),
         lift_state(helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)),
         lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, controller_id)),
-        lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id))
+        lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)),
+        lift_state(helper_invariants::vrs_does_not_have_deletion_timestamp(vrs))
     );
 
     assert forall |s, s_prime| pre(s) && #[trigger] stronger_next(s, s_prime) implies pre(s_prime) || post(s_prime) by {