Add the liveness theorem for the consumer controller (#507)

Signed-off-by: Xudong Sun <[email protected]>

src/controller_examples/composition_example/consumer_controller/trusted/liveness_theorem.rs

@@ -0,0 +1,50 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+#![allow(unused_imports)]
+use crate::consumer_controller::trusted::{spec_types::*, step::*};
+use crate::kubernetes_api_objects::spec::{container::*, prelude::*};
+use crate::kubernetes_cluster::spec::{cluster::*, cluster_state_machine::Step, message::*};
+use crate::temporal_logic::defs::*;
+use vstd::prelude::*;
+
+verus! {
+
+pub open spec fn liveness_theorem() -> bool { cluster_spec().entails(tla_forall(|consumer: ConsumerView| liveness(consumer))) }
+
+pub open spec fn cluster_spec() -> TempPred<CCluster> { CCluster::sm_spec() }
+
+pub open spec fn liveness(consumer: ConsumerView) -> TempPred<CCluster> {
+    always(lift_state(CCluster::desired_state_is(consumer))).leads_to(always(lift_state(current_state_matches(consumer))))
+}
+
+pub open spec fn current_state_matches(consumer: ConsumerView) -> StatePred<CCluster> {
+    |s: CCluster| {
+        let obj = s.resources()[pod_key(consumer)];
+        let pod = PodView::unmarshal(obj).get_Ok_0();
+        &&& s.resources().contains_key(pod_key(consumer))
+        &&& PodView::unmarshal(obj).is_Ok()
+        &&& pod.metadata.labels.get_Some_0().contains_pair("consumer_message"@, consumer.spec.message)
+        &&& pod.spec == Some(PodSpecView {
+                containers: seq![ContainerView {
+                    name: "nginx"@,
+                    image: Some("nginx:1.14.2"@),
+                    ports: Some(seq![ContainerPortView {
+                        container_port: 80,
+                        ..ContainerPortView::default()
+                    }]),
+                    ..ContainerView::default()
+                }],
+                ..PodSpecView::default()
+            })
+    }
+}
+
+pub open spec fn pod_key(consumer: ConsumerView) -> ObjectRef {
+    ObjectRef {
+        name: consumer.metadata.name.get_Some_0(),
+        namespace: consumer.metadata.namespace.get_Some_0(),
+        kind: Kind::PodKind,
+    }
+}
+
+}

src/controller_examples/composition_example/consumer_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;

src/controller_examples/composition_example/consumer_controller/trusted/spec_types.rs

@@ -10,11 +10,11 @@ use vstd::prelude::*;
 
 verus! {
 
-pub type VRSStep = Step<VRSMessage>;
+pub type CStep = Step<CMessage>;
 
-pub type VRSCluster = Cluster<ConsumerView, EmptyAPI, ConsumerReconciler>;
+pub type CCluster = Cluster<ConsumerView, EmptyAPI, ConsumerReconciler>;
 
-pub type VRSMessage = Message<EmptyTypeView, EmptyTypeView>;
+pub type CMessage = Message<EmptyTypeView, EmptyTypeView>;
 
 pub struct ConsumerReconciler {}