From c9f4fa7762eae9b0a5bab90f82a8c575abbbfc49 Mon Sep 17 00:00:00 2001 From: Xudong Sun Date: Sun, 15 Sep 2024 12:47:37 -0500 Subject: [PATCH] Merge wf1 lemmas into wf1_helpers (#528) Signed-off-by: Xudong Sun --- .../proof/api_server_liveness.rs | 38 ------ .../proof/external_liveness.rs | 39 ------- src/v2/kubernetes_cluster/proof/mod.rs | 16 --- .../kubernetes_cluster/proof/wf1_helpers.rs | 108 +++++++++++++++++- .../spec/cluster_state_machine.rs | 10 +- 5 files changed, 111 insertions(+), 100 deletions(-) delete mode 100644 src/v2/kubernetes_cluster/proof/api_server_liveness.rs delete mode 100644 src/v2/kubernetes_cluster/proof/external_liveness.rs diff --git a/src/v2/kubernetes_cluster/proof/api_server_liveness.rs b/src/v2/kubernetes_cluster/proof/api_server_liveness.rs deleted file mode 100644 index e3e8faa4f..000000000 --- a/src/v2/kubernetes_cluster/proof/api_server_liveness.rs +++ /dev/null @@ -1,38 +0,0 @@ -// 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, input: Option, next: ActionPred, step: APIServerStep, pre: StatePred, post: StatePred -) - 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::>(spec, |i| self.api_server_next().weak_fairness(i), input); - self.api_server_action_pre_implies_next_pre(step, input); - valid_implies_trans::( - 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); -} - -} - -} diff --git a/src/v2/kubernetes_cluster/proof/external_liveness.rs b/src/v2/kubernetes_cluster/proof/external_liveness.rs deleted file mode 100644 index ce0bfb5ea..000000000 --- a/src/v2/kubernetes_cluster/proof/external_liveness.rs +++ /dev/null @@ -1,39 +0,0 @@ -// 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, controller_id: int, input: Option, next: ActionPred, - step: ExternalStep, pre: StatePred, post: StatePred -) - 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::>(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::( - 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); -} - -} - -} diff --git a/src/v2/kubernetes_cluster/proof/mod.rs b/src/v2/kubernetes_cluster/proof/mod.rs index a219b1a47..7593ae911 100644 --- a/src/v2/kubernetes_cluster/proof/mod.rs +++ b/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; diff --git a/src/v2/kubernetes_cluster/proof/wf1_helpers.rs b/src/v2/kubernetes_cluster/proof/wf1_helpers.rs index 51a4e335a..1c837ae6a 100644 --- a/src/v2/kubernetes_cluster/proof/wf1_helpers.rs +++ b/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, input: Option, next: ActionPred, + step: APIServerStep, pre: StatePred, post: StatePred +) + 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::>(spec, |i| self.api_server_next().weak_fairness(i), input); + self.api_server_action_pre_implies_next_pre(step, input); + valid_implies_trans::( + 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, input: (BuiltinControllerChoice, ObjectRef), next: ActionPred, + step: BuiltinControllersStep, pre: StatePred, post: StatePred +) + 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::(spec, |i| self.builtin_controllers_next().weak_fairness(i), input); + self.builtin_controllers_action_pre_implies_next_pre(step, input); + valid_implies_trans::( + 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, controller_id: int, input: (Option, Option), next: ActionPred, + step: ControllerStep, pre: StatePred, post: StatePred +) + 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, Option)| 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::, Option)>(spec, |i: (Option, Option)| 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, controller_id: int, input: ObjectRef, next: ActionPred, + pre: StatePred, post: StatePred +) + 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::(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, controller_id: int, input: Option, next: ActionPred, + step: ExternalStep, pre: StatePred, post: StatePred +) + 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::>(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::( + 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) ensures valid(lift_state(self.api_server_action_pre(step, input)).implies(lift_state(self.api_server_next().pre(input)))), { diff --git a/src/v2/kubernetes_cluster/spec/cluster_state_machine.rs b/src/v2/kubernetes_cluster/spec/cluster_state_machine.rs index ea19c9e02..569094217 100644 --- a/src/v2/kubernetes_cluster/spec/cluster_state_machine.rs +++ b/src/v2/kubernetes_cluster/spec/cluster_state_machine.rs @@ -241,8 +241,7 @@ impl Cluster { precondition: |input: (int, Option, Option), 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, Option), s: ClusterState| { let controller_id = input.0; @@ -270,6 +269,7 @@ impl Cluster { }; Action { precondition: |input: (Option, Option), 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), 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), s: ClusterState| { let controller_id = input.0; @@ -500,6 +498,8 @@ impl Cluster { }; Action { precondition: |input: Option, 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()