|
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>
|
