Finally prove delete lemma again

Signed-off-by: Cody Rivera <[email protected]>

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

@@ -223,6 +223,54 @@ pub open spec fn every_delete_matching_pod_request_implies_at_after_delete_pod_s
     }
 }
 
+pub open spec fn each_vrs_in_reconcile_implies_filtered_pods_owned_by_vrs(controller_id: int) -> StatePred<ClusterState> {
+    |s: ClusterState| {
+        forall |key: ObjectRef|
+            #[trigger] s.ongoing_reconciles(controller_id).contains_key(key)
+            ==> {
+                let state = VReplicaSetReconcileState::unmarshal(s.ongoing_reconciles(controller_id)[key].local_state).unwrap();
+                let triggering_cr = VReplicaSetView::unmarshal(s.ongoing_reconciles(controller_id)[key].triggering_cr).unwrap();
+                let filtered_pods = state.filtered_pods.unwrap();
+                &&& triggering_cr.object_ref() == 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 == 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(
+                                triggering_cr.controller_owner_ref()
+                            ))
+                    )
+                // Special case: the above property holds on a list response to the
+                // appropriate request. 
+                &&& forall |msg| {
+                        let req_msg = s.ongoing_reconciles(controller_id)[triggering_cr.object_ref()].pending_req_msg.get_Some_0();
+                        &&& #[trigger] s.in_flight().contains(msg)
+                        &&& s.ongoing_reconciles(controller_id)[triggering_cr.object_ref()].pending_req_msg.is_Some()
+                        &&& resp_msg_matches_req_msg(msg, req_msg)
+                        &&& msg.content.is_list_response()
+                    } ==> {
+                        let resp_objs = msg.content.get_list_response().res.unwrap();
+                        &&& msg.content.get_list_response().res.is_Ok()
+                        &&& resp_objs.filter(|o: DynamicObjectView| PodView::unmarshal(o).is_err()).len() != 0 
+                        &&& forall |i| #![auto] 0 <= i < resp_objs.len() ==>
+                        (
+                            resp_objs[i].object_ref().namespace == triggering_cr.metadata.namespace.unwrap()
+                            && (s.resources().contains_key(resp_objs[i].object_ref()) ==>
+                                    s.resources()[resp_objs[i].object_ref()].metadata
+                                        == resp_objs[i].metadata
+                                )
+                        )
+                    }
+            }
+    }
+}
+
 pub open spec fn at_after_delete_pod_step_implies_filtered_pods_in_matching_pod_entries(
     vrs: VReplicaSetView, controller_id: int,
 ) -> StatePred<ClusterState> {
@@ -258,4 +306,32 @@ pub open spec fn at_after_delete_pod_step_implies_filtered_pods_in_matching_pod_
 // on other invariants.
 //
 
+pub open spec fn every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(
+    vrs: VReplicaSetView, controller_id: int,
+) -> StatePred<ClusterState> {
+    |s: ClusterState| {
+        forall |msg: Message| #![trigger s.in_flight().contains(msg)] {
+            let content = msg.content;
+            let req = content.get_delete_request();
+            &&& s.in_flight().contains(msg)
+            &&& msg.src.is_Controller()
+            &&& msg.src.get_Controller_0() == controller_id
+            &&& msg.content.is_APIRequest()
+            &&& content.is_delete_request()
+        } ==> {
+            let content = msg.content;
+            let req = content.get_delete_request();
+            &&& req.preconditions.is_Some()
+            &&& req.preconditions.unwrap().resource_version.is_Some()
+            &&& req.preconditions.unwrap().uid.is_None()
+            &&& req.preconditions.unwrap().resource_version.unwrap() < s.api_server.resource_version_counter
+        }
+    }
+}
+//
+// TODO: Prove this.
+//
+// Every delete request must be on an object with a resource version less than the resource version counter.
+//
+
 }

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

@@ -13,6 +13,7 @@ use crate::vreplicaset_controller::{
     trusted::{liveness_theorem::*, spec_types::*, step::*},
     proof::{predicate::*, helper_lemmas, helper_invariants::{predicate::*}},
 };
