Prove key invariants for VReplicaSet possibly involving PodEvent (#549)

The following invariants have been proven:
`every_create_matching_pod_request_implies_at_after_create_pod_step`
`every_delete_matching_pod_request_implies_at_after_delete_pod_step`
(partially).

Investigating the latter led to addition of delete preconditions to the
V2 state machine to which the controller will be ported.

---------

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

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

@@ -25,6 +25,10 @@ use vstd::{multiset::*, prelude::*, string::*};
 
 verus! {
 
+pub open spec fn vrs_is_well_formed(vrs: VReplicaSetView) -> StatePred<VRSCluster> {
+    |s: VRSCluster| vrs.well_formed()
+}
+
 pub open spec fn cluster_resources_is_finite() -> StatePred<VRSCluster> {
     |s: VRSCluster| s.resources().dom().finite()
 } 
@@ -109,6 +113,7 @@ pub open spec fn every_create_request_is_well_formed() -> StatePred<VRSCluster>
                 status: marshalled_default_status::<VReplicaSetView>(req.obj.kind), // Overwrite the status with the default one
             };
             &&& obj.metadata.deletion_timestamp.is_None()
+            &&& obj.metadata.namespace.is_Some()
             &&& content.get_create_request().namespace == obj.metadata.namespace.unwrap()
             &&& unmarshallable_object::<VReplicaSetView>(obj)
             &&& created_object_validity_check::<VReplicaSetView>(created_obj).is_none()
@@ -192,6 +197,32 @@ pub open spec fn every_delete_matching_pod_request_implies_at_after_delete_pod_s
 // The proof sketch for this invariant is similar to the above.
 //
 
+pub open spec fn each_vrs_in_reconcile_implies_filtered_pods_owned_by_vrs_if_in_etcd() -> StatePred<VRSCluster> {
+    |s: VRSCluster| {
+        forall |key: ObjectRef|
+            #[trigger] s.ongoing_reconciles().contains_key(key)
+            ==> {
+                let state = s.ongoing_reconciles()[key].local_state; 
+                let filtered_pods = state.filtered_pods.unwrap();
+                &&& s.ongoing_reconciles()[key].triggering_cr.object_ref() == key
+                &&& s.ongoing_reconciles()[key].triggering_cr.metadata().well_formed()
+                &&& state.filtered_pods.is_Some()
+                // Maintained across deletes, 
+                // maintained across creates since all new keys with generate_name
+                // are unique, maintained across updates since there are
+                // no updates.
+                &&& forall |i| #![auto] 0 <= i < filtered_pods.len() ==>
+                    (
+                        filtered_pods[i].object_ref().namespace == s.ongoing_reconciles()[key].triggering_cr.metadata.namespace.unwrap()
+                        && (s.resources().contains_key(filtered_pods[i].object_ref()) ==>
+                            s.resources()[filtered_pods[i].object_ref()].metadata.owner_references_contains(
+                                s.ongoing_reconciles()[key].triggering_cr.controller_owner_ref()
+                            ))
+                    )
+            }
+    }
+}
+
 pub open spec fn at_after_delete_pod_step_implies_filtered_pods_in_matching_pod_entries(
     vrs: VReplicaSetView
 ) -> StatePred<VRSCluster> {

src/controller_examples/v_replica_set_controller/proof/liveness/resource_match.rs

@@ -16,7 +16,7 @@ use crate::kubernetes_cluster::spec::{
 use crate::temporal_logic::{defs::*, rules::*};
 use crate::v_replica_set_controller::{
     model::reconciler::*,
-    proof::{helper_invariants, liveness::api_actions::*, predicate::*},
+    proof::{utility_lemmas::*, helper_invariants, liveness::api_actions::*, predicate::*},
     trusted::{liveness_theorem::*, spec_types::*, step::*},
 };
 use crate::vstd_ext::{map_lib::*, seq_lib::*, set_lib::*, string_view::*};

src/controller_examples/v_replica_set_controller/proof/liveness/spec.rs

@@ -100,6 +100,7 @@ pub proof fn spec_of_previous_phases_entails_eventually_new_invariants(i: nat, v
     }
 }
 
+
 #[verifier(external_body)]
 pub proof fn assumption_and_invariants_of_all_phases_is_stable(vrs: VReplicaSetView)
     ensures

src/controller_examples/v_replica_set_controller/proof/mod.rs

@@ -3,3 +3,4 @@
 pub mod helper_invariants;
 pub mod liveness;
 pub mod predicate;
+pub mod utility_lemmas;

src/controller_examples/v_replica_set_controller/proof/utility_lemmas.rs

@@ -0,0 +1,52 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+#![allow(unused_imports)]
+use crate::kubernetes_api_objects::spec::{
+    api_method::*, common::*, prelude::*, resource::*, stateful_set::*,
+};
+use crate::kubernetes_cluster::proof::controller_runtime::*;
+use crate::kubernetes_cluster::spec::{
+    cluster::*,
+    cluster_state_machine::Step,
+    controller::types::{ControllerActionInput, ControllerStep},
+    message::*,
+};
+use crate::temporal_logic::defs::*;
+use crate::v_replica_set_controller::model::{reconciler::*};
+use crate::v_replica_set_controller::trusted::{
+    liveness_theorem::*, spec_types::*, step::*,
+};
+use crate::v_replica_set_controller::proof::{
+    predicate::*,
+};
+use vstd::{prelude::*, math::abs};
+
+verus! {
+
+#[verifier(external_body)]
+pub proof fn lemma_filtered_pods_set_equals_matching_pods(
+    s: VRSCluster, vrs: VReplicaSetView, resp_msg: VRSMessage
+)
+    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()
+        }),
+{}
+//
+// 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.
+//
+
+}

