GUEST-plan: deferred work shipped — pieces A B C D

Replace the single-pass body run with table-2-slg-iter / table-3-slg-iter:
each iteration stores the current vals in cache and re-runs the body;
loop until vals length stops growing. The cache thus grows
monotonically until no new answers appear.

For simple cycles (single tabled relation) this is sound and
terminating — len comparison is O(1) and the cache only grows.

Limitation: mutually-recursive tabled relations have INDEPENDENT
iteration loops. Each runs to its own fixed point in isolation; the
two don't coordinate. True SLG uses a worklist that cross-fires
re-iteration when any subgoal's cache grows. Left as a future
refinement.

All 5 SLG tests still pass (Fibonacci unchanged, 3 cyclic-patho
cases unchanged).

hosts/ocaml/lib/sx_primitives.ml

@@ -3124,6 +3124,108 @@ let () =
     | [String pat] -> List (List.map (fun s -> String s) (glob_paths pat))
     | _ -> raise (Eval_error "file-glob: (pattern)"));
 
+  (* === File metadata + ops (Phase 5d) === *)
+  let stat_or = function
+    | String path -> (try Some (Unix.stat path) with _ -> None)
+    | _ -> raise (Eval_error "file: path must be a string")
+  in
+  register "file-size" (fun args ->
+    match args with
+    | [v] -> (match stat_or v with Some s -> Integer s.Unix.st_size | None -> Integer 0)
+    | _ -> raise (Eval_error "file-size: (path)"));
+  register "file-mtime" (fun args ->
+    match args with
+    | [v] -> (match stat_or v with Some s -> Integer (int_of_float s.Unix.st_mtime) | None -> Integer 0)
+    | _ -> raise (Eval_error "file-mtime: (path)"));
+  register "file-isfile?" (fun args ->
+    match args with
+    | [v] -> (match stat_or v with Some s -> Bool (s.Unix.st_kind = Unix.S_REG) | None -> Bool false)
+    | _ -> raise (Eval_error "file-isfile?: (path)"));
+  register "file-isdir?" (fun args ->
+    match args with
+    | [v] -> (match stat_or v with Some s -> Bool (s.Unix.st_kind = Unix.S_DIR) | None -> Bool false)
+    | _ -> raise (Eval_error "file-isdir?: (path)"));
+  register "file-readable?" (fun args ->
+    match args with
+    | [String path] ->
+      Bool (try Unix.access path [Unix.R_OK]; true with _ -> false)
+    | _ -> raise (Eval_error "file-readable?: (path)"));
+  register "file-writable?" (fun args ->
+    match args with
+    | [String path] ->
+      Bool (try Unix.access path [Unix.W_OK]; true with _ -> false)
+    | _ -> raise (Eval_error "file-writable?: (path)"));
+  register "file-stat" (fun args ->
+    match args with
+    | [v] ->
+      (match stat_or v with
+       | None -> Nil
+       | Some s ->
+         let d = Hashtbl.create 6 in
+         Hashtbl.replace d "size" (Integer s.Unix.st_size);
+         Hashtbl.replace d "mtime" (Integer (int_of_float s.Unix.st_mtime));
+         Hashtbl.replace d "atime" (Integer (int_of_float s.Unix.st_atime));
+         Hashtbl.replace d "ctime" (Integer (int_of_float s.Unix.st_ctime));
+         Hashtbl.replace d "mode" (Integer s.Unix.st_perm);
+         Hashtbl.replace d "type" (String (match s.Unix.st_kind with
+           | Unix.S_REG -> "file" | Unix.S_DIR -> "directory"
+           | Unix.S_LNK -> "link" | Unix.S_CHR -> "characterSpecial"
+           | Unix.S_BLK -> "blockSpecial" | Unix.S_FIFO -> "fifo"
+           | Unix.S_SOCK -> "socket"));
+         Dict d)
+    | _ -> raise (Eval_error "file-stat: (path)"));
+  register "file-delete" (fun args ->
+    match args with
+    | [String path] ->
+      (try
+        if Sys.is_directory path then Unix.rmdir path
+        else Unix.unlink path
+      with
+      | Unix.Unix_error (Unix.ENOENT, _, _) -> ()  (* tolerate missing *)
+      | Unix.Unix_error (e, _, _) -> raise (Eval_error ("file-delete: " ^ Unix.error_message e)));
+      Nil
+    | _ -> raise (Eval_error "file-delete: (path)"));
+  register "file-mkdir" (fun args ->
+    match args with
+    | [String path] ->
+      let rec mk p =
+        if p = "" || p = "." || p = "/" then ()
+        else if Sys.file_exists p then ()
+        else begin
+          mk (Filename.dirname p);
+          (try Unix.mkdir p 0o755
+           with Unix.Unix_error (Unix.EEXIST, _, _) -> ())
+        end
+      in
+      (try mk path
+       with Unix.Unix_error (e, _, _) -> raise (Eval_error ("file-mkdir: " ^ Unix.error_message e)));
+      Nil
+    | _ -> raise (Eval_error "file-mkdir: (path)"));
+  register "file-copy" (fun args ->
+    match args with
+    | [String src; String dst] ->
+      (try
+        let ic = open_in_bin src in
+        let oc = open_out_bin dst in
+        let buf = Bytes.create 8192 in
+        let rec loop () =
+          let n = input ic buf 0 (Bytes.length buf) in
+          if n > 0 then (output oc buf 0 n; loop ())
+        in
+        loop ();
+        close_in ic;
+        close_out oc;
+        Nil
+      with
+      | Sys_error msg -> raise (Eval_error ("file-copy: " ^ msg)))
+    | _ -> raise (Eval_error "file-copy: (src dst)"));
+  register "file-rename" (fun args ->
+    match args with
+    | [String src; String dst] ->
+      (try Sys.rename src dst with Sys_error msg -> raise (Eval_error ("file-rename: " ^ msg)));
+      Nil
+    | _ -> raise (Eval_error "file-rename: (src dst)"));
+
   (* === Channels (random-access + blocking control) === *)
   let channel_table : (string, Unix.file_descr * string * bool ref * bool ref) Hashtbl.t = Hashtbl.create 16 in
   let channel_next_id = ref 0 in
@@ -3337,6 +3439,43 @@ let () =
       String name
     | _ -> raise (Eval_error "socket-connect: (host port)"));
 
+  (* Non-blocking connect: returns channel immediately. Connection completes
+     when the channel becomes writable; query channel-async-error? after to
+     confirm success or get the error. *)
+  register "socket-connect-async" (fun args ->
+    match args with
+    | [String host; port_v] ->
+      let port = port_of port_v in
+      let addr = Unix.ADDR_INET (resolve_inet_addr host, port) in
+      let sock = Unix.socket Unix.PF_INET Unix.SOCK_STREAM 0 in
+      Unix.set_nonblock sock;
+      (try Unix.connect sock addr
+       with
+       | Unix.Unix_error (Unix.EINPROGRESS, _, _)
+       | Unix.Unix_error (Unix.EWOULDBLOCK, _, _) -> ()
+       | Unix.Unix_error (e, _, _) ->
+         (try Unix.close sock with _ -> ());
+         raise (Eval_error ("socket-connect-async: " ^ Unix.error_message e)));
+      let name = alloc_chan_name () in
+      Hashtbl.replace channel_table name (sock, "rw", ref false, ref false);
+      String name
+    | _ -> raise (Eval_error "socket-connect-async: (host port)"));
+
+  (* After a non-blocking connect completes (channel writable), check whether
+     the connect succeeded. Returns "" on success, error message on failure. *)
+  register "channel-async-error" (fun args ->
+    match args with
+    | [String name] ->
+      let (fd, _, _, _) = chan_get name in
+      (try
+        let err = Unix.getsockopt_error fd in
+        match err with
+        | None -> String ""
+        | Some e -> String (Unix.error_message e)
+      with
+      | Unix.Unix_error (e, _, _) -> String (Unix.error_message e))
+    | _ -> raise (Eval_error "channel-async-error: (channel)"));
+
   register "socket-server" (fun args ->
     let (host, port) = match args with
       | [port_v] -> ("", port_of port_v)
@@ -3432,11 +3571,8 @@ let () =
     | [] -> Integer (int_of_float (Unix.gettimeofday () *. 1000.0))
     | _ -> raise (Eval_error "clock-milliseconds: no args"));
 
-  register "clock-format" (fun args ->
-    match args with
-    | [Integer t] | [Integer t; String _] ->
-      let fmt = (match args with [_; String f] -> f | _ -> "%a %b %e %H:%M:%S %Z %Y") in
-      let tm = Unix.gmtime (float_of_int t) in
+  let format_tm tm tz_label =
+    fun fmt ->
       let buf = Buffer.create 32 in
       let n = String.length fmt in
       let i = ref 0 in
@@ -3444,14 +3580,19 @@ let () =
         if fmt.[!i] = '%' && !i + 1 < n then begin
           (match fmt.[!i + 1] with
            | 'Y' -> Buffer.add_string buf (Printf.sprintf "%04d" (1900 + tm.Unix.tm_year))
+           | 'y' -> Buffer.add_string buf (Printf.sprintf "%02d" ((1900 + tm.Unix.tm_year) mod 100))
            | 'm' -> Buffer.add_string buf (Printf.sprintf "%02d" (tm.Unix.tm_mon + 1))
            | 'd' -> Buffer.add_string buf (Printf.sprintf "%02d" tm.Unix.tm_mday)
            | 'e' -> Buffer.add_string buf (Printf.sprintf "%2d"  tm.Unix.tm_mday)
            | 'H' -> Buffer.add_string buf (Printf.sprintf "%02d" tm.Unix.tm_hour)
+           | 'I' -> let h = tm.Unix.tm_hour mod 12 in
+                    Buffer.add_string buf (Printf.sprintf "%02d" (if h = 0 then 12 else h))
+           | 'p' -> Buffer.add_string buf (if tm.Unix.tm_hour < 12 then "AM" else "PM")
            | 'M' -> Buffer.add_string buf (Printf.sprintf "%02d" tm.Unix.tm_min)
            | 'S' -> Buffer.add_string buf (Printf.sprintf "%02d" tm.Unix.tm_sec)
            | 'j' -> Buffer.add_string buf (Printf.sprintf "%03d" (tm.Unix.tm_yday + 1))
-           | 'Z' -> Buffer.add_string buf "UTC"
+           | 'w' -> Buffer.add_string buf (string_of_int tm.Unix.tm_wday)
+           | 'Z' -> Buffer.add_string buf tz_label
            | 'a' -> let days = [|"Sun";"Mon";"Tue";"Wed";"Thu";"Fri";"Sat"|] in
                     Buffer.add_string buf days.(tm.Unix.tm_wday)
            | 'A' -> let days = [|"Sunday";"Monday";"Tuesday";"Wednesday";"Thursday";"Friday";"Saturday"|] in
@@ -3460,6 +3601,7 @@ let () =
                     Buffer.add_string buf mons.(tm.Unix.tm_mon)
            | 'B' -> let mons = [|"January";"February";"March";"April";"May";"June";"July";"August";"September";"October";"November";"December"|] in
                     Buffer.add_string buf mons.(tm.Unix.tm_mon)
+           | '%' -> Buffer.add_char buf '%'
            | c -> Buffer.add_char buf '%'; Buffer.add_char buf c);
           i := !i + 2
         end else begin
@@ -3467,8 +3609,100 @@ let () =
           incr i
         end
       done;
-      String (Buffer.contents buf)
-    | _ -> raise (Eval_error "clock-format: (seconds [format])"));
+      Buffer.contents buf
+  in
+  register "clock-format" (fun args ->
+    let (t, fmt, tz) = match args with
+      | [Integer t] -> (t, "%a %b %e %H:%M:%S %Z %Y", "utc")
+      | [Integer t; String f] -> (t, f, "utc")
+      | [Integer t; String f; String z] -> (t, f, z)
+      | _ -> raise (Eval_error "clock-format: (seconds [format [tz]])")
+    in
+    let tm =
+      if tz = "local" then Unix.localtime (float_of_int t)
+      else Unix.gmtime (float_of_int t)
+    in
+    let label = if tz = "local" then "" else "UTC" in
+    String (format_tm tm label fmt));
+
+  (* clock-scan: parse a date string with format, return seconds.
+     Supports the same format specifiers as clock-format (fixed-width ones).
+     tz: "utc" (default) or "local". *)
+  let timegm (tm : Unix.tm) =
+    let is_leap y = y mod 4 = 0 && (y mod 100 <> 0 || y mod 400 = 0) in
+    let days_in_month = [|31;28;31;30;31;30;31;31;30;31;30;31|] in
+    let year = tm.Unix.tm_year + 1900 in
+    let mon = tm.Unix.tm_mon in
+    let mday = tm.Unix.tm_mday in
+    let total_days = ref 0 in
+    if year >= 1970 then begin
+      for y = 1970 to year - 1 do
+        total_days := !total_days + (if is_leap y then 366 else 365)
+      done
+    end else begin
+      for y = year to 1969 do
+        total_days := !total_days - (if is_leap y then 366 else 365)
+      done
+    end;
+    for m = 0 to mon - 1 do
+      total_days := !total_days + days_in_month.(m);
+      if m = 1 && is_leap year then incr total_days
+    done;
+    total_days := !total_days + mday - 1;
+    !total_days * 86400
+    + tm.Unix.tm_hour * 3600
+    + tm.Unix.tm_min * 60
+    + tm.Unix.tm_sec
+  in
+  register "clock-scan" (fun args ->
+    let (str, fmt, tz) = match args with
+      | [String s; String f] -> (s, f, "utc")
+      | [String s; String f; String z] -> (s, f, z)
+      | _ -> raise (Eval_error "clock-scan: (str fmt [tz])")
+    in
+    let n = String.length fmt and sn = String.length str in
+    let tm = ref { Unix.tm_year = 70; tm_mon = 0; tm_mday = 1;
+                   tm_hour = 0; tm_min = 0; tm_sec = 0;
+                   tm_wday = 0; tm_yday = 0; tm_isdst = false } in
+    let i = ref 0 and j = ref 0 in
+    let read_n_digits k =
+      let s = ref "" in
+      let cnt = ref 0 in
+      while !cnt < k && !j < sn && str.[!j] >= '0' && str.[!j] <= '9' do
+        s := !s ^ String.make 1 str.[!j];
+        incr j; incr cnt
+      done;
+      if !s = "" then 0 else int_of_string !s
+    in
+    let skip_ws () =
+      while !j < sn && (str.[!j] = ' ' || str.[!j] = '\t') do incr j done
+    in
+    while !i < n do
+      if fmt.[!i] = '%' && !i + 1 < n then begin
+        (match fmt.[!i + 1] with
+         | 'Y' -> tm := { !tm with tm_year = read_n_digits 4 - 1900 }
+         | 'y' -> let y = read_n_digits 2 in
+                  tm := { !tm with tm_year = (if y < 70 then 100 + y else y) }
+         | 'm' -> tm := { !tm with tm_mon = read_n_digits 2 - 1 }
+         | 'd' | 'e' -> skip_ws (); tm := { !tm with tm_mday = read_n_digits 2 }
+         | 'H' | 'I' -> tm := { !tm with tm_hour = read_n_digits 2 }
+         | 'M' -> tm := { !tm with tm_min = read_n_digits 2 }
+         | 'S' -> tm := { !tm with tm_sec = read_n_digits 2 }
+         | '%' -> if !j < sn && str.[!j] = '%' then incr j
+         | _ -> ()  (* unsupported specifier — skip *)
+        );
+        i := !i + 2
+      end else begin
+        if fmt.[!i] = ' ' then skip_ws ()
+        else if !j < sn && str.[!j] = fmt.[!i] then incr j;
+        incr i
+      end
+    done;
+    let secs =
+      if tz = "local" then int_of_float (fst (Unix.mktime !tm))
+      else timegm !tm
+    in
+    Integer secs);
 
   (* === Env-as-value (Phase 4) === *)
 

lib/guest/ast.sx

@@ -0,0 +1,92 @@
+;; lib/guest/ast.sx — canonical AST node shapes.
+;;
+;; A guest's parser may emit its own AST in whatever shape is convenient
+;; for that language's evaluator/transpiler. This file gives a SHARED
+;; canonical shape that cross-language tools (formatters, highlighters,
+;; debuggers) can target without per-language adapters.
+;;
+;; Each canonical node is a tagged list: (KIND ...payload).
+;;
+;; Constructors (return a canonical node):
+;;
+;;   (ast-literal       VALUE)               — number / string / bool / nil
+;;   (ast-var           NAME)                — identifier reference
+;;   (ast-app           FN ARGS)             — function application
+;;   (ast-lambda        PARAMS BODY)         — anonymous function
+;;   (ast-let           BINDINGS BODY)       — local bindings
+;;   (ast-letrec        BINDINGS BODY)       — recursive local bindings
+;;   (ast-if            TEST THEN ELSE)      — conditional
+;;   (ast-match-clause  PATTERN BODY)        — one match arm
+;;   (ast-module        NAME BODY)           — module declaration
+;;   (ast-import        NAME)                — import directive
+;;
+;; Predicates: (ast-literal? X), (ast-var? X), …
+;; Generic:    (ast? X)         — any canonical node
+;;             (ast-kind X)     — :literal / :var / :app / …
+;;
+;; Accessors  (one per payload field):
+;;   (ast-literal-value N)
+;;   (ast-var-name N)
+;;   (ast-app-fn N)             (ast-app-args N)
+;;   (ast-lambda-params N)      (ast-lambda-body N)
+;;   (ast-let-bindings N)       (ast-let-body N)
+;;   (ast-letrec-bindings N)    (ast-letrec-body N)
+;;   (ast-if-test N)            (ast-if-then N)         (ast-if-else N)
+;;   (ast-match-clause-pattern N)
+;;   (ast-match-clause-body N)
+;;   (ast-module-name N)        (ast-module-body N)
+;;   (ast-import-name N)
+
+(define ast-literal      (fn (v)         (list :literal v)))
+(define ast-var          (fn (n)         (list :var n)))
+(define ast-app          (fn (f args)    (list :app f args)))
+(define ast-lambda       (fn (ps body)   (list :lambda ps body)))
+(define ast-let          (fn (bs body)   (list :let bs body)))
+(define ast-letrec       (fn (bs body)   (list :letrec bs body)))
+(define ast-if           (fn (t th el)   (list :if t th el)))
+(define ast-match-clause (fn (p body)    (list :match-clause p body)))
+(define ast-module       (fn (n body)    (list :module n body)))
+(define ast-import       (fn (n)         (list :import n)))
+
+(define ast-kind (fn (x) (if (and (list? x) (not (empty? x))) (first x) nil)))
+
+(define
+  ast?
+  (fn (x)
+    (and (list? x)
+         (not (empty? x))
+         (let ((k (first x)))
+           (or (= k :literal) (= k :var) (= k :app)
+               (= k :lambda)  (= k :let) (= k :letrec)
+               (= k :if)      (= k :match-clause)
+               (= k :module)  (= k :import))))))
+
+(define ast-literal?      (fn (x) (and (ast? x) (= (first x) :literal))))
+(define ast-var?          (fn (x) (and (ast? x) (= (first x) :var))))
+(define ast-app?          (fn (x) (and (ast? x) (= (first x) :app))))
+(define ast-lambda?       (fn (x) (and (ast? x) (= (first x) :lambda))))
+(define ast-let?          (fn (x) (and (ast? x) (= (first x) :let))))
+(define ast-letrec?       (fn (x) (and (ast? x) (= (first x) :letrec))))
+(define ast-if?           (fn (x) (and (ast? x) (= (first x) :if))))
+(define ast-match-clause? (fn (x) (and (ast? x) (= (first x) :match-clause))))
+(define ast-module?       (fn (x) (and (ast? x) (= (first x) :module))))
+(define ast-import?       (fn (x) (and (ast? x) (= (first x) :import))))
+
+(define ast-literal-value (fn (n) (nth n 1)))
+(define ast-var-name      (fn (n) (nth n 1)))
+(define ast-app-fn        (fn (n) (nth n 1)))
+(define ast-app-args      (fn (n) (nth n 2)))
+(define ast-lambda-params (fn (n) (nth n 1)))
+(define ast-lambda-body   (fn (n) (nth n 2)))
+(define ast-let-bindings  (fn (n) (nth n 1)))
+(define ast-let-body      (fn (n) (nth n 2)))
+(define ast-letrec-bindings (fn (n) (nth n 1)))
+(define ast-letrec-body     (fn (n) (nth n 2)))
+(define ast-if-test       (fn (n) (nth n 1)))
+(define ast-if-then       (fn (n) (nth n 2)))
+(define ast-if-else       (fn (n) (nth n 3)))
+(define ast-match-clause-pattern (fn (n) (nth n 1)))
+(define ast-match-clause-body    (fn (n) (nth n 2)))
+(define ast-module-name   (fn (n) (nth n 1)))
+(define ast-module-body   (fn (n) (nth n 2)))
+(define ast-import-name   (fn (n) (nth n 1)))

lib/guest/match.sx

