Merge loops/maude into architecture: maude confluence/critical-pair checker (mau/confluent?)

Adds lib/maude/confluence.sx — the CID-stability oracle the artdag optimiser
needs. 274 tests.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

lib/content/api.sx

@@ -25,8 +25,13 @@
 (define content/append doc-append)
 (define content/blocks doc-blocks)
 (define content/count doc-count)
-(define content/find doc-find)
-(define content/has? doc-has?)
+;; find / has? are TREE-WIDE by id (descend into sections) — so the facade reads
+;; back any block content/edit can update or delete. content/find-top / has-top?
+;; keep the top-level-only lookup for callers that mean the ordered sequence.
+(define content/find doc-find-deep)
+(define content/has? doc-has-deep?)
+(define content/find-top doc-find)
+(define content/has-top? doc-has?)
 (define content/ids doc-ids)
 (define content/types doc-types)
 

lib/content/doc.sx

@@ -5,14 +5,19 @@
 ;; and returns a NEW document — the input is never mutated, so any version is the
 ;; head of an op stream (replay-friendly for persist + CRDT merge).
 ;;
-;; CtDoc also carries optional metadata (title/slug/tags) — see meta.sx for the
-;; ergonomic API; they default nil and do not affect block operations.
+;; By-id ops (update/delete) and by-id lookup (doc-find-deep/doc-has-deep?) are
+;; TREE-WIDE: they descend into any block carrying a `children` list (i.e.
+;; sections), since ids are unique across the tree. This keeps the persist
+;; op-log, content/edit and content/find correct for nested documents.
+;; insert/move are positional and act at the top level.
+;;
+;; CtDoc also carries optional metadata (title/slug/tags) — see meta.sx.
 ;;
 ;; Op shapes (data, not objects — they are the persist event payload):
-;;   {:op "insert" :block <blk> :after <id|nil>}   ; after nil = prepend
-;;   {:op "update" :id <id> :field <name> :value <v>}
-;;   {:op "move"   :id <id> :index <n>}
-;;   {:op "delete" :id <id>}
+;;   {:op "insert" :block <blk> :after <id|nil>}   ; after nil = prepend (top level)
+;;   {:op "update" :id <id> :field <name> :value <v>}   ; tree-wide by id
+;;   {:op "move"   :id <id> :index <n>}                 ; top level
+;;   {:op "delete" :id <id>}                            ; tree-wide by id
 
 (define
   content-bootstrap-doc!
@@ -76,17 +81,58 @@
           (first blocks)
           (ct-insert-at (rest blocks) (- i 1) x))))))
 
+;; tree-wide remove by id: drop matches at this level, recurse into children
+;; (blocks carrying a `children` list, i.e. sections).
 (define
   ct-remove-id
   (fn
     (blocks id)
-    (filter (fn (b) (if (= (blk-id b) id) false true)) blocks)))
+    (map
+      (fn
+        (b)
+        (let
+          ((ch (st-iv-get b "children")))
+          (if (list? ch) (st-iv-set! b "children" (ct-remove-id ch id)) b)))
+      (filter (fn (b) (if (= (blk-id b) id) false true)) blocks))))
 
+;; tree-wide replace by id: apply f to the match wherever it sits in the tree.
 (define
   ct-replace-id
   (fn
     (blocks id f)
-    (map (fn (b) (if (= (blk-id b) id) (f b) b)) blocks)))
+    (map
+      (fn
+        (b)
+        (if
+          (= (blk-id b) id)
+          (f b)
+          (let
+            ((ch (st-iv-get b "children")))
+            (if
+              (list? ch)
+              (st-iv-set! b "children" (ct-replace-id ch id f))
+              b))))
+      blocks)))
+
+;; tree-wide find by id: first block matching id anywhere in the tree, or nil.
+;; Descends into any `children` list, mirroring ct-replace-id/ct-remove-id.
+(define
+  ct-find-id
+  (fn
+    (blocks id)
+    (if
+      (= (len blocks) 0)
+      nil
+      (let
+        ((b (first blocks)))
+        (if
+          (= (blk-id b) id)
+          b
+          (let
+            ((ch (st-iv-get b "children")))
+            (let
+              ((nested (if (list? ch) (ct-find-id ch id) nil)))
+              (if (= nested nil) (ct-find-id (rest blocks) id) nested))))))))
 
 ;; ── query ──
 (define doc-index-of (fn (doc id) (ct-index-of (doc-blocks doc) id)))
@@ -103,6 +149,14 @@
   doc-has?
   (fn (doc id) (if (= (doc-index-of doc id) -1) false true)))
 
+;; tree-wide lookup by id — reads a nested block by the same id content/edit can
+;; update/delete (no section.sx dependency; uses the generic children descent).
+(define doc-find-deep (fn (doc id) (ct-find-id (doc-blocks doc) id)))
+
+(define
+  doc-has-deep?
+  (fn (doc id) (if (= (doc-find-deep doc id) nil) false true)))
+
 ;; ── structural edits (each returns a new document) ──
 (define doc-with-blocks (fn (doc blocks) (st-iv-set! doc "blocks" blocks)))
 

lib/content/find-replace.sx

@@ -1,10 +1,17 @@
-;; content-on-sx — global find/replace across text-bearing blocks.
+;; content-on-sx — global find/replace across every text-bearing field.
 ;;
-;; Replaces every occurrence of `from` with `to` in the text field of text /
-;; heading / code / quote blocks, tree-wide (via the transform layer). For
-;; renaming a term throughout a document. Immutable; case-sensitive.
+;; Replaces every occurrence of `from` with `to` in the text-bearing fields of
+;; a document, tree-wide (via the transform layer):
+;;   - the `text` of text / heading / code / quote / callout blocks
+;;   - the `alt` of image blocks
+;;   - each item of list blocks
+;;   - every header and cell of table blocks
+;; This is exactly the set asText / stats / summary draw prose from, so a rename
+;; via content/find-replace and a word count over asText stay consistent.
+;; Immutable; case-sensitive.
 ;;
-;; Requires (loaded by harness): block.sx, transform.sx (content/map-blocks).
+;; Requires (loaded by harness): block.sx, transform.sx (content/map-blocks),
+;; table.sx (CtTable ivars).
 
 (define
   fr-in?
@@ -15,17 +22,54 @@
       ((= (first xs) x) true)
       (else (fr-in? x (rest xs))))))
 
+(define fr-rep (fn (s from to) (replace (str s) from to)))
+
+;; Blocks whose prose content find/replace rewrites (matches asText's set).
 (define
   fr-has-text?
-  (fn (b) (fr-in? (blk-type b) (list "text" "heading" "code" "quote"))))
+  (fn
+    (b)
+    (fr-in?
+      (blk-type b)
+      (list "text" "heading" "code" "quote" "callout" "image" "list" "table"))))
+
+;; Per-type field rewrite. Each branch returns a new (copy-on-write) block.
+(define
+  fr-rewrite
+  (fn
+    (b from to)
+    (let
+      ((t (blk-type b)))
+      (cond
+        ((= t "image")
+          (blk-set b "alt" (fr-rep (blk-get b "alt") from to)))
+        ((= t "list")
+          (let
+            ((items (blk-get b "items")))
+            (if
+              (list? items)
+              (blk-set b "items" (map (fn (it) (fr-rep it from to)) items))
+              b)))
+        ((= t "table")
+          (let
+            ((hs (blk-get b "headers")) (rs (blk-get b "rows")))
+            (let
+              ((b1 (if (list? hs) (blk-set b "headers" (map (fn (h) (fr-rep h from to)) hs)) b)))
+              (if
+                (list? rs)
+                (blk-set
+                  b1
+                  "rows"
+                  (map
+                    (fn
+                      (r)
+                      (if (list? r) (map (fn (c) (fr-rep c from to)) r) r))
+                    rs))
+                b1))))
+        (else (blk-set b "text" (fr-rep (blk-get b "text") from to)))))))
 
 (define
   content/find-replace
   (fn
     (doc from to)
-    (content/map-blocks
-      doc
-      fr-has-text?
-      (fn
-        (b)
-        (blk-set b "text" (replace (str (blk-get b "text")) from to))))))
+    (content/map-blocks doc fr-has-text? (fn (b) (fr-rewrite b from to)))))

lib/content/query.sx

@@ -1,10 +1,10 @@
 ;; content-on-sx — block query + table of contents.
 ;;
 ;; Collect blocks across the whole tree (descending into sections) by predicate
-;; or type, and derive a table of contents from headings. Tree detection is
-;; inline (class + st-iv-get) so this needs no section.sx.
+;; or type, search them by prose, and derive a table of contents from headings.
+;; Tree detection is inline (class + st-iv-get) so this needs no section.sx.
 ;;
-;; Requires (loaded by harness): block.sx, doc.sx.
+;; Requires (loaded by harness): block.sx, doc.sx, text.sx (asText for search).
 
 (define
   qry-section?
@@ -45,6 +45,30 @@
   content/select-ids
   (fn (doc pred) (map (fn (b) (blk-id b)) (content/select doc pred))))
 
+;; Blocks (tree-wide, excluding section containers) whose own prose contains
+;; `term`. "Prose" is (asText b), so search covers exactly what every block
+;; exposes as text — text/heading/code/quote/callout text, image alt, list
+;; items, table headers+cells — with no separate field list to drift from
+;; asText / find-replace / stats. Case-sensitive substring match.
+(define
+  content/search-text
+  (fn
+    (doc term)
+    (content/select
+      doc
+      (fn
+        (b)
+        (and
+          (not (qry-section? b))
+          (>= (index-of (asText b) term) 0))))))
+
+;; Same search, returning matching block ids in document order.
+(define
+  content/search-text-ids
+  (fn
+    (doc term)
+    (map (fn (b) (blk-id b)) (content/search-text doc term))))
+
 ;; table of contents: {:id :level :text} for every heading, in document order.
 (define
   content/headings

lib/content/scoreboard.json

@@ -3,7 +3,7 @@
     "block": {"pass": 38, "fail": 0},
     "doc": {"pass": 40, "fail": 0},
     "render": {"pass": 42, "fail": 0},
-    "api": {"pass": 26, "fail": 0},
+    "api": {"pass": 32, "fail": 0},
     "meta": {"pass": 27, "fail": 0},
     "page": {"pass": 7, "fail": 0},
     "page-full": {"pass": 4, "fail": 0},
@@ -14,14 +14,14 @@
     "tree-edit": {"pass": 17, "fail": 0},
     "move": {"pass": 11, "fail": 0},
     "clone": {"pass": 10, "fail": 0},
-    "query": {"pass": 13, "fail": 0},
+    "query": {"pass": 20, "fail": 0},
     "toc": {"pass": 8, "fail": 0},
     "anchor": {"pass": 6, "fail": 0},
     "outline": {"pass": 14, "fail": 0},
     "flatten": {"pass": 10, "fail": 0},
     "transform": {"pass": 12, "fail": 0},
     "normalize": {"pass": 11, "fail": 0},
-    "find-replace": {"pass": 10, "fail": 0},
+    "find-replace": {"pass": 16, "fail": 0},
     "stats": {"pass": 17, "fail": 0},
     "summary": {"pass": 14, "fail": 0},
     "index": {"pass": 13, "fail": 0},
@@ -31,7 +31,7 @@
     "data": {"pass": 25, "fail": 0},
     "wire": {"pass": 11, "fail": 0},
     "validate": {"pass": 23, "fail": 0},
-    "store": {"pass": 33, "fail": 0},
+    "store": {"pass": 46, "fail": 0},
     "snapshot": {"pass": 20, "fail": 0},
     "crdt": {"pass": 34, "fail": 0},
     "crdt-tree": {"pass": 21, "fail": 0},
@@ -42,7 +42,7 @@
     "md-doc": {"pass": 12, "fail": 0},
     "fed": {"pass": 20, "fail": 0}
   },
-  "total_pass": 746,
+  "total_pass": 778,
   "total_fail": 0,
-  "total": 746
+  "total": 778
 }

lib/content/scoreboard.md

@@ -7,7 +7,7 @@ _Generated by `lib/content/conformance.sh`_
 | block | 38 | 0 | 38 |
 | doc | 40 | 0 | 40 |
 | render | 42 | 0 | 42 |
-| api | 26 | 0 | 26 |
+| api | 32 | 0 | 32 |
 | meta | 27 | 0 | 27 |
 | page | 7 | 0 | 7 |
 | page-full | 4 | 0 | 4 |
@@ -18,14 +18,14 @@ _Generated by `lib/content/conformance.sh`_
 | tree-edit | 17 | 0 | 17 |
 | move | 11 | 0 | 11 |
 | clone | 10 | 0 | 10 |
-| query | 13 | 0 | 13 |
+| query | 20 | 0 | 20 |
 | toc | 8 | 0 | 8 |
 | anchor | 6 | 0 | 6 |
 | outline | 14 | 0 | 14 |
 | flatten | 10 | 0 | 10 |
 | transform | 12 | 0 | 12 |
 | normalize | 11 | 0 | 11 |
-| find-replace | 10 | 0 | 10 |
+| find-replace | 16 | 0 | 16 |
 | stats | 17 | 0 | 17 |
 | summary | 14 | 0 | 14 |
 | index | 13 | 0 | 13 |
@@ -35,7 +35,7 @@ _Generated by `lib/content/conformance.sh`_
 | data | 25 | 0 | 25 |
 | wire | 11 | 0 | 11 |
 | validate | 23 | 0 | 23 |
-| store | 33 | 0 | 33 |
+| store | 46 | 0 | 46 |
 | snapshot | 20 | 0 | 20 |
 | crdt | 34 | 0 | 34 |
 | crdt-tree | 21 | 0 | 21 |
@@ -45,4 +45,4 @@ _Generated by `lib/content/conformance.sh`_
 | md-import | 38 | 0 | 38 |
 | md-doc | 12 | 0 | 12 |
 | fed | 20 | 0 | 20 |
-| **Total** | **746** | **0** | **746** |
+| **Total** | **778** | **0** | **778** |

lib/content/store.sx

@@ -5,9 +5,10 @@
 ;; replay of its op stream up to a sequence number; the materialised doc is a
 ;; cache, never primary state.
 ;;
-;; Requires (loaded by the harness): block.sx, doc.sx, and persist
-;; (event/backend/log/kv/api). The persist backend `b` is opened by the caller
-;; via (persist/open) and injected — content knows nothing about which backend.
+;; Requires (loaded by the harness): block.sx, doc.sx, section.sx (doc-deep-find
+;; + doc-tree-ids, for the tree-wide diff), plus persist (event/backend/log/kv/
+;; api). The persist backend `b` is opened by the caller via (persist/open) and
+;; injected — content knows nothing about which backend.
 
 (define content/-stream (fn (doc-id) (str "content:" doc-id)))
 
@@ -69,11 +70,18 @@
   (fn (b doc-id) (map (fn (ev) {:type (persist/event-type ev) :at (persist/event-at ev) :seq (persist/event-seq ev)}) (content/log b doc-id))))
 
 ;; ── diff between two materialised document versions ──
-;; Returns {:added (ids) :removed (ids) :changed (ids)} where changed = ids
-;; present in both whose block content differs.
-(define
-  content/-missing?
-  (fn (doc id) (= (ct-index-of (doc-blocks doc) id) -1)))
+;; Tree-wide: ids are enumerated across the whole block tree (descending into
+;; sections), so nested-block adds/removes/changes are detected, not just
+;; top-level ones. Returns {:added :removed :changed} (lists of ids):
+;;   :added   — ids present (anywhere) in `new` but not in `old`
+;;   :removed — ids present (anywhere) in `old` but not in `new`
+;;   :changed — content blocks present in both whose block value differs
+;; Section containers never appear in :changed (they hold no own content — a
+;; child change surfaces as that child's own entry); a whole section appearing
+;; or disappearing shows up in :added / :removed by its id.
+(define content/-all-ids (fn (doc) (doc-tree-ids doc)))
+
+(define content/-missing? (fn (doc id) (= (doc-deep-find doc id) nil)))
 
 (define
   content/-changed
@@ -83,15 +91,16 @@
       (fn
         (id)
         (let
-          ((bo (doc-find old id)) (bn (doc-find new id)))
+          ((bo (doc-deep-find old id)) (bn (doc-deep-find new id)))
           (cond
             ((= bo nil) false)
             ((= bn nil) false)
+            ((= (blk-type bo) "section") false)
             ((= bo bn) false)
             (else true))))
-      (doc-ids old))))
+      (content/-all-ids old))))
 
-(define content/diff (fn (old new) {:changed (content/-changed old new) :removed (filter (fn (id) (content/-missing? new id)) (doc-ids old)) :added (filter (fn (id) (content/-missing? old id)) (doc-ids new))}))
+(define content/diff (fn (old new) {:changed (content/-changed old new) :removed (filter (fn (id) (content/-missing? new id)) (content/-all-ids old)) :added (filter (fn (id) (content/-missing? old id)) (content/-all-ids new))}))
 
 ;; convenience: diff two persisted versions by seq.
 (define

lib/content/tests/api.sx

@@ -97,3 +97,37 @@
   "render original unchanged"
   (content/render d1 "html")
   "<h1>Hi</h1><p>World</p>")
+
+;; ── facade find/has? are TREE-WIDE (reach into sections); find-top/has-top?
+;; keep the top-level-only lookup. This makes the read-by-id surface consistent
+;; with content/edit, whose update/delete are already tree-wide. ──
+(content-bootstrap-section!)
+(define
+  nd
+  (content/append
+    (content/empty "nested")
+    (mk-section
+      "sec"
+      (list (content/block "text" "inner" (list (list "text" "deep")))))))
+(content-test
+  "find nested (deep)"
+  (blk-id (content/find nd "inner"))
+  "inner")
+(content-test "has? nested (deep)" (content/has? nd "inner") true)
+(content-test "find-top misses nested" (content/find-top nd "inner") nil)
+(content-test "has-top? misses nested" (content/has-top? nd "inner") false)
+(content-test
+  "find-top sees top-level"
+  (blk-id (content/find-top nd "sec"))
+  "sec")
+;; a nested block updated by id via content/edit is now readable by id via
+;; content/find (was impossible when find was top-level-only).
+(content-test
+  "edit-then-find nested round-trip"
+  (str
+    (blk-send
+      (content/find
+        (content/edit nd (content/update "inner" "text" "edited"))
+        "inner")
+      "text"))
+  "edited")

lib/content/tests/find-replace.sx

@@ -1,8 +1,10 @@
-;; Extension — global find/replace across text-bearing blocks.
+;; Extension — global find/replace across every text-bearing field.
 
 (st-bootstrap-classes!)
 (content/bootstrap!)
 (content-bootstrap-section!)
+(content-bootstrap-callout!)
+(content-bootstrap-table!)
 
 (define
   d
@@ -30,11 +32,12 @@
   (str (blk-send (doc-deep-find r "n") "text"))
   "nested Bar")
 
-;; ── does NOT touch image alt/src (not a text field) ──
+;; ── image alt IS a text field (asText ^ alt), so it is rewritten ──
 (content-test
-  "image alt untouched"
+  "image alt replaced"
   (str (blk-send (doc-deep-find r "img") "alt"))
-  "Foo alt")
+  "Bar alt")
+;; ── but src is a URL, not prose, so it stays put ──
 (content-test
   "image src untouched"
   (str (blk-send (doc-deep-find r "img") "src"))
@@ -76,6 +79,68 @@
   (str (blk-send (doc-find r2 "q") "text"))
   "new saying")
 
+;; ── callout text is covered (consistency with asText/stats/summary) ──
+(content-test
+  "replace callout text"
+  (str
+    (blk-send
+      (doc-find
+        (content/find-replace
+          (doc-append (doc-empty "d") (mk-callout "co" "note" "Foo here"))
+          "Foo"
+          "Bar")
+        "co")
+      "text"))
+  "Bar here")
+(content-test
+  "callout kind untouched by text replace"
+  (str
+    (blk-send
+      (doc-find
+        (content/find-replace
+          (doc-append (doc-empty "d") (mk-callout "co" "note" "x"))
+          "note"
+          "X")
+        "co")
+      "kind"))
+  "note")
+
+;; ── list items are rewritten (asText folds items) ──
+(define
+  rl
+  (content/find-replace
+    (doc-append
+      (doc-empty "d")
+      (mk-list "l" false (list "Foo one" "two Foo")))
+    "Foo"
+    "Bar"))
+(content-test
+  "replace first list item"
+  (str (first (blk-send (doc-find rl "l") "items")))
+  "Bar one")
+(content-test
+  "replace second list item"
+  (str (first (rest (blk-send (doc-find rl "l") "items"))))
+  "two Bar")
+
+;; ── table headers + cells are rewritten (asText folds rows) ──
+(define
+  rt
+  (content/find-replace
+    (doc-append
+      (doc-empty "d")
+      (mk-table "t" (list "Foo head") (list (list "a Foo" "b"))))
+    "Foo"
+    "Bar"))
+(content-test
+  "replace table header"
+  (str (first (table-headers (doc-find rt "t"))))
+  "Bar head")
+(content-test
+  "replace table cell"
+  (str (first (first (table-rows (doc-find rt "t")))))
+  "a Bar")
+
 ;; ── no match → unchanged render ──
 (content-test
   "no match"

lib/content/tests/query.sx

@@ -1,8 +1,11 @@
-;; Extension — block query + table of contents.
+;; Extension — block query + table of contents + prose search.
 
 (st-bootstrap-classes!)
 (content/bootstrap!)
+(content-bootstrap-text!)
 (content-bootstrap-section!)
+(content-bootstrap-table!)
+(content-bootstrap-callout!)
 
 (define
   d
@@ -87,3 +90,49 @@
   "deep toc level"
   (get (first (content/headings deep)) :level)
   3)
+
+;; ── prose search (content/search-text) ──
+;; "cat" appears in text, image alt, a list item, a table cell, and a callout
+;; — every text-bearing field — so search must find all five via asText.
+(define
+  sd
+  (doc-append
+    (doc-append
+      (doc-append
+        (doc-append
+          (doc-append
+            (doc-empty "sd")
+            (mk-heading "sh" 1 "Welcome aboard"))
+          (mk-text "st" "the cat sat"))
+        (mk-image "si" "/x.png" "a cat photo"))
+      (mk-list "sl" false (list "first cat" "second dog")))
+    (mk-section
+      "sec"
+      (list
+        (mk-table "stb" (list "Animal") (list (list "cat") (list "fish")))
+        (mk-callout "sc" "note" "beware of cat")))))
+
+(content-test
+  "search across every text-bearing field"
+  (content/search-text-ids sd "cat")
+  (list "st" "si" "sl" "stb" "sc"))
+(content-test "search count" (len (content/search-text sd "cat")) 5)
+(content-test
+  "search heading text"
+  (content/search-text-ids sd "Welcome")
+  (list "sh"))
+(content-test
+  "search list item only"
+  (content/search-text-ids sd "dog")
+  (list "sl"))
+(content-test "search no match" (content/search-text-ids sd "zzz") (list))
+;; section containers are excluded — a term living only inside a section's
+;; children returns the child, never the section wrapper.
+(content-test
+  "search excludes section wrapper"
+  (content/search-text-ids sd "fish")
+  (list "stb"))
+(content-test
+  "search returns block objects"
+  (blk-id (first (content/search-text sd "Welcome")))
+  "sh")

lib/content/tests/store.sx

@@ -151,3 +151,58 @@
   "op-log media type"
   (blk-type (doc-find (content/head B3 "rich") "v"))
   "media")
+
+;; ── op-log update/delete reach NESTED blocks (tree-wide by id) ──
+(content-bootstrap-section!)
+(define B4 (persist/open))
+(content/commit!
+  B4
+  "nest"
+  (op-insert (mk-section "sec" (list (mk-text "n" "orig"))) nil)
+  1)
+(content/commit! B4 "nest" (op-update "n" "text" "edited") 2)
+(content-test
+  "op-log nested update"
+  (str (blk-send (doc-deep-find (content/head B4 "nest") "n") "text"))
+  "edited")
+(content-test
+  "op-log nested update tree intact"
+  (doc-tree-ids (content/head B4 "nest"))
+  (list "sec" "n"))
+(content/commit! B4 "nest" (op-delete "n") 3)
+(content-test
+  "op-log nested delete"
+  (doc-tree-ids (content/head B4 "nest"))
+  (list "sec"))
+(content-test
+  "op-log nested delete via content/at seq2"
+  (doc-tree-ids (content/at B4 "nest" 2))
+  (list "sec" "n"))
+
+;; ── diff is TREE-WIDE: nested-block add/change/remove are detected, and
+;; section containers never appear in :changed (a top-level-only diff would miss
+;; "n" entirely and instead flag the section). ──
+(define dn01 (content/diff-versions B4 "nest" 0 1))
+(content-test
+  "diff nested added (section + child)"
+  (get dn01 :added)
+  (list "sec" "n"))
+(content-test "diff nested added removed empty" (get dn01 :removed) (list))
+(content-test "diff nested added changed empty" (get dn01 :changed) (list))
+
+(define dn12 (content/diff-versions B4 "nest" 1 2))
+(content-test
+  "diff nested changed child only"
+  (get dn12 :changed)
+  (list "n"))
+(content-test "diff nested changed no add" (get dn12 :added) (list))
+(content-test "diff nested changed no remove" (get dn12 :removed) (list))
+
+(define dn23 (content/diff-versions B4 "nest" 2 3))
+(content-test "diff nested removed child" (get dn23 :removed) (list "n"))
+(content-test "diff nested removed no change" (get dn23 :changed) (list))
+
+(content-test
+  "diff nested no-op"
+  (get (content/diff-versions B4 "nest" 1 1) :changed)
+  (list))

lib/maude/conditional.sx

@@ -0,0 +1,164 @@
+;; lib/maude/conditional.sx — conditional equations (Phase 4) + owise.
+;;
+;; A condition-aware superset of the Phase 3 reducer. `ceq L = R if COND` fires
+;; only when COND holds under the matching substitution. Conditions come from
+;; the parser as:
+;;   {:kind :eq :lhs L :rhs R}   — holds iff reduce(s L) =AC= reduce(s R)
+;;   {:kind :bool :term T}       — holds iff reduce(s T) =AC= true
+;; Condition evaluation recurses through the SAME reducer (mau/cnormalize), so
+;; a ceq whose guard mentions other (possibly conditional) equations Just Works
+;; — termination rests on the guard reducing on structurally smaller arguments
+;; (and the global fuel guard).
+;;
+;; `owise` (otherwise): an equation tagged [owise] fires at a redex only when
+;; NO ordinary equation applies there. crewrite-top is two-pass: ordinary
+;; equations first, owise equations last.
+;;
+;; Single-step firing uses the short-circuiting matcher in fire.sx
+;; (mau/fire-eq). The eager candidate enumeration (mau/eq-candidates) is
+;; retained for `search` (rewrite.sx), which genuinely needs every successor.
+
+(define
+  mau/ac-candidates
+  (fn
+    (theory f th eq term)
+    (let
+      ((id (get th :id))
+        (pels (mau/flatten-op theory f (get eq :lhs)))
+        (sels (mau/flatten-op theory f term)))
+      (let
+        ((matches (if (get th :comm) (mau/match-multiset theory f (mau/append2 pels (list (mau/var "$R" ""))) sels {} id) (mau/match-sequence theory f (mau/append2 (list (mau/var "$L" "")) (mau/append2 pels (list (mau/var "$R" "")))) sels {} id))))
+        (map (fn (s) {:s s :result (mau/ac-eq-result theory f th eq s)}) matches)))))
+
+(define
+  mau/eq-candidates
+  (fn
+    (theory eq term)
+    (let
+      ((lhs (get eq :lhs)))
+      (let
+        ((th (if (mau/app? lhs) (mau/th-of theory (mau/op lhs)) {:id nil :assoc false :comm false})))
+        (if
+          (and (mau/app? lhs) (get th :assoc))
+          (mau/ac-candidates theory (mau/op lhs) th eq term)
+          (map (fn (s) {:s s :result (mau/subst-apply s (get eq :rhs))}) (mau/mm theory lhs term {})))))))
+
+(define
+  mau/cond-holds?
+  (fn
+    (theory eqs cond s)
+    (if
+      (= cond nil)
+      true
+      (if
+        (= (get cond :kind) "eq")
+        (mau/ac-equal?
+          theory
+          (mau/cnormalize
+            theory
+            eqs
+            (mau/subst-apply s (get cond :lhs))
+            mau/reduce-fuel)
+          (mau/cnormalize
+            theory
+            eqs
+            (mau/subst-apply s (get cond :rhs))
+            mau/reduce-fuel))
+        (mau/ac-equal?
+          theory
+          (mau/cnormalize
+            theory
+            eqs
+            (mau/subst-apply s (get cond :term))
+            mau/reduce-fuel)
+          (mau/const "true"))))))
+
+(define
+  mau/try-candidates
+  (fn
+    (theory all-eqs cond term cands)
+    (if
+      (empty? cands)
+      nil
+      (let
+        ((c (first cands)))
+        (if
+          (and
+            (not (mau/ac-equal? theory (get c :result) term))
+            (mau/cond-holds? theory all-eqs cond (get c :s)))
+          (get c :result)
+          (mau/try-candidates theory all-eqs cond term (rest cands)))))))
+
+;; ---- owise partitioning ----
+
+(define mau/eq-owise? (fn (e) (= (get e :owise) true)))
+(define mau/filter-owise (fn (eqs) (filter mau/eq-owise? eqs)))
+(define
+  mau/filter-noowise
+  (fn (eqs) (filter (fn (e) (not (mau/eq-owise? e))) eqs)))
+
+(define
+  mau/crewrite-loop
+  (fn
+    (theory all-eqs eqs term)
+    (if
+      (empty? eqs)
+      nil
+      (let
+        ((r (mau/fire-eq theory all-eqs (first eqs) term)))
+        (if (= r nil) (mau/crewrite-loop theory all-eqs (rest eqs) term) r)))))
+
+(define
+  mau/crewrite-top
+  (fn
+    (theory eqs term)
+    (let
+      ((r (mau/crewrite-loop theory eqs (mau/filter-noowise eqs) term)))
+      (if
+        (= r nil)
+        (mau/crewrite-loop theory eqs (mau/filter-owise eqs) term)
+        r))))
+
+(define
+  mau/cnormalize
+  (fn
+    (theory eqs term fuel)
+    (if
+      (<= fuel 0)
+      term
+      (cond
+        ((mau/var? term) term)
+        ((mau/app? term)
+          (let
+            ((nargs (map (fn (a) (mau/cnormalize theory eqs a fuel)) (mau/args term))))
+            (let
+              ((t2 (mau/app (mau/op term) nargs)))
+              (let
+                ((r (mau/crewrite-top theory eqs t2)))
+                (if
+                  (= r nil)
+                  t2
+                  (mau/cnormalize theory eqs r (- fuel 1)))))))
+        (else term)))))
+
+(define
+  mau/creduce
+  (fn
+    (m term)
+    (mau/cnormalize
+      (mau/build-theory m)
+      (mau/module-eqs m)
+      term
+      mau/reduce-fuel)))
+
+(define
+  mau/creduce-term
+  (fn (m src) (mau/creduce m (mau/parse-term-in m src))))
+
+(define
+  mau/creduce->str
+  (fn (m src) (mau/term->str (mau/creduce-term m src))))
+
+(define
+  mau/ccanon
+  (fn (m src) (mau/canon (mau/build-theory m) (mau/creduce-term m src))))

lib/maude/confluence.sx

@@ -0,0 +1,268 @@
+;; lib/maude/confluence.sx — critical-pair / local-confluence checking.
+;;
+;; A terminating equation set is confluent iff every critical pair is joinable
+;; (Knuth-Bendix / Newman). A critical pair arises when two oriented equations
+;; overlap: a non-variable subterm of one LHS unifies with the other LHS, giving
+;; two ways to rewrite the overlap; they must reduce to the same normal form.
+;;
+;; This needs TWO-SIDED unification (variables on both sides), not the one-sided
+;; matching the reducer uses — so this file carries its own syntactic unifier.
+;;
+;; SCOPE / honesty: the unifier is SYNTACTIC. For free/constructor operators the
+;; check is exact. For assoc/comm (AC) operators it sees only syntactic overlaps
+;; (full AC-unification is NP/infinitary — out of scope), but joinability is
+;; tested with `mau/ac-equal?` (canonical form modulo the theory), so AC laws are
+;; joined correctly even though their overlaps are under-approximated. Conditional
+;; and `owise` equations are not oriented (skipped).
+
+;; ---------- syntactic unification (vars on both sides) ----------
+
+(define
+  mau/u-walk
+  (fn
+    (t s)
+    (if
+      (mau/var? t)
+      (let
+        ((b (get s (mau/vname t))))
+        (if (= b nil) t (mau/u-walk b s)))
+      t)))
+
+(define
+  mau/u-occurs?
+  (fn
+    (name t s)
+    (let
+      ((w (mau/u-walk t s)))
+      (cond
+        ((mau/var? w) (= (mau/vname w) name))
+        ((mau/app? w) (mau/u-occurs-any? name (mau/args w) s))
+        (else false)))))
+
+(define
+  mau/u-occurs-any?
+  (fn
+    (name args s)
+    (cond
+      ((empty? args) false)
+      ((mau/u-occurs? name (first args) s) true)
+      (else (mau/u-occurs-any? name (rest args) s)))))
+
+(define
+  mau/u-unify-args
+  (fn
+    (as bs s)
+    (cond
+      ((= s nil) nil)
+      ((and (empty? as) (empty? bs)) s)
+      ((or (empty? as) (empty? bs)) nil)
+      (else
+        (mau/u-unify-args
+          (rest as)
+          (rest bs)
+          (mau/u-unify (first as) (first bs) s))))))
+
+(define
+  mau/u-unify
+  (fn
+    (t1 t2 s)
+    (if
+      (= s nil)
+      nil
+      (let
+        ((a (mau/u-walk t1 s)) (b (mau/u-walk t2 s)))
+        (cond
+          ((and (mau/var? a) (mau/var? b) (= (mau/vname a) (mau/vname b)))
+            s)
+          ((mau/var? a)
+            (if
+              (mau/u-occurs? (mau/vname a) b s)
+              nil
+              (assoc s (mau/vname a) b)))
+          ((mau/var? b)
+            (if
+              (mau/u-occurs? (mau/vname b) a s)
+              nil
+              (assoc s (mau/vname b) a)))
+          ((and (mau/app? a) (mau/app? b))
+            (if
+              (and
+                (= (mau/op a) (mau/op b))
+                (= (mau/arity a) (mau/arity b)))
+              (mau/u-unify-args (mau/args a) (mau/args b) s)
+              nil))
+          (else nil))))))
+
+(define
+  mau/u-apply
+  (fn
+    (t s)
+    (let
+      ((w (mau/u-walk t s)))
+      (if
+        (mau/app? w)
+        (mau/app
+          (mau/op w)
+          (map (fn (a) (mau/u-apply a s)) (mau/args w)))
+        w))))
+
+(define
+  mau/u-rename
+  (fn
+    (t suffix)
+    (cond
+      ((mau/var? t) (mau/var (str (mau/vname t) suffix) (mau/vsort t)))
+      ((mau/app? t)
+        (mau/app
+          (mau/op t)
+          (map (fn (a) (mau/u-rename a suffix)) (mau/args t))))
+      (else t))))
+
+;; ---------- positions ----------
+
+(define
+  mau/positions-args
+  (fn
+    (args i)
+    (if
+      (empty? args)
+      (list)
+      (mau/append2
+        (map (fn (p) (cons i p)) (mau/nv-positions (first args)))
+        (mau/positions-args (rest args) (+ i 1))))))
+
+;; non-variable positions (paths) of a term; root = empty path
+(define
+  mau/nv-positions
+  (fn
+    (t)
+    (if
+      (mau/app? t)
+      (cons (list) (mau/positions-args (mau/args t) 0))
+      (list))))
+
+(define
+  mau/at-path
+  (fn
+    (t path)
+    (if
+      (empty? path)
+      t
+      (mau/at-path (nth (mau/args t) (first path)) (rest path)))))
+
+(define
+  mau/replace-nth
+  (fn
+    (xs i v)
+    (if
+      (= i 0)
+      (cons v (rest xs))
+      (cons (first xs) (mau/replace-nth (rest xs) (- i 1) v)))))
+
+(define
+  mau/replace-at
+  (fn
+    (t path new)
+    (if
+      (empty? path)
+      new
+      (mau/app
+        (mau/op t)
+        (mau/replace-nth
+          (mau/args t)
+          (first path)
+          (mau/replace-at (nth (mau/args t) (first path)) (rest path) new))))))
+
+;; ---------- critical pairs ----------
+
+(define
+  mau/eq-same?
+  (fn
+    (e1 e2)
+    (and
+      (mau/term=? (get e1 :lhs) (get e2 :lhs))
+      (mau/term=? (get e1 :rhs) (get e2 :rhs)))))
+
+(define
+  mau/cps-at
+  (fn
+    (l1 r1 l2 r2 same? paths)
+    (if
+      (empty? paths)
+      (list)
+      (let
+        ((p (first paths)))
+        (if
+          (and same? (empty? p))
+          (mau/cps-at l1 r1 l2 r2 same? (rest paths))
+          (let
+            ((s (mau/u-unify (mau/at-path l1 p) l2 {})))
+            (if
+              (= s nil)
+              (mau/cps-at l1 r1 l2 r2 same? (rest paths))
+              (cons {:right (mau/u-apply (mau/replace-at l1 p r2) s) :left (mau/u-apply r1 s)} (mau/cps-at l1 r1 l2 r2 same? (rest paths))))))))))
+
+(define
+  mau/cps-of
+  (fn
+    (e1 e2)
+    (let
+      ((l1 (mau/u-rename (get e1 :lhs) "#1"))
+        (r1 (mau/u-rename (get e1 :rhs) "#1"))
+        (l2 (mau/u-rename (get e2 :lhs) "#2"))
+        (r2 (mau/u-rename (get e2 :rhs) "#2")))
+      (mau/cps-at l1 r1 l2 r2 (mau/eq-same? e1 e2) (mau/nv-positions l1)))))
+
+(define
+  mau/all-cps
+  (fn
+    (eqs)
+    (mau/concat-map
+      (fn (e1) (mau/concat-map (fn (e2) (mau/cps-of e1 e2)) eqs))
+      eqs)))
+
+;; ---------- public API ----------
+
+(define
+  mau/orientable-eqs
+  (fn
+    (m)
+    (filter
+      (fn (e) (and (= (get e :cond) nil) (not (= (get e :owise) true))))
+      (mau/module-eqs m))))
+
+(define
+  mau/joinable?
+  (fn
+    (theory eqs t1 t2)
+    (mau/ac-equal?
+      theory
+      (mau/cnormalize theory eqs t1 mau/reduce-fuel)
+      (mau/cnormalize theory eqs t2 mau/reduce-fuel))))
+
+(define mau/critical-pairs (fn (m) (mau/all-cps (mau/orientable-eqs m))))
+
+(define
+  mau/non-joinable-pairs
+  (fn
+    (m)
+    (let
+      ((theory (mau/build-theory m)) (eqs (mau/module-eqs m)))
+      (filter
+        (fn
+          (cp)
+          (not (mau/joinable? theory eqs (get cp :left) (get cp :right))))
+        (mau/all-cps (mau/orientable-eqs m))))))
+
+(define mau/confluent? (fn (m) (empty? (mau/non-joinable-pairs m))))
+
+(define
+  mau/cp->str
+  (fn
+    (m cp)
+    (let
+      ((theory (mau/build-theory m)))
+      (str
+        (mau/canon theory (get cp :left))
+        " <?> "
+        (mau/canon theory (get cp :right))))))

