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. 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**.

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.

## 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. ∎

## 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.