Skip to content

Commit

Permalink
Simplify compositional proof obligations (anvil-verifier#509)
Browse files Browse the repository at this point in the history 
Signed-off-by: Xudong Sun <[email protected]>
  • Loading branch information
@marshtompsxd
marshtompsxd authored Aug 9, 2024
1 parent b632959 commit 0218b70
Show file tree
Hide file tree
Showing 2 changed files with 175 additions and 208 deletions.
226 changes: 74 additions & 152 deletions src/soundness/compositionality/proof.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,192 +7,114 @@ use vstd::prelude::*;

verus! {

// The top level property of the controller a (e.g., ESR)
closed spec fn a_property<S>() -> TempPred<S>;

// The top level property of the controller b (e.g., ESR)
closed spec fn b_property<S>() -> TempPred<S>;

// The inv that a has to satisfy to make b's property hold when a runs with b
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 shape shifter can do anything that a or b might do */

// Behaviors of a are covered by behaviors of the shape shifter
#[verifier(external_body)]
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)
==> shape_shifter_next(ss_input)(s, s_prime)
{
arbitrary()
}

// Behaviors of b are covered by behaviors of the shape shifter
// The top level property of the consumer controller (e.g., ESR)
spec fn consumer_property<S>() -> TempPred<S>;

// The top level property of the producer controller (e.g., ESR)
spec fn producer_property<S>() -> TempPred<S>;

// The inv saying that no one interferes with the producer's reconcile
spec fn no_one_interferes_producer<S, I>(any: Controller<S, I>) -> StatePred<S>;

// Our goal is to prove that both producer and consumer are correct
// requires
// spec.entails(lift_state(consumer_and_producer::<S, I>().init())),
// spec.entails(always(lift_action(consumer_and_producer::<S, I>().next()))),
// spec.entails(producer_fairness::<S, I>()),
// spec.entails(consumer_fairness::<S, I>()),
// ensures
// spec.entails(producer_property::<S>()),
// spec.entails(consumer_property::<S>()),
//
// To do so, there are three proof obligations:

// Proof obligation 1:
// Producer is correct when running with the shape shifter assuming no interference.
// In fact, this theorem is all you need if you only care about the producer, not the
// consumer.
#[verifier(external_body)]
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)
==> shape_shifter_next(ss_input)(s, s_prime)
{
arbitrary()
}

/* 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)]
proof fn a_inv_holds_locally<S, I>(spec: TempPred<S>)
proof fn producer_property_holds_if_no_interference<S, I>(spec: TempPred<S>, any: Controller<S, I>)
requires
spec.entails(lift_state(init::<S>())),
spec.entails(always(lift_action(next_with_a_only::<S, I>()))),
spec.entails(lift_state(producer_and_any::<S, I>(any).init())),
spec.entails(always(lift_action(producer_and_any::<S, I>(any).next()))),
spec.entails(producer_fairness::<S, I>()),
spec.entails(always(lift_state(no_one_interferes_producer::<S, I>(any)))),
ensures
spec.entails(always(lift_state(a_inv::<S>()))),
spec.entails(producer_property::<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 create a pod so that a can update the pod
// Proof obligation 2:
// Consumer is correct when running with the producer assuming the producer is correct.
#[verifier(external_body)]
proof fn a_property_holds_locally<S, I>(spec: TempPred<S>)
proof fn consumer_property_holds_if_producer_property_holds<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(a_fairness::<S>()),
spec.entails(always(lift_state(b_inv::<S>()))),
spec.entails(b_property::<S>()),
spec.entails(lift_state(consumer_and_producer::<S, I>().init())),
spec.entails(always(lift_action(consumer_and_producer::<S, I>().next()))),
spec.entails(producer_fairness::<S, I>()),
spec.entails(consumer_fairness::<S, I>()),
spec.entails(producer_property::<S>()),
ensures
spec.entails(a_property::<S>()),
spec.entails(consumer_property::<S>()),
{}

/* The following two proof functions are theorems of the local cluster including shape shifter and b */

// b's invariant holds in the local cluster
// Proof obligation 3:
// Consumer does not interfere with the producer.
#[verifier(external_body)]
proof fn b_inv_holds_locally<S, I>(spec: TempPred<S>)
proof fn consumer_does_not_interfere_with_the_producer<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(lift_state(consumer_and_producer::<S, I>().init())),
spec.entails(always(lift_action(consumer_and_producer::<S, I>().next()))),
ensures
spec.entails(always(lift_state(b_inv::<S>()))),
spec.entails(always(lift_state(no_one_interferes_producer::<S, I>(consumer())))),
{}

// b's property holds in the local cluster if the a's invariant also holds
#[verifier(external_body)]
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(b_fairness::<S>()),
spec.entails(always(lift_state(a_inv::<S>()))),
ensures
spec.entails(b_property::<S>()),
{}

/* The following two proof functions are top-level theorems */

// a's property holds in the global cluster
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(a_fairness::<S>()),
spec.entails(b_fairness::<S>()),
ensures
spec.entails(a_property::<S>()),
{
b_property_holds_globally::<S, I>(spec);

assert forall |ex| #[trigger] spec.satisfied_by(ex)
implies always(lift_action(next_with_a_only::<S, I>())).satisfied_by(ex) by {
assert(spec.implies(always(lift_action(next::<S, I>()))).satisfied_by(ex));
assert forall |i| #[trigger] lift_action(next_with_a_only::<S, I>()).satisfied_by(ex.suffix(i)) by {
assert(lift_action(next::<S, I>()).satisfied_by(ex.suffix(i)));
next_does_nothing_beyond_next_with_a_only::<S, I>(ex.suffix(i).head(), ex.suffix(i).head_next());
}
}

