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 --- sort/sleep.go | 5 ++++- sort/sort_test.go | 17 +++++++++++++---- 2 files changed, 17 insertions(+), 5 deletions(-) (limited to 'sort') diff --git a/sort/sleep.go b/sort/sleep.go index 3ca45b2..146ff3a 100644 --- a/sort/sleep.go +++ b/sort/sleep.go @@ -7,7 +7,10 @@ import ( ) func Sleep[V ds.Integer](a ds.ArrayList[V]) ds.ArrayList[V] { - sorted := ds.NewArrayList[V](len(a)) + // Start empty with capacity len(a): the received values are appended below. + // NewArrayList(len(a)) would create a slice of that *length* (all zeros) and + // the appends would then produce len(a) spurious leading zeros. + sorted := make(ds.ArrayList[V], 0, len(a)) numCh := make(chan V) var wg sync.WaitGroup diff --git a/sort/sort_test.go b/sort/sort_test.go index ee49893..4fd2a04 100644 --- a/sort/sort_test.go +++ b/sort/sort_test.go @@ -18,10 +18,19 @@ const maxSlowLength int = 100000 type sortAlgorithm[V ds.Number] func(ds.ArrayList[V]) ds.ArrayList[V] func TestSleepSort(t *testing.T) { - a := ds.NewRandomArrayList[int](10, 10) - a = Sleep(a) - if !a.Sorted() { - t.Errorf("Array not sorted: %v", a) + orig := ds.NewRandomArrayList[int](10, 10) + in := make([]int, len(orig)) + copy(in, orig) + + out := Sleep(orig) + if !out.Sorted() { + t.Errorf("Array not sorted: %v", out) + } + // Also require the output to be a permutation of the input: sortedness alone + // would not catch a dropped or duplicated value. (Exhaustive termination / + // deadlock guarantees for the coordination live in formal/tla/SleepSort.tla.) + if !sameMultiset(in, out) { + t.Errorf("Sleep sort output is not a permutation of input: in=%v out=%v", in, out) } } -- cgit v1.2.3