+use crate::vstd_ext::seq_lib::*;
 use vstd::prelude::*;
 
 verus!{
@@ -194,8 +195,6 @@ pub proof fn lemma_eventually_always_every_create_matching_pod_request_implies_a
 
                     assert(requirements(msg, s_prime));
                 } else {
-                    // This seems not to be needed in the analogous delete proof???
-                    // but I don't want to remove it yet.
                     let step = choose |step| cluster.next_step(s, s_prime, step);
                     let cr_key = step.get_ControllerStep_0().2.get_Some_0();
                     let local_step = VReplicaSetReconcileState::unmarshal(s.ongoing_reconciles(controller_id)[cr_key].local_state).unwrap().reconcile_step;
@@ -256,11 +255,15 @@ pub proof fn lemma_eventually_always_every_delete_matching_pod_request_implies_a
         spec.entails(always(lift_state(cluster.each_builtin_object_in_etcd_is_well_formed()))),
         spec.entails(always(lift_state(cluster.each_object_in_etcd_is_well_formed::<VReplicaSetView>()))),
         spec.entails(always(lift_state(cluster.every_in_flight_req_msg_from_controller_has_valid_controller_id()))),
+        spec.entails(always(lift_state(Cluster::each_object_in_etcd_has_at_most_one_controller_owner()))),
+        spec.entails(always(lift_state(Cluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata(controller_id)))),
+        spec.entails(always(lift_state(Cluster::the_object_in_reconcile_has_spec_and_uid_as::<VReplicaSetView>(controller_id, vrs)))),
         forall |other_id| cluster.controller_models.remove(controller_id).contains_key(other_id)
             ==> spec.entails(always(lift_state(#[trigger] vrs_not_interfered_by(other_id)))),
-        //spec.entails(always(lift_state(each_vrs_in_reconcile_implies_filtered_pods_owned_by_vrs_if_in_etcd()))),
         spec.entails(always(lift_state(no_pending_update_or_update_status_request_on_pods()))),
         spec.entails(always(lift_state(every_create_request_is_well_formed(cluster, controller_id)))),
+        spec.entails(always(lift_state(every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)))),
+        spec.entails(always(lift_state(each_vrs_in_reconcile_implies_filtered_pods_owned_by_vrs(controller_id)))),
     ensures spec.entails(true_pred().leads_to(always(lift_state(every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id))))),
 {
     let key = vrs.object_ref();
@@ -280,7 +283,7 @@ pub proof fn lemma_eventually_always_every_delete_matching_pod_request_implies_a
             // Delete precondition clauses.
             &&& req.preconditions.is_Some()
             &&& req.preconditions.unwrap().resource_version.is_Some()
-            &&& obj.metadata.uid.is_None()
+            &&& req.preconditions.unwrap().uid.is_None()
             &&& obj.metadata.resource_version.is_Some()
             &&& obj.metadata.resource_version.unwrap() == req_rv
         } ==> {
@@ -308,7 +311,7 @@ pub proof fn lemma_eventually_always_every_delete_matching_pod_request_implies_a
         // Delete precondition clauses.
         &&& req.preconditions.is_Some()
         &&& req.preconditions.unwrap().resource_version.is_Some()
-        &&& obj.metadata.uid.is_None()
+        &&& req.preconditions.unwrap().uid.is_None()
         &&& obj.metadata.resource_version.is_Some()
         &&& obj.metadata.resource_version.unwrap() == req_rv
     };
@@ -326,18 +329,24 @@ pub proof fn lemma_eventually_always_every_delete_matching_pod_request_implies_a
         &&& cluster.each_builtin_object_in_etcd_is_well_formed()(s)
         &&& cluster.each_object_in_etcd_is_well_formed::<VReplicaSetView>()(s)
         &&& cluster.every_in_flight_req_msg_from_controller_has_valid_controller_id()(s)
+        &&& Cluster::each_object_in_etcd_has_at_most_one_controller_owner()(s)
+        &&& Cluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata(controller_id)(s)
+        &&& Cluster::the_object_in_reconcile_has_spec_and_uid_as::<VReplicaSetView>(controller_id, vrs)(s)
         &&& forall |other_id| cluster.controller_models.remove(controller_id).contains_key(other_id)
                 ==> #[trigger] vrs_not_interfered_by(other_id)(s)
         &&& forall |other_id| cluster.controller_models.remove(controller_id).contains_key(other_id)
                 ==> #[trigger] vrs_not_interfered_by(other_id)(s_prime)
         &&& no_pending_update_or_update_status_request_on_pods()(s)
         &&& every_create_request_is_well_formed(cluster, controller_id)(s)
+        &&& every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)(s)
+        &&& each_vrs_in_reconcile_implies_filtered_pods_owned_by_vrs(controller_id)(s)
     };
 
     assert forall |s: ClusterState, s_prime: ClusterState| #[trigger]  #[trigger] stronger_next(s, s_prime) implies Cluster::every_new_req_msg_if_in_flight_then_satisfies(requirements)(s, s_prime) by {
         assert forall |msg: Message| (!s.in_flight().contains(msg) || requirements(msg, s)) && #[trigger] s_prime.in_flight().contains(msg)
         implies requirements(msg, s_prime) by {
             VReplicaSetReconcileState::marshal_preserves_integrity();
+            VReplicaSetView::marshal_preserves_integrity();
             if requirements_antecedent(msg, s) {
                 if s.in_flight().contains(msg) {
                     assert(requirements(msg, s));
@@ -348,6 +357,73 @@ pub proof fn lemma_eventually_always_every_delete_matching_pod_request_implies_a
                         || at_vrs_step_with_vrs(vrs, controller_id, VReplicaSetReconcileStep::AfterDeletePod((diff + 1) as usize))(s_prime));
 
                     assert(requirements(msg, s_prime));
+                } else {
+                    let content = msg.content;
+                    let request_key = content.get_delete_request().key;
+                    let obj = s.resources()[content.get_delete_request().key];
+
+                    let step = choose |step| cluster.next_step(s, s_prime, step);
+                    let cr_key = step.get_ControllerStep_0().2.get_Some_0();
+                    let local_step = VReplicaSetReconcileState::unmarshal(s.ongoing_reconciles(controller_id)[cr_key].local_state).unwrap().reconcile_step;
+                    let local_step_prime = VReplicaSetReconcileState::unmarshal(s_prime.ongoing_reconciles(controller_id)[cr_key].local_state).unwrap().reconcile_step;
+                    let new_diff = local_step_prime.get_AfterDeletePod_0();
+
+                    let triggering_cr = VReplicaSetView::unmarshal(s.ongoing_reconciles(controller_id)[cr_key].triggering_cr).unwrap();
+
+                    if local_step.is_AfterListPods() {
+                        let cr_msg = step.get_ControllerStep_0().1.get_Some_0();
+                        let req_msg = s.ongoing_reconciles(controller_id)[cr_key].pending_req_msg.get_Some_0();
+                        let objs = cr_msg.content.get_list_response().res.unwrap();
+                        let triggering_cr = VReplicaSetView::unmarshal(s.ongoing_reconciles(controller_id)[cr_key].triggering_cr).unwrap();
+                        let desired_replicas: usize = triggering_cr.spec.replicas.unwrap_or(0) as usize;
+                        let pods_or_none = objects_to_pods(objs);
+                        let pods = pods_or_none.unwrap();
+                        let filtered_pods = filter_pods(pods, triggering_cr);
+                        let diff = filtered_pods.len() - desired_replicas;
+                        seq_filter_contains_implies_seq_contains(
+                            pods,
+                            |pod: PodView|
+                            pod.metadata.owner_references_contains(triggering_cr.controller_owner_ref())
+                            && triggering_cr.spec.selector.matches(pod.metadata.labels.unwrap_or(Map::empty()))
+                            && pod.metadata.deletion_timestamp.is_None(),
+                            filtered_pods[diff - 1]
+                        );
+
+                        let idx1 = choose |i| pods[i] == filtered_pods[diff - 1];
+                        assert(pods[idx1] == filtered_pods[diff - 1]);
+                        assert(pods[idx1] == PodView::unmarshal(objs[idx1]).unwrap());
+                        assert(filtered_pods[diff - 1].object_ref() == request_key);
+                    }
+
+                    let controller_owners = obj.metadata.owner_references.unwrap().filter(
+                        |o: OwnerReferenceView| o.controller.is_Some() && o.controller.get_Some_0()
+                    );
+                    assert(controller_owners.contains(
+                        VReplicaSetView::unmarshal(s.ongoing_reconciles(controller_id)[cr_key].triggering_cr)
+                            .unwrap().controller_owner_ref()
+                    ));
+                    assert(controller_owners.contains(vrs.controller_owner_ref()));
+                    assert(cr_key.name == key.name);
+
+                    assert(at_vrs_step_with_vrs(vrs, controller_id, VReplicaSetReconcileStep::AfterDeletePod(new_diff))(s_prime));
+                    assert(requirements(msg, s_prime));
+                }
+            } else {
+                if s.in_flight().contains(msg) {
+                    assert(!requirements_antecedent(msg, s));
+                    let content = msg.content;
+                    let req = content.get_delete_request();
+                    let key = req.key;
+                    let obj = s.resources()[key];
+
+                    let step = choose |step| cluster.next_step(s, s_prime, step);
+                    match step {
+                        Step::APIServerStep(input) => {
+                            // Invariant every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter
+                            // is essential here.
+                        },
+                        _ => {}
+                    }
                 }
             }
         }
