Port lemmas on network liveness (#527)

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

src/kubernetes_cluster/proof/api_server_liveness.rs

@@ -63,142 +63,6 @@ pub proof fn lemma_pre_leads_to_post_by_builtin_controllers(
     Self::builtin_controllers_next().wf1(input, spec, next, pre, post);
 }
 
-pub proof fn lemma_pre_leads_to_post_by_builtin_controllers_borrow_from_spec(
-    spec: TempPred<Self>, input: (BuiltinControllerChoice, ObjectRef), next: ActionPred<Self>, action: BuiltinControllersAction<E::Input, E::Output>, c: StatePred<Self>, pre: StatePred<Self>, post: StatePred<Self>
-)
-    requires
-        Self::builtin_controllers().actions.contains(action),
-        forall |s, s_prime: Self| pre(s) && c(s) && #[trigger] next(s, s_prime) ==> pre(s_prime) || post(s_prime),
-        forall |s, s_prime: Self| pre(s) && c(s) && #[trigger] next(s, s_prime) && Self::builtin_controllers_next().forward(input)(s, s_prime) ==> post(s_prime),
-        forall |s: Self| #[trigger] pre(s) && c(s) ==> Self::builtin_controllers_action_pre(action, input)(s),
-        spec.entails(always(lift_action(next))),
-        spec.entails(tla_forall(|i| Self::builtin_controllers_next().weak_fairness(i))),
-        spec.entails(always(lift_state(c))),
-    ensures spec.entails(lift_state(pre).leads_to(lift_state(post))),
-{
-    use_tla_forall::<Self, (BuiltinControllerChoice, ObjectRef)>(spec, |i| Self::builtin_controllers_next().weak_fairness(i), input);
-    Self::builtin_controllers_action_pre_implies_next_pre(action, input);
-    valid_implies_trans::<Self>(
-        lift_state(pre).and(lift_state(c)),
-        lift_state(Self::builtin_controllers_action_pre(action, input)),
-        lift_state(Self::builtin_controllers_next().pre(input))
-    );
-    Self::builtin_controllers_next().wf1_borrow_from_spec(input, spec, next, c, pre, post);
-}
-
-pub proof fn lemma_get_req_leads_to_some_resp(spec: TempPred<Self>, msg: MsgType<E>, key: ObjectRef)
-    requires
-        spec.entails(always(lift_action(Self::next()))),
-        spec.entails(tla_forall(|i| Self::kubernetes_api_next().weak_fairness(i))),
-    ensures
-        spec.entails(lift_state(|s: Self| {
-                    &&& s.in_flight().contains(msg)
-                    &&& msg.dst == HostId::ApiServer
-                    &&& msg.content.is_get_request()
-                    &&& msg.content.get_get_request().key == key
-            }).leads_to(lift_state(|s: Self|
-                exists |resp_msg: MsgType<E>| {
-                    &&& #[trigger] s.in_flight().contains(resp_msg)
-                    &&& Message::resp_msg_matches_req_msg(resp_msg, msg)}))),
-{
-    let input = Some(msg);
-    let pre = |s: Self| {
-        &&& s.in_flight().contains(msg)
-        &&& msg.dst == HostId::ApiServer
-        &&& msg.content.is_get_request()
-        &&& msg.content.get_get_request().key == key
-    };
-    let post = |s: Self| exists |resp_msg: MsgType<E>| {
-        &&& #[trigger] s.in_flight().contains(resp_msg)
-        &&& Message::resp_msg_matches_req_msg(resp_msg, msg)
-    };
-    assert forall |s, s_prime: Self| pre(s) && #[trigger] Self::next()(s, s_prime) implies
-    pre(s_prime) || post(s_prime) by {
-        let step = choose |step| Self::next_step(s, s_prime, step);
-        match step {
-            Step::ApiServerStep(input) => {
-                if input.get_Some_0() == msg {
-                    if s.resources().contains_key(key) {
-                        let ok_resp_msg = Message::form_get_resp_msg(msg, GetResponse{res: Ok(s.resources()[key])});
-                        assert(s_prime.in_flight().contains(ok_resp_msg));
-                        assert(Message::resp_msg_matches_req_msg(ok_resp_msg, msg));
-                    } else {
-                        let err_resp_msg = Message::form_get_resp_msg(msg, GetResponse{res: Err(APIError::ObjectNotFound)});
-                        assert(s_prime.in_flight().contains(err_resp_msg));
-                        assert(Message::resp_msg_matches_req_msg(err_resp_msg, msg));
-                    }
-                } else {
-                    assert(pre(s_prime));
-                }
-            },
-            Step::FailTransientlyStep(input) => {
-                if input.0 == msg {
-                    let resp = Message::form_matched_err_resp_msg(msg, input.1);
-                    assert(s_prime.in_flight().contains(resp));
-                    assert(Message::resp_msg_matches_req_msg(resp, msg));
-                    assert(post(s_prime));
-                } else {
-                    assert(pre(s_prime));
-                }
-            },
-            _ => assert(pre(s_prime)),
-        }
-    }
-    assert forall |s, s_prime: Self|
-        pre(s) && #[trigger] Self::next()(s, s_prime) && Self::kubernetes_api_next().forward(input)(s, s_prime)
-    implies post(s_prime) by {
-        if s.resources().contains_key(key) {
-            let ok_resp_msg = Message::form_get_resp_msg(msg, GetResponse{res: Ok(s.resources()[key])});
-            assert(s_prime.in_flight().contains(ok_resp_msg));
-            assert(Message::resp_msg_matches_req_msg(ok_resp_msg, msg));
-        } else {
-            let err_resp_msg = Message::form_get_resp_msg(msg, GetResponse{res: Err(APIError::ObjectNotFound)});
-            assert(s_prime.in_flight().contains(err_resp_msg));
-            assert(Message::resp_msg_matches_req_msg(err_resp_msg, msg));
-        }
-    };
-    Self::lemma_pre_leads_to_post_by_kubernetes_api(spec, input, Self::next(), Self::handle_request(), pre, post);
-}
-
-pub proof fn lemma_get_req_leads_to_ok_or_err_resp(spec: TempPred<Self>, msg: MsgType<E>, key: ObjectRef)
-    requires
-        spec.entails(always(lift_state(Self::busy_disabled()))),
-        spec.entails(always(lift_action(Self::next()))),
-        spec.entails(tla_forall(|i| Self::kubernetes_api_next().weak_fairness(i))),
-    ensures
-        spec.entails(lift_state(|s: Self| {
-            &&& s.in_flight().contains(msg)
-            &&& msg.dst == HostId::ApiServer
-            &&& msg.content.is_get_request()
-            &&& msg.content.get_get_request().key == key
-        }).leads_to(
-                lift_state(|s: Self| s.in_flight().contains(Message::form_get_resp_msg(msg, GetResponse{res: Ok(s.resources()[key])})))
-                .or(lift_state(|s: Self| s.in_flight().contains(Message::form_get_resp_msg(msg, GetResponse{res: Err(APIError::ObjectNotFound)}))))
-        )),
-{
-    let pre = |s: Self| {
-        &&& s.in_flight().contains(msg)
-        &&& msg.dst == HostId::ApiServer
-        &&& msg.content.is_get_request()
-        &&& msg.content.get_get_request().key == key
-    };
-    let post = |s: Self| {
-        ||| s.in_flight().contains(Message::form_get_resp_msg(msg, GetResponse{res: Ok(s.resources()[key])}))
-        ||| s.in_flight().contains(Message::form_get_resp_msg(msg, GetResponse{res: Err(APIError::ObjectNotFound)}))
-    };
-    let stronger_next = |s, s_prime: Self| {
-        Self::next()(s, s_prime)
-        && !s.transient_failure_enabled
-    };
-    strengthen_next::<Self>(spec, Self::next(), Self::busy_disabled(), stronger_next);
-    Self::lemma_pre_leads_to_post_by_kubernetes_api(spec, Some(msg), stronger_next, Self::handle_request(), pre, post);
-    temp_pred_equality::<Self>(
-        lift_state(post),
-        lift_state(|s: Self| s.in_flight().contains(Message::form_get_resp_msg(msg, GetResponse{res: Ok(s.resources()[key])})))
-        .or(lift_state(|s: Self| s.in_flight().contains(Message::form_get_resp_msg(msg, GetResponse{res: Err(APIError::ObjectNotFound)}))))
-    );
-}
-
 pub open spec fn no_req_before_rest_id_is_in_flight(rest_id: RestId) -> StatePred<Self> {
     |s: Self| {
         forall |msg: MsgType<E>| !{

src/v2/kubernetes_cluster/proof/api_server_liveness.rs

@@ -0,0 +1,38 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+#![allow(unused_imports)]
+use crate::kubernetes_api_objects::spec::prelude::*;
+use crate::temporal_logic::{defs::*, rules::*};
+use crate::v2::kubernetes_cluster::spec::{
+    api_server::types::*, cluster_state_machine::*, message::*,
+};
+use vstd::prelude::*;
+
+verus! {
+
+impl Cluster {
+
+pub proof fn lemma_pre_leads_to_post_by_api_server(
+    self, spec: TempPred<ClusterState>, input: Option<Message>, next: ActionPred<ClusterState>, step: APIServerStep, pre: StatePred<ClusterState>, post: StatePred<ClusterState>
+)
+    requires
+        forall |s, s_prime| pre(s) && #[trigger] next(s, s_prime) ==> pre(s_prime) || post(s_prime),
+        forall |s, s_prime| pre(s) && #[trigger] next(s, s_prime) && self.api_server_next().forward(input)(s, s_prime) ==> post(s_prime),
+        forall |s| #[trigger] pre(s) ==> self.api_server_action_pre(step, input)(s),
+        spec.entails(always(lift_action(next))),
+        spec.entails(tla_forall(|i| self.api_server_next().weak_fairness(i))),
+    ensures spec.entails(lift_state(pre).leads_to(lift_state(post))),
+{
+    use_tla_forall::<ClusterState, Option<Message>>(spec, |i| self.api_server_next().weak_fairness(i), input);
+    self.api_server_action_pre_implies_next_pre(step, input);
+    valid_implies_trans::<ClusterState>(
+        lift_state(pre),
+        lift_state(self.api_server_action_pre(step, input)),
+        lift_state(self.api_server_next().pre(input))
+    );
+    self.api_server_next().wf1(input, spec, next, pre, post);
+}
+
+}
+
+}

src/v2/kubernetes_cluster/proof/external_liveness.rs

@@ -0,0 +1,39 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+#![allow(unused_imports)]
+use crate::kubernetes_api_objects::spec::prelude::*;
+use crate::temporal_logic::{defs::*, rules::*};
+use crate::v2::kubernetes_cluster::spec::{
+    cluster_state_machine::*, external::types::*, message::*,
+};
+use vstd::prelude::*;
+
+verus! {
+
+impl Cluster {
+
+pub proof fn lemma_pre_leads_to_post_by_external(
+    self, spec: TempPred<ClusterState>, controller_id: int, input: Option<Message>, next: ActionPred<ClusterState>,
+    step: ExternalStep, pre: StatePred<ClusterState>, post: StatePred<ClusterState>
+)
+    requires
+        forall |s, s_prime| pre(s) && #[trigger] next(s, s_prime) ==> pre(s_prime) || post(s_prime),
+        forall |s, s_prime| pre(s) && #[trigger] next(s, s_prime) && self.external_next().forward((controller_id, input))(s, s_prime) ==> post(s_prime),
+        forall |s| #[trigger] pre(s) ==> self.external_action_pre(step, (controller_id, input))(s),
+        spec.entails(always(lift_action(next))),
+        spec.entails(tla_forall(|i| self.external_next().weak_fairness((controller_id, i)))),
+    ensures spec.entails(lift_state(pre).leads_to(lift_state(post))),
+{
+    use_tla_forall::<ClusterState, Option<Message>>(spec, |i| self.external_next().weak_fairness((controller_id, i)), input);
+    self.external_action_pre_implies_next_pre(step, (controller_id, input));
+    valid_implies_trans::<ClusterState>(
+        lift_state(pre),
+        lift_state(self.external_action_pre(step, (controller_id, input))),
+        lift_state(self.external_next().pre((controller_id, input)))
+    );
+    self.external_next().wf1((controller_id, input), spec, next, pre, post);
+}
+
+}
+
+}

src/v2/kubernetes_cluster/proof/mod.rs

@@ -14,11 +14,15 @@
 // pub mod message;
 // pub mod stateful_set_controller;
 // pub mod validation_rule;
+pub mod api_server_liveness;
 pub mod cluster;
 pub mod compositionality;
-pub mod failures;
+pub mod external_liveness;
+pub mod failures_liveness;
 pub mod network;
+pub mod network_liveness;
 pub mod objects_in_reconcile;
 pub mod objects_in_store;
 pub mod req_resp;
+pub mod stability;
 pub mod wf1_helpers;