diff --git a/PROOF_DIFFICULTY.md b/PROOF_DIFFICULTY.md new file mode 100644 index 00000000..b2f31b5a --- /dev/null +++ b/PROOF_DIFFICULTY.md @@ -0,0 +1,302 @@ +# Proof difficulty ranking + +This document ranks every `THEOREM` in the repository by the expected +difficulty of producing a TLAPS proof for it. It is meant as a roadmap for +contributors who want to pick off proof obligations roughly in order of +ascending effort. + +The survey covers all `*.tla` files under `specifications/` (excluding +`.tlacache/` directories), 230 `THEOREM`s in total. Of those, 107 already +carry a `BY` or structured proof. The remaining 123 — the focus of the +ranking below — are either stated without proof or marked `OMITTED`. + +### Recent progress + +A first round added 18 Band-T/E proofs in companion `_proof.tla` files; +a follow-up round added 3 Band-M proofs in `Paxos/Voting_proof.tla` +(`OneValuePerBallot => OneVote`, `VotesSafeImpliesConsistency`, +`ShowsSafety`). A fourth round added a Band-M strengthening for +TwoPhase Commit: `TPSpec => []TC!TCConsistent` (no conflicting +decisions), with the inductive invariant first validated via Apalache +in `transaction_commit/MCTwoPhaseApa.tla` per the trifecta workflow. +A third round added 6 more Band-M proofs: + +- `PaxosHowToWinATuringAward/Voting`: `AllSafeAtZero`, `ChoosableThm` + (Band E helpers), and `ShowsSafety` (Band M, ported from the + sibling `Paxos/Voting` proof). +- `allocator/SimpleAllocator`: `[]TypeInvariant`, `[]ResourceMutex`. +- `allocator/SchedulingAllocator`: `[]TypeInvariant`, `[]ResourceMutex`. +- `allocator/AllocatorImplementation`: `[]TypeInvariant`. + +See `git log` for the commits. Highlights: + +- 12 of the 16 Band T theorems are now done (the 4 outstanding either + involve community-modules unfolding or were re-classified as Band M + after attempting them). +- 6 of the 21 Band E theorems are done; 8 more were re-classified as + Band M because the obvious-looking inductive invariant turned out to + need a real strengthening. + +The most informative bumps were: + +- `InternalMemory` `ISpec => []TypeInvariant`: strengthened with + `BufConsistent` (the per-`ctl[p]` typing of `buf[p]`). +- `MultiPaxos_MC` `TypeOK` and `Chameneos` `SumMet`: both need + monotone-counter / set-cardinality invariants that aren't part of + `TypeOK` itself. +- `Voucher{Issue,Cancel,Redeem,Transfer}` `VTPConsistent`: requires the + message-sequencing invariant that `Issue` and `Abort` are mutually + exclusive in `msgs`. +- `PaxosCommit` `Phase2a`: needs the auxiliary invariant + "phase1b messages with `bal # -1` carry a non-`"none"` `val`". + +## Methodology + +For each unproved `THEOREM` I estimated: + +- the **shape** of the inductive invariant required (is the theorem itself + inductive? does it need a small strengthening? a substantial one?); +- whether **liveness** machinery is involved (`WF`/`SF` fairness, + well-founded measures, `PTL`/`LATTICE` reasoning); +- whether the theorem is a **refinement** between two non-trivial specs + (refinement mapping, possibly with auxiliary or prophecy variables); +- whether **real-time** or **probabilistic** reasoning is required (TLAPS + support for these is thin); +- whether **community-modules** predicates such as `IsTreeWithRoot`, + `SimplePath`, `IsFiniteSet`/`Cardinality` need to be unfolded. + +Estimates assume a TLAPS-fluent prover with the community modules in scope. +Person-day numbers are very approximate. + +| Band | Label | Effort | Typical work | +|:------:|:------------|:---------------|:------------------------------------------------------------------| +| **T** | Trivial | ≤ ½ day | Single-action spec, type invariant, mechanical | +| **E** | Easy | ½–2 days | Inductive invariant ≈ goal, no liveness | +| **M** | Moderate | 2–10 days | Real strengthening, or small algebraic / cardinality lemmas | +| **H** | Hard | 1–4 weeks | Refinement mapping, distributed-algorithm safety, or routine WF-based liveness | +| **VH** | Very Hard | ≥ 1 month | Liveness with well-founded measure, real-time, deep refinement, or foundational mathematics | + +Reality routinely surprises: any band-T/E item that touches `IsFiniteSet`, +`Cardinality`, `Seq`, or `Graphs` can blow up because of awkward unfolding. + +--- + +Items marked `[done]` have been proven in a companion `_proof.tla` file +under the same directory. Items marked `[bumped]` turned out to be harder +than the band suggests once attempted; their actual band is shown in +parentheses. + +## Band T — Trivial (16 items, 12 done) + +Single-action / textbook specs; one inductive invariant equal to the type +predicate. + +- `[done]` `specifications/SpecifyingSystems/HourClock/HourClock.tla:8` — `HC => []HCini` +- `[done]` `specifications/SpecifyingSystems/Composing/HourClock.tla:8` — same +- `[done]` `specifications/SpecifyingSystems/Liveness/HourClock.tla:8` — same +- `[done]` `specifications/SpecifyingSystems/RealTime/HourClock.tla:8` — same (Init/Next identical to plain version) +- `specifications/SpecifyingSystems/HourClock/HourClock2.tla:18` — `HC <=> HC2` (definitional equivalence) +- `[done]` `specifications/SpecifyingSystems/AsynchronousInterface/Channel.tla:21` — `Spec => []TypeInvariant` +- `[done]` `specifications/SpecifyingSystems/Composing/Channel.tla:21` — same +- `[done]` `specifications/SpecifyingSystems/FIFO/Channel.tla:21` — same +- `[done]` `specifications/SpecifyingSystems/AsynchronousInterface/AsynchInterface.tla:27` — `Spec => []TypeInvariant` +- `[done] [bumped → M]` `specifications/SpecifyingSystems/CachingMemory/InternalMemory.tla:42` — `ISpec => []TypeInvariant` (needed `BufConsistent` strengthening: `ctl[p]="busy" => buf[p] \in MReq`, etc.) +- `[done] [bumped → M]` `specifications/SpecifyingSystems/Composing/InternalMemory.tla:42` — same +- `[done] [bumped → M]` `specifications/SpecifyingSystems/Liveness/InternalMemory.tla:42` — same +- `[done] [bumped → M]` `specifications/SpecifyingSystems/RealTime/InternalMemory.tla:42` — same +- `specifications/SpecifyingSystems/CachingMemory/MCWriteThroughCache.tla:90` — `LM_Inner_ISpec => []LM_Inner_TypeInvariant` +- `specifications/SpecifyingSystems/AdvancedExamples/InnerSequential.tla:74` — `Spec => []DataInvariant` (re-classified to Band M: `Cardinality({i \in DOMAIN opQ[p] : opQ[p][i].reg = r}) = ...` invariant requires non-trivial reasoning about the queue/regfile correspondence) +- `[done]` `specifications/byihive/VoucherLifeCycle.tla:96` — `VSpec => [](VTypeOK /\ VConsistent)` (small CSL state) + +## Band E — Easy (21 items, 6 done) + +Two-to-five-action specs, type + simple safety; the inductive invariant is +the obvious one or `TypeOK ∧ goal`. + +- `[done]` `specifications/SpecifyingSystems/FIFO/InnerFIFO.tla:38` — `Spec => []TypeInvariant` +- `specifications/SpecifyingSystems/FIFO/InnerFIFOInstanced.tla:101` — same +- `[done]` `specifications/SpecifyingSystems/TLC/AlternatingBit.tla:77` — `ABSpec => []ABTypeInv` +- `[bumped → M]` `specifications/byihive/VoucherIssue.tla:261` — `VTPSpec => [](VTPTypeOK /\ VTPConsistent)` (VTPConsistent needs message-sequencing strengthening: Issue and Abort are mutually exclusive in `msgs`, etc.) +- `[bumped → M]` `specifications/byihive/VoucherCancel.tla:260` — same +- `[bumped → M]` `specifications/byihive/VoucherTransfer.tla:267` — same +- `[bumped → M]` `specifications/byihive/VoucherRedeem.tla:258` — same +- `[done]` `specifications/transaction_commit/TCommit.tla:62` — `TCSpec => [](TCTypeOK /\ TCConsistent)` +- `[done]` `specifications/transaction_commit/TwoPhase.tla:149` — `TPSpec => []TPTypeOK` +- `[done, partial]` `specifications/transaction_commit/PaxosCommit.tla:268` — `PCSpec => PCTypeOK` (proven for the initial state, which is all the literal theorem statement requires; the stronger `[]PCTypeOK` would need an extra invariant about phase1b messages) +- `[bumped → M]` `specifications/MultiPaxos-SMR/MultiPaxos_MC.tla:32` — `Spec => []TypeOK` (`Cardinality(Range(pending)) = Len(pending)` requires the auxiliary invariant that `pending` has distinct elements) +- `[done]` `specifications/PaxosHowToWinATuringAward/Voting.tla:124` — `AllSafeAtZero` (pure first-order) +- `[done]` `specifications/PaxosHowToWinATuringAward/Voting.tla:131` — `ChoosableThm` +- `specifications/Paxos/Voting.tla:94` — `AllSafeAtZero` (same content) +- `specifications/Paxos/Voting.tla:96` — `ChoosableThm` (same) +- `[bumped → M]` `specifications/Chameneos/Chameneos.tla:79` — `Spec => []SumMet` (needs strengthening `Sum(f, ChameneosID) = 2 * numMeetings` plus reasoning about the `RECURSIVE Sum` operator) +- `[bumped → M]` `specifications/SingleLaneBridge/SingleLaneBridge.tla:114` — `Spec => []TypeOK` (`Len(WaitingBeforeBridge) <= Cardinality(Cars)` is not invariant without additional reasoning that a car may not be enqueued twice) +- `[bumped → M]` `specifications/SingleLaneBridge/SingleLaneBridge.tla:112` — `Spec => []Invariants` (uses `Cardinality(CarsInBridge) < Cardinality(Bridge) + 1`) +- `[done]` `specifications/KeyValueStore/KeyValueStore.tla:105` — `Spec => [](TypeInvariant /\ TxLifecycle)` +- `[done in companion]` `specifications/MisraReachability/Reachable.tla:195` — `Spec => []PartialCorrectness` (now proven as `PartialCorrectnessThm` in `ReachableProofs.tla`, and the existing structurally-equivalent unnamed theorem there is now named `Thm4` for downstream reuse; the spec-file stub itself remains unproven for the usual no-circular-spec→companion-imports reason) +- `[bumped → M]` `specifications/Huang/Huang.tla:106` — `Spec => Safe` (`[](TerminationDetected => []Terminated)` requires the dyadic-rational weight conservation invariant; depends on the `DyadicRationals` community module) + +## Band M — Moderate (24 items) + +Need a real inductive strengthening, or small algebraic / cardinality +lemmas, but follow well-known patterns. + +- `[done]` `specifications/Paxos/Voting.tla:111` — `VotesSafeImpliesConsistency` (proven via the `TwoChosenSameValue` / `TwoChosenEqual` chain that uses Quorum intersection and `OneVote`; 116 obligations) +- `[done]` `specifications/Paxos/Voting.tla:124` — `ShowsSafety` (proven by trichotomy on the witness ballot `c` from `ShowsSafeAt`; 215 total obligations including helpers) +- `[done]` `specifications/Paxos/Voting.tla:109` — `OneValuePerBallot => OneVote` (one-line BY) +- `[done]` `specifications/PaxosHowToWinATuringAward/Voting.tla:179` — `ShowsSafety` (direct port of `Paxos/Voting`'s ShowsSafety_T) +- `specifications/Paxos/Voting.tla:178` — `Invariance == Spec => []Inv` (cf. `byzpaxos/VoteProof.tla` already proves the analogous theorem; should largely transfer; the `SafeAtMonotone` lemma needed for the `VotesSafe` preservation case was attempted but requires careful arithmetic over `Ballot \cup {-1}` and `EXCEPT` reasoning, deferred) +- `specifications/PaxosHowToWinATuringAward/Paxos.tla:319` — `Invariance == Spec => []Inv` (analogous) +- `specifications/SpecifyingSystems/CachingMemory/WriteThroughCache.tla:89` — `Spec => [](TypeInvariant /\ Coherence)` (Coherence needs a non-trivial invariant about clean/dirty cache lines) +- `specifications/SpecifyingSystems/CachingMemory/WriteThroughCacheInstanced.tla:151` — same +- `specifications/SpecifyingSystems/CachingMemory/WriteThroughCacheInstanced.tla:162` — `ISpec => []TypeInvariant` +- `specifications/SpecifyingSystems/RealTime/WriteThroughCache.tla:89` — same Coherence (real-time variant) +- `specifications/SpecifyingSystems/Liveness/WriteThroughCacheInstanced.tla:151` — same Coherence +- `specifications/SpecifyingSystems/Liveness/WriteThroughCacheInstanced.tla:162` — `ISpec => []TypeInvariant` +- `[done]` `specifications/allocator/SimpleAllocator.tla:109` — `SimpleAllocator => []TypeInvariant` +- `[done]` `specifications/allocator/SimpleAllocator.tla:110` — `SimpleAllocator => []ResourceMutex` (uses the disjoint-from-`available` argument; same shape generalises to `SchedulingAllocator`) +- `[done]` `specifications/allocator/SchedulingAllocator.tla:170` — `Allocator => []TypeInvariant` (needs `Drop`, `\circ`, and a `PermSeqsType` lemma that is left `OMITTED` because it requires induction on the recursive `PermSeqs` definition) +- `[done]` `specifications/allocator/SchedulingAllocator.tla:171` — `Allocator => []ResourceMutex` +- `specifications/allocator/SchedulingAllocator.tla:172` — `Allocator => []AllocatorInvariant` (the heavy lifting; pool of pending requests) +- `[done]` `specifications/allocator/AllocatorImplementation.tla:190` — `Specification => []TypeInvariant` (uses the same `Drop` / `PermSeqs` machinery via the `Sched!` instance) +- `specifications/allocator/AllocatorImplementation.tla:191` — `Specification => []ResourceMutex` (the *client-side* mutex on `holding` needs the cross-spec `Invariant` connecting `holding[c] \subseteq alloc[c]` plus `Sched!ResourceMutex`; deferred along with `Sched!AllocatorInvariant`) +- `specifications/allocator/AllocatorImplementation.tla:192` — `Specification => []Invariant` +- `specifications/NanoBlockchain/Nano.tla:488` — `Safety == Spec => TypeInvariant /\ SafetyInvariant` (no-double-spend; hash-graph state) +- `specifications/NanoBlockchain/MCNano.tla:119` — same (model wrapper) +- `specifications/ewd998/EWD998ChanID.tla:210` — `Spec => []Max3TokenRounds` (counter argument over token rounds) +- `specifications/FiniteMonotonic/DistributedReplicatedLog.tla:59` — `Spec => []BoundedLag` + +## Band H — Hard (32 items) + +Refinement between non-trivial specs, distributed-algorithm safety, +well-founded termination, or routine WF-based liveness. + +- `specifications/PaxosHowToWinATuringAward/Paxos.tla:321` — `Implementation == Spec => V!Spec` +- `specifications/Paxos/Paxos.tla:197` — `Spec => V!Spec` +- `specifications/byihive/VoucherIssue.tla:278` — `VTPSpec => VSpec` (TPC refines voucher issuance) +- `specifications/byihive/VoucherCancel.tla:277` — same pattern +- `specifications/byihive/VoucherRedeem.tla:275` — same +- `specifications/byihive/VoucherTransfer.tla:284` — same +- `[partial] / [done for TC!TCConsistent]` `specifications/transaction_commit/TwoPhase.tla:165` — `TPSpec => TC!TCSpec` (canonical Lamport refinement; the safety corollary `TPSpec => []TC!TCConsistent` is now proven in `TwoPhase_proof.tla` with a 10-conjunct strengthening validated via Apalache before TLAPS, but the full refinement is still Band H — it would additionally need a refinement mapping that abstracts the message-level state away) +- `specifications/transaction_commit/PaxosCommit.tla:280` — `PCSpec => TC!TCSpec` +- `specifications/byzpaxos/PConProof.tla:511` — `PT1` (`ShowsSafeAt => SafeAt` lemma) +- `specifications/byzpaxos/PConProof.tla:517` — `Invariance == Spec => []PInv` +- `specifications/byzpaxos/PConProof.tla:520` — `Implementation == Spec => V!Spec` +- `specifications/byzpaxos/PConProof.tla:527` — `Spec => [](chosen = V!chosen)` +- `specifications/MisraReachability/ParReach.tla:223` — `Spec => Refines` (= `Spec => R!Spec`; depends on the fairness-refinement piece below, since `R!Spec` includes `WF_R!vars(R!Next)`) +- `specifications/MisraReachability/ParReach.tla:235` — `Spec => WF_R!vars(R!Next)` (fairness refinement; the per-process `WF_vars(p(self))` of the parallel spec needs to be lifted via the refinement mapping to `WF_R!vars(R!Next)` of Misra's algorithm; non-trivial PTL reasoning) +- `[done in companion]` `specifications/MisraReachability/ParReach.tla:234` — `Spec => R!Init /\ [][R!Next]_R!vars` (now named `RefinementSafety` in `ParReachProofs.tla`; the spec-file stub remains unproven as above) +- `specifications/MisraReachability/Reachable.tla:209` — `IsFiniteSet(Reachable) => Spec => <>(pc = "Done")` (termination, well-founded measure on the lex pair `<>`; uses `WF_vars(Next)` plus `WellFoundedInduction`. Multi-day TLAPS proof; deferred) +- `specifications/Huang/Huang.tla:111` — `Spec => Live` (termination detection liveness) +- `specifications/KnuthYao/Prob.tla:38` — `Converges == Spec => <>(state \in Accepting \/ Norm(p) = 0)` (probabilistic, treated as `<>`termination) +- `specifications/Prisoners/Prisoners.tla:178` — `Spec => Safety /\ Liveness` +- `specifications/SingleLaneBridge/SingleLaneBridge.tla:117` — `Spec => CarsEnterBridge` (small WF liveness) +- `specifications/SingleLaneBridge/SingleLaneBridge.tla:116` — `Spec => CarsInBridgeExitBridge` +- `specifications/allocator/SimpleAllocator.tla:111` — `SimpleAllocator => ClientsWillReturn` +- `specifications/allocator/SimpleAllocator.tla:112` — `SimpleAllocator2 => ClientsWillReturn` +- `specifications/allocator/SchedulingAllocator.tla:173` — `Allocator => ClientsWillReturn` +- `specifications/allocator/AllocatorImplementation.tla:193` — `Specification => ClientsWillReturn` +- `specifications/ewd998/EWD998Chan.tla:192` — `Spec => EWD998Spec` (refinement to EWD998) +- `specifications/ewd998/EWD998PCal.tla:153` — `Spec => EWD998Spec` (PlusCal version) +- `specifications/ewd998/EWD998ChanID.tla:262` — `Spec => EWD998ChanSpec` +- `specifications/ewd998/EWD998ChanID.tla:267` — `Spec => EWD998Safe /\ EWD998Live` +- `specifications/MultiPaxos-SMR/MultiPaxos_MC.tla:73` — `Spec => Linearizability` +- `specifications/FiniteMonotonic/ReplicatedLog.tla:48` — `Spec => []TypeOK` (small but with monotonic data structures) +- `specifications/FiniteMonotonic/DistributedReplicatedLog.tla:67` — `Spec => AllExtending` (WF liveness) +- `specifications/CoffeeCan/CoffeeCan.tla:115` — `TypeInvariant /\ MonotonicDecrease /\ EventuallyTerminates /\ LoopInvariant /\ TerminationHypothesis` (mixed safety + termination) +- `specifications/MultiCarElevator/Elevator.tla:235` — `Spec => [](TypeInvariant /\ SafetyInvariant /\ TemporalInvariant)` +- `specifications/CheckpointCoordination/CheckpointCoordination.tla:527` — `Spec => /\ []TypeInvariant /\ []SafetyInvariant /\ []TemporalInvariant` +- `specifications/ewd687a/EWD687a_proof.tla:553` & `specifications/ewd687a/EWD687a.tla:430` — `Spec => TreeWithRoot` (needs unfolding of `IsTreeWithRoot` / `SimplePath` from community Graphs module) + +## Band VH — Very Hard (15+ items) + +Strong-fairness liveness, deep refinement, real-time, or foundational +mathematics. + +- `specifications/allocator/AllocatorRefinement.tla:11` — `Allocator => SimpleAllocator` (refining a richer allocator into a simpler one — fairness too) +- `specifications/allocator/AllocatorImplementation.tla:203` — `Specification => SchedAllocator` (full refinement of scheduling allocator) +- `specifications/diskpaxos/DiskSynod.tla:126` — `DiskSynodSpec => SynodSpec` (Disk Paxos refines abstract Synod — extensive) +- `specifications/byzpaxos/PConProof.tla:572` — `Liveness == Spec => …` (Paxos liveness with explicit assumption package) +- `specifications/allocator/SimpleAllocator.tla:113` — `SimpleAllocator => ClientsWillObtain` (SF-style liveness with scheduling) +- `specifications/allocator/SimpleAllocator.tla:114` — `SimpleAllocator => InfOftenSatisfied` +- `specifications/allocator/SchedulingAllocator.tla:174` — `Allocator => ClientsWillObtain` +- `specifications/allocator/SchedulingAllocator.tla:175` — `Allocator => InfOftenSatisfied` +- `specifications/allocator/AllocatorImplementation.tla:194` — `Specification => ClientsWillObtain` +- `specifications/allocator/AllocatorImplementation.tla:195` — `Specification => InfOftenSatisfied` +- `specifications/FiniteMonotonic/ReplicatedLog.tla:70` — `ExecFairSpec => Convergence` (CRDT convergence on infinite fair runs) +- `specifications/FiniteMonotonic/ReplicatedLog.tla:71` — `WriteFairSpec => Convergence` +- `specifications/SpecifyingSystems/Liveness/LiveHourClock.tla:35` — `LSpec => AlwaysTick /\ AllTimes /\ TypeInvariance` (real-time liveness; TLAPS support thin) +- `specifications/SpecifyingSystems/Liveness/LiveInternalMemory.tla:44` — `LISpec => LivenessProperty` +- `specifications/SpecifyingSystems/RealTime/RTWriteThroughCache.tla:50` — `RTSpec => RTM!RTSpec` (real-time refinement) +- `specifications/SpecifyingSystems/CachingMemory/WriteThroughCache.tla:92` — `Spec => LM!Spec` (memory refinement; refinement mapping with auxiliary state — small project) +- `specifications/SpecifyingSystems/RealTime/WriteThroughCache.tla:92` — same with real time +- `specifications/ewd687a/EWD687a_proof.tla:568` & `specifications/ewd687a/EWD687a.tla:456` — `Spec => DT2` (termination detection liveness; needs WF + multiset measure on `(msgs, rcvdUnacked, acks, sentUnacked)`) +- `specifications/SpecifyingSystems/Standard/ProtoReals.tla:36` — `\E R, Plus, Times, Leq : IsModelOfReals(R, Plus, Times, Leq)` (constructive existence of the real-number system from Peano — Dedekind cuts; arguably the single hardest theorem in the repo) + +--- + +## Already proved (107 theorems) + +No work to do; listed by file with theorem count for completeness. + +| File | Count | +|-------------------------------------------------------------------|------:| +| `specifications/Bakery-Boulangerie/Bakery.tla` | 2 | +| `specifications/Bakery-Boulangerie/Boulanger.tla` | 2 | +| `specifications/FiniteMonotonic/CRDT_proof.tla` | 7 | +| `specifications/LearnProofs/AddTwo.tla` | 2 | +| `specifications/LearnProofs/FindHighest.tla` | 4 | +| `specifications/LoopInvariance/BinarySearch.tla` | 1 | +| `specifications/LoopInvariance/Quicksort.tla` | 1 | +| `specifications/LoopInvariance/SumSequence.tla` | 2 | +| `specifications/MisraReachability/ReachableProofs.tla` | 4 | +| `specifications/MisraReachability/ParReachProofs.tla` | 1 | +| `specifications/Paxos/Consensus.tla` | 2 | +| `specifications/Paxos/Voting.tla` (1 of 8) | 1 | +| `specifications/PaxosHowToWinATuringAward/Consensus.tla` | 1 | +| `specifications/PaxosHowToWinATuringAward/Voting.tla` (2 of 5) | 2 | +| `specifications/TeachingConcurrency/Simple.tla` | 2 | +| `specifications/TeachingConcurrency/SimpleRegular.tla` | 2 | +| `specifications/TwoPhase/TwoPhase.tla` | 1 | +| `specifications/barriers/Barriers.tla` (6 of 7) | 6 | +| `specifications/bcastByz/bcastByz.tla` | 13 | +| `specifications/byzpaxos/Consensus.tla` | 3 | +| `specifications/byzpaxos/BPConProof.tla` | 5 | +| `specifications/byzpaxos/VoteProof.tla` | 12 | +| `specifications/byzpaxos/PConProof.tla` (1 of 6) | 1 | +| `specifications/ewd687a/EWD687a_proof.tla` (3 of 5) | 3 | +| `specifications/ewd840/EWD840_proof.tla` | 4 | +| `specifications/ewd840/SyncTerminationDetection_proof.tla` | 4 | +| `specifications/ewd998/EWD998_proof.tla` | 5 | +| `specifications/ewd998/AsyncTerminationDetection_proof.tla` | 3 | +| `specifications/lamport_mutex/LamportMutex_proofs.tla` | 3 | +| `specifications/locks_auxiliary_vars/Lock.tla` | 1 | +| `specifications/locks_auxiliary_vars/LockHS.tla` | 2 | +| `specifications/locks_auxiliary_vars/Peterson.tla` | 2 | +| `specifications/sums_even/sums_even.tla` | 2 | + +`EWD998_proof.tla:Refinement` subsumes `EWD998.tla:207` (`Spec => TDSpec`), +and the structural pieces in `ReachableProofs.tla`/`ParReachProofs.tla` +mostly cover the goals stated in `Reachable.tla`/`ParReach.tla` (the latter +still need final wrap-up theorems, listed in Bands E–H above). + +--- + +## Caveats + +- "Difficulty" is *expected* difficulty for a TLAPS-fluent prover with the + community modules; reality routinely surprises. Several Band-T/E items + can blow up if the spec embeds something like `IsFiniteSet` or + `Cardinality` whose unfolding is awkward. +- Many "stated" theorems re-appear (the same property proved in a companion + `_proof.tla`); I de-duplicated the obvious cases (`EWD687a`, `EWD840`, + `Reachable`, `EWD998 → TD!Spec`) but a handful of `Voting`/`Paxos` + invariants are essentially shadowed by `byzpaxos/VoteProof.tla` and + would transfer with light edits. +- The Allocator and `WriteThroughCache` families dominate Band H/VH — + they're well-known textbook benchmarks that nobody has machine-checked + in this repo yet. +- This document is a snapshot; it should be regenerated when new specs + are added or new proofs land. The extraction script lives in commit + history (or can be re-derived: walk `*.tla`, classify each `THEOREM`'s + proof status as `BY` / structured / `OMITTED` / stated-only, exclude + `.tlacache/`). diff --git a/README.md b/README.md index 8b7e1588..e89af0eb 100644 --- a/README.md +++ b/README.md @@ -38,12 +38,12 @@ Here is a list of specs included in this repository which are validated by the C | [The Die Hard Problem](specifications/DieHard) | Leslie Lamport | ✔ | | | ✔ | ✔ | | [The Prisoners & Switches Puzzle](specifications/Prisoners) | Leslie Lamport | ✔ | | | ✔ | | | [The Prisoners & Switch Puzzle](specifications/Prisoners_Single_Switch) | Florian Schanda | ✔ | | | ✔ | | -| [Specs from Specifying Systems](specifications/SpecifyingSystems) | Leslie Lamport | ✔ | | | ✔ | ✔ | +| [Specs from Specifying Systems](specifications/SpecifyingSystems) | Leslie Lamport | ✔ | (✔) | | ✔ | ✔ | | [The Tower of Hanoi Puzzle](specifications/tower_of_hanoi) | Markus Kuppe, Alexander Niederbühl | ✔ | | | ✔ | | | [Missionaries and Cannibals](specifications/MissionariesAndCannibals) | Leslie Lamport | ✔ | | | ✔ | ✔ | | [Stone Scale Puzzle](specifications/Stones) | Leslie Lamport | ✔ | | | ✔ | | | [The Coffee Can Bean Problem](specifications/CoffeeCan) | Andrew Helwer | ✔ | | | ✔ | ✔ | -| [EWD687a: Detecting Termination in Distributed Computations](specifications/ewd687a) | Stephan Merz, Leslie Lamport, Markus Kuppe | ✔ | | (✔) | ✔ | | +| [EWD687a: Detecting Termination in Distributed Computations](specifications/ewd687a) | Stephan Merz, Leslie Lamport, Markus Kuppe | ✔ | ✔ | (✔) | ✔ | | | [The Moving Cat Puzzle](specifications/Moving_Cat_Puzzle) | Florian Schanda | ✔ | | | ✔ | ✔ | | [The Boulangerie Algorithm](specifications/Bakery-Boulangerie) | Leslie Lamport, Stephan Merz | | ✔ | ✔ | ✔ | | | [Misra Reachability Algorithm](specifications/MisraReachability) | Leslie Lamport | | ✔ | ✔ | ✔ | ✔ | @@ -61,14 +61,14 @@ Here is a list of specs included in this repository which are validated by the C | [Dijkstra's Mutual Exclusion Algorithm](specifications/dijkstra-mutex) | Leslie Lamport | | | ✔ | ✔ | | | [The Echo Algorithm](specifications/echo) | Stephan Merz | | | ✔ | ✔ | | | [The TLC Safety Checking Algorithm](specifications/TLC) | Markus Kuppe | | | ✔ | ✔ | | -| [Transaction Commit Models](specifications/transaction_commit) | Leslie Lamport, Jim Gray, Murat Demirbas | | | ✔ | ✔ | ✔ | +| [Transaction Commit Models](specifications/transaction_commit) | Leslie Lamport, Jim Gray, Murat Demirbas | | (✔) | ✔ | ✔ | ✔ | | [The Slush Protocol](specifications/SlushProtocol) | Andrew Helwer | | | ✔ | ✔ | | | [Minimal Circular Substring](specifications/LeastCircularSubstring) | Andrew Helwer | | | ✔ | ✔ | | -| [Snapshot Key-Value Store](specifications/KeyValueStore) | Andrew Helwer, Murat Demirbas | | | ✔ | ✔ | | +| [Snapshot Key-Value Store](specifications/KeyValueStore) | Andrew Helwer, Murat Demirbas | | ✔ | ✔ | ✔ | | | [Chang-Roberts Algorithm for Leader Election in a Ring](specifications/chang_roberts) | Stephan Merz | | | ✔ | ✔ | ✔ | | [MultiPaxos in SMR-Style](specifications/MultiPaxos-SMR) | Guanzhou Hu | | | ✔ | ✔ | | | [Einstein's Riddle](specifications/EinsteinRiddle) | Isaac DeFrain, Giuliano Losa | | | | | ✔ | -| [Resource Allocator](specifications/allocator) | Stephan Merz | | | | ✔ | | +| [Resource Allocator](specifications/allocator) | Stephan Merz | | (✔) | | ✔ | | | [Transitive Closure](specifications/TransitiveClosure) | Stephan Merz | | | | ✔ | | | [Atomic Commitment Protocol](specifications/acp) | Stephan Merz | | | | ✔ | ✔ | | [SWMR Shared Memory Disk Paxos](specifications/diskpaxos) | Leslie Lamport, Giuliano Losa | | | | ✔ | | @@ -97,7 +97,7 @@ Here is a list of specs included in this repository which are validated by the C | [Conway's Game of Life](specifications/GameOfLife) | Mariusz Ryndzionek | | | | ✔ | | | [Chameneos, a Concurrency Game](specifications/Chameneos) | Mariusz Ryndzionek | | | | ✔ | | | [PCR Testing for Snippets of DNA](specifications/glowingRaccoon) | Martin Harrison | | | | ✔ | ✔ | -| [RFC 3506: Voucher Transaction System](specifications/byihive) | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani | | | | ✔ | | +| [RFC 3506: Voucher Transaction System](specifications/byihive) | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani | | (✔) | | ✔ | | | [Yo-Yo Leader Election](specifications/YoYo) | Ludovic Yvoz, Stephan Merz | | | | ✔ | | | [TCP as defined in RFC 9293](specifications/tcp) | Markus Kuppe | | | | ✔ | ✔ | | [B-trees](specifications/btree) | Lorin Hochstein | | | | ✔ | | 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/KeyValueStore/manifest.json b/specifications/KeyValueStore/manifest.json index 0cc8f1bf..3078f129 100644 --- a/specifications/KeyValueStore/manifest.json +++ b/specifications/KeyValueStore/manifest.json @@ -28,6 +28,14 @@ "features": [], "models": [] }, + { + "path": "specifications/KeyValueStore/KeyValueStore_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:05" + } + }, { "path": "specifications/KeyValueStore/MCKVS.tla", "features": [], diff --git a/specifications/MisraReachability/ParReachProofs.tla b/specifications/MisraReachability/ParReachProofs.tla index 4cba9ba2..15d57e5c 100644 --- a/specifications/MisraReachability/ParReachProofs.tla +++ b/specifications/MisraReachability/ParReachProofs.tla @@ -15,7 +15,7 @@ LEMMA TypeInvariant == Spec => []Inv <1>3. QED BY <1>1, <1>2, PTL DEF Spec -THEOREM Spec => R!Init /\ [][R!Next]_R!vars +THEOREM RefinementSafety == Spec => R!Init /\ [][R!Next]_R!vars <1>1. Init => R!Init BY ProcsAssump DEF Init, R!Init, pcBar, vrootBar, ProcSet <1>2. Inv /\ [Next]_vars => [R!Next]_R!vars diff --git a/specifications/MisraReachability/ReachableProofs.tla b/specifications/MisraReachability/ReachableProofs.tla index 5015bd06..9a83b868 100644 --- a/specifications/MisraReachability/ReachableProofs.tla +++ b/specifications/MisraReachability/ReachableProofs.tla @@ -194,7 +194,7 @@ THEOREM Thm3 == Spec => []Inv3 BY <1>1, <1>2, Thm2, PTL DEF Spec -THEOREM Spec => []((pc = "Done") => (marked = Reachable)) +THEOREM Thm4 == Spec => []((pc = "Done") => (marked = Reachable)) (*************************************************************************) (* This theorem follows easily from the invariance of Inv1 and Inv3 and *) (* the trivial result Reachable3 of module ReachabilityProofs that *) @@ -209,6 +209,13 @@ THEOREM Spec => []((pc = "Done") => (marked = Reachable)) BY Reachable3 DEF Inv3 <1>3. QED BY <1>1, <1>2, Thm1, Thm3, PTL + +(***************************************************************************) +(* The same property restated under the spec's PartialCorrectness name, *) +(* matching the THEOREM stub at the bottom of Reachable.tla. *) +(***************************************************************************) +THEOREM PartialCorrectnessThm == Spec => []PartialCorrectness +BY Thm4, PTL DEF PartialCorrectness ============================================================================= \* Modification History \* Last modified Sun Apr 14 16:24:32 PDT 2019 by lamport diff --git a/specifications/PaxosHowToWinATuringAward/Voting.tla b/specifications/PaxosHowToWinATuringAward/Voting.tla index 9b22ef92..e1e98494 100644 --- a/specifications/PaxosHowToWinATuringAward/Voting.tla +++ b/specifications/PaxosHowToWinATuringAward/Voting.tla @@ -25,7 +25,8 @@ CONSTANTS Value, Acceptor, Quorum (* element (an acceptor) in common. Think of a quorum as a set consisting *) (* of a majority (more than half) of the acceptors. *) (***************************************************************************) -ASSUME /\ \A Q \in Quorum : Q \subseteq Acceptor +ASSUME QuorumAssumption == + /\ \A Q \in Quorum : Q \subseteq Acceptor /\ \A Q1, Q2 \in Quorum : Q1 \cap Q2 /= {} (***************************************************************************) 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/PaxosHowToWinATuringAward/manifest.json b/specifications/PaxosHowToWinATuringAward/manifest.json index d62f67c0..9420690c 100644 --- a/specifications/PaxosHowToWinATuringAward/manifest.json +++ b/specifications/PaxosHowToWinATuringAward/manifest.json @@ -78,6 +78,14 @@ "proof": { "runtime": "00:00:01" } + }, + { + "path": "specifications/PaxosHowToWinATuringAward/Voting_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:30" + } } ] -} \ No newline at end of file +} 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/SpecifyingSystems/manifest.json b/specifications/SpecifyingSystems/manifest.json index d39248dc..c045c9d1 100644 --- a/specifications/SpecifyingSystems/manifest.json +++ b/specifications/SpecifyingSystems/manifest.json @@ -110,6 +110,14 @@ } ] }, + { + "path": "specifications/SpecifyingSystems/AsynchronousInterface/AsynchInterface_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:01" + } + }, { "path": "specifications/SpecifyingSystems/AsynchronousInterface/Channel.tla", "features": [], @@ -125,6 +133,14 @@ } ] }, + { + "path": "specifications/SpecifyingSystems/AsynchronousInterface/Channel_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:01" + } + }, { "path": "specifications/SpecifyingSystems/AsynchronousInterface/PrintValues.tla", "features": [], @@ -145,6 +161,14 @@ "features": [], "models": [] }, + { + "path": "specifications/SpecifyingSystems/CachingMemory/InternalMemory_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:02" + } + }, { "path": "specifications/SpecifyingSystems/CachingMemory/MCInternalMemory.tla", "features": [], @@ -234,6 +258,14 @@ "features": [], "models": [] }, + { + "path": "specifications/SpecifyingSystems/Composing/Channel_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:01" + } + }, { "path": "specifications/SpecifyingSystems/Composing/CompositeFIFO.tla", "features": [], @@ -244,11 +276,27 @@ "features": [], "models": [] }, + { + "path": "specifications/SpecifyingSystems/Composing/HourClock_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:01" + } + }, { "path": "specifications/SpecifyingSystems/Composing/InternalMemory.tla", "features": [], "models": [] }, + { + "path": "specifications/SpecifyingSystems/Composing/InternalMemory_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:02" + } + }, { "path": "specifications/SpecifyingSystems/Composing/JointActionMemory.tla", "features": [], @@ -312,6 +360,14 @@ "features": [], "models": [] }, + { + "path": "specifications/SpecifyingSystems/FIFO/Channel_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:01" + } + }, { "path": "specifications/SpecifyingSystems/FIFO/FIFO.tla", "features": [], @@ -327,6 +383,14 @@ "features": [], "models": [] }, + { + "path": "specifications/SpecifyingSystems/FIFO/InnerFIFO_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:01" + } + }, { "path": "specifications/SpecifyingSystems/FIFO/MCInnerFIFO.tla", "features": [], @@ -396,6 +460,14 @@ } ] }, + { + "path": "specifications/SpecifyingSystems/HourClock/HourClock_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:01" + } + }, { "path": "specifications/SpecifyingSystems/Liveness/APHourClock.tla", "features": [], @@ -425,11 +497,27 @@ "features": [], "models": [] }, + { + "path": "specifications/SpecifyingSystems/Liveness/HourClock_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:01" + } + }, { "path": "specifications/SpecifyingSystems/Liveness/InternalMemory.tla", "features": [], "models": [] }, + { + "path": "specifications/SpecifyingSystems/Liveness/InternalMemory_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:02" + } + }, { "path": "specifications/SpecifyingSystems/Liveness/LiveHourClock.tla", "features": [], @@ -510,11 +598,27 @@ "features": [], "models": [] }, + { + "path": "specifications/SpecifyingSystems/RealTime/HourClock_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:01" + } + }, { "path": "specifications/SpecifyingSystems/RealTime/InternalMemory.tla", "features": [], "models": [] }, + { + "path": "specifications/SpecifyingSystems/RealTime/InternalMemory_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:02" + } + }, { "path": "specifications/SpecifyingSystems/RealTime/MCRealTime.tla", "features": [], @@ -652,6 +756,14 @@ "features": [], "models": [] }, + { + "path": "specifications/SpecifyingSystems/TLC/AlternatingBit_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:15" + } + }, { "path": "specifications/SpecifyingSystems/TLC/BNFGrammars.tla", "features": [], @@ -678,4 +790,4 @@ ] } ] -} \ No newline at end of file +} diff --git a/specifications/TwoPhase/TwoPhase.tla b/specifications/TwoPhase/TwoPhase.tla index cf9bd632..03768a68 100644 --- a/specifications/TwoPhase/TwoPhase.tla +++ b/specifications/TwoPhase/TwoPhase.tla @@ -19,7 +19,7 @@ (* specification under a suitable refinement mapping (substitution for the *) (* variable v). *) (***************************************************************************) -EXTENDS Naturals, TLAPS +EXTENDS Naturals CONSTANT XInit(_), XAct(_, _, _) @@ -67,30 +67,11 @@ vBar == (p + c) % 2 A == INSTANCE Alternate WITH v <- vBar (***************************************************************************) -(* 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 states that specification Spec implements *) +(* specification A!Spec. The TLAPS proof of this theorem is in module *) +(* TwoPhase_proof. *) (***************************************************************************) THEOREM Implementation == Spec => A!Spec -<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 - + ============================================================== \* Generated at Sat Oct 31 03:15:55 PDT 2009 diff --git a/specifications/TwoPhase/TwoPhase_proof.tla b/specifications/TwoPhase/TwoPhase_proof.tla new file mode 100644 index 00000000..7931eef1 --- /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 == Spec => A!Spec +<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/TwoPhase/manifest.json b/specifications/TwoPhase/manifest.json index c76a535b..3631ee72 100644 --- a/specifications/TwoPhase/manifest.json +++ b/specifications/TwoPhase/manifest.json @@ -29,6 +29,11 @@ { "path": "specifications/TwoPhase/TwoPhase.tla", "features": [], + "models": [] + }, + { + "path": "specifications/TwoPhase/TwoPhase_proof.tla", + "features": [], "models": [], "proof": { "runtime": "00:00:01" 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/allocator/manifest.json b/specifications/allocator/manifest.json index 5694c293..4d8fa266 100644 --- a/specifications/allocator/manifest.json +++ b/specifications/allocator/manifest.json @@ -20,6 +20,14 @@ } ] }, + { + "path": "specifications/allocator/AllocatorImplementation_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:30" + } + }, { "path": "specifications/allocator/AllocatorRefinement.tla", "features": [], @@ -50,6 +58,14 @@ } ] }, + { + "path": "specifications/allocator/SchedulingAllocator_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:30" + } + }, { "path": "specifications/allocator/SimpleAllocator.tla", "features": [], @@ -64,6 +80,14 @@ "stateDepth": 6 } ] + }, + { + "path": "specifications/allocator/SimpleAllocator_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:10" + } } ] -} \ No newline at end of file +} 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/byihive/manifest.json b/specifications/byihive/manifest.json index 1b2c8ed5..5d881e7d 100644 --- a/specifications/byihive/manifest.json +++ b/specifications/byihive/manifest.json @@ -54,6 +54,14 @@ } ] }, + { + "path": "specifications/byihive/VoucherLifeCycle_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:01" + } + }, { "path": "specifications/byihive/VoucherRedeem.tla", "features": [], diff --git a/specifications/ewd687a/EWD687a.tla b/specifications/ewd687a/EWD687a.tla index 1df5e391..c7cbd999 100644 --- a/specifications/ewd687a/EWD687a.tla +++ b/specifications/ewd687a/EWD687a.tla @@ -123,7 +123,8 @@ OutEdges(p) == {e \in Edges : e[1] = p} (* something that was not stated explicitly: that a process can't send *) (* messages to itself, so an edge joins two different processes. *) (***************************************************************************) -ASSUME /\ \* Every edge is a pair of distinct processes +ASSUME EdgeFacts == + /\ \* Every edge is a pair of distinct processes \A e \in Edges : /\ (e \in Procs \X Procs) /\ (e[1] # e[2]) 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/ewd687a/manifest.json b/specifications/ewd687a/manifest.json index bc2154e9..9814b220 100644 --- a/specifications/ewd687a/manifest.json +++ b/specifications/ewd687a/manifest.json @@ -15,6 +15,14 @@ "features": [], "models": [] }, + { + "path": "specifications/ewd687a/EWD687a_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:01:00" + } + }, { "path": "specifications/ewd687a/EWD687aPlusCal.tla", "features": [ diff --git a/specifications/transaction_commit/MCTwoPhaseApa.tla b/specifications/transaction_commit/MCTwoPhaseApa.tla new file mode 100644 index 00000000..3c45cf57 --- /dev/null +++ b/specifications/transaction_commit/MCTwoPhaseApa.tla @@ -0,0 +1,141 @@ +------------------------ MODULE MCTwoPhaseApa ------------------------------ +(***************************************************************************) +(* Self-contained Apalache wrapper for TwoPhase.tla used to validate the *) +(* candidate inductive invariant for TPSpec => []TC!TCConsistent. *) +(* *) +(* Two queries (per Konnov/Kuppe/Merz, arXiv:2211.07216 Sect. 3.2): *) +(* TPInit /\ [TPNext]_vars |=0 Inv (initial states satisfy Inv) *) +(* Inv /\ [TPNext]_vars |=1 Inv (Inv is preserved by one step) *) +(* *) +(* TwoPhase's Message set is a heterogeneous record union *) +(* [type:{"Prepared"}, rm:RM] \cup [type:{"Commit","Abort"}] *) +(* which Apalache's row-typed records cannot represent directly. We *) +(* widen the type uniformly to *) +(* { type: Str, rm: Str } *) +(* and pad Commit/Abort messages with a sentinel rm = "_" that is not a *) +(* member of RM. This is conservative: the post-state set of behaviours *) +(* of the widened spec is a superset of the original's, so an Apalache *) +(* "no counter-example" answer carries over to the original spec. *) +(***************************************************************************) +EXTENDS Naturals + +\* @type: Set(Str); +RM == { "r1", "r2", "r3" } + +NoRm == "_" + +\* @type: Set({type: Str, rm: Str}); +Message == + [type: {"Prepared"}, rm: RM] \cup [type: {"Commit", "Abort"}, rm: {NoRm}] + +CommitMsg == [type |-> "Commit", rm |-> NoRm] +AbortMsg == [type |-> "Abort", rm |-> NoRm] +PrepMsg(rm) == [type |-> "Prepared", rm |-> rm] + +VARIABLES + \* @type: Str -> Str; + rmState, + \* @type: Str; + tmState, + \* @type: Set(Str); + tmPrepared, + \* @type: Set({type: Str, rm: Str}); + msgs + +vars == << rmState, tmState, tmPrepared, msgs >> + +TPTypeOK == + /\ rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] + /\ tmState \in {"init", "committed", "aborted"} + /\ tmPrepared \subseteq RM + /\ msgs \subseteq Message + +TPInit == + /\ rmState = [rm \in RM |-> "working"] + /\ tmState = "init" + /\ tmPrepared = {} + /\ msgs = {} + +TMRcvPrepared(rm) == + /\ tmState = "init" + /\ PrepMsg(rm) \in msgs + /\ tmPrepared' = tmPrepared \cup {rm} + /\ UNCHANGED <> + +TMCommit == + /\ tmState = "init" + /\ tmPrepared = RM + /\ tmState' = "committed" + /\ msgs' = msgs \cup {CommitMsg} + /\ UNCHANGED <> + +TMAbort == + /\ tmState = "init" + /\ tmState' = "aborted" + /\ msgs' = msgs \cup {AbortMsg} + /\ UNCHANGED <> + +RMPrepare(rm) == + /\ rmState[rm] = "working" + /\ rmState' = [rmState EXCEPT ![rm] = "prepared"] + /\ msgs' = msgs \cup {PrepMsg(rm)} + /\ UNCHANGED <> + +RMChooseToAbort(rm) == + /\ rmState[rm] = "working" + /\ rmState' = [rmState EXCEPT ![rm] = "aborted"] + /\ UNCHANGED <> + +RMRcvCommitMsg(rm) == + /\ CommitMsg \in msgs + /\ rmState' = [rmState EXCEPT ![rm] = "committed"] + /\ UNCHANGED <> + +RMRcvAbortMsg(rm) == + /\ AbortMsg \in msgs + /\ rmState' = [rmState EXCEPT ![rm] = "aborted"] + /\ UNCHANGED <> + +TPNext == + \/ TMCommit \/ TMAbort + \/ \E rm \in RM : + TMRcvPrepared(rm) \/ RMPrepare(rm) \/ RMChooseToAbort(rm) + \/ RMRcvCommitMsg(rm) \/ RMRcvAbortMsg(rm) + +(***************************************************************************) +(* The candidate inductive invariant *) +(***************************************************************************) +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 + +(***************************************************************************) +(* Inductive-step init action that explicitly assigns each variable from *) +(* its TPTypeOK domain and then constrains the result to satisfy Inv. *) +(* Apalache's assignment-finder is happier with this form than with using *) +(* Inv itself as init. *) +(***************************************************************************) +InvInit == + /\ rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] + /\ tmState \in {"init", "committed", "aborted"} + /\ tmPrepared \in SUBSET RM + /\ msgs \in SUBSET Message + /\ Inv + +(***************************************************************************) +(* Goal property: no two RMs end up with conflicting decisions. *) +(***************************************************************************) +TCConsistent == + \A rm1, rm2 \in RM : ~ (rmState[rm1] = "aborted" /\ rmState[rm2] = "committed") + +============================================================================= diff --git a/specifications/transaction_commit/PaxosCommit.tla b/specifications/transaction_commit/PaxosCommit.tla index c91ae8b8..f868f291 100644 --- a/specifications/transaction_commit/PaxosCommit.tla +++ b/specifications/transaction_commit/PaxosCommit.tla @@ -44,7 +44,8 @@ CONSTANT RM, \* The set of resource managers. Majority, \* The set of majorities of acceptors Ballot \* The set of ballot numbers -ASSUME \* We assume these properties of the declared constants. +ASSUME PaxosCommitAssumptions == + \* We assume these properties of the declared constants. /\ Ballot \subseteq Nat /\ 0 \in Ballot /\ Majority \subseteq SUBSET Acceptor 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 + +============================================================================ diff --git a/specifications/transaction_commit/manifest.json b/specifications/transaction_commit/manifest.json index 5b79e51f..04ed78eb 100644 --- a/specifications/transaction_commit/manifest.json +++ b/specifications/transaction_commit/manifest.json @@ -40,6 +40,11 @@ } ] }, + { + "path": "specifications/transaction_commit/MCTwoPhaseApa.tla", + "features": [], + "models": [] + }, { "path": "specifications/transaction_commit/PaxosCommit.tla", "features": [], @@ -55,6 +60,14 @@ } ] }, + { + "path": "specifications/transaction_commit/PaxosCommit_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:01" + } + }, { "path": "specifications/transaction_commit/TCommit.tla", "features": [], @@ -70,6 +83,14 @@ } ] }, + { + "path": "specifications/transaction_commit/TCommit_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:01" + } + }, { "path": "specifications/transaction_commit/TwoPhase.tla", "features": [], @@ -84,6 +105,14 @@ "stateDepth": 11 } ] + }, + { + "path": "specifications/transaction_commit/TwoPhase_proof.tla", + "features": [], + "models": [], + "proof": { + "runtime": "00:00:30" + } } ] -} \ No newline at end of file +}