Add liveness specification for VReplicaSet controller (#497)

Here I state a basic liveness theorem, based on Eventually Stable
Reconciliation, for ReplicaSets. To check whether the cluster state
matches the spec, I gather up all pods that match the label selector
`selector` and are owned by the ReplicaSet into a Verus set. I then
check whether the cardinality of that set is equal to the `replicas`
field.

---------

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

src/controller_examples/v_replica_set_controller/model/mod.rs

@@ -0,0 +1,3 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+pub mod reconciler;

src/controller_examples/v_replica_set_controller/model/reconciler.rs

@@ -0,0 +1,59 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+#![allow(unused_imports)]
+use crate::external_api::spec::*;
+use crate::v_replica_set_controller::trusted::{
+    spec_types::*, step::*,
+};
+use crate::kubernetes_api_objects::spec::prelude::*;
+use crate::reconciler::spec::{io::*, reconciler::*};
+use vstd::{prelude::*, string::*};
+
+verus! {
+
+impl Reconciler<VReplicaSetView, EmptyAPI> for VReplicaSetReconciler {
+    type T = VReplicaSetReconcileState;
+
+    open spec fn reconcile_init_state() -> VReplicaSetReconcileState {
+        reconcile_init_state()
+    }
+
+    open spec fn reconcile_core(fb: VReplicaSetView, resp_o: Option<ResponseView<EmptyTypeView>>, state: VReplicaSetReconcileState)
+    -> (VReplicaSetReconcileState, Option<RequestView<EmptyTypeView>>) {
+        reconcile_core(fb, resp_o, state)
+    }
+
+    open spec fn reconcile_done(state: VReplicaSetReconcileState) -> bool {
+        reconcile_done(state)
+    }
+
+    open spec fn reconcile_error(state: VReplicaSetReconcileState) -> bool {
+        reconcile_error(state)
+    }
+
+    open spec fn expect_from_user(obj: DynamicObjectView) -> bool { false /* expect nothing: stub */ }
+}
+
+pub open spec fn reconcile_init_state() -> VReplicaSetReconcileState { 
+    VReplicaSetReconcileState { 
+        reconcile_step: VReplicaSetReconcileStepView::Init,
+        filtered_pods: None,
+    } 
+}
+
+pub open spec fn reconcile_done(state: VReplicaSetReconcileState) -> bool {
+    false
+}
+
+pub open spec fn reconcile_error(state: VReplicaSetReconcileState) -> bool {
+    false
+}
+
+pub open spec fn reconcile_core(
+    fb: VReplicaSetView, resp_o: Option<ResponseView<EmptyTypeView>>, state: VReplicaSetReconcileState
+) -> (VReplicaSetReconcileState, Option<RequestView<EmptyTypeView>>) {
+    (state, None)
+}
+
+}
+

src/controller_examples/v_replica_set_controller/trusted/liveness_theorem.rs

@@ -0,0 +1,44 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+#![allow(unused_imports)]
+use crate::v_replica_set_controller::trusted::{spec_types::*, step::*};
+use crate::kubernetes_api_objects::spec::prelude::*;
+use crate::kubernetes_cluster::spec::{cluster::*, cluster_state_machine::Step, message::*};
+use crate::temporal_logic::defs::*;
+use crate::vstd_ext::string_view::int_to_string_view;
+use vstd::prelude::*;
+
+verus! {
+
+pub open spec fn liveness_theorem() -> bool { cluster_spec().entails(tla_forall(|vrs: VReplicaSetView| liveness(vrs))) }
+
+pub open spec fn cluster_spec() -> TempPred<VRSCluster> { VRSCluster::sm_spec() }
+
+pub open spec fn liveness(vrs: VReplicaSetView) -> TempPred<VRSCluster> {
+    always(lift_state(desired_state_is(vrs))).leads_to(always(lift_state(current_state_matches(vrs))))
+}
+
+pub open spec fn desired_state_is(vrs: VReplicaSetView) -> StatePred<VRSCluster> { VRSCluster::desired_state_is(vrs) }
+
+pub open spec fn current_state_matches(vrs: VReplicaSetView) -> StatePred<VRSCluster> {
+    |s: VRSCluster| {
+        resource_state_matches(vrs, s.resources())
+    }
+}
+
+pub open spec fn resource_state_matches(vrs: VReplicaSetView, resources: StoredState) -> bool {
+    let pods: Set<ObjectRef> = Set::new(|k: ObjectRef| owned_selector_match_is(vrs, resources, k));
+    &&& pods.finite()
+    &&& pods.len() == vrs.spec.replicas.unwrap_or(0)
+}
+
+pub open spec fn owned_selector_match_is(vrs: VReplicaSetView, resources: StoredState, key: ObjectRef) -> bool {
+    let obj = resources[key];
+    &&& resources.contains_key(key)
+    &&& obj.kind == PodView::kind()
+    &&& 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/controller_examples/v_replica_set_controller/trusted/mod.rs

@@ -1,5 +1,6 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
 pub mod exec_types;
+pub mod liveness_theorem;
 pub mod spec_types;
 pub mod step;