Port lemmas on controller runtime liveness (#530)

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

src/temporal_logic/defs.rs

@@ -177,4 +177,8 @@ pub open spec fn true_pred<T>() -> TempPred<T> {
     lift_state(|s: T| true)
 }
 
+pub open spec fn false_pred<T>() -> TempPred<T> {
+    lift_state(|s: T| false)
+}
+
 }

src/temporal_logic/rules.rs

@@ -2005,4 +2005,31 @@ proof fn leads_to_rank_step_one_usize_help<T>(spec: TempPred<T>, p: spec_fn(usiz
     }
 }
 
+/// Proving p leads to q vacuously.
+/// pre:
+///     spec |= []r
+///     p /\ r == false
+/// post:
+///     spec |= p ~> q
+pub proof fn vacuous_leads_to<T>(spec: TempPred<T>, p: TempPred<T>, q: TempPred<T>, r: TempPred<T>)
+    requires
+        spec.entails(always(r)),
+        p.and(r) == false_pred::<T>(),
+    ensures
+        spec.entails(p.leads_to(q)),
+{
+    assert forall |ex| #[trigger] spec.satisfied_by(ex) implies p.leads_to(q).satisfied_by(ex) by {
+        assert forall |i| #[trigger] p.satisfied_by(ex.suffix(i)) implies eventually(q).satisfied_by(ex.suffix(i)) by {
+            assert_by(!p.satisfied_by(ex.suffix(i)), {
+                implies_apply::<T>(ex, spec, always(r));
+                assert(r.satisfied_by(ex.suffix(i)));
+                if p.satisfied_by(ex.suffix(i)) {
+                    assert(p.and(r).satisfied_by(ex.suffix(i)));
+                    assert(p.and(r) != false_pred::<T>());
+                }
+            });
+        }
+    }
+}
+
 }

src/v2/kubernetes_cluster/proof/cluster.rs

@@ -25,6 +25,25 @@ pub proof fn lemma_always_there_is_the_controller_state(self, spec: TempPred<Clu
     init_invariant::<ClusterState>(spec, self.init(), self.next(), invariant);
 }
 
+pub open spec fn there_is_the_external_state(controller_id: int) -> StatePred<ClusterState> {
+    |s: ClusterState| {
+        &&& s.controller_and_externals.contains_key(controller_id)
+        &&& s.controller_and_externals[controller_id].external.is_Some()
+    }
+}
+
+pub proof fn lemma_always_there_is_the_external_state_if_external_model_exists(self, spec: TempPred<ClusterState>, controller_id: int)
+    requires
+        spec.entails(lift_state(self.init())),
+        spec.entails(always(lift_action(self.next()))),
+        self.controller_models.contains_key(controller_id),
+        self.controller_models[controller_id].external_model.is_Some(),
+    ensures spec.entails(always(lift_state(Self::there_is_the_external_state(controller_id)))),
+{
+    let invariant = Self::there_is_the_external_state(controller_id);
+    init_invariant::<ClusterState>(spec, self.init(), self.next(), invariant);
+}
+
 }
 
 }

src/v2/kubernetes_cluster/proof/mod.rs

@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: MIT
 pub mod cluster;
 pub mod compositionality;
+pub mod controller_runtime_liveness;
 pub mod failures_liveness;
 pub mod garbage_collector;
 pub mod network;

src/v2/kubernetes_cluster/spec/external/state_machine.rs

@@ -1,13 +1,26 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
 #![allow(unused_imports)]
-use crate::state_machine::action::*;
-use crate::state_machine::state_machine::*;
+use crate::kubernetes_api_objects::spec::prelude::*;
+use crate::state_machine::{action::*, state_machine::*};
 use crate::v2::kubernetes_cluster::spec::{external::types::*, message::*};
 use vstd::{multiset::*, prelude::*};
 
 verus! {
 
+pub open spec fn transition_by_external(model: ExternalModel, req_msg: Message, resources: StoredState, s: ExternalState) -> (ExternalState, Message)
+    recommends
+        req_msg.content.is_ExternalRequest(),
+{
+    let (inner_s_prime, resp) = (model.transition)(req_msg.content.get_ExternalRequest_0(), s.state, resources);
+    let s_prime = ExternalState {
+        state: inner_s_prime,
+        ..s
+    };
+    let resp_msg = form_external_resp_msg(req_msg, resp);
+    (s_prime, resp_msg)
+}
+
 pub open spec fn handle_external_request(model: ExternalModel) -> ExternalAction {
     Action {
         precondition: |input: ExternalActionInput, s: ExternalState| {
@@ -17,12 +30,7 @@ pub open spec fn handle_external_request(model: ExternalModel) -> ExternalAction
         transition: |input: ExternalActionInput, s: ExternalState| {
             let req_msg = input.recv.get_Some_0();
             let resources = input.resources;
-            let (inner_s_prime, resp) = (model.transition)(req_msg.content.get_ExternalRequest_0(), s.state, resources);
-            let s_prime = ExternalState {
-                state: inner_s_prime,
-                ..s
-            };
-            let resp_msg = form_external_resp_msg(req_msg, resp);
+            let (s_prime, resp_msg) = transition_by_external(model, req_msg, resources, s);
             (s_prime, ExternalActionOutput {
                 send: Multiset::singleton(resp_msg),
             })

src/v2/kubernetes_cluster/spec/external/types.rs

@@ -2,10 +2,10 @@
 // SPDX-License-Identifier: MIT
 #![allow(unused_imports)]
 use crate::external_api::spec::*;
-use crate::kubernetes_api_objects::spec::{api_method::*, common::*, dynamic::*};
-use crate::v2::kubernetes_cluster::spec::{message::*, opaque::*};
+use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::state_machine::action::*;
 use crate::state_machine::state_machine::*;
+use crate::v2::kubernetes_cluster::spec::{message::*, opaque::*};
 
 use crate::temporal_logic::defs::*;
 use vstd::{multiset::*, prelude::*};