diff options
Diffstat (limited to 'docs/verification.md')
| -rw-r--r-- | docs/verification.md | 213 |
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. ∎ |