From 624d788b7e6599716931984bfd3007e237fd8dbc Mon Sep 17 00:00:00 2001 From: Cody Rivera Date: Tue, 29 Oct 2024 14:12:32 -0500 Subject: [PATCH 1/8] Modify Wf1 lemma proofs to support the proof of another lemma Signed-off-by: Cody Rivera --- .../proof/liveness/resource_match.rs | 4 +- .../proof/helper_lemmas.rs | 91 ++++++- .../proof/liveness/resource_match.rs | 246 +++++++++++++++++- .../vreplicaset_controller/proof/predicate.rs | 2 + src/vstd_ext/seq_lib.rs | 5 +- src/vstd_ext/set_lib.rs | 10 + 6 files changed, 348 insertions(+), 10 deletions(-) diff --git a/src/controller_examples/v_replica_set_controller/proof/liveness/resource_match.rs b/src/controller_examples/v_replica_set_controller/proof/liveness/resource_match.rs index 4c55f84e2..64fcf26d8 100644 --- a/src/controller_examples/v_replica_set_controller/proof/liveness/resource_match.rs +++ b/src/controller_examples/v_replica_set_controller/proof/liveness/resource_match.rs @@ -483,7 +483,7 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp( assert(resp_objs == selected_elements.to_seq()); assert(selected_elements.contains(o)); } - seq_pred_false_on_all_elements_implies_empty_filter(resp_objs, |o: DynamicObjectView| PodView::unmarshal(o).is_err()); + seq_pred_false_on_all_elements_is_equivalent_to_empty_filter(resp_objs, |o: DynamicObjectView| PodView::unmarshal(o).is_err()); assert({ &&& s_prime.in_flight().contains(resp_msg) @@ -535,7 +535,7 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp( assert(resp_objs == selected_elements.to_seq()); assert(selected_elements.contains(o)); } - seq_pred_false_on_all_elements_implies_empty_filter(resp_objs, |o: DynamicObjectView| PodView::unmarshal(o).is_err()); + seq_pred_false_on_all_elements_is_equivalent_to_empty_filter(resp_objs, |o: DynamicObjectView| PodView::unmarshal(o).is_err()); assert({ &&& s_prime.in_flight().contains(resp_msg) diff --git a/src/v2/controllers/vreplicaset_controller/proof/helper_lemmas.rs b/src/v2/controllers/vreplicaset_controller/proof/helper_lemmas.rs index d584d1cb5..2c4cb844e 100644 --- a/src/v2/controllers/vreplicaset_controller/proof/helper_lemmas.rs +++ b/src/v2/controllers/vreplicaset_controller/proof/helper_lemmas.rs @@ -11,7 +11,7 @@ use crate::temporal_logic::{defs::*, rules::*}; use crate::vreplicaset_controller::{ model::{install::*, reconciler::*}, trusted::{liveness_theorem::*, spec_types::*, step::*}, - proof::{predicate::*}, + proof::{helper_invariants, predicate::*}, }; use vstd::prelude::*; @@ -68,4 +68,93 @@ pub proof fn vrs_non_interference_property_equivalent_to_lifted_vrs_non_interfer ); } +#[verifier(external_body)] +pub proof fn lemma_filtered_pods_set_equals_matching_pods( + s: ClusterState, vrs: VReplicaSetView, cluster: Cluster, + controller_id: int, resp_msg: Message +) + requires + //cluster.next_step(s, s_prime, Step::ControllerStep((controller_id, Some(resp_msg), Some(vrs.object_ref())))), + resp_msg_is_the_in_flight_list_resp_at_after_list_pods_step(vrs, controller_id, resp_msg)(s), + // Cluster::each_object_in_etcd_is_weakly_well_formed()(s), + // 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), + // 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_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)), + // forall |diff: usize| !(#[trigger] at_vrs_step_with_vrs(vrs, controller_id, VReplicaSetReconcileStep::AfterDeletePod(diff))(s)), + // forall |other_id| cluster.controller_models.remove(controller_id).contains_key(other_id) + // ==> #[trigger] vrs_not_interfered_by(other_id)(s) + ensures + ({ + let objs = resp_msg.content.get_list_response().res.unwrap(); + let pods_or_none = objects_to_pods(objs); + let pods = pods_or_none.unwrap(); + let filtered_pods = filter_pods(pods, vrs); + &&& filtered_pods.no_duplicates() + &&& filtered_pods.len() == matching_pod_entries(vrs, s.resources()).len() + &&& filtered_pods.map_values(|p: PodView| p.marshal()).to_set() == matching_pod_entries(vrs, s.resources()).values() + }), +{ + let pre = resp_msg_is_the_in_flight_list_resp_at_after_list_pods_step(vrs, controller_id, resp_msg)(s); + let objs = resp_msg.content.get_list_response().res.unwrap(); + let pods_or_none = objects_to_pods(objs); + let pods = pods_or_none.unwrap(); + let filtered_pods = filter_pods(pods, vrs); + + assert(objs.no_duplicates()); + + assert forall |i: int, j: int| #![auto] + 0 <= i && i < pods.len() && (0 <= j && j < pods.len()) && !(i == j) + && pre + implies !(pods.index(i) == pods.index(j)) by { + + // assert(pods_or_none == objects_to_pods(objs)); + // assert(pods_or_none.is_Some()); + //assert(objs.filter(|o: DynamicObjectView| PodView::unmarshal(o).is_err()).len() == 0); + assert(pods == objs.map_values(|o: DynamicObjectView| PodView::unmarshal(o).unwrap())); + PodView::marshal_preserves_integrity(); + assert(pods[i] == PodView::unmarshal(objs[i]).unwrap()); + assert(pods[j] == PodView::unmarshal(objs[j]).unwrap()); + assert(pods[i].marshal() == objs[i]); + assert(pods[j].marshal() == objs[j]); + assert(!(objs[i] == objs[j])); + + //assume(false); + } + +// // First operation -- conversion from DynamicObjectView to PodView +// let pods_as_dov_set = Set::new(|o: DynamicObjectView| { +// let pod_or_error = PodView::unmarshal(o); +// &&& PodView::unmarshal(o).is_Ok() +// &&& pods.contains(pod_or_error.unwrap()) +// }); +// assert(objs.to_set() == pods_as_dov_set); + +// // Second operation -- filtered out. + + +// //assert(objs.to_set().subset_of(s.resources().values())); +// assert({&&& matching_pod_entries(vrs, s.resources()).values().subset_of(objs.to_set()) +// &&& objects_to_pods(objs).is_Some()}); + + assert(pods.no_duplicates()); + assert(filtered_pods.to_set().subset_of(pods.to_set())); + assert(filtered_pods.no_duplicates()); + assert(filtered_pods.len() == matching_pod_entries(vrs, s.resources()).len()); + + // let filtered_pods_set = filtered_pods.map_values(|p: PodView| p.marshal()).to_set(); + // let matching_pods_set = matching_pod_entries(vrs, s.resources()).values(); + // assert forall |o: DynamicObjectView| #[trigger] filtered_pods_set.contains(o) implies matching_pods_set.contains(o) by { + // //assume(false); + // } + // assert forall |o: DynamicObjectView| #[trigger] matching_pods_set.contains(o) implies filtered_pods_set.contains(o) by { + // //assume(false); + // } +} + } \ 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 5c4008dc9..1d501c09c 100644 --- a/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs +++ b/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs @@ -15,10 +15,14 @@ use crate::vreplicaset_controller::{ proof::{helper_invariants, helper_lemmas, liveness::{api_actions::*}, predicate::*}, }; use crate::vstd_ext::{map_lib::*, set_lib::*, seq_lib::*}; -use vstd::{map_lib::*, prelude::*}; +use vstd::{map_lib::*, math::*, prelude::*}; verus! { +// -------------------- WF1 Reasoning ---------------------- + +// List lemmas + pub proof fn lemma_from_init_step_to_send_list_pods_req( vrs: VReplicaSetView, spec: TempPred, cluster: Cluster, controller_id: int, diff: int ) @@ -279,7 +283,52 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp( assert(resp_objs == selected_elements.to_seq()); assert(selected_elements.contains(o)); } - seq_pred_false_on_all_elements_implies_empty_filter(resp_objs, |o: DynamicObjectView| PodView::unmarshal(o).is_err()); + seq_pred_false_on_all_elements_is_equivalent_to_empty_filter(resp_objs, |o: DynamicObjectView| PodView::unmarshal(o).is_err()); + + // TODO: Shorten up this proof. + assert_by(objects_to_pods(resp_objs).unwrap().no_duplicates(), { + let selector = |o: DynamicObjectView| { + &&& o.object_ref().namespace == vrs.metadata.namespace.unwrap() + &&& o.object_ref().kind == PodView::kind() + }; + let selected_elements = s.resources().values().filter(selector); + lemma_values_finite(s.resources()); + finite_set_to_seq_has_no_duplicates(selected_elements); + let selected_elements_seq = selected_elements.to_seq(); + let pods_seq = objects_to_pods(selected_elements_seq).unwrap(); + assert(selected_elements_seq.no_duplicates()); + + assert forall |x: DynamicObjectView, y: DynamicObjectView| #![auto] + x != y + && selected_elements_seq.contains(x) + && selected_elements_seq.contains(y) implies x.object_ref() != y.object_ref() by { + finite_set_to_seq_contains_all_set_elements(selected_elements); + assert(selected_elements.contains(x)); + assert(selected_elements.contains(y)); + } + + let lem = forall |x: DynamicObjectView, y: DynamicObjectView| #![auto] + x != y + && selected_elements_seq.contains(x) + && selected_elements_seq.contains(y) ==> x.object_ref() != y.object_ref(); + + assert forall |i: int, j: int| #![auto] + 0 <= i && i < pods_seq.len() && (0 <= j && j < pods_seq.len()) && !(i == j) + && objects_to_pods(selected_elements_seq).is_Some() + && lem + implies pods_seq[i] != pods_seq[j] by { + let o1 = selected_elements_seq[i]; + let o2 = selected_elements_seq[j]; + assert(o1.object_ref() != o2.object_ref()); + PodView::marshal_preserves_integrity(); + seq_pred_false_on_all_elements_is_equivalent_to_empty_filter(selected_elements_seq, |o: DynamicObjectView| PodView::unmarshal(o).is_err()); + assert(selected_elements_seq.filter(|o: DynamicObjectView| PodView::unmarshal(o).is_err()).len() == 0); + assert(selected_elements_seq.contains(o1)); + assert(selected_elements_seq.contains(o2)); + } + + assert(pods_seq.no_duplicates()); + }); assert({ &&& s_prime.in_flight().contains(resp_msg) @@ -290,6 +339,7 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp( // The matching pods must be a subset of the response. &&& matching_pod_entries(vrs, s_prime.resources()).values().subset_of(resp_objs.to_set()) &&& objects_to_pods(resp_objs).is_Some() + &&& objects_to_pods(resp_objs).unwrap().no_duplicates() } }); assert(post(s_prime)); @@ -332,7 +382,52 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp( assert(selected_elements.contains(o)); assert(s.resources().contains_value(o)); } - seq_pred_false_on_all_elements_implies_empty_filter(resp_objs, |o: DynamicObjectView| PodView::unmarshal(o).is_err()); + seq_pred_false_on_all_elements_is_equivalent_to_empty_filter(resp_objs, |o: DynamicObjectView| PodView::unmarshal(o).is_err()); + + // TODO: Shorten up this proof. + assert_by(objects_to_pods(resp_objs).unwrap().no_duplicates(), { + let selector = |o: DynamicObjectView| { + &&& o.object_ref().namespace == vrs.metadata.namespace.unwrap() + &&& o.object_ref().kind == PodView::kind() + }; + let selected_elements = s.resources().values().filter(selector); + lemma_values_finite(s.resources()); + finite_set_to_seq_has_no_duplicates(selected_elements); + let selected_elements_seq = selected_elements.to_seq(); + let pods_seq = objects_to_pods(selected_elements_seq).unwrap(); + assert(selected_elements_seq.no_duplicates()); + + assert forall |x: DynamicObjectView, y: DynamicObjectView| #![auto] + x != y + && selected_elements_seq.contains(x) + && selected_elements_seq.contains(y) implies x.object_ref() != y.object_ref() by { + finite_set_to_seq_contains_all_set_elements(selected_elements); + assert(selected_elements.contains(x)); + assert(selected_elements.contains(y)); + } + + let lem = forall |x: DynamicObjectView, y: DynamicObjectView| #![auto] + x != y + && selected_elements_seq.contains(x) + && selected_elements_seq.contains(y) ==> x.object_ref() != y.object_ref(); + + assert forall |i: int, j: int| #![auto] + 0 <= i && i < pods_seq.len() && (0 <= j && j < pods_seq.len()) && !(i == j) + && objects_to_pods(selected_elements_seq).is_Some() + && lem + implies pods_seq[i] != pods_seq[j] by { + let o1 = selected_elements_seq[i]; + let o2 = selected_elements_seq[j]; + assert(o1.object_ref() != o2.object_ref()); + PodView::marshal_preserves_integrity(); + seq_pred_false_on_all_elements_is_equivalent_to_empty_filter(selected_elements_seq, |o: DynamicObjectView| PodView::unmarshal(o).is_err()); + assert(selected_elements_seq.filter(|o: DynamicObjectView| PodView::unmarshal(o).is_err()).len() == 0); + assert(selected_elements_seq.contains(o1)); + assert(selected_elements_seq.contains(o2)); + } + + assert(pods_seq.no_duplicates()); + }); assert({ &&& s_prime.in_flight().contains(resp_msg) @@ -343,6 +438,7 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp( // The matching pods must be a subset of the response. &&& matching_pod_entries(vrs, s_prime.resources()).values().subset_of(resp_objs.to_set()) &&& objects_to_pods(resp_objs).is_Some() + &&& objects_to_pods(resp_objs).unwrap().no_duplicates() } }); assert(post(s_prime)); @@ -352,5 +448,147 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp( spec, input, stronger_next, APIServerStep::HandleRequest, pre, post ); } - + +// Create lemmas + +pub proof fn lemma_from_after_receive_list_pods_resp_to_send_create_pod_req( + vrs: VReplicaSetView, spec: TempPred, cluster: Cluster, controller_id: int, + resp_msg: Message, diff: int +) + requires + spec.entails(always(lift_action(cluster.next()))), + cluster.type_is_installed_in_cluster::(), + cluster.controller_models.contains_pair(controller_id, vrs_controller_model()), + spec.entails(tla_forall(|i: (Option, Option)| cluster.controller_next().weak_fairness((controller_id, i.0, i.1)))), + spec.entails(always(lift_state(Cluster::there_is_the_controller_state(controller_id)))), + spec.entails(always(lift_state(Cluster::crash_disabled(controller_id)))), + spec.entails(always(lift_state(Cluster::req_drop_disabled()))), + spec.entails(always(lift_state(Cluster::pod_monkey_disabled()))), + spec.entails(always(lift_state(Cluster::every_in_flight_msg_has_unique_id()))), + spec.entails(always(lift_state(Cluster::each_object_in_etcd_is_weakly_well_formed()))), + 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_reconcile_has_consistent_key_and_valid_metadata(controller_id)))), + spec.entails(always(lift_state(Cluster::pending_req_of_key_is_unique_with_unique_id(controller_id, vrs.object_ref())))), + 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(helper_invariants::cluster_resources_is_finite()))), + spec.entails(always(lift_state(helper_invariants::vrs_replicas_bounded(vrs)))), + 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_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, + ensures + spec.entails( + lift_state( + |s: ClusterState| { + &&& resp_msg_is_the_in_flight_list_resp_at_after_list_pods_step(vrs, controller_id, resp_msg)(s) + &&& num_diff_pods_is(vrs, diff)(s) + } + ).leads_to( + lift_state( + |s: ClusterState| { + &&& pending_req_in_flight_at_after_create_pod_step(vrs, controller_id, (abs(diff) - 1) as nat)(s) + &&& num_diff_pods_is(vrs, diff)(s) + } + ) + ) + ), +{ + let pre = |s: ClusterState| { + &&& resp_msg_is_the_in_flight_list_resp_at_after_list_pods_step(vrs, controller_id, resp_msg)(s) + &&& num_diff_pods_is(vrs, diff)(s) + }; + let post = |s: ClusterState| { + &&& pending_req_in_flight_at_after_create_pod_step(vrs, controller_id, (abs(diff) - 1) as nat)(s) + &&& num_diff_pods_is(vrs, diff)(s) + }; + let input = (Some(resp_msg), Some(vrs.object_ref())); + let stronger_next = |s, s_prime: ClusterState| { + &&& cluster.next()(s, s_prime) + &&& Cluster::there_is_the_controller_state(controller_id)(s) + &&& Cluster::crash_disabled(controller_id)(s) + &&& Cluster::req_drop_disabled()(s) + &&& Cluster::pod_monkey_disabled()(s) + &&& Cluster::every_in_flight_msg_has_unique_id()(s) + &&& Cluster::each_object_in_etcd_is_weakly_well_formed()(s) + &&& 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_reconcile_has_consistent_key_and_valid_metadata(controller_id)(s) + &&& Cluster::pending_req_of_key_is_unique_with_unique_id(controller_id, vrs.object_ref())(s) + &&& forall |other_id| cluster.controller_models.remove(controller_id).contains_key(other_id) + ==> #[trigger] vrs_not_interfered_by(other_id)(s) + &&& helper_invariants::cluster_resources_is_finite()(s) + &&& helper_invariants::vrs_replicas_bounded(vrs)(s) + &&& 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_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_lemmas::vrs_non_interference_property_equivalent_to_lifted_vrs_non_interference_property( + spec, cluster, controller_id + ); + + combine_spec_entails_always_n!( + spec, lift_action(stronger_next), + lift_action(cluster.next()), + lift_state(Cluster::there_is_the_controller_state(controller_id)), + lift_state(Cluster::crash_disabled(controller_id)), + lift_state(Cluster::req_drop_disabled()), + lift_state(Cluster::pod_monkey_disabled()), + lift_state(Cluster::every_in_flight_msg_has_unique_id()), + lift_state(Cluster::each_object_in_etcd_is_weakly_well_formed()), + 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_reconcile_has_consistent_key_and_valid_metadata(controller_id)), + lift_state(Cluster::pending_req_of_key_is_unique_with_unique_id(controller_id, vrs.object_ref())), + lifted_vrs_non_interference_property(cluster, controller_id), + lift_state(helper_invariants::cluster_resources_is_finite()), + lift_state(helper_invariants::vrs_replicas_bounded(vrs)), + 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_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)) + ); + + assert forall |s, s_prime| pre(s) && #[trigger] stronger_next(s, s_prime) implies pre(s_prime) || post(s_prime) by { + let step = choose |step| cluster.next_step(s, s_prime, step); + match step { + Step::APIServerStep(input) => { + let msg = input.get_Some_0(); + lemma_api_request_outside_create_or_delete_loop_maintains_matching_pods( + s, s_prime, vrs, cluster, controller_id, diff, msg + ); + // Prod for the theorem prover to realize num_diff_pods_is(vrs, diff) is maintained. + assert(matching_pod_entries(vrs, s.resources()) == matching_pod_entries(vrs, s_prime.resources())); + }, + Step::ControllerStep(input) => { + if input.0 == controller_id + && input.1 == Some(resp_msg) + && input.2 == Some(vrs.object_ref()) { + VReplicaSetReconcileState::marshal_preserves_integrity(); + helper_lemmas::lemma_filtered_pods_set_equals_matching_pods( + s, vrs, cluster, controller_id, resp_msg + ); + } + }, + _ => {} + } + } + + cluster.lemma_pre_leads_to_post_by_controller( + spec, controller_id, input, stronger_next, ControllerStep::ContinueReconcile, pre, post + ); +} + +// Delete lemmas + } diff --git a/src/v2/controllers/vreplicaset_controller/proof/predicate.rs b/src/v2/controllers/vreplicaset_controller/proof/predicate.rs index d69437d04..b6d0e4c47 100644 --- a/src/v2/controllers/vreplicaset_controller/proof/predicate.rs +++ b/src/v2/controllers/vreplicaset_controller/proof/predicate.rs @@ -153,6 +153,7 @@ pub open spec fn exists_resp_in_flight_at_after_list_pods_step( // The matching pods must be a subset of the response. &&& matching_pod_entries(vrs, s.resources()).values().subset_of(resp_objs.to_set()) &&& objects_to_pods(resp_objs).is_Some() + &&& objects_to_pods(resp_objs).unwrap().no_duplicates() } } } @@ -183,6 +184,7 @@ pub open spec fn resp_msg_is_the_in_flight_list_resp_at_after_list_pods_step( // The matching pods must be a subset of the response. &&& matching_pod_entries(vrs, s.resources()).values().subset_of(resp_objs.to_set()) &&& objects_to_pods(resp_objs).is_Some() + &&& objects_to_pods(resp_objs).unwrap().no_duplicates() } } } diff --git a/src/vstd_ext/seq_lib.rs b/src/vstd_ext/seq_lib.rs index 7bb59b84a..77890c19c 100644 --- a/src/vstd_ext/seq_lib.rs +++ b/src/vstd_ext/seq_lib.rs @@ -104,9 +104,8 @@ pub proof fn seq_unequal_preserved_by_add_auto(suffix: Seq) } #[verifier(external_body)] -pub proof fn seq_pred_false_on_all_elements_implies_empty_filter(s: Seq, pred: spec_fn(A) -> bool) - requires forall |e: A| #![auto] s.contains(e) ==> !pred(e), - ensures s.filter(pred).len() == 0; +pub proof fn seq_pred_false_on_all_elements_is_equivalent_to_empty_filter(s: Seq, pred: spec_fn(A) -> bool) + ensures (forall |e: A| #![auto] s.contains(e) ==> !pred(e)) <==> s.filter(pred).len() == 0; // // TODO: Prove this -- Trivial. // diff --git a/src/vstd_ext/set_lib.rs b/src/vstd_ext/set_lib.rs index 71eb39413..ab1bb169f 100644 --- a/src/vstd_ext/set_lib.rs +++ b/src/vstd_ext/set_lib.rs @@ -18,4 +18,14 @@ pub proof fn finite_set_to_seq_contains_all_set_elements(s: Set) // anything in that constructed sequence will be part of the original set. // +#[verifier(external_body)] +pub proof fn finite_set_to_seq_has_no_duplicates(s: Set) + requires s.finite(), + ensures s.to_seq().no_duplicates(); +// +// TODO: Prove this -- Trivial. +// +// The `to_seq()` construction applied to a set will not introduce duplicates. +// + } From fedd2b4c123be33f6560cbbcbc66aa646ed98c5f Mon Sep 17 00:00:00 2001 From: Cody Rivera Date: Wed, 30 Oct 2024 13:23:13 -0500 Subject: [PATCH 2/8] Reasoning about sequences is hard Signed-off-by: Cody Rivera --- .../proof/helper_lemmas.rs | 61 +++---------------- src/vstd_ext/seq_lib.rs | 11 ++++ 2 files changed, 21 insertions(+), 51 deletions(-) diff --git a/src/v2/controllers/vreplicaset_controller/proof/helper_lemmas.rs b/src/v2/controllers/vreplicaset_controller/proof/helper_lemmas.rs index 2c4cb844e..624f038c7 100644 --- a/src/v2/controllers/vreplicaset_controller/proof/helper_lemmas.rs +++ b/src/v2/controllers/vreplicaset_controller/proof/helper_lemmas.rs @@ -13,6 +13,7 @@ use crate::vreplicaset_controller::{ trusted::{liveness_theorem::*, spec_types::*, step::*}, proof::{helper_invariants, predicate::*}, }; +use crate::vstd_ext::seq_lib::*; use vstd::prelude::*; verus! { @@ -68,27 +69,15 @@ pub proof fn vrs_non_interference_property_equivalent_to_lifted_vrs_non_interfer ); } +// TODO: Prove this lemma. +// Annoying sequence reasoning. #[verifier(external_body)] pub proof fn lemma_filtered_pods_set_equals_matching_pods( s: ClusterState, vrs: VReplicaSetView, cluster: Cluster, controller_id: int, resp_msg: Message ) requires - //cluster.next_step(s, s_prime, Step::ControllerStep((controller_id, Some(resp_msg), Some(vrs.object_ref())))), resp_msg_is_the_in_flight_list_resp_at_after_list_pods_step(vrs, controller_id, resp_msg)(s), - // Cluster::each_object_in_etcd_is_weakly_well_formed()(s), - // 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), - // 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_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)), - // forall |diff: usize| !(#[trigger] at_vrs_step_with_vrs(vrs, controller_id, VReplicaSetReconcileStep::AfterDeletePod(diff))(s)), - // forall |other_id| cluster.controller_models.remove(controller_id).contains_key(other_id) - // ==> #[trigger] vrs_not_interfered_by(other_id)(s) ensures ({ let objs = resp_msg.content.get_list_response().res.unwrap(); @@ -105,47 +94,17 @@ pub proof fn lemma_filtered_pods_set_equals_matching_pods( let pods_or_none = objects_to_pods(objs); let pods = pods_or_none.unwrap(); let filtered_pods = filter_pods(pods, vrs); - - assert(objs.no_duplicates()); - - assert forall |i: int, j: int| #![auto] - 0 <= i && i < pods.len() && (0 <= j && j < pods.len()) && !(i == j) - && pre - implies !(pods.index(i) == pods.index(j)) by { - - // assert(pods_or_none == objects_to_pods(objs)); - // assert(pods_or_none.is_Some()); - //assert(objs.filter(|o: DynamicObjectView| PodView::unmarshal(o).is_err()).len() == 0); - assert(pods == objs.map_values(|o: DynamicObjectView| PodView::unmarshal(o).unwrap())); - PodView::marshal_preserves_integrity(); - assert(pods[i] == PodView::unmarshal(objs[i]).unwrap()); - assert(pods[j] == PodView::unmarshal(objs[j]).unwrap()); - assert(pods[i].marshal() == objs[i]); - assert(pods[j].marshal() == objs[j]); - assert(!(objs[i] == objs[j])); - - //assume(false); - } - -// // First operation -- conversion from DynamicObjectView to PodView -// let pods_as_dov_set = Set::new(|o: DynamicObjectView| { -// let pod_or_error = PodView::unmarshal(o); -// &&& PodView::unmarshal(o).is_Ok() -// &&& pods.contains(pod_or_error.unwrap()) -// }); -// assert(objs.to_set() == pods_as_dov_set); - -// // Second operation -- filtered out. - - -// //assert(objs.to_set().subset_of(s.resources().values())); -// assert({&&& matching_pod_entries(vrs, s.resources()).values().subset_of(objs.to_set()) -// &&& objects_to_pods(objs).is_Some()}); assert(pods.no_duplicates()); - assert(filtered_pods.to_set().subset_of(pods.to_set())); + let pred = |pod: PodView| + pod.metadata.owner_references_contains(vrs.controller_owner_ref()) + && vrs.spec.selector.matches(pod.metadata.labels.unwrap_or(Map::empty())) + && pod.metadata.deletion_timestamp.is_None(); + seq_filter_preserves_no_duplicates(pods, pred); assert(filtered_pods.no_duplicates()); + assert(filtered_pods.len() == matching_pod_entries(vrs, s.resources()).len()); + assume(filtered_pods.map_values(|p: PodView| p.marshal()).to_set() == matching_pod_entries(vrs, s.resources()).values()); // let filtered_pods_set = filtered_pods.map_values(|p: PodView| p.marshal()).to_set(); // let matching_pods_set = matching_pod_entries(vrs, s.resources()).values(); diff --git a/src/vstd_ext/seq_lib.rs b/src/vstd_ext/seq_lib.rs index 77890c19c..35f754b4f 100644 --- a/src/vstd_ext/seq_lib.rs +++ b/src/vstd_ext/seq_lib.rs @@ -112,4 +112,15 @@ pub proof fn seq_pred_false_on_all_elements_is_equivalent_to_empty_filter(s: // If `pred` is false on every element, filter will return an empty sequence. // +#[verifier(external_body)] +pub proof fn seq_filter_preserves_no_duplicates(s: Seq, pred: spec_fn(A) -> bool) + requires s.no_duplicates(), + ensures s.filter(pred).no_duplicates(); +// +// TODO: Prove this -- Trivial. +// +// Since the parent sequence has no duplicates, and the filtered sequence only removes elements, +// that sequence also has no duplicates. +// + } From 28df1f05a18aa35e1d4315c3cca2124745eac1ab Mon Sep 17 00:00:00 2001 From: Cody Rivera Date: Thu, 31 Oct 2024 14:01:25 -0500 Subject: [PATCH 3/8] Prove Create WF1 Modulo Lemmas Signed-off-by: Cody Rivera --- .../proof/liveness/api_actions.rs | 69 ++++ .../proof/liveness/resource_match.rs | 352 +++++++++++++++++- 2 files changed, 420 insertions(+), 1 deletion(-) 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 8fb6c5896..4b503b37a 100644 --- a/src/v2/controllers/vreplicaset_controller/proof/liveness/api_actions.rs +++ b/src/v2/controllers/vreplicaset_controller/proof/liveness/api_actions.rs @@ -81,6 +81,75 @@ pub proof fn lemma_api_request_outside_create_or_delete_loop_maintains_matching_ _ => {} }; } + +// TODO: Prove this. +#[verifier(external_body)] +pub proof fn lemma_api_request_not_made_by_vrs_maintains_matching_pods( + s: ClusterState, s_prime: ClusterState, vrs: VReplicaSetView, cluster: Cluster, controller_id: int, + diff: int, msg: Message, req_msg: Option +) + requires + req_msg.is_Some() ==> msg != req_msg.get_Some_0(), + req_msg == s.ongoing_reconciles(controller_id)[vrs.object_ref()].pending_req_msg, + cluster.controller_models.contains_pair(controller_id, vrs_controller_model()), + cluster.next_step(s, s_prime, Step::APIServerStep(Some(msg))), + Cluster::each_object_in_etcd_is_weakly_well_formed()(s), + 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), + 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_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)), + // forall |diff: usize| !(#[trigger] at_vrs_step_with_vrs(vrs, controller_id, VReplicaSetReconcileStep::AfterDeletePod(diff))(s)), + forall |other_id| cluster.controller_models.remove(controller_id).contains_key(other_id) + ==> #[trigger] vrs_not_interfered_by(other_id)(s) + ensures + matching_pod_entries(vrs, s.resources()) == matching_pod_entries(vrs, s_prime.resources()), +{ + if msg.src.is_Controller() { + let id = msg.src.get_Controller_0(); + assert( + (id != controller_id ==> cluster.controller_models.remove(controller_id).contains_key(id))); + // Invoke non-interference lemma by trigger. + assert(id != controller_id ==> vrs_not_interfered_by(id)(s)); + } + + // Dispatch through all the requests which may mutate the k-v store. + let mutates_key = if msg.content.is_create_request() { + let req = msg.content.get_create_request(); + Some(ObjectRef{ + kind: req.obj.kind, + name: if req.obj.metadata.name.is_Some() { + req.obj.metadata.name.unwrap() + } else { + generate_name(s.api_server) + }, + namespace: req.namespace, + }) + } else if msg.content.is_delete_request() { + let req = msg.content.get_delete_request(); + Some(req.key) + } else if msg.content.is_update_request() { + let req = msg.content.get_update_request(); + Some(req.key()) + } else if msg.content.is_update_status_request() { + let req = msg.content.get_update_status_request(); + Some(req.key()) + } else { + None + }; + + match mutates_key { + Some(key) => { + assert_maps_equal!(s.resources().remove(key) == s_prime.resources().remove(key)); + assert_maps_equal!(matching_pod_entries(vrs, s.resources()) == matching_pod_entries(vrs, s_prime.resources())); + }, + _ => {} + }; +} } 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 1d501c09c..ba04aff04 100644 --- a/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs +++ b/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs @@ -15,7 +15,7 @@ use crate::vreplicaset_controller::{ proof::{helper_invariants, helper_lemmas, liveness::{api_actions::*}, predicate::*}, }; use crate::vstd_ext::{map_lib::*, set_lib::*, seq_lib::*}; -use vstd::{map_lib::*, math::*, prelude::*}; +use vstd::{map::*, map_lib::*, math::*, prelude::*}; verus! { @@ -589,6 +589,356 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_send_create_pod_req( ); } +pub proof fn lemma_from_after_send_create_pod_req_to_receive_ok_resp( + vrs: VReplicaSetView, spec: TempPred, cluster: Cluster, controller_id: int, + req_msg: Message, diff: int +) + requires + spec.entails(always(lift_action(cluster.next()))), + cluster.type_is_installed_in_cluster::(), + cluster.controller_models.contains_pair(controller_id, vrs_controller_model()), + spec.entails(tla_forall(|i| cluster.api_server_next().weak_fairness(i))), + spec.entails(always(lift_state(Cluster::there_is_the_controller_state(controller_id)))), + spec.entails(always(lift_state(Cluster::crash_disabled(controller_id)))), + spec.entails(always(lift_state(Cluster::req_drop_disabled()))), + spec.entails(always(lift_state(Cluster::pod_monkey_disabled()))), + spec.entails(always(lift_state(Cluster::every_in_flight_msg_has_unique_id()))), + spec.entails(always(lift_state(Cluster::each_object_in_etcd_is_weakly_well_formed()))), + 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()))), + 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(helper_invariants::cluster_resources_is_finite()))), + spec.entails(always(lift_state(helper_invariants::vrs_selector_matches_template_labels(vrs)))), + 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_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, + ensures + spec.entails( + lift_state( + |s: ClusterState| { + &&& req_msg_is_the_in_flight_create_request_at_after_create_pod_step(vrs, controller_id, req_msg, (abs(diff) - 1) as nat)(s) + &&& num_diff_pods_is(vrs, diff)(s) + } + ).leads_to( + lift_state( + |s: ClusterState| { + &&& exists_ok_resp_in_flight_at_after_create_pod_step(vrs, controller_id, (abs(diff) - 1) as nat)(s) + &&& num_diff_pods_is(vrs, diff + 1)(s) + } + ) + ) + ), +{ + let pre = |s: ClusterState| { + &&& req_msg_is_the_in_flight_create_request_at_after_create_pod_step(vrs, controller_id, req_msg, (abs(diff) - 1) as nat)(s) + &&& num_diff_pods_is(vrs, diff)(s) + }; + let post = |s: ClusterState| { + &&& exists_ok_resp_in_flight_at_after_create_pod_step(vrs, controller_id, (abs(diff) - 1) as nat)(s) + &&& num_diff_pods_is(vrs, diff + 1)(s) + }; + let input = Some(req_msg); + let stronger_next = |s, s_prime: ClusterState| { + &&& cluster.next()(s, s_prime) + &&& Cluster::there_is_the_controller_state(controller_id)(s) + &&& Cluster::crash_disabled(controller_id)(s) + &&& Cluster::req_drop_disabled()(s) + &&& Cluster::pod_monkey_disabled()(s) + &&& Cluster::every_in_flight_msg_has_unique_id()(s) + &&& Cluster::each_object_in_etcd_is_weakly_well_formed()(s) + &&& 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) + &&& forall |other_id| cluster.controller_models.remove(controller_id).contains_key(other_id) + ==> #[trigger] vrs_not_interfered_by(other_id)(s) + &&& helper_invariants::cluster_resources_is_finite()(s) + &&& helper_invariants::vrs_selector_matches_template_labels(vrs)(s) + &&& 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_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_lemmas::vrs_non_interference_property_equivalent_to_lifted_vrs_non_interference_property( + spec, cluster, controller_id + ); + + combine_spec_entails_always_n!( + spec, lift_action(stronger_next), + lift_action(cluster.next()), + lift_state(Cluster::there_is_the_controller_state(controller_id)), + lift_state(Cluster::crash_disabled(controller_id)), + lift_state(Cluster::req_drop_disabled()), + lift_state(Cluster::pod_monkey_disabled()), + lift_state(Cluster::every_in_flight_msg_has_unique_id()), + lift_state(Cluster::each_object_in_etcd_is_weakly_well_formed()), + 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()), + lifted_vrs_non_interference_property(cluster, controller_id), + lift_state(helper_invariants::cluster_resources_is_finite()), + lift_state(helper_invariants::vrs_selector_matches_template_labels(vrs)), + 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_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)) + ); + + + assert forall |s, s_prime| pre(s) && #[trigger] stronger_next(s, s_prime) implies pre(s_prime) || post(s_prime) by { + let step = choose |step| cluster.next_step(s, s_prime, step); + match step { + Step::APIServerStep(input) => { + let msg = input.get_Some_0(); + // Case 1: We're processing the create request + if msg == req_msg { + let resp_msg = handle_create_request_msg(cluster.installed_types, req_msg, s.api_server).1; + let req = req_msg.content.get_create_request(); + let created_obj = DynamicObjectView { + kind: req.obj.kind, + metadata: ObjectMetaView { + // Set name for new object if name is not provided, here we generate + // a unique name. The uniqueness is guaranteed by generated_name_is_unique. + name: if req.obj.metadata.name.is_Some() { + req.obj.metadata.name + } else { + Some(generate_name(s.api_server)) + }, + namespace: Some(req.namespace), // Set namespace for new object + resource_version: Some(s.api_server.resource_version_counter), // Set rv for new object + uid: Some(s.api_server.uid_counter), // Set uid for new object + deletion_timestamp: None, // Unset deletion timestamp for new object + ..req.obj.metadata + }, + spec: req.obj.spec, + status: marshalled_default_status(req.obj.kind, cluster.installed_types), // Overwrite the status with the default one + }; + let key = created_obj.object_ref(); + + // Asserts properties about the response message + generated_name_is_unique(s.api_server); + assert({ + &&& s_prime.in_flight().contains(resp_msg) + &&& resp_msg_matches_req_msg(resp_msg, msg) + &&& resp_msg.content.get_create_response().res.is_Ok() + }); + + // Asserts properties about the newly inserted object. + assert_maps_equal!(s.resources().insert(key, created_obj) == s_prime.resources()); + assert(s.resources().len() + 1 == s_prime.resources().len()); + assert(created_obj.metadata.owner_references.unwrap()[0] == vrs.controller_owner_ref()); + assert(owned_selector_match_is(vrs, created_obj)); + + // Small prod for the theorem prover to realize num_diff_pods_is(vrs, diff) is increased. + a_submap_of_a_finite_map_is_finite(matching_pod_entries(vrs, s.resources()), s.resources()); + assert(matching_pod_entries(vrs, s.resources()).insert(key, created_obj) == matching_pod_entries(vrs, s_prime.resources())); + } else { + a_submap_of_a_finite_map_is_finite(matching_pod_entries(vrs, s.resources()), s.resources()); + lemma_api_request_not_made_by_vrs_maintains_matching_pods( + s, s_prime, vrs, cluster, controller_id, diff, msg, Some(req_msg), + ); + assert(matching_pod_entries(vrs, s.resources()) == matching_pod_entries(vrs, s_prime.resources())); + } + }, + _ => {} + } + } + + assert forall |s, s_prime: ClusterState| pre(s) && #[trigger] stronger_next(s, s_prime) && cluster.api_server_next().forward(input)(s, s_prime) implies post(s_prime) by { + let resp_msg = handle_create_request_msg(cluster.installed_types, req_msg, s.api_server).1; + let req = req_msg.content.get_create_request(); + let created_obj = DynamicObjectView { + kind: req.obj.kind, + metadata: ObjectMetaView { + // Set name for new object if name is not provided, here we generate + // a unique name. The uniqueness is guaranteed by generated_name_is_unique. + name: if req.obj.metadata.name.is_Some() { + req.obj.metadata.name + } else { + Some(generate_name(s.api_server)) + }, + namespace: Some(req.namespace), // Set namespace for new object + resource_version: Some(s.api_server.resource_version_counter), // Set rv for new object + uid: Some(s.api_server.uid_counter), // Set uid for new object + deletion_timestamp: None, // Unset deletion timestamp for new object + ..req.obj.metadata + }, + spec: req.obj.spec, + status: marshalled_default_status(req.obj.kind, cluster.installed_types), // Overwrite the status with the default one + }; + let key = created_obj.object_ref(); + + // Asserts properties about the response message + generated_name_is_unique(s.api_server); + assert({ + &&& s_prime.in_flight().contains(resp_msg) + &&& resp_msg_matches_req_msg(resp_msg, req_msg) + &&& resp_msg.content.get_create_response().res.is_Ok() + }); + + // Asserts properties about the newly inserted object. + assert_maps_equal!(s.resources().insert(key, created_obj) == s_prime.resources()); + assert(s.resources().len() + 1 == s_prime.resources().len()); + assert(created_obj.metadata.owner_references.unwrap()[0] == vrs.controller_owner_ref()); + assert(owned_selector_match_is(vrs, created_obj)); + + // Small prod for the theorem prover to realize num_diff_pods_is(vrs, diff) is increased. + a_submap_of_a_finite_map_is_finite(matching_pod_entries(vrs, s.resources()), s.resources()); + assert(matching_pod_entries(vrs, s.resources()).insert(key, created_obj) == matching_pod_entries(vrs, s_prime.resources())); + } + + cluster.lemma_pre_leads_to_post_by_api_server( + spec, input, stronger_next, APIServerStep::HandleRequest, pre, post + ); +} + +pub proof fn lemma_from_after_receive_ok_resp_to_send_create_pod_req( + vrs: VReplicaSetView, spec: TempPred, cluster: Cluster, controller_id: int, + resp_msg: Message, diff: int +) + requires + spec.entails(always(lift_action(cluster.next()))), + cluster.type_is_installed_in_cluster::(), + cluster.controller_models.contains_pair(controller_id, vrs_controller_model()), + spec.entails(tla_forall(|i: (Option, Option)| cluster.controller_next().weak_fairness((controller_id, i.0, i.1)))), + spec.entails(always(lift_state(Cluster::there_is_the_controller_state(controller_id)))), + spec.entails(always(lift_state(Cluster::crash_disabled(controller_id)))), + spec.entails(always(lift_state(Cluster::req_drop_disabled()))), + spec.entails(always(lift_state(Cluster::pod_monkey_disabled()))), + spec.entails(always(lift_state(Cluster::every_in_flight_msg_has_unique_id()))), + spec.entails(always(lift_state(Cluster::each_object_in_etcd_is_weakly_well_formed()))), + 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_reconcile_has_consistent_key_and_valid_metadata(controller_id)))), + spec.entails(always(lift_state(Cluster::pending_req_of_key_is_unique_with_unique_id(controller_id, vrs.object_ref())))), + 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(helper_invariants::cluster_resources_is_finite()))), + spec.entails(always(lift_state(helper_invariants::vrs_replicas_bounded(vrs)))), + 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_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, + ensures + spec.entails( + lift_state( + |s: ClusterState| { + &&& resp_msg_is_the_in_flight_ok_resp_at_after_create_pod_step(vrs, controller_id, resp_msg, abs(diff))(s) + &&& num_diff_pods_is(vrs, diff)(s) + } + ).leads_to( + lift_state( + |s: ClusterState| { + &&& pending_req_in_flight_at_after_create_pod_step(vrs, controller_id, (abs(diff) - 1) as nat)(s) + &&& num_diff_pods_is(vrs, diff)(s) + } + ) + ) + ), +{ + let pre = |s: ClusterState| { + &&& resp_msg_is_the_in_flight_ok_resp_at_after_create_pod_step(vrs, controller_id, resp_msg, abs(diff))(s) + &&& num_diff_pods_is(vrs, diff)(s) + }; + let post = |s: ClusterState| { + &&& pending_req_in_flight_at_after_create_pod_step(vrs, controller_id, (abs(diff) - 1) as nat)(s) + &&& num_diff_pods_is(vrs, diff)(s) + }; + let input = (Some(resp_msg), Some(vrs.object_ref())); + + let stronger_next = |s, s_prime: ClusterState| { + &&& cluster.next()(s, s_prime) + &&& Cluster::there_is_the_controller_state(controller_id)(s) + &&& Cluster::crash_disabled(controller_id)(s) + &&& Cluster::req_drop_disabled()(s) + &&& Cluster::pod_monkey_disabled()(s) + &&& Cluster::every_in_flight_msg_has_unique_id()(s) + &&& Cluster::each_object_in_etcd_is_weakly_well_formed()(s) + &&& 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_reconcile_has_consistent_key_and_valid_metadata(controller_id)(s) + &&& Cluster::pending_req_of_key_is_unique_with_unique_id(controller_id, vrs.object_ref())(s) + &&& forall |other_id| cluster.controller_models.remove(controller_id).contains_key(other_id) + ==> #[trigger] vrs_not_interfered_by(other_id)(s) + &&& helper_invariants::cluster_resources_is_finite()(s) + &&& helper_invariants::vrs_replicas_bounded(vrs)(s) + &&& 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_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_lemmas::vrs_non_interference_property_equivalent_to_lifted_vrs_non_interference_property( + spec, cluster, controller_id + ); + + combine_spec_entails_always_n!( + spec, lift_action(stronger_next), + lift_action(cluster.next()), + lift_state(Cluster::there_is_the_controller_state(controller_id)), + lift_state(Cluster::crash_disabled(controller_id)), + lift_state(Cluster::req_drop_disabled()), + lift_state(Cluster::pod_monkey_disabled()), + lift_state(Cluster::every_in_flight_msg_has_unique_id()), + lift_state(Cluster::each_object_in_etcd_is_weakly_well_formed()), + 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_reconcile_has_consistent_key_and_valid_metadata(controller_id)), + lift_state(Cluster::pending_req_of_key_is_unique_with_unique_id(controller_id, vrs.object_ref())), + lifted_vrs_non_interference_property(cluster, controller_id), + lift_state(helper_invariants::cluster_resources_is_finite()), + lift_state(helper_invariants::vrs_replicas_bounded(vrs)), + 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_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)) + ); + + assert forall |s, s_prime| pre(s) && #[trigger] stronger_next(s, s_prime) implies pre(s_prime) || post(s_prime) by { + let step = choose |step| cluster.next_step(s, s_prime, step); + match step { + Step::APIServerStep(input) => { + let msg = input.get_Some_0(); + let pending_req_msg = s.ongoing_reconciles(controller_id)[vrs.object_ref()].pending_req_msg; + lemma_api_request_not_made_by_vrs_maintains_matching_pods( + s, s_prime, vrs, cluster, controller_id, diff, msg, pending_req_msg + ); + // Small prod for the theorem prover to realize num_diff_pods_is(vrs, diff) is maintained. + assert(matching_pod_entries(vrs, s.resources()) == matching_pod_entries(vrs, s_prime.resources())); + }, + Step::ControllerStep(..) => { + VReplicaSetReconcileState::marshal_preserves_integrity(); + }, + _ => {} + } + } + + assert forall |s, s_prime| pre(s) && #[trigger] stronger_next(s, s_prime) + && cluster.controller_next().forward((controller_id, input.0, input.1))(s, s_prime) implies post(s_prime) by { + VReplicaSetReconcileState::marshal_preserves_integrity(); + } + + cluster.lemma_pre_leads_to_post_by_controller( + spec, controller_id, input, stronger_next, ControllerStep::ContinueReconcile, pre, post + ); +} + // Delete lemmas } From 599d6376515e3d4974409d1be219874c14a10a3b Mon Sep 17 00:00:00 2001 From: Cody Rivera Date: Thu, 31 Oct 2024 14:56:18 -0500 Subject: [PATCH 4/8] Clean up unused import warnings Signed-off-by: Cody Rivera --- .../vreplicaset_controller/proof/liveness/proof.rs | 6 +++--- src/v2/kubernetes_cluster/proof/network.rs | 5 +---- 2 files changed, 4 insertions(+), 7 deletions(-) diff --git a/src/v2/controllers/vreplicaset_controller/proof/liveness/proof.rs b/src/v2/controllers/vreplicaset_controller/proof/liveness/proof.rs index df4df082b..84e0c8063 100644 --- a/src/v2/controllers/vreplicaset_controller/proof/liveness/proof.rs +++ b/src/v2/controllers/vreplicaset_controller/proof/liveness/proof.rs @@ -1,9 +1,9 @@ use crate::kubernetes_api_objects::spec::prelude::*; use crate::kubernetes_cluster::spec::{cluster::*, message::*}; -use crate::temporal_logic::{defs::*, rules::*}; +use crate::temporal_logic::{defs::*}; use crate::vreplicaset_controller::{ - model::{install::*, reconciler::*}, - trusted::{liveness_theorem::*, spec_types::*, step::*}, + model::{install::*}, + trusted::{liveness_theorem::*, spec_types::*}, }; use vstd::prelude::*; diff --git a/src/v2/kubernetes_cluster/proof/network.rs b/src/v2/kubernetes_cluster/proof/network.rs index 1db8c486a..81a59b68b 100644 --- a/src/v2/kubernetes_cluster/proof/network.rs +++ b/src/v2/kubernetes_cluster/proof/network.rs @@ -1,10 +1,7 @@ use crate::kubernetes_api_objects::spec::prelude::*; use crate::temporal_logic::{defs::*, rules::*}; use crate::kubernetes_cluster::spec::{ - api_server::{ - state_machine::transition_by_etcd, - types::*, - }, + api_server::state_machine::transition_by_etcd, cluster::*, controller::types::*, message::*, From 845361ba90d4e9adafd0f0bcc36530a7f716ce2d Mon Sep 17 00:00:00 2001 From: Cody Rivera Date: Thu, 31 Oct 2024 14:56:53 -0500 Subject: [PATCH 5/8] Simple proof speed optimization Signed-off-by: Cody Rivera --- .../proof/liveness/resource_match.rs | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) 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 ba04aff04..75780a5fa 100644 --- a/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs +++ b/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs @@ -741,11 +741,12 @@ pub proof fn lemma_from_after_send_create_pod_req_to_receive_ok_resp( a_submap_of_a_finite_map_is_finite(matching_pod_entries(vrs, s.resources()), s.resources()); assert(matching_pod_entries(vrs, s.resources()).insert(key, created_obj) == matching_pod_entries(vrs, s_prime.resources())); } else { - a_submap_of_a_finite_map_is_finite(matching_pod_entries(vrs, s.resources()), s.resources()); - lemma_api_request_not_made_by_vrs_maintains_matching_pods( - s, s_prime, vrs, cluster, controller_id, diff, msg, Some(req_msg), - ); - assert(matching_pod_entries(vrs, s.resources()) == matching_pod_entries(vrs, s_prime.resources())); + assert_by(matching_pod_entries(vrs, s.resources()) == matching_pod_entries(vrs, s_prime.resources()), { + a_submap_of_a_finite_map_is_finite(matching_pod_entries(vrs, s.resources()), s.resources()); + lemma_api_request_not_made_by_vrs_maintains_matching_pods( + s, s_prime, vrs, cluster, controller_id, diff, msg, Some(req_msg), + ); + }); } }, _ => {} From 636c4d1b39b08d166478d3bcd5469c3b9022fc07 Mon Sep 17 00:00:00 2001 From: Cody Rivera Date: Thu, 31 Oct 2024 16:06:18 -0500 Subject: [PATCH 6/8] Add a trigger Signed-off-by: Cody Rivera --- src/vstd_ext/seq_lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/vstd_ext/seq_lib.rs b/src/vstd_ext/seq_lib.rs index 35f754b4f..2db15dc12 100644 --- a/src/vstd_ext/seq_lib.rs +++ b/src/vstd_ext/seq_lib.rs @@ -105,7 +105,7 @@ pub proof fn seq_unequal_preserved_by_add_auto(suffix: Seq) #[verifier(external_body)] pub proof fn seq_pred_false_on_all_elements_is_equivalent_to_empty_filter(s: Seq, pred: spec_fn(A) -> bool) - ensures (forall |e: A| #![auto] s.contains(e) ==> !pred(e)) <==> s.filter(pred).len() == 0; + ensures (forall |e: A| #[trigger] s.contains(e) ==> !pred(e)) <==> s.filter(pred).len() == 0; // // TODO: Prove this -- Trivial. // From dd45ba115377f1b337a8e8ef20086aca4c640308 Mon Sep 17 00:00:00 2001 From: Cody Rivera Date: Thu, 31 Oct 2024 16:11:25 -0500 Subject: [PATCH 7/8] Describe unproved sequence reasoning lemma Signed-off-by: Cody Rivera --- .../proof/helper_lemmas.rs | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/src/v2/controllers/vreplicaset_controller/proof/helper_lemmas.rs b/src/v2/controllers/vreplicaset_controller/proof/helper_lemmas.rs index 624f038c7..93f229e6b 100644 --- a/src/v2/controllers/vreplicaset_controller/proof/helper_lemmas.rs +++ b/src/v2/controllers/vreplicaset_controller/proof/helper_lemmas.rs @@ -70,7 +70,7 @@ pub proof fn vrs_non_interference_property_equivalent_to_lifted_vrs_non_interfer } // TODO: Prove this lemma. -// Annoying sequence reasoning. +// More comments sketching an informal proof in the body. #[verifier(external_body)] pub proof fn lemma_filtered_pods_set_equals_matching_pods( s: ClusterState, vrs: VReplicaSetView, cluster: Cluster, @@ -95,6 +95,7 @@ pub proof fn lemma_filtered_pods_set_equals_matching_pods( let pods = pods_or_none.unwrap(); let filtered_pods = filter_pods(pods, vrs); + // We've proved the first property of filtered_pods. assert(pods.no_duplicates()); let pred = |pod: PodView| pod.metadata.owner_references_contains(vrs.controller_owner_ref()) @@ -103,17 +104,13 @@ pub proof fn lemma_filtered_pods_set_equals_matching_pods( seq_filter_preserves_no_duplicates(pods, pred); assert(filtered_pods.no_duplicates()); + // We now must prove that the number of elements of `filtered_pods` is equal to the number + // of matching pods. This is true by the way we construct `filtered_pods`. assert(filtered_pods.len() == matching_pod_entries(vrs, s.resources()).len()); - assume(filtered_pods.map_values(|p: PodView| p.marshal()).to_set() == matching_pod_entries(vrs, s.resources()).values()); - // let filtered_pods_set = filtered_pods.map_values(|p: PodView| p.marshal()).to_set(); - // let matching_pods_set = matching_pod_entries(vrs, s.resources()).values(); - // assert forall |o: DynamicObjectView| #[trigger] filtered_pods_set.contains(o) implies matching_pods_set.contains(o) by { - // //assume(false); - // } - // assert forall |o: DynamicObjectView| #[trigger] matching_pods_set.contains(o) implies filtered_pods_set.contains(o) by { - // //assume(false); - // } + // We now must prove that the elements of `filtered_pods` are precisely the matching pod + // entries. This is also true by construction. + assert(filtered_pods.map_values(|p: PodView| p.marshal()).to_set() == matching_pod_entries(vrs, s.resources()).values()); } } \ No newline at end of file From 30535a65dbd074b88b845343b02c465309b6ca69 Mon Sep 17 00:00:00 2001 From: Cody Rivera Date: Thu, 31 Oct 2024 16:16:17 -0500 Subject: [PATCH 8/8] Prove API action lemma --- .../vreplicaset_controller/proof/liveness/api_actions.rs | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) 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 4b503b37a..e03f15741 100644 --- a/src/v2/controllers/vreplicaset_controller/proof/liveness/api_actions.rs +++ b/src/v2/controllers/vreplicaset_controller/proof/liveness/api_actions.rs @@ -82,8 +82,6 @@ pub proof fn lemma_api_request_outside_create_or_delete_loop_maintains_matching_ }; } -// TODO: Prove this. -#[verifier(external_body)] pub proof fn lemma_api_request_not_made_by_vrs_maintains_matching_pods( s: ClusterState, s_prime: ClusterState, vrs: VReplicaSetView, cluster: Cluster, controller_id: int, diff: int, msg: Message, req_msg: Option @@ -102,8 +100,6 @@ pub proof fn lemma_api_request_not_made_by_vrs_maintains_matching_pods( helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()(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)), - // forall |diff: usize| !(#[trigger] at_vrs_step_with_vrs(vrs, controller_id, VReplicaSetReconcileStep::AfterDeletePod(diff))(s)), forall |other_id| cluster.controller_models.remove(controller_id).contains_key(other_id) ==> #[trigger] vrs_not_interfered_by(other_id)(s) ensures @@ -149,7 +145,6 @@ pub proof fn lemma_api_request_not_made_by_vrs_maintains_matching_pods( }, _ => {} }; -} - +} }