Prove VReplicaSet WF1 Lemmas for Create Path (#571)

Modulo some auxiliary lemmas, this PR provides proofs for WF1 lemmas on
the Create path of the ReplicaSet controller.

---------

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

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)

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());
+}
+
 }

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<Message>
+)
+    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::<VReplicaSetView>()(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()));
+        },
+        _ => {}
+    };
+} 
 
 }

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::*;