src/controller_examples/v_replica_set_controller/trusted/liveness_theorem.rs

@@ -37,7 +37,8 @@ pub open spec fn resource_state_matches(vrs: VReplicaSetView, resources: StoredS
 
 pub open spec fn owned_selector_match_is(vrs: VReplicaSetView, obj: DynamicObjectView) -> bool {
     &&& obj.kind == PodView::kind()
-    &&& obj.metadata.namespace.unwrap() == vrs.metadata.namespace.unwrap()
+    &&& obj.metadata.namespace.is_Some()
+    &&& obj.metadata.namespace == vrs.metadata.namespace
     &&& obj.metadata.owner_references_contains(vrs.controller_owner_ref())
     &&& vrs.spec.selector.matches(obj.metadata.labels.unwrap_or(Map::empty()))
     &&& obj.metadata.deletion_timestamp.is_None()

src/kubernetes_cluster/proof/cluster_safety.rs

@@ -107,6 +107,22 @@ pub proof fn lemma_always_each_object_in_etcd_is_well_formed(spec: TempPred<Self
     init_invariant(spec, Self::init(), Self::next(), invariant);
 }
 
+// TODO: Prove this.
+pub open spec fn each_object_in_etcd_has_at_most_one_controller_owner() -> StatePred<Self> {
+    |s: Self| {
+        forall |key: ObjectRef|
+            #[trigger] s.resources().contains_key(key)
+                ==> {
+                    let obj = s.resources()[key];
+                    let owners = obj.metadata.owner_references.get_Some_0();
+                    let controller_owners = owners.filter(
+                        |o: OwnerReferenceView| o.controller.is_Some() && o.controller.get_Some_0()
+                    );
+                    obj.metadata.owner_references.is_Some() ==> controller_owners.len() <= 1
+                }
+    }
+}
+
 pub open spec fn each_scheduled_object_has_consistent_key_and_valid_metadata() -> StatePred<Self> {
     |s: Self| {
         forall |key: ObjectRef|