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 --- sort/sort_test.go | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'sort/sort_test.go') diff --git a/sort/sort_test.go b/sort/sort_test.go index b632be8..ee49893 100644 --- a/sort/sort_test.go +++ b/sort/sort_test.go @@ -15,10 +15,7 @@ const maxLength int = 1000000 const factor int = 100 const maxSlowLength int = 100000 -var arrayListCache map[string]ds.ArrayList[int] - type sortAlgorithm[V ds.Number] func(ds.ArrayList[V]) ds.ArrayList[V] -type sortAlgorithmInt func([]int) []int func TestSleepSort(t *testing.T) { a := ds.NewRandomArrayList[int](10, 10) @@ -153,8 +150,17 @@ func BenchmarkShuffleSort(b *testing.B) { } */ +// shortMaxLength caps the largest input size exercised under `go test -short` +// (used by `make verify`, which runs under the race detector where the +// million-element cases would be far too slow). The full range still runs in a +// plain `make test`. +const shortMaxLength int = 10000 + func test[V ds.Number](sort sortAlgorithm[V], l int, t *testing.T) { cb := func(t *testing.T) { + if testing.Short() && l > shortMaxLength { + t.Skipf("skipping size %d in -short mode", l) + } t.Parallel() a := ds.NewRandomArrayList[V](l, -1) a = sort(a) @@ -167,6 +173,9 @@ func test[V ds.Number](sort sortAlgorithm[V], l int, t *testing.T) { func testShuffleSort[V ds.Number](sort sortAlgorithm[V], l int, t *testing.T) { cb := func(t *testing.T) { + if testing.Short() && l > shortMaxLength { + t.Skipf("skipping size %d in -short mode", l) + } t.Parallel() a := sort(ds.NewAscendingArrayList[V](l)) if a.Sorted() { -- cgit v1.2.3