@@ -0,0 +1,185 @@
+;; lib/guest/match.sx — pure pattern-match + unification kit.
+;;
+;; Shipped for miniKanren / Datalog / future logic-flavoured guests that
+;; want immutable unification without writing it from scratch. The two
+;; existing prolog/haskell engines stay as-is — porting them in place
+;; risks the 746 tests they currently pass; consumers can migrate
+;; gradually via the converters in lib/guest/ast.sx.
+;;
+;; Term shapes (canonical wire format)
+;; -----------------------------------
+;;   var          (:var NAME)            NAME a string
+;;   constructor  (:ctor HEAD ARGS)      HEAD a string, ARGS a list of terms
+;;   literal      number / string / boolean / nil
+;;
+;; Guests with their own shape pass adapter callbacks via the cfg arg —
+;; see (unify-with cfg ...) and (match-pat-with cfg ...) below. The
+;; default canonical entry points (unify / match-pat) use the wire shape.
+;;
+;; Substitution / env
+;; ------------------
+;; A substitution is a SX dict mapping VAR-NAME → term. There are no
+;; trails, no mutation: each step either returns an extended dict or nil.
+;;
+;;   (empty-subst)                  → {}
+;;   (walk term s)                  → term with top-level vars resolved
+;;   (walk* term s)                 → term with all vars resolved (recursive)
+;;   (extend name term s)           → s with NAME → term added
+;;   (occurs? name term s)          → bool
+;;
+;; Unify (symmetric, miniKanren-flavour)
+;; -------------------------------------
+;;   (unify u v s)                  → extended subst or nil
+;;   (unify-with cfg u v s)         → ditto, with adapter callbacks:
+;;                                      :var? :var-name :ctor? :ctor-head
+;;                                      :ctor-args :occurs-check?
+;;
+;; Match (asymmetric, haskell-flavour: pattern → value, vars only in pat)
+;; ---------------------------------------------------------------------
+;;   (match-pat pat val env)        → extended env or nil
+;;   (match-pat-with cfg pat val env)
+
+(define mk-var  (fn (name) (list :var name)))
+(define mk-ctor (fn (head args) (list :ctor head args)))
+
+(define is-var?    (fn (t) (and (list? t) (not (empty? t)) (= (first t) :var))))
+(define is-ctor?   (fn (t) (and (list? t) (not (empty? t)) (= (first t) :ctor))))
+(define var-name   (fn (t) (nth t 1)))
+(define ctor-head  (fn (t) (nth t 1)))
+(define ctor-args  (fn (t) (nth t 2)))
+
+(define empty-subst (fn () {}))
+
+(define
+  walk
+  (fn (t s)
+    (if (and (is-var? t) (has-key? s (var-name t)))
+      (walk (get s (var-name t)) s)
+      t)))
+
+(define
+  walk*
+  (fn (t s)
+    (let ((w (walk t s)))
+      (cond
+        ((is-ctor? w)
+          (mk-ctor (ctor-head w) (map (fn (a) (walk* a s)) (ctor-args w))))
+        (:else w)))))
+
+(define
+  extend
+  (fn (name term s)
+    (assoc s name term)))
+
+(define
+  occurs?
+  (fn (name term s)
+    (let ((w (walk term s)))
+      (cond
+        ((is-var? w) (= (var-name w) name))
+        ((is-ctor? w) (some (fn (a) (occurs? name a s)) (ctor-args w)))
+        (:else false)))))
+
+(define
+  unify-with
+  (fn (cfg u v s)
+    (let ((var?-fn (get cfg :var?))
+          (var-name-fn (get cfg :var-name))
+          (ctor?-fn (get cfg :ctor?))
+          (ctor-head-fn (get cfg :ctor-head))
+          (ctor-args-fn (get cfg :ctor-args))
+          (occurs?-on (get cfg :occurs-check?)))
+      (let ((wu (walk-with cfg u s))
+            (wv (walk-with cfg v s)))
+        (cond
+          ((and (var?-fn wu) (var?-fn wv) (= (var-name-fn wu) (var-name-fn wv))) s)
+          ((var?-fn wu)
+            (if (and occurs?-on (occurs-with cfg (var-name-fn wu) wv s))
+              nil
+              (extend (var-name-fn wu) wv s)))
+          ((var?-fn wv)
+            (if (and occurs?-on (occurs-with cfg (var-name-fn wv) wu s))
+              nil
+              (extend (var-name-fn wv) wu s)))
+          ((and (ctor?-fn wu) (ctor?-fn wv))
+            (if (= (ctor-head-fn wu) (ctor-head-fn wv))
+              (unify-list-with
+                cfg
+                (ctor-args-fn wu)
+                (ctor-args-fn wv)
+                s)
+              nil))
+          (:else (if (= wu wv) s nil)))))))
+
+(define
+  walk-with
+  (fn (cfg t s)
+    (if (and ((get cfg :var?) t) (has-key? s ((get cfg :var-name) t)))
+      (walk-with cfg (get s ((get cfg :var-name) t)) s)
+      t)))
+
+(define
+  occurs-with
+  (fn (cfg name term s)
+    (let ((w (walk-with cfg term s)))
+      (cond
+        (((get cfg :var?) w) (= ((get cfg :var-name) w) name))
+        (((get cfg :ctor?) w)
+          (some (fn (a) (occurs-with cfg name a s)) ((get cfg :ctor-args) w)))
+        (:else false)))))
+
+(define
+  unify-list-with
+  (fn (cfg xs ys s)
+    (cond
+      ((and (empty? xs) (empty? ys)) s)
+      ((or (empty? xs) (empty? ys)) nil)
+      (:else
+        (let ((s2 (unify-with cfg (first xs) (first ys) s)))
+          (if (= s2 nil)
+            nil
+            (unify-list-with cfg (rest xs) (rest ys) s2)))))))
+
+(define canonical-cfg
+  {:var? is-var? :var-name var-name
+   :ctor? is-ctor? :ctor-head ctor-head :ctor-args ctor-args
+   :occurs-check? true})
+
+(define unify (fn (u v s) (unify-with canonical-cfg u v s)))
+
+;; Asymmetric pattern match (haskell-style): only patterns may contain vars;
+;; values are concrete. On a var pattern, bind name to value.
+(define
+  match-pat-with
+  (fn (cfg pat val env)
+    (let ((var?-fn (get cfg :var?))
+          (var-name-fn (get cfg :var-name))
+          (ctor?-fn (get cfg :ctor?))
+          (ctor-head-fn (get cfg :ctor-head))
+          (ctor-args-fn (get cfg :ctor-args)))
+      (cond
+        ((var?-fn pat) (extend (var-name-fn pat) val env))
+        ((and (ctor?-fn pat) (ctor?-fn val))
+          (if (= (ctor-head-fn pat) (ctor-head-fn val))
+            (match-list-pat-with
+              cfg
+              (ctor-args-fn pat)
+              (ctor-args-fn val)
+              env)
+            nil))
+        ((ctor?-fn pat) nil)
+        (:else (if (= pat val) env nil))))))
+
+(define
+  match-list-pat-with
+  (fn (cfg pats vals env)
+    (cond
+      ((and (empty? pats) (empty? vals)) env)
+      ((or (empty? pats) (empty? vals)) nil)
+      (:else
+        (let ((env2 (match-pat-with cfg (first pats) (first vals) env)))
+          (if (= env2 nil)
+            nil
+            (match-list-pat-with cfg (rest pats) (rest vals) env2)))))))
+
+(define match-pat (fn (pat val env) (match-pat-with canonical-cfg pat val env)))

lib/guest/pratt.sx

@@ -0,0 +1,28 @@
+;; lib/guest/pratt.sx — operator-table format + lookup for Pratt-style
+;; precedence climbing.
+;;
+;; The climbing loop stays per-language because the two canaries use
+;; opposite conventions (Lua: higher prec = tighter; Prolog: lower prec =
+;; tighter, with xfx/xfy/yfx assoc tags). Forcing a single loop adds
+;; callback indirection that obscures more than it shares.
+;;
+;; What IS shared and gets extracted: the operator-table format and lookup.
+;; "Grammar is a dict, not hardcoded cond."
+;;
+;; Entry shape: (NAME PREC ASSOC).
+;;   NAME   — string, the operator's source token.
+;;   PREC   — integer, in the host's own convention.
+;;   ASSOC  — :left | :right | :none for languages with traditional
+;;            associativity, or "xfx" / "xfy" / "yfx" for Prolog-style.
+
+(define
+  pratt-op-lookup
+  (fn (table name)
+    (cond
+      ((empty? table) nil)
+      ((= (first (first table)) name) (first table))
+      (:else (pratt-op-lookup (rest table) name)))))
+
+(define pratt-op-name  (fn (entry) (first entry)))
+(define pratt-op-prec  (fn (entry) (nth entry 1)))
+(define pratt-op-assoc (fn (entry) (nth entry 2)))

lib/guest/tests/ast.sx

@@ -0,0 +1,63 @@
+;; lib/guest/tests/ast.sx — exercises every constructor / predicate /
+;; accessor in lib/guest/ast.sx so future ports have a stable contract
+;; to point at.
+
+(define gast-test-pass 0)
+(define gast-test-fail 0)
+(define gast-test-fails (list))
+
+(define
+  gast-test
+  (fn (name actual expected)
+    (if (= actual expected)
+      (set! gast-test-pass (+ gast-test-pass 1))
+      (begin
+        (set! gast-test-fail (+ gast-test-fail 1))
+        (append! gast-test-fails {:name name :expected expected :actual actual})))))
+
+;; Constructors round-trip.
+(gast-test "literal-int"    (ast-literal-value (ast-literal 42)) 42)
+(gast-test "literal-str"    (ast-literal-value (ast-literal "hi")) "hi")
+(gast-test "literal-bool"   (ast-literal-value (ast-literal true)) true)
+(gast-test "var-name"       (ast-var-name (ast-var "x")) "x")
+(gast-test "app-fn"         (ast-app-fn (ast-app (ast-var "f") (list (ast-literal 1)))) (ast-var "f"))
+(gast-test "app-args-len"   (len (ast-app-args (ast-app (ast-var "f") (list (ast-literal 1))))) 1)
+(gast-test "lambda-params"  (ast-lambda-params (ast-lambda (list "x" "y") (ast-var "x"))) (list "x" "y"))
+(gast-test "lambda-body"    (ast-lambda-body (ast-lambda (list "x") (ast-var "x"))) (ast-var "x"))
+(gast-test "let-bindings"   (len (ast-let-bindings (ast-let (list {:name "x" :value (ast-literal 1)}) (ast-var "x")))) 1)
+(gast-test "letrec-body"    (ast-letrec-body (ast-letrec (list) (ast-literal 0))) (ast-literal 0))
+(gast-test "if-test"        (ast-if-test (ast-if (ast-literal true) (ast-literal 1) (ast-literal 0))) (ast-literal true))
+(gast-test "if-then"        (ast-if-then (ast-if (ast-literal true) (ast-literal 1) (ast-literal 0))) (ast-literal 1))
+(gast-test "if-else"        (ast-if-else (ast-if (ast-literal true) (ast-literal 1) (ast-literal 0))) (ast-literal 0))
+(gast-test "match-pattern"  (ast-match-clause-pattern (ast-match-clause "P" (ast-literal 1))) "P")
+(gast-test "match-body"     (ast-match-clause-body (ast-match-clause "P" (ast-literal 1))) (ast-literal 1))
+(gast-test "module-name"    (ast-module-name (ast-module "m" (list))) "m")
+(gast-test "import-name"    (ast-import-name (ast-import "lib/foo")) "lib/foo")
+
+;; Predicates fire only on matching kinds.
+(gast-test "is-literal"     (ast-literal? (ast-literal 1)) true)
+(gast-test "not-literal"    (ast-literal? (ast-var "x")) false)
+(gast-test "is-var"         (ast-var? (ast-var "x")) true)
+(gast-test "is-app"         (ast-app? (ast-app (ast-var "f") (list))) true)
+(gast-test "is-lambda"      (ast-lambda? (ast-lambda (list) (ast-literal 0))) true)
+(gast-test "is-let"         (ast-let? (ast-let (list) (ast-literal 0))) true)
+(gast-test "is-letrec"      (ast-letrec? (ast-letrec (list) (ast-literal 0))) true)
+(gast-test "is-if"          (ast-if? (ast-if (ast-literal true) (ast-literal 1) (ast-literal 0))) true)
+(gast-test "is-match"       (ast-match-clause? (ast-match-clause "P" (ast-literal 1))) true)
+(gast-test "is-module"      (ast-module? (ast-module "m" (list))) true)
+(gast-test "is-import"      (ast-import? (ast-import "x")) true)
+
+;; ast? recognises any canonical node.
+(gast-test "ast?-literal"   (ast? (ast-literal 0)) true)
+(gast-test "ast?-foreign"   (ast? (list "lua-num" 0)) false)
+(gast-test "ast?-non-list"  (ast? 42) false)
+
+;; ast-kind dispatch.
+(gast-test "kind-literal"   (ast-kind (ast-literal 0)) :literal)
+(gast-test "kind-import"    (ast-kind (ast-import "x")) :import)
+
+(define gast-tests-run!
+  (fn ()
+    {:passed gast-test-pass
+     :failed gast-test-fail
+     :total  (+ gast-test-pass gast-test-fail)}))

lib/guest/tests/match.sx

@@ -0,0 +1,108 @@
+;; lib/guest/tests/match.sx — exercises lib/guest/match.sx.
+
+(define gmatch-test-pass 0)
+(define gmatch-test-fail 0)
+(define gmatch-test-fails (list))
+
+(define
+  gmatch-test
+  (fn (name actual expected)
+    (if (= actual expected)
+      (set! gmatch-test-pass (+ gmatch-test-pass 1))
+      (begin
+        (set! gmatch-test-fail (+ gmatch-test-fail 1))
+        (append! gmatch-test-fails {:name name :expected expected :actual actual})))))
+
+;; ── walk / extend / occurs ────────────────────────────────────────
+(gmatch-test "walk-direct"
+  (walk (mk-var "x") (extend "x" 5 (empty-subst))) 5)
+
+(gmatch-test "walk-chain"
+  (walk (mk-var "a") (extend "a" (mk-var "b") (extend "b" 7 (empty-subst)))) 7)
+
+(gmatch-test "walk-no-binding"
+  (let ((v (mk-var "u"))) (= (walk v (empty-subst)) v)) true)
+
+(gmatch-test "walk*-recursive"
+  (walk* (mk-ctor "Just" (list (mk-var "x"))) (extend "x" 9 (empty-subst)))
+  (mk-ctor "Just" (list 9)))
+
+(gmatch-test "occurs-direct"
+  (occurs? "x" (mk-var "x") (empty-subst)) true)
+
+(gmatch-test "occurs-nested"
+  (occurs? "x" (mk-ctor "f" (list (mk-var "x"))) (empty-subst)) true)
+
+(gmatch-test "occurs-not"
+  (occurs? "x" (mk-var "y") (empty-subst)) false)
+
+;; ── unify (symmetric) ─────────────────────────────────────────────
+(gmatch-test "unify-equal-literals"
+  (len (unify 5 5 (empty-subst))) 0)
+
+(gmatch-test "unify-different-literals"
+  (unify 5 6 (empty-subst)) nil)
+
+(gmatch-test "unify-var-literal"
+  (get (unify (mk-var "x") 5 (empty-subst)) "x") 5)
+
+(gmatch-test "unify-literal-var"
+  (get (unify 5 (mk-var "x") (empty-subst)) "x") 5)
+
+(gmatch-test "unify-same-var"
+  (len (unify (mk-var "x") (mk-var "x") (empty-subst))) 0)
+
+(gmatch-test "unify-two-vars"
+  (let ((s (unify (mk-var "x") (mk-var "y") (empty-subst))))
+    (or (= (get s "x") (mk-var "y")) (= (get s "y") (mk-var "x")))) true)
+
+(gmatch-test "unify-ctor-equal"
+  (len (unify (mk-ctor "f" (list 1 2)) (mk-ctor "f" (list 1 2)) (empty-subst))) 0)
+
+(gmatch-test "unify-ctor-with-var"
+  (get (unify (mk-ctor "Just" (list (mk-var "x"))) (mk-ctor "Just" (list 7)) (empty-subst)) "x") 7)
+
+(gmatch-test "unify-ctor-head-mismatch"
+  (unify (mk-ctor "Just" (list 1)) (mk-ctor "Nothing" (list)) (empty-subst)) nil)
+
+(gmatch-test "unify-ctor-arity-mismatch"
+  (unify (mk-ctor "f" (list 1 2)) (mk-ctor "f" (list 1)) (empty-subst)) nil)
+
+(gmatch-test "unify-occurs-check"
+  (unify (mk-var "x") (mk-ctor "f" (list (mk-var "x"))) (empty-subst)) nil)
+
+(gmatch-test "unify-transitive-vars"
+  (let ((s (unify (mk-var "x") (mk-var "y") (empty-subst))))
+    (let ((s2 (unify (mk-var "y") 42 s)))
+      (walk (mk-var "x") s2))) 42)
+
+;; ── match-pat (asymmetric) ────────────────────────────────────────
+(gmatch-test "match-var-binds"
+  (get (match-pat (mk-var "x") 99 (empty-subst)) "x") 99)
+
+(gmatch-test "match-literal-equal"
+  (len (match-pat 5 5 (empty-subst))) 0)
+
+(gmatch-test "match-literal-mismatch"
+  (match-pat 5 6 (empty-subst)) nil)
+
+(gmatch-test "match-ctor-binds"
+  (get (match-pat (mk-ctor "Just" (list (mk-var "y")))
+                  (mk-ctor "Just" (list 11))
+                  (empty-subst)) "y") 11)
+
+(gmatch-test "match-ctor-head-mismatch"
+  (match-pat (mk-ctor "Just" (list (mk-var "y")))
+             (mk-ctor "Nothing" (list))
+             (empty-subst)) nil)
+
+(gmatch-test "match-ctor-arity-mismatch"
+  (match-pat (mk-ctor "f" (list (mk-var "x") (mk-var "y")))
+             (mk-ctor "f" (list 1))
+             (empty-subst)) nil)
+
+(define gmatch-tests-run!
+  (fn ()
+    {:passed gmatch-test-pass
+     :failed gmatch-test-fail
+     :total  (+ gmatch-test-pass gmatch-test-fail)}))

lib/lua/parser.sx

@@ -3,28 +3,33 @@
 (define lua-tok-value (fn (t) (if (= t nil) nil (get t :value))))
 
 (define
-  lua-binop-prec
-  (fn
-    (op)
-    (cond
-      ((= op "or") 1)
-      ((= op "and") 2)
-      ((= op "<") 3)
-      ((= op ">") 3)
-      ((= op "<=") 3)
-      ((= op ">=") 3)
-      ((= op "==") 3)
-      ((= op "~=") 3)
-      ((= op "..") 5)
-      ((= op "+") 6)
-      ((= op "-") 6)
-      ((= op "*") 7)
-      ((= op "/") 7)
-      ((= op "%") 7)
-      ((= op "^") 10)
-      (else 0))))
+  lua-op-table
+  (list
+    (list "or"  1 :left)
+    (list "and" 2 :left)
+    (list "<"   3 :left)
+    (list ">"   3 :left)
+    (list "<="  3 :left)
+    (list ">="  3 :left)
+    (list "=="  3 :left)
+    (list "~="  3 :left)
+    (list ".."  5 :right)
+    (list "+"   6 :left)
+    (list "-"   6 :left)
+    (list "*"   7 :left)
+    (list "/"   7 :left)
+    (list "%"   7 :left)
+    (list "^"  10 :right)))
 
