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/README.md | 25 ++++++++++++++----------- 1 file changed, 14 insertions(+), 11 deletions(-) (limited to 'formal/README.md') diff --git a/formal/README.md b/formal/README.md index f667bdf..1bbb7e0 100644 --- a/formal/README.md +++ b/formal/README.md @@ -1,22 +1,24 @@ -# Gobra deductive proof +# Gobra deductive proofs -`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 +`insertion.go` and `selection.go` are **machine-checked** proofs that these +sorts are 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`: +Unlike the TLA+ models (which check a hand-written abstraction) and the property +tests (which sample inputs), these verify the **actual Go source** for **all** +inputs. Gobra proves two things about each sort: 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. + (`forall p < q :: a[p] <= a[q]`), established via the loop invariants in the + annotations. Selection sort needs the stronger "every prefix element ≤ every + suffix element" invariant; insertion sort uses a "sorted except at the + in-flight index" invariant. 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 @@ -45,7 +47,8 @@ or directly: ```sh podman run --rm -v "$PWD/formal:/gobra/formal:z" \ - ghcr.io/viperproject/gobra:latest -i /gobra/formal/insertion.go + ghcr.io/viperproject/gobra:latest \ + -i /gobra/formal/insertion.go /gobra/formal/selection.go ``` Expected output ends with: -- cgit v1.2.3