mk: phase 5B — project, escape into host SX

(project (vars ...) goal ...) defmacro walks each named var via mk-walk*,
rebinds them in the body's lexical scope, then mk-conjs the body goals on
the same substitution. Hygienic — gensym'd s-param so user vars survive.

Lets you reach into host SX for arithmetic, string ops, anything that
needs a ground value: (project (n) (== q (* n n))), (project (s)
(== q (str s \"!\"))), and so on.

6 new tests, 194/194 cumulative.

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

plans/minikanren-on-sx.md

@@ -120,8 +120,9 @@ Key semantic mappings:
       `tests/relations.sx`; reverseo/flatteno/permuteo/lengtho deferred)
 
 ### Phase 5 — `project` + `matche` + negation
-- [ ] `project` `(x ...) body` — access reified values of logic vars inside a goal;
-      escapes to ground values for arithmetic or string ops
+- [x] `project` `(x ...) body` — defmacro: rebinds named vars to `(mk-walk* var s)`
+      in the body's lexical scope, then runs `(mk-conj body...)` on the same
+      substitution. Hygienic via gensym'd `s`-param. (`Phase 5 piece B`)
 - [ ] `matche` — pattern matching over logic terms (extension from core.logic)
       `(matche l ((head . tail) goal) (() goal))`
 - [x] `conda` — soft-cut: first non-failing head wins; ALL of head's answers
@@ -156,6 +157,10 @@ _(none yet)_
 
 _Newest first._
 
+- **2026-05-07** — **Phase 5 piece B — project**: `lib/minikanren/project.sx` —
+  defmacro that walks each named var, rebinds them, and runs the body's mk-conj.
+  Demonstrated escape into host arithmetic / string ops (`(* n n)`, `(str s "!")`).
+  Hygienic gensym'd s-param. 6 new tests, 194/194 cumulative.
 - **2026-05-07** — **Peano arithmetic** (`lib/minikanren/peano.sx`): zeroo, pluso,
   minuso, lteo, lto, *o on Peano-encoded naturals (`:z` / `(:s n)`). pluso runs
   forward, backward, and enumerates: `(run* q (fresh (a b) (pluso a b 3)