maude: Phase 8 design proposal — gate met, thin-kernel cut rejected on consumer evidence (facade recommended)

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

plans/maude-on-sx.md

@@ -130,18 +130,63 @@ 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 public API facade, not a relocation:**
+add `lib/maude/api.sx` re-exporting exactly the ~12 consumed symbols as the
+supported surface (`mau/parse-module`, `mau/creduce*`/`mau/ccanon`,
+`mau/confluent?`/`mau/non-joinable-pairs`/`mau/cp->str`, term ctors/accessors).
+artdag imports the facade instead of nine `load "lib/maude/<internal>.sx"` lines;
+the internal file layout becomes free to change without breaking the consumer.
+This delivers the *encapsulation* value of extraction (a named, stable boundary)
+without moving files across three trees (`lib/guest/` + `lib/maude/` +
+`lib/artdag/`) or risking the two green suites (maude 274, artdag 225).
+
+**Defer the physical `lib/guest/rewriting/` split** until a *third* consumer
+appears whose needs actually diverge from artdag's — at that point the boundary
+will be drawn by two real shapes, not one plus a guess. The data dependency DAG
+and the 7-symbol coupling set above are recorded so that cut is a 1-session job
+when justified. **Sole remaining action if desired: the `api.sx` facade (in
+scope: `lib/maude/**` only); coordinate artdag's import-side change separately.**
 
 ### SATURATION (post-roadmap)