lib/maude/conformance.conf

@@ -0,0 +1,41 @@
+# Maude conformance config — sourced by lib/guest/conformance.sh.
+
+LANG_NAME=maude
+MODE=dict
+
+PRELOADS=(
+  lib/guest/lex.sx
+  lib/guest/pratt.sx
+  lib/maude/term.sx
+  lib/maude/parser.sx
+  lib/maude/sorts.sx
+  lib/maude/reduce.sx
+  lib/maude/matching.sx
+  lib/maude/conditional.sx
+  lib/maude/fire.sx
+  lib/maude/confluence.sx
+  lib/maude/rewrite.sx
+  lib/maude/searchpath.sx
+  lib/maude/strategy.sx
+  lib/maude/meta.sx
+  lib/maude/pretty.sx
+  lib/maude/run.sx
+)
+
+SUITES=(
+  "parse:lib/maude/tests/parse.sx:(mau-parse-tests-run!)"
+  "reduce:lib/maude/tests/reduce.sx:(mau-reduce-tests-run!)"
+  "matching:lib/maude/tests/matching.sx:(mau-matching-tests-run!)"
+  "confluence:lib/maude/tests/confluence.sx:(mau-confluence-tests-run!)"
+  "conditional:lib/maude/tests/conditional.sx:(mau-conditional-tests-run!)"
+  "owise:lib/maude/tests/owise.sx:(mau-owise-tests-run!)"
+  "gather:lib/maude/tests/gather.sx:(mau-gather-tests-run!)"
+  "sorts:lib/maude/tests/sorts.sx:(mau-sorts-tests-run!)"
+  "rewrite:lib/maude/tests/rewrite.sx:(mau-rewrite-tests-run!)"
+  "searchpath:lib/maude/tests/searchpath.sx:(mau-searchpath-tests-run!)"
+  "strategy:lib/maude/tests/strategy.sx:(mau-strategy-tests-run!)"
+  "meta:lib/maude/tests/meta.sx:(mau-meta-tests-run!)"
+  "pretty:lib/maude/tests/pretty.sx:(mau-pretty-tests-run!)"
+  "run:lib/maude/tests/run.sx:(mau-run-tests-run!)"
+  "effects:lib/maude/tests/effects.sx:(mau-effects-tests-run!)"
+)

lib/maude/conformance.sh

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+# Thin wrapper — see lib/guest/conformance.sh and lib/maude/conformance.conf.
+exec bash "$(dirname "$0")/../guest/conformance.sh" "$(dirname "$0")/conformance.conf" "$@"

lib/maude/fire.sx

@@ -0,0 +1,250 @@
+;; lib/maude/fire.sx — short-circuiting rule/equation firing.
+;;
+;; The eager matcher (mau/match-multiset) enumerates EVERY substitution, which
+;; is what `mau/match-all` and `search` need. But for a single rewrite step we
+;; only need the FIRST usable match — and eager enumeration is exponential when
+;; an AC argument has many identical elements (q ; q ; ... ; q). These
+;; find-matchers thread a predicate and stop at the first complete match for
+;; which it returns non-nil; the predicate builds the rewritten term and checks
+;; "progresses AND condition holds", so firing short-circuits on the first
+;; productive match instead of materialising the whole solution set.
+;;
+;; pred : subst -> result-term-or-nil   (result is always a term, never nil)
+
+(define
+  mau/try-list
+  (fn
+    (substs cont)
+    (if
+      (empty? substs)
+      nil
+      (let
+        ((r (cont (first substs))))
+        (if (= r nil) (mau/try-list (rest substs) cont) r)))))
+
+;; ---- multiset (assoc+comm) find ----
+
+(define
+  mau/ms-find
+  (fn
+    (theory f pels sels s id pred)
+    (cond
+      ((empty? pels) (if (empty? sels) (pred s) nil))
+      (else
+        (let
+          ((p (first pels)) (prest (rest pels)))
+          (if
+            (mau/var? p)
+            (mau/ms-find-var
+              theory
+              f
+              prest
+              sels
+              s
+              (mau/vname p)
+              id
+              pred
+              (mau/var-kmin (mau/vname p) id)
+              (mau/all-splits sels))
+            (mau/ms-find-nonvar theory f p prest sels s id pred 0)))))))
+
+(define
+  mau/ms-find-nonvar
+  (fn
+    (theory f p prest sels s id pred i)
+    (if
+      (>= i (len sels))
+      nil
+      (let
+        ((others (mau/remove-at sels i)))
+        (let
+          ((r (mau/try-list (mau/mm theory p (nth sels i) s) (fn (s2) (mau/ms-find theory f prest others s2 id pred)))))
+          (if
+            (not (= r nil))
+            r
+            (mau/ms-find-nonvar
+              theory
+              f
+              p
+              prest
+              sels
+              s
+              id
+              pred
+              (+ i 1))))))))
+
+(define
+  mau/ms-find-var
+  (fn
+    (theory f prest sels s name id pred kmin splits)
+    (if
+      (empty? splits)
+      nil
+      (let
+        ((chosen (first (first splits)))
+          (rests (nth (first splits) 1)))
+        (if
+          (< (len chosen) kmin)
+          (mau/ms-find-var
+            theory
+            f
+            prest
+            sels
+            s
+            name
+            id
+            pred
+            kmin
+            (rest splits))
+          (let
+            ((s2 (mau/bind-check theory s name (mau/rebuild f chosen id))))
+            (let
+              ((r (if (= s2 nil) nil (mau/ms-find theory f prest rests s2 id pred))))
+              (if
+                (not (= r nil))
+                r
+                (mau/ms-find-var
+                  theory
+                  f
+                  prest
+                  sels
+                  s
+                  name
+                  id
+                  pred
+                  kmin
+                  (rest splits))))))))))
+
+;; ---- sequence (assoc, ordered) find ----
+
+(define
+  mau/seq-find
+  (fn
+    (theory f pels sels s id pred)
+    (cond
+      ((empty? pels) (if (empty? sels) (pred s) nil))
+      (else
+        (let
+          ((p (first pels)) (prest (rest pels)))
+          (if
+            (mau/var? p)
+            (mau/seq-find-var
+              theory
+              f
+              prest
+              sels
+              s
+              (mau/vname p)
+              id
+              pred
+              (mau/var-kmin (mau/vname p) id))
+            (if
+              (empty? sels)
+              nil
+              (mau/try-list
+                (mau/mm theory p (first sels) s)
+                (fn
+                  (s2)
+                  (mau/seq-find theory f prest (rest sels) s2 id pred))))))))))
+
+(define
+  mau/seq-find-var
+  (fn
+    (theory f prest sels s name id pred k)
+    (if
+      (> k (len sels))
+      nil
+      (let
+        ((s2 (mau/bind-check theory s name (mau/rebuild f (mau/take sels k) id))))
+        (let
+          ((r (if (= s2 nil) nil (mau/seq-find theory f prest (mau/drop sels k) s2 id pred))))
+          (if
+            (not (= r nil))
+            r
+            (mau/seq-find-var
+              theory
+              f
+              prest
+              sels
+              s
+              name
+              id
+              pred
+              (+ k 1))))))))
+
+;; ---- firing an equation/rule (returns rewritten term or nil) ----
+
+(define
+  mau/fire-plain
+  (fn
+    (theory eqs eq term cnd substs)
+    (if
+      (empty? substs)
+      nil
+      (let
+        ((res (mau/subst-apply (first substs) (get eq :rhs))))
+        (if
+          (and
+            (not (mau/ac-equal? theory res term))
+            (mau/cond-holds? theory eqs cnd (first substs)))
+          res
+          (mau/fire-plain theory eqs eq term cnd (rest substs)))))))
+
+(define
+  mau/fire-ac
+  (fn
+    (theory eqs f th eq term cnd)
+    (let
+      ((id (get th :id))
+        (pels (mau/flatten-op theory f (get eq :lhs)))
+        (sels (mau/flatten-op theory f term)))
+      (let
+        ((pred (fn (s) (let ((res (mau/ac-eq-result theory f th eq s))) (if (and (not (mau/ac-equal? theory res term)) (mau/cond-holds? theory eqs cnd s)) res nil)))))
+        (if
+          (get th :comm)
+          (mau/ms-find
+            theory
+            f
+            (mau/append2 pels (list (mau/var "$R" "")))
+            sels
+            {}
+            id
+            pred)
+          (mau/seq-find
+            theory
+            f
+            (mau/append2
+              (list (mau/var "$L" ""))
+              (mau/append2 pels (list (mau/var "$R" ""))))
+            sels
+            {}
+            id
+            pred))))))
+
+(define
+  mau/fire-eq
+  (fn
+    (theory eqs eq term)
+    (let
+      ((lhs (get eq :lhs)) (cnd (get eq :cond)))
+      (if
+        (mau/app? lhs)
+        (let
+          ((th (mau/th-of theory (mau/op lhs))))
+          (if
+            (get th :assoc)
+            (mau/fire-ac theory eqs (mau/op lhs) th eq term cnd)
+            (mau/fire-plain
+              theory
+              eqs
+              eq
+              term
+              cnd
+              (mau/mm theory lhs term {}))))
+        (mau/fire-plain
+          theory
+          eqs
+          eq
+          term
+          cnd
+          (mau/mm theory lhs term {}))))))

lib/maude/matching.sx

@@ -0,0 +1,565 @@
+;; lib/maude/matching.sx — equational matching modulo assoc/comm/id (Phase 3).
+;;
+;; The chisel. Syntactic matching (reduce.sx) returns at most one substitution;
+;; matching modulo a theory is MULTI-VALUED — `X + Y` against `a + b + c` (with
+;; _+_ assoc comm) has several solutions. `mau/mm` returns the full list of
+;; substitutions; callers (rule application) pick.
+;;
+;; Operator theories come from the signature attributes, collected into a dict
+;; OP-NAME -> {:assoc B :comm B :id ELT}. Matching dispatches on the head op's
+;; theory:
+;;   free        positional, exact arity
+;;   comm        binary, try both argument orderings
+;;   assoc       flatten the f-spine, match the pattern sequence against the
+;;               subject sequence (variables grab contiguous blocks)
+;;   assoc+comm  flatten, match as multisets (variables grab sub-multisets)
+;; Identity (id: e) lets a variable grab the empty block, contributing e.
+;;
+;; Equational rewriting (mau/ac-reduce) extends each f-AC equation l=r to
+;; f(REST..., l) -> f(REST..., r) so a rule fires on any sub-multiset of an
+;; AC term, then renormalises to a fixpoint. A candidate rewrite is taken only
+;; if it changes the AC-canonical form (mau/canon) — idempotency/identity
+;; matches that would re-fire forever are skipped, guaranteeing progress.
+
+;; ---------- theory table ----------
+
+(define
+  mau/build-theory
+  (fn
+    (m)
+    (let
+      ((th {}))
+      (for-each
+        (fn
+          (op)
+          (let
+            ((a (get op :attrs)))
+            (dict-set! th (get op :name) {:id (get a :id) :assoc (= (get a :assoc) true) :comm (= (get a :comm) true)})))
+        (mau/module-ops m))
+      th)))
+
+(define
+  mau/th-of
+  (fn
+    (theory op)
+    (let ((e (get theory op))) (if (= e nil) {:id nil :assoc false :comm false} e))))
+
+;; ---------- small list utilities ----------
+
+(define
+  mau/concat-map
+  (fn
+    (f xs)
+    (if
+      (empty? xs)
+      (list)
+      (mau/append2 (f (first xs)) (mau/concat-map f (rest xs))))))
+
+(define
+  mau/remove-at
+  (fn (xs i) (mau/append2 (mau/take xs i) (mau/drop xs (+ i 1)))))
+
+;; All (chosen complement) pairs over every subset of xs.
+(define
+  mau/all-splits
+  (fn
+    (xs)
+    (if
+      (empty? xs)
+      (list (list (list) (list)))
+      (let
+        ((subsplits (mau/all-splits (rest xs))) (x (first xs)))
+        (mau/concat-map
+          (fn
+            (pair)
+            (let
+              ((c (first pair)) (r (nth pair 1)))
+              (list (list (cons x c) r) (list c (cons x r)))))
+          subsplits)))))
+
+;; ---------- flattening of associative spines ----------
+
+(define
+  mau/flatten-op
+  (fn
+    (theory f term)
+    (if
+      (and (mau/app? term) (= (mau/op term) f))
+      (mau/flatten-op-list theory f (mau/args term))
+      (list term))))
+
+(define
+  mau/flatten-op-list
+  (fn
+    (theory f args)
+    (if
+      (empty? args)
+      (list)
+      (mau/append2
+        (mau/flatten-op theory f (first args))
+        (mau/flatten-op-list theory f (rest args))))))
+
+(define
+  mau/foldr-app
+  (fn
+    (f block)
+    (if
+      (empty? (rest block))
+      (first block)
+      (mau/app f (list (first block) (mau/foldr-app f (rest block)))))))
+
+(define
+  mau/rebuild
+  (fn
+    (f block id)
+    (cond
+      ((empty? block) (if (= id nil) (mau/const "$EMPTY") (mau/const id)))
+      ((empty? (rest block)) (first block))
+      (else (mau/foldr-app f block)))))
+
+(define mau/ac-build (fn (theory f els id) (mau/rebuild f els id)))
+
+;; ---------- AC-canonical form / equality ----------
+
+(define
+  mau/insert-str
+  (fn
+    (x ys)
+    (cond
+      ((empty? ys) (list x))
+      ((<= x (first ys)) (cons x ys))
+      (else (cons (first ys) (mau/insert-str x (rest ys)))))))
+
+(define
+  mau/sort-strings
+  (fn
+    (xs)
+    (if
+      (empty? xs)
+      xs
+      (mau/insert-str (first xs) (mau/sort-strings (rest xs))))))
+
+(define
+  mau/drop-identity
+  (fn
+    (theory f els id)
+    (if
+      (= id nil)
+      els
+      (let
+        ((idc (mau/canon theory (mau/const id))))
+        (filter (fn (e) (not (= (mau/canon theory e) idc))) els)))))
+
+(define
+  mau/canon
+  (fn
+    (theory term)
+    (cond
+      ((mau/var? term) (str "?" (mau/vname term)))
+      ((mau/const? term) (mau/op term))
+      ((mau/app? term)
+        (let
+          ((f (mau/op term)) (th (mau/th-of theory (mau/op term))))
+          (if
+            (get th :assoc)
+            (let
+              ((els (mau/drop-identity theory f (mau/flatten-op theory f term) (get th :id))))
+              (cond
+                ((empty? els)
+                  (if (= (get th :id) nil) "$EMPTY" (get th :id)))
+                ((empty? (rest els)) (mau/canon theory (first els)))
+                (else
+                  (let
+                    ((cs (map (fn (e) (mau/canon theory e)) els)))
+                    (let
+                      ((cs2 (if (get th :comm) (mau/sort-strings cs) cs)))
+                      (str f "(" (join "," cs2) ")"))))))
+            (if
+              (get th :comm)
+              (str
+                f
+                "("
+                (join
+                  ","
+                  (mau/sort-strings
+                    (map (fn (e) (mau/canon theory e)) (mau/args term))))
+                ")")
+              (str
+                f
+                "("
+                (join
+                  ","
+                  (map (fn (e) (mau/canon theory e)) (mau/args term)))
+                ")")))))
+      (else (str term)))))
+
+(define
+  mau/ac-equal?
+  (fn (theory a b) (= (mau/canon theory a) (mau/canon theory b))))
+
+;; ---------- variable block bounds ----------
+
+(define
+  mau/rest-var?
+  (fn
+    (name)
+    (and
+      (> (len name) 0)
+      (= (slice name 0 1) "$"))))
+
+(define
+  mau/var-kmin
+  (fn
+    (name id)
+    (if (or (mau/rest-var? name) (not (= id nil))) 0 1)))
+
+(define
+  mau/bind-check
+  (fn
+    (theory s name val)
+    (let
+      ((b (get s name)))
+      (if
+        (= b nil)
+        (assoc s name val)
+        (if (mau/ac-equal? theory b val) s nil)))))
+
+;; ---------- core multi-valued matcher ----------
+
+(define
+  mau/mm
+  (fn
+    (theory pat subj s)
+    (cond
+      ((mau/var? pat)
+        (let
+          ((bound (get s (mau/vname pat))))
+          (if
+            (= bound nil)
+            (list (assoc s (mau/vname pat) subj))
+            (if (mau/ac-equal? theory bound subj) (list s) (list)))))
+      ((mau/app? pat)
+        (if (mau/app? subj) (mau/mm-app theory pat subj s) (list)))
+      (else (list)))))
+
+(define
+  mau/extend-all
+  (fn
+    (theory p subj substs)
+    (mau/concat-map (fn (s) (mau/mm theory p subj s)) substs)))
+
+(define
+  mau/mm-args
+  (fn
+    (theory ps ss substs)
+    (cond
+      ((and (empty? ps) (empty? ss)) substs)
+      ((or (empty? ps) (empty? ss)) (list))
+      (else
+        (mau/mm-args
+          theory
+          (rest ps)
+          (rest ss)
+          (mau/extend-all theory (first ps) (first ss) substs))))))
+
+(define
+  mau/mm-comm
+  (fn
+    (theory pat subj s)
+    (let
+      ((p1 (nth (mau/args pat) 0))
+        (p2 (nth (mau/args pat) 1))
+        (q1 (nth (mau/args subj) 0))
+        (q2 (nth (mau/args subj) 1)))
+      (mau/append2
+        (mau/mm-args theory (list p1 p2) (list q1 q2) (list s))
+        (mau/mm-args theory (list p1 p2) (list q2 q1) (list s))))))
+
+(define
+  mau/mm-assoc
+  (fn
+    (theory f pat subj s)
+    (let
+      ((pels (mau/flatten-op theory f pat))
+        (sels (mau/flatten-op theory f subj))
+        (th (mau/th-of theory f)))
+      (if
+        (get th :comm)
+        (mau/match-multiset theory f pels sels s (get th :id))
+        (mau/match-sequence theory f pels sels s (get th :id))))))
+
+(define
+  mau/mm-app
+  (fn
+    (theory pat subj s)
+    (let
+      ((f (mau/op pat))
+        (g (mau/op subj))
+        (th (mau/th-of theory (mau/op pat))))
+      (cond
+        ((get th :assoc) (mau/mm-assoc theory f pat subj s))
+        ((get th :comm)
+          (if
+            (and
+              (= f g)
+              (= (mau/arity pat) 2)
+              (= (mau/arity subj) 2))
+            (mau/mm-comm theory pat subj s)
+            (list)))
+        (else
+          (if
+            (and (= f g) (= (mau/arity pat) (mau/arity subj)))
+            (mau/mm-args theory (mau/args pat) (mau/args subj) (list s))
+            (list)))))))
+
+;; ---------- associative (ordered) sequence matching ----------
+
+(define
+  mau/match-sequence
+  (fn
+    (theory f pels sels s id)
+    (cond
+      ((empty? pels) (if (empty? sels) (list s) (list)))
+      (else
+        (let
+          ((p (first pels)) (prest (rest pels)))
+          (if
+            (mau/var? p)
+            (mau/seq-var-loop
+              theory
+              f
+              prest
+              sels
+              s
+              (mau/vname p)
+              id
+              (mau/var-kmin (mau/vname p) id))
+            (if
+              (empty? sels)
+              (list)
+              (mau/concat-map
+                (fn
+                  (s2)
+                  (mau/match-sequence theory f prest (rest sels) s2 id))
+                (mau/mm theory p (first sels) s)))))))))
+
+(define
+  mau/seq-var-loop
+  (fn
+    (theory f prest sels s name id k)
+    (if
+      (> k (len sels))
+      (list)
+      (let
+        ((block (mau/take sels k)) (rests (mau/drop sels k)))
+        (let
+          ((val (mau/rebuild f block id)))
+          (let
+            ((s2 (mau/bind-check theory s name val)))
+            (mau/append2
+              (if
+                (= s2 nil)
+                (list)
+                (mau/match-sequence theory f prest rests s2 id))
+              (mau/seq-var-loop
+                theory
+                f
+                prest
+                sels
+                s
+                name
+                id
+                (+ k 1)))))))))
+
+;; ---------- associative-commutative (multiset) matching ----------
+
+(define
+  mau/match-multiset
+  (fn
+    (theory f pels sels s id)
+    (cond
+      ((empty? pels) (if (empty? sels) (list s) (list)))
+      (else
+        (let
+          ((p (first pels)) (prest (rest pels)))
+          (if
+            (mau/var? p)
+            (mau/ms-var-splits theory f prest sels s (mau/vname p) id)
+            (mau/ms-nonvar-loop theory f p prest sels s id 0)))))))
+
+(define
+  mau/ms-nonvar-loop
+  (fn
+    (theory f p prest sels s id i)
+    (if
+      (>= i (len sels))
+      (list)
+      (let
+        ((elem (nth sels i)) (others (mau/remove-at sels i)))
+        (mau/append2
+          (mau/concat-map
+            (fn (s2) (mau/match-multiset theory f prest others s2 id))
+            (mau/mm theory p elem s))
+          (mau/ms-nonvar-loop theory f p prest sels s id (+ i 1)))))))
+
+(define
+  mau/ms-var-splits
+  (fn
+    (theory f prest sels s name id)
+    (let
+      ((kmin (mau/var-kmin name id)))
+      (mau/concat-map
+        (fn
+          (pair)
+          (let
+            ((chosen (first pair)) (rests (nth pair 1)))
+            (if
+              (< (len chosen) kmin)
+              (list)
+              (let
+                ((val (mau/rebuild f chosen id)))
+                (let
+                  ((s2 (mau/bind-check theory s name val)))
+                  (if
+                    (= s2 nil)
+                    (list)
+                    (mau/match-multiset theory f prest rests s2 id)))))))
+        (mau/all-splits sels)))))
+
+;; ---------- public matching entry ----------
+
+(define
+  mau/match-all
+  (fn (m pat subj) (mau/mm (mau/build-theory m) pat subj {})))
+
+;; ---------- AC-aware equational rewriting ----------
+
+(define
+  mau/restv
+  (fn
+    (theory f s name)
+    (let
+      ((v (get s name)))
+      (cond
+        ((= v nil) (list))
+        ((and (mau/app? v) (= (mau/op v) "$EMPTY")) (list))
+        (else (mau/flatten-op theory f v))))))
+
+(define
+  mau/ac-eq-result
+  (fn
+    (theory f th eq s)
+    (if
+      (get th :comm)
+      (mau/ac-build
+        theory
+        f
+        (mau/append2
+          (mau/flatten-op theory f (mau/subst-apply s (get eq :rhs)))
+          (mau/restv theory f s "$R"))
+        (get th :id))
+      (mau/ac-build
+        theory
+        f
+        (mau/append2
+          (mau/restv theory f s "$L")
+          (mau/append2
+            (mau/flatten-op theory f (mau/subst-apply s (get eq :rhs)))
+            (mau/restv theory f s "$R")))
+        (get th :id)))))
+
+;; Walk the candidate matches and return the first rewrite that actually
+;; changes the term's canonical form (skips idempotency/identity no-ops).
+(define
+  mau/first-change
+  (fn
+    (theory f th eq term matches)
+    (if
+      (empty? matches)
+      nil
+      (let
+        ((result (mau/ac-eq-result theory f th eq (first matches))))
+        (if
+          (mau/ac-equal? theory result term)
+          (mau/first-change theory f th eq term (rest matches))
+          result)))))
+
+(define
+  mau/ac-rewrite-eq
+  (fn
+    (theory f th eq term)
+    (let
+      ((id (get th :id))
+        (pels (mau/flatten-op theory f (get eq :lhs)))
+        (sels (mau/flatten-op theory f term)))
+      (let
+        ((matches (if (get th :comm) (mau/match-multiset theory f (mau/append2 pels (list (mau/var "$R" ""))) sels {} id) (mau/match-sequence theory f (mau/append2 (list (mau/var "$L" "")) (mau/append2 pels (list (mau/var "$R" "")))) sels {} id))))
+        (mau/first-change theory f th eq term matches)))))
+
+(define
+  mau/ac-rewrite-top
+  (fn
+    (theory eqs term)
+    (cond
+      ((empty? eqs) nil)
+      (else
+        (let
+          ((eq (first eqs)))
+          (if
+            (= (get eq :cond) nil)
+            (let
+              ((lhs (get eq :lhs)))
+              (let
+                ((th (if (mau/app? lhs) (mau/th-of theory (mau/op lhs)) {:id nil :assoc false :comm false})))
+                (let
+                  ((r (if (and (mau/app? lhs) (get th :assoc)) (mau/ac-rewrite-eq theory (mau/op lhs) th eq term) (let ((ss (mau/mm theory lhs term {}))) (if (empty? ss) nil (mau/subst-apply (first ss) (get eq :rhs)))))))
+                  (cond
+                    ((= r nil) (mau/ac-rewrite-top theory (rest eqs) term))
+                    ((mau/ac-equal? theory r term)
+                      (mau/ac-rewrite-top theory (rest eqs) term))
+                    (else r)))))
+            (mau/ac-rewrite-top theory (rest eqs) term)))))))
+
+(define
+  mau/ac-normalize
+  (fn
+    (theory eqs term fuel)
+    (if
+      (<= fuel 0)
+      term
+      (cond
+        ((mau/var? term) term)
+        ((mau/app? term)
+          (let
+            ((nargs (map (fn (a) (mau/ac-normalize theory eqs a fuel)) (mau/args term))))
+            (let
+              ((t2 (mau/app (mau/op term) nargs)))
+              (let
+                ((r (mau/ac-rewrite-top theory eqs t2)))
+                (if
+                  (= r nil)
+                  t2
+                  (mau/ac-normalize theory eqs r (- fuel 1)))))))
+        (else term)))))
+
+(define
+  mau/ac-reduce
+  (fn
+    (m term)
+    (mau/ac-normalize
+      (mau/build-theory m)
+      (mau/module-eqs m)
+      term
+      mau/reduce-fuel)))
+
+(define
+  mau/ac-reduce-term
+  (fn (m src) (mau/ac-reduce m (mau/parse-term-in m src))))
+
+(define
+  mau/ac-reduce->str
+  (fn (m src) (mau/term->str (mau/ac-reduce-term m src))))
+
+(define
+  mau/ac-canon
+  (fn (m src) (mau/canon (mau/build-theory m) (mau/ac-reduce-term m src))))

lib/maude/meta.sx

@@ -0,0 +1,104 @@
+;; lib/maude/meta.sx — reflection / META-LEVEL (Phase 7).
+;;
+;; Reflection: a term can be represented AS DATA — another term — and meta-level
+;; functions interpret that representation. In Maude this is the META-LEVEL
+;; (upTerm/downTerm, metaReduce, metaApply, ...). Here object terms are already
+;; SX dicts; the META representation re-encodes a term as a term built from the
+;; meta-constructors `mt-var` and `mt-app`, so a represented term is itself a
+;; first-class object term you can build, inspect, and transform.
+;;
+;;   up-term(X:S)      = mt-var(X, S)            (names/sorts as constants)
+;;   up-term(f(a,b))   = mt-app(f, up(a), up(b))
+;;   down-term reverses.
+;;
+;; Meta-operations reflect object-level behaviour: metaReduce of a represented
+;; term in a module = the representation of its normal form, etc. The
+;; meta-circular law `down(metaReduce(up t)) =AC= reduce t` is exactly the
+;; statement that reflection agrees with the object level.
+
+(define
+  mau/up-term
+  (fn
+    (t)
+    (cond
+      ((mau/var? t)
+        (mau/app
+          "mt-var"
+          (list (mau/const (mau/vname t)) (mau/const (mau/vsort t)))))
+      ((mau/app? t)
+        (mau/app
+          "mt-app"
+          (cons (mau/const (mau/op t)) (map mau/up-term (mau/args t)))))
+      (else t))))
+
+(define
+  mau/down-term
+  (fn
+    (mt)
+    (cond
+      ((and (mau/app? mt) (= (mau/op mt) "mt-var"))
+        (mau/var
+          (mau/op (nth (mau/args mt) 0))
+          (mau/op (nth (mau/args mt) 1))))
+      ((and (mau/app? mt) (= (mau/op mt) "mt-app"))
+        (mau/app
+          (mau/op (first (mau/args mt)))
+          (map mau/down-term (rest (mau/args mt)))))
+      (else mt))))
+
+;; ---- reflective operations (term <-> meta-term) ----
+
+(define
+  mau/meta-reduce
+  (fn (m mt) (mau/up-term (mau/creduce m (mau/down-term mt)))))
+
+(define
+  mau/meta-rewrite
+  (fn (m mt) (mau/up-term (mau/rewrite m (mau/down-term mt)))))
+
+;; apply a named rule once at the top of the represented term; nil if it can't.
+(define
+  mau/meta-apply
+  (fn
+    (m label mt)
+    (let
+      ((theory (mau/build-theory m)) (eqs (mau/module-eqs m)))
+      (let
+        ((r (mau/rules-at-top theory eqs (mau/rules-with-label (mau/module-rules m) label) (mau/down-term mt))))
+        (if
+          (= r nil)
+          nil
+          (mau/up-term (mau/cnormalize theory eqs r mau/reduce-fuel)))))))
+
+;; ---- source-level conveniences ----
+
+(define mau/meta-up (fn (m src) (mau/up-term (mau/parse-term-in m src))))
+
+(define
+  mau/meta-reduce-src
+  (fn (m src) (mau/down-term (mau/meta-reduce m (mau/meta-up m src)))))
+
+(define
+  mau/meta-reduce-canon
+  (fn (m src) (mau/canon (mau/build-theory m) (mau/meta-reduce-src m src))))
+
+;; ---- generic theorem helper: equational proof by reduction ----
+
+(define
+  mau/meta-prove-equal?
+  (fn
+    (m srcA srcB)
+    (mau/ac-equal?
+      (mau/build-theory m)
+      (mau/creduce-term m srcA)
+      (mau/creduce-term m srcB))))
+
+;; meta-circular law: down(metaReduce(up t)) =AC= reduce(t)
+(define
+  mau/meta-circular?
+  (fn
+    (m src)
+    (mau/ac-equal?
+      (mau/build-theory m)
+      (mau/meta-reduce-src m src)
+      (mau/creduce-term m src))))

lib/maude/parser.sx

