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 --- Makefile | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) (limited to 'Makefile') diff --git a/Makefile b/Makefile index fab5d52..8632e8c 100644 --- a/Makefile +++ b/Makefile @@ -1,6 +1,30 @@ test: go clean -testcache go test ./... -v + +# verify: static + dynamic correctness checks. Fast enough for routine use. +# go vet / staticcheck - static analysis +# go test -race -short - race detector over the (size-capped) test + property +# suites; -short keeps the million-element cases out so +# the race build stays quick. See docs/verification.md. +verify: + go vet ./... + staticcheck ./... + go test -race -short ./... + +# verify-model: exhaustively model-check the concurrent sleep sort with TLA+/TLC +# (a model of sort/sleep.go, not the Go code itself). See formal/tla/README.md. +verify-model: + java -cp $(HOME)/tools/tlaplus/tla2tools.jar tlc2.TLC -workers auto \ + -metadir /tmp/tlc-algorithms \ + -config formal/tla/SleepSort.cfg formal/tla/SleepSort.tla + +# verify-formal: machine-checked deductive proof of a monomorphized insertion +# sort with Gobra (Go verifier, Viper+Z3 backend), run from its container image. +# See formal/README.md. +verify-formal: + podman run --rm -v $(PWD)/formal:/gobra/formal:z \ + ghcr.io/viperproject/gobra:latest -i /gobra/formal/insertion.go bench: go test -run=xxx -bench=. ./... | tee bench.out sortbench: -- cgit v1.2.3