From 3f906d03262150892e2297e621bfc56e425ef142 Mon Sep 17 00:00:00 2001 From: Paul Buetow Date: Mon, 6 Jul 2026 10:32:34 +0300 Subject: Close verification-coverage gaps; harness finds two more bugs 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 --- docs/case-study-bugs-found.md | 218 ++++++++++++++++++++++++++++++++++++++ docs/case-study-hash-shift-bug.md | 157 --------------------------- docs/verification.md | 213 ++++++++++++++++++++++++++++++++++--- 3 files changed, 419 insertions(+), 169 deletions(-) create mode 100644 docs/case-study-bugs-found.md delete mode 100644 docs/case-study-hash-shift-bug.md (limited to 'docs') diff --git a/docs/case-study-bugs-found.md b/docs/case-study-bugs-found.md new file mode 100644 index 0000000..3f5f0a9 --- /dev/null +++ b/docs/case-study-bugs-found.md @@ -0,0 +1,218 @@ +# Case study: three latent bugs the verification harness found + +Adding the verification layers (see [`verification.md`](verification.md)) did not +just re-confirm working code — it surfaced **three real, pre-existing bugs**, all +invisible to the original test suite. Each is documented below with how it was +caught, why it is genuinely wrong, why the old tests missed it, and the fix. + +A theme runs through all three: the original tests were **too weak in a specific +dimension**, and the new checks are strong in exactly that dimension. + +| # | Location | Bug | Caught by | Old test's blind spot | +|---|----------|-----|-----------|-----------------------| +| 1 | `search/hash.go` | shift wider than a narrow key type → term is always 0 | `go vet` (in `make verify`) | only ever used 64-bit `int` keys | +| 2 | `queue/elementarypriority.go` | `max()` seeded at `0` → wrong for all-negative queues | queue permutation property | test data was never negative | +| 3 | `sort/sleep.go` | result built on a pre-sized slice → doubled length with leading zeros | sleep permutation property | only checked `.Sorted()`, not completeness | + +--- + +## Bug 1 — a shift wider than the key type (`search/hash.go`) + +### The offending code + +```go +func (h *Hash[K,V]) hash(key K) int { + i := key + key*2 + key<<10 + key>>2 + ... +} +``` + +`K` is constrained by `ds.Integer`, so it may be **any** width down to `int8`. +The `key<<10` term is meant to spread low bits into high bits. + +### What the tool reported + +``` +$ make verify +go vet ./... +search/hash.go:29:21: key (may be 8 bits) too small for shift of 10 +``` + +`go vet`'s shift analyzer is a lightweight formal check: for every shift it +computes a conservative lower bound on the left operand's bit width and flags any +shift count `>=` that width. The narrowest `K` can be is `int8` (8 bits), and +`10 >= 8`. + +### Why it is genuinely a bug (Go shift semantics) + +The Go spec defines non-constant left shifts operationally: *"Shifts behave as if +the left operand is shifted n times by 1 … There is no upper limit on the shift +count."* Shifting an 8-bit value ten times pushes every bit out of the value's +width, so for `K = int8`/`uint8`: + +``` +key<<10 == 0 // always, for every key +``` + +The intended high-bit mixing silently disappears. Note it is width-dependent +(fine for `int16`+), and it is a *distribution/quality* bug, not a Set-contract +violation — chaining keeps the table correct, but narrow-key instantiations +degrade toward `O(n)` per operation. Exactly the kind of silent rot no assertion +would flag. + +### Why the tests missed it + +Every test uses `int` keys (`test[int,int](NewHash[int,int](i*2), …)`), where +`int` is 64 bits and the shift is fine. The bug lives in the **type dimension**, +not the value dimension — no value-space test or fuzzer over `int` could reach +it; only a type-aware tool (or an actual `int8` instantiation) can. + +### The fix + +```go +func (h *Hash[K,V]) hash(key K) int { + // Mix the key in a full-width int64 rather than in K. ... + i := int64(key) + i = i + i*2 + i<<10 + i>>2 + ... +} +``` + +Widening to `int64` before the shift keeps the result **byte-identical for +64-bit `int` keys** (so all existing tests still pass unchanged) while making the +mixing well-defined for every width. It does not *suppress* the warning; it +removes the condition (`shift >= width`) that made it true. + +--- + +## Bug 2 — a maximum seeded at zero (`queue/elementarypriority.go`) + +### The offending code + +```go +func (q *ElementaryPriority[T]) max() (ind int, max T) { + for i, a := range q.a { + if a > max { // max starts at the zero value of T, i.e. 0 + ind, max = i, a + } + } + return ind, max +} +``` + +`max` is a named return, so it starts at `T`'s zero value, `0`. + +### How it was caught + +The new completeness/permutation property in `queue/property_test.go` drives +each queue with `testing/quick`, which generates **negative** values too. It +failed immediately for `ElementaryPriority` (and passed for `HeapPriority`): + +``` +ElementaryPriority violated ordered-permutation property: + #1: failed on input []int{-1881664299226649700, 1264358012858162353, ...} +``` + +### Why it is genuinely a bug + +If **every** element in the queue is negative, no element is `> 0`, so the loop +never updates and `max()` returns `(0, 0)` — reporting a maximum of `0`, a value +that is not even in the queue. `DeleteMax` then removes the wrong element (index +0) and returns a phantom `0`. Both the ordering and completeness of a drain +break. + +### Why the tests missed it + +The original queue test builds inputs with +`ds.NewRandomArrayList[int](l, -1)`, whose values come from `rand.Int()` — always +**non-negative**. And `queue_test.go` only checked that `DeleteMax` was +non-increasing; it never checked that all inserted elements come back. So a queue +of non-negative numbers, checked only for ordering, sailed through. + +### The fix + +```go + if len(q.a) == 0 { + return 0, 0 + } + ind, max = 0, q.a[0] // seed from a real element, not the zero value + for i, a := range q.a { + if a > max { ind, max = i, a } + } +``` + +Seeding from `q.a[0]` makes the scan correct for any value range. +(`HeapPriority` was already immune: it compares actual array elements and returns +`a[1]` as the max.) + +--- + +## Bug 3 — a sort that doubled its output (`sort/sleep.go`) + +### The offending code + +```go +func Sleep[V ds.Integer](a ds.ArrayList[V]) ds.ArrayList[V] { + sorted := ds.NewArrayList[V](len(a)) // slice of LENGTH len(a): len(a) zeros + ... + for num := range numCh { + sorted = append(sorted, num) // appends AFTER those zeros + } + return sorted +} +``` + +`ds.NewArrayList(len(a))` is `make(ArrayList, len(a))` — a slice of that +**length**, pre-filled with `len(a)` zeros. Appending then adds the real values +*after* them. + +### How it was caught + +`TestSleepSort`, strengthened to check permutation, failed: + +``` +Sleep sort output is not a permutation of input: + in =[1 1 2 8 8 7 3 0 6 7] (10 elements) + out=[0 0 0 0 0 0 0 0 0 0 0 1 1 2 3 6 7 7 8 8] (21 elements!) +``` + +The output is **eleven leading zeros followed by the ten real values** — more +than double the input length. + +### Why the tests missed it + +The original `TestSleepSort` only asserted `a.Sorted()`. Zeros followed by an +ascending sequence **is** sorted, so the wildly-wrong 21-element result passed. +This is the textbook case for the *permutation* invariant: ordering alone cannot +detect dropped, duplicated, or (here) invented elements. + +### The fix + +```go + // Start empty with capacity len(a): the received values are appended below. + sorted := make(ds.ArrayList[V], 0, len(a)) +``` + +Length `0`, capacity `len(a)`: the appends now fill it to exactly `len(a)` +elements with no spurious zeros. + +--- + +## The through-line + +Two independent lessons, each reinforced twice: + +1. **Ordering is not correctness.** Bugs 2 and 3 both produced *ordered* output + that was wrong (missing/extra elements). Only the **permutation / completeness** + invariant — added to the sort and queue property tests — catches them. This is + the single most valuable check added by this work. + +2. **Test data has blind spots the code doesn't.** Bugs 1 and 2 both hid behind + the test suite's fixed input distribution — always 64-bit, always + non-negative. `go vet` (reasoning over *types*) and `testing/quick` (sampling + the *whole* value range, negatives included) each see past a blind spot that + hand-picked or `rand.Int()` data does not. + +None of these required the heavy layers (TLA+, Gobra). The cheapest checks — +`go vet` and a stronger property assertion — found all three. Breadth first; +depth where it earns its keep. diff --git a/docs/case-study-hash-shift-bug.md b/docs/case-study-hash-shift-bug.md deleted file mode 100644 index 6ec4f7d..0000000 --- a/docs/case-study-hash-shift-bug.md +++ /dev/null @@ -1,157 +0,0 @@ -# Case study: a latent bug the verification harness caught - -This documents a real defect that the verification work found **on the very -first run** of the new `make verify` target — before any of the heavier layers -(TLA+, Gobra) were even involved. It is a good illustration of *why* wiring -these checks into a gate pays off: the bug had been sitting in the repository -undetected because the existing tests could never trigger it. - -## TL;DR - -- **Where:** `search/hash.go`, the `Hash.hash` method. -- **What:** `key << 10`, where `key` has a generic integer type, silently - evaluates to `0` for narrow key types (`int8`/`uint8`), discarding a whole - term of the hash mix. -- **Who found it:** `go vet`'s shift analyzer, run as part of `make verify`. -- **Why the tests missed it:** every test instantiates the hash with 64-bit - `int` keys, where the shift is perfectly fine — so the bug is *latent*. -- **Fix:** compute the mix in a full-width `int64`. - -## The offending code - -Before: - -```go -func (h *Hash[K,V]) hash(key K) int { - i := key + key*2 + key<<10 + key>>2 - if i < 0 { - i = -i - } - return int(i) % h.capacity -} -``` - -`K` is a type parameter constrained by `ds.Integer` (`ds/types.go`), which -embeds `constraints.Integer` — i.e. `K` may be **any** of `int, int8, int16, -int32, int64, uint, uint8, …`. The intent of `key<<10` is clearly to spread the -key's low bits up into the high bits so that keys differing only in their low -bits land in different buckets. - -## What the tool reported - -``` -$ make verify -go vet ./... -search/hash.go:29:21: key (may be 8 bits) too small for shift of 10 -``` - -`go vet` bundles a *shift* analyzer that is, in effect, a lightweight formal -check: for every shift expression it computes a conservative lower bound on the -bit width of the left operand and flags any shift whose count is `>=` that -width. Here the narrowest type `K` can take is `int8` (8 bits), and `10 >= 8`, -so the analyzer proves that *for at least one legal instantiation* the shift is -degenerate. - -## Why it is genuinely a bug (Go shift semantics) - -This is not a false positive. The Go specification defines non-constant left -shifts operationally: - -> Shifts behave as if the left operand is shifted `n` times by 1 for a shift -> count of `n`. […] There is no upper limit on the shift count. - -For an 8-bit value, shifting "one bit at a time" ten times pushes **every** -original bit out of the value's width. The result is therefore always `0`. So -for `K = int8`/`uint8`: - -``` -key<<10 == 0 // always, for every key -``` - -and the hash silently collapses to `key + key*2 + key>>2` — the high-bit mixing -the author intended is simply gone. - -Two subtleties worth recording: - -1. **It is width-dependent, not universally broken.** For `int16` the count - `10 < 16`, so the term is fine; for 32-/64-bit types it is obviously fine. - `go vet` still (correctly) flags the expression because it must be sound for - *all* instantiations, and `int8` is in the constraint set. The narrowest - type is what governs safety. - -2. **It is a quality/portability bug, not a memory-safety or a Set-contract - violation.** The hash table stays *functionally correct* even for `int8` - keys: `Put`, `Get`, and `Del` all call the same `hash`, and collisions are - resolved by chaining in the per-bucket `Elementary` list. What degrades is - the *distribution* — more keys collide into the same bucket, turning the - intended O(1) operations toward O(n). So the failure mode is silent - performance rot for narrow-key instantiations, exactly the kind of thing that - never shows up as a failing assertion. - -## Why no test caught it - -Every instantiation in the test suite uses `int` keys: - -```go -test[int,int](NewHash[int,int](i*2), i, t) // search/search_test.go -``` - -`int` is 64 bits on this platform, so `key<<10` behaves as intended and all -tests pass. There is no `Hash[int8, …]` anywhere, so the degenerate path is -never exercised. A property test or a fuzz run over `int` keys would *also* miss -it — the bug lives in the *type dimension*, not the value dimension, and only a -tool that reasons about the type (like `go vet`) or an actual narrow-type -instantiation can surface it. This is precisely the class of latent defect that -static analysis is good at and dynamic testing is blind to. - -## The fix - -Perform the mixing in a full-width `int64`, then reduce: - -```go -func (h *Hash[K,V]) hash(key K) int { - // Mix the key in a full-width int64 rather than in K. K is any ds.Integer, - // so for a narrow type (e.g. int8) the "key<<10" term would shift past the - // type width and vanish to 0, destroying the intended high-bit mixing (and - // go vet rightly flags it). Widening to int64 first keeps the result - // identical for 64-bit int keys while making the mix well-defined for every - // integer width. - i := int64(key) - i = i + i*2 + i<<10 + i>>2 - if i < 0 { - i = -i - } - return int(i) % h.capacity -} -``` - -Why this is the right fix: - -- **Behavior-preserving for the code that exists.** For `K = int` (64-bit), the - arithmetic is byte-for-byte identical to before — `int64(key)` is a no-op - widening, and every operation stays in 64 bits — so every existing test still - passes unchanged. -- **Correct for the code that might exist.** For narrow `K`, the key is widened - *before* the shift, so `i<<10` now mixes real bits instead of vanishing. The - hash finally does for `int8` keys what it always did for `int` keys. -- **It silences the analyzer for the right reason.** `int64` is 64 bits, `10 < - 64`, so the shift is provably well-defined for the actual operand type. We are - not suppressing the warning; we are removing the condition that made it true. - -An `int64` cast rather than the value's own width also documents intent: "this -mixing is meant to happen in a wide register, independent of the key type." - -> Residual note, left as-is: `if i < 0 { i = -i }` still has the classic -> `-math.MinInt64` overflow corner. It predates this change, is astronomically -> unlikely for these inputs, and is out of scope here — recorded for honesty. - -## How this maps to the verification layers - -This defect was caught by **Layer 2** of the harness (see -[`verification.md`](verification.md)) — `go vet` inside `make verify`. It is the -cheapest layer, and it found a bug that the paper proofs (Layer 0, which focus -on the sorts) and the property tests (Layer 1, which only ever run `int`) did -not. The lesson is the ordering of the layers is not the ordering of their -value: a one-line static check surfaced a real, shipped-in latent bug that no -amount of value-space testing would have. Cheap, broad checks first; deep proofs -where they earn their keep. 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. ∎ -- cgit v1.2.3