From f74812f8eda48194b622bdd318f35d3a6b6328cd Mon Sep 17 00:00:00 2001
From: Paul Buetow <paul@buetow.org>
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 <noreply@anthropic.com>
---
 formal/insertion.go | 42 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)
 create mode 100644 formal/insertion.go

(limited to 'formal/insertion.go')

diff --git a/formal/insertion.go b/formal/insertion.go
new file mode 100644
index 0000000..cf053a7
--- /dev/null
+++ b/formal/insertion.go
@@ -0,0 +1,42 @@
+package formal
+
+// Insertion sorts a in ascending order, in place. This is a monomorphized
+// (non-generic, plain []int, inlined swap) copy of sort.Insertion, annotated so
+// the Gobra verifier can prove -- with the Viper/Z3 backend -- BOTH:
+//
+//   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), and
+//   2. functional correctness (ordering): on return, a is sorted ascending
+//      (the postcondition "forall p<q :: a[p] <= a[q]").
+//
+// The permutation half of correctness (that the output is a rearrangement of
+// the input) is left to the property tests + the paper proof in
+// docs/verification.md; proving it here would require ghost multiset state.
+//
+//@ requires forall k int :: 0 <= k && k < len(a) ==> acc(&a[k])
+//@ ensures  forall k int :: 0 <= k && k < len(a) ==> acc(&a[k])
+//@ ensures  forall p, q int :: 0 <= p && p < q && q < len(a) ==> a[p] <= a[q]
+func Insertion(a []int) {
+	i := 0
+	//@ invariant 0 <= i && i <= len(a)
+	//@ invariant forall k int :: 0 <= k && k < len(a) ==> acc(&a[k])
+	// The prefix a[0..i) is already fully sorted.
+	//@ invariant forall p, q int :: 0 <= p && p < q && q < i ==> a[p] <= a[q]
+	for i < len(a) {
+		j := i
+		//@ invariant 0 <= j && j <= i && i < len(a)
+		//@ invariant forall k int :: 0 <= k && k < len(a) ==> acc(&a[k])
+		// a[0..i] is sorted once position j is ignored as either endpoint...
+		//@ invariant forall p, q int :: 0 <= p && p < q && q <= i && p != j && q != j ==> a[p] <= a[q]
+		// ...and the in-flight element a[j] is <= everything to its right.
+		//@ invariant forall q int :: j < q && q <= i ==> a[j] <= a[q]
+		for j > 0 && a[j] < a[j-1] {
+			tmp := a[j]
+			a[j] = a[j-1]
+			a[j-1] = tmp
+			j = j - 1
+		}
+		i = i + 1
+	}
+}
-- 
cgit v1.2.3