mk: cyclic-graph behaviour test — motivates Phase 7 tabling

Demonstrates the naive-patho behaviour on a 2-cycle (a <-> b, plus
b -> c). Without Phase-7 tabling, the search produces ever-longer
paths: (a b), (a b a b), (a b a b a b), ... `run 5` truncates to a
finite prefix; `run*` diverges. Documenting this as a regression-style
test gives Phase 7 a concrete starting point.

3 new tests, 331/331 cumulative.

lib/minikanren/conda.sx

@@ -0,0 +1,42 @@
+;; lib/minikanren/conda.sx — Phase 5 piece A: `conda`, the soft-cut.
+;;
+;;   (conda (g0 g ...) (h0 h ...) ...)
+;;     — first clause whose head g0 produces ANY answer wins; ALL of g0's
+;;       answers are then conj'd with the rest of that clause; later
+;;       clauses are NOT tried.
+;;     — differs from condu only in not wrapping g0 in onceo: condu
+;;       commits to the SINGLE first answer, conda lets the head's full
+;;       answer-set flow into the rest of the clause.
+;;       (Reasoned Schemer chapter 10; Byrd 5.3.)
+
+(define
+  conda-try
+  (fn
+    (clauses s)
+    (cond
+      ((empty? clauses) mzero)
+      (:else
+        (let
+          ((cl (first clauses)))
+          (let
+            ((head-goal (first cl)) (rest-goals (rest cl)))
+            (let
+              ((peek (stream-take 1 (head-goal s))))
+              (if
+                (empty? peek)
+                (conda-try (rest clauses) s)
+                (mk-bind (head-goal s) (mk-conj-list rest-goals))))))))))
+
+(defmacro
+  conda
+  (&rest clauses)
+  (quasiquote
+    (fn
+      (s)
+      (conda-try
+        (list
+          (splice-unquote
+            (map
+              (fn (cl) (quasiquote (list (splice-unquote cl))))
+              clauses)))
+        s))))

lib/minikanren/conde.sx

@@ -0,0 +1,39 @@
+;; lib/minikanren/conde.sx — Phase 2 piece C: `conde`, the canonical
+;; miniKanren and-or form, with implicit Zzz inverse-eta delay so recursive
+;; relations like appendo terminate.
+;;
+;;   (conde (g1a g1b ...) (g2a g2b ...) ...)
+;;     ≡ (mk-disj (Zzz (mk-conj g1a g1b ...))
+;;                (Zzz (mk-conj g2a g2b ...)) ...)
+;;
+;; `Zzz g` wraps a goal expression in (fn (S) (fn () (g S))) so that
+;; `g`'s body isn't constructed until the surrounding fn is applied to a
+;; substitution AND the returned thunk is forced. This is what gives
+;; miniKanren its laziness — recursive goal definitions can be `(conde
+;; ... (... (recur ...)))` without infinite descent at construction time.
+;;
+;; Hygiene: the substitution parameter is gensym'd so that user goal
+;; expressions which themselves bind `s` (e.g. `(appendo l s ls)`) keep
+;; their lexical `s` and don't accidentally reference the wrapper's
+;; substitution. Without gensym, miniKanren relations that follow the
+;; common (l s ls) parameter convention are silently miscompiled.
+
+(defmacro
+  Zzz
+  (g)
+  (let
+    ((s-sym (gensym "zzz-s-")))
+    (quasiquote
+      (fn ((unquote s-sym)) (fn () ((unquote g) (unquote s-sym)))))))
+
+(defmacro
+  conde
+  (&rest clauses)
+  (quasiquote
+    (mk-disj
+      (splice-unquote
+        (map
+          (fn
+            (clause)
+            (quasiquote (Zzz (mk-conj (splice-unquote clause)))))
+          clauses)))))

lib/minikanren/condu.sx

@@ -0,0 +1,58 @@
+;; lib/minikanren/condu.sx — Phase 2 piece D: `condu` and `onceo`.
+;;
+;; Both are commitment forms (no backtracking into discarded options):
+;;
+;;   (onceo g)        — succeeds at most once: takes the first answer
+;;                      stream-take produces from (g s).
+;;
+;;   (condu (g0 g ...) (h0 h ...) ...)
+;;                    — first clause whose head goal succeeds wins; only
+;;                      the first answer of the head is propagated to the
+;;                      rest of that clause; later clauses are not tried.
+;;                      (Reasoned Schemer chapter 10; Byrd 5.4.)
+
+(define
+  onceo
+  (fn
+    (g)
+    (fn
+      (s)
+      (let
+        ((peek (stream-take 1 (g s))))
+        (if (empty? peek) mzero (unit (first peek)))))))
+
+;; condu-try — runtime walker over a list of clauses (each clause a list of
+;; goals). Forces the head with stream-take 1; if head fails, recurse to
+;; the next clause; if head succeeds, commits its single answer through
+;; the rest of the clause.
+(define
+  condu-try
+  (fn
+    (clauses s)
+    (cond
+      ((empty? clauses) mzero)
+      (:else
+        (let
+          ((cl (first clauses)))
+          (let
+            ((head-goal (first cl)) (rest-goals (rest cl)))
+            (let
+              ((peek (stream-take 1 (head-goal s))))
+              (if
+                (empty? peek)
+                (condu-try (rest clauses) s)
+                ((mk-conj-list rest-goals) (first peek))))))))))
+
+(defmacro
+  condu
+  (&rest clauses)
+  (quasiquote
+    (fn
+      (s)
+      (condu-try
+        (list
+          (splice-unquote
+            (map
+              (fn (cl) (quasiquote (list (splice-unquote cl))))
+              clauses)))
+        s))))

lib/minikanren/fd.sx

@@ -0,0 +1,25 @@
+;; lib/minikanren/fd.sx — Phase 6 piece A: minimal finite-domain helpers.
+;;
+;; A full CLP(FD) engine (arc consistency, native integer domains, fd-plus
+;; etc.) is Phase 6 proper. For now we expose two small relations layered
+;; on the existing list machinery — they're sufficient for permutation
+;; puzzles, the N-queens-style core of constraint solving:
+;;
+;;   (ino x dom)         — x is a member of dom (alias for membero with the
+;;                         constraint-store-friendly argument order).
+;;   (all-distincto l)   — all elements of l are pairwise distinct.
+;;
+;; all-distincto uses nafc + membero on the tail — it requires the head
+;; element of each recursive step to be ground enough for membero to be
+;; finitary, so order matters: prefer (in x dom) goals BEFORE
+;; (all-distincto (list x ...)) so values get committed first.
+
+(define ino (fn (x dom) (membero x dom)))
+
+(define
+  all-distincto
+  (fn
+    (l)
+    (conde
+      ((nullo l))
+      ((fresh (a d) (conso a d l) (nafc (membero a d)) (all-distincto d))))))

lib/minikanren/fresh.sx

@@ -0,0 +1,23 @@
+;; lib/minikanren/fresh.sx — Phase 2 piece B: `fresh` for introducing
+;; logic variables inside a goal body.
+;;
+;;   (fresh (x y z) goal1 goal2 ...)
+;;     ≡ (let ((x (make-var)) (y (make-var)) (z (make-var)))
+;;         (mk-conj goal1 goal2 ...))
+;;
+;; A macro rather than a function so user-named vars are real lexical
+;; bindings — which is also what miniKanren convention expects.
+;; The empty-vars form (fresh () goal ...) is just a goal grouping.
+
+(defmacro
+  fresh
+  (vars &rest goals)
+  (quasiquote
+    (let
+      (unquote (map (fn (v) (list v (list (quote make-var)))) vars))
+      (mk-conj (splice-unquote goals)))))
+
+;; call-fresh — functional alternative for code that builds goals
+;; programmatically:
+;;   ((call-fresh (fn (x) (== x 7))) empty-s) → ({:_.N 7})
+(define call-fresh (fn (f) (fn (s) ((f (make-var)) s))))

lib/minikanren/goals.sx

@@ -0,0 +1,58 @@
+;; lib/minikanren/goals.sx — Phase 2 piece B: core goals.
+;;
+;; A goal is a function (fn (s) → stream-of-substitutions).
+;; Goals built here:
+;;   succeed         — always returns (unit s)
+;;   fail            — always returns mzero
+;;   ==              — unifies two terms; succeeds with a singleton, else fails
+;;   ==-check        — opt-in occurs-checked equality
+;;   conj2 / mk-conj — sequential conjunction of goals
+;;   disj2 / mk-disj — interleaved disjunction of goals (raw — `conde` adds
+;;                     the implicit-conj-per-clause sugar in a later commit)
+
+(define succeed (fn (s) (unit s)))
+
+(define fail (fn (s) mzero))
+
+(define
+  ==
+  (fn
+    (u v)
+    (fn
+      (s)
+      (let ((s2 (mk-unify u v s))) (if (= s2 nil) mzero (unit s2))))))
+
+(define
+  ==-check
+  (fn
+    (u v)
+    (fn
+      (s)
+      (let ((s2 (mk-unify-check u v s))) (if (= s2 nil) mzero (unit s2))))))
+
+(define conj2 (fn (g1 g2) (fn (s) (mk-bind (g1 s) g2))))
+
+(define disj2 (fn (g1 g2) (fn (s) (mk-mplus (g1 s) (g2 s)))))
+
+;; Fold goals in a list. (mk-conj-list ()) ≡ succeed; (mk-disj-list ()) ≡ fail.
+(define
+  mk-conj-list
+  (fn
+    (gs)
+    (cond
+      ((empty? gs) succeed)
+      ((empty? (rest gs)) (first gs))
+      (:else (conj2 (first gs) (mk-conj-list (rest gs)))))))
+
+(define
+  mk-disj-list
+  (fn
+    (gs)
+    (cond
+      ((empty? gs) fail)
+      ((empty? (rest gs)) (first gs))
+      (:else (disj2 (first gs) (mk-disj-list (rest gs)))))))
+
+(define mk-conj (fn (&rest gs) (mk-conj-list gs)))
+
+(define mk-disj (fn (&rest gs) (mk-disj-list gs)))

lib/minikanren/intarith.sx

@@ -0,0 +1,62 @@
+;; lib/minikanren/intarith.sx — fast integer arithmetic via project.
+;;
+;; These are ground-only escapes into host arithmetic. They run at native
+;; speed (host ints) but require their arguments to walk to actual numbers
+;; — they are not relational the way `pluso` (Peano) is. Use them when
+;; the puzzle size makes Peano impractical.
+;;
+;; Naming: `-i` suffix marks "integer-only" goals.
+
+(define
+  pluso-i
+  (fn
+    (a b c)
+    (project
+      (a b)
+      (if (and (number? a) (number? b)) (== c (+ a b)) fail))))
+
+(define
+  minuso-i
+  (fn
+    (a b c)
+    (project
+      (a b)
+      (if (and (number? a) (number? b)) (== c (- a b)) fail))))
+
+(define
+  *o-i
+  (fn
+    (a b c)
+    (project
+      (a b)
+      (if (and (number? a) (number? b)) (== c (* a b)) fail))))
+
+(define
+  lto-i
+  (fn
+    (a b)
+    (project
+      (a b)
+      (if (and (number? a) (and (number? b) (< a b))) succeed fail))))
+
+(define
+  lteo-i
+  (fn
+    (a b)
+    (project
+      (a b)
+      (if (and (number? a) (and (number? b) (<= a b))) succeed fail))))
+
+(define
+  neqo-i
+  (fn
+    (a b)
+    (project
+      (a b)
+      (if (and (number? a) (and (number? b) (not (= a b)))) succeed fail))))
+
+(define numbero (fn (x) (project (x) (if (number? x) succeed fail))))
+
+(define stringo (fn (x) (project (x) (if (string? x) succeed fail))))
+
+(define symbolo (fn (x) (project (x) (if (symbol? x) succeed fail))))

lib/minikanren/matche.sx

@@ -0,0 +1,76 @@
+;; lib/minikanren/matche.sx — Phase 5 piece D: pattern matching over terms.
+;;
+;;   (matche TARGET
+;;     (PATTERN1 g1 g2 ...)
+;;     (PATTERN2 g1 ...)
+;;     ...)
+;;
+;; Pattern grammar:
+;;   _                 wildcard — fresh anonymous var
+;;   x                 plain symbol — fresh var, bind by name
+;;   ATOM              literal (number, string, boolean) — must equal
+;;   :keyword          keyword literal — emitted bare (keywords self-evaluate
+;;                     to their string name in SX, so quoting them changes
+;;                     their type from string to keyword)
+;;   ()                empty list — must equal
+;;   (p1 p2 ... pn)    list pattern — recurse on each element
+;;
+;; The macro expands to a `conde` whose clauses are
+;;   `((fresh (vars-in-pat) (== target pat-expr) body...))`.
+;;
+;; Repeated symbol names within a pattern produce the same fresh var, so
+;; they unify by `==`. Fixed-length list patterns only — head/tail
+;; destructuring uses `(fresh (a d) (conso a d target) body)` directly.
+;;
+;; Note: the macro builds the expansion via `cons` / `list` rather than a
+;; quasiquote — quasiquote does not recurse into nested lambda bodies in
+;; SX, so `\`(matche-clause (quote ,target) cl)` left literal
+;; `(unquote target)` in the output.
+
+(define matche-symbol-var? (fn (s) (symbol? s)))
+
+(define
+  matche-collect-vars-acc
+  (fn
+    (pat acc)
+    (cond
+      ((matche-symbol-var? pat)
+        (if (some (fn (s) (= s pat)) acc) acc (append acc (list pat))))
+      ((and (list? pat) (not (empty? pat)))
+        (reduce (fn (a p) (matche-collect-vars-acc p a)) acc pat))
+      (:else acc))))
+
+(define
+  matche-collect-vars
+  (fn (pat) (matche-collect-vars-acc pat (list))))
+
+(define
+  matche-pattern->expr
+  (fn
+    (pat)
+    (cond
+      ((matche-symbol-var? pat) pat)
+      ((and (list? pat) (empty? pat)) (list (quote list)))
+      ((list? pat) (cons (quote list) (map matche-pattern->expr pat)))
+      ((keyword? pat) pat)
+      (:else (list (quote quote) pat)))))
+
+(define
+  matche-clause
+  (fn
+    (target cl)
+    (let
+      ((pat (first cl)) (body (rest cl)))
+      (let
+        ((vars (matche-collect-vars pat)))
+        (let
+          ((pat-expr (matche-pattern->expr pat)))
+          (list
+            (cons
+              (quote fresh)
+              (cons vars (cons (list (quote ==) target pat-expr) body)))))))))
+
+(defmacro
+  matche
+  (target &rest clauses)
+  (cons (quote conde) (map (fn (cl) (matche-clause target cl)) clauses)))

lib/minikanren/nafc.sx

@@ -0,0 +1,24 @@
+;; lib/minikanren/nafc.sx — Phase 5 piece C: negation as finite failure.
+;;
+;;   (nafc g)
+;;     succeeds (yields the input substitution) if g has zero answers
+;;     against that substitution; fails (mzero) if g has at least one.
+;;
+;; Caveat: `nafc` is unsound under the open-world assumption. It only
+;; makes sense for goals over fully-ground terms, or with the explicit
+;; understanding that adding more facts could flip the answer. Use
+;; `(project (...) ...)` to ensure the relevant vars are ground first.
+;;
+;; Caveat 2: stream-take forces g for at least one answer; if g is
+;; infinitely-ground (say, a divergent search over an unbound list),
+;; nafc itself will diverge. Standard miniKanren limitation.
+
+(define
+  nafc
+  (fn
+    (g)
+    (fn
+      (s)
+      (let
+        ((peek (stream-take 1 (g s))))
+        (if (empty? peek) (unit s) mzero)))))

lib/minikanren/peano.sx

@@ -0,0 +1,35 @@
+;; lib/minikanren/peano.sx — Peano-encoded natural-number relations.
+;;
+;; Same encoding as `lengtho`: zero is the keyword `:z`; successors are
+;; `(:s n)`. So 3 = `(:s (:s (:s :z)))`. `(:z)` and `(:s ...)` are normal
+;; SX values that unify positionally — no special primitives needed.
+;;
+;; Peano arithmetic is the canonical miniKanren way to test addition /
+;; multiplication / less-than relationally without an FD constraint store.
+;; (CLP(FD) integers come in Phase 6.)
+
+(define zeroo (fn (n) (== n :z)))
+
+(define succ-of (fn (n m) (== m (list :s n))))
+
+(define
+  pluso
+  (fn
+    (a b c)
+    (conde
+      ((== a :z) (== b c))
+      ((fresh (a-1 c-1) (== a (list :s a-1)) (== c (list :s c-1)) (pluso a-1 b c-1))))))
+
+(define minuso (fn (a b c) (pluso b c a)))
+
+(define lteo (fn (a b) (fresh (k) (pluso a k b))))
+
+(define lto (fn (a b) (fresh (sa) (succ-of a sa) (lteo sa b))))
+
+(define
+  *o
+  (fn
+    (a b c)
+    (conde
+      ((== a :z) (== c :z))
+      ((fresh (a-1 ab-1) (== a (list :s a-1)) (*o a-1 b ab-1) (pluso b ab-1 c))))))

