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 --- formal/README.md | 59 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 59 insertions(+) create mode 100644 formal/README.md (limited to 'formal/README.md') diff --git a/formal/README.md b/formal/README.md new file mode 100644 index 0000000..f667bdf --- /dev/null +++ b/formal/README.md @@ -0,0 +1,59 @@ +# Gobra deductive proof + +`insertion.go` is a **machine-checked** proof that an insertion sort is correct, +verified by [Gobra](https://github.com/viperproject/gobra) — ETH Zurich's +deductive verifier for Go, which translates annotated Go to the Viper +intermediate language and discharges the proof obligations with the Z3 SMT +solver. + +Unlike the TLA+ model (which checks a hand-written abstraction) and the property +tests (which sample inputs), this verifies the **actual Go source** for **all** +inputs. Gobra proves two things about `Insertion`: + +1. **Memory safety** — every index access is in bounds. The permission + invariants `forall k :: 0 <= k < len(a) ==> acc(&a[k])` carry write access to + every element through both loops; Go itself cannot prove the absence of + index-out-of-range panics, Gobra can. +2. **Ordering** — on return `a` is sorted ascending + (`forall p < q :: a[p] <= a[q]`), established via the two insertion-sort loop + invariants in the annotations. + +The **permutation** half of full correctness (output is a rearrangement of the +input) is intentionally left to the property tests and the paper proof in +[`docs/verification.md`](../docs/verification.md); proving it in Gobra needs +ghost multiset state and is noted there as future work. + +## Why a separate, non-generic copy? + +Gobra's support for Go generics and method-based abstractions is limited, so +this file is a deliberately monomorphized copy of `sort.Insertion` +([`sort/insertion.go`](../sort/insertion.go)): plain `[]int` instead of +`ds.ArrayList[V]`, and an inlined swap instead of the `.Swap` method. The +algorithm is otherwise identical. + +## Running + +Gobra is distributed as a container image (it bundles its own Z3, so no separate +solver install is needed). With `podman` (or `docker`): + +```sh +podman pull ghcr.io/viperproject/gobra:latest +make verify-formal +``` + +or directly: + +```sh +podman run --rm -v "$PWD/formal:/gobra/formal:z" \ + ghcr.io/viperproject/gobra:latest -i /gobra/formal/insertion.go +``` + +Expected output ends with: + +``` +Gobra found 0 errors. +``` + +To convince yourself the proof is not vacuous, flip the inner comparison +`a[j] < a[j-1]` to `>` and re-run: Gobra reports +`Loop invariant might not be preserved`. -- cgit v1.2.3