diff options
Diffstat (limited to 'docs/case-study-bugs-found.md')
| -rw-r--r-- | docs/case-study-bugs-found.md | 218 |
1 files changed, 218 insertions, 0 deletions
diff --git a/docs/case-study-bugs-found.md b/docs/case-study-bugs-found.md new file mode 100644 index 0000000..3f5f0a9 --- /dev/null +++ b/docs/case-study-bugs-found.md @@ -0,0 +1,218 @@ +# Case study: three latent bugs the verification harness found + +Adding the verification layers (see [`verification.md`](verification.md)) did not +just re-confirm working code — it surfaced **three real, pre-existing bugs**, all +invisible to the original test suite. Each is documented below with how it was +caught, why it is genuinely wrong, why the old tests missed it, and the fix. + +A theme runs through all three: the original tests were **too weak in a specific +dimension**, and the new checks are strong in exactly that dimension. + +| # | Location | Bug | Caught by | Old test's blind spot | +|---|----------|-----|-----------|-----------------------| +| 1 | `search/hash.go` | shift wider than a narrow key type → term is always 0 | `go vet` (in `make verify`) | only ever used 64-bit `int` keys | +| 2 | `queue/elementarypriority.go` | `max()` seeded at `0` → wrong for all-negative queues | queue permutation property | test data was never negative | +| 3 | `sort/sleep.go` | result built on a pre-sized slice → doubled length with leading zeros | sleep permutation property | only checked `.Sorted()`, not completeness | + +--- + +## Bug 1 — a shift wider than the key type (`search/hash.go`) + +### The offending code + +```go +func (h *Hash[K,V]) hash(key K) int { + i := key + key*2 + key<<10 + key>>2 + ... +} +``` + +`K` is constrained by `ds.Integer`, so it may be **any** width down to `int8`. +The `key<<10` term is meant to spread low bits into high bits. + +### What the tool reported + +``` +$ make verify +go vet ./... +search/hash.go:29:21: key (may be 8 bits) too small for shift of 10 +``` + +`go vet`'s shift analyzer is a lightweight formal check: for every shift it +computes a conservative lower bound on the left operand's bit width and flags any +shift count `>=` that width. The narrowest `K` can be is `int8` (8 bits), and +`10 >= 8`. + +### Why it is genuinely a bug (Go shift semantics) + +The Go spec defines non-constant left shifts operationally: *"Shifts behave as if +the left operand is shifted n times by 1 … There is no upper limit on the shift +count."* Shifting an 8-bit value ten times pushes every bit out of the value's +width, so for `K = int8`/`uint8`: + +``` +key<<10 == 0 // always, for every key +``` + +The intended high-bit mixing silently disappears. Note it is width-dependent +(fine for `int16`+), and it is a *distribution/quality* bug, not a Set-contract +violation — chaining keeps the table correct, but narrow-key instantiations +degrade toward `O(n)` per operation. Exactly the kind of silent rot no assertion +would flag. + +### Why the tests missed it + +Every test uses `int` keys (`test[int,int](NewHash[int,int](i*2), …)`), where +`int` is 64 bits and the shift is fine. The bug lives in the **type dimension**, +not the value dimension — no value-space test or fuzzer over `int` could reach +it; only a type-aware tool (or an actual `int8` instantiation) can. + +### The fix + +```go +func (h *Hash[K,V]) hash(key K) int { + // Mix the key in a full-width int64 rather than in K. ... + i := int64(key) + i = i + i*2 + i<<10 + i>>2 + ... +} +``` + +Widening to `int64` before the shift keeps the result **byte-identical for +64-bit `int` keys** (so all existing tests still pass unchanged) while making the +mixing well-defined for every width. It does not *suppress* the warning; it +removes the condition (`shift >= width`) that made it true. + +--- + +## Bug 2 — a maximum seeded at zero (`queue/elementarypriority.go`) + +### The offending code + +```go +func (q *ElementaryPriority[T]) max() (ind int, max T) { + for i, a := range q.a { + if a > max { // max starts at the zero value of T, i.e. 0 + ind, max = i, a + } + } + return ind, max +} +``` + +`max` is a named return, so it starts at `T`'s zero value, `0`. + +### How it was caught + +The new completeness/permutation property in `queue/property_test.go` drives +each queue with `testing/quick`, which generates **negative** values too. It +failed immediately for `ElementaryPriority` (and passed for `HeapPriority`): + +``` +ElementaryPriority violated ordered-permutation property: + #1: failed on input []int{-1881664299226649700, 1264358012858162353, ...} +``` + +### Why it is genuinely a bug + +If **every** element in the queue is negative, no element is `> 0`, so the loop +never updates and `max()` returns `(0, 0)` — reporting a maximum of `0`, a value +that is not even in the queue. `DeleteMax` then removes the wrong element (index +0) and returns a phantom `0`. Both the ordering and completeness of a drain +break. + +### Why the tests missed it + +The original queue test builds inputs with +`ds.NewRandomArrayList[int](l, -1)`, whose values come from `rand.Int()` — always +**non-negative**. And `queue_test.go` only checked that `DeleteMax` was +non-increasing; it never checked that all inserted elements come back. So a queue +of non-negative numbers, checked only for ordering, sailed through. + +### The fix + +```go + if len(q.a) == 0 { + return 0, 0 + } + ind, max = 0, q.a[0] // seed from a real element, not the zero value + for i, a := range q.a { + if a > max { ind, max = i, a } + } +``` + +Seeding from `q.a[0]` makes the scan correct for any value range. +(`HeapPriority` was already immune: it compares actual array elements and returns +`a[1]` as the max.) + +--- + +## Bug 3 — a sort that doubled its output (`sort/sleep.go`) + +### The offending code + +```go +func Sleep[V ds.Integer](a ds.ArrayList[V]) ds.ArrayList[V] { + sorted := ds.NewArrayList[V](len(a)) // slice of LENGTH len(a): len(a) zeros + ... + for num := range numCh { + sorted = append(sorted, num) // appends AFTER those zeros + } + return sorted +} +``` + +`ds.NewArrayList(len(a))` is `make(ArrayList, len(a))` — a slice of that +**length**, pre-filled with `len(a)` zeros. Appending then adds the real values +*after* them. + +### How it was caught + +`TestSleepSort`, strengthened to check permutation, failed: + +``` +Sleep sort output is not a permutation of input: + in =[1 1 2 8 8 7 3 0 6 7] (10 elements) + out=[0 0 0 0 0 0 0 0 0 0 0 1 1 2 3 6 7 7 8 8] (21 elements!) +``` + +The output is **eleven leading zeros followed by the ten real values** — more +than double the input length. + +### Why the tests missed it + +The original `TestSleepSort` only asserted `a.Sorted()`. Zeros followed by an +ascending sequence **is** sorted, so the wildly-wrong 21-element result passed. +This is the textbook case for the *permutation* invariant: ordering alone cannot +detect dropped, duplicated, or (here) invented elements. + +### The fix + +```go + // Start empty with capacity len(a): the received values are appended below. + sorted := make(ds.ArrayList[V], 0, len(a)) +``` + +Length `0`, capacity `len(a)`: the appends now fill it to exactly `len(a)` +elements with no spurious zeros. + +--- + +## The through-line + +Two independent lessons, each reinforced twice: + +1. **Ordering is not correctness.** Bugs 2 and 3 both produced *ordered* output + that was wrong (missing/extra elements). Only the **permutation / completeness** + invariant — added to the sort and queue property tests — catches them. This is + the single most valuable check added by this work. + +2. **Test data has blind spots the code doesn't.** Bugs 1 and 2 both hid behind + the test suite's fixed input distribution — always 64-bit, always + non-negative. `go vet` (reasoning over *types*) and `testing/quick` (sampling + the *whole* value range, negatives included) each see past a blind spot that + hand-picked or `rand.Int()` data does not. + +None of these required the heavy layers (TLA+, Gobra). The cheapest checks — +`go vet` and a stronger property assertion — found all three. Breadth first; +depth where it earns its keep. |