lib/minikanren/project.sx

@@ -0,0 +1,25 @@
+;; lib/minikanren/project.sx — Phase 5 piece B: `project`.
+;;
+;;   (project (x y) g1 g2 ...)
+;;     — rebinds each named var to (mk-walk* var s) within the body's
+;;       lexical scope, then runs the conjunction of the body goals on
+;;       the same substitution. Use to escape into regular SX (arithmetic,
+;;       string ops, host predicates) when you need a ground value.
+;;
+;; If any of the projected vars is still unbound at this point, the body
+;; sees the raw `(:var NAME)` term — that is intentional and lets you
+;; mix project with `(== ground? var)` patterns or with conda guards.
+;;
+;; Hygiene: substitution parameter is gensym'd so it doesn't capture user
+;; vars (`s` is a popular relation parameter name).
+
+(defmacro
+  project
+  (vars &rest goals)
+  (let
+    ((s-sym (gensym "proj-s-")))
+    (quasiquote
+      (fn
+        ((unquote s-sym))
+        ((let (unquote (map (fn (v) (list v (list (quote mk-walk*) v s-sym))) vars)) (mk-conj (splice-unquote goals)))
+          (unquote s-sym))))))

lib/minikanren/queens.sx

@@ -0,0 +1,67 @@
+;; lib/minikanren/queens.sx — N-queens via ino + all-distincto + project.
+;;
+;; Encoding: q = (c1 c2 ... cn) where ci is the column of the queen in
+;; row i. Each ci ∈ {1..n}; all distinct (no two queens share a column);
+;; no two queens on the same diagonal (|ci - cj| ≠ |i - j| for i ≠ j).
+;;
+;; The diagonal check uses `project` to escape into host arithmetic
+;; once both column values are ground.
+
+(define
+  safe-diag
+  (fn
+    (a b dist)
+    (project (a b) (if (= (abs (- a b)) dist) fail succeed))))
+
+(define
+  safe-cell-vs-rest
+  (fn
+    (c c-row others next-row)
+    (cond
+      ((empty? others) succeed)
+      (:else
+        (mk-conj
+          (safe-diag c (first others) (- next-row c-row))
+          (safe-cell-vs-rest c c-row (rest others) (+ next-row 1)))))))
+
+(define
+  all-cells-safe
+  (fn
+    (cols start-row)
+    (cond
+      ((empty? cols) succeed)
+      (:else
+        (mk-conj
+          (safe-cell-vs-rest
+            (first cols)
+            start-row
+            (rest cols)
+            (+ start-row 1))
+          (all-cells-safe (rest cols) (+ start-row 1)))))))
+
+(define
+  range-1-to-n
+  (fn
+    (n)
+    (cond
+      ((= n 0) (list))
+      (:else (append (range-1-to-n (- n 1)) (list n))))))
+
+(define
+  ino-each
+  (fn
+    (cols dom)
+    (cond
+      ((empty? cols) succeed)
+      (:else (mk-conj (ino (first cols) dom) (ino-each (rest cols) dom))))))
+
+(define
+  queens-cols
+  (fn
+    (cols n)
+    (let
+      ((dom (range-1-to-n n)))
+      (mk-conj
+        (ino-each cols dom)
+        (all-distincto cols)
+        (all-cells-safe cols 1)))))

lib/minikanren/relations.sx

@@ -0,0 +1,158 @@
+;; lib/minikanren/relations.sx — Phase 4 standard relations.
+;;
+;; Programs use native SX lists as data. Relations decompose lists via the
+;; tagged cons-cell shape `(:cons h t)` because SX has no improper pairs;
+;; the unifier treats `(:cons h t)` and the native list `(h . t)` as
+;; equivalent, and `mk-walk*` flattens cons cells back to flat lists for
+;; reification.
+
+;; --- pair / list shape relations ---
+
+(define nullo (fn (l) (== l (list))))
+
+(define pairo (fn (p) (fresh (a d) (== p (mk-cons a d)))))
+
+(define caro (fn (p a) (fresh (d) (== p (mk-cons a d)))))
+
+(define cdro (fn (p d) (fresh (a) (== p (mk-cons a d)))))
+
+(define conso (fn (a d p) (== p (mk-cons a d))))
+
+(define firsto caro)
+(define resto cdro)
+
+(define
+  listo
+  (fn (l) (conde ((nullo l)) ((fresh (a d) (conso a d l) (listo d))))))
+
+;; --- appendo: the canary ---
+;;
+;; (appendo l s ls) — `ls` is the concatenation of `l` and `s`.
+;; Runs forwards (l, s known → ls), backwards (ls known → all (l, s) pairs),
+;; and bidirectionally (mix of bound + unbound).
+
+(define
+  appendo
+  (fn
+    (l s ls)
+    (conde
+      ((nullo l) (== s ls))
+      ((fresh (a d res) (conso a d l) (conso a res ls) (appendo d s res))))))
+
+;; --- membero ---
+;; (membero x l) — x appears (at least once) in l.
+
+(define
+  membero
+  (fn
+    (x l)
+    (conde
+      ((fresh (d) (conso x d l)))
+      ((fresh (a d) (conso a d l) (membero x d))))))
+
+(define
+  reverseo
+  (fn
+    (l r)
+    (conde
+      ((nullo l) (nullo r))
+      ((fresh (a d res-rev) (conso a d l) (reverseo d res-rev) (appendo res-rev (list a) r))))))
+
+(define
+  lengtho
+  (fn
+    (l n)
+    (conde
+      ((nullo l) (== n :z))
+      ((fresh (a d n-1) (conso a d l) (== n (list :s n-1)) (lengtho d n-1))))))
+
+(define
+  inserto
+  (fn
+    (a l p)
+    (conde
+      ((conso a l p))
+      ((fresh (h t pt) (conso h t l) (conso h pt p) (inserto a t pt))))))
+
+(define
+  permuteo
+  (fn
+    (l p)
+    (conde
+      ((nullo l) (nullo p))
+      ((fresh (a d perm-d) (conso a d l) (permuteo d perm-d) (inserto a perm-d p))))))
+
+(define
+  flatteno
+  (fn
+    (tree flat)
+    (conde
+      ((nullo tree) (nullo flat))
+      ((pairo tree)
+        (fresh
+          (h t hf tf)
+          (conso h t tree)
+          (flatteno h hf)
+          (flatteno t tf)
+          (appendo hf tf flat)))
+      ((nafc (nullo tree)) (nafc (pairo tree)) (== flat (list tree))))))
+
+
+(define
+  rembero
+  (fn
+    (x l out)
+    (conde
+      ((nullo l) (nullo out))
+      ((fresh (a d) (conso a d l) (== a x) (== out d)))
+      ((fresh (a d res) (conso a d l) (nafc (== a x)) (conso a res out) (rembero x d res))))))
+
+(define
+  assoco
+  (fn
+    (key pairs val)
+    (fresh
+      (rest)
+      (conde
+        ((conso (list key val) rest pairs))
+        ((fresh (other) (conso other rest pairs) (assoco key rest val)))))))
+
+(define
+  nth-o
+  (fn
+    (n l elem)
+    (conde
+      ((== n :z) (fresh (d) (conso elem d l)))
+      ((fresh (n-1 a d) (== n (list :s n-1)) (conso a d l) (nth-o n-1 d elem))))))
+
+(define
+  samelengtho
+  (fn
+    (l1 l2)
+    (conde
+      ((nullo l1) (nullo l2))
+      ((fresh (a d a-prime d-prime) (conso a d l1) (conso a-prime d-prime l2) (samelengtho d d-prime))))))
+
+(define
+  mapo
+  (fn
+    (rel l1 l2)
+    (conde
+      ((nullo l1) (nullo l2))
+      ((fresh (a d a-prime d-prime) (conso a d l1) (conso a-prime d-prime l2) (rel a a-prime) (mapo rel d d-prime))))))
+
+(define
+  everyo
+  (fn
+    (rel l)
+    (conde
+      ((nullo l))
+      ((fresh (a d) (conso a d l) (rel a) (everyo rel d))))))
+
+(define
+  someo
+  (fn
+    (rel l)
+    (conde
+      ((fresh (a d) (conso a d l) (rel a)))
+      ((fresh (a d) (conso a d l) (someo rel d))))))

lib/minikanren/run.sx

@@ -0,0 +1,56 @@
+;; lib/minikanren/run.sx — Phase 3: drive a goal + reify the query var.
+;;
+;; reify-name N        — make the canonical "_.N" reified symbol.
+;; reify-s term rs     — walk term in rs, add a mapping from each fresh
+;;                       unbound var to its _.N name (left-to-right order).
+;; reify q s           — walk* q in s, build reify-s, walk* again to
+;;                       substitute reified names in.
+;; run-n n q-name g... — defmacro: bind q-name to a fresh var, conj goals,
+;;                       take ≤ n answers from the stream, reify each
+;;                       through q-name. n = -1 takes all (used by run*).
+;; run*                — defmacro: (run* q g...) ≡ (run-n -1 q g...)
+;; run                 — defmacro: (run n q g...) ≡ (run-n n q g...)
+;;                       The two-segment form is the standard TRS API.
+
+(define reify-name (fn (n) (make-symbol (str "_." n))))
+
+(define
+  reify-s
+  (fn
+    (term rs)
+    (let
+      ((w (mk-walk term rs)))
+      (cond
+        ((is-var? w) (extend (var-name w) (reify-name (len rs)) rs))
+        ((mk-list-pair? w) (reduce (fn (acc a) (reify-s a acc)) rs w))
+        (:else rs)))))
+
+(define
+  reify
+  (fn
+    (term s)
+    (let
+      ((w (mk-walk* term s)))
+      (let ((rs (reify-s w (empty-subst)))) (mk-walk* w rs)))))
+
+(defmacro
+  run-n
+  (n q-name &rest goals)
+  (quasiquote
+    (let
+      (((unquote q-name) (make-var)))
+      (map
+        (fn (s) (reify (unquote q-name) s))
+        (stream-take
+          (unquote n)
+          ((mk-conj (splice-unquote goals)) empty-s))))))
+
+(defmacro
+  run*
+  (q-name &rest goals)
+  (quasiquote (run-n -1 (unquote q-name) (splice-unquote goals))))
+
+(defmacro
+  run
+  (n q-name &rest goals)
+  (quasiquote (run-n (unquote n) (unquote q-name) (splice-unquote goals))))

lib/minikanren/stream.sx

@@ -0,0 +1,66 @@
+;; lib/minikanren/stream.sx — Phase 2 piece A: lazy streams of substitutions.
+;;
+;; SX has no improper pairs (cons requires a list cdr), so we use a
+;; tagged stream-cell shape for mature stream elements:
+;;
+;;   stream  ::= mzero                        empty (the SX empty list)
+;;             | (:s HEAD TAIL)               mature cell, TAIL is a stream
+;;             | thunk                        (fn () ...) → stream when forced
+;;
+;; HEAD is a substitution dict. TAIL is again a stream (possibly a thunk),
+;; which is what gives us laziness — mk-mplus can return a mature head with
+;; a thunk in the tail, deferring the rest of the search.
+
+(define mzero (list))
+
+(define s-cons (fn (h t) (list :s h t)))
+
+(define
+  s-cons?
+  (fn (s) (and (list? s) (not (empty? s)) (= (first s) :s))))
+
+(define s-car (fn (s) (nth s 1)))
+(define s-cdr (fn (s) (nth s 2)))
+
+(define unit (fn (s) (s-cons s mzero)))
+
+(define stream-pause? (fn (s) (and (not (list? s)) (callable? s))))
+
+;; mk-mplus — interleave two streams. If s1 is paused we suspend and
+;; swap (Reasoned Schemer "interleave"); otherwise mature-cons head with
+;; mk-mplus of the rest.
+(define
+  mk-mplus
+  (fn
+    (s1 s2)
+    (cond
+      ((empty? s1) s2)
+      ((stream-pause? s1) (fn () (mk-mplus s2 (s1))))
+      (:else (s-cons (s-car s1) (mk-mplus (s-cdr s1) s2))))))
+
+;; mk-bind — apply goal g to every substitution in stream s, mk-mplus-ing.
+(define
+  mk-bind
+  (fn
+    (s g)
+    (cond
+      ((empty? s) mzero)
+      ((stream-pause? s) (fn () (mk-bind (s) g)))
+      (:else (mk-mplus (g (s-car s)) (mk-bind (s-cdr s) g))))))
+
+;; stream-take — force up to n results out of a (possibly lazy) stream
+;; into a flat SX list of substitutions. n = -1 means take all.
+(define
+  stream-take
+  (fn
+    (n s)
+    (cond
+      ((= n 0) (list))
+      ((empty? s) (list))
+      ((stream-pause? s) (stream-take n (s)))
+      (:else
+        (cons
+          (s-car s)
+          (stream-take
+            (if (= n -1) -1 (- n 1))
+            (s-cdr s)))))))

lib/minikanren/tests/classics.sx

@@ -0,0 +1,87 @@
+;; lib/minikanren/tests/classics.sx — small classic-style puzzles that
+;; exercise the full system end to end (relations + conde + matche +
+;; fresh + run*). Each test is a self-contained miniKanren program.
+
+;; -----------------------------------------------------------------------
+;; Pet puzzle (3 friends, 3 pets, 1-each).
+;; -----------------------------------------------------------------------
+
+(mk-test
+  "classics-pet-puzzle"
+  (run*
+    q
+    (fresh
+      (a b c)
+      (== q (list a b c))
+      (permuteo (list :dog :cat :fish) (list a b c))
+      (== b :fish)
+      (conde ((== a :cat)) ((== a :fish)))))
+  (list (list :cat :fish :dog)))
+
+;; -----------------------------------------------------------------------
+;; Family-relations puzzle (uses membero on a fact list).
+;; -----------------------------------------------------------------------
+
+(define
+  parent-facts
+  (list
+    (list "alice" "bob")
+    (list "alice" "carol")
+    (list "bob" "dave")
+    (list "carol" "eve")
+    (list "dave" "frank")))
+
+(define parento (fn (x y) (membero (list x y) parent-facts)))
+
+(define grandparento (fn (x z) (fresh (y) (parento x y) (parento y z))))
+
+(mk-test
+  "classics-grandparents-of-frank"
+  (run* q (grandparento q "frank"))
+  (list "bob"))
+
+(mk-test
+  "classics-grandchildren-of-alice"
+  (run* q (grandparento "alice" q))
+  (list "dave" "eve"))
+
+;; -----------------------------------------------------------------------
+;; Symbolic differentiation, matche-driven.
+;;   Variable :x:                d/dx x  = 1
+;;   Sum (:+ a b):                d/dx (a+b) = (da + db)
+;;   Product (:* a b):            d/dx (a*b) = (da*b + a*db)
+;; -----------------------------------------------------------------------
+
+(define
+  diffo
+  (fn
+    (expr var d)
+    (matche
+      expr
+      (:x (== d 1))
+      ((:+ a b)
+        (fresh
+          (da db)
+          (== d (list :+ da db))
+          (diffo a var da)
+          (diffo b var db)))
+      ((:* a b)
+        (fresh
+          (da db)
+          (== d (list :+ (list :* da b) (list :* a db)))
+          (diffo a var da)
+          (diffo b var db))))))
+
+(mk-test "classics-diff-of-x" (run* q (diffo :x :x q)) (list 1))
+
+(mk-test
+  "classics-diff-of-x-plus-x"
+  (run* q (diffo (list :+ :x :x) :x q))
+  (list (list :+ 1 1)))
+
+(mk-test
+  "classics-diff-of-x-times-x"
+  (run* q (diffo (list :* :x :x) :x q))
+  (list (list :+ (list :* 1 :x) (list :* :x 1))))
+
+(mk-tests-run!)

lib/minikanren/tests/conda.sx

