D-MPS-9 MORK query_multi oracle + math-compiler Stage A matrix and Stage B (E1) probe

.claude/board/AGENT_LOG.md

@@ -1,3 +1,14 @@
+## 2026-10-22 — Stage B E1 probe (Opus spec, Sonnet draft)
+
+- One Sonnet drafter from a written spec (no cargo). The main thread replaced its hand-written variable expansion (a second rewriter outside egglog) with an egglog constructor cost, fixed a test that pinned egglog's cost tie-break, withheld the out-of-fold egglog timing pending an operator ruling, compiled, and ran 6 disable runs (all red).
+- Result: `entries/2026-10-22-math-compiler-stage-b-e1.md`. Written by the orchestrating main thread only.
+
+## 2026-10-22 — D-MPS-9 `query_multi` oracle (Haiku map, Opus spec, Sonnet draft)
+
+- Two Haiku `substrate-mapper` runs: MORK `space.rs`/`expr` (PARTIAL: the read stopped at line 1076/1094; `query_multi`, `Bindings`, `ExprEnv` read on the main thread) and the probe boundary plus fixtures (complete).
+- One Sonnet drafter from a written spec (no cargo). The main thread compiled, ran the disable runs (3, all red), fixed one clippy lint and one measurement gap (the deferred `Bindings` handle had no timed enumeration).
+- Result: `entries/2026-10-22-d-mps-9-mork-oracle.md`. Written by the orchestrating main thread only.
+
 ## 2026-10-21 — 5+3 council: the tuple is a zero-copy violation (blast radius)
 
 - Five savants: prior-art-savant, iron-rule-savant, runtime-archaeologist (code truth), cascade-impact-savant (blast radius, Opus), creative-explorer-savant. Three reviewers on draft v2 only: overclaim-auditor (2 BLOCK, wording/grading, fixed), dilution-collapse-sentinel (0 BLOCK, 2 collapses restored), firewall-warden (0 BLOCK).

.claude/board/STATUS_BOARD.md

