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, 201 insertions, 12 deletions

diff --git a/docs/verification.md b/docs/verification.md
index 3959e5b..e845d79 100644
--- a/docs/verification.md
+++ b/docs/verification.md
@@ -1,21 +1,28 @@
 # Hand-written correctness proofs
 
 This document contains human-written (paper) correctness proofs for the
-algorithms in this repository, derived by reading the actual source. Each proof
-is a Hoare-style argument: a **precondition**, a **postcondition**, one **loop
-invariant** per loop, a **termination measure**, and — for the sorts — a
-**permutation argument**.
+algorithms in this repository, derived by reading the actual source. It covers
+the **sorts**, the **search/set structures**, and the **priority queues**. Each
+proof is a Hoare-style argument: a **precondition**, a **postcondition**, the
+relevant **invariant** (loop invariant, BST order, heap order, …), a
+**termination measure**, and — where relevant — a **permutation argument**.
 
 These proofs are the human-readable source of truth. They are *human-checked*,
 not machine-checked; the automated layers corroborate them:
 
-- `sort/property_test.go` checks *ordering* **and** *permutation* on thousands
-  of random inputs (empirical corroboration — see the "permutation" note below).
-- `make verify` runs `go vet`, `staticcheck`, and the race detector. This layer
-  already paid off: it caught a latent bug in `search/hash.go` on its first run
-  — see [`case-study-hash-shift-bug.md`](case-study-hash-shift-bug.md).
-- `formal/tla/SleepSort.tla` exhaustively model-checks the concurrent sleep sort.
-- `formal/insertion.go` is a machine-checked (Gobra) proof of insertion sort.
+- `sort/property_test.go` and `queue/property_test.go` check *ordering* **and**
+  *permutation* on thousands of random inputs; `search/search_test.go`
+  oracle-checks the set contract against Go's `map`.
+- `make verify` runs `go vet`, `staticcheck`, and the race detector.
+- `formal/tla/` exhaustively model-checks the concurrent sorts.
+- `formal/` holds machine-checked (Gobra) proofs of the actual source.
+
+**These checks have already found three latent bugs** that the pre-existing
+tests missed (all documented in
+[`case-study-bugs-found.md`](case-study-bugs-found.md)): a width-dependent shift
+in `hash()`, a zero-seed maximum in `ElementaryPriority`, and a double-length
+result in `Sleep`. The last two were caught precisely by the *permutation*
+invariant added here — the pre-existing tests only checked ordering.
 
 ## Common notation and lemmas
 
@@ -237,7 +244,9 @@ operate on **disjoint** subranges:
 Given disjointness + the `WaitGroup` join fence, the parallel executions compute
 the same result as their sequential counterparts, whose correctness is proven
 above. The **race detector** (`make verify`) corroborates the disjointness claim
-dynamically. ∎
+dynamically, and `formal/tla/ParallelSort.tla` model-checks it **exhaustively**
+over the whole recursion tree (no two concurrently-writing tasks overlap; the
+join always completes). ∎
 
 ## Sleep sort — `sort/sleep.go:9`
 
@@ -253,3 +262,183 @@ termination without deadlock) — is **not** something a paper proof can settle
 convincingly. It is instead model-checked exhaustively in
 `formal/tla/SleepSort.tla`, which is the appropriate tool for this coordination
 logic. See that model and its README for the machine-checked result.
