[AdaWorldAPI]

Lab only. MORK stays behind the boundary module as the oracle; nothing is wired into Quack or R2IL, and the native execution path is unchanged.

This branch carries three pieces, in commit order:

1. D-MPS-9: the MORK query_multi oracle.
2. Docs only: the Stage A gap matrix.
3. Stage B: the E1 probe, crates/egglog-r2il-probe/.

1. D-MPS-9: MORK as differential oracle

mork-pathmap-probe/src/boundary.rs: a general MORK arm, mork_rules(facts, rules).

• Input is Lance-owned plain data (OracleRule, OracleAtom, OracleTerm, OracleFacts). No crepe type enters the crate, and no upstream type leaves it.
• Output is the distinct head tuples (TupleSet, MORK's set semantics, oracle only) plus OracleCost.
• Each rule runs as its own MM2 exec.
• Before the exec, the body is parsed with Space::parse_sexpr and enumerated with Space::query_multi, counting callbacks. That times MORK's unification alone, without text decode.
  • The callback's bool is a continue flag (space.rs:1253, :1343, :1364).
  • The callback fires only after a successful unify.
• Rules wider than MORK's 63-child arity are refused before parsing (MORK_MAX_CHILDREN).

crepe-plan-probe/src/mork_api.rs: to_oracle(rule) runs admit first and returns its refusal unchanged. A constant above u32 is refused by name (ConstOutOfRange).

crepe-plan-probe/tests/mork_differential.rs (new, 7 tests):

• Six fixtures, each with MORK's set equal to the reference set, and each non-empty:
  • family;
  • family_noisy;
  • two_way;
  • star3;
  • a body constant;
  • a three-atom chain.
• MORK's callback count equals the reference derivation count over deduplicated facts.
• to_oracle refuses exactly what admit refuses.

crepe-plan-probe/examples/mork_split.rs (new): cost split, native vs MORK. It asserts answer-set equality first.

Verification:

• 47 + 59 tests pass.
• Clippy and fmt are clean.
• Four disable runs are red: constants encoded as variables, counting only Ok callbacks, to_oracle without admit, and the arity guard removed.

Cost split (n = 10,000; median of 5; Xeon @ 2.10 GHz, 4 vCPU, shared host):

arm	µs
native prepare	162
native Count(BAG) terminal	17.6
native Bindings(BAG) handle (deferred)	2.8
native: enumerate all answers	188
MORK encode + build	3,564
MORK unification only	12,289
MORK exec + text decode	23,548

The MORK rows are oracle reference costs, not gates. See the open question below on reporting out-of-fold costs.

2. Stage A gap matrix (docs only)

entries/2026-10-22-math-compiler-gap-matrix.md: an inventory of egglog → R2IL pieces against falsifiers E1–E5, under D-RFT-2.

3. Stage B: E1 end to end, probe-local (crates/egglog-r2il-probe/)

E1 is exact-integer symbolic substitution: a = 2b, b = 2c, z = 2a gives z = 8c. It is not a population measure, so there is no SUM fold, contract::Measure is unchanged, and no opcode or egglog change is added. Coordinated on EXO-50 /043.

The pipeline:

• Laws. Two probe laws, MulAssoc and ConstFold. The rule id carries the contract's set_rules::Arith domain:
  • Exact admits both;
  • Wrapping admits MulAssoc only;
  • Checked and Ieee refuse both.
• egglog, cold and bounded, public API only:
  • proofs mode;
  • (run arith 1) stepped up to fuel, with a typed Saturated / Incomplete;
  • prove-variants gives the extraction plus a proof, which egglog checks before and after simplification.
• Extraction is egglog's own. Non-target variables are (Def String :cost 1000), so the cheapest non-trivial variant is the answer.
• Lowering is straight-line R2IL scalar INT_MULT through FoldDialect, in the procs.rs pattern.
• Oracle: an independent i128 substitution over the original premises.

Results (13 tests):

• Exact: (Mul (Num 8) (Var "c")), one INT_MULT, equal to the oracle.
• Checked: three INT_MULTs. The domain changes the program.
• Missing premise: refused (UnboundVar), the oracle returns None, and egglog cannot prove z = 8c while it can prove z = 4b.
• Overflow counterexamples refuse in both domains; the boundary passes.
• A Wrapping term is not lowered onto checked arithmetic.
• Extraction is deterministic, and bounded fuel reports Incomplete.
• A nine-hop logical traceroute.

Six disable runs, 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. The egglog phase is timed in Compiled::timings.egglog but deliberately not printed.

Open

• Operator ruling needed: may cold, out-of-fold costs (the egglog compile, the MORK oracle) be reported? CLAUDE.md forbids millisecond results anywhere. The MORK rows above and the egglog phase are of that kind.
• MORK's add_sexpr, remove_sexpr, dump_sexpr and transform_multi_multi verbs; the memory/sharing measurement; allocation counts (D-MPS-4).
• E2–E5 beyond what E1 exercises. Measure::Scale stays gated on a real population-measure consumer, in a separate PR.

Board:

• entries/2026-10-22-d-mps-9-mork-oracle.md
• entries/2026-10-22-math-compiler-gap-matrix.md
• entries/2026-10-22-math-compiler-stage-b-e1.md
• STATUS_BOARD D-MPS-9, plan §7d, AGENT_LOG

🤖 Generated with Claude Code

https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg

[coderabbitai]

Important

• 🔍 Trigger review

This repository does not receive automatic reviews because it has fewer than 10 stars.

⚙️ Run configuration

• Configuration used: Organization UI
• Review profile: CHILL
• Plan: Advanced
• Run ID: 02ae2fd6-3c96-417e-bf2a-98261f83f888

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Warning

Billing warning: we have not been able to collect payment for this subscription for more than 72 hours. Please update the payment method or pay any pending invoices in Billing to avoid service interruption.

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-22T05:39:02.106994Z	bd62d55	Draft marked ready

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: bd62d55f37

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".