Merge loops/maude into architecture: maude-on-sx — term rewriting modulo AC

Full Maude 3 functional+system core on SX (lib/maude): parser (sorts/subsorts/
overloading/mixfix), equational reduction modulo assoc/comm/id (the chisel),
conditional eqs + owise, system rules (rew + BFS search), strategy language,
META-LEVEL reflection, order-sorted least-sort, mixfix printer, end-to-end
program runner, gather right-assoc. 262 tests, 14 suites. Includes the
artdag-on-sx optimiser fit prototype (effects.sx).

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

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,36 @@ 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.
+
+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 +184,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)_