-(define lua-binop-right? (fn (op) (or (= op "..") (= op "^"))))
+(define lua-binop-prec
+  (fn (op)
+    (let ((entry (pratt-op-lookup lua-op-table op)))
+      (if (= entry nil) 0 (pratt-op-prec entry)))))
+
+(define lua-binop-right?
+  (fn (op)
+    (let ((entry (pratt-op-lookup lua-op-table op)))
+      (and (not (= entry nil)) (= (pratt-op-assoc entry) :right)))))
 
 (define
   lua-parse

lib/lua/test.sh

@@ -30,6 +30,7 @@ cat > "$TMPFILE" << 'EPOCHS'
 (epoch 1)
 (load "lib/guest/lex.sx")
 (load "lib/guest/prefix.sx")
+(load "lib/guest/pratt.sx")
 (load "lib/lua/tokenizer.sx")
 (epoch 2)
 (load "lib/lua/parser.sx")

lib/minikanren/clpfd.sx

@@ -0,0 +1,858 @@
+;; lib/minikanren/clpfd.sx — Phase 6: native CLP(FD) on miniKanren.
+;;
+;; The substitution dict carries an extra reserved key "_fd" that holds a
+;; constraint-store record:
+;;
+;;   {:domains    {var-name -> sorted-int-list}
+;;    :constraints (... pending constraint closures ...)}
+;;
+;; Domains are sorted SX lists of ints (no duplicates).
+;; Constraints are functions s -> s-or-nil that propagate / re-check.
+;; They are re-fired after every label binding via fd-fire-store.
+
+(define fd-key "_fd")
+
+;; --- domain primitives ---
+
+(define
+  fd-dom-rev
+  (fn
+    (xs acc)
+    (cond
+      ((empty? xs) acc)
+      (:else (fd-dom-rev (rest xs) (cons (first xs) acc))))))
+
+(define
+  fd-dom-insert
+  (fn
+    (x desc)
+    (cond
+      ((empty? desc) (list x))
+      ((= x (first desc)) desc)
+      ((> x (first desc)) (cons x desc))
+      (:else (cons (first desc) (fd-dom-insert x (rest desc)))))))
+
+(define
+  fd-dom-sort-dedupe
+  (fn
+    (xs acc)
+    (cond
+      ((empty? xs) (fd-dom-rev acc (list)))
+      (:else (fd-dom-sort-dedupe (rest xs) (fd-dom-insert (first xs) acc))))))
+
+(define fd-dom-from-list (fn (xs) (fd-dom-sort-dedupe xs (list))))
+
+(define fd-dom-empty? (fn (d) (empty? d)))
+(define
+  fd-dom-singleton?
+  (fn (d) (and (not (empty? d)) (empty? (rest d)))))
+(define fd-dom-min (fn (d) (first d)))
+
+(define
+  fd-dom-last
+  (fn
+    (d)
+    (cond ((empty? (rest d)) (first d)) (:else (fd-dom-last (rest d))))))
+
+(define fd-dom-max (fn (d) (fd-dom-last d)))
+(define fd-dom-member? (fn (x d) (some (fn (y) (= x y)) d)))
+
+(define
+  fd-dom-intersect
+  (fn
+    (a b)
+    (cond
+      ((empty? a) (list))
+      ((empty? b) (list))
+      ((= (first a) (first b))
+        (cons (first a) (fd-dom-intersect (rest a) (rest b))))
+      ((< (first a) (first b)) (fd-dom-intersect (rest a) b))
+      (:else (fd-dom-intersect a (rest b))))))
+
+(define
+  fd-dom-without
+  (fn
+    (x d)
+    (cond
+      ((empty? d) (list))
+      ((= (first d) x) (rest d))
+      ((> (first d) x) d)
+      (:else (cons (first d) (fd-dom-without x (rest d)))))))
+
+(define
+  fd-dom-range
+  (fn
+    (lo hi)
+    (cond
+      ((> lo hi) (list))
+      (:else (cons lo (fd-dom-range (+ lo 1) hi))))))
+
+;; --- constraint store accessors ---
+
+(define fd-store-empty (fn () {:domains {} :constraints (list)}))
+
+(define
+  fd-store-of
+  (fn
+    (s)
+    (cond ((has-key? s fd-key) (get s fd-key)) (:else (fd-store-empty)))))
+
+(define fd-domains-of (fn (s) (get (fd-store-of s) :domains)))
+(define fd-with-store (fn (s store) (assoc s fd-key store)))
+
+(define
+  fd-domain-of
+  (fn
+    (s var-name)
+    (let
+      ((doms (fd-domains-of s)))
+      (cond ((has-key? doms var-name) (get doms var-name)) (:else nil)))))
+
+(define
+  fd-set-domain
+  (fn
+    (s var-name d)
+    (cond
+      ((fd-dom-empty? d) nil)
+      (:else
+        (let
+          ((store (fd-store-of s)))
+          (let
+            ((doms-prime (assoc (get store :domains) var-name d)))
+            (let
+              ((store-prime (assoc store :domains doms-prime)))
+              (fd-with-store s store-prime))))))))
+
+(define
+  fd-add-constraint
+  (fn
+    (s c)
+    (let
+      ((store (fd-store-of s)))
+      (let
+        ((cs-prime (cons c (get store :constraints))))
+        (let
+          ((store-prime (assoc store :constraints cs-prime)))
+          (fd-with-store s store-prime))))))
+
+(define
+  fd-fire-list
+  (fn
+    (cs s)
+    (cond
+      ((empty? cs) s)
+      (:else
+        (let
+          ((s2 ((first cs) s)))
+          (cond ((= s2 nil) nil) (:else (fd-fire-list (rest cs) s2))))))))
+
+(define
+  fd-store-signature
+  (fn
+    (s)
+    (let
+      ((doms (fd-domains-of s)))
+      (let
+        ((dom-sizes (reduce (fn (acc k) (+ acc (len (get doms k)))) 0 (keys doms))))
+        (+ dom-sizes (len (keys s)))))))
+
+(define
+  fd-fire-store
+  (fn
+    (s)
+    (let
+      ((s2 (fd-fire-list (get (fd-store-of s) :constraints) s)))
+      (cond
+        ((= s2 nil) nil)
+        ((= (fd-store-signature s) (fd-store-signature s2)) s2)
+        (:else (fd-fire-store s2))))))
+
+;; --- user-facing goals ---
+
+(define
+  fd-in
+  (fn
+    (x dom-list)
+    (fn
+      (s)
+      (let
+        ((new-dom (fd-dom-from-list dom-list)))
+        (let
+          ((wx (mk-walk x s)))
+          (cond
+            ((number? wx)
+              (cond ((fd-dom-member? wx new-dom) (unit s)) (:else mzero)))
+            ((is-var? wx)
+              (let
+                ((existing (fd-domain-of s (var-name wx))))
+                (let
+                  ((narrowed (cond ((= existing nil) new-dom) (:else (fd-dom-intersect existing new-dom)))))
+                  (let
+                    ((s2 (fd-set-domain s (var-name wx) narrowed)))
+                    (cond ((= s2 nil) mzero) (:else (unit s2)))))))
+            (:else mzero)))))))
+
+;; --- fd-neq ---
+
+(define
+  fd-neq-prop
+  (fn
+    (x y s)
+    (let
+      ((wx (mk-walk x s)) (wy (mk-walk y s)))
+      (cond
+        ((and (number? wx) (number? wy))
+          (cond ((= wx wy) nil) (:else s)))
+        ((and (number? wx) (is-var? wy))
+          (let
+            ((y-dom (fd-domain-of s (var-name wy))))
+            (cond
+              ((= y-dom nil) s)
+              (:else
+                (fd-set-domain s (var-name wy) (fd-dom-without wx y-dom))))))
+        ((and (number? wy) (is-var? wx))
+          (let
+            ((x-dom (fd-domain-of s (var-name wx))))
+            (cond
+              ((= x-dom nil) s)
+              (:else
+                (fd-set-domain s (var-name wx) (fd-dom-without wy x-dom))))))
+        (:else s)))))
+
+(define
+  fd-neq
+  (fn
+    (x y)
+    (fn
+      (s)
+      (let
+        ((c (fn (s-prime) (fd-neq-prop x y s-prime))))
+        (let
+          ((s2 (fd-add-constraint s c)))
+          (let
+            ((s2-or-nil (c s2)))
+            (let
+              ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
+              (cond ((= s3 nil) mzero) (:else (unit s3))))))))))
+
+;; --- fd-lt ---
+
+(define
+  fd-lt-prop
+  (fn
+    (x y s)
+    (let
+      ((wx (mk-walk x s)) (wy (mk-walk y s)))
+      (cond
+        ((and (number? wx) (number? wy))
+          (cond ((< wx wy) s) (:else nil)))
+        ((and (number? wx) (is-var? wy))
+          (let
+            ((yd (fd-domain-of s (var-name wy))))
+            (cond
+              ((= yd nil) s)
+              (:else
+                (fd-set-domain
+                  s
+                  (var-name wy)
+                  (filter (fn (v) (> v wx)) yd))))))
+        ((and (is-var? wx) (number? wy))
+          (let
+            ((xd (fd-domain-of s (var-name wx))))
+            (cond
+              ((= xd nil) s)
+              (:else
+                (fd-set-domain
+                  s
+                  (var-name wx)
+                  (filter (fn (v) (< v wy)) xd))))))
+        ((and (is-var? wx) (is-var? wy))
+          (let
+            ((xd (fd-domain-of s (var-name wx)))
+              (yd (fd-domain-of s (var-name wy))))
+            (cond
+              ((or (= xd nil) (= yd nil)) s)
+              (:else
+                (let
+                  ((xd-prime (filter (fn (v) (< v (fd-dom-max yd))) xd)))
+                  (let
+                    ((s2 (fd-set-domain s (var-name wx) xd-prime)))
+                    (cond
+                      ((= s2 nil) nil)
+                      (:else
+                        (let
+                          ((yd-prime (filter (fn (v) (> v (fd-dom-min xd-prime))) yd)))
+                          (fd-set-domain s2 (var-name wy) yd-prime))))))))))
+        (:else s)))))
+
+(define
+  fd-lt
+  (fn
+    (x y)
+    (fn
+      (s)
+      (let
+        ((c (fn (sp) (fd-lt-prop x y sp))))
+        (let
+          ((s2 (fd-add-constraint s c)))
+          (let
+            ((s2-or-nil (c s2)))
+            (let
+              ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
+              (cond ((= s3 nil) mzero) (:else (unit s3))))))))))
+
+;; --- fd-lte ---
+
+(define
+  fd-lte-prop
+  (fn
+    (x y s)
+    (let
+      ((wx (mk-walk x s)) (wy (mk-walk y s)))
+      (cond
+        ((and (number? wx) (number? wy))
+          (cond ((<= wx wy) s) (:else nil)))
+        ((and (number? wx) (is-var? wy))
+          (let
+            ((yd (fd-domain-of s (var-name wy))))
+            (cond
+              ((= yd nil) s)
+              (:else
+                (fd-set-domain
+                  s
+                  (var-name wy)
+                  (filter (fn (v) (>= v wx)) yd))))))
+        ((and (is-var? wx) (number? wy))
+          (let
+            ((xd (fd-domain-of s (var-name wx))))
+            (cond
+              ((= xd nil) s)
+              (:else
+                (fd-set-domain
+                  s
+                  (var-name wx)
+                  (filter (fn (v) (<= v wy)) xd))))))
+        ((and (is-var? wx) (is-var? wy))
+          (let
+            ((xd (fd-domain-of s (var-name wx)))
+              (yd (fd-domain-of s (var-name wy))))
+            (cond
+              ((or (= xd nil) (= yd nil)) s)
+              (:else
+                (let
+                  ((xd-prime (filter (fn (v) (<= v (fd-dom-max yd))) xd)))
+                  (let
+                    ((s2 (fd-set-domain s (var-name wx) xd-prime)))
+                    (cond
+                      ((= s2 nil) nil)
+                      (:else
+                        (let
+                          ((yd-prime (filter (fn (v) (>= v (fd-dom-min xd-prime))) yd)))
+                          (fd-set-domain s2 (var-name wy) yd-prime))))))))))
+        (:else s)))))
+
+(define
+  fd-lte
+  (fn
+    (x y)
+    (fn
+      (s)
+      (let
+        ((c (fn (sp) (fd-lte-prop x y sp))))
+        (let
+          ((s2 (fd-add-constraint s c)))
+          (let
+            ((s2-or-nil (c s2)))
+            (let
+              ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
+              (cond ((= s3 nil) mzero) (:else (unit s3))))))))))
+
+;; --- fd-eq ---
+
+(define
+  fd-eq-prop
+  (fn
+    (x y s)
+    (let
+      ((wx (mk-walk x s)) (wy (mk-walk y s)))
+      (cond
+        ((and (number? wx) (number? wy))
+          (cond ((= wx wy) s) (:else nil)))
+        ((and (number? wx) (is-var? wy))
+          (let
+            ((yd (fd-domain-of s (var-name wy))))
+            (cond
+              ((and (not (= yd nil)) (not (fd-dom-member? wx yd))) nil)
+              (:else
+                (let
+                  ((s2 (mk-unify wy wx s)))
+                  (cond ((= s2 nil) nil) (:else s2)))))))
+        ((and (is-var? wx) (number? wy))
+          (let
+            ((xd (fd-domain-of s (var-name wx))))
+            (cond
+              ((and (not (= xd nil)) (not (fd-dom-member? wy xd))) nil)
+              (:else
+                (let
+                  ((s2 (mk-unify wx wy s)))
+                  (cond ((= s2 nil) nil) (:else s2)))))))
+        ((and (is-var? wx) (is-var? wy))
+          (let
+            ((xd (fd-domain-of s (var-name wx)))
+              (yd (fd-domain-of s (var-name wy))))
+            (cond
+              ((and (= xd nil) (= yd nil))
+                (let
+                  ((s2 (mk-unify wx wy s)))
+                  (cond ((= s2 nil) nil) (:else s2))))
+              (:else
+                (let
+                  ((shared (cond ((= xd nil) yd) ((= yd nil) xd) (:else (fd-dom-intersect xd yd)))))
+                  (cond
+                    ((fd-dom-empty? shared) nil)
+                    (:else
+                      (let
+                        ((s2 (fd-set-domain s (var-name wx) shared)))
+                        (cond
+                          ((= s2 nil) nil)
+                          (:else
+                            (let
+                              ((s3 (fd-set-domain s2 (var-name wy) shared)))
+                              (cond
+                                ((= s3 nil) nil)
+                                (:else (mk-unify wx wy s3))))))))))))))
+        (:else s)))))
+
+(define
+  fd-eq
+  (fn
+    (x y)
+    (fn
+      (s)
+      (let
+        ((c (fn (sp) (fd-eq-prop x y sp))))
+        (let
+          ((s2 (fd-add-constraint s c)))
+          (let
+            ((s2-or-nil (c s2)))
+            (let
+              ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
+              (cond ((= s3 nil) mzero) (:else (unit s3))))))))))
+
+;; --- labelling ---
+
+(define
+  fd-try-each-value
+  (fn
+    (x dom s)
+    (cond
+      ((empty? dom) mzero)
+      (:else
+        (let
+          ((s2 (mk-unify x (first dom) s)))
+          (let
+            ((s3 (cond ((= s2 nil) nil) (:else (fd-fire-store s2)))))
+            (let
+              ((this-stream (cond ((= s3 nil) mzero) (:else (unit s3))))
+                (rest-stream (fd-try-each-value x (rest dom) s)))
+              (mk-mplus this-stream rest-stream))))))))
+
+(define
+  fd-label-one
+  (fn
+    (x)
+    (fn
+      (s)
+      (let
+        ((wx (mk-walk x s)))
+        (cond
+          ((number? wx) (unit s))
+          ((is-var? wx)
+            (let
+              ((dom (fd-domain-of s (var-name wx))))
+              (cond
+                ((= dom nil) mzero)
+                (:else (fd-try-each-value wx dom s)))))
+          (:else mzero))))))
+
+(define
+  fd-label
+  (fn
+    (vars)
+    (cond
+      ((empty? vars) succeed)
+      (:else (mk-conj (fd-label-one (first vars)) (fd-label (rest vars)))))))
+
+;; --- fd-distinct (pairwise distinct via fd-neq) ---
+
+(define
+  fd-distinct-from-head
+  (fn
+    (x others)
+    (cond
+      ((empty? others) succeed)
+      (:else
+        (mk-conj
+          (fd-neq x (first others))
+          (fd-distinct-from-head x (rest others)))))))
+
+(define
+  fd-distinct
+  (fn
+    (vars)
+    (cond
+      ((empty? vars) succeed)
+      ((empty? (rest vars)) succeed)
+      (:else
+        (mk-conj
+          (fd-distinct-from-head (first vars) (rest vars))
+          (fd-distinct (rest vars)))))))
+
+;; --- fd-plus (x + y = z, ground-cases propagator) ---
+
+(define
+  fd-bind-or-narrow
+  (fn
+    (w target s)
+    (cond
+      ((number? w) (cond ((= w target) s) (:else nil)))
+      ((is-var? w)
+        (let
+          ((wd (fd-domain-of s (var-name w))))
+          (cond
+            ((and (not (= wd nil)) (not (fd-dom-member? target wd))) nil)
+            (:else
+              (let
+                ((s2 (mk-unify w target s)))
+                (cond ((= s2 nil) nil) (:else s2)))))))
+      (:else nil))))
+
+(define
+  fd-narrow-or-skip
+  (fn
+    (s var-key d lo hi)
+    (cond
+      ((= d nil) s)
+      (:else
+        (fd-set-domain
+          s
+          var-key
+          (filter (fn (v) (and (>= v lo) (<= v hi))) d))))))
+
+(define
+  fd-plus-prop-vvn
+  (fn
+    (wx wy wz s)
+    (let
+      ((xd (fd-domain-of s (var-name wx)))
+        (yd (fd-domain-of s (var-name wy))))
+      (cond
+        ((or (= xd nil) (= yd nil)) s)
+        (:else
+          (let
+            ((s1 (fd-narrow-or-skip s (var-name wx) xd (- wz (fd-dom-max yd)) (- wz (fd-dom-min yd)))))
+            (cond
+              ((= s1 nil) nil)
+              (:else
+                (let
+                  ((xd2 (fd-domain-of s1 (var-name wx))))
+                  (fd-narrow-or-skip
+                    s1
+                    (var-name wy)
+                    yd
+                    (- wz (fd-dom-max xd2))
+                    (- wz (fd-dom-min xd2))))))))))))
+
+(define
+  fd-plus-prop-nvv
+  (fn
+    (wx wy wz s)
+    (let
+      ((yd (fd-domain-of s (var-name wy)))
+        (zd (fd-domain-of s (var-name wz))))
+      (cond
+        ((or (= yd nil) (= zd nil)) s)
+        (:else
+          (let
+            ((s1 (fd-narrow-or-skip s (var-name wy) yd (- (fd-dom-min zd) wx) (- (fd-dom-max zd) wx))))
+            (cond
+              ((= s1 nil) nil)
+              (:else
+                (let
+                  ((yd2 (fd-domain-of s1 (var-name wy))))
+                  (fd-narrow-or-skip
+                    s1
+                    (var-name wz)
+                    zd
+                    (+ wx (fd-dom-min yd2))
+                    (+ wx (fd-dom-max yd2))))))))))))
+
+(define
+  fd-plus-prop-vnv
+  (fn
+    (wx wy wz s)
+    (let
+      ((xd (fd-domain-of s (var-name wx)))
+        (zd (fd-domain-of s (var-name wz))))
+      (cond
+        ((or (= xd nil) (= zd nil)) s)
+        (:else
+          (let
+            ((s1 (fd-narrow-or-skip s (var-name wx) xd (- (fd-dom-min zd) wy) (- (fd-dom-max zd) wy))))
+            (cond
+              ((= s1 nil) nil)
+              (:else
+                (let
+                  ((xd2 (fd-domain-of s1 (var-name wx))))
+                  (fd-narrow-or-skip
+                    s1
+                    (var-name wz)
+                    zd
+                    (+ (fd-dom-min xd2) wy)
+                    (+ (fd-dom-max xd2) wy))))))))))) 
+
+(define
+  fd-plus-prop-vvv
+  (fn
+    (wx wy wz s)
+    (let
+      ((xd (fd-domain-of s (var-name wx)))
+        (yd (fd-domain-of s (var-name wy)))
+        (zd (fd-domain-of s (var-name wz))))
+      (cond
+        ((or (= xd nil) (or (= yd nil) (= zd nil))) s)
+        (:else
+          (let
+            ((s1 (fd-narrow-or-skip s (var-name wx) xd (- (fd-dom-min zd) (fd-dom-max yd)) (- (fd-dom-max zd) (fd-dom-min yd)))))
+            (cond
+              ((= s1 nil) nil)
+              (:else
+                (let
+                  ((s2 (fd-narrow-or-skip s1 (var-name wy) yd (- (fd-dom-min zd) (fd-dom-max xd)) (- (fd-dom-max zd) (fd-dom-min xd)))))
+                  (cond
+                    ((= s2 nil) nil)
+                    (:else
+                      (fd-narrow-or-skip
+                        s2
+                        (var-name wz)
+                        zd
+                        (+ (fd-dom-min xd) (fd-dom-min yd))
+                        (+ (fd-dom-max xd) (fd-dom-max yd))))))))))))))
+
+(define
+  fd-plus-prop
+  (fn
+    (x y z s)
+    (let
+      ((wx (mk-walk x s)) (wy (mk-walk y s)) (wz (mk-walk z s)))
+      (cond
+        ((and (number? wx) (number? wy) (number? wz))
+          (cond ((= (+ wx wy) wz) s) (:else nil)))
+        ((and (number? wx) (number? wy))
+          (fd-bind-or-narrow wz (+ wx wy) s))
+        ((and (number? wx) (number? wz))
+          (fd-bind-or-narrow wy (- wz wx) s))
+        ((and (number? wy) (number? wz))
+          (fd-bind-or-narrow wx (- wz wy) s))
+        ((and (is-var? wx) (is-var? wy) (number? wz))
+          (fd-plus-prop-vvn wx wy wz s))
+        ((and (number? wx) (is-var? wy) (is-var? wz))
+          (fd-plus-prop-nvv wx wy wz s))
+        ((and (is-var? wx) (number? wy) (is-var? wz))
+          (fd-plus-prop-vnv wx wy wz s))
+        ((and (is-var? wx) (is-var? wy) (is-var? wz))
+          (fd-plus-prop-vvv wx wy wz s))
+        (:else s)))))
+
+(define
+  fd-plus
+  (fn
+    (x y z)
+    (fn
+      (s)
+      (let
+        ((c (fn (sp) (fd-plus-prop x y z sp))))
+        (let
+          ((s2 (fd-add-constraint s c)))
+          (let
+            ((s2-or-nil (c s2)))
+            (let
+              ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
+              (cond ((= s3 nil) mzero) (:else (unit s3))))))))))
+
+;; --- fd-times (x * y = z, ground-cases propagator) ---
+
+(define
+  fd-int-ceil-div
+  (fn
+    (a b)
+    (cond
+      ((= (mod a b) 0) (/ a b))
+      (:else (+ (fd-int-floor-div a b) 1)))))
+
+(define fd-int-floor-div (fn (a b) (/ (- a (mod a b)) b)))
+
+(define
+  fd-dom-positive?
+  (fn
+    (d)
+    (cond ((empty? d) false) (:else (>= (fd-dom-min d) 1)))))
+
+(define
+  fd-times-prop-vvv
+  (fn
+    (wx wy wz s)
+    (let
+      ((xd (fd-domain-of s (var-name wx)))
+        (yd (fd-domain-of s (var-name wy)))
+        (zd (fd-domain-of s (var-name wz))))
+      (cond
+        ((or (= xd nil) (or (= yd nil) (= zd nil))) s)
+        ((not (and (fd-dom-positive? xd) (and (fd-dom-positive? yd) (fd-dom-positive? zd))))
+          s)
+        (:else
+          (let
+            ((s1 (fd-narrow-or-skip s (var-name wx) xd (fd-int-ceil-div (fd-dom-min zd) (fd-dom-max yd)) (fd-int-floor-div (fd-dom-max zd) (fd-dom-min yd)))))
+            (cond
+              ((= s1 nil) nil)
+              (:else
+                (let
+                  ((s2 (fd-narrow-or-skip s1 (var-name wy) yd (fd-int-ceil-div (fd-dom-min zd) (fd-dom-max xd)) (fd-int-floor-div (fd-dom-max zd) (fd-dom-min xd)))))
+                  (cond
+                    ((= s2 nil) nil)
+                    (:else
+                      (fd-narrow-or-skip
+                        s2
+                        (var-name wz)
+                        zd
+                        (* (fd-dom-min xd) (fd-dom-min yd))
+                        (* (fd-dom-max xd) (fd-dom-max yd))))))))))))))
+
+(define
+  fd-times-prop-vvn
+  (fn
+    (wx wy wz s)
+    (let
+      ((xd (fd-domain-of s (var-name wx)))
+        (yd (fd-domain-of s (var-name wy))))
+      (cond
+        ((or (= xd nil) (= yd nil)) s)
+        ((not (and (fd-dom-positive? xd) (fd-dom-positive? yd))) s)
+        ((<= wz 0) s)
+        (:else
+          (let
+            ((s1 (fd-narrow-or-skip s (var-name wx) xd (fd-int-ceil-div wz (fd-dom-max yd)) (fd-int-floor-div wz (fd-dom-min yd)))))
+            (cond
+              ((= s1 nil) nil)
+              (:else
+                (let
+                  ((xd2 (fd-domain-of s1 (var-name wx))))
+                  (fd-narrow-or-skip
+                    s1
+                    (var-name wy)
+                    yd
+                    (fd-int-ceil-div wz (fd-dom-max xd2))
+                    (fd-int-floor-div wz (fd-dom-min xd2))))))))))))
+
+(define
+  fd-times-prop-nvv
+  (fn
+    (wx wy wz s)
+    (cond
+      ((<= wx 0) s)
+      (:else
+        (let
+          ((yd (fd-domain-of s (var-name wy)))
+            (zd (fd-domain-of s (var-name wz))))
+          (cond
+            ((or (= yd nil) (= zd nil)) s)
+            ((not (and (fd-dom-positive? yd) (fd-dom-positive? zd))) s)
+            (:else
+              (let
+                ((s1 (fd-narrow-or-skip s (var-name wy) yd (fd-int-ceil-div (fd-dom-min zd) wx) (fd-int-floor-div (fd-dom-max zd) wx))))
+                (cond
+                  ((= s1 nil) nil)
+                  (:else
+                    (let
+                      ((yd2 (fd-domain-of s1 (var-name wy))))
+                      (fd-narrow-or-skip
+                        s1
+                        (var-name wz)
+                        zd
+                        (* wx (fd-dom-min yd2))
+                        (* wx (fd-dom-max yd2))))))))))))))
+
+(define
+  fd-times-prop-vnv
+  (fn
+    (wx wy wz s)
+    (cond
+      ((<= wy 0) s)
+      (:else
+        (let
+          ((xd (fd-domain-of s (var-name wx)))
+            (zd (fd-domain-of s (var-name wz))))
+          (cond
+            ((or (= xd nil) (= zd nil)) s)
+            ((not (and (fd-dom-positive? xd) (fd-dom-positive? zd))) s)
+            (:else
+              (let
+                ((s1 (fd-narrow-or-skip s (var-name wx) xd (fd-int-ceil-div (fd-dom-min zd) wy) (fd-int-floor-div (fd-dom-max zd) wy))))
+                (cond
+                  ((= s1 nil) nil)
+                  (:else
+                    (let
+                      ((xd2 (fd-domain-of s1 (var-name wx))))
+                      (fd-narrow-or-skip
+                        s1
+                        (var-name wz)
+                        zd
+                        (* (fd-dom-min xd2) wy)
+                        (* (fd-dom-max xd2) wy))))))))))))) 
+
+(define
+  fd-times-prop
+  (fn
+    (x y z s)
+    (let
+      ((wx (mk-walk x s)) (wy (mk-walk y s)) (wz (mk-walk z s)))
+      (cond
+        ((and (number? wx) (number? wy) (number? wz))
+          (cond ((= (* wx wy) wz) s) (:else nil)))
+        ((and (number? wx) (number? wy))
+          (fd-bind-or-narrow wz (* wx wy) s))
+        ((and (number? wx) (number? wz))
+          (cond
+            ((= wx 0) (cond ((= wz 0) s) (:else nil)))
+            ((not (= (mod wz wx) 0)) nil)
+            (:else (fd-bind-or-narrow wy (/ wz wx) s))))
+        ((and (number? wy) (number? wz))
+          (cond
+            ((= wy 0) (cond ((= wz 0) s) (:else nil)))
+            ((not (= (mod wz wy) 0)) nil)
+            (:else (fd-bind-or-narrow wx (/ wz wy) s))))
+        ((and (is-var? wx) (is-var? wy) (number? wz))
+          (fd-times-prop-vvn wx wy wz s))
+        ((and (number? wx) (is-var? wy) (is-var? wz))
+          (fd-times-prop-nvv wx wy wz s))
+        ((and (is-var? wx) (number? wy) (is-var? wz))
+          (fd-times-prop-vnv wx wy wz s))
+        ((and (is-var? wx) (is-var? wy) (is-var? wz))
+          (fd-times-prop-vvv wx wy wz s))
+        (:else s)))))
+
+(define
+  fd-times
+  (fn
+    (x y z)
+    (fn
+      (s)
+      (let
+        ((c (fn (sp) (fd-times-prop x y z sp))))
+        (let
+          ((s2 (fd-add-constraint s c)))
+          (let
+            ((s2-or-nil (c s2)))
+            (let
+              ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
+              (cond ((= s3 nil) mzero) (:else (unit s3))))))))))

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/defrel.sx

@@ -0,0 +1,25 @@
+;; lib/minikanren/defrel.sx — Prolog-style defrel macro.
+;;
+;;   (defrel (NAME ARG1 ARG2 ...)
+;;     (CLAUSE1 ...)
+;;     (CLAUSE2 ...)
+;;     ...)
+;;
+;; expands to
+;;
+;;   (define NAME (fn (ARG1 ARG2 ...) (conde (CLAUSE1 ...) (CLAUSE2 ...))))
+;;
+;; This puts each clause's goals immediately after the head, mirroring
+;; Prolog's `name(Args) :- goals.` shape. Clauses are conde-conjoined
+;; goals — `Zzz`-wrapping is automatic via `conde`, so recursive
+;; relations terminate on partial answers.
+
+(defmacro
+  defrel
+  (head &rest clauses)
+  (let
+    ((name (first head)) (args (rest head)))
+    (list
+      (quote define)
+      name
+      (list (quote fn) args (cons (quote conde) clauses)))))

lib/minikanren/diseq.sx

@@ -0,0 +1,71 @@
+;; lib/minikanren/diseq.sx — Phase 5 polish: =/= disequality with a
+;; constraint store, generalising nafc / fd-neq to logic terms.
+;;
+;; The constraint store lives under the same `_fd` reserved key as the
+;; CLP(FD) propagators (a disequality is just another constraint
+;; closure that the existing fd-fire-store machinery re-runs).
+;;
+;; =/= semantics:
+;;   - If u and v walk to ground non-unifiable terms, succeed (drop).
+;;   - If they walk to terms that COULD become equal under a future
+;;     binding, store the constraint; re-check after each binding.
+;;   - If they're already equal (unify with no new bindings), fail.
+;;
+;; Implementation: each =/= test attempts (mk-unify wu wv s).
+;;   nil      — distinct, keep s, drop the constraint (return s).
+;;   subst eq — equal, fail (return nil).
+;;   subst >  — partially unifiable; keep the constraint, return s.
+;;
+;; "Substitution equal to s" is detected via key-count: mk-unify only
+;; ever extends a substitution, never removes from it, so equal
+;; key-count means no new bindings were needed.
+
+(define
+  =/=-prop
+  (fn
+    (u v s)
+    (let
+      ((s-after (mk-unify u v s)))
+      (cond
+        ((= s-after nil) s)
+        ((= (len (keys s)) (len (keys s-after))) nil)
+        (:else s)))))
+
+(define
+  =/=
+  (fn
+    (u v)
+    (fn
+      (s)
+      (let
+        ((c (fn (sp) (=/=-prop u v sp))))
+        (let
+          ((s2 (fd-add-constraint s c)))
+          (let
+            ((s2-or-nil (c s2)))
+            (let
+              ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
+              (cond ((= s3 nil) mzero) (:else (unit s3))))))))))
+
+;; --- constraint-aware == ---
+;;
+;; Plain `==` doesn't fire the constraint store, so a binding that
+;; should violate a pending =/= goes undetected. `==-cs` is the
+;; drop-in replacement that fires fd-fire-store after each binding.
+;; Use ==-cs in any program that mixes =/= (or fd-* goals that should
+;; re-check after non-FD bindings) with regular unification.
+
+(define
+  ==-cs
+  (fn
+    (u v)
+    (fn
+      (s)
+      (let
+        ((s2 (mk-unify u v s)))
+        (cond
+          ((= s2 nil) mzero)
+          (:else
+            (let
+              ((s3 (fd-fire-store s2)))
+              (cond ((= s3 nil) mzero) (:else (unit s3))))))))))

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,151 @@
+;; 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))))
+
+(define
+  even-i
+  (fn (n) (project (n) (if (and (number? n) (even? n)) succeed fail))))
+
+(define
+  odd-i
+  (fn (n) (project (n) (if (and (number? n) (odd? n)) succeed fail))))
+
+(define
+  sortedo
+  (fn
+    (l)
+    (conde
+      ((nullo l))
+      ((fresh (a) (== l (list a))))
+      ((fresh (a b rest mid) (conso a mid l) (conso b rest mid) (lteo-i a b) (sortedo mid))))))
+
+(define
+  mino
+  (fn
+    (l m)
+    (conde
+      ((fresh (a) (== l (list a)) (== m a)))
+      ((fresh (a d rest-min) (conso a d l) (mino d rest-min) (conde ((lteo-i a rest-min) (== m a)) ((lto-i rest-min a) (== m rest-min))))))))
+
+(define
+  maxo
+  (fn
+    (l m)
+    (conde
+      ((fresh (a) (== l (list a)) (== m a)))
+      ((fresh (a d rest-max) (conso a d l) (maxo d rest-max) (conde ((lteo-i rest-max a) (== m a)) ((lto-i a rest-max) (== m rest-max))))))))
+
+(define
+  sumo
+  (fn
+    (l total)
+    (conde
+      ((nullo l) (== total 0))
+      ((fresh (a d rest-sum) (conso a d l) (sumo d rest-sum) (pluso-i a rest-sum total))))))
+
+(define
+  producto
+  (fn
+    (l total)
+    (conde
+      ((nullo l) (== total 1))
+      ((fresh (a d rest-prod) (conso a d l) (producto d rest-prod) (*o-i a rest-prod total))))))
+
+(define
+  lengtho-i
+  (fn
+    (l n)
+    (conde
+      ((nullo l) (== n 0))
+      ((fresh (a d n-1) (conso a d l) (lengtho-i d n-1) (pluso-i 1 n-1 n))))))
+
+(define
+  enumerate-from-i
+  (fn
+    (start l result)
+    (conde
+      ((nullo l) (nullo result))
+      ((fresh (a d r-rest start-prime) (conso a d l) (conso (list start a) r-rest result) (pluso-i 1 start start-prime) (enumerate-from-i start-prime d r-rest))))))
+
+(define enumerate-i (fn (l result) (enumerate-from-i 0 l result)))
+
+(define
+  counto
+  (fn
+    (x l n)
+    (conde
+      ((nullo l) (== n 0))
+      ((fresh (a d n-rest) (conso a d l) (conde ((== a x) (counto x d n-rest) (pluso-i 1 n-rest n)) ((nafc (== a x)) (counto x d n))))))))
+
+(define
+  mk-arith-prog
+  (fn
+    (start step len)
+    (cond
+      ((= len 0) (list))
+      (:else (cons start (mk-arith-prog (+ start step) step (- len 1)))))))
+
+(define
+  arith-progo
+  (fn
+    (start step len result)
+    (project (start step len) (== result (mk-arith-prog start step len)))))

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,51 @@
+;; 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
+  eveno
+  (fn
+    (n)
+    (conde
+      ((== n :z))
+      ((fresh (m) (== n (list :s (list :s m))) (eveno m))))))
+
+(define
+  oddo
+  (fn
+    (n)
+    (conde
+      ((== n (list :s :z)))
+      ((fresh (m) (== n (list :s (list :s m))) (oddo m))))))
+
+(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,361 @@
+;; 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
+  appendo3
+  (fn
+    (l1 l2 l3 result)
+    (fresh (l12) (appendo l1 l2 l12) (appendo l12 l3 result))))
+
+(define
+  partitiono
+  (fn
+    (pred l yes no)
+    (conde
+      ((nullo l) (nullo yes) (nullo no))
+      ((fresh (a d y-rest n-rest) (conso a d l) (conde ((pred a) (conso a y-rest yes) (== no n-rest) (partitiono pred d y-rest n-rest)) ((nafc (pred a)) (== yes y-rest) (conso a n-rest no) (partitiono pred d y-rest n-rest))))))))
+
+(define
+  foldr-o
+  (fn
+    (rel l acc result)
+    (conde
+      ((nullo l) (== result acc))
+      ((fresh (a d r-rest) (conso a d l) (foldr-o rel d acc r-rest) (rel a r-rest result))))))
+
+(define
+  foldl-o
+  (fn
+    (rel l acc result)
+    (conde
+      ((nullo l) (== result acc))
+      ((fresh (a d new-acc) (conso a d l) (rel acc a new-acc) (foldl-o rel d new-acc result))))))
+
+(define
+  flat-mapo
+  (fn
+    (rel l result)
+    (conde
+      ((nullo l) (nullo result))
+      ((fresh (a d a-result rest-result) (conso a d l) (rel a a-result) (flat-mapo rel d rest-result) (appendo a-result rest-result result))))))
+
+(define
+  nub-o
+  (fn
+    (l result)
+    (conde
+      ((nullo l) (nullo result))
+      ((fresh (a d r-rest) (conso a d l) (conde ((membero a d) (nub-o d result)) ((nafc (membero a d)) (conso a r-rest result) (nub-o d r-rest))))))))
+
+
+(define
+  take-while-o
+  (fn
+    (pred l result)
+    (conde
+      ((nullo l) (nullo result))
+      ((fresh (a d r-rest) (conso a d l) (conde ((pred a) (conso a r-rest result) (take-while-o pred d r-rest)) ((nafc (pred a)) (== result (list)))))))))
+
+(define
+  drop-while-o
+  (fn
+    (pred l result)
+    (conde
+      ((nullo l) (nullo result))
+      ((fresh (a d) (conso a d l) (conde ((pred a) (drop-while-o pred d result)) ((nafc (pred a)) (== result l))))))))
+
+(define
+  membero
+  (fn
+    (x l)
+    (conde
+      ((fresh (d) (conso x d l)))
+      ((fresh (a d) (conso a d l) (membero x d))))))
+
+(define
+  not-membero
+  (fn
+    (x l)
+    (conde
+      ((nullo l))
+      ((fresh (a d) (conso a d l) (nafc (== a x)) (not-membero x d))))))
+
+(define
+  subseto
+  (fn
+    (l1 l2)
+    (conde
+      ((nullo l1))
+      ((fresh (a d) (conso a d l1) (membero a l2) (subseto d l2))))))
+
+(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
+  rev-acco
+  (fn
+    (l acc result)
+    (conde
+      ((nullo l) (== result acc))
+      ((fresh (a d acc-prime) (conso a d l) (conso a acc acc-prime) (rev-acco d acc-prime result))))))
+
+(define rev-2o (fn (l result) (rev-acco l (list) result)))
+
+(define palindromeo (fn (l) (fresh (rev) (reverseo l rev) (== l rev))))
+
+(define prefixo (fn (p l) (fresh (rest) (appendo p rest l))))
+
+(define suffixo (fn (s l) (fresh (front) (appendo front s l))))
+
+(define
+  subo
+  (fn
+    (s l)
+    (fresh
+      (front-and-s back front)
+      (appendo front-and-s back l)
+      (appendo front s front-and-s))))
+
+(define
+  selecto
+  (fn
+    (x rest l)
+    (conde
+      ((conso x rest l))
+      ((fresh (a d r) (conso a d l) (conso a r rest) (selecto x r d))))))
+
+(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
+  removeo-allo
+  (fn
+    (x l result)
+    (conde
+      ((nullo l) (nullo result))
+      ((fresh (a d) (conso a d l) (== a x) (removeo-allo x d result)))
+      ((fresh (a d r-rest) (conso a d l) (nafc (== a x)) (conso a r-rest result) (removeo-allo x d r-rest))))))
+
+(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
+  iterate-no
+  (fn
+    (rel n x result)
+    (conde
+      ((== n :z) (== result x))
+      ((fresh (n-1 mid) (== n (list :s n-1)) (rel x mid) (iterate-no rel n-1 mid result))))))
+
+(define
+  pairlisto
+  (fn
+    (l1 l2 pairs)
+    (conde
+      ((nullo l1) (nullo l2) (nullo pairs))
+      ((fresh (a1 d1 a2 d2 d-pairs) (conso a1 d1 l1) (conso a2 d2 l2) (conso (list a1 a2) d-pairs pairs) (pairlisto d1 d2 d-pairs))))))
+
+(define
+  zip-with-o
+  (fn
+    (rel l1 l2 result)
+    (conde
+      ((nullo l1) (nullo l2) (nullo result))
+      ((fresh (a1 d1 a2 d2 a-result d-result) (conso a1 d1 l1) (conso a2 d2 l2) (rel a1 a2 a-result) (conso a-result d-result result) (zip-with-o rel d1 d2 d-result))))))
+
+(define
+  swap-firsto
+  (fn
+    (l result)
+    (fresh
+      (a b rest mid-l mid-r)
+      (conso a mid-l l)
+      (conso b rest mid-l)
+      (conso b mid-r result)
+      (conso a rest mid-r))))
+
+(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))))))
+
+(define
+  lasto
+  (fn
+    (l x)
+    (conde
+      ((conso x (list) l))
+      ((fresh (a d) (conso a d l) (lasto d x))))))
+
+(define
+  init-o
+  (fn
+    (l init)
+    (conde
+      ((fresh (x) (conso x (list) l) (== init (list))))
+      ((fresh (a d d-init) (conso a d l) (conso a d-init init) (init-o d d-init))))))
+
+(define
+  tako
+  (fn
+    (n l prefix)
+    (conde
+      ((== n :z) (== prefix (list)))
+      ((fresh (n-1 a d p-rest) (== n (list :s n-1)) (conso a d l) (conso a p-rest prefix) (tako n-1 d p-rest))))))
+
+(define
+  dropo
+  (fn
+    (n l suffix)
+    (conde
+      ((== n :z) (== suffix l))
+      ((fresh (n-1 a d) (== n (list :s n-1)) (conso a d l) (dropo n-1 d suffix))))))
+
+(define
+  repeato
+  (fn
+    (x n result)
+    (conde
+      ((== n :z) (== result (list)))
+      ((fresh (n-1 r-rest) (== n (list :s n-1)) (conso x r-rest result) (repeato x n-1 r-rest))))))
+
+(define
+  concato
+  (fn
+    (lists result)
+    (conde
+      ((nullo lists) (nullo result))
+      ((fresh (h t r-rest) (conso h t lists) (appendo h r-rest result) (concato t r-rest))))))

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/tabling-slg.sx

