From 9e1ee3c17fa57959fc5f218ca741b758156af0fe Mon Sep 17 00:00:00 2001 From: Xudong Sun Date: Mon, 5 Aug 2024 18:16:54 -0500 Subject: [PATCH] Introduce shape shifter Signed-off-by: Xudong Sun --- src/soundness/compositionality/proof.rs | 37 ++++++++++--------- .../compositionality/state_machine.rs | 24 +++++++----- 2 files changed, 34 insertions(+), 27 deletions(-) diff --git a/src/soundness/compositionality/proof.rs b/src/soundness/compositionality/proof.rs index b22ddff52..09c3b5699 100644 --- a/src/soundness/compositionality/proof.rs +++ b/src/soundness/compositionality/proof.rs @@ -19,27 +19,27 @@ closed spec fn a_inv() -> StatePred; // The inv that b has to satisfy to make a's property hold when b runs with a closed spec fn b_inv() -> StatePred; -/* The following two proof functions show that env can do anything that a or b might do */ +/* The following two proof functions show that shape shifter can do anything that a or b might do */ -// Behaviors of a are covered by behaviors of the env +// Behaviors of a are covered by behaviors of the shape shifter #[verifier(external_body)] -proof fn a_does_nothing_beyond_what_env_does(input: I) -> (env_input: I) +proof fn a_does_nothing_beyond_what_shape_shifter_does(input: I) -> (ss_input: I) ensures forall |s, s_prime: S| #[trigger] controller_a_next(input)(s, s_prime) - ==> environment_next(env_input)(s, s_prime) + ==> shape_shifter_next(ss_input)(s, s_prime) { arbitrary() } -// Behaviors of b are covered by behaviors of the env +// Behaviors of b are covered by behaviors of the shape shifter #[verifier(external_body)] -proof fn b_does_nothing_beyond_what_env_does(input: I) -> (env_input: I) +proof fn b_does_nothing_beyond_what_shape_shifter_does(input: I) -> (ss_input: I) ensures forall |s, s_prime: S| #[trigger] controller_b_next(input)(s, s_prime) - ==> environment_next(env_input)(s, s_prime) + ==> shape_shifter_next(ss_input)(s, s_prime) { arbitrary() } -/* The following two proof functions are theorems of the local cluster including env and a */ +/* The following two proof functions are theorems of the local cluster including shape shifter and a */ // a's invariant holds in the local cluster #[verifier(external_body)] @@ -53,20 +53,20 @@ proof fn a_inv_holds_locally(spec: TempPred) // a's property holds in the local cluster if the b's property and invariant also hold // note that a's property depends on b's property -// for example, a waits for b to make some progress so that a can finish its job +// for example, a waits for b to create a pod so that a can update the pod #[verifier(external_body)] proof fn a_property_holds_locally(spec: TempPred) requires spec.entails(lift_state(init::())), spec.entails(always(lift_action(next_with_a_only::()))), - spec.entails(fairness::()), + spec.entails(a_fairness::()), spec.entails(always(lift_state(b_inv::()))), spec.entails(b_property::()), ensures spec.entails(a_property::()), {} -/* The following two proof functions are theorems of the local cluster including env and b */ +/* The following two proof functions are theorems of the local cluster including shape shifter and b */ // b's invariant holds in the local cluster #[verifier(external_body)] @@ -84,7 +84,7 @@ proof fn b_property_holds_locally(spec: TempPred) requires spec.entails(lift_state(init::())), spec.entails(always(lift_action(next_with_b_only::()))), - spec.entails(fairness::()), + spec.entails(b_fairness::()), spec.entails(always(lift_state(a_inv::()))), ensures spec.entails(b_property::()), @@ -97,7 +97,8 @@ proof fn a_property_holds_globally(spec: TempPred) requires spec.entails(lift_state(init::())), spec.entails(always(lift_action(next::()))), - spec.entails(fairness::()), + spec.entails(a_fairness::()), + spec.entails(b_fairness::()), ensures spec.entails(a_property::()), { @@ -131,7 +132,7 @@ proof fn b_property_holds_globally(spec: TempPred) requires spec.entails(lift_state(init::())), spec.entails(always(lift_action(next::()))), - spec.entails(fairness::()), + spec.entails(b_fairness::()), ensures spec.entails(b_property::()), { @@ -169,8 +170,8 @@ proof fn next_does_nothing_beyond_next_with_a_only(s: S, s_prime: S) assert(next_step(s, s_prime, step)); match step { Step::ControllerBStep(input) => { - let env_input = b_does_nothing_beyond_what_env_does::(input); - assert(next_step_with_a_only(s, s_prime, Step::EnvStep(env_input))); + let ss_input = b_does_nothing_beyond_what_shape_shifter_does::(input); + assert(next_step_with_a_only(s, s_prime, Step::ControllerBStep(ss_input))); } _ => { assert(next_step_with_a_only(s, s_prime, step)); @@ -188,8 +189,8 @@ proof fn next_does_nothing_beyond_next_with_b_only(s: S, s_prime: S) assert(next_step(s, s_prime, step)); match step { Step::ControllerAStep(input) => { - let env_input = a_does_nothing_beyond_what_env_does::(input); - assert(next_step_with_b_only(s, s_prime, Step::EnvStep(env_input))); + let ss_input = a_does_nothing_beyond_what_shape_shifter_does::(input); + assert(next_step_with_b_only(s, s_prime, Step::ControllerAStep(ss_input))); } _ => { assert(next_step_with_b_only(s, s_prime, step)); diff --git a/src/soundness/compositionality/state_machine.rs b/src/soundness/compositionality/state_machine.rs index ceee17607..dcb125cfe 100644 --- a/src/soundness/compositionality/state_machine.rs +++ b/src/soundness/compositionality/state_machine.rs @@ -12,12 +12,15 @@ pub closed spec fn init() -> StatePred; // next step action of the environment pub closed spec fn environment_next(input: I) -> ActionPred; -// next step action of controller a +// next step action of the controller a pub closed spec fn controller_a_next(input: I) -> ActionPred; -// next step action of controller b +// next step action of the controller b pub closed spec fn controller_b_next(input: I) -> ActionPred; +// next step action of the shape shifter +pub closed spec fn shape_shifter_next(input: I) -> ActionPred; + // stutter step action to make always(next) hold pub open spec fn stutter() -> ActionPred { |s, s_prime: S| s == s_prime @@ -31,7 +34,7 @@ pub enum Step { StutterStep(), } -// next step action of the *global* cluster including env, a and b +// next step action of the *global* cluster including both a and b pub open spec fn next() -> ActionPred { |s, s_prime: S| exists |step: Step| #[trigger] next_step(s, s_prime, step) } @@ -45,7 +48,7 @@ pub open spec fn next_step(s: S, s_prime: S, step: Step) -> bool { } } -// next step action of the *local* cluster including env and b +// next step action of the *local* cluster that replaces a with the shape shifter pub open spec fn next_with_b_only() -> ActionPred { |s, s_prime: S| exists |step: Step| #[trigger] next_step_with_b_only(s, s_prime, step) } @@ -53,13 +56,13 @@ pub open spec fn next_with_b_only() -> ActionPred { pub open spec fn next_step_with_b_only(s: S, s_prime: S, step: Step) -> bool { match step { Step::EnvStep(input) => environment_next(input)(s, s_prime), - Step::ControllerAStep(input) => environment_next(input)(s, s_prime), + Step::ControllerAStep(input) => shape_shifter_next(input)(s, s_prime), Step::ControllerBStep(input) => controller_b_next(input)(s, s_prime), Step::StutterStep() => stutter()(s, s_prime), } } -// next step action of the *local* cluster including env and a +// next step action of the *local* cluster that replaces b with the shape shifter pub open spec fn next_with_a_only() -> ActionPred { |s, s_prime: S| exists |step: Step| #[trigger] next_step_with_a_only(s, s_prime, step) } @@ -68,12 +71,15 @@ pub open spec fn next_step_with_a_only(s: S, s_prime: S, step: Step) -> match step { Step::EnvStep(input) => environment_next(input)(s, s_prime), Step::ControllerAStep(input) => controller_a_next(input)(s, s_prime), - Step::ControllerBStep(input) => environment_next(input)(s, s_prime), + Step::ControllerBStep(input) => shape_shifter_next(input)(s, s_prime), Step::StutterStep() => stutter()(s, s_prime), } } -// fairness condition that is needed for liveness -pub closed spec fn fairness() -> TempPred; +// fairness condition of controller a +pub closed spec fn a_fairness() -> TempPred; + +// fairness condition of controller b +pub closed spec fn b_fairness() -> TempPred; }