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

diff --git a/formal/README.md b/formal/README.md
new file mode 100644
index 0000000..f667bdf
--- /dev/null
+++ b/formal/README.md
@@ -0,0 +1,59 @@
+# Gobra deductive proof
+
+`insertion.go` is a **machine-checked** proof that an insertion sort is correct,
+verified by [Gobra](https://github.com/viperproject/gobra) — ETH Zurich's
+deductive verifier for Go, which translates annotated Go to the Viper
+intermediate language and discharges the proof obligations with the Z3 SMT
+solver.
+
+Unlike the TLA+ model (which checks a hand-written abstraction) and the property
+tests (which sample inputs), this verifies the **actual Go source** for **all**
+inputs. Gobra proves two things about `Insertion`:
+
+1. **Memory safety** — every index access is in bounds. The permission
+   invariants `forall k :: 0 <= k < len(a) ==> acc(&a[k])` carry write access to
+   every element through both loops; Go itself cannot prove the absence of
+   index-out-of-range panics, Gobra can.
+2. **Ordering** — on return `a` is sorted ascending
+   (`forall p < q :: a[p] <= a[q]`), established via the two insertion-sort loop
+   invariants in the annotations.
+
+The **permutation** half of full correctness (output is a rearrangement of the
+input) is intentionally left to the property tests and the paper proof in
+[`docs/verification.md`](../docs/verification.md); proving it in Gobra needs
+ghost multiset state and is noted there as future work.
+
+## Why a separate, non-generic copy?
+
+Gobra's support for Go generics and method-based abstractions is limited, so
+this file is a deliberately monomorphized copy of `sort.Insertion`
+([`sort/insertion.go`](../sort/insertion.go)): plain `[]int` instead of
+`ds.ArrayList[V]`, and an inlined swap instead of the `.Swap` method. The
+algorithm is otherwise identical.
+
+## Running
+
+Gobra is distributed as a container image (it bundles its own Z3, so no separate
+solver install is needed). With `podman` (or `docker`):
+
+```sh
+podman pull ghcr.io/viperproject/gobra:latest
+make verify-formal
+```
+
+or directly:
+
+```sh
+podman run --rm -v "$PWD/formal:/gobra/formal:z" \
+  ghcr.io/viperproject/gobra:latest -i /gobra/formal/insertion.go
+```
+
+Expected output ends with:
+
+```
+Gobra found 0 errors.
+```
+
+To convince yourself the proof is not vacuous, flip the inner comparison
+`a[j] < a[j-1]` to `>` and re-run: Gobra reports
+`Loop invariant might not be preserved`.