@@ -41,7 +41,7 @@ Plan `mork-pathmap-schnellverschluss-v1.md`; entry `entries/2026-10-19-mork-path
 | D-MPS-5 | upstream MORK: leapfrog join generic over a cursor provider + reindex hook | PROPOSAL | MORK corpus unchanged on `PathMap<()>` |
 | D-MPS-6 | Lance-owned PathMap-trait cursor over a sealed `RelationOrder` | BLOCKED (`RelationOrder` not built) | no copy, or the copy stated |
 | D-MPS-7 | licence: no MORK source vendored until a licence is declared (#148 unmerged) | OPEN (intent stated, clearance incomplete): MIT intent stated by the maintainer (Adam-Vandervorst, trueagi-io/MORK issue #2, 2025-05-21: "Yes! It's now under MIT."); formal repository-level clearance incomplete: PR #148 "Add MIT License and Cargo manifest metadata" proposed 2026-08-20, still open when observed 2026-10-19. PathMap already advertises MIT Scope (operator, 2026-10-20): the gate covers using MORK code — vendoring, redistributing or translating its source. An independent implementation, written from documented behaviour and checked against our own tests and oracles, is not blocked by it; "openmork" was named as a further option (not located by this session, URL needed). The Schnellverschluss is the design answer to this gate (operator, 2026-10-20: "That's why we implemented it with Schnellverschluss"): MORK is fetched, never vendored; nothing outside `boundary.rs` names it; deleting it is one `Index` variant, two helpers and one `Cargo.toml` line (§3 removal test); and the native arm (D-MPS-8) answers the same join without MORK code. | probe vendors nothing; vendoring waits for #148 or an equivalent LICENSE file in MORK |
-| D-MPS-9 | MORK `Space` verbs (`add_sexpr`/`remove_sexpr`/`query_multi`/`transform_multi_multi`/`dump_sexpr`) as the standard API, answered by our folding; MORK as the differential oracle behind the Schnellverschluss; first scope fixed-arity shared-variable patterns, other shapes refused by name (`mork-pathmap-schnellverschluss-v1.md` §7c) | Queued (lab; DECISION 2026-10-20) | answers == MORK (sets) and datafrog (bags) per verb and fixture; disable: silently flatten a nested pattern |
+| D-MPS-9 | MORK `Space` verbs (`add_sexpr`/`remove_sexpr`/`query_multi`/`transform_multi_multi`/`dump_sexpr`) as the standard API, answered by our folding; MORK as the differential oracle behind the Schnellverschluss; first scope fixed-arity shared-variable patterns, other shapes refused by name (`mork-pathmap-schnellverschluss-v1.md` §7c) | MEASURED (lab) for `query_multi` only, 2026-10-22; other verbs Queued | `entries/2026-10-22-d-mps-9-mork-oracle.md`: 6 fixtures MORK set == reference, match count == reference over distinct facts, 3 disable runs red; flatten-nested disable not expressible (native has no nested facts) |
 
 ## Plan links for #1601–#1617 (2026-10-20)
 

.claude/board/entries/2026-10-22-d-mps-9-mork-oracle.md

@@ -0,0 +1,41 @@
+# 2026-10-22 — D-MPS-9: MORK as the differential oracle for every admitted `query_multi`
+
+**Status:** MEASURED (lab; mork-pathmap-probe, crepe-plan-probe). Not admitted, not wired into Quack or R2IL.
+
+## What changed
+
+- `boundary.rs` gains a general MORK arm, `mork_rules(facts, rules)`. It takes Lance-owned plain data (`OracleRule`, `OracleAtom`, `OracleTerm`, `OracleFacts`) and returns the distinct head tuples (`TupleSet`, a set, oracle only) plus `OracleCost`. No crepe type enters the crate; nothing upstream-typed leaves it.
+- Each rule runs as its own MM2 `exec`, so one rule's output never feeds another. Before the `exec`, the body is parsed with `Space::parse_sexpr` and enumerated with `Space::query_multi`, counting the effect callbacks. That times MORK's unification alone, with no answer decode. The callback's `bool` is a continue flag (`space.rs:1253`, `:1343`, `:1364`); it is called only after a successful unify.
+- `mork_api::to_oracle(rule)` runs `admit` first and returns its refusal unchanged; constants above `u32` are refused (`ConstOutOfRange`).
+
+## Tests (`crepe-plan-probe/tests/mork_differential.rs`, 7; `mork-pathmap-probe/tests/differential.rs` +1)
+
+- Six fixtures, MORK set == reference set, each non-empty: `family` (two rules, head constant, repeated relation, a duplicated fact), `family_noisy` (== `family`'s set), `two_way`, `star3`, a body constant, a three-atom chain (acyclic; the native star refuses it, MORK answers it).
+- MORK's callback count == the reference's derivation count over DEDUPLICATED facts, and the bag count over raw facts exceeds it on `family` (the duplicate `Allowed(2)`), so the dedup is not a no-op.
+- `to_oracle` refuses exactly what `admit` refuses (Tri `Cyclic`, Loop `RepeatedVarInAtom`; Chain admitted).
+- The general arm agrees with the fixed `Q(x,y,z)` query.
+- Disable runs, each red then restored: constants encoded as variables (5 tests red); counting only `Ok` callbacks (match-count test red); `to_oracle` skipping `admit` (refusal test red).
+
+## Cost split (`examples/mork_split.rs`, release, median of 5, n = 10 000, 12 500 input rows, 10 000 answers; Xeon @ 2.10 GHz, 4 vCPU, shared host)
+
+| arm | µs | ns / input row |
+|---|---|---|
+| native prepare (layout) | 162 | 13.0 |
+| native execute, `Count(BAG)` terminal | 17.6 | 1.4 |
+| native execute, `Bindings(BAG)` (deferred handle) | 2.8 | 0.2 |
+| native: enumerate all 10 000 answers (no allocation per answer) | 188 | 15.0 |
+| MORK encode + build | 3 564 | 285 |
+| MORK unification only (`query_multi`) | 12 289 | 983 |
+| MORK exec + text decode | 23 548 | 1 884 |
+
+- The `Bindings` outcome's `execute` does not read answers; enumeration is timed separately. Reading the answers costs 10× the count terminal here.
+- MORK numbers are oracle reference costs, not gates. MORK's unification alone is about half its exec + decode time; the earlier §6 MORK query column (exec + dump + parse) is therefore roughly 2× MORK's join.
+
+## Not covered (OPEN)
+
+- `add_sexpr` / `remove_sexpr` / `dump_sexpr` / `transform_multi_multi` façade verbs: not built. Removal is a full re-prepare on the native side.
+- Binding and witness validation are still inside `prepare`; not split out.
+- The §7c disable "silently flatten a nested pattern" is not run: the native side has no representation for nested facts, so the flattened arm cannot be expressed. The nested refusal test stands.
+- Structural sharing and memory across versions: not measured. Allocations: still blocked (MORK installs PathMap's jemalloc, D-MPS-4).
+
+**Correction (chat, 2026-10-22):** PathMap's default build uses `slim_ptrs` (`TrieNodeODRc` = `SlimNodePtr` + allocator, `trie_node.rs:3020`); `Arc<dyn TrieNode>` is only the non-`slim_ptrs` build (`:2721`/`:2726`).

.claude/board/entries/2026-10-22-math-compiler-gap-matrix.md

@@ -0,0 +1,27 @@
+# 2026-10-22 — Proof-carrying math compiler: Stage A gap matrix (egglog → R2IL)
+
+**Status:** OPEN. Inventory only; no code. Read at `origin/main` `3b723df1`, egglog fork `main` `9c8396d`. Falsifiers E1–E5 are the ones registered in `.arxiv/2304.04332_egglog_equality_saturation_datalog_excerpt.md:23-28` (P6/P12 in `.arxiv/2026-10_qr256_gaussian_egglog_rotation_falsifier_paths.md`). D-RFT-2 (`d-rft-relalg-thought-git-frontier-v1.md`) is the owning plan; no new plan.
+
+| Piece | State | Where | Note |
+|---|---|---|---|
+| egglog equality saturation + proofs | EXISTS (fork) | AdaWorldAPI/egglog `prove`, `prove-variants` (#1, #2), `ProofStore`/`ProofId` | no lance-graph crate depends on egglog today (no Cargo.toml names it) |
+| independent proof check callable from outside egglog | MISSING | `ProofStore::check_proof` is `pub(crate)` | demonstrated gap for E4; the only fork change this slice needs |
+| bounded saturation | EXISTS | egglog `run` with iteration limit; no node/time limit exposed as a typed outcome | E5 needs a typed "incomplete" result, not an error |
+| typed single-table measure IR + guarded rules | EXISTS | contract `set_rules`: `Measure {Const, Count, Sum, CountRows, Opaque, Add, Sub}`, `Semantics {universe, arith, truth, sums, population}`, 8 rules with per-rule `Refusal` | the guard vocabulary (Exact/Wrapping/Checked/Ieee, TwoValued/ThreeValued, Distinct/Bag, Plain/Sym) already covers E3's OR/XOR-free half |
+| multiplication / scale-by-constant in the measure IR | MISSING | `Measure` has no `Mul`/`Scale` | E1 (`z = 8c`) cannot be written in the contract IR today |
+| Boolean OR vs GF(2) XOR as separate laws | PARTIAL | R2IL has `INT_OR` and `INT_XOR` as distinct ops; `set_algebra` is Boolean; no XOR set law | E3's OR/XOR arm needs an egglog sort split, not a contract change |
+| relalg lowering to R2IL / mask-risc | EXISTS | `relalg::lower::run`, `run_with_program`, `run_as_written`; `program::run_program` (`let` planes, U2) | lowers `Rel` + `Measure {Count, Sum, Min, Max, Keep}` |
+| scalar arithmetic in R2IL | EXISTS | `INT_ADD`, `INT_SUB`, `INT_MULT`, `INT_S_DIV`: scalar × scalar, checked `i64` | |
+| lane arithmetic in R2IL | MISSING (by design) | `FoldError::LaneVersusLane` | a lane-scale `8 * c[i]` is not expressible; `SUM(8·c) = 8·SUM(c)` is (scalar after the fold) |
+| reusable parameterized procedures | EXISTS | `r2il::procs` (`filter_lt`, `count`, `sum`, `group_sum`, `avg_parts`, …) | the compile target for B |
+| group counts keyed by a slot | EXISTS | mask-risc `Terminal::GroupReduce { key: GroupKey, fold }` (COUNT/MIN/…), `GroupSumI32`, `GroupPowerSumsI32` | Example B's `GROUP_COUNT(R, y)` |
+| dot product over a shared domain (`Σ_y r[y]·s[y]`) | MISSING | no Terminal with a dot/product doc line | Example B's last step is a scalar loop today (`join.rs` `bag_count`) |
+| co-addressed domain for B | EXISTS (lab) | `mork-pathmap-probe::join::JoinDomain`, `JoinTable` (D-MPS-8, not admitted) | ADMISSION B review still owed |
+| shared `let` planes (Example C) | EXISTS | contract `set_program` + `relalg::program` (U2 measured), `crepe-plan-probe::cse` (U3) | no egglog needed for C's baseline |
+| Boolean composition (Example D) | EXISTS (lab) | `rmap::Tile`, `tile_gemm`, DR256 (#1666), `dir-rmap-probe` (#1685) | |
+| Thought-Git replay receipt | EXISTS (lab) | `thought-git-probe::receipt` (generations, ABA guard) | no substitution/proof link; grep `substitut`/`egglog` in the crate: 0 hits |
+| ClassView method DAG | EXISTS | contract `ClassView::compute_dag` (`class_view.rs:1403`), `ComputeEdge` | consumer for compiled-pattern identity, later |
+| logical traceroute | PARTIAL | `set_rules::Trace { steps, refusals, budget_exhausted }` | rule-level only; no proof link, no binding requirements |
+| three cache identities (law / pattern / register) | MISSING as types | witnesses exist separately (`RelationView.generation`, receipts) | |
+
+**Smallest seam for Stage B (E1):** one lab crate that (1) encodes an exact-integer term language in egglog, (2) proves `z = 8c` from the premises with `prove`/`prove-variants`, (3) checks the proof with a newly public egglog checker, (4) extracts by a declared cost, (5) lowers to existing R2IL scalar ops over a `SUM` fold, (6) runs it on mask-risc, (7) compares with an exact oracle, (8) prints the traceroute. Open choice: whether the term language lives in the probe or `Measure` gains a guarded `Scale` in the contract (contract owner).

.claude/board/entries/2026-10-22-math-compiler-stage-b-e1.md

@@ -0,0 +1,48 @@
+# 2026-10-22 — Proof-carrying math compiler: Stage B, E1 end to end (probe-local)
+
+**Status:** MEASURED (lab). Crate `crates/egglog-r2il-probe/`, own workspace root. egglog = AdaWorldAPI/egglog `main` (public API only, unmodified). Coordination: EXO-50 /043. Continues `entries/2026-10-22-math-compiler-gap-matrix.md`; falsifier E1 from `.arxiv/2304.04332_egglog_equality_saturation_datalog_excerpt.md`; D-RFT-2 owns the plan.
+
+**Shape (operator decision):** E1 is exact-integer symbolic substitution, `a = 2b, b = 2c, z = 2a ⇒ z = 8c`. It is not a population measure, so there is no SUM fold, no lane and no mask, and `contract::Measure` is unchanged. This supersedes the Stage A seam's "over a SUM fold" step.
+
+| Hop | What runs | Owner |
+|---|---|---|
+| law admission | two probe laws, `MulAssoc` and `ConstFold`; the rule id carries the contract's `set_rules::Arith` domain. Exact admits both; Wrapping admits only `MulAssoc`; Checked and Ieee admit neither | probe (`laws.rs`) |
+| saturation | egglog proofs mode, `(run arith 1)` stepped up to `fuel`, `Saturated` / `Incomplete` read from the step's own iteration report | egglog, cold |
+| extraction | egglog's own: `prove-variants` on the goal, cheapest first under the default AST-size cost, non-target variables as `(Def String :cost 1000)`; the answer is the cheapest variant other than the goal's own name | egglog |
+| proof | the variant's proof from `prove-variants`, checked by egglog's `check_proof` before and after simplification (`src/proofs/proof_extraction.rs:126-139`) | egglog |
+| lowering | straight-line R2IL scalar calls (`push`, `INT_MULT`) through `FoldDialect` over empty planes, the `procs.rs` pattern; no new opcode | existing R2IL |
+| oracle | i128 substitution over the original premises, no shared code | probe (`oracle.rs`) |
+
+**Results (13 tests, release):**
+- Exact: `(Mul (Num 8) (Var "c"))`, one `INT_MULT`, agreeing with the oracle for c ∈ {0, ±1, 7, -123456, i64::MAX/8, i64::MIN/8}.
+- Checked: both laws are refused and the program is three `INT_MULT`s. The domain changes the program.
+- Missing premise (`b = 2c` dropped):
+  - no variant contains `(Num 8)` and the result is not closed;
+  - lowering refuses `UnboundVar` (`a` or `b`; which one is egglog's cost tie-break, both cost 1002);
+  - the oracle returns None;
+  - egglog's `prove` of `z = 8c` fails, while the paired claim `z = 4·b` proves.
+- Overflow counterexamples (c = i64::MAX/8 + 1, i64::MIN/8 − 1, i64::MAX): `Overflow` in both Exact and Checked, and the oracle's value lies outside i64. The boundary i64::MAX/8 passes.
+- Wrapping: lowering refuses, because R2IL scalar arithmetic is checked, not wrapping.
+- Determinism: three fresh e-graphs give an identical extraction, variant list and call list.
+- Bounded fuel: the six-link chain is `Incomplete` at fuel 1 and `Saturated` at fuel 16.
+- Traceroute: the hops are Premises, Laws, Saturation, Extracted, Proof, R2IL, Value, Oracle, Verdict.
+
+**Disable runs (6, all red):**
+- Checked admits `MulAssoc`;
+- `Def` without its cost;
+- Wrapping is lowered;
+- `Overflow` is mapped away;
+- the goal's own name is accepted as the answer;
+- every step is read as saturated.
+
+**Cost:** encode 2 µs; lower + execute 5 µs (median of 5, release). The egglog phase (saturation + `prove-variants`) is timed in `Compiled::timings.egglog` but not printed or reported here. It is above the workspace's microsecond budget, and whether cold, out-of-fold compile costs may be reported is an open operator decision (CLAUDE.md "no millisecond results").
+
+**Corrections to Stage A:**
+- "Independent proof check MISSING" overstated the gap. egglog already checks every proof it returns. What is missing is a check callable from outside egglog on a proof object. The i128 oracle covers answer correctness independently.
+- No egglog change was needed.
+
+OPEN:
+- the ruling on reporting cold-compile cost;
+- E2–E5 beyond what E1 exercises;
+- a lowering target for wrapping arithmetic (none exists; by design?);
+- `Measure::Scale` stays gated on a real population-measure consumer in a separate PR.

.claude/board/entries/README.md

@@ -25,10 +25,13 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately
 opposite directions; the stranding this convention prevents shows up in
 exactly one of them, never both.
 
-425 entries, 2026-08-06 .. 2026-10-21.
+428 entries, 2026-08-06 .. 2026-10-22.
 
 | date | entry id | finding | file |
 |---|---|---|---|
+| 2026-10-22 | `math-compiler-stage-b-e1` |  | [2026-10-22-math-compiler-stage-b-e1.md](2026-10-22-math-compiler-stage-b-e1.md) |
+| 2026-10-22 | `math-compiler-gap-matrix` |  | [2026-10-22-math-compiler-gap-matrix.md](2026-10-22-math-compiler-gap-matrix.md) |
+| 2026-10-22 | `D-MPS-9` |  | [2026-10-22-d-mps-9-mork-oracle.md](2026-10-22-d-mps-9-mork-oracle.md) |
 | 2026-10-21 | `zero-copy-join-index-map` |  | [2026-10-21-zero-copy-join-index-map.md](2026-10-21-zero-copy-join-index-map.md) |
 | 2026-10-21 | `D-RU-4` |  | [2026-10-21-u4-coaddressed-join.md](2026-10-21-u4-coaddressed-join.md) |
 | 2026-10-21 | `D-RU-3` |  | [2026-10-21-u3-cross-rule-cse.md](2026-10-21-u3-cross-rule-cse.md) |

.claude/plans/mork-pathmap-schnellverschluss-v1.md

@@ -192,6 +192,10 @@ Neo4j loaders, symbol and tree backup/restore and the parsers are out of scope.
 
 **Falsifier:** for every verb and fixture, the façade's answer equals MORK's through `boundary.rs` (as sets, since MORK stores sets) and datafrog's (as bags where multiplicity matters); a refused shape is refused by name on both arms. Disable: let the façade answer a nested pattern by flattening it silently; the oracle must then disagree.
 
+## 7d. D-MPS-9 `query_multi`: measured (2026-10-22)
+
+`boundary::mork_rules` runs any admitted rule set through MORK (set answers, plus `Space::query_multi` unification timed alone); `crepe-plan-probe/tests/mork_differential.rs` compares six fixtures with the reference. Results, costs and the open verbs: `entries/2026-10-22-d-mps-9-mork-oracle.md`. The other §7c verbs stay Queued.
+
 ## 8. Deliverables
 
 | D-id | Item | Status | Gate / evidence |