From f74812f8eda48194b622bdd318f35d3a6b6328cd Mon Sep 17 00:00:00 2001 From: Paul Buetow Date: Mon, 6 Jul 2026 10:15:56 +0300 Subject: Add layered formal-verification harness Adds four complementary layers to verify correctness, all runnable locally, weakest-but-broadest to strongest-but-narrowest: 0. Paper proofs (docs/verification.md): Hoare invariants, termination measures, and permutation arguments for every algorithm. 1. Property tests (sort/property_test.go): testing/quick asserting ordering AND permutation for every sort. Closes a real gap -- the existing tests only checked .Sorted(), so a sort dropping/duplicating elements passed. 2. make verify: go vet + staticcheck + go test -race -short, with -short gating of the large sizes in sort/search tests so the race build is quick. 3. make verify-model: TLA+/TLC model check of sleep sort (termination, deadlock-freedom, sorted permutation) -- formal/tla/. 4. make verify-formal: Gobra deductive proof (Viper+Z3) that a monomorphized insertion sort is memory-safe and sorted for all inputs -- formal/. The static layer already found a latent bug: hash() used key<<10 on a generic integer, which silently yields 0 for narrow key types (int8), degrading the hash. Tests missed it because they only use int keys. Fixed by mixing in int64; documented extensively in docs/case-study-hash-shift-bug.md. Also cleans up dead code and a blank-identifier range flagged by staticcheck. Co-Authored-By: Claude Opus 4.8 --- .gitignore | 6 + Makefile | 24 ++++ docs/case-study-hash-shift-bug.md | 157 +++++++++++++++++++++++ docs/verification.md | 255 ++++++++++++++++++++++++++++++++++++++ formal/README.md | 59 +++++++++ formal/insertion.go | 42 +++++++ formal/tla/README.md | 62 +++++++++ formal/tla/SleepSort.cfg | 13 ++ formal/tla/SleepSort.tla | 108 ++++++++++++++++ search/hash.go | 9 +- search/search_test.go | 8 ++ sort/insertion.go | 2 +- sort/property_test.go | 110 ++++++++++++++++ sort/sort_test.go | 15 ++- staticcheck.conf | 6 + 15 files changed, 871 insertions(+), 5 deletions(-) create mode 100644 .gitignore create mode 100644 docs/case-study-hash-shift-bug.md create mode 100644 docs/verification.md create mode 100644 formal/README.md create mode 100644 formal/insertion.go create mode 100644 formal/tla/README.md create mode 100644 formal/tla/SleepSort.cfg create mode 100644 formal/tla/SleepSort.tla create mode 100644 sort/property_test.go create mode 100644 staticcheck.conf diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..b38974f --- /dev/null +++ b/.gitignore @@ -0,0 +1,6 @@ +# TLC model-checker metadata (verify-model directs it to /tmp, but guard anyway) +states/ + +# Go profiling output from the `profile` make target +memprofile.out +cpuprofile.out diff --git a/Makefile b/Makefile index fab5d52..8632e8c 100644 --- a/Makefile +++ b/Makefile @@ -1,6 +1,30 @@ test: go clean -testcache go test ./... -v + +# verify: static + dynamic correctness checks. Fast enough for routine use. +# go vet / staticcheck - static analysis +# go test -race -short - race detector over the (size-capped) test + property +# suites; -short keeps the million-element cases out so +# the race build stays quick. See docs/verification.md. +verify: + go vet ./... + staticcheck ./... + go test -race -short ./... + +# verify-model: exhaustively model-check the concurrent sleep sort with TLA+/TLC +# (a model of sort/sleep.go, not the Go code itself). See formal/tla/README.md. +verify-model: + java -cp $(HOME)/tools/tlaplus/tla2tools.jar tlc2.TLC -workers auto \ + -metadir /tmp/tlc-algorithms \ + -config formal/tla/SleepSort.cfg formal/tla/SleepSort.tla + +# verify-formal: machine-checked deductive proof of a monomorphized insertion +# sort with Gobra (Go verifier, Viper+Z3 backend), run from its container image. +# See formal/README.md. +verify-formal: + podman run --rm -v $(PWD)/formal:/gobra/formal:z \ + ghcr.io/viperproject/gobra:latest -i /gobra/formal/insertion.go bench: go test -run=xxx -bench=. ./... | tee bench.out sortbench: diff --git a/docs/case-study-hash-shift-bug.md b/docs/case-study-hash-shift-bug.md new file mode 100644 index 0000000..6ec4f7d --- /dev/null +++ b/docs/case-study-hash-shift-bug.md @@ -0,0 +1,157 @@ +# 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 new file mode 100644 index 0000000..3959e5b --- /dev/null +++ b/docs/verification.md @@ -0,0 +1,255 @@ +# 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. diff --git a/formal/README.md b/formal/README.md new file mode 100644 index 0000000..f667bdf --- /dev/null +++ b/formal/README.md @@ -0,0 +1,59 @@ +# Gobra deductive proof + +`insertion.go` is a **machine-checked** proof that an insertion sort is correct, +verified by [Gobra](https://github.com/viperproject/gobra) — ETH Zurich's +deductive verifier for Go, which translates annotated Go to the Viper +intermediate language and discharges the proof obligations with the Z3 SMT +solver. + +Unlike the TLA+ model (which checks a hand-written abstraction) and the property +tests (which sample inputs), this verifies the **actual Go source** for **all** +inputs. Gobra proves two things about `Insertion`: + +1. **Memory safety** — every index access is in bounds. The permission + invariants `forall k :: 0 <= k < len(a) ==> acc(&a[k])` carry write access to + every element through both loops; Go itself cannot prove the absence of + index-out-of-range panics, Gobra can. +2. **Ordering** — on return `a` is sorted ascending + (`forall p < q :: a[p] <= a[q]`), established via the two insertion-sort loop + invariants in the annotations. + +The **permutation** half of full correctness (output is a rearrangement of the +input) is intentionally left to the property tests and the paper proof in +[`docs/verification.md`](../docs/verification.md); proving it in Gobra needs +ghost multiset state and is noted there as future work. + +## Why a separate, non-generic copy? + +Gobra's support for Go generics and method-based abstractions is limited, so +this file is a deliberately monomorphized copy of `sort.Insertion` +([`sort/insertion.go`](../sort/insertion.go)): plain `[]int` instead of +`ds.ArrayList[V]`, and an inlined swap instead of the `.Swap` method. The +algorithm is otherwise identical. + +## Running + +Gobra is distributed as a container image (it bundles its own Z3, so no separate +solver install is needed). With `podman` (or `docker`): + +```sh +podman pull ghcr.io/viperproject/gobra:latest +make verify-formal +``` + +or directly: + +```sh +podman run --rm -v "$PWD/formal:/gobra/formal:z" \ + ghcr.io/viperproject/gobra:latest -i /gobra/formal/insertion.go +``` + +Expected output ends with: + +``` +Gobra found 0 errors. +``` + +To convince yourself the proof is not vacuous, flip the inner comparison +`a[j] < a[j-1]` to `>` and re-run: Gobra reports +`Loop invariant might not be preserved`. diff --git a/formal/insertion.go b/formal/insertion.go new file mode 100644 index 0000000..cf053a7 --- /dev/null +++ b/formal/insertion.go @@ -0,0 +1,42 @@ +package formal + +// Insertion sorts a in ascending order, in place. This is a monomorphized +// (non-generic, plain []int, inlined swap) copy of sort.Insertion, annotated so +// the Gobra verifier can prove -- with the Viper/Z3 backend -- BOTH: +// +// 1. memory safety: every index access is in bounds (the permission +// invariants "forall k :: 0<=k acc(&a[k])" carry write access +// to every element through both loops), and +// 2. functional correctness (ordering): on return, a is sorted ascending +// (the postcondition "forall p acc(&a[k]) +//@ ensures forall k int :: 0 <= k && k < len(a) ==> acc(&a[k]) +//@ ensures forall p, q int :: 0 <= p && p < q && q < len(a) ==> a[p] <= a[q] +func Insertion(a []int) { + i := 0 + //@ invariant 0 <= i && i <= len(a) + //@ invariant forall k int :: 0 <= k && k < len(a) ==> acc(&a[k]) + // The prefix a[0..i) is already fully sorted. + //@ invariant forall p, q int :: 0 <= p && p < q && q < i ==> a[p] <= a[q] + for i < len(a) { + j := i + //@ invariant 0 <= j && j <= i && i < len(a) + //@ invariant forall k int :: 0 <= k && k < len(a) ==> acc(&a[k]) + // a[0..i] is sorted once position j is ignored as either endpoint... + //@ invariant forall p, q int :: 0 <= p && p < q && q <= i && p != j && q != j ==> a[p] <= a[q] + // ...and the in-flight element a[j] is <= everything to its right. + //@ invariant forall q int :: j < q && q <= i ==> a[j] <= a[q] + for j > 0 && a[j] < a[j-1] { + tmp := a[j] + a[j] = a[j-1] + a[j-1] = tmp + j = j - 1 + } + i = i + 1 + } +} diff --git a/formal/tla/README.md b/formal/tla/README.md new file mode 100644 index 0000000..a80c687 --- /dev/null +++ b/formal/tla/README.md @@ -0,0 +1,62 @@ +# TLA+ model check of sleep sort + +`SleepSort.tla` is a [TLA+](https://lamport.azurewebsites.net/tla/tla.html) +model of the concurrent sleep sort in [`sort/sleep.go`](../../sort/sleep.go), +checked exhaustively by the TLC model checker. + +## What this does and does NOT prove + +Model checking verifies a **hand-written model**, not the Go source. TLC +explores *every* reachable state of the model and confirms: + +- **`OutputSorted`** (safety) — the collected output is always non-decreasing. +- **`PermutationWhenDone`** (safety) — the output is a multiset permutation of + the input; nothing is dropped, duplicated, or invented. +- **`Terminates`** (liveness) — the collector eventually receives every value: + no deadlock and no value left sleeping forever. + +The gap you keep responsibility for: that the model faithfully abstracts +`sleep.go`. The model represents the sleeps as a discrete clock and the +unbuffered channel + `WaitGroup` as an urgent single-value rendezvous — see the +header comment in `SleepSort.tla`. + +Sortedness is **not** assumed. It emerges from one rule: time cannot pass while +a fired-but-unreceived timer waits (`Tick`'s urgency guard). Delete that guard +and TLC finds an unsorted counterexample — proof the check has teeth. + +## Running + +Needs Java and `tla2tools.jar` (download once): + +```sh +mkdir -p ~/tools/tlaplus +curl -fsSL -o ~/tools/tlaplus/tla2tools.jar \ + https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar +``` + +Then, from the repository root: + +```sh +make verify-model +``` + +or directly: + +```sh +java -cp ~/tools/tlaplus/tla2tools.jar tlc2.TLC \ + -config formal/tla/SleepSort.cfg formal/tla/SleepSort.tla +``` + +Expected output ends with: + +``` +Model checking completed. No error has been found. +``` + +## The input + +`SleepSort.cfg` checks the input `<<3, 1, 4, 1, 2>>` (defined as `InputValue` +in the module, because a `.cfg` cannot hold a sequence literal). It has a +duplicate and is out of order — enough to exercise ordering, ties, and +termination. Edit `InputValue` in `SleepSort.tla` to try others; the state space +stays small because the clock never exceeds the largest input value. diff --git a/formal/tla/SleepSort.cfg b/formal/tla/SleepSort.cfg new file mode 100644 index 0000000..6c86d67 --- /dev/null +++ b/formal/tla/SleepSort.cfg @@ -0,0 +1,13 @@ +\* TLC configuration for the SleepSort model. +\* Input is a small multiset with a duplicate (the two 1s) and out-of-order +\* values -- enough to exercise ordering, ties, and termination exhaustively. +\* It is defined as InputValue in the module (a .cfg cannot hold a <<..>>). +CONSTANT Input <- InputValue + +SPECIFICATION Spec + +INVARIANT TypeOK +INVARIANT OutputSorted +INVARIANT PermutationWhenDone + +PROPERTY Terminates diff --git a/formal/tla/SleepSort.tla b/formal/tla/SleepSort.tla new file mode 100644 index 0000000..45cc0e0 --- /dev/null +++ b/formal/tla/SleepSort.tla @@ -0,0 +1,108 @@ +------------------------------ MODULE SleepSort ------------------------------ +(***************************************************************************) +(* A TLA+ model of the sleep sort in sort/sleep.go. *) +(* *) +(* This verifies a *model*, not the Go source. It abstracts the goroutines *) +(* + WaitGroup + unbuffered channel of sleep.go into: *) +(* *) +(* - a global discrete clock (stand-in for wall-clock time / sleeps), *) +(* - one "timer" per input element that fires when the clock reaches *) +(* that element's value (a value-v element sleeps v seconds), and *) +(* - a single collector that receives one fired value at a time *) +(* (an unbuffered channel with one receiver hands off exactly one *) +(* value per rendezvous, with no buffering or reordering). *) +(* *) +(* Crucially, sortedness of the output is NOT baked in: it must *emerge* *) +(* from the timing mechanism. The only thing that enforces order is Tick's *) +(* urgency guard (time cannot pass while a fired-but-unreceived timer is *) +(* waiting). Remove that guard and TLC finds an unsorted counterexample -- *) +(* which is exactly what makes this a real check rather than a tautology. *) +(***************************************************************************) +EXTENDS Naturals, Sequences, FiniteSets + +CONSTANT Input \* the values to sort, as a sequence, e.g. <<3, 1, 2>> + +\* Concrete value for the model. TLC config files cannot parse a sequence +\* literal in a "CONSTANT Input = ..." assignment, so SleepSort.cfg overrides the +\* constant with this operator via "CONSTANT Input <- InputValue". +InputValue == <<3, 1, 4, 1, 2>> + +Idx == DOMAIN Input +Values == { Input[i] : i \in Idx } + +VARIABLES + clock, \* global time; the sleeps are measured against it + sent, \* sent[i] = TRUE once element i has been received + output \* the values collected so far, in arrival order + +vars == <> + +\* Multiplicity of value v in a sequence s (compares the two as multisets). +Count(v, s) == Cardinality({ k \in DOMAIN s : s[k] = v }) + +TypeOK == + /\ clock \in Nat + /\ sent \in [Idx -> BOOLEAN] + /\ \A k \in DOMAIN output : output[k] \in Values + /\ Len(output) =< Cardinality(Idx) + +Init == + /\ clock = 0 + /\ sent = [i \in Idx |-> FALSE] + /\ output = << >> + +\* Element i's timer has fired (its sleep of Input[i] seconds has elapsed) and +\* it has not yet been received. +Ready(i) == /\ ~sent[i] + /\ clock >= Input[i] + +AllDone == \A i \in Idx : sent[i] + +\* The collector receives one ready value (channel rendezvous: exactly one +\* value transfers, chosen nondeterministically among those currently ready). +Receive == + /\ \E i \in Idx : + /\ Ready(i) + /\ sent' = [sent EXCEPT ![i] = TRUE] + /\ output' = Append(output, Input[i]) + /\ clock' = clock + +\* Time advances only when no fired timer is waiting to be received: every +\* not-yet-received element still has its deadline strictly in the future. +\* This urgency is what guarantees shorter sleeps deliver before longer ones. +Tick == + /\ ~AllDone + /\ \A i \in Idx : ~sent[i] => clock < Input[i] + /\ clock' = clock + 1 + /\ UNCHANGED <> + +\* Once everything has been collected, stutter (models the closed channel / +\* finished range loop) so termination is not mistaken for a deadlock. +Done == + /\ AllDone + /\ UNCHANGED vars + +Next == Receive \/ Tick \/ Done + +Spec == Init /\ [][Next]_vars /\ WF_vars(Receive) /\ WF_vars(Tick) + +----------------------------------------------------------------------------- +\* Properties checked by TLC (see SleepSort.cfg). + +\* SAFETY: whatever has been collected so far is always non-decreasing. +IsSorted(s) == \A a, b \in DOMAIN s : a < b => s[a] <= s[b] +OutputSorted == IsSorted(output) + +\* SAFETY: the output never invents or duplicates values, and once finished it +\* is exactly a permutation (multiset) of the input. +PermutationWhenDone == + AllDone => \A v \in Values : Count(v, output) = Count(v, Input) + +\* LIVENESS: the collector eventually receives every value (no deadlock, no +\* value left sleeping forever) -- i.e. the algorithm terminates. +Terminates == <>AllDone + +\* Note: the state space is already finite without a constraint -- Tick is +\* disabled once clock reaches the largest input value, so clock never grows +\* unbounded and TLC explores every reachable state. +============================================================================= diff --git a/search/hash.go b/search/hash.go index 0b41b6b..7302d1a 100644 --- a/search/hash.go +++ b/search/hash.go @@ -26,7 +26,14 @@ func (h *Hash[K,V]) Size() int { } func (h *Hash[K,V]) hash(key K) int { - i := key + key*2 + key<<10 + key>>2 + // 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 } diff --git a/search/search_test.go b/search/search_test.go index 36ef4bf..b2c167a 100644 --- a/search/search_test.go +++ b/search/search_test.go @@ -45,7 +45,15 @@ func TestGoMap(t *testing.T) { } } +// shortMaxLength caps the largest input size exercised under `go test -short` +// (used by `make verify`, which runs under the race detector). The full range +// still runs in a plain `make test`. +const shortMaxLength int = 1000 + func test[K ds.Integer, V ds.Number](s Set[K,V], l int, t *testing.T) { + if testing.Short() && l > shortMaxLength { + t.Skipf("skipping size %d in -short mode", l) + } keys := ds.NewRandomArrayList[K](l, l) randoms := ds.NewRandomArrayList[V](l, -1) mapping := make(map[K]V, l) diff --git a/sort/insertion.go b/sort/insertion.go index a6b3c85..d869a7c 100644 --- a/sort/insertion.go +++ b/sort/insertion.go @@ -5,7 +5,7 @@ import ( ) func Insertion[V ds.Number](a ds.ArrayList[V]) ds.ArrayList[V] { - for i, _ := range a { + for i := range a { for j := i; j > 0; j-- { if a[j] > a[j-1] { break diff --git a/sort/property_test.go b/sort/property_test.go new file mode 100644 index 0000000..1f3dd88 --- /dev/null +++ b/sort/property_test.go @@ -0,0 +1,110 @@ +package sort + +import ( + "math/rand" + "testing" + quickcheck "testing/quick" // aliased: this package already has a quick() sort + + "codeberg.org/snonux/algorithms/ds" +) + +// This file provides property-based verification for every sort. Unlike the +// size-driven tests in sort_test.go, which only assert a.Sorted(), these tests +// also assert the *permutation* invariant: the output must contain exactly the +// same elements as the input. A buggy sort that drops or duplicates an element +// while still returning an ordered slice would pass a Sorted()-only check but +// fail here. Together, "ordered" + "permutation of the input" is the full +// functional-correctness postcondition proven on paper in docs/verification.md. + +// sortUnderTest is the shared signature of every sort in this package. An +// ds.ArrayList[int] shares []int's representation, so the property helpers +// convert between them for free. +type sortUnderTest func(ds.ArrayList[int]) ds.ArrayList[int] + +// allSorts lists every sort to verify, keyed by name for readable subtests. +func allSorts() map[string]sortUnderTest { + return map[string]sortUnderTest{ + "Selection": Selection[int], + "Insertion": Insertion[int], + "Shell": Shell[int], + "Merge": Merge[int], + "BottomUpMerge": BottomUpMerge[int], + "ParallelMerge": ParallelMerge[int], + "Quick": Quick[int], + "ParallelQuick": ParallelQuick[int], + "Quick3Way": Quick3Way[int], + } +} + +// sameMultiset reports whether b is a permutation of a: equal length and equal +// element multiplicities. This is the invariant the Sorted()-only tests miss. +func sameMultiset(a, b []int) bool { + if len(a) != len(b) { + return false + } + counts := make(map[int]int, len(a)) + for _, v := range a { + counts[v]++ + } + for _, v := range b { + counts[v]-- + if counts[v] < 0 { + return false // b has an element a doesn't have (enough of) + } + } + // Equal lengths plus no negative count implies the multisets match exactly. + return true +} + +// sortedPermutationOf runs sort on a copy of orig and checks both invariants: +// the result is ordered and is a permutation of orig. orig is not mutated. +func sortedPermutationOf(sort sortUnderTest, orig []int) bool { + work := make([]int, len(orig)) + copy(work, orig) + out := sort(ds.ArrayList[int](work)) + return out.Sorted() && sameMultiset(orig, out) +} + +// TestPropertyOrderedPermutation uses testing/quick to throw many randomly +// shaped small slices (arbitrary values, lengths up to ~50) at each sort, +// asserting the ordered-permutation property on every trial. +func TestPropertyOrderedPermutation(t *testing.T) { + cfg := &quickcheck.Config{MaxCount: 2000} + for name, sort := range allSorts() { + name, sort := name, sort + t.Run(name, func(t *testing.T) { + t.Parallel() + prop := func(in []int) bool { return sortedPermutationOf(sort, in) } + if err := quickcheck.Check(prop, cfg); err != nil { + t.Errorf("%s violated ordered-permutation property: %v", name, err) + } + }) + } +} + +// TestPropertySizes exercises input sizes that cross the algorithms' internal +// thresholds: the len<=10 insertion-sort cutoffs, the len<1000 sequential +// fallbacks in the parallel sorts, and the odd-length merge clamp. The largest +// sizes (which drive the real goroutine fan-out) run only outside -short. +func TestPropertySizes(t *testing.T) { + sizes := []int{0, 1, 2, 10, 11, 100, 999, 1000, 1001} + if !testing.Short() { + sizes = append(sizes, 5000, 20001) + } + for name, sort := range allSorts() { + name, sort := name, sort + t.Run(name, func(t *testing.T) { + t.Parallel() + rng := rand.New(rand.NewSource(1)) + for _, n := range sizes { + in := make([]int, n) + for i := range in { + in[i] = rng.Intn(50) - 25 // small range ⇒ many duplicates + } + if !sortedPermutationOf(sort, in) { + t.Errorf("%s failed ordered-permutation at size %d", name, n) + } + } + }) + } +} diff --git a/sort/sort_test.go b/sort/sort_test.go index b632be8..ee49893 100644 --- a/sort/sort_test.go +++ b/sort/sort_test.go @@ -15,10 +15,7 @@ const maxLength int = 1000000 const factor int = 100 const maxSlowLength int = 100000 -var arrayListCache map[string]ds.ArrayList[int] - type sortAlgorithm[V ds.Number] func(ds.ArrayList[V]) ds.ArrayList[V] -type sortAlgorithmInt func([]int) []int func TestSleepSort(t *testing.T) { a := ds.NewRandomArrayList[int](10, 10) @@ -153,8 +150,17 @@ func BenchmarkShuffleSort(b *testing.B) { } */ +// shortMaxLength caps the largest input size exercised under `go test -short` +// (used by `make verify`, which runs under the race detector where the +// million-element cases would be far too slow). The full range still runs in a +// plain `make test`. +const shortMaxLength int = 10000 + func test[V ds.Number](sort sortAlgorithm[V], l int, t *testing.T) { cb := func(t *testing.T) { + if testing.Short() && l > shortMaxLength { + t.Skipf("skipping size %d in -short mode", l) + } t.Parallel() a := ds.NewRandomArrayList[V](l, -1) a = sort(a) @@ -167,6 +173,9 @@ func test[V ds.Number](sort sortAlgorithm[V], l int, t *testing.T) { func testShuffleSort[V ds.Number](sort sortAlgorithm[V], l int, t *testing.T) { cb := func(t *testing.T) { + if testing.Short() && l > shortMaxLength { + t.Skipf("skipping size %d in -short mode", l) + } t.Parallel() a := sort(ds.NewAscendingArrayList[V](l)) if a.Sorted() { diff --git a/staticcheck.conf b/staticcheck.conf new file mode 100644 index 0000000..939bace --- /dev/null +++ b/staticcheck.conf @@ -0,0 +1,6 @@ +# The `verify` make target uses staticcheck as a correctness gate. We inherit +# staticcheck's default analyzers (bug detection SA*, simplifications S*, unused +# code U*) but disable ST1012, a purely cosmetic convention that error variables +# be named ErrFoo. Renaming the package's existing NotFound/NotImplemented would +# be lint churn unrelated to verification, so it is intentionally not enforced. +checks = ["inherit", "-ST1012"] -- cgit v1.2.3