Skip to content

Commit

Permalink
comment
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 13, 2024
1 parent 02e20de commit 178fb7e
Show file tree
Hide file tree
Showing 2 changed files with 98 additions and 74 deletions.
169 changes: 95 additions & 74 deletions src/soundness/compositionality/proof.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,83 +17,34 @@ spec fn producer_property<S>(p_index: int) -> TempPred<S>;
// This invariant, if opened, should state something like:
// forall |message| message is sent by the controller indexed by good_citizen_id ==> message does not modify object X,
// where X is something that the consumer cares about.
// Note that the invariant likely will not hold when good_citizen_id points to the consumer itself, that is,
//
// To tell whether a message in the network is sent by a controller, our cluster state machine should attach the
// controller id (the index) to each message sent by the controller, regardless of the controller's implementation.
//
// Note that the invariant likely does not hold when good_citizen_id points to the consumer itself, that is,
// if there are two consumers, they will interfere with each other.
// This is not a problem because there is no reason to run two separate consumer instances at the same time.
// However, when proving the invariant we need to be careful so that good_citizen_id does not point to another consumer.
// However, when proving the invariant we need to be careful so that good_citizen_id does not point to another
// consumer instance.
spec fn one_does_not_interfere_with_consumer<S, I>(cluster: Cluster<S, I>, good_citizen_id: int) -> StatePred<S>;

// The inv asserts that the controller indexed by good_citizen_id does not interfere with the producer's reconcile
// The inv asserts that the controller indexed by good_citizen_id does not interfere with the producer's reconcile,
// similar to the one above.
spec fn one_does_not_interfere_with_producer<S, I>(cluster: Cluster<S, I>, good_citizen_id: int, p_index: int) -> StatePred<S>;

// The only reason I need this spec fun is to use it as a trigger (in the case that no one else can serve as a trigger).
// The only reason I need this spec fun is to use it as a trigger in the case that no one else can serve as a trigger.
pub open spec fn within_range<A>(seq: Seq<A>, index: int) -> bool {
0 <= index < seq.len()
}

pub open spec fn consumer_and_producers<S, I>() -> Cluster<S, I> {
Cluster {
controllers: producers::<S, I>().push(consumer::<S, I>()),
}
}

// This is our end-goal theorem: in a cluster with all the producers and the consumer,
// all controllers are correct.
proof fn consumer_and_producer_properties_hold_in_a_concrete_cluster<S, I>(spec: TempPred<S>)
requires
spec.entails(lift_state(consumer_and_producers::<S, I>().init())),
spec.entails(always(lift_action(consumer_and_producers::<S, I>().next()))),
forall |p_index: int| 0 <= p_index < producers::<S, I>().len()
==> #[trigger] spec.entails(producer_fairness::<S, I>(p_index)),
spec.entails(consumer_fairness::<S, I>()),
ensures
forall |p_index: int| 0 <= p_index < producers::<S, I>().len()
==> #[trigger] spec.entails(producer_property::<S>(p_index)),
spec.entails(consumer_property::<S>()),
{
let cluster = consumer_and_producers::<S, I>();

let producer_ids = producers::<S, I>().map(|i: int, producer: Controller<S, I>| i);
let consumer_id = cluster.controllers.len() - 1;

assert forall |s| #[trigger] cluster.init()(s) implies consumer::<S, I>().init()(s) by {
assert forall |i| 0 <= i < cluster.controllers.len() implies #[trigger] cluster.controllers[i].init()(s) by {}
assert(consumer::<S, I>() =~= cluster.controllers.last());
}

assert forall |p_index| #![trigger producers::<S, I>()[p_index]] 0 <= p_index < producers::<S, I>().len()
implies forall |s| #[trigger] cluster.init()(s) ==> producers::<S, I>()[p_index].init()(s) by {
assert forall |s| #[trigger] cluster.init()(s) implies producers::<S, I>()[p_index].init()(s) by {
assert forall |i| 0 <= i < cluster.controllers.len() implies #[trigger] cluster.controllers[i].init()(s) by {}
assert(producers::<S, I>()[p_index] =~= cluster.controllers[p_index]);
}
}

