diff options
| author | Paul Buetow <paul@buetow.org> | 2026-07-06 10:32:34 +0300 |
|---|---|---|
| committer | Paul Buetow <paul@buetow.org> | 2026-07-06 10:32:34 +0300 |
| commit | 3f906d03262150892e2297e621bfc56e425ef142 (patch) | |
| tree | 79d69a4b011882716626565c27793ce04532227e /Makefile | |
| parent | f74812f8eda48194b622bdd318f35d3a6b6328cd (diff) | |
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>
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 8 |
1 files changed, 6 insertions, 2 deletions
@@ -16,15 +16,19 @@ verify: # (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 \ + -metadir /tmp/tlc-sleepsort \ -config formal/tla/SleepSort.cfg formal/tla/SleepSort.tla + java -cp $(HOME)/tools/tlaplus/tla2tools.jar tlc2.TLC -workers auto \ + -metadir /tmp/tlc-parallelsort \ + -config formal/tla/ParallelSort.cfg formal/tla/ParallelSort.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 + ghcr.io/viperproject/gobra:latest \ + -i /gobra/formal/insertion.go /gobra/formal/selection.go bench: go test -run=xxx -bench=. ./... | tee bench.out sortbench: |