From 2ae848dfe78d39890ce0b1d8eca283e2bfbc950e Mon Sep 17 00:00:00 2001
From: giles <giles.bradshaw@rose-ash.com>
Date: Fri, 8 May 2026 10:43:45 +0000
Subject: [PATCH] =?UTF-8?q?mk:=20laziness=20tests=20=E2=80=94=20Zzz-conde?=
 =?UTF-8?q?=20+=20interleaving=20fairness?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Verifies that the Zzz-wraps-each-conde-clause + mk-mplus-suspend-on-
paused-left machinery produces fair interleaving and gives finite
prefixes from infinitely-recursive relations:

- listo-aux has no base case under run* but run 4 q ... produces
  exactly the four shortest list shapes, in order.
- mk-disj of two infinite generators (ones-gen, twos-gen) with
  run 4 q ... must include both 1-prefixed and 2-prefixed answers
  (no starvation).
- run* terminates on a goal that has a finite answer set.

3 tests, 246/246 cumulative.
---
 lib/minikanren/tests/laziness.sx | 77 ++++++++++++++++++++++++++++++++
 plans/minikanren-on-sx.md        |  6 +++
 2 files changed, 83 insertions(+)
 create mode 100644 lib/minikanren/tests/laziness.sx

diff --git a/lib/minikanren/tests/laziness.sx b/lib/minikanren/tests/laziness.sx
new file mode 100644
index 00000000..d3440ac4
--- /dev/null
+++ b/lib/minikanren/tests/laziness.sx
@@ -0,0 +1,77 @@
+;; lib/minikanren/tests/laziness.sx — verify Zzz wrapping (in conde)
+;; lets infinitely-recursive relations produce finite prefixes via run-n.
+
+;; --- a relation that has no base case but conde-protects via Zzz ---
+
+(define
+  listo-aux
+  (fn
+    (l)
+    (conde ((nullo l)) ((fresh (a d) (conso a d l) (listo-aux d))))))
+
+(mk-test
+  "infinite-relation-truncates-via-run-n"
+  (run 4 q (listo-aux q))
+  (list
+    (list)
+    (list (make-symbol "_.0"))
+    (list (make-symbol "_.0") (make-symbol "_.1"))
+    (list (make-symbol "_.0") (make-symbol "_.1") (make-symbol "_.2"))))
+
+;; --- two infinite generators interleaved via mk-disj must both produce
+;;     answers (no starvation) — the fairness test ---
+
+(define
+  ones-gen
+  (fn
+    (l)
+    (conde
+      ((== l (list)))
+      ((fresh (d) (conso 1 d l) (ones-gen d))))))
+
+(define
+  twos-gen
+  (fn
+    (l)
+    (conde
+      ((== l (list)))
+      ((fresh (d) (conso 2 d l) (twos-gen d))))))
+
+(mk-test
+  "interleaving-keeps-both-streams-alive"
+  (let
+    ((res (run 4 q (mk-disj (ones-gen q) (twos-gen q)))))
+    (and
+      (= (len res) 4)
+      (and
+        (some
+          (fn
+            (x)
+            (and
+              (list? x)
+              (and (not (empty? x)) (= (first x) 1))))
+          res)
+        (some
+          (fn
+            (x)
+            (and
+              (list? x)
+              (and (not (empty? x)) (= (first x) 2))))
+          res))))
+  true)
+
+;; --- run* terminates on a relation whose conde has finite base case
+;;     reached from any starting point ---
+
+(mk-test
+  "run-star-terminates-on-bounded-relation"
+  (run*
+    q
+    (fresh
+      (l)
+      (== l (list 1 2 3))
+      (listo l)
+      (== q :ok)))
+  (list :ok))
+
+(mk-tests-run!)
diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md
index 35b5193d..4151863d 100644
--- a/plans/minikanren-on-sx.md
+++ b/plans/minikanren-on-sx.md
@@ -169,6 +169,12 @@ _(none yet)_
 
 _Newest first._
 
+- **2026-05-08** — **Laziness tests**: explicitly verifies the
+  Zzz-on-conde-clauses + mk-mplus-swap-on-paused machinery: an
+  infinitely-recursive relation truncated via `run 4 q (listo-aux q)`
+  produces exactly `(() (_.0) (_.0 _.1) (_.0 _.1 _.2))`; mixing two
+  infinite generators via `mk-disj` keeps both alive (no starvation);
+  `run*` terminates on a bounded query. 3 new tests, 246/246 cumulative.
 - **2026-05-08** — **N-queens (classic miniKanren benchmark green)**:
   `lib/minikanren/queens.sx`. Encoding cols(i) = column of queen in row i;
   `ino-each` + `all-distincto` cover row/column constraints; `safe-diag`