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 --- search/hash.go | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'search/hash.go') 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 } -- cgit v1.2.3