1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
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.
|