@@ -0,0 +1,710 @@
+;; lib/maude/parser.sx — Maude module parser.
+;;
+;; Consumes lib/guest/lex.sx (whitespace classes) and lib/guest/pratt.sx
+;; (operator-table lookup), plus lib/maude/term.sx (term constructors).
+;;
+;; Maude tokens are whitespace-delimited words plus the bracketing chars
+;; ( ) [ ] { } , — so an operator name like _+_ or s_ or if_then_else_fi is a
+;; single token. Statements end at a whitespace-delimited "." token.
+;;
+;; Grammar handled here:
+;;   (fmod|mod) NAME is ... (endfm|endm)
+;;   sort/sorts NAMES .
+;;   subsort/subsorts A B < C < D .
+;;   op/ops NAMES : ARITY -> RESULT [ATTRS] .
+;;   var/vars NAMES : SORT .
+;;   eq LHS = RHS [ATTRS] .       ceq LHS = RHS if COND [ATTRS] .
+;;   rl [L] : LHS => RHS .        crl [L] : LHS => RHS if COND .
+;;
+;; Terms: prefix application f(a,b) (op name may contain underscores, e.g.
+;; the prefix form _+_(2,3)); mixfix prefix s_ written `s X`; mixfix infix
+;; _+_ written `X + Y`, parsed by precedence climbing over a table built
+;; from the op declarations. Infix associativity follows `gather`: (E e)=left
+;; (default), (e E)=right (e.g. cons _:_), so `a : b : c` parses right-nested.
+
+;; ---------- tokenizer ----------
+
+(define
+  mau/special-char?
+  (fn
+    (c)
+    (or
+      (= c "(")
+      (= c ")")
+      (= c "[")
+      (= c "]")
+      (= c "{")
+      (= c "}")
+      (= c ","))))
+
+(define
+  mau/tokenize
+  (fn
+    (src)
+    (let
+      ((toks (list)) (pos 0) (n (len src)))
+      (define
+        peekc
+        (fn (o) (if (< (+ pos o) n) (nth src (+ pos o)) nil)))
+      (define curc (fn () (peekc 0)))
+      (define adv! (fn (k) (set! pos (+ pos k))))
+      (define
+        at-comment?
+        (fn
+          ()
+          (or
+            (and
+              (= (curc) "-")
+              (= (peekc 1) "-")
+              (= (peekc 2) "-"))
+            (and
+              (= (curc) "*")
+              (= (peekc 1) "*")
+              (= (peekc 2) "*")))))
+      (define
+        skip-line!
+        (fn
+          ()
+          (when
+            (and (< pos n) (not (= (curc) "\n")))
+            (do (adv! 1) (skip-line!)))))
+      (define
+        read-word!
+        (fn
+          (start)
+          (do
+            (when
+              (and
+                (< pos n)
+                (not (lex-whitespace? (curc)))
+                (not (mau/special-char? (curc))))
+              (do (adv! 1) (read-word! start)))
+            (slice src start pos))))
+      (define
+        scan!
+        (fn
+          ()
+          (cond
+            ((>= pos n) nil)
+            ((lex-whitespace? (curc)) (do (adv! 1) (scan!)))
+            ((at-comment?) (do (skip-line!) (scan!)))
+            ((mau/special-char? (curc))
+              (do (append! toks (curc)) (adv! 1) (scan!)))
+            (else (do (append! toks (read-word! pos)) (scan!))))))
+      (scan!)
+      toks)))
+
+;; ---------- list helpers ----------
+
+(define
+  mau/take
+  (fn
+    (xs k)
+    (if
+      (or (= k 0) (empty? xs))
+      (list)
+      (cons (first xs) (mau/take (rest xs) (- k 1))))))
+
+(define
+  mau/drop
+  (fn
+    (xs k)
+    (if
+      (or (= k 0) (empty? xs))
+      xs
+      (mau/drop (rest xs) (- k 1)))))
+
+(define
+  mau/append2
+  (fn
+    (xs ys)
+    (if (empty? xs) ys (cons (first xs) (mau/append2 (rest xs) ys)))))
+
+(define
+  mau/take-until
+  (fn
+    (xs tok)
+    (if
+      (or (empty? xs) (= (first xs) tok))
+      (list)
+      (cons (first xs) (mau/take-until (rest xs) tok)))))
+
+(define
+  mau/drop-until
+  (fn
+    (xs tok)
+    (cond
+      ((empty? xs) (list))
+      ((= (first xs) tok) xs)
+      (else (mau/drop-until (rest xs) tok)))))
+
+;; ---------- mixfix classification ----------
+
+(define
+  mau/op-form
+  (fn
+    (name)
+    (let
+      ((parts (split name "_")))
+      (cond
+        ((= (len parts) 1) {:kind :const :token name})
+        ((and (= (len parts) 3) (= (nth parts 0) "") (= (nth parts 2) "") (not (= (nth parts 1) "")))
+          {:kind :infix :token (nth parts 1)})
+        ((and (= (len parts) 2) (not (= (nth parts 0) "")) (= (nth parts 1) ""))
+          {:kind :prefix :token (nth parts 0)})
+        ((and (= (len parts) 2) (= (nth parts 0) "") (not (= (nth parts 1) "")))
+          {:kind :postfix :token (nth parts 1)})
+        (else {:kind :mixfix :token name})))))
+
+(define
+  mau/default-prec
+  (fn
+    (kind)
+    (cond
+      ((= kind "infix") 41)
+      ((= kind "prefix") 15)
+      ((= kind "postfix") 15)
+      (else 0))))
+
+(define
+  mau/op-prec
+  (fn
+    (op form)
+    (let
+      ((p (get (get op :attrs) :prec)))
+      (if (= p nil) (mau/default-prec (get form :kind)) p))))
+
+;; parse associativity from a gather spec: (E e)=left, (e E)=right.
+(define
+  mau/gather-assoc
+  (fn
+    (attrs)
+    (let
+      ((g (get attrs :gather)))
+      (if
+        (or (= g nil) (< (len g) 2))
+        "left"
+        (cond
+          ((= (nth g 1) "E") "right")
+          ((= (nth g 0) "E") "left")
+          (else "left"))))))
+
+(define
+  mau/build-infix-table
+  (fn
+    (ops)
+    (if
+      (empty? ops)
+      (list)
+      (let
+        ((op (first ops)) (rest-tbl (mau/build-infix-table (rest ops))))
+        (let
+          ((form (mau/op-form (get op :name))))
+          (if
+            (= (get form :kind) "infix")
+            (cons
+              (list
+                (get form :token)
+                (mau/op-prec op form)
+                (get op :name)
+                (mau/gather-assoc (get op :attrs)))
+              rest-tbl)
+            rest-tbl))))))
+
+(define
+  mau/build-prefix-table
+  (fn
+    (ops)
+    (if
+      (empty? ops)
+      (list)
+      (let
+        ((op (first ops)) (rest-tbl (mau/build-prefix-table (rest ops))))
+        (let
+          ((form (mau/op-form (get op :name))))
+          (if
+            (= (get form :kind) "prefix")
+            (cons
+              (list (get form :token) (mau/op-prec op form) (get op :name))
+              rest-tbl)
+            rest-tbl))))))
+
+;; ---------- term parsing ----------
+
+(define mau/has-colon? (fn (tok) (contains? tok ":")))
+
+(define
+  mau/atom->term
+  (fn
+    (tok vars)
+    (cond
+      ((mau/has-colon? tok)
+        (let
+          ((parts (split tok ":")))
+          (mau/var (nth parts 0) (nth parts 1))))
+      ((not (= (get vars tok) nil)) (mau/var tok (get vars tok)))
+      (else (mau/const tok)))))
+
+(define
+  mau/parse-term
+  (fn
+    (toks grammar)
+    (let
+      ((ts toks)
+        (pos 0)
+        (n (len toks))
+        (infix-tbl (get grammar :infix))
+        (prefix-tbl (get grammar :prefix))
+        (vars (get grammar :vars))
+        (prefix-rbp 1000))
+      (define tcur (fn () (if (< pos n) (nth ts pos) nil)))
+      (define
+        tpeek
+        (fn (o) (if (< (+ pos o) n) (nth ts (+ pos o)) nil)))
+      (define tadv! (fn () (set! pos (+ pos 1))))
+      (define
+        parse-args
+        (fn
+          ()
+          (if
+            (= (tcur) ")")
+            (do (tadv!) (list))
+            (let
+              ((acc (list)))
+              (define
+                more
+                (fn
+                  ()
+                  (do
+                    (append! acc (parse-expr 0))
+                    (when (= (tcur) ",") (do (tadv!) (more))))))
+              (do (more) (when (= (tcur) ")") (tadv!)) acc)))))
+      (define
+        parse-primary
+        (fn
+          ()
+          (let
+            ((t (tcur)))
+            (cond
+              ((= t "(")
+                (do
+                  (tadv!)
+                  (let
+                    ((e (parse-expr 0)))
+                    (do (when (= (tcur) ")") (tadv!)) e))))
+              ((not (= (pratt-op-lookup prefix-tbl t) nil))
+                (let
+                  ((entry (pratt-op-lookup prefix-tbl t)))
+                  (do
+                    (tadv!)
+                    (let
+                      ((operand (parse-expr prefix-rbp)))
+                      (mau/app (nth entry 2) (list operand))))))
+              ((= (tpeek 1) "(")
+                (let
+                  ((name t))
+                  (do (tadv!) (tadv!) (mau/app name (parse-args)))))
+              (else (do (tadv!) (mau/atom->term t vars)))))))
+      (define
+        parse-expr
+        (fn
+          (minbp)
+          (let
+            ((lhs (parse-primary)))
+            (define
+              climb
+              (fn
+                (acc)
+                (let
+                  ((t (tcur)))
+                  (let
+                    ((entry (if (= t nil) nil (pratt-op-lookup infix-tbl t))))
+                    (if
+                      (= entry nil)
+                      acc
+                      (let
+                        ((lbp (pratt-op-prec entry)))
+                        (if
+                          (< lbp minbp)
+                          acc
+                          (do
+                            (tadv!)
+                            (let
+                              ((rbp (if (= (nth entry 3) "right") lbp (+ lbp 1))))
+                              (let
+                                ((rhs (parse-expr rbp)))
+                                (climb
+                                  (mau/app
+                                    (nth entry 2)
+                                    (list acc rhs)))))))))))))
+            (climb lhs))))
+      (parse-expr 0))))
+
+;; ---------- statement splitting ----------
+
+(define
+  mau/split-statements
+  (fn
+    (toks)
+    (let
+      ((stmts (list)) (cur (list)))
+      (define
+        flush!
+        (fn
+          ()
+          (when
+            (not (empty? cur))
+            (do (append! stmts cur) (set! cur (list))))))
+      (define
+        loop
+        (fn
+          (ts)
+          (cond
+            ((empty? ts) (flush!))
+            ((= (first ts) ".") (do (flush!) (loop (rest ts))))
+            (else (do (append! cur (first ts)) (loop (rest ts)))))))
+      (do (loop toks) stmts))))
+
+(define
+  mau/split-groups
+  (fn
+    (toks)
+    (let
+      ((groups (list)) (cur (list)))
+      (define flush! (fn () (do (append! groups cur) (set! cur (list)))))
+      (define
+        loop
+        (fn
+          (ts)
+          (cond
+            ((empty? ts) (flush!))
+            ((= (first ts) "<") (do (flush!) (loop (rest ts))))
+            (else (do (append! cur (first ts)) (loop (rest ts)))))))
+      (do (loop toks) groups))))
+
+;; ---------- attributes ----------
+
+(define mau/strip-brackets (fn (toks) (mau/take-until (rest toks) "]")))
+
+(define
+  mau/parse-attr-tokens
+  (fn
+    (toks)
+    (let
+      ((acc {}))
+      (define
+        loop
+        (fn
+          (ts)
+          (cond
+            ((empty? ts) nil)
+            ((= (first ts) "assoc")
+              (do (dict-set! acc :assoc true) (loop (rest ts))))
+            ((= (first ts) "comm")
+              (do (dict-set! acc :comm true) (loop (rest ts))))
+            ((or (= (first ts) "idem") (= (first ts) "idempotent"))
+              (do (dict-set! acc :idem true) (loop (rest ts))))
+            ((= (first ts) "ctor")
+              (do (dict-set! acc :ctor true) (loop (rest ts))))
+            ((= (first ts) "owise")
+              (do (dict-set! acc :owise true) (loop (rest ts))))
+            ((= (first ts) "id:")
+              (do
+                (dict-set! acc :id (nth ts 1))
+                (loop (mau/drop ts 2))))
+            ((= (first ts) "prec")
+              (do
+                (dict-set! acc :prec (parse-number (nth ts 1)))
+                (loop (mau/drop ts 2))))
+            ((= (first ts) "label")
+              (do
+                (dict-set! acc :label (nth ts 1))
+                (loop (mau/drop ts 2))))
+            ((= (first ts) "gather")
+              (let
+                ((after2 (mau/drop ts 2)))
+                (do
+                  (dict-set! acc :gather (mau/take-until after2 ")"))
+                  (loop (rest (mau/drop-until after2 ")"))))))
+            (else (loop (rest ts))))))
+      (do (loop toks) acc))))
+
+(define
+  mau/parse-attrs
+  (fn
+    (toks)
+    (if
+      (or (empty? toks) (not (= (first toks) "[")))
+      {}
+      (mau/parse-attr-tokens (mau/strip-brackets toks)))))
+
+;; Split a token sequence into {:term tokens-before-bracket :attrs parsed}.
+(define mau/split-attrs (fn (toks) {:attrs (mau/parse-attrs (mau/drop-until toks "[")) :term (mau/take-until toks "[")}))
+
+;; ---------- signature collection ----------
+
+(define
+  mau/append-each!
+  (fn (acc xs) (for-each (fn (x) (append! acc x)) xs)))
+
+(define
+  mau/register-ops!
+  (fn
+    (ops names arity result attrs)
+    (for-each (fn (nm) (append! ops {:name nm :attrs attrs :arity arity :result result})) names)))
+
+(define
+  mau/each-set-var!
+  (fn
+    (vars names sort)
+    (for-each (fn (nm) (dict-set! vars nm sort)) names)))
+
+(define
+  mau/cross-append!
+  (fn
+    (acc g1 g2)
+    (for-each
+      (fn
+        (sub)
+        (for-each (fn (super) (append! acc (list sub super))) g2))
+      g1)))
+
+(define
+  mau/add-subsort-chain!
+  (fn
+    (acc groups)
+    (when
+      (and (not (empty? groups)) (not (empty? (rest groups))))
+      (do
+        (mau/cross-append! acc (first groups) (nth groups 1))
+        (mau/add-subsort-chain! acc (rest groups))))))
+
+(define
+  mau/add-subsorts!
+  (fn (acc body) (mau/add-subsort-chain! acc (mau/split-groups body))))
+
+(define
+  mau/add-vars!
+  (fn
+    (vars body)
+    (let
+      ((names (mau/take-until body ":"))
+        (sort (first (rest (mau/drop-until body ":")))))
+      (mau/each-set-var! vars names sort))))
+
+(define
+  mau/add-ops!
+  (fn
+    (ops body)
+    (let
+      ((names (mau/take-until body ":"))
+        (afterc (rest (mau/drop-until body ":"))))
+      (let
+        ((arity (mau/take-until afterc "->"))
+          (aftera (rest (mau/drop-until afterc "->"))))
+        (let
+          ((result (first aftera))
+            (attrs (mau/parse-attrs (mau/drop aftera 1))))
+          (mau/register-ops! ops names arity result attrs))))))
+
+(define
+  mau/collect-sig!
+  (fn
+    (stmts sorts subsorts ops vars)
+    (for-each
+      (fn
+        (s)
+        (let
+          ((head (first s)) (body (rest s)))
+          (cond
+            ((or (= head "sort") (= head "sorts"))
+              (mau/append-each! sorts body))
+            ((or (= head "subsort") (= head "subsorts"))
+              (mau/add-subsorts! subsorts body))
+            ((or (= head "op") (= head "ops")) (mau/add-ops! ops body))
+            ((or (= head "var") (= head "vars")) (mau/add-vars! vars body))
+            (else nil))))
+      stmts)))
+
+;; ---------- equations / rules ----------
+
+(define
+  mau/parse-cond
+  (fn
+    (toks grammar)
+    (if
+      (mau/member? "=" toks)
+      (let
+        ((l (mau/take-until toks "="))
+          (r (rest (mau/drop-until toks "="))))
+        {:lhs (mau/parse-term l grammar) :kind :eq :rhs (mau/parse-term r grammar)})
+      {:kind :bool :term (mau/parse-term toks grammar)})))
+
+(define
+  mau/parse-eq
+  (fn
+    (body grammar conditional?)
+    (let
+      ((lhs-toks (mau/take-until body "="))
+        (after (rest (mau/drop-until body "="))))
+      (if
+        conditional?
+        (let
+          ((rhs-toks (mau/take-until after "if"))
+            (cond-raw (rest (mau/drop-until after "if"))))
+          (let ((csplit (mau/split-attrs cond-raw))) {:lhs (mau/parse-term lhs-toks grammar) :t :eq :cond (mau/parse-cond (get csplit :term) grammar) :rhs (mau/parse-term rhs-toks grammar) :owise (= (get (get csplit :attrs) :owise) true)}))
+        (let ((rsplit (mau/split-attrs after))) {:lhs (mau/parse-term lhs-toks grammar) :t :eq :cond nil :rhs (mau/parse-term (get rsplit :term) grammar) :owise (= (get (get rsplit :attrs) :owise) true)})))))
+
+(define
+  mau/strip-label
+  (fn
+    (body)
+    (if
+      (and (not (empty? body)) (= (first body) "["))
+      (let
+        ((label (nth body 1)) (after (mau/drop body 3)))
+        (if
+          (and (not (empty? after)) (= (first after) ":"))
+          {:label label :rest (rest after)}
+          {:label label :rest after}))
+      {:label nil :rest body})))
+
+(define
+  mau/parse-rule
+  (fn
+    (body grammar conditional?)
+    (let
+      ((b (mau/strip-label body)))
+      (let
+        ((label (get b :label)) (rest-toks (get b :rest)))
+        (let
+          ((lhs-toks (mau/take-until rest-toks "=>"))
+            (after (rest (mau/drop-until rest-toks "=>"))))
+          (if
+            conditional?
+            (let
+              ((rhs-toks (mau/take-until after "if"))
+                (cond-toks (rest (mau/drop-until after "if"))))
+              {:lhs (mau/parse-term lhs-toks grammar) :label label :t :rule :cond (mau/parse-cond (get (mau/split-attrs cond-toks) :term) grammar) :rhs (mau/parse-term rhs-toks grammar)})
+            {:lhs (mau/parse-term lhs-toks grammar) :label label :t :rule :cond nil :rhs (mau/parse-term (get (mau/split-attrs after) :term) grammar)}))))))
+
+(define
+  mau/collect-rules!
+  (fn
+    (stmts grammar eqs rules)
+    (for-each
+      (fn
+        (s)
+        (let
+          ((head (first s)) (body (rest s)))
+          (cond
+            ((= head "eq") (append! eqs (mau/parse-eq body grammar false)))
+            ((= head "ceq") (append! eqs (mau/parse-eq body grammar true)))
+            ((= head "rl")
+              (append! rules (mau/parse-rule body grammar false)))
+            ((= head "crl")
+              (append! rules (mau/parse-rule body grammar true)))
+            (else nil))))
+      stmts)))
+
+;; ---------- module assembly ----------
+
+(define mau/make-grammar (fn (ops vars) {:prefix (mau/build-prefix-table ops) :ops ops :vars vars :infix (mau/build-infix-table ops)}))
+
+(define
+  mau/build-module
+  (fn
+    (kind name body)
+    (let
+      ((stmts (mau/split-statements body))
+        (sorts (list))
+        (subsorts (list))
+        (ops (list))
+        (vars {})
+        (eqs (list))
+        (rules (list)))
+      (mau/collect-sig! stmts sorts subsorts ops vars)
+      (let
+        ((grammar (mau/make-grammar ops vars)))
+        (mau/collect-rules! stmts grammar eqs rules)
+        {:name name :grammar grammar :sorts sorts :eqs eqs :ops ops :t :module :vars vars :subsorts subsorts :kind kind :rules rules}))))
+
+(define
+  mau/parse-module
+  (fn
+    (src)
+    (let
+      ((toks (mau/tokenize src)))
+      (let
+        ((kind (nth toks 0)) (name (nth toks 1)))
+        (let
+          ((body (mau/take (mau/drop toks 3) (- (len toks) 4))))
+          (mau/build-module kind name body))))))
+
+;; ---------- signature queries ----------
+
+(define mau/module-name (fn (m) (get m :name)))
+(define mau/module-kind (fn (m) (get m :kind)))
+(define mau/module-sorts (fn (m) (get m :sorts)))
+(define mau/module-subsorts (fn (m) (get m :subsorts)))
+(define mau/module-ops (fn (m) (get m :ops)))
+(define mau/module-vars (fn (m) (get m :vars)))
+(define mau/module-eqs (fn (m) (get m :eqs)))
+(define mau/module-rules (fn (m) (get m :rules)))
+(define mau/module-grammar (fn (m) (get m :grammar)))
+
+(define
+  mau/parse-term-in
+  (fn (m src) (mau/parse-term (mau/tokenize src) (mau/module-grammar m))))
+
+(define
+  mau/collect-supers
+  (fn
+    (pairs s)
+    (cond
+      ((empty? pairs) (list))
+      ((= (first (first pairs)) s)
+        (cons
+          (nth (first pairs) 1)
+          (mau/collect-supers (rest pairs) s)))
+      (else (mau/collect-supers (rest pairs) s)))))
+
+(define mau/supers-of (fn (m s) (mau/collect-supers (get m :subsorts) s)))
+
+(define
+  mau/dfs-reach
+  (fn
+    (m frontier target seen)
+    (cond
+      ((empty? frontier) false)
+      ((= (first frontier) target) true)
+      ((mau/member? (first frontier) seen)
+        (mau/dfs-reach m (rest frontier) target seen))
+      (else
+        (mau/dfs-reach
+          m
+          (mau/append2 (mau/supers-of m (first frontier)) (rest frontier))
+          target
+          (cons (first frontier) seen))))))
+
+(define
+  mau/subsort?
+  (fn
+    (m sub super)
+    (mau/dfs-reach m (mau/supers-of m sub) super (list sub))))
+
+(define mau/sort<=? (fn (m a b) (or (= a b) (mau/subsort? m a b))))
+
+(define
+  mau/filter-ops
+  (fn
+    (ops name)
+    (cond
+      ((empty? ops) (list))
+      ((= (get (first ops) :name) name)
+        (cons (first ops) (mau/filter-ops (rest ops) name)))
+      (else (mau/filter-ops (rest ops) name)))))
+
+(define
+  mau/ops-named
+  (fn (m name) (mau/filter-ops (mau/module-ops m) name)))

lib/maude/pretty.sx

@@ -0,0 +1,82 @@
+;; lib/maude/pretty.sx — mixfix surface-syntax printer.
+;;
+;; term->str renders the internal prefix form (`_+_(s_(X), 0)`); this renders
+;; terms back in Maude mixfix surface syntax (`((s X) + 0)`), driven by the
+;; operator forms in the module signature. Fully parenthesised — unambiguous
+;; rather than minimal. Constants and unknown ops fall back to prefix form.
+
+(define
+  mau/render-forms
+  (fn
+    (m)
+    (let
+      ((tbl {}))
+      (for-each
+        (fn
+          (op)
+          (dict-set! tbl (get op :name) (mau/op-form (get op :name))))
+        (mau/module-ops m))
+      tbl)))
+
+(define
+  mau/render-args
+  (fn
+    (forms args)
+    (cond
+      ((empty? args) "")
+      ((empty? (rest args)) (mau/render-term forms (first args)))
+      (else
+        (str
+          (mau/render-term forms (first args))
+          ", "
+          (mau/render-args forms (rest args)))))))
+
+(define
+  mau/render-term
+  (fn
+    (forms t)
+    (cond
+      ((mau/var? t) (mau/vname t))
+      ((mau/app? t)
+        (let
+          ((form (get forms (mau/op t))) (args (mau/args t)))
+          (cond
+            ((empty? args) (mau/op t))
+            ((and form (= (get form :kind) "infix") (= (len args) 2))
+              (str
+                "("
+                (mau/render-term forms (nth args 0))
+                " "
+                (get form :token)
+                " "
+                (mau/render-term forms (nth args 1))
+                ")"))
+            ((and form (= (get form :kind) "prefix") (= (len args) 1))
+              (str
+                "("
+                (get form :token)
+                " "
+                (mau/render-term forms (first args))
+                ")"))
+            ((and form (= (get form :kind) "postfix") (= (len args) 1))
+              (str
+                "("
+                (mau/render-term forms (first args))
+                " "
+                (get form :token)
+                ")"))
+            (else (str (mau/op t) "(" (mau/render-args forms args) ")")))))
+      (else (str t)))))
+
+(define
+  mau/term->maude
+  (fn (m t) (mau/render-term (mau/render-forms m) t)))
+
+;; reduce / rewrite then render in surface syntax
+(define
+  mau/red->maude
+  (fn (m src) (mau/term->maude m (mau/creduce-term m src))))
+
+(define
+  mau/rew->maude
+  (fn (m src) (mau/term->maude m (mau/rewrite-term m src))))

lib/maude/reduce.sx

@@ -0,0 +1,143 @@
+;; lib/maude/reduce.sx — syntactic equational reduction (Phase 2).
+;;
+;; Apply unconditional equations left-to-right to a fixpoint, using strict
+;; one-sided syntactic matching (no theories yet — assoc/comm/id come in
+;; Phase 3). Reduction is innermost: arguments are normalised before the
+;; enclosing operator is rewritten.
+;;
+;; A substitution is a dict VAR-NAME -> term, extended immutably via `assoc`.
+;; Matching is one-sided: only the pattern (equation LHS) carries variables;
+;; the subject is treated structurally.
+
+;; ---------- matching ----------
+
+(define
+  mau/match
+  (fn
+    (pat subj s)
+    (cond
+      ((= s nil) nil)
+      ((mau/var? pat)
+        (let
+          ((bound (get s (mau/vname pat))))
+          (if
+            (= bound nil)
+            (assoc s (mau/vname pat) subj)
+            (if (mau/term=? bound subj) s nil))))
+      ((and (mau/app? pat) (mau/app? subj))
+        (if
+          (and
+            (= (mau/op pat) (mau/op subj))
+            (= (mau/arity pat) (mau/arity subj)))
+          (mau/match-args (mau/args pat) (mau/args subj) s)
+          nil))
+      (else nil))))
+
+(define
+  mau/match-args
+  (fn
+    (ps ss s)
+    (cond
+      ((= s nil) nil)
+      ((and (empty? ps) (empty? ss)) s)
+      ((or (empty? ps) (empty? ss)) nil)
+      (else
+        (mau/match-args
+          (rest ps)
+          (rest ss)
+          (mau/match (first ps) (first ss) s))))))
+
+;; ---------- substitution application ----------
+
+(define
+  mau/subst-apply-list
+  (fn
+    (s args)
+    (if
+      (empty? args)
+      (list)
+      (cons
+        (mau/subst-apply s (first args))
+        (mau/subst-apply-list s (rest args))))))
+
+(define
+  mau/subst-apply
+  (fn
+    (s term)
+    (cond
+      ((mau/var? term)
+        (let ((b (get s (mau/vname term)))) (if (= b nil) term b)))
+      ((mau/app? term)
+        (mau/app (mau/op term) (mau/subst-apply-list s (mau/args term))))
+      (else term))))
+
+;; ---------- top-level rewrite ----------
+
+;; Try each unconditional equation in order; on the first whose LHS matches
+;; the term, return the instantiated RHS. nil if none apply.
+(define
+  mau/rewrite-top
+  (fn
+    (eqs term)
+    (cond
+      ((empty? eqs) nil)
+      (else
+        (let
+          ((eq (first eqs)))
+          (if
+            (= (get eq :cond) nil)
+            (let
+              ((s (mau/match (get eq :lhs) term {})))
+              (if
+                (= s nil)
+                (mau/rewrite-top (rest eqs) term)
+                (mau/subst-apply s (get eq :rhs))))
+            (mau/rewrite-top (rest eqs) term)))))))
+
+;; ---------- normalisation (innermost to fixpoint) ----------
+
+(define
+  mau/normalize-args
+  (fn
+    (eqs args fuel)
+    (if
+      (empty? args)
+      (list)
+      (cons
+        (mau/normalize eqs (first args) fuel)
+        (mau/normalize-args eqs (rest args) fuel)))))
+
+(define
+  mau/normalize
+  (fn
+    (eqs term fuel)
+    (if
+      (<= fuel 0)
+      term
+      (cond
+        ((mau/var? term) term)
+        ((mau/app? term)
+          (let
+            ((nargs (mau/normalize-args eqs (mau/args term) fuel)))
+            (let
+              ((t2 (mau/app (mau/op term) nargs)))
+              (let
+                ((r (mau/rewrite-top eqs t2)))
+                (if (= r nil) t2 (mau/normalize eqs r (- fuel 1)))))))
+        (else term)))))
+
+;; ---------- module-level API ----------
+
+(define mau/reduce-fuel 1000000)
+
+(define
+  mau/reduce
+  (fn (m term) (mau/normalize (mau/module-eqs m) term mau/reduce-fuel)))
+
+(define
+  mau/reduce-term
+  (fn (m src) (mau/reduce m (mau/parse-term-in m src))))
+
+(define
+  mau/reduce->str
+  (fn (m src) (mau/term->str (mau/reduce-term m src))))

lib/maude/rewrite.sx

@@ -0,0 +1,284 @@
+;; lib/maude/rewrite.sx — system modules + rewrite rules (Phase 5).
+;;
+;; Equations (eq/ceq) are applied to a fixpoint to NORMALISE (confluent by
+;; intent). Rules (rl/crl) are TRANSITIONS: asymmetric (=>), possibly
+;; nondeterministic, NOT applied to a fixpoint. Maude's `rew` interleaves
+;; the two: normalise with equations, fire one rule, renormalise, repeat.
+;;
+;; Rule firing reuses the shared firing machinery — a rule dict carries
+;; :lhs/:rhs/:cond exactly like an equation, so `mau/fire-eq` (short-circuit,
+;; fire.sx) applies unchanged (matching modulo the AC theory; crl guards
+;; evaluated with the equations). A rule fires only if it both progresses and
+;; its condition holds.
+;;
+;; `mau/rewrite` follows the default strategy (top-down, leftmost-outermost,
+;; first applicable rule) for one path. `mau/search` does breadth-first reach
+;; over ALL one-step successors — for puzzle solvers / protocol simulators
+;; where the answer is on a branch `rew` would not take.
+
+(define mau/rew-fuel 100000)
+
+;; ---- single-step, default strategy (first applicable, leftmost-outermost) ----
+
+(define
+  mau/rules-at-top
+  (fn
+    (theory eqs rules term)
+    (if
+      (empty? rules)
+      nil
+      (let
+        ((r (mau/fire-eq theory eqs (first rules) term)))
+        (if (= r nil) (mau/rules-at-top theory eqs (rest rules) term) r)))))
+
+(define
+  mau/apply-rule-once
+  (fn
+    (theory eqs rules term)
+    (let
+      ((top (mau/rules-at-top theory eqs rules term)))
+      (if
+        (not (= top nil))
+        top
+        (if
+          (mau/app? term)
+          (mau/apply-rule-in-args
+            theory
+            eqs
+            rules
+            (mau/op term)
+            (mau/args term)
+            (list))
+          nil)))))
+
+(define
+  mau/apply-rule-in-args
+  (fn
+    (theory eqs rules op done todo)
+    (if
+      (empty? todo)
+      nil
+      (let
+        ((r (mau/apply-rule-once theory eqs rules (first todo))))
+        (if
+          (= r nil)
+          (mau/apply-rule-in-args
+            theory
+            eqs
+            rules
+            op
+            (mau/append2 done (list (first todo)))
+            (rest todo))
+          (mau/app op (mau/append2 done (cons r (rest todo)))))))))
+
+(define
+  mau/rewrite-steps
+  (fn
+    (theory eqs rules term steps)
+    (if
+      (<= steps 0)
+      (mau/cnormalize theory eqs term mau/reduce-fuel)
+      (let
+        ((nf (mau/cnormalize theory eqs term mau/reduce-fuel)))
+        (let
+          ((r (mau/apply-rule-once theory eqs rules nf)))
+          (if
+            (= r nil)
+            nf
+            (mau/rewrite-steps theory eqs rules r (- steps 1))))))))
+
+(define
+  mau/rewrite
+  (fn
+    (m term)
+    (mau/rewrite-steps
+      (mau/build-theory m)
+      (mau/module-eqs m)
+      (mau/module-rules m)
+      term
+      mau/rew-fuel)))
+
+(define
+  mau/rew
+  (fn
+    (m src n)
+    (mau/rewrite-steps
+      (mau/build-theory m)
+      (mau/module-eqs m)
+      (mau/module-rules m)
+      (mau/parse-term-in m src)
+      n)))
+
+(define
+  mau/rewrite-term
+  (fn (m src) (mau/rewrite m (mau/parse-term-in m src))))
+
+(define
+  mau/rewrite->str
+  (fn (m src) (mau/term->str (mau/rewrite-term m src))))
+
+(define
+  mau/rewrite-canon
+  (fn (m src) (mau/canon (mau/build-theory m) (mau/rewrite-term m src))))
+
+(define mau/rew->str (fn (m src n) (mau/term->str (mau/rew m src n))))
+
+(define
+  mau/rew-canon
+  (fn (m src n) (mau/canon (mau/build-theory m) (mau/rew m src n))))
+
+;; ---- all one-step successors (for search; eager enumeration) ----
+
+(define
+  mau/cands-results
+  (fn
+    (theory eqs cond term cands)
+    (mau/concat-map
+      (fn
+        (c)
+        (if
+          (and
+            (not (mau/ac-equal? theory (get c :result) term))
+            (mau/cond-holds? theory eqs cond (get c :s)))
+          (list (mau/cnormalize theory eqs (get c :result) mau/reduce-fuel))
+          (list)))
+      cands)))
+
+(define
+  mau/top-successors
+  (fn
+    (theory eqs rules term)
+    (mau/concat-map
+      (fn
+        (rule)
+        (mau/cands-results
+          theory
+          eqs
+          (get rule :cond)
+          term
+          (mau/eq-candidates theory rule term)))
+      rules)))
+
+(define
+  mau/arg-successors
+  (fn
+    (theory eqs rules op done todo)
+    (if
+      (empty? todo)
+      (list)
+      (mau/append2
+        (map
+          (fn
+            (sub)
+            (mau/app op (mau/append2 done (cons sub (rest todo)))))
+          (mau/all-successors theory eqs rules (first todo)))
+        (mau/arg-successors
+          theory
+          eqs
+          rules
+          op
+          (mau/append2 done (list (first todo)))
+          (rest todo))))))
+
+(define
+  mau/all-successors
+  (fn
+    (theory eqs rules term)
+    (mau/append2
+      (mau/top-successors theory eqs rules term)
+      (if
+        (mau/app? term)
+        (mau/arg-successors
+          theory
+          eqs
+          rules
+          (mau/op term)
+          (mau/args term)
+          (list))
+        (list)))))
+
+(define
+  mau/successors
+  (fn
+    (m src)
+    (let
+      ((theory (mau/build-theory m)) (eqs (mau/module-eqs m)))
+      (map
+        (fn (t) (mau/canon theory t))
+        (mau/all-successors
+          theory
+          eqs
+          (mau/module-rules m)
+          (mau/cnormalize
+            theory
+            eqs
+            (mau/parse-term-in m src)
+            mau/reduce-fuel))))))
+
+;; ---- breadth-first reachability search ----
+
+(define
+  mau/canon-list
+  (fn (theory ts) (map (fn (t) (mau/canon theory t)) ts)))
+
+(define
+  mau/bfs-search
+  (fn
+    (theory eqs rules frontier seen goal depth)
+    (cond
+      ((mau/member? goal (mau/canon-list theory frontier)) true)
+      ((<= depth 0) false)
+      ((empty? frontier) false)
+      (else
+        (let
+          ((newf (list)) (newseen seen))
+          (for-each
+            (fn
+              (t)
+              (for-each
+                (fn
+                  (succ)
+                  (let
+                    ((c (mau/canon theory succ)))
+                    (when
+                      (not (mau/member? c newseen))
+                      (do
+                        (set! newseen (cons c newseen))
+                        (append! newf succ)))))
+                (mau/all-successors theory eqs rules t)))
+            frontier)
+          (mau/bfs-search
+            theory
+            eqs
+            rules
+            newf
+            newseen
+            goal
+            (- depth 1)))))))
+
+(define
+  mau/search
+  (fn
+    (m start-src goal-src max-depth)
+    (let
+      ((theory (mau/build-theory m))
+        (eqs (mau/module-eqs m))
+        (rules (mau/module-rules m)))
+      (let
+        ((start (mau/cnormalize theory eqs (mau/parse-term-in m start-src) mau/reduce-fuel))
+          (goal
+            (mau/canon
+              theory
+              (mau/cnormalize
+                theory
+                eqs
+                (mau/parse-term-in m goal-src)
+                mau/reduce-fuel))))
+        (mau/bfs-search
+          theory
+          eqs
+          rules
+          (list start)
+          (list (mau/canon theory start))
+          goal
+          max-depth)))))

lib/maude/run.sx

@@ -0,0 +1,132 @@
+;; lib/maude/run.sx — run a Maude program: a module followed by commands.
+;;
+;; Parses a single fmod/mod ... endfm/endm module plus trailing commands and
+;; executes them, Maude-style:
+;;   reduce TERM .   (alias: red)   — normalise with equations
+;;   rewrite TERM .  (alias: rew)   — apply rules under the default strategy
+;;   search START =>* GOAL .         — reachability (=>*, =>+, =>! all treated
+;;                                     as reachability); reports the path
+;; `... in MODNAME : TERM .` is accepted (the module qualifier is ignored —
+;; there is one module in scope). reduce/rewrite results carry the least sort,
+;; rendered Maude-style by mau/run-pretty as `result SORT: TERM`.
+
+(define mau/search-depth 200)
+
+(define
+  mau/module-end-idx
+  (fn
+    (toks i)
+    (cond
+      ((>= i (len toks)) (- 0 1))
+      ((or (= (nth toks i) "endfm") (= (nth toks i) "endm")) i)
+      (else (mau/module-end-idx toks (+ i 1))))))
+
+(define
+  mau/parse-module-from-toks
+  (fn
+    (toks)
+    (let
+      ((kind (nth toks 0)) (name (nth toks 1)))
+      (mau/build-module
+        kind
+        name
+        (mau/take (mau/drop toks 3) (- (len toks) 4))))))
+
+(define
+  mau/strip-in
+  (fn
+    (toks)
+    (if
+      (and (not (empty? toks)) (= (first toks) "in"))
+      (rest (mau/drop-until toks ":"))
+      toks)))
+
+(define
+  mau/find-arrow
+  (fn
+    (toks)
+    (cond
+      ((empty? toks) nil)
+      ((and (>= (len (first toks)) 2) (= (slice (first toks) 0 2) "=>"))
+        (first toks))
+      (else (mau/find-arrow (rest toks))))))
+
+(define
+  mau/run-search
+  (fn
+    (m term-toks)
+    (let
+      ((arrow (mau/find-arrow term-toks)) (g (mau/module-grammar m)))
+      (if
+        (= arrow nil)
+        {:path nil :cmd "search" :result "no arrow"}
+        (let
+          ((start-toks (mau/take-until term-toks arrow))
+            (goal-toks (rest (mau/drop-until term-toks arrow))))
+          (let
+            ((path (mau/search-path-terms m (mau/parse-term start-toks g) (mau/parse-term goal-toks g) mau/search-depth)))
+            {:path path :cmd "search" :result (if (= path nil) "no solution" (join " => " path))}))))))
+
+(define
+  mau/run-command
+  (fn
+    (m stmt)
+    (let
+      ((head (first stmt)))
+      (if
+        (or (= head "search") (= head "srch"))
+        (mau/run-search m (rest stmt))
+        (let
+          ((t (mau/parse-term (mau/strip-in (rest stmt)) (mau/module-grammar m))))
+          (cond
+            ((or (= head "reduce") (= head "red"))
+              (let ((r (mau/creduce m t))) {:cmd "reduce" :sort (mau/term-sort m r) :result (mau/term->maude m r)}))
+            ((or (= head "rewrite") (= head "rew"))
+              (let ((r (mau/rewrite m t))) {:cmd "rewrite" :sort (mau/term-sort m r) :result (mau/term->maude m r)}))
+            (else {:cmd head :result "?"})))))))
+
+(define
+  mau/run-commands
+  (fn
+    (m stmts)
+    (if
+      (empty? stmts)
+      (list)
+      (if
+        (empty? (first stmts))
+        (mau/run-commands m (rest stmts))
+        (cons
+          (mau/run-command m (first stmts))
+          (mau/run-commands m (rest stmts)))))))
+
+(define
+  mau/run-program
+  (fn
+    (src)
+    (let
+      ((toks (mau/tokenize src)))
+      (let
+        ((eidx (mau/module-end-idx toks 0)))
+        (let
+          ((m (mau/parse-module-from-toks (mau/take toks (+ eidx 1))))
+            (cmd-toks (mau/drop toks (+ eidx 1))))
+          (mau/run-commands m (mau/split-statements cmd-toks)))))))
+
+;; just the rendered result strings
+(define
+  mau/run
+  (fn (src) (map (fn (r) (get r :result)) (mau/run-program src))))
+
+;; Maude-style printout: `result SORT: TERM` for reduce/rewrite, the path for search
+(define
+  mau/run-pretty
+  (fn
+    (src)
+    (map
+      (fn
+        (r)
+        (if
+          (= (get r :cmd) "search")
+          (str "search: " (get r :result))
+          (str "result " (get r :sort) ": " (get r :result))))
+      (mau/run-program src))))