assert forall |good_citizen_id: int| 0 <= good_citizen_id < cluster.controllers.len()
&& good_citizen_id != consumer_id
&& !(exists |i| 0 <= i < producer_ids.len() && good_citizen_id == producer_ids[i])
implies
spec.entails(always(lift_state(#[trigger] one_does_not_interfere_with_consumer::<S, I>(cluster, good_citizen_id))))
&& forall |p_index: int| 0 <= p_index < producers::<S, I>().len()
==> spec.entails(always(lift_state(#[trigger] one_does_not_interfere_with_producer::<S, I>(cluster, good_citizen_id, p_index))))
by {
assert forall |controller_id| #[trigger] within_range(cluster.controllers, controller_id)
implies controller_id == consumer_id || exists |i| #[trigger] within_range(producer_ids, i) && controller_id == producer_ids[i] by {
if controller_id == cluster.controllers.len() - 1 {
assert(controller_id == consumer_id);
} else {
let i = controller_id;
assert(within_range(producer_ids, i) && controller_id == producer_ids[i]);
}
}
assert(within_range(cluster.controllers, good_citizen_id));
assert(good_citizen_id == consumer_id || exists |i| #[trigger] within_range(producer_ids, i) && good_citizen_id == producer_ids[i]);
}

consumer_and_producer_properties_hold(spec, cluster, consumer_id, producer_ids);
}

proof fn consumer_and_producer_properties_hold<S, I>(spec: TempPred<S>, cluster: Cluster<S, I>, consumer_id: int, producer_ids: Seq<int>)
// This is our end-goal theorem: the consumer and producers are correct in any cluster
// if the other controllers in that cluster do not interfere with the consumer or producers.
// # Arguments:
// * spec: the temporal predicate that represents the state machine
// * cluster: the cluster that we want to run the consumers/producers in
// * consumer_id: the index of the consumer inside cluster.controllers
// * producer_ids: the sequence of indexes of the producers inside cluster.controllers
proof fn consumer_and_producers_are_correct<S, I>(spec: TempPred<S>, cluster: Cluster<S, I>, consumer_id: int, producer_ids: Seq<int>)
requires
spec.entails(lift_state(cluster.init())),
spec.entails(always(lift_action(cluster.next()))),
Expand Down Expand Up @@ -143,7 +94,7 @@ proof fn consumer_and_producer_properties_hold<S, I>(spec: TempPred<S>, cluster:
assert(spec.entails(always(lift_state(one_does_not_interfere_with_producer::<S, I>(cluster, good_citizen_id, p_index)))));
}
}
producer_property_holds_if_no_interference(spec, cluster, producer_id, p_index);
producer_is_correct(spec, cluster, producer_id, p_index);
}

assert forall |good_citizen_id| 0 <= good_citizen_id < cluster.controllers.len() && good_citizen_id != consumer_id
Expand All @@ -155,15 +106,80 @@ proof fn consumer_and_producer_properties_hold<S, I>(spec: TempPred<S>, cluster:
assert(spec.entails(always(lift_state(one_does_not_interfere_with_consumer::<S, I>(cluster, good_citizen_id)))));
}
}
consumer_property_holds_if_no_interference(spec, cluster, consumer_id);
consumer_is_correct(spec, cluster, consumer_id);
}

// To prove the above theorem, there are three proof obligations.
// A concrete cluster with only producers and consumer
pub open spec fn consumer_and_producers<S, I>() -> Cluster<S, I> {
Cluster {
controllers: producers::<S, I>().push(consumer::<S, I>()),
}
}

// We can apply consumer_and_producers_are_correct to the concrete cluster above to conclude that
// the consumer and producers are correct in a cluster where there are only consumer and producers.
proof fn consumer_and_producers_are_correct_in_a_concrete_cluster<S, I>(spec: TempPred<S>)
requires
spec.entails(lift_state(consumer_and_producers::<S, I>().init())),
spec.entails(always(lift_action(consumer_and_producers::<S, I>().next()))),
forall |p_index: int| 0 <= p_index < producers::<S, I>().len()
==> #[trigger] spec.entails(producer_fairness::<S, I>(p_index)),
spec.entails(consumer_fairness::<S, I>()),
ensures
forall |p_index: int| 0 <= p_index < producers::<S, I>().len()
==> #[trigger] spec.entails(producer_property::<S>(p_index)),
spec.entails(consumer_property::<S>()),
{
let cluster = consumer_and_producers::<S, I>();

let producer_ids = producers::<S, I>().map(|i: int, producer: Controller<S, I>| i);
let consumer_id = cluster.controllers.len() - 1;

assert forall |s| #[trigger] cluster.init()(s) implies consumer::<S, I>().init()(s) by {
assert forall |i| 0 <= i < cluster.controllers.len() implies #[trigger] cluster.controllers[i].init()(s) by {}
assert(consumer::<S, I>() =~= cluster.controllers.last());
}

assert forall |p_index| #![trigger producers::<S, I>()[p_index]] 0 <= p_index < producers::<S, I>().len()
implies forall |s| #[trigger] cluster.init()(s) ==> producers::<S, I>()[p_index].init()(s) by {
assert forall |s| #[trigger] cluster.init()(s) implies producers::<S, I>()[p_index].init()(s) by {
assert forall |i| 0 <= i < cluster.controllers.len() implies #[trigger] cluster.controllers[i].init()(s) by {}
assert(producers::<S, I>()[p_index] =~= cluster.controllers[p_index]);
}
}

