From f74812f8eda48194b622bdd318f35d3a6b6328cd Mon Sep 17 00:00:00 2001 From: Paul Buetow Date: Mon, 6 Jul 2026 10:15:56 +0300 Subject: Add layered formal-verification harness Adds four complementary layers to verify correctness, all runnable locally, weakest-but-broadest to strongest-but-narrowest: 0. Paper proofs (docs/verification.md): Hoare invariants, termination measures, and permutation arguments for every algorithm. 1. Property tests (sort/property_test.go): testing/quick asserting ordering AND permutation for every sort. Closes a real gap -- the existing tests only checked .Sorted(), so a sort dropping/duplicating elements passed. 2. make verify: go vet + staticcheck + go test -race -short, with -short gating of the large sizes in sort/search tests so the race build is quick. 3. make verify-model: TLA+/TLC model check of sleep sort (termination, deadlock-freedom, sorted permutation) -- formal/tla/. 4. make verify-formal: Gobra deductive proof (Viper+Z3) that a monomorphized insertion sort is memory-safe and sorted for all inputs -- formal/. The static layer already found a latent bug: hash() used key<<10 on a generic integer, which silently yields 0 for narrow key types (int8), degrading the hash. Tests missed it because they only use int keys. Fixed by mixing in int64; documented extensively in docs/case-study-hash-shift-bug.md. Also cleans up dead code and a blank-identifier range flagged by staticcheck. Co-Authored-By: Claude Opus 4.8 --- formal/tla/README.md | 62 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 formal/tla/README.md (limited to 'formal/tla/README.md') diff --git a/formal/tla/README.md b/formal/tla/README.md new file mode 100644 index 0000000..a80c687 --- /dev/null +++ b/formal/tla/README.md @@ -0,0 +1,62 @@ +# TLA+ model check of sleep sort + +`SleepSort.tla` is a [TLA+](https://lamport.azurewebsites.net/tla/tla.html) +model of the concurrent sleep sort in [`sort/sleep.go`](../../sort/sleep.go), +checked exhaustively by the TLC model checker. + +## What this does and does NOT prove + +Model checking verifies a **hand-written model**, not the Go source. TLC +explores *every* reachable state of the model and confirms: + +- **`OutputSorted`** (safety) — the collected output is always non-decreasing. +- **`PermutationWhenDone`** (safety) — the output is a multiset permutation of + the input; nothing is dropped, duplicated, or invented. +- **`Terminates`** (liveness) — the collector eventually receives every value: + no deadlock and no value left sleeping forever. + +The gap you keep responsibility for: that the model faithfully abstracts +`sleep.go`. The model represents the sleeps as a discrete clock and the +unbuffered channel + `WaitGroup` as an urgent single-value rendezvous — see the +header comment in `SleepSort.tla`. + +Sortedness is **not** assumed. It emerges from one rule: time cannot pass while +a fired-but-unreceived timer waits (`Tick`'s urgency guard). Delete that guard +and TLC finds an unsorted counterexample — proof the check has teeth. + +## Running + +Needs Java and `tla2tools.jar` (download once): + +```sh +mkdir -p ~/tools/tlaplus +curl -fsSL -o ~/tools/tlaplus/tla2tools.jar \ + https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar +``` + +Then, from the repository root: + +```sh +make verify-model +``` + +or directly: + +```sh +java -cp ~/tools/tlaplus/tla2tools.jar tlc2.TLC \ + -config formal/tla/SleepSort.cfg formal/tla/SleepSort.tla +``` + +Expected output ends with: + +``` +Model checking completed. No error has been found. +``` + +## The input + +`SleepSort.cfg` checks the input `<<3, 1, 4, 1, 2>>` (defined as `InputValue` +in the module, because a `.cfg` cannot hold a sequence literal). It has a +duplicate and is out of order — enough to exercise ordering, ties, and +termination. Edit `InputValue` in `SleepSort.tla` to try others; the state space +stays small because the clock never exceeds the largest input value. -- cgit v1.2.3