From 259ff8f8a630cacca98a7ecb5e1af833c5c0ec21 Mon Sep 17 00:00:00 2001 From: Cody Rivera Date: Wed, 11 Dec 2024 17:42:21 -0600 Subject: [PATCH] Finally prove delete lemma again Signed-off-by: Cody Rivera --- .../proof/helper_invariants/predicate.rs | 76 +++++++++++++++ .../proof/helper_invariants/proof.rs | 97 +++++++++++++++++-- .../proof/liveness/api_actions.rs | 2 + .../proof/liveness/resource_match.rs | 23 ++++- .../proof/controller_runtime_liveness.rs | 2 + .../proof/objects_in_store.rs | 16 +++ src/vstd_ext/seq_lib.rs | 10 ++ 7 files changed, 215 insertions(+), 11 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 index fb0b215d..c412ca57 100644 --- a/src/v2/controllers/vreplicaset_controller/proof/helper_invariants/predicate.rs +++ b/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 { + |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 { @@ -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 { + |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. +// + } \ No newline at end of file diff --git a/src/v2/controllers/vreplicaset_controller/proof/helper_invariants/proof.rs b/src/v2/controllers/vreplicaset_controller/proof/helper_invariants/proof.rs index dfd8b054..114ce8b2 100644 --- a/src/v2/controllers/vreplicaset_controller/proof/helper_invariants/proof.rs +++ b/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::()))), 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::(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::()(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::(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::()), 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::(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); diff --git a/src/v2/controllers/vreplicaset_controller/proof/liveness/api_actions.rs b/src/v2/controllers/vreplicaset_controller/proof/liveness/api_actions.rs index e03f1574..7b55d33e 100644 --- a/src/v2/controllers/vreplicaset_controller/proof/liveness/api_actions.rs +++ b/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) 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 682536c2..cf0f765e 100644 --- a/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs +++ b/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs @@ -46,6 +46,7 @@ pub proof fn lemma_from_init_step_to_send_list_pods_req( spec.entails(always(lift_state(helper_invariants::every_create_request_is_well_formed(cluster, controller_id)))), spec.entails(always(lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()))), spec.entails(always(lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()))), + 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)))), ensures @@ -90,6 +91,7 @@ pub proof fn lemma_from_init_step_to_send_list_pods_req( &&& 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) }; @@ -113,6 +115,7 @@ pub proof fn lemma_from_init_step_to_send_list_pods_req( lift_state(helper_invariants::every_create_request_is_well_formed(cluster, controller_id)), lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()), 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)) ); @@ -167,8 +170,9 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp( spec.entails(always(lift_state(helper_invariants::every_create_request_is_well_formed(cluster, controller_id)))), spec.entails(always(lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()))), spec.entails(always(lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()))), + 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::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)))) ensures spec.entails( lift_state( @@ -212,6 +216,7 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp( &&& 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) }; @@ -236,6 +241,7 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp( lift_state(helper_invariants::every_create_request_is_well_formed(cluster, controller_id)), lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()), 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)) ); @@ -479,6 +485,7 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_send_create_pod_req( spec.entails(always(lift_state(helper_invariants::every_create_request_is_well_formed(cluster, controller_id)))), spec.entails(always(lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()))), spec.entails(always(lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()))), + 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)))), diff < 0, @@ -528,6 +535,7 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_send_create_pod_req( &&& 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) }; @@ -555,6 +563,7 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_send_create_pod_req( lift_state(helper_invariants::every_create_request_is_well_formed(cluster, controller_id)), lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()), 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)) ); @@ -829,6 +838,7 @@ pub proof fn lemma_from_after_receive_ok_resp_to_send_create_pod_req( spec.entails(always(lift_state(helper_invariants::every_create_request_is_well_formed(cluster, controller_id)))), spec.entails(always(lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()))), spec.entails(always(lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()))), + 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)))), @@ -880,6 +890,7 @@ pub proof fn lemma_from_after_receive_ok_resp_to_send_create_pod_req( &&& 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) }; @@ -907,6 +918,7 @@ pub proof fn lemma_from_after_receive_ok_resp_to_send_create_pod_req( lift_state(helper_invariants::every_create_request_is_well_formed(cluster, controller_id)), lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()), 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)) ); @@ -970,6 +982,7 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_send_delete_pod_req( spec.entails(always(lift_state(helper_invariants::every_create_request_is_well_formed(cluster, controller_id)))), spec.entails(always(lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()))), spec.entails(always(lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()))), + 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)))), diff > 0, @@ -1019,6 +1032,7 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_send_delete_pod_req( &&& 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) }; @@ -1046,6 +1060,7 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_send_delete_pod_req( lift_state(helper_invariants::every_create_request_is_well_formed(cluster, controller_id)), lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()), 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)) ); @@ -1119,6 +1134,7 @@ pub proof fn lemma_from_after_send_delete_pod_req_to_receive_ok_resp( spec.entails(always(lift_state(helper_invariants::every_create_request_is_well_formed(cluster, controller_id)))), spec.entails(always(lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()))), spec.entails(always(lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()))), + 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)))), @@ -1167,6 +1183,7 @@ pub proof fn lemma_from_after_send_delete_pod_req_to_receive_ok_resp( &&& 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) }; @@ -1192,6 +1209,7 @@ pub proof fn lemma_from_after_send_delete_pod_req_to_receive_ok_resp( lift_state(helper_invariants::every_create_request_is_well_formed(cluster, controller_id)), lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()), 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)) ); @@ -1282,6 +1300,7 @@ pub proof fn lemma_from_after_receive_ok_resp_to_send_delete_pod_req( spec.entails(always(lift_state(helper_invariants::every_create_request_is_well_formed(cluster, controller_id)))), spec.entails(always(lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()))), spec.entails(always(lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()))), + 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::at_after_delete_pod_step_implies_filtered_pods_in_matching_pod_entries(vrs, controller_id)))), @@ -1335,6 +1354,7 @@ pub proof fn lemma_from_after_receive_ok_resp_to_send_delete_pod_req( &&& 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) &&& helper_invariants::at_after_delete_pod_step_implies_filtered_pods_in_matching_pod_entries(vrs, controller_id)(s) @@ -1366,6 +1386,7 @@ pub proof fn lemma_from_after_receive_ok_resp_to_send_delete_pod_req( lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()), 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_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)), lift_state(helper_invariants::at_after_delete_pod_step_implies_filtered_pods_in_matching_pod_entries(vrs, controller_id)) ); diff --git a/src/v2/kubernetes_cluster/proof/controller_runtime_liveness.rs b/src/v2/kubernetes_cluster/proof/controller_runtime_liveness.rs index 32ef27ac..f9bf9dbf 100644 --- a/src/v2/kubernetes_cluster/proof/controller_runtime_liveness.rs +++ b/src/v2/kubernetes_cluster/proof/controller_runtime_liveness.rs @@ -592,6 +592,7 @@ pub proof fn lemma_from_pending_req_in_flight_at_some_state_to_in_flight_resp_ma pub open spec fn the_object_in_schedule_has_spec_and_uid_as(controller_id: int, cr: T) -> StatePred { |s: ClusterState| s.scheduled_reconciles(controller_id).contains_key(cr.object_ref()) ==> s.scheduled_reconciles(controller_id)[cr.object_ref()].metadata.uid == cr.metadata().uid + && T::unmarshal(s.scheduled_reconciles(controller_id)[cr.object_ref()]).is_Ok() && T::unmarshal(s.scheduled_reconciles(controller_id)[cr.object_ref()]).get_Ok_0().spec() == cr.spec() } @@ -633,6 +634,7 @@ pub proof fn lemma_true_leads_to_always_the_object_in_schedule_has_spec_and_uid_ pub open spec fn the_object_in_reconcile_has_spec_and_uid_as(controller_id: int, cr: T) -> StatePred { |s: ClusterState| s.ongoing_reconciles(controller_id).contains_key(cr.object_ref()) ==> s.ongoing_reconciles(controller_id)[cr.object_ref()].triggering_cr.metadata.uid == cr.metadata().uid + && T::unmarshal(s.ongoing_reconciles(controller_id)[cr.object_ref()].triggering_cr).is_Ok() && T::unmarshal(s.ongoing_reconciles(controller_id)[cr.object_ref()].triggering_cr).get_Ok_0().spec() == cr.spec() } diff --git a/src/v2/kubernetes_cluster/proof/objects_in_store.rs b/src/v2/kubernetes_cluster/proof/objects_in_store.rs index c2e8d2cb..82d50986 100644 --- a/src/v2/kubernetes_cluster/proof/objects_in_store.rs +++ b/src/v2/kubernetes_cluster/proof/objects_in_store.rs @@ -226,6 +226,22 @@ pub proof fn lemma_always_each_object_in_etcd_is_well_formed(spec, lift_state(p), lift_state(invariant)); } +// TODO: Prove this. +pub open spec fn each_object_in_etcd_has_at_most_one_controller_owner() -> StatePred { + |s: ClusterState| { + forall |key: ObjectRef| + #[trigger] s.resources().contains_key(key) + ==> { + let obj = s.resources()[key]; + let owners = obj.metadata.owner_references.get_Some_0(); + let controller_owners = owners.filter( + |o: OwnerReferenceView| o.controller.is_Some() && o.controller.get_Some_0() + ); + obj.metadata.owner_references.is_Some() ==> controller_owners.len() <= 1 + } + } +} + } } diff --git a/src/vstd_ext/seq_lib.rs b/src/vstd_ext/seq_lib.rs index 2db15dc1..4d0e8935 100644 --- a/src/vstd_ext/seq_lib.rs +++ b/src/vstd_ext/seq_lib.rs @@ -123,4 +123,14 @@ pub proof fn seq_filter_preserves_no_duplicates(s: Seq, pred: spec_fn(A) - // that sequence also has no duplicates. // +#[verifier(external_body)] +pub proof fn seq_filter_contains_implies_seq_contains(s: Seq, pred: spec_fn(A) -> bool, elt: A) + requires s.filter(pred).contains(elt), + ensures s.contains(elt); +// +// TODO: Prove this -- Trivial. +// +// Anything in the +// + }