|
| 1 | +# 2026-10-22 — Proof-carrying math compiler: Stage B, E1 end to end (probe-local) |
| 2 | + |
| 3 | +**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. |
| 4 | + |
| 5 | +**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. |
| 6 | + |
| 7 | +| Hop | What runs | Owner | |
| 8 | +|---|---|---| |
| 9 | +| 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`) | |
| 10 | +| saturation | egglog proofs mode, `(run arith 1)` stepped up to `fuel`, `Saturated` / `Incomplete` read from the step's own iteration report | egglog, cold | |
| 11 | +| 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 | |
| 12 | +| 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 | |
| 13 | +| lowering | straight-line R2IL scalar calls (`push`, `INT_MULT`) through `FoldDialect` over empty planes, the `procs.rs` pattern; no new opcode | existing R2IL | |
| 14 | +| oracle | i128 substitution over the original premises, no shared code | probe (`oracle.rs`) | |
| 15 | + |
| 16 | +**Results (13 tests, release):** |
| 17 | +- 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}. |
| 18 | +- Checked: both laws are refused and the program is three `INT_MULT`s. The domain changes the program. |
| 19 | +- Missing premise (`b = 2c` dropped): |
| 20 | + - no variant contains `(Num 8)` and the result is not closed; |
| 21 | + - lowering refuses `UnboundVar` (`a` or `b`; which one is egglog's cost tie-break, both cost 1002); |
| 22 | + - the oracle returns None; |
| 23 | + - egglog's `prove` of `z = 8c` fails, while the paired claim `z = 4·b` proves. |
| 24 | +- 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. |
| 25 | +- Wrapping: lowering refuses, because R2IL scalar arithmetic is checked, not wrapping. |
| 26 | +- Determinism: three fresh e-graphs give an identical extraction, variant list and call list. |
| 27 | +- Bounded fuel: the six-link chain is `Incomplete` at fuel 1 and `Saturated` at fuel 16. |
| 28 | +- Traceroute: the hops are Premises, Laws, Saturation, Extracted, Proof, R2IL, Value, Oracle, Verdict. |
| 29 | + |
| 30 | +**Disable runs (6, all red):** |
| 31 | +- Checked admits `MulAssoc`; |
| 32 | +- `Def` without its cost; |
| 33 | +- Wrapping is lowered; |
| 34 | +- `Overflow` is mapped away; |
| 35 | +- the goal's own name is accepted as the answer; |
| 36 | +- every step is read as saturated. |
| 37 | + |
| 38 | +**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"). |
| 39 | + |
| 40 | +**Corrections to Stage A:** |
| 41 | +- "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. |
| 42 | +- No egglog change was needed. |
| 43 | + |
| 44 | +OPEN: |
| 45 | +- the ruling on reporting cold-compile cost; |
| 46 | +- E2–E5 beyond what E1 exercises; |
| 47 | +- a lowering target for wrapping arithmetic (none exists; by design?); |
| 48 | +- `Measure::Scale` stays gated on a real population-measure consumer in a separate PR. |
0 commit comments