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 <noreply@anthropic.com>

1 files changed, 62 insertions, 0 deletions

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.