+
+Separately from the timing/coordination, the *result assembly* must return
+exactly the received values. The collector starts from an **empty** slice and
+appends each received value, so `perm(out, a₀)` holds and `len(out) = len(a)`.
+(This is what the fixed double-length bug violated — see the case study — and
+what `TestSleepSort`'s permutation check now guards.) ∎
+
+-----------------------------------------------------------------------------
+
+# Part II — Search / set structures
+
+Every type in `search/` implements the same `Set[K,V]` interface
+(`search/set.go`): a partial map from keys to values with `Put`, `Get`, `Del`,
+`Size`, `Empty`. The **contract** each must satisfy — its shared postcondition —
+is that it behaves as a finite map:
+
+- after `Put(k, v)`, `Get(k) = (v, nil)`;
+- if `k` was never put (or was deleted), `Get(k) = (0, NotFound)`;
+- `Del(k)` removes `k` (subsequent `Get(k) = NotFound`) and returns its value;
+- `Size` counts the live keys, `Empty ≡ Size = 0`.
+
+`search/search_test.go` verifies exactly this contract by running each structure
+in lockstep against Go's built-in `map` (an oracle). The proofs below establish
+the **structural invariant** that makes each structure meet the contract.
+
+## GoMap — `search/gomap.go`
+
+A thin wrapper over Go's built-in `map[K]V`. `Put`/`Get`/`Del`/`Size` delegate
+directly to the runtime map, so correctness is inherited from Go's map
+semantics. Serves as the reference oracle in spirit. ∎
+
+## Elementary (unordered linked list) — `search/elementary.go`
+
+**Invariant:** the singly-linked list rooted at `s.root` contains exactly one
+node per live key, and `s.size` equals the node count.
+
+- `Put` (`elementary.go:30`): scans; on a key match, overwrites `val` (no size
+  change — invariant preserved: same key set); on reaching the tail, links a new
+  node and increments `size`. Loop measure: position advances toward the tail.
+- `Get` (`elementary.go:53`): linear scan; returns the value at the matching
+  node or `NotFound`. Correct by the membership invariant.
+- `Del` (`elementary.go:66`): unlinks the matching node (head case via the
+  deferred `s.root = s.root.next`; interior case by splicing `elem.next`),
+  decrements `size`. Preserves the one-node-per-key invariant.
+
+Termination: every loop walks a finite list. Correctness follows because "key is
+in the set" ⟺ "a node with that key is in the list". ∎
+
+## Hash (separate chaining) — `search/hash.go`
+
+**Invariant:** key `k` is stored **iff** it appears in the Elementary list at
+`buckets[hash(k)]`.
+
+Because `hash` (`hash.go:28`) is a deterministic total function `K → [0,
+capacity)`, `Put`, `Get`, and `Del` all probe the **same** bucket for a given
+key, so each reduces to the corresponding Elementary operation *within one
+bucket* — already proven correct above. Collisions are resolved by chaining, so
+correctness holds for **any** deterministic `hash`; the specific mixing function
+affects only the distribution (performance), not correctness.
+
+Caveat established by the verification harness: `hash` must be *well-defined for
+every key width*. The original `key<<10` degenerated to `0` for narrow key types
+(fixed to mix in `int64`); this changed distribution, never the contract. See
+[`case-study-bugs-found.md`](case-study-bugs-found.md). ∎
+
+## BST (unbalanced binary search tree) — `search/bst.go`
+
+**Invariant (BST order):** for every node `n`, all keys in `n.left` are `< n.key`
+and all keys in `n.right` are `> n.key`.
+
+- `search` (`bst.go:125`) walks the tree by the invariant — left when `key <
+  n.key`, right when `key > n.key`, match on equality — and returns either the
+  node or the `**node` slot where a missing key *would* attach. This is correct
+  by the ordering invariant: if `key` exists it lies on exactly this path.
+- `Put` (`bst.go:55`) inserts a new leaf at that empty slot, which by
+  construction sits in the correct ordered position, preserving the invariant;
+  an existing key is left unchanged.
+- `Del` (`bst.go:83`) does **Hibbard deletion**: leaf → detach; one child →
+  splice the child up; two children → replace the node with its **successor**
+  (the minimum of the right subtree, extracted by `deleteMin`), rewiring the
+  successor's children to `n`'s. The successor is greater than everything in
+  `n.left` and less than the rest of `n.right`, so BST order is preserved.
+
+Termination: `search`/`min` descend strictly toward the leaves; the tree height
+is finite. No balancing is performed, so height may be `O(n)` — a *performance*
+property, not a correctness one. ∎
+
+## RedBlackBST (left-leaning red-black tree) — `search/redblackbst.go`
+
+The LLRB adds balancing on top of BST order. **Invariants:**
+
+1. **BST order** (as above), on `key`.
+2. **Left-leaning:** no right-leaning red link (`isRed(n.right) ⇒ isRed(n.left)`
+   is disallowed at rest).
+3. **No two reds in a row:** a red link's child link is not also red.
+4. **Perfect black balance:** every root-to-leaf path crosses the same number of
+   black links.
+
+`put` (`redblackbst.go:100`) inserts the new node **red** at the bottom (as in
+the BST), then re-establishes the invariants bottom-up on the return path with
+three fix-ups (`redblackbst.go:119`):
+
+- `rotateLeft` when the right child is red and the left is not (repairs a
+  right-leaning red, invariant 2);
+- `rotateRight` when the left child *and* its left child are red (repairs two
+  reds in a row, invariant 3);
+- `flipColors` when both children are red (splits a temporary 4-node, pushing
+  redness up while preserving invariant 4).
+
+`Put` (`redblackbst.go:95`) recolours the root black afterwards. These are
+exactly Sedgewick's LLRB transformations; each rotation/flip preserves BST order
+and black-balance while removing one local violation, so by induction on the
+return path the whole tree satisfies invariants 1–4 after every `Put`. The
+`capacity` field is maintained as the subtree size (`1 + left.Capacity() +
+right.Capacity()`) and correctly transferred by the rotations
+(`x.capacity = n.capacity`, then `n` recomputed). The invariants bound the
+height at `≤ 2·log₂(n)`, giving logarithmic `Get`/`Put`.
+
+**Deletion is lazy (tombstoning)** and deliberately *not* the full LLRB delete —
+the source notes it is "not fully implemented in lecture." `Del`
+(`redblackbst.go:158`) locates the node and sets `deleted = true`, decrements
+`size`, and zeroes `val`; `Get` (`redblackbst.go:136`) returns `NotFound` for a
+tombstoned node. This satisfies the **Set contract** (a deleted key reads as
+absent, `Size` is accurate) but leaves the node in the tree: space is not
+reclaimed and balance is unchanged (structure is untouched). Termination:
+`get`/`put`/`del` recurse strictly downward. ∎
+
+-----------------------------------------------------------------------------
+
+# Part III — Priority queues
+
+Both queues implement `PriorityQueue` (`queue/priority.go`) over `int`. The
+**contract**: `Insert` adds an element; `Max` returns a current maximum;
+`DeleteMax` removes and returns a current maximum; and draining a queue by
+repeated `DeleteMax` yields the inserted elements in **non-increasing order**
+and returns **exactly the multiset** inserted (completeness). The last part is
+the *permutation* invariant now checked by `queue/property_test.go`.
+
+## ElementaryPriority (unordered slice) — `queue/elementarypriority.go`
+
+**Invariant:** `q.a` holds exactly the current multiset of elements (in
+arbitrary order); `Size = len(q.a)`.
+
+- `Insert` (`elementarypriority.go:17`) appends — trivially preserves the
+  invariant.
+- `max` (`elementarypriority.go:52`) returns the index and value of a maximum by
+  a linear scan. **This must seed from an actual element**, `q.a[0]`, not the
+  zero value of `T`: an all-negative queue has no element `> 0`, so a zero seed
+  reports a phantom `(0, 0)`. This was the fixed bug — see
+  [`case-study-bugs-found.md`](case-study-bugs-found.md).
+- `DeleteMax` (`elementarypriority.go:26`) removes the max element (shifting the
+  tail left by one) and returns it — multiset minus one maximum.
+
+Draining is non-increasing because each step removes *a* current maximum from
+the remaining multiset. Completeness holds because `Insert` and `DeleteMax` only
+add/remove single elements. Termination: `Size` strictly decreases per
+`DeleteMax`. ∎
+
+## HeapPriority (binary max-heap) — `queue/heappriority.go`
+
+A binary heap in `q.a` with index `0` unused, so `a[1]` is the root and node
+`k`'s children are `2k`, `2k+1`. **Invariant (heap order):** for every
+`2 ≤ k ≤ Size`, `a[k/2] ≥ a[k]` (each parent ≥ its children). It follows that
+`a[1]` is a maximum of the whole heap.
+
+- `Insert` (`heappriority.go:29`) appends the new element at the end and
+  `swim`s it: while it exceeds its parent, swap upward. **swim invariant:** heap
+  order holds everywhere except possibly between `k` and its parent; the loop
+  restores it. Measure: `k` halves toward the root.
+- `DeleteMax` (`heappriority.go:42`) returns `a[1]` (a maximum, by the
+  invariant), moves the last element to the root, truncates, and `sink`s it:
+  while a child is larger, swap with the **larger** child. **sink invariant:**
+  heap order holds except possibly between `k` and its children. Measure: `2k`
+  grows toward `Size`.
+- `Max` (`heappriority.go:34`) returns `a[1]` without modification.
+
+Completeness: `swim`/`sink` mutate only via `Swap` (multiset-preserving, Lemma
+S), and `DeleteMax` removes exactly one element; so a full drain returns the
+inserted multiset, in non-increasing order. Termination: both `swim` and `sink`
+strictly move `k` toward their bound. ∎