From 3432a72510c7c7f2a3e495772562169b629c5939 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 20:07:34 +0000 Subject: [PATCH] artdag: maude-bridge dag<->term adapter + 14 round-trip tests Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/artdag/conformance.sh | 24 +++++- lib/artdag/maude-bridge.sx | 118 +++++++++++++++++++++++++++++ lib/artdag/scoreboard.json | 7 +- lib/artdag/scoreboard.md | 3 +- lib/artdag/tests/maude-optimize.sx | 112 +++++++++++++++++++++++++++ plans/artdag-on-sx.md | 19 ++++- 6 files changed, 276 insertions(+), 7 deletions(-) create mode 100644 lib/artdag/maude-bridge.sx create mode 100644 lib/artdag/tests/maude-optimize.sx diff --git a/lib/artdag/conformance.sh b/lib/artdag/conformance.sh index f71d193a..0d2924c6 100755 --- a/lib/artdag/conformance.sh +++ b/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)") diff --git a/lib/artdag/maude-bridge.sx b/lib/artdag/maude-bridge.sx new file mode 100644 index 00000000..b9dfdc39 --- /dev/null +++ b/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)))) diff --git a/lib/artdag/scoreboard.json b/lib/artdag/scoreboard.json index 52d1d93b..ce9ab602 100644 --- a/lib/artdag/scoreboard.json +++ b/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 } diff --git a/lib/artdag/scoreboard.md b/lib/artdag/scoreboard.md index ea91478b..14a9652f 100644 --- a/lib/artdag/scoreboard.md +++ b/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** | diff --git a/lib/artdag/tests/maude-optimize.sx b/lib/artdag/tests/maude-optimize.sx new file mode 100644 index 00000000..2f699150 --- /dev/null +++ b/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) diff --git a/plans/artdag-on-sx.md b/plans/artdag-on-sx.md index 7264266a..bfee934e 100644 --- a/plans/artdag-on-sx.md +++ b/plans/artdag-on-sx.md @@ -31,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. @@ -145,7 +145,7 @@ 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`. -- [ ] `lib/artdag/maude-bridge.sx` — adapter between an effect DAG node and a +- [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). @@ -179,6 +179,21 @@ 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`.