// Due to our cluster construct, you won't find a good_citizen_id that is neither the consumer nor any producer.
// So we prove the following assertion by contradiction.
assert forall |good_citizen_id: int| 0 <= good_citizen_id < cluster.controllers.len()
&& good_citizen_id != consumer_id
&& !(exists |i| 0 <= i < producer_ids.len() && good_citizen_id == producer_ids[i])
implies
spec.entails(always(lift_state(#[trigger] one_does_not_interfere_with_consumer::<S, I>(cluster, good_citizen_id))))
&& forall |p_index: int| 0 <= p_index < producers::<S, I>().len()
==> spec.entails(always(lift_state(#[trigger] one_does_not_interfere_with_producer::<S, I>(cluster, good_citizen_id, p_index))))
by {
assert forall |controller_id| #[trigger] within_range(cluster.controllers, controller_id) // I am using within_range here because no one else can be a trigger
implies controller_id == consumer_id || exists |i| #[trigger] within_range(producer_ids, i) && controller_id == producer_ids[i] by {
if controller_id == cluster.controllers.len() - 1 {
assert(controller_id == consumer_id);
} else {
let i = controller_id;
assert(within_range(producer_ids, i) && controller_id == producer_ids[i]);
}
}
assert(within_range(cluster.controllers, good_citizen_id));
assert(good_citizen_id == consumer_id || exists |i| #[trigger] within_range(producer_ids, i) && good_citizen_id == producer_ids[i]);
}

consumer_and_producers_are_correct(spec, cluster, consumer_id, producer_ids);
}

// To prove consumer_and_producers_are_correct, there are five proof obligations.

// Proof obligation 1:
// Producer is correct when running in any cluster where there is no interference.
#[verifier(external_body)]
proof fn producer_property_holds_if_no_interference<S, I>(spec: TempPred<S>, cluster: Cluster<S, I>, producer_id: int, p_index: int)
proof fn producer_is_correct<S, I>(spec: TempPred<S>, cluster: Cluster<S, I>, producer_id: int, p_index: int)
requires
0 <= p_index < producers::<S, I>().len(),
0 <= producer_id < cluster.controllers.len(),
Expand All @@ -184,7 +200,7 @@ proof fn producer_property_holds_if_no_interference<S, I>(spec: TempPred<S>, clu
// Proof obligation 2:
// Consumer is correct when running in any cluster where each producer's spec is available and there is no interference.
#[verifier(external_body)]
proof fn consumer_property_holds_if_no_interference<S, I>(spec: TempPred<S>, cluster: Cluster<S, I>, consumer_id: int)
proof fn consumer_is_correct<S, I>(spec: TempPred<S>, cluster: Cluster<S, I>, consumer_id: int)
requires
0 <= consumer_id < cluster.controllers.len(),
spec.entails(lift_state(cluster.init())),
Expand All @@ -205,7 +221,7 @@ proof fn consumer_property_holds_if_no_interference<S, I>(spec: TempPred<S>, clu
{}

// Proof obligation 3:
// Consumer does not interfere with the producer.
// Consumer does not interfere with the producer in any cluster.
#[verifier(external_body)]
proof fn consumer_does_not_interfere_with_the_producer<S, I>(spec: TempPred<S>, cluster: Cluster<S, I>, good_citizen_id: int, p_index: int)
requires
Expand All @@ -219,7 +235,8 @@ proof fn consumer_does_not_interfere_with_the_producer<S, I>(spec: TempPred<S>,
spec.entails(always(lift_state(one_does_not_interfere_with_producer::<S, I>(cluster, good_citizen_id, p_index)))),
{}


// Proof obligation 4:
// Producer does not interfere with the consumer in any cluster.
#[verifier(external_body)]
proof fn producer_does_not_interfere_with_the_consumer<S, I>(spec: TempPred<S>, cluster: Cluster<S, I>, good_citizen_id: int, p_index: int)
requires
Expand All @@ -233,11 +250,15 @@ proof fn producer_does_not_interfere_with_the_consumer<S, I>(spec: TempPred<S>,
spec.entails(always(lift_state(one_does_not_interfere_with_consumer::<S, I>(cluster, good_citizen_id)))),
{}

// Proof obligation 4:
// Producer does not interfere with another producer in any cluster.
#[verifier(external_body)]
proof fn producer_does_not_interfere_with_the_producer<S, I>(spec: TempPred<S>, cluster: Cluster<S, I>, good_citizen_id: int, p_index: int, q_index: int)
requires
0 <= p_index < producers::<S, I>().len(),
0 <= q_index < producers::<S, I>().len(),
// We require the two producers to be different because there is no point to prove
// a producer does not interfere with another instance of itself.
p_index != q_index,
0 <= good_citizen_id < cluster.controllers.len(),
spec.entails(lift_state(cluster.init())),
Expand Down
3 changes: 3 additions & 0 deletions src/soundness/compositionality/state_machine.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,9 @@ impl<S, I> Cluster<S, I> {
}
}

// Inside this action, we need to require the message sent by controllers[i]
// to piggyback i so that we can tell which message in network is sent by who.
// In other words, the index i here serves as a sender id.
pub open spec fn controller_next(self, index: int, input: I) -> ActionPred<S> {
|s, s_prime| {
&&& 0 <= index < self.controllers.len()
Expand Down

0 comments on commit 178fb7e

Please sign in to comment.