@@ -0,0 +1,75 @@
+;; lib/minikanren/tests/conda.sx — Phase 5 piece A tests for `conda`.
+
+;; --- conda commits to first non-failing head, keeps ALL its answers ---
+
+(mk-test
+  "conda-first-clause-keeps-all"
+  (run*
+    q
+    (conda
+      ((mk-disj (== q 1) (== q 2)))
+      ((== q 100))))
+  (list 1 2))
+
+(mk-test
+  "conda-skips-failing-head"
+  (run*
+    q
+    (conda
+      ((== 1 2))
+      ((mk-disj (== q 10) (== q 20)))))
+  (list 10 20))
+
+(mk-test
+  "conda-all-fail"
+  (run*
+    q
+    (conda ((== 1 2)) ((== 3 4))))
+  (list))
+
+(mk-test "conda-no-clauses" (run* q (conda)) (list))
+
+;; --- conda DIFFERS from condu: conda keeps all head answers ---
+
+(mk-test
+  "conda-vs-condu-divergence"
+  (list
+    (run*
+      q
+      (conda
+        ((mk-disj (== q 1) (== q 2)))
+        ((== q 100))))
+    (run*
+      q
+      (condu
+        ((mk-disj (== q 1) (== q 2)))
+        ((== q 100)))))
+  (list (list 1 2) (list 1)))
+
+;; --- conda head's rest-goals run on every head answer ---
+
+(mk-test
+  "conda-rest-goals-run-on-all-answers"
+  (run*
+    q
+    (fresh
+      (x r)
+      (conda
+        ((mk-disj (== x 1) (== x 2))
+          (== r (list :tag x))))
+      (== q r)))
+  (list (list :tag 1) (list :tag 2)))
+
+;; --- if rest-goals fail on a head answer, that head answer is filtered;
+;;     the clause does not fall through to next clauses (per soft-cut). ---
+
+(mk-test
+  "conda-rest-fails-no-fallthrough"
+  (run*
+    q
+    (conda
+      ((mk-disj (== q 1) (== q 2)) (== q 99))
+      ((== q 200))))
+  (list))
+
+(mk-tests-run!)

lib/minikanren/tests/conde.sx

@@ -0,0 +1,89 @@
+;; lib/minikanren/tests/conde.sx — Phase 2 piece C tests for `conde`.
+;;
+;; Note on ordering: conde clauses are wrapped in Zzz (inverse-eta delay),
+;; so applying the conde goal to a substitution returns thunks. mk-mplus
+;; suspends-and-swaps when its left operand is paused, giving fair
+;; interleaving — this is exactly what makes recursive relations work,
+;; but it does mean conde answers can interleave rather than appear in
+;; strict left-to-right clause order.
+
+;; --- single-clause conde ≡ conj of clause body ---
+
+(mk-test
+  "conde-one-clause"
+  (let ((q (mk-var "q"))) (run* q (conde ((== q 7)))))
+  (list 7))
+
+(mk-test
+  "conde-one-clause-multi-goals"
+  (let
+    ((q (mk-var "q")))
+    (run* q (conde ((fresh (x) (== x 5) (== q (list x x)))))))
+  (list (list 5 5)))
+
+;; --- multi-clause: produces one row per clause (interleaved) ---
+
+(mk-test
+  "conde-three-clauses-as-set"
+  (let
+    ((qs (run* q (conde ((== q 1)) ((== q 2)) ((== q 3))))))
+    (and
+      (= (len qs) 3)
+      (and
+        (some (fn (x) (= x 1)) qs)
+        (and
+          (some (fn (x) (= x 2)) qs)
+          (some (fn (x) (= x 3)) qs)))))
+  true)
+
+(mk-test
+  "conde-mixed-success-failure-as-set"
+  (let
+    ((qs (run* q (conde ((== q "a")) ((== 1 2)) ((== q "b"))))))
+    (and
+      (= (len qs) 2)
+      (and (some (fn (x) (= x "a")) qs) (some (fn (x) (= x "b")) qs))))
+  true)
+
+;; --- conde with conjuncts inside clauses ---
+
+(mk-test
+  "conde-clause-conj-as-set"
+  (let
+    ((rows (run* q (fresh (x y) (conde ((== x 1) (== y 10)) ((== x 2) (== y 20))) (== q (list x y))))))
+    (and
+      (= (len rows) 2)
+      (and
+        (some (fn (r) (= r (list 1 10))) rows)
+        (some (fn (r) (= r (list 2 20))) rows))))
+  true)
+
+;; --- nested conde ---
+
+(mk-test
+  "conde-nested-yields-three"
+  (let
+    ((qs (run* q (conde ((conde ((== q 1)) ((== q 2)))) ((== q 3))))))
+    (and
+      (= (len qs) 3)
+      (and
+        (some (fn (x) (= x 1)) qs)
+        (and
+          (some (fn (x) (= x 2)) qs)
+          (some (fn (x) (= x 3)) qs)))))
+  true)
+
+;; --- conde all clauses fail → empty stream ---
+
+(mk-test
+  "conde-all-fail"
+  (run*
+    q
+    (conde ((== 1 2)) ((== 3 4))))
+  (list))
+
+;; --- empty conde: no clauses ⇒ fail ---
+
+(mk-test "conde-no-clauses" (run* q (conde)) (list))
+
+(mk-tests-run!)

lib/minikanren/tests/condu.sx

@@ -0,0 +1,86 @@
+;; lib/minikanren/tests/condu.sx — Phase 2 piece D tests for `onceo` and `condu`.
+
+;; --- onceo: at most one answer ---
+
+(mk-test
+  "onceo-single-success-passes-through"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((res (stream-take 5 ((onceo (== q 7)) empty-s))))
+      (map (fn (s) (mk-walk q s)) res)))
+  (list 7))
+
+(mk-test
+  "onceo-multi-success-trimmed-to-one"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((res (stream-take 5 ((onceo (mk-disj (== q 1) (== q 2) (== q 3))) empty-s))))
+      (map (fn (s) (mk-walk q s)) res)))
+  (list 1))
+
+(mk-test
+  "onceo-failure-stays-failure"
+  ((onceo (== 1 2)) empty-s)
+  (list))
+
+(mk-test
+  "onceo-conde-trimmed"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((res (stream-take 5 ((onceo (conde ((== q "a")) ((== q "b")))) empty-s))))
+      (map (fn (s) (mk-walk q s)) res)))
+  (list "a"))
+
+;; --- condu: first clause with successful head wins ---
+
+(mk-test
+  "condu-first-clause-wins"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((res (stream-take 10 ((condu ((== q 1)) ((== q 2))) empty-s))))
+      (map (fn (s) (mk-walk q s)) res)))
+  (list 1))
+
+(mk-test
+  "condu-skips-failing-head"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((res (stream-take 10 ((condu ((== 1 2)) ((== q 100)) ((== q 200))) empty-s))))
+      (map (fn (s) (mk-walk q s)) res)))
+  (list 100))
+
+(mk-test
+  "condu-all-fail-empty"
+  ((condu ((== 1 2)) ((== 3 4)))
+    empty-s)
+  (list))
+
+(mk-test "condu-empty-clauses-fail" ((condu) empty-s) (list))
+
+;; --- condu commits head's first answer; rest-goals can still backtrack
+;;     within that committed substitution but cannot revisit other heads. ---
+
+(mk-test
+  "condu-head-onceo-rest-runs"
+  (let
+    ((q (mk-var "q")) (r (mk-var "r")))
+    (let
+      ((res (stream-take 10 ((condu ((mk-disj (== q 1) (== q 2)) (== r 99))) empty-s))))
+      (map (fn (s) (list (mk-walk q s) (mk-walk r s))) res)))
+  (list (list 1 99)))
+
+(mk-test
+  "condu-rest-goals-can-fail-the-clause"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((res (stream-take 10 ((condu ((== q 1) (== 2 3)) ((== q 99))) empty-s))))
+      (map (fn (s) (mk-walk q s)) res)))
+  (list))
+
+(mk-tests-run!)

lib/minikanren/tests/cyclic-graph.sx

@@ -0,0 +1,48 @@
+;; lib/minikanren/tests/cyclic-graph.sx — demonstrates the naive-patho
+;; behaviour on a cyclic graph. Without Phase-7 tabling/SLG, the search
+;; produces ever-longer paths revisiting the cycle. `run n` truncates;
+;; `run*` would diverge.
+
+(define cyclic-edges (list (list :a :b) (list :b :a) (list :b :c)))
+
+(define cyclic-edgeo (fn (x y) (membero (list x y) cyclic-edges)))
+
+(define
+  cyclic-patho
+  (fn
+    (x y path)
+    (conde
+      ((cyclic-edgeo x y) (== path (list x y)))
+      ((fresh (z mid) (cyclic-edgeo x z) (cyclic-patho z y mid) (conso x mid path))))))
+
+;; --- direct edge ---
+
+(mk-test
+  "cyclic-direct"
+  (run 1 q (cyclic-patho :a :b q))
+  (list (list :a :b)))
+
+;; --- runs first 5 paths from a to b: bare edge, then increasing
+;;     numbers of cycle traversals (a->b->a->b, etc.) ---
+
+(mk-test
+  "cyclic-enumerates-prefix-via-run-n"
+  (let
+    ((paths (run 5 q (cyclic-patho :a :b q))))
+    (and
+      (= (len paths) 5)
+      (and
+        (every? (fn (p) (= (first p) :a)) paths)
+        (every? (fn (p) (= (last p) :b)) paths))))
+  true)
+
+(mk-test
+  "cyclic-finds-c-via-cycle-or-direct"
+  (let
+    ((paths (run 3 q (cyclic-patho :a :c q))))
+    (and
+      (>= (len paths) 1)
+      (some (fn (p) (= p (list :a :b :c))) paths)))
+  true)
+
+(mk-tests-run!)

lib/minikanren/tests/fd.sx

@@ -0,0 +1,75 @@
+;; lib/minikanren/tests/fd.sx — Phase 6 piece A: ino + all-distincto.
+
+;; --- ino ---
+
+(mk-test
+  "ino-element-in-domain"
+  (run* q (ino q (list 1 2 3)))
+  (list 1 2 3))
+
+(mk-test "ino-empty-domain" (run* q (ino q (list))) (list))
+
+(mk-test
+  "ino-singleton-domain"
+  (run* q (ino q (list 42)))
+  (list 42))
+
+;; --- all-distincto ---
+
+(mk-test
+  "all-distincto-empty"
+  (run* q (all-distincto (list)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "all-distincto-singleton"
+  (run* q (all-distincto (list 1)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "all-distincto-distinct-three"
+  (run* q (all-distincto (list 1 2 3)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "all-distincto-duplicate-fails"
+  (run* q (all-distincto (list 1 2 1)))
+  (list))
+
+(mk-test
+  "all-distincto-adjacent-duplicate-fails"
+  (run* q (all-distincto (list 1 1 2)))
+  (list))
+
+;; --- ino + all-distincto: classic enumerate-all-permutations ---
+
+(mk-test
+  "fd-puzzle-three-distinct-from-domain"
+  (let
+    ((perms (run* q (fresh (a b c) (== q (list a b c)) (ino a (list 1 2 3)) (ino b (list 1 2 3)) (ino c (list 1 2 3)) (all-distincto (list a b c))))))
+    (and
+      (= (len perms) 6)
+      (and
+        (some (fn (p) (= p (list 1 2 3))) perms)
+        (and
+          (some
+            (fn (p) (= p (list 1 3 2)))
+            perms)
+          (and
+            (some
+              (fn (p) (= p (list 2 1 3)))
+              perms)
+            (and
+              (some
+                (fn (p) (= p (list 2 3 1)))
+                perms)
+              (and
+                (some
+                  (fn (p) (= p (list 3 1 2)))
+                  perms)
+                (some
+                  (fn (p) (= p (list 3 2 1)))
+                  perms))))))))
+  true)
+
+(mk-tests-run!)

lib/minikanren/tests/flatteno.sx

@@ -0,0 +1,42 @@
+(mk-test "flatteno-empty" (run* q (flatteno (list) q)) (list (list)))
+
+(mk-test
+  "flatteno-atom"
+  (run* q (flatteno 5 q))
+  (list (list 5)))
+
+(mk-test
+  "flatteno-flat-list"
+  (run* q (flatteno (list 1 2 3) q))
+  (list (list 1 2 3)))
+
+(mk-test
+  "flatteno-singleton"
+  (run* q (flatteno (list 1) q))
+  (list (list 1)))
+
+(mk-test
+  "flatteno-nested-once"
+  (run*
+    q
+    (flatteno (list 1 (list 2 3) 4) q))
+  (list (list 1 2 3 4)))
+
+(mk-test
+  "flatteno-nested-twice"
+  (run*
+    q
+    (flatteno
+      (list
+        1
+        (list 2 (list 3 4))
+        5)
+      q))
+  (list (list 1 2 3 4 5)))
+
+(mk-test
+  "flatteno-keywords"
+  (run* q (flatteno (list :a (list :b :c) :d) q))
+  (list (list :a :b :c :d)))
+
+(mk-tests-run!)

lib/minikanren/tests/fresh.sx

@@ -0,0 +1,101 @@
+;; lib/minikanren/tests/fresh.sx — Phase 2 piece B tests for `fresh`.
+
+;; --- empty fresh: pure goal grouping ---
+
+(mk-test
+  "fresh-empty-vars-equiv-conj"
+  (stream-take 5 ((fresh () (== 1 1)) empty-s))
+  (list empty-s))
+
+(mk-test
+  "fresh-empty-vars-no-goals-is-succeed"
+  (stream-take 5 ((fresh ()) empty-s))
+  (list empty-s))
+
+;; --- single var ---
+
+(mk-test
+  "fresh-one-var-bound"
+  (let
+    ((s (first (stream-take 5 ((fresh (x) (== x 7)) empty-s)))))
+    (first (vals s)))
+  7)
+
+;; --- multiple vars + multiple goals ---
+
+(mk-test
+  "fresh-two-vars-three-goals"
+  (let
+    ((q (mk-var "q"))
+      (g
+        (fresh
+          (x y)
+          (== x 10)
+          (== y 20)
+          (== q (list x y)))))
+    (mk-walk* q (first (stream-take 5 (g empty-s)))))
+  (list 10 20))
+
+(mk-test
+  "fresh-three-vars"
+  (let
+    ((q (mk-var "q"))
+      (g
+        (fresh
+          (a b c)
+          (== a 1)
+          (== b 2)
+          (== c 3)
+          (== q (list a b c)))))
+    (mk-walk* q (first (stream-take 5 (g empty-s)))))
+  (list 1 2 3))
+
+;; --- fresh interacts with disj ---
+
+(mk-test
+  "fresh-with-disj"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((g (fresh (x) (mk-disj (== x 1) (== x 2)) (== q x))))
+      (let
+        ((res (stream-take 5 (g empty-s))))
+        (map (fn (s) (mk-walk q s)) res))))
+  (list 1 2))
+
+;; --- nested fresh ---
+
+(mk-test
+  "fresh-nested"
+  (let
+    ((q (mk-var "q"))
+      (g
+        (fresh
+          (x)
+          (fresh
+            (y)
+            (== x 1)
+            (== y 2)
+            (== q (list x y))))))
+    (mk-walk* q (first (stream-take 5 (g empty-s)))))
+  (list 1 2))
+
+;; --- call-fresh (functional alternative) ---
+
+(mk-test
+  "call-fresh-binds-and-walks"
+  (let
+    ((s (first (stream-take 5 ((call-fresh (fn (x) (== x 99))) empty-s)))))
+    (first (vals s)))
+  99)
+
+(mk-test
+  "call-fresh-distinct-from-outer-vars"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((g (call-fresh (fn (x) (mk-conj (== x 5) (== q (list x x)))))))
+      (mk-walk* q (first (stream-take 5 (g empty-s))))))
+  (list 5 5))
+
+(mk-tests-run!)

lib/minikanren/tests/goals.sx

@@ -0,0 +1,260 @@
+;; lib/minikanren/tests/goals.sx — Phase 2 tests for stream.sx + goals.sx.
+;;
+;; Streams use a tagged shape internally (`(:s head tail)`) so that mature
+;; cells can have thunk tails — SX has no improper pairs. Test assertions
+;; therefore stream-take into a plain SX list, or check goal effects via
+;; mk-walk on the resulting subst, instead of inspecting raw streams.
+
+;; --- stream-take base cases (input streams use s-cons / mzero) ---
+
+(mk-test
+  "stream-take-zero-from-mature"
+  (stream-take 0 (s-cons (empty-subst) mzero))
+  (list))
+
+(mk-test "stream-take-from-mzero" (stream-take 5 mzero) (list))
+
+(mk-test
+  "stream-take-mature-pair"
+  (stream-take 5 (s-cons :a (s-cons :b mzero)))
+  (list :a :b))
+
+(mk-test
+  "stream-take-fewer-than-available"
+  (stream-take 1 (s-cons :a (s-cons :b mzero)))
+  (list :a))
+
+(mk-test
+  "stream-take-all-with-neg-1"
+  (stream-take -1 (s-cons :a (s-cons :b (s-cons :c mzero))))
+  (list :a :b :c))
+
+;; --- stream-take forces immature thunks ---
+
+(mk-test
+  "stream-take-forces-thunk"
+  (stream-take 5 (fn () (s-cons :x mzero)))
+  (list :x))
+
+(mk-test
+  "stream-take-forces-nested-thunks"
+  (stream-take 5 (fn () (fn () (s-cons :y mzero))))
+  (list :y))
+
+;; --- mk-mplus interleaves ---
+
+(mk-test
+  "mplus-empty-left"
+  (stream-take 5 (mk-mplus mzero (s-cons :r mzero)))
+  (list :r))
+
+(mk-test
+  "mplus-empty-right"
+  (stream-take 5 (mk-mplus (s-cons :l mzero) mzero))
+  (list :l))
+
+(mk-test
+  "mplus-mature-mature"
+  (stream-take
+    5
+    (mk-mplus (s-cons :a (s-cons :b mzero)) (s-cons :c (s-cons :d mzero))))
+  (list :a :b :c :d))
+
+(mk-test
+  "mplus-with-paused-left-swaps"
+  (stream-take
+    5
+    (mk-mplus
+      (fn () (s-cons :a (s-cons :b mzero)))
+      (s-cons :c (s-cons :d mzero))))
+  (list :c :d :a :b))
+
+;; --- mk-bind ---
+
+(mk-test
+  "bind-empty-stream"
+  (stream-take 5 (mk-bind mzero (fn (s) (unit s))))
+  (list))
+
+(mk-test
+  "bind-singleton-identity"
+  (stream-take
+    5
+    (mk-bind (s-cons 5 mzero) (fn (x) (unit x))))
+  (list 5))
+
+(mk-test
+  "bind-flat-multi"
+  (stream-take
+    10
+    (mk-bind
+      (s-cons 1 (s-cons 2 mzero))
+      (fn (x) (s-cons x (s-cons (* x 10) mzero)))))
+  (list 1 10 2 20))
+
+(mk-test
+  "bind-fail-prunes-some"
+  (stream-take
+    10
+    (mk-bind
+      (s-cons 1 (s-cons 2 (s-cons 3 mzero)))
+      (fn (x) (if (= x 2) mzero (unit x)))))
+  (list 1 3))
+
+;; --- core goals: succeed / fail ---
+
+(mk-test
+  "succeed-yields-singleton"
+  (stream-take 5 (succeed empty-s))
+  (list empty-s))
+
+(mk-test "fail-yields-mzero" (stream-take 5 (fail empty-s)) (list))
+
+;; --- == ---
+
+(mk-test
+  "eq-ground-success"
+  (stream-take 5 ((== 1 1) empty-s))
+  (list empty-s))
+
+(mk-test
+  "eq-ground-failure"
+  (stream-take 5 ((== 1 2) empty-s))
+  (list))
+
+(mk-test
+  "eq-binds-var"
+  (let
+    ((x (mk-var "x")))
+    (mk-walk
+      x
+      (first (stream-take 5 ((== x 7) empty-s)))))
+  7)
+
+(mk-test
+  "eq-list-success"
+  (let
+    ((x (mk-var "x")))
+    (mk-walk
+      x
+      (first
+        (stream-take
+          5
+          ((== x (list 1 2)) empty-s)))))
+  (list 1 2))
+
+(mk-test
+  "eq-list-mismatch-fails"
+  (stream-take
+    5
+    ((== (list 1 2) (list 1 3)) empty-s))
+  (list))
+
+;; --- conj2 / mk-conj ---
+
+(mk-test
+  "conj2-both-bind"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")))
+    (let
+      ((s (first (stream-take 5 ((conj2 (== x 1) (== y 2)) empty-s)))))
+      (list (mk-walk x s) (mk-walk y s))))
+  (list 1 2))
+
+(mk-test
+  "conj2-conflict-empty"
+  (let
+    ((x (mk-var "x")))
+    (stream-take
+      5
+      ((conj2 (== x 1) (== x 2)) empty-s)))
+  (list))
+
+(mk-test
+  "conj-empty-is-succeed"
+  (stream-take 5 ((mk-conj) empty-s))
+  (list empty-s))
+
+(mk-test
+  "conj-single-is-goal"
+  (let
+    ((x (mk-var "x")))
+    (mk-walk
+      x
+      (first
+        (stream-take 5 ((mk-conj (== x 99)) empty-s)))))
+  99)
+
+(mk-test
+  "conj-three-bindings"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")) (z (mk-var "z")))
+    (let
+      ((s (first (stream-take 5 ((mk-conj (== x 1) (== y 2) (== z 3)) empty-s)))))
+      (list (mk-walk x s) (mk-walk y s) (mk-walk z s))))
+  (list 1 2 3))
+
+;; --- disj2 / mk-disj ---
+
+(mk-test
+  "disj2-both-succeed"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((res (stream-take 5 ((disj2 (== q 1) (== q 2)) empty-s))))
+      (map (fn (s) (mk-walk q s)) res)))
+  (list 1 2))
+
+(mk-test
+  "disj2-fail-or-succeed"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((res (stream-take 5 ((disj2 fail (== q 5)) empty-s))))
+      (map (fn (s) (mk-walk q s)) res)))
+  (list 5))
+
+(mk-test
+  "disj-empty-is-fail"
+  (stream-take 5 ((mk-disj) empty-s))
+  (list))
+
+(mk-test
+  "disj-three-clauses"
+  (let
+    ((q (mk-var "q")))
+    (let
+      ((res (stream-take 5 ((mk-disj (== q "a") (== q "b") (== q "c")) empty-s))))
+      (map (fn (s) (mk-walk q s)) res)))
+  (list "a" "b" "c"))
+
+;; --- conj/disj nesting ---
+
+(mk-test
+  "disj-of-conj"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")))
+    (let
+      ((res (stream-take 5 ((mk-disj (mk-conj (== x 1) (== y 2)) (mk-conj (== x 3) (== y 4))) empty-s))))
+      (map (fn (s) (list (mk-walk x s) (mk-walk y s))) res)))
+  (list (list 1 2) (list 3 4)))
+
+;; --- ==-check ---
+
+(mk-test
+  "eq-check-no-occurs-fails"
+  (let
+    ((x (mk-var "x")))
+    (stream-take 5 ((==-check x (list 1 x)) empty-s)))
+  (list))
+
+(mk-test
+  "eq-check-no-occurs-non-occurring-succeeds"
+  (let
+    ((x (mk-var "x")))
+    (mk-walk
+      x
+      (first (stream-take 5 ((==-check x 5) empty-s)))))
+  5)
+
+(mk-tests-run!)

