path: root/docs/verification.md

# Hand-written correctness proofs

This document contains human-written (paper) correctness proofs for the
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` 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

- `a[p..q]` denotes the inclusive slice of indices `p, p+1, …, q`. An empty
  range (`p > q`) is vacuously sorted and vacuously a permutation of itself.
- **sorted(a[p..q])** ≡ `∀ p ≤ r < q : a[r] ≤ a[r+1]`.
- **perm(a, a₀)** ≡ the multiset `{a[0], …, a[n-1]}` equals the multiset of the
  original contents `a₀`.

### Lemma S (Swap preserves the multiset)

The **only** operation any sort here uses to mutate the backing array is
`ArrayList.Swap` (`ds/arraylist.go:74`), which exchanges two elements. Swapping
two positions leaves the multiset of stored values unchanged. By induction over
the sequence of swaps performed by any algorithm below, **perm(a, a₀) holds at
every point** — the output is always a permutation of the input. This single
lemma discharges the permutation half of every sort's postcondition, so the
per-algorithm proofs below focus on *ordering* and *termination*.

> The exceptions are `Merge`/`BottomUpMerge`, which write elements via `aux`
> rather than `Swap`; their permutation argument is given inline (Lemma M).

---

## Selection sort — `sort/selection.go:7`

- **Pre:** `a` holds arbitrary values; `l = len(a)`.
- **Post:** `sorted(a[0..l-1]) ∧ perm(a, a₀)`.

**Outer invariant** (before iteration `i`, `0 ≤ i ≤ l`):
`sorted(a[0..i-1]) ∧ ∀ p < i ≤ q : a[p] ≤ a[q]` — i.e. the prefix `a[0..i-1]`
is sorted and every prefix element is ≤ every suffix element.

**Inner loop** (`j := i+1 … l-1`) computes `min` = index of the smallest element
in `a[i..l-1]` (invariant: `a[min]` is the minimum of `a[i..j-1]`). After the
loop, `a.Swap(i, min)` moves that minimum to position `i`. This element is ≥ all
of `a[0..i-1]` (by the outer invariant, everything in `a[i..]` is ≥ the prefix)
and ≤ everything remaining in `a[i+1..]`, so the outer invariant re-establishes
for `i+1`.

**Termination:** outer `i` and inner `j` each range over a fixed finite index
set and strictly increase. **Permutation:** Lemma S. At `i = l` the invariant
gives `sorted(a[0..l-1])`. ∎

## Insertion sort — `sort/insertion.go:7`

- **Post:** `sorted(a[0..l-1]) ∧ perm(a, a₀)`.

**Outer invariant** (before iteration `i`): `sorted(a[0..i-1])`.

**Inner loop** (`j := i; j > 0; j--`) bubbles `a[i]` left, stopping via `break`
as soon as `a[j] > a[j-1]` (the pair is already in order) or when `j = 0`.
**Inner invariant** (at each test): `a[0..i]` is a permutation of its original
prefix contents; `sorted(a[j..i])`; and `∀ j < r ≤ i : a[r] ≥ a[j]`. When the
loop stops, the entire prefix `a[0..i]` is sorted, re-establishing the outer
invariant for `i+1`.

Note the loop swaps on *equality* too (it breaks only on strict `a[j] > a[j-1]`),
which is harmless — it performs a few extra swaps but preserves both sortedness
and (by Lemma S) the multiset.

**Termination:** inner measure `j` strictly decreases and is bounded below by 0;
outer `i` ranges over `range a`. ∎

## Shell sort — `sort/shell.go:7`

Shell sort is insertion sort applied on a decreasing sequence of gaps
`h ∈ {…, 40, 13, 4, 1}` (built by `h = 3h+1`, then `h /= 3`).

- **Post:** `sorted(a[0..l-1]) ∧ perm(a, a₀)`.

For a fixed gap `h`, the body is an *h-interleaved* insertion sort: the inner
loop (`j := i; j >= h; j -= h`) inserts `a[i]` into the sorted-by-`h`
subsequence `…, a[i-2h], a[i-h], a[i]`, breaking when `a[j-h] < a[j]`. By the
insertion-sort argument applied to each residue class mod `h`, after the `h`
pass every h-strided subsequence is sorted (the array is "h-sorted").

The final gap is always `h = 1` (the loop condition is `h >= 1` and integer
division reaches 1). A 1-sorted array is fully `sorted(a[0..l-1])`. The earlier
larger-gap passes only reorder via `Swap`, so they neither break the final
1-sort's correctness nor the multiset.

**Termination:** the gap loop strictly decreases `h` via `h /= 3` until `h < 1`;
each inner loop terminates as in insertion sort. **Permutation:** Lemma S. ∎

## Merge sort — `sort/merge.go:7`

Recursive top-down merge sort; base case (`l ≤ 10`) delegates to insertion sort.

- **Post of `mergeSort(a, aux)`:** `sorted(a) ∧ perm(a, a₀)`.

**Induction on `l = len(a)`.** *Base* (`l ≤ 10`): insertion sort, proven above.
*Step*: `mi = l/2`; the two recursive calls sort the disjoint halves `a[0..mi-1]`
and `a[mi..l-1]` (IH). `merge(a, aux, 0, mi, l-1)` then combines them.

### Lemma M (merge is correct and permutation-preserving) — `sort/merge.go:27`

`merge` first copies `a[lo..hi]` into `aux[lo..hi]`, then walks `k = lo … hi`
with two read cursors `i` (into the left run, starting `lo`) and `j` (into the
right run, starting `mi`). **Invariant** at each `k`: `a[lo..k-1]` is sorted and
is exactly the `k-lo` smallest elements of `aux[lo..hi]`, with `i`, `j` pointing
at the unconsumed heads of the two (individually sorted) runs. The 4-way
`switch` picks the smaller available head (`aux[i] > aux[j]` → take right, else
take left; boundary cases when a run is exhausted: `i >= mi` or `j > hi`). Each
step consumes exactly one source element and advances exactly one cursor, so
after `hi-lo+1` steps every element of `aux[lo..hi]` has been written back once
→ `perm` holds and `a[lo..hi]` is sorted. ∎

Because the merge preserves the multiset and produces a sorted whole from two
sorted halves, the step re-establishes the postcondition.

**Termination:** each recursion halves the length, bottoming out at `l ≤ 10`. ∎

## Bottom-up merge sort — `sort/bottomupmerge.go:7`

Iterative merge sort. **Outer invariant** (before the pass with subarray size
`sz`, a power of two): every aligned block `a[k·sz .. (k+1)·sz - 1]` is sorted.
The inner loop merges adjacent pairs of `sz`-blocks via the same `merge`
(Lemma M), using `min(lo+sz+sz-1, l-1)` (`sort/bottomupmerge.go:20`) to clamp
the final, possibly short, block to the array end. After the pass, every block
of size `2·sz` is sorted — the invariant for the next pass.

**Termination:** `sz` doubles (`sz = sz + sz`) until `sz ≥ l`; the loop then
stops with the whole array as one sorted block. **Permutation:** Lemma M applied
to each merge. ∎

## Quick sort — `sort/quick.go:9` (highest scrutiny)

Recursive quicksort; base case (`l ≤ 10`) delegates to insertion sort. The
interesting part is `quickPartition` (`sort/quick.go:25`), examined line by line
because its index bounds are the most error-prone code in the repo.

Setup for an array of length `l ≥ 11` (partition is only reached from
`quick` when `l > 10`, so `hi = l-1 ≥ 10`):

```
i := 0;  j := l;  hi := l-1
a.Swap(0, median(a, l));  v := a[0]   // pivot chosen by median-of-3, parked at index 0
```

**Left scan** `for i++; a[i] < v && i < hi; i++`:
`i` starts at 1. Because the test `i < hi` is ANDed in, `i` can advance at most
to `hi`; when `i == hi` the guard `i < hi` is false and the loop stops. The
array access `a[i]` therefore uses indices in `[1, hi] = [1, l-1]` — **always in
bounds**. The scan stops at the first index with `a[i] ≥ v` (or at `hi`), so on
exit `∀ 1 ≤ r < i : a[r] < v`.

**Right scan** `for j--; v < a[j] && j > 0; j--`:
`j` starts at `l`, immediately decremented to `l-1 = hi`. The guard `j > 0`
caps it at 0; and since `a[0] == v`, the head test `v < a[0]` is false, so the
scan halts at `j = 0` at the latest — `j` **never goes negative**. Accesses use
`[0, hi]`. On exit `∀ j < r ≤ hi : a[r] > v`, and `a[j] ≤ v`.

**Loop:** if `i ≥ j` the scans have crossed → `break`; otherwise `a.Swap(i, j)`
sends the `≥ v` element right and the `≤ v` element left, and the invariant
`a[1..i-1] < v ∧ a[j+1..hi] > v` is maintained across iterations.

**Finalize** `a.Swap(0, j)`: at break, `a[j] ≤ v` (right scan stopped there), so
after the swap `a[j] = v` with `a[0..j-1] ≤ v ≤ a[j+1..hi]`. Return `j`.

**Verdict:** the invariant *closes* — no out-of-bounds and no off-by-one. The
`i < hi` bound and the `a[0] == v` sentinel are exactly what keep the two scans
in range without relying on external sentinels. Duplicates equal to `v` are
handled correctly: strict inequalities make both scans stop on equal keys, which
is the standard technique to avoid quadratic blow-up on many duplicates and does
not violate the partition postcondition. On the all-equal input the scans meet
near the middle and the recursion still shrinks, so there is no infinite loop.

`quick` then recurses on `a[0..j-1]` and `a[j+1..]`, which by the partition
postcondition are correctly ordered relative to `v`; by induction on length the
whole array is sorted. **Termination:** each partition removes the pivot and
splits the rest into two strictly-smaller subranges. **Permutation:** Lemma S. ∎

## 3-way quicksort — `sort/quick3way.go:8`

Dijkstra's 3-way (Dutch-national-flag) partition; shuffles first, base case
(`l ≤ 10`) insertion sort. Pivot `v = a[0]` (after `Swap(0, median)`).

**Invariant** of the partition loop (`for i <= gt`), with `lt`, `i`, `gt`:
`a[0..lt-1] < v`, `a[lt..i-1] == v`, `a[gt+1..hi] > v`, and `a[i..gt]` unexamined.
The `switch` maintains it: `a[i] < v` → `Swap(lt, i); lt++; i++`; `a[i] > v` →
`Swap(i, gt); gt--` (leaves `i`, since the swapped-in element is unexamined);
`a[i] == v` → `i++`. When `i > gt` the middle band `a[lt..gt]` equals `v` and is
in final position, so only `a[0..lt-1]` and `a[gt+1..hi]` need recursion.

**Termination:** each iteration either advances `i` or lowers `gt`, so the gap
`gt - i` strictly decreases; recursion shrinks the ranges. **Permutation:**
Lemma S. ∎

## Shuffle — `sort/shuffle.go:9` (NOT a sort)

`Shuffle` produces a uniformly random permutation (used by `Quick3Way` and the
`TestShuffleSort` negative test). For each `i`, `r := l - rand.Intn(l-i) - 1`.
Since `rand.Intn(l-i) ∈ [0, l-i-1]`, we get `r ∈ [i, l-1]`, so each `Swap(i, r)`
exchanges `a[i]` with a uniformly chosen element of the unshuffled suffix — this
is the Fisher–Yates shuffle, yielding each of the `l!` permutations with equal
probability. **Post:** `perm(a, a₀)` (Lemma S); ordering is intentionally *not*
guaranteed. ∎

## Parallel merge / parallel quick — `sort/parallelmerge.go:9`, `sort/parallelquick.go:9`

These reuse the sequential `mergeSort`/`quick`/`quickPartition` proven above and
parallelize the two recursive calls once the length crosses a threshold
(`< 1000` falls back to sequential).

**Correctness reduces to data-race freedom.** In both, the two goroutines
operate on **disjoint** subranges:

- `parallelMerge`: `a[0:mi]` / `a[mi:]` and, crucially, `aux[0:mi]` / `aux[mi:]`
  are non-overlapping slices, so the two subtrees touch disjoint memory. The
  `wg.Wait()` **happens-before** the top-level `merge`, so the merge observes
  both halves fully sorted. No goroutine reads memory another writes
  concurrently.
- `parallelQuick`: `quickPartition` runs *before* the goroutines are spawned and
  fixes the pivot at index `j`; the children then own `a[0:j]` and `a[j+1:]` —
  disjoint, and both exclude the settled pivot `a[j]`. `wg.Wait()` joins before
  returning.

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, 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`

`Sleep` (integers only) spawns one goroutine per element that sleeps
`num` seconds, then sends `num` on a shared channel; a `WaitGroup` closes the
channel once all sends complete; the main goroutine appends received values.

Correctness rests on the *timing assumption* that a larger value's sleep
finishes strictly later, so values arrive on the channel in non-decreasing
order. This assumption — and the concurrency safety (the closer goroutine's
`wg.Wait()` happening-after every `wg.Done()`, no send on a closed channel, and
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. ∎