Cleanup and explain unproven assumptions

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

src/controller_examples/v_replica_set_controller/proof/helper_invariants/predicate.rs

@@ -29,14 +29,18 @@ pub open spec fn cluster_resources_is_finite() -> StatePred<VRSCluster> {
     |s: VRSCluster| s.resources().dom().finite()
 } 
 
-// The proof will probabily involve more changes elsewhere.
 pub open spec fn vrs_replicas_bounded(
     vrs: VReplicaSetView
 ) -> StatePred<VRSCluster> {
     |s: VRSCluster| {
         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<VRSCluster> {
     |s: VRSCluster| {
@@ -101,6 +115,12 @@ pub open spec fn every_create_request_is_well_formed() -> StatePred<VRSCluster>
         }
     }
 }
+//
+// 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<VRSCluster> {
     |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.
+//
 
 }

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.
 //
 
 }

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<VRSCluster>, vrs: VReplicaSetView, p: TempPred<VRSCluster>
@@ -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.
+//
 
 }

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<VRSCluster> {
@@ -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.
+//
 
 }

src/vstd_ext/map_lib.rs

@@ -17,9 +17,9 @@ pub proof fn a_submap_of_a_finite_map_is_finite<K, V>(m1: Map<K, V>, m2: Map<K,
         m2.dom().finite(),
     ensures m1.dom().finite();
 //
-// @Xudong Sun take a look.
-// 
-// A submap of a finite map is finite -- prove this by showing m1.dom() <= m2.dom().
+// TODO: Prove this -- Trivial.
+//
+// A submap of a finite map is in turn finite.
 //
 
 

src/vstd_ext/seq_lib.rs

@@ -108,8 +108,8 @@ pub proof fn seq_pred_false_on_all_elements_implies_empty_filter<A>(s: Seq<A>, 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.
 //
 

src/vstd_ext/set_lib.rs

@@ -12,7 +12,7 @@ pub proof fn finite_set_to_seq_contains_all_set_elements<A>(s: Set<A>)
     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.