lib/minikanren/tests/graph.sx

@@ -0,0 +1,70 @@
+;; lib/minikanren/tests/graph.sx — directed-graph reachability via patho.
+
+(define
+  test-edges
+  (list (list :a :b) (list :b :c) (list :c :d) (list :a :c) (list :d :e)))
+
+(define edgeo (fn (from to) (membero (list from to) test-edges)))
+
+(define
+  patho
+  (fn
+    (x y path)
+    (conde
+      ((edgeo x y) (== path (list x y)))
+      ((fresh (z mid-path) (edgeo x z) (patho z y mid-path) (conso x mid-path path))))))
+
+;; --- direct edges ---
+
+(mk-test "patho-direct" (run* q (patho :a :b q)) (list (list :a :b)))
+
+(mk-test "patho-no-direct-edge" (run* q (patho :e :a q)) (list))
+
+;; --- indirect ---
+
+(mk-test
+  "patho-multi-hop"
+  (let
+    ((paths (run* q (patho :a :d q))))
+    (and
+      (= (len paths) 2)
+      (and
+        (some (fn (p) (= p (list :a :b :c :d))) paths)
+        (some (fn (p) (= p (list :a :c :d))) paths))))
+  true)
+
+(mk-test
+  "patho-to-leaf"
+  (let
+    ((paths (run* q (patho :a :e q))))
+    (and
+      (= (len paths) 2)
+      (and
+        (some (fn (p) (= p (list :a :b :c :d :e))) paths)
+        (some (fn (p) (= p (list :a :c :d :e))) paths))))
+  true)
+
+;; --- enumeration with multiplicity ---
+;; Each path contributes one tuple, so reachable nodes can repeat. Here
+;; targets are: b (1 path), c (2 paths), d (2 paths), e (2 paths) = 7.
+
+(mk-test
+  "patho-enumerate-from-a-with-multiplicity"
+  (let
+    ((targets (run* q (fresh (path) (patho :a q path)))))
+    (and
+      (= (len targets) 7)
+      (and
+        (some (fn (t) (= t :b)) targets)
+        (and
+          (some (fn (t) (= t :c)) targets)
+          (and
+            (some (fn (t) (= t :d)) targets)
+            (some (fn (t) (= t :e)) targets))))))
+  true)
+
+;; --- unreachable target ---
+
+(mk-test "patho-unreachable" (run* q (patho :a :z q)) (list))
+
+(mk-tests-run!)

lib/minikanren/tests/intarith.sx

@@ -0,0 +1,89 @@
+;; lib/minikanren/tests/intarith.sx — ground-only integer arithmetic
+;; goals that escape into host operations via project.
+
+;; --- pluso-i ---
+
+(mk-test
+  "pluso-i-forward"
+  (run* q (pluso-i 7 8 q))
+  (list 15))
+(mk-test
+  "pluso-i-zero"
+  (run* q (pluso-i 0 0 q))
+  (list 0))
+(mk-test
+  "pluso-i-negatives"
+  (run* q (pluso-i -5 3 q))
+  (list -2))
+(mk-test
+  "pluso-i-non-ground-fails"
+  (run* q (fresh (a) (pluso-i a 3 5)))
+  (list))
+
+;; --- minuso-i ---
+
+(mk-test
+  "minuso-i-forward"
+  (run* q (minuso-i 10 4 q))
+  (list 6))
+(mk-test
+  "minuso-i-zero"
+  (run* q (minuso-i 5 5 q))
+  (list 0))
+
+;; --- *o-i ---
+
+(mk-test
+  "times-i-forward"
+  (run* q (*o-i 6 7 q))
+  (list 42))
+(mk-test
+  "times-i-by-zero"
+  (run* q (*o-i 0 99 q))
+  (list 0))
+(mk-test
+  "times-i-by-one"
+  (run* q (*o-i 1 17 q))
+  (list 17))
+
+;; --- comparisons ---
+
+(mk-test
+  "lto-i-true"
+  (run 1 q (lto-i 2 5))
+  (list (make-symbol "_.0")))
+(mk-test "lto-i-false" (run* q (lto-i 5 2)) (list))
+(mk-test "lto-i-equal-false" (run* q (lto-i 3 3)) (list))
+
+(mk-test
+  "lteo-i-equal"
+  (run 1 q (lteo-i 4 4))
+  (list (make-symbol "_.0")))
+(mk-test
+  "lteo-i-less"
+  (run 1 q (lteo-i 1 4))
+  (list (make-symbol "_.0")))
+(mk-test "lteo-i-more" (run* q (lteo-i 9 4)) (list))
+
+(mk-test
+  "neqo-i-different"
+  (run 1 q (neqo-i 3 5))
+  (list (make-symbol "_.0")))
+(mk-test "neqo-i-same" (run* q (neqo-i 3 3)) (list))
+
+;; --- composition with relational vars ---
+
+(mk-test
+  "intarith-with-membero"
+  (run*
+    q
+    (fresh
+      (x)
+      (membero
+        x
+        (list 1 2 3 4 5))
+      (lto-i x 3)
+      (== q x)))
+  (list 1 2))
+
+(mk-tests-run!)

lib/minikanren/tests/latin.sx

@@ -0,0 +1,61 @@
+;; lib/minikanren/tests/latin.sx — 2x2 Latin square via ino + all-distincto.
+;;
+;; A 2x2 Latin square has 2 distinct fillings:
+;;   ((1 2) (2 1))  and  ((2 1) (1 2)).
+;; The 3x3 version has 12 fillings but takes minutes under naive search;
+;; full CLP(FD) (Phase 6 proper) would handle it in milliseconds.
+
+(define
+  latin-2x2
+  (fn
+    (cells)
+    (let
+      ((c11 (nth cells 0))
+        (c12 (nth cells 1))
+        (c21 (nth cells 2))
+        (c22 (nth cells 3))
+        (dom (list 1 2)))
+      (mk-conj
+        (ino c11 dom)
+        (ino c12 dom)
+        (ino c21 dom)
+        (ino c22 dom)
+        (all-distincto (list c11 c12))
+        (all-distincto (list c21 c22))
+        (all-distincto (list c11 c21))
+        (all-distincto (list c12 c22))))))   ;; col 2
+
+(mk-test
+  "latin-2x2-count"
+  (let
+    ((squares (run* q (fresh (a b c d) (== q (list a b c d)) (latin-2x2 (list a b c d))))))
+    (len squares))
+  2)
+
+(mk-test
+  "latin-2x2-as-set"
+  (let
+    ((squares (run* q (fresh (a b c d) (== q (list a b c d)) (latin-2x2 (list a b c d))))))
+    (and
+      (= (len squares) 2)
+      (and
+        (some
+          (fn (s) (= s (list 1 2 2 1)))
+          squares)
+        (some
+          (fn (s) (= s (list 2 1 1 2)))
+          squares))))
+  true)
+
+(mk-test
+  "latin-2x2-with-clue"
+  (run*
+    q
+    (fresh
+      (a b c d)
+      (== a 1)
+      (== q (list a b c d))
+      (latin-2x2 (list a b c d))))
+  (list (list 1 2 2 1)))
+
+(mk-tests-run!)

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!)

lib/minikanren/tests/list-relations.sx

