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 4c55f84e..64fcf26d 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 d584d1cb..93f229e6 100644 --- a/src/v2/controllers/vreplicaset_controller/proof/helper_lemmas.rs +++ b/src/v2/controllers/vreplicaset_controller/proof/helper_lemmas.rs @@ -11,8 +11,9 @@ 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 crate::vstd_ext::seq_lib::*; use vstd::prelude::*; verus! { @@ -68,4 +69,48 @@ pub proof fn vrs_non_interference_property_equivalent_to_lifted_vrs_non_interfer ); } +// TODO: Prove this lemma. +// 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, + controller_id: int, resp_msg: Message +) + requires + resp_msg_is_the_in_flight_list_resp_at_after_list_pods_step(vrs, controller_id, resp_msg)(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); + + // 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()) + && 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()); + + // 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()); + + // 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 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 8fb6c589..e03f1574 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,70 @@ pub proof fn lemma_api_request_outside_create_or_delete_loop_maintains_matching_ _ => {} }; } - + +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 |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/proof.rs b/src/v2/controllers/vreplicaset_controller/proof/liveness/proof.rs index df4df082..84e0c806 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/controllers/vreplicaset_controller/proof/liveness/resource_match.rs b/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs index 5c4008dc..75780a5f 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::*, 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,498 @@ 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 + ); +} + +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 { + 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), + ); + }); + } + }, + _ => {} + } + } + + 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 + } diff --git a/src/v2/controllers/vreplicaset_controller/proof/predicate.rs b/src/v2/controllers/vreplicaset_controller/proof/predicate.rs index d69437d0..b6d0e4c4 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/v2/kubernetes_cluster/proof/network.rs b/src/v2/kubernetes_cluster/proof/network.rs index 1db8c486..81a59b68 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::*, diff --git a/src/vstd_ext/seq_lib.rs b/src/vstd_ext/seq_lib.rs index 7bb59b84..2db15dc1 100644 --- a/src/vstd_ext/seq_lib.rs +++ b/src/vstd_ext/seq_lib.rs @@ -104,13 +104,23 @@ 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| #[trigger] s.contains(e) ==> !pred(e)) <==> s.filter(pred).len() == 0; // // TODO: Prove this -- Trivial. // // 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. +// + } diff --git a/src/vstd_ext/set_lib.rs b/src/vstd_ext/set_lib.rs index 71eb3941..ab1bb169 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. +// + }