diff --git a/specifications/KeyValueStore/KeyValueStore_proof.tla b/specifications/KeyValueStore/KeyValueStore_proof.tla new file mode 100644 index 00000000..4fe98b0e --- /dev/null +++ b/specifications/KeyValueStore/KeyValueStore_proof.tla @@ -0,0 +1,43 @@ +------------------------- MODULE KeyValueStore_proof ----------------------- +(***************************************************************************) +(* TLAPS proof of *) +(* THEOREM Spec => [](TypeInvariant /\ TxLifecycle) *) +(* stated in KeyValueStore.tla. *) +(***************************************************************************) +EXTENDS KeyValueStore, TLAPS + +Inv == TypeInvariant /\ TxLifecycle + +THEOREM TypeAndLifecycle == Spec => []Inv +<1>1. Init => Inv + BY DEF Init, Inv, TypeInvariant, TxLifecycle, Store +<1>2. Inv /\ [Next]_<> => Inv' + <2> SUFFICES ASSUME Inv, + [Next]_<> + PROVE Inv' + OBVIOUS + <2>. USE DEF Inv, TypeInvariant, TxLifecycle, Store + <2>1. ASSUME NEW t \in TxId, OpenTx(t) + PROVE Inv' + BY <2>1 DEF OpenTx + <2>2. ASSUME NEW t \in tx, NEW k \in Key, NEW v \in Val, Add(t, k, v) + PROVE Inv' + BY <2>2 DEF Add + <2>3. ASSUME NEW t \in tx, NEW k \in Key, NEW v \in Val, Update(t, k, v) + PROVE Inv' + BY <2>3 DEF Update + <2>4. ASSUME NEW t \in tx, NEW k \in Key, Remove(t, k) + PROVE Inv' + BY <2>4 DEF Remove + <2>5. ASSUME NEW t \in tx, RollbackTx(t) + PROVE Inv' + BY <2>5 DEF RollbackTx + <2>6. ASSUME NEW t \in tx, CloseTx(t) + PROVE Inv' + BY <2>6 DEF CloseTx + <2>7. CASE UNCHANGED <> + BY <2>7 + <2>. QED BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7 DEF Next +<1>. QED BY <1>1, <1>2, PTL DEF Spec, Inv + +============================================================================ diff --git a/specifications/MultiCarElevator/Elevator_proof.tla b/specifications/MultiCarElevator/Elevator_proof.tla new file mode 100644 index 00000000..2b6add28 --- /dev/null +++ b/specifications/MultiCarElevator/Elevator_proof.tla @@ -0,0 +1,484 @@ +---------------------------- MODULE Elevator_proof ---------------------------- +(***************************************************************************) +(* Proofs checked by TLAPS about the multi-car elevator specification. *) +(* *) +(* THEOREM TypeCorrect == Spec => []TypeInvariant *) +(* THEOREM SafetyCorrect == Spec => []SafetyInvariant *) +(* *) +(* These cover the safety part of the spec-stub at Elevator.tla:235: *) +(* Spec => [](TypeInvariant /\ SafetyInvariant /\ TemporalInvariant) *) +(* The TemporalInvariant (liveness) part is not addressed here. *) +(* *) +(* Strategy: prove a strengthened state invariant `Inv` and derive both *) +(* TypeInvariant and SafetyInvariant as corollaries. *) +(***************************************************************************) +EXTENDS Elevator, TLAPS + +(***************************************************************************) +(* The spec does not explicitly state that the CONSTANT `Elevator` is *) +(* disjoint from `Floor` (= 1..FloorCount). In TLC the assumption is *) +(* implicit because users supply model values for `Elevator`; we make it *) +(* explicit here so PersonState[p].location \in Floor and *) +(* PersonState[p].location = e \in Elevator can never both hold. *) +(***************************************************************************) +ASSUME ElevatorFloorDisjoint == Floor \cap Elevator = {} + +(***************************************************************************) +(* Function-evaluation primitives. *) +(* *) +(* TLAPS does not currently unfold multi-arg function applications *) +(* `f[a, b]` for definitions `f[x, y \in S] == E` via `BY DEF f`. We *) +(* state the unfolding explicitly here as primitive axioms. These are *) +(* trivially true by the function-application sugar in TLA+. *) +(* *) +(* This is a known TLAPS backend limitation (SMT, Zenon, Isabelle all *) +(* reject the unfolding); see Stephan Merz's reply on the tlaplus list: *) +(* https://discuss.tlapl.us/msg01519.html *) +(* The recommended workaround there is to use either a curried form *) +(* f[x \in S] == [y \in S |-> E] *) +(* or a single-argument form over a Cartesian product *) +(* f[t \in S \X S] == E[x \ t[1], y \ t[2]] *) +(* both of which TLAPS handles via `BY DEF f`. We deliberately do not *) +(* apply those workarounds here because we want to leave the actual spec *) +(* in Elevator.tla unchanged. *) +(***************************************************************************) +LEMMA GetDirectionEval == + ASSUME NEW c \in Floor, NEW d \in Floor + PROVE GetDirection[c, d] = IF d > c THEN "Up" ELSE "Down" + PROOF OMITTED + +LEMMA GetDistanceEval == + ASSUME NEW f1 \in Floor, NEW f2 \in Floor + PROVE GetDistance[f1, f2] = IF f1 > f2 THEN f1 - f2 ELSE f2 - f1 + PROOF OMITTED + +LEMMA CanServiceCallEval == + ASSUME NEW e \in Elevator, NEW c \in ElevatorCall + PROVE CanServiceCall[e, c] <=> + (c.floor = ElevatorState[e].floor /\ c.direction = ElevatorState[e].direction) + PROOF OMITTED + +LEMMA PeopleWaitingEval == + ASSUME NEW f \in Floor, NEW d \in Direction + PROVE PeopleWaiting[f, d] = + {p \in Person : /\ PersonState[p].location = f + /\ PersonState[p].waiting + /\ GetDirection[PersonState[p].location, PersonState[p].destination] = d} + PROOF OMITTED + +(***************************************************************************) +(* Type-level helpers (single-arg, so TLAPS handles via DEF). *) +(***************************************************************************) + +LEMMA DirectionInElevatorDirectionState == + Direction \subseteq ElevatorDirectionState + BY DEF Direction, ElevatorDirectionState + +LEMMA StationaryInElevatorDirectionState == + "Stationary" \in ElevatorDirectionState + BY DEF ElevatorDirectionState + +LEMMA GetDirectionType == + ASSUME NEW c \in Floor, NEW d \in Floor + PROVE GetDirection[c, d] \in Direction + <1>1. GetDirection[c, d] = IF d > c THEN "Up" ELSE "Down" + BY GetDirectionEval + <1>. QED BY <1>1 DEF Direction + +LEMMA ElevatorCallFields == + ASSUME NEW c \in ElevatorCall + PROVE /\ c.floor \in Floor + /\ c.direction \in Direction + BY DEF ElevatorCall + +(***************************************************************************) +(* Strengthened invariant -- enough to prove TypeInvariant inductive. *) +(***************************************************************************) +WaitingFloor == + \A p \in Person : ~PersonState[p].waiting => PersonState[p].location \in Floor + +Inv1 == TypeInvariant /\ WaitingFloor + +(***************************************************************************) +(* Init implies Inv1. *) +(***************************************************************************) +LEMMA InitImpliesInv1 == Init => Inv1 + <1>. SUFFICES ASSUME Init PROVE Inv1 + OBVIOUS + <1>1. PersonState \in [Person -> [location : Floor, destination : Floor, waiting : {FALSE}]] + BY DEF Init + <1>2. ActiveElevatorCalls = {} + BY DEF Init + <1>3. ElevatorState \in [Elevator -> [floor : Floor, + direction : {"Stationary"}, + doorsOpen : {FALSE}, + buttonsPressed : {{}}]] + BY DEF Init + <1>4. TypeInvariant + <2>1. PersonState \in [Person -> [location : Floor \cup Elevator, + destination : Floor, + waiting : BOOLEAN]] + <3>. [location : Floor, destination : Floor, waiting : {FALSE}] + \subseteq [location : Floor \cup Elevator, destination : Floor, waiting : BOOLEAN] + OBVIOUS + <3>. QED BY <1>1 + <2>2. ActiveElevatorCalls \subseteq ElevatorCall + BY <1>2 + <2>3. ElevatorState \in [Elevator -> [floor : Floor, + direction : ElevatorDirectionState, + doorsOpen : BOOLEAN, + buttonsPressed : SUBSET Floor]] + <3>. [floor : Floor, direction : {"Stationary"}, doorsOpen : {FALSE}, buttonsPressed : {{}}] + \subseteq [floor : Floor, direction : ElevatorDirectionState, + doorsOpen : BOOLEAN, buttonsPressed : SUBSET Floor] + BY StationaryInElevatorDirectionState + <3>. QED BY <1>3 + <2>. QED BY <2>1, <2>2, <2>3 DEF TypeInvariant + <1>5. WaitingFloor + BY <1>1 DEF WaitingFloor + <1>. QED BY <1>4, <1>5 DEF Inv1 + +(***************************************************************************) +(* Inductive step. *) +(***************************************************************************) +LEMMA Inv1Next == Inv1 /\ [Next]_Vars => Inv1' + <1>. SUFFICES ASSUME Inv1, [Next]_Vars PROVE Inv1' + OBVIOUS + <1>. USE DEF Inv1, TypeInvariant, WaitingFloor + <1>1. CASE UNCHANGED Vars + BY <1>1 DEF Vars + <1>2. ASSUME NEW p \in Person, PickNewDestination(p) + PROVE Inv1' + BY <1>2 DEF PickNewDestination + <1>3. ASSUME NEW p \in Person, CallElevator(p) + PROVE Inv1' + <2>. USE <1>3 DEF CallElevator + <2>1. PersonState' \in [Person -> [location : Floor \cup Elevator, + destination : Floor, waiting : BOOLEAN]] + OBVIOUS + <2>2. ActiveElevatorCalls' \subseteq ElevatorCall + <3>. DEFINE call == [floor |-> PersonState[p].location, + direction |-> GetDirection[PersonState[p].location, + PersonState[p].destination]] + <3>1. PersonState[p].location \in Floor + \* From WaitingFloor + ~waiting precondition. + OBVIOUS + <3>2. PersonState[p].destination \in Floor + OBVIOUS + <3>3. GetDirection[PersonState[p].location, PersonState[p].destination] \in Direction + BY <3>1, <3>2, GetDirectionType + <3>4. call \in ElevatorCall + BY <3>1, <3>3 DEF ElevatorCall + <3>. QED BY <3>4 + <2>3. ElevatorState' \in [Elevator -> [floor : Floor, + direction : ElevatorDirectionState, + doorsOpen : BOOLEAN, + buttonsPressed : SUBSET Floor]] + OBVIOUS + <2>4. WaitingFloor' + \* For p: waiting'(p)=TRUE, so premise FALSE, vacuous. For other q: unchanged. + BY DEF WaitingFloor + <2>. QED BY <2>1, <2>2, <2>3, <2>4 DEF TypeInvariant + <1>4. ASSUME NEW e \in Elevator, OpenElevatorDoors(e) + PROVE Inv1' + <2>. USE <1>4 DEF OpenElevatorDoors + <2>1. PersonState' = PersonState + OBVIOUS + <2>2. ActiveElevatorCalls' \subseteq ElevatorCall + OBVIOUS + <2>3. ElevatorState' \in [Elevator -> [floor : Floor, + direction : ElevatorDirectionState, + doorsOpen : BOOLEAN, + buttonsPressed : SUBSET Floor]] + OBVIOUS + <2>. QED BY <2>1, <2>2, <2>3 DEF TypeInvariant, WaitingFloor + <1>5. ASSUME NEW e \in Elevator, EnterElevator(e) + PROVE Inv1' + <2>. USE <1>5 DEF EnterElevator + <2>1. PersonState' \in [Person -> [location : Floor \cup Elevator, + destination : Floor, waiting : BOOLEAN]] + OBVIOUS + <2>2. ActiveElevatorCalls' = ActiveElevatorCalls + OBVIOUS + <2>3. ElevatorState' \in [Elevator -> [floor : Floor, + direction : ElevatorDirectionState, + doorsOpen : BOOLEAN, + buttonsPressed : SUBSET Floor]] + <3>. DEFINE eState == ElevatorState[e] + gettingOn == PeopleWaiting[eState.floor, eState.direction] + destinations == {PersonState[p1].destination : p1 \in gettingOn} + <3>0. \A p1 \in Person : PersonState[p1].destination \in Floor + BY DEF TypeInvariant + <3>0a. eState.floor \in Floor /\ eState.direction \in Direction + BY DEF TypeInvariant, Direction, ElevatorDirectionState + <3>0b. gettingOn \subseteq Person + <4>1. gettingOn = {p2 \in Person : /\ PersonState[p2].location = eState.floor + /\ PersonState[p2].waiting + /\ GetDirection[PersonState[p2].location, PersonState[p2].destination] = eState.direction} + BY <3>0a, PeopleWaitingEval + <4>. QED BY <4>1 + <3>1. destinations \subseteq Floor + BY <3>0, <3>0b + <3>2. eState.buttonsPressed \cup destinations \subseteq Floor + BY <3>1 + <3>. QED BY <3>2 + <2>4. WaitingFloor' + \* For p \in gettingOn, location' = e (Elevator), waiting unchanged. + \* gettingOn members have waiting = TRUE (PeopleWaiting requires waiting). + \* So if ~waiting'(p1), then p1 \notin gettingOn, so location' = location \in Floor. + <3>. SUFFICES ASSUME NEW p1 \in Person, ~PersonState'[p1].waiting + PROVE PersonState'[p1].location \in Floor + BY DEF WaitingFloor + <3>. DEFINE eState == ElevatorState[e] + gettingOn == PeopleWaiting[eState.floor, eState.direction] + <3>1. PersonState'[p1].waiting = PersonState[p1].waiting + OBVIOUS + <3>2. ~PersonState[p1].waiting + BY <3>1 + <3>3. PersonState[p1].location \in Floor + BY <3>2 DEF WaitingFloor + <3>4. eState.direction \in Direction + \* From EnterElevator's precondition: direction != "Stationary". + BY DEF Direction, ElevatorDirectionState + <3>5. eState.floor \in Floor + OBVIOUS + <3>6. p1 \notin gettingOn + \* PeopleWaiting requires waiting = TRUE, so p1 (with ~waiting) isn't in. + BY <3>2, <3>4, <3>5, PeopleWaitingEval + <3>7. PersonState'[p1] = PersonState[p1] + BY <3>6 + <3>. QED BY <3>3, <3>7 + <2>. QED BY <2>1, <2>2, <2>3, <2>4 DEF TypeInvariant + <1>6. ASSUME NEW e \in Elevator, ExitElevator(e) + PROVE Inv1' + <2>. USE <1>6 DEF ExitElevator + <2>1. PersonState' \in [Person -> [location : Floor \cup Elevator, + destination : Floor, waiting : BOOLEAN]] + OBVIOUS + <2>2. ActiveElevatorCalls' = ActiveElevatorCalls + OBVIOUS + <2>3. ElevatorState' = ElevatorState + OBVIOUS + <2>4. WaitingFloor' + \* Persons in gettingOff have location' = eState.floor \in Floor, waiting' = FALSE. + <3>. SUFFICES ASSUME NEW p1 \in Person, ~PersonState'[p1].waiting + PROVE PersonState'[p1].location \in Floor + BY DEF WaitingFloor + <3>. DEFINE eState == ElevatorState[e] + gettingOff == {pp \in Person : PersonState[pp].location = e + /\ PersonState[pp].destination = eState.floor} + <3>1. CASE p1 \in gettingOff + <4>1. PersonState'[p1].location = eState.floor + BY <3>1 + <4>. QED BY <4>1 + <3>2. CASE p1 \notin gettingOff + <4>1. PersonState'[p1] = PersonState[p1] + BY <3>2 + <4>2. ~PersonState[p1].waiting + BY <4>1 + <4>3. PersonState[p1].location \in Floor + BY <4>2 DEF WaitingFloor + <4>. QED BY <4>1, <4>3 + <3>. QED BY <3>1, <3>2 + <2>. QED BY <2>1, <2>2, <2>3, <2>4 DEF TypeInvariant + <1>7. ASSUME NEW e \in Elevator, CloseElevatorDoors(e) + PROVE Inv1' + BY <1>7 DEF CloseElevatorDoors + <1>8. ASSUME NEW e \in Elevator, MoveElevator(e) + PROVE Inv1' + BY <1>8 DEF MoveElevator + <1>9. ASSUME NEW e \in Elevator, StopElevator(e) + PROVE Inv1' + <2>. USE <1>9 DEF StopElevator + <2>1. ElevatorState' \in [Elevator -> [floor : Floor, + direction : ElevatorDirectionState, + doorsOpen : BOOLEAN, + buttonsPressed : SUBSET Floor]] + BY StationaryInElevatorDirectionState + <2>. QED BY <2>1 + <1>10. ASSUME NEW c \in ElevatorCall, DispatchElevator(c) + PROVE Inv1' + <2>. USE <1>10 DEF DispatchElevator + <2>1. PersonState' = PersonState + OBVIOUS + <2>2. ActiveElevatorCalls' = ActiveElevatorCalls + OBVIOUS + <2>3. c.floor \in Floor /\ c.direction \in Direction + BY ElevatorCallFields + <2>4. ElevatorState' \in [Elevator -> [floor : Floor, + direction : ElevatorDirectionState, + doorsOpen : BOOLEAN, + buttonsPressed : SUBSET Floor]] + \* DispatchElevator's effect: ElevatorState' is either ElevatorState + \* (if closest \notin stationary) or [ElevatorState EXCEPT ![closest] + \* = [@ EXCEPT !.floor = c.floor, !.direction = c.direction]] for some + \* closest \in Elevator. In both cases the type schema is preserved. + <3>. DEFINE T == [floor : Floor, direction : ElevatorDirectionState, + doorsOpen : BOOLEAN, buttonsPressed : SUBSET Floor] + <3>1. ASSUME NEW closest \in Elevator + PROVE [ElevatorState[closest] EXCEPT !.floor = c.floor, !.direction = c.direction] \in T + BY <2>3, DirectionInElevatorDirectionState DEF TypeInvariant + <3>. QED + BY <3>1, <2>3, DirectionInElevatorDirectionState DEF TypeInvariant + <2>. QED BY <2>1, <2>2, <2>4 + <1>. QED + BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6, <1>7, <1>8, <1>9, <1>10 DEF Next + +(***************************************************************************) +(* Spec => []TypeInvariant. *) +(***************************************************************************) +THEOREM TypeCorrect == Spec => []TypeInvariant + <1>1. Inv1 => TypeInvariant + BY DEF Inv1 + <1>. QED BY InitImpliesInv1, Inv1Next, <1>1, PTL DEF Spec + +(***************************************************************************) +(* Strengthened invariant for SafetyInvariant. *) +(* *) +(* The seven auxiliaries (besides TypeInvariant + WaitingFloor + *) +(* SafetyInvariant) are mutually inductive: each is needed to discharge *) +(* one of the per-action obligations of the others. *) +(* *) +(* WaitingDestinationDistinct *) +(* waiting(p) => location(p) /= destination(p) *) +(* DoorsOpenImpliesNotInButtonsPressed *) +(* doorsOpen(e) => floor(e) \notin buttonsPressed(e) *) +(* NoServiceableActiveCall *) +(* doorsOpen(e) /\ direction(e) \in Direction => *) +(* [floor(e), direction(e)] \notin ActiveElevatorCalls *) +(* DoorsOpenImpliesNotStationary *) +(* doorsOpen(e) => direction(e) \in Direction *) +(* StationaryNoPassenger *) +(* direction(e) = "Stationary" => \A p : location(p) /= e *) +(* PersonImpliesButton *) +(* location(p) = e => *) +(* destination(p) \in buttonsPressed(e) *) +(* \/ (doorsOpen(e) /\ floor(e) = destination(p)) *) +(* PersonInElevatorDirection (== SafetyInvariant Property 2) *) +(***************************************************************************) +WaitingDestinationDistinct == + \A p \in Person : + PersonState[p].waiting => PersonState[p].location /= PersonState[p].destination + +DoorsOpenImpliesNotInButtonsPressed == + \A e \in Elevator : + ElevatorState[e].doorsOpen => + ElevatorState[e].floor \notin ElevatorState[e].buttonsPressed + +NoServiceableActiveCall == + \A e \in Elevator : + (ElevatorState[e].doorsOpen /\ ElevatorState[e].direction \in Direction) => + [floor |-> ElevatorState[e].floor, direction |-> ElevatorState[e].direction] + \notin ActiveElevatorCalls + +DoorsOpenImpliesNotStationary == + \A e \in Elevator : + ElevatorState[e].doorsOpen => ElevatorState[e].direction \in Direction + +StationaryNoPassenger == + \A e \in Elevator : + ElevatorState[e].direction = "Stationary" => + \A p \in Person : PersonState[p].location /= e + +PersonImpliesButton == + \A p \in Person, e \in Elevator : + PersonState[p].location = e => + \/ PersonState[p].destination \in ElevatorState[e].buttonsPressed + \/ (ElevatorState[e].doorsOpen + /\ ElevatorState[e].floor = PersonState[p].destination) + +Inv2 == + /\ Inv1 + /\ WaitingDestinationDistinct + /\ DoorsOpenImpliesNotInButtonsPressed + /\ NoServiceableActiveCall + /\ DoorsOpenImpliesNotStationary + /\ StationaryNoPassenger + /\ PersonImpliesButton + /\ SafetyInvariant + +(***************************************************************************) +(* The full Spec => []Inv2 proof is OMITTED. The seven auxiliary *) +(* invariants above plus TypeInvariant and SafetyInvariant are mutually *) +(* inductive (each discharges one of the per-action obligations of the *) +(* others); closing the inductive step requires: *) +(* *) +(* - per-action case analysis (9 actions + stutter) for each of the *) +(* ~10 conjuncts (~90 inductive sub-cases), *) +(* - explicit `~ENABLED EnterElevator(e)` / `~ENABLED ExitElevator(e)` *) +(* / `~ENABLED OpenElevatorDoors(e)` reasoning via `ExpandENABLED` *) +(* (used by CloseElevatorDoors and StopElevator), *) +(* - careful arithmetic on `Floor = 1..FloorCount` for the *) +(* extreme-floor argument that closes the StopElevator case for *) +(* SafetyInvariant Property 2. *) +(* *) +(* This is genuine Band-H work, comparable to the EWD998 refinement *) +(* proof, and is left to a follow-up. *) +(***************************************************************************) +LEMMA InitImpliesInv2 == Init => Inv2 + <1>. SUFFICES ASSUME Init PROVE Inv2 + OBVIOUS + <1>1. Inv1 + BY InitImpliesInv1 + <1>2. PersonState \in [Person -> [location : Floor, destination : Floor, waiting : {FALSE}]] + BY DEF Init + <1>3. ActiveElevatorCalls = {} + BY DEF Init + <1>4. ElevatorState \in [Elevator -> [floor : Floor, + direction : {"Stationary"}, + doorsOpen : {FALSE}, + buttonsPressed : {{}}]] + BY DEF Init + <1>. \A p \in Person : PersonState[p].waiting = FALSE + BY <1>2 + <1>. \A e \in Elevator : ElevatorState[e].doorsOpen = FALSE + /\ ElevatorState[e].direction = "Stationary" + /\ ElevatorState[e].buttonsPressed = {} + BY <1>4 + <1>. \A p \in Person : PersonState[p].location \in Floor + BY <1>2 + <1>5. WaitingDestinationDistinct + BY DEF WaitingDestinationDistinct + <1>6. DoorsOpenImpliesNotInButtonsPressed + BY DEF DoorsOpenImpliesNotInButtonsPressed + <1>7. NoServiceableActiveCall + BY <1>3 DEF NoServiceableActiveCall + <1>8. DoorsOpenImpliesNotStationary + BY DEF DoorsOpenImpliesNotStationary + <1>9. StationaryNoPassenger + \* PersonState[p].location \in Floor for all p (by Init), so + \* location(p) /= e for any e \in Elevator (using ElevatorFloorDisjoint). + <2>. SUFFICES ASSUME NEW e \in Elevator, NEW p \in Person + PROVE PersonState[p].location /= e + BY DEF StationaryNoPassenger + <2>1. PersonState[p].location \in Floor + BY <1>2 + <2>. QED BY <2>1, ElevatorFloorDisjoint + <1>10. PersonImpliesButton + \* Same reasoning: location \in Floor implies premise FALSE. + <2>. SUFFICES ASSUME NEW p \in Person, NEW e \in Elevator, + PersonState[p].location = e + PROVE FALSE + BY DEF PersonImpliesButton + <2>1. PersonState[p].location \in Floor + BY <1>2 + <2>. QED BY <2>1, ElevatorFloorDisjoint + <1>11. SafetyInvariant + <2>1. \A e \in Elevator : ElevatorState[e].buttonsPressed = {} + BY <1>4 + <2>2. \A p \in Person, e \in Elevator : PersonState[p].location /= e + BY <1>2, ElevatorFloorDisjoint + <2>. QED + BY <2>1, <2>2, <1>3 DEF SafetyInvariant + <1>. QED + BY <1>1, <1>5, <1>6, <1>7, <1>8, <1>9, <1>10, <1>11 DEF Inv2 + +LEMMA Inv2Next == Inv2 /\ [Next]_Vars => Inv2' + PROOF OMITTED + +THEOREM SafetyCorrect == Spec => []SafetyInvariant + <1>1. Inv2 => SafetyInvariant + BY DEF Inv2 + <1>. QED BY InitImpliesInv2, Inv2Next, <1>1, PTL DEF Spec + +============================================================================= diff --git a/specifications/PaxosHowToWinATuringAward/Voting_proof.tla b/specifications/PaxosHowToWinATuringAward/Voting_proof.tla new file mode 100644 index 00000000..504ce146 --- /dev/null +++ b/specifications/PaxosHowToWinATuringAward/Voting_proof.tla @@ -0,0 +1,142 @@ +--------------------------- MODULE Voting_proof ---------------------------- +(***************************************************************************) +(* TLAPS proofs of theorems stated in Voting.tla. The spec is essentially *) +(* the same as Paxos/Voting.tla; the proofs are direct ports. *) +(* *) +(* AllSafeAtZero (Band E) *) +(* ChoosableThm (Band E) *) +(* ShowsSafety (Band M) *) +(* *) +(* Invariance and Implementation depend on a SafeAtMonotone lemma not yet *) +(* established; see Paxos/Voting_proof.tla for the same deferral. *) +(***************************************************************************) +EXTENDS Voting + +LEMMA QuorumNonEmpty == \A Q \in Quorum : Q # {} +BY QuorumAssumption + +(***************************************************************************) +(* HELPERS *) +(***************************************************************************) + +THEOREM AllSafeAtZero_T == \A v \in Value : SafeAt(0, v) +BY DEF SafeAt + +THEOREM ChoosableThm_T == + \A b \in Ballot, v \in Value : ChosenAt(b, v) => NoneOtherChoosableAt(b, v) +<1>1. SUFFICES ASSUME NEW b \in Ballot, NEW v \in Value, ChosenAt(b, v) + PROVE NoneOtherChoosableAt(b, v) + OBVIOUS +<1>2. PICK Q \in Quorum : \A a \in Q : VotedFor(a, b, v) + BY <1>1 DEF ChosenAt +<1>. QED BY <1>2 DEF NoneOtherChoosableAt + +(***************************************************************************) +(* OneValuePerBallot in ASSUME/PROVE form. *) +(***************************************************************************) +LEMMA OneValuePerBallotApply == + ASSUME OneValuePerBallot, + NEW a1 \in Acceptor, NEW a2 \in Acceptor, NEW bb \in Ballot, + NEW v1 \in Value, NEW v2 \in Value, + VotedFor(a1, bb, v1), VotedFor(a2, bb, v2) + PROVE v1 = v2 +BY DEF OneValuePerBallot + +(***************************************************************************) +(* Convenience: any two quorums intersect in at least one acceptor. *) +(***************************************************************************) +LEMMA QuorumIntersect == + ASSUME NEW Q1 \in Quorum, NEW Q2 \in Quorum + PROVE \E a \in Q1 \cap Q2 : a \in Acceptor +<1>1. Q1 \cap Q2 # {} + BY QuorumAssumption +<1>2. PICK a \in Q1 \cap Q2 : TRUE + BY <1>1 +<1>3. a \in Acceptor + BY <1>2, QuorumAssumption +<1>. QED BY <1>2, <1>3 + +(***************************************************************************) +(* ShowsSafety (Band M) *) +(***************************************************************************) + +THEOREM ShowsSafety_T == + Inv => \A Q \in Quorum, b \in Ballot, v \in Value : + ShowsSafeAt(Q, b, v) => SafeAt(b, v) +<1>0. SUFFICES ASSUME Inv, + NEW Q \in Quorum, NEW b \in Ballot, NEW v \in Value, + ShowsSafeAt(Q, b, v) + PROVE SafeAt(b, v) + OBVIOUS +<1>0a. TypeOK /\ VotesSafe /\ OneValuePerBallot + BY <1>0 DEF Inv +<1>1. \A a \in Q : maxBal[a] >= b + BY <1>0 DEF ShowsSafeAt +<1>2. PICK c \in -1..(b-1) : + /\ (c /= -1) => \E a \in Q : VotedFor(a, c, v) + /\ \A d \in (c+1)..(b-1), a \in Q : DidNotVoteAt(a, d) + BY <1>0 DEF ShowsSafeAt +<1>3. Q \subseteq Acceptor + BY QuorumAssumption +<1>4. SUFFICES ASSUME NEW c0 \in 0..(b-1) + PROVE NoneOtherChoosableAt(c0, v) + BY DEF SafeAt +<1>5. b \in Nat /\ c0 \in Nat + BY DEF Ballot +<1>6. CASE c0 > c + <2>1. c0 \in (c+1)..(b-1) + BY <1>5, <1>2, <1>6 + <2>2. \A a \in Q : DidNotVoteAt(a, c0) + BY <1>2, <2>1 + <2>3. \A a \in Q : maxBal[a] \in Ballot \cup {-1} + BY <1>3, <1>0a DEF TypeOK + <2>4. \A a \in Q : maxBal[a] > c0 + BY <1>1, <2>3, <1>5, <1>6 DEF Ballot + <2>5. \A a \in Q : VotedFor(a, c0, v) \/ CannotVoteAt(a, c0) + BY <2>2, <2>4 DEF CannotVoteAt + <2>. QED BY <2>5 DEF NoneOtherChoosableAt +<1>7. CASE c0 = c + <2>1. c \in Nat + BY <1>5, <1>7 + <2>2. c \in Ballot + BY <2>1 DEF Ballot + <2>3. PICK aStar \in Q : VotedFor(aStar, c, v) + BY <1>2, <1>5, <1>7 + <2>4. aStar \in Acceptor + BY <1>3, <2>3 + <2>5. \A a \in Q : VotedFor(a, c, v) \/ DidNotVoteAt(a, c) + <3> SUFFICES ASSUME NEW a \in Q, + ~ DidNotVoteAt(a, c) + PROVE VotedFor(a, c, v) + OBVIOUS + <3>1. PICK w \in Value : VotedFor(a, c, w) + BY DEF DidNotVoteAt + <3>2. a \in Acceptor + BY <1>3 + <3>3. w = v + BY <2>3, <2>4, <3>1, <3>2, <2>2, <1>0a, OneValuePerBallotApply + <3>. QED BY <3>1, <3>3 + <2>6. \A a \in Q : maxBal[a] \in Ballot \cup {-1} + BY <1>3, <1>0a DEF TypeOK + <2>7. \A a \in Q : maxBal[a] > c + BY <1>1, <2>6, <1>5, <1>7, <2>1 DEF Ballot + <2>8. \A a \in Q : VotedFor(a, c, v) \/ CannotVoteAt(a, c) + BY <2>5, <2>7 DEF CannotVoteAt + <2>. QED BY <2>8, <1>7 DEF NoneOtherChoosableAt +<1>8. CASE c0 < c + <2>1. c \in Nat /\ c0 < c + BY <1>5, <1>8 + <2>2. c \in Ballot + BY <2>1 DEF Ballot + <2>3. PICK aStar \in Q : VotedFor(aStar, c, v) + BY <1>2, <1>5, <1>8 + <2>4. aStar \in Acceptor + BY <1>3, <2>3 + <2>5. SafeAt(c, v) + BY <2>3, <2>4, <2>2, <1>0a DEF VotesSafe + <2>6. c0 \in 0..(c-1) + BY <1>5, <2>1 + <2>. QED BY <2>5, <2>6 DEF SafeAt +<1>. QED BY <1>6, <1>7, <1>8 + +============================================================================ diff --git a/specifications/SpecifyingSystems/AsynchronousInterface/AsynchInterface_proof.tla b/specifications/SpecifyingSystems/AsynchronousInterface/AsynchInterface_proof.tla new file mode 100644 index 00000000..52d61c3e --- /dev/null +++ b/specifications/SpecifyingSystems/AsynchronousInterface/AsynchInterface_proof.tla @@ -0,0 +1,14 @@ +------------------------ MODULE AsynchInterface_proof ---------------------- +(***************************************************************************) +(* TLAPS proof of the theorem stated in AsynchInterface.tla. *) +(***************************************************************************) +EXTENDS AsynchInterface, TLAPS + +THEOREM TypeCorrect == Spec => []TypeInvariant +<1>1. Init => TypeInvariant + BY DEF Init, TypeInvariant +<1>2. TypeInvariant /\ [Next]_<> => TypeInvariant' + BY DEF TypeInvariant, Next, Send, Rcv +<1>. QED BY <1>1, <1>2, PTL DEF Spec + +============================================================================ diff --git a/specifications/SpecifyingSystems/AsynchronousInterface/Channel_proof.tla b/specifications/SpecifyingSystems/AsynchronousInterface/Channel_proof.tla new file mode 100644 index 00000000..9cf3e494 --- /dev/null +++ b/specifications/SpecifyingSystems/AsynchronousInterface/Channel_proof.tla @@ -0,0 +1,14 @@ +--------------------------- MODULE Channel_proof --------------------------- +(***************************************************************************) +(* TLAPS proof of the theorem stated in Channel.tla. *) +(***************************************************************************) +EXTENDS Channel, TLAPS + +THEOREM TypeCorrect == Spec => []TypeInvariant +<1>1. Init => TypeInvariant + BY DEF Init +<1>2. TypeInvariant /\ [Next]_chan => TypeInvariant' + BY DEF TypeInvariant, Next, Send, Rcv +<1>. QED BY <1>1, <1>2, PTL DEF Spec + +============================================================================ diff --git a/specifications/SpecifyingSystems/CachingMemory/InternalMemory_proof.tla b/specifications/SpecifyingSystems/CachingMemory/InternalMemory_proof.tla new file mode 100644 index 00000000..5ae8971f --- /dev/null +++ b/specifications/SpecifyingSystems/CachingMemory/InternalMemory_proof.tla @@ -0,0 +1,76 @@ +------------------------- MODULE InternalMemory_proof ---------------------- +(***************************************************************************) +(* TLAPS proof of *) +(* *) +(* THEOREM ISpec => []TypeInvariant *) +(* *) +(* stated in InternalMemory.tla. *) +(* *) +(* TypeInvariant alone is not inductive: in Do(p), the next-state *) +(* expression accesses buf[p].adr / buf[p].op, which only makes sense *) +(* when buf[p] is in MReq. We strengthen TypeInvariant with *) +(* BufConsistent, which records the buf typing for each value of ctl[p]. *) +(***************************************************************************) +EXTENDS InternalMemory, TLAPS + +BufConsistent == + /\ \A p \in Proc : (ctl[p] = "rdy") => (buf[p] \in Val \cup {NoVal}) + /\ \A p \in Proc : (ctl[p] = "busy") => (buf[p] \in MReq) + /\ \A p \in Proc : (ctl[p] = "done") => (buf[p] \in Val \cup {NoVal}) + +Inv == TypeInvariant /\ BufConsistent + +LEMMA InvInductive == ISpec => []Inv +<1>1. IInit => Inv + BY DEF IInit, Inv, TypeInvariant, BufConsistent +<1>2. Inv /\ [INext]_<> => Inv' + <2> SUFFICES ASSUME Inv, + [INext]_<> + PROVE Inv' + OBVIOUS + <2>. USE DEF Inv, TypeInvariant, BufConsistent + <2>1. ASSUME NEW p \in Proc, Req(p) + PROVE Inv' + \* After Req(p): ctl[p]' = "busy", buf[p]' \in MReq. For q # p, + \* ctl/buf unchanged. mem unchanged. + BY <2>1 DEF Req + <2>2. ASSUME NEW p \in Proc, Do(p) + PROVE Inv' + \* Pre: ctl[p] = "busy", so buf[p] \in MReq, hence buf[p].adr \in Adr, + \* and buf[p].op \in {"Rd","Wr"}. + <3>1. buf[p] \in MReq + BY <2>2 DEF Do + <3>2. buf[p].adr \in Adr /\ buf[p].op \in {"Rd","Wr"} + BY <3>1 DEF MReq + <3>3. CASE buf[p].op = "Wr" + \* mem' \in [Adr->Val] because we update at adr \in Adr to val \in Val. + \* buf[p]' = NoVal \in Val \cup {NoVal}, ctl[p]' = "done". + <4>1. buf[p].val \in Val + BY <3>1, <3>3 DEF MReq + <4>2. mem' = [mem EXCEPT ![buf[p].adr] = buf[p].val] + BY <2>2, <3>3 DEF Do + <4>3. mem' \in [Adr -> Val] + BY <3>2, <4>1, <4>2 + <4>. QED BY <2>2, <3>3, <4>3 DEF Do + <3>4. CASE buf[p].op = "Rd" + \* mem' = mem. buf[p]' = mem[buf[p].adr] \in Val. ctl[p]' = "done". + <4>1. mem' = mem + BY <2>2, <3>4 DEF Do + <4>2. mem[buf[p].adr] \in Val + BY <3>2 + <4>. QED BY <2>2, <3>4, <4>1, <4>2 DEF Do + <3>. QED BY <3>2, <3>3, <3>4 + <2>3. ASSUME NEW p \in Proc, Rsp(p) + PROVE Inv' + \* ctl[p]' = "rdy"; buf, mem unchanged. buf[p] was \in Val \cup {NoVal} + \* (since pre ctl[p] = "done"), so it remains so under "rdy". + BY <2>3 DEF Rsp + <2>4. CASE UNCHANGED <> + BY <2>4 + <2>. QED BY <2>1, <2>2, <2>3, <2>4 DEF INext +<1>. QED BY <1>1, <1>2, PTL DEF ISpec + +THEOREM TypeCorrect == ISpec => []TypeInvariant +BY InvInductive, PTL DEF Inv + +============================================================================ diff --git a/specifications/SpecifyingSystems/Composing/Channel_proof.tla b/specifications/SpecifyingSystems/Composing/Channel_proof.tla new file mode 100644 index 00000000..9cf3e494 --- /dev/null +++ b/specifications/SpecifyingSystems/Composing/Channel_proof.tla @@ -0,0 +1,14 @@ +--------------------------- MODULE Channel_proof --------------------------- +(***************************************************************************) +(* TLAPS proof of the theorem stated in Channel.tla. *) +(***************************************************************************) +EXTENDS Channel, TLAPS + +THEOREM TypeCorrect == Spec => []TypeInvariant +<1>1. Init => TypeInvariant + BY DEF Init +<1>2. TypeInvariant /\ [Next]_chan => TypeInvariant' + BY DEF TypeInvariant, Next, Send, Rcv +<1>. QED BY <1>1, <1>2, PTL DEF Spec + +============================================================================ diff --git a/specifications/SpecifyingSystems/Composing/HourClock_proof.tla b/specifications/SpecifyingSystems/Composing/HourClock_proof.tla new file mode 100644 index 00000000..6d396e14 --- /dev/null +++ b/specifications/SpecifyingSystems/Composing/HourClock_proof.tla @@ -0,0 +1,14 @@ +-------------------------- MODULE HourClock_proof -------------------------- +(***************************************************************************) +(* TLAPS proof of the theorem stated in HourClock.tla. *) +(***************************************************************************) +EXTENDS HourClock, TLAPS + +THEOREM HCini_Invariant == HC => []HCini +<1>1. HCini => HCini + OBVIOUS +<1>2. HCini /\ [HCnxt]_hr => HCini' + BY DEF HCini, HCnxt +<1>. QED BY <1>1, <1>2, PTL DEF HC + +============================================================================ diff --git a/specifications/SpecifyingSystems/Composing/InternalMemory_proof.tla b/specifications/SpecifyingSystems/Composing/InternalMemory_proof.tla new file mode 100644 index 00000000..5ae8971f --- /dev/null +++ b/specifications/SpecifyingSystems/Composing/InternalMemory_proof.tla @@ -0,0 +1,76 @@ +------------------------- MODULE InternalMemory_proof ---------------------- +(***************************************************************************) +(* TLAPS proof of *) +(* *) +(* THEOREM ISpec => []TypeInvariant *) +(* *) +(* stated in InternalMemory.tla. *) +(* *) +(* TypeInvariant alone is not inductive: in Do(p), the next-state *) +(* expression accesses buf[p].adr / buf[p].op, which only makes sense *) +(* when buf[p] is in MReq. We strengthen TypeInvariant with *) +(* BufConsistent, which records the buf typing for each value of ctl[p]. *) +(***************************************************************************) +EXTENDS InternalMemory, TLAPS + +BufConsistent == + /\ \A p \in Proc : (ctl[p] = "rdy") => (buf[p] \in Val \cup {NoVal}) + /\ \A p \in Proc : (ctl[p] = "busy") => (buf[p] \in MReq) + /\ \A p \in Proc : (ctl[p] = "done") => (buf[p] \in Val \cup {NoVal}) + +Inv == TypeInvariant /\ BufConsistent + +LEMMA InvInductive == ISpec => []Inv +<1>1. IInit => Inv + BY DEF IInit, Inv, TypeInvariant, BufConsistent +<1>2. Inv /\ [INext]_<> => Inv' + <2> SUFFICES ASSUME Inv, + [INext]_<> + PROVE Inv' + OBVIOUS + <2>. USE DEF Inv, TypeInvariant, BufConsistent + <2>1. ASSUME NEW p \in Proc, Req(p) + PROVE Inv' + \* After Req(p): ctl[p]' = "busy", buf[p]' \in MReq. For q # p, + \* ctl/buf unchanged. mem unchanged. + BY <2>1 DEF Req + <2>2. ASSUME NEW p \in Proc, Do(p) + PROVE Inv' + \* Pre: ctl[p] = "busy", so buf[p] \in MReq, hence buf[p].adr \in Adr, + \* and buf[p].op \in {"Rd","Wr"}. + <3>1. buf[p] \in MReq + BY <2>2 DEF Do + <3>2. buf[p].adr \in Adr /\ buf[p].op \in {"Rd","Wr"} + BY <3>1 DEF MReq + <3>3. CASE buf[p].op = "Wr" + \* mem' \in [Adr->Val] because we update at adr \in Adr to val \in Val. + \* buf[p]' = NoVal \in Val \cup {NoVal}, ctl[p]' = "done". + <4>1. buf[p].val \in Val + BY <3>1, <3>3 DEF MReq + <4>2. mem' = [mem EXCEPT ![buf[p].adr] = buf[p].val] + BY <2>2, <3>3 DEF Do + <4>3. mem' \in [Adr -> Val] + BY <3>2, <4>1, <4>2 + <4>. QED BY <2>2, <3>3, <4>3 DEF Do + <3>4. CASE buf[p].op = "Rd" + \* mem' = mem. buf[p]' = mem[buf[p].adr] \in Val. ctl[p]' = "done". + <4>1. mem' = mem + BY <2>2, <3>4 DEF Do + <4>2. mem[buf[p].adr] \in Val + BY <3>2 + <4>. QED BY <2>2, <3>4, <4>1, <4>2 DEF Do + <3>. QED BY <3>2, <3>3, <3>4 + <2>3. ASSUME NEW p \in Proc, Rsp(p) + PROVE Inv' + \* ctl[p]' = "rdy"; buf, mem unchanged. buf[p] was \in Val \cup {NoVal} + \* (since pre ctl[p] = "done"), so it remains so under "rdy". + BY <2>3 DEF Rsp + <2>4. CASE UNCHANGED <> + BY <2>4 + <2>. QED BY <2>1, <2>2, <2>3, <2>4 DEF INext +<1>. QED BY <1>1, <1>2, PTL DEF ISpec + +THEOREM TypeCorrect == ISpec => []TypeInvariant +BY InvInductive, PTL DEF Inv + +============================================================================ diff --git a/specifications/SpecifyingSystems/FIFO/Channel_proof.tla b/specifications/SpecifyingSystems/FIFO/Channel_proof.tla new file mode 100644 index 00000000..9cf3e494 --- /dev/null +++ b/specifications/SpecifyingSystems/FIFO/Channel_proof.tla @@ -0,0 +1,14 @@ +--------------------------- MODULE Channel_proof --------------------------- +(***************************************************************************) +(* TLAPS proof of the theorem stated in Channel.tla. *) +(***************************************************************************) +EXTENDS Channel, TLAPS + +THEOREM TypeCorrect == Spec => []TypeInvariant +<1>1. Init => TypeInvariant + BY DEF Init +<1>2. TypeInvariant /\ [Next]_chan => TypeInvariant' + BY DEF TypeInvariant, Next, Send, Rcv +<1>. QED BY <1>1, <1>2, PTL DEF Spec + +============================================================================ diff --git a/specifications/SpecifyingSystems/FIFO/InnerFIFO_proof.tla b/specifications/SpecifyingSystems/FIFO/InnerFIFO_proof.tla new file mode 100644 index 00000000..b90dd86e --- /dev/null +++ b/specifications/SpecifyingSystems/FIFO/InnerFIFO_proof.tla @@ -0,0 +1,35 @@ +------------------------- MODULE InnerFIFO_proof --------------------------- +(***************************************************************************) +(* TLAPS proof of *) +(* THEOREM Spec => []TypeInvariant *) +(* stated in InnerFIFO.tla. *) +(***************************************************************************) +EXTENDS InnerFIFO, TLAPS + +THEOREM TypeCorrect == Spec => []TypeInvariant +<1>1. Init => TypeInvariant + BY DEF Init, TypeInvariant, + InChan!Init, OutChan!Init, + InChan!TypeInvariant, OutChan!TypeInvariant +<1>2. TypeInvariant /\ [Next]_<> => TypeInvariant' + <2> SUFFICES ASSUME TypeInvariant, [Next]_<> + PROVE TypeInvariant' + OBVIOUS + <2>. USE DEF TypeInvariant, InChan!TypeInvariant, OutChan!TypeInvariant + <2>1. ASSUME NEW msg \in Message, SSend(msg) + PROVE TypeInvariant' + BY <2>1 DEF SSend, InChan!Send + <2>2. CASE BufRcv + BY <2>2 DEF BufRcv, InChan!Rcv + <2>3. CASE BufSend + \* OutChan!Send(Head(q)) requires Head(q) \in Message; q \in Seq(Message) + \* and q # <<>>, so Head(q) \in Message. + BY <2>3 DEF BufSend, OutChan!Send + <2>4. CASE RRcv + BY <2>4 DEF RRcv, OutChan!Rcv + <2>5. CASE UNCHANGED <> + BY <2>5 + <2>. QED BY <2>1, <2>2, <2>3, <2>4, <2>5 DEF Next +<1>. QED BY <1>1, <1>2, PTL DEF Spec + +============================================================================ diff --git a/specifications/SpecifyingSystems/HourClock/HourClock_proof.tla b/specifications/SpecifyingSystems/HourClock/HourClock_proof.tla new file mode 100644 index 00000000..6d396e14 --- /dev/null +++ b/specifications/SpecifyingSystems/HourClock/HourClock_proof.tla @@ -0,0 +1,14 @@ +-------------------------- MODULE HourClock_proof -------------------------- +(***************************************************************************) +(* TLAPS proof of the theorem stated in HourClock.tla. *) +(***************************************************************************) +EXTENDS HourClock, TLAPS + +THEOREM HCini_Invariant == HC => []HCini +<1>1. HCini => HCini + OBVIOUS +<1>2. HCini /\ [HCnxt]_hr => HCini' + BY DEF HCini, HCnxt +<1>. QED BY <1>1, <1>2, PTL DEF HC + +============================================================================ diff --git a/specifications/SpecifyingSystems/Liveness/HourClock_proof.tla b/specifications/SpecifyingSystems/Liveness/HourClock_proof.tla new file mode 100644 index 00000000..6d396e14 --- /dev/null +++ b/specifications/SpecifyingSystems/Liveness/HourClock_proof.tla @@ -0,0 +1,14 @@ +-------------------------- MODULE HourClock_proof -------------------------- +(***************************************************************************) +(* TLAPS proof of the theorem stated in HourClock.tla. *) +(***************************************************************************) +EXTENDS HourClock, TLAPS + +THEOREM HCini_Invariant == HC => []HCini +<1>1. HCini => HCini + OBVIOUS +<1>2. HCini /\ [HCnxt]_hr => HCini' + BY DEF HCini, HCnxt +<1>. QED BY <1>1, <1>2, PTL DEF HC + +============================================================================ diff --git a/specifications/SpecifyingSystems/Liveness/InternalMemory_proof.tla b/specifications/SpecifyingSystems/Liveness/InternalMemory_proof.tla new file mode 100644 index 00000000..5ae8971f --- /dev/null +++ b/specifications/SpecifyingSystems/Liveness/InternalMemory_proof.tla @@ -0,0 +1,76 @@ +------------------------- MODULE InternalMemory_proof ---------------------- +(***************************************************************************) +(* TLAPS proof of *) +(* *) +(* THEOREM ISpec => []TypeInvariant *) +(* *) +(* stated in InternalMemory.tla. *) +(* *) +(* TypeInvariant alone is not inductive: in Do(p), the next-state *) +(* expression accesses buf[p].adr / buf[p].op, which only makes sense *) +(* when buf[p] is in MReq. We strengthen TypeInvariant with *) +(* BufConsistent, which records the buf typing for each value of ctl[p]. *) +(***************************************************************************) +EXTENDS InternalMemory, TLAPS + +BufConsistent == + /\ \A p \in Proc : (ctl[p] = "rdy") => (buf[p] \in Val \cup {NoVal}) + /\ \A p \in Proc : (ctl[p] = "busy") => (buf[p] \in MReq) + /\ \A p \in Proc : (ctl[p] = "done") => (buf[p] \in Val \cup {NoVal}) + +Inv == TypeInvariant /\ BufConsistent + +LEMMA InvInductive == ISpec => []Inv +<1>1. IInit => Inv + BY DEF IInit, Inv, TypeInvariant, BufConsistent +<1>2. Inv /\ [INext]_<> => Inv' + <2> SUFFICES ASSUME Inv, + [INext]_<> + PROVE Inv' + OBVIOUS + <2>. USE DEF Inv, TypeInvariant, BufConsistent + <2>1. ASSUME NEW p \in Proc, Req(p) + PROVE Inv' + \* After Req(p): ctl[p]' = "busy", buf[p]' \in MReq. For q # p, + \* ctl/buf unchanged. mem unchanged. + BY <2>1 DEF Req + <2>2. ASSUME NEW p \in Proc, Do(p) + PROVE Inv' + \* Pre: ctl[p] = "busy", so buf[p] \in MReq, hence buf[p].adr \in Adr, + \* and buf[p].op \in {"Rd","Wr"}. + <3>1. buf[p] \in MReq + BY <2>2 DEF Do + <3>2. buf[p].adr \in Adr /\ buf[p].op \in {"Rd","Wr"} + BY <3>1 DEF MReq + <3>3. CASE buf[p].op = "Wr" + \* mem' \in [Adr->Val] because we update at adr \in Adr to val \in Val. + \* buf[p]' = NoVal \in Val \cup {NoVal}, ctl[p]' = "done". + <4>1. buf[p].val \in Val + BY <3>1, <3>3 DEF MReq + <4>2. mem' = [mem EXCEPT ![buf[p].adr] = buf[p].val] + BY <2>2, <3>3 DEF Do + <4>3. mem' \in [Adr -> Val] + BY <3>2, <4>1, <4>2 + <4>. QED BY <2>2, <3>3, <4>3 DEF Do + <3>4. CASE buf[p].op = "Rd" + \* mem' = mem. buf[p]' = mem[buf[p].adr] \in Val. ctl[p]' = "done". + <4>1. mem' = mem + BY <2>2, <3>4 DEF Do + <4>2. mem[buf[p].adr] \in Val + BY <3>2 + <4>. QED BY <2>2, <3>4, <4>1, <4>2 DEF Do + <3>. QED BY <3>2, <3>3, <3>4 + <2>3. ASSUME NEW p \in Proc, Rsp(p) + PROVE Inv' + \* ctl[p]' = "rdy"; buf, mem unchanged. buf[p] was \in Val \cup {NoVal} + \* (since pre ctl[p] = "done"), so it remains so under "rdy". + BY <2>3 DEF Rsp + <2>4. CASE UNCHANGED <> + BY <2>4 + <2>. QED BY <2>1, <2>2, <2>3, <2>4 DEF INext +<1>. QED BY <1>1, <1>2, PTL DEF ISpec + +THEOREM TypeCorrect == ISpec => []TypeInvariant +BY InvInductive, PTL DEF Inv + +============================================================================ diff --git a/specifications/SpecifyingSystems/RealTime/HourClock_proof.tla b/specifications/SpecifyingSystems/RealTime/HourClock_proof.tla new file mode 100644 index 00000000..6d396e14 --- /dev/null +++ b/specifications/SpecifyingSystems/RealTime/HourClock_proof.tla @@ -0,0 +1,14 @@ +-------------------------- MODULE HourClock_proof -------------------------- +(***************************************************************************) +(* TLAPS proof of the theorem stated in HourClock.tla. *) +(***************************************************************************) +EXTENDS HourClock, TLAPS + +THEOREM HCini_Invariant == HC => []HCini +<1>1. HCini => HCini + OBVIOUS +<1>2. HCini /\ [HCnxt]_hr => HCini' + BY DEF HCini, HCnxt +<1>. QED BY <1>1, <1>2, PTL DEF HC + +============================================================================ diff --git a/specifications/SpecifyingSystems/RealTime/InternalMemory_proof.tla b/specifications/SpecifyingSystems/RealTime/InternalMemory_proof.tla new file mode 100644 index 00000000..5ae8971f --- /dev/null +++ b/specifications/SpecifyingSystems/RealTime/InternalMemory_proof.tla @@ -0,0 +1,76 @@ +------------------------- MODULE InternalMemory_proof ---------------------- +(***************************************************************************) +(* TLAPS proof of *) +(* *) +(* THEOREM ISpec => []TypeInvariant *) +(* *) +(* stated in InternalMemory.tla. *) +(* *) +(* TypeInvariant alone is not inductive: in Do(p), the next-state *) +(* expression accesses buf[p].adr / buf[p].op, which only makes sense *) +(* when buf[p] is in MReq. We strengthen TypeInvariant with *) +(* BufConsistent, which records the buf typing for each value of ctl[p]. *) +(***************************************************************************) +EXTENDS InternalMemory, TLAPS + +BufConsistent == + /\ \A p \in Proc : (ctl[p] = "rdy") => (buf[p] \in Val \cup {NoVal}) + /\ \A p \in Proc : (ctl[p] = "busy") => (buf[p] \in MReq) + /\ \A p \in Proc : (ctl[p] = "done") => (buf[p] \in Val \cup {NoVal}) + +Inv == TypeInvariant /\ BufConsistent + +LEMMA InvInductive == ISpec => []Inv +<1>1. IInit => Inv + BY DEF IInit, Inv, TypeInvariant, BufConsistent +<1>2. Inv /\ [INext]_<> => Inv' + <2> SUFFICES ASSUME Inv, + [INext]_<> + PROVE Inv' + OBVIOUS + <2>. USE DEF Inv, TypeInvariant, BufConsistent + <2>1. ASSUME NEW p \in Proc, Req(p) + PROVE Inv' + \* After Req(p): ctl[p]' = "busy", buf[p]' \in MReq. For q # p, + \* ctl/buf unchanged. mem unchanged. + BY <2>1 DEF Req + <2>2. ASSUME NEW p \in Proc, Do(p) + PROVE Inv' + \* Pre: ctl[p] = "busy", so buf[p] \in MReq, hence buf[p].adr \in Adr, + \* and buf[p].op \in {"Rd","Wr"}. + <3>1. buf[p] \in MReq + BY <2>2 DEF Do + <3>2. buf[p].adr \in Adr /\ buf[p].op \in {"Rd","Wr"} + BY <3>1 DEF MReq + <3>3. CASE buf[p].op = "Wr" + \* mem' \in [Adr->Val] because we update at adr \in Adr to val \in Val. + \* buf[p]' = NoVal \in Val \cup {NoVal}, ctl[p]' = "done". + <4>1. buf[p].val \in Val + BY <3>1, <3>3 DEF MReq + <4>2. mem' = [mem EXCEPT ![buf[p].adr] = buf[p].val] + BY <2>2, <3>3 DEF Do + <4>3. mem' \in [Adr -> Val] + BY <3>2, <4>1, <4>2 + <4>. QED BY <2>2, <3>3, <4>3 DEF Do + <3>4. CASE buf[p].op = "Rd" + \* mem' = mem. buf[p]' = mem[buf[p].adr] \in Val. ctl[p]' = "done". + <4>1. mem' = mem + BY <2>2, <3>4 DEF Do + <4>2. mem[buf[p].adr] \in Val + BY <3>2 + <4>. QED BY <2>2, <3>4, <4>1, <4>2 DEF Do + <3>. QED BY <3>2, <3>3, <3>4 + <2>3. ASSUME NEW p \in Proc, Rsp(p) + PROVE Inv' + \* ctl[p]' = "rdy"; buf, mem unchanged. buf[p] was \in Val \cup {NoVal} + \* (since pre ctl[p] = "done"), so it remains so under "rdy". + BY <2>3 DEF Rsp + <2>4. CASE UNCHANGED <> + BY <2>4 + <2>. QED BY <2>1, <2>2, <2>3, <2>4 DEF INext +<1>. QED BY <1>1, <1>2, PTL DEF ISpec + +THEOREM TypeCorrect == ISpec => []TypeInvariant +BY InvInductive, PTL DEF Inv + +============================================================================ diff --git a/specifications/SpecifyingSystems/TLC/AlternatingBit_proof.tla b/specifications/SpecifyingSystems/TLC/AlternatingBit_proof.tla new file mode 100644 index 00000000..48977b21 --- /dev/null +++ b/specifications/SpecifyingSystems/TLC/AlternatingBit_proof.tla @@ -0,0 +1,62 @@ +------------------------ MODULE AlternatingBit_proof ----------------------- +(***************************************************************************) +(* TLAPS proof of *) +(* THEOREM ABSpec => []ABTypeInv *) +(* stated in AlternatingBit.tla. *) +(***************************************************************************) +EXTENDS AlternatingBit, TLAPS + +LEMMA AppendType == + ASSUME NEW T, NEW s \in Seq(T), NEW e \in T + PROVE Append(s, e) \in Seq(T) + OBVIOUS + +LEMMA TailType == + ASSUME NEW T, NEW s \in Seq(T), s # << >> + PROVE Tail(s) \in Seq(T) + OBVIOUS + +LEMMA HeadType == + ASSUME NEW T, NEW s \in Seq(T), s # << >> + PROVE Head(s) \in T + OBVIOUS + +LEMMA LosePreservesType == + ASSUME NEW T, NEW q \in Seq(T), q # << >>, + NEW i \in 1..Len(q), + NEW q2, + q2 = [j \in 1..(Len(q)-1) |-> IF j < i THEN q[j] ELSE q[j+1]] + PROVE q2 \in Seq(T) + OBVIOUS + +THEOREM TypeCorrect == ABSpec => []ABTypeInv +<1>1. ABInit => ABTypeInv + BY DEF ABInit, ABTypeInv +<1>2. ABTypeInv /\ [ABNext]_abvars => ABTypeInv' + <2> SUFFICES ASSUME ABTypeInv, [ABNext]_abvars + PROVE ABTypeInv' + OBVIOUS + <2>. USE DEF ABTypeInv + <2>1. ASSUME NEW d \in Data, SndNewValue(d) + PROVE ABTypeInv' + \* msgQ' = Append(msgQ, <>); sBit' \in {0,1}, d \in Data, + \* so <> \in {0,1} \X Data; AppendType. + BY <2>1, AppendType DEF SndNewValue + <2>2. CASE ReSndMsg + BY <2>2, AppendType DEF ReSndMsg + <2>3. CASE RcvMsg + BY <2>3, TailType, HeadType DEF RcvMsg + <2>4. CASE SndAck + BY <2>4, AppendType DEF SndAck + <2>5. CASE RcvAck + BY <2>5, TailType, HeadType DEF RcvAck + <2>6. CASE LoseMsg + BY <2>6, LosePreservesType DEF LoseMsg, Lose + <2>7. CASE LoseAck + BY <2>7, LosePreservesType DEF LoseAck, Lose + <2>8. CASE UNCHANGED abvars + BY <2>8 DEF abvars + <2>. QED BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7, <2>8 DEF ABNext +<1>. QED BY <1>1, <1>2, PTL DEF ABSpec + +============================================================================ diff --git a/specifications/TwoPhase/TwoPhase_proof.tla b/specifications/TwoPhase/TwoPhase_proof.tla new file mode 100644 index 00000000..10c845c1 --- /dev/null +++ b/specifications/TwoPhase/TwoPhase_proof.tla @@ -0,0 +1,35 @@ +------------------------ MODULE TwoPhase_proof ----------------------- +(***************************************************************************) +(* TLAPS proof of *) +(* THEOREM Implementation == Spec => A!Spec *) +(* stated in TwoPhase.tla. *) +(***************************************************************************) +EXTENDS TwoPhase, TLAPS + +(***************************************************************************) +(* The following theorem is a standard proof that one specification *) +(* implements (the safety part of) another specification under a *) +(* refinement mapping. In fact, the temporal leaf proofs will be exactly *) +(* the same one-liners for every such proof. In realistic example, the *) +(* non-temporal leaf proofs will be replaced by fairly long structured *) +(* proofs--especially the two substeps numbered <2>2. *) +(***************************************************************************) +THEOREM Implementation +<1>1. Spec => []Inv + <2>1. Init => Inv + BY DEF Init, Inv + <2>2. Inv /\ [Next]_<> => Inv' + BY Z3 DEF Inv, Next, ProducerStep, ConsumerStep + <2>. QED + BY <2>1, <2>2, PTL DEF Spec +<1>2. QED + <2>1. Init => A!Init + BY Z3 DEF Init, A!Init, vBar + <2>2. Inv /\ [Next]_<> => [A!Next]_<> + BY Z3 DEF Inv, Next, ProducerStep, ConsumerStep, A!Next, vBar + <2>3. []Inv /\ [][Next]_<> => [][A!Next]_<> + BY <2>1, <2>2, PTL + <2>. QED + BY <2>1, <2>3, <1>1, PTL DEF Spec, A!Spec + +============================================================== diff --git a/specifications/allocator/AllocatorImplementation_proof.tla b/specifications/allocator/AllocatorImplementation_proof.tla new file mode 100644 index 00000000..dfd377b3 --- /dev/null +++ b/specifications/allocator/AllocatorImplementation_proof.tla @@ -0,0 +1,123 @@ +--------------------- MODULE AllocatorImplementation_proof ----------------- +(***************************************************************************) +(* TLAPS proofs of two safety theorems stated in *) +(* AllocatorImplementation.tla: *) +(* *) +(* Specification => []TypeInvariant *) +(* Specification => []ResourceMutex *) +(* *) +(* TypeInvariant uses the SchedulingAllocator's TypeInvariant via the *) +(* Sched! instance, plus the type of the additional client-side variables *) +(* (requests, holding, network). The proof essentially mirrors *) +(* SchedulingAllocator_proof.tla. *) +(* *) +(* ResourceMutex here is the *client-side* mutex *) +(* \A c1, c2: holding[c1] \cap holding[c2] # {} => c1 = c2. *) +(* The argument is: holding only grows from RAlloc(m) where m is an *) +(* in-transit "allocate" message; for that m to exist Sched!Allocate(c,S) *) +(* fired earlier, which by Sched's mutex means S is disjoint from *) +(* alloc[c'] for c' # c, and (by an interplay invariant) from holding[c'] *) +(* too. *) +(* *) +(* Here we prove TypeInvariant fully and ResourceMutex assuming the *) +(* (internal) Invariant -- which combines the Sched-level *) +(* AllocatorInvariant with the network/holding consistency invariant *) +(* "alloc[c] = holding[c] \cup AllocsInTransit(c) \cup ReturnsInTransit(c)".*) +(* We do not (yet) prove that combined Invariant inductive; that piece is *) +(* deferred to future work along with the Sched!AllocatorInvariant proof. *) +(***************************************************************************) +EXTENDS AllocatorImplementation, Integers, SequenceTheorems, TLAPS + +(***************************************************************************) +(* SchedulingAllocator-level helpers, copied for in-module access. *) +(***************************************************************************) +LEMMA SubSeqInRange == + ASSUME NEW T, NEW s \in Seq(T), NEW m \in Int, NEW n \in Int, + m >= 1, n <= Len(s) + PROVE SubSeq(s, m, n) \in Seq(T) +<1>1. \A i \in m..n : s[i] \in T + OBVIOUS +<1>. QED BY <1>1, SubSeqProperties + +LEMMA ConcatType == + ASSUME NEW T, NEW s1 \in Seq(T), NEW s2 \in Seq(T) + PROVE s1 \o s2 \in Seq(T) + OBVIOUS + +LEMMA DropType == + ASSUME NEW T, NEW s \in Seq(T), NEW i \in 1..Len(s) + PROVE Sched!Drop(s, i) \in Seq(T) +<1>1. SubSeq(s, 1, i-1) \in Seq(T) + BY SubSeqInRange +<1>2. SubSeq(s, i+1, Len(s)) \in Seq(T) + BY SubSeqInRange +<1>. QED BY <1>1, <1>2, ConcatType DEF Sched!Drop + +LEMMA PermSeqsType == + ASSUME NEW T, NEW S \in SUBSET T, NEW sq \in Sched!PermSeqs(S) + PROVE sq \in Seq(T) + OMITTED \* requires induction on the recursive PermSeqs definition + +(***************************************************************************) +(* Specification => []TypeInvariant *) +(***************************************************************************) + +THEOREM TypeCorrect == Specification => []TypeInvariant +<1>1. Init => TypeInvariant + BY DEF Init, TypeInvariant, Sched!Init, Sched!TypeInvariant +<1>2. TypeInvariant /\ [Next]_vars => TypeInvariant' + <2> SUFFICES ASSUME TypeInvariant, [Next]_vars + PROVE TypeInvariant' + OBVIOUS + <2>. USE DEF TypeInvariant, Sched!TypeInvariant, Messages + <2>1. ASSUME NEW c \in Clients, NEW S \in SUBSET Resources, Request(c, S) + PROVE TypeInvariant' + BY <2>1 DEF Request + <2>2. ASSUME NEW c \in Clients, NEW S \in SUBSET Resources, Allocate(c, S) + PROVE TypeInvariant' + \* Allocate calls Sched!Allocate which updates unsat, alloc, sched. + \* network grows. requests, holding unchanged. + <3>1. PICK i \in DOMAIN sched : + /\ sched[i] = c + /\ \A j \in 1..i-1 : unsat[sched[j]] \cap S = {} + /\ sched' = IF S = unsat[c] THEN Sched!Drop(sched, i) ELSE sched + BY <2>2 DEF Allocate, Sched!Allocate + <3>2. unsat' \in [Clients -> SUBSET Resources] + BY <2>2 DEF Allocate, Sched!Allocate + <3>3. alloc' \in [Clients -> SUBSET Resources] + BY <2>2 DEF Allocate, Sched!Allocate + <3>4. i \in 1..Len(sched) + BY <3>1 + <3>5. sched' \in Seq(Clients) + BY <3>1, <3>4, DropType + <3>6. network' \in SUBSET Messages + BY <2>2 DEF Allocate, Messages + <3>. QED BY <2>2, <3>2, <3>3, <3>5, <3>6 DEF Allocate + <2>3. ASSUME NEW c \in Clients, NEW S \in SUBSET Resources, Return(c, S) + PROVE TypeInvariant' + BY <2>3 DEF Return, Messages + <2>4. ASSUME NEW m \in network, RReq(m) + PROVE TypeInvariant' + BY <2>4 DEF RReq, Messages + <2>5. ASSUME NEW m \in network, RAlloc(m) + PROVE TypeInvariant' + BY <2>5 DEF RAlloc, Messages + <2>6. ASSUME NEW m \in network, RRet(m) + PROVE TypeInvariant' + BY <2>6 DEF RRet, Messages + <2>7. CASE Schedule + <3>1. PICK sq \in Sched!PermSeqs(Sched!toSchedule) : sched' = sched \o sq + BY <2>7 DEF Schedule, Sched!Schedule + <3>2. Sched!toSchedule \subseteq Clients + BY DEF Sched!toSchedule + <3>3. sq \in Seq(Clients) + BY <3>1, <3>2, PermSeqsType + <3>4. sched' \in Seq(Clients) + BY <3>1, <3>3, ConcatType + <3>. QED BY <2>7, <3>4 DEF Schedule, Sched!Schedule + <2>8. CASE UNCHANGED vars + BY <2>8 DEF vars + <2>. QED BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7, <2>8 DEF Next +<1>. QED BY <1>1, <1>2, PTL DEF Specification + +============================================================================ diff --git a/specifications/allocator/SchedulingAllocator_proof.tla b/specifications/allocator/SchedulingAllocator_proof.tla new file mode 100644 index 00000000..117d06ad --- /dev/null +++ b/specifications/allocator/SchedulingAllocator_proof.tla @@ -0,0 +1,193 @@ +--------------------- MODULE SchedulingAllocator_proof --------------------- +(***************************************************************************) +(* TLAPS proofs of the safety theorems stated in SchedulingAllocator.tla: *) +(* *) +(* Allocator => []TypeInvariant *) +(* Allocator => []ResourceMutex *) +(* *) +(* TypeInvariant is directly inductive (the only subtlety is that *) +(* Drop(sched, i) and sched \circ sq stay in Seq(Clients)). ResourceMutex *) +(* uses the same argument as in SimpleAllocator: an Allocate(c, S) action *) +(* takes S from `available`, so S is disjoint from every alloc[c']. *) +(* *) +(* AllocatorInvariant is left as future work; its preservation across the *) +(* Schedule action requires careful reasoning about Range(sched \circ sq) *) +(* and the way toSchedule changes. *) +(***************************************************************************) +EXTENDS SchedulingAllocator, Integers, SequenceTheorems, TLAPS + +(***************************************************************************) +(* Allocator => []TypeInvariant *) +(***************************************************************************) + +LEMMA SubSeqInRange == + ASSUME NEW T, NEW s \in Seq(T), NEW m \in Int, NEW n \in Int, + m >= 1, n <= Len(s) + PROVE SubSeq(s, m, n) \in Seq(T) +<1>1. \A i \in m..n : s[i] \in T + OBVIOUS +<1>. QED BY <1>1, SubSeqProperties + +LEMMA ConcatType == + ASSUME NEW T, NEW s1 \in Seq(T), NEW s2 \in Seq(T) + PROVE s1 \o s2 \in Seq(T) + OBVIOUS + +LEMMA DropType == + ASSUME NEW T, NEW s \in Seq(T), NEW i \in 1..Len(s) + PROVE Drop(s, i) \in Seq(T) +<1>1. SubSeq(s, 1, i-1) \in Seq(T) + BY SubSeqInRange +<1>2. SubSeq(s, i+1, Len(s)) \in Seq(T) + BY SubSeqInRange +<1>. QED BY <1>1, <1>2, ConcatType DEF Drop + +(***************************************************************************) +(* Permutations of a finite set, packaged as sequences, are sequences over *) +(* (a superset of) the set. The recursion in PermSeqs builds each output *) +(* by Append-ing elements of S. *) +(***************************************************************************) +LEMMA PermSeqsType == + ASSUME NEW T, NEW S \in SUBSET T, NEW sq \in PermSeqs(S) + PROVE sq \in Seq(T) + OMITTED \* requires induction on the recursive PermSeqs function + +THEOREM TypeCorrect == Allocator => []TypeInvariant +<1>1. Init => TypeInvariant + BY DEF Init, TypeInvariant +<1>2. TypeInvariant /\ [Next]_vars => TypeInvariant' + <2> SUFFICES ASSUME TypeInvariant, [Next]_vars + PROVE TypeInvariant' + OBVIOUS + <2>. USE DEF TypeInvariant + <2>1. ASSUME NEW c \in Clients, NEW S \in SUBSET Resources, Request(c, S) + PROVE TypeInvariant' + BY <2>1 DEF Request + <2>2. ASSUME NEW c \in Clients, NEW S \in SUBSET Resources, Allocate(c, S) + PROVE TypeInvariant' + \* alloc' EXCEPT, unsat' EXCEPT. sched' = Drop(sched, i) or sched. + <3>1. PICK i \in DOMAIN sched : + /\ sched[i] = c + /\ \A j \in 1..i-1 : unsat[sched[j]] \cap S = {} + /\ sched' = IF S = unsat[c] THEN Drop(sched, i) ELSE sched + BY <2>2 DEF Allocate + <3>2. unsat' \in [Clients -> SUBSET Resources] + BY <2>2 DEF Allocate + <3>3. alloc' \in [Clients -> SUBSET Resources] + BY <2>2 DEF Allocate + <3>4. i \in 1..Len(sched) + BY <3>1 + <3>5. sched' \in Seq(Clients) + BY <3>1, <3>4, DropType + <3>. QED BY <3>2, <3>3, <3>5 + <2>3. ASSUME NEW c \in Clients, NEW S \in SUBSET Resources, Return(c, S) + PROVE TypeInvariant' + BY <2>3 DEF Return + <2>4. CASE Schedule + <3>1. PICK sq \in PermSeqs(toSchedule) : sched' = sched \o sq + BY <2>4 DEF Schedule + <3>2. toSchedule \subseteq Clients + BY DEF toSchedule + <3>3. sq \in Seq(Clients) + BY <3>1, <3>2, PermSeqsType + <3>4. sched' \in Seq(Clients) + BY <3>1, <3>3, ConcatType + <3>. QED BY <2>4, <3>4 DEF Schedule + <2>5. CASE UNCHANGED vars + BY <2>5 DEF vars + <2>. QED BY <2>1, <2>2, <2>3, <2>4, <2>5 DEF Next +<1>. QED BY <1>1, <1>2, PTL DEF Allocator + +(***************************************************************************) +(* Allocator => []ResourceMutex *) +(***************************************************************************) + +Inv == TypeInvariant /\ ResourceMutex + +THEOREM Mutex == Allocator => []ResourceMutex +<1>1. Init => Inv + BY DEF Init, Inv, TypeInvariant, ResourceMutex +<1>2. Inv /\ [Next]_vars => Inv' + <2> SUFFICES ASSUME Inv, [Next]_vars + PROVE Inv' + OBVIOUS + <2>. USE DEF Inv, TypeInvariant, ResourceMutex + <2>1. ASSUME NEW c \in Clients, NEW S \in SUBSET Resources, Request(c, S) + PROVE Inv' + BY <2>1 DEF Request + <2>2. ASSUME NEW c \in Clients, NEW S \in SUBSET Resources, Allocate(c, S) + PROVE Inv' + \* Same argument as SimpleAllocator: S \subseteq available => + \* S \cap alloc[c'] = {} for all c'. + <3>0. TypeInvariant' + \* re-derive via the TypeCorrect step proof (inlined). + <4>1. PICK i \in DOMAIN sched : + /\ sched[i] = c + /\ \A j \in 1..i-1 : unsat[sched[j]] \cap S = {} + /\ sched' = IF S = unsat[c] THEN Drop(sched, i) ELSE sched + BY <2>2 DEF Allocate + <4>2. i \in 1..Len(sched) + BY <4>1 + <4>3. sched' \in Seq(Clients) + BY <4>1, <4>2, DropType + <4>. QED BY <2>2, <4>3 DEF Allocate + <3>2. alloc' = [alloc EXCEPT ![c] = @ \cup S] + BY <2>2 DEF Allocate + <3>3. \A cc \in Clients : alloc'[cc] = IF cc = c THEN alloc[cc] \cup S + ELSE alloc[cc] + BY <3>2 + <3>4. S \subseteq available + BY <2>2 DEF Allocate + <3>5. \A cc \in Clients : S \cap alloc[cc] = {} + BY <3>4 DEF available + <3>9. ResourceMutex' + <4>1. SUFFICES ASSUME NEW c1 \in Clients, NEW c2 \in Clients, c1 # c2 + PROVE alloc'[c1] \cap alloc'[c2] = {} + BY DEF ResourceMutex + <4>6. CASE c1 = c + <5>1. alloc'[c1] = alloc[c] \cup S + BY <3>3, <4>6 + <5>2. alloc'[c2] = alloc[c2] + BY <3>3, <4>6, <4>1 + <5>3. alloc[c] \cap alloc[c2] = {} + BY <4>6, <4>1 + <5>4. S \cap alloc[c2] = {} + BY <3>5 + <5>. QED BY <5>1, <5>2, <5>3, <5>4 + <4>7. CASE c2 = c + <5>1. alloc'[c2] = alloc[c] \cup S + BY <3>3, <4>7 + <5>2. alloc'[c1] = alloc[c1] + BY <3>3, <4>7, <4>1 + <5>3. alloc[c1] \cap alloc[c] = {} + BY <4>7, <4>1 + <5>4. alloc[c1] \cap S = {} + BY <3>5 + <5>. QED BY <5>1, <5>2, <5>3, <5>4 + <4>8. CASE c1 # c /\ c2 # c + <5>1. alloc'[c1] = alloc[c1] /\ alloc'[c2] = alloc[c2] + BY <3>3, <4>8 + <5>. QED BY <5>1, <4>1 + <4>. QED BY <4>6, <4>7, <4>8 + <3>. QED BY <3>0, <3>9 DEF Inv + <2>3. ASSUME NEW c \in Clients, NEW S \in SUBSET Resources, Return(c, S) + PROVE Inv' + \* (alloc[c] \ S) \cap alloc[c'] \subseteq alloc[c] \cap alloc[c'] = {}. + BY <2>3 DEF Return + <2>4. CASE Schedule + \* alloc unchanged. + <3>1. PICK sq \in PermSeqs(toSchedule) : sched' = sched \o sq + BY <2>4 DEF Schedule + <3>2. toSchedule \subseteq Clients + BY DEF toSchedule + <3>3. sq \in Seq(Clients) + BY <3>1, <3>2, PermSeqsType + <3>4. sched' \in Seq(Clients) + BY <3>1, <3>3, ConcatType + <3>. QED BY <2>4, <3>4 DEF Schedule + <2>5. CASE UNCHANGED vars + BY <2>5 DEF vars + <2>. QED BY <2>1, <2>2, <2>3, <2>4, <2>5 DEF Next +<1>. QED BY <1>1, <1>2, PTL DEF Allocator, Inv + +============================================================================ diff --git a/specifications/allocator/SimpleAllocator_proof.tla b/specifications/allocator/SimpleAllocator_proof.tla new file mode 100644 index 00000000..43850779 --- /dev/null +++ b/specifications/allocator/SimpleAllocator_proof.tla @@ -0,0 +1,122 @@ +----------------------- MODULE SimpleAllocator_proof ----------------------- +(***************************************************************************) +(* TLAPS proofs of two safety properties of the SimpleAllocator spec: *) +(* *) +(* SimpleAllocator => []TypeInvariant *) +(* SimpleAllocator => []ResourceMutex *) +(* *) +(* TypeInvariant is directly inductive. ResourceMutex needs TypeInvariant *) +(* together with the simple observation that an Allocate(c, S) action *) +(* takes S from the `available` resources, so S is disjoint from every *) +(* alloc[c'] for c' # c. *) +(***************************************************************************) +EXTENDS SimpleAllocator, TLAPS + +(***************************************************************************) +(* SimpleAllocator => []TypeInvariant *) +(***************************************************************************) + +THEOREM TypeCorrect == SimpleAllocator => []TypeInvariant +<1>1. Init => TypeInvariant + BY DEF Init, TypeInvariant +<1>2. TypeInvariant /\ [Next]_vars => TypeInvariant' + <2> SUFFICES ASSUME TypeInvariant, [Next]_vars + PROVE TypeInvariant' + OBVIOUS + <2>. USE DEF TypeInvariant + <2>1. ASSUME NEW c \in Clients, NEW S \in SUBSET Resources, Request(c, S) + PROVE TypeInvariant' + BY <2>1 DEF Request + <2>2. ASSUME NEW c \in Clients, NEW S \in SUBSET Resources, Allocate(c, S) + PROVE TypeInvariant' + BY <2>2 DEF Allocate + <2>3. ASSUME NEW c \in Clients, NEW S \in SUBSET Resources, Return(c, S) + PROVE TypeInvariant' + BY <2>3 DEF Return + <2>4. CASE UNCHANGED vars + BY <2>4 DEF vars + <2>. QED BY <2>1, <2>2, <2>3, <2>4 DEF Next +<1>. QED BY <1>1, <1>2, PTL DEF SimpleAllocator + +(***************************************************************************) +(* SimpleAllocator => []ResourceMutex *) +(***************************************************************************) + +(***************************************************************************) +(* The combined inductive invariant. We need TypeInvariant in scope to *) +(* type-check alloc[c]; ResourceMutex on its own is preserved given *) +(* TypeInvariant. *) +(***************************************************************************) +Inv == TypeInvariant /\ ResourceMutex + +THEOREM Mutex == SimpleAllocator => []ResourceMutex +<1>1. Init => Inv + BY DEF Init, Inv, TypeInvariant, ResourceMutex +<1>2. Inv /\ [Next]_vars => Inv' + <2> SUFFICES ASSUME Inv, [Next]_vars + PROVE Inv' + OBVIOUS + <2>. USE DEF Inv, TypeInvariant, ResourceMutex + <2>1. ASSUME NEW c \in Clients, NEW S \in SUBSET Resources, Request(c, S) + PROVE Inv' + \* alloc unchanged. + BY <2>1 DEF Request + <2>2. ASSUME NEW c \in Clients, NEW S \in SUBSET Resources, Allocate(c, S) + PROVE Inv' + \* alloc'[c] = alloc[c] \cup S; for c' # c, alloc'[c'] = alloc[c']. + \* S \subseteq available means S \cap (UNION {alloc[c''] : c'' \in Clients}) = {}, + \* so in particular S \cap alloc[c'] = {} for any c'. Combined with + \* the IH alloc[c] \cap alloc[c'] = {}, the new alloc'[c] is still + \* disjoint from alloc'[c']. + <3>0. TypeInvariant' + BY <2>2 DEF Allocate + <3>2. alloc' = [alloc EXCEPT ![c] = @ \cup S] + BY <2>2 DEF Allocate + <3>3. \A cc \in Clients : alloc'[cc] = IF cc = c THEN alloc[cc] \cup S + ELSE alloc[cc] + BY <3>2 + <3>4. S \subseteq available + BY <2>2 DEF Allocate + <3>5. \A cc \in Clients : S \cap alloc[cc] = {} + BY <3>4 DEF available + <3>9. ResourceMutex' + <4>1. SUFFICES ASSUME NEW c1 \in Clients, NEW c2 \in Clients, c1 # c2 + PROVE alloc'[c1] \cap alloc'[c2] = {} + BY DEF ResourceMutex + <4>6. CASE c1 = c + <5>1. alloc'[c1] = alloc[c] \cup S + BY <3>3, <4>6 + <5>2. alloc'[c2] = alloc[c2] + BY <3>3, <4>6, <4>1 + <5>3. alloc[c] \cap alloc[c2] = {} + BY <4>6, <4>1 + <5>4. S \cap alloc[c2] = {} + BY <3>5 + <5>. QED BY <5>1, <5>2, <5>3, <5>4 + <4>7. CASE c2 = c + <5>1. alloc'[c2] = alloc[c] \cup S + BY <3>3, <4>7 + <5>2. alloc'[c1] = alloc[c1] + BY <3>3, <4>7, <4>1 + <5>3. alloc[c1] \cap alloc[c] = {} + BY <4>7, <4>1 + <5>4. alloc[c1] \cap S = {} + BY <3>5 + <5>. QED BY <5>1, <5>2, <5>3, <5>4 + <4>8. CASE c1 # c /\ c2 # c + <5>1. alloc'[c1] = alloc[c1] /\ alloc'[c2] = alloc[c2] + BY <3>3, <4>8 + <5>. QED BY <5>1, <4>1 + <4>. QED BY <4>6, <4>7, <4>8 + <3>. QED BY <3>0, <3>9 DEF Inv + <2>3. ASSUME NEW c \in Clients, NEW S \in SUBSET Resources, Return(c, S) + PROVE Inv' + \* alloc'[c] = alloc[c] \ S; for c' # c, alloc'[c'] = alloc[c']. + \* (alloc[c] \ S) \cap alloc[c'] \subseteq alloc[c] \cap alloc[c'] = {}. + BY <2>3 DEF Return + <2>4. CASE UNCHANGED vars + BY <2>4 DEF vars + <2>. QED BY <2>1, <2>2, <2>3, <2>4 DEF Next +<1>. QED BY <1>1, <1>2, PTL DEF SimpleAllocator, Inv + +============================================================================ diff --git a/specifications/byihive/VoucherLifeCycle_proof.tla b/specifications/byihive/VoucherLifeCycle_proof.tla new file mode 100644 index 00000000..6cb42cb0 --- /dev/null +++ b/specifications/byihive/VoucherLifeCycle_proof.tla @@ -0,0 +1,19 @@ +------------------------ MODULE VoucherLifeCycle_proof ---------------------- +(***************************************************************************) +(* TLAPS proof of *) +(* THEOREM VSpec => [](VTypeOK /\ VConsistent) *) +(* stated in VoucherLifeCycle.tla. TypeOK and VConsistent together form *) +(* an inductive invariant. *) +(***************************************************************************) +EXTENDS VoucherLifeCycle, TLAPS + +Inv == VTypeOK /\ VConsistent + +THEOREM Spec_TypeOK_Consistent == VSpec => []Inv +<1>1. VInit => Inv + BY DEF VInit, Inv, VTypeOK, VConsistent +<1>2. Inv /\ [VNext]_<> => Inv' + BY DEF Inv, VTypeOK, VConsistent, VNext, Issue, Transfer, Redeem, Cancel +<1>. QED BY <1>1, <1>2, PTL DEF VSpec, Inv + +============================================================================ diff --git a/specifications/ewd687a/EWD687a_proof.tla b/specifications/ewd687a/EWD687a_proof.tla new file mode 100644 index 00000000..9870bbb7 --- /dev/null +++ b/specifications/ewd687a/EWD687a_proof.tla @@ -0,0 +1,813 @@ +--------------------------- MODULE EWD687a_proof --------------------------- +(***************************************************************************) +(* TLAPS proofs of the theorems stated in EWD687a.tla. *) +(***************************************************************************) +EXTENDS EWD687a, NaturalsInduction, FiniteSetTheorems, TLAPS + +----------------------------------------------------------------------------- +(***************************************************************************) +(* Theorem 1: Spec => CountersConsistent *) +(* *) +(* The four counters per edge are always consistent: the number of *) +(* messages ever sent on an edge equals the messages received and *) +(* acknowledged plus the messages received and not yet acked plus the *) +(* acks in flight plus the messages still in flight. *) +(* *) +(* TypeOK on its own is not inductive: in RcvAck and SendAck a counter is *) +(* decremented, and we can only show that the result stays in Nat by also *) +(* knowing the counters are consistent. We therefore prove TypeOK and the *) +(* state predicate Counters together as a single inductive invariant. *) +(***************************************************************************) +Counters == \A e \in Edges : sentUnacked[e] = rcvdUnacked[e] + acks[e] + msgs[e] + +Inv1 == TypeOK /\ Counters + +LEMMA Inv1Init == Init => Inv1 +BY DEF Init, Inv1, TypeOK, Counters, NotAnEdge + +LEMMA Inv1Step == Inv1 /\ [Next]_vars => Inv1' + <2> SUFFICES ASSUME Inv1, [Next]_vars + PROVE Inv1' + OBVIOUS + <2>. USE DEF Inv1, TypeOK, Counters + <2>1. ASSUME NEW p \in Procs, SendMsg(p) + PROVE Inv1' + BY <2>1 DEF SendMsg, OutEdges + <2>2. ASSUME NEW p \in Procs, RcvAck(p) + PROVE Inv1' + BY <2>2 DEF RcvAck, OutEdges + <2>3. ASSUME NEW p \in Procs, SendAck(p) + PROVE Inv1' + BY <2>3 DEF SendAck, InEdges, neutral + <2>4. ASSUME NEW p \in Procs, RcvMsg(p) + PROVE Inv1' + <3>1. PICK e \in InEdges(p) : + /\ msgs[e] > 0 + /\ msgs' = [msgs EXCEPT ![e] = @ - 1] + /\ rcvdUnacked' = [rcvdUnacked EXCEPT ![e] = @ + 1] + /\ active' = [active EXCEPT ![p] = TRUE] + /\ upEdge' = IF neutral(p) THEN [upEdge EXCEPT ![p] = e] + ELSE upEdge + /\ UNCHANGED <> + BY <2>4 DEF RcvMsg + <3>2. p # Leader + BY <3>1, EdgeFacts DEF InEdges + <3>3. e[2] = p /\ e \in Edges + BY <3>1 DEF InEdges + <3>. QED + BY <3>1, <3>2, <3>3 DEF InEdges, neutral, NotAnEdge + <2>5. ASSUME NEW p \in Procs, Idle(p) + PROVE Inv1' + BY <2>5 DEF Idle + <2>6. CASE UNCHANGED vars + BY <2>6 DEF vars + <2>. QED BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6 DEF Next + +LEMMA Inv1Inductive == Spec => []Inv1 +BY Inv1Init, Inv1Step, PTL DEF Spec + +THEOREM TypeCorrect == Spec => []TypeOK +BY Inv1Inductive, PTL DEF Inv1 + +THEOREM Thm_CountersConsistent == Spec => CountersConsistent +BY Inv1Inductive, PTL DEF CountersConsistent, Inv1, Counters + +----------------------------------------------------------------------------- +(***************************************************************************) +(* Theorem 3: Spec => []DT1Inv *) +(* *) +(* Main safety property: when the leader is neutral, the entire *) +(* computation has terminated, i.e., every non-leader process is also *) +(* neutral. *) +(* *) +(* DT1Inv is not directly inductive. We strengthen it by adding two *) +(* invariants describing the structure of the overlay tree: *) +(* *) +(* - Non-neutral non-leader processes always have an upEdge (so they *) +(* are part of the overlay tree). *) +(* - If p is in the tree, then upEdge[p] is a well-formed incoming edge *) +(* of p, the edge has at least one unacknowledged message *) +(* (rcvdUnacked >= 1), and (the key fact for DT1Inv) the parent of p *) +(* in the overlay tree is itself non-neutral. *) +(* *) +(* From the second invariant, the chain of upEdges from any non-neutral *) +(* non-leader p consists of non-neutral processes, so the leader cannot *) +(* be neutral whenever any other process is non-neutral. Formalising the *) +(* finite-chain argument needs Procs to be finite and a small amount of *) +(* well-founded reasoning, factored out as a separate lemma. *) +(***************************************************************************) +ASSUME ProcsFinite == IsFiniteSet(Procs) + +InTree(p) == upEdge[p] # NotAnEdge + +Inv2 == /\ \A p \in Procs \ {Leader} : ~neutral(p) => InTree(p) + /\ \A p \in Procs \ {Leader} : + InTree(p) => + /\ upEdge[p] \in Edges + /\ upEdge[p][2] = p + /\ upEdge[p][1] \in Procs \ {p} + /\ rcvdUnacked[upEdge[p]] >= 1 + +(***************************************************************************) +(* The chain step. *) +(* *) +(* Assume Inv2 and neutral(Leader). Suppose, for contradiction, that *) +(* S == {p \in Procs \ {Leader} : ~neutral(p)} is non-empty. *) +(* *) +(* - Conjunct 3 of Inv2 gives InTree(p) for every p in S. *) +(* - Conjunct 4 of Inv2 + Counters give sentUnacked[upEdge[p]] >= 1, *) +(* so the parent upEdge[p][1] is non-neutral. *) +(* - Since neutral(Leader), the parent is not Leader, hence the parent *) +(* is itself in S. *) +(* *) +(* So upEdge[_][1] defines a function f : S -> S with no fixed points. *) +(* In any non-empty set such an f might still admit a cycle, so we need an *) +(* auxiliary invariant ruling out cycles in the upEdge graph. We use the *) +(* following formulation: there is no non-empty set of in-tree non-leader *) +(* processes that is closed under taking the parent. (Equivalently: every *) +(* in-tree process can reach the leader by following upEdge.) *) +(* *) +(* NoCycle is established inductively (NoCycleInductive below). All *) +(* actions other than RcvMsg either leave upEdge unchanged or, in the *) +(* case of SendAck removing p from the tree, leave p with no children *) +(* (its OutEdges are quiescent), so any putative new closed set would *) +(* already have been a closed set in the previous state. RcvMsg may *) +(* attach a new process p to the tree with parent e[1]; if a closed set *) +(* S' arose in the new state with p \in S', then by Counters and Inv2 *) +(* conjunct 4 no other in-tree process points to p (since p was neutral, *) +(* every OutEdge of p has sentUnacked = 0), so removing p from S' yields *) +(* a smaller closed set in the previous state - contradicting the *) +(* induction hypothesis. *) +(***************************************************************************) +NoCycle == \A S \in SUBSET (Procs \ {Leader}) : + ~ (/\ S # {} + /\ \A q \in S : InTree(q) /\ upEdge[q][1] \in S) + +LEMMA Inv2Inductive == Spec => []Inv2 +<1>1. Init => Inv2 + <2>. SUFFICES ASSUME Init PROVE Inv2 + OBVIOUS + <2>2. \A p \in Procs \ {Leader} : ~neutral(p) => InTree(p) + BY DEF Init, neutral, InEdges, OutEdges + <2>3. \A p \in Procs \ {Leader} : ~ InTree(p) + BY DEF Init, InTree, NotAnEdge + <2>. QED BY <2>2, <2>3 DEF Inv2 +<1>2. Inv1 /\ Inv1' /\ Inv2 /\ [Next]_vars => Inv2' + <2> SUFFICES ASSUME Inv1, Inv1', Inv2, [Next]_vars + PROVE Inv2' + OBVIOUS + <2>. USE DEF Inv1, Inv2, TypeOK, Counters, InTree, NotAnEdge + <2>1. ASSUME NEW p \in Procs, SendMsg(p) + PROVE Inv2' + \* SendMsg only changes sentUnacked and msgs on one out-edge of p. + \* It does not change active, rcvdUnacked, or upEdge. + BY <2>1, EdgeFacts DEF SendMsg, OutEdges, InEdges, neutral + <2>5. ASSUME NEW p \in Procs, Idle(p) + PROVE Inv2' + \* Idle only changes active[p] to FALSE. Counters and upEdge are + \* unchanged. Neutral status of any p' might switch from non-neutral + \* to neutral, but the conjuncts of Inv2 are upper bounds, so they + \* are preserved. + BY <2>5, EdgeFacts DEF Idle, OutEdges, InEdges, neutral + <2>6. CASE UNCHANGED vars + BY <2>6 DEF vars, neutral, InEdges, OutEdges + <2>2. ASSUME NEW p \in Procs, RcvAck(p) + PROVE Inv2' + <3>1. PICK e \in OutEdges(p) : + /\ acks[e] > 0 + /\ acks' = [acks EXCEPT ![e] = @ - 1] + /\ sentUnacked' = [sentUnacked EXCEPT ![e] = @ - 1] + /\ UNCHANGED <> + BY <2>2 DEF RcvAck + <3>2. e \in Edges /\ e[1] = p /\ e[1] # e[2] /\ e[2] \in Procs \ {p} + BY <3>1, EdgeFacts DEF OutEdges + \* Only sentUnacked and acks for e change. active, rcvdUnacked, msgs, + \* and upEdge are unchanged. The neutrality of any q with q # p is + \* unaffected (sentUnacked, acks change only on edges in OutEdges(p)). + <3>3. \A q \in Procs : q # p => (neutral(q) <=> neutral(q)') + BY <3>1, <3>2 DEF neutral, OutEdges, InEdges + \* For p, the new sentUnacked[e] is one less; if that makes p neutral, + \* the conjunct "non-neutral implies InTree" still holds (vacuously + \* for p) since others' status is preserved. + <3>4. \A q \in Procs \ {Leader} : ~ neutral(q)' => InTree(q)' + <4>1. SUFFICES ASSUME NEW q \in Procs \ {Leader}, ~ neutral(q)' + PROVE InTree(q)' + OBVIOUS + <4>2. CASE q = p + \* upEdge unchanged, so InTree(p)' = InTree(p). Need ~neutral(p). + \* If neutral(p) before, then sentUnacked[e] = 0 (since e \in + \* OutEdges(p)). By Counters, acks[e] = 0, contradicting <3>1. + <5>1. ~ neutral(p) + <6>1. SUFFICES ASSUME neutral(p) PROVE FALSE + OBVIOUS + <6>2. sentUnacked[e] = 0 + BY <3>2, <6>1 DEF neutral + <6>3. acks[e] = 0 + BY <3>2, <6>2 DEF Counters + <6>4. acks[e] > 0 + BY <3>1 + <6>. QED BY <6>3, <6>4 + <5>2. InTree(p) + BY <4>2, <5>1 + <5>3. upEdge'[p] = upEdge[p] + BY <3>1 + <5>. QED BY <4>2, <5>2, <5>3 + <4>3. CASE q # p + <5>1. ~ neutral(q) + BY <3>3, <4>3, <4>1 + <5>2. InTree(q) + BY <5>1 + <5>3. upEdge'[q] = upEdge[q] + BY <3>1 + <5>. QED BY <5>2, <5>3 + <4>. QED BY <4>2, <4>3 + <3>5. \A q \in Procs \ {Leader} : + InTree(q)' => + /\ upEdge'[q] \in Edges + /\ upEdge'[q][2] = q + /\ upEdge'[q][1] \in Procs \ {q} + /\ rcvdUnacked'[upEdge'[q]] >= 1 + <4>1. SUFFICES ASSUME NEW q \in Procs \ {Leader}, InTree(q)' + PROVE /\ upEdge'[q] \in Edges + /\ upEdge'[q][2] = q + /\ upEdge'[q][1] \in Procs \ {q} + /\ rcvdUnacked'[upEdge'[q]] >= 1 + OBVIOUS + <4>2. upEdge'[q] = upEdge[q] + BY <3>1 + <4>3. InTree(q) + BY <4>1, <4>2 + <4>4. /\ upEdge[q] \in Edges + /\ upEdge[q][2] = q + /\ upEdge[q][1] \in Procs \ {q} + /\ rcvdUnacked[upEdge[q]] >= 1 + BY <4>3 + <4>5. rcvdUnacked'[upEdge[q]] = rcvdUnacked[upEdge[q]] + BY <3>1 + <4>. QED BY <4>2, <4>4, <4>5 + <3>. QED BY <3>4, <3>5 DEF Inv2 + <2>3. ASSUME NEW p \in Procs, SendAck(p) + PROVE Inv2' + <3>1. PICK e \in InEdges(p) : + /\ rcvdUnacked[e] > 0 + /\ (e = upEdge[p]) => + \/ rcvdUnacked[e] > 1 + \/ /\ ~ active[p] + /\ \A d \in InEdges(p) \ {e} : rcvdUnacked[d] = 0 + /\ \A d \in OutEdges(p) : sentUnacked[d] = 0 + /\ rcvdUnacked' = [rcvdUnacked EXCEPT ![e] = @ - 1] + /\ acks' = [acks EXCEPT ![e] = @ + 1] + BY <2>3 DEF SendAck + <3>2. /\ UNCHANGED <> + /\ upEdge' = IF neutral(p)' THEN [upEdge EXCEPT ![p] = NotAnEdge] + ELSE upEdge + BY <2>3 DEF SendAck + <3>3a. e \in Edges /\ e[2] = p /\ e \in Procs \X Procs /\ e[1] # e[2] + BY <3>1, EdgeFacts DEF InEdges + <3>3b. p # Leader + <4>1. SUFFICES ASSUME p = Leader PROVE FALSE + OBVIOUS + <4>2. e \in InEdges(Leader) + BY <3>1, <4>1 + <4>3. InEdges(Leader) = {} + BY EdgeFacts + <4>. QED BY <4>2, <4>3 + <3>3. p \in Procs \ {Leader} /\ e \in Edges /\ e[2] = p /\ e[1] # p /\ e[1] \in Procs + BY <3>3a, <3>3b + \* For q # p, neutrality is unchanged (rcvdUnacked, acks change only on + \* edge e in InEdges(p), so for q # p, no relevant counters change). + <3>4. \A q \in Procs : q # p => (neutral(q) <=> neutral(q)') + BY <3>1, <3>2, <3>3 DEF neutral, OutEdges, InEdges + \* Conjunct 3 of Inv2. + <3>5. \A q \in Procs \ {Leader} : ~ neutral(q)' => InTree(q)' + <4>1. SUFFICES ASSUME NEW q \in Procs \ {Leader}, ~ neutral(q)' + PROVE InTree(q)' + OBVIOUS + <4>2. CASE q = p + \* If neutral'(p) holds, ~ neutral(p)' is false; trivial. + \* Otherwise, upEdge' = upEdge. We must show p was non-neutral + \* before, hence upEdge[p] # NotAnEdge (i.e., InTree(p)). + <5>1. ~ neutral(p) + \* p was non-neutral because rcvdUnacked[e] > 0 with e \in + \* InEdges(p), so the conjunct rcvdUnacked = 0 of neutral fails. + BY <3>1, <3>3 DEF neutral + <5>2. InTree(p) + BY <4>2, <5>1 + <5>3. ~ neutral(p)' + BY <4>1, <4>2 + <5>4. upEdge'[p] = upEdge[p] + BY <3>2, <5>3 + <5>. QED BY <4>2, <5>2, <5>4 + <4>3. CASE q # p + <5>1. ~ neutral(q) + BY <3>4, <4>3, <4>1 + <5>2. InTree(q) + BY <5>1 + <5>3. upEdge'[q] = upEdge[q] + \* upEdge'[q] = upEdge[q] regardless of the conditional, since + \* the conditional only changes upEdge[p]. + BY <3>2, <4>3 + <5>. QED BY <5>2, <5>3 + <4>. QED BY <4>2, <4>3 + \* Conjunct 4 of Inv2. + <3>6. \A q \in Procs \ {Leader} : + InTree(q)' => + /\ upEdge'[q] \in Edges + /\ upEdge'[q][2] = q + /\ upEdge'[q][1] \in Procs \ {q} + /\ rcvdUnacked'[upEdge'[q]] >= 1 + <4>1. SUFFICES ASSUME NEW q \in Procs \ {Leader}, InTree(q)' + PROVE /\ upEdge'[q] \in Edges + /\ upEdge'[q][2] = q + /\ upEdge'[q][1] \in Procs \ {q} + /\ rcvdUnacked'[upEdge'[q]] >= 1 + OBVIOUS + <4>2. CASE q = p + \* InTree(p)' implies upEdge'[p] # NotAnEdge. By <3>2, this means + \* either ~neutral'(p) and upEdge unchanged for p, or neutral'(p) + \* and upEdge'[p] = NotAnEdge (contradicting InTree(p)'). + <5>1. ~ neutral(p)' + BY <4>1, <4>2, <3>2, <3>3 DEF NotAnEdge + <5>2. upEdge'[p] = upEdge[p] + BY <3>2, <5>1 + <5>3. InTree(p) + BY <4>1, <4>2, <5>2 + <5>4. /\ upEdge[p] \in Edges + /\ upEdge[p][2] = p + /\ upEdge[p][1] \in Procs \ {p} + /\ rcvdUnacked[upEdge[p]] >= 1 + BY <5>3, <3>3 + \* For the rcvdUnacked' >= 1 part: + \* - If upEdge[p] # e (the SendAck edge), then rcvdUnacked' is + \* unchanged at upEdge[p]. + \* - If upEdge[p] = e, then SendAck's case-2a/2b applies: either + \* rcvdUnacked[e] > 1 (so rcvdUnacked' >= 1), or neutral'(p) + \* holds, contradicting <5>1. + <5>5. rcvdUnacked'[upEdge[p]] >= 1 + <6>1. CASE upEdge[p] # e + BY <3>1, <5>4, <6>1 + <6>2. CASE upEdge[p] = e + <7>1. CASE rcvdUnacked[e] > 1 + \* rcvdUnacked'[e] = rcvdUnacked[e] - 1 >= 1. + BY <3>1, <3>3, <5>4, <6>2, <7>1 + <7>2. CASE ~ rcvdUnacked[e] > 1 + \* Then rcvdUnacked[e] = 1 (since rcvdUnacked[e] > 0). + \* From SendAck precondition (since case 2a fails), case 2b + \* must hold: ~active[p] /\ all other rcvdUnacked = 0 /\ all + \* sentUnacked = 0 on OutEdges(p). Combined with + \* rcvdUnacked'[e] = 0, we obtain neutral'(p), contradicting + \* ~neutral'(p). + <8>0. rcvdUnacked[e] = 1 + BY <3>1, <3>3, <7>2 DEF Counters, TypeOK + <8>1. /\ ~active[p] + /\ \A d \in InEdges(p) \ {e} : rcvdUnacked[d] = 0 + /\ \A d \in OutEdges(p) : sentUnacked[d] = 0 + BY <3>1, <6>2, <7>2 + <8>2. rcvdUnacked'[e] = 0 + BY <3>1, <3>3, <8>0 + <8>3. \A d \in InEdges(p) : rcvdUnacked'[d] = 0 + <9>1. SUFFICES ASSUME NEW d \in InEdges(p) + PROVE rcvdUnacked'[d] = 0 + OBVIOUS + <9>2. CASE d = e + BY <8>2, <9>2 + <9>3. CASE d # e + <10>1. rcvdUnacked'[d] = rcvdUnacked[d] + BY <3>1, <9>1, <9>3 DEF InEdges + <10>2. rcvdUnacked[d] = 0 + BY <8>1, <9>1, <9>3 + <10>. QED BY <10>1, <10>2 + <9>. QED BY <9>2, <9>3 + <8>4. \A d \in OutEdges(p) : sentUnacked'[d] = 0 + BY <3>2, <8>1 + <8>5. ~active[p]' + BY <3>2, <8>1 + <8>6. neutral(p)' + BY <8>3, <8>4, <8>5 DEF neutral + <8>. QED BY <8>6, <5>1 + <7>. QED BY <7>1, <7>2 + <6>. QED BY <6>1, <6>2 + <5>. QED BY <4>2, <5>2, <5>4, <5>5 + <4>3. CASE q # p + <5>1. upEdge'[q] = upEdge[q] + BY <3>2, <4>3 + <5>2. InTree(q) + BY <4>1, <5>1 + <5>3. /\ upEdge[q] \in Edges + /\ upEdge[q][2] = q + /\ upEdge[q][1] \in Procs \ {q} + /\ rcvdUnacked[upEdge[q]] >= 1 + BY <5>2 + \* upEdge[q][2] = q and e[2] = p (from <3>3), with q # p, + \* so upEdge[q] # e. Hence rcvdUnacked' is unchanged at upEdge[q]. + <5>4. upEdge[q] # e + BY <3>3, <4>3, <5>3 + <5>5. rcvdUnacked'[upEdge[q]] = rcvdUnacked[upEdge[q]] + BY <3>1, <5>3, <5>4 + <5>. QED BY <5>1, <5>3, <5>5 + <4>. QED BY <4>2, <4>3 + <3>. QED BY <3>5, <3>6 DEF Inv2 + <2>4. ASSUME NEW p \in Procs, RcvMsg(p) + PROVE Inv2' + <3>1. PICK e \in InEdges(p) : + /\ msgs[e] > 0 + /\ msgs' = [msgs EXCEPT ![e] = @ - 1] + /\ rcvdUnacked' = [rcvdUnacked EXCEPT ![e] = @ + 1] + /\ active' = [active EXCEPT ![p] = TRUE] + /\ upEdge' = IF neutral(p) THEN [upEdge EXCEPT ![p] = e] + ELSE upEdge + /\ UNCHANGED <> + BY <2>4 DEF RcvMsg + <3>2. p \in Procs \ {Leader} /\ e \in Edges /\ e[2] = p /\ e[1] # p /\ e[1] \in Procs + BY <3>1, EdgeFacts DEF InEdges + \* Active'[p] = TRUE, hence ~neutral'(p) (due to active flag). + \* For q # p, neutrality status is unchanged by RcvMsg(p). + <3>3. \A q \in Procs : q # p => (neutral(q) <=> neutral(q)') + BY <3>1, <3>2 DEF neutral, InEdges, OutEdges + <3>4. ~ (neutral(p))' + BY <3>1, <3>2 DEF neutral + <3>5. \A q \in Procs \ {Leader} : ~ neutral(q)' => InTree(q)' + <4>1. SUFFICES ASSUME NEW q \in Procs \ {Leader}, ~ neutral(q)' + PROVE InTree(q)' + OBVIOUS + <4>2. CASE q = p + \* If p was neutral, upEdge' is set to e, so InTree'(p). + \* If p was non-neutral, upEdge' = upEdge and we use the IH. + <5>1. CASE neutral(p) + \* upEdge'[p] = e \in Edges, e \in Procs \X Procs, so e is a + \* 2-tuple, hence e # NotAnEdge = <<>>. + <6>1. upEdge'[p] = e + BY <3>1, <3>2, <5>1 + <6>2. e \in Procs \X Procs + BY <3>2, EdgeFacts + <6>3. e # NotAnEdge + BY <6>2 DEF NotAnEdge + <6>. QED BY <4>2, <6>1, <6>3 + <5>2. CASE ~neutral(p) + <6>1. InTree(p) + BY <5>2, <3>2 + <6>2. upEdge'[p] = upEdge[p] + BY <3>1, <5>2 + <6>. QED BY <4>2, <6>1, <6>2 + <5>. QED BY <5>1, <5>2 + <4>3. CASE q # p + <5>1. ~neutral(q) + BY <3>3, <4>3, <4>1 + <5>2. InTree(q) + BY <5>1 + <5>3. upEdge'[q] = upEdge[q] + BY <3>1, <4>3 + <5>. QED BY <5>2, <5>3 + <4>. QED BY <4>2, <4>3 + <3>6. \A q \in Procs \ {Leader} : + InTree(q)' => + /\ upEdge'[q] \in Edges + /\ upEdge'[q][2] = q + /\ upEdge'[q][1] \in Procs \ {q} + /\ rcvdUnacked'[upEdge'[q]] >= 1 + <4>1. SUFFICES ASSUME NEW q \in Procs \ {Leader}, InTree(q)' + PROVE /\ upEdge'[q] \in Edges + /\ upEdge'[q][2] = q + /\ upEdge'[q][1] \in Procs \ {q} + /\ rcvdUnacked'[upEdge'[q]] >= 1 + OBVIOUS + <4>2. CASE q = p + <5>1. CASE neutral(p) + \* upEdge'[p] = e, e[2] = p, e \in Edges, e[1] \in Procs \ {p}. + \* rcvdUnacked'[e] = rcvdUnacked[e] + 1 >= 1. + BY <3>1, <3>2, <4>2, <5>1 + <5>2. CASE ~neutral(p) + \* upEdge'[p] = upEdge[p], use IH for p. + <6>1. InTree(p) + BY <5>2, <3>2 + <6>2. upEdge'[p] = upEdge[p] + BY <3>1, <5>2 + <6>3. /\ upEdge[p] \in Edges + /\ upEdge[p][2] = p + /\ upEdge[p][1] \in Procs \ {p} + /\ rcvdUnacked[upEdge[p]] >= 1 + BY <6>1, <3>2 + \* Either upEdge[p] = e (then rcvdUnacked' = rcvdUnacked+1 >= 2) + \* or upEdge[p] # e (then rcvdUnacked'[upEdge[p]] = rcvdUnacked[upEdge[p]]). + <6>4. rcvdUnacked'[upEdge[p]] >= 1 + BY <3>1, <6>3 + <6>. QED BY <4>2, <6>2, <6>3, <6>4 + <5>. QED BY <5>1, <5>2 + <4>3. CASE q # p + \* upEdge'[q] = upEdge[q]. Neutrality of q unchanged. + <5>1. upEdge'[q] = upEdge[q] + BY <3>1, <4>3 + <5>2. InTree(q) + BY <4>1, <5>1 + <5>3. /\ upEdge[q] \in Edges + /\ upEdge[q][2] = q + /\ upEdge[q][1] \in Procs \ {q} + /\ rcvdUnacked[upEdge[q]] >= 1 + BY <5>2 + \* upEdge[q][2] = q and e[2] = p, with q # p, so upEdge[q] # e. + <5>4. upEdge[q] # e + BY <3>2, <4>3, <5>3 + <5>5. rcvdUnacked'[upEdge[q]] = rcvdUnacked[upEdge[q]] + BY <3>1, <5>3, <5>4 + <5>. QED BY <5>1, <5>3, <5>5 + <4>. QED BY <4>2, <4>3 + <3>. QED BY <3>5, <3>6 DEF Inv2 + <2>. QED BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6 DEF Next +<1>. QED BY <1>1, <1>2, Inv1Inductive, PTL DEF Spec + +----------------------------------------------------------------------------- +(***************************************************************************) +(* Inductiveness of the auxiliary acyclicity invariant NoCycle (defined *) +(* alongside Inv2 above). The proof depends on Inv2 (in particular *) +(* Counters and conjunct 4) for the RcvMsg case. *) +(***************************************************************************) +LEMMA NoCycleInit == Init => NoCycle + <1>. SUFFICES ASSUME Init, + NEW S \in SUBSET (Procs \ {Leader}), + S # {}, + \A q \in S : InTree(q) /\ upEdge[q][1] \in S + PROVE FALSE + BY DEF NoCycle + <1>1. PICK q \in S : TRUE + OBVIOUS + <1>2. q \in Procs \ {Leader} + OBVIOUS + <1>3. upEdge[q] = NotAnEdge + BY <1>2 DEF Init + <1>4. ~ InTree(q) + BY <1>3 DEF InTree + <1>. QED BY <1>1, <1>4 + +LEMMA NoCycleStep == Inv1 /\ Inv2 /\ NoCycle /\ [Next]_vars => NoCycle' + <1>. SUFFICES ASSUME Inv1, Inv2, NoCycle, [Next]_vars + PROVE NoCycle' + OBVIOUS + <1>. USE DEF Inv1, Inv2, TypeOK, Counters, InTree, NotAnEdge + <1>1. ASSUME NEW p \in Procs, SendMsg(p) + PROVE NoCycle' + <2>1. upEdge' = upEdge + BY <1>1 DEF SendMsg + <2>. SUFFICES ASSUME NEW S \in SUBSET (Procs \ {Leader}), + S # {}, + \A q \in S : InTree(q)' /\ upEdge'[q][1] \in S + PROVE FALSE + BY DEF NoCycle + <2>. QED BY <2>1 DEF NoCycle + <1>2. ASSUME NEW p \in Procs, RcvAck(p) + PROVE NoCycle' + <2>1. upEdge' = upEdge + BY <1>2 DEF RcvAck + <2>. SUFFICES ASSUME NEW S \in SUBSET (Procs \ {Leader}), + S # {}, + \A q \in S : InTree(q)' /\ upEdge'[q][1] \in S + PROVE FALSE + BY DEF NoCycle + <2>. QED BY <2>1 DEF NoCycle + <1>3. ASSUME NEW p \in Procs, Idle(p) + PROVE NoCycle' + <2>1. upEdge' = upEdge + BY <1>3 DEF Idle + <2>. SUFFICES ASSUME NEW S \in SUBSET (Procs \ {Leader}), + S # {}, + \A q \in S : InTree(q)' /\ upEdge'[q][1] \in S + PROVE FALSE + BY DEF NoCycle + <2>. QED BY <2>1 DEF NoCycle + <1>4. CASE UNCHANGED vars + <2>1. upEdge' = upEdge + BY <1>4 DEF vars + <2>. SUFFICES ASSUME NEW S \in SUBSET (Procs \ {Leader}), + S # {}, + \A q \in S : InTree(q)' /\ upEdge'[q][1] \in S + PROVE FALSE + BY DEF NoCycle + <2>. QED BY <2>1 DEF NoCycle + <1>5. ASSUME NEW p \in Procs, SendAck(p) + PROVE NoCycle' + <2>0. PICK e \in InEdges(p) : + /\ rcvdUnacked[e] > 0 + /\ rcvdUnacked' = [rcvdUnacked EXCEPT ![e] = @ - 1] + /\ acks' = [acks EXCEPT ![e] = @ + 1] + BY <1>5 DEF SendAck + <2>1. upEdge' = IF neutral(p)' THEN [upEdge EXCEPT ![p] = NotAnEdge] + ELSE upEdge + BY <1>5 DEF SendAck + <2>2. p # Leader + <3>1. SUFFICES ASSUME p = Leader PROVE FALSE + OBVIOUS + <3>2. e \in InEdges(Leader) + BY <2>0, <3>1 + <3>3. InEdges(Leader) = {} + BY EdgeFacts + <3>. QED BY <3>2, <3>3 + <2>. SUFFICES ASSUME NEW S \in SUBSET (Procs \ {Leader}), + S # {}, + \A q \in S : InTree(q)' /\ upEdge'[q][1] \in S + PROVE FALSE + BY DEF NoCycle + <2>case1. CASE ~ neutral(p)' + <3>1. upEdge' = upEdge + BY <2>1, <2>case1 + <3>2. \A q \in S : InTree(q) /\ upEdge[q][1] \in S + BY <3>1 + <3>. QED BY <3>2 DEF NoCycle + <2>case2. CASE neutral(p)' + <3>1. upEdge' = [upEdge EXCEPT ![p] = NotAnEdge] + BY <2>1, <2>case2 + <3>2. p \in DOMAIN upEdge + BY <2>2 + <3>3. upEdge'[p] = NotAnEdge + BY <3>1, <3>2 + <3>4. ~ InTree(p)' + BY <3>3 + <3>5. p \notin S + BY <3>4 + <3>6. \A q \in S : q # p + BY <3>5 + <3>7. \A q \in S : upEdge'[q] = upEdge[q] + BY <3>1, <3>6 + <3>8. \A q \in S : InTree(q) /\ upEdge[q][1] \in S + BY <3>7 + <3>. QED BY <3>8 DEF NoCycle + <2>. QED BY <2>case1, <2>case2 + <1>6. ASSUME NEW p \in Procs, RcvMsg(p) + PROVE NoCycle' + <2>0. PICK e \in InEdges(p) : + /\ msgs[e] > 0 + /\ msgs' = [msgs EXCEPT ![e] = @ - 1] + /\ rcvdUnacked' = [rcvdUnacked EXCEPT ![e] = @ + 1] + /\ active' = [active EXCEPT ![p] = TRUE] + /\ upEdge' = IF neutral(p) THEN [upEdge EXCEPT ![p] = e] + ELSE upEdge + /\ UNCHANGED <> + BY <1>6 DEF RcvMsg + <2>1. p \in Procs \ {Leader} /\ e \in Edges /\ e[2] = p /\ e[1] # p /\ e[1] \in Procs + BY <2>0, EdgeFacts DEF InEdges + <2>. SUFFICES ASSUME NEW S \in SUBSET (Procs \ {Leader}), + S # {}, + \A q \in S : InTree(q)' /\ upEdge'[q][1] \in S + PROVE FALSE + BY DEF NoCycle + <2>case1. CASE ~ neutral(p) + <3>1. upEdge' = upEdge + BY <2>0, <2>case1 + <3>2. \A q \in S : InTree(q) /\ upEdge[q][1] \in S + BY <3>1 + <3>. QED BY <3>2 DEF NoCycle + <2>case2. CASE neutral(p) + <3>1. upEdge' = [upEdge EXCEPT ![p] = e] + BY <2>0, <2>case2 + <3>2. p \in DOMAIN upEdge + BY <2>1 + <3>caseA. CASE p \notin S + <4>1. \A q \in S : q # p + BY <3>caseA + <4>2. \A q \in S : upEdge'[q] = upEdge[q] + BY <3>1, <4>1 + <4>3. \A q \in S : InTree(q) /\ upEdge[q][1] \in S + BY <4>2 + <4>. QED BY <4>3 DEF NoCycle + <3>caseB. CASE p \in S + <4>0. upEdge'[p] = e + BY <3>1, <3>2 + <4>1. upEdge'[p][1] = e[1] + BY <4>0 + <4>2. e[1] \in S + BY <3>caseB, <4>1 + <4>3. e[1] # p + BY <2>1 + <4>4. e[1] \in S \ {p} + BY <4>2, <4>3 + <4>5. SUFFICES ASSUME NEW q \in S \ {p} + PROVE InTree(q) /\ upEdge[q][1] \in (S \ {p}) + BY <4>4 DEF NoCycle + <4>9. q \in S /\ q # p /\ q \in Procs \ {Leader} + OBVIOUS + <4>11. upEdge'[q] = upEdge[q] + BY <3>1, <4>9 + <4>12. InTree(q) + BY <4>9, <4>11 + <4>13. upEdge[q][1] \in S + BY <4>9, <4>11 + <4>14. /\ upEdge[q] \in Edges + /\ upEdge[q][2] = q + /\ upEdge[q][1] \in Procs \ {q} + /\ rcvdUnacked[upEdge[q]] >= 1 + BY <4>9, <4>12 + <4>15. sentUnacked[upEdge[q]] >= 1 + BY <4>14 + <4>16. upEdge[q][1] # p + <5>1. SUFFICES ASSUME upEdge[q][1] = p PROVE FALSE + OBVIOUS + <5>2. upEdge[q] \in OutEdges(p) + BY <5>1, <4>14 DEF OutEdges + <5>3. sentUnacked[upEdge[q]] = 0 + BY <2>case2, <5>2 DEF neutral + <5>. QED BY <4>15, <5>3 + <4>17. upEdge[q][1] \in (S \ {p}) + BY <4>13, <4>16 + <4>. QED BY <4>12, <4>17 + <3>. QED BY <3>caseA, <3>caseB + <2>. QED BY <2>case1, <2>case2 + <1>. QED + BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6 DEF Next + +LEMMA NoCycleInductive == Spec => []NoCycle + <1>1. Init => NoCycle + BY NoCycleInit + <1>2. Inv1 /\ Inv2 /\ NoCycle /\ [Next]_vars => NoCycle' + BY NoCycleStep + <1>3. Spec => []Inv2 + BY Inv2Inductive + <1>4. Spec => []Inv1 + BY Inv1Inductive + <1>. QED + BY <1>1, <1>2, <1>3, <1>4, PTL DEF Spec + +(***************************************************************************) +(* Discharge of DT1FromInv2 using Inv2 and the acyclicity invariant. *) +(***************************************************************************) +LEMMA DT1FromInv2 == Inv1 /\ Inv2 /\ NoCycle => DT1Inv + <1>. SUFFICES ASSUME Inv1, Inv2, NoCycle PROVE DT1Inv + OBVIOUS + <1>. USE DEF Inv1, Inv2, TypeOK, Counters, InTree, NotAnEdge + <1>. SUFFICES ASSUME neutral(Leader), + NEW p0 \in Procs \ {Leader} + PROVE neutral(p0) + BY DEF DT1Inv + <1>contra. ASSUME ~ neutral(p0) PROVE FALSE + <2>. DEFINE S == {q \in Procs \ {Leader} : ~ neutral(q)} + <2>4. S # {} + BY <1>contra DEF S + <2>5. S \in SUBSET (Procs \ {Leader}) + BY DEF S + <2>6. SUFFICES ASSUME NEW q \in S + PROVE InTree(q) /\ upEdge[q][1] \in S + BY <2>4, <2>5 DEF NoCycle + <2>8. q \in Procs \ {Leader} /\ ~ neutral(q) + BY DEF S + <2>9. InTree(q) + BY <2>8 + <2>10. /\ upEdge[q] \in Edges + /\ upEdge[q][2] = q + /\ upEdge[q][1] \in Procs \ {q} + /\ rcvdUnacked[upEdge[q]] >= 1 + BY <2>8, <2>9 + <2>11. sentUnacked[upEdge[q]] >= 1 + BY <2>10 + <2>12. upEdge[q] \in OutEdges(upEdge[q][1]) + BY <2>10 DEF OutEdges + <2>13. ~ neutral(upEdge[q][1]) + BY <2>11, <2>12 DEF neutral + <2>16. upEdge[q][1] \in S + BY <2>10, <2>13 DEF S + <2>. QED BY <2>9, <2>16 + <1>. QED BY <1>contra + +THEOREM Thm_DT1Inv == Spec => []DT1Inv + <1>0. Spec => []Inv1 + BY Inv1Inductive + <1>1. Spec => []Inv2 + BY Inv2Inductive + <1>2. Spec => []NoCycle + BY NoCycleInductive + <1>3. Inv1 /\ Inv2 /\ NoCycle => DT1Inv + BY DT1FromInv2 + <1>. QED + BY <1>0, <1>1, <1>2, <1>3, PTL + +----------------------------------------------------------------------------- +(***************************************************************************) +(* Theorem 2: Spec => TreeWithRoot *) +(* *) +(* The set E of upEdges (excluding NotAnEdge), with N the set of nodes *) +(* appearing in those edges, forms (when transposed) a tree rooted at *) +(* the leader, and every node of that tree is non-neutral. *) +(* *) +(* This requires reasoning about the IsTreeWithRoot predicate from the *) +(* community-modules Graphs module, in particular about the existence of *) +(* simple paths from every node to the root and the uniqueness of edges. *) +(* The structural invariant Inv2 above already captures the tree shape; *) +(* what is missing is the unfolding of IsTreeWithRoot/SimplePath/ *) +(* Cardinality from the community-modules definitions, left as future *) +(* work. *) +(***************************************************************************) +THEOREM Thm_TreeWithRoot == Spec => TreeWithRoot +OMITTED + +----------------------------------------------------------------------------- +(***************************************************************************) +(* Theorem 4: Spec => DT2 (liveness) *) +(* *) +(* Liveness: Terminated ~> neutral(Leader). *) +(* *) +(* Once the computation has globally terminated, the WF_vars(Next) *) +(* fairness assumption guarantees progress on each remaining *) +(* RcvMsg/SendAck/RcvAck step until all counters drain to 0 and the *) +(* leader becomes neutral. A multiset/well-founded measure on *) +(* (msgs, rcvdUnacked, acks, sentUnacked) is needed; left as future work. *) +(***************************************************************************) +THEOREM Thm_DT2 == Spec => DT2 +OMITTED + +============================================================================= diff --git a/specifications/ewd998/EWD998PCal_proof.tla b/specifications/ewd998/EWD998PCal_proof.tla new file mode 100644 index 00000000..aa31b1c3 --- /dev/null +++ b/specifications/ewd998/EWD998PCal_proof.tla @@ -0,0 +1,1443 @@ +---------------------------- MODULE EWD998PCal_proof ---------------------------- +(***************************************************************************) +(* Proofs checked by TLAPS about the EWD998PCal specification. *) +(* *) +(* The EWD998PCal module is a PlusCal-translated version of EWD998 in *) +(* which the per-node `pending` counter and the global `token` of EWD998 *) +(* are replaced by a single `network` variable holding a per-node bag of *) +(* messages (payload "pl" messages and the unique token "tok" message). *) +(* The refinement mapping (in EWD998PCal.tla) recovers EWD998's `pending` *) +(* and `token` from `network`: *) +(* *) +(* pending = [n |-> count of [type|->"pl"] in network[n]] *) +(* token = the unique tok msg in the network, with its position *) +(* *) +(* This module proves the safety part of the refinement, *) +(* *) +(* THEOREM Refinement == Spec => EWD998Spec *) +(* *) +(* where EWD998Spec == EWD998!Init /\ [][EWD998!Next]_EWD998!vars (no *) +(* fairness; the comment in the spec explains why). *) +(* *) +(* The proof shape mirrors EWD998_proof.tla's `Refinement` theorem: *) +(* an inductive invariant (network well-formedness + Safra's invariant *) +(* transferred to PCal) plus a per-disjunct case analysis. *) +(***************************************************************************) +EXTENDS EWD998PCal, TLAPS + +USE NAssumption + +\* The spec defines `Initiator == 0`; expose it as a fact for TLAPS. +LEMMA InitiatorIsZero == Initiator = 0 BY DEF Initiator + +\* Node = 0..N-1. +LEMMA NodeFact == 0 \in Node BY DEF Node + +(***************************************************************************) +(* Type-level abbreviations. *) +(***************************************************************************) +ColorSet == {"white", "black"} +PMsg == [type: {"pl"}] +TMsg == [type: {"tok"}, q: Int, color: ColorSet] +Msg == PMsg \cup TMsg + +(***************************************************************************) +(* Bag-level facts about the message-bag operators used in the spec. *) +(* *) +(* `EmptyBag`, `SetToBag`, `BagAdd`, `BagRemove` are imported from *) +(* Bags / BagsExt. We restate just enough about each so TLAPS can *) +(* unfold them in proofs. *) +(***************************************************************************) +LEMMA EmptyBagDom == DOMAIN EmptyBag = {} + BY DEF EmptyBag, SetToBag + +LEMMA SetToBagSingleton == + ASSUME NEW x + PROVE /\ DOMAIN SetToBag({x}) = {x} + /\ SetToBag({x})[x] = 1 + BY DEF SetToBag + +LEMMA BagAddDom == + ASSUME NEW B, NEW x + PROVE DOMAIN BagAdd(B, x) = DOMAIN B \cup {x} + BY DEF BagAdd + +LEMMA BagRemoveDom == + ASSUME NEW B, NEW x, x \in DOMAIN B + PROVE /\ B[x] = 1 => DOMAIN BagRemove(B, x) = DOMAIN B \ {x} + /\ B[x] # 1 => DOMAIN BagRemove(B, x) = DOMAIN B + BY DEF BagRemove + +(***************************************************************************) +(* Network well-formedness: *) +(* (a) every network[n] is a function from a subset of Msg to positive *) +(* naturals (the `IsABag` predicate, restricted to typed messages); *) +(* (b) exactly one node holds a token, with multiplicity 1. *) +(***************************************************************************) +BagOf(S) == UNION { [T -> Nat \ {0}] : T \in SUBSET S } + +NetworkOK == + /\ network \in [Node -> BagOf(Msg)] + /\ \E n \in Node : \E t \in DOMAIN network[n] : + /\ t.type = "tok" + /\ network[n][t] = 1 + /\ \A n2 \in Node : \A t2 \in DOMAIN network[n2] : + t2.type = "tok" => (n2 = n /\ t2 = t) + +PCalTypeOK == + /\ active \in [Node -> BOOLEAN] + /\ color \in [Node -> ColorSet] + /\ counter \in [Node -> Int] + /\ NetworkOK + +(***************************************************************************) +(* The initial state has the unique token (with q=0, color="black") at the*) +(* Initiator (=0) and empty bags everywhere else. *) +(***************************************************************************) +InitTok == [type |-> "tok", q |-> 0, color |-> "black"] + +LEMMA InitNetworkUniqueTok == + ASSUME network = [n \in Node |-> + IF n = Initiator + THEN SetToBag({InitTok}) + ELSE EmptyBag] + PROVE /\ DOMAIN network[Initiator] = {InitTok} + /\ network[Initiator][InitTok] = 1 + /\ \A n \in Node \ {Initiator} : DOMAIN network[n] = {} + <1>1. DOMAIN network[Initiator] = DOMAIN SetToBag({InitTok}) + BY DEF Initiator, Node + <1>2. DOMAIN SetToBag({InitTok}) = {InitTok} + BY SetToBagSingleton + <1>3. network[Initiator][InitTok] = SetToBag({InitTok})[InitTok] + BY DEF Initiator, Node + <1>4. SetToBag({InitTok})[InitTok] = 1 + BY SetToBagSingleton + <1>5. ASSUME NEW n \in Node \ {Initiator} + PROVE DOMAIN network[n] = {} + <2>1. network[n] = EmptyBag + BY <1>5 DEF Initiator, Node + <2>. QED BY <2>1, EmptyBagDom + <1>. QED BY <1>1, <1>2, <1>3, <1>4, <1>5 + +(***************************************************************************) +(* The initial state satisfies the network type invariant. *) +(***************************************************************************) +LEMMA InitNetworkOK == Init => NetworkOK + <1>. SUFFICES ASSUME Init PROVE NetworkOK + OBVIOUS + <1>. USE InitiatorIsZero, NodeFact + <1>1. network = [n \in Node |-> + IF n = Initiator + THEN SetToBag({InitTok}) + ELSE EmptyBag] + BY DEF Init, InitTok + <1>2. \A n \in Node \ {Initiator} : DOMAIN network[n] = {} + BY <1>1, InitNetworkUniqueTok + <1>3. /\ DOMAIN network[Initiator] = {InitTok} + /\ network[Initiator][InitTok] = 1 + BY <1>1, InitNetworkUniqueTok + <1>4. InitTok \in Msg + BY DEF Msg, TMsg, ColorSet, InitTok + <1>5. network \in [Node -> BagOf(Msg)] + <2>0. network = [n \in Node |-> IF n = Initiator THEN SetToBag({InitTok}) ELSE EmptyBag] + BY <1>1 + <2>1. ASSUME NEW n \in Node + PROVE (IF n = Initiator THEN SetToBag({InitTok}) ELSE EmptyBag) \in BagOf(Msg) + <3>1. CASE n = Initiator + <4>1. SetToBag({InitTok}) = [e \in {InitTok} |-> 1] + BY DEF SetToBag + <4>2. [e \in {InitTok} |-> 1] \in [{InitTok} -> Nat \ {0}] + OBVIOUS + <4>3. {InitTok} \in SUBSET Msg + BY <1>4 + <4>. QED BY <3>1, <4>1, <4>2, <4>3 DEF BagOf + <3>2. CASE n # Initiator + <4>1. EmptyBag = [e \in {} |-> 1] + BY DEF EmptyBag, SetToBag + <4>2. [e \in {} |-> 1] \in [{} -> Nat \ {0}] + OBVIOUS + <4>3. {} \in SUBSET Msg + OBVIOUS + <4>. QED BY <3>2, <4>1, <4>2, <4>3 DEF BagOf + <3>. QED BY <3>1, <3>2 + <2>. QED BY <2>0, <2>1 + <1>6. \E n \in Node : \E t \in DOMAIN network[n] : + /\ t.type = "tok" + /\ network[n][t] = 1 + /\ \A n2 \in Node : \A t2 \in DOMAIN network[n2] : + t2.type = "tok" => (n2 = n /\ t2 = t) + <2>1. InitTok \in DOMAIN network[Initiator] + BY <1>3 + <2>2. InitTok.type = "tok" BY DEF InitTok + <2>3. network[Initiator][InitTok] = 1 BY <1>3 + <2>4. \A n2 \in Node : \A t2 \in DOMAIN network[n2] : + t2.type = "tok" => (n2 = Initiator /\ t2 = InitTok) + <3>. SUFFICES ASSUME NEW n2 \in Node, NEW t2 \in DOMAIN network[n2], + t2.type = "tok" + PROVE n2 = Initiator /\ t2 = InitTok + OBVIOUS + <3>1. n2 = Initiator + BY <1>2 + <3>2. t2 \in DOMAIN network[Initiator] + BY <3>1 + <3>3. t2 = InitTok + BY <3>2, <1>3 + <3>. QED BY <3>1, <3>3 + <2>. QED BY <2>1, <2>2, <2>3, <2>4, Initiator \in Node, InitiatorIsZero, NodeFact + <1>. QED BY <1>5, <1>6 DEF NetworkOK + +(***************************************************************************) +(* The initial state satisfies the full PCalTypeOK. *) +(***************************************************************************) +LEMMA InitTypeOK == Init => PCalTypeOK + <1>. SUFFICES ASSUME Init PROVE PCalTypeOK + OBVIOUS + <1>1. active \in [Node -> BOOLEAN] + BY DEF Init + <1>2. color \in [Node -> ColorSet] + BY DEF Init, ColorSet + <1>3. counter \in [Node -> Int] + <2>. counter = [self \in Node |-> 0] BY DEF Init + <2>. QED BY Isa + <1>4. NetworkOK + BY InitNetworkOK + <1>. QED BY <1>1, <1>2, <1>3, <1>4 DEF PCalTypeOK + +(***************************************************************************) +(* Init refinement: the PCal Init satisfies EWD998!Init under the *) +(* refinement mapping for `pending` and `token`. *) +(***************************************************************************) +LEMMA InitPending == Init => pending = [i \in Node |-> 0] + <1>. SUFFICES ASSUME Init PROVE pending = [i \in Node |-> 0] + OBVIOUS + <1>. USE InitiatorIsZero, NodeFact + <1>1. network = [n \in Node |-> + IF n = Initiator + THEN SetToBag({InitTok}) + ELSE EmptyBag] + BY DEF Init, InitTok + <1>2. ASSUME NEW i \in Node + PROVE pending[i] = 0 + <2>1. CASE i = Initiator + <3>1. DOMAIN network[i] = {InitTok} + BY <2>1, <1>1, InitNetworkUniqueTok + <3>2. [type |-> "pl"] # InitTok + BY DEF InitTok + <3>3. [type |-> "pl"] \notin DOMAIN network[i] + BY <3>1, <3>2 + <3>. QED BY <3>3 DEF pending + <2>2. CASE i # Initiator + <3>1. DOMAIN network[i] = {} + BY <2>2, <1>1, InitNetworkUniqueTok + <3>. QED BY <3>1 DEF pending + <2>. QED BY <2>1, <2>2 + <1>3. pending = [i \in Node |-> 0] + <2>1. pending = [n \in Node |-> IF [type|->"pl"] \in DOMAIN network[n] + THEN network[n][[type|->"pl"]] ELSE 0] + BY DEF pending + <2>2. \A n \in Node : (IF [type|->"pl"] \in DOMAIN network[n] + THEN network[n][[type|->"pl"]] ELSE 0) = 0 + <3>. SUFFICES ASSUME NEW n \in Node + PROVE (IF [type|->"pl"] \in DOMAIN network[n] + THEN network[n][[type|->"pl"]] ELSE 0) = 0 + OBVIOUS + <3>1. CASE n = Initiator + <4>1. DOMAIN network[n] = {InitTok} + BY <3>1, <1>1, InitNetworkUniqueTok + <4>2. [type|->"pl"] # InitTok + BY DEF InitTok + <4>. QED BY <4>1, <4>2 + <3>2. CASE n # Initiator + <4>1. DOMAIN network[n] = {} + BY <3>2, <1>1, InitNetworkUniqueTok + <4>. QED BY <4>1 + <3>. QED BY <3>1, <3>2 + <2>. QED BY <2>1, <2>2 + <1>. QED BY <1>3 + +LEMMA InitToken == Init => token = [pos |-> 0, q |-> 0, color |-> "black"] + <1>. SUFFICES ASSUME Init PROVE token = [pos |-> 0, q |-> 0, color |-> "black"] + OBVIOUS + <1>. USE InitiatorIsZero, NodeFact + <1>1. network = [n \in Node |-> + IF n = Initiator + THEN SetToBag({InitTok}) + ELSE EmptyBag] + BY DEF Init, InitTok + <1>2. \A n \in Node \ {Initiator} : DOMAIN network[n] = {} + BY <1>1, InitNetworkUniqueTok + <1>3. DOMAIN network[Initiator] = {InitTok} + BY <1>1, InitNetworkUniqueTok + <1>4. (CHOOSE i \in Node : \E m \in DOMAIN network[i]: m.type = "tok") = Initiator + <2>1. \E m \in DOMAIN network[Initiator] : m.type = "tok" + <3>1. InitTok \in DOMAIN network[Initiator] BY <1>3 + <3>2. InitTok.type = "tok" BY DEF InitTok + <3>. QED BY <3>1, <3>2 + <2>2. \A i \in Node : + (\E m \in DOMAIN network[i] : m.type = "tok") => i = Initiator + <3>. SUFFICES ASSUME NEW i \in Node, + \E m \in DOMAIN network[i] : m.type = "tok" + PROVE i = Initiator + OBVIOUS + <3>1. CASE i # Initiator + <4>1. DOMAIN network[i] = {} BY <3>1, <1>2 + <4>. QED BY <4>1 + <3>. QED BY <3>1 + <2>. QED BY <2>1, <2>2 + <1>5. (CHOOSE m \in DOMAIN network[Initiator] : m.type = "tok") = InitTok + <2>1. InitTok \in DOMAIN network[Initiator] BY <1>3 + <2>2. InitTok.type = "tok" BY DEF InitTok + <2>3. \A m \in DOMAIN network[Initiator] : m.type = "tok" => m = InitTok + BY <1>3 + <2>. QED BY <2>1, <2>2, <2>3 + <1>6. token = [pos |-> Initiator, q |-> InitTok.q, color |-> InitTok.color] + BY <1>4, <1>5 DEF token + <1>. QED BY <1>6 DEF InitTok + +THEOREM InitRefinement == Init => EWD998!Init + <1>. SUFFICES ASSUME Init PROVE EWD998!Init + OBVIOUS + <1>. USE InitiatorIsZero, NodeFact + <1>1. EWD998!Node = Node + BY DEF EWD998!Node, Node + <1>2. EWD998!Color = ColorSet + BY DEF EWD998!Color, ColorSet + <1>3. active \in [Node -> BOOLEAN] + BY DEF Init + <1>4. color \in [Node -> EWD998!Color] + BY <1>1, <1>2 DEF Init, ColorSet + <1>5. counter = [i \in Node |-> 0] + BY <1>1 DEF Init + <1>6. pending = [i \in Node |-> 0] + BY InitPending, <1>1 + <1>7. token \in [pos: Node, q: {0}, color: {"black"}] + <2>1. token = [pos |-> 0, q |-> 0, color |-> "black"] + BY InitToken + <2>. QED BY <2>1 + <1>. QED BY <1>1, <1>3, <1>4, <1>5, <1>6, <1>7 DEF EWD998!Init + +(***************************************************************************) +(* Helper: for any well-typed bag B and any new "pl" message added with *) +(* BagAdd (which is a fresh element if not already in DOMAIN, otherwise *) +(* a multiplicity bump), the result is still a well-typed bag of typed *) +(* messages. *) +(***************************************************************************) +LEMMA BagAddOfMsg == + ASSUME NEW B \in BagOf(Msg), NEW m \in Msg + PROVE BagAdd(B, m) \in BagOf(Msg) + <1>. PICK S \in SUBSET Msg : B \in [S -> Nat \ {0}] + BY DEF BagOf + <1>1. DOMAIN B = S + OBVIOUS + <1>2. CASE m \in DOMAIN B + <2>1. BagAdd(B, m) = [e \in DOMAIN B |-> IF e = m THEN B[e]+1 ELSE B[e]] + BY <1>2 DEF BagAdd + <2>2. ASSUME NEW e \in DOMAIN B + PROVE (IF e = m THEN B[e]+1 ELSE B[e]) \in Nat \ {0} + <3>1. B[e] \in Nat /\ B[e] > 0 OBVIOUS + <3>2. B[e]+1 \in Nat /\ B[e]+1 > 0 + BY <3>1 + <3>. QED BY <3>1, <3>2 + <2>3. BagAdd(B, m) \in [DOMAIN B -> Nat \ {0}] + BY <2>1, <2>2 + <2>. QED BY <2>3, <1>1, S \in SUBSET Msg DEF BagOf + <1>3. CASE m \notin DOMAIN B + <2>1. BagAdd(B, m) = [e \in DOMAIN B \cup {m} |-> IF e = m THEN 1 ELSE B[e]] + BY <1>3 DEF BagAdd + <2>2. ASSUME NEW e \in DOMAIN B \cup {m} + PROVE (IF e = m THEN 1 ELSE B[e]) \in Nat \ {0} + <3>1. CASE e = m + BY <3>1 + <3>2. CASE e # m + <4>1. e \in DOMAIN B BY <2>2, <3>2 + <4>2. B[e] \in Nat /\ B[e] > 0 BY <4>1 + <4>. QED BY <3>2, <4>2 + <3>. QED BY <3>1, <3>2 + <2>3. DOMAIN B \cup {m} \in SUBSET Msg + BY <1>1, S \in SUBSET Msg + <2>4. BagAdd(B, m) \in [DOMAIN B \cup {m} -> Nat \ {0}] + BY <2>1, <2>2 + <2>. QED BY <2>3, <2>4 DEF BagOf + <1>. QED BY <1>2, <1>3 + +(***************************************************************************) +(* Helper: BagRemove on a typed bag yields a typed bag. This is true *) +(* regardless of whether x is in DOMAIN B (BagRemove returns B unchanged *) +(* in that case) or with multiplicity > 1 or = 1. *) +(***************************************************************************) +LEMMA BagRemoveOfMsg == + ASSUME NEW B \in BagOf(Msg), NEW x + PROVE BagRemove(B, x) \in BagOf(Msg) + <1>. PICK S \in SUBSET Msg : B \in [S -> Nat \ {0}] + BY DEF BagOf + <1>1. DOMAIN B = S + OBVIOUS + <1>2. CASE x \notin DOMAIN B + <2>. BagRemove(B, x) = B BY <1>2 DEF BagRemove + <2>. QED BY DEF BagOf + <1>3. CASE x \in DOMAIN B /\ B[x] = 1 + <2>1. BagRemove(B, x) = [e \in DOMAIN B \ {x} |-> B[e]] + BY <1>3 DEF BagRemove + <2>2. ASSUME NEW e \in DOMAIN B \ {x} + PROVE B[e] \in Nat \ {0} + OBVIOUS + <2>3. BagRemove(B, x) \in [DOMAIN B \ {x} -> Nat \ {0}] + BY <2>1, <2>2 + <2>4. DOMAIN B \ {x} \in SUBSET Msg + BY <1>1, S \in SUBSET Msg + <2>. QED BY <2>3, <2>4 DEF BagOf + <1>4. CASE x \in DOMAIN B /\ B[x] # 1 + <2>1. BagRemove(B, x) = [e \in DOMAIN B |-> IF e=x THEN B[e]-1 ELSE B[e]] + BY <1>4 DEF BagRemove + <2>2. ASSUME NEW e \in DOMAIN B + PROVE (IF e=x THEN B[e]-1 ELSE B[e]) \in Nat \ {0} + <3>1. CASE e = x + <4>1. B[x] \in Nat \ {0} + BY <1>4 + <4>2. B[x] # 1 + BY <1>4 + <4>3. B[x] - 1 \in Nat /\ B[x] - 1 # 0 + BY <4>1, <4>2 + <4>. QED BY <3>1, <4>3 + <3>2. CASE e # x + <4>1. B[e] \in Nat \ {0} OBVIOUS + <4>. QED BY <3>2, <4>1 + <3>. QED BY <3>1, <3>2 + <2>3. BagRemove(B, x) \in [DOMAIN B -> Nat \ {0}] + BY <2>1, <2>2 + <2>. QED BY <2>3, <1>1, S \in SUBSET Msg DEF BagOf + <1>. QED BY <1>2, <1>3, <1>4 + +(***************************************************************************) +(* Helper: a "pl" message is in Msg. *) +(***************************************************************************) +LEMMA PlMsgInMsg == [type |-> "pl"] \in Msg + BY DEF Msg, PMsg + +(***************************************************************************) +(* Helper: a "pl" message and a "tok" message are distinct (their `type` *) +(* fields differ). *) +(***************************************************************************) +LEMMA PlMsgIsNotTok == ~ ([type |-> "pl"].type = "tok") + OBVIOUS + +(***************************************************************************) +(* Helper: the "new token" produced by a PassToken/InitiateProbe step is *) +(* in Msg whenever its q-field is in Int and color-field is in ColorSet. *) +(***************************************************************************) +LEMMA NewTokInMsg == + ASSUME NEW q \in Int, NEW c \in ColorSet + PROVE [type |-> "tok", q |-> q, color |-> c] \in Msg + BY DEF Msg, TMsg + +(***************************************************************************) +(* Helper: BagAdd of a non-tok message x to a bag B: *) +(* (a) preserves token presence: any tok in DOMAIN B remains in *) +(* DOMAIN BagAdd(B,x) with the same multiplicity; *) +(* (b) does not introduce new toks: any tok in DOMAIN BagAdd(B,x) *) +(* was already in DOMAIN B (since x has type # "tok"). *) +(***************************************************************************) +LEMMA BagAddPreservesToks == + ASSUME NEW B, NEW x, x.type # "tok" + PROVE /\ \A t : t.type = "tok" /\ t \in DOMAIN B + => /\ t \in DOMAIN BagAdd(B, x) + /\ BagAdd(B, x)[t] = B[t] + /\ \A t : t.type = "tok" /\ t \in DOMAIN BagAdd(B, x) + => t \in DOMAIN B + <1>1. CASE x \in DOMAIN B + <2>1. BagAdd(B, x) = [e \in DOMAIN B |-> IF e = x THEN B[e] + 1 ELSE B[e]] + BY <1>1 DEF BagAdd + <2>2. DOMAIN BagAdd(B, x) = DOMAIN B + BY <2>1 + <2>3. ASSUME NEW t, t.type = "tok", t \in DOMAIN B + PROVE /\ t \in DOMAIN BagAdd(B, x) + /\ BagAdd(B, x)[t] = B[t] + <3>. t # x BY <2>3 + <3>. QED BY <2>1, <2>2, <2>3 + <2>. QED BY <2>2, <2>3 + <1>2. CASE x \notin DOMAIN B + <2>1. BagAdd(B, x) = [e \in DOMAIN B \cup {x} |-> IF e = x THEN 1 ELSE B[e]] + BY <1>2 DEF BagAdd + <2>2. DOMAIN BagAdd(B, x) = DOMAIN B \cup {x} + BY <2>1 + <2>3. ASSUME NEW t, t.type = "tok", t \in DOMAIN B + PROVE /\ t \in DOMAIN BagAdd(B, x) + /\ BagAdd(B, x)[t] = B[t] + <3>. t # x BY <2>3 + <3>. QED BY <2>1, <2>2, <2>3 + <2>4. ASSUME NEW t, t.type = "tok", t \in DOMAIN BagAdd(B, x) + PROVE t \in DOMAIN B + <3>. t # x BY <2>4 + <3>. QED BY <2>2, <2>4 + <2>. QED BY <2>3, <2>4 + <1>. QED BY <1>1, <1>2 + +(***************************************************************************) +(* Helper: BagRemove of a non-tok message x from a bag B: *) +(* (a) preserves any tok in DOMAIN B (whether x was in B or not); *) +(* (b) does not introduce new toks. *) +(***************************************************************************) +LEMMA BagRemovePreservesToks == + ASSUME NEW B, NEW x, x.type # "tok" + PROVE /\ \A t : t.type = "tok" /\ t \in DOMAIN B + => /\ t \in DOMAIN BagRemove(B, x) + /\ BagRemove(B, x)[t] = B[t] + /\ \A t : t.type = "tok" /\ t \in DOMAIN BagRemove(B, x) + => t \in DOMAIN B + <1>1. CASE x \notin DOMAIN B + <2>. BagRemove(B, x) = B BY <1>1 DEF BagRemove + <2>. QED OBVIOUS + <1>2. CASE x \in DOMAIN B /\ B[x] = 1 + <2>1. BagRemove(B, x) = [e \in DOMAIN B \ {x} |-> B[e]] + BY <1>2 DEF BagRemove + <2>2. DOMAIN BagRemove(B, x) = DOMAIN B \ {x} + BY <2>1 + <2>3. ASSUME NEW t, t.type = "tok", t \in DOMAIN B + PROVE /\ t \in DOMAIN BagRemove(B, x) + /\ BagRemove(B, x)[t] = B[t] + <3>. t # x BY <2>3 + <3>. QED BY <2>1, <2>2, <2>3 + <2>4. ASSUME NEW t, t.type = "tok", t \in DOMAIN BagRemove(B, x) + PROVE t \in DOMAIN B + BY <2>2, <2>4 + <2>. QED BY <2>3, <2>4 + <1>3. CASE x \in DOMAIN B /\ B[x] # 1 + <2>1. BagRemove(B, x) = [e \in DOMAIN B |-> IF e = x THEN B[e] - 1 ELSE B[e]] + BY <1>3 DEF BagRemove + <2>2. DOMAIN BagRemove(B, x) = DOMAIN B + BY <2>1 + <2>3. ASSUME NEW t, t.type = "tok", t \in DOMAIN B + PROVE /\ t \in DOMAIN BagRemove(B, x) + /\ BagRemove(B, x)[t] = B[t] + <3>. t # x BY <2>3 + <3>. QED BY <2>1, <2>2, <2>3 + <2>4. ASSUME NEW t, t.type = "tok", t \in DOMAIN BagRemove(B, x) + PROVE t \in DOMAIN B + BY <2>2, <2>4 + <2>. QED BY <2>3, <2>4 + <1>. QED BY <1>1, <1>2, <1>3 + +(***************************************************************************) +(* The unique-token witness extracted from NetworkOK. *) +(***************************************************************************) +TokenAt(n) == \E t \in DOMAIN network[n] : t.type = "tok" + +(***************************************************************************) +(* Inductive step for PCalTypeOK -- per disjunct of node(self). *) +(* *) +(* Of the four conjuncts of PCalTypeOK we discharge `active`, `color`, *) +(* `counter`, and the bag-typing of `network` for all five PCal *) +(* disjuncts. The unique-token preservation in NetworkOK is OMITTED *) +(* and left for a later round. *) +(***************************************************************************) +LEMMA TypeOK_Step == + PCalTypeOK /\ [Next]_vars => PCalTypeOK' + <1>. SUFFICES ASSUME PCalTypeOK, [Next]_vars PROVE PCalTypeOK' + OBVIOUS + <1>. USE DEF PCalTypeOK, NetworkOK + <1>1. CASE UNCHANGED vars + BY <1>1 DEF vars + <1>2. (\E self \in Node : node(self)) => PCalTypeOK' + <2>. SUFFICES ASSUME NEW self \in Node, node(self) + PROVE PCalTypeOK' + OBVIOUS + <2>. USE DEF sendMsg, dropMsg, passMsg, pendingMsgs + \* Lift node(self) into the proof context as a named fact so the + \* disjunct-combine QED can reference it. + <2>NodeFact. node(self) + OBVIOUS + \* Disjunct 1: send a payload message. + <2>1. ASSUME active[self], + NEW to \in Node \ {self}, + network' = sendMsg(network, to, [type |-> "pl"]), + counter' = [counter EXCEPT ![self] = counter[self] + 1], + UNCHANGED <> + PROVE PCalTypeOK' + <3>1. active' \in [Node -> BOOLEAN] + BY <2>1 + <3>2. color' \in [Node -> ColorSet] + BY <2>1 + <3>3. counter' \in [Node -> Int] + <4>1. counter' = [counter EXCEPT ![self] = counter[self] + 1] + BY <2>1 + <4>2. counter[self] + 1 \in Int + OBVIOUS + <4>. QED BY <4>1, <4>2 + <3>4. network' \in [Node -> BagOf(Msg)] + <4>1. network[to] \in BagOf(Msg) + OBVIOUS + <4>2. BagAdd(network[to], [type |-> "pl"]) \in BagOf(Msg) + BY <4>1, BagAddOfMsg, PlMsgInMsg + <4>3. network' = [network EXCEPT ![to] = BagAdd(network[to], [type |-> "pl"])] + BY <2>1 DEF sendMsg + <4>. QED BY <4>2, <4>3 + <3>5. NetworkOK' + \* network' agrees with network except at `to`, where a "pl" msg + \* (not a tok) is added. The unique-token witness is preserved. + <4>0. PICK n0 \in Node : + \E t \in DOMAIN network[n0] : + /\ t.type = "tok" + /\ network[n0][t] = 1 + /\ \A n2 \in Node : \A t2 \in DOMAIN network[n2] : + t2.type = "tok" => (n2 = n0 /\ t2 = t) + BY DEF NetworkOK + <4>0a. PICK t0 \in DOMAIN network[n0] : + /\ t0.type = "tok" + /\ network[n0][t0] = 1 + /\ \A n2 \in Node : \A t2 \in DOMAIN network[n2] : + t2.type = "tok" => (n2 = n0 /\ t2 = t0) + BY <4>0 + <4>1. network' = [network EXCEPT ![to] = BagAdd(network[to], [type |-> "pl"])] + BY <2>1 DEF sendMsg + <4>2. [type |-> "pl"].type # "tok" + BY PlMsgIsNotTok + <4>3. \* Token at n0 with t0 is preserved in network'. + /\ t0 \in DOMAIN network'[n0] + /\ network'[n0][t0] = 1 + <5>1. CASE n0 = to + <6>1. network'[n0] = BagAdd(network[to], [type |-> "pl"]) + BY <4>1, <5>1 + <6>. QED BY <5>1, <6>1, <4>0a, <4>2, BagAddPreservesToks + <5>2. CASE n0 # to + <6>. network'[n0] = network[n0] + BY <4>1, <5>2 + <6>. QED BY <4>0a + <5>. QED BY <5>1, <5>2 + <4>4. \* No new tok is introduced. + \A n2 \in Node : \A t2 \in DOMAIN network'[n2] : + t2.type = "tok" => (n2 = n0 /\ t2 = t0) + <5>. SUFFICES ASSUME NEW n2 \in Node, + NEW t2 \in DOMAIN network'[n2], + t2.type = "tok" + PROVE n2 = n0 /\ t2 = t0 + OBVIOUS + <5>1. t2 \in DOMAIN network[n2] + <6>1. CASE n2 = to + <7>1. network'[n2] = BagAdd(network[to], [type |-> "pl"]) + BY <4>1, <6>1 + <7>2. t2 \in DOMAIN BagAdd(network[to], [type |-> "pl"]) + BY <7>1 + <7>3. t2 \in DOMAIN network[to] + BY <7>2, <4>2, BagAddPreservesToks + <7>. QED BY <6>1, <7>3 + <6>2. CASE n2 # to + <7>. network'[n2] = network[n2] + BY <4>1, <6>2 + <7>. QED + <6>. QED BY <6>1, <6>2 + <5>. QED BY <5>1, <4>0a + <4>5. \E n \in Node : \E t \in DOMAIN network'[n] : + /\ t.type = "tok" + /\ network'[n][t] = 1 + /\ \A n2 \in Node : \A t2 \in DOMAIN network'[n2] : + t2.type = "tok" => (n2 = n /\ t2 = t) + BY <4>0a, <4>3, <4>4 + <4>. QED BY <3>4, <4>5 DEF NetworkOK + <3>. QED BY <3>1, <3>2, <3>3, <3>4, <3>5 DEF PCalTypeOK + \* Disjunct 2: receive a payload message. + <2>2. ASSUME NEW msg \in pendingMsgs(network, self), + msg.type = "pl", + counter' = [counter EXCEPT ![self] = counter[self] - 1], + active' = [active EXCEPT ![self] = TRUE], + color' = [color EXCEPT ![self] = "black"], + network' = dropMsg(network, self, msg) + PROVE PCalTypeOK' + <3>1. active' \in [Node -> BOOLEAN] + BY <2>2 + <3>2. color' \in [Node -> ColorSet] + <4>1. "black" \in ColorSet BY DEF ColorSet + <4>. QED BY <2>2, <4>1 + <3>3. counter' \in [Node -> Int] + <4>1. counter' = [counter EXCEPT ![self] = counter[self] - 1] + BY <2>2 + <4>2. counter[self] - 1 \in Int + OBVIOUS + <4>. QED BY <4>1, <4>2 + <3>4. network' \in [Node -> BagOf(Msg)] + <4>1. network[self] \in BagOf(Msg) + OBVIOUS + <4>2. BagRemove(network[self], msg) \in BagOf(Msg) + BY <4>1, BagRemoveOfMsg + <4>3. network' = [network EXCEPT ![self] = BagRemove(network[self], msg)] + BY <2>2 DEF dropMsg + <4>. QED BY <4>2, <4>3 + <3>5. NetworkOK' + \* network' agrees with network except at self, where the matched + \* "pl" msg (not a tok) is removed. Token witness preserved. + <4>0. PICK n0 \in Node : + \E t \in DOMAIN network[n0] : + /\ t.type = "tok" + /\ network[n0][t] = 1 + /\ \A n2 \in Node : \A t2 \in DOMAIN network[n2] : + t2.type = "tok" => (n2 = n0 /\ t2 = t) + BY DEF NetworkOK + <4>0a. PICK t0 \in DOMAIN network[n0] : + /\ t0.type = "tok" + /\ network[n0][t0] = 1 + /\ \A n2 \in Node : \A t2 \in DOMAIN network[n2] : + t2.type = "tok" => (n2 = n0 /\ t2 = t0) + BY <4>0 + <4>1. network' = [network EXCEPT ![self] = BagRemove(network[self], msg)] + BY <2>2 DEF dropMsg + <4>2. msg.type # "tok" + BY <2>2 + <4>3. /\ t0 \in DOMAIN network'[n0] + /\ network'[n0][t0] = 1 + <5>1. CASE n0 = self + <6>1. network'[n0] = BagRemove(network[self], msg) + BY <4>1, <5>1 + <6>. QED BY <5>1, <6>1, <4>0a, <4>2, BagRemovePreservesToks + <5>2. CASE n0 # self + <6>. network'[n0] = network[n0] + BY <4>1, <5>2 + <6>. QED BY <4>0a + <5>. QED BY <5>1, <5>2 + <4>4. \A n2 \in Node : \A t2 \in DOMAIN network'[n2] : + t2.type = "tok" => (n2 = n0 /\ t2 = t0) + <5>. SUFFICES ASSUME NEW n2 \in Node, + NEW t2 \in DOMAIN network'[n2], + t2.type = "tok" + PROVE n2 = n0 /\ t2 = t0 + OBVIOUS + <5>1. t2 \in DOMAIN network[n2] + <6>1. CASE n2 = self + <7>1. network'[n2] = BagRemove(network[self], msg) + BY <4>1, <6>1 + <7>2. t2 \in DOMAIN BagRemove(network[self], msg) + BY <7>1 + <7>3. t2 \in DOMAIN network[self] + BY <7>2, <4>2, BagRemovePreservesToks + <7>. QED BY <6>1, <7>3 + <6>2. CASE n2 # self + <7>. network'[n2] = network[n2] + BY <4>1, <6>2 + <7>. QED + <6>. QED BY <6>1, <6>2 + <5>. QED BY <5>1, <4>0a + <4>5. \E n \in Node : \E t \in DOMAIN network'[n] : + /\ t.type = "tok" + /\ network'[n][t] = 1 + /\ \A n2 \in Node : \A t2 \in DOMAIN network'[n2] : + t2.type = "tok" => (n2 = n /\ t2 = t) + BY <4>0a, <4>3, <4>4 + <4>. QED BY <3>4, <4>5 DEF NetworkOK + <3>. QED BY <3>1, <3>2, <3>3, <3>4, <3>5 DEF PCalTypeOK + \* Disjunct 3: deactivate. + <2>3. ASSUME active' = [active EXCEPT ![self] = FALSE], + UNCHANGED <> + PROVE PCalTypeOK' + <3>1. active' \in [Node -> BOOLEAN] + BY <2>3 + <3>2. color' \in [Node -> ColorSet] + BY <2>3 + <3>3. counter' \in [Node -> Int] + BY <2>3 + <3>4. NetworkOK' + BY <2>3 DEF NetworkOK + <3>. QED BY <3>1, <3>2, <3>3, <3>4 DEF PCalTypeOK + \* Disjunct 4: pass the token. + <2>4. ASSUME self # Initiator, + NEW tok \in pendingMsgs(network, self), + tok.type = "tok" /\ ~active[self], + network' = passMsg(network, self, tok, self-1, [type|-> "tok", q |-> tok.q + counter[self], color |-> (IF color[self] = "black" THEN "black" ELSE tok.color)]), + color' = [color EXCEPT ![self] = "white"], + UNCHANGED <> + PROVE PCalTypeOK' + <3>. DEFINE newTok == [type |-> "tok", + q |-> tok.q + counter[self], + color |-> IF color[self] = "black" + THEN "black" ELSE tok.color] + <3>1. active' \in [Node -> BOOLEAN] + BY <2>4 + <3>2. color' \in [Node -> ColorSet] + <4>1. "white" \in ColorSet BY DEF ColorSet + <4>. QED BY <2>4, <4>1 + <3>3. counter' \in [Node -> Int] + BY <2>4 + <3>. self - 1 \in Node + <4>1. self \in Node /\ self # Initiator + BY <2>4 + <4>2. self \in 0..N-1 /\ self # 0 + BY <4>1, InitiatorIsZero DEF Node + <4>. QED BY <4>2 DEF Node + <3>. tok \in DOMAIN network[self] + BY <2>4 DEF pendingMsgs + <3>. tok \in Msg + <4>1. network[self] \in BagOf(Msg) OBVIOUS + <4>2. PICK S \in SUBSET Msg : network[self] \in [S -> Nat \ {0}] + BY <4>1 DEF BagOf + <4>3. DOMAIN network[self] = S + BY <4>2 + <4>. QED BY <4>3, S \in SUBSET Msg, tok \in DOMAIN network[self] + <3>. tok \in TMsg + <4>1. tok \in Msg /\ tok.type = "tok" + BY <2>4 + <4>2. tok \notin PMsg + BY <4>1 DEF PMsg + <4>. QED BY <4>1, <4>2 DEF Msg + <3>. tok.q \in Int + BY DEF TMsg + <3>. tok.color \in ColorSet + BY DEF TMsg + <3>. counter[self] \in Int + OBVIOUS + <3>. tok.q + counter[self] \in Int + OBVIOUS + <3>. (IF color[self] = "black" THEN "black" ELSE tok.color) \in ColorSet + <4>1. "black" \in ColorSet BY DEF ColorSet + <4>. QED BY <4>1 + <3>. newTok \in Msg + BY NewTokInMsg + <3>. self \in Int /\ self - 1 \in Int /\ self - 1 # self + <4>1. self \in 0..N-1 + BY <2>4 DEF Node + <4>. QED BY <4>1 + \* The two-EXCEPT network update, with @ resolved (self # self-1): + <3>NetEq. network' = [network EXCEPT ![self] = BagRemove(network[self], tok), + ![self - 1] = BagAdd(network[self - 1], newTok)] + BY <2>4 DEF passMsg + <3>4. network' \in [Node -> BagOf(Msg)] + <4>1. network[self] \in BagOf(Msg) + OBVIOUS + <4>2. BagRemove(network[self], tok) \in BagOf(Msg) + BY <4>1, BagRemoveOfMsg + <4>3. network[self - 1] \in BagOf(Msg) + OBVIOUS + <4>4. BagAdd(network[self - 1], newTok) \in BagOf(Msg) + BY <4>3, BagAddOfMsg + <4>. QED BY <4>2, <4>4, <3>NetEq + <3>5. NetworkOK' + \* The token moves from `self` (where the unique tok was, by + \* NetworkOK uniqueness on tok \in DOMAIN network[self]) to + \* `self-1` (where a fresh `newTok` is added). + <4>0. PICK n0 \in Node : + \E t \in DOMAIN network[n0] : + /\ t.type = "tok" + /\ network[n0][t] = 1 + /\ \A n2 \in Node : \A t2 \in DOMAIN network[n2] : + t2.type = "tok" => (n2 = n0 /\ t2 = t) + BY DEF NetworkOK + <4>0a. PICK t0 \in DOMAIN network[n0] : + /\ t0.type = "tok" + /\ network[n0][t0] = 1 + /\ \A n2 \in Node : \A t2 \in DOMAIN network[n2] : + t2.type = "tok" => (n2 = n0 /\ t2 = t0) + BY <4>0 + \* `tok` is the unique token, so it equals `t0` at `self = n0`. + <4>0b. /\ n0 = self + /\ t0 = tok + BY <4>0a, <2>4 DEF pendingMsgs + <4>0c. network[self][tok] = 1 + BY <4>0a, <4>0b + \* No "tok" message in network[m] for m # self. + <4>0d. \A m \in Node \ {self} : \A t \in DOMAIN network[m] : t.type # "tok" + BY <4>0a, <4>0b + \* In particular, newTok is not in DOMAIN network[self - 1]. + <4>0e. newTok \notin DOMAIN network[self - 1] + <5>1. self - 1 # self + OBVIOUS + <5>2. self - 1 \in Node \ {self} + OBVIOUS + <5>3. \A t \in DOMAIN network[self - 1] : t.type # "tok" + BY <4>0d, <5>2 + <5>. QED BY <5>3 + \* The new tok at self-1 has multiplicity 1. + <4>1. /\ newTok \in DOMAIN network'[self - 1] + /\ network'[self - 1][newTok] = 1 + <5>1. network'[self - 1] = BagAdd(network[self - 1], newTok) + BY <3>NetEq + <5>2. BagAdd(network[self - 1], newTok) = + [e \in DOMAIN network[self - 1] \cup {newTok} |-> + IF e = newTok THEN 1 ELSE network[self - 1][e]] + BY <4>0e DEF BagAdd + <5>3. DOMAIN network'[self - 1] = DOMAIN network[self - 1] \cup {newTok} + BY <5>1, <5>2 + <5>. QED BY <5>1, <5>2, <5>3 + \* Uniqueness: any tok in network'[n] for any n must be newTok at self-1. + <4>2. \A n2 \in Node : \A t2 \in DOMAIN network'[n2] : + t2.type = "tok" => (n2 = self - 1 /\ t2 = newTok) + <5>. SUFFICES ASSUME NEW n2 \in Node, + NEW t2 \in DOMAIN network'[n2], + t2.type = "tok" + PROVE n2 = self - 1 /\ t2 = newTok + OBVIOUS + <5>1. CASE n2 = self + \* network'[self] = BagRemove(network[self], tok); tok had mult 1 + \* and was the only tok at self, so no tok remains here. + <6>1. network'[self] = BagRemove(network[self], tok) + BY <3>NetEq, <5>1 + <6>2. BagRemove(network[self], tok) = + [e \in DOMAIN network[self] \ {tok} |-> network[self][e]] + BY <4>0c DEF BagRemove + <6>3. DOMAIN network'[self] = DOMAIN network[self] \ {tok} + BY <6>1, <6>2 + <6>4. t2 \in DOMAIN network[self] \ {tok} + BY <5>1, <6>3 + \* By NetworkOK uniqueness, t2 in DOMAIN network[self] with + \* t2.type = "tok" implies t2 = tok = t0. Contradiction. + <6>5. t2 = tok + BY <4>0a, <4>0b, <5>1, <6>4 + <6>. QED BY <6>4, <6>5 + <5>2. CASE n2 = self - 1 + <6>1. network'[n2] = BagAdd(network[self - 1], newTok) + BY <3>NetEq, <5>2 + <6>2. DOMAIN network'[n2] = DOMAIN network[self - 1] \cup {newTok} + BY <4>0e, <6>1 DEF BagAdd + <6>3. CASE t2 = newTok + BY <5>2, <6>3 + <6>4. CASE t2 # newTok + <7>1. t2 \in DOMAIN network[self - 1] + BY <6>2, <6>4 + \* By NetworkOK uniqueness with t2.type = "tok" and self-1 # self, + \* this can't happen: t2 must equal tok at self. + <7>2. self - 1 \in Node \ {self} + OBVIOUS + <7>3. t2.type # "tok" + BY <4>0d, <7>1, <7>2 + <7>. QED BY <7>3 + <6>. QED BY <6>3, <6>4 + <5>3. CASE n2 # self /\ n2 # self - 1 + <6>1. network'[n2] = network[n2] + BY <3>NetEq, <5>3 + <6>2. t2 \in DOMAIN network[n2] + BY <6>1 + \* By NetworkOK, t2 must be tok at self. But n2 # self. + <6>3. n2 = self + BY <4>0a, <4>0b, <6>2 + <6>. QED BY <5>3, <6>3 + <5>. QED BY <5>1, <5>2, <5>3 + <4>3. \E n \in Node : \E t \in DOMAIN network'[n] : + /\ t.type = "tok" + /\ network'[n][t] = 1 + /\ \A n2 \in Node : \A t2 \in DOMAIN network'[n2] : + t2.type = "tok" => (n2 = n /\ t2 = t) + <5>. self - 1 \in Node OBVIOUS + <5>. newTok.type = "tok" BY DEF Msg + <5>. QED BY <4>1, <4>2 + <4>. QED BY <3>4, <4>3 DEF NetworkOK + <3>. QED BY <3>1, <3>2, <3>3, <3>4, <3>5 DEF PCalTypeOK + \* Disjunct 5: initiate the token. + <2>5. ASSUME self = Initiator, + NEW tok \in pendingMsgs(network, self), + tok.type = "tok" /\ (color[self] = "black" \/ tok.q + counter[self] # 0 \/ tok.color = "black"), + network' = passMsg(network, self, tok, N-1, [type|-> "tok", q |-> 0, color |-> "white"]), + color' = [color EXCEPT ![self] = "white"], + UNCHANGED <> + PROVE PCalTypeOK' + <3>. DEFINE newTok == [type |-> "tok", q |-> 0, color |-> "white"] + <3>1. active' \in [Node -> BOOLEAN] + BY <2>5 + <3>2. color' \in [Node -> ColorSet] + <4>1. "white" \in ColorSet BY DEF ColorSet + <4>. QED BY <2>5, <4>1 + <3>3. counter' \in [Node -> Int] + BY <2>5 + <3>. N - 1 \in Node + BY DEF Node + <3>. newTok \in Msg + <4>1. 0 \in Int OBVIOUS + <4>2. "white" \in ColorSet BY DEF ColorSet + <4>. QED BY <4>1, <4>2, NewTokInMsg + <3>4. network' \in [Node -> BagOf(Msg)] + \* The two EXCEPT keys are `self` (= 0) and `N-1`. These coincide + \* when N = 1, in which case the second EXCEPT writes over the + \* first (its @ being `BagRemove(network[self], tok)`). We handle + \* both cases uniformly via per-element typing. + <4>1. network' = [network EXCEPT ![self] = BagRemove(@, tok), + ![N-1] = BagAdd(@, newTok)] + BY <2>5 DEF passMsg + <4>2. ASSUME NEW n \in Node + PROVE network'[n] \in BagOf(Msg) + <5>. self \in Node /\ self = 0 + BY <2>5, InitiatorIsZero + <5>. N - 1 \in Node + BY DEF Node + <5>. network[self] \in BagOf(Msg) /\ network[N-1] \in BagOf(Msg) + OBVIOUS + <5>. BagRemove(network[self], tok) \in BagOf(Msg) + BY BagRemoveOfMsg + <5>. BagAdd(network[N-1], newTok) \in BagOf(Msg) + BY BagAddOfMsg + <5>. BagAdd(BagRemove(network[self], tok), newTok) \in BagOf(Msg) + BY BagRemoveOfMsg, BagAddOfMsg + <5>1. CASE self = N - 1 + \* The second EXCEPT writes at the same key with @ being the + \* result of the first EXCEPT, so it overwrites with BagAdd. + <6>1. network' = [network EXCEPT ![self] = BagAdd(BagRemove(network[self], tok), newTok)] + BY <4>1, <5>1 + <6>. QED BY <5>1, <6>1 + <5>2. CASE self # N - 1 + <6>1. network' = [network EXCEPT ![self] = BagRemove(network[self], tok), + ![N-1] = BagAdd(network[N-1], newTok)] + BY <4>1, <5>2 + <6>. QED BY <6>1, <5>2 + <5>. QED BY <5>1, <5>2 + <4>. QED BY <4>1, <4>2 + <3>5. NetworkOK' + \* The token moves from `self` (= Initiator = 0) to `N-1`. When + \* N = 1 the two EXCEPT keys collapse into a BagAdd-of-BagRemove; + \* the new unique-token witness is `(N-1, newTok)` in both cases. + <4>0. PICK n0 \in Node : + \E t \in DOMAIN network[n0] : + /\ t.type = "tok" + /\ network[n0][t] = 1 + /\ \A n2 \in Node : \A t2 \in DOMAIN network[n2] : + t2.type = "tok" => (n2 = n0 /\ t2 = t) + BY DEF NetworkOK + <4>0a. PICK t0 \in DOMAIN network[n0] : + /\ t0.type = "tok" + /\ network[n0][t0] = 1 + /\ \A n2 \in Node : \A t2 \in DOMAIN network[n2] : + t2.type = "tok" => (n2 = n0 /\ t2 = t0) + BY <4>0 + <4>0b. /\ n0 = self + /\ t0 = tok + BY <4>0a, <2>5 DEF pendingMsgs + <4>0c. network[self][tok] = 1 + BY <4>0a, <4>0b + <4>0d. \A m \in Node \ {self} : \A t \in DOMAIN network[m] : t.type # "tok" + BY <4>0a, <4>0b + <4>0e. self = 0 /\ N - 1 \in Node + BY <2>5, InitiatorIsZero DEF Node + \* For N >= 2 (self # N - 1), newTok is fresh at N-1. + \* For N = 1 (self = N - 1), newTok is added to BagRemove(network[0], tok). + <4>0f. tok # newTok \/ TRUE OBVIOUS \* (just to flag tok and newTok are unrelated for type purposes) + <4>1. /\ newTok \in DOMAIN network'[N-1] + /\ network'[N-1][newTok] = 1 + <5>1. CASE self # N - 1 + <6>1. network' = [network EXCEPT ![self] = BagRemove(network[self], tok), + ![N-1] = BagAdd(network[N-1], newTok)] + BY <2>5, <5>1 DEF passMsg + <6>2. network'[N-1] = BagAdd(network[N-1], newTok) + BY <6>1, <5>1 + <6>3. newTok \notin DOMAIN network[N-1] + <7>1. N - 1 \in Node \ {self} + BY <4>0e, <5>1 + <7>2. \A t \in DOMAIN network[N-1] : t.type # "tok" + BY <4>0d, <7>1 + <7>3. newTok.type = "tok" + BY DEF Msg + <7>. QED BY <7>2, <7>3 + <6>4. BagAdd(network[N-1], newTok) = + [e \in DOMAIN network[N-1] \cup {newTok} |-> + IF e = newTok THEN 1 ELSE network[N-1][e]] + BY <6>3 DEF BagAdd + <6>. QED BY <6>2, <6>4 + <5>2. CASE self = N - 1 + <6>1. network' = [network EXCEPT ![self] = BagAdd(BagRemove(network[self], tok), newTok)] + BY <2>5, <5>2 DEF passMsg + <6>2. network'[N-1] = BagAdd(BagRemove(network[self], tok), newTok) + BY <6>1, <5>2 + <6>3. BagRemove(network[self], tok) = + [e \in DOMAIN network[self] \ {tok} |-> network[self][e]] + BY <4>0c DEF BagRemove + <6>4. DOMAIN BagRemove(network[self], tok) = DOMAIN network[self] \ {tok} + BY <6>3 + <6>5. newTok \notin DOMAIN BagRemove(network[self], tok) + \* If newTok were in DOMAIN BagRemove(network[self], tok), + \* it would be in DOMAIN network[self] \ {tok} -- so newTok + \* is in DOMAIN network[self] *and* newTok # tok. Then by + \* NetworkOK uniqueness (every "tok" in DOMAIN network[self] + \* equals tok = t0), newTok = tok. Contradiction. + <7>2. \A e \in DOMAIN network[self] : + e.type = "tok" => e = tok + BY <4>0a, <4>0b, <2>5 DEF pendingMsgs + <7>3. ASSUME newTok \in DOMAIN BagRemove(network[self], tok) + PROVE FALSE + <8>1. newTok \in DOMAIN network[self] \ {tok} + BY <6>4, <7>3 + <8>2. newTok \in DOMAIN network[self] /\ newTok # tok + BY <8>1 + <8>3. newTok.type = "tok" + BY DEF Msg + <8>4. newTok = tok + BY <7>2, <8>2, <8>3 + <8>. QED BY <8>2, <8>4 + <7>. QED BY <7>3 + <6>6. BagAdd(BagRemove(network[self], tok), newTok) = + [e \in DOMAIN BagRemove(network[self], tok) \cup {newTok} |-> + IF e = newTok THEN 1 ELSE BagRemove(network[self], tok)[e]] + BY <6>5 DEF BagAdd + <6>. QED BY <6>2, <6>6 + <5>. QED BY <5>1, <5>2 + <4>2. \A n2 \in Node : \A t2 \in DOMAIN network'[n2] : + t2.type = "tok" => (n2 = N - 1 /\ t2 = newTok) + <5>. SUFFICES ASSUME NEW n2 \in Node, + NEW t2 \in DOMAIN network'[n2], + t2.type = "tok" + PROVE n2 = N - 1 /\ t2 = newTok + OBVIOUS + <5>1. CASE self # N - 1 + <6>1. network' = [network EXCEPT ![self] = BagRemove(network[self], tok), + ![N-1] = BagAdd(network[N-1], newTok)] + BY <2>5, <5>1 DEF passMsg + <6>2. CASE n2 = self + \* network'[self] = BagRemove(network[self], tok); tok had mult 1. + <7>1. network'[n2] = BagRemove(network[self], tok) + BY <6>1, <5>1, <6>2 + <7>2. BagRemove(network[self], tok) = + [e \in DOMAIN network[self] \ {tok} |-> network[self][e]] + BY <4>0c DEF BagRemove + <7>3. DOMAIN network'[n2] = DOMAIN network[self] \ {tok} + BY <7>1, <7>2 + <7>4. t2 \in DOMAIN network[self] \ {tok} + BY <6>2, <7>3 + <7>5. t2 = tok + BY <4>0a, <4>0b, <6>2, <7>4 + <7>. QED BY <7>4, <7>5 + <6>3. CASE n2 = N - 1 + <7>1. network'[n2] = BagAdd(network[N-1], newTok) + BY <6>1, <5>1, <6>3 + <7>2. newTok \notin DOMAIN network[N-1] + <8>1. N - 1 \in Node \ {self} + BY <4>0e, <5>1 + <8>2. \A t \in DOMAIN network[N-1] : t.type # "tok" + BY <4>0d, <8>1 + <8>3. newTok.type = "tok" + BY DEF Msg + <8>. QED BY <8>2, <8>3 + <7>3. BagAdd(network[N-1], newTok) = + [e \in DOMAIN network[N-1] \cup {newTok} |-> + IF e = newTok THEN 1 ELSE network[N-1][e]] + BY <7>2 DEF BagAdd + <7>4. DOMAIN network'[n2] = DOMAIN network[N-1] \cup {newTok} + BY <7>1, <7>3 + <7>5. CASE t2 = newTok + BY <6>3, <7>5 + <7>6. CASE t2 # newTok + <8>1. t2 \in DOMAIN network[N-1] + BY <7>4, <7>6 + <8>2. N - 1 \in Node \ {self} + BY <4>0e, <5>1 + <8>3. t2.type # "tok" + BY <4>0d, <8>1, <8>2 + <8>. QED BY <8>3 + <7>. QED BY <7>5, <7>6 + <6>4. CASE n2 # self /\ n2 # N - 1 + <7>1. network'[n2] = network[n2] + BY <6>1, <6>4 + <7>2. t2 \in DOMAIN network[n2] + BY <7>1 + <7>3. n2 = self + BY <4>0a, <4>0b, <7>2 + <7>. QED BY <6>4, <7>3 + <6>. QED BY <6>2, <6>3, <6>4 + <5>2. CASE self = N - 1 + <6>1. network' = [network EXCEPT ![self] = BagAdd(BagRemove(network[self], tok), newTok)] + BY <2>5, <5>2 DEF passMsg + <6>2. CASE n2 = self + <7>1. network'[n2] = BagAdd(BagRemove(network[self], tok), newTok) + BY <6>1, <6>2 + \* newTok \notin DOMAIN BagRemove(network[self], tok); see <4>1's <5>2 case. + <7>2. BagRemove(network[self], tok) = + [e \in DOMAIN network[self] \ {tok} |-> network[self][e]] + BY <4>0c DEF BagRemove + <7>3. DOMAIN BagRemove(network[self], tok) = DOMAIN network[self] \ {tok} + BY <7>2 + <7>4. \A e \in DOMAIN network[self] : e.type = "tok" => e = tok + BY <4>0a, <4>0b, <2>5 DEF pendingMsgs + <7>5. newTok \notin DOMAIN BagRemove(network[self], tok) + <8>1. ASSUME newTok \in DOMAIN BagRemove(network[self], tok) + PROVE FALSE + <9>1. newTok \in DOMAIN network[self] \ {tok} + BY <7>3, <8>1 + <9>2. newTok \in DOMAIN network[self] + BY <9>1 + <9>3. newTok.type = "tok" + BY DEF Msg + <9>4. newTok = tok + BY <7>4, <9>2, <9>3 + <9>5. newTok # tok + BY <9>1 + <9>. QED BY <9>4, <9>5 + <8>. QED BY <8>1 + <7>6. BagAdd(BagRemove(network[self], tok), newTok) = + [e \in DOMAIN BagRemove(network[self], tok) \cup {newTok} |-> + IF e = newTok THEN 1 ELSE BagRemove(network[self], tok)[e]] + BY <7>5 DEF BagAdd + <7>7. DOMAIN network'[n2] = (DOMAIN network[self] \ {tok}) \cup {newTok} + BY <7>1, <7>3, <7>6 + <7>8. CASE t2 = newTok + BY <5>2, <6>2, <7>8 + <7>9. CASE t2 # newTok + <8>1. t2 \in DOMAIN network[self] \ {tok} + BY <6>2, <7>7, <7>9 + <8>2. t2 \in DOMAIN network[self] + BY <8>1 + <8>3. t2 = tok + BY <7>4, <8>2 + <8>. QED BY <8>1, <8>3 + <7>. QED BY <7>8, <7>9 + <6>3. CASE n2 # self + \* network'[n2] = network[n2] for n2 # self + <7>1. network'[n2] = network[n2] + BY <6>1, <6>3 + <7>2. t2 \in DOMAIN network[n2] + BY <7>1 + <7>3. n2 = self + BY <4>0a, <4>0b, <7>2 + <7>. QED BY <6>3, <7>3 + <6>. QED BY <6>2, <6>3 + <5>. QED BY <5>1, <5>2 + <4>3. \E n \in Node : \E t \in DOMAIN network'[n] : + /\ t.type = "tok" + /\ network'[n][t] = 1 + /\ \A n2 \in Node : \A t2 \in DOMAIN network'[n2] : + t2.type = "tok" => (n2 = n /\ t2 = t) + <5>. N - 1 \in Node BY DEF Node + <5>. newTok.type = "tok" BY DEF Msg + <5>. QED BY <4>1, <4>2 + <4>. QED BY <3>4, <4>3 DEF NetworkOK + <3>. QED BY <3>1, <3>2, <3>3, <3>4, <3>5 DEF PCalTypeOK + \* Combine the per-disjunct cases. Each CASE matches one disjunct of + \* `node(self)` exactly and reduces (via PICK on the existential + \* witness) to the corresponding `<2>i.` per-disjunct lemma above. + \* The five CASEs together cover `node(self)`; the QED uses `node(self)` + \* (in scope from <1>2's ASSUME) to dispatch to one of them. + <2>6. CASE /\ active[self] + /\ \E to \in Node \ {self}: + network' = sendMsg(network, to, [type|-> "pl"]) + /\ counter' = [counter EXCEPT ![self] = counter[self] + 1] + /\ UNCHANGED <> + <3>1. PICK to \in Node \ {self} : + network' = sendMsg(network, to, [type|-> "pl"]) + BY <2>6 + <3>. QED BY <2>1, <2>6, <3>1 + <2>7. CASE /\ \E msg \in pendingMsgs(network, self): + /\ msg.type = "pl" + /\ counter' = [counter EXCEPT ![self] = counter[self] - 1] + /\ active' = [active EXCEPT ![self] = TRUE] + /\ color' = [color EXCEPT ![self] = "black"] + /\ network' = dropMsg(network, self, msg) + <3>1. PICK msg \in pendingMsgs(network, self) : + /\ msg.type = "pl" + /\ counter' = [counter EXCEPT ![self] = counter[self] - 1] + /\ active' = [active EXCEPT ![self] = TRUE] + /\ color' = [color EXCEPT ![self] = "black"] + /\ network' = dropMsg(network, self, msg) + BY <2>7 + <3>. QED BY <2>2, <3>1 + <2>8. CASE /\ active' = [active EXCEPT ![self] = FALSE] + /\ UNCHANGED <> + BY <2>3, <2>8 + <2>9. CASE /\ self # Initiator + /\ \E tok \in pendingMsgs(network, self): + /\ tok.type = "tok" /\ ~active[self] + /\ network' = passMsg(network, self, tok, self-1, [type|-> "tok", q |-> tok.q + counter[self], color |-> (IF color[self] = "black" THEN "black" ELSE tok.color)]) + /\ color' = [color EXCEPT ![self] = "white"] + /\ UNCHANGED <> + <3>1. PICK tok \in pendingMsgs(network, self) : + /\ tok.type = "tok" /\ ~active[self] + /\ network' = passMsg(network, self, tok, self-1, [type|-> "tok", q |-> tok.q + counter[self], color |-> (IF color[self] = "black" THEN "black" ELSE tok.color)]) + /\ color' = [color EXCEPT ![self] = "white"] + BY <2>9 + <3>. QED BY <2>4, <2>9, <3>1 + <2>10. CASE /\ self = Initiator + /\ \E tok \in pendingMsgs(network, self): + /\ tok.type = "tok" /\ (color[self] = "black" \/ tok.q + counter[self] # 0 \/ tok.color = "black") + /\ network' = passMsg(network, self, tok, N-1, [type|-> "tok", q |-> 0, color |-> "white"]) + /\ color' = [color EXCEPT ![self] = "white"] + /\ UNCHANGED <> + <3>1. PICK tok \in pendingMsgs(network, self) : + /\ tok.type = "tok" /\ (color[self] = "black" \/ tok.q + counter[self] # 0 \/ tok.color = "black") + /\ network' = passMsg(network, self, tok, N-1, [type|-> "tok", q |-> 0, color |-> "white"]) + /\ color' = [color EXCEPT ![self] = "white"] + BY <2>10 + <3>. QED BY <2>5, <2>10, <3>1 + \* Final case combination: explicit case-by-case dispatch. + <2>. QED + <3>1. CASE /\ active[self] + /\ \E to \in Node \ {self}: + network' = sendMsg(network, to, [type|-> "pl"]) + /\ counter' = [counter EXCEPT ![self] = counter[self] + 1] + /\ UNCHANGED <> + BY <2>6, <3>1 + <3>2. CASE /\ \E msg \in pendingMsgs(network, self): + /\ msg.type = "pl" + /\ counter' = [counter EXCEPT ![self] = counter[self] - 1] + /\ active' = [active EXCEPT ![self] = TRUE] + /\ color' = [color EXCEPT ![self] = "black"] + /\ network' = dropMsg(network, self, msg) + BY <2>7, <3>2 + <3>3. CASE /\ active' = [active EXCEPT ![self] = FALSE] + /\ UNCHANGED <> + BY <2>8, <3>3 + <3>4. CASE /\ self # Initiator + /\ \E tok \in pendingMsgs(network, self): + /\ tok.type = "tok" /\ ~active[self] + /\ network' = passMsg(network, self, tok, self-1, [type|-> "tok", q |-> tok.q + counter[self], color |-> (IF color[self] = "black" THEN "black" ELSE tok.color)]) + /\ color' = [color EXCEPT ![self] = "white"] + /\ UNCHANGED <> + BY <2>9, <3>4 + <3>5. CASE /\ self = Initiator + /\ \E tok \in pendingMsgs(network, self): + /\ tok.type = "tok" /\ (color[self] = "black" \/ tok.q + counter[self] # 0 \/ tok.color = "black") + /\ network' = passMsg(network, self, tok, N-1, [type|-> "tok", q |-> 0, color |-> "white"]) + /\ color' = [color EXCEPT ![self] = "white"] + /\ UNCHANGED <> + BY <2>10, <3>5 + <3>. QED BY <2>NodeFact, <3>1, <3>2, <3>3, <3>4, <3>5 DEF node + <1>. QED BY <1>1, <1>2 DEF Next + +THEOREM TypeCorrect == Spec => []PCalTypeOK + <1>1. Init => PCalTypeOK + BY InitTypeOK + <1>. QED BY <1>1, TypeOK_Step, PTL DEF Spec + +(***************************************************************************) +(* Bag-level helpers for the step-refinement (`Refinement` theorem below).*) +(* *) +(* Each is about how the spec's `pending` operator (which counts *) +(* [type|->"pl"] occurrences in `network[n]`) changes under *) +(* BagAdd/BagRemove of payload or token messages. These are the *) +(* missing primitives the per-disjunct step-simulation needs. *) +(***************************************************************************) + +\* The "pl" multiplicity in a single bag (== pending[n] for B = network[n]). +PlCount(B) == IF [type |-> "pl"] \in DOMAIN B THEN B[[type |-> "pl"]] ELSE 0 + +LEMMA PendingIsPlCount == + pending = [n \in Node |-> PlCount(network[n])] + BY DEF pending, PlCount + +\* BagAdd of a "pl" message increments PlCount by 1. +LEMMA BagAdd_pl_increments == + ASSUME NEW B + PROVE PlCount(BagAdd(B, [type |-> "pl"])) = PlCount(B) + 1 + <1>1. CASE [type |-> "pl"] \in DOMAIN B + <2>1. BagAdd(B, [type |-> "pl"]) = + [e \in DOMAIN B |-> IF e = [type |-> "pl"] THEN B[e] + 1 ELSE B[e]] + BY <1>1 DEF BagAdd + <2>2. DOMAIN BagAdd(B, [type |-> "pl"]) = DOMAIN B + BY <2>1 + <2>3. BagAdd(B, [type |-> "pl"])[[type |-> "pl"]] = B[[type |-> "pl"]] + 1 + BY <2>1, <1>1 + <2>4. PlCount(B) = B[[type |-> "pl"]] + BY <1>1 DEF PlCount + <2>. QED BY <1>1, <2>2, <2>3, <2>4 DEF PlCount + <1>2. CASE [type |-> "pl"] \notin DOMAIN B + <2>1. BagAdd(B, [type |-> "pl"]) = + [e \in DOMAIN B \cup {[type |-> "pl"]} |-> + IF e = [type |-> "pl"] THEN 1 ELSE B[e]] + BY <1>2 DEF BagAdd + <2>2. [type |-> "pl"] \in DOMAIN BagAdd(B, [type |-> "pl"]) + BY <2>1 + <2>3. BagAdd(B, [type |-> "pl"])[[type |-> "pl"]] = 1 + BY <2>1 + <2>4. PlCount(B) = 0 + BY <1>2 DEF PlCount + <2>. QED BY <1>2, <2>2, <2>3, <2>4 DEF PlCount + <1>. QED BY <1>1, <1>2 + +\* BagRemove of a "pl" message decrements PlCount by 1, when "pl" is present. +LEMMA BagRemove_pl_decrements == + ASSUME NEW B, [type |-> "pl"] \in DOMAIN B, + B[[type |-> "pl"]] \in Nat \ {0} + PROVE PlCount(BagRemove(B, [type |-> "pl"])) = PlCount(B) - 1 + <1>. DEFINE pl == [type |-> "pl"] + <1>1. CASE B[pl] = 1 + <2>1. BagRemove(B, pl) = [e \in DOMAIN B \ {pl} |-> B[e]] + BY <1>1 DEF BagRemove + <2>2. pl \notin DOMAIN BagRemove(B, pl) + BY <2>1 + <2>3. PlCount(BagRemove(B, pl)) = 0 + BY <2>2 DEF PlCount + <2>4. PlCount(B) = 1 + BY <1>1 DEF PlCount + <2>. QED BY <2>3, <2>4 + <1>2. CASE B[pl] # 1 + <2>1. BagRemove(B, pl) = [e \in DOMAIN B |-> IF e = pl THEN B[e] - 1 ELSE B[e]] + BY <1>2 DEF BagRemove + <2>2. pl \in DOMAIN BagRemove(B, pl) + BY <2>1 + <2>3. BagRemove(B, pl)[pl] = B[pl] - 1 + BY <2>1 + <2>4. PlCount(B) = B[pl] + BY DEF PlCount + <2>. QED BY <2>2, <2>3, <2>4 DEF PlCount + <1>. QED BY <1>1, <1>2 + +\* BagAdd of a token message preserves PlCount (since "tok" != "pl"). +LEMMA BagAdd_tok_preserves_pl == + ASSUME NEW B, NEW t, t.type = "tok" + PROVE PlCount(BagAdd(B, t)) = PlCount(B) + <1>. DEFINE pl == [type |-> "pl"] + <1>0. pl # t BY DEF Msg + <1>1. CASE t \in DOMAIN B + <2>1. BagAdd(B, t) = [e \in DOMAIN B |-> IF e = t THEN B[e] + 1 ELSE B[e]] + BY <1>1 DEF BagAdd + <2>2. DOMAIN BagAdd(B, t) = DOMAIN B + BY <2>1 + <2>3. ASSUME pl \in DOMAIN B PROVE BagAdd(B, t)[pl] = B[pl] + BY <2>1, <1>0, <2>3 + <2>. QED BY <2>2, <2>3 DEF PlCount + <1>2. CASE t \notin DOMAIN B + <2>1. BagAdd(B, t) = [e \in DOMAIN B \cup {t} |-> IF e = t THEN 1 ELSE B[e]] + BY <1>2 DEF BagAdd + <2>2. pl \in DOMAIN BagAdd(B, t) <=> pl \in DOMAIN B + BY <2>1, <1>0 + <2>3. ASSUME pl \in DOMAIN B PROVE BagAdd(B, t)[pl] = B[pl] + BY <2>1, <1>0, <2>3 + <2>. QED BY <2>2, <2>3 DEF PlCount + <1>. QED BY <1>1, <1>2 + +\* BagRemove of a token message preserves PlCount. +LEMMA BagRemove_tok_preserves_pl == + ASSUME NEW B, NEW t, t.type = "tok" + PROVE PlCount(BagRemove(B, t)) = PlCount(B) + <1>. DEFINE pl == [type |-> "pl"] + <1>0. pl # t BY DEF Msg + <1>1. CASE t \notin DOMAIN B + <2>. BagRemove(B, t) = B BY <1>1 DEF BagRemove + <2>. QED OBVIOUS + <1>2. CASE t \in DOMAIN B /\ B[t] = 1 + <2>1. BagRemove(B, t) = [e \in DOMAIN B \ {t} |-> B[e]] + BY <1>2 DEF BagRemove + <2>2. pl \in DOMAIN BagRemove(B, t) <=> pl \in DOMAIN B + BY <2>1, <1>0 + <2>3. ASSUME pl \in DOMAIN B PROVE BagRemove(B, t)[pl] = B[pl] + BY <2>1, <1>0, <2>3 + <2>. QED BY <2>2, <2>3 DEF PlCount + <1>3. CASE t \in DOMAIN B /\ B[t] # 1 + <2>1. BagRemove(B, t) = [e \in DOMAIN B |-> IF e = t THEN B[e] - 1 ELSE B[e]] + BY <1>3 DEF BagRemove + <2>2. DOMAIN BagRemove(B, t) = DOMAIN B + BY <2>1 + <2>3. ASSUME pl \in DOMAIN B PROVE BagRemove(B, t)[pl] = B[pl] + BY <2>1, <1>0, <2>3 + <2>. QED BY <2>2, <2>3 DEF PlCount + <1>. QED BY <1>1, <1>2, <1>3 + +(***************************************************************************) +(* Refinement theorem (Spec => EWD998Spec). *) +(* *) +(* The proof has the standard shape: *) +(* <1>1. Init => EWD998!Init -- via InitRefinement *) +(* <1>2. step refinement -- per-disjunct analysis *) +(* <1>. QED by combining the temporal pieces. *) +(* *) +(* For the step refinement, each PCal disjunct of `node(self)` implements *) +(* one of EWD998's actions under the refinement mapping for `pending` and *) +(* `token`: *) +(* *) +(* PCal disjunct 1 (send pl) -> EWD998!SendMsg(self) *) +(* PCal disjunct 2 (recv pl) -> EWD998!RecvMsg(self) *) +(* PCal disjunct 3 (deactivate) -> EWD998!Deactivate(self) or stutter *) +(* PCal disjunct 4 (pass tok) -> EWD998!PassToken(self) *) +(* PCal disjunct 5 (init tok) -> EWD998!InitiateProbe *) +(* *) +(* The hardest case is disjunct 5 (InitiateProbe), where PCal's trigger *) +(* condition (`tok.q + counter[Initiator] # 0`) is weaker than EWD998's *) +(* (`> 0`). Bridging this gap requires Safra's P0 invariant transferred *) +(* to PCal: `B = Sum(counter, Node)` where B is the total count of "pl" *) +(* messages in the network. The other disjuncts only need bag-level *) +(* reasoning about how `pending` and `token` change under the spec's *) +(* BagAdd/BagRemove updates. *) +(* *) +(* This stub remains OMITTED -- the per-disjunct step-simulation requires *) +(* substantial bag-level lemmas that are out of scope for this round. *) +(***************************************************************************) +THEOREM Refinement == Spec => EWD998Spec +OMITTED + +============================================================================= diff --git a/specifications/transaction_commit/PaxosCommit_proof.tla b/specifications/transaction_commit/PaxosCommit_proof.tla new file mode 100644 index 00000000..690675d2 --- /dev/null +++ b/specifications/transaction_commit/PaxosCommit_proof.tla @@ -0,0 +1,357 @@ +------------------------- MODULE PaxosCommit_proof ------------------------- +(***************************************************************************) +(* TLAPS proof of *) +(* THEOREM PCSpec => []PCTypeOK *) +(* stated (as a non-temporal version) in PaxosCommit.tla. *) +(* *) +(* The inductive strengthening follows the template of the Paxos *) +(* consensus proof in tlapm/examples/paxos/Paxos.tla. Beyond PCTypeOK *) +(* itself we maintain *) +(* *) +(* AccInv: for every acceptor state, val = "none" iff bal = -1 *) +(* (analogue of the first conjunct of AccInv in the Paxos *) +(* proof, with None --> "none" and Values --> {"prepared", *) +(* "aborted"}), *) +(* *) +(* MsgInv1b: every "phase1b" message m with m.bal # -1 has *) +(* m.val \in {"prepared", "aborted"} *) +(* (the projection onto Paxos Commit of the first disjunct of *) +(* MsgInv for "1b" messages in the Paxos proof). *) +(* *) +(* MsgInv1b is the auxiliary fact alluded to in the original comment of *) +(* this module: it is what is needed to discharge type-correctness for *) +(* Phase2a, namely that the value the leader picks for the new "phase2a" *) +(* message lies in {"prepared", "aborted"}. *) +(* *) +(* We additionally carry IsFiniteSet(msgs) so that the Maximum operator *) +(* used in Phase2a behaves as expected on the finite set of phase 1b *) +(* ballot numbers. *) +(***************************************************************************) +EXTENDS PaxosCommit, FiniteSets, FiniteSetTheorems, TLAPS + +vars == <> + +AccInv == + \A rm \in RM, ac \in Acceptor : + aState[rm][ac].val = "none" <=> aState[rm][ac].bal = -1 + +MsgInv1b == + \A m \in msgs : + (m.type = "phase1b" /\ m.bal # -1) => m.val \in {"prepared", "aborted"} + +Inv == PCTypeOK /\ AccInv /\ MsgInv1b /\ IsFiniteSet(msgs) + +(***************************************************************************) +(* The following lemma states the standard fact that for a non-empty *) +(* finite set of integers, Maximum returns an element of the set that is *) +(* an upper bound. Its proof proceeds by structural induction over the *) +(* recursive definition of Maximum (see PaxosCommit.tla) using *) +(* FS_Induction. We leave the technical induction step as OMITTED; this *) +(* is the only piece of arithmetic content used in the proof below. *) +(***************************************************************************) +LEMMA MaximumProp == + ASSUME NEW S, IsFiniteSet(S), S \subseteq Int, S # {} + PROVE /\ Maximum(S) \in S + /\ \A n \in S : n =< Maximum(S) +PROOF OMITTED + +(***************************************************************************) +(* Auxiliary fact used in the Phase2a case: any majority is non-empty, *) +(* since by PaxosCommitAssumptions any two majorities have non-empty *) +(* intersection (in particular MS \cap MS = MS). *) +(***************************************************************************) +LEMMA MajorityNonEmpty == \A MS \in Majority : MS # {} +BY PaxosCommitAssumptions + +(***************************************************************************) +(* Initiation: the inductive invariant holds in the initial state. *) +(***************************************************************************) +LEMMA InitInv == PCInit => Inv +<1> SUFFICES ASSUME PCInit + PROVE Inv + OBVIOUS +<1> USE PaxosCommitAssumptions +<1> USE DEF PCInit, Inv, PCTypeOK, AccInv, MsgInv1b +<1>1. PCTypeOK + OBVIOUS +<1>2. AccInv + OBVIOUS +<1>3. MsgInv1b + OBVIOUS +<1>4. IsFiniteSet(msgs) + BY FS_EmptySet +<1>. QED BY <1>1, <1>2, <1>3, <1>4 + +(***************************************************************************) +(* Consecution: the inductive invariant is preserved by every step of the *) +(* next-state relation (and trivially by stuttering steps). *) +(***************************************************************************) +LEMMA NextInv == Inv /\ [PCNext]_vars => Inv' +<1> SUFFICES ASSUME Inv, [PCNext]_vars + PROVE Inv' + OBVIOUS +<1> USE PaxosCommitAssumptions +<1> USE DEF Inv, PCTypeOK, AccInv, MsgInv1b, vars, Send, Message + +<1>1. ASSUME NEW rm \in RM, RMPrepare(rm) + PROVE Inv' + BY <1>1, FS_AddElement DEF RMPrepare + +<1>2. ASSUME NEW rm \in RM, RMChooseToAbort(rm) + PROVE Inv' + BY <1>2, FS_AddElement DEF RMChooseToAbort + +<1>3. ASSUME NEW rm \in RM, RMRcvCommitMsg(rm) + PROVE Inv' + BY <1>3 DEF RMRcvCommitMsg + +<1>4. ASSUME NEW rm \in RM, RMRcvAbortMsg(rm) + PROVE Inv' + BY <1>4 DEF RMRcvAbortMsg + +<1>5. ASSUME NEW b \in Ballot \ {0}, NEW rm \in RM, Phase1a(b, rm) + PROVE Inv' + BY <1>5, FS_AddElement DEF Phase1a + +<1>6. ASSUME NEW b \in Ballot \ {0}, NEW rm \in RM, Phase2a(b, rm) + PROVE Inv' + <2>1. PICK MS \in Majority : + LET mset == {m \in msgs : /\ m.type = "phase1b" + /\ m.ins = rm + /\ m.mbal = b + /\ m.acc \in MS} + maxbal == Maximum({m.bal : m \in mset}) + val == IF maxbal = -1 + THEN "aborted" + ELSE (CHOOSE m \in mset : m.bal = maxbal).val + IN /\ \A ac \in MS : \E m \in mset : m.acc = ac + /\ Send([type |-> "phase2a", ins |-> rm, + bal |-> b, val |-> val]) + BY <1>6, Zenon DEF Phase2a + <2> DEFINE mset == {m \in msgs : /\ m.type = "phase1b" + /\ m.ins = rm + /\ m.mbal = b + /\ m.acc \in MS} + bset == {m.bal : m \in mset} + maxbal == Maximum(bset) + val == IF maxbal = -1 + THEN "aborted" + ELSE (CHOOSE m \in mset : m.bal = maxbal).val + nm == [type |-> "phase2a", ins |-> rm, + bal |-> b, val |-> val] + <2>2. UNCHANGED <> /\ msgs' = msgs \cup {nm} + BY <1>6, <2>1 DEF Phase2a + <2>3. mset \subseteq msgs + OBVIOUS + <2>4. IsFiniteSet(mset) + BY <2>3, FS_Subset + <2>5. bset \subseteq Int + BY DEF Message + <2>6. IsFiniteSet(bset) + BY <2>4, FS_Image + <2>7. MS # {} + BY MajorityNonEmpty + <2>8. mset # {} + <3>1. PICK ac \in MS : TRUE + BY <2>7 + <3>2. \E m \in mset : m.acc = ac + BY <2>1, <3>1 + <3>. QED BY <3>2 + <2>9. bset # {} + BY <2>8 + <2>10. val \in {"prepared", "aborted"} + <3>1. CASE maxbal = -1 + BY <3>1 + <3>2. CASE maxbal # -1 + <4>1. maxbal \in bset + BY <2>5, <2>6, <2>9, MaximumProp + <4>2. PICK m0 \in mset : m0.bal = maxbal + BY <4>1 + <4>3. m0.type = "phase1b" /\ m0.bal # -1 + BY <3>2, <4>2 + <4>4. m0.val \in {"prepared", "aborted"} + BY <4>2, <4>3 + <4>5. \A m \in mset : m.bal = maxbal => m.val \in {"prepared", "aborted"} + BY <3>2 DEF Message + <4>6. \E m \in mset : m.bal = maxbal + BY <4>2 + <4>7. (CHOOSE m \in mset : m.bal = maxbal) \in mset + /\ (CHOOSE m \in mset : m.bal = maxbal).bal = maxbal + BY <4>6 + <4>. QED BY <3>2, <4>5, <4>7 + <3>. QED BY <3>1, <3>2 + <2>11. nm \in Message + BY <2>10 DEF Message + <2>12. PCTypeOK' + BY <2>2, <2>11 + <2>13. AccInv' + BY <2>2 + <2>14. MsgInv1b' + <3>1. \A m \in msgs : (m.type = "phase1b" /\ m.bal # -1) + => m.val \in {"prepared","aborted"} + OBVIOUS + <3>2. nm.type = "phase2a" + OBVIOUS + <3>. QED BY <2>2, <3>1, <3>2 + <2>15. IsFiniteSet(msgs)' + BY <2>2, FS_AddElement + <2>. QED BY <2>12, <2>13, <2>14, <2>15 + +<1>7. ASSUME Decide + PROVE Inv' + BY <1>7, FS_AddElement DEF Decide + +<1>8. ASSUME NEW ac \in Acceptor, Phase1b(ac) + PROVE Inv' + <2>1. PICK m \in msgs : + /\ m.type = "phase1a" + /\ aState[m.ins][ac].mbal < m.bal + /\ aState' = [aState EXCEPT ![m.ins][ac].mbal = m.bal] + /\ Send([type |-> "phase1b", + ins |-> m.ins, + mbal |-> m.bal, + bal |-> aState[m.ins][ac].bal, + val |-> aState[m.ins][ac].val, + acc |-> ac]) + /\ UNCHANGED rmState + BY <1>8, Zenon DEF Phase1b + <2>2. m.ins \in RM /\ m.bal \in Ballot \ {0} + BY <2>1 DEF Message + <2> DEFINE nm == [type |-> "phase1b", + ins |-> m.ins, + mbal |-> m.bal, + bal |-> aState[m.ins][ac].bal, + val |-> aState[m.ins][ac].val, + acc |-> ac] + <2>3. nm \in Message + BY <2>2 DEF Message + <2>4. msgs' = msgs \cup {nm} + BY <2>1 + <2>5. PCTypeOK' + <3>1. aState' \in [RM -> [Acceptor -> [mbal : Ballot, + bal : Ballot \cup {-1}, + val : {"prepared","aborted","none"}]]] + BY <2>1, <2>2 + <3>2. msgs' \subseteq Message + BY <2>3, <2>4 + <3>3. rmState' \in [RM -> {"working", "prepared", "committed", "aborted"}] + BY <2>1 + <3>. QED BY <3>1, <3>2, <3>3 + <2>6. AccInv' + \** Phase1b only updates the mbal field; bal and val are unchanged. + BY <2>1 DEF Message + <2>7. MsgInv1b' + <3>1. nm.bal # -1 => nm.val \in {"prepared","aborted"} + <4>1. nm.bal = aState[m.ins][ac].bal + OBVIOUS + <4>2. nm.val = aState[m.ins][ac].val + OBVIOUS + <4>3. aState[m.ins][ac] \in [mbal : Ballot, + bal : Ballot \cup {-1}, + val : {"prepared","aborted","none"}] + BY <2>2 + <4>4. CASE aState[m.ins][ac].bal = -1 + BY <4>1, <4>4 + <4>5. CASE aState[m.ins][ac].bal # -1 + <5>1. aState[m.ins][ac].val # "none" + BY <4>5, <2>2 + <5>2. aState[m.ins][ac].val \in {"prepared","aborted"} + BY <4>3, <5>1 + <5>. QED BY <4>2, <5>2 + <4>. QED BY <4>4, <4>5 + <3>2. \A mm \in msgs : (mm.type = "phase1b" /\ mm.bal # -1) + => mm.val \in {"prepared","aborted"} + OBVIOUS + <3>. QED BY <2>4, <3>1, <3>2 + <2>8. IsFiniteSet(msgs)' + BY <2>4, FS_AddElement + <2>. QED BY <2>5, <2>6, <2>7, <2>8 + +<1>9. ASSUME NEW ac \in Acceptor, Phase2b(ac) + PROVE Inv' + <2>1. PICK m \in msgs : + /\ m.type = "phase2a" + /\ aState[m.ins][ac].mbal \leq m.bal + /\ aState' = [aState EXCEPT ![m.ins][ac].mbal = m.bal, + ![m.ins][ac].bal = m.bal, + ![m.ins][ac].val = m.val] + /\ Send([type |-> "phase2b", ins |-> m.ins, bal |-> m.bal, + val |-> m.val, acc |-> ac]) + /\ UNCHANGED rmState + BY <1>9, Zenon DEF Phase2b + <2>2. m.ins \in RM /\ m.bal \in Ballot /\ m.val \in {"prepared","aborted"} + BY <2>1 DEF Message + <2>3. m.bal # -1 + BY <2>2 + <2> DEFINE nm == [type |-> "phase2b", ins |-> m.ins, bal |-> m.bal, + val |-> m.val, acc |-> ac] + <2>4. nm \in Message + BY <2>2 DEF Message + <2>5. msgs' = msgs \cup {nm} + BY <2>1 + <2>6. PCTypeOK' + <3>1. aState' \in [RM -> [Acceptor -> [mbal : Ballot, + bal : Ballot \cup {-1}, + val : {"prepared","aborted","none"}]]] + BY <2>1, <2>2 + <3>2. msgs' \subseteq Message + BY <2>4, <2>5 + <3>3. rmState' \in [RM -> {"working", "prepared", "committed", "aborted"}] + BY <2>1 + <3>. QED BY <3>1, <3>2, <3>3 + <2>7. AccInv' + <3> SUFFICES ASSUME NEW rm \in RM, NEW a \in Acceptor + PROVE aState'[rm][a].val = "none" <=> aState'[rm][a].bal = -1 + BY DEF AccInv + <3>1. CASE rm = m.ins /\ a = ac + <4>1. aState'[rm][a] = [aState[m.ins][ac] EXCEPT + !.mbal = m.bal, !.bal = m.bal, !.val = m.val] + BY <2>1, <3>1 + <4>2. aState'[rm][a].bal = m.bal /\ aState'[rm][a].val = m.val + BY <4>1, <2>2 DEF Message + <4>3. aState'[rm][a].bal # -1 /\ aState'[rm][a].val # "none" + BY <4>2, <2>2, <2>3 + <4>. QED BY <4>3 + <3>2. CASE ~(rm = m.ins /\ a = ac) + <4>1. aState'[rm][a] = aState[rm][a] + BY <2>1, <3>2, <2>2 + <4>. QED BY <4>1 + <3>. QED BY <3>1, <3>2 + <2>8. MsgInv1b' + <3>1. nm.type = "phase2b" + OBVIOUS + <3>2. \A mm \in msgs : (mm.type = "phase1b" /\ mm.bal # -1) + => mm.val \in {"prepared","aborted"} + OBVIOUS + <3>. QED BY <2>5, <3>1, <3>2 + <2>9. IsFiniteSet(msgs)' + BY <2>5, FS_AddElement + <2>. QED BY <2>6, <2>7, <2>8, <2>9 + +<1>10. CASE UNCHANGED vars + BY <1>10 + +<1>. QED + BY <1>1, <1>2, <1>3, <1>4, <1>5, <1>6, <1>7, <1>8, <1>9, <1>10 + DEF PCNext + +(***************************************************************************) +(* Main theorem: PCTypeOK is an invariant of PCSpec. *) +(***************************************************************************) +THEOREM TypeOK_Invariant == PCSpec => []PCTypeOK +<1>1. PCInit => Inv + BY InitInv +<1>2. Inv /\ [PCNext]_vars => Inv' + BY NextInv +<1>3. Inv => PCTypeOK + BY DEF Inv +<1>. QED BY <1>1, <1>2, <1>3, PTL DEF PCSpec, vars + +(***************************************************************************) +(* The non-temporal version of the theorem stated in PaxosCommit.tla *) +(* (PCSpec => PCTypeOK) is an immediate corollary. *) +(***************************************************************************) +THEOREM TypeOK_Init == PCSpec => PCTypeOK +BY TypeOK_Invariant, PTL + +============================================================================ diff --git a/specifications/transaction_commit/TCommit_proof.tla b/specifications/transaction_commit/TCommit_proof.tla new file mode 100644 index 00000000..0b91ed62 --- /dev/null +++ b/specifications/transaction_commit/TCommit_proof.tla @@ -0,0 +1,31 @@ +--------------------------- MODULE TCommit_proof --------------------------- +(***************************************************************************) +(* TLAPS proof of *) +(* THEOREM TCSpec => [](TCTypeOK /\ TCConsistent) *) +(* stated in TCommit.tla. *) +(***************************************************************************) +EXTENDS TCommit, TLAPS + +Inv == TCTypeOK /\ TCConsistent + +THEOREM TCorrect == TCSpec => []Inv +<1>1. TCInit => Inv + BY DEF TCInit, Inv, TCTypeOK, TCConsistent +<1>2. Inv /\ [TCNext]_rmState => Inv' + <2> SUFFICES ASSUME Inv, + [TCNext]_rmState + PROVE Inv' + OBVIOUS + <2>. USE DEF Inv, TCTypeOK, TCConsistent + <2>1. ASSUME NEW rm \in RM, Prepare(rm) + PROVE Inv' + BY <2>1 DEF Prepare + <2>2. ASSUME NEW rm \in RM, Decide(rm) + PROVE Inv' + BY <2>2 DEF Decide, canCommit, notCommitted + <2>3. CASE UNCHANGED rmState + BY <2>3 + <2>. QED BY <2>1, <2>2, <2>3 DEF TCNext +<1>. QED BY <1>1, <1>2, PTL DEF TCSpec, Inv + +============================================================================ diff --git a/specifications/transaction_commit/TwoPhase_proof.tla b/specifications/transaction_commit/TwoPhase_proof.tla new file mode 100644 index 00000000..76c92dc6 --- /dev/null +++ b/specifications/transaction_commit/TwoPhase_proof.tla @@ -0,0 +1,154 @@ +--------------------------- MODULE TwoPhase_proof -------------------------- +(***************************************************************************) +(* TLAPS proofs of TwoPhase.tla theorems: *) +(* *) +(* TPSpec => []TPTypeOK (Band E, directly inductive) *) +(* TPSpec => []TC!TCConsistent (Band M, no conflicting decisions) *) +(* *) +(* TC!TCConsistent says no two RMs end up "committed" and "aborted" *) +(* simultaneously. It is not directly inductive; the strengthening below *) +(* tracks the message-sequencing facts that explain why the TM-broadcast *) +(* "Commit" and "Abort" decisions are mutually exclusive, and how each *) +(* RM's local state correlates with what is on the wire. *) +(* *) +(* The candidate inductive invariant was first validated with Apalache *) +(* (per Konnov/Kuppe/Merz, arXiv:2211.07216 Sec. 3.2) on a finite *) +(* instance with 3 RMs: *) +(* *) +(* TPInit /\ [TPNext]_vars |=0 Inv (initial states satisfy Inv) *) +(* InvInit /\ [TPNext]_vars |=1 Inv (Inv is preserved one step) *) +(* Inv => TCConsistent (Inv implies the goal) *) +(***************************************************************************) +EXTENDS TwoPhase, TLAPS + +(***************************************************************************) +(* TPSpec => []TPTypeOK *) +(***************************************************************************) + +THEOREM TypeCorrect == TPSpec => []TPTypeOK +<1>1. TPInit => TPTypeOK + BY DEF TPInit, TPTypeOK +<1>2. TPTypeOK /\ [TPNext]_<> => TPTypeOK' + <2> SUFFICES ASSUME TPTypeOK, + [TPNext]_<> + PROVE TPTypeOK' + OBVIOUS + <2>. USE DEF TPTypeOK, Message + <2>1. CASE TMCommit BY <2>1 DEF TMCommit + <2>2. CASE TMAbort BY <2>2 DEF TMAbort + <2>3. ASSUME NEW rm \in RM, TMRcvPrepared(rm) + PROVE TPTypeOK' + BY <2>3 DEF TMRcvPrepared + <2>4. ASSUME NEW rm \in RM, RMPrepare(rm) + PROVE TPTypeOK' + BY <2>4 DEF RMPrepare + <2>5. ASSUME NEW rm \in RM, RMChooseToAbort(rm) + PROVE TPTypeOK' + BY <2>5 DEF RMChooseToAbort + <2>6. ASSUME NEW rm \in RM, RMRcvCommitMsg(rm) + PROVE TPTypeOK' + BY <2>6 DEF RMRcvCommitMsg + <2>7. ASSUME NEW rm \in RM, RMRcvAbortMsg(rm) + PROVE TPTypeOK' + BY <2>7 DEF RMRcvAbortMsg + <2>8. CASE UNCHANGED <> + BY <2>8 + <2>. QED BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7, <2>8 DEF TPNext +<1>. QED BY <1>1, <1>2, PTL DEF TPSpec + +(***************************************************************************) +(* TPSpec => []TC!TCConsistent (Band M) *) +(***************************************************************************) + +CommitMsg == [type |-> "Commit"] +AbortMsg == [type |-> "Abort"] +PrepMsg(rm) == [type |-> "Prepared", rm |-> rm] + +(***************************************************************************) +(* The strengthened inductive invariant. Each conjunct is a fact that *) +(* the protocol's actions preserve and that together imply TCConsistent. *) +(* *) +(* 1. TPTypeOK *) +(* 2. The TM commits at most one decision (mutex on Commit/Abort msgs). *) +(* 3-5. tmState mirrors which decision message has been broadcast. *) +(* 6. tmPrepared only contains RMs that actually sent "Prepared". *) +(* 7. RMs that have a "Prepared" msg in flight are no longer "working". *) +(* 8. "committed" RMs imply CommitMsg has been broadcast. *) +(* 9. CommitMsg in msgs implies every RM had sent "Prepared" first *) +(* (preserved from TMCommit's tmPrepared = RM precondition). *) +(* 10. "aborted" RMs split into two cases: *) +(* - via RMRcvAbortMsg (AbortMsg in msgs), or *) +(* - via RMChooseToAbort (the RM never sent "Prepared"). *) +(***************************************************************************) +Inv == + /\ TPTypeOK + /\ ~ (CommitMsg \in msgs /\ AbortMsg \in msgs) + /\ tmState = "init" => CommitMsg \notin msgs /\ AbortMsg \notin msgs + /\ tmState = "committed" => CommitMsg \in msgs + /\ tmState = "aborted" => AbortMsg \in msgs + /\ \A rm \in tmPrepared : PrepMsg(rm) \in msgs + /\ \A rm \in RM : PrepMsg(rm) \in msgs => rmState[rm] # "working" + /\ \A rm \in RM : rmState[rm] = "committed" => CommitMsg \in msgs + /\ CommitMsg \in msgs => \A rm \in RM : PrepMsg(rm) \in msgs + /\ \A rm \in RM : rmState[rm] = "aborted" => + \/ AbortMsg \in msgs + \/ PrepMsg(rm) \notin msgs + +LEMMA InvInductive == TPSpec => []Inv +<1>1. TPInit => Inv + BY DEF TPInit, Inv, TPTypeOK, Message, CommitMsg, AbortMsg, PrepMsg +<1>2. Inv /\ [TPNext]_<> => Inv' + <2> SUFFICES ASSUME Inv, + [TPNext]_<> + PROVE Inv' + OBVIOUS + <2>. USE DEF Inv, TPTypeOK, Message, CommitMsg, AbortMsg, PrepMsg + <2>1. CASE TMCommit + \* tmState : init -> committed; CommitMsg added to msgs. + \* AbortMsg notin msgs in pre-state (tmState=init). tmPrepared = RM + \* gives \A rm \in RM : PrepMsg(rm) \in msgs (via conjunct 6). + BY <2>1 DEF TMCommit + <2>2. CASE TMAbort + \* tmState : init -> aborted; AbortMsg added. CommitMsg notin msgs. + BY <2>2 DEF TMAbort + <2>3. ASSUME NEW rm \in RM, TMRcvPrepared(rm) + PROVE Inv' + \* tmPrepared grows by {rm}, msgs unchanged. PrepMsg(rm) \in msgs is + \* the precondition, so the new tmPrepared still satisfies conjunct 6. + BY <2>3 DEF TMRcvPrepared + <2>4. ASSUME NEW rm \in RM, RMPrepare(rm) + PROVE Inv' + \* rmState[rm] : working -> prepared; PrepMsg(rm) added to msgs. + BY <2>4 DEF RMPrepare + <2>5. ASSUME NEW rm \in RM, RMChooseToAbort(rm) + PROVE Inv' + \* rmState[rm] : working -> aborted, no msg change. PrepMsg(rm) + \* could only have been in msgs if rmState[rm] # "working", but the + \* precondition says it WAS "working", so PrepMsg(rm) \notin msgs; + \* conjunct 10 holds via the second disjunct. + BY <2>5 DEF RMChooseToAbort + <2>6. ASSUME NEW rm \in RM, RMRcvCommitMsg(rm) + PROVE Inv' + \* rmState[rm] becomes "committed"; preconditions: CommitMsg \in msgs. + BY <2>6 DEF RMRcvCommitMsg + <2>7. ASSUME NEW rm \in RM, RMRcvAbortMsg(rm) + PROVE Inv' + \* rmState[rm] becomes "aborted"; preconditions: AbortMsg \in msgs. + BY <2>7 DEF RMRcvAbortMsg + <2>8. CASE UNCHANGED <> + BY <2>8 + <2>. QED BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7, <2>8 DEF TPNext +<1>. QED BY <1>1, <1>2, PTL DEF TPSpec + +THEOREM Consistency == TPSpec => []TC!TCConsistent +<1>1. Inv => TC!TCConsistent + \* Suppose rmState[rm1] = "aborted" and rmState[rm2] = "committed". + \* From conjunct 8: CommitMsg \in msgs. + \* From conjunct 9: PrepMsg(rm1) \in msgs. + \* From conjunct 2: AbortMsg \notin msgs. + \* From conjunct 10 applied to rm1: AbortMsg \in msgs (false) or + \* PrepMsg(rm1) \notin msgs (false). Contradiction. + BY DEF Inv, TC!TCConsistent, CommitMsg, AbortMsg, PrepMsg +<1>. QED BY <1>1, InvInductive, PTL + +============================================================================