@@ -0,0 +1,126 @@
+;; lib/minikanren/tests/list-relations.sx — rembero, assoco, nth-o, samelengtho.
+
+;; --- rembero (remove first occurrence) ---
+
+(mk-test
+  "rembero-element-present"
+  (run*
+    q
+    (rembero 2 (list 1 2 3 2) q))
+  (list (list 1 3 2)))
+
+(mk-test
+  "rembero-element-not-present"
+  (run* q (rembero 99 (list 1 2 3) q))
+  (list (list 1 2 3)))
+
+(mk-test
+  "rembero-empty"
+  (run* q (rembero 1 (list) q))
+  (list (list)))
+
+(mk-test
+  "rembero-only-element"
+  (run* q (rembero 5 (list 5) q))
+  (list (list)))
+
+(mk-test
+  "rembero-first-of-many"
+  (run*
+    q
+    (rembero 1 (list 1 2 3 4) q))
+  (list (list 2 3 4)))
+
+;; --- assoco (alist lookup) ---
+
+(define
+  test-pairs
+  (list
+    (list "alice" 30)
+    (list "bob" 25)
+    (list "carol" 35)))
+
+(mk-test
+  "assoco-found"
+  (run* q (assoco "bob" test-pairs q))
+  (list 25))
+
+(mk-test
+  "assoco-first"
+  (run* q (assoco "alice" test-pairs q))
+  (list 30))
+
+(mk-test "assoco-missing" (run* q (assoco "dave" test-pairs q)) (list))
+
+(mk-test
+  "assoco-find-keys-with-value"
+  (run* q (assoco q test-pairs 25))
+  (list "bob"))
+
+;; --- nth-o (Peano-indexed access) ---
+
+(mk-test
+  "nth-o-zero"
+  (run* q (nth-o :z (list 10 20 30) q))
+  (list 10))
+
+(mk-test
+  "nth-o-one"
+  (run* q (nth-o (list :s :z) (list 10 20 30) q))
+  (list 20))
+
+(mk-test
+  "nth-o-two"
+  (run*
+    q
+    (nth-o (list :s (list :s :z)) (list 10 20 30) q))
+  (list 30))
+
+(mk-test
+  "nth-o-out-of-range"
+  (run*
+    q
+    (nth-o
+      (list :s (list :s (list :s :z)))
+      (list 10 20 30)
+      q))
+  (list))
+
+;; --- samelengtho ---
+
+(mk-test
+  "samelengtho-equal"
+  (run*
+    q
+    (samelengtho (list 1 2 3) (list :a :b :c)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "samelengtho-different-fails"
+  (run* q (samelengtho (list 1 2) (list :a :b :c)))
+  (list))
+
+(mk-test
+  "samelengtho-empty-equal"
+  (run* q (samelengtho (list) (list)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "samelengtho-builds-vars"
+  (run 1 q (samelengtho (list 1 2 3) q))
+  (list (list (make-symbol "_.0") (make-symbol "_.1") (make-symbol "_.2"))))
+
+(mk-test
+  "samelengtho-enumerates-pairs"
+  (run
+    3
+    q
+    (fresh (l1 l2) (samelengtho l1 l2) (== q (list l1 l2))))
+  (list
+    (list (list) (list))
+    (list (list (make-symbol "_.0")) (list (make-symbol "_.1")))
+    (list
+      (list (make-symbol "_.0") (make-symbol "_.1"))
+      (list (make-symbol "_.2") (make-symbol "_.3")))))
+
+(mk-tests-run!)

lib/minikanren/tests/mapo.sx

@@ -0,0 +1,62 @@
+;; lib/minikanren/tests/mapo.sx — relational map.
+
+(mk-test
+  "mapo-identity"
+  (run*
+    q
+    (mapo (fn (a b) (== a b)) (list 1 2 3) q))
+  (list (list 1 2 3)))
+
+(mk-test
+  "mapo-tag-each"
+  (run*
+    q
+    (mapo
+      (fn (a b) (== b (list :tag a)))
+      (list 1 2 3)
+      q))
+  (list
+    (list
+      (list :tag 1)
+      (list :tag 2)
+      (list :tag 3))))
+
+(mk-test
+  "mapo-backward"
+  (run*
+    q
+    (mapo (fn (a b) (== a b)) q (list 1 2 3)))
+  (list (list 1 2 3)))
+
+(mk-test
+  "mapo-empty"
+  (run* q (mapo (fn (a b) (== a b)) (list) q))
+  (list (list)))
+
+(mk-test
+  "mapo-duplicate"
+  (run* q (mapo (fn (a b) (== b (list a a))) (list :x :y) q))
+  (list (list (list :x :x) (list :y :y))))
+
+(mk-test
+  "mapo-different-length-fails"
+  (run*
+    q
+    (mapo
+      (fn (a b) (== a b))
+      (list 1 2)
+      (list 1 2 3)))
+  (list))
+
+;; mapo + arithmetic via intarith
+(mk-test
+  "mapo-square-each"
+  (run*
+    q
+    (mapo
+      (fn (a b) (*o-i a a b))
+      (list 1 2 3 4)
+      q))
+  (list (list 1 4 9 16)))
+
+(mk-tests-run!)

lib/minikanren/tests/matche.sx

@@ -0,0 +1,138 @@
+;; lib/minikanren/tests/matche.sx — Phase 5 piece D tests for `matche`.
+
+;; --- literal patterns ---
+
+(mk-test
+  "matche-literal-number"
+  (run* q (matche q (1 (== q 1))))
+  (list 1))
+
+(mk-test
+  "matche-literal-string"
+  (run* q (matche q ("hello" (== q "hello"))))
+  (list "hello"))
+
+(mk-test
+  "matche-literal-no-clause-matches"
+  (run*
+    q
+    (matche 7 (1 (== q :a)) (2 (== q :b))))
+  (list))
+
+;; --- variable patterns ---
+
+(mk-test
+  "matche-symbol-pattern"
+  (run* q (fresh (x) (== x 99) (matche x (a (== q a)))))
+  (list 99))
+
+(mk-test
+  "matche-wildcard"
+  (run* q (fresh (x) (== x 7) (matche x (_ (== q :any)))))
+  (list :any))
+
+;; --- list patterns ---
+
+(mk-test
+  "matche-empty-list"
+  (run* q (matche (list) (() (== q :ok))))
+  (list :ok))
+
+(mk-test
+  "matche-pair-binds"
+  (run*
+    q
+    (fresh
+      (x)
+      (== x (list 1 2))
+      (matche x ((a b) (== q (list b a))))))
+  (list (list 2 1)))
+
+(mk-test
+  "matche-triple-binds"
+  (run*
+    q
+    (fresh
+      (x)
+      (== x (list 1 2 3))
+      (matche x ((a b c) (== q (list :sum a b c))))))
+  (list (list :sum 1 2 3)))
+
+(mk-test
+  "matche-mixed-literal-and-var"
+  (run*
+    q
+    (fresh
+      (x)
+      (== x (list 1 99 3))
+      (matche x ((1 m 3) (== q m)))))
+  (list 99))
+
+;; --- multi-clause dispatch ---
+
+(mk-test
+  "matche-multi-clause-shape"
+  (run*
+    q
+    (fresh
+      (x)
+      (== x (list 5 6))
+      (matche
+        x
+        (() (== q :empty))
+        ((a) (== q (list :one a)))
+        ((a b) (== q (list :two a b))))))
+  (list (list :two 5 6)))
+
+(mk-test
+  "matche-three-shapes-via-fresh"
+  (run*
+    q
+    (fresh
+      (x)
+      (matche
+        x
+        (() (== q :empty))
+        ((a) (== q (list :one a)))
+        ((a b) (== q (list :two a b))))))
+  (list
+    :empty (list :one (make-symbol "_.0"))
+    (list :two (make-symbol "_.0") (make-symbol "_.1"))))
+
+;; --- nested patterns ---
+
+(mk-test
+  "matche-nested"
+  (run*
+    q
+    (fresh
+      (x)
+      (==
+        x
+        (list (list 1 2) (list 3 4)))
+      (matche x (((a b) (c d)) (== q (list a b c d))))))
+  (list (list 1 2 3 4)))
+
+;; --- repeated var names create the same fresh var → must unify ---
+
+(mk-test
+  "matche-repeated-var-implies-equality"
+  (run*
+    q
+    (fresh
+      (x)
+      (== x (list 7 7))
+      (matche x ((a a) (== q a)))))
+  (list 7))
+
+(mk-test
+  "matche-repeated-var-mismatch-fails"
+  (run*
+    q
+    (fresh
+      (x)
+      (== x (list 7 8))
+      (matche x ((a a) (== q a)))))
+  (list))
+
+(mk-tests-run!)

lib/minikanren/tests/nafc.sx

@@ -0,0 +1,50 @@
+;; lib/minikanren/tests/nafc.sx — Phase 5 piece C tests for `nafc`.
+
+(mk-test
+  "nafc-failed-goal-succeeds"
+  (run* q (nafc (== 1 2)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "nafc-successful-goal-fails"
+  (run* q (nafc (== 1 1)))
+  (list))
+
+(mk-test
+  "nafc-double-negation"
+  (run* q (nafc (nafc (== 1 1))))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "nafc-with-conde-no-clauses-succeed"
+  (run*
+    q
+    (nafc
+      (conde ((== 1 2)) ((== 3 4)))))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "nafc-with-conde-some-clause-succeeds-fails"
+  (run*
+    q
+    (nafc
+      (conde ((== 1 1)) ((== 3 4)))))
+  (list))
+
+;; --- composing nafc with == as a guard ---
+
+(mk-test
+  "nafc-as-guard"
+  (run*
+    q
+    (fresh (x) (== x 5) (nafc (== x 99)) (== q x)))
+  (list 5))
+
+(mk-test
+  "nafc-guard-blocking"
+  (run*
+    q
+    (fresh (x) (== x 5) (nafc (== x 5)) (== q x)))
+  (list))
+
+(mk-tests-run!)

lib/minikanren/tests/peano.sx

@@ -0,0 +1,119 @@
+;; lib/minikanren/tests/peano.sx — Peano arithmetic.
+;;
+;; Builds Peano numbers via a host-side helper so tests stay readable.
+;; (mk-nat 3) → (:s (:s (:s :z))).
+
+(define
+  mk-nat
+  (fn (n) (if (= n 0) :z (list :s (mk-nat (- n 1))))))
+
+;; --- zeroo ---
+
+(mk-test
+  "zeroo-zero-succeeds"
+  (run* q (zeroo :z))
+  (list (make-symbol "_.0")))
+(mk-test
+  "zeroo-non-zero-fails"
+  (run* q (zeroo (mk-nat 1)))
+  (list))
+
+;; --- pluso forward ---
+
+(mk-test
+  "pluso-forward-2-3"
+  (run* q (pluso (mk-nat 2) (mk-nat 3) q))
+  (list (mk-nat 5)))
+
+(mk-test "pluso-forward-zero-zero" (run* q (pluso :z :z q)) (list :z))
+
+(mk-test
+  "pluso-forward-zero-n"
+  (run* q (pluso :z (mk-nat 4) q))
+  (list (mk-nat 4)))
+
+(mk-test
+  "pluso-forward-n-zero"
+  (run* q (pluso (mk-nat 4) :z q))
+  (list (mk-nat 4)))
+
+;; --- pluso backward ---
+
+(mk-test
+  "pluso-recover-augend"
+  (run* q (pluso q (mk-nat 2) (mk-nat 5)))
+  (list (mk-nat 3)))
+
+(mk-test
+  "pluso-recover-addend"
+  (run* q (pluso (mk-nat 2) q (mk-nat 5)))
+  (list (mk-nat 3)))
+
+(mk-test
+  "pluso-enumerate-pairs-summing-to-3"
+  (run*
+    q
+    (fresh (a b) (pluso a b (mk-nat 3)) (== q (list a b))))
+  (list
+    (list :z (mk-nat 3))
+    (list (mk-nat 1) (mk-nat 2))
+    (list (mk-nat 2) (mk-nat 1))
+    (list (mk-nat 3) :z)))
+
+;; --- minuso ---
+
+(mk-test
+  "minuso-5-2-3"
+  (run* q (minuso (mk-nat 5) (mk-nat 2) q))
+  (list (mk-nat 3)))
+
+(mk-test
+  "minuso-n-n-zero"
+  (run* q (minuso (mk-nat 7) (mk-nat 7) q))
+  (list :z))
+
+;; --- *o ---
+
+(mk-test
+  "times-2-3"
+  (run* q (*o (mk-nat 2) (mk-nat 3) q))
+  (list (mk-nat 6)))
+
+(mk-test
+  "times-zero-anything-zero"
+  (run* q (*o :z (mk-nat 99) q))
+  (list :z))
+
+(mk-test
+  "times-3-4"
+  (run* q (*o (mk-nat 3) (mk-nat 4) q))
+  (list (mk-nat 12)))
+
+;; --- lteo / lto ---
+
+(mk-test
+  "lteo-success"
+  (run 1 q (lteo (mk-nat 2) (mk-nat 5)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "lteo-equal-success"
+  (run 1 q (lteo (mk-nat 3) (mk-nat 3)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "lteo-greater-fails"
+  (run* q (lteo (mk-nat 5) (mk-nat 2)))
+  (list))
+
+(mk-test
+  "lto-strict-success"
+  (run 1 q (lto (mk-nat 2) (mk-nat 5)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "lto-equal-fails"
+  (run* q (lto (mk-nat 3) (mk-nat 3)))
+  (list))
+
+(mk-tests-run!)

lib/minikanren/tests/predicates.sx

@@ -0,0 +1,87 @@
+;; lib/minikanren/tests/predicates.sx — everyo, someo.
+
+;; --- everyo ---
+
+(mk-test
+  "everyo-empty-trivially-true"
+  (run* q (everyo (fn (x) (== x 1)) (list)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "everyo-all-match"
+  (run*
+    q
+    (everyo
+      (fn (x) (== x 1))
+      (list 1 1 1)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "everyo-some-mismatch"
+  (run*
+    q
+    (everyo
+      (fn (x) (== x 1))
+      (list 1 2 1)))
+  (list))
+
+(mk-test
+  "everyo-with-intarith"
+  (run*
+    q
+    (everyo
+      (fn (x) (lto-i x 10))
+      (list 1 5 9)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "everyo-with-intarith-fail"
+  (run*
+    q
+    (everyo
+      (fn (x) (lto-i x 5))
+      (list 1 5 9)))
+  (list))
+
+;; --- someo ---
+
+(mk-test
+  "someo-finds-element"
+  (run*
+    q
+    (someo
+      (fn (x) (== x 2))
+      (list 1 2 3)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "someo-not-found"
+  (run*
+    q
+    (someo
+      (fn (x) (== x 99))
+      (list 1 2 3)))
+  (list))
+
+(mk-test
+  "someo-empty-fails"
+  (run* q (someo (fn (x) (== x 1)) (list)))
+  (list))
+
+(mk-test
+  "someo-multiple-matches-yields-multiple"
+  (let
+    ((res (run* q (fresh (x) (someo (fn (y) (== y x)) (list 1 2 1)) (== q x)))))
+    (len res))
+  3)
+
+(mk-test
+  "someo-with-intarith"
+  (run*
+    q
+    (someo
+      (fn (x) (lto-i 100 x))
+      (list 5 50 200)))
+  (list (make-symbol "_.0")))
+
+(mk-tests-run!)

lib/minikanren/tests/project.sx

@@ -0,0 +1,60 @@
+;; lib/minikanren/tests/project.sx — Phase 5 piece B tests for `project`.
+
+;; --- project rebinds vars to ground values for SX use ---
+
+(mk-test
+  "project-square-via-host"
+  (run* q (fresh (n) (== n 5) (project (n) (== q (* n n)))))
+  (list 25))
+
+(mk-test
+  "project-multi-vars"
+  (run*
+    q
+    (fresh
+      (a b)
+      (== a 3)
+      (== b 4)
+      (project (a b) (== q (+ a b)))))
+  (list 7))
+
+(mk-test
+  "project-with-string-host-op"
+  (run* q (fresh (s) (== s "hello") (project (s) (== q (str s "!")))))
+  (list "hello!"))
+
+;; --- project nested inside conde ---
+
+(mk-test
+  "project-inside-conde"
+  (run*
+    q
+    (fresh
+      (n)
+      (conde ((== n 3)) ((== n 4)))
+      (project (n) (== q (* n 10)))))
+  (list 30 40))
+
+;; --- project body can be multiple goals (mk-conj'd) ---
+
+(mk-test
+  "project-multi-goal-body"
+  (run*
+    q
+    (fresh
+      (n)
+      (== n 7)
+      (project (n) (== q (+ n 1)) (== q (+ n 1)))))
+  (list 8))
+
+(mk-test
+  "project-multi-goal-body-conflict"
+  (run*
+    q
+    (fresh
+      (n)
+      (== n 7)
+      (project (n) (== q (+ n 1)) (== q (+ n 2)))))
+  (list))
+
+(mk-tests-run!)

lib/minikanren/tests/pythag.sx

@@ -0,0 +1,36 @@
+;; lib/minikanren/tests/pythag.sx — Pythagorean triple search.
+;;
+;; Uses ino + intarith goals to find triples (a, b, c) with
+;; a, b, c ∈ [1..N], a ≤ b, a² + b² = c². With intarith escapes
+;; the search runs at host-arithmetic speed.
+
+(define
+  digits-1-10
+  (list
+    1
+    2
+    3
+    4
+    5
+    6
+    7
+    8
+    9
+    10))
+
+(mk-test
+  "pythag-triples-1-to-10"
+  (let
+    ((triples (run* q (fresh (a b c a-sq b-sq sum c-sq) (ino a digits-1-10) (ino b digits-1-10) (ino c digits-1-10) (lteo-i a b) (*o-i a a a-sq) (*o-i b b b-sq) (*o-i c c c-sq) (pluso-i a-sq b-sq sum) (== sum c-sq) (== q (list a b c))))))
+    (and
+      (= (len triples) 2)
+      (and
+        (some
+          (fn (t) (= t (list 3 4 5)))
+          triples)
+        (some
+          (fn (t) (= t (list 6 8 10)))
+          triples))))
+  true)
+
+(mk-tests-run!)

lib/minikanren/tests/queens.sx

@@ -0,0 +1,45 @@
+;; lib/minikanren/tests/queens.sx — N-queens, the classic miniKanren benchmark.
+
+;; --- safe-diag (helper) ---
+
+(mk-test
+  "safe-diag-different-cols-different-distance"
+  (run* q (safe-diag 1 4 2))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "safe-diag-same-distance-fails"
+  (run* q (safe-diag 1 4 3))
+  (list))
+
+(mk-test
+  "safe-diag-same-distance-other-direction-fails"
+  (run* q (safe-diag 4 1 3))
+  (list))
+
+;; --- ino-each / range ---
+
+(mk-test
+  "range-1-to-4"
+  (range-1-to-n 4)
+  (list 1 2 3 4))
+(mk-test "range-empty" (range-1-to-n 0) (list))
+
+;; --- 4-queens: two solutions ---
+
+(mk-test
+  "queens-4"
+  (let
+    ((sols (run* q (fresh (a b c d) (== q (list a b c d)) (queens-cols (list a b c d) 4)))))
+    (and
+      (= (len sols) 2)
+      (and
+        (some
+          (fn (s) (= s (list 2 4 1 3)))
+          sols)
+        (some
+          (fn (s) (= s (list 3 1 4 2)))
+          sols))))
+  true)
+
+(mk-tests-run!)

lib/minikanren/tests/relations.sx

@@ -0,0 +1,291 @@
+;; lib/minikanren/tests/relations.sx — Phase 4 standard relations.
+;;
+;; Includes the classic miniKanren canaries: appendo forwards / backwards /
+;; bidirectionally, membero, listo enumeration.
+
+;; --- nullo / pairo ---
+
+(mk-test
+  "nullo-empty-succeeds"
+  (run* q (nullo (list)))
+  (list (make-symbol "_.0")))
+
+(mk-test "nullo-non-empty-fails" (run* q (nullo (list 1))) (list))
+
+(mk-test
+  "pairo-non-empty-succeeds"
+  (run* q (pairo (list 1 2)))
+  (list (make-symbol "_.0")))
+
+(mk-test "pairo-empty-fails" (run* q (pairo (list))) (list))
+
+;; --- caro / cdro / firsto / resto ---
+
+(mk-test
+  "caro-extracts-head"
+  (run* q (caro (list 1 2 3) q))
+  (list 1))
+
+(mk-test
+  "cdro-extracts-tail"
+  (run* q (cdro (list 1 2 3) q))
+  (list (list 2 3)))
+
+(mk-test
+  "firsto-alias-of-caro"
+  (run* q (firsto (list 10 20) q))
+  (list 10))
+
+(mk-test
+  "resto-alias-of-cdro"
+  (run* q (resto (list 10 20) q))
+  (list (list 20)))
+
+(mk-test
+  "caro-cdro-build"
+  (run*
+    q
+    (fresh
+      (h t)
+      (caro (list 1 2 3) h)
+      (cdro (list 1 2 3) t)
+      (== q (list h t))))
+  (list (list 1 (list 2 3))))
+
+;; --- conso ---
+
+(mk-test
+  "conso-forward"
+  (run* q (conso 0 (list 1 2 3) q))
+  (list (list 0 1 2 3)))
+
+(mk-test
+  "conso-extract-head"
+  (run*
+    q
+    (conso
+      q
+      (list 2 3)
+      (list 1 2 3)))
+  (list 1))
+
+(mk-test
+  "conso-extract-tail"
+  (run* q (conso 1 q (list 1 2 3)))
+  (list (list 2 3)))
+
+;; --- listo ---
+
+(mk-test
+  "listo-empty-succeeds"
+  (run* q (listo (list)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "listo-finite-list-succeeds"
+  (run* q (listo (list 1 2 3)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "listo-enumerates-shapes"
+  (run 3 q (listo q))
+  (list
+    (list)
+    (list (make-symbol "_.0"))
+    (list (make-symbol "_.0") (make-symbol "_.1"))))
+
+;; --- appendo: the canary ---
+
+(mk-test
+  "appendo-forward-simple"
+  (run*
+    q
+    (appendo (list 1 2) (list 3 4) q))
+  (list (list 1 2 3 4)))
+
+(mk-test
+  "appendo-forward-empty-l"
+  (run* q (appendo (list) (list 3 4) q))
+  (list (list 3 4)))
+
+(mk-test
+  "appendo-forward-empty-s"
+  (run* q (appendo (list 1 2) (list) q))
+  (list (list 1 2)))
+
+(mk-test
+  "appendo-recovers-tail"
+  (run*
+    q
+    (appendo
+      (list 1 2)
+      q
+      (list 1 2 3 4)))
+  (list (list 3 4)))
+
+(mk-test
+  "appendo-recovers-prefix"
+  (run*
+    q
+    (appendo
+      q
+      (list 3 4)
+      (list 1 2 3 4)))
+  (list (list 1 2)))
+
+(mk-test
+  "appendo-backward-all-splits"
+  (run*
+    q
+    (fresh
+      (l s)
+      (appendo l s (list 1 2 3))
+      (== q (list l s))))
+  (list
+    (list (list) (list 1 2 3))
+    (list (list 1) (list 2 3))
+    (list (list 1 2) (list 3))
+    (list (list 1 2 3) (list))))
+
+(mk-test
+  "appendo-empty-empty-empty"
+  (run* q (appendo (list) (list) q))
+  (list (list)))
+
+;; --- membero ---
+
+(mk-test
+  "membero-element-present"
+  (run
+    1
+    q
+    (membero 2 (list 1 2 3)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "membero-element-absent-empty"
+  (run* q (membero 99 (list 1 2 3)))
+  (list))
+
+(mk-test
+  "membero-enumerates"
+  (run* q (membero q (list "a" "b" "c")))
+  (list "a" "b" "c"))
+
+;; --- reverseo ---
+
+(mk-test
+  "reverseo-forward"
+  (run* q (reverseo (list 1 2 3) q))
+  (list (list 3 2 1)))
+
+(mk-test "reverseo-empty" (run* q (reverseo (list) q)) (list (list)))
+
+(mk-test
+  "reverseo-singleton"
+  (run* q (reverseo (list 42) q))
+  (list (list 42)))
+
+(mk-test
+  "reverseo-five"
+  (run*
+    q
+    (reverseo (list 1 2 3 4 5) q))
+  (list (list 5 4 3 2 1)))
+
+(mk-test
+  "reverseo-backward-one"
+  (run 1 q (reverseo q (list 1 2 3)))
+  (list (list 3 2 1)))
+
+(mk-test
+  "reverseo-round-trip"
+  (run*
+    q
+    (fresh (mid) (reverseo (list "a" "b" "c") mid) (reverseo mid q)))
+  (list (list "a" "b" "c")))
+
+;; --- lengtho (Peano-style) ---
+
+(mk-test "lengtho-empty-is-z" (run* q (lengtho (list) q)) (list :z))
+
+(mk-test
+  "lengtho-of-3"
+  (run* q (lengtho (list "a" "b" "c") q))
+  (list (list :s (list :s (list :s :z)))))
+
+(mk-test
+  "lengtho-empty-from-zero"
+  (run 1 q (lengtho q :z))
+  (list (list)))
+
+(mk-test
+  "lengtho-enumerates-of-length-2"
+  (run 1 q (lengtho q (list :s (list :s :z))))
+  (list (list (make-symbol "_.0") (make-symbol "_.1"))))
+
+;; --- inserto ---
+
+(mk-test
+  "inserto-front"
+  (run* q (inserto 0 (list 1 2 3) q))
+  (list
+    (list 0 1 2 3)
+    (list 1 0 2 3)
+    (list 1 2 0 3)
+    (list 1 2 3 0)))
+
+(mk-test
+  "inserto-empty"
+  (run* q (inserto 0 (list) q))
+  (list (list 0)))
+
+;; --- permuteo ---
+
+(mk-test "permuteo-empty" (run* q (permuteo (list) q)) (list (list)))
+
+(mk-test
+  "permuteo-singleton"
+  (run* q (permuteo (list 42) q))
+  (list (list 42)))
+
+(mk-test
+  "permuteo-two"
+  (run* q (permuteo (list 1 2) q))
+  (list (list 1 2) (list 2 1)))
+
+(mk-test
+  "permuteo-three-as-set"
+  (let
+    ((perms (run* q (permuteo (list 1 2 3) q))))
+    (and
+      (= (len perms) 6)
+      (and
+        (some (fn (p) (= p (list 1 2 3))) perms)
+        (and
+          (some
+            (fn (p) (= p (list 2 1 3)))
+            perms)
+          (and
+            (some
+              (fn (p) (= p (list 1 3 2)))
+              perms)
+            (and
+              (some
+                (fn (p) (= p (list 2 3 1)))
+                perms)
+              (and
+                (some
+                  (fn (p) (= p (list 3 1 2)))
+                  perms)
+                (some
+                  (fn (p) (= p (list 3 2 1)))
+                  perms))))))))
+  true)
+
+(mk-test
+  "permuteo-backward-finds-input"
+  (run 1 q (permuteo q (list "a" "b" "c")))
+  (list (list "a" "b" "c")))
+
+(mk-tests-run!)

lib/minikanren/tests/run.sx

@@ -0,0 +1,114 @@
+;; lib/minikanren/tests/run.sx — Phase 3 tests for run* / run / reify.
+
+;; --- canonical TRS one-liners ---
+
+(mk-test "run*-eq-one" (run* q (== q 1)) (list 1))
+(mk-test "run*-eq-string" (run* q (== q "hello")) (list "hello"))
+(mk-test "run*-eq-symbol" (run* q (== q (quote sym))) (list (quote sym)))
+(mk-test "run*-fail-empty" (run* q (== 1 2)) (list))
+
+;; --- run with a count ---
+
+(mk-test
+  "run-3-of-many"
+  (run
+    3
+    q
+    (conde
+      ((== q 1))
+      ((== q 2))
+      ((== q 3))
+      ((== q 4))
+      ((== q 5))))
+  (list 1 2 3))
+
+(mk-test "run-zero-empty" (run 0 q (== q 1)) (list))
+
+(mk-test
+  "run-1-takes-one"
+  (run 1 q (conde ((== q "a")) ((== q "b"))))
+  (list "a"))
+
+;; --- reification: unbound vars get _.N left-to-right ---
+
+(mk-test
+  "reify-single-unbound"
+  (run* q (fresh (x) (== q x)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "reify-pair-unbound"
+  (run* q (fresh (x y) (== q (list x y))))
+  (list (list (make-symbol "_.0") (make-symbol "_.1"))))
+
+(mk-test
+  "reify-mixed-bound-unbound"
+  (run* q (fresh (x y) (== q (list 1 x 2 y))))
+  (list
+    (list 1 (make-symbol "_.0") 2 (make-symbol "_.1"))))
+
+(mk-test
+  "reify-shared-unbound-same-name"
+  (run* q (fresh (x) (== q (list x x))))
+  (list (list (make-symbol "_.0") (make-symbol "_.0"))))
+
+(mk-test
+  "reify-distinct-unbound-distinct-names"
+  (run* q (fresh (x y) (== q (list x y x y))))
+  (list
+    (list
+      (make-symbol "_.0")
+      (make-symbol "_.1")
+      (make-symbol "_.0")
+      (make-symbol "_.1"))))
+
+;; --- conde + run* ---
+
+(mk-test
+  "run*-conde-three"
+  (run*
+    q
+    (conde ((== q 1)) ((== q 2)) ((== q 3))))
+  (list 1 2 3))
+
+(mk-test
+  "run*-conde-fresh-mix"
+  (run*
+    q
+    (conde ((fresh (x) (== q (list 1 x)))) ((== q "ground"))))
+  (list (list 1 (make-symbol "_.0")) "ground"))
+
+;; --- run* + conjunction ---
+
+(mk-test
+  "run*-conj-binds-q"
+  (run* q (fresh (x) (== x 5) (== q (list x x))))
+  (list (list 5 5)))
+
+;; --- run* + condu ---
+
+(mk-test
+  "run*-condu-first-wins"
+  (run* q (condu ((== q 1)) ((== q 2))))
+  (list 1))
+
+(mk-test
+  "run*-onceo-trim"
+  (run* q (onceo (conde ((== q "a")) ((== q "b")))))
+  (list "a"))
+
+;; --- multi-goal run ---
+
+(mk-test
+  "run*-three-goals"
+  (run*
+    q
+    (fresh
+      (x y z)
+      (== x 1)
+      (== y 2)
+      (== z 3)
+      (== q (list x y z))))
+  (list (list 1 2 3)))
+
+(mk-tests-run!)

lib/minikanren/tests/types.sx

@@ -0,0 +1,52 @@
+;; lib/minikanren/tests/types.sx — type-predicate goals.
+
+(mk-test
+  "numbero-on-int"
+  (run* q (numbero 5))
+  (list (make-symbol "_.0")))
+(mk-test "numbero-on-string" (run* q (numbero "5")) (list))
+(mk-test "numbero-on-symbol" (run* q (numbero (quote x))) (list))
+(mk-test "numbero-on-list" (run* q (numbero (list 1))) (list))
+
+(mk-test
+  "stringo-on-string"
+  (run* q (stringo "hi"))
+  (list (make-symbol "_.0")))
+(mk-test "stringo-on-int" (run* q (stringo 5)) (list))
+(mk-test
+  "stringo-on-keyword"
+  (run* q (stringo :k))
+  (list (make-symbol "_.0")))  ;; SX keywords ARE strings
+
+(mk-test
+  "symbolo-on-symbol"
+  (run* q (symbolo (quote x)))
+  (list (make-symbol "_.0")))
+(mk-test "symbolo-on-string" (run* q (symbolo "x")) (list))
+(mk-test "symbolo-on-int" (run* q (symbolo 5)) (list))
+
+;; --- combine with membero for type-filtered enumeration ---
+
+(mk-test
+  "membero-numbero-filter"
+  (run*
+    q
+    (fresh
+      (x)
+      (membero x (list 1 "a" 2 "b" 3))
+      (numbero x)
+      (== q x)))
+  (list 1 2 3))
+
+(mk-test
+  "membero-stringo-filter"
+  (run*
+    q
+    (fresh
+      (x)
+      (membero x (list 1 "a" 2 "b" 3))
+      (stringo x)
+      (== q x)))
+  (list "a" "b"))
+
+(mk-tests-run!)

lib/minikanren/tests/unify.sx

@@ -0,0 +1,293 @@
+;; lib/minikanren/tests/unify.sx — Phase 1 tests for unify.sx.
+;;
+;; Loads into a session that already has lib/guest/match.sx and
+;; lib/minikanren/unify.sx defined. Tests are top-level forms.
+;; Call (mk-tests-run!) afterwards to get the totals.
+;;
+;; Note: SX dict equality is reference-based, so tests check the *effect*
+;; of a unification (success/failure flag, or walked bindings) rather than
+;; the raw substitution dict.
+
+(define mk-test-pass 0)
+(define mk-test-fail 0)
+(define mk-test-fails (list))
+
+(define
+  mk-test
+  (fn
+    (name actual expected)
+    (if
+      (= actual expected)
+      (set! mk-test-pass (+ mk-test-pass 1))
+      (begin
+        (set! mk-test-fail (+ mk-test-fail 1))
+        (append! mk-test-fails {:name name :expected expected :actual actual})))))
+
+(define mk-tests-run! (fn () {:total (+ mk-test-pass mk-test-fail) :passed mk-test-pass :failed mk-test-fail :fails mk-test-fails}))
+
+(define mk-unified? (fn (s) (if (= s nil) false true)))
+
+;; --- fresh variable construction ---
+
+(mk-test
+  "make-var-distinct"
+  (let ((a (make-var)) (b (make-var))) (= (var-name a) (var-name b)))
+  false)
+
+(mk-test "make-var-is-var" (mk-var? (make-var)) true)
+(mk-test "var?-num" (mk-var? 5) false)
+(mk-test "var?-list" (mk-var? (list 1 2)) false)
+(mk-test "var?-string" (mk-var? "hi") false)
+(mk-test "var?-empty" (mk-var? (list)) false)
+(mk-test "var?-bool" (mk-var? true) false)
+
+;; --- empty substitution ---
+
+(mk-test "empty-s-walk-num" (mk-walk 5 empty-s) 5)
+(mk-test "empty-s-walk-str" (mk-walk "x" empty-s) "x")
+(mk-test
+  "empty-s-walk-list"
+  (mk-walk (list 1 2) empty-s)
+  (list 1 2))
+(mk-test
+  "empty-s-walk-unbound-var"
+  (let ((x (make-var))) (= (mk-walk x empty-s) x))
+  true)
+
+;; --- walk: top-level chain resolution ---
+
+(mk-test
+  "walk-direct-binding"
+  (mk-walk (mk-var "x") (extend "x" 7 empty-s))
+  7)
+
+(mk-test
+  "walk-two-step-chain"
+  (mk-walk
+    (mk-var "x")
+    (extend "x" (mk-var "y") (extend "y" 9 empty-s)))
+  9)
+
+(mk-test
+  "walk-three-step-chain"
+  (mk-walk
+    (mk-var "a")
+    (extend
+      "a"
+      (mk-var "b")
+      (extend "b" (mk-var "c") (extend "c" 42 empty-s))))
+  42)
+
+(mk-test
+  "walk-stops-at-list"
+  (mk-walk (list 1 (mk-var "x")) (extend "x" 5 empty-s))
+  (list 1 (mk-var "x")))
+
+;; --- walk*: deep walk into lists ---
+
+(mk-test
+  "walk*-flat-list-with-vars"
+  (mk-walk*
+    (list (mk-var "x") 2 (mk-var "y"))
+    (extend "x" 1 (extend "y" 3 empty-s)))
+  (list 1 2 3))
+
+(mk-test
+  "walk*-nested-list"
+  (mk-walk*
+    (list 1 (mk-var "x") (list 2 (mk-var "y")))
+    (extend "x" 5 (extend "y" 6 empty-s)))
+  (list 1 5 (list 2 6)))
+
+(mk-test
+  "walk*-unbound-stays-var"
+  (let
+    ((x (mk-var "x")))
+    (= (mk-walk* (list 1 x) empty-s) (list 1 x)))
+  true)
+
+(mk-test "walk*-atom" (mk-walk* 5 empty-s) 5)
+
+;; --- unify atoms (success / failure semantics, not dict shape) ---
+
+(mk-test
+  "unify-num-eq-succeeds"
+  (mk-unified? (mk-unify 5 5 empty-s))
+  true)
+(mk-test "unify-num-neq-fails" (mk-unify 5 6 empty-s) nil)
+(mk-test
+  "unify-str-eq-succeeds"
+  (mk-unified? (mk-unify "a" "a" empty-s))
+  true)
+(mk-test "unify-str-neq-fails" (mk-unify "a" "b" empty-s) nil)
+(mk-test
+  "unify-bool-eq-succeeds"
+  (mk-unified? (mk-unify true true empty-s))
+  true)
+(mk-test "unify-bool-neq-fails" (mk-unify true false empty-s) nil)
+(mk-test
+  "unify-nil-eq-succeeds"
+  (mk-unified? (mk-unify nil nil empty-s))
+  true)
+(mk-test
+  "unify-empty-list-succeeds"
+  (mk-unified? (mk-unify (list) (list) empty-s))
+  true)
+
+;; --- unify var with anything (walk to verify binding) ---
+
+(mk-test
+  "unify-var-num-binds"
+  (mk-walk (mk-var "x") (mk-unify (mk-var "x") 5 empty-s))
+  5)
+
+(mk-test
+  "unify-num-var-binds"
+  (mk-walk (mk-var "x") (mk-unify 5 (mk-var "x") empty-s))
+  5)
+
+(mk-test
+  "unify-var-list-binds"
+  (mk-walk
+    (mk-var "x")
+    (mk-unify (mk-var "x") (list 1 2) empty-s))
+  (list 1 2))
+
+(mk-test
+  "unify-var-var-same-no-extend"
+  (mk-unified? (mk-unify (mk-var "x") (mk-var "x") empty-s))
+  true)
+
+(mk-test
+  "unify-var-var-different-walks-equal"
+  (let
+    ((s (mk-unify (mk-var "x") (mk-var "y") empty-s)))
+    (= (mk-walk (mk-var "x") s) (mk-walk (mk-var "y") s)))
+  true)
+
+;; --- unify lists positionally ---
+
+(mk-test
+  "unify-list-equal-succeeds"
+  (mk-unified?
+    (mk-unify
+      (list 1 2 3)
+      (list 1 2 3)
+      empty-s))
+  true)
+
+(mk-test
+  "unify-list-different-length-fails-1"
+  (mk-unify
+    (list 1 2)
+    (list 1 2 3)
+    empty-s)
+  nil)
+
+(mk-test
+  "unify-list-different-length-fails-2"
+  (mk-unify
+    (list 1 2 3)
+    (list 1 2)
+    empty-s)
+  nil)
+
+(mk-test
+  "unify-list-mismatch-fails"
+  (mk-unify
+    (list 1 2)
+    (list 1 3)
+    empty-s)
+  nil)
+
+(mk-test
+  "unify-list-vs-atom-fails"
+  (mk-unify (list 1 2) 5 empty-s)
+  nil)
+
+(mk-test
+  "unify-empty-vs-non-empty-fails"
+  (mk-unify (list) (list 1) empty-s)
+  nil)
+
+(mk-test
+  "unify-list-with-vars-walks"
+  (mk-walk*
+    (list (mk-var "x") (mk-var "y"))
+    (mk-unify
+      (list (mk-var "x") (mk-var "y"))
+      (list 1 2)
+      empty-s))
+  (list 1 2))
+
+(mk-test
+  "unify-nested-lists-with-vars-walks"
+  (mk-walk*
+    (list (mk-var "x") (list (mk-var "y") 3))
+    (mk-unify
+      (list (mk-var "x") (list (mk-var "y") 3))
+      (list 1 (list 2 3))
+      empty-s))
+  (list 1 (list 2 3)))
+
+;; --- unify chained substitutions ---
+
+(mk-test
+  "unify-chain-var-var-then-atom"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")))
+    (let
+      ((s1 (mk-unify x y empty-s)))
+      (mk-walk x (mk-unify y 7 s1))))
+  7)
+
+(mk-test
+  "unify-already-bound-consistent"
+  (let
+    ((s (extend "x" 5 empty-s)))
+    (mk-unified? (mk-unify (mk-var "x") 5 s)))
+  true)
+
+(mk-test
+  "unify-already-bound-conflict-fails"
+  (let
+    ((s (extend "x" 5 empty-s)))
+    (mk-unify (mk-var "x") 6 s))
+  nil)
+
+;; --- occurs check (opt-in) ---
+
+(mk-test
+  "unify-no-occurs-default-succeeds"
+  (let
+    ((x (mk-var "x")))
+    (mk-unified? (mk-unify x (list 1 x) empty-s)))
+  true)
+
+(mk-test
+  "unify-occurs-direct-fails"
+  (let ((x (mk-var "x"))) (mk-unify-check x (list 1 x) empty-s))
+  nil)
+
+(mk-test
+  "unify-occurs-nested-fails"
+  (let
+    ((x (mk-var "x")))
+    (mk-unify-check x (list 1 (list 2 x)) empty-s))
+  nil)
+
+(mk-test
+  "unify-occurs-non-occurring-succeeds"
+  (let
+    ((x (mk-var "x")))
+    (mk-unified? (mk-unify-check x 5 empty-s)))
+  true)
+
+(mk-test
+  "unify-occurs-via-chain-fails"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")))
+    (let ((s (extend "y" (list x) empty-s))) (mk-unify-check x y s)))
+  nil)
+
+(mk-tests-run!)

lib/minikanren/unify.sx

@@ -0,0 +1,82 @@
+;; lib/minikanren/unify.sx — Phase 1 + cons-cell extension.
+;;
+;; miniKanren-on-SX, built on lib/guest/match.sx. The kit ships the heavy
+;; lifting (walk-with, unify-with, occurs-with, extend, empty-subst,
+;; mk-var/is-var?/var-name); this file supplies a miniKanren-shaped cfg
+;; and a thin public API.
+;;
+;; Term shapes:
+;;   logic var   : (:var NAME)              — kit's mk-var
+;;   cons cell   : (:cons HEAD TAIL)        — for relational programming
+;;                 (built by mk-cons; lets relations decompose lists by
+;;                 head/tail without proper improper pairs in the host)
+;;   native list : SX list (a b c)          — also unifies pair-style:
+;;                 args = (head, tail) so (1 2 3) ≡ (:cons 1 (:cons 2 (:cons 3 ())))
+;;   atom        : number / string / symbol / boolean / nil / ()
+;;
+;; Substitution: SX dict mapping VAR-NAME → term. Empty = (empty-subst).
+
+(define mk-cons (fn (h t) (list :cons h t)))
+
+(define
+  mk-cons-cell?
+  (fn (t) (and (list? t) (not (empty? t)) (= (first t) :cons))))
+
+(define mk-cons-head (fn (t) (nth t 1)))
+(define mk-cons-tail (fn (t) (nth t 2)))
+
+(define
+  mk-list-pair?
+  (fn (t) (and (list? t) (not (empty? t)) (not (is-var? t)))))
+
+(define mk-list-pair-head (fn (t) :pair))
+
+(define
+  mk-list-pair-args
+  (fn
+    (t)
+    (cond
+      ((mk-cons-cell? t) (list (mk-cons-head t) (mk-cons-tail t)))
+      (:else (list (first t) (rest t))))))
+
+(define mk-cfg {:ctor-head mk-list-pair-head :var? is-var? :ctor? mk-list-pair? :occurs-check? false :var-name var-name :ctor-args mk-list-pair-args})
+
+(define mk-cfg-occurs {:ctor-head mk-list-pair-head :var? is-var? :ctor? mk-list-pair? :occurs-check? true :var-name var-name :ctor-args mk-list-pair-args})
+
+(define empty-s (empty-subst))
+
+(define mk-fresh-counter 0)
+
+(define
+  make-var
+  (fn
+    ()
+    (begin
+      (set! mk-fresh-counter (+ mk-fresh-counter 1))
+      (mk-var (str "_." mk-fresh-counter)))))
+
+(define mk-var? is-var?)
+
+(define mk-walk (fn (t s) (walk-with mk-cfg t s)))
+
+(define
+  mk-walk*
+  (fn
+    (t s)
+    (let
+      ((w (mk-walk t s)))
+      (cond
+        ((mk-cons-cell? w)
+          (let
+            ((h (mk-walk* (mk-cons-head w) s))
+              (tl (mk-walk* (mk-cons-tail w) s)))
+            (cond
+              ((empty? tl) (list h))
+              ((mk-cons-cell? tl) tl)
+              ((list? tl) (cons h tl))
+              (:else (mk-cons h tl)))))
+        ((mk-list-pair? w) (map (fn (a) (mk-walk* a s)) w))
+        (:else w)))))
+
+(define mk-unify (fn (u v s) (unify-with mk-cfg u v s)))
+(define mk-unify-check (fn (u v s) (unify-with mk-cfg-occurs u v s)))

plans/minikanren-on-sx.md

@@ -50,68 +50,106 @@ Key semantic mappings:
 ## Roadmap
 
 ### Phase 1 — variables + unification
-- [ ] `make-var` → fresh logic variable (unique mutable box)
+- [x] `make-var` → fresh logic variable (unique mutable box)
-- [ ] `var?` `v` → bool — is this a logic variable?
+- [x] `var?` `v` → bool — is this a logic variable?
-- [ ] `walk` `term` `subst` → follow substitution chain to ground term or unbound var
+- [x] `walk` `term` `subst` → follow substitution chain to ground term or unbound var
-- [ ] `walk*` `term` `subst` → deep walk (recurse into lists/dicts)
+- [x] `walk*` `term` `subst` → deep walk (recurse into lists/dicts)
-- [ ] `unify` `u` `v` `subst` → extended substitution or `#f` (failure)
+- [x] `unify` `u` `v` `subst` → extended substitution or `#f` (failure)
       Handles: var/var, var/term, term/var, list unification, number/string/symbol equality.
       No occurs check by default; `unify-check` with occurs check as opt-in.
-- [ ] Empty substitution `empty-s` = `(list)` (empty assoc list)
+- [x] Empty substitution `empty-s` (dict-based via kit's `empty-subst` — assoc list was a sketch; kit ships dict, kept it)
-- [ ] Tests in `lib/minikanren/tests/unify.sx`: ground terms, vars, lists, failure, occurs
+- [x] Tests in `lib/minikanren/tests/unify.sx`: ground terms, vars, lists, failure, occurs
 
 ### Phase 2 — streams + goals
-- [ ] Stream type: `mzero` (empty stream = `nil`), `unit s` (singleton = `(list s)`),
+- [x] Stream type: `mzero` (empty), `unit s` (singleton), `mk-mplus` (interleave),
-      `mplus` (interleave two streams), `bind` (apply goal to stream)
+      `mk-bind` (apply goal to stream). Names mk-prefixed because SX has a host
-- [ ] Lazy streams via `delay`/`force` — mature pairs for depth-first, immature for lazy
+      `bind` primitive that silently shadows user defines.
-- [ ] `==` goal: `(fn (s) (let ((s2 (unify u v s))) (if s2 (unit s2) mzero)))`
+- [x] Lazy streams via thunks: a paused stream is a zero-arg fn; mk-mplus suspends
-- [ ] `succeed` / `fail` — trivial goals
+      and swaps when its left operand is paused, giving fair interleaving.
-- [ ] `fresh` — `(fn (f) (fn (s) ((f (make-var)) s)))` — introduces one var; `fresh*` for many
+- [x] `==` goal: `(fn (s) (let ((s2 (mk-unify u v s))) (if s2 (unit s2) mzero)))`
-- [ ] `conde` — interleaving disjunction of goal lists
+- [x] `==-check` — opt-in occurs-checked equality goal
-- [ ] `condu` — committed choice (soft-cut): only explores first successful clause
+- [x] `succeed` / `fail` — trivial goals
-- [ ] `onceo` — succeeds at most once
+- [x] `conj2` / `mk-conj` (variadic) — sequential conjunction
-- [ ] Tests: basic goal composition, backtracking, interleaving
+- [x] `disj2` / `mk-disj` (variadic) — interleaved disjunction (raw — `conde`
+      adds the implicit-conj-per-clause sugar later)
+- [x] `fresh` — introduces logic variables inside a goal body. Implemented as a
+      defmacro: `(fresh (x y) g1 g2 ...)` ⇒ `(let ((x (make-var)) (y (make-var)))
+      (mk-conj g1 g2 ...))`. Also `call-fresh` for programmatic goal building.
+- [x] `conde` — sugar over disj+conj, one row per clause; defmacro that
+      wraps each clause body in `mk-conj` and folds via `mk-disj`. Notes:
+      with eager streams ordering is left-clause-first DFS; true interleaving
+      requires paused thunks (Phase 4 recursive relations).
+- [x] `condu` — committed choice. defmacro folding clauses into a runtime
+      `condu-try` walker; first clause whose head goal yields a non-empty
+      stream commits its first answer, rest-goals run on that single subst.
+- [x] `onceo` — `(stream-take 1 (g s))`; trims a goal's stream to ≤1 answer.
+- [x] Tests: basic goal composition, backtracking, interleaving (110 cumulative)
 
 ### Phase 3 — run + reification
-- [ ] `run*` `goal` → list of all answers (reified)
+- [x] `run*` `goal` → list of all answers (reified). defmacro: bind q-name as
-- [ ] `run n` `goal` → list of first n answers
+      fresh var, conj goals, take all from stream, reify each.
-- [ ] `reify` `term` `subst` → replace unbound vars with `_0`, `_1`, ... names
+- [x] `run n` `goal` → list of first n answers (defmacro; n = -1 means all)
-- [ ] `reify-s` → builds reification substitution for naming unbound vars consistently
+- [x] `reify` `term` `subst` → walk* + build reification subst + walk* again
-- [ ] `fresh` with multiple variables: `(fresh (x y z) goal)` sugar
+- [x] `reify-s` → maps each unbound var (in left-to-right walk order) to a
-- [ ] Query variable conventions: `q` as canonical query variable
+      `_.N` symbol via `(make-symbol (str "_." n))`
-- [ ] Tests: classic miniKanren programs — `(run* q (== q 1))` → `(1)`,
+- [x] `fresh` with multiple variables — already shipped Phase 2B.
+- [x] Query variable conventions: `q` as canonical query variable (matches TRS)
+- [x] Tests: classic miniKanren programs — `(run* q (== q 1))` → `(1)`,
       `(run* q (conde ((== q 1)) ((== q 2))))` → `(1 2)`,
-      Peano arithmetic, `appendo` preview
+      `(run* q (fresh (x y) (== q (list x y))))` → `((_.0 _.1))`. Peano +
+      `appendo` deferred to Phase 4.
 
 ### Phase 4 — standard relations
-- [ ] `appendo` `l` `s` `ls` — list append, runs forwards and backwards
+- [x] `appendo` `l` `s` `ls` — list append, runs forwards AND backwards.
-- [ ] `membero` `x` `l` — x is a member of l
+      Canary green: `(run* q (appendo (1 2) (3 4) q))` → `((1 2 3 4))`;
-- [ ] `listo` `l` — l is a proper list
+      `(run* q (fresh (l s) (appendo l s (1 2 3)) (== q (list l s))))` →
-- [ ] `nullo` `l` — l is empty
+      all four splits.
-- [ ] `pairo` `p` — p is a pair (cons cell)
+- [x] `membero` `x` `l` — enumerates: `(run* q (membero q (a b c)))` → `(a b c)`
-- [ ] `caro` `p` `a` — car of pair
+- [x] `listo` `l` — l is a proper list; enumerates list shapes with laziness
-- [ ] `cdro` `p` `d` — cdr of pair
+- [x] `nullo` `l` — l is empty
-- [ ] `conso` `a` `d` `p` — cons
+- [x] `pairo` `p` — p is a (non-empty) cons-cell / list
-- [ ] `firsto` / `resto` — aliases for caro/cdro
+- [x] `caro` / `cdro` / `conso` / `firsto` / `resto`
-- [ ] `reverseo` `l` `r` — reverse of list
+- [x] `reverseo` `l` `r` — reverse of list. Forward is fast; backward is `run 1`-clean,
-- [ ] `flatteno` `l` `f` — flatten nested lists
+      `run*` diverges due to interleaved unbounded list search (canonical TRS issue).
-- [ ] `permuteo` `l` `p` — permutation of list
+- [x] `flatteno` `l` `f` — flatten nested lists. Three conde clauses:
-- [ ] `lengtho` `l` `n` — length as a relation (Peano or integer)
+      empty → empty; pair → recurse on car & cdr + appendo; otherwise atom →
-- [ ] Tests: run each relation forwards and backwards; generate from partial inputs
+      `(== flat (list tree))`. Atom-ness is asserted via `nafc (nullo tree)
+      + nafc (pairo tree)` — both succeed only when tree is a ground non-list.
+      Works on ground inputs.
+- [x] `permuteo` `l` `p` — permutation of list. Built on `inserto` (insert at any
+      position) and recursive permutation of tail. All 6 perms of (1 2 3) generated
+      forward; backward `run 1 q (permuteo q (a b c))` finds the input.
+- [x] `lengtho` `l` `n` — length as a relation, Peano-encoded:
+      `:z` / `(:s :z)` / `(:s (:s :z))` ... matches TRS. Forward is direct;
+      backward enumerates lists of a given length.
+- [x] Tests: run each relation forwards and backwards (so far 25 in
+      `tests/relations.sx`; reverseo/flatteno/permuteo/lengtho deferred)
 
 ### Phase 5 — `project` + `matche` + negation
-- [ ] `project` `(x ...) body` — access reified values of logic vars inside a goal;
+- [x] `project` `(x ...) body` — defmacro: rebinds named vars to `(mk-walk* var s)`
-      escapes to ground values for arithmetic or string ops
+      in the body's lexical scope, then runs `(mk-conj body...)` on the same
-- [ ] `matche` — pattern matching over logic terms (extension from core.logic)
+      substitution. Hygienic via gensym'd `s`-param. (`Phase 5 piece B`)
-      `(matche l ((head . tail) goal) (() goal))`
+- [x] `matche` — pattern matching over logic terms. Pattern grammar: `_` /
-- [ ] `conda` — soft-cut disjunction (like Prolog `->`)
+      symbol / atom / `()` / `(p1 p2 ... pn)`. Each clause becomes
-- [ ] `condu` — committed choice (already in phase 2; refine semantics here)
+      `(fresh (vars-in-pat) (== target pat-expr) body...)`. Repeated symbol
-- [ ] `nafc` — negation as finite failure with constraint
+      names in a pattern produce the same fresh var, so they unify (== check).
+      Built without quasiquote (the expander does not recurse into lambda
+      bodies). Fixed-length list patterns only — head/tail destructuring uses
+      `(fresh (a d) (conso a d target) body)` directly.
+- [x] `conda` — soft-cut: first non-failing head wins; ALL of head's answers
+      flow through rest-goals; later clauses not tried (`Phase 5 piece A`)
+- [x] `condu` — committed choice (Phase 2)
+- [x] `nafc` — negation as finite failure: `(nafc g)` yields the input subst
+      iff g has zero answers. Standard caveats apply (open-world unsoundness;
+      diverges if g is infinite). `Phase 5 piece C`.
 - [ ] Tests: Zebra puzzle, N-queens, Sudoku via `project`, family relations via `matche`
 
 ### Phase 6 — arithmetic constraints CLP(FD)
 - [ ] Finite domain variables: `fd-var` with domain `[lo..hi]`
-- [ ] `in` `x` `domain` — constrain x to domain
+- [x] `ino` `x` `domain` — alias for `(membero x domain)` with the
+      constraint-store-friendly argument order. Sufficient for the
+      enumerate-then-filter style of finite-domain solving.
+- [x] `all-distincto` `l` — pairwise-distinct elements via `nafc + membero`.
 - [ ] `fd-eq` `x` `y` — x = y (constraint propagation)
 - [ ] `fd-neq` `x` `y` — x ≠ y
 - [ ] `fd-lt` `fd-lte` `fd-gt` `fd-gte` — ordering constraints
@@ -135,4 +173,167 @@ _(none yet)_
 
 _Newest first._
 
-_(awaiting phase 1)_
+- **2026-05-08** — **Cyclic graph behaviour test (motivates Phase 7 tabling)**:
+  Demonstrates that naive patho on a 2-cycle generates ever-longer paths.
+  `run 5` truncates to a finite prefix; `run*` would diverge. This is
+  exactly the test case Phase 7 (tabled / SLG resolution) is designed
+  to fix. 3 new tests, 331/331 cumulative.
+- **2026-05-08** — **numbero / stringo / symbolo (type predicates)**: ground-only
+  type tests via project. Compose with `membero` for type-filtered enumeration:
+  `(fresh (x) (membero x (1 "a" 2 "b" 3)) (numbero x) (== q x))` → `(1 2 3)`.
+  Note: SX keywords are strings, so `(stringo :k)` succeeds. 12 new tests,
+  328/328 cumulative.
+- **2026-05-08** — **Graph reachability via patho**: classic miniKanren
+  graph search. `edgeo` looks up edges in a fact list via `membero`; `patho`
+  recursively builds paths via direct-edge OR (one edge + recurse + cons).
+  Enumerates all paths between two nodes, including alternates through
+  shortcuts. 6 new tests, 316/316 cumulative.
+- **2026-05-08** — **everyo / someo (predicate-style relations)**:
+  `(everyo rel l)` — every element of l satisfies rel; `(someo rel l)` —
+  some element does. Both compose with intarith for numeric tests:
+  `(everyo (fn (x) (lto-i x 10)) (list 1 5 9))` succeeds. 10 new tests,
+  310/310 cumulative.
+- **2026-05-08** — **mapo (relational map) — 300 test milestone**: `(mapo
+  rel l1 l2)` succeeds when l2 is l1 with each element rel-related. Works
+  forward and backward; composes with intarith — `(mapo (fn (a b) (*o-i
+  a a b)) (1 2 3 4) q)` → `((1 4 9 16))`. 7 new tests, **300/300** cumulative.
+- **2026-05-08** — **samelengtho**: classic miniKanren relation that
+  succeeds when two lists have equal length. Symmetric — works to enumerate
+  both lists fresh: `(run 3 q (fresh (l1 l2) (samelengtho l1 l2) (== q
+  (list l1 l2))))` produces empty/empty, then 1-elem pairs, then 2-elem.
+  5 new tests, 293/293 cumulative.
+- **2026-05-08** — **Pythagorean triples (intarith showcase)**: search for
+  (a, b, c) ∈ [1..10]³, a ≤ b, a² + b² = c² via `ino + lteo-i + *o-i +
+  pluso-i + ==`. Finds exactly `(3 4 5)` and `(6 8 10)`. Demonstrates the
+  enumerate-then-filter pattern with intarith escape into host arithmetic.
+  1 new test, 288/288 cumulative.
+- **2026-05-08** — **intarith.sx — fast ground-only integer arithmetic**:
+  pluso-i / minuso-i / *o-i / lto-i / lteo-i / neqo-i wrap host arithmetic
+  via `project`. They are not relational like Peano `pluso` (require args
+  to walk to numbers), but run at native host speed — a viable escape
+  hatch when puzzle size makes Peano impractical. Composes with relational
+  goals: `(membero x dom) (lto-i x 3)` filters dom by `< 3`. 18 new tests,
+  287/287 cumulative.
+- **2026-05-08** — **2x2 Latin square**: small classic constraint demo using
+  `ino` + 4 `all-distincto` constraints. Enumerates exactly 2 squares
+  (`((1 2)(2 1))` and `((2 1)(1 2))`); a clue (top-left = 1) narrows to one.
+  3 new tests, 269/269 cumulative. Note: 3x3 (12 squares) is the natural
+  showcase but too slow under naive enumerate-then-filter — needs Phase 6
+  arc-consistency.
+- **2026-05-08** — **rembero / assoco / nth-o**: more standard list relations.
+  rembero removes the first occurrence (uses `nafc (== a x)` to gate the
+  skip clause, so it's well-defined on ground lists). assoco is alist
+  lookup — works forward (key → value) and backward (value → key). nth-o
+  uses Peano indices into a list. 13 new tests, 266/266 cumulative.
+- **2026-05-08** — **flatteno**: nested-list flattener via conde + appendo.
+  Atom-ness is detected via `nafc (nullo ...) + nafc (pairo ...)` so the
+  third clause only fires when the input is a ground non-list. Works for
+  `()` / atoms / flat lists / arbitrarily-nested lists. 7 new tests,
+  253/253 cumulative. Phase 4 list relations all complete.
+- **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`
+  uses `project` to escape into host arithmetic for the `|c_i - c_j| ≠
+  |i - j|` diagonal check; `all-cells-safe` walks pairs at construction
+  time. `(run* q (fresh (a b c d) (== q (list a b c d)) (queens-cols
+  (list a b c d) 4)))` returns the two valid 4-queens placements
+  `(2 4 1 3)` and `(3 1 4 2)`. 6 new tests, 243/243 cumulative.
+- **2026-05-08** — **Phase 6 piece A — minimal FD (ino + all-distincto)**:
+  `lib/minikanren/fd.sx`. `ino` is `membero` with the FD-style argument
+  order; `all-distincto` is `nafc + membero` walking the list. Together
+  they cover the enumerate-then-filter style of finite-domain solving —
+  `(fresh (a b c) (ino a D) (ino b D) (ino c D) (all-distincto (list a b c)))`
+  enumerates all distinct triples from D. Full FD with arc-consistency,
+  fd-plus etc. is still pending. 9 new tests, 237/237 cumulative.
+- **2026-05-08** — **Classic puzzles + matche keyword fix**: matche now emits
+  keywords bare in the pattern->expr conversion so they self-evaluate to their
+  string name and unify with the same-keyword target value (instead of becoming
+  a quoted-keyword type). New `tests/classics.sx`: pet permutation puzzle,
+  parent/grandparent inference over a fact list, symbolic differentiation
+  driven by matche dispatch on `:x` / `(:+ a b)` / `(:* a b)` patterns.
+  6 new tests, 228/228 cumulative.
+- **2026-05-08** — **Phase 5 piece D — matche, Phase 5 done**: pattern matching
+  macro (`lib/minikanren/matche.sx`) — symbols become fresh vars, atoms become
+  literals, lists recurse positionally, repeated names unify. 14 new tests
+  (literals, vars, wildcards, list patterns, multi-clause dispatch, nested
+  patterns, repeated-var-implies-eq). Built via `cons`/`list` rather than
+  quasiquote because SX's quasiquote does not recurse into lambda bodies — a
+  worth-knowing gotcha. 222/222 cumulative.
+- **2026-05-08** — **Phase 4 piece C — permuteo + inserto**: standard recursive
+  insert-at-any-position + permute-tail. 7 new tests, including all-6-perms-of-3
+  as a set check. 208/208 cumulative.
+- **2026-05-07** — **Phase 5 piece C — nafc**: `lib/minikanren/nafc.sx`. Three-line
+  primitive: stream-take 1; if empty, `(unit s)`, else `mzero`. 7 tests including
+  double-negation and use as a guard. 201/201 cumulative.
+- **2026-05-07** — **Phase 5 piece B — project**: `lib/minikanren/project.sx` —
+  defmacro that walks each named var, rebinds them, and runs the body's mk-conj.
+  Demonstrated escape into host arithmetic / string ops (`(* n n)`, `(str s "!")`).
+  Hygienic gensym'd s-param. 6 new tests, 194/194 cumulative.
+- **2026-05-07** — **Peano arithmetic** (`lib/minikanren/peano.sx`): zeroo, pluso,
+  minuso, lteo, lto, *o on Peano-encoded naturals (`:z` / `(:s n)`). pluso runs
+  forward, backward, and enumerates: `(run* q (fresh (a b) (pluso a b 3)
+  (== q (list a b))))` → all 4 pairs summing to 3. *o uses repeated pluso —
+  works for small inputs, slower for larger. 19 new tests, 188/188 cumulative.
+- **2026-05-07** — **Phase 5 piece A — conda**: soft-cut. Mirrors `condu` minus
+  the `onceo` on the head: all head answers are conjuncted through the rest of
+  the chosen clause. 7 new tests including the conda-vs-condu divergence test.
+  169/169 cumulative.
+- **2026-05-07** — **Phase 4 piece B — reverseo + lengtho**: reverseo runs forward
+  cleanly and `run 1`-cleanly backward; lengtho uses Peano-encoded lengths so it
+  works as a true relation in both directions (tests use the encoding directly).
+  10 new tests, 162/162 cumulative.
+- **2026-05-07** — **Phase 4 piece A — appendo canary green**: cons-cell support
+  in `unify.sx` + `(:s head tail)` lazy stream refactor in `stream.sx` + hygienic
+  `Zzz` (gensym'd subst-name) wrapping each `conde` clause + `lib/minikanren/
+  relations.sx` with `nullo` / `pairo` / `caro` / `cdro` / `conso` / `firsto` /
+  `resto` / `listo` / `appendo` / `membero`. 25 new tests in `tests/relations.sx`,
+  152/152 cumulative.
+  - **Three deep fixes shipped together**, all required to make `appendo`
+    terminate in both directions:
+    1. SX has no improper pairs, so a stream cell of mature subst + thunk
+       tail can't use `cons` — moved to a `(:s head tail)` tagged shape.
+    2. `(Zzz g)` wrapped its inner fn in a parameter named `s`, capturing
+       the user goal's own `s` binding (the `(appendo l s ls)` convention).
+       Replaced with `(gensym "zzz-s-")` for hygiene.
+    3. SX cons cells `(:cons h t)` for relational decomposition (so
+       `(conso a d l)` can split a list by head/tail without proper
+       improper pairs); `mk-walk*` re-flattens cons cells back to native
+       lists for clean reification output.
+- **2026-05-07** — **Phase 3 done** (run + reification): `lib/minikanren/run.sx` (~28 lines).
+  `reify`/`reify-s`/`reify-name` for canonical `_.N` rendering of unbound vars in
+  left-to-right occurrence order; `run*` / `run` / `run-n` defmacros. 18 new tests
+  in `tests/run.sx`, including the **first classic miniKanren tests green**:
+  `(run* q (== q 1))` → `(1)`; `(run* q (fresh (x y) (== q (list x y))))` →
+  `((_.0 _.1))`. 128/128 cumulative.
+- **2026-05-07** — **Phase 2 piece D + done** (`condu` / `onceo`): `lib/minikanren/condu.sx`.
+  Both are commitment forms: `onceo` is `(stream-take 1 ...)`; `condu` walks clauses
+  and commits the first one whose head produces an answer. 10 tests in `tests/condu.sx`,
+  110/110 cumulative. Phase 2 complete — ready for Phase 3 (run + reification).
+- **2026-05-07** — **Phase 2 piece C** (`conde`): `lib/minikanren/conde.sx` — single
+  defmacro folding clauses through `mk-disj` with internal `mk-conj`. 9 tests in
+  `tests/conde.sx`, 100/100 cumulative. Confirmed eager DFS ordering for ==-only
+  streams; true interleaving is a Phase 4 concern (paused thunks under recursion).
+- **2026-05-07** — **Phase 2 piece B** (`fresh`): `lib/minikanren/fresh.sx` (~10 lines).
+  defmacro form for nice user-facing syntax + `call-fresh` for programmatic use.
+  9 new tests in `tests/fresh.sx`, 91/91 cumulative.
+- **2026-05-07** — **Phase 2 piece A** (streams + ==/conj/disj): `lib/minikanren/stream.sx`
+  (mzero/unit/mk-mplus/mk-bind/stream-take, ~25 lines of code) + `lib/minikanren/goals.sx`
+  (succeed/fail/==/==-check/conj2/disj2/mk-conj/mk-disj, ~30 lines). Found and noted
+  a host-primitive name clash: `bind` is built in and silently shadows user defines —
+  must use `mk-bind`/`mk-mplus` etc. throughout. 34 tests in `tests/goals.sx`,
+  82/82 cumulative all green. fresh/conde/condu/onceo still pending.
+- **2026-05-07** — **Phase 1 done**: `lib/minikanren/unify.sx` (53 lines, ~22 lines of actual code) +
+  `lib/minikanren/tests/unify.sx` (48 tests, all green). Kit consumption: `walk-with`,
+  `unify-with`, `occurs-with`, `extend`, `empty-subst`, `mk-var`, `is-var?`, `var-name`
+  all supplied by `lib/guest/match.sx`. Local additions: a miniKanren-flavoured cfg
+  (treats native SX lists as cons-pairs via `:ctor-head = :pair`, occurs-check off),
+  `make-var` fresh-counter, deep `mk-walk*` (kit's `walk*` only recurses into `:ctor`
+  form, not native lists), and `mk-unify` / `mk-unify-check` thin wrappers. The kit
+  earns its keep ~3× over by line count — confirms lib-guest match kit is reusable
+  for logic-language hosts as designed.