From 15d1412b9092368903849330faa9fd3dfdb82812 Mon Sep 17 00:00:00 2001
From: catoverflow <55503205+Catoverflow@users.noreply.github.com>
Date: Mon, 13 Jan 2025 15:58:42 -0600
Subject: [PATCH 1/2] support for deletion timestamp added, tests failed

---
 .../vreplicaset_controller/exec/reconciler.rs |  7 ++
 .../model/reconciler.rs                       | 90 ++++++++++---------
 .../proof/helper_invariants/predicate.rs      |  8 ++
 .../proof/liveness/resource_match.rs          |  5 +-
 4 files changed, 68 insertions(+), 42 deletions(-)

diff --git a/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs b/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs
index 31c96408..4188a266 100644
--- a/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs
+++ b/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs
@@ -120,6 +120,13 @@ pub fn reconcile_core(v_replica_set: &VReplicaSet, resp_o: Option<Response<VoidE
             if pods_or_none.is_none() {
                 return (error_state(state), None);
             }
+            if v_replica_set.metadata().has_deletion_timestamp() {
+                let state_prime = VReplicaSetReconcileState {
+                    reconcile_step: VReplicaSetReconcileStep::Done,
+                    ..state
+                };
+                return (state_prime, None);
+            }
             let pods = pods_or_none.unwrap();
             let filtered_pods = filter_pods(pods, v_replica_set);
             let replicas = v_replica_set.spec().replicas().unwrap_or(0);
diff --git a/src/v2/controllers/vreplicaset_controller/model/reconciler.rs b/src/v2/controllers/vreplicaset_controller/model/reconciler.rs
index 059be698..54a4ff71 100644
--- a/src/v2/controllers/vreplicaset_controller/model/reconciler.rs
+++ b/src/v2/controllers/vreplicaset_controller/model/reconciler.rs
@@ -77,53 +77,61 @@ pub open spec fn reconcile_core(v_replica_set: VReplicaSetView, resp_o: Option<R
                     (error_state(state), None)
                 } else {
                     let pods = pods_or_none.unwrap();
-                    let filtered_pods = filter_pods(pods, v_replica_set);
-                    let replicas = v_replica_set.spec.replicas.unwrap_or(0);
-                    if replicas < 0 {
-                        (error_state(state), None)
-                    } else {
-                        let desired_replicas: usize = replicas as usize;
-                        if filtered_pods.len() == desired_replicas {
-                            let state_prime = VReplicaSetReconcileState {
-                                reconcile_step: VReplicaSetReconcileStep::Done,
-                                ..state
-                            };
-                            (state_prime, None)
-                        } else if filtered_pods.len() < desired_replicas {
-                            let diff =  desired_replicas - filtered_pods.len();
-                            let pod = make_pod(v_replica_set);
-                            let req = APIRequest::CreateRequest(CreateRequest {
-                                namespace: namespace,
-                                obj: pod.marshal(),
-                            });
-                            let state_prime = VReplicaSetReconcileState {
-                                reconcile_step: VReplicaSetReconcileStep::AfterCreatePod((diff - 1) as usize),
-                                ..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 filtered_pods = filter_pods(pods, v_replica_set);
+                        let replicas = v_replica_set.spec.replicas.unwrap_or(0);
+                        if replicas < 0 {
+                            (error_state(state), None)
                         } else {
-                            let diff = filtered_pods.len() - desired_replicas;
-                            let pod_name_or_none = filtered_pods[diff - 1].metadata.name;
-                            if pod_name_or_none.is_none() {
-                                (error_state(state), None)
-                            } else {
-                                let req = APIRequest::DeleteRequest(DeleteRequest {
-                                    key: ObjectRef {
-                                        kind: PodView::kind(),
-                                        name: pod_name_or_none.unwrap(),
-                                        namespace: namespace,
-                                    },
-                                    preconditions: Some(PreconditionsView {
-                                        uid: None,
-                                        resource_version: filtered_pods[diff - 1].metadata.resource_version
-                                    }),
+                            let desired_replicas: usize = replicas as usize;
+                            if filtered_pods.len() == desired_replicas {
+                                let state_prime = VReplicaSetReconcileState {
+                                    reconcile_step: VReplicaSetReconcileStep::Done,
+                                    ..state
+                                };
+                                (state_prime, None)
+                            } else if filtered_pods.len() < desired_replicas {
+                                let diff =  desired_replicas - filtered_pods.len();
+                                let pod = make_pod(v_replica_set);
+                                let req = APIRequest::CreateRequest(CreateRequest {
+                                    namespace: namespace,
+                                    obj: pod.marshal(),
                                 });
                                 let state_prime = VReplicaSetReconcileState {
-                                    reconcile_step: VReplicaSetReconcileStep::AfterDeletePod((diff - 1) as usize),
-                                    filtered_pods: Some(filtered_pods),
+                                    reconcile_step: VReplicaSetReconcileStep::AfterCreatePod((diff - 1) as usize),
                                     ..state
                                 };
                                 (state_prime, Some(RequestView::KRequest(req)))
+                            } else {
+                                let diff = filtered_pods.len() - desired_replicas;
+                                let pod_name_or_none = filtered_pods[diff - 1].metadata.name;
+                                if pod_name_or_none.is_none() {
+                                    (error_state(state), None)
+                                } else {
+                                    let req = APIRequest::DeleteRequest(DeleteRequest {
+                                        key: ObjectRef {
+                                            kind: PodView::kind(),
+                                            name: pod_name_or_none.unwrap(),
+                                            namespace: namespace,
+                                        },
+                                        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),
+                                        filtered_pods: Some(filtered_pods),
+                                        ..state
+                                    };
+                                    (state_prime, Some(RequestView::KRequest(req)))
+                                }
                             }
                         }
                     }
diff --git a/src/v2/controllers/vreplicaset_controller/proof/helper_invariants/predicate.rs b/src/v2/controllers/vreplicaset_controller/proof/helper_invariants/predicate.rs
index c412ca57..98189445 100644
--- a/src/v2/controllers/vreplicaset_controller/proof/helper_invariants/predicate.rs
+++ b/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()
+    }
+}
 }
\ No newline at end of file
diff --git a/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs b/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs
index cf0f765e..dfd25cad 100644
--- a/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs
+++ b/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs
@@ -538,6 +538,7 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_send_create_pod_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
@@ -565,7 +566,8 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_send_create_pod_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 {
@@ -985,6 +987,7 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_send_delete_pod_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)))),
         diff > 0,
     ensures
         spec.entails(

From fa24de246fc8abe3b39b79d17bd9069c1f865727 Mon Sep 17 00:00:00 2001
From: catoverflow <55503205+Catoverflow@users.noreply.github.com>
Date: Tue, 14 Jan 2025 17:27:25 -0600
Subject: [PATCH 2/2] move timestamp to init part

---
 .../vreplicaset_controller/exec/reconciler.rs |  14 +--
 .../model/reconciler.rs                       | 116 +++++++++---------
 .../proof/liveness/resource_match.rs          |  10 +-
 3 files changed, 70 insertions(+), 70 deletions(-)

diff --git a/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs b/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs
index 4188a266..abe03245 100644
--- a/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs
+++ b/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,
@@ -120,13 +127,6 @@ pub fn reconcile_core(v_replica_set: &VReplicaSet, resp_o: Option<Response<VoidE
             if pods_or_none.is_none() {
                 return (error_state(state), None);
             }
-            if v_replica_set.metadata().has_deletion_timestamp() {
-                let state_prime = VReplicaSetReconcileState {
-                    reconcile_step: VReplicaSetReconcileStep::Done,
-                    ..state
-                };
-                return (state_prime, None);
-            }
             let pods = pods_or_none.unwrap();
             let filtered_pods = filter_pods(pods, v_replica_set);
             let replicas = v_replica_set.spec().replicas().unwrap_or(0);
diff --git a/src/v2/controllers/vreplicaset_controller/model/reconciler.rs b/src/v2/controllers/vreplicaset_controller/model/reconciler.rs
index 54a4ff71..873a2813 100644
--- a/src/v2/controllers/vreplicaset_controller/model/reconciler.rs
+++ b/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()
@@ -77,61 +85,53 @@ pub open spec fn reconcile_core(v_replica_set: VReplicaSetView, resp_o: Option<R
                     (error_state(state), None)
                 } else {
                     let pods = pods_or_none.unwrap();
-                    if v_replica_set.metadata.deletion_timestamp.is_some() {
-                        let state_prime = VReplicaSetReconcileState {
-                            reconcile_step: VReplicaSetReconcileStep::Done,
-                            ..state
-                        };
-                        (state_prime, None)
-                    }  else {
-                        let filtered_pods = filter_pods(pods, v_replica_set);
-                        let replicas = v_replica_set.spec.replicas.unwrap_or(0);
-                        if replicas < 0 {
-                            (error_state(state), None)
+                    let filtered_pods = filter_pods(pods, v_replica_set);
+                    let replicas = v_replica_set.spec.replicas.unwrap_or(0);
+                    if replicas < 0 {
+                        (error_state(state), None)
+                    } else {
+                        let desired_replicas: usize = replicas as usize;
+                        if filtered_pods.len() == desired_replicas {
+                            let state_prime = VReplicaSetReconcileState {
+                                reconcile_step: VReplicaSetReconcileStep::Done,
+                                ..state
+                            };
+                            (state_prime, None)
+                        } else if filtered_pods.len() < desired_replicas {
+                            let diff =  desired_replicas - filtered_pods.len();
+                            let pod = make_pod(v_replica_set);
+                            let req = APIRequest::CreateRequest(CreateRequest {
+                                namespace: namespace,
+                                obj: pod.marshal(),
+                            });
+                            let state_prime = VReplicaSetReconcileState {
+                                reconcile_step: VReplicaSetReconcileStep::AfterCreatePod((diff - 1) as usize),
+                                ..state
+                            };
+                            (state_prime, Some(RequestView::KRequest(req)))
                         } else {
-                            let desired_replicas: usize = replicas as usize;
-                            if filtered_pods.len() == desired_replicas {
-                                let state_prime = VReplicaSetReconcileState {
-                                    reconcile_step: VReplicaSetReconcileStep::Done,
-                                    ..state
-                                };
-                                (state_prime, None)
-                            } else if filtered_pods.len() < desired_replicas {
-                                let diff =  desired_replicas - filtered_pods.len();
-                                let pod = make_pod(v_replica_set);
-                                let req = APIRequest::CreateRequest(CreateRequest {
-                                    namespace: namespace,
-                                    obj: pod.marshal(),
+                            let diff = filtered_pods.len() - desired_replicas;
+                            let pod_name_or_none = filtered_pods[diff - 1].metadata.name;
+                            if pod_name_or_none.is_none() {
+                                (error_state(state), None)
+                            } else {
+                                let req = APIRequest::DeleteRequest(DeleteRequest {
+                                    key: ObjectRef {
+                                        kind: PodView::kind(),
+                                        name: pod_name_or_none.unwrap(),
+                                        namespace: namespace,
+                                    },
+                                    preconditions: Some(PreconditionsView {
+                                        uid: None,
+                                        resource_version: filtered_pods[diff - 1].metadata.resource_version
+                                    }),
                                 });
                                 let state_prime = VReplicaSetReconcileState {
-                                    reconcile_step: VReplicaSetReconcileStep::AfterCreatePod((diff - 1) as usize),
+                                    reconcile_step: VReplicaSetReconcileStep::AfterDeletePod((diff - 1) as usize),
+                                    filtered_pods: Some(filtered_pods),
                                     ..state
                                 };
                                 (state_prime, Some(RequestView::KRequest(req)))
-                            } else {
-                                let diff = filtered_pods.len() - desired_replicas;
-                                let pod_name_or_none = filtered_pods[diff - 1].metadata.name;
-                                if pod_name_or_none.is_none() {
-                                    (error_state(state), None)
-                                } else {
-                                    let req = APIRequest::DeleteRequest(DeleteRequest {
-                                        key: ObjectRef {
-                                            kind: PodView::kind(),
-                                            name: pod_name_or_none.unwrap(),
-                                            namespace: namespace,
-                                        },
-                                        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),
-                                        filtered_pods: Some(filtered_pods),
-                                        ..state
-                                    };
-                                    (state_prime, Some(RequestView::KRequest(req)))
-                                }
                             }
                         }
                     }
diff --git a/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs b/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs
index dfd25cad..28d28a16 100644
--- a/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs
+++ b/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 {
@@ -538,7 +541,6 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_send_create_pod_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
@@ -566,8 +568,7 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_send_create_pod_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::vrs_does_not_have_deletion_timestamp(vrs))
+        lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id))
     );
 
     assert forall |s, s_prime| pre(s) && #[trigger] stronger_next(s, s_prime) implies pre(s_prime) || post(s_prime) by {
@@ -987,7 +988,6 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_send_delete_pod_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)))),
         diff > 0,
     ensures
         spec.entails(