@@ -0,0 +1,94 @@
+;; lib/minikanren/tabling-slg.sx — Phase 7 piece A: SLG-style tabling.
+;;
+;; Naive memoization (table-1/2/3 in tabling.sx) drains the body's
+;; answer stream eagerly, then caches. Recursive tabled calls with the
+;; SAME ground key see an empty cache (the in-progress entry doesn't
+;; exist), so they recurse and the host overflows on cyclic relations.
+;;
+;; This module ships the in-progress-sentinel piece of SLG resolution:
+;; before evaluating the body, mark the cache entry as :in-progress;
+;; any recursive call to the same key sees the sentinel and returns
+;; mzero (no answers yet). Outer recursion thus terminates on cycles.
+;; Limitation: a single pass — answers found by cycle-dependent
+;; recursive calls are NOT discovered. Full SLG with fixed-point
+;; iteration (re-running until no new answers) is left for follow-up.
+
+(define
+  table-2-slg-iter
+  (fn
+    (rel-fn input output s key prev-vals)
+    (begin
+      (mk-tab-store! key prev-vals)
+      (let
+        ((all-substs (stream-take -1 ((rel-fn input output) s))))
+        (let
+          ((vals (map (fn (s2) (mk-walk* output s2)) all-substs)))
+          (cond
+            ((= (len vals) (len prev-vals))
+              (begin
+                (mk-tab-store! key vals)
+                (mk-tab-replay-vals vals output s)))
+            (:else (table-2-slg-iter rel-fn input output s key vals))))))))
+
+(define
+  table-2-slg
+  (fn
+    (name rel-fn)
+    (fn
+      (input output)
+      (fn
+        (s)
+        (let
+          ((winput (mk-walk* input s)))
+          (cond
+            ((mk-tab-ground-term? winput)
+              (let
+                ((key (str name "/slg/" winput)))
+                (let
+                  ((cached (mk-tab-lookup key)))
+                  (cond
+                    ((not (= cached :miss))
+                      (mk-tab-replay-vals cached output s))
+                    (:else
+                      (table-2-slg-iter rel-fn input output s key (list)))))))
+            (:else ((rel-fn input output) s))))))))
+
+(define
+  table-3-slg-iter
+  (fn
+    (rel-fn i1 i2 output s key prev-vals)
+    (begin
+      (mk-tab-store! key prev-vals)
+      (let
+        ((all-substs (stream-take -1 ((rel-fn i1 i2 output) s))))
+        (let
+          ((vals (map (fn (s2) (mk-walk* output s2)) all-substs)))
+          (cond
+            ((= (len vals) (len prev-vals))
+              (begin
+                (mk-tab-store! key vals)
+                (mk-tab-replay-vals vals output s)))
+            (:else (table-3-slg-iter rel-fn i1 i2 output s key vals))))))))
+
+(define
+  table-3-slg
+  (fn
+    (name rel-fn)
+    (fn
+      (i1 i2 output)
+      (fn
+        (s)
+        (let
+          ((wi1 (mk-walk* i1 s)) (wi2 (mk-walk* i2 s)))
+          (cond
+            ((and (mk-tab-ground-term? wi1) (mk-tab-ground-term? wi2))
+              (let
+                ((key (str name "/slg3/" wi1 "/" wi2)))
+                (let
+                  ((cached (mk-tab-lookup key)))
+                  (cond
+                    ((not (= cached :miss))
+                      (mk-tab-replay-vals cached output s))
+                    (:else
+                      (table-3-slg-iter rel-fn i1 i2 output s key (list)))))))
+            (:else ((rel-fn i1 i2 output) s))))))))

lib/minikanren/tabling.sx