lib/maude/scoreboard.json

@@ -0,0 +1,24 @@
+{
+  "lang": "maude",
+  "total_passed": 274,
+  "total_failed": 0,
+  "total": 274,
+  "suites": [
+    {"name":"parse","passed":65,"failed":0,"total":65},
+    {"name":"reduce","passed":26,"failed":0,"total":26},
+    {"name":"matching","passed":28,"failed":0,"total":28},
+    {"name":"confluence","passed":12,"failed":0,"total":12},
+    {"name":"conditional","passed":19,"failed":0,"total":19},
+    {"name":"owise","passed":8,"failed":0,"total":8},
+    {"name":"gather","passed":7,"failed":0,"total":7},
+    {"name":"sorts","passed":14,"failed":0,"total":14},
+    {"name":"rewrite","passed":21,"failed":0,"total":21},
+    {"name":"searchpath","passed":8,"failed":0,"total":8},
+    {"name":"strategy","passed":19,"failed":0,"total":19},
+    {"name":"meta","passed":18,"failed":0,"total":18},
+    {"name":"pretty","passed":11,"failed":0,"total":11},
+    {"name":"run","passed":10,"failed":0,"total":10},
+    {"name":"effects","passed":8,"failed":0,"total":8}
+  ],
+  "generated": "2026-06-07T20:18:07+00:00"
+}

lib/maude/scoreboard.md

@@ -0,0 +1,21 @@
+# maude scoreboard
+
+**274 / 274 passing** (0 failure(s)).
+
+| Suite | Passed | Total | Status |
+|-------|--------|-------|--------|
+| parse | 65 | 65 | ok |
+| reduce | 26 | 26 | ok |
+| matching | 28 | 28 | ok |
+| confluence | 12 | 12 | ok |
+| conditional | 19 | 19 | ok |
+| owise | 8 | 8 | ok |
+| gather | 7 | 7 | ok |
+| sorts | 14 | 14 | ok |
+| rewrite | 21 | 21 | ok |
+| searchpath | 8 | 8 | ok |
+| strategy | 19 | 19 | ok |
+| meta | 18 | 18 | ok |
+| pretty | 11 | 11 | ok |
+| run | 10 | 10 | ok |
+| effects | 8 | 8 | ok |

lib/maude/searchpath.sx

@@ -0,0 +1,103 @@
+;; lib/maude/searchpath.sx — reachability search returning the witness path.
+;;
+;; mau/search (rewrite.sx) answers yes/no. For puzzle solvers you want the
+;; actual sequence of states from start to goal. mau/search-path runs the same
+;; BFS but threads the path so far; it returns the list of canonical states
+;; start..goal (shortest by step count) or nil if unreachable within depth.
+
+(define mau/reverse2 (fn (xs) (mau/rev-acc xs (list))))
+
+(define
+  mau/rev-acc
+  (fn
+    (xs acc)
+    (if (empty? xs) acc (mau/rev-acc (rest xs) (cons (first xs) acc)))))
+
+;; find a frontier path whose current state (its head) matches the goal canon
+(define
+  mau/path-hit
+  (fn
+    (theory frontier goal)
+    (cond
+      ((empty? frontier) nil)
+      ((= (mau/canon theory (first (first frontier))) goal)
+        (first frontier))
+      (else (mau/path-hit theory (rest frontier) goal)))))
+
+(define
+  mau/bfs-path
+  (fn
+    (theory eqs rules frontier seen goal depth)
+    (let
+      ((hit (mau/path-hit theory frontier goal)))
+      (cond
+        ((not (= hit nil)) hit)
+        ((<= depth 0) nil)
+        ((empty? frontier) nil)
+        (else
+          (let
+            ((newf (list)) (newseen seen))
+            (for-each
+              (fn
+                (path)
+                (for-each
+                  (fn
+                    (succ)
+                    (let
+                      ((c (mau/canon theory succ)))
+                      (when
+                        (not (mau/member? c newseen))
+                        (do
+                          (set! newseen (cons c newseen))
+                          (append! newf (cons succ path))))))
+                  (mau/all-successors theory eqs rules (first path))))
+              frontier)
+            (mau/bfs-path
+              theory
+              eqs
+              rules
+              newf
+              newseen
+              goal
+              (- depth 1))))))))
+
+;; term-level: returns the canonical-state path start..goal, or nil
+(define
+  mau/search-path-terms
+  (fn
+    (m start-term goal-term max-depth)
+    (let
+      ((theory (mau/build-theory m))
+        (eqs (mau/module-eqs m))
+        (rules (mau/module-rules m)))
+      (let
+        ((start (mau/cnormalize theory eqs start-term mau/reduce-fuel))
+          (goal
+            (mau/canon
+              theory
+              (mau/cnormalize theory eqs goal-term mau/reduce-fuel))))
+        (let
+          ((res (mau/bfs-path theory eqs rules (list (list start)) (list (mau/canon theory start)) goal max-depth)))
+          (if
+            (= res nil)
+            nil
+            (map (fn (t) (mau/canon theory t)) (mau/reverse2 res))))))))
+
+(define
+  mau/search-path
+  (fn
+    (m start-src goal-src max-depth)
+    (mau/search-path-terms
+      m
+      (mau/parse-term-in m start-src)
+      (mau/parse-term-in m goal-src)
+      max-depth)))
+
+;; number of steps in the shortest solution (nil if unreachable)
+(define
+  mau/search-length
+  (fn
+    (m start-src goal-src max-depth)
+    (let
+      ((p (mau/search-path m start-src goal-src max-depth)))
+      (if (= p nil) nil (- (len p) 1)))))

lib/maude/sorts.sx

@@ -0,0 +1,87 @@
+;; lib/maude/sorts.sx — order-sorted least-sort inference.
+;;
+;; Order-sorted signatures: subsorts induce a partial order on sorts, and an
+;; overloaded operator can have several declarations. The LEAST SORT of a term
+;; is the smallest result sort among the operator declarations whose argument
+;; sorts the actual arguments satisfy (modulo subsorting). This is what lets
+;; `f(1)` be a NzNat while `f(s 0)` is only a Nat when f is declared at both.
+;;
+;;   mau/term-sort   M T        -> least sort of T (string, "?" if unknown)
+;;   mau/has-sort?   M T SORT   -> does T's least sort fit under SORT?
+
+(define
+  mau/arg-sorts-ok?
+  (fn
+    (m argsorts declared)
+    (cond
+      ((and (empty? argsorts) (empty? declared)) true)
+      ((or (empty? argsorts) (empty? declared)) false)
+      ((mau/sort<=? m (first argsorts) (first declared))
+        (mau/arg-sorts-ok? m (rest argsorts) (rest declared)))
+      (else false))))
+
+(define
+  mau/matching-ops
+  (fn
+    (m name argsorts)
+    (filter
+      (fn
+        (op)
+        (and
+          (= (len (get op :arity)) (len argsorts))
+          (mau/arg-sorts-ok? m argsorts (get op :arity))))
+      (mau/ops-named m name))))
+
+(define
+  mau/least-loop
+  (fn
+    (m best rst)
+    (cond
+      ((empty? rst) best)
+      ((mau/sort<=? m (first rst) best)
+        (mau/least-loop m (first rst) (rest rst)))
+      (else (mau/least-loop m best (rest rst))))))
+
+(define
+  mau/least-sort
+  (fn
+    (m sorts)
+    (if (empty? sorts) "?" (mau/least-loop m (first sorts) (rest sorts)))))
+
+(define
+  mau/result-sort
+  (fn
+    (m name argsorts)
+    (let
+      ((cands (mau/matching-ops m name argsorts)))
+      (if
+        (empty? cands)
+        (let
+          ((any (mau/ops-named m name)))
+          (if (empty? any) "?" (get (first any) :result)))
+        (mau/least-sort m (map (fn (op) (get op :result)) cands))))))
+
+(define
+  mau/term-sort
+  (fn
+    (m t)
+    (cond
+      ((mau/var? t) (mau/vsort t))
+      ((mau/app? t)
+        (mau/result-sort
+          m
+          (mau/op t)
+          (map (fn (a) (mau/term-sort m a)) (mau/args t))))
+      (else "?"))))
+
+(define
+  mau/term-sort-src
+  (fn (m src) (mau/term-sort m (mau/parse-term-in m src))))
+
+(define
+  mau/has-sort?
+  (fn (m t sort) (mau/sort<=? m (mau/term-sort m t) sort)))
+
+(define
+  mau/has-sort-src?
+  (fn (m src sort) (mau/has-sort? m (mau/parse-term-in m src) sort)))

lib/maude/strategy.sx

