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