@@ -0,0 +1,157 @@
+;; lib/minikanren/tabling.sx — Phase 7 piece A: naive memoization.
+;;
+;; A `table-2` wrapper for 2-arg relations (input, output). Caches by
+;; ground input (walked at call time). On hit, replays the cached output
+;; values; on miss, runs the relation, collects all output values from
+;; the answer stream, stores, then replays.
+;;
+;; Limitations of naive memoization (vs proper SLG / producer-consumer
+;; tabling):
+;;   - Each call must terminate before its result enters the cache —
+;;     so cyclic recursive calls with the SAME ground input would still
+;;     diverge (not addressed here).
+;;   - Caching by full ground walk only; partially-ground args fall
+;;     through to the underlying relation.
+;;
+;; Despite the limitations, naive memoization is enough for the
+;; canonical demo: Fibonacci goes from exponential to linear because
+;; each fib(k) result is computed at most once.
+;;
+;; Cache lifetime: a single global mk-tab-cache. Use `(mk-tab-clear!)`
+;; between independent queries.
+
+(define mk-tab-cache {})
+
+(define mk-tab-clear! (fn () (set! mk-tab-cache {})))
+
+(define
+  mk-tab-lookup
+  (fn
+    (key)
+    (cond
+      ((has-key? mk-tab-cache key) (get mk-tab-cache key))
+      (:else :miss))))
+
+(define
+  mk-tab-store!
+  (fn (key vals) (set! mk-tab-cache (assoc mk-tab-cache key vals))))
+
+(define
+  mk-tab-ground-term?
+  (fn
+    (t)
+    (cond
+      ((is-var? t) false)
+      ((mk-cons-cell? t)
+        (and
+          (mk-tab-ground-term? (mk-cons-head t))
+          (mk-tab-ground-term? (mk-cons-tail t))))
+      ((mk-list-pair? t) (every? mk-tab-ground-term? t))
+      (:else true))))
+
+(define
+  mk-tab-replay-vals
+  (fn
+    (vals output s)
+    (cond
+      ((empty? vals) mzero)
+      (:else
+        (let
+          ((sp (mk-unify output (first vals) s)))
+          (let
+            ((this-stream (cond ((= sp nil) mzero) (:else (unit sp)))))
+            (mk-mplus this-stream (mk-tab-replay-vals (rest vals) output s))))))))
+
+(define
+  table-2
+  (fn
+    (name rel-fn)
+    (fn
+      (input output)
+      (fn
+        (s)
+        (let
+          ((winput (mk-walk* input s)))
+          (cond
+            ((mk-tab-ground-term? winput)
+              (let
+                ((key (str name "@" winput)))
+                (let
+                  ((cached (mk-tab-lookup key)))
+                  (cond
+                    ((= cached :miss)
+                      (let
+                        ((all-substs (stream-take -1 ((rel-fn input output) s))))
+                        (let
+                          ((vals (map (fn (s2) (mk-walk* output s2)) all-substs)))
+                          (begin
+                            (mk-tab-store! key vals)
+                            (mk-tab-replay-vals vals output s)))))
+                    (:else (mk-tab-replay-vals cached output s))))))
+            (:else ((rel-fn input output) s))))))))
+
+;; --- table-1: 1-arg relation (one input, no output to cache) ---
+;; The relation is a predicate `(p input)` that succeeds or fails.
+;; Cache stores either :ok or :no.
+
+(define
+  table-1
+  (fn
+    (name rel-fn)
+    (fn
+      (input)
+      (fn
+        (s)
+        (let
+          ((winput (mk-walk* input s)))
+          (cond
+            ((mk-tab-ground-term? winput)
+              (let
+                ((key (str name "@1@" winput)))
+                (let
+                  ((cached (mk-tab-lookup key)))
+                  (cond
+                    ((= cached :miss)
+                      (let
+                        ((stream ((rel-fn input) s)))
+                        (let
+                          ((peek (stream-take 1 stream)))
+                          (cond
+                            ((empty? peek)
+                              (begin (mk-tab-store! key :no) mzero))
+                            (:else (begin (mk-tab-store! key :ok) stream))))))
+                    ((= cached :ok) (unit s))
+                    ((= cached :no) mzero)
+                    (:else mzero)))))
+            (:else ((rel-fn input) s))))))))
+
+;; --- table-3: 3-arg relation (input1 input2 output) ---
+;; Cache keyed by (input1, input2). Output values cached as a list.
+
+(define
+  table-3
+  (fn
+    (name rel-fn)
+    (fn
+      (i1 i2 output)
+      (fn
+        (s)
+        (let
+          ((wi1 (mk-walk* i1 s)) (wi2 (mk-walk* i2 s)))
+          (cond
+            ((and (mk-tab-ground-term? wi1) (mk-tab-ground-term? wi2))
+              (let
+                ((key (str name "@3@" wi1 "/" wi2)))
+                (let
+                  ((cached (mk-tab-lookup key)))
+                  (cond
+                    ((= cached :miss)
+                      (let
+                        ((all-substs (stream-take -1 ((rel-fn i1 i2 output) s))))
+                        (let
+                          ((vals (map (fn (s2) (mk-walk* output s2)) all-substs)))
+                          (begin
+                            (mk-tab-store! key vals)
+                            (mk-tab-replay-vals vals output s)))))
+                    (:else (mk-tab-replay-vals cached output s))))))
+            (:else ((rel-fn i1 i2 output) s))))))))

lib/minikanren/tests/appendo3.sx

@@ -0,0 +1,49 @@
+;; lib/minikanren/tests/appendo3.sx — 3-list append.
+
+(mk-test
+  "appendo3-forward"
+  (run*
+    q
+    (appendo3
+      (list 1 2)
+      (list 3 4)
+      (list 5 6)
+      q))
+  (list
+    (list 1 2 3 4 5 6)))
+
+(mk-test
+  "appendo3-empty-everything"
+  (run* q (appendo3 (list) (list) (list) q))
+  (list (list)))
+
+(mk-test
+  "appendo3-recover-middle"
+  (run*
+    q
+    (appendo3
+      (list 1 2)
+      q
+      (list 5 6)
+      (list 1 2 3 4 5 6)))
+  (list (list 3 4)))
+
+(mk-test
+  "appendo3-empty-middle"
+  (run*
+    q
+    (appendo3
+      (list 1 2)
+      (list)
+      (list 3 4)
+      q))
+  (list (list 1 2 3 4)))
+
+(mk-test
+  "appendo3-empty-first-and-last"
+  (run*
+    q
+    (appendo3 (list) (list 1 2 3) (list) q))
+  (list (list 1 2 3)))
+
+(mk-tests-run!)

lib/minikanren/tests/arith-prog.sx

@@ -0,0 +1,33 @@
+;; lib/minikanren/tests/arith-prog.sx — arithmetic progression generation.
+
+(mk-test
+  "arith-progo-zero-len"
+  (run* q (arith-progo 5 1 0 q))
+  (list (list)))
+
+(mk-test
+  "arith-progo-1-to-5"
+  (run* q (arith-progo 1 1 5 q))
+  (list (list 1 2 3 4 5)))
+
+(mk-test
+  "arith-progo-evens-from-0"
+  (run* q (arith-progo 0 2 5 q))
+  (list (list 0 2 4 6 8)))
+
+(mk-test
+  "arith-progo-descending"
+  (run* q (arith-progo 10 -1 4 q))
+  (list (list 10 9 8 7)))
+
+(mk-test
+  "arith-progo-zero-step"
+  (run* q (arith-progo 7 0 3 q))
+  (list (list 7 7 7)))
+
+(mk-test
+  "arith-progo-negative-start"
+  (run* q (arith-progo -3 2 4 q))
+  (list (list -3 -1 1 3)))
+
+(mk-tests-run!)

lib/minikanren/tests/btree-walko.sx

@@ -0,0 +1,54 @@
+;; lib/minikanren/tests/btree-walko.sx — walk a leaves-of-binary-tree relation
+;; using matche dispatch on (:leaf v) and (:node left right) patterns.
+
+(define
+  btree-walko
+  (fn
+    (tree v)
+    (matche
+      tree
+      ((:leaf x) (== v x))
+      ((:node l r) (conde ((btree-walko l v)) ((btree-walko r v)))))))
+
+;; A small test tree: ((1 2) (3 (4 5))).
+(define
+  test-btree
+  (list
+    :node (list :node (list :leaf 1) (list :leaf 2))
+    (list
+      :node (list :leaf 3)
+      (list :node (list :leaf 4) (list :leaf 5)))))
+
+(mk-test
+  "btree-walko-enumerates-all-leaves"
+  (let
+    ((leaves (run* q (btree-walko test-btree q))))
+    (and
+      (= (len leaves) 5)
+      (and
+        (some (fn (l) (= l 1)) leaves)
+        (and
+          (some (fn (l) (= l 2)) leaves)
+          (and
+            (some (fn (l) (= l 3)) leaves)
+            (and
+              (some (fn (l) (= l 4)) leaves)
+              (some (fn (l) (= l 5)) leaves)))))))
+  true)
+
+(mk-test
+  "btree-walko-find-3-membership"
+  (run 1 q (btree-walko test-btree 3))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "btree-walko-find-99-not-present"
+  (run* q (btree-walko test-btree 99))
+  (list))
+
+(mk-test
+  "btree-walko-leaf-only"
+  (run* q (btree-walko (list :leaf 42) q))
+  (list 42))
+
+(mk-tests-run!)

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/clpfd-bounds.sx

@@ -0,0 +1,316 @@
+;; lib/minikanren/tests/clpfd-bounds.sx — Phase 6 piece B: bounds-consistency
+;; for fd-plus and fd-times in the partial- and all-domain cases.
+;;
+;; We probe domains directly (peek at the FD store) before any labelling
+;; happens. This isolates the propagator's narrowing behaviour from the
+;; search engine.
+
+(define
+  probe-dom
+  (fn
+    (goal var-key)
+    (let
+      ((s (first (stream-take 1 (goal empty-s)))))
+      (cond ((= s nil) :no-subst) (:else (fd-domain-of s var-key))))))
+
+;; --- fd-plus partial-domain narrowing ---
+
+(mk-test
+  "fd-plus-vvn-narrows-x"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")))
+    (probe-dom
+      (mk-conj
+        (fd-in
+          x
+          (list
+            1
+            2
+            3
+            4
+            5
+            6
+            7
+            8
+            9
+            10))
+        (fd-in y (list 1 2 3))
+        (fd-plus x y 10))
+      "x"))
+  (list 7 8 9))
+
+(mk-test
+  "fd-plus-vvn-narrows-y"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")))
+    (probe-dom
+      (mk-conj
+        (fd-in
+          x
+          (list
+            1
+            2
+            3
+            4
+            5
+            6
+            7
+            8
+            9
+            10))
+        (fd-in y (list 1 2 3))
+        (fd-plus x y 10))
+      "y"))
+  (list 1 2 3))
+
+(mk-test
+  "fd-plus-nvv-narrows"
+  (let
+    ((y (mk-var "y")) (z (mk-var "z")))
+    (probe-dom
+      (mk-conj
+        (fd-in y (list 1 2 3))
+        (fd-in
+          z
+          (list
+            1
+            2
+            3
+            4
+            5
+            6
+            7
+            8
+            9
+            10
+            11
+            12
+            13
+            14
+            15
+            16
+            17
+            18
+            19
+            20))
+        (fd-plus 5 y z))
+      "z"))
+  (list 6 7 8))
+
+(mk-test
+  "fd-plus-vvv-narrows-z"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")) (z (mk-var "z")))
+    (probe-dom
+      (mk-conj
+        (fd-in x (list 1 2 3))
+        (fd-in y (list 1 2 3))
+        (fd-in
+          z
+          (list
+            1
+            2
+            3
+            4
+            5
+            6
+            7
+            8
+            9
+            10
+            11
+            12
+            13
+            14
+            15
+            16
+            17
+            18
+            19
+            20))
+        (fd-plus x y z))
+      "z"))
+  (list 2 3 4 5 6))
+
+(mk-test
+  "fd-plus-vvv-narrows-x"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")) (z (mk-var "z")))
+    (probe-dom
+      (mk-conj
+        (fd-in
+          x
+          (list
+            1
+            2
+            3
+            4
+            5
+            6
+            7
+            8
+            9
+            10))
+        (fd-in y (list 1 2 3))
+        (fd-in z (list 5 6 7))
+        (fd-plus x y z))
+      "x"))
+  (list 2 3 4 5 6))
+
+;; --- fd-times partial-domain narrowing (positive domains) ---
+
+(mk-test
+  "fd-times-vvn-narrows"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")))
+    (probe-dom
+      (mk-conj
+        (fd-in
+          x
+          (list
+            1
+            2
+            3
+            4
+            5
+            6))
+        (fd-in
+          y
+          (list
+            1
+            2
+            3
+            4
+            5
+            6))
+        (fd-times x y 12))
+      "x"))
+  (list 2 3 4 5 6))
+
+(mk-test
+  "fd-times-nvv-narrows"
+  (let
+    ((y (mk-var "y")) (z (mk-var "z")))
+    (probe-dom
+      (mk-conj
+        (fd-in y (list 1 2 3 4))
+        (fd-in
+          z
+          (list
+            1
+            2
+            3
+            4
+            5
+            6
+            7
+            8
+            9
+            10
+            11
+            12
+            13
+            14
+            15
+            16
+            17
+            18
+            19
+            20))
+        (fd-times 3 y z))
+      "z"))
+  (list
+    3
+    4
+    5
+    6
+    7
+    8
+    9
+    10
+    11
+    12))
+
+(mk-test
+  "fd-times-vvv-narrows"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")) (z (mk-var "z")))
+    (probe-dom
+      (mk-conj
+        (fd-in x (list 1 2 3))
+        (fd-in y (list 1 2 3))
+        (fd-in
+          z
+          (list
+            1
+            2
+            3
+            4
+            5
+            6
+            7
+            8
+            9
+            10
+            11
+            12
+            13
+            14
+            15
+            16
+            17
+            18
+            19
+            20))
+        (fd-times x y z))
+      "z"))
+  (list
+    1
+    2
+    3
+    4
+    5
+    6
+    7
+    8
+    9))
+
+;; --- bounds force impossible branches to fail early ---
+
+(mk-test
+  "fd-plus-impossible-via-bounds"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")))
+    (probe-dom
+      (mk-conj
+        (fd-in
+          x
+          (list
+            1
+            2
+            3
+            4
+            5
+            6
+            7
+            8
+            9
+            10))
+        (fd-in
+          y
+          (list
+            1
+            2
+            3
+            4
+            5
+            6
+            7
+            8
+            9
+            10))
+        (fd-plus x y 100))
+      "x"))
+  :no-subst)
+
+(mk-tests-run!)

lib/minikanren/tests/clpfd-distinct.sx

