From 3f906d03262150892e2297e621bfc56e425ef142 Mon Sep 17 00:00:00 2001 From: Paul Buetow Date: Mon, 6 Jul 2026 10:32:34 +0300 Subject: Close verification-coverage gaps; harness finds two more bugs Extends the verification harness from sorts-only to the whole repo, and in doing so surfaces two further latent bugs (on top of the earlier hash-shift one): Bugs found and fixed: - queue/elementarypriority.go: max() seeded at the zero value, so an all-negative queue reported a phantom max of 0 and DeleteMax returned/removed the wrong element. Caught by the new queue permutation property (testing/quick generates negatives; the old test data never did). Seed from a[0] instead. - sort/sleep.go: result built on NewArrayList(len(a)) -- a slice of that LENGTH (len(a) zeros) -- then appended to, yielding double-length output with leading zeros. The old .Sorted()-only test passed because zeros-then-ascending is sorted. Caught by the new Sleep permutation check. Build from an empty slice. Coverage added: - queue/property_test.go: ordering + permutation (completeness) for both queues. - TestSleepSort now also checks permutation, not just Sorted(). - docs/verification.md: paper proofs for all search/set structures (Elementary, Hash, BST, red-black BST invariants, GoMap) and both priority queues. - formal/tla/ParallelSort.tla: exhaustive fork/join model of ParallelMerge/ ParallelQuick -- disjoint write-ranges (no data race) + termination. Wired into make verify-model. - formal/selection.go: second Gobra proof (memory safety + sortedness). Wired into make verify-formal. - docs/case-study-bugs-found.md: extensive write-up of all three bugs, how each was caught, why the old tests missed it, and the fix (supersedes the earlier single-bug case study). Co-Authored-By: Claude Opus 4.8 --- formal/selection.go | 48 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) create mode 100644 formal/selection.go (limited to 'formal/selection.go') diff --git a/formal/selection.go b/formal/selection.go new file mode 100644 index 0000000..1a9028d --- /dev/null +++ b/formal/selection.go @@ -0,0 +1,48 @@ +package formal + +// Selection sorts a in ascending order, in place. This is a monomorphized +// (non-generic, plain []int, inlined swap, no `continue`) copy of +// sort.Selection, annotated so Gobra proves memory safety AND that the result +// is sorted ascending, for all inputs. +// +// Selection sort's proof needs a stronger outer invariant than insertion sort: +// not only is the prefix a[0..i) sorted, but every element of that prefix is +// <= every element of the unsorted suffix a[i..len). That second invariant is +// what lets the newly selected minimum extend the sorted prefix. +// +//@ 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 Selection(a []int) { + i := 0 + //@ invariant 0 <= i && i <= len(a) + //@ invariant forall k int :: 0 <= k && k < len(a) ==> acc(&a[k]) + // a[0..i) is sorted... + //@ invariant forall p, q int :: 0 <= p && p < q && q < i ==> a[p] <= a[q] + // ...and every prefix element is <= every suffix element. + //@ invariant forall p, q int :: 0 <= p && p < i && i <= q && q < len(a) ==> a[p] <= a[q] + for i < len(a) { + min := i + j := i + 1 + //@ invariant i < len(a) && i+1 <= j && j <= len(a) + //@ invariant i <= min && min < len(a) + //@ invariant forall k int :: 0 <= k && k < len(a) ==> acc(&a[k]) + // a[min] is the smallest of the scanned suffix a[i..j). + //@ invariant forall k int :: i <= k && k < j ==> a[min] <= a[k] + // The outer invariants still hold (the inner loop reads only). + //@ invariant forall p, q int :: 0 <= p && p < q && q < i ==> a[p] <= a[q] + //@ invariant forall p, q int :: 0 <= p && p < i && i <= q && q < len(a) ==> a[p] <= a[q] + for j < len(a) { + if a[j] < a[min] { + min = j + } + j = j + 1 + } + if min != i { + tmp := a[i] + a[i] = a[min] + a[min] = tmp + } + i = i + 1 + } +} -- cgit v1.2.3