diff --git a/src/soundness/compositionality/proof.rs b/src/soundness/compositionality/proof.rs index 40ddced96..ed13c43e4 100644 --- a/src/soundness/compositionality/proof.rs +++ b/src/soundness/compositionality/proof.rs @@ -17,83 +17,34 @@ spec fn producer_property(p_index: int) -> TempPred; // 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(cluster: Cluster, good_citizen_id: int) -> StatePred; -// 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(cluster: Cluster, good_citizen_id: int, p_index: int) -> StatePred; -// 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(seq: Seq, index: int) -> bool { 0 <= index < seq.len() } -pub open spec fn consumer_and_producers() -> Cluster { - Cluster { - controllers: producers::().push(consumer::()), - } -} - -// 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(spec: TempPred) - requires - spec.entails(lift_state(consumer_and_producers::().init())), - spec.entails(always(lift_action(consumer_and_producers::().next()))), - forall |p_index: int| 0 <= p_index < producers::().len() - ==> #[trigger] spec.entails(producer_fairness::(p_index)), - spec.entails(consumer_fairness::()), - ensures - forall |p_index: int| 0 <= p_index < producers::().len() - ==> #[trigger] spec.entails(producer_property::(p_index)), - spec.entails(consumer_property::()), -{ - let cluster = consumer_and_producers::(); - - let producer_ids = producers::().map(|i: int, producer: Controller| i); - let consumer_id = cluster.controllers.len() - 1; - - assert forall |s| #[trigger] cluster.init()(s) implies consumer::().init()(s) by { - assert forall |i| 0 <= i < cluster.controllers.len() implies #[trigger] cluster.controllers[i].init()(s) by {} - assert(consumer::() =~= cluster.controllers.last()); - } - - assert forall |p_index| #![trigger producers::()[p_index]] 0 <= p_index < producers::().len() - implies forall |s| #[trigger] cluster.init()(s) ==> producers::()[p_index].init()(s) by { - assert forall |s| #[trigger] cluster.init()(s) implies producers::()[p_index].init()(s) by { - assert forall |i| 0 <= i < cluster.controllers.len() implies #[trigger] cluster.controllers[i].init()(s) by {} - assert(producers::()[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::(cluster, good_citizen_id)))) - && forall |p_index: int| 0 <= p_index < producers::().len() - ==> spec.entails(always(lift_state(#[trigger] one_does_not_interfere_with_producer::(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(spec: TempPred, cluster: Cluster, consumer_id: int, producer_ids: Seq) +// 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(spec: TempPred, cluster: Cluster, consumer_id: int, producer_ids: Seq) requires spec.entails(lift_state(cluster.init())), spec.entails(always(lift_action(cluster.next()))), @@ -143,7 +94,7 @@ proof fn consumer_and_producer_properties_hold(spec: TempPred, cluster: assert(spec.entails(always(lift_state(one_does_not_interfere_with_producer::(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 @@ -155,15 +106,80 @@ proof fn consumer_and_producer_properties_hold(spec: TempPred, cluster: assert(spec.entails(always(lift_state(one_does_not_interfere_with_consumer::(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() -> Cluster { + Cluster { + controllers: producers::().push(consumer::()), + } +} + +// 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(spec: TempPred) + requires + spec.entails(lift_state(consumer_and_producers::().init())), + spec.entails(always(lift_action(consumer_and_producers::().next()))), + forall |p_index: int| 0 <= p_index < producers::().len() + ==> #[trigger] spec.entails(producer_fairness::(p_index)), + spec.entails(consumer_fairness::()), + ensures + forall |p_index: int| 0 <= p_index < producers::().len() + ==> #[trigger] spec.entails(producer_property::(p_index)), + spec.entails(consumer_property::()), +{ + let cluster = consumer_and_producers::(); + + let producer_ids = producers::().map(|i: int, producer: Controller| i); + let consumer_id = cluster.controllers.len() - 1; + + assert forall |s| #[trigger] cluster.init()(s) implies consumer::().init()(s) by { + assert forall |i| 0 <= i < cluster.controllers.len() implies #[trigger] cluster.controllers[i].init()(s) by {} + assert(consumer::() =~= cluster.controllers.last()); + } + + assert forall |p_index| #![trigger producers::()[p_index]] 0 <= p_index < producers::().len() + implies forall |s| #[trigger] cluster.init()(s) ==> producers::()[p_index].init()(s) by { + assert forall |s| #[trigger] cluster.init()(s) implies producers::()[p_index].init()(s) by { + assert forall |i| 0 <= i < cluster.controllers.len() implies #[trigger] cluster.controllers[i].init()(s) by {} + assert(producers::()[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::(cluster, good_citizen_id)))) + && forall |p_index: int| 0 <= p_index < producers::().len() + ==> spec.entails(always(lift_state(#[trigger] one_does_not_interfere_with_producer::(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(spec: TempPred, cluster: Cluster, producer_id: int, p_index: int) +proof fn producer_is_correct(spec: TempPred, cluster: Cluster, producer_id: int, p_index: int) requires 0 <= p_index < producers::().len(), 0 <= producer_id < cluster.controllers.len(), @@ -184,7 +200,7 @@ proof fn producer_property_holds_if_no_interference(spec: TempPred, 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(spec: TempPred, cluster: Cluster, consumer_id: int) +proof fn consumer_is_correct(spec: TempPred, cluster: Cluster, consumer_id: int) requires 0 <= consumer_id < cluster.controllers.len(), spec.entails(lift_state(cluster.init())), @@ -205,7 +221,7 @@ proof fn consumer_property_holds_if_no_interference(spec: TempPred, 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(spec: TempPred, cluster: Cluster, good_citizen_id: int, p_index: int) requires @@ -219,7 +235,8 @@ proof fn consumer_does_not_interfere_with_the_producer(spec: TempPred, spec.entails(always(lift_state(one_does_not_interfere_with_producer::(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(spec: TempPred, cluster: Cluster, good_citizen_id: int, p_index: int) requires @@ -233,11 +250,15 @@ proof fn producer_does_not_interfere_with_the_consumer(spec: TempPred, spec.entails(always(lift_state(one_does_not_interfere_with_consumer::(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(spec: TempPred, cluster: Cluster, good_citizen_id: int, p_index: int, q_index: int) requires 0 <= p_index < producers::().len(), 0 <= q_index < producers::().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())), diff --git a/src/soundness/compositionality/state_machine.rs b/src/soundness/compositionality/state_machine.rs index 3277d02b8..06dda2a2d 100644 --- a/src/soundness/compositionality/state_machine.rs +++ b/src/soundness/compositionality/state_machine.rs @@ -68,6 +68,9 @@ impl Cluster { } } + // 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_prime| { &&& 0 <= index < self.controllers.len()