Merge wf1 lemmas into wf1_helpers (#528)

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

src/v2/kubernetes_cluster/proof/mod.rs

@@ -1,23 +1,7 @@
 // Copyright 2022 VMware, Inc.
 // SPDX-License-Identifier: MIT
-// pub mod api_server_liveness;
-// pub mod api_server_safety;
-// pub mod builtin_controllers;
-// pub mod cluster;
-// pub mod cluster_safety;
-// pub mod controller_runtime;
-// pub mod controller_runtime_eventual_safety;
-// pub mod controller_runtime_liveness;
-// pub mod controller_runtime_safety;
-// pub mod daemon_set_controller;
-// pub mod external_api_liveness;
-// 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 external_liveness;
 pub mod failures_liveness;
 pub mod network;
 pub mod network_liveness;

src/v2/kubernetes_cluster/proof/wf1_helpers.rs

@@ -2,6 +2,8 @@
 // SPDX-License-Identifier: MIT
 #![allow(unused_imports)]
 use crate::kubernetes_api_objects::spec::prelude::*;
+use crate::state_machine::{action::*, state_machine::*};
+use crate::temporal_logic::{defs::*, rules::*};
 use crate::v2::kubernetes_cluster::spec::{
     api_server::state_machine::api_server,
     api_server::types::*,
@@ -16,14 +18,116 @@ use crate::v2::kubernetes_cluster::spec::{
     network::state_machine::network,
     network::types::*,
 };
-use crate::state_machine::{action::*, state_machine::*};
-use crate::temporal_logic::defs::*;
 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);
+}
+
+pub proof fn lemma_pre_leads_to_post_by_builtin_controllers(
+    self, spec: TempPred<ClusterState>, input: (BuiltinControllerChoice, ObjectRef), next: ActionPred<ClusterState>,
+    step: BuiltinControllersStep, 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.builtin_controllers_next().forward(input)(s, s_prime) ==> post(s_prime),
+        forall |s| #[trigger] pre(s) ==> self.builtin_controllers_action_pre(step, input)(s),
+        spec.entails(always(lift_action(next))),
+        spec.entails(tla_forall(|i| self.builtin_controllers_next().weak_fairness(i))),
+    ensures spec.entails(lift_state(pre).leads_to(lift_state(post))),
+{
+    use_tla_forall::<ClusterState, (BuiltinControllerChoice, ObjectRef)>(spec, |i| self.builtin_controllers_next().weak_fairness(i), input);
+    self.builtin_controllers_action_pre_implies_next_pre(step, input);
+    valid_implies_trans::<ClusterState>(
+        lift_state(pre),
+        lift_state(self.builtin_controllers_action_pre(step, input)),
+        lift_state(self.builtin_controllers_next().pre(input))
+    );
+    self.builtin_controllers_next().wf1(input, spec, next, pre, post);
+}
+
+pub proof fn lemma_pre_leads_to_post_by_controller(
+    self, spec: TempPred<ClusterState>, controller_id: int, input: (Option<Message>, Option<ObjectRef>), next: ActionPred<ClusterState>,
+    step: ControllerStep, 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.controller_next().forward((controller_id, input.0, input.1))(s, s_prime) ==> post(s_prime),
+        forall |s| #[trigger] pre(s) ==> self.controller_action_pre(step, (controller_id, input.0, input.1))(s),
+        spec.entails(always(lift_action(next))),
+        spec.entails(tla_forall(|i: (Option<Message>, Option<ObjectRef>)| self.controller_next().weak_fairness((controller_id, i.0, i.1)))),
+    ensures spec.entails(lift_state(pre).leads_to(lift_state(post))),
+{
+    use_tla_forall::<ClusterState, (Option<Message>, Option<ObjectRef>)>(spec, |i: (Option<Message>, Option<ObjectRef>)| self.controller_next().weak_fairness((controller_id, i.0, i.1)), input);
+    self.controller_action_pre_implies_next_pre(step, (controller_id, input.0, input.1));
+    valid_implies_trans(
+        lift_state(pre),
+        lift_state(self.controller_action_pre(step, (controller_id, input.0, input.1))),
+        lift_state(self.controller_next().pre((controller_id, input.0, input.1)))
+    );
+    self.controller_next().wf1((controller_id, input.0, input.1), spec, next, pre, post);
+}
+
+pub proof fn lemma_pre_leads_to_post_by_schedule_controller_reconcile(
+    self, spec: TempPred<ClusterState>, controller_id: int, input: ObjectRef, next: ActionPred<ClusterState>,
+    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.schedule_controller_reconcile().forward((controller_id, input))(s, s_prime) ==> post(s_prime),
+        forall |s| #[trigger] pre(s) ==> self.schedule_controller_reconcile().pre((controller_id, input))(s),
+        spec.entails(always(lift_action(next))),
+        spec.entails(tla_forall(|i| self.schedule_controller_reconcile().weak_fairness((controller_id, i)))),
+    ensures spec.entails(lift_state(pre).leads_to(lift_state(post))),
+{
+    use_tla_forall::<ClusterState, ObjectRef>(spec, |i| self.schedule_controller_reconcile().weak_fairness((controller_id, i)), input);
+    self.schedule_controller_reconcile().wf1((controller_id, input), spec, next, pre, post);
+}
+
+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);
+}
+
 pub proof fn api_server_action_pre_implies_next_pre(self, step: APIServerStep, input: Option<Message>)
     ensures valid(lift_state(self.api_server_action_pre(step, input)).implies(lift_state(self.api_server_next().pre(input)))),
 {

src/v2/kubernetes_cluster/spec/cluster_state_machine.rs

@@ -241,8 +241,7 @@ impl Cluster {
             precondition: |input: (int, Option<Message>, Option<ObjectRef>), s: ClusterState| {
                 let controller_id = input.0;
                 let chosen_action = self.chosen_controller_next(controller_id);
-                &&& self.controller_models.contains_key(input.0)
-                &&& (chosen_action.precondition)((input.1, input.2), s)
+                (chosen_action.precondition)((input.1, input.2), s)
             },
             transition: |input: (int, Option<Message>, Option<ObjectRef>), s: ClusterState| {
                 let controller_id = input.0;
@@ -270,6 +269,7 @@ impl Cluster {
         };
         Action {
             precondition: |input: (Option<Message>, Option<ObjectRef>), s: ClusterState| {
+                &&& self.controller_models.contains_key(controller_id)
                 &&& received_msg_destined_for(input.0, HostId::Controller(controller_id))
                 &&& result(input, s).0.is_Enabled()
                 &&& result(input, s).1.is_Enabled()
@@ -470,9 +470,7 @@ impl Cluster {
             precondition: |input: (int, Option<Message>), s: ClusterState| {
                 let controller_id = input.0;
                 let chosen_action = self.chosen_external_next(controller_id);
-                &&& self.controller_models.contains_key(input.0)
-                &&& self.controller_models[controller_id].external_model.is_Some()
-                &&& (chosen_action.precondition)((input.1), s)
+                (chosen_action.precondition)((input.1), s)
             },
             transition: |input: (int, Option<Message>), s: ClusterState| {
                 let controller_id = input.0;
@@ -500,6 +498,8 @@ impl Cluster {
         };
         Action {
             precondition: |input: Option<Message>, s: ClusterState| {
+                &&& self.controller_models.contains_key(controller_id)
+                &&& self.controller_models[controller_id].external_model.is_Some()
                 &&& received_msg_destined_for(input, HostId::External(controller_id))
                 &&& result(input, s).0.is_Enabled()
                 &&& result(input, s).1.is_Enabled()