assert forall |ex| #[trigger] spec.satisfied_by(ex)
implies always(lift_action(next_with_b_only::<S, I>())).satisfied_by(ex) by {
assert(spec.implies(always(lift_action(next::<S, I>()))).satisfied_by(ex));
assert forall |i| #[trigger] lift_action(next_with_b_only::<S, I>()).satisfied_by(ex.suffix(i)) by {
assert(lift_action(next::<S, I>()).satisfied_by(ex.suffix(i)));
next_does_nothing_beyond_next_with_b_only::<S, I>(ex.suffix(i).head(), ex.suffix(i).head_next());
}
}

b_inv_holds_locally::<S, I>(spec);
a_property_holds_locally::<S, I>(spec);
}

// b's property holds in the global cluster
proof fn b_property_holds_globally<S, I>(spec: TempPred<S>)
// Now we can draw the final conclusion with the lemmas above.
proof fn consumer_property_holds<S, I>(spec: TempPred<S>)
requires
spec.entails(lift_state(init::<S>())),
spec.entails(always(lift_action(next::<S, I>()))),
spec.entails(b_fairness::<S>()),
spec.entails(lift_state(consumer_and_producer::<S, I>().init())),
spec.entails(always(lift_action(consumer_and_producer::<S, I>().next()))),
spec.entails(producer_fairness::<S, I>()),
spec.entails(consumer_fairness::<S, I>()),
ensures
spec.entails(b_property::<S>()),
spec.entails(producer_property::<S>()),
spec.entails(consumer_property::<S>()),
{
assert forall |ex| #[trigger] spec.satisfied_by(ex)
implies always(lift_action(next_with_a_only::<S, I>())).satisfied_by(ex) by {
assert(spec.implies(always(lift_action(next::<S, I>()))).satisfied_by(ex));
assert forall |i| #[trigger] lift_action(next_with_a_only::<S, I>()).satisfied_by(ex.suffix(i)) by {
assert(lift_action(next::<S, I>()).satisfied_by(ex.suffix(i)));
next_does_nothing_beyond_next_with_a_only::<S, I>(ex.suffix(i).head(), ex.suffix(i).head_next());
}
implies lift_state(producer_and_any::<S, I>(consumer()).init()).satisfied_by(ex) by {
assert(spec.implies(lift_state(consumer_and_producer::<S, I>().init())).satisfied_by(ex));
}

assert forall |ex| #[trigger] spec.satisfied_by(ex)
implies always(lift_action(next_with_b_only::<S, I>())).satisfied_by(ex) by {
assert(spec.implies(always(lift_action(next::<S, I>()))).satisfied_by(ex));
assert forall |i| #[trigger] lift_action(next_with_b_only::<S, I>()).satisfied_by(ex.suffix(i)) by {
assert(lift_action(next::<S, I>()).satisfied_by(ex.suffix(i)));
next_does_nothing_beyond_next_with_b_only::<S, I>(ex.suffix(i).head(), ex.suffix(i).head_next());
implies always(lift_action(producer_and_any::<S, I>(consumer()).next())).satisfied_by(ex) by {
assert(spec.implies(always(lift_action(consumer_and_producer::<S, I>().next()))).satisfied_by(ex));
assert forall |i| #[trigger] lift_action(producer_and_any::<S, I>(consumer()).next()).satisfied_by(ex.suffix(i)) by {
assert(lift_action(consumer_and_producer::<S, I>().next()).satisfied_by(ex.suffix(i)));
state_machine_simulation::<S, I>(ex.suffix(i).head(), ex.suffix(i).head_next());
}
}

a_inv_holds_locally::<S, I>(spec);
b_property_holds_locally::<S, I>(spec);
consumer_does_not_interfere_with_the_producer::<S, I>(spec);
producer_property_holds_if_no_interference::<S, I>(spec, consumer());
consumer_property_holds_if_producer_property_holds::<S, I>(spec);
}

/* Helper lemmas on the relations of the local and global clusters' transitions */

proof fn next_does_nothing_beyond_next_with_a_only<S, I>(s: S, s_prime: S)
proof fn state_machine_simulation<S, I>(s: S, s_prime: S)
requires
next::<S, I>()(s, s_prime),
consumer_and_producer::<S, I>().next()(s, s_prime),
ensures
next_with_a_only::<S, I>()(s, s_prime),
producer_and_any::<S, I>(consumer()).next()(s, s_prime),
{
let step = choose |step: Step<I>| next_step(s, s_prime, step);
assert(next_step(s, s_prime, step));
let step = choose |step: Step<I>| consumer_and_producer::<S, I>().next_step(s, s_prime, step);
assert(consumer_and_producer::<S, I>().next_step(s, s_prime, step));
match step {
Step::ControllerBStep(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));
Step::TargetControllerStep(input) => {
assert(producer_and_any::<S, I>(consumer()).next_step(s, s_prime, Step::AnotherControllerStep(input)));
}
}
}

proof fn next_does_nothing_beyond_next_with_b_only<S, I>(s: S, s_prime: S)
requires
next::<S, I>()(s, s_prime),
ensures
next_with_b_only::<S, I>()(s, s_prime),
{
let step = choose |step: Step<I>| next_step(s, s_prime, step);
assert(next_step(s, s_prime, step));
match step {
Step::ControllerAStep(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)));
Step::AnotherControllerStep(input) => {
assert(producer_and_any::<S, I>(consumer()).next_step(s, s_prime, Step::TargetControllerStep(input)));
}
_ => {
assert(next_step_with_b_only(s, s_prime, step));
assert(producer_and_any::<S, I>(consumer()).next_step(s, s_prime, step));
}
}
}
Expand Down
Loading

0 comments on commit 0218b70

Please sign in to comment.