|
Extends the verification harness from sorts-only to the whole repo, and in
doing so surfaces two further latent bugs (on top of the earlier hash-shift one):
Bugs found and fixed:
- queue/elementarypriority.go: max() seeded at the zero value, so an
all-negative queue reported a phantom max of 0 and DeleteMax returned/removed
the wrong element. Caught by the new queue permutation property (testing/quick
generates negatives; the old test data never did). Seed from a[0] instead.
- sort/sleep.go: result built on NewArrayList(len(a)) -- a slice of that LENGTH
(len(a) zeros) -- then appended to, yielding double-length output with leading
zeros. The old .Sorted()-only test passed because zeros-then-ascending is
sorted. Caught by the new Sleep permutation check. Build from an empty slice.
Coverage added:
- queue/property_test.go: ordering + permutation (completeness) for both queues.
- TestSleepSort now also checks permutation, not just Sorted().
- docs/verification.md: paper proofs for all search/set structures (Elementary,
Hash, BST, red-black BST invariants, GoMap) and both priority queues.
- formal/tla/ParallelSort.tla: exhaustive fork/join model of ParallelMerge/
ParallelQuick -- disjoint write-ranges (no data race) + termination. Wired
into make verify-model.
- formal/selection.go: second Gobra proof (memory safety + sortedness). Wired
into make verify-formal.
- docs/case-study-bugs-found.md: extensive write-up of all three bugs, how each
was caught, why the old tests missed it, and the fix (supersedes the earlier
single-bug case study).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
|
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>
|