@@ -0,0 +1,217 @@
+;; lib/maude/strategy.sx — strategy language (Phase 6).
+;;
+;; A strategy controls HOW rules are applied. Strategies are first-class values
+;; (tagged dicts) and SET-VALUED: applying a strategy to a term yields the set
+;; (deduped by canonical form) of result terms. The same rule set under
+;; different strategies computes different things — `;` sequences, `|` unions,
+;; `*`/`+` iterate, `!` normalises.
+;;
+;; Constructors:
+;;   (mau/s-idle)            identity (the term itself)
+;;   (mau/s-fail)            empty set
+;;   (mau/s-all)             apply any rule once, anywhere
+;;   (mau/s-rule LABEL)      apply a named rule once, anywhere
+;;   (mau/s-seq A B)         A ; B   (apply B to every result of A)
+;;   (mau/s-alt A B)         A | B   (union of results)
+;;   (mau/s-star A)          A *     (reflexive-transitive closure)
+;;   (mau/s-plus A)          A +     (one or more)
+;;   (mau/s-bang A)          A !     (normal forms: results where A can't apply)
+;;   (mau/s-name N)          look up named strategy N in the env
+;;
+;; Run with (mau/srun M STRATS STRAT SRC): STRATS is a dict NAME -> strategy.
+
+(define mau/s-idle (fn () {:s :idle}))
+(define mau/s-fail (fn () {:s :fail}))
+(define mau/s-all (fn () {:s :all}))
+(define mau/s-rule (fn (label) {:label label :s :rule}))
+(define mau/s-seq (fn (a b) {:a a :b b :s :seq}))
+(define mau/s-alt (fn (a b) {:a a :b b :s :alt}))
+(define mau/s-star (fn (a) {:a a :s :star}))
+(define mau/s-plus (fn (a) {:a a :s :plus}))
+(define mau/s-bang (fn (a) {:a a :s :bang}))
+(define mau/s-name (fn (n) {:n n :s :name}))
+
+(define
+  mau/rules-with-label
+  (fn (rules label) (filter (fn (r) (= (get r :label) label)) rules)))
+
+(define
+  mau/dedup-loop
+  (fn
+    (theory ts seen acc)
+    (if
+      (empty? ts)
+      acc
+      (let
+        ((c (mau/canon theory (first ts))))
+        (if
+          (mau/member? c seen)
+          (mau/dedup-loop theory (rest ts) seen acc)
+          (mau/dedup-loop
+            theory
+            (rest ts)
+            (cons c seen)
+            (mau/append2 acc (list (first ts)))))))))
+
+(define
+  mau/dedup-canon
+  (fn (theory ts) (mau/dedup-loop theory ts (list) (list))))
+
+;; ---- strategy interpreter ----
+
+(define
+  mau/sapply
+  (fn
+    (ctx strat term)
+    (let
+      ((k (get strat :s)) (theory (get ctx :theory)))
+      (cond
+        ((= k "idle") (list term))
+        ((= k "fail") (list))
+        ((= k "all")
+          (mau/dedup-canon
+            theory
+            (mau/all-successors theory (get ctx :eqs) (get ctx :rules) term)))
+        ((= k "rule")
+          (mau/dedup-canon
+            theory
+            (mau/all-successors
+              theory
+              (get ctx :eqs)
+              (mau/rules-with-label (get ctx :rules) (get strat :label))
+              term)))
+        ((= k "seq")
+          (mau/dedup-canon
+            theory
+            (mau/concat-map
+              (fn (t) (mau/sapply ctx (get strat :b) t))
+              (mau/sapply ctx (get strat :a) term))))
+        ((= k "alt")
+          (mau/dedup-canon
+            theory
+            (mau/append2
+              (mau/sapply ctx (get strat :a) term)
+              (mau/sapply ctx (get strat :b) term))))
+        ((= k "star") (mau/sstar ctx (get strat :a) term))
+        ((= k "plus")
+          (mau/dedup-canon
+            theory
+            (mau/concat-map
+              (fn (t) (mau/sstar ctx (get strat :a) t))
+              (mau/sapply ctx (get strat :a) term))))
+        ((= k "bang")
+          (mau/dedup-canon theory (mau/sbang ctx (get strat :a) term)))
+        ((= k "name")
+          (mau/sapply ctx (get (get ctx :strats) (get strat :n)) term))
+        (else (list))))))
+
+;; reflexive-transitive closure: term plus everything reachable via A
+(define
+  mau/sstar
+  (fn
+    (ctx a term)
+    (mau/sstar-loop
+      ctx
+      a
+      (list term)
+      (list (mau/canon (get ctx :theory) term))
+      (list term))))
+
+(define
+  mau/sstar-loop
+  (fn
+    (ctx a frontier seen acc)
+    (if
+      (empty? frontier)
+      acc
+      (let
+        ((newf (list))
+          (newseen seen)
+          (newacc acc)
+          (theory (get ctx :theory)))
+        (for-each
+          (fn
+            (t)
+            (for-each
+              (fn
+                (succ)
+                (let
+                  ((c (mau/canon theory succ)))
+                  (when
+                    (not (mau/member? c newseen))
+                    (do
+                      (set! newseen (cons c newseen))
+                      (append! newf succ)
+                      (append! newacc succ)))))
+              (mau/sapply ctx a t)))
+          frontier)
+        (mau/sstar-loop ctx a newf newseen newacc)))))
+
+;; normal forms: terms reachable via A where A yields nothing more
+(define
+  mau/sbang
+  (fn
+    (ctx a term)
+    (mau/sbang-loop
+      ctx
+      a
+      (list term)
+      (list (mau/canon (get ctx :theory) term))
+      (list))))
+
+(define
+  mau/sbang-loop
+  (fn
+    (ctx a frontier seen acc)
+    (if
+      (empty? frontier)
+      acc
+      (let
+        ((newf (list))
+          (newseen seen)
+          (newacc acc)
+          (theory (get ctx :theory)))
+        (for-each
+          (fn
+            (t)
+            (let
+              ((succs (mau/sapply ctx a t)))
+              (if
+                (empty? succs)
+                (append! newacc t)
+                (for-each
+                  (fn
+                    (succ)
+                    (let
+                      ((c (mau/canon theory succ)))
+                      (when
+                        (not (mau/member? c newseen))
+                        (do
+                          (set! newseen (cons c newseen))
+                          (append! newf succ)))))
+                  succs))))
+          frontier)
+        (mau/sbang-loop ctx a newf newseen newacc)))))
+
+;; ---- public API ----
+
+(define mau/make-sctx (fn (m strats) {:eqs (mau/module-eqs m) :theory (mau/build-theory m) :strats strats :rules (mau/module-rules m)}))
+
+(define
+  mau/srun
+  (fn
+    (m strats strat src)
+    (let
+      ((ctx (mau/make-sctx m strats)))
+      (let
+        ((t0 (mau/cnormalize (get ctx :theory) (get ctx :eqs) (mau/parse-term-in m src) mau/reduce-fuel)))
+        (mau/dedup-canon (get ctx :theory) (mau/sapply ctx strat t0))))))
+
+(define
+  mau/srun-canon
+  (fn
+    (m strats strat src)
+    (let
+      ((theory (mau/build-theory m)))
+      (mau/sort-strings
+        (map (fn (t) (mau/canon theory t)) (mau/srun m strats strat src))))))

lib/maude/term.sx

@@ -0,0 +1,114 @@
+;; lib/maude/term.sx — Maude term representation.
+;;
+;; A term is one of:
+;;   variable     {:t :var :name "X" :sort "Nat"}
+;;   application  {:t :app :op "_+_" :args (a b ...)}   (constant: empty args)
+;;
+;; Sorts attach to variables; operator/result sorts live on op declarations
+;; in the module signature, not on the term node. Overloading is resolved at
+;; reduction time, so the parser only records the operator name.
+
+(define mau/var (fn (name sort) {:name name :t :var :sort sort}))
+
+(define mau/app (fn (op args) {:op op :t :app :args args}))
+
+(define mau/const (fn (op) {:op op :t :app :args (list)}))
+
+(define mau/var? (fn (t) (and (dict? t) (= (get t :t) "var"))))
+
+(define mau/app? (fn (t) (and (dict? t) (= (get t :t) "app"))))
+
+(define mau/term? (fn (t) (or (mau/var? t) (mau/app? t))))
+
+(define mau/op (fn (t) (get t :op)))
+(define mau/args (fn (t) (get t :args)))
+(define mau/vname (fn (t) (get t :name)))
+(define mau/vsort (fn (t) (get t :sort)))
+(define mau/arity (fn (t) (len (get t :args))))
+
+(define mau/const? (fn (t) (and (mau/app? t) (empty? (mau/args t)))))
+
+(define
+  mau/args=?
+  (fn
+    (as bs)
+    (cond
+      ((and (empty? as) (empty? bs)) true)
+      ((or (empty? as) (empty? bs)) false)
+      (else
+        (and
+          (mau/term=? (first as) (first bs))
+          (mau/args=? (rest as) (rest bs)))))))
+
+(define
+  mau/term=?
+  (fn
+    (a b)
+    (cond
+      ((and (mau/var? a) (mau/var? b))
+        (and
+          (= (mau/vname a) (mau/vname b))
+          (= (mau/vsort a) (mau/vsort b))))
+      ((and (mau/app? a) (mau/app? b))
+        (and
+          (= (mau/op a) (mau/op b))
+          (mau/args=? (mau/args a) (mau/args b))))
+      (else false))))
+
+(define
+  mau/join-args
+  (fn
+    (args)
+    (cond
+      ((empty? args) "")
+      ((empty? (rest args)) (mau/term->str (first args)))
+      (else
+        (str (mau/term->str (first args)) ", " (mau/join-args (rest args)))))))
+
+(define
+  mau/term->str
+  (fn
+    (t)
+    (cond
+      ((mau/var? t) (mau/vname t))
+      ((mau/const? t) (mau/op t))
+      ((mau/app? t) (str (mau/op t) "(" (mau/join-args (mau/args t)) ")"))
+      (else "?"))))
+
+(define
+  mau/member?
+  (fn
+    (x xs)
+    (cond
+      ((empty? xs) false)
+      ((= x (first xs)) true)
+      (else (mau/member? x (rest xs))))))
+
+(define
+  mau/union
+  (fn
+    (xs ys)
+    (cond
+      ((empty? xs) ys)
+      ((mau/member? (first xs) ys) (mau/union (rest xs) ys))
+      (else (cons (first xs) (mau/union (rest xs) ys))))))
+
+(define
+  mau/term-vars
+  (fn
+    (t)
+    (cond
+      ((mau/var? t) (list (mau/vname t)))
+      ((mau/app? t) (mau/term-vars-list (mau/args t)))
+      (else (list)))))
+
+(define
+  mau/term-vars-list
+  (fn
+    (args)
+    (if
+      (empty? args)
+      (list)
+      (mau/union
+        (mau/term-vars (first args))
+        (mau/term-vars-list (rest args))))))

lib/maude/tests/conditional.sx

@@ -0,0 +1,108 @@
+;; lib/maude/tests/conditional.sx — Phase 4: conditional equations.
+
+(define mct-pass 0)
+(define mct-fail 0)
+(define mct-failures (list))
+
+(define
+  mct-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! mct-pass (+ mct-pass 1))
+      (do
+        (set! mct-fail (+ mct-fail 1))
+        (append!
+          mct-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+;; ---- gcd (equational guard, recursive) ----
+
+(define
+  mct-gcd
+  (mau/parse-module
+    "fmod GCD is\n  sorts Nat Bool .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op true : -> Bool .\n  op false : -> Bool .\n  op _>_ : Nat Nat -> Bool .\n  op _-_ : Nat Nat -> Nat .\n  op gcd : Nat Nat -> Nat .\n  vars X Y : Nat .\n  eq 0 > Y = false .\n  eq s X > 0 = true .\n  eq s X > s Y = X > Y .\n  eq X - 0 = X .\n  eq 0 - Y = 0 .\n  eq s X - s Y = X - Y .\n  eq gcd(X, 0) = X .\n  eq gcd(0, Y) = Y .\n  eq gcd(X, X) = X .\n  ceq gcd(X, Y) = gcd(X - Y, Y) if X > Y = true .\n  ceq gcd(X, Y) = gcd(Y, X) if Y > X = true .\nendfm"))
+
+(mct-check!
+  "gcd-6-4"
+  (mau/creduce->str mct-gcd "gcd(s s s s s s 0, s s s s 0)")
+  "s_(s_(0))")
+(mct-check!
+  "gcd-3-6"
+  (mau/creduce->str mct-gcd "gcd(s s s 0, s s s s s s 0)")
+  "s_(s_(s_(0)))")
+(mct-check!
+  "gcd-base-zero"
+  (mau/creduce->str mct-gcd "gcd(s s 0, 0)")
+  "s_(s_(0))")
+(mct-check!
+  "gcd-equal"
+  (mau/creduce->str mct-gcd "gcd(s s 0, s s 0)")
+  "s_(s_(0))")
+(mct-check!
+  "gcd-coprime"
+  (mau/creduce->str mct-gcd "gcd(s s s 0, s s 0)")
+  "s_(0)")
+;; guard predicate reductions
+(mct-check! "gt-true" (mau/creduce->str mct-gcd "s s 0 > s 0") "true")
+(mct-check! "gt-false" (mau/creduce->str mct-gcd "s 0 > s s 0") "false")
+
+;; ---- insertion sort (true/false guards) ----
+
+(define
+  mct-sort
+  (mau/parse-module
+    "fmod SORT is\n  sorts Nat List Bool .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op true : -> Bool .\n  op false : -> Bool .\n  op _<=_ : Nat Nat -> Bool .\n  op nil : -> List .\n  op _:_ : Nat List -> List .\n  op insert : Nat List -> List .\n  op sort : List -> List .\n  vars M N : Nat .\n  var L : List .\n  eq 0 <= N = true .\n  eq s M <= 0 = false .\n  eq s M <= s N = M <= N .\n  eq insert(N, nil) = N : nil .\n  ceq insert(N, M : L) = N : (M : L) if N <= M = true .\n  ceq insert(N, M : L) = M : insert(N, L) if N <= M = false .\n  eq sort(nil) = nil .\n  eq sort(N : L) = insert(N, sort(L)) .\nendfm"))
+
+(mct-check!
+  "sort-321"
+  (mau/creduce->str mct-sort "sort(s s s 0 : (s 0 : (s s 0 : nil)))")
+  "_:_(s_(0), _:_(s_(s_(0)), _:_(s_(s_(s_(0))), nil)))")
+(mct-check! "sort-empty" (mau/creduce->str mct-sort "sort(nil)") "nil")
+(mct-check!
+  "sort-singleton"
+  (mau/creduce->str mct-sort "sort(s s 0 : nil)")
+  "_:_(s_(s_(0)), nil)")
+(mct-check!
+  "insert-front"
+  (mau/creduce->str mct-sort "insert(0, s 0 : (s s 0 : nil))")
+  "_:_(0, _:_(s_(0), _:_(s_(s_(0)), nil)))")
+(mct-check!
+  "insert-back"
+  (mau/creduce->str mct-sort "insert(s s s 0, s 0 : (s s 0 : nil))")
+  "_:_(s_(0), _:_(s_(s_(0)), _:_(s_(s_(s_(0))), nil)))")
+
+;; ---- max (conditional simplification, both branches) ----
+
+(define
+  mct-max
+  (mau/parse-module
+    "fmod MAX is\n  sorts Nat Bool .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op true : -> Bool .\n  op false : -> Bool .\n  op _<=_ : Nat Nat -> Bool .\n  op max : Nat Nat -> Nat .\n  vars M N : Nat .\n  eq 0 <= N = true .\n  eq s M <= 0 = false .\n  eq s M <= s N = M <= N .\n  ceq max(M, N) = M if N <= M = true .\n  ceq max(M, N) = N if N <= M = false .\nendfm"))
+
+(mct-check!
+  "max-left"
+  (mau/creduce->str mct-max "max(s s s 0, s 0)")
+  "s_(s_(s_(0)))")
+(mct-check!
+  "max-right"
+  (mau/creduce->str mct-max "max(s 0, s s 0)")
+  "s_(s_(0))")
+(mct-check!
+  "max-equal"
+  (mau/creduce->str mct-max "max(s s 0, s s 0)")
+  "s_(s_(0))")
+
+;; ---- boolean-kind condition (`if pred`) ----
+
+(define
+  mct-even
+  (mau/parse-module
+    "fmod EVEN is\n  sorts Nat Bool Tag .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op true : -> Bool .\n  op false : -> Bool .\n  op even : Nat -> Bool .\n  op evn : -> Tag .\n  op odd : -> Tag .\n  op tag : Nat -> Tag .\n  var N : Nat .\n  eq even(0) = true .\n  eq even(s 0) = false .\n  eq even(s s N) = even(N) .\n  ceq tag(N) = evn if even(N) .\n  ceq tag(N) = odd if even(N) = false .\nendfm"))
+
+(mct-check! "even-4" (mau/creduce->str mct-even "even(s s s s 0)") "true")
+(mct-check! "even-3" (mau/creduce->str mct-even "even(s s s 0)") "false")
+(mct-check! "tag-even-bool" (mau/creduce->str mct-even "tag(s s 0)") "evn")
+(mct-check! "tag-odd" (mau/creduce->str mct-even "tag(s s s 0)") "odd")
+
+(define mau-conditional-tests-run! (fn () {:failures mct-failures :total (+ mct-pass mct-fail) :passed mct-pass :failed mct-fail}))

lib/maude/tests/confluence.sx

@@ -0,0 +1,101 @@
+;; lib/maude/tests/confluence.sx — critical-pair / local-confluence checking.
+
+(define mcf-pass 0)
+(define mcf-fail 0)
+(define mcf-failures (list))
+
+(define
+  mcf-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! mcf-pass (+ mcf-pass 1))
+      (do
+        (set! mcf-fail (+ mcf-fail 1))
+        (append!
+          mcf-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+;; peano addition: no LHS overlaps -> confluent
+(define
+  mcf-peano
+  (mau/parse-module
+    "fmod P is\n  sort Nat .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op _+_ : Nat Nat -> Nat .\n  vars X Y : Nat .\n  eq 0 + Y = Y .\n  eq s X + Y = s (X + Y) .\nendfm"))
+
+(mcf-check! "peano-confluent" (mau/confluent? mcf-peano) true)
+(mcf-check!
+  "peano-no-bad-pairs"
+  (len (mau/non-joinable-pairs mcf-peano))
+  0)
+
+;; f(a)=b, a=c : the inner `a` overlaps -> critical pair b vs f(c), NOT joinable
+(define
+  mcf-bad
+  (mau/parse-module
+    "fmod B is\n  sort T .\n  op a : -> T .\n  op b : -> T .\n  op c : -> T .\n  op f : T -> T .\n  eq f(a) = b .\n  eq a = c .\nendfm"))
+
+(mcf-check! "bad-not-confluent" (mau/confluent? mcf-bad) false)
+(mcf-check! "bad-one-pair" (len (mau/non-joinable-pairs mcf-bad)) 1)
+(mcf-check!
+  "bad-pair-shape"
+  (mau/cp->str mcf-bad (first (mau/non-joinable-pairs mcf-bad)))
+  "b <?> f(c)")
+(mcf-check!
+  "bad-has-cps"
+  (> (len (mau/critical-pairs mcf-bad)) 0)
+  true)
+
+;; adding f(c)=b joins the pair -> confluent
+(define
+  mcf-fixed
+  (mau/parse-module
+    "fmod F is\n  sort T .\n  op a : -> T .\n  op b : -> T .\n  op c : -> T .\n  op f : T -> T .\n  eq f(a) = b .\n  eq a = c .\n  eq f(c) = b .\nendfm"))
+
+(mcf-check! "fixed-confluent" (mau/confluent? mcf-fixed) true)
+
+;; self-overlap that is joinable: idempotent d(d(X)) = d(X)
+(define
+  mcf-idem
+  (mau/parse-module
+    "fmod I is\n  sort T .\n  op d : T -> T .\n  op x : -> T .\n  var X : T .\n  eq d(d(X)) = d(X) .\nendfm"))
+
+(mcf-check! "idem-confluent" (mau/confluent? mcf-idem) true)
+
+;; a free-op overlap that joins: g(h(X)) over h(a)
+(define
+  mcf-join
+  (mau/parse-module
+    "fmod J is\n  sort T .\n  op a : -> T .\n  op k : -> T .\n  op h : T -> T .\n  op g : T -> T .\n  op r : T -> T .\n  var X : T .\n  eq g(h(X)) = r(X) .\n  eq h(a) = k .\nendfm"))
+
+;; g(h(a)) -> r(a) (rule1) or g(k) (rule2 inside). Not joinable unless g(k) reduces.
+(mcf-check! "join-not-confluent" (mau/confluent? mcf-join) false)
+
+;; AC operator, genuinely confluent; joinability uses canonical form
+(define
+  mcf-ac
+  (mau/parse-module
+    "fmod AC is\n  sort S .\n  op a : -> S .\n  op b : -> S .\n  op _+_ : S S -> S [assoc comm] .\n  eq a + a = b .\nendfm"))
+
+(mcf-check! "ac-confluent" (mau/confluent? mcf-ac) true)
+
+;; unifier sanity (two-sided): f(X, b) unifies with f(a, Y)
+(mcf-check!
+  "unify-twosided"
+  (=
+    nil
+    (mau/u-unify
+      (mau/app "f" (list (mau/var "X" "T") (mau/const "b")))
+      (mau/app "f" (list (mau/const "a") (mau/var "Y" "T")))
+      {}))
+  false)
+;; occurs check: X vs f(X) fails
+(mcf-check!
+  "unify-occurs"
+  (mau/u-unify
+    (mau/var "X" "T")
+    (mau/app "f" (list (mau/var "X" "T")))
+    {})
+  nil)
+
+(define mau-confluence-tests-run! (fn () {:failures mcf-failures :total (+ mcf-pass mcf-fail) :passed mcf-pass :failed mcf-fail}))

lib/maude/tests/effects.sx

@@ -0,0 +1,79 @@
+;; lib/maude/tests/effects.sx — artdag-on-sx fit prototype.
+;;
+;; Demonstrates that artdag's effect-pipeline optimisation passes (adjacent-op
+;; fusion, no-op / dead-op elimination, identity elimination, CSE/idempotent
+;; dedup) are exactly equational rewriting: declare them as `eq`s and the
+;; OPTIMISED pipeline is the normal form. Because the equation set is confluent
+;; (and terminating), the normal form is unique regardless of rewrite order —
+;; which is precisely what makes the optimised pipeline's content id stable.
+;;
+;; This is the "second consumer" spike justifying a maude-driven optimiser in
+;; lib/artdag and the eventual lib/guest/rewriting/ extraction.
+
+(define mef-pass 0)
+(define mef-fail 0)
+(define mef-failures (list))
+
+(define
+  mef-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! mef-pass (+ mef-pass 1))
+      (do
+        (set! mef-fail (+ mef-fail 1))
+        (append!
+          mef-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+(define
+  mef-m
+  (mau/parse-module
+    "fmod EFFECTS is\n  sorts Img Num .\n  op src : -> Img .\n  op 0 : -> Num .\n  op s_ : Num -> Num .\n  op _+_ : Num Num -> Num .\n  op blur : Img Num -> Img .\n  op bright : Img Num -> Img .\n  op id : Img -> Img .\n  op over : Img Img -> Img [comm] .\n  vars I J : Img .\n  vars M N : Num .\n  eq 0 + N = N .\n  eq s M + N = s (M + N) .\n  eq id(I) = I .\n  eq blur(I, 0) = I .\n  eq bright(I, 0) = I .\n  eq blur(blur(I, M), N) = blur(I, M + N) .\n  eq bright(bright(I, M), N) = bright(I, M + N) .\n  eq over(I, I) = I .\nendfm"))
+
+;; adjacent-op fusion: two blurs collapse, radii add
+(mef-check!
+  "fuse-blur"
+  (mau/creduce->str mef-m "blur(blur(src, s 0), s s 0)")
+  "blur(src, s_(s_(s_(0))))")
+;; chain fusion
+(mef-check!
+  "fuse-chain"
+  (mau/creduce->str mef-m "blur(blur(blur(src, s 0), s 0), s 0)")
+  "blur(src, s_(s_(s_(0))))")
+;; no-op / dead-op elimination
+(mef-check! "noop-blur" (mau/creduce->str mef-m "blur(src, 0)") "src")
+;; identity elimination + no-op together
+(mef-check!
+  "id-elim"
+  (mau/creduce->str mef-m "bright(id(blur(src, s 0)), 0)")
+  "blur(src, s_(0))")
+;; CSE / idempotent dedup (same subpipeline composited with itself)
+(mef-check!
+  "cse-dedup"
+  (mau/creduce->str mef-m "over(blur(src, s 0), blur(src, s 0))")
+  "blur(src, s_(0))")
+;; commutative compositing: over is comm, so swapped duplicates also dedup
+(mef-check!
+  "cse-dedup-comm"
+  (mau/creduce->str mef-m "over(blur(src, s 0), blur(src, s 0))")
+  "blur(src, s_(0))")
+
+;; confluence in practice: two different surface pipelines that optimise to the
+;; SAME normal form (=> same content id). bright-fused twice vs once-by-3.
+(mef-check!
+  "same-normal-form"
+  (=
+    (mau/ccanon mef-m "bright(bright(src, s 0), s s 0)")
+    (mau/ccanon mef-m "bright(src, s s s 0)"))
+  true)
+;; distinct pipelines stay distinct
+(mef-check!
+  "distinct-stay-distinct"
+  (=
+    (mau/ccanon mef-m "blur(src, s 0)")
+    (mau/ccanon mef-m "bright(src, s 0)"))
+  false)
+
+(define mau-effects-tests-run! (fn () {:failures mef-failures :total (+ mef-pass mef-fail) :passed mef-pass :failed mef-fail}))

lib/maude/tests/gather.sx

@@ -0,0 +1,66 @@
+;; lib/maude/tests/gather.sx — gather / parse-time associativity.
+
+(define mga-pass 0)
+(define mga-fail 0)
+(define mga-failures (list))
+
+(define
+  mga-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! mga-pass (+ mga-pass 1))
+      (do
+        (set! mga-fail (+ mga-fail 1))
+        (append!
+          mga-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+(define
+  mga-m
+  (mau/parse-module
+    "fmod L is\n  sorts Nat List .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op nil : -> List .\n  op _:_ : Nat List -> List [gather (e E)] .\n  op _+_ : Nat Nat -> Nat .\n  op _-_ : Nat Nat -> Nat [gather (E e)] .\n  vars X Y : Nat .\nendfm"))
+
+;; cons is right-associative: a : b : c  ==  a : (b : c)
+(mga-check!
+  "cons-right"
+  (mau/term->str (mau/parse-term-in mga-m "0 : s 0 : nil"))
+  "_:_(0, _:_(s_(0), nil))")
+;; + has no gather -> default left-assoc
+(mga-check!
+  "plus-left"
+  (mau/term->str (mau/parse-term-in mga-m "X + Y + X"))
+  "_+_(_+_(X, Y), X)")
+;; explicit (E e) is left
+(mga-check!
+  "minus-left"
+  (mau/term->str (mau/parse-term-in mga-m "X - Y - X"))
+  "_-_(_-_(X, Y), X)")
+;; gather attr recorded
+(mga-check!
+  "gather-recorded"
+  (get (get (first (mau/ops-named mga-m "_:_")) :attrs) :gather)
+  (list "e" "E"))
+
+;; ---- full insertion sort over BARE cons lists (no parens needed) ----
+
+(define
+  mga-sort
+  (mau/parse-module
+    "fmod SORT is\n  sorts Nat List Bool .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op true : -> Bool .\n  op false : -> Bool .\n  op _<=_ : Nat Nat -> Bool .\n  op nil : -> List .\n  op _:_ : Nat List -> List [gather (e E)] .\n  op insert : Nat List -> List .\n  op sort : List -> List .\n  vars M N : Nat .\n  var L : List .\n  eq 0 <= N = true .\n  eq s M <= 0 = false .\n  eq s M <= s N = M <= N .\n  eq insert(N, nil) = N : nil .\n  ceq insert(N, M : L) = N : M : L if N <= M = true .\n  ceq insert(N, M : L) = M : insert(N, L) if N <= M = false .\n  eq sort(nil) = nil .\n  eq sort(N : L) = insert(N, sort(L)) .\nendfm"))
+
+(mga-check!
+  "sort-bare"
+  (mau/creduce->str mga-sort "sort(s s s 0 : s 0 : s s 0 : nil)")
+  "_:_(s_(0), _:_(s_(s_(0)), _:_(s_(s_(s_(0))), nil)))")
+(mga-check!
+  "sort-bare-5"
+  (mau/creduce->str mga-sort "sort(s s 0 : 0 : s 0 : nil)")
+  "_:_(0, _:_(s_(0), _:_(s_(s_(0)), nil)))")
+(mga-check!
+  "insert-bare"
+  (mau/creduce->str mga-sort "insert(s 0, 0 : s s 0 : nil)")
+  "_:_(0, _:_(s_(0), _:_(s_(s_(0)), nil)))")
+
+(define mau-gather-tests-run! (fn () {:failures mga-failures :total (+ mga-pass mga-fail) :passed mga-pass :failed mga-fail}))

lib/maude/tests/matching.sx

@@ -0,0 +1,170 @@
+;; lib/maude/tests/matching.sx — Phase 3: matching modulo assoc/comm/id.
+
+(define mmt-pass 0)
+(define mmt-fail 0)
+(define mmt-failures (list))
+
+(define
+  mmt-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! mmt-pass (+ mmt-pass 1))
+      (do
+        (set! mmt-fail (+ mmt-fail 1))
+        (append!
+          mmt-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+;; ---- multi-valued matching enumeration ----
+
+(define
+  mmt-acg
+  (mau/parse-module
+    "fmod ACG is\n  sort S .\n  op a : -> S .\n  op b : -> S .\n  op c : -> S .\n  op _+_ : S S -> S [assoc comm] .\n  op _._ : S S -> S [assoc] .\n  vars X Y : S .\nendfm"))
+
+;; X + Y against a + b + c (AC, no id): 6 solutions (each non-empty 2-split).
+(mmt-check!
+  "ac-match-count"
+  (len
+    (mau/match-all
+      mmt-acg
+      (mau/parse-term-in mmt-acg "X + Y")
+      (mau/parse-term-in mmt-acg "a + b + c")))
+  6)
+;; X + a against a + b + c: X must be b + c (one solution, multiset).
+(mmt-check!
+  "ac-match-partial"
+  (len
+    (mau/match-all
+      mmt-acg
+      (mau/parse-term-in mmt-acg "X + a")
+      (mau/parse-term-in mmt-acg "a + b + c")))
+  1)
+;; assoc-only X . Y against a . b . c: ordered 2-splits -> 2 solutions.
+(mmt-check!
+  "assoc-match-count"
+  (len
+    (mau/match-all
+      mmt-acg
+      (mau/parse-term-in mmt-acg "X . Y")
+      (mau/parse-term-in mmt-acg "a . b . c")))
+  2)
+;; no match: a + a pattern against a + b
+(mmt-check!
+  "ac-no-match"
+  (len
+    (mau/match-all
+      mmt-acg
+      (mau/parse-term-in mmt-acg "a + a")
+      (mau/parse-term-in mmt-acg "a + b")))
+  0)
+
+;; ---- comm (non-assoc) matching ----
+
+(define
+  mmt-pair
+  (mau/parse-module
+    "fmod PAIR is\n  sort S .\n  op a : -> S .\n  op b : -> S .\n  op p : S S -> S [comm] .\n  op fst : S -> S .\n  vars X Y : S .\n  eq fst(p(X, a)) = X .\nendfm"))
+
+(mmt-check!
+  "comm-both-orders"
+  (mau/ac-reduce->str mmt-pair "fst(p(b, a))")
+  "b")
+(mmt-check! "comm-swapped" (mau/ac-reduce->str mmt-pair "fst(p(a, b))") "b")
+
+;; ---- identity ----
+
+(define
+  mmt-id
+  (mau/parse-module
+    "fmod IDMOD is\n  sort S .\n  op a : -> S .\n  op b : -> S .\n  op e : -> S .\n  op _*_ : S S -> S [assoc comm id: e] .\n  vars X Y : S .\nendfm"))
+
+(mmt-check! "id-drop" (mau/ac-canon mmt-id "a * e") "a")
+(mmt-check! "id-drop-mid" (mau/ac-canon mmt-id "a * e * b") "_*_(a,b)")
+(mmt-check! "id-only" (mau/ac-canon mmt-id "e * e") "e")
+;; with id, X * Y matching a (singleton) succeeds (one var empty)
+(mmt-check!
+  "id-match-singleton"
+  (>
+    (len
+      (mau/match-all
+        mmt-id
+        (mau/parse-term-in mmt-id "X * Y")
+        (mau/parse-term-in mmt-id "a")))
+    0)
+  true)
+
+;; ---- multiset / bag rewriting ----
+
+(define
+  mmt-bag
+  (mau/parse-module
+    "fmod BAG is\n  sort S .\n  op a : -> S .\n  op b : -> S .\n  op c : -> S .\n  op _+_ : S S -> S [assoc comm] .\n  eq a + a = a .\nendfm"))
+
+(mmt-check! "bag-collapse" (mau/ac-canon mmt-bag "a + b + a") "_+_(a,b)")
+(mmt-check! "bag-deep" (mau/ac-canon mmt-bag "a + a + a") "a")
+(mmt-check! "bag-reorder" (mau/ac-canon mmt-bag "c + a + b + a") "_+_(a,b,c)")
+(mmt-check!
+  "bag-flatten-assoc"
+  (mau/ac-canon mmt-bag "(a + b) + (a + c)")
+  "_+_(a,b,c)")
+
+;; ---- set theory: idempotent union with empty (identity) ----
+
+(define
+  mmt-set
+  (mau/parse-module
+    "fmod SET is\n  sort Set .\n  op empty : -> Set .\n  op a : -> Set .\n  op b : -> Set .\n  op c : -> Set .\n  op _U_ : Set Set -> Set [assoc comm id: empty] .\n  var X : Set .\n  eq X U X = X .\nendfm"))
+
+(mmt-check! "set-dedup" (mau/ac-canon mmt-set "a U b U a") "_U_(a,b)")
+(mmt-check! "set-triple" (mau/ac-canon mmt-set "a U a U a") "a")
+(mmt-check!
+  "set-union"
+  (mau/ac-canon mmt-set "a U b U c U a U b")
+  "_U_(a,b,c)")
+(mmt-check! "set-empty" (mau/ac-canon mmt-set "a U empty") "a")
+(mmt-check! "set-empty-only" (mau/ac-canon mmt-set "empty U empty") "empty")
+
+;; ---- group equations (assoc, non-comm, identity + inverse) ----
+
+(define
+  mmt-group
+  (mau/parse-module
+    "fmod GROUP is\n  sort G .\n  op e : -> G .\n  op a : -> G .\n  op b : -> G .\n  op _*_ : G G -> G [assoc] .\n  op i : G -> G .\n  var X : G .\n  eq e * X = X .\n  eq X * e = X .\n  eq i(X) * X = e .\n  eq X * i(X) = e .\n  eq i(e) = e .\n  eq i(i(X)) = X .\nendfm"))
+
+(mmt-check! "group-inverse" (mau/ac-canon mmt-group "i(a) * a") "e")
+(mmt-check! "group-cancel" (mau/ac-canon mmt-group "i(a) * a * b") "b")
+(mmt-check! "group-cancel-mid" (mau/ac-canon mmt-group "b * i(a) * a") "b")
+(mmt-check! "group-double-inv" (mau/ac-canon mmt-group "i(i(a))") "a")
+(mmt-check! "group-id-left" (mau/ac-canon mmt-group "e * a") "a")
+(mmt-check! "group-right-inv" (mau/ac-canon mmt-group "a * i(a) * b") "b")
+
+;; ---- AC equality (canonical form) ----
+
+(define mmt-th (mau/build-theory mmt-acg))
+
+(mmt-check!
+  "ac-equal-reorder"
+  (mau/ac-equal?
+    mmt-th
+    (mau/parse-term-in mmt-acg "a + b + c")
+    (mau/parse-term-in mmt-acg "c + a + b"))
+  true)
+(mmt-check!
+  "ac-equal-renest"
+  (mau/ac-equal?
+    mmt-th
+    (mau/parse-term-in mmt-acg "(a + b) + c")
+    (mau/parse-term-in mmt-acg "a + (b + c)"))
+  true)
+(mmt-check!
+  "ac-noncomm-order"
+  (mau/ac-equal?
+    mmt-th
+    (mau/parse-term-in mmt-acg "a . b")
+    (mau/parse-term-in mmt-acg "b . a"))
+  false)
+
+(define mau-matching-tests-run! (fn () {:failures mmt-failures :total (+ mmt-pass mmt-fail) :passed mmt-pass :failed mmt-fail}))

lib/maude/tests/meta.sx

@@ -0,0 +1,144 @@
+;; lib/maude/tests/meta.sx — Phase 7: reflection (META-LEVEL).
+
+(define mmtt-pass 0)
+(define mmtt-fail 0)
+(define mmtt-failures (list))
+
+(define
+  mmtt-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! mmtt-pass (+ mmtt-pass 1))
+      (do
+        (set! mmtt-fail (+ mmtt-fail 1))
+        (append!
+          mmtt-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+(define
+  mmtt-peano
+  (mau/parse-module
+    "fmod PEANO is\n  sort Nat .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op _+_ : Nat Nat -> Nat [assoc comm] .\n  vars X Y : Nat .\n  eq 0 + Y = Y .\n  eq s X + Y = s (X + Y) .\nendfm"))
+
+(define
+  mmtt-ndet
+  (mau/parse-module
+    "mod NDET is\n  sort S .\n  ops a b c : -> S .\n  rl [r1] : a => b .\n  rl [r2] : b => c .\nendm"))
+
+;; ---- terms-as-data: up / down ----
+
+(mmtt-check!
+  "up-const"
+  (mau/term->str (mau/meta-up mmtt-peano "0"))
+  "mt-app(0)")
+(mmtt-check!
+  "up-s0"
+  (mau/term->str (mau/meta-up mmtt-peano "s 0"))
+  "mt-app(s_, mt-app(0))")
+(mmtt-check!
+  "up-var"
+  (mau/term->str (mau/up-term (mau/var "X" "Nat")))
+  "mt-var(X, Nat)")
+(mmtt-check!
+  "up-plus"
+  (mau/term->str (mau/meta-up mmtt-peano "s 0 + 0"))
+  "mt-app(_+_, mt-app(s_, mt-app(0)), mt-app(0))")
+
+;; round trip: down(up(t)) = t
+(mmtt-check!
+  "roundtrip-const"
+  (mau/term=?
+    (mau/down-term (mau/meta-up mmtt-peano "0"))
+    (mau/parse-term-in mmtt-peano "0"))
+  true)
+(mmtt-check!
+  "roundtrip-nested"
+  (mau/term=?
+    (mau/down-term (mau/meta-up mmtt-peano "s (s 0 + 0)"))
+    (mau/parse-term-in mmtt-peano "s (s 0 + 0)"))
+  true)
+(mmtt-check!
+  "roundtrip-var"
+  (mau/term=?
+    (mau/down-term (mau/up-term (mau/var "X" "Nat")))
+    (mau/var "X" "Nat"))
+  true)
+
+;; ---- reflective metaReduce ----
+
+(mmtt-check!
+  "meta-reduce"
+  (mau/term->str (mau/meta-reduce-src mmtt-peano "s 0 + s s 0"))
+  "s_(s_(s_(0)))")
+;; metaReduce returns a REPRESENTED result (a meta-term)
+(mmtt-check!
+  "meta-reduce-is-meta"
+  (=
+    (mau/op (mau/meta-reduce mmtt-peano (mau/meta-up mmtt-peano "s 0 + 0")))
+    "mt-app")
+  true)
+
+;; ---- meta-circular law: down(metaReduce(up t)) =AC= reduce t ----
+
+(mmtt-check!
+  "meta-circular-1"
+  (mau/meta-circular? mmtt-peano "s 0 + s s 0")
+  true)
+(mmtt-check!
+  "meta-circular-2"
+  (mau/meta-circular? mmtt-peano "s (s 0 + s 0)")
+  true)
+(mmtt-check!
+  "meta-reduce-eq-up"
+  (mau/term=?
+    (mau/meta-reduce mmtt-peano (mau/meta-up mmtt-peano "s 0 + s 0"))
+    (mau/up-term (mau/creduce-term mmtt-peano "s 0 + s 0")))
+  true)
+
+;; ---- metaApply: reflect a single rule step ----
+
+(mmtt-check!
+  "meta-apply-r1"
+  (mau/term=?
+    (mau/down-term
+      (mau/meta-apply mmtt-ndet "r1" (mau/meta-up mmtt-ndet "a")))
+    (mau/parse-term-in mmtt-ndet "b"))
+  true)
+(mmtt-check!
+  "meta-apply-fail"
+  (mau/meta-apply mmtt-ndet "r2" (mau/meta-up mmtt-ndet "a"))
+  nil)
+
+;; ---- generic theorem helper: equational proof by reduction ----
+
+;; commutativity instance: 1 + 2 and 2 + 1 reduce to the same normal form.
+(mmtt-check!
+  "prove-comm-instance"
+  (mau/meta-prove-equal? mmtt-peano "s 0 + s s 0" "s s 0 + s 0")
+  true)
+;; associativity instance
+(mmtt-check!
+  "prove-assoc-instance"
+  (mau/meta-prove-equal? mmtt-peano "(s 0 + s 0) + s 0" "s 0 + (s 0 + s 0)")
+  true)
+;; a non-theorem
+(mmtt-check!
+  "prove-false"
+  (mau/meta-prove-equal? mmtt-peano "s 0 + s 0" "s 0")
+  false)
+
+;; ---- build a program meta-level, then run it ----
+
+;; construct the meta-representation of s(s(0)) by hand, down it, reduce.
+(define
+  mmtt-built
+  (mau/up-term
+    (mau/app "s_" (list (mau/app "s_" (list (mau/const "0")))))))
+(mmtt-check!
+  "built-down-reduce"
+  (mau/term->str (mau/creduce mmtt-peano (mau/down-term mmtt-built)))
+  "s_(s_(0))")
+
+(define mau-meta-tests-run! (fn () {:failures mmtt-failures :total (+ mmtt-pass mmtt-fail) :passed mmtt-pass :failed mmtt-fail}))

lib/maude/tests/owise.sx

@@ -0,0 +1,61 @@
+;; lib/maude/tests/owise.sx — owise (otherwise) equations.
+
+(define mow-pass 0)
+(define mow-fail 0)
+(define mow-failures (list))
+
+(define
+  mow-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! mow-pass (+ mow-pass 1))
+      (do
+        (set! mow-fail (+ mow-fail 1))
+        (append!
+          mow-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+;; The owise catch-all is declared FIRST, yet must only fire when no ordinary
+;; equation applies — proving owise is order-independent, not just last-match.
+(define
+  mow-lookup
+  (mau/parse-module
+    "fmod LOOKUP is\n  sorts Key Val .\n  ops k1 k2 k3 : -> Key .\n  ops v1 v2 none : -> Val .\n  op lookup : Key -> Val .\n  var K : Key .\n  eq lookup(K) = none [owise] .\n  eq lookup(k1) = v1 .\n  eq lookup(k2) = v2 .\nendfm"))
+
+(mow-check!
+  "owise-parsed"
+  (get (first (mau/module-eqs mow-lookup)) :owise)
+  true)
+(mow-check!
+  "ordinary-not-owise"
+  (get (nth (mau/module-eqs mow-lookup) 1) :owise)
+  false)
+
+(mow-check! "lookup-hit-1" (mau/creduce->str mow-lookup "lookup(k1)") "v1")
+(mow-check! "lookup-hit-2" (mau/creduce->str mow-lookup "lookup(k2)") "v2")
+(mow-check!
+  "lookup-default"
+  (mau/creduce->str mow-lookup "lookup(k3)")
+  "none")
+
+;; owise with a guard among the ordinary equations
+(define
+  mow-sign
+  (mau/parse-module
+    "fmod SIGN is\n  sorts Nat Sign Bool .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op true : -> Bool .\n  op false : -> Bool .\n  op _>_ : Nat Nat -> Bool .\n  op pos : -> Sign .\n  op zero : -> Sign .\n  op sign : Nat -> Sign .\n  var N : Nat .\n  eq 0 > N = false .\n  eq s N > 0 = true .\n  eq s N > s M = N > M .\n  eq sign(N) = pos [owise] .\n  eq sign(0) = zero .\n  vars M : Nat .\nendfm"))
+
+(mow-check! "sign-zero" (mau/creduce->str mow-sign "sign(0)") "zero")
+(mow-check! "sign-pos" (mau/creduce->str mow-sign "sign(s s 0)") "pos")
+
+;; without owise, an overlapping catch-all declared first would shadow others
+(define
+  mow-noowise
+  (mau/parse-module
+    "fmod NOOW is\n  sorts Key Val .\n  ops k1 k2 : -> Key .\n  ops v1 def : -> Val .\n  op f : Key -> Val .\n  var K : Key .\n  eq f(K) = def .\n  eq f(k1) = v1 .\nendfm"))
+
+;; here f(k1) hits the first (catch-all) equation -> def (no owise tag)
+(mow-check! "noowise-shadows" (mau/creduce->str mow-noowise "f(k1)") "def")
+
+(define mau-owise-tests-run! (fn () {:failures mow-failures :total (+ mow-pass mow-fail) :passed mow-pass :failed mow-fail}))

lib/maude/tests/parse.sx

@@ -0,0 +1,250 @@
+;; lib/maude/tests/parse.sx — Phase 1: tokenizer, signatures, term/eq parsing.
+
+(define mpt-pass 0)
+(define mpt-fail 0)
+(define mpt-failures (list))
+
+(define
+  mpt-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! mpt-pass (+ mpt-pass 1))
+      (do
+        (set! mpt-fail (+ mpt-fail 1))
+        (append!
+          mpt-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+;; ---- modules under test ----
+
+(define
+  mpt-peano
+  (mau/parse-module
+    "fmod PEANO is\n  sort Nat .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op _+_ : Nat Nat -> Nat [assoc comm prec 33] .\n  op _*_ : Nat Nat -> Nat [assoc comm] .\n  vars X Y : Nat .\n  eq 0 + X = X .\n  eq s X + Y = s (X + Y) .\n  eq 0 * X = 0 .\nendfm"))
+
+(define
+  mpt-natlist
+  (mau/parse-module
+    "fmod NATLIST is\n  sorts Zero NzNat Nat List .\n  subsort Zero < Nat .\n  subsort NzNat < Nat .\n  subsort Nat < List .\n  op 0 : -> Zero .\n  op nil : -> List .\n  op _;_ : List List -> List [assoc id: nil] .\n  op head : List -> Nat .\n  op length : List -> Nat .\n  vars L M : List .\n  var N : Nat .\n  eq length(nil) = 0 .\n  eq head(N ; L) = N .\nendfm"))
+
+;; ---- tokenizer ----
+
+(define mpt-toks (mau/tokenize "op _+_ : Nat Nat -> Nat [assoc] ."))
+
+(mpt-check! "tok-count" (len mpt-toks) 11)
+(mpt-check! "tok-op" (nth mpt-toks 0) "op")
+(mpt-check! "tok-mixfix" (nth mpt-toks 1) "_+_")
+(mpt-check! "tok-colon" (nth mpt-toks 2) ":")
+(mpt-check! "tok-arrow" (nth mpt-toks 5) "->")
+(mpt-check! "tok-lbrack" (nth mpt-toks 7) "[")
+(mpt-check! "tok-dot" (nth mpt-toks 10) ".")
+(mpt-check!
+  "tok-comment"
+  (len (mau/tokenize "sort Nat . --- a comment\nop 0 : -> Nat ."))
+  9)
+
+;; ---- mixfix classification ----
+
+(mpt-check! "form-infix" (get (mau/op-form "_+_") :kind) "infix")
+(mpt-check! "form-infix-tok" (get (mau/op-form "_+_") :token) "+")
+(mpt-check! "form-prefix" (get (mau/op-form "s_") :kind) "prefix")
+(mpt-check! "form-prefix-tok" (get (mau/op-form "s_") :token) "s")
+(mpt-check! "form-postfix" (get (mau/op-form "_!") :kind) "postfix")
+(mpt-check! "form-const" (get (mau/op-form "nil") :kind) "const")
+(mpt-check!
+  "form-mixfix"
+  (get (mau/op-form "if_then_else_fi") :kind)
+  "mixfix")
+
+;; ---- module header / sorts ----
+
+(mpt-check! "mod-name" (mau/module-name mpt-peano) "PEANO")
+(mpt-check! "mod-kind" (mau/module-kind mpt-peano) "fmod")
+(mpt-check! "mod-sorts" (mau/module-sorts mpt-peano) (list "Nat"))
+(mpt-check!
+  "natlist-sorts-count"
+  (len (mau/module-sorts mpt-natlist))
+  4)
+
+;; ---- subsorts (direct + transitive) ----
+
+(mpt-check! "subsort-direct" (mau/subsort? mpt-natlist "NzNat" "Nat") true)
+(mpt-check! "subsort-trans" (mau/subsort? mpt-natlist "NzNat" "List") true)
+(mpt-check! "subsort-trans2" (mau/subsort? mpt-natlist "Zero" "List") true)
+(mpt-check! "subsort-none" (mau/subsort? mpt-natlist "List" "Nat") false)
+(mpt-check! "sort<=-refl" (mau/sort<=? mpt-natlist "Nat" "Nat") true)
+(mpt-check! "sort<=-trans" (mau/sort<=? mpt-natlist "Zero" "List") true)
+
+;; ---- operators / overloading ----
+
+(mpt-check! "ops-count" (len (mau/module-ops mpt-peano)) 4)
+(mpt-check!
+  "op-arity"
+  (get (first (mau/ops-named mpt-peano "_+_")) :arity)
+  (list "Nat" "Nat"))
+(mpt-check!
+  "op-result"
+  (get (first (mau/ops-named mpt-peano "s_")) :result)
+  "Nat")
+(mpt-check!
+  "op-const-arity"
+  (len (get (first (mau/ops-named mpt-peano "0")) :arity))
+  0)
+(mpt-check!
+  "natlist-ops-count"
+  (len (mau/module-ops mpt-natlist))
+  5)
+
+;; ---- attributes ----
+
+(mpt-check!
+  "attr-assoc"
+  (get (get (first (mau/ops-named mpt-peano "_+_")) :attrs) :assoc)
+  true)
+(mpt-check!
+  "attr-comm"
+  (get (get (first (mau/ops-named mpt-peano "_+_")) :attrs) :comm)
+  true)
+(mpt-check!
+  "attr-prec"
+  (get (get (first (mau/ops-named mpt-peano "_+_")) :attrs) :prec)
+  33)
+(mpt-check!
+  "attr-id"
+  (get (get (first (mau/ops-named mpt-natlist "_;_")) :attrs) :id)
+  "nil")
+(mpt-check!
+  "attr-absent"
+  (get (get (first (mau/ops-named mpt-peano "_*_")) :attrs) :prec)
+  nil)
+
+;; ---- variables ----
+
+(mpt-check! "var-sort" (get (mau/module-vars mpt-peano) "X") "Nat")
+(mpt-check! "var-list-sort" (get (mau/module-vars mpt-natlist) "L") "List")
+
+;; ---- term parsing ----
+
+(mpt-check!
+  "term-const"
+  (mau/term->str (mau/parse-term-in mpt-peano "0"))
+  "0")
+(mpt-check!
+  "term-prefix-mixfix"
+  (mau/term->str (mau/parse-term-in mpt-peano "s 0"))
+  "s_(0)")
+(mpt-check!
+  "term-nested-prefix"
+  (mau/term->str (mau/parse-term-in mpt-peano "s s 0"))
+  "s_(s_(0))")
+(mpt-check!
+  "term-infix"
+  (mau/term->str (mau/parse-term-in mpt-peano "X + Y"))
+  "_+_(X, Y)")
+(mpt-check!
+  "term-prec"
+  (mau/term->str (mau/parse-term-in mpt-peano "s X + Y"))
+  "_+_(s_(X), Y)")
+(mpt-check!
+  "term-paren"
+  (mau/term->str (mau/parse-term-in mpt-peano "s (X + Y)"))
+  "s_(_+_(X, Y))")
+(mpt-check!
+  "term-left-assoc"
+  (mau/term->str (mau/parse-term-in mpt-peano "X + Y + X"))
+  "_+_(_+_(X, Y), X)")
+(mpt-check!
+  "term-prefix-form"
+  (mau/term->str (mau/parse-term-in mpt-peano "_+_(X, 0)"))
+  "_+_(X, 0)")
+(mpt-check!
+  "term-funcall"
+  (mau/term->str (mau/parse-term-in mpt-natlist "length(nil)"))
+  "length(nil)")
+(mpt-check!
+  "term-onthefly-var"
+  (mau/var? (mau/parse-term-in mpt-peano "Z:Nat"))
+  true)
+(mpt-check!
+  "term-onthefly-sort"
+  (mau/vsort (mau/parse-term-in mpt-peano "Z:Nat"))
+  "Nat")
+(mpt-check!
+  "term-var-vs-const"
+  (mau/var? (mau/parse-term-in mpt-peano "X"))
+  true)
+(mpt-check!
+  "term-const-not-var"
+  (mau/var? (mau/parse-term-in mpt-peano "0"))
+  false)
+
+;; ---- equations ----
+
+(mpt-check! "eq-count" (len (mau/module-eqs mpt-peano)) 3)
+(mpt-check!
+  "eq-lhs"
+  (mau/term->str (get (nth (mau/module-eqs mpt-peano) 1) :lhs))
+  "_+_(s_(X), Y)")
+(mpt-check!
+  "eq-rhs"
+  (mau/term->str (get (nth (mau/module-eqs mpt-peano) 1) :rhs))
+  "s_(_+_(X, Y))")
+(mpt-check!
+  "eq-uncond"
+  (get (nth (mau/module-eqs mpt-peano) 0) :cond)
+  nil)
+(mpt-check!
+  "natlist-eq-head"
+  (mau/term->str (get (nth (mau/module-eqs mpt-natlist) 1) :lhs))
+  "head(_;_(N, L))")
+
+;; ---- conditional equations ----
+
+(define
+  mpt-gcd
+  (mau/parse-module
+    "fmod GCD is\n  sort Nat .\n  op _>_ : Nat Nat -> Bool .\n  op _-_ : Nat Nat -> Nat .\n  op gcd : Nat Nat -> Nat .\n  vars X Y : Nat .\n  ceq gcd(X, Y) = gcd(X - Y, Y) if X > Y = true .\nendfm"))
+
+(mpt-check! "ceq-count" (len (mau/module-eqs mpt-gcd)) 1)
+(mpt-check!
+  "ceq-has-cond"
+  (= (get (first (mau/module-eqs mpt-gcd)) :cond) nil)
+  false)
+(mpt-check!
+  "ceq-cond-kind"
+  (get (get (first (mau/module-eqs mpt-gcd)) :cond) :kind)
+  "eq")
+(mpt-check!
+  "ceq-cond-lhs"
+  (mau/term->str (get (get (first (mau/module-eqs mpt-gcd)) :cond) :lhs))
+  "_>_(X, Y)")
+
+;; ---- system module + rules ----
+
+(define
+  mpt-vending
+  (mau/parse-module
+    "mod VENDING is\n  sort State .\n  op _coin : State -> State .\n  op buy : State -> State .\n  var S : State .\n  rl [insert] : S coin => buy(S) .\n  crl [guard] : buy(S) => S if S = S .\nendfm"))
+
+(mpt-check! "mod-kind-mod" (mau/module-kind mpt-vending) "mod")
+(mpt-check! "rules-count" (len (mau/module-rules mpt-vending)) 2)
+(mpt-check!
+  "rule-label"
+  (get (first (mau/module-rules mpt-vending)) :label)
+  "insert")
+(mpt-check!
+  "rule-rhs"
+  (mau/term->str (get (first (mau/module-rules mpt-vending)) :rhs))
+  "buy(S)")
+(mpt-check!
+  "crl-label"
+  (get (nth (mau/module-rules mpt-vending) 1) :label)
+  "guard")
+(mpt-check!
+  "crl-cond-kind"
+  (get (get (nth (mau/module-rules mpt-vending) 1) :cond) :kind)
+  "eq")
+
+(define mau-parse-tests-run! (fn () {:failures mpt-failures :total (+ mpt-pass mpt-fail) :passed mpt-pass :failed mpt-fail}))

lib/maude/tests/pretty.sx

@@ -0,0 +1,50 @@
+;; lib/maude/tests/pretty.sx — mixfix surface-syntax printer.
+
+(define mpp-pass 0)
+(define mpp-fail 0)
+(define mpp-failures (list))
+
+(define
+  mpp-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! mpp-pass (+ mpp-pass 1))
+      (do
+        (set! mpp-fail (+ mpp-fail 1))
+        (append!
+          mpp-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+(define
+  mpp-m
+  (mau/parse-module
+    "fmod PEANO is\n  sort Nat .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op _+_ : Nat Nat -> Nat .\n  op _! : Nat -> Nat .\n  op f : Nat Nat -> Nat .\n  vars X Y : Nat .\n  eq 0 + Y = Y .\n  eq s X + Y = s (X + Y) .\nendfm"))
+
+(define
+  mpp-render
+  (fn (src) (mau/term->maude mpp-m (mau/parse-term-in mpp-m src))))
+
+(mpp-check! "const" (mpp-render "0") "0")
+(mpp-check! "var" (mau/term->maude mpp-m (mau/var "X" "Nat")) "X")
+(mpp-check! "prefix" (mpp-render "s 0") "(s 0)")
+(mpp-check! "infix" (mpp-render "X + Y") "(X + Y)")
+(mpp-check! "nested" (mpp-render "s X + Y") "((s X) + Y)")
+(mpp-check! "paren" (mpp-render "s (X + Y)") "(s (X + Y))")
+;; postfix: built directly (the parser does not produce postfix applications)
+(mpp-check!
+  "postfix"
+  (mau/term->maude mpp-m (mau/app "_!" (list (mau/var "X" "Nat"))))
+  "(X !)")
+(mpp-check! "funcall" (mpp-render "f(0, s 0)") "f(0, (s 0))")
+(mpp-check! "prefix-form-infix" (mpp-render "_+_(0, 0)") "(0 + 0)")
+
+;; reduce then render in surface syntax
+(mpp-check!
+  "red-surface"
+  (mau/red->maude mpp-m "s 0 + s s 0")
+  "(s (s (s 0)))")
+(mpp-check! "red-zero" (mau/red->maude mpp-m "0 + 0") "0")
+
+(define mau-pretty-tests-run! (fn () {:failures mpp-failures :total (+ mpp-pass mpp-fail) :passed mpp-pass :failed mpp-fail}))

lib/maude/tests/reduce.sx

@@ -0,0 +1,120 @@
+;; lib/maude/tests/reduce.sx — Phase 2: syntactic equational reduction.
+
+(define mrt-pass 0)
+(define mrt-fail 0)
+(define mrt-failures (list))
+
+(define
+  mrt-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! mrt-pass (+ mrt-pass 1))
+      (do
+        (set! mrt-fail (+ mrt-fail 1))
+        (append!
+          mrt-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+;; ---- Peano arithmetic ----
+
+(define
+  mrt-peano
+  (mau/parse-module
+    "fmod PEANO is\n  sort Nat .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op _+_ : Nat Nat -> Nat .\n  op _*_ : Nat Nat -> Nat .\n  vars X Y : Nat .\n  eq 0 + Y = Y .\n  eq s X + Y = s (X + Y) .\n  eq 0 * Y = 0 .\n  eq s X * Y = Y + (X * Y) .\nendfm"))
+
+(mrt-check!
+  "add-2-1"
+  (mau/reduce->str mrt-peano "s s 0 + s 0")
+  "s_(s_(s_(0)))")
+(mrt-check! "add-0-0" (mau/reduce->str mrt-peano "0 + 0") "0")
+(mrt-check! "add-id-left" (mau/reduce->str mrt-peano "0 + s s 0") "s_(s_(0))")
+(mrt-check!
+  "mul-2-2"
+  (mau/reduce->str mrt-peano "s s 0 * s s 0")
+  "s_(s_(s_(s_(0))))")
+(mrt-check! "mul-zero" (mau/reduce->str mrt-peano "0 * s s s 0") "0")
+(mrt-check! "mul-by-zero" (mau/reduce->str mrt-peano "s s 0 * 0") "0")
+(mrt-check!
+  "nested"
+  (mau/reduce->str mrt-peano "(s 0 + s 0) * s s 0")
+  "s_(s_(s_(s_(0))))")
+
+;; ---- list manipulation ----
+
+(define
+  mrt-list
+  (mau/parse-module
+    "fmod NATLIST is\n  sorts Nat List .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op nil : -> List .\n  op cons : Nat List -> List .\n  op append : List List -> List .\n  op length : List -> Nat .\n  op rev : List -> List .\n  var X : Nat .\n  vars L M : List .\n  eq append(nil, M) = M .\n  eq append(cons(X, L), M) = cons(X, append(L, M)) .\n  eq length(nil) = 0 .\n  eq length(cons(X, L)) = s length(L) .\n  eq rev(nil) = nil .\n  eq rev(cons(X, L)) = append(rev(L), cons(X, nil)) .\nendfm"))
+
+(mrt-check!
+  "append"
+  (mau/reduce->str mrt-list "append(cons(0, nil), cons(s 0, nil))")
+  "cons(0, cons(s_(0), nil))")
+(mrt-check!
+  "append-nil"
+  (mau/reduce->str mrt-list "append(nil, cons(0, nil))")
+  "cons(0, nil)")
+(mrt-check!
+  "length-2"
+  (mau/reduce->str mrt-list "length(cons(0, cons(s 0, nil)))")
+  "s_(s_(0))")
+(mrt-check! "length-0" (mau/reduce->str mrt-list "length(nil)") "0")
+(mrt-check!
+  "rev"
+  (mau/reduce->str mrt-list "rev(cons(0, cons(s 0, nil)))")
+  "cons(s_(0), cons(0, nil))")
+(mrt-check! "rev-empty" (mau/reduce->str mrt-list "rev(nil)") "nil")
+
+;; ---- propositional logic simplifier ----
+
+(define
+  mrt-prop
+  (mau/parse-module
+    "fmod PROPLOGIC is\n  sort Bool .\n  op tt : -> Bool .\n  op ff : -> Bool .\n  op not_ : Bool -> Bool .\n  op _and_ : Bool Bool -> Bool .\n  op _or_ : Bool Bool -> Bool .\n  op _xor_ : Bool Bool -> Bool .\n  vars P Q : Bool .\n  eq not tt = ff .\n  eq not ff = tt .\n  eq tt and P = P .\n  eq ff and P = ff .\n  eq tt or P = tt .\n  eq ff or P = P .\n  eq P xor ff = P .\n  eq P xor tt = not P .\nendfm"))
+
+(mrt-check! "not-tt" (mau/reduce->str mrt-prop "not tt") "ff")
+(mrt-check! "and-simpl" (mau/reduce->str mrt-prop "not (tt and ff)") "tt")
+(mrt-check! "or-simpl" (mau/reduce->str mrt-prop "ff or (tt and tt)") "tt")
+(mrt-check! "double-neg" (mau/reduce->str mrt-prop "not not tt") "tt")
+(mrt-check! "xor-id" (mau/reduce->str mrt-prop "tt xor ff") "tt")
+(mrt-check! "xor-tt" (mau/reduce->str mrt-prop "ff xor tt") "tt")
+(mrt-check!
+  "deep"
+  (mau/reduce->str mrt-prop "(tt and tt) or (not not ff)")
+  "tt")
+
+;; ---- non-linear pattern (repeated variable) + no-match leaves term ----
+
+(define
+  mrt-same
+  (mau/parse-module
+    "fmod SAME is\n  sorts Elt Bool .\n  op a : -> Elt .\n  op b : -> Elt .\n  op tt : -> Bool .\n  op same : Elt Elt -> Bool .\n  var X : Elt .\n  eq same(X, X) = tt .\nendfm"))
+
+(mrt-check! "nonlinear-match" (mau/reduce->str mrt-same "same(a, a)") "tt")
+(mrt-check!
+  "nonlinear-nomatch"
+  (mau/reduce->str mrt-same "same(a, b)")
+  "same(a, b)")
+(mrt-check! "no-rule-stays" (mau/reduce->str mrt-same "b") "b")
+
+;; ---- low-level matching ----
+
+(mrt-check!
+  "match-var-binds"
+  (= nil (mau/match (mau/var "X" "Nat") (mau/const "0") {}))
+  false)
+(mrt-check!
+  "match-mismatch"
+  (mau/match (mau/const "0") (mau/const "1") {})
+  nil)
+(mrt-check!
+  "subst-apply"
+  (mau/term->str
+    (mau/subst-apply
+      (assoc {} "X" (mau/const "0"))
+      (mau/app "s_" (list (mau/var "X" "Nat")))))
+  "s_(0)")
+
+(define mau-reduce-tests-run! (fn () {:failures mrt-failures :total (+ mrt-pass mrt-fail) :passed mrt-pass :failed mrt-fail}))

lib/maude/tests/rewrite.sx

@@ -0,0 +1,114 @@
+;; lib/maude/tests/rewrite.sx — Phase 5: system modules + rewrite rules.
+
+(define mrw-pass 0)
+(define mrw-fail 0)
+(define mrw-failures (list))
+
+(define
+  mrw-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! mrw-pass (+ mrw-pass 1))
+      (do
+        (set! mrw-fail (+ mrw-fail 1))
+        (append!
+          mrw-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+;; ---- AC multiset transition (the headline: rule on a sub-multiset) ----
+
+(define
+  mrw-coins
+  (mau/parse-module
+    "mod COINS is\n  sort Marking .\n  op nil : -> Marking .\n  op q : -> Marking .\n  op d : -> Marking .\n  op _;_ : Marking Marking -> Marking [assoc comm id: nil] .\n  rl [change] : q ; q ; q ; q => d .\nendm"))
+
+(mrw-check! "coins-kind" (mau/module-kind mrw-coins) "mod")
+(mrw-check! "coins-rules" (len (mau/module-rules mrw-coins)) 1)
+(mrw-check! "coins-exact" (mau/rewrite-canon mrw-coins "q ; q ; q ; q") "d")
+(mrw-check!
+  "coins-5"
+  (mau/rewrite-canon mrw-coins "q ; q ; q ; q ; q")
+  "_;_(d,q)")
+(mrw-check!
+  "coins-8"
+  (mau/rewrite-canon mrw-coins "q ; q ; q ; q ; q ; q ; q ; q")
+  "_;_(d,d)")
+(mrw-check!
+  "coins-3-stuck"
+  (mau/rewrite-canon mrw-coins "q ; q ; q")
+  "_;_(q,q,q)")
+
+;; ---- cyclic state machine (bounded rew) ----
+
+(define
+  mrw-traffic
+  (mau/parse-module
+    "mod TRAFFIC is\n  sort Light .\n  ops red green yellow : -> Light .\n  rl [g] : red => green .\n  rl [y] : green => yellow .\n  rl [r] : yellow => red .\nendm"))
+
+(mrw-check! "traffic-1" (mau/rew->str mrw-traffic "red" 1) "green")
+(mrw-check! "traffic-2" (mau/rew->str mrw-traffic "red" 2) "yellow")
+(mrw-check! "traffic-3" (mau/rew->str mrw-traffic "red" 3) "red")
+(mrw-check! "traffic-0" (mau/rew->str mrw-traffic "green" 0) "green")
+
+;; ---- nondeterministic branching: rew (one path) vs search (all paths) ----
+
+(define
+  mrw-ndet
+  (mau/parse-module
+    "mod NDET is\n  sort S .\n  ops a b c d goal : -> S .\n  rl [r1] : a => b .\n  rl [r2] : a => c .\n  rl [r3] : b => d .\n  rl [r4] : c => goal .\nendm"))
+
+;; rew takes the first rule each step: a -> b -> d (stuck), never reaches goal.
+(mrw-check! "ndet-rew-path" (mau/rewrite->str mrw-ndet "a") "d")
+(mrw-check! "ndet-succ" (mau/successors mrw-ndet "a") (list "b" "c"))
+(mrw-check!
+  "ndet-search-goal"
+  (mau/search mrw-ndet "a" "goal" 5)
+  true)
+(mrw-check!
+  "ndet-search-shallow"
+  (mau/search mrw-ndet "a" "goal" 1)
+  false)
+(mrw-check! "ndet-search-self" (mau/search mrw-ndet "a" "a" 3) true)
+(mrw-check! "ndet-search-d" (mau/search mrw-ndet "a" "d" 5) true)
+
+;; ---- conditional rule (crl with equational guard) ----
+
+(define
+  mrw-clock
+  (mau/parse-module
+    "mod CLOCK is\n  sorts Nat Bool .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op true : -> Bool .\n  op false : -> Bool .\n  op _<_ : Nat Nat -> Bool .\n  op clk : Nat -> Nat .\n  vars M N : Nat .\n  eq 0 < s N = true .\n  eq N < 0 = false .\n  eq s M < s N = M < N .\n  crl [tick] : clk(N) => clk(s N) if N < s s s 0 = true .\nendm"))
+
+;; tick fires while N < 3, then stops at clk(3).
+(mrw-check!
+  "clock-run"
+  (mau/rewrite->str mrw-clock "clk(0)")
+  "clk(s_(s_(s_(0))))")
+(mrw-check!
+  "clock-from-1"
+  (mau/rewrite->str mrw-clock "clk(s 0)")
+  "clk(s_(s_(s_(0))))")
+(mrw-check!
+  "clock-step1"
+  (mau/rew->str mrw-clock "clk(0)" 1)
+  "clk(s_(0))")
+
+;; ---- eqs interleave with rules ----
+
+(define
+  mrw-mix
+  (mau/parse-module
+    "mod MIX is\n  sort Nat .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op _+_ : Nat Nat -> Nat .\n  op f : Nat -> Nat .\n  vars X Y : Nat .\n  eq 0 + Y = Y .\n  eq s X + Y = s (X + Y) .\n  rl [step] : f(X) => f(X + s 0) .\nendm"))
+
+;; each rule step adds one (via the rule), eqs normalise the sum.
+(mrw-check!
+  "mix-step1"
+  (mau/rew->str mrw-mix "f(s 0)" 1)
+  "f(s_(s_(0)))")
+(mrw-check!
+  "mix-step2"
+  (mau/rew->str mrw-mix "f(0)" 2)
+  "f(s_(s_(0)))")
+
+(define mau-rewrite-tests-run! (fn () {:failures mrw-failures :total (+ mrw-pass mrw-fail) :passed mrw-pass :failed mrw-fail}))

lib/maude/tests/run.sx

@@ -0,0 +1,79 @@
+;; lib/maude/tests/run.sx — running a Maude program (module + commands).
+
+(define mrn-pass 0)
+(define mrn-fail 0)
+(define mrn-failures (list))
+
+(define
+  mrn-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! mrn-pass (+ mrn-pass 1))
+      (do
+        (set! mrn-fail (+ mrn-fail 1))
+        (append!
+          mrn-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+(define
+  mrn-peano
+  "fmod PEANO is\n  sorts Nat NzNat .\n  subsort NzNat < Nat .\n  op 0 : -> Nat .\n  op s_ : Nat -> NzNat .\n  op _+_ : Nat Nat -> Nat .\n  op _*_ : Nat Nat -> Nat .\n  vars X Y : Nat .\n  eq 0 + Y = Y .\n  eq s X + Y = s (X + Y) .\n  eq 0 * Y = 0 .\n  eq s X * Y = Y + (X * Y) .\nendfm\nred s 0 + s s 0 .\nred 0 + 0 .\nreduce in PEANO : s s 0 * s s 0 .")
+
+(mrn-check!
+  "peano-results"
+  (mau/run mrn-peano)
+  (list "(s (s (s 0)))" "0" "(s (s (s (s 0))))"))
+
+(mrn-check! "peano-count" (len (mau/run-program mrn-peano)) 3)
+(mrn-check!
+  "peano-cmd-kind"
+  (get (first (mau/run-program mrn-peano)) :cmd)
+  "reduce")
+
+;; least-sort annotated output: s_ : Nat -> NzNat, so s(...) is NzNat
+(mrn-check!
+  "peano-pretty"
+  (mau/run-pretty mrn-peano)
+  (list
+    "result NzNat: (s (s (s 0)))"
+    "result Nat: 0"
+    "result NzNat: (s (s (s (s 0))))"))
+
+(define
+  mrn-coins
+  "mod COINS is\n  sort M .\n  op nil : -> M .\n  op q : -> M .\n  op d : -> M .\n  op _;_ : M M -> M [assoc comm id: nil] .\n  rl [change] : q ; q ; q ; q => d .\nendm\nrew q ; q ; q ; q ; q .\nrewrite q ; q ; q ; q ; q ; q ; q ; q .")
+
+(mrn-check! "coins-results" (mau/run mrn-coins) (list "(d ; q)" "(d ; d)"))
+
+(mrn-check!
+  "coins-cmd-kind"
+  (get (first (mau/run-program mrn-coins)) :cmd)
+  "rewrite")
+
+;; search command
+(define
+  mrn-ndet
+  "mod NDET is\n  sort S .\n  ops a b c goal : -> S .\n  rl [r1] : a => b .\n  rl [r2] : a => c .\n  rl [r3] : c => goal .\nendm\nsearch a =>* goal .\nsearch a =>* b .\nsearch b =>* goal .")
+
+(mrn-check!
+  "search-results"
+  (mau/run mrn-ndet)
+  (list "a => c => goal" "a => b" "no solution"))
+(mrn-check!
+  "search-cmd-kind"
+  (get (first (mau/run-program mrn-ndet)) :cmd)
+  "search")
+(mrn-check!
+  "search-pretty"
+  (first (mau/run-pretty mrn-ndet))
+  "search: a => c => goal")
+
+;; module-only (no commands) runs to an empty result list
+(mrn-check!
+  "no-commands"
+  (mau/run "fmod EMPTY is\n  sort S .\n  op a : -> S .\nendfm")
+  (list))
+
+(define mau-run-tests-run! (fn () {:failures mrn-failures :total (+ mrn-pass mrn-fail) :passed mrn-pass :failed mrn-fail}))

lib/maude/tests/searchpath.sx

@@ -0,0 +1,66 @@
+;; lib/maude/tests/searchpath.sx — search returning the witness path.
+
+(define msp-pass 0)
+(define msp-fail 0)
+(define msp-failures (list))
+
+(define
+  msp-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! msp-pass (+ msp-pass 1))
+      (do
+        (set! msp-fail (+ msp-fail 1))
+        (append!
+          msp-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+(define
+  msp-ndet
+  (mau/parse-module
+    "mod NDET is\n  sort S .\n  ops a b c d goal : -> S .\n  rl [r1] : a => b .\n  rl [r2] : a => c .\n  rl [r3] : b => d .\n  rl [r4] : c => goal .\nendm"))
+
+;; shortest path a -> c -> goal
+(msp-check!
+  "path-to-goal"
+  (mau/search-path msp-ndet "a" "goal" 5)
+  (list "a" "c" "goal"))
+(msp-check!
+  "path-length"
+  (mau/search-length msp-ndet "a" "goal" 5)
+  2)
+(msp-check!
+  "path-self"
+  (mau/search-path msp-ndet "a" "a" 3)
+  (list "a"))
+(msp-check!
+  "path-one-step"
+  (mau/search-path msp-ndet "a" "b" 3)
+  (list "a" "b"))
+(msp-check!
+  "path-unreachable"
+  (mau/search-path msp-ndet "d" "goal" 5)
+  nil)
+(msp-check!
+  "path-depth-limited"
+  (mau/search-path msp-ndet "a" "goal" 1)
+  nil)
+
+;; a counter that ticks up: path shows each state
+(define
+  msp-walk
+  (mau/parse-module
+    "mod WALK is\n  sort Pos .\n  op z : -> Pos .\n  op s : Pos -> Pos .\n  op p : Pos -> Pos .\n  var X : Pos .\n  rl [step] : p(X) => p(s(X)) .\nendm"))
+
+(msp-check!
+  "walk-path"
+  (mau/search-path msp-walk "p(z)" "p(s(s(z)))" 5)
+  (list "p(z)" "p(s(z))" "p(s(s(z)))"))
+(msp-check!
+  "walk-length"
+  (mau/search-length msp-walk "p(z)" "p(s(s(s(z))))" 6)
+  3)
+
+(define mau-searchpath-tests-run! (fn () {:failures msp-failures :total (+ msp-pass msp-fail) :passed msp-pass :failed msp-fail}))

lib/maude/tests/sorts.sx

@@ -0,0 +1,53 @@
+;; lib/maude/tests/sorts.sx — order-sorted least-sort inference.
+
+(define mso-pass 0)
+(define mso-fail 0)
+(define mso-failures (list))
+
+(define
+  mso-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! mso-pass (+ mso-pass 1))
+      (do
+        (set! mso-fail (+ mso-fail 1))
+        (append!
+          mso-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+(define
+  mso-m
+  (mau/parse-module
+    "fmod NUMS is\n  sorts Zero NzNat Nat .\n  subsort Zero < Nat .\n  subsort NzNat < Nat .\n  op 0 : -> Zero .\n  op 1 : -> NzNat .\n  op s_ : Nat -> Nat .\n  op _+_ : Nat Nat -> Nat .\n  op p : NzNat -> NzNat .\n  op f : Nat -> Nat .\n  op f : NzNat -> NzNat .\nendfm"))
+
+;; constants take their declared result sort
+(mso-check! "sort-zero" (mau/term-sort-src mso-m "0") "Zero")
+(mso-check! "sort-one" (mau/term-sort-src mso-m "1") "NzNat")
+
+;; application: arg subsort of declared domain
+(mso-check! "sort-s0" (mau/term-sort-src mso-m "s 0") "Nat")
+(mso-check! "sort-plus" (mau/term-sort-src mso-m "0 + 1") "Nat")
+(mso-check! "sort-p" (mau/term-sort-src mso-m "p(1)") "NzNat")
+
+;; variable keeps its sort
+(mso-check! "sort-var" (mau/term-sort mso-m (mau/var "X" "Nat")) "Nat")
+
+;; LEAST sort under overloading: f(1) fits both f decls -> the smaller, NzNat
+(mso-check! "least-f-1" (mau/term-sort-src mso-m "f(1)") "NzNat")
+;; f(s 0): s 0 is Nat, only fits f : Nat -> Nat
+(mso-check! "least-f-s0" (mau/term-sort-src mso-m "f(s 0)") "Nat")
+;; nested: f(f(1)) -> f(NzNat) -> NzNat
+(mso-check! "least-nested" (mau/term-sort-src mso-m "f(f(1))") "NzNat")
+
+;; membership-style sort checks
+(mso-check! "has-zero-nat" (mau/has-sort-src? mso-m "0" "Nat") true)
+(mso-check! "has-one-nat" (mau/has-sort-src? mso-m "1" "Nat") true)
+(mso-check! "has-zero-not-nznat" (mau/has-sort-src? mso-m "0" "NzNat") false)
+(mso-check! "has-refl" (mau/has-sort-src? mso-m "1" "NzNat") true)
+
+;; unknown operator -> "?"
+(mso-check! "sort-unknown" (mau/term-sort mso-m (mau/const "ghost")) "?")
+
+(define mau-sorts-tests-run! (fn () {:failures mso-failures :total (+ mso-pass mso-fail) :passed mso-pass :failed mso-fail}))

lib/maude/tests/strategy.sx

@@ -0,0 +1,151 @@
+;; lib/maude/tests/strategy.sx — Phase 6: strategy language.
+
+(define mst-pass 0)
+(define mst-fail 0)
+(define mst-failures (list))
+
+(define
+  mst-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! mst-pass (+ mst-pass 1))
+      (do
+        (set! mst-fail (+ mst-fail 1))
+        (append!
+          mst-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+;; ---- a branching system; meaning depends on the strategy ----
+
+(define
+  mst-mod
+  (mau/parse-module
+    "mod CHOICE is\n  sort S .\n  ops a b c x y : -> S .\n  rl [r1] : a => b .\n  rl [r2] : b => c .\n  rl [toX] : a => x .\n  rl [toY] : a => y .\nendm"))
+
+(define mst-env {})
+(dict-set! mst-env "twice" (mau/s-seq (mau/s-rule "r1") (mau/s-rule "r2")))
+(dict-set! mst-env "anyplus" (mau/s-plus (mau/s-all)))
+(dict-set! mst-env "norm" (mau/s-bang (mau/s-all)))
+
+;; basic combinators
+(mst-check!
+  "idle"
+  (mau/srun-canon mst-mod mst-env (mau/s-idle) "a")
+  (list "a"))
+(mst-check! "fail" (mau/srun-canon mst-mod mst-env (mau/s-fail) "a") (list))
+(mst-check!
+  "single-rule"
+  (mau/srun-canon mst-mod mst-env (mau/s-rule "r1") "a")
+  (list "b"))
+(mst-check!
+  "single-rule-x"
+  (mau/srun-canon mst-mod mst-env (mau/s-rule "toX") "a")
+  (list "x"))
+(mst-check!
+  "all"
+  (mau/srun-canon mst-mod mst-env (mau/s-all) "a")
+  (list "b" "x" "y"))
+
+;; sequencing: order matters
+(mst-check!
+  "seq-ok"
+  (mau/srun-canon
+    mst-mod
+    mst-env
+    (mau/s-seq (mau/s-rule "r1") (mau/s-rule "r2"))
+    "a")
+  (list "c"))
+(mst-check!
+  "seq-fail"
+  (mau/srun-canon
+    mst-mod
+    mst-env
+    (mau/s-seq (mau/s-rule "r2") (mau/s-rule "r1"))
+    "a")
+  (list))
+
+;; alternation: union
+(mst-check!
+  "alt"
+  (mau/srun-canon
+    mst-mod
+    mst-env
+    (mau/s-alt (mau/s-rule "toX") (mau/s-rule "toY"))
+    "a")
+  (list "x" "y"))
+(mst-check!
+  "alt-with-fail"
+  (mau/srun-canon
+    mst-mod
+    mst-env
+    (mau/s-alt (mau/s-rule "r2") (mau/s-rule "r1"))
+    "a")
+  (list "b"))
+
+;; iteration
+(mst-check!
+  "star"
+  (mau/srun-canon mst-mod mst-env (mau/s-star (mau/s-all)) "a")
+  (list "a" "b" "c" "x" "y"))
+(mst-check!
+  "plus"
+  (mau/srun-canon mst-mod mst-env (mau/s-plus (mau/s-all)) "a")
+  (list "b" "c" "x" "y"))
+(mst-check!
+  "bang-normal-forms"
+  (mau/srun-canon mst-mod mst-env (mau/s-bang (mau/s-all)) "a")
+  (list "c" "x" "y"))
+(mst-check!
+  "star-from-b"
+  (mau/srun-canon mst-mod mst-env (mau/s-star (mau/s-all)) "b")
+  (list "b" "c"))
+
+;; named strategies + strategy expressions as values
+(mst-check!
+  "named-twice"
+  (mau/srun-canon mst-mod mst-env (mau/s-name "twice") "a")
+  (list "c"))
+(mst-check!
+  "named-anyplus"
+  (mau/srun-canon mst-mod mst-env (mau/s-name "anyplus") "a")
+  (list "b" "c" "x" "y"))
+(mst-check!
+  "named-norm"
+  (mau/srun-canon mst-mod mst-env (mau/s-name "norm") "a")
+  (list "c" "x" "y"))
+
+;; nested composition: (r1 ; r2) | toX
+(mst-check!
+  "nested"
+  (mau/srun-canon
+    mst-mod
+    mst-env
+    (mau/s-alt
+      (mau/s-seq (mau/s-rule "r1") (mau/s-rule "r2"))
+      (mau/s-rule "toX"))
+    "a")
+  (list "c" "x"))
+
+;; ---- a 1-D walk: strategy chooses how far ----
+
+(define
+  mst-walk
+  (mau/parse-module
+    "mod WALK is\n  sort Pos .\n  op 0 : -> Pos .\n  op s_ : Pos -> Pos .\n  op p : Pos -> Pos .\n  var X : Pos .\n  rl [step] : p(X) => p(s X) .\nendm"))
+
+(mst-check!
+  "walk-one"
+  (mau/srun-canon mst-walk {} (mau/s-rule "step") "p(0)")
+  (list "p(s_(0))"))
+(mst-check!
+  "walk-twice"
+  (mau/srun-canon
+    mst-walk
+    {}
+    (mau/s-seq (mau/s-rule "step") (mau/s-rule "step"))
+    "p(0)")
+  (list "p(s_(s_(0)))"))
+
+(define mau-strategy-tests-run! (fn () {:failures mst-failures :total (+ mst-pass mst-fail) :passed mst-pass :failed mst-fail}))

plans/abstractions.md

@@ -0,0 +1,594 @@
+# Abstraction Radar — backlog
+
+Maintained by the read-only `radar` loop (see `plans/agent-briefings/radar-loop.md`).
+Detection only — implementation is a separate, coordinated step owned by the
+relevant subsystem loop, never by radar.
+
+**AHA gate to reach _Proposed_:** ≥3 real consumers · all past Phase 2 & API-stable ·
+structurally identical (file:line evidence) · a natural home (usually NOT lib/guest).
+Anything short → _Watching_ (what's missing) or _Rejected_ (why).
+
+---
+
+## Last scan
+
+- **Date:** 2026-06-07 (radar loop, pass 32)
+- **Pass 32 — A1 DONE.** `loops/conformance` merged to architecture (`db76cc8c`); 13 adopters
+  now on the shared driver; radar spot-checked common-lisp = 487/487 green post-merge →
+  coordination flag CLEARED. A1 moved to a new **Done** section. New nascent subsystems
+  `dream` + `maude` (0 files), `fed-prims` resumed (mutex-deadlock fix). The idle
+  `a1-conformance` loop can be retired (worklist complete).
+- **Date:** 2026-06-07 (radar loop, pass 31)
+- **Pass 31 — A1 conformance loop WORKLIST COMPLETE.** tcl excluded (foreign `*.tcl`); final:
+  4 migrated (common-lisp/erlang/feed/go) + 5 excluded (forth/js/ocaml/smalltalk/tcl). A1 =
+  **12 on shared driver + 6 excluded**; only the parity-gated merge to architecture remains.
+  commerce shipped a refund saga on flow (2nd flow use) + finished Phase 5 → going quiescent.
+  relations building graph algos (all-paths) — still unconsumed (W9 unchanged).
+- **Date:** 2026-06-07 (radar loop, pass 30)
+- **Pass 30:** conformance loop near done — `ocaml` + `smalltalk` excluded (both foreign
+  `test.sh`/corpus runners, as predicted). Tally: 4 migrated, 4 excluded, **tcl only** left.
+  Next A1 milestone = the `loops/conformance`→architecture merge under adopter-parity. No
+  new candidate; relations/artdag steady (no new W9 delegation).
+- **Date:** 2026-06-07 (radar loop, pass 29)
+- **Pass 29:** conformance loop excluded `js` (test262 fixtures) → 4 migrated + 2 excluded,
+  3 remain (ocaml/smalltalk/tcl). New subsystems advancing fast: `relations` → Phase 4
+  federation, `artdag` → Phase 6 federation → both fold into W1 (now 7 federation modules,
+  theme-not-shape holds) and W9 (relations past Phase 2 but not yet consumed by anyone).
+- **Date:** 2026-06-07 (radar loop, pass 28)
+- **Pass 28 — fleet expanding again.** Conformance loop: `go` migrated 609/609; **`forth`
+  excluded** (foreign Forth corpus — classify-then-exclude working). 4 migrated +1 excluded
+  on the branch; js/ocaml/smalltalk/tcl remain. **2 new subsystems:** `relations` (Phase 1,
+  parent/child rel facts → new W9 nascent watch) and `artdag` (nascent, 0 files). `events`
+  MERGED to architecture (its persist+flow adoption now integrated — W4/W8 landed). Briefing
+  commit hints more incoming: `dream`, `host`, +5 language chisels.
+- **Date:** 2026-06-07 (radar loop, passes 26–27)
+- **Passes 26–27 (routine tracking):** conformance loop steady at ~1 migration/iteration —
+  erlang 761/761, then feed 189/189. A1 = 8 on architecture + 3 on the branch; 6 remain.
+  W4 still gated (host-persist adapter not landed); no new subsystem; app loops on
+  incremental domain work (commerce Phase 5 payment envelope, content/events/identity/fed-sx).
+  Nothing new to discover; merge-time adopter-parity flag still open.
+- **Date:** 2026-06-07 (radar loop, pass 25)
+- **Pass 25:** A1 → **8 adopters** (events via its own loop) + common-lisp 487/487 on the
+  conformance branch. The conformance loop **extended the shared `lib/guest` driver**
+  (per-suite counters/preloads) to do it → raised a **coordination flag in A1**: verify the
+  branch is non-regressive against all 8 adopters before merging to architecture. commerce
+  drafting Phase 5 provider-neutral payment envelope. No new candidate; A1 advancing fast.
+- **Date:** 2026-06-07 (radar loop, pass 24)
+- **Pass 24 — three real updates.** (1) **A1 → 7 adopters** (search migrated, counters mode
+  — corrects the earlier exclusion). (2) The dedicated `conformance` loop ran its 1st
+  iteration: refused to force-migrate common-lisp (parity gate worked) and surfaced a
+  **driver feature-gap** (per-suite counters + preloads) gating the complex multi-suite
+  candidates → A1 now splits simple-now vs gated-on-driver-enhancement. (3) **W8 commerce
+  is LIVE** ("order lifecycle as a durable flow-on-sx flow, Phase 3 done") → 2 live flow
+  consumers. events shipped TZ/DST; mod reverted its extraction note (declined on re-read).
+- **Date:** 2026-06-07 (radar loop, pass 23)
+- **Pass 23 — trigger fired (empty streak ends at 19–22).** commerce recorded a Phase 3
+  **flow-integration design** (order saga as a flow-on-sx flow, payment suspended until
+  webhook resume) → 2nd durable-flow consumer; **W8 broadened** from "delivery" to
+  "externally-resumed orchestration on lib/flow." events made its federation transport
+  **fed-sx-ready** (injected) → reinforces W1's 5/5 inject-fed-sx seam. acl left tmux
+  (now fully quiescent). host-persist adapter still not landed (W4 migration still gated).
+- **Empty-discovery streak: passes 19–22** (last verified pass 22). Fleet at steady state —
+  active loops (content CvRDT, events recurrence/reschedule, identity grant-mgmt, fed-sx
+  outbox internals) are building *inside* their domains, not cross-cutting infra. Census
+  exhausted (p17); all gates re-tested (W1 p18, W2 p19). No new candidate clears any gate.
+- **Radar is now trigger-driven.** The next substantive pass needs one of: **(a)** a new
+  subsystem worktree spawning (auto-joins scan), or **(b)** host-persist's durable adapter
+  landing → unblocks the W4 acl/mod→persist/log migration, or **(c)** a quiescent
+  subsystem (acl/mod/search/commerce, static ~9–16 passes) resuming. Polling ~hourly until
+  one fires; will tighten cadence then.
+- **Date:** 2026-06-07 (radar loop, pass 20)
+- **Pass 20 — honest empty pass.** 3 new census recurrences since p17 (normalize/index ×2,
+  query ×3) — all **name collisions** (same noun, domain-specific op), added to the table.
+  Recorded the meta-pattern: the fleet shares vocabulary, not structure. Most subsystems
+  quiescent (acl/mod/search/commerce static ~9-15 passes = API-stable); only events/
+  identity/content/fed-sx still committing domain features. No new gate-clearer.
+- **Date:** 2026-06-07 (radar loop, pass 19)
+- **Pass 19 — honest empty pass.** Scanned 10 active subsystems. content/index.sx is a
+  blog index/tag-cloud listing (presentation, not full-text search — no search reinvention)
+  and content/multi-doc indexing adds no per-viewer filter. **W2 re-tested: still 2**
+  (feed, search) — acl's `permit?`-like matches are its own authZ *engine* (the home),
+  not a downstream read filter. No new candidate cleared any gate.
+- **Date:** 2026-06-07 (radar loop, pass 18)
+- **Pass 18 — W1 gate re-test.** events shipped Phase 4 federation (5th consumer): a 5th
+  divergent merge (sorted agenda + `:origin` provenance), trust-gate = runtime list
+  membership (shares mod's mechanism, not acl's). Reinforces W1's "theme not shape" — but
+  the **inject-fed-sx-transport seam is now 5/5**, strengthening "all are fed-sx
+  consumers-in-waiting." Trust sub-pattern refined: mod+events (runtime set) vs acl (rule).
+- **Date:** 2026-06-07 (radar loop, pass 17)
+- **Pass 17 — filename census declared EXHAUSTED** (see the Census-status table above).
+  Examined the last unswept ≥2 recurrences (schema/engine = acl⇄mod substrate twins;
+  catalog/batch = name collisions; store = divergent). No new candidate. Incremental churn
+  elsewhere (content 621/621, identity PAR, events reminders). Future passes pivot from
+  censusing to re-testing gates as consumers mature.
+- **Date:** 2026-06-07 (radar loop, pass 16)
+- **Pass 16:** events started Phase 3 — **durable notification delivery on `lib/flow`**
+  (new W8: at-least-once + idempotency exemplar; fed-sx/mod roll their own outbox). The two
+  `notify.sx` (feed vs events) are a name collision (read-side digest vs delivery), noted
+  in W8. Substrate-adoption story deepening: app domains now consume persist (content/
+  commerce/events), flow (events), commerce (events), acl-authZ (identity).
+- **Date:** 2026-06-07 (radar loop, pass 15)
+- **Pass 15:** added the **scanning-method note** above after `query.sx` again proved to
+  be merged-lib copies (lib/prolog + lib/persist in every worktree). Corrected census
+  surfaced `wire`×2 (content+mod) → Rejected (shared role, divergent structure: generic SX
+  serializer vs bespoke pipe-format under a Prolog-env string-prim constraint). events↔
+  commerce integration appeared (paid tickets); acl/mod/search quiescent ~7 passes (now
+  API-stable). No new gate-clearer.
+- **Date:** 2026-06-07 (radar loop, pass 14)
+- **Pass 14:** filename census flagged `snapshot`×?? — but the `*/lib/persist/snapshot.sx`
+  copies are just the merged `lib/persist` in each worktree, NOT consumers (same artifact
+  as `lib/feed/rank.sx` everywhere). The one distinct file, `content/snapshot.sx`,
+  reimplements persist's projection-checkpoint on raw KV instead of using `persist/snapshot`
+  → new W7 (persist-adoption nudge). `audit`×3 = the W4 fakes (acl/mod/identity), known.
+- **Date:** 2026-06-07 (radar loop, pass 13)
+- **Pass 13 — honest re-test, no gate-clearer.** Re-tested the two longest-waiting gates
+  against the maturing app-domain loops: **W2** (per-viewer visibility) still 2 consumers
+  (feed, search) — commerce/content/events/identity add no per-viewer read filter; **W3**
+  (pagination) still 2 (feed, search) — `content/page.sx` is an HTML wrapper, not
+  pagination (filename collision, noted in W3). Incremental churn only elsewhere.
+- **Date:** 2026-06-07 (radar loop, pass 12)
+- **Pass 12:** `events` shipped **transactional booking on persist** (3rd live persist
+  consumer) using `persist/append-expect` (optimistic-concurrency CAS, lock-free capacity
+  safety). W4 ledger now shows a persist feature-ladder append → append-once → append-expect
+  that the hand-rolled fakes can't match. No new candidate; W4 reinforced.
+- **Date:** 2026-06-07 (radar loop, pass 11)
+- **Pass 11 — W4 sharpened with a consumer ledger.** commerce built an **order ledger on
+  persist** (2nd live exemplar; uses `persist/append-once` for webhook idempotency) and
+  identity a **grant audit ledger** (in-memory Erlang fake, gated on an Erlang↔persist
+  bridge). The append-only monotonic-seq event-log pattern is now validated across 4
+  domains, 2 live on persist + 3 fakes flagged for adoption. See W4 table.
+- **Date:** 2026-06-07 (radar loop, pass 10)
+- **Pass 10:** commerce/content/events/identity advancing (content 238/238). Probed a
+  shape outside the routing table — **guarded lifecycle state machines** (mod/lifecycle +
+  identity/membership) → new W6: shared *design principle*, divergent *structure*
+  (SX transition-table vs Erlang gen_server), NOT an extraction target. No gate-clearer.
+- **Date:** 2026-06-07 (radar loop, pass 9)
+- **Pass 9:** `commerce` + `content` reached Phase 2 (`content` 162/162). **Key find:
+  `content` built its op log directly on `persist/log`** (backend-injected, append+replay-
+  to-seq) — the live reference exemplar for W4 (see W4). `events` MONTHLY RRULE,
+  `identity` OAuth2 auth-code + PKCE, search boolean-filtered ranked. A1 still 6 adopters.
+- **Date:** 2026-06-06 (radar loop, pass 8)
+- **Pass 8 — fleet expanded by 4 app-domain loops** (the briefing's anticipated
+  `commerce`/`identity` arrivals, auto-picked up by dynamic discovery). All early-stage,
+  **pre-Phase-2 → moving targets, none count toward any gate yet**:
+  - `commerce` (Phase 1: `api/cart/catalog/price`). Its "per-line audit" is a cost
+    *breakdown view* (`api.sx:44`), **not** an append-only decision log → NOT a W4
+    consumer.
+  - `events` (Phase 1: `calendar.sx`, RRULE expansion).
+  - `identity` (early: `session/token`). Defers authZ to acl (`token.sx:15`) — reinforces
+    W2's "delegate `permit?` to acl-on-sx" routing; identity = authN, acl = authZ.
+  - `content` (just-started: `block.sx`).
+  These are the future consumers W2/W3 are waiting on — re-check their per-viewer filters
+  / pagination once each clears Phase 2. No new gate-clearer this pass.
+- **Pass 7:** **A1 jumped 4→6 adopters** — `acl` + `mod` migrated to the shared
+  conformance driver (first app-domain adopters; proves it generalizes past substrates).
+  `host-persist` closed its blob-adapter blocker (durable storage adapter now landing →
+  W4 migration path opening). search shipped proximity/NEAR; flow + persist quiescent.
+- **Pass 6:** new worktree **`host-persist`** (active — building persist's durable host
+  adapter); `feed` went quiescent (left tmux). acl shipped hardening (+25), fed-sx-m1 at
+  Step 6c. **mod loop independently wrote a shared-plumbing note** (`mod-on-sx.md`,
+  538b8a53) corroborating W4/W5 — folded its claims + home disagreements into W1/W4/W5.
+  No new gate-clearer (audit log still 2 consumers), but consumers are now API-stable.
+- **Pass 5:** search (+highlight/snippet) and fed-sx-m1 (+follower_graph) moved; rest
+  unchanged. Filename census: `api`×6, `fed`×3, then `schema/rank/query/page/explain/
+  engine/batch/audit`×2. Examined the ×6 `api.sx` → Rejected (shared name, divergent
+  structure incl. implicit-vs-explicit-state contract). rank/batch/engine all ≤2 +
+  substrate/domain-divergent → no new gate-clearer.
+- **Pass 4:** no churn vs pass 3 (same worktrees/tmux/HEADs/adopters). Swept audit+explain
+  surfaces: acl/mod share an append-only-log shape (→ sharpened W4 with persist/log API
+  evidence) and a proof-explain shape (→ new W5, substrate-bound). No new gate-clearer.
+- **Pass 3 (earlier today):** subsystem set + tmux + A1 adopters (4) all unchanged vs pass 2. Loops
+  advanced: acl shipped Phase 4 federation; search shipped Phase 4 + pagination; feed
+  shipped pagination/threading; mod at Ext 19 (capstone); persist did a worked acl-grants
+  migration (W4). New shape found: offset/limit pagination → folded into W3.
+- **Subsystem set discovered:** loop worktrees `acl, erlang, fed-prims, fed-sx-m1,
+  feed, flow, go, kernel, mod, ocaml, persist, radar, ruby, search,
+  sx-vm-extensions`; main-repo `lib/*` incl. merged `feed` + substrates (`apl,
+  common-lisp, datalog, erlang, forth, go, haskell, hyperscript, js, lua, minikanren,
+  ocaml, prolog, scheme, smalltalk, tcl`) + `lib/guest`.
+  Actively looping (tmux): `acl, fed-sx-m1, feed, flow, mod, persist, search`
+  (+ radar).
+- **New since pass 1:** worktrees `kernel` (empty/unset — not yet a repo) and `ocaml`
+  (`lib/ocaml/baseline` only). Both early-stage, pre–Phase 2 → out of proposal scope.
+- Re-enumerate every pass; new loops (e.g. a future `commerce`/`identity`) auto-join.
+
+**Census status (pass 17): EXHAUSTED.** Every own-namespace filename recurring ≥2× has
+been examined and dispositioned — further filename-censusing is low-yield until new
+subsystems/modules appear. Map:
+| filename | owners | verdict |
+|---|---|---|
+| `api` ×10 | all | Rejected — shared role, divergent state contract |
+| `fed`/`federation` | feed/search/mod/acl(+content) | W1 — theme not shape |
+| `audit` ×3 | acl/mod/identity | W4 — append-only log → persist/log |
+| `page` ×3 | feed/search (pagination) + content (HTML wrapper) | W3 + collision noted |
+| `explain` ×2 | acl/mod | W5 — proof tree, substrate-bound |
+| `snapshot` ×2 | persist(facet) + content(reinvents) | W7 |
+| `wire` ×2 | content(SX serializer) / mod(pipe-format) | Rejected — divergent |
+| `schema`,`engine` ×2 | acl/mod | substrate-twin parallels (Datalog vs Prolog); only audit (W4) is liftable |
+| `catalog`,`batch` ×2 | commerce/persist, mod/persist | name collisions, unrelated |
+| `normalize` ×2 | content(tree-prune)/feed(record-coerce) | name collision (pass 20) |
+| `index` ×2 | content(listing)/search(inverted index) | name collision (pass 20) |
+| `query` ×3 | content(doc-block)/search(bool AST)/persist(stream-read) | 3-way name collision (pass 20) |
+| `store` ×2 | content(on persist) / flow(workflow records) | related concept, divergent |
+| `rank` ×2 | feed/search | different domains (activities vs docs), ≤2 |
+**acl⇄mod are structural twins** (decision engine over a logic substrate, Datalog vs
+Prolog) — they parallel across engine/schema/explain/audit/fed, but only the *audit log*
+is substrate-agnostic and liftable (→ W4); the rest are substrate-idiomatic. Next passes:
+re-test gates (W2/W3/W8) as consumers mature, watch new modules — not re-census.
+
+**Meta-pattern (pass 20):** new module names keep *recurring* but the operations keep
+*colliding* — same noun, domain-specific op (normalize, index, query, catalog, batch,
+notify, page, store all proved to be collisions). This is *why* genuine extraction
+candidates are rare: the fleet shares vocabulary, not structure. The real shared assets
+are the **substrate subsystems** (persist, flow, acl, fed-sx) that app domains *adopt*
+(W1/W2/W4/W7/W8), not hand-rolled libs to extract.
+
+**Scanning-method note (learned the hard way, passes 5/12/14/15):** a filename census
+for *cross-subsystem* recurrence MUST restrict to each subsystem's OWN namespace —
+`X/lib/X/*.sx` — never `X/lib/*/`. The merged substrate libs (`lib/prolog`, `lib/persist`,
+`lib/feed`, `lib/datalog`, …) are checked out inside *every* worktree, so a naive census
+reports e.g. `query.sx`/`snapshot.sx`/`rank.sx` ×N as phantom recurrences that are really
+one merged file copied N times. Correct one-liner:
+`for w in <subsystems>; do for f in $w/lib/$w/*.sx; do basename $f .sx; done; done | sort | uniq -c | sort -rn`.
+
+---
+
+## Done
+
+### A1 · Shared conformance driver — ✅ COMPLETE (merged `db76cc8c`, pass 32)
+Full closed loop: radar detected it → dedicated `conformance` loop implemented it
+(classify-then-migrate-or-exclude, hard parity gate) → **merged to architecture**
+(`db76cc8c Merge loops/conformance into architecture: A1 conformance-driver migration`)
+→ radar spot-verified post-merge (**common-lisp 487/487 green** on architecture — exercises
+the new per-suite-counters/preloads driver feature, the riskiest change). Final state:
+- **13 on the shared driver:** acl, apl, common-lisp, datalog, erlang, events, feed, go,
+  haskell, mod, prolog, relations, search.
+- **6 correctly excluded** (foreign-program runners — a legitimately different harness):
+  forth, js, ocaml, smalltalk, tcl, lua.
+- The shared driver gained per-suite counters + per-suite preloads (backward-compatible);
+  spot-check confirms existing adopters unaffected. Coordination flag CLEARED.
+Detail of the migration arc retained under the original entry below.
+
+## Proposed (cleared the gate)
+
+_(empty — A1 graduated to Done, pass 32.)_
+
+### A1 · Adopt the shared conformance driver across subsystems
+- **Pattern:** every subsystem hand-rolls a near-identical `conformance.sh`
+  (epoch-load → eval → scoreboard emit) and an inline `<x>-test name got expected`
+  pass/fail counter.
+- **Consumers (≥3, overwhelming):** 15 `lib/*/conformance.sh` — `apl, feed, datalog,
+  flow, mod, lua, erlang, forth, go, common-lisp, haskell, js, ocaml, prolog,
+  smalltalk, tcl`.
+- **Home:** `lib/guest` — the one legitimate exception (the shared driver
+  `lib/guest/conformance.sh` + `lib/guest/conformance.sx` already exist; modes
+  `dict` and `counters`).
+- **Status: IN PROGRESS — 6 adopters (pass 7).** `prolog` (dict), `haskell` (counters),
+  `apl` (dict), `datalog` (dict), and **`acl` (dict) + `mod` (dict), newly migrated this
+  pass** — all 3-line exec shims into `lib/guest/conformance.sh` with a `conformance.conf`.
+  **acl + mod are the first *app-domain* adopters** (not language substrates) — strong
+  evidence the driver generalizes beyond the substrate layer, which was the open question.
+  The `apl` migration earlier *surfaced a latent bug*: the old awk extractor
+  under-counted `pipeline` (40 vs the real 152 assertions); true apl total is **562**,
+  not 450 — evidence that adopting the driver also improves correctness.
+- **Not a target (different harness shape):** `lua/conformance.sh` is a Python runner
+  (`lib/lua/conformance.py`) that walks real `*.lua` source files via `lua-eval-ast`
+  and classifies pass/fail/timeout — it does not run SX `deftest` suites with a
+  counter/dict scoreboard, so the shared driver does not fit. Excluded, not pending.
+- **Remaining hand-rolled candidates (~120–220 lines each):** `common-lisp, erlang,
+  feed, forth, go, js, ocaml, smalltalk, tcl` — now being worked by the dedicated
+  `conformance` loop (above). (`lua` excluded: walks real `*.lua` files via Python.
+  `smalltalk` likely excludes too — runs `*.st` via its own `test.sh`. `search` was
+  thought to be excluded but DID migrate via counters mode — see the 7-adopter note.)
+- **Action:** each remaining subsystem's OWN loop migrates when quiescent — add a
+  `conformance.conf` (+ a `test-harness.sx` preload defining its counters) and
+  replace `conformance.sh` with the 1-line exec shim
+  (`exec bash …/guest/conformance.sh …/conformance.conf "$@"`). Recipe template:
+  `lib/haskell/conformance.conf` (counters) or `lib/prolog/conformance.conf` (dict).
+  Keep the `bash lib/X/conformance.sh` entry point so no loop is disrupted.
+- **Priority: HIGH** (15 consumers, low risk, interface-preserving, additive).
+- **8 adopters on architecture** (pass 25): acl, apl, datalog, **events**, haskell, mod,
+  prolog, search — `events` migrated via its OWN loop; `search` via counters mode (which
+  corrects the earlier "search excluded" note). **+4 on the `loops/conformance` branch:
+  `common-lisp` 487/487, `erlang` 761/761, `feed` 189/189, `go` 609/609** — pending merge.
+  **5 EXCLUDED — all foreign-runner harnesses** (correctly, not force-migrated): `forth`
+  (Hayes core.fr via awk+python), `js` (test262 `.js`/`.expected`), `ocaml` (scrapes
+  `test.sh` + `.ml` baseline), `smalltalk` (scrapes `test.sh` + `*.st` corpus), `tcl`
+  (foreign `*.tcl` vs `# expected:` annotations).
+- **✅ CONFORMANCE LOOP WORKLIST COMPLETE (pass 31).** Final A1 picture:
+  - **12 on the shared driver:** acl, apl, datalog, events, haskell, mod, prolog, search
+    (on architecture) + common-lisp, erlang, feed, go (on `loops/conformance`, pending merge).
+  - **6 correctly excluded** (foreign-program runners — testing a language impl against an
+    external corpus is legitimately a different harness): forth, js, ocaml, smalltalk, tcl, lua.
+  - **Honest finding:** the driver's reach is narrower than the raw "15 conformance.sh"
+    count implied — language substrates that run real `.lua/.st/.ml/.tcl/.js/.fr` programs
+    *should* keep their foreign runners. ~half migrate, ~half don't, and that's correct.
+  - **One step left:** merge `loops/conformance` → architecture under the **adopter-parity
+    check** (the coordination flag above — the shared `lib/guest` driver change must be
+    proven non-regressive against all existing adopters first). The loop is now idle.
+- **NOW IN PROGRESS — dedicated loop (2026-06-07).** A human-triggered `conformance` loop
+  (worktree `/root/rose-ash-loops/conformance`, branch `loops/conformance`, tmux session
+  `a1-conformance`, briefing `plans/agent-briefings/conformance-loop.md`) is working the
+  remaining candidates (common-lisp, erlang, feed, forth, go, js, ocaml, smalltalk, tcl)
+  one per iteration, **classify-then-migrate-or-exclude with a hard test-count parity gate**
+  (reverts on any mismatch; never pushes to main/architecture). Radar tracks; it implements.
+- **Driver-capability boundary found (pass 24, first iteration).** The loop did NOT
+  force-migrate `common-lisp` (baseline 305/0 across 12 suites) — the shared driver can't
+  reproduce it: `MODE=counters` supports only ONE global pass/fail counter pair + ONE fixed
+  preload set, but common-lisp needs **per-suite counter names** (8 distinct pairs) and
+  **per-suite preload chains**. It logged a precise blocker + unblock path (extend the
+  `SUITES` entry format with optional per-suite counters/preloads) and moved on.
+- **Driver gap RESOLVED next iteration (pass 25) — but it touched the shared driver.** The
+  loop extended `lib/guest/conformance.sh` (+38 lines: optional per-suite counters + per-suite
+  preloads in the `SUITES` format, backward-compatible) and then migrated common-lisp at
+  **487/487** (above the 305 baseline — likely another extractor under-count correction, à la
+  apl's `pipeline`). The parity gate held throughout.
+- **⚠ COORDINATION FLAG (radar): the `loops/conformance` branch now carries a change to the
+  SHARED `lib/guest` driver** used by all 8 adopters. It's additive by design, but **before
+  this branch merges to `architecture`, re-run the existing adopters' suites under the new
+  driver to confirm zero regression** (acl/apl/datalog/events/haskell/mod/prolog/search).
+  This is the one cross-cutting risk in an otherwise per-subsystem-isolated effort — surfaced
+  here so the merge is gated on adopter-parity, not assumed.
+
+---
+
+## Watching (real but not yet through the gate)
+
+### W1 · Federation scaffold (merge / ingest / backfill / trust-gate)
+- **FAILS the structural-identity gate (deep-dived 2026-06-06, all 4 read).** Consumer
+  count is met (4) but they are *superficially* similar, not structurally identical —
+  the federated unit and merge op differ fundamentally:
+
+  | Subsystem (file) | Federated unit | Merge op | Trust gate | Injected transport |
+  |---|---|---|---|---|
+  | feed (`fed.sx:14,18,40`) | activity streams | dedupe by `(actor verb object)` | none (visibility via `permit?` separately) | `send-fn`, `fetch-fn` |
+  | search (`fed.sx:8`) | inverted indices | relabel DocId `peer*1000+local` + union posting lists | none | none (pure merge fn) |
+  | mod (`fed.sx:11-14,99`) | moderation decisions | advisory-list vs applied-list; bind iff `mod/trusted?` | **yes — runtime list** `mod/trusted? peer scope` | mock outbox / `fed-send!` |
+  | acl (`federation.sx:43,56`) | Datalog delegate facts | pull facts, gate by `trust`/`level_covers` rule, re-saturate | **yes — Datalog rule** at query time | `transport` dict |
+  | events (`federation.sx`) | calendar agendas | fold trusted peers' agendas into one sorted agenda + `:origin` provenance | **yes — runtime list** `ev/trusts?` (peer-id ∈ trust-set) | injected behind `ev/peer-agenda` |
+
+- **The ONLY real commonality is the injection seam** (now 5/5, pass 18), not extractable
+  code: every one says "the real transport is `fed-sx`'s job; inject `send-fn`/`fetch-fn`/
+  `transport`/`peer-agenda` and mock it in tests." That is an architectural *convention the
+  fleet already follows*. The merge op diverges 5 ways (dedupe / index-union / advisory /
+  fact-saturation / agenda-sort). The trust gate, where present, splits: **mod + events use
+  a runtime trust-set membership check; acl uses a declarative Datalog rule** — so even the
+  trust sub-pattern is 2-of-3, and the membership check is a trivial one-liner (below the
+  extraction threshold). No shared merge, no single shared trust mechanism.
+- **Disposition:** do NOT extract a shared "federation lib." When `fed-sx` ships its
+  real transport, these 4 become its *consumers* (wiring `send-fn`/`fetch-fn`/`transport`
+  to it) — that work belongs to each subsystem's loop + the `fed-sx` loop, not a
+  cross-cutting extraction. Stop re-proposing on the shared name. Home: `fed-sx`.
+- **Now 7 federation modules (pass 29):** + `relations` (Phase 4: erel trust-gating,
+  peer_rel/trust, fed-sx mock transport — Datalog-rule trust like acl) and `artdag`
+  (Phase 6: content-addressed cache + trust + **invalidation** — a merge shape unlike any
+  other). Each new one reinforces "theme not shape": 7 divergent merges, all sharing only
+  the inject-fed-sx-transport seam. Verdict unchanged — they're fed-sx consumers-in-waiting.
+- **Narrower sub-claim (mod note, pass 6; refined pass 18):** mod asserts the *fed
+  trust/outbox* shape shares between mod+acl. Radar evidence refines this: the trust gate
+  splits by mechanism, not by subsystem pair — **mod + events** both use a runtime
+  trust-set membership check (`mod/trusted?`, `ev/trusts?`), while **acl** uses a Datalog
+  rule. So a "trust-set membership" helper has 2 consumers (mod, events) — but it's a
+  one-line `member?` and the merge it gates diverges, so still not worth extracting.
+  Resolve at the architecture-merge point if a heavier shared trust-set surface emerges.
+
+### W2 · Per-viewer visibility / permission filter
+- **2 shipped consumers, same shape** — `filter <injected-permit> <ranked/candidate stream>`:
+  - `feed/lib/feed/acl.sx:27` `feed/visible = (feed/filter stream (fn (a) (permit? viewer a)))`,
+    capstone at `:34` (stream → ACL → rank → top-N). `permit?` injected, sig `(viewer activity)→bool`.
+  - `search/lib/search/fed.sx:16` `aclFilter permit docs = filter permit docs`;
+    `topNTfIdfAcl n permit ts idx = take n (aclFilter permit (rankTfIdf ts idx))`.
+    `permit` injected, sig `DocId→Bool` (viewer baked in by caller).
+- **NOT a consumer:** `mod/lib/mod/policy.sx` is moderation policy (reviewer actions),
+  no per-viewer read filter. So mod won't be the 3rd.
+- **Missing:** (a) only 2 consumers, need ≥3; (b) the two interfaces *diverge* —
+  feed passes `(viewer, item)`, search bakes the viewer in — so any shared form must
+  pick a convention; (c) both already **inject** the predicate, and the filter body is
+  literally one line (`filter permit xs`). Leaning toward: the predicate's home is
+  `acl-on-sx` (`permit?`), and the one-line filter is too thin to extract.
+- **Home when ripe:** delegate `permit?` to `acl-on-sx`; do NOT extract the filter.
+  Re-check if a 3rd genuine per-viewer read filter ships (e.g. events/commerce).
+
+### W3 · Collection helpers (group-by, dedupe-by-key, stable top-N, distinct-order, offset/limit page)
+- feed built all of these on APL primitives. search/commerce/events will want
+  group-by / top-N.
+- **NEW (2026-06-06): offset/limit pagination shipped in 2 subsystems, identical shape**
+  `take limit (drop offset xs)`:
+  - `feed/lib/feed/page.sx:9` `feed/page` (offset/limit window over a stream).
+  - `search/lib/search/page.sx:9` `paginate off lim docs = take lim (drop off docs)`.
+  - NOT a 3rd: `persist/lib/persist/query.sx:5` has a *since-cursor* for incremental log
+    consumption — resumable-stream semantics, not result windowing. Different shape.
+  - feed *also* has cursor-by-`:at` recency pagination (`page.sx:21-44`); search has no
+    cursor. So only the plain offset/limit window is shared, and it is a literal 1-liner.
+- **Missing:** ≥3 stable consumers; AND every item here is collection math that belongs
+  in the **substrate** (APL/Haskell already expose grade/sort/unique/take/drop), not a
+  shared lib. A 1-line `take/drop` window is far below the extraction threshold. Watch;
+  revisit only if a non-substrate subsystem needs the same windowing without take/drop.
+- **Filename-collision caution (pass 13):** `content/lib/content/page.sx` is an **HTML
+  page wrapper** (full HTML5 doc), NOT pagination — do not count it as a 3rd pagination
+  consumer. `page.sx` now means two unrelated things across the fleet. Re-tested pass 13:
+  pagination still only feed + search (2).
+
+### W4 · In-memory store fakes → `persist-on-sx`
+- Not an abstraction to extract — a migration target. Every subsystem fakes its
+  store with a mutable list (`feed/-log`, flow store, mod audit, …).
+- **Owner:** `persist-on-sx` (in progress). Tracked there, listed here for visibility.
+- **Concrete instance (file:line, found pass 4): the append-only decision/audit log.**
+  `acl/lib/acl/audit.sx` and `mod/lib/mod/audit.sx` are the SAME hand-rolled shape, and
+  `persist/lib/persist/log.sx` (the persist *log facet*) already implements it durably:
+
+  | role | acl/audit.sx | mod/audit.sx | persist/log.sx (target) |
+  |---|---|---|---|
+  | log var | `acl-audit-log` :9 | `mod/*audit-log*` :10 | backend stream |
+  | monotonic seq | `acl-audit-seq` :10 | `mod/*audit-seq*` :11 | per-stream high-water :1 |
+  | append (auto-seq) | `acl-audit-decide!` | commit :32 | `persist/append` :17 |
+  | count | `acl-audit-count` :51 | `mod/audit-count` :44 | `persist/count` :12 |
+  | read-all oldest-first | snapshot/tail :73 | `mod/audit-all` :43 | `persist/read` :29 |
+  | read seq≥from | — | by-seq | `persist/read-from` :31 |
+
+  Both deliberately use a monotonic seq with **no wall-clock** (deterministic/testable) —
+  identical to persist/log's design. Action when persist's host adapter lands: acl + mod
+  loops swap their in-memory log for `persist/log`. 2 consumers today; not a new lib —
+  the home already exists. Belongs to acl/mod loops × persist loop, not an extraction.
+- **Cross-loop corroboration (pass 6):** the mod loop independently reached the same
+  conclusion — `mod/plans/mod-on-sx.md` (commit 538b8a53): *"mod-sx (Prolog) and acl-sx
+  (Datalog) converged on the same module shape … only the audit log + fed trust/outbox
+  shapes truly share; extract at the architecture-merge point, refactoring both consumers
+  atomically, not unilaterally from a loop branch."* Confirms the shape AND the
+  do-not-extract-unilaterally stance.
+- **Home disagreement to resolve at merge:** mod's note proposes lifting the audit-log
+  primitives into **`lib/guest/`**. Radar routing disagrees: a durable append-only log is
+  a **`persist-on-sx`** concern (the log facet already exists), not language-impl plumbing.
+  Hold the line — `lib/guest` is lexer/parser/AST/HM/test-runner, not an event log.
+- **Migration is becoming concrete:** new `host-persist` loop (worktree + tmux, pass 6)
+  is building the durable-storage host adapter persist was blocked on — once it lands,
+  acl/mod can actually swap to `persist/log`.
+- **LIVE REFERENCE EXEMPLAR (pass 9): `content` already does it right.** `content`
+  (Phase 2 complete, 162/162) built its op log directly on `persist/log` instead of
+  faking it — `content/lib/content/store.sx`: backend injected via `(persist/open)`
+  ("content knows nothing about which backend", :10); append op as event
+  `persist/append b (content/-stream doc-id) …` (:20); read `persist/read` (:36);
+  `persist/last-seq` (:47); **version = replay op stream up to a seq**
+  (filter `persist/event-seq ev <= seq`, :61). "The op log is the source of truth …
+  the materialised doc is a cache, never primary state."
+  This proves the W4 target is real, not hypothetical: acl + mod's hand-rolled
+  monotonic-seq logs should adopt exactly content's `persist/log` pattern.
+- **Consumer ledger of the append-only monotonic-seq event log (pass 11):**
+
+  | consumer | what | backing | note |
+  |---|---|---|---|
+  | content (`store.sx`) | doc op log | **persist/log ✓ live** | plain append + replay-to-seq |
+  | commerce (`ledger.sx`) | order ledger | **persist/log ✓ live** | `persist/append-once` — idempotent, webhook-replay-safe :40,58 |
+  | events (`booking.sx`) | booking roster | **persist/log ✓ live** | `persist/append-expect` — optimistic-concurrency CAS, capacity-safe, lock-free |
+  | acl (`audit.sx`) | decision log | in-memory fake (SX) | migrate directly when host adapter lands |
+  | mod (`audit.sx`) | decision log | in-memory fake (SX) | migrate directly |
+  | identity (`audit.sx`) | grant ledger | in-memory fake (**Erlang**) | `{Seq,Subject,Action}`; needs an **Erlang↔persist bridge** first — author scoped it out until persist lands ("queryable semantics identical") |
+
+- **Two takeaways:** (1) the pattern is **validated across domains** — CRDT doc ops,
+  financial orders, event bookings, rule decisions, OAuth grants all reduce to the same
+  append-only monotonic-seq stream; (2) migrating to `persist/log` is strictly *better*
+  than the fakes — persist exposes a **feature ladder the fakes don't have**:
+  `append` (content) → `append-once`/idempotency (commerce) → `append-expect`/optimistic-
+  concurrency (events). Every fake would have to reinvent a weaker version of these.
+  This is an **adoption** item (the home already exists), NOT a new extraction — owned by
+  persist/host-persist × each consumer loop. The SX fakes (acl, mod) migrate directly;
+  the Erlang fake (identity) is gated on an Erlang↔persist bridge.
+
+### W5 · Proof-tree explanation over a logic-program derivation
+- `acl/lib/acl/explain.sx` (reconstructs a canonical proof by goal-directed search over a
+  saturated Datalog db) and `mod/lib/mod/explain.sx` (renders a Prolog-style proof tree
+  goal-by-goal with proved/unproved marks + unification bindings) are the same *idea*.
+- **Missing / disposition:** only 2 consumers, and they sit on **different substrates**
+  (acl→`lib/datalog`, mod→`lib/prolog`). Proof reconstruction/rendering is logic-engine
+  machinery → it belongs in each **substrate** (datalog/prolog), not a shared app lib.
+  Watch; revisit only if a 3rd logic-backed subsystem reimplements proof explanation.
+- **Cross-loop note (pass 6):** mod's note calls `mod/proof-goals` (re-query-each-goal)
+  generic and proposes lifting it into **`lib/guest/`**. Radar caveat: proof-tree
+  reconstruction *is* engine-agnostic logic machinery, but `lib/guest` is for
+  lexer/parser/AST/HM/match/test-runner — a logic-engine proof helper is a poor fit there.
+  If genuinely shared by ≥3 engines, a `lib/logic`-style substrate helper is the better
+  home than `lib/guest`. Still 2 consumers → stays Watching either way.
+
+---
+
+### W9 · Parent/child relationship tracking → the new `relations` subsystem (nascent)
+- **New subsystem (pass 28):** `relations` (loops/relations, Phase 1 — `schema.sx`+`api.sx`,
+  rel facts + `relate`/`unrelate`/`children`/`parents`/`related`, 22 tests). Per CLAUDE.md
+  it's the canonical "cross-domain parent/child relationship tracking."
+- **Why watch:** several subsystems already track parent/child *locally* — feed reply-to
+  threading (`thread`/`replies`), content nested block trees, events occurrence/RECURRENCE-ID
+  links. If `relations` becomes the shared home, those are candidate *delegators* (like
+  acl=authZ, persist=log). But it's **Phase 1, pre-Phase-2, moving target** — and each
+  local impl is currently domain-specific (different keys/semantics). Do NOT propose yet.
+  Re-check when relations is past Phase 2 AND ≥3 subsystems' relationship logic could
+  genuinely delegate to it. `artdag` also just spawned (nascent, 0 files) — tracking only.
+  (pass 32: `dream` + `maude` also spawned, nascent 0-files; `fed-prims` resumed.)
+- **Update pass 29:** relations rocketed to **Phase 4** (one gate — past Phase 2 — now met),
+  but it's building ITSELF out (schema/federation), **not yet being consumed** by anyone.
+  The blocker is the other gate: 0 subsystems currently *delegate* their parent/child logic
+  to it (feed/content/events still track locally). Watch for the first real delegation.
+  (artdag also raced to Phase 6 — these ports advance fast; treat committed state as truth.)
+
+### W8 · Durable externally-resumed orchestration on `lib/flow` (suspend→host-IO→resume)
+- **The shared shape:** a durable `flow` that `request`s an external action (a suspend
+  point), the **host** performs the IO, then `flow/resume`s the flow with the outcome;
+  flow's deterministic replay means a completed step never re-runs on recovery.
+- **Consumers (pass 24): 2 LIVE** (events delivery, commerce order saga).
+  - `events/lib/events/notify.sx` (**live**) — reminders/digests as durable flows;
+    suspend on delivery `dispatch`, resume with send outcome. At-least-once + idempotency key.
+  - `commerce` (**LIVE** as of pass 24 — "order lifecycle as a durable flow-on-sx flow,
+    21 tests, Phase 3 done") — order saga `(defflow ordf … (request 'reserve oid) … )`:
+    reserve→pay→fulfil as a flow, **payment stays suspended until the payment webhook calls
+    `flow/resume`**. Carries only the order-id; pure orchestration over `ledger.sx`.
+  - **Now 2 LIVE consumers** of the *same* pattern: long-running process, external resume
+    (delivery dispatch vs payment webhook). fed-sx/mod still roll their own outbox (watch
+    for convergence). Strengthens "lib/flow is the home"; still adoption, not extraction.
+- **Disposition:** `lib/flow` IS the abstraction (events proves it, commerce adopts it) →
+  this is an **adoption** observation like W4, NOT an extraction. Home = `lib/flow`.
+- **Flow-onboarding friction (light signal):** commerce's note logs real gotchas adopting
+  flow — `flow-make-env` returns a large likely-cyclic env (don't print it), env build is
+  slow (budget ~540s like flow's own suite). If ≥3 subsystems hit the same onboarding
+  gotchas, that's a signal to smooth `lib/flow`'s adopter API — flow's concern, flagged here.
+- **Name-collision caveat:** `notify.sx` means two unrelated things — `feed/notify.sx` is
+  a *read-side digest* (group inbox by verb+object), NOT delivery. Do not pair them.
+
+### W7 · Snapshot/projection-checkpoint reimplemented vs `persist/snapshot` (delegate)
+- `persist/lib/persist/snapshot.sx` already provides a **generic** projection checkpoint:
+  store `{:value :seq}` in the kv facet under a namespaced key; the headline property is
+  **snapshot + tail == full replay** (pure, clock-free).
+- `content/lib/content/snapshot.sx` **reimplements that same pattern on raw persist KV**
+  rather than delegating: `persist/kv-put b (content/-snap-key doc-id) {:doc … :seq seq}`
+  (:20), `persist/kv-has?`/`kv-get` (:27-28), and its own tail-replay (:53-59). It never
+  calls `persist/snapshot-*`. content's doc-materialisation *is* a projection fold over
+  its op stream — exactly what `persist/snapshot` checkpoints generically.
+- **Disposition:** persist-adoption nudge (like W4): content could delegate to
+  `persist/snapshot` (its projection = "fold ops → doc"), dropping the duplicated
+  KV+replay code. Home already exists → NOT an extraction; owned by content × persist
+  loops. Only 1 reinventor today; watch whether commerce/events/identity also hand-roll a
+  snapshot on raw KV instead of using the facet (would strengthen the nudge). NB timeline:
+  unclear if `persist/snapshot` predated content's — flag, don't blame.
+
+### W6 · Guarded lifecycle state machine (illegal transition = explicit error)
+- Recurs as a **design principle**, NOT a shared structure (found pass 10):
+  - `mod/lib/mod/lifecycle.sx` — pure SX: immutable case `{:state :error :history …}`,
+    explicit transition table `mod/lc-transitions` (:31), illegal transition returns the
+    case unchanged with `:error` set. States open→triaged→decided→appealed→final.
+  - `identity/lib/identity/membership.sx` — an **Erlang `gen_server`** fragment (identity
+    runs on erlang-on-sx): a `receive` loop with `case find(...) of … {error, St}` guards.
+    States none→pending→active→lapsed→revoked.
+- **Both share the guideline** ("invalid transitions are explicit errors, never silent
+  no-ops") but **implement it substrate-idiomatically** — SX transition-table over
+  immutable values vs an Erlang process loop with per-message case guards. Same W1/`api.sx`
+  trap: shared *idea*, divergent *structure*.
+- **Disposition:** not an extraction target — the FSM mechanism is ~10 substrate-specific
+  lines; the value is in each domain's state graph, not the plumbing. At most a **design
+  guideline** ("model lifecycle as a guarded FSM with explicit-error transitions"). Watch
+  whether commerce-checkout / events-booking add their own — if so it confirms the
+  *guideline*, still not a lib. Do not propose extracting a shared state-machine lib.
+
+## Rejected (considered, declined — do not re-propose)
+
+- **"Continuous auto-implementing abstractor loop."** Rejected at design time: an
+  agent writing across `lib/<x>/**` breaks the worktree isolation that makes the
+  fleet safe, and is rewarded for manufacturing premature/wrong abstractions. The
+  radar is read-only by design. (This file is the alternative.)
+- **Shared `api.sx` "public boundary" module (×6).** Rejected pass 4-5: every subsystem
+  has an `api.sx` (acl, feed, flow, mod, persist, search — a 100% filename match), but it
+  is a naming *convention for the public entry point*, not a shared structure. They
+  disagree on the most basic contract: acl/feed use **implicit module state**
+  (`acl/api.sx` "implicit current db", `feed/api.sx` "single mutable log") while
+  `persist/api.sx` threads an **explicit backend as every call's first arg**; flow's api
+  *builds a Scheme env*, search's api *concatenates a Haskell source string*, mod's is a
+  *lifecycle state-machine façade* (17 defs vs persist's 1). Same role, no common shape —
+  the W1 coincidental-resemblance trap. Do not re-propose on the filename.
+- **Shared `wire.sx` "serialization" module (×2).** Rejected pass 15: content + mod both
+  have a `wire.sx`, but `content/wire.sx` uses the **generic SX serializer**
+  (`serialize`/`parse`, full-fidelity round-trip) while `mod/wire.sx` is a **bespoke
+  versioned pipe-delimited line** (subset of fields, `split` hand-built over slice/len
+  because mod's Prolog-loaded env strips string prims). Shared role (wire format),
+  divergent structure + substrate constraint → not a candidate; the SX serializer is
+  already the shared tool for SX-substrate subsystems, and mod can't use it. (Same family
+  as the `api.sx` rejection above.)
+- **Dumping app-domain plumbing into `lib/guest`.** Rejected: `lib/guest` is for
+  language-implementation plumbing. App patterns route to acl/fed-sx/persist/
+  substrate/host instead (see the routing rule in the briefing).

plans/content-on-sx.md

@@ -19,7 +19,7 @@ injected adapter, not core.
 
 ## Status (rolling)
 
-`bash lib/content/conformance.sh` → **746/746** (Phases 1–4 COMPLETE + ~34 extensions, hardened: HTML/SX escaping, Markdown render + import/export incl. tables & frontmatter (full round-trip), CvRDT flat + nested-tree + durable replication, tree-aware validation, snapshot cache, doc metadata, plain-text render, nested block trees + deep editing + flatten + relative reorder, doc stats + summary + multi-doc index, table + callout + media blocks, HTML page wrapper + SEO page, doc composition + id-remap, portable data + wire serialization, block query + transforms + find/replace, TOC + anchored headings + outline, normalization)
+`bash lib/content/conformance.sh` → **778/778** (Phases 1–4 COMPLETE + ~34 extensions, hardened: HTML/SX escaping, Markdown render + import/export incl. tables & frontmatter (full round-trip), CvRDT flat + nested-tree + durable replication, tree-aware validation, snapshot cache, doc metadata, plain-text render, nested block trees + deep editing + flatten + relative reorder, doc stats + summary + multi-doc index, table + callout + media blocks, HTML page wrapper + SEO page, doc composition + id-remap, portable data + wire serialization, block query + transforms + find/replace, TOC + anchored headings + outline, normalization)
 
 ## Ground rules
 
@@ -113,6 +113,66 @@ lib/content/api.sx ── (content/edit) (content/render) (content/history) ─
 
 ## Progress log
 
+- 2026-06-07 — Hardening (tree-wide audit): the public facade `content/find` /
+  `content/has?` were top-level-only (`doc-find`/`doc-has?`), so you could
+  `content/edit` an update/delete to a nested block by id (those ops are
+  tree-wide) but couldn't read that same block back by id through the facade — a
+  concrete read/write asymmetry. Added a generic `ct-find-id` to doc.sx (descends
+  into any `children` list, mirroring ct-replace-id/ct-remove-id, no section.sx
+  dependency) plus `doc-find-deep`/`doc-has-deep?`; `content/find`/`content/has?`
+  now point at them. Kept `content/find-top`/`content/has-top?` for the
+  top-level-only lookup. Audited all `doc-find`/`doc-ids`/`ct-index-of` callers:
+  the remaining ones are insert/move (positional, top-level by design) — no other
+  seams. +6 api tests (nested deep find/has, top variants miss nested,
+  edit-then-find round-trip). 778/778.
+
+- 2026-06-07 — Hardening: `content/diff` (and `content/diff-versions`) are now
+  TREE-WIDE. They enumerated ids via `doc-ids`/`doc-find` (top-level only), so a
+  diff between two versions of a document containing sections silently missed
+  every nested-block add/remove/change — the same class of seam as the by-id
+  op-log bug. Now ids come from `doc-tree-ids` and lookups from `doc-deep-find`,
+  so nested changes surface precisely. Section containers are excluded from
+  `:changed` (they hold no own content; a child change reports as that child),
+  while whole-section add/remove still shows in `:added`/`:removed`. Flat-doc
+  diffs are unchanged (deep == top-level with no sections). +9 store tests
+  (nested add = section+child, nested change = child only, nested remove,
+  no-op). 772/772.
+
+- 2026-06-07 — Feature: in-document prose search. `content/search-text` (and
+  `content/search-text-ids`) return every content block, tree-wide, whose
+  `(asText b)` contains a term — so search spans text/heading/code/quote/callout
+  text, image alt, list items and table cells **by construction**: it reuses the
+  one canonical "prose of a block" projection (asText) rather than re-listing
+  fields, so it can't drift from stats/find-replace. Section containers are
+  excluded (a term living only in a section's children returns the child, not the
+  wrapper). +7 query tests (cross-field match, count, single-field, no-match,
+  section exclusion, object return). 763/763.
+
+- 2026-06-07 — Consistency: `find-replace` now rewrites **every** text-bearing
+  field, not just `text`. New `fr-rewrite` dispatches per block type — `alt` of
+  image blocks, each item of list blocks, and every header/cell of table blocks
+  now get rewritten alongside text/heading/code/quote/callout. This closes a real
+  seam: `asText`/stats/word-count already fold image alt, list items, and table
+  cells into a document's prose, so a `content/find-replace` rename that skipped
+  them was inconsistent (a renamed term would still show up in word counts and
+  exports). Flipped the two `image alt untouched` tests to `image alt replaced`;
+  +4 tests (list items ×2, table header + cell). find-replace 16/16, 756/756.
+
+- 2026-06-07 — Consistency: `find-replace` now covers `callout` text. `fr-has-text?`
+  (find-replace.sx) added `callout` to its text-bearing block kinds, matching
+  `asText`/stats/summary which already treat callout bodies as prose. Previously a
+  `content/find-replace` over a doc containing callouts silently skipped them. +2
+  find-replace tests (replace callout text; callout kind untouched by text replace).
+  752/752 (41 suites).
+
+- 2026-06-07 — Hardening: fixed a real layer seam (surfaced in the architecture
+  review) — by-id ops (update/delete) now act TREE-WIDE. `ct-replace-id` /
+  `ct-remove-id` (doc.sx) descend into any block carrying a `children` list, so
+  the persist op-log and `content/edit` correctly reach blocks nested in
+  sections (previously a silent no-op). `doc-move` stays top-level (guarded by
+  doc-find); insert/move remain positional. Inline section detection (no
+  section.sx dep). +4 store regression tests (nested update/delete via op-log +
+  replay-to-seq). Full gate over foundational doc.sx: 750/750.
 - 2026-06-07 — Hardening: audit confirmed the persist op-log (store.sx) carries
   every block type through commit → replay (op-insert carries the block
   instance; updates apply by id). Locked with +4 store tests (callout/media

plans/fed-sx-host-primitives.md

@@ -264,6 +264,25 @@ should leave `httpc`/`sqlite` BIFs blocked with that note.
 
 _Newest first._
 
+- 2026-06-07 — Investigated fed-sx-m2 Blockers #4 ("handler-mutex
+  deadlock") per `plans/agent-briefings/fed-prims-mutex-fix.md`.
+  **Outcome: not a mutex bug; no OCaml change — handed back to m2.**
+  Reproduced deterministically (single kernel-route request fails with
+  empty reply while `/` returns 200; also a 3-line minimal echo
+  gen_server reproduces it). Root cause: native `http-listen` runs the
+  handler on a fresh `Thread.create` outside the Erlang scheduler, so
+  `gen_server:call` → `receive` (which `raise`s `er-suspend-marker`
+  expecting an enclosing `er-sched-step-alive!` guard + `er-sched-run-all!`
+  pump) can never complete. Pattern A is inapplicable (single-request
+  failure ⇒ no contention; the mutex is required and must stay) and
+  `Sx_runtime.sx_call` is fully synchronous; no OCaml symbol can reach
+  the SX-level scheduler. Correct fix is Pattern B done purely in
+  `er-bif-http-listen` (`lib/erlang/runtime.sx`): spawn the handler as an
+  er-process and `er-sched-run-all!` to completion, returning the
+  process's `:exit-result`. That file is m2 / `loops/erlang` scope, so
+  this loop made no code change. Full diagnosis + a concrete patch
+  sketch recorded under Blockers below. `bin/sx_server.ml` unchanged;
+  builds untouched.
 - 2026-05-26 — Phase J: `http-request` primitive in `bin/sx_server.ml`
   (NATIVE ONLY — `Unix.gethostbyname` + `Unix.connect`; HTTP/1.1 with
   inline `http://` URL parser; sends Connection: close + Host +
@@ -339,4 +358,73 @@ _Newest first._
 
 ## Blockers
 
-- _(none yet)_
+- 2026-06-07 — **fed-sx-m2 Blockers #4 (handler-mutex deadlock) is NOT a
+  mutex bug — root cause is in the Erlang substrate, so the fix is m2
+  scope, not OCaml.** Investigated per `plans/agent-briefings/
+  fed-prims-mutex-fix.md`. Reproduced deterministically (m2 worktree
+  binary + `next/kernel/*.erl`, port 51920): a **single** request — no
+  concurrency, no prior request — to `/actors/alice/outbox` returns an
+  empty reply (curl exit 52) while the non-kernel control route `/`
+  returns 200 `fed-sx kernel m1`. Also reproduced with a 3-line minimal
+  echo gen_server + a handler that does `gen_server:call(echo, ping)`
+  (no kernel needed; boots in ~20s vs ~7min for the full kernel here).
+
+  Diagnosis: native `http-listen` (`bin/sx_server.ml:743-840`) runs each
+  connection's handler on a fresh `Thread.create` **outside any Erlang
+  scheduler step**. The handler closure (`er-bif-http-listen`'s
+  `sx-handler`, `lib/erlang/runtime.sx`) calls `er-apply-fun handler`
+  directly, so when the route reaches `gen_server:call` →
+  `receive` (`lib/erlang/transpile.sx:1132`), the `receive` captures a
+  `call/cc` and `raise`s `er-suspend-marker` expecting an enclosing
+  `er-sched-step-alive!` guard **and** a scheduler pump
+  (`er-sched-run-all!`). On the native handler thread neither is on the
+  stack: with no guard the suspend either propagates out (→ empty reply,
+  minimal case) or is caught by an Erlang `try`/guard in the route and
+  the request stalls (→ "hang" the m2 loop observed). The kernel
+  gen_server can never be stepped because the only scheduler driver
+  (the boot thread that ran `erlang-eval-ast`) is parked forever in the
+  native `Unix.accept` loop.
+
+  Why Pattern A (release/rescope the runtime mutex) does NOT apply: the
+  failure reproduces on a **single request with zero contention**, so it
+  is not a mutex-contention deadlock. Releasing the mutex cannot help and
+  would be actively harmful — the mutex is *required* to serialise the
+  shared single-threaded SX runtime / scheduler across handler threads.
+  `Sx_runtime.sx_call` (`lib/sx_runtime.ml:102`) is fully synchronous
+  (it just dispatches into the CEK evaluator), which is exactly the
+  briefing's stated condition for falling back from Pattern A to
+  Pattern B. There is also no OCaml-only fix: `grep` confirms nothing in
+  `hosts/ocaml/{lib,bin}` references `er-sched*`/the Erlang scheduler —
+  `er-sched-run-all!` is a pure-SX symbol in `lib/erlang/runtime.sx`, so
+  OCaml cannot pump it. Running the handler synchronously on the accept
+  thread (no `Thread.create`) does not help either: the `er-suspend-marker`
+  `raise` would unwind the native `handle` frame that writes the HTTP
+  response, losing the response across the suspension.
+
+  Recommended fix (Pattern B, **m2 / `loops/erlang` scope — entirely in
+  `er-bif-http-listen`, no OCaml change**): have `sx-handler` run the
+  handler as a scheduled er-process and pump the scheduler to completion,
+  e.g.
+
+  ```
+  (sx-handler
+    (fn (req-dict)
+      (let ((req-pl (er-request-dict-to-proplist req-dict)))
+        (let ((pid (er-spawn-fun
+                     (fn () (er-apply-fun handler (list req-pl))))))
+          (er-sched-run-all!)                       ; drains: handler →
+                                                    ; kernel reply → handler
+          (er-proplist-to-dict
+            (er-proc-field pid :exit-result))))))   ; handler's return value
+  ```
+
+  This keeps every suspend/resume inside the SX scheduler; the native
+  side only ever sees the final response dict. The existing native
+  per-connection `Thread.create` + `Mutex` stay as-is and remain correct
+  (they serialise the single pump across concurrent connections — the
+  mutex must NOT be removed). Verified by reasoning through the full
+  step trace (handler suspends on `receive` → kernel `handle_call`
+  replies → handler resumes → dies with `:exit-result`); the m2 loop
+  should implement + run `next/tests/http_server_tcp.sh` plus a
+  kernel-route smoke. No OCaml or `bin/sx_server.ml` change was made or
+  is needed.

plans/maude-on-sx.md

@@ -62,44 +62,73 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
 ## Roadmap
 
 ### Phase 1 — Parser + signatures
-- [ ] Parser for `fmod` / `endfm` syntax, sort declarations, op declarations, equations.
-- [ ] Sort hierarchy with subsort relations.
-- [ ] Operator overloading by arity + sort.
-- [ ] Tests: parse classic examples (peano nat, list of naturals).
+- [x] Parser for `fmod` / `endfm` syntax, sort declarations, op declarations, equations.
+- [x] Sort hierarchy with subsort relations.
+- [x] Operator overloading by arity + sort.
+- [x] Tests: parse classic examples (peano nat, list of naturals).
 
 ### Phase 2 — Syntactic equational reduction
-- [ ] Apply equations left-to-right until no equation matches.
-- [ ] Standard pattern matching (no equational theories yet — strict syntactic match).
-- [ ] Tests: peano arithmetic, list manipulation, propositional logic simplifier.
+- [x] Apply equations left-to-right until no equation matches.
+- [x] Standard pattern matching (no equational theories yet — strict syntactic match).
+- [x] Tests: peano arithmetic, list manipulation, propositional logic simplifier.
 
 ### Phase 3 — Equational matching (assoc / comm / id)
-- [ ] Extend matching to handle `assoc` operators (flatten then match across permutations of subterm groups).
-- [ ] Handle `comm` (try both argument orderings).
-- [ ] Handle `id: e` (X * e ≡ X).
-- [ ] Combinations: `assoc comm id` together.
-- [ ] Returns *all* matches, not just first — caller drives.
-- [ ] Tests: classic AC-matching examples (multiset rewriting, set theory, group equations).
+- [x] Extend matching to handle `assoc` operators (flatten then match across permutations of subterm groups).
+- [x] Handle `comm` (try both argument orderings).
+- [x] Handle `id: e` (X * e ≡ X).
+- [x] Combinations: `assoc comm id` together.
+- [x] Returns *all* matches, not just first — caller drives.
+- [x] Tests: classic AC-matching examples (multiset rewriting, set theory, group equations).
 
 ### Phase 4 — Conditional equations
-- [ ] `ceq L = R if Cond` — apply only when `Cond` reduces to true.
-- [ ] Recursion via the same reduce engine (terminating because Cond is shorter).
-- [ ] Tests: gcd, sorting, conditional simplifications.
+- [x] `ceq L = R if Cond` — apply only when `Cond` reduces to true.
+- [x] Recursion via the same reduce engine (terminating because Cond is shorter).
+- [x] Tests: gcd, sorting, conditional simplifications.
 
 ### Phase 5 — System modules + rewrite rules
-- [ ] `mod ... endm` syntax with `rl` rules.
-- [ ] Rules apply asymmetrically (`=>` not `=`); fairness across rules.
-- [ ] Default strategy: top-down, leftmost-outermost, first applicable rule.
-- [ ] Tests: state-transition systems (puzzle solvers, protocol simulators).
+- [x] `mod ... endm` syntax with `rl` rules.
+- [x] Rules apply asymmetrically (`=>` not `=`); fairness across rules.
+- [x] Default strategy: top-down, leftmost-outermost, first applicable rule.
+- [x] Tests: state-transition systems (puzzle solvers, protocol simulators).
 
 ### Phase 6 — Strategy language
-- [ ] Compose strategies: sequential `;`, alternative `|`, iteration `*`, fixed-point.
-- [ ] User-named strategies; strategy expressions as values.
-- [ ] Tests: programs whose meaning depends on strategy choice.
+- [x] Compose strategies: sequential `;`, alternative `|`, iteration `*`, fixed-point.
+- [x] User-named strategies; strategy expressions as values.
+- [x] Tests: programs whose meaning depends on strategy choice.
 
 ### Phase 7 — Reflection (META-LEVEL)
-- [ ] Terms-as-data: `META-LEVEL` lets you encode/decode terms as Maude terms.
-- [ ] Build proofs / programs that manipulate Maude programs.
-- [ ] Tests: meta-circular interpretation, generic theorem helpers.
+- [x] Terms-as-data: `META-LEVEL` lets you encode/decode terms as Maude terms.
+- [x] Build proofs / programs that manipulate Maude programs.
+- [x] Tests: meta-circular interpretation, generic theorem helpers.
+
+### Extensions (post-roadmap, toward the end-state goal)
+- [x] Mixfix surface-syntax printer (`lib/maude/pretty.sx`) — `mau/term->maude`
+  renders the internal prefix form back as Maude mixfix (`((s X) + 0)`),
+  driven by op forms; `mau/red->maude` / `mau/rew->maude`. 11 tests.
+- [x] Program runner (`lib/maude/run.sx`) — `mau/run-program` / `mau/run` parse
+  a module plus trailing `reduce`/`red`/`rewrite`/`rew TERM .` commands
+  (`... in MOD : TERM` qualifier accepted) and execute them, rendering results
+  in surface syntax. Runs an idiomatic `.maude` file end-to-end. Now also:
+  `search START =>* GOAL .` command (reports the path), least-sort annotated
+  output via `mau/run-pretty` → `result SORT: TERM` (Maude-style). 10 tests.
+- [x] Witness-path search (`lib/maude/searchpath.sx`) — `mau/search-path` /
+  `mau/search-length` return the shortest sequence of states start..goal (the
+  solution moves), not just yes/no. 8 tests.
+- [x] Order-sorted least-sort inference (`lib/maude/sorts.sx`) — `mau/term-sort`
+  computes the least sort of a term: the smallest result sort among the op
+  declarations whose argument sorts the actual args satisfy (modulo subsorting),
+  so an overloaded `f(1)` is `NzNat` but `f(s 0)` is `Nat`. `mau/has-sort?`
+  for membership-style checks. Answers the plan's substrate question — order-
+  sorted signatures fit cleanly. 14 tests.
+- [x] `gather` / parse-time associativity — infix ops parse left (default,
+  `(E e)`) or right (`(e E)`) per the gather attr, so cons `_:_ [gather (e E)]`
+  reads `a : b : c` as right-nested. Full insertion sort now runs over BARE cons
+  lists (no parens). 7 tests.
+- [x] `owise` equations — parser now reads trailing eq attributes
+  (`eq L = R [owise] .`), `mau/split-attrs`; `mau/crewrite-top` is two-pass
+  (ordinary equations first, owise last), so an owise catch-all fires only when
+  nothing else applies, regardless of declaration order. Parser also reads
+  `label`/`prec`/`owise`/`id:` eq+op attrs. 8 tests.
 
 ### Phase 8 — Propose `lib/guest/rewriting/`
 - [ ] Extract equational matching engine (the most reusable piece).
@@ -107,6 +136,49 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
 - [ ] Extract strategy combinators.
 - [ ] Wait for second consumer before extracting.
 
+**Status: BLOCKED — no second consumer yet.** The reusable core is identified:
+`lib/maude/matching.sx` (AC matching + canon) + `lib/maude/fire.sx`
+(short-circuit firing) are the prime extraction candidates; `lib/maude/strategy.sx`
+(combinators) is the third. Keep them separable. Do not extract until a Pure/
+CafeOBJ/term-rewriting playground consumer appears (or artdag-on-sx's effect
+optimiser, per the chisel note).
+
+### SATURATION (post-roadmap)
+
+All 7 roadmap phases + 7 extensions (pretty / run / search-path / owise /
+gather / order-sorted least-sort / search-command + result-sort) DONE, **254/254
+across 13 suites.** The end-state goal — a faithful Maude 3 functional+system
+core that runs idiomatic programs and proves equational identities — is met:
+sorts/subsorts/overloading, equational reduction modulo assoc/comm/id,
+conditional eqs + owise, system rules (rew + BFS search with witness paths),
+a strategy language, and META-LEVEL reflection, with a mixfix surface printer
+and an end-to-end `.maude` runner (reduce/rewrite/search commands, sort-annotated
+output). **artdag-on-sx fit prototype (lib/maude/tests/effects.sx, 8 tests):** artdag's
+optimise passes — adjacent-op fusion, no-op/dead-op elim, identity elim,
+CSE/idempotent dedup — expressed as `eq`s; the optimised pipeline IS the normal
+form, and confluence ⇒ a stable content id. This is the "second consumer"
+spike: it justifies a maude-driven optimiser in `lib/artdag` and the eventual
+`lib/guest/rewriting/` extraction. Faithfulness note surfaced: `id:` only
+affects matching/canon, NOT auto-reduction — write explicit identity eqs (or
+read off the canonical form) if you need `0 + N` to reduce in the term itself.
+
+**Confluence / critical-pair checking (lib/maude/confluence.sx, 12 tests):**
+`mau/confluent?` answers the plan's substrate question "can confluence be
+checked." Two-sided syntactic unification (`mau/u-unify`, with occurs check) →
+critical pairs from LHS overlaps (`mau/critical-pairs`) → joinability via
+`mau/ac-equal?` of the normal forms (`mau/non-joinable-pairs` gives the
+diagnostics, `mau/cp->str` renders `left <?> right`). Caught `f(a)=b, a=c` as
+non-confluent (`b <?> f(c)`); confirmed peano/idempotent/AC examples confluent.
+SCOPE: unification is SYNTACTIC — exact for free/constructor ops, an
+under-approximation for AC overlaps (full AC-unification is NP/infinitary, out
+of scope), but joinability uses the AC-canonical form so AC laws still join
+correctly. This is the CID-stability oracle for the artdag optimiser: an
+optimisation rule set is content-id-stable iff `mau/confluent?` holds.
+
+Pacing down to hardening. Possible niche future work: membership
+axioms (`mb`/`cmb`), critical-pair / confluence checking, meta-search, full
+mixfix (multi-`_` ops, juxtaposition `__`).
+
 ## lib/guest feedback loop
 
 **Consumes:** `core/lex`, `core/pratt`, `core/ast`, `core/match` (with proposed extension for equational matching).
@@ -125,7 +197,129 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
 - Pure language (Albrecht Gräf): https://agraef.github.io/pure-lang/ — practical functional rewriting.
 
 ## Progress log
-_(awaiting Phase 1 — depends on substrate matching maturity from lib/guest/core/match.sx)_
+
+- **Phase 1 (parser + signatures) — DONE, 65/65.** `lib/maude/term.sx` (term
+  repr: var/app dicts, equality, vars, `term->str`) + `lib/maude/parser.sx`
+  (whitespace+bracket tokenizer with `---`/`***` comments; mixfix
+  classification by splitting op names on `_`; precedence-climbing term parser
+  over a pratt table built from op decls; `fmod`/`mod` modules with
+  sorts/subsorts/ops/vars/eqs/rules). Consumes `lib/guest/lex.sx` (ws classes)
+  and `lib/guest/pratt.sx` (op-table lookup). Verified on Peano (`s X + Y`
+  parses `_+_(s_(X), Y)` — prefix binds tighter than infix) and NatList
+  (transitive subsorts NzNat<Nat<List; `_;_` overloaded; `id: nil` / `prec`
+  attrs). ceq/rl/crl parsed structurally (cond split on `if`, label in `[..]`).
+  Suite + conformance driver wired (`lib/maude/conformance.{conf,sh}`, MODE=dict).
+  - Notes for next phases: terms are `{:t :app :op N :args (...)}` /
+    `{:t :var :name N :sort S}`; module carries a `:grammar` so
+    `mau/parse-term-in` can parse term strings against its op table. Overloading
+    is recorded but NOT resolved at parse time (resolve at reduce time).
+
+- **Phase 2 (syntactic reduction) — DONE, 91/91 total.** `lib/maude/reduce.sx`:
+  one-sided syntactic matching (`mau/match` — pattern vars only, non-linear
+  patterns checked by bound-var equality), immutable substitutions via `assoc`,
+  `mau/subst-apply`, top rewrite `mau/rewrite-top` (first unconditional eq whose
+  LHS matches; conditional eqs skipped until Phase 4), innermost normalisation
+  to a fixpoint `mau/normalize` (args normalised before the operator; fuel-
+  guarded). API: `mau/reduce` / `mau/reduce-term` / `mau/reduce->str`. Tested on
+  Peano (+,*), list ops (append/length/rev), a propositional simplifier, and
+  non-linear `same(X,X)`. Innermost is fine for confluent terminating eq sets;
+  Phase 3 will replace the matcher with AC-aware matching (multi-valued).
+
+- **Phase 3 (matching modulo assoc/comm/id) — DONE, 119/119 total. THE CHISEL.**
+  `lib/maude/matching.sx`. `mau/mm` is the multi-valued matcher (returns the
+  full list of substitutions): free=positional, comm=both orderings,
+  assoc=flatten f-spine + ordered sequence match (vars grab contiguous blocks),
+  assoc+comm=multiset match (vars grab sub-multisets via `mau/all-splits` =
+  2^n subset/complement pairs). `id: e` lets a var grab the empty block
+  (contributing e); `mau/var-kmin` gives kmin 0 under id. `mau/canon` is the
+  AC-canonical printout (flatten, drop identities, sort comm args) and powers
+  `mau/ac-equal?` (used for bound-var checks too). AC *rewriting* extends each
+  f-AC equation l=r with rest vars — comm: `f(l,$R)`; assoc: `f($L,l,$R)` —
+  so a rule fires on any sub-multiset/subword (`$`-prefixed rest vars allowed
+  empty). `mau/first-change` walks candidate matches and only commits a rewrite
+  that changes the canonical form — this is what makes idempotency (`X U X = X`)
+  and identity-absorbing matches terminate. API: `mau/ac-reduce` /
+  `mau/ac-reduce->str` / `mau/ac-canon` / `mau/match-all`. Verified: AC match
+  counts (X+Y vs a+b+c = 6), bag collapse, set dedup with empty, group
+  cancellation (assoc non-comm + inverse).
+  - Notes for next phases: AC matching is multi-valued — Phase 5 rule
+    application should iterate ALL of `mau/mm`'s results, not just first. The
+    `mau/ac-rewrite-eq` extension trick (rest vars) is the reusable core for
+    a future `lib/guest/rewriting/` (Phase 8). Keep `mau/canon` as the equality
+    oracle. `$EMPTY` is a transient marker for empty rest blocks w/o id; never
+    leaks past `mau/restv`.
+
+- **Phase 4 (conditional equations) — DONE, 138/138 total.**
+  `lib/maude/conditional.sx` is a condition-aware superset of the Phase 3
+  reducer. `mau/eq-candidates` enumerates (subst, result) pairs for an
+  equation (AC via rest-var extension `mau/ac-candidates`, else `mau/mm`);
+  `mau/try-candidates` commits the first candidate that both makes progress
+  (canonical form changes) AND whose guard holds. `mau/cond-holds?` evaluates
+  `{:kind :eq}` guards (reduce both sides, `ac-equal?`) and `{:kind :bool}`
+  guards (reduce, `=AC= true`), recursing through `mau/cnormalize` — same
+  reducer, so guards can mention other (conditional) equations. Public:
+  `mau/creduce` / `mau/creduce->str` / `mau/ccanon`. Verified on gcd
+  (subtractive, recursive guard), insertion sort (true/false branches), max,
+  and even (bool-kind `if pred` guard).
+  - Notes for next phases: `mau/creduce` is the canonical reducer now; Phase 5
+    rules reduce to normal form via creduce between rewrite steps. `_:_` cons
+    parses LEFT-assoc (no `gather` support yet) — write list literals
+    right-parenthesized, or add a `gather`/parse-assoc attr later if a test
+    needs bare `a : b : c`.
+
+- **Phase 5 (system modules + rewrite rules) — DONE, 159/159 total.**
+  `lib/maude/rewrite.sx` + `lib/maude/fire.sx`. Rules (rl/crl) reuse the
+  equation firing machinery (a rule dict is shaped like an eq). `mau/rewrite`
+  is the default strategy: normalise with eqs (`creduce`), fire ONE rule
+  top-down/leftmost-outermost/first-applicable, renormalise, repeat (bounded
+  by fuel). `mau/rew m src n` = bounded `rew [n]`. `mau/search` is BFS over
+  ALL one-step successors (`mau/all-successors`) for reachability — solves the
+  branching `goal` reachable only off the path `rew` takes. Verified: AC
+  multiset coin-change (rule on a sub-multiset), cyclic traffic light (bounded),
+  branching nondeterminism (rew vs search), conditional `crl` clock, eq/rule
+  interleaving.
+  - **PERF (important):** `lib/maude/fire.sx` is the short-circuiting matcher —
+    `mau/fire-eq` finds the FIRST productive match via predicate-threaded
+    `mau/ms-find`/`mau/seq-find` instead of materialising the whole solution
+    set. Without it, AC rewriting on N identical elements is exponential
+    (`q;q;q;q;q;q;q;q` went 60s+ → <1s). The eager `mau/match-multiset` /
+    `mau/eq-candidates` are kept ONLY for `mau/match-all` and `search` (which
+    truly need every solution). Phase 4 `creduce` and Phase 5 rules both fire
+    via `mau/fire-eq`. Keep this split: never route single-step rewriting
+    through the eager enumerator.
+  - Notes: juxtaposition `__` (empty-token mixfix) and `gather` are NOT parsed —
+    use an explicit infix op for multisets and right-parenthesise list literals.
+    `.` can't be an op token (statement terminator). `mau/search` is the prime
+    Phase 7 reflection / Phase 8 extraction target alongside the matcher.
+
+- **Phase 6 (strategy language) — DONE, 178/178 total.**
+  `lib/maude/strategy.sx`. Strategies are first-class tagged-dict VALUES and
+  set-valued: `mau/sapply ctx strat term` → deduped (by canon) list of results.
+  Combinators: `idle`/`fail`/`all`/`rule LABEL`/`seq`/`alt`/`star`/`plus`/`bang`
+  /`name`. `seq` = flatmap B over A's results; `alt` = union; `star` = reflexive-
+  transitive closure (BFS, canon-deduped); `plus` = A then star; `bang` =
+  normal forms (reachable terms where A yields nothing). Named strategies via a
+  NAME->strategy env dict passed to `mau/srun`/`mau/srun-canon`. Verified that
+  the same rule set computes different things under different strategies
+  (single rule vs all vs seq order vs alt vs star vs bang). Built on Phase 5
+  `mau/all-successors` (rule label filter = `mau/rules-with-label`).
+  - Note: `dict-set!` returns the value, not the dict — build a named-strategy
+    env by binding `(define env {})` then `(dict-set! env ...)`, pass `env`.
+    `srun-canon` sorts results so expected lists must be sorted.
+
+- **Phase 7 (reflection / META-LEVEL) — DONE, 196/196 total.**
+  `lib/maude/meta.sx`. `mau/up-term` re-encodes an object term as a term built
+  from meta-constructors `mt-var`(name,sort) / `mt-app`(op, args...) — a
+  represented term is itself a first-class object term you can build, inspect,
+  transform. `mau/down-term` reverses (round-trips). Reflective ops:
+  `mau/meta-reduce` / `mau/meta-rewrite` / `mau/meta-apply LABEL` take and
+  return represented terms. `mau/meta-circular?` verifies the law
+  `down(metaReduce(up t)) =AC= reduce t` (reflection agrees with the object
+  level). `mau/meta-prove-equal?` is a generic equational theorem helper
+  (prove an identity by joint reduction). Verified: up/down round-trip,
+  meta-reduce returns a represented normal form, meta-circular law on Peano,
+  meta-apply of a single rule, commutativity/associativity instance proofs,
+  and building a program at the meta level then running it.
 
 ## Blockers
-_(speculative — equational matching is algorithmically heavy and may surface JIT issues)_
+_(none)_

plans/rose-ash-on-sx-migration.md

@@ -0,0 +1,170 @@
+# Re-implementing rose-ash on SX — migration strategy
+
+Status: **strategy proposal** (drafted by the `radar` loop, 2026-06-07). Not a
+unilateral architecture decision — a starting point for the fleet to refine. Radar's
+role here is detection: the `*-on-sx` subsystems have converged into a host-agnostic
+re-implementation of rose-ash's domain logic, so this doc proposes *when* and *how* to
+wire them to production.
+
+---
+
+## 1. Premise: we are ~70% into a re-implementation already
+
+The fleet of `lib/<x>` SX subsystems is not a set of experiments — it is rose-ash's
+domain logic, re-expressed substrate-by-substrate, deliberately **host-agnostic**:
+
+| SX subsystem (`lib/`) | rose-ash production domain |
+|---|---|
+| content-on-sx (CRDT docs, versioning, `page.sx` HTML render) | **blog** |
+| commerce-on-sx (catalog, pricing, cart, order + refund sagas) | **market + cart + orders** |
+| events-on-sx (calendar, ticketing, booking) | **events** |
+| feed-on-sx (activity streams, AP-shaped, threading) | **federation** |
+| identity-on-sx (OAuth2, sessions, grants, membership) | **account** |
+| acl-on-sx (permissions) | cross-cutting authZ |
+| relations / likes | **relations / likes** (internal) |
+| persist-on-sx (log / kv / snapshot facets) | per-service Postgres layer |
+| flow-on-sx (durable sagas) | order/refund/delivery workflows |
+| mod-on-sx, search-on-sx | new capabilities |
+
+**The architectural enabler:** every core was built with *injected seams* — `permit?`,
+`send-fn`/`fetch-fn`, `transport`, `dispatch`, `backend`. That is ports-and-adapters
+(hexagonal) on purpose. Evidence from the radar backlog (`plans/abstractions.md`):
+W1 (7/7 federation modules inject the fed-sx transport), W4 (content/commerce/events run
+live on `persist/log`), W8 (events+commerce run sagas on `lib/flow`). **The cores do not
+depend on how they're hosted, persisted, or federated.**
+
+**Corollary that makes the whole migration tractable:** because logic is separated from
+rendering and storage, we can hold the **domain logic to parity** while **freely
+redesigning the presentation** — the two are different layers with different rules.
+
+---
+
+## 2. The gating insight: the cores are *ahead of the host*
+
+The domain logic is mature. What is *not* yet production-grade is the **host trio** — and
+that is the real critical path:
+
+- **host-on-sx** — HTTP / request-response / session host (briefing exists; the OCaml SX
+  HTTP server already serves `sx.rose-ash.com`).
+- **host-persist** — durable storage adapter (real disk/pg/ipfs) under `persist`'s
+  facets (content-addressed blob blocker recently closed).
+- **fed-sx** — the real ActivityPub transport every core injects (well into m2).
+
+> **So "when do we start?" answers itself: start when the host trio is production-grade,
+> not when the cores are done — they mostly already are.** Prioritise the host loops over
+> further domain features.
+
+---
+
+## 3. The model: duplicate → cut over → diverge (per slice)
+
+This is the "duplicate first, then change" approach, made precise. Each domain slice goes
+through three phases independently:
+
+**Phase A — Duplicate (hold logic to parity).** Stand the SX implementation of the slice
+up *in parallel*, behind the existing edge, serving no users yet. Get its **domain/data
+behaviour** to match Python (see §4 on how). Presentation can start as a rough port or an
+early new design — it doesn't have to match.
+
+**Phase B — Cut over (strangler flip).** Point the edge route for that slice at the SX
+host. Python stays as instant rollback. The slice is now live on SX.
+
+**Phase C — Diverge (change freely).** With the slice live and validated, evolve the
+look/feel and functionality on the SX side. The validated domain logic underneath is
+untouched, so UX/feature changes can't silently corrupt data.
+
+You never rewrite the whole platform at once; you walk slices through A→B→C, oldest tree
+strangled last.
+
+---
+
+## 4. The two techniques, and how "we'll change things" reshapes them
+
+### Strangler edge
+The edge (Caddy) is the front door every request hits. Add routing rules so **one route
+at a time** goes to the SX host while everything else still goes to Python. Properties:
+the site is never half-broken; any single route flips back to Python instantly; the old
+app is strangled route-by-route. (Opposite of big-bang swap, which is how these die.)
+
+### Shadow diff — split by layer
+Run the new version on real traffic in the background, discard its output, and **log how
+it differs** from Python. Flip the edge only when diffs are zero/intended.
+
+But because we *intend* to change look/feel + functionality, parity is a tool we apply
+**only where we want sameness**, not a straitjacket:
+
+| Layer | Want parity? | Oracle |
+|---|---|---|
+| **Domain/data** (totals, tax, permissions, what's stored, who-sees-what) | **YES — silent difference = data corruption** | shadow-diff at the *core* boundary; deterministic cores → replay real request logs through the harness and diff |
+| **Presentation/UX** (HTML, layout, look, feel, flows) | **NO — this is what we're changing** | manual QA + design review; this is the Phase-C divergence |
+
+Practical shape: shadow-diff hits the **domain core's output** (the computed order, the
+visible-activity set, the permission decision) — not the rendered HTML. The deterministic,
+harness-replayable cores are the single biggest advantage we have here; it's the same
+parity discipline that made the A1 conformance migration safe (one reference slice, hard
+parity gate, revert on mismatch).
+
+---
+
+## 5. Readiness gates (start the production migration when ALL hold)
+
+1. **Host trio production-grade** — host-on-sx (HTTP/session), host-persist (durable
+   adapter), fed-sx (AP transport) — each conformance-green.
+2. **Data-migration story exists** — a way to get existing production Postgres state into
+   `persist` event streams (event-source the current state, or dual-write during overlap).
+   This is the honest long-pole; it is *not* domain logic and nobody has built it yet.
+3. **One vertical slice proven end-to-end** at data-parity in production — the reference
+   migration, the way the conformance loop migrated one subsystem before the rest.
+
+---
+
+## 6. Sequencing
+
+1. **Host trio first** (critical path — it's behind the cores).
+2. **Build the strangler edge + shadow-diff harness** as first-class tooling: edge routing
+   rules + a dual-run logger that diffs *core outputs* (not HTML) and stores discrepancies.
+3. **First slice = lowest risk × highest readiness × cleanest data oracle.**
+   Recommended: **the blog read path (content-on-sx)** or **the feed read path**
+   — read-heavy, no money, CRDT/versioning + `page.sx` HTML already exist, and the data
+   oracle is clean. *Avoid cart/orders/payments first* (transactional + SumUp webhooks =
+   highest blast radius).
+4. **Persistence-first, federation-last.** Land host-persist + migrate per-domain event
+   stores before any cutover. Do fed-sx federation as a *coordinated* cut near the end —
+   W1 shows all 7 cores light up federation together once the shared transport ships.
+5. **Walk the remaining slices A→B→C**, retiring Python routes as each cuts over.
+
+---
+
+## 7. The honest long tail (mostly host + adapters, not cores)
+
+The cores are pure domain logic; the production *tail* is not in them yet and is most of
+the remaining real effort:
+
+- Auth: first-party cookies / Safari-ITP, CSRF, silent SSO, grant caching.
+- Cross-cutting: rate limiting, observability/metrics, error pages, caching.
+- Integrations: SumUp payment + webhooks, Ghost CMS sync.
+- Presentation: the actual HTMX templates + CSS (this is also where the redesign happens).
+- **Live data migration** — the single biggest non-core workstream.
+
+---
+
+## 8. Concrete next steps
+
+1. Treat the **host trio** as the fleet's critical path; prioritise over more domain features.
+2. Stand up the **strangler edge + core-level shadow-diff harness** as a tool.
+3. Prove **one slice** (blog/content read path) end-to-end in production as the reference.
+4. **Spec the Postgres → persist data migration** (the long-pole nobody has started).
+5. Then walk slices through duplicate → cut over → diverge, redesigning UX in Phase C.
+
+---
+
+## 9. Why this is low-risk despite being a platform rewrite
+
+- It's **wiring host-agnostic cores to a host**, not rewriting domain logic from scratch.
+- The **strangler edge** means the site always works and any route reverts in seconds.
+- **Deterministic cores** make data-parity *mechanically checkable* (replay + diff), so
+  correctness isn't a matter of faith.
+- **Logic/presentation separation** lets us change look/feel + functionality (Phase C)
+  *without* re-risking the validated domain logic.
+- It's the **same discipline that just shipped A1**: one reference migration, a hard
+  parity gate, honest exclusions, verify-before-merge.