@@ -356,10 +432,6 @@ pub proof fn lemma_eventually_always_every_delete_matching_pod_request_implies_a
     helper_lemmas::vrs_non_interference_property_equivalent_to_lifted_vrs_non_interference_property_action(
         spec, cluster, controller_id
     );
-    let valid_controller_id_action = |s, s_prime| {
-        cluster.every_in_flight_req_msg_from_controller_has_valid_controller_id()(s) &&
-        cluster.every_in_flight_req_msg_from_controller_has_valid_controller_id()(s_prime)
-    };
     invariant_n!(
         spec, lift_action(stronger_next),
         lift_action(Cluster::every_new_req_msg_if_in_flight_then_satisfies(requirements)),
@@ -375,9 +447,14 @@ pub proof fn lemma_eventually_always_every_delete_matching_pod_request_implies_a
         lift_state(cluster.each_builtin_object_in_etcd_is_well_formed()),
         lift_state(cluster.each_object_in_etcd_is_well_formed::<VReplicaSetView>()),
         lift_state(cluster.every_in_flight_req_msg_from_controller_has_valid_controller_id()),
+        lift_state(Cluster::each_object_in_etcd_has_at_most_one_controller_owner()),
+        lift_state(Cluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata(controller_id)),
+        lift_state(Cluster::the_object_in_reconcile_has_spec_and_uid_as::<VReplicaSetView>(controller_id, vrs)),
         lifted_vrs_non_interference_property_action(cluster, controller_id),
         lift_state(no_pending_update_or_update_status_request_on_pods()),
-        lift_state(every_create_request_is_well_formed(cluster, controller_id))
+        lift_state(every_create_request_is_well_formed(cluster, controller_id)),
+        lift_state(every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)),
+        lift_state(each_vrs_in_reconcile_implies_filtered_pods_owned_by_vrs(controller_id))
     );
 
     cluster.lemma_true_leads_to_always_every_in_flight_req_msg_satisfies(spec, requirements);

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

@@ -31,6 +31,7 @@ pub proof fn lemma_api_request_outside_create_or_delete_loop_maintains_matching_
         helper_invariants::every_create_request_is_well_formed(cluster, controller_id)(s),
         helper_invariants::no_pending_update_or_update_status_request_on_pods()(s),
         helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()(s),
+        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),
         forall |diff: usize| !(#[trigger] at_vrs_step_with_vrs(vrs, controller_id, VReplicaSetReconcileStep::AfterCreatePod(diff))(s)),
@@ -98,6 +99,7 @@ pub proof fn lemma_api_request_not_made_by_vrs_maintains_matching_pods(
         helper_invariants::every_create_request_is_well_formed(cluster, controller_id)(s),
         helper_invariants::no_pending_update_or_update_status_request_on_pods()(s),
         helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()(s),
+        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),
         forall |other_id| cluster.controller_models.remove(controller_id).contains_key(other_id)