From 3c05a393cf4f03f5c04f3585ba2bd76518526867 Mon Sep 17 00:00:00 2001 From: Cody Rivera Date: Wed, 11 Sep 2024 13:29:38 -0500 Subject: [PATCH] Cleanup and explain unproven assumptions Signed-off-by: Cody Rivera --- .../proof/helper_invariants/predicate.rs | 52 ++++++++++++- .../proof/liveness/api_actions.rs | 11 ++- .../proof/liveness/resource_match.rs | 76 ++++++------------- .../proof/liveness/spec.rs | 10 +++ src/vstd_ext/map_lib.rs | 6 +- src/vstd_ext/seq_lib.rs | 4 +- src/vstd_ext/set_lib.rs | 2 +- 7 files changed, 93 insertions(+), 68 deletions(-) diff --git a/src/controller_examples/v_replica_set_controller/proof/helper_invariants/predicate.rs b/src/controller_examples/v_replica_set_controller/proof/helper_invariants/predicate.rs index 3935e7f8f..5ba9463df 100644 --- a/src/controller_examples/v_replica_set_controller/proof/helper_invariants/predicate.rs +++ b/src/controller_examples/v_replica_set_controller/proof/helper_invariants/predicate.rs @@ -29,7 +29,6 @@ pub open spec fn cluster_resources_is_finite() -> StatePred { |s: VRSCluster| s.resources().dom().finite() } -// The proof will probabily involve more changes elsewhere. pub open spec fn vrs_replicas_bounded( vrs: VReplicaSetView ) -> StatePred { @@ -37,6 +36,11 @@ pub open spec fn vrs_replicas_bounded( 0 <= vrs.spec.replicas.unwrap_or(0) <= i32::MAX // As allowed by Kubernetes. } } +// +// TODO: Prove this. +// +// This should be easy to enforce with state validation. +// pub open spec fn matching_pods_bounded( vrs: VReplicaSetView @@ -45,6 +49,11 @@ pub open spec fn matching_pods_bounded( 0 <= matching_pod_entries(vrs, s.resources()).len() <= i32::MAX // As allowed by the previous invariant. } } +// +// TODO: Prove this. +// +// This should be easy to enforce with state validation. +// pub open spec fn vrs_selector_matches_template_labels( vrs: VReplicaSetView @@ -61,6 +70,11 @@ pub open spec fn vrs_selector_matches_template_labels( vrs.spec.selector.matches(match_value) } } +// +// TODO: Prove this. +// +// This should be easy to enforce with state validation. +// pub open spec fn every_create_request_is_well_formed() -> StatePred { |s: VRSCluster| { @@ -101,6 +115,12 @@ pub open spec fn every_create_request_is_well_formed() -> StatePred } } } +// +// TODO: Prove this. +// +// Proving this for the VReplicaSet controller should be easy; we'd need to do a similar +// proof for other state machines within the compound state machine. +// pub open spec fn no_pending_update_or_update_status_request_on_pods() -> StatePred { |s: VRSCluster| { @@ -114,7 +134,12 @@ pub open spec fn no_pending_update_or_update_status_request_on_pods() -> StatePr } } } - +// +// TODO: Prove this. +// +// Proving this for the VReplicaSet controller should be easy; we'd need to do a similar +// proof for other state machines within the compound state machine. +// pub open spec fn every_create_matching_pod_request_implies_at_after_create_pod_step( vrs: VReplicaSetView @@ -134,6 +159,12 @@ pub open spec fn every_create_matching_pod_request_implies_at_after_create_pod_s } } } +// +// TODO: Prove this. +// +// We know that if VReplicaSet sends a create matching pod request, that it's at an `AfterCreatePod` state. +// We show this for the other state machines by showing they don't create matching pods. +// pub open spec fn every_delete_matching_pod_request_implies_at_after_delete_pod_step( vrs: VReplicaSetView @@ -155,6 +186,11 @@ pub open spec fn every_delete_matching_pod_request_implies_at_after_delete_pod_s } } } +// +// TODO: Prove this. +// +// The proof sketch for this invariant is similar to the above. +// pub open spec fn at_after_delete_pod_step_implies_filtered_pods_in_matching_pod_entries( vrs: VReplicaSetView @@ -177,5 +213,17 @@ pub open spec fn at_after_delete_pod_step_implies_filtered_pods_in_matching_pod_ } } } +// +// TODO: Prove this. +// +// We prove this by first showing that in the AfterListPods -> AfterDeletePod transition, that +// the `filtered_pods` variable contains matching pods in etcd. Next, we show that for +// AfterDeletePod(diff) => AfterDeletePod(diff - 1), that the pods `filtered_pods[i]`, for +// i = 1..diff - 2 are unaffected, since `filtered_pods[diff - 1]` is deleted, and the invariant +// will hold after `diff` is decreased. +// +// This invariant may have to be moved to a later phase, since I think this invariant will rely +// on other invariants. +// } diff --git a/src/controller_examples/v_replica_set_controller/proof/liveness/api_actions.rs b/src/controller_examples/v_replica_set_controller/proof/liveness/api_actions.rs index 1e739c759..6494ef968 100644 --- a/src/controller_examples/v_replica_set_controller/proof/liveness/api_actions.rs +++ b/src/controller_examples/v_replica_set_controller/proof/liveness/api_actions.rs @@ -74,16 +74,13 @@ pub proof fn lemma_api_request_outside_create_or_delete_loop_maintains_matching_ } #[verifier(external_body)] -pub proof fn lemma_api_request_not_on_matching_pods_maintains_matching_pods( +pub proof fn lemma_api_request_not_made_by_vrs_maintains_matching_pods( s: VRSCluster, s_prime: VRSCluster, vrs: VReplicaSetView, diff: int, msg: VRSMessage, req_msg: VRSMessage, ) requires msg != req_msg, req_msg == s.ongoing_reconciles()[vrs.object_ref()].pending_req_msg.get_Some_0(), VRSCluster::next_step(s, s_prime, Step::ApiServerStep(Some(msg))), - VRSCluster::crash_disabled()(s), - VRSCluster::busy_disabled()(s), - VRSCluster::every_in_flight_msg_has_unique_id()(s), VRSCluster::each_object_in_etcd_is_well_formed()(s), helper_invariants::every_create_request_is_well_formed()(s), helper_invariants::no_pending_update_or_update_status_request_on_pods()(s), @@ -92,10 +89,12 @@ pub proof fn lemma_api_request_not_on_matching_pods_maintains_matching_pods( ensures matching_pod_entries(vrs, s.resources()) == matching_pod_entries(vrs, s_prime.resources()); // -// @Xudong Sun take a look +// TODO: Prove this. // // This is very similar to the proof above, but we'll need to explicitly handle the case that we're on -// an after create or delete pod step. +// an after create or delete pod step. But fortunately, `every_create` and `every_delete` require that +// every create/delete matching pod request is VRS's pending request message, which clearly `msg` +// is not. // } 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 6fb4a0f33..4c3af685d 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 @@ -20,7 +20,10 @@ use crate::v_replica_set_controller::{ proof::{helper_invariants, predicate::*, liveness::api_actions::*}, trusted::{spec_types::*, step::*, liveness_theorem::*}, }; -use vstd::{prelude::*, seq::*, seq_lib::*, set_lib::*, string::*, map::*, map_lib::*, math::abs}; +use vstd::{ + prelude::*, seq::*, seq_lib::*, set_lib::*, + string::*, map::*, map_lib::*, math::abs +}; verus! { @@ -37,8 +40,6 @@ pub proof fn lemma_from_diff_and_init_to_current_state_matches( spec.entails(always(lift_state(VRSCluster::each_object_in_etcd_is_well_formed()))), spec.entails(always(lift_state(VRSCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()))), spec.entails(always(lift_state(VRSCluster::pending_req_of_key_is_unique_with_unique_id(vrs.object_ref())))), - spec.entails(always(lift_state(VRSCluster::no_pending_req_msg_at_reconcile_state( - vrs.object_ref(), |s: VReplicaSetReconcileState| s.reconcile_step == VReplicaSetReconcileStep::Init)))), 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::matching_pods_bounded(vrs)))), @@ -68,8 +69,6 @@ pub proof fn lemma_from_diff_and_init_to_current_state_matches( &&& spec.entails(always(lift_state(VRSCluster::each_object_in_etcd_is_well_formed()))) &&& spec.entails(always(lift_state(VRSCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()))) &&& spec.entails(always(lift_state(VRSCluster::pending_req_of_key_is_unique_with_unique_id(vrs.object_ref())))) - &&& spec.entails(always(lift_state(VRSCluster::no_pending_req_msg_at_reconcile_state( - vrs.object_ref(), |s: VReplicaSetReconcileState| s.reconcile_step == VReplicaSetReconcileStep::Init)))) &&& 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::matching_pods_bounded(vrs)))) @@ -302,8 +301,6 @@ pub proof fn lemma_from_init_step_to_send_list_pods_req( spec.entails(always(lift_state(VRSCluster::busy_disabled()))), spec.entails(always(lift_state(VRSCluster::every_in_flight_msg_has_unique_id()))), spec.entails(always(lift_state(VRSCluster::each_object_in_etcd_is_well_formed()))), - spec.entails(always(lift_state(VRSCluster::no_pending_req_msg_at_reconcile_state( - vrs.object_ref(), |s: VReplicaSetReconcileState| s.reconcile_step == VReplicaSetReconcileStep::Init)))), spec.entails(always(lift_state(helper_invariants::every_create_request_is_well_formed()))), spec.entails(always(lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()))), spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs)))), @@ -340,8 +337,6 @@ pub proof fn lemma_from_init_step_to_send_list_pods_req( &&& VRSCluster::busy_disabled()(s) &&& VRSCluster::every_in_flight_msg_has_unique_id()(s) &&& VRSCluster::each_object_in_etcd_is_well_formed()(s) - &&& VRSCluster::no_pending_req_msg_at_reconcile_state(vrs.object_ref(), - |s: VReplicaSetReconcileState| s.reconcile_step == VReplicaSetReconcileStep::Init)(s) &&& helper_invariants::every_create_request_is_well_formed()(s) &&& helper_invariants::no_pending_update_or_update_status_request_on_pods()(s) &&& helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs)(s) @@ -355,7 +350,6 @@ pub proof fn lemma_from_init_step_to_send_list_pods_req( lift_state(VRSCluster::busy_disabled()), lift_state(VRSCluster::every_in_flight_msg_has_unique_id()), lift_state(VRSCluster::each_object_in_etcd_is_well_formed()), - lift_state(VRSCluster::no_pending_req_msg_at_reconcile_state(vrs.object_ref(), state_is_init)), lift_state(helper_invariants::every_create_request_is_well_formed()), lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()), lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs)), @@ -604,24 +598,6 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_receive_create_pod_resp( ) ), { - let invariants = { - &&& spec.entails(always(lift_action(VRSCluster::next()))) - &&& spec.entails(tla_forall(|i| VRSCluster::controller_next().weak_fairness(i))) - &&& spec.entails(tla_forall(|i| VRSCluster::kubernetes_api_next().weak_fairness(i))) - &&& spec.entails(always(lift_state(VRSCluster::crash_disabled()))) - &&& spec.entails(always(lift_state(VRSCluster::busy_disabled()))) - &&& spec.entails(always(lift_state(VRSCluster::every_in_flight_msg_has_unique_id()))) - &&& spec.entails(always(lift_state(VRSCluster::each_object_in_etcd_is_well_formed()))) - &&& spec.entails(always(lift_state(VRSCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()))) - &&& spec.entails(always(lift_state(VRSCluster::pending_req_of_key_is_unique_with_unique_id(vrs.object_ref())))) - &&& 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::vrs_selector_matches_template_labels(vrs)))) - &&& spec.entails(always(lift_state(helper_invariants::every_create_request_is_well_formed()))) - &&& spec.entails(always(lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()))) - &&& spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs)))) - &&& spec.entails(always(lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs)))) - }; let list_resp = |diff: int| lift_state( |s: VRSCluster| { &&& exists_resp_in_flight_at_after_list_pods_step(vrs)(s) @@ -754,24 +730,6 @@ pub proof fn lemma_from_after_receive_create_pod_resp_to_receive_create_pod_resp ) ), { - let invariants = { - &&& spec.entails(always(lift_action(VRSCluster::next()))) - &&& spec.entails(tla_forall(|i| VRSCluster::controller_next().weak_fairness(i))) - &&& spec.entails(tla_forall(|i| VRSCluster::kubernetes_api_next().weak_fairness(i))) - &&& spec.entails(always(lift_state(VRSCluster::crash_disabled()))) - &&& spec.entails(always(lift_state(VRSCluster::busy_disabled()))) - &&& spec.entails(always(lift_state(VRSCluster::every_in_flight_msg_has_unique_id()))) - &&& spec.entails(always(lift_state(VRSCluster::each_object_in_etcd_is_well_formed()))) - &&& spec.entails(always(lift_state(VRSCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()))) - &&& spec.entails(always(lift_state(VRSCluster::pending_req_of_key_is_unique_with_unique_id(vrs.object_ref())))) - &&& 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::vrs_selector_matches_template_labels(vrs)))) - &&& spec.entails(always(lift_state(helper_invariants::every_create_request_is_well_formed()))) - &&& spec.entails(always(lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()))) - &&& spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs)))) - &&& spec.entails(always(lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs)))) - }; let create_req_msg = |req_msg: VRSMessage, diff: int| lift_state(|s: VRSCluster| { &&& req_msg_is_the_in_flight_create_request_at_after_create_pod_step(vrs, req_msg, (abs(diff) - 1) as nat)(s) &&& num_diff_pods_is(vrs, diff)(s) @@ -963,11 +921,11 @@ pub proof fn lemma_filtered_pods_len_equals_matching_pods_len( }), {} // -// @Xudong Sun take a look. +// TODO: Prove this. // // filter_pods filters pods in a very similar way to matching_pods, but the former // works on a sequence of PodViews, while the latter works on the key-value store directly. -// I'll probably come back to this soon. +// I need to do some manual effort to make the two representations work together. // @@ -1091,7 +1049,7 @@ pub proof fn lemma_from_after_send_create_pod_req_to_receive_ok_resp( 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_on_matching_pods_maintains_matching_pods( + lemma_api_request_not_made_by_vrs_maintains_matching_pods( s, s_prime, vrs, diff, msg, req_msg, ); assert(matching_pod_entries(vrs, s.resources()) == matching_pod_entries(vrs, s_prime.resources())); } @@ -1618,7 +1576,14 @@ pub proof fn lemma_filtered_pods_set_equals_matching_pods( }), {} // -// This might actually be slightly trickier than the previous one. +// TODO: Prove this. +// +// filter_pods filters pods in a very similar way to matching_pods, but the former +// works on a sequence of PodViews, while the latter works on the key-value store directly. +// I need to do some manual effort to make the two representations work together. +// +// Once proven, this will supplant the earlier lemma +// lemma_filtered_pods_len_equals_matching_pods_len. // @@ -1716,7 +1681,7 @@ pub proof fn lemma_from_after_send_delete_pod_req_to_receive_ok_resp( assert(matching_pod_entries(vrs, s.resources()).remove(key) == 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_on_matching_pods_maintains_matching_pods( + lemma_api_request_not_made_by_vrs_maintains_matching_pods( s, s_prime, vrs, diff, msg, req_msg, ); assert(matching_pod_entries(vrs, s.resources()) == matching_pod_entries(vrs, s_prime.resources())); @@ -1849,9 +1814,6 @@ pub proof fn lemma_from_after_receive_ok_resp_to_send_delete_pod_req( ); } -// Ensures that once we've reconciled, we stay reconciled. - -// This is actually trickier than I thought it'd be... #[verifier(external_body)] pub proof fn lemma_current_state_matches_is_stable( spec: TempPred, vrs: VReplicaSetView, p: TempPred @@ -1903,5 +1865,11 @@ pub proof fn lemma_current_state_matches_is_stable( leads_to_stable_temp(spec, lift_action(stronger_next), p, lift_state(post)); } +// +// TODO: Prove this. +// +// The earlier controllers only created resources and never deleted them, so stability of reconciliation +// was trivial, while it seems more difficult here since the controller can delete resources. +// } diff --git a/src/controller_examples/v_replica_set_controller/proof/liveness/spec.rs b/src/controller_examples/v_replica_set_controller/proof/liveness/spec.rs index dc68220d6..868ed8d5a 100644 --- a/src/controller_examples/v_replica_set_controller/proof/liveness/spec.rs +++ b/src/controller_examples/v_replica_set_controller/proof/liveness/spec.rs @@ -77,6 +77,11 @@ pub proof fn assumption_and_invariants_of_all_phases_is_stable(vrs: VReplicaSetV forall |i: nat| 1 <= i <= 8 ==> valid(stable(#[trigger] spec_before_phase_n(i, vrs))), { } +// +// TODO: Prove this. +// +// Main body for showing invariant stability. +// // Next and all the wf conditions. pub open spec fn next_with_wf() -> TempPred { @@ -165,5 +170,10 @@ pub proof fn sm_spec_entails_all_invariants(vrs: VReplicaSetView) ensures cluster_spec().entails(derived_invariants_since_beginning(vrs)), { } +// +// TODO: Prove this. +// +// Main body for showing that invariants hold. +// } diff --git a/src/vstd_ext/map_lib.rs b/src/vstd_ext/map_lib.rs index 755f3c991..2a2bb3acd 100644 --- a/src/vstd_ext/map_lib.rs +++ b/src/vstd_ext/map_lib.rs @@ -17,9 +17,9 @@ pub proof fn a_submap_of_a_finite_map_is_finite(m1: Map, m2: Map(s: Seq, p requires forall |e: A| #![auto] s.contains(e) ==> !pred(e), ensures s.filter(pred).len() == 0; // -// @Xudong Sun take a look. -// +// TODO: Prove this -- Trivial. +// // If `pred` is false on every element, filter will return an empty sequence. // diff --git a/src/vstd_ext/set_lib.rs b/src/vstd_ext/set_lib.rs index 229148ff2..71eb39413 100644 --- a/src/vstd_ext/set_lib.rs +++ b/src/vstd_ext/set_lib.rs @@ -12,7 +12,7 @@ pub proof fn finite_set_to_seq_contains_all_set_elements(s: Set) requires s.finite(), ensures forall |e: A| #![auto] s.contains(e) <==> s.to_seq().contains(e); // -// @Xudong Sun take a look. +// TODO: Prove this -- Trivial. // // Anything in a finite set will be in a sequence composed of its elements; likewise // anything in that constructed sequence will be part of the original set.