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