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, 24 insertions, 0 deletions

diff --git a/Makefile b/Makefile
index fab5d52..8632e8c 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,30 @@
 test:
 	go clean -testcache
 	go test ./... -v
+
+# verify: static + dynamic correctness checks. Fast enough for routine use.
+#   go vet / staticcheck  - static analysis
+#   go test -race -short  - race detector over the (size-capped) test + property
+#                           suites; -short keeps the million-element cases out so
+#                           the race build stays quick. See docs/verification.md.
+verify:
+	go vet ./...
+	staticcheck ./...
+	go test -race -short ./...
+
+# verify-model: exhaustively model-check the concurrent sleep sort with TLA+/TLC
+# (a model of sort/sleep.go, not the Go code itself). See formal/tla/README.md.
+verify-model:
+	java -cp $(HOME)/tools/tlaplus/tla2tools.jar tlc2.TLC -workers auto \
+		-metadir /tmp/tlc-algorithms \
+		-config formal/tla/SleepSort.cfg formal/tla/SleepSort.tla
+
+# verify-formal: machine-checked deductive proof of a monomorphized insertion
+# sort with Gobra (Go verifier, Viper+Z3 backend), run from its container image.
+# See formal/README.md.
+verify-formal:
+	podman run --rm -v $(PWD)/formal:/gobra/formal:z \
+		ghcr.io/viperproject/gobra:latest -i /gobra/formal/insertion.go
 bench:
 	go test -run=xxx -bench=. ./... | tee bench.out
 sortbench: