Close verification-coverage gaps; harness finds two more bugsHEADmaster

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>

1 files changed, 21 insertions, 4 deletions

diff --git a/formal/tla/README.md b/formal/tla/README.md
index a80c687..16a6744 100644
--- a/formal/tla/README.md
+++ b/formal/tla/README.md
@@ -1,8 +1,25 @@
-# TLA+ model check of sleep sort
+# TLA+ model checks of the concurrent sorts
 
-`SleepSort.tla` is a [TLA+](https://lamport.azurewebsites.net/tla/tla.html)
-model of the concurrent sleep sort in [`sort/sleep.go`](../../sort/sleep.go),
-checked exhaustively by the TLC model checker.
+Two [TLA+](https://lamport.azurewebsites.net/tla/tla.html) models, checked
+exhaustively by the TLC model checker:
+
+- **`SleepSort.tla`** — the sleep sort in [`sort/sleep.go`](../../sort/sleep.go).
+- **`ParallelSort.tla`** — the fork/join structure shared by
+  [`sort/parallelmerge.go`](../../sort/parallelmerge.go) and
+  [`sort/parallelquick.go`](../../sort/parallelquick.go): checks that
+  concurrently-writing tasks own **disjoint** array ranges (no data race) and
+  that the join always completes (termination). Removing the WaitGroup fence
+  (letting a parent merge before its children finish) makes TLC report
+  `Invariant NoDataRace is violated` — so the check has teeth. This model
+  complements the dynamic race detector (`make verify`) with an *exhaustive*
+  guarantee over the whole recursion tree.
+
+The rest of this file documents `SleepSort.tla`.
+
+## SleepSort
+
+`SleepSort.tla` models the concurrent sleep sort in
+[`sort/sleep.go`](../../sort/sleep.go).
 
 ## What this does and does NOT prove