@@ -0,0 +1,52 @@
+;; lib/minikanren/tests/clpfd-distinct.sx — fd-distinct (alldifferent).
+
+(mk-test
+  "fd-distinct-empty"
+  (run* q (fd-distinct (list)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "fd-distinct-singleton"
+  (run* q (fd-distinct (list 5)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "fd-distinct-pair-distinct"
+  (run* q (fd-distinct (list 1 2)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "fd-distinct-pair-equal-fails"
+  (run* q (fd-distinct (list 5 5)))
+  (list))
+
+(mk-test
+  "fd-distinct-3-perms-of-3"
+  (let
+    ((res (run* q (fresh (a b c) (fd-in a (list 1 2 3)) (fd-in b (list 1 2 3)) (fd-in c (list 1 2 3)) (fd-distinct (list a b c)) (fd-label (list a b c)) (== q (list a b c))))))
+    (= (len res) 6))
+  true)
+
+(mk-test
+  "fd-distinct-4-perms-of-4-count"
+  (let
+    ((res (run* q (fresh (a b c d) (fd-in a (list 1 2 3 4)) (fd-in b (list 1 2 3 4)) (fd-in c (list 1 2 3 4)) (fd-in d (list 1 2 3 4)) (fd-distinct (list a b c d)) (fd-label (list a b c d)) (== q (list a b c d))))))
+    (= (len res) 24))
+  true)
+
+(mk-test
+  "fd-distinct-pigeonhole-fails"
+  (run*
+    q
+    (fresh
+      (a b c d)
+      (fd-in a (list 1 2 3))
+      (fd-in b (list 1 2 3))
+      (fd-in c (list 1 2 3))
+      (fd-in d (list 1 2 3))
+      (fd-distinct (list a b c d))
+      (fd-label (list a b c d))
+      (== q (list a b c d))))
+  (list))
+
+(mk-tests-run!)

lib/minikanren/tests/clpfd-domains.sx

@@ -0,0 +1,133 @@
+;; lib/minikanren/tests/clpfd-domains.sx — Phase 6 piece B: domain primitives.
+
+;; --- domain construction ---
+
+(mk-test
+  "fd-dom-from-list-sorts"
+  (fd-dom-from-list
+    (list 3 1 2 1 5))
+  (list 1 2 3 5))
+
+(mk-test "fd-dom-from-list-empty" (fd-dom-from-list (list)) (list))
+
+(mk-test
+  "fd-dom-from-list-single"
+  (fd-dom-from-list (list 7))
+  (list 7))
+
+(mk-test
+  "fd-dom-range-1-5"
+  (fd-dom-range 1 5)
+  (list 1 2 3 4 5))
+
+(mk-test "fd-dom-range-empty" (fd-dom-range 5 1) (list))
+
+;; --- predicates ---
+
+(mk-test "fd-dom-empty-yes" (fd-dom-empty? (list)) true)
+(mk-test "fd-dom-empty-no" (fd-dom-empty? (list 1)) false)
+(mk-test "fd-dom-singleton-yes" (fd-dom-singleton? (list 5)) true)
+(mk-test
+  "fd-dom-singleton-multi"
+  (fd-dom-singleton? (list 1 2))
+  false)
+(mk-test "fd-dom-singleton-empty" (fd-dom-singleton? (list)) false)
+
+(mk-test
+  "fd-dom-min"
+  (fd-dom-min (list 3 7 9))
+  3)
+(mk-test
+  "fd-dom-max"
+  (fd-dom-max (list 3 7 9))
+  9)
+
+(mk-test
+  "fd-dom-member-yes"
+  (fd-dom-member?
+    3
+    (list 1 2 3 4))
+  true)
+(mk-test
+  "fd-dom-member-no"
+  (fd-dom-member?
+    9
+    (list 1 2 3 4))
+  false)
+
+;; --- intersect / without ---
+
+(mk-test
+  "fd-dom-intersect"
+  (fd-dom-intersect
+    (list 1 2 3 4 5)
+    (list 2 4 6))
+  (list 2 4))
+
+(mk-test
+  "fd-dom-intersect-disjoint"
+  (fd-dom-intersect
+    (list 1 2 3)
+    (list 4 5 6))
+  (list))
+
+(mk-test
+  "fd-dom-intersect-empty"
+  (fd-dom-intersect (list) (list 1 2 3))
+  (list))
+
+(mk-test
+  "fd-dom-intersect-equal"
+  (fd-dom-intersect
+    (list 1 2 3)
+    (list 1 2 3))
+  (list 1 2 3))
+
+(mk-test
+  "fd-dom-without-mid"
+  (fd-dom-without
+    3
+    (list 1 2 3 4 5))
+  (list 1 2 4 5))
+
+(mk-test
+  "fd-dom-without-missing"
+  (fd-dom-without 9 (list 1 2 3))
+  (list 1 2 3))
+
+(mk-test
+  "fd-dom-without-min"
+  (fd-dom-without 1 (list 1 2 3))
+  (list 2 3))
+
+;; --- store accessors ---
+
+(mk-test "fd-domain-of-unset" (fd-domain-of {} "x") nil)
+
+(mk-test
+  "fd-domain-of-set"
+  (let
+    ((s (fd-set-domain {} "x" (list 1 2 3))))
+    (fd-domain-of s "x"))
+  (list 1 2 3))
+
+(mk-test
+  "fd-set-domain-empty-fails"
+  (fd-set-domain {} "x" (list))
+  nil)
+
+(mk-test
+  "fd-set-domain-overrides"
+  (let
+    ((s (fd-set-domain {} "x" (list 1 2 3))))
+    (fd-domain-of (fd-set-domain s "x" (list 5)) "x"))
+  (list 5))
+
+(mk-test
+  "fd-set-domain-multiple-vars"
+  (let
+    ((s (fd-set-domain (fd-set-domain {} "x" (list 1)) "y" (list 2 3))))
+    (list (fd-domain-of s "x") (fd-domain-of s "y")))
+  (list (list 1) (list 2 3)))
+
+(mk-tests-run!)

lib/minikanren/tests/clpfd-in-label.sx

@@ -0,0 +1,120 @@
+;; lib/minikanren/tests/clpfd-in-label.sx — fd-in (domain narrowing) + fd-label.
+
+;; --- fd-in: domain narrowing ---
+
+(mk-test
+  "fd-in-bare-label"
+  (run*
+    q
+    (fresh
+      (x)
+      (fd-in x (list 1 2 3 4 5))
+      (fd-label (list x))
+      (== q x)))
+  (list 1 2 3 4 5))
+
+(mk-test
+  "fd-in-intersection"
+  (run*
+    q
+    (fresh
+      (x)
+      (fd-in x (list 1 2 3 4 5))
+      (fd-in x (list 3 4 5 6 7))
+      (fd-label (list x))
+      (== q x)))
+  (list 3 4 5))
+
+(mk-test
+  "fd-in-disjoint-empty"
+  (run*
+    q
+    (fresh
+      (x)
+      (fd-in x (list 1 2 3))
+      (fd-in x (list 7 8 9))
+      (fd-label (list x))
+      (== q x)))
+  (list))
+
+(mk-test
+  "fd-in-singleton-domain"
+  (run*
+    q
+    (fresh (x) (fd-in x (list 5)) (fd-label (list x)) (== q x)))
+  (list 5))
+
+;; --- ground value checks the domain ---
+
+(mk-test
+  "fd-in-ground-in-domain"
+  (run*
+    q
+    (fresh
+      (x)
+      (== x 3)
+      (fd-in x (list 1 2 3 4 5))
+      (== q x)))
+  (list 3))
+
+(mk-test
+  "fd-in-ground-not-in-domain"
+  (run*
+    q
+    (fresh
+      (x)
+      (== x 9)
+      (fd-in x (list 1 2 3 4 5))
+      (== q x)))
+  (list))
+
+;; --- fd-label across multiple vars ---
+
+(mk-test
+  "fd-label-multiple-vars"
+  (let
+    ((res (run* q (fresh (a b) (fd-in a (list 1 2 3)) (fd-in b (list 10 20)) (fd-label (list a b)) (== q (list a b))))))
+    (= (len res) 6))
+  true)
+
+(mk-test
+  "fd-label-empty-vars"
+  (run* q (fd-label (list)))
+  (list (make-symbol "_.0")))
+
+;; --- composition with regular goals ---
+
+(mk-test
+  "fd-in-with-membero-style-filtering"
+  (run*
+    q
+    (fresh
+      (x)
+      (fd-in
+        x
+        (list
+          1
+          2
+          3
+          4
+          5
+          6
+          7
+          8
+          9
+          10))
+      (fd-label (list x))
+      (== q x)))
+  (list
+    1
+    2
+    3
+    4
+    5
+    6
+    7
+    8
+    9
+    10))
+
+(mk-tests-run!)

lib/minikanren/tests/clpfd-neq.sx

@@ -0,0 +1,82 @@
+;; lib/minikanren/tests/clpfd-neq.sx — fd-neq with constraint propagation.
+
+;; --- ground / domain interaction ---
+
+(mk-test
+  "fd-neq-ground-distinct"
+  (run*
+    q
+    (fresh
+      (x)
+      (fd-neq x 5)
+      (fd-in x (list 4 5 6))
+      (fd-label (list x))
+      (== q x)))
+  (list 4 6))
+
+(mk-test
+  "fd-neq-ground-equal-fails"
+  (run* q (fresh (x) (== x 5) (fd-neq x 5) (== q x)))
+  (list))
+
+(mk-test
+  "fd-neq-symmetric"
+  (run*
+    q
+    (fresh
+      (x)
+      (fd-neq 7 x)
+      (fd-in x (list 5 6 7 8 9))
+      (fd-label (list x))
+      (== q x)))
+  (list 5 6 8 9))
+
+;; --- two vars with overlapping domains ---
+
+(mk-test
+  "fd-neq-pair-from-3"
+  (let
+    ((res (run* q (fresh (x y) (fd-in x (list 1 2 3)) (fd-in y (list 1 2 3)) (fd-neq x y) (fd-label (list x y)) (== q (list x y))))))
+    (= (len res) 6))
+  true)
+
+(mk-test
+  "fd-all-distinct-3-of-3"
+  (let
+    ((res (run* q (fresh (a b c) (fd-in a (list 1 2 3)) (fd-in b (list 1 2 3)) (fd-in c (list 1 2 3)) (fd-neq a b) (fd-neq a c) (fd-neq b c) (fd-label (list a b c)) (== q (list a b c))))))
+    (= (len res) 6))
+  true)
+
+(mk-test
+  "fd-pigeonhole-fails"
+  (run*
+    q
+    (fresh
+      (a b c)
+      (fd-in a (list 1 2))
+      (fd-in b (list 1 2))
+      (fd-in c (list 1 2))
+      (fd-neq a b)
+      (fd-neq a c)
+      (fd-neq b c)
+      (fd-label (list a b c))
+      (== q (list a b c))))
+  (list))
+
+;; --- propagation when one side becomes ground ---
+
+(mk-test
+  "fd-neq-propagates-after-ground"
+  (run*
+    q
+    (fresh
+      (x y)
+      (fd-in x (list 1 2 3))
+      (fd-in y (list 1 2 3))
+      (fd-neq x y)
+      (== x 2)
+      (fd-label (list y))
+      (== q y)))
+  (list 1 3))
+
+(mk-tests-run!)

lib/minikanren/tests/clpfd-ord.sx

@@ -0,0 +1,128 @@
+;; lib/minikanren/tests/clpfd-ord.sx — fd-lt / fd-lte / fd-eq.
+
+;; --- fd-lt ---
+
+(mk-test
+  "fd-lt-narrows-x-against-num"
+  (run*
+    q
+    (fresh
+      (x)
+      (fd-in x (list 1 2 3 4 5))
+      (fd-lt x 3)
+      (fd-label (list x))
+      (== q x)))
+  (list 1 2))
+
+(mk-test
+  "fd-lt-narrows-x-against-num-symmetric"
+  (run*
+    q
+    (fresh
+      (x)
+      (fd-in x (list 1 2 3 4 5))
+      (fd-lt 3 x)
+      (fd-label (list x))
+      (== q x)))
+  (list 4 5))
+
+(mk-test
+  "fd-lt-pair-ordered"
+  (let
+    ((res (run* q (fresh (x y) (fd-in x (list 1 2 3 4)) (fd-in y (list 1 2 3 4)) (fd-lt x y) (fd-label (list x y)) (== q (list x y))))))
+    (= (len res) 6))
+  true)
+
+(mk-test
+  "fd-lt-impossible-fails"
+  (run*
+    q
+    (fresh
+      (x)
+      (fd-in x (list 5 6 7))
+      (fd-lt x 3)
+      (fd-label (list x))
+      (== q x)))
+  (list))
+
+;; --- fd-lte ---
+
+(mk-test
+  "fd-lte-includes-equal"
+  (run*
+    q
+    (fresh
+      (x)
+      (fd-in x (list 1 2 3 4 5))
+      (fd-lte x 3)
+      (fd-label (list x))
+      (== q x)))
+  (list 1 2 3))
+
+(mk-test
+  "fd-lte-equal-bound"
+  (run*
+    q
+    (fresh
+      (x)
+      (fd-in x (list 1 2 3 4 5))
+      (fd-lte 3 x)
+      (fd-label (list x))
+      (== q x)))
+  (list 3 4 5))
+
+;; --- fd-eq ---
+
+(mk-test
+  "fd-eq-bind"
+  (run*
+    q
+    (fresh
+      (x)
+      (fd-in x (list 1 2 3 4 5))
+      (fd-eq x 3)
+      (== q x)))
+  (list 3))
+
+(mk-test
+  "fd-eq-out-of-domain-fails"
+  (run*
+    q
+    (fresh
+      (x)
+      (fd-in x (list 1 2 3))
+      (fd-eq x 5)
+      (== q x)))
+  (list))
+
+(mk-test
+  "fd-eq-two-vars-share-domain"
+  (run*
+    q
+    (fresh
+      (x y)
+      (fd-in x (list 1 2 3))
+      (fd-in y (list 2 3 4))
+      (fd-eq x y)
+      (fd-label (list x y))
+      (== q (list x y))))
+  (list (list 2 2) (list 3 3)))
+
+;; --- combine fd-lt + fd-neq for "between" puzzle ---
+
+(mk-test
+  "fd-lt-neq-combined"
+  (run*
+    q
+    (fresh
+      (x y z)
+      (fd-in x (list 1 2 3))
+      (fd-in y (list 1 2 3))
+      (fd-in z (list 1 2 3))
+      (fd-lt x y)
+      (fd-lt y z)
+      (fd-label (list x y z))
+      (== q (list x y z))))
+  (list (list 1 2 3)))
+
+(mk-tests-run!)

lib/minikanren/tests/clpfd-plus.sx

@@ -0,0 +1,62 @@
+;; lib/minikanren/tests/clpfd-plus.sx — fd-plus (x + y = z).
+
+(mk-test
+  "fd-plus-all-ground"
+  (run* q (fresh (z) (fd-plus 2 3 z) (== q z)))
+  (list 5))
+
+(mk-test
+  "fd-plus-recover-x"
+  (run* q (fresh (x) (fd-plus x 3 5) (== q x)))
+  (list 2))
+
+(mk-test
+  "fd-plus-recover-y"
+  (run* q (fresh (y) (fd-plus 2 y 5) (== q y)))
+  (list 3))
+
+(mk-test
+  "fd-plus-impossible-fails"
+  (run*
+    q
+    (fresh
+      (z)
+      (fd-plus 2 3 z)
+      (== z 99)
+      (== q z)))
+  (list))
+
+(mk-test
+  "fd-plus-domain-check"
+  (run*
+    q
+    (fresh
+      (x)
+      (fd-in x (list 3 4 5))
+      (fd-plus x 3 5)
+      (== q x)))
+  (list))
+
+(mk-test
+  "fd-plus-pairs-summing-to-5"
+  (run*
+    q
+    (fresh
+      (x y)
+      (fd-in x (list 1 2 3 4))
+      (fd-in y (list 1 2 3 4))
+      (fd-plus x y 5)
+      (fd-label (list x y))
+      (== q (list x y))))
+  (list
+    (list 1 4)
+    (list 2 3)
+    (list 3 2)
+    (list 4 1)))
+
+(mk-test
+  "fd-plus-z-derived"
+  (run* q (fresh (z) (fd-plus 7 8 z) (== q z)))
+  (list 15))
+
+(mk-tests-run!)

lib/minikanren/tests/clpfd-times.sx

@@ -0,0 +1,85 @@
+;; lib/minikanren/tests/clpfd-times.sx — fd-times (x * y = z).
+
+(mk-test
+  "fd-times-3-4"
+  (run* q (fresh (z) (fd-times 3 4 z) (== q z)))
+  (list 12))
+
+(mk-test
+  "fd-times-recover-divisor"
+  (run* q (fresh (x) (fd-times x 5 30) (== q x)))
+  (list 6))
+
+(mk-test
+  "fd-times-non-divisible-fails"
+  (run* q (fresh (x) (fd-times x 5 31) (== q x)))
+  (list))
+
+(mk-test
+  "fd-times-by-zero"
+  (run* q (fresh (z) (fd-times 0 99 z) (== q z)))
+  (list 0))
+
+(mk-test
+  "fd-times-zero-by-anything-zero"
+  (run*
+    q
+    (fresh
+      (x)
+      (fd-in x (list 1 2 3))
+      (fd-times x 0 0)
+      (fd-label (list x))
+      (== q x)))
+  (list 1 2 3))
+
+(mk-test
+  "fd-times-12-divisor-pairs"
+  (run*
+    q
+    (fresh
+      (x y)
+      (fd-in
+        x
+        (list
+          1
+          2
+          3
+          4
+          5
+          6))
+      (fd-in
+        y
+        (list
+          1
+          2
+          3
+          4
+          5
+          6))
+      (fd-times x y 12)
+      (fd-label (list x y))
+      (== q (list x y))))
+  (list
+    (list 2 6)
+    (list 3 4)
+    (list 4 3)
+    (list 6 2)))
+
+(mk-test
+  "fd-times-square-of-each"
+  (run*
+    q
+    (fresh
+      (x z)
+      (fd-in x (list 1 2 3 4 5))
+      (fd-times x x z)
+      (fd-label (list x))
+      (== q (list x z))))
+  (list
+    (list 1 1)
+    (list 2 4)
+    (list 3 9)
+    (list 4 16)
+    (list 5 25)))
+
+(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/counto.sx

@@ -0,0 +1,35 @@
+;; lib/minikanren/tests/counto.sx — count occurrences of x in l (intarith).
+
+(mk-test
+  "counto-empty"
+  (run* q (counto 1 (list) q))
+  (list 0))
+(mk-test
+  "counto-not-found"
+  (run* q (counto 99 (list 1 2 3) q))
+  (list 0))
+(mk-test
+  "counto-once"
+  (run* q (counto 2 (list 1 2 3) q))
+  (list 1))
+(mk-test
+  "counto-thrice"
+  (run*
+    q
+    (counto
+      1
+      (list 1 2 1 3 1)
+      q))
+  (list 3))
+(mk-test
+  "counto-all-same"
+  (run*
+    q
+    (counto 7 (list 7 7 7 7) q))
+  (list 4))
+(mk-test
+  "counto-string"
+  (run* q (counto "x" (list "x" "y" "x") q))
+  (list 2))
+
+(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/defrel.sx

@@ -0,0 +1,40 @@
+;; lib/minikanren/tests/defrel.sx — Prolog-style relation definition macro.
+
+(defrel
+  (my-membero x l)
+  ((fresh (d) (conso x d l)))
+  ((fresh (a d) (conso a d l) (my-membero x d))))
+
+(mk-test
+  "defrel-defines-membero"
+  (run* q (my-membero q (list 1 2 3)))
+  (list 1 2 3))
+
+(defrel
+  (my-listo l)
+  ((nullo l))
+  ((fresh (a d) (conso a d l) (my-listo d))))
+
+(mk-test
+  "defrel-listo-bounded"
+  (run 3 q (my-listo q))
+  (list
+    (list)
+    (list (make-symbol "_.0"))
+    (list (make-symbol "_.0") (make-symbol "_.1"))))
+
+;; Multi-arg relation with arithmetic.
+
+(defrel
+  (my-pluso a b c)
+  ((== a :z) (== b c))
+  ((fresh (a-1 c-1) (== a (list :s a-1)) (== c (list :s c-1)) (my-pluso a-1 b c-1))))
+
+(mk-test
+  "defrel-pluso-2-3"
+  (run*
+    q
+    (my-pluso (list :s (list :s :z)) (list :s (list :s (list :s :z))) q))
+  (list (list :s (list :s (list :s (list :s (list :s :z)))))))
+
+(mk-tests-run!)

lib/minikanren/tests/diseq.sx

@@ -0,0 +1,83 @@
+;; lib/minikanren/tests/diseq.sx — Phase 5 polish: =/= disequality.
+
+;; --- ground cases ---
+
+(mk-test
+  "=/=-ground-distinct"
+  (run* q (=/= 1 2))
+  (list (make-symbol "_.0")))
+(mk-test "=/=-ground-equal" (run* q (=/= 1 1)) (list))
+(mk-test
+  "=/=-ground-strings"
+  (run* q (=/= "a" "b"))
+  (list (make-symbol "_.0")))
+(mk-test "=/=-ground-strings-eq" (run* q (=/= "a" "a")) (list))
+
+;; --- structural ---
+
+(mk-test
+  "=/=-pair-distinct"
+  (run* q (=/= (list 1 2) (list 1 3)))
+  (list (make-symbol "_.0")))
+(mk-test
+  "=/=-pair-equal"
+  (run* q (=/= (list 1 2) (list 1 2)))
+  (list))
+(mk-test
+  "=/=-pair-vs-atom"
+  (run* q (=/= (list 1) 1))
+  (list (make-symbol "_.0")))
+
+;; --- partial / late binding ---
+;;
+;; ==-cs is required to wake up the constraint store after a binding;
+;; plain == doesn't fire constraints.
+
+(mk-test
+  "=/=-late-bind-violates"
+  (run* q (fresh (x) (=/= x 5) (==-cs x 5) (== q x)))
+  (list))
+
+(mk-test
+  "=/=-late-bind-ok"
+  (run* q (fresh (x) (=/= x 5) (==-cs x 7) (== q x)))
+  (list 7))
+
+(mk-test
+  "=/=-two-vars-equal-late-fails"
+  (run*
+    q
+    (fresh
+      (x y)
+      (=/= x y)
+      (==-cs x 1)
+      (==-cs y 1)
+      (== q (list x y))))
+  (list))
+
+(mk-test
+  "=/=-two-vars-distinct-late"
+  (run*
+    q
+    (fresh
+      (x y)
+      (=/= x y)
+      (==-cs x 1)
+      (==-cs y 2)
+      (== q (list x y))))
+  (list (list 1 2)))
+
+;; --- compose with conde / fresh ---
+
+(mk-test
+  "=/=-with-membero-filter"
+  (run*
+    q
+    (fresh
+      (x)
+      (membero x (list 1 2 3))
+      (=/= x 2)
+      (== q x)))
+  (list 1 3))
+
+(mk-tests-run!)

lib/minikanren/tests/enumerate.sx

@@ -0,0 +1,31 @@
+;; lib/minikanren/tests/enumerate.sx — index-each-element relation.
+
+(mk-test
+  "enumerate-i-empty"
+  (run* q (enumerate-i (list) q))
+  (list (list)))
+
+(mk-test
+  "enumerate-i-three"
+  (run* q (enumerate-i (list :a :b :c) q))
+  (list
+    (list (list 0 :a) (list 1 :b) (list 2 :c))))
+
+(mk-test
+  "enumerate-i-strings"
+  (run* q (enumerate-i (list "x" "y" "z") q))
+  (list
+    (list (list 0 "x") (list 1 "y") (list 2 "z"))))
+
+(mk-test
+  "enumerate-from-i-100"
+  (run* q (enumerate-from-i 100 (list :x :y :z) q))
+  (list
+    (list (list 100 :x) (list 101 :y) (list 102 :z))))
+
+(mk-test
+  "enumerate-from-i-singleton"
+  (run* q (enumerate-from-i 0 (list :only) q))
+  (list (list (list 0 :only))))
+
+(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/flat-mapo.sx

@@ -0,0 +1,39 @@
+;; lib/minikanren/tests/flat-mapo.sx — concatMap-style relation.
+
+(mk-test
+  "flat-mapo-empty"
+  (run* q (flat-mapo (fn (x r) (== r (list x x))) (list) q))
+  (list (list)))
+
+(mk-test
+  "flat-mapo-duplicate-each"
+  (run*
+    q
+    (flat-mapo
+      (fn (x r) (== r (list x x)))
+      (list 1 2 3)
+      q))
+  (list
+    (list 1 1 2 2 3 3)))
+
+(mk-test
+  "flat-mapo-empty-from-each"
+  (run* q (flat-mapo (fn (x r) (== r (list))) (list :a :b :c) q))
+  (list (list)))
+
+(mk-test
+  "flat-mapo-singleton-from-each-is-identity"
+  (run* q (flat-mapo (fn (x r) (== r (list x))) (list :a :b :c) q))
+  (list (list :a :b :c)))
+
+(mk-test
+  "flat-mapo-tag-each"
+  (run*
+    q
+    (flat-mapo
+      (fn (x r) (== r (list :tag x)))
+      (list 1 2)
+      q))
+  (list (list :tag 1 :tag 2)))
+
+(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/foldl-o.sx

@@ -0,0 +1,48 @@
+;; lib/minikanren/tests/foldl-o.sx — relational left fold.
+
+(mk-test
+  "foldl-o-empty"
+  (run* q (foldl-o pluso-i (list) 42 q))
+  (list 42))
+
+(mk-test
+  "foldl-o-sum"
+  (run*
+    q
+    (foldl-o
+      pluso-i
+      (list 1 2 3 4 5)
+      0
+      q))
+  (list 15))
+
+(mk-test
+  "foldl-o-product"
+  (run*
+    q
+    (foldl-o
+      *o-i
+      (list 1 2 3 4)
+      1
+      q))
+  (list 24))
+
+(mk-test
+  "foldl-o-reverse-via-flip-conso"
+  (run*
+    q
+    (foldl-o
+      (fn (acc x r) (conso x acc r))
+      (list 1 2 3 4)
+      (list)
+      q))
+  (list (list 4 3 2 1)))
+
+(mk-test
+  "foldl-o-with-init"
+  (run*
+    q
+    (foldl-o pluso-i (list 1 2 3) 100 q))
+  (list 106))
+
+(mk-tests-run!)

lib/minikanren/tests/foldr-o.sx

@@ -0,0 +1,38 @@
+;; lib/minikanren/tests/foldr-o.sx — relational right fold.
+
+(mk-test
+  "foldr-o-empty"
+  (run* q (foldr-o conso (list) (list 99) q))
+  (list (list 99)))
+
+(mk-test
+  "foldr-o-conso-rebuilds-list"
+  (run* q (foldr-o conso (list 1 2 3) (list) q))
+  (list (list 1 2 3)))
+
+(mk-test
+  "foldr-o-appendo-flattens"
+  (run*
+    q
+    (foldr-o
+      appendo
+      (list
+        (list 1 2)
+        (list 3)
+        (list 4 5))
+      (list)
+      q))
+  (list (list 1 2 3 4 5)))
+
+(mk-test
+  "foldr-o-with-acc-init"
+  (run*
+    q
+    (foldr-o
+      conso
+      (list 1 2)
+      (list 9 9)
+      q))
+  (list (list 1 2 9 9)))
+
+(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,103 @@
+;; 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-test "even-i-pos" (run* q (even-i 4)) (list (make-symbol "_.0")))
+
+(mk-test "even-i-neg" (run* q (even-i 5)) (list))
+
+(mk-test "odd-i-pos" (run* q (odd-i 7)) (list (make-symbol "_.0")))
+
+(mk-test "odd-i-neg" (run* q (odd-i 4)) (list))
+
+(mk-test
+  "even-i-filter"
+  (run* q (fresh (x) (membero x (list 1 2 3 4 5 6)) (even-i x) (== q x)))
+  (list 2 4 6))
+
+(mk-tests-run!)
+

lib/minikanren/tests/iterate-no.sx

@@ -0,0 +1,38 @@
+;; lib/minikanren/tests/iterate-no.sx — iterated relation application.
+
+(define
+  mk-nat
+  (fn (n) (if (= n 0) :z (list :s (mk-nat (- n 1))))))
+
+(mk-test
+  "iterate-no-zero"
+  (run*
+    q
+    (iterate-no
+      (fn (a b) (== b (list :wrap a)))
+      (mk-nat 0)
+      :seed q))
+  (list :seed))
+
+(mk-test
+  "iterate-no-three-wraps"
+  (run*
+    q
+    (iterate-no (fn (a b) (== b (list :wrap a))) (mk-nat 3) :x q))
+  (list (list :wrap (list :wrap (list :wrap :x)))))
+
+(mk-test
+  "iterate-no-succ-three-times"
+  (run*
+    q
+    (iterate-no (fn (a b) (== b (list :s a))) (mk-nat 3) :z q))
+  (list (mk-nat 3)))
+
+(mk-test
+  "iterate-no-with-list-cons"
+  (run*
+    q
+    (iterate-no (fn (a b) (conso :a a b)) (mk-nat 4) (list) q))
+  (list (list :a :a :a :a)))
+
+(mk-tests-run!)

lib/minikanren/tests/lasto.sx

@@ -0,0 +1,38 @@
+;; lib/minikanren/tests/lasto.sx — last-element + init-without-last.
+
+(mk-test
+  "lasto-singleton"
+  (run* q (lasto (list 5) q))
+  (list 5))
+(mk-test
+  "lasto-multi"
+  (run* q (lasto (list 1 2 3 4) q))
+  (list 4))
+(mk-test "lasto-empty" (run* q (lasto (list) q)) (list))
+
+(mk-test "lasto-strings" (run* q (lasto (list "a" "b" "c") q)) (list "c"))
+
+(mk-test
+  "init-o-multi"
+  (run* q (init-o (list 1 2 3 4) q))
+  (list (list 1 2 3)))
+
+(mk-test
+  "init-o-singleton"
+  (run* q (init-o (list 7) q))
+  (list (list)))
+
+(mk-test "init-o-empty" (run* q (init-o (list) q)) (list))
+
+(mk-test
+  "lasto-init-o-roundtrip"
+  (run*
+    q
+    (fresh
+      (init last)
+      (lasto (list 1 2 3 4) last)
+      (init-o (list 1 2 3 4) init)
+      (appendo init (list last) q)))
+  (list (list 1 2 3 4)))
+
+(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/lengtho-i.sx

@@ -0,0 +1,28 @@
+;; lib/minikanren/tests/lengtho-i.sx — integer-indexed length (fast).
+
+(mk-test "lengtho-i-empty" (run* q (lengtho-i (list) q)) (list 0))
+(mk-test
+  "lengtho-i-singleton"
+  (run* q (lengtho-i (list :a) q))
+  (list 1))
+(mk-test
+  "lengtho-i-three"
+  (run* q (lengtho-i (list 1 2 3) q))
+  (list 3))
+(mk-test
+  "lengtho-i-five"
+  (run*
+    q
+    (lengtho-i
+      (list 1 2 3 4 5)
+      q))
+  (list 5))
+
+(mk-test
+  "lengtho-i-mixed-types"
+  (run*
+    q
+    (lengtho-i (list 1 "two" :three (list 4 5)) q))
+  (list 4))
+
+(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/minmax.sx

@@ -0,0 +1,49 @@
+;; lib/minikanren/tests/minmax.sx — mino + maxo via intarith.
+
+(mk-test
+  "mino-singleton"
+  (run* q (mino (list 7) q))
+  (list 7))
+(mk-test
+  "mino-of-3"
+  (run* q (mino (list 5 1 3) q))
+  (list 1))
+(mk-test
+  "mino-of-5"
+  (run*
+    q
+    (mino (list 5 1 3 2 4) q))
+  (list 1))
+(mk-test
+  "mino-with-dups"
+  (run* q (mino (list 3 3 3) q))
+  (list 3))
+(mk-test "mino-empty-fails" (run* q (mino (list) q)) (list))
+
+(mk-test
+  "maxo-singleton"
+  (run* q (maxo (list 7) q))
+  (list 7))
+(mk-test
+  "maxo-of-5"
+  (run*
+    q
+    (maxo (list 5 1 3 2 4) q))
+  (list 5))
+(mk-test
+  "maxo-of-negs"
+  (run* q (maxo (list -5 -1 -3) q))
+  (list -1))
+
+(mk-test
+  "min-and-max-of-list"
+  (run*
+    q
+    (fresh
+      (mn mx)
+      (mino (list 5 1 3 2 4) mn)
+      (maxo (list 5 1 3 2 4) mx)
+      (== q (list mn mx))))
+  (list (list 1 5)))
+
+(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/not-membero.sx

@@ -0,0 +1,29 @@
+;; lib/minikanren/tests/not-membero.sx — relational "not in list".
+
+(mk-test
+  "not-membero-absent"
+  (run* q (not-membero 99 (list 1 2 3)))
+  (list (make-symbol "_.0")))
+(mk-test
+  "not-membero-present"
+  (run* q (not-membero 2 (list 1 2 3)))
+  (list))
+(mk-test
+  "not-membero-empty"
+  (run* q (not-membero 1 (list)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "not-membero-as-filter"
+  (run*
+    q
+    (fresh
+      (x)
+      (membero
+        x
+        (list 1 2 3 4 5))
+      (not-membero x (list 2 4))
+      (== q x)))
+  (list 1 3 5))
+
+(mk-tests-run!)

lib/minikanren/tests/nub-o.sx

@@ -0,0 +1,31 @@
+;; lib/minikanren/tests/nub-o.sx — relational dedupe (keep last occurrence).
+
+(mk-test "nub-o-empty" (run* q (nub-o (list) q)) (list (list)))
+
+(mk-test
+  "nub-o-no-duplicates"
+  (run* q (nub-o (list 1 2 3) q))
+  (list (list 1 2 3)))
+
+(mk-test
+  "nub-o-with-duplicates"
+  (run*
+    q
+    (nub-o
+      (list 1 2 1 3 2 4)
+      q))
+  (list (list 1 3 2 4)))
+
+(mk-test
+  "nub-o-all-same"
+  (let
+    ((res (run* q (nub-o (list 1 1 1) q))))
+    (every? (fn (r) (= r (list 1))) res))
+  true)
+
+(mk-test
+  "nub-o-keeps-last"
+  (run* q (nub-o (list 1 2 1) q))
+  (list (list 2 1)))
+
+(mk-tests-run!)

lib/minikanren/tests/pairlisto.sx

@@ -0,0 +1,41 @@
+;; lib/minikanren/tests/pairlisto.sx — zip two lists into pair list.
+
+(mk-test
+  "pairlisto-empty"
+  (run* q (pairlisto (list) (list) q))
+  (list (list)))
+
+(mk-test
+  "pairlisto-equal-lengths"
+  (run*
+    q
+    (pairlisto (list 1 2 3) (list :a :b :c) q))
+  (list
+    (list (list 1 :a) (list 2 :b) (list 3 :c))))
+
+(mk-test
+  "pairlisto-recover-l1"
+  (run*
+    q
+    (pairlisto
+      q
+      (list :a :b :c)
+      (list (list 10 :a) (list 20 :b) (list 30 :c))))
+  (list (list 10 20 30)))
+
+(mk-test
+  "pairlisto-recover-l2"
+  (run*
+    q
+    (pairlisto
+      (list 1 2 3)
+      q
+      (list (list 1 :x) (list 2 :y) (list 3 :z))))
+  (list (list :x :y :z)))
+
+(mk-test
+  "pairlisto-different-lengths-fails"
+  (run* q (pairlisto (list 1 2) (list :a :b :c) q))
+  (list))
+
+(mk-tests-run!)

lib/minikanren/tests/palindromeo.sx

@@ -0,0 +1,44 @@
+;; lib/minikanren/tests/palindromeo.sx — palindromic list relation.
+
+(mk-test
+  "palindromeo-empty"
+  (run* q (palindromeo (list)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "palindromeo-singleton"
+  (run* q (palindromeo (list :a)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "palindromeo-pair-equal"
+  (run* q (palindromeo (list 1 1)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "palindromeo-pair-unequal-fails"
+  (run* q (palindromeo (list 1 2)))
+  (list))
+
+(mk-test
+  "palindromeo-five-yes"
+  (run*
+    q
+    (palindromeo
+      (list 1 2 3 2 1)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "palindromeo-five-no"
+  (run*
+    q
+    (palindromeo
+      (list 1 2 3 4 5)))
+  (list))
+
+(mk-test
+  "palindromeo-strings"
+  (run* q (palindromeo (list "a" "b" "a")))
+  (list (make-symbol "_.0")))
+
+(mk-tests-run!)

lib/minikanren/tests/parity.sx

@@ -0,0 +1,58 @@
+;; lib/minikanren/tests/parity.sx — eveno + oddo Peano predicates.
+
+(define
+  mk-nat
+  (fn (n) (if (= n 0) :z (list :s (mk-nat (- n 1))))))
+
+(mk-test "eveno-zero" (run* q (eveno :z)) (list (make-symbol "_.0")))
+(mk-test
+  "eveno-2"
+  (run* q (eveno (mk-nat 2)))
+  (list (make-symbol "_.0")))
+(mk-test
+  "eveno-4"
+  (run* q (eveno (mk-nat 4)))
+  (list (make-symbol "_.0")))
+(mk-test "eveno-1-fails" (run* q (eveno (mk-nat 1))) (list))
+(mk-test "eveno-3-fails" (run* q (eveno (mk-nat 3))) (list))
+
+(mk-test
+  "oddo-1"
+  (run* q (oddo (mk-nat 1)))
+  (list (make-symbol "_.0")))
+(mk-test
+  "oddo-3"
+  (run* q (oddo (mk-nat 3)))
+  (list (make-symbol "_.0")))
+(mk-test "oddo-zero-fails" (run* q (oddo :z)) (list))
+(mk-test "oddo-2-fails" (run* q (oddo (mk-nat 2))) (list))
+
+;; Enumerate small evens.
+(mk-test
+  "eveno-enumerates"
+  (run 4 q (eveno q))
+  (list
+    (mk-nat 0)
+    (mk-nat 2)
+    (mk-nat 4)
+    (mk-nat 6)))
+
+;; Enumerate small odds.
+(mk-test
+  "oddo-enumerates"
+  (run 4 q (oddo q))
+  (list
+    (mk-nat 1)
+    (mk-nat 3)
+    (mk-nat 5)
+    (mk-nat 7)))
+
+;; A number is even XOR odd (no overlap).
+(mk-test
+  "even-odd-no-overlap"
+  (run*
+    q
+    (mk-conj (eveno (mk-nat 4)) (oddo (mk-nat 4))))
+  (list))
+
+(mk-tests-run!)

lib/minikanren/tests/partitiono.sx

@@ -0,0 +1,75 @@
+;; lib/minikanren/tests/partitiono.sx — partition list by predicate.
+
+(mk-test
+  "partitiono-empty"
+  (run*
+    q
+    (fresh
+      (yes no)
+      (partitiono (fn (x) (== x 1)) (list) yes no)
+      (== q (list yes no))))
+  (list (list (list) (list))))
+
+(mk-test
+  "partitiono-by-equality"
+  (run*
+    q
+    (fresh
+      (yes no)
+      (partitiono
+        (fn (x) (== x 2))
+        (list 1 2 3 2 4)
+        yes
+        no)
+      (== q (list yes no))))
+  (list
+    (list
+      (list 2 2)
+      (list 1 3 4))))
+
+(mk-test
+  "partitiono-by-numeric-pred"
+  (run*
+    q
+    (fresh
+      (yes no)
+      (partitiono
+        (fn (x) (lto-i x 5))
+        (list 1 7 2 8 3)
+        yes
+        no)
+      (== q (list yes no))))
+  (list
+    (list
+      (list 1 2 3)
+      (list 7 8))))
+
+(mk-test
+  "partitiono-all-yes"
+  (run*
+    q
+    (fresh
+      (yes no)
+      (partitiono
+        (fn (x) (lto-i x 100))
+        (list 1 2 3)
+        yes
+        no)
+      (== q (list yes no))))
+  (list (list (list 1 2 3) (list))))
+
+(mk-test
+  "partitiono-all-no"
+  (run*
+    q
+    (fresh
+      (yes no)
+      (partitiono
+        (fn (x) (lto-i 100 x))
+        (list 1 2 3)
+        yes
+        no)
+      (== q (list yes no))))
+  (list (list (list) (list 1 2 3))))
+
+(mk-tests-run!)

lib/minikanren/tests/path-cycle-free.sx

@@ -0,0 +1,40 @@
+;; lib/minikanren/tests/path-cycle-free.sx — cycle-free reachability search.
+;;
+;; Threads a "visited" accumulator through the recursion, using nafc +
+;; membero to prevent revisiting nodes. Demonstrates how to make the
+;; cyclic-graph divergence problem (see tests/cyclic-graph.sx) tractable
+;; for graphs with cycles, without invoking Phase-7 tabling.
+
+(define
+  cf-edges
+  (list (list :a :b) (list :b :a) (list :b :c) (list :c :d) (list :d :a)))      ; another cycle
+
+(define cf-edgeo (fn (from to) (membero (list from to) cf-edges)))
+
+(define
+  patho-no-cycles
+  (fn
+    (x y visited path)
+    (conde
+      ((cf-edgeo x y) (nafc (membero y visited)) (== path (list x y)))
+      ((fresh (z mid v-prime) (cf-edgeo x z) (nafc (membero z visited)) (conso z visited v-prime) (patho-no-cycles z y v-prime mid) (conso x mid path))))))
+
+(define cf-patho (fn (x y path) (patho-no-cycles x y (list x) path)))
+
+(mk-test
+  "cycle-free-finds-finitely"
+  (let
+    ((paths (run* q (cf-patho :a :d q))))
+    (and
+      (>= (len paths) 1)
+      (every? (fn (p) (and (= (first p) :a) (= (last p) :d))) paths)))
+  true)
+
+(mk-test
+  "cycle-free-direct-edge"
+  (run* q (cf-patho :a :b q))
+  (list (list :a :b)))
+
+(mk-test "cycle-free-no-self-loop" (run* q (cf-patho :a :a q)) (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/prefix-suffix.sx

@@ -0,0 +1,76 @@
+;; lib/minikanren/tests/prefix-suffix.sx — appendo-derived sublist relations.
+
+(mk-test
+  "prefixo-empty"
+  (run* q (prefixo (list) (list 1 2 3)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "prefixo-full"
+  (run*
+    q
+    (prefixo
+      (list 1 2 3)
+      (list 1 2 3)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "prefixo-partial"
+  (run*
+    q
+    (prefixo
+      (list 1 2)
+      (list 1 2 3 4)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "prefixo-mismatch-fails"
+  (run*
+    q
+    (prefixo
+      (list 1 3)
+      (list 1 2 3)))
+  (list))
+
+(mk-test
+  "prefixo-enumerates-all"
+  (run* q (prefixo q (list 1 2 3)))
+  (list
+    (list)
+    (list 1)
+    (list 1 2)
+    (list 1 2 3)))
+
+(mk-test
+  "suffixo-empty"
+  (run* q (suffixo (list) (list 1 2 3)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "suffixo-full"
+  (run*
+    q
+    (suffixo
+      (list 1 2 3)
+      (list 1 2 3)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "suffixo-partial"
+  (run*
+    q
+    (suffixo
+      (list 2 3)
+      (list 1 2 3)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "suffixo-enumerates-all"
+  (run* q (suffixo q (list 1 2 3)))
+  (list
+    (list 1 2 3)
+    (list 2 3)
+    (list 3)
+    (list)))
+
+(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-fd.sx

@@ -0,0 +1,97 @@
+;; lib/minikanren/tests/queens-fd.sx — N-queens via CLP(FD).
+;;
+;; Native FD propagation makes N-queens tractable: 4-queens finds both
+;; solutions instantly; 5-queens finds all 10 in seconds. Compare with
+;; the naive enumerate-then-filter version in queens.sx, which struggles
+;; past N=4.
+
+(define
+  fd-no-diag
+  (fn
+    (ci cj k)
+    (fresh
+      (a b)
+      (fd-plus cj k a)
+      (fd-plus ci k b)
+      (fd-neq ci a)
+      (fd-neq cj b))))
+
+(define
+  n-queens-4-fd
+  (fn
+    (cs)
+    (let
+      ((c1 (nth cs 0))
+        (c2 (nth cs 1))
+        (c3 (nth cs 2))
+        (c4 (nth cs 3)))
+      (mk-conj
+        (fd-in c1 (list 1 2 3 4))
+        (fd-in c2 (list 1 2 3 4))
+        (fd-in c3 (list 1 2 3 4))
+        (fd-in c4 (list 1 2 3 4))
+        (fd-distinct cs)
+        (fd-no-diag c1 c2 1)
+        (fd-no-diag c1 c3 2)
+        (fd-no-diag c1 c4 3)
+        (fd-no-diag c2 c3 1)
+        (fd-no-diag c2 c4 2)
+        (fd-no-diag c3 c4 1)
+        (fd-label cs)))))
+
+(define
+  n-queens-5-fd
+  (fn
+    (cs)
+    (let
+      ((c1 (nth cs 0))
+        (c2 (nth cs 1))
+        (c3 (nth cs 2))
+        (c4 (nth cs 3))
+        (c5 (nth cs 4)))
+      (mk-conj
+        (fd-in
+          c1
+          (list 1 2 3 4 5))
+        (fd-in
+          c2
+          (list 1 2 3 4 5))
+        (fd-in
+          c3
+          (list 1 2 3 4 5))
+        (fd-in
+          c4
+          (list 1 2 3 4 5))
+        (fd-in
+          c5
+          (list 1 2 3 4 5))
+        (fd-distinct cs)
+        (fd-no-diag c1 c2 1)
+        (fd-no-diag c1 c3 2)
+        (fd-no-diag c1 c4 3)
+        (fd-no-diag c1 c5 4)
+        (fd-no-diag c2 c3 1)
+        (fd-no-diag c2 c4 2)
+        (fd-no-diag c2 c5 3)
+        (fd-no-diag c3 c4 1)
+        (fd-no-diag c3 c5 2)
+        (fd-no-diag c4 c5 1)
+        (fd-label cs)))))
+
+(mk-test
+  "n-queens-4-fd-two-solutions"
+  (run*
+    q
+    (fresh (a b c d) (== q (list a b c d)) (n-queens-4-fd (list a b c d))))
+  (list
+    (list 2 4 1 3)
+    (list 3 1 4 2)))
+
+(mk-test
+  "n-queens-5-fd-ten-solutions"
+  (let
+    ((sols (run* q (fresh (a b c d e) (== q (list a b c d e)) (n-queens-5-fd (list a b c d e))))))
+    (= (len sols) 10))
+  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/rdb.sx

@@ -0,0 +1,90 @@
+;; lib/minikanren/tests/rdb.sx — relational database queries.
+;;
+;; Demonstrates how miniKanren can serve as a Datalog-style query engine
+;; over fact tables. Tables are SX lists of tuples; the relation just
+;; wraps `membero` over the table.
+
+(define
+  rdb-employees
+  (list
+    (list "alice" "engineering" 100000)
+    (list "bob" "marketing" 80000)
+    (list "carol" "engineering" 90000)
+    (list "dave" "engineering" 85000)
+    (list "eve" "sales" 75000)))
+
+(define
+  rdb-projects
+  (list
+    (list "alice" "compiler")
+    (list "carol" "compiler")
+    (list "dave" "runtime")
+    (list "alice" "runtime")
+    (list "eve" "outreach")))
+
+;; Relation views over the tables.
+
+(define
+  employees
+  (fn (name dept salary) (membero (list name dept salary) rdb-employees)))
+
+(define
+  on-project
+  (fn (name project) (membero (list name project) rdb-projects)))
+
+;; --- queries ---
+
+(mk-test
+  "rdb-engineering-staff"
+  (let
+    ((res (run* q (fresh (n s) (employees n "engineering" s) (== q n)))))
+    (and
+      (= (len res) 3)
+      (and
+        (some (fn (n) (= n "alice")) res)
+        (and
+          (some (fn (n) (= n "carol")) res)
+          (some (fn (n) (= n "dave")) res)))))
+  true)
+
+(mk-test
+  "rdb-high-salary"
+  (let
+    ((res (run* q (fresh (n d s) (employees n d s) (lto-i 85000 s) (== q (list n s))))))
+    (and
+      (= (len res) 2)
+      (and
+        (some (fn (r) (= r (list "alice" 100000))) res)
+        (some (fn (r) (= r (list "carol" 90000))) res))))
+  true)
+
+(mk-test
+  "rdb-join-employee-project"
+  (let
+    ((res (run* q (fresh (n d s) (employees n d s) (on-project n "compiler") (== q n)))))
+    (and
+      (= (len res) 2)
+      (and
+        (some (fn (n) (= n "alice")) res)
+        (some (fn (n) (= n "carol")) res))))
+  true)
+
+(mk-test
+  "rdb-engineers-on-runtime"
+  (let
+    ((res (run* q (fresh (n s) (employees n "engineering" s) (on-project n "runtime") (== q n)))))
+    (and
+      (= (len res) 2)
+      (and
+        (some (fn (n) (= n "alice")) res)
+        (some (fn (n) (= n "dave")) res))))
+  true)
+
+(mk-test
+  "rdb-people-on-multiple-projects"
+  (let
+    ((res (run* q (fresh (n p1 p2) (on-project n p1) (on-project n p2) (nafc (== p1 p2)) (== q n)))))
+    (some (fn (n) (= n "alice")) res))
+  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/removeo-allo.sx

@@ -0,0 +1,39 @@
+;; lib/minikanren/tests/removeo-allo.sx — remove every occurrence of x.
+
+(mk-test
+  "removeo-allo-multi"
+  (run*
+    q
+    (removeo-allo
+      2
+      (list 1 2 3 2 4 2)
+      q))
+  (list (list 1 3 4)))
+
+(mk-test
+  "removeo-allo-single"
+  (run*
+    q
+    (removeo-allo 2 (list 1 2 3) q))
+  (list (list 1 3)))
+
+(mk-test
+  "removeo-allo-no-match"
+  (run*
+    q
+    (removeo-allo 99 (list 1 2 3) q))
+  (list (list 1 2 3)))
+
+(mk-test
+  "removeo-allo-everything"
+  (run*
+    q
+    (removeo-allo 1 (list 1 1 1) q))
+  (list (list)))
+
+(mk-test
+  "removeo-allo-empty"
+  (run* q (removeo-allo 1 (list) q))
+  (list (list)))
+
+(mk-tests-run!)

lib/minikanren/tests/repeato-concato.sx

@@ -0,0 +1,69 @@
+;; lib/minikanren/tests/repeato-concato.sx — repeat element n times +
+;; concatenate a list of lists.
+
+(define
+  mk-nat
+  (fn (n) (if (= n 0) :z (list :s (mk-nat (- n 1))))))
+
+;; --- repeato ---
+
+(mk-test
+  "repeato-zero"
+  (run* q (repeato :a (mk-nat 0) q))
+  (list (list)))
+(mk-test
+  "repeato-one"
+  (run* q (repeato :a (mk-nat 1) q))
+  (list (list :a)))
+(mk-test
+  "repeato-three"
+  (run* q (repeato :a (mk-nat 3) q))
+  (list (list :a :a :a)))
+
+(mk-test
+  "repeato-numeric"
+  (run* q (repeato 7 (mk-nat 4) q))
+  (list (list 7 7 7 7)))
+
+(mk-test
+  "repeato-recover-count"
+  (run* q (repeato :x q (list :x :x :x :x)))
+  (list (mk-nat 4)))
+
+;; --- concato ---
+
+(mk-test "concato-empty" (run* q (concato (list) q)) (list (list)))
+
+(mk-test
+  "concato-single"
+  (run* q (concato (list (list 1 2 3)) q))
+  (list (list 1 2 3)))
+
+(mk-test
+  "concato-multi"
+  (run*
+    q
+    (concato
+      (list
+        (list 1 2)
+        (list 3)
+        (list 4 5 6))
+      q))
+  (list
+    (list 1 2 3 4 5 6)))
+
+(mk-test
+  "concato-all-empty"
+  (run* q (concato (list (list) (list) (list)) q))
+  (list (list)))
+
+(mk-test
+  "concato-mixed-empty"
+  (run*
+    q
+    (concato
+      (list (list 1) (list) (list 2 3))
+      q))
+  (list (list 1 2 3)))
+
+(mk-tests-run!)

lib/minikanren/tests/rev-acco.sx

@@ -0,0 +1,46 @@
+;; lib/minikanren/tests/rev-acco.sx — accumulator-style reverse.
+;;
+;; Faster than reverseo for forward queries (no quadratic appendos).
+;; Trade-off: rev-acco is asymmetric (acc=initial-empty for the public
+;; interface), so it does not cleanly run backwards in run* the way
+;; reverseo does.
+
+(mk-test "rev-2o-empty" (run* q (rev-2o (list) q)) (list (list)))
+
+(mk-test
+  "rev-2o-singleton"
+  (run* q (rev-2o (list 7) q))
+  (list (list 7)))
+
+(mk-test
+  "rev-2o-three"
+  (run* q (rev-2o (list 1 2 3) q))
+  (list (list 3 2 1)))
+
+(mk-test
+  "rev-2o-five"
+  (run*
+    q
+    (rev-2o (list 1 2 3 4 5) q))
+  (list (list 5 4 3 2 1)))
+
+(mk-test
+  "rev-2o-strings"
+  (run* q (rev-2o (list "a" "b" "c") q))
+  (list (list "c" "b" "a")))
+
+(mk-test
+  "rev-2o-reverseo-agree"
+  (let
+    ((via-reverseo (first (run* q (reverseo (list 1 2 3 4 5) q))))
+      (via-rev-2o
+        (first
+          (run*
+            q
+            (rev-2o
+              (list 1 2 3 4 5)
+              q)))))
+    (= via-reverseo via-rev-2o))
+  true)
+
+(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/selecto.sx

@@ -0,0 +1,46 @@
+;; lib/minikanren/tests/selecto.sx — choose an element + rest of list.
+
+(mk-test
+  "selecto-enumerate"
+  (run*
+    q
+    (fresh
+      (x r)
+      (selecto x r (list 1 2 3))
+      (== q (list x r))))
+  (list
+    (list 1 (list 2 3))
+    (list 2 (list 1 3))
+    (list 3 (list 1 2))))
+
+(mk-test
+  "selecto-find-rest"
+  (run* q (selecto 2 q (list 1 2 3)))
+  (list (list 1 3)))
+
+(mk-test
+  "selecto-find-element"
+  (run*
+    q
+    (selecto
+      q
+      (list 1 3)
+      (list 1 2 3)))
+  (list 2))
+
+(mk-test
+  "selecto-element-not-present-fails"
+  (run* q (selecto 99 q (list 1 2 3)))
+  (list))
+
+(mk-test
+  "selecto-empty-list-fails"
+  (run* q (selecto q (list) (list)))
+  (list))
+
+(mk-test
+  "selecto-singleton"
+  (run* q (fresh (x r) (selecto x r (list :only)) (== q (list x r))))
+  (list (list :only (list))))
+
+(mk-tests-run!)

lib/minikanren/tests/send-more-money.sx

@@ -0,0 +1,97 @@
+;; lib/minikanren/tests/send-more-money.sx — classic cryptarithmetic
+;;
+;;     S E N D
+;;   + M O R E
+;;   ---------
+;;   M O N E Y
+;;
+;; Column-by-column encoding with carries c1, c2, c3, and the
+;; leftmost column produces a carry which equals M (the result is 5 digits).
+;; All 8 letters distinct; S ≠ 0, M ≠ 0.
+;; Unique solution: S=9, E=5, N=6, D=7, M=1, O=0, R=8, Y=2.
+;;
+;; Note: the full search labelling 11 variables from {0..9} is too slow
+;; for naive labelling order (10^11 combinations naively, even with
+;; bounds-consistency the branching factor dominates). Real CLP(FD)
+;; systems use first-fail heuristics. Here we only verify the encoding
+;; against the known answer.
+
+(define
+  digits-0-9
+  (list
+    0
+    1
+    2
+    3
+    4
+    5
+    6
+    7
+    8
+    9))
+(define
+  digits-1-9
+  (list
+    1
+    2
+    3
+    4
+    5
+    6
+    7
+    8
+    9))
+
+(define
+  smm-col-with-carry
+  (fn
+    (x y carry-in z carry-out)
+    (fresh
+      (xy xyc ten-cout z-plus-ten-cout)
+      (fd-plus x y xy)
+      (fd-plus xy carry-in xyc)
+      (fd-times 10 carry-out ten-cout)
+      (fd-plus z ten-cout z-plus-ten-cout)
+      (fd-eq xyc z-plus-ten-cout))))
+
+(define
+  send-more-money
+  (fn
+    (S E N D M O R Y)
+    (fresh
+      (c1 c2 c3)
+      (mk-conj
+        (fd-in S digits-1-9)
+        (fd-in M digits-1-9)
+        (fd-in E digits-0-9)
+        (fd-in N digits-0-9)
+        (fd-in D digits-0-9)
+        (fd-in O digits-0-9)
+        (fd-in R digits-0-9)
+        (fd-in Y digits-0-9)
+        (fd-in c1 (list 0 1))
+        (fd-in c2 (list 0 1))
+        (fd-in c3 (list 0 1))
+        (fd-distinct (list S E N D M O R Y))
+        (smm-col-with-carry D E 0 Y c1)
+        (smm-col-with-carry N R c1 E c2)
+        (smm-col-with-carry E O c2 N c3)
+        (smm-col-with-carry S M c3 O M)
+        (fd-label (list S E N D M O R Y c1 c2 c3))))))
+
+(mk-test
+  "send-more-money-verify-known-solution"
+  (run*
+    q
+    (send-more-money
+      9
+      5
+      6
+      7
+      1
+      0
+      8
+      2))
+  (list (make-symbol "_.0")))
+
+(mk-tests-run!)

lib/minikanren/tests/simplifyo.sx

@@ -0,0 +1,47 @@
+;; lib/minikanren/tests/simplifyo.sx — algebraic expression simplifier
+;; demo using conda for first-match-wins dispatch.
+
+(define
+  simplify-step-o
+  (fn
+    (expr result)
+    (conda
+      ((fresh (x) (== expr (list :+ 0 x)) (== result x)))
+      ((fresh (x) (== expr (list :+ x 0)) (== result x)))
+      ((fresh (y) (== expr (list :* 0 y)) (== result 0)))
+      ((fresh (x) (== expr (list :* x 0)) (== result 0)))
+      ((fresh (x) (== expr (list :* 1 x)) (== result x)))
+      ((fresh (x) (== expr (list :* x 1)) (== result x)))
+      ((== result expr)))))                                  ;; default: unchanged
+
+(mk-test
+  "simplify-zero-plus"
+  (run* q (simplify-step-o (list :+ 0 :y) q))
+  (list :y))
+
+(mk-test
+  "simplify-plus-zero"
+  (run* q (simplify-step-o (list :+ :x 0) q))
+  (list :x))
+
+(mk-test
+  "simplify-zero-times"
+  (run* q (simplify-step-o (list :* 0 :y) q))
+  (list 0))
+
+(mk-test
+  "simplify-one-times"
+  (run* q (simplify-step-o (list :* 1 :y) q))
+  (list :y))
+
+(mk-test
+  "simplify-no-rule-applies"
+  (run* q (simplify-step-o (list :+ :x :y) q))
+  (list (list :+ :x :y)))
+
+(mk-test
+  "simplify-non-identity-form"
+  (run* q (simplify-step-o (list :+ 5 7) q))
+  (list (list :+ 5 7)))
+
+(mk-tests-run!)

lib/minikanren/tests/sortedo.sx

@@ -0,0 +1,40 @@
+;; lib/minikanren/tests/sortedo.sx — checks list is non-decreasing.
+
+(mk-test
+  "sortedo-empty"
+  (run* q (sortedo (list)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "sortedo-singleton"
+  (run* q (sortedo (list 42)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "sortedo-ascending"
+  (run* q (sortedo (list 1 2 3 4)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "sortedo-with-equal-adjacent"
+  (run*
+    q
+    (sortedo (list 1 1 2 2 3)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "sortedo-out-of-order-fails"
+  (run* q (sortedo (list 1 3 2)))
+  (list))
+
+(mk-test
+  "sortedo-descending-fails"
+  (run* q (sortedo (list 3 2 1)))
+  (list))
+
+(mk-test
+  "sortedo-pair-equal"
+  (run* q (sortedo (list 5 5)))
+  (list (make-symbol "_.0")))
+
+(mk-tests-run!)

lib/minikanren/tests/subo.sx

@@ -0,0 +1,60 @@
+;; lib/minikanren/tests/subo.sx — contiguous-sublist relation.
+
+(mk-test
+  "subo-simple-found"
+  (run*
+    q
+    (subo
+      (list 2 3)
+      (list 1 2 3 4)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "subo-not-contiguous-fails"
+  (run*
+    q
+    (subo
+      (list 2 4)
+      (list 1 2 3 4)))
+  (list))
+
+(mk-test
+  "subo-full-list-found"
+  (run*
+    q
+    (subo
+      (list 1 2 3)
+      (list 1 2 3)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "subo-empty-list-found"
+  (let
+    ((res (run* q (subo (list) (list 1 2 3)))))
+    (= (len res) 4))
+  true)
+
+(mk-test
+  "subo-prefix"
+  (run*
+    q
+    (subo
+      (list 1 2)
+      (list 1 2 3 4)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "subo-suffix"
+  (run*
+    q
+    (subo
+      (list 3 4)
+      (list 1 2 3 4)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "subo-strings"
+  (run* q (subo (list "b" "c") (list "a" "b" "c" "d")))
+  (list (make-symbol "_.0")))
+
+(mk-tests-run!)

lib/minikanren/tests/subseto.sx

@@ -0,0 +1,62 @@
+;; lib/minikanren/tests/subseto.sx — every element of l1 is in l2.
+
+(mk-test
+  "subseto-empty"
+  (run* q (subseto (list) (list 1 2 3)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "subseto-singleton-yes"
+  (run*
+    q
+    (subseto (list 2) (list 1 2 3)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "subseto-singleton-no"
+  (run*
+    q
+    (subseto (list 99) (list 1 2 3)))
+  (list))
+
+(mk-test
+  "subseto-multi-yes"
+  (run
+    1
+    q
+    (subseto
+      (list 1 3)
+      (list 1 2 3 4)))
+  (list (make-symbol "_.0")))
+
+(mk-test
+  "subseto-multi-no"
+  (run*
+    q
+    (subseto
+      (list 1 99)
+      (list 1 2 3)))
+  (list))
+
+(mk-test
+  "subseto-equal-sets"
+  (run
+    1
+    q
+    (subseto
+      (list 1 2 3)
+      (list 1 2 3)))
+  (list (make-symbol "_.0")))
+
+;; allow duplicates in l1 — each just needs membership in l2.
+(mk-test
+  "subseto-duplicates-allowed"
+  (run
+    1
+    q
+    (subseto
+      (list 1 1 2)
+      (list 1 2 3)))
+  (list (make-symbol "_.0")))
+
+(mk-tests-run!)

lib/minikanren/tests/sudoku-4x4.sx

@@ -0,0 +1,89 @@
+;; lib/minikanren/tests/sudoku-4x4.sx — Sudoku 4×4 via CLP(FD).
+;;
+;; Grid in row-major order:
+;;
+;;   c0 c1 | c2 c3
+;;   c4 c5 | c6 c7
+;;   ------+------
+;;   c8 c9 | cA cB
+;;   cC cD | cE cF
+;;
+;; Each cell ∈ {1, 2, 3, 4}. 4 rows + 4 cols + 4 2x2 boxes are each a
+;; distinct permutation.
+
+(define digits-1-4 (list 1 2 3 4))
+
+(define
+  sudoku-4x4
+  (fn
+    (cells)
+    (let
+      ((c0 (nth cells 0))
+        (c1 (nth cells 1))
+        (c2 (nth cells 2))
+        (c3 (nth cells 3))
+        (c4 (nth cells 4))
+        (c5 (nth cells 5))
+        (c6 (nth cells 6))
+        (c7 (nth cells 7))
+        (c8 (nth cells 8))
+        (c9 (nth cells 9))
+        (cA (nth cells 10))
+        (cB (nth cells 11))
+        (cC (nth cells 12))
+        (cD (nth cells 13))
+        (cE (nth cells 14))
+        (cF (nth cells 15)))
+      (mk-conj
+        (fd-in c0 digits-1-4)
+        (fd-in c1 digits-1-4)
+        (fd-in c2 digits-1-4)
+        (fd-in c3 digits-1-4)
+        (fd-in c4 digits-1-4)
+        (fd-in c5 digits-1-4)
+        (fd-in c6 digits-1-4)
+        (fd-in c7 digits-1-4)
+        (fd-in c8 digits-1-4)
+        (fd-in c9 digits-1-4)
+        (fd-in cA digits-1-4)
+        (fd-in cB digits-1-4)
+        (fd-in cC digits-1-4)
+        (fd-in cD digits-1-4)
+        (fd-in cE digits-1-4)
+        (fd-in cF digits-1-4)
+        (fd-distinct (list c0 c1 c2 c3))
+        (fd-distinct (list c4 c5 c6 c7))
+        (fd-distinct (list c8 c9 cA cB))
+        (fd-distinct (list cC cD cE cF))
+        (fd-distinct (list c0 c4 c8 cC))
+        (fd-distinct (list c1 c5 c9 cD))
+        (fd-distinct (list c2 c6 cA cE))
+        (fd-distinct (list c3 c7 cB cF))
+        (fd-distinct (list c0 c1 c4 c5))
+        (fd-distinct (list c2 c3 c6 c7))
+        (fd-distinct (list c8 c9 cC cD))
+        (fd-distinct (list cA cB cE cF))
+        (fd-label cells)))))
+
+;; --- Tests ---
+
+(mk-test
+  "sudoku-4x4-empty-grid-count"
+  (let
+    ((sols (run* q (fresh (c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF) (== q (list c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF)) (sudoku-4x4 (list c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF))))))
+    (len sols))
+  288)
+
+(mk-test
+  "sudoku-4x4-impossible-clue-empty"
+  (run*
+    q
+    (fresh
+      (c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF)
+      (== c0 1)
+      (== c1 1)
+      (== q (list c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF))
+      (sudoku-4x4 (list c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF))))
+  (list))
+
+(mk-tests-run!)

lib/minikanren/tests/sum-product.sx

@@ -0,0 +1,44 @@
+;; lib/minikanren/tests/sum-product.sx — fold list to integer.
+
+(mk-test "sumo-empty" (run* q (sumo (list) q)) (list 0))
+(mk-test
+  "sumo-1-to-5"
+  (run*
+    q
+    (sumo (list 1 2 3 4 5) q))
+  (list 15))
+(mk-test
+  "sumo-zeros"
+  (run* q (sumo (list 0 0 0) q))
+  (list 0))
+(mk-test
+  "sumo-negs"
+  (run* q (sumo (list 5 -3 8) q))
+  (list 10))
+
+(mk-test "producto-empty" (run* q (producto (list) q)) (list 1))
+(mk-test
+  "producto-1-to-4"
+  (run* q (producto (list 1 2 3 4) q))
+  (list 24))
+(mk-test
+  "producto-with-0"
+  (run* q (producto (list 5 0 7) q))
+  (list 0))
+(mk-test
+  "producto-of-1s"
+  (run* q (producto (list 1 1 1) q))
+  (list 1))
+
+(mk-test
+  "sum-product-pythagorean-square"
+  (run*
+    q
+    (fresh
+      (s sq2)
+      (sumo (list 3 4 5) s)
+      (producto (list 3 3) sq2)
+      (== q (list s sq2))))
+  (list (list 12 9)))
+
+(mk-tests-run!)

lib/minikanren/tests/swap-firsto.sx

@@ -0,0 +1,32 @@
+;; lib/minikanren/tests/swap-firsto.sx — swap first two elements.
+
+(mk-test
+  "swap-firsto-pair"
+  (run* q (swap-firsto (list 1 2) q))
+  (list (list 2 1)))
+
+(mk-test
+  "swap-firsto-with-tail"
+  (run* q (swap-firsto (list 1 2 3 4) q))
+  (list (list 2 1 3 4)))
+
+(mk-test
+  "swap-firsto-singleton-fails"
+  (run* q (swap-firsto (list 1) q))
+  (list))
+
+(mk-test "swap-firsto-empty-fails" (run* q (swap-firsto (list) q)) (list))
+
+(mk-test
+  "swap-firsto-self-inverse"
+  (run*
+    q
+    (fresh (mid) (swap-firsto (list :a :b :c :d) mid) (swap-firsto mid q)))
+  (list (list :a :b :c :d)))
+
+(mk-test
+  "swap-firsto-backward"
+  (run* q (swap-firsto q (list :y :x :z)))
+  (list (list :x :y :z)))
+
+(mk-tests-run!)

lib/minikanren/tests/tabling-more.sx

@@ -0,0 +1,55 @@
+;; lib/minikanren/tests/tabling-more.sx — table-1 + table-3.
+
+;; --- table-1 (predicate caching) ---
+
+(define
+  tab-in-list
+  (table-1
+    "in-list"
+    (fn
+      (x)
+      (membero
+        x
+        (list 1 2 3 4 5)))))
+
+(mk-tab-clear!)
+(mk-test
+  "table-1-hit"
+  (run* q (tab-in-list 3))
+  (list (make-symbol "_.0")))
+(mk-test "table-1-miss-no" (run* q (tab-in-list 99)) (list))
+(mk-test
+  "table-1-replay"
+  (run* q (tab-in-list 3))
+  (list (make-symbol "_.0")))
+
+;; --- table-3 (Ackermann) ---
+
+(define
+  ack-o
+  (table-3
+    "ack"
+    (fn
+      (m n result)
+      (conde
+        ((== m 0) (pluso-i n 1 result))
+        ((fresh (m-1) (lto-i 0 m) (== n 0) (minuso-i m 1 m-1) (ack-o m-1 1 result)))
+        ((fresh (m-1 n-1 inner) (lto-i 0 m) (lto-i 0 n) (minuso-i m 1 m-1) (minuso-i n 1 n-1) (ack-o m n-1 inner) (ack-o m-1 inner result)))))))
+
+(mk-tab-clear!)
+(mk-test
+  "ack-0-0"
+  (run* q (ack-o 0 0 q))
+  (list 1))
+(mk-tab-clear!)
+(mk-test
+  "ack-2-3"
+  (run* q (ack-o 2 3 q))
+  (list 9))
+(mk-tab-clear!)
+(mk-test
+  "ack-3-3"
+  (run* q (ack-o 3 3 q))
+  (list 61))
+
+(mk-tests-run!)

lib/minikanren/tests/tabling-slg.sx

@@ -0,0 +1,56 @@
+;; lib/minikanren/tests/tabling-slg.sx — Phase 7 piece A: SLG-style tabling.
+
+;; --- table-2-slg with Fibonacci (sanity: same answer as naive table-2) ---
+
+(mk-tab-clear!)
+(define
+  slg-fib-o
+  (table-2-slg
+    "slg-fib"
+    (fn
+      (n result)
+      (conde
+        ((== n 0) (== result 0))
+        ((== n 1) (== result 1))
+        ((fresh (n-1 n-2 r-1 r-2) (lto-i 1 n) (minuso-i n 1 n-1) (minuso-i n 2 n-2) (slg-fib-o n-1 r-1) (slg-fib-o n-2 r-2) (pluso-i r-1 r-2 result)))))))
+
+(mk-tab-clear!)
+(mk-test "slg-fib-five" (run* q (slg-fib-o 5 q)) (list 5))
+(mk-tab-clear!)
+(mk-test "slg-fib-ten" (run* q (slg-fib-o 10 q)) (list 55))
+
+;; --- table-3-slg with cyclic-graph patho ---
+
+(define slg-cyc-edges (list (list :a :b) (list :b :a) (list :b :c)))
+(define slg-cyc-edgeo (fn (x y) (membero (list x y) slg-cyc-edges)))
+
+(mk-tab-clear!)
+(define
+  tab-patho
+  (table-3-slg
+    "patho"
+    (fn
+      (x y path)
+      (conde
+        ((slg-cyc-edgeo x y) (== path (list x y)))
+        ((fresh (z mid) (slg-cyc-edgeo x z) (tab-patho z y mid) (conso x mid path)))))))
+
+(mk-tab-clear!)
+(mk-test
+  "slg-cyclic-direct"
+  (run* q (tab-patho :a :b q))
+  (list (list :a :b)))
+
+(mk-tab-clear!)
+(mk-test
+  "slg-cyclic-multi-hop"
+  (run* q (tab-patho :a :c q))
+  (list (list :a :b :c)))
+
+(mk-tab-clear!)
+(mk-test
+  "slg-cyclic-self-loop-finite"
+  (run* q (tab-patho :a :a q))
+  (list (list :a :b :a)))
+
+(mk-tests-run!)

lib/minikanren/tests/tabling.sx

@@ -0,0 +1,60 @@
+;; lib/minikanren/tests/tabling.sx — Phase 7 piece A: naive memoization.
+
+;; --- Fibonacci canary: tabled vs naive --
+
+(define
+  tab-fib-o
+  (table-2
+    "fib"
+    (fn
+      (n result)
+      (conde
+        ((== n 0) (== result 0))
+        ((== n 1) (== result 1))
+        ((fresh (n-1 n-2 r-1 r-2) (lto-i 1 n) (minuso-i n 1 n-1) (minuso-i n 2 n-2) (tab-fib-o n-1 r-1) (tab-fib-o n-2 r-2) (pluso-i r-1 r-2 result)))))))
+
+(mk-tab-clear!)
+
+(mk-test "tab-fib-zero" (run* q (tab-fib-o 0 q)) (list 0))
+(mk-tab-clear!)
+(mk-test "tab-fib-one" (run* q (tab-fib-o 1 q)) (list 1))
+(mk-tab-clear!)
+(mk-test "tab-fib-two" (run* q (tab-fib-o 2 q)) (list 1))
+(mk-tab-clear!)
+(mk-test "tab-fib-five" (run* q (tab-fib-o 5 q)) (list 5))
+(mk-tab-clear!)
+(mk-test "tab-fib-ten" (run* q (tab-fib-o 10 q)) (list 55))
+(mk-tab-clear!)
+(mk-test
+  "tab-fib-twenty"
+  (run* q (tab-fib-o 20 q))
+  (list 6765))
+
+;; --- ground-term predicate ---
+
+(mk-test "tab-ground-term-num" (mk-tab-ground-term? 5) true)
+(mk-test "tab-ground-term-str" (mk-tab-ground-term? "hi") true)
+(mk-test
+  "tab-ground-term-list"
+  (mk-tab-ground-term? (list 1 2 3))
+  true)
+(mk-test "tab-ground-term-var" (mk-tab-ground-term? (mk-var "x")) false)
+(mk-test
+  "tab-ground-term-nested"
+  (mk-tab-ground-term?
+    (list 1 (list 2 (mk-var "y")) 3))
+  false)
+
+;; --- caching reduces work — count cache hits via repeated query ---
+
+(mk-test
+  "tab-cache-replay"
+  (begin
+    (mk-tab-clear!)
+    (let
+      ((first (run* q (tab-fib-o 10 q)))
+        (second (run* q (tab-fib-o 10 q))))
+      (and (= first (list 55)) (= second (list 55)))))
+  true)
+
+(mk-tests-run!)

lib/minikanren/tests/take-drop.sx

@@ -0,0 +1,92 @@
+;; lib/minikanren/tests/take-drop.sx — Peano-indexed prefix/suffix.
+
+(define
+  mk-nat
+  (fn (n) (if (= n 0) :z (list :s (mk-nat (- n 1))))))
+
+;; --- tako ---
+
+(mk-test
+  "tako-zero"
+  (run*
+    q
+    (tako (mk-nat 0) (list 1 2 3) q))
+  (list (list)))
+
+(mk-test
+  "tako-two"
+  (run*
+    q
+    (tako
+      (mk-nat 2)
+      (list 1 2 3 4 5)
+      q))
+  (list (list 1 2)))
+
+(mk-test
+  "tako-all"
+  (run*
+    q
+    (tako (mk-nat 3) (list 1 2 3) q))
+  (list (list 1 2 3)))
+
+(mk-test
+  "tako-too-many"
+  (run*
+    q
+    (tako (mk-nat 5) (list 1 2 3) q))
+  (list))
+
+;; --- dropo ---
+
+(mk-test
+  "dropo-zero"
+  (run*
+    q
+    (dropo (mk-nat 0) (list 1 2 3) q))
+  (list (list 1 2 3)))
+
+(mk-test
+  "dropo-two"
+  (run*
+    q
+    (dropo
+      (mk-nat 2)
+      (list 1 2 3 4 5)
+      q))
+  (list (list 3 4 5)))
+
+(mk-test
+  "dropo-all"
+  (run*
+    q
+    (dropo (mk-nat 3) (list 1 2 3) q))
+  (list (list)))
+
+(mk-test
+  "dropo-too-many"
+  (run*
+    q
+    (dropo (mk-nat 5) (list 1 2 3) q))
+  (list))
+
+;; --- take + drop round-trip ---
+
+(mk-test
+  "tako-dropo-roundtrip"
+  (run*
+    q
+    (fresh
+      (p s)
+      (tako
+        (mk-nat 2)
+        (list 1 2 3 4 5)
+        p)
+      (dropo
+        (mk-nat 2)
+        (list 1 2 3 4 5)
+        s)
+      (appendo p s q)))
+  (list (list 1 2 3 4 5)))
+
+(mk-tests-run!)