maude: load-order.txt single-source manifest (driver-level facade; .sx facade proven infeasible)

load is an epoch command not an evaluator symbol, so an .sx file can't wrap the
load list. Extract the dependency-ordered file list to lib/maude/load-order.txt;
conformance.conf reads it via mapfile. 274/274 green. lib/artdag can source the
same file to drop its duplicated load lines.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

lib/maude/conformance.conf

@@ -3,24 +3,10 @@
 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
-)
+# Load order is the single source of truth in load-order.txt (also consumable
+# by other drivers, e.g. lib/artdag). Sourced after the driver cd's to repo
+# top-level, so the relative path resolves; #-comments and blanks are stripped.
+mapfile -t PRELOADS < <(grep -vE '^[[:space:]]*(#|$)' lib/maude/load-order.txt)
 
 SUITES=(
   "parse:lib/maude/tests/parse.sx:(mau-parse-tests-run!)"

lib/maude/load-order.txt

@@ -0,0 +1,23 @@
+# lib/maude load order — single source of truth for the dependency-ordered
+# file list needed to load the maude engine (parser + rewriting + confluence +
+# reflection). Sourced by lib/maude/conformance.conf; other drivers (e.g.
+# lib/artdag, which today hardcodes its own copy of these load lines) can read
+# the same list instead of duplicating it, so a file rename here is a one-line
+# change. Repo-root-relative paths, one per line; blank lines and #-comments
+# are ignored by readers.
+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

plans/maude-on-sx.md

@@ -130,18 +130,81 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
   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).
-- [ ] Extract normal-form-by-equations infrastructure.
-- [ ] Extract strategy combinators.
-- [ ] Wait for second consumer before extracting.
+### Phase 8 — `lib/guest/rewriting/` extraction — DESIGN PROPOSAL (gate satisfied; thin-kernel cut REJECTED on evidence)
+- [x] Wait for second consumer before extracting. **SATISFIED** — `lib/artdag`
+  is a live, saturated consumer (Phase-7 maude optimiser: `optimize-rules.sx`
+  parses a `fmod`, reduces, and gates on `mau/confluent?`). It is the only
+  external consumer; zero Blockers were filed against `lib/maude`, so the API
+  held under real use.
+- [~] Extract equational matching engine — **DO NOT, as specified.** See below.
+- [~] Extract normal-form-by-equations infrastructure — folds into the facade.
+- [~] Extract strategy combinators — **DO NOT.** Zero external consumers.
 
-**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).
+**Status: gate met, mechanical extraction NOT recommended.** Before cutting,
+the consumer was measured. The result overturns the pre-registered plan.
+
+**What the plan assumed:** the reusable core is `matching.sx` (AC matching +
+canon) + `fire.sx` (short-circuit firing), with `strategy.sx` third.
+
+**What the second consumer actually imports** (measured across `lib/artdag/*.sx`):
+
+| Layer | Symbols artdag uses | In planned kernel? |
+|-------|--------------------|--------------------|
+| `term.sx`        | `mau/app` `mau/app?` `mau/const` `mau/op` `mau/args` | yes |
+| `parser.sx`      | `mau/parse-module` (artdag writes rules as `fmod … endfm` text) | **no — left in surface** |
+| `conditional.sx` | `mau/creduce` `mau/creduce-term` `mau/creduce->str` `mau/ccanon` | partial |
+| `confluence.sx`  | `mau/confluent?` `mau/non-joinable-pairs` `mau/cp->str` | **no — added post-plan** |
+| `matching.sx` / `fire.sx` / `strategy.sx` | **none directly** | the whole planned kernel |
+
+So the consumer reuses a **vertical** (term → parser → conditional → confluence),
+not the horizontal AC kernel the plan named. It touches **none** of
+matching/fire/strategy directly, and `strategy.sx` has **no consumer at all**.
+Extracting matching+fire+strategy would produce a "reusable kernel" with nobody
+reusing it — extraction-for-its-own-sake, exactly what the gate existed to prevent.
+
+**Why the vertical can't be cleanly thinned into a kernel:** the kernel
+candidates' only coupling to the front-end is 7 parser symbols —
+list utils `mau/take` `mau/drop` `mau/append2` (relocatable, theory-agnostic) and
+module accessors `mau/module-eqs` `mau/module-ops` `mau/module-rules`
+`mau/parse-term-in` (the eqs/ops/rules feed + in-signature term parsing). But the
+real consumer *wants* the `fmod` parser — it authors rules as Maude text. A thin
+term-rewriting kernel that excludes the parser does not serve it; a "kernel" that
+includes the parser is just `lib/maude` renamed.
+
+**Recommended move (cheap, low-risk, real) — a driver-level manifest, not a
+relocation and not an `.sx` re-export** (the `.sx` facade was tried and proven
+infeasible; see FINDING below). The consumed surface is `mau/parse-module`,
+`mau/creduce*`/`mau/ccanon`, `mau/confluent?`/`mau/non-joinable-pairs`/`mau/cp->str`,
+term ctors/accessors.
+
+**FINDING (2026-07, smoke-tested): an `.sx`-file facade is architecturally
+impossible.** `load` is an *epoch-protocol command*, not an evaluator symbol —
+`(load "…")` forms **inside** a loaded `.sx` file error with "Undefined symbol:
+load" (verified: a would-be `api.sx` of `(load …)` lines fails on every line).
+The nested-load seen in `common-lisp/tests/runtime.sx` works only because that
+harness feeds each form as a *command*, not because `load` is callable from
+evaluated code. So the load list is inherently a **driver-level** concern
+(shell / `conformance.conf`), and no `.sx` file can wrap "nine loads into one".
+
+**BUILT INSTEAD — `lib/maude/load-order.txt`** (driver-level manifest, the
+working form of the facade): the dependency-ordered file list as the single
+source of truth. `lib/maude/conformance.conf` now reads it
+(`mapfile -t PRELOADS < <(grep -vE '^\s*(#|$)' lib/maude/load-order.txt)`) —
+proven by the 274 suite staying green. A file rename is now a one-line change,
+and `lib/artdag`'s driver can `mapfile` the same file to drop its hardcoded copy
+of these load lines (artdag-side change, its scope — a documented follow-up, not
+done here). This delivers the load-list DRY + file-rename freedom that the
+`.sx` facade could not.
+
+**Symbol-contract (optional, not built):** a pure-manifest `mau/api-symbols`
+list (the ~25 public symbols, no `load` forms so it loads fine) + an `api` test
+exercising each end-to-end would pin the *symbol* surface as a tripwire. Modest;
+skipped as gilding — the file-level manifest is the higher-value half.
+
+**Defer the physical `lib/guest/rewriting/` split** until a *third* consumer
+diverges from artdag — the boundary should be drawn by two real shapes, not one
+plus a guess. The dependency DAG and 7-symbol coupling set above make that cut a
+1-session job when justified.
 
 ### SATURATION (post-roadmap)