maude: artdag-on-sx fit prototype — optimise passes as equations (8 tests, 262 total)

lib/maude/tests/effects.sx — proves artdag's effect-pipeline optimisations
(fusion, no-op/dead-op elim, identity elim, CSE/idempotent dedup) are
equational rewriting: the optimised pipeline is the normal form, confluence
gives a stable content id. The 'second consumer' spike for a maude-driven
optimiser in lib/artdag. Surfaced faithfulness note: id: affects matching/canon
not auto-reduction.

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

lib/maude/conformance.conf

@@ -35,4 +35,5 @@ SUITES=(
   "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/scoreboard.json

@@ -1,8 +1,8 @@
 {
   "lang": "maude",
-  "total_passed": 254,
+  "total_passed": 262,
   "total_failed": 0,
-  "total": 254,
+  "total": 262,
   "suites": [
     {"name":"parse","passed":65,"failed":0,"total":65},
     {"name":"reduce","passed":26,"failed":0,"total":26},
@@ -16,7 +16,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":"run","passed":10,"failed":0,"total":10},
+    {"name":"effects","passed":8,"failed":0,"total":8}
   ],
-  "generated": "2026-06-07T15:51:45+00:00"
+  "generated": "2026-06-07T19:38:27+00:00"
 }

lib/maude/scoreboard.md

@@ -1,6 +1,6 @@
 # maude scoreboard
 
-**254 / 254 passing** (0 failure(s)).
+**262 / 262 passing** (0 failure(s)).
 
 | Suite | Passed | Total | Status |
 |-------|--------|-------|--------|
@@ -17,3 +17,4 @@
 | meta | 18 | 18 | ok |
 | pretty | 11 | 11 | ok |
 | run | 10 | 10 | ok |
+| effects | 8 | 8 | ok |

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

plans/maude-on-sx.md

@@ -153,7 +153,16 @@ 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). Pacing down to hardening. Possible niche future work: membership
+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.
+
+Pacing down to hardening. Possible niche future work: membership
 axioms (`mb`/`cmb`), critical-pair / confluence checking, meta-search, full
 mixfix (multi-`_` ops, juxtaposition `__`).