artdag: Phase 7 consumes lib/maude mau/confluent? (no bespoke confluence checker)

The CID-stability check now calls mau/confluent? / mau/non-joinable-pairs from
lib/maude/confluence.sx (merged in) instead of re-implementing critical-pair
analysis inside lib/artdag. Picks up confluence.sx via the architecture merge.

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

lib/artdag/conformance.sh

@@ -13,7 +13,7 @@ if [ ! -x "$SX_SERVER" ]; then
   exit 1
 fi
 
-SUITES=(dag analyze plan execute optimize fed cost serialize stats fault)
+SUITES=(dag analyze plan execute optimize fed cost serialize stats fault maude-optimize)
 
 OUT_JSON="lib/artdag/scoreboard.json"
 OUT_MD="lib/artdag/scoreboard.md"
@@ -23,6 +23,26 @@ run_suite() {
   local file="lib/artdag/tests/${suite}.sx"
   local TMP
   TMP=$(mktemp)
+  local MAUDE_LOADS=""
+  local BRIDGE_LOAD=""
+  if [ "$suite" = "maude-optimize" ]; then
+    MAUDE_LOADS='(load "lib/guest/lex.sx")
+(load "lib/guest/pratt.sx")
+(load "lib/maude/term.sx")
+(load "lib/maude/parser.sx")
+(load "lib/maude/sorts.sx")
+(load "lib/maude/reduce.sx")
+(load "lib/maude/matching.sx")
+(load "lib/maude/conditional.sx")
+(load "lib/maude/fire.sx")
+(load "lib/maude/rewrite.sx")
+(load "lib/maude/searchpath.sx")
+(load "lib/maude/strategy.sx")
+(load "lib/maude/meta.sx")
+(load "lib/maude/pretty.sx")
+(load "lib/maude/run.sx")'
+    BRIDGE_LOAD='(load "lib/artdag/maude-bridge.sx")'
+  fi
   cat > "$TMP" << EPOCHS
 (epoch 1)
 (load "spec/stdlib.sx")
@@ -41,6 +61,7 @@ run_suite() {
 (load "lib/persist/log.sx")
 (load "lib/persist/kv.sx")
 (load "lib/persist/api.sx")
+${MAUDE_LOADS}
 (load "lib/artdag/dag.sx")
 (load "lib/artdag/analyze.sx")
 (load "lib/artdag/plan.sx")
@@ -52,6 +73,7 @@ run_suite() {
 (load "lib/artdag/stats.sx")
 (load "lib/artdag/fault.sx")
 (load "lib/artdag/api.sx")
+${BRIDGE_LOAD}
 (epoch 2)
 (eval "(define artdag-test-pass 0)")
 (eval "(define artdag-test-fail 0)")

lib/artdag/maude-bridge.sx

@@ -0,0 +1,118 @@
+; lib/artdag/maude-bridge.sx — adapter between an artdag effect DAG and maude terms.
+; A node {:op :inputs :params :commutative} <-> a maude (mau/app op (args...)).
+; Inputs become argument subterms (recursively from the DAG). A trailing
+; "artdag:meta" subterm carries the params (a write-to-string token) and the
+; commutativity flag, so the encoding is lossless and dag->term->dag is the
+; identity on canonical (content-id) form. Commutative ops map to maude AC
+; operators in the optimizer module, so input order is irrelevant there —
+; mirroring the content-id's order-insensitivity for commutative nodes.
+;
+; maude (lib/maude) is a READ-ONLY consumed substrate: mau/app, mau/const,
+; mau/op, mau/args, mau/app? are its term constructors/accessors.
+
+; ---- list helpers (no host last/but-last) ----
+
+(define
+  artdag/mb-last
+  (fn
+    (xs)
+    (if (empty? (rest xs)) (first xs) (artdag/mb-last (rest xs)))))
+
+(define
+  artdag/mb-but-last
+  (fn
+    (xs)
+    (if
+      (empty? (rest xs))
+      (list)
+      (cons (first xs) (artdag/mb-but-last (rest xs))))))
+
+; ---- params <-> token ----
+; params are keyword-keyed dicts; write-to-string/read round-trips them
+; (key order may differ but the dicts compare structurally equal).
+
+(define artdag/mb-meta-op "artdag:meta")
+
+(define artdag/params->token (fn (params) (write-to-string params)))
+
+(define artdag/token->params (fn (token) (read (open-input-string token))))
+
+(define
+  artdag/mb-meta-term
+  (fn
+    (params commutative)
+    (mau/app
+      artdag/mb-meta-op
+      (list
+        (mau/const (artdag/params->token params))
+        (mau/const (if commutative "c" "n"))))))
+
+(define
+  artdag/mb-meta-term?
+  (fn (t) (and (mau/app? t) (= (mau/op t) artdag/mb-meta-op))))
+
+; ---- dag -> term ----
+
+(define
+  artdag/node->term
+  (fn
+    (node input-terms)
+    (mau/app
+      (artdag/node-op node)
+      (concat
+        input-terms
+        (list
+          (artdag/mb-meta-term
+            (artdag/node-params node)
+            (get node :commutative)))))))
+
+(define
+  artdag/dag->term
+  (fn
+    (dag id)
+    (let
+      ((node (artdag/dag-get dag id)))
+      (artdag/node->term
+        node
+        (map (fn (in) (artdag/dag->term dag in)) (artdag/node-inputs node))))))
+
+; ---- term -> dag ----
+; build-entries with synthesized local names; artdag/build recomputes content-ids
+; (which are name-independent), so the reconstructed dag is identical on canonical
+; form. Shared subterms re-collapse to one node/id during build's dedup.
+
+(define artdag/term-meta (fn (t) (artdag/mb-last (mau/args t))))
+
+(define artdag/term-input-terms (fn (t) (artdag/mb-but-last (mau/args t))))
+
+(define
+  artdag/term-params
+  (fn
+    (t)
+    (artdag/token->params (mau/op (first (mau/args (artdag/term-meta t)))))))
+
+(define
+  artdag/term-commutative
+  (fn
+    (t)
+    (= "c" (mau/op (nth (mau/args (artdag/term-meta t)) 1)))))
+
+(define
+  artdag/term->build
+  (fn
+    (t counter acc)
+    (let
+      ((built (reduce (fn (st child) (let ((r (artdag/term->build child (get st :counter) (get st :acc)))) {:counter (get r :counter) :acc (get r :acc) :names (concat (get st :names) (list (get r :name)))})) {:counter counter :acc acc :names (list)} (artdag/term-input-terms t))))
+      (let ((my-name (str "mb" (get built :counter)))) {:name my-name :counter (+ (get built :counter) 1) :acc (concat (get built :acc) (list (list my-name (mau/op t) (get built :names) (artdag/term-params t) (artdag/term-commutative t))))}))))
+
+(define
+  artdag/term->entries
+  (fn (t) (get (artdag/term->build t 0 (list)) :acc)))
+
+(define artdag/term->dag (fn (t) (artdag/build (artdag/term->entries t))))
+
+; ---- round-trip convenience ----
+
+(define
+  artdag/mb-roundtrip
+  (fn (dag id) (artdag/term->dag (artdag/dag->term dag id))))

lib/artdag/scoreboard.json

@@ -9,9 +9,10 @@
     "cost": {"pass": 13, "fail": 0},
     "serialize": {"pass": 13, "fail": 0},
     "stats": {"pass": 12, "fail": 0},
-    "fault": {"pass": 14, "fail": 0}
+    "fault": {"pass": 14, "fail": 0},
+    "maude-optimize": {"pass": 14, "fail": 0}
   },
-  "total_pass": 158,
+  "total_pass": 172,
   "total_fail": 0,
-  "total": 158
+  "total": 172
 }

lib/artdag/scoreboard.md

@@ -14,4 +14,5 @@ _Generated by `lib/artdag/conformance.sh`_
 | serialize | 13 | 0 | 13 |
 | stats | 12 | 0 | 12 |
 | fault | 14 | 0 | 14 |
-| **Total** | **158** | **0** | **158** |
+| maude-optimize | 14 | 0 | 14 |
+| **Total** | **172** | **0** | **172** |

lib/artdag/tests/maude-optimize.sx

@@ -0,0 +1,112 @@
+; Phase 7 — rule-based optimization via maude-on-sx.
+; Bridge round-trip: dag->term->dag is the identity on canonical (content-id) form.
+
+; ---- linear chain a -> b -> c (b carries params) ----
+
+(define
+  mo-chain
+  (artdag/build
+    (list
+      (list "a" "in" (list) {:v 5})
+      (list "b" "blur" (list "a") {:radius 2})
+      (list "c" "blur" (list "b") {:radius 3}))))
+(define mo-c-id (artdag/dag-id mo-chain "c"))
+(define mo-chain-rt (artdag/mb-roundtrip mo-chain mo-c-id))
+
+(artdag-test
+  "roundtrip: sink id preserved"
+  (artdag/member? mo-c-id (keys (artdag/dag-nodes mo-chain-rt)))
+  true)
+
+(artdag-test
+  "roundtrip: node count preserved"
+  (artdag/node-count mo-chain-rt)
+  3)
+
+(artdag-test
+  "roundtrip: sink op preserved"
+  (artdag/node-op (artdag/dag-get mo-chain-rt mo-c-id))
+  "blur")
+
+(artdag-test
+  "roundtrip: sink params preserved"
+  (artdag/node-params (artdag/dag-get mo-chain-rt mo-c-id))
+  {:radius 3})
+
+(artdag-test
+  "roundtrip: full reconstructed node equals original"
+  (= (artdag/dag-get mo-chain-rt mo-c-id) (artdag/dag-get mo-chain mo-c-id))
+  true)
+
+; ---- term shape ----
+
+(define mo-c-term (artdag/dag->term mo-chain mo-c-id))
+
+(artdag-test "term: sink op is the maude operator" (mau/op mo-c-term) "blur")
+
+(artdag-test
+  "term: params recovered from meta"
+  (artdag/term-params mo-c-term)
+  {:radius 3})
+
+(artdag-test
+  "term: commutative flag recovered (false)"
+  (artdag/term-commutative mo-c-term)
+  false)
+
+(artdag-test
+  "term->entries: one entry per node"
+  (len (artdag/term->entries mo-c-term))
+  3)
+
+; ---- commutative node: order-insensitive id survives round-trip ----
+
+(define
+  mo-comm
+  (artdag/build
+    (list
+      (list "x" "src" (list) {})
+      (list "y" "noise" (list) {})
+      (list "z" "over" (list "x" "y") {} true))))
+(define mo-z-id (artdag/dag-id mo-comm "z"))
+(define mo-comm-rt (artdag/mb-roundtrip mo-comm mo-z-id))
+
+(artdag-test
+  "roundtrip comm: commutative id preserved"
+  (artdag/member? mo-z-id (keys (artdag/dag-nodes mo-comm-rt)))
+  true)
+
+(artdag-test
+  "term comm: commutative flag recovered (true)"
+  (artdag/term-commutative (artdag/dag->term mo-comm mo-z-id))
+  true)
+
+; ---- diamond: shared subgraph re-collapses to one node ----
+
+(define
+  mo-diamond
+  (artdag/build
+    (list
+      (list "a" "src" (list) {})
+      (list "b" "blur" (list "a") {:radius 1})
+      (list "c" "bright" (list "a") {:gain 2})
+      (list "d" "over" (list "b" "c") {} true))))
+(define mo-d-id (artdag/dag-id mo-diamond "d"))
+(define mo-diamond-rt (artdag/mb-roundtrip mo-diamond mo-d-id))
+
+(artdag-test
+  "roundtrip diamond: shared node not duplicated"
+  (artdag/node-count mo-diamond-rt)
+  4)
+
+(artdag-test
+  "roundtrip diamond: sink id preserved"
+  (artdag/member? mo-d-id (keys (artdag/dag-nodes mo-diamond-rt)))
+  true)
+
+(artdag-test
+  "roundtrip diamond: shared src id preserved"
+  (artdag/member?
+    (artdag/dag-id mo-diamond "a")
+    (keys (artdag/dag-nodes mo-diamond-rt)))
+  true)

plans/artdag-on-sx.md

@@ -20,8 +20,9 @@ the same SX substrates already serve the phases:
 - **Execute** (composable effects + content-addressed memo) → SX's own
   `perform`/`cek-resume` + a **persist**-backed content-addressed result cache;
   incremental recompute drops the cost of re-rendering to the dirty subgraph.
-- **Optimize** (fuse/dedup effect pipelines) → term rewriting (a later, optional
-  consumer of `maude-on-sx`'s engine — see `plans/maude-on-sx.md`).
+- **Optimize** (fuse/dedup effect pipelines) → term rewriting, the declarative
+  consumer of `maude-on-sx`'s engine — now ACTIVE as Phase 7 (lib/maude is on
+  this branch; fit proven in `lib/maude/tests/effects.sx`).
 
 End-state: a content-addressed dataflow engine in `lib/artdag/` with analyze, plan,
 incremental execute, effect-pipeline optimization, and a shared-cache federation
@@ -30,7 +31,7 @@ edges.
 
 ## Status (rolling)
 
-`bash lib/artdag/conformance.sh` → **158/158** (10 suites: dag, analyze, plan, execute, optimize, fed, cost, serialize, stats, fault)
+`bash lib/artdag/conformance.sh` → **172/172** (11 suites: dag, analyze, plan, execute, optimize, fed, cost, serialize, stats, fault, maude-optimize)
 
 Base roadmap (Phases 1–6) COMPLETE. Now extending.
 
@@ -124,8 +125,7 @@ lib/artdag/optimize.sx                  lib/artdag/federation.sx
 - [x] optimizations are content-id-preserving where semantically identical; assert
   the optimized DAG produces identical results
 - [x] `lib/artdag/tests/optimize.sx` — DCE, CSE dedup, fusion equivalence
-- [ ] (optional/later) rule-based optimization via `maude-on-sx`'s rewriting engine —
-  flag the integration point, don't block on it
+- [x] (superseded by Phase 7) integration point flagged
 
 ## Phase 6 — Federation (shared content-addressed cache)
 
@@ -136,8 +136,69 @@ lib/artdag/optimize.sx                  lib/artdag/federation.sx
 - [x] revocation/invalidation — drop a remote result if its provenance is withdrawn
 - [x] `lib/artdag/tests/fed.sx` — remote cache hit, trust gating, invalidation
 
+## Phase 7 — Rule-based optimization via maude-on-sx  (ACTIVE — start here)
+
+`lib/maude/` is now present on this branch (term rewriting modulo assoc/comm/id;
+262 tests). The fit is PROVEN — see `lib/maude/tests/effects.sx`: artdag's
+optimise passes (fusion, no-op/dead-op elim, identity elim, CSE/idempotent
+dedup) expressed as equations, where the optimised pipeline IS the normal form
+and confluence ⇒ a stable content id. Reimplement Phase-5 optimisation
+declaratively and prove it equivalent to the hand-written `optimize.sx`.
+
+- [x] `lib/artdag/maude-bridge.sx` — adapter between an effect DAG node and a
+  maude term: `(op, sorted-input-ids, params)` ⟷ `(mau/app op (args...))`.
+  Params become constant subterms; for commutative ops use a maude AC operator
+  so input order is irrelevant (mirror the content-id's order-insensitivity).
+  Round-trip `dag→term→dag` must be identity on canonical form.
+- [ ] `lib/artdag/optimize-rules.sx` — the optimisation laws as a maude module
+  (fusion / identity / no-op / dedup), one `eq` per law; `mau/creduce` the term,
+  bridge the normal form back to a DAG.
+- [ ] Equivalence: assert the maude-optimised DAG == `optimize.sx`'s output on
+  the existing fixtures (same nodes, same content ids) — the rule set must cover
+  at least the hand-written passes.
+- [ ] Confluence / CID-stability check: **consume `mau/confluent?` from
+  `lib/maude/confluence.sx`** — do NOT build your own checker. Assert the
+  optimisation rule module is confluent (`(mau/confluent? rules-module)` is
+  true) so different rewrite orders reach the same normal form and the optimised
+  pipeline's content id is stable. On failure, `mau/non-joinable-pairs` +
+  `mau/cp->str` name the offending critical pair (fix the rule set, e.g. add the
+  joining law — see the `f(a)=b,a=c` → add `f(c)=b` pattern). It is a syntactic
+  critical-pair checker (exact for free/constructor ops; AC overlaps under-
+  approximated but joined via canonical form) — that matches what this optimiser
+  needs. API also: `mau/critical-pairs`, `mau/joinable?`.
+- [ ] `lib/artdag/tests/maude-optimize.sx` — bridge round-trip, each law,
+  equivalence-with-`optimize.sx`, `(mau/confluent? rules-module)` holds.
+- [ ] (later) cost-directed choice among confluent-equivalent forms; (optional)
+  miniKanren scheduling.
+
+maude is a READ-ONLY consumed substrate (like datalog/persist) — load it, don't
+edit it. Entry points: `mau/parse-module`, `mau/creduce`/`mau/creduce->str`,
+`mau/canon`/`mau/ac-equal?`, `mau/term->maude`, `mau/app`/`mau/const`/`mau/var`
++ accessors. Load order: see `lib/maude/conformance.conf` PRELOADS.
+Gotchas (from building it): `id:` affects matching/canon only, not auto-
+reduction — write explicit identity `eq`s or read `mau/canon`; `mau/match-all`/
+`search` enumerate ALL matches (exponential on many identical AC args — keep
+rule sets small + confluent), single-step rewriting is short-circuit and fast;
+juxtaposition `__`/multi-`_` mixfix unparsed (use explicit infix ops); `.` can't
+be an op token.
+
 ## Progress log
 
+- **2026-06-07 Phase 7 — maude-bridge** (maude-optimize suite 14/14, total 172/172).
+  `lib/artdag/maude-bridge.sx`: lossless adapter between an artdag effect DAG and a
+  maude term. `artdag/dag->term dag id` walks from a sink, emitting `(mau/app op
+  input-terms ++ meta)` per node; the trailing `artdag:meta` subterm carries params
+  (a `write-to-string` token) + a commutativity flag, so no side table is needed.
+  `artdag/term->dag` synthesizes build-entries (names `mb0…`) and re-runs
+  `artdag/build`, which recomputes content-ids (name-independent) and re-collapses
+  shared subterms — so `artdag/mb-roundtrip` is the identity on canonical form:
+  sink id, op, params, and the full node survive; commutative ids stay
+  order-insensitive; a diamond's shared node de-duplicates back to one (4→4).
+  Maude entry points used: `mau/app`/`mau/const`/`mau/op`/`mau/args`/`mau/app?`.
+  `conformance.sh` now gates the maude PRELOADS + bridge load to the maude-optimize
+  suite (other suites stay maude-free). Gotcha: `write-to-string`/`read` round-trips
+  keyword dicts but may reorder keys — fine, dicts compare structurally with `=`.
+
 - **Ext: public API facade** (`lib/artdag/api.sx`, total 158/158 unchanged).
   Reference index matching the datalog/persist convention: canonical load order +
   the full public surface across all 10 modules + `artdag/version`.