Skip to content

Commit

Permalink
Introduce shape shifter
Browse files Browse the repository at this point in the history 
Signed-off-by: Xudong Sun <[email protected]>
  • Loading branch information
@marshtompsxd
marshtompsxd committed Aug 5, 2024
1 parent 426eb20 commit 9e1ee3c
Show file tree
Hide file tree
Showing 2 changed files with 34 additions and 27 deletions.
37 changes: 19 additions & 18 deletions src/soundness/compositionality/proof.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,27 +19,27 @@ closed spec fn a_inv<S>() -> StatePred<S>;
// The inv that b has to satisfy to make a's property hold when b runs with a
closed spec fn b_inv<S>() -> StatePred<S>;

/* 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<S, I>(input: I) -> (env_input: I)
proof fn a_does_nothing_beyond_what_shape_shifter_does<S, I>(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<S, I>(input: I) -> (env_input: I)
proof fn b_does_nothing_beyond_what_shape_shifter_does<S, I>(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)]
Expand All @@ -53,20 +53,20 @@ proof fn a_inv_holds_locally<S, I>(spec: TempPred<S>)

// 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<S, I>(spec: TempPred<S>)
requires
spec.entails(lift_state(init::<S>())),
spec.entails(always(lift_action(next_with_a_only::<S, I>()))),
spec.entails(fairness::<S>()),
spec.entails(a_fairness::<S>()),
spec.entails(always(lift_state(b_inv::<S>()))),
spec.entails(b_property::<S>()),
ensures
spec.entails(a_property::<S>()),
{}

/* 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)]
Expand All @@ -84,7 +84,7 @@ proof fn b_property_holds_locally<S, I>(spec: TempPred<S>)
requires
spec.entails(lift_state(init::<S>())),
spec.entails(always(lift_action(next_with_b_only::<S, I>()))),
spec.entails(fairness::<S>()),
spec.entails(b_fairness::<S>()),
spec.entails(always(lift_state(a_inv::<S>()))),
ensures
spec.entails(b_property::<S>()),
Expand All @@ -97,7 +97,8 @@ proof fn a_property_holds_globally<S, I>(spec: TempPred<S>)
requires
spec.entails(lift_state(init::<S>())),
spec.entails(always(lift_action(next::<S, I>()))),
spec.entails(fairness::<S>()),
spec.entails(a_fairness::<S>()),
spec.entails(b_fairness::<S>()),
ensures
spec.entails(a_property::<S>()),
{
Expand Down Expand Up @@ -131,7 +132,7 @@ proof fn b_property_holds_globally<S, I>(spec: TempPred<S>)
requires
spec.entails(lift_state(init::<S>())),
spec.entails(always(lift_action(next::<S, I>()))),
spec.entails(fairness::<S>()),
spec.entails(b_fairness::<S>()),
ensures
spec.entails(b_property::<S>()),
{
Expand Down Expand Up @@ -169,8 +170,8 @@ proof fn next_does_nothing_beyond_next_with_a_only<S, I>(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::<S, I>(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::<S, I>(input);
assert(next_step_with_a_only(s, s_prime, Step::ControllerBStep(ss_input)));
}
_ => {
assert(next_step_with_a_only(s, s_prime, step));
Expand All @@ -188,8 +189,8 @@ proof fn next_does_nothing_beyond_next_with_b_only<S, I>(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::<S, I>(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::<S, I>(input);
assert(next_step_with_b_only(s, s_prime, Step::ControllerAStep(ss_input)));
}
_ => {
assert(next_step_with_b_only(s, s_prime, step));
Expand Down
24 changes: 15 additions & 9 deletions src/soundness/compositionality/state_machine.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,12 +12,15 @@ pub closed spec fn init<S>() -> StatePred<S>;
// next step action of the environment
pub closed spec fn environment_next<S, I>(input: I) -> ActionPred<S>;

// next step action of controller a
// next step action of the controller a
pub closed spec fn controller_a_next<S, I>(input: I) -> ActionPred<S>;

// next step action of controller b
// next step action of the controller b
pub closed spec fn controller_b_next<S, I>(input: I) -> ActionPred<S>;

// next step action of the shape shifter
pub closed spec fn shape_shifter_next<S, I>(input: I) -> ActionPred<S>;

// stutter step action to make always(next) hold
pub open spec fn stutter<S>() -> ActionPred<S> {
|s, s_prime: S| s == s_prime
Expand All @@ -31,7 +34,7 @@ pub enum Step<I> {
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<S, I>() -> ActionPred<S> {
|s, s_prime: S| exists |step: Step<I>| #[trigger] next_step(s, s_prime, step)
}
Expand All @@ -45,21 +48,21 @@ pub open spec fn next_step<S, I>(s: S, s_prime: S, step: Step<I>) -> 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<S, I>() -> ActionPred<S> {
|s, s_prime: S| exists |step: Step<I>| #[trigger] next_step_with_b_only(s, s_prime, step)
}

pub open spec fn next_step_with_b_only<S, I>(s: S, s_prime: S, step: Step<I>) -> 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<S, I>() -> ActionPred<S> {
|s, s_prime: S| exists |step: Step<I>| #[trigger] next_step_with_a_only(s, s_prime, step)
}
Expand All @@ -68,12 +71,15 @@ pub open spec fn next_step_with_a_only<S, I>(s: S, s_prime: S, step: Step<I>) ->
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<S>() -> TempPred<S>;
// fairness condition of controller a
pub closed spec fn a_fairness<S>() -> TempPred<S>;

// fairness condition of controller b
pub closed spec fn b_fairness<S>() -> TempPred<S>;

}

0 comments on commit 9e1ee3c

Please sign in to comment.