From 3f906d03262150892e2297e621bfc56e425ef142 Mon Sep 17 00:00:00 2001
From: Paul Buetow <paul@buetow.org>
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 <noreply@anthropic.com>
---
 queue/elementarypriority.go |  7 +++++
 queue/property_test.go      | 76 +++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 83 insertions(+)
 create mode 100644 queue/property_test.go

(limited to 'queue')

diff --git a/queue/elementarypriority.go b/queue/elementarypriority.go
index 391d948..9cb9e54 100644
--- a/queue/elementarypriority.go
+++ b/queue/elementarypriority.go
@@ -50,6 +50,13 @@ func (q *ElementaryPriority[T]) Clear() {
 }
 
 func (q *ElementaryPriority[T]) max() (ind int, max T) {
+	// Seed from the first element, not the zero value of T: for a queue holding
+	// only negative values nothing is greater than 0, so a zero seed would
+	// wrongly report index 0 / value 0 (an element not even in the queue).
+	if len(q.a) == 0 {
+		return 0, 0
+	}
+	ind, max = 0, q.a[0]
 	for i, a := range q.a {
 		if a > max {
 			ind, max = i, a
diff --git a/queue/property_test.go b/queue/property_test.go
new file mode 100644
index 0000000..e4ab044
--- /dev/null
+++ b/queue/property_test.go
@@ -0,0 +1,76 @@
+package queue
+
+import (
+	"testing"
+	"testing/quick"
+)
+
+// Property-based verification for the priority queues. The existing tests in
+// queue_test.go only check that DeleteMax yields a non-increasing sequence; they
+// never check *completeness* -- that every inserted element comes back out. A
+// queue that dropped, duplicated, or invented an element could still emit an
+// ordered sequence and pass. These tests add the missing multiset (permutation)
+// invariant, and -- because testing/quick generates negative values too -- they
+// also exercise inputs the fixed-seed NewRandomArrayList tests never reach.
+
+// sameMultiset reports whether b is a permutation of a.
+func sameMultiset(a, b []int) bool {
+	if len(a) != len(b) {
+		return false
+	}
+	counts := make(map[int]int, len(a))
+	for _, v := range a {
+		counts[v]++
+	}
+	for _, v := range b {
+		counts[v]--
+		if counts[v] < 0 {
+			return false
+		}
+	}
+	return true
+}
+
+// drainedInOrder inserts every value of in into a fresh queue, then drains it
+// with DeleteMax, checking two invariants: the drained sequence is
+// non-increasing (max-first) AND it is a permutation of the input (nothing
+// dropped, duplicated, or invented). Size must also match after all inserts.
+func drainedInOrder(newQ func() PriorityQueue, in []int) bool {
+	q := newQ()
+	for _, v := range in {
+		q.Insert(v)
+	}
+	if q.Size() != len(in) {
+		return false
+	}
+
+	out := make([]int, 0, len(in))
+	prev, started := 0, false
+	for !q.Empty() {
+		m := q.DeleteMax()
+		if started && m > prev {
+			return false // not non-increasing
+		}
+		prev, started = m, true
+		out = append(out, m)
+	}
+	return sameMultiset(in, out)
+}
+
+func TestPropertyPriorityQueues(t *testing.T) {
+	queues := map[string]func() PriorityQueue{
+		"ElementaryPriority": func() PriorityQueue { return NewElementaryPriority[int](1) },
+		"HeapPriority":       func() PriorityQueue { return NewHeapPriority[int](1) },
+	}
+	cfg := &quick.Config{MaxCount: 2000}
+	for name, newQ := range queues {
+		name, newQ := name, newQ
+		t.Run(name, func(t *testing.T) {
+			t.Parallel()
+			prop := func(in []int) bool { return drainedInOrder(newQ, in) }
+			if err := quick.Check(prop, cfg); err != nil {
+				t.Errorf("%s violated ordered-permutation property: %v", name, err)
+			}
+		})
+	}
+}
-- 
cgit v1.2.3