Name proof endpoints by value, and stop tabling reflexive proofs

[oflatt-claude]

Name proof endpoints by value, and stop tabling reflexive proofs

The proof encoding used to reach a term's reflexive proof (t = t) by looking it up. Every sort got a @<Sort>Proof : (S) -> @Proof table, every constructor wrote one row into it per node built, and every sort also got an @Ast<Sort> wrapper so a @Fiat could name endpoints of any sort through a single erased @Ast sort. Both are now gone.

A reflexive anchor is instead projected out of a row proof already in scope. A view row's proof states an equality whose right-hand side is the row's term, so a child of that term is @Proj(row, i), the row's e-class is the row proof reflexivized, and a container element — whose position in the term form is only known once the term is in hand — is @ProjAll_<Sort>(row, element). @Proj is the branch's one new checker rule; @ProjAll_<Sort> is raw-only and conversion desugars it to the @Proj at the position it finds, exactly as it already did for @CongrAll. With endpoints named by value, @Fiat_<Sort> and @ProjAll_<Sort> are specialized per sort and the @Ast sort and its per-sort wrappers disappear.

Three further reductions in what a firing writes:

• One statement per node. Every relation whose last input is a minted id gets a mint-<Relation>! primitive, so (let v (get-fresh! "Math")) (set (Add a b v) ()) becomes (let v (mint-Add! a b)). Registered through the backend SPI (Backend::register_mint_row), with the DD backend servicing it against its mirror.
• delete lowers directly. The @to_delete_<F> marker table and its maintenance rule are gone; the action deletes the view row. The backend already stages removals and applies them ahead of the same batch's insertions, which is the uninstrumented meaning of delete, so lowering it directly preserves it — the marker did not, and diverged from native egglog in 4 of 6 adversarial cases (deleting rows a same-batch insert should have kept; failing to delete rows that were subsumed or that rebuild had re-keyed). Subsumption stays deferred (its marker has to survive re-keying), but its scaffolding is now declared on first subsume rather than with every constructor.
• A base-value premise is recomputed, not recorded. A fact whose premise is a reflexive fiat over a base value — a guard like (> n 0), or the (= len n) a custom function's output leaves behind — is re-evaluated by proof conversion from the bindings earlier facts made. Encoder and conversion share one gate (recomputable_premises) so they cannot drift.

The proof checker is unchanged from the base of this branch apart from the Proj rule: git diff <base> HEAD -- proof_checker.rs is 54 insertions, 0 deletions.

Measured effect

Root ./bench.py, main backend, 12 rounds, default workload set. An A/A control (same source, two builds) put the noise floor at ±1% per file on min-of-12 wall and ±0.1% on peak RSS; deltas below that are not reported as signal. Wall deltas are min-based, reproduced across two independent passes.

Proof mode — suite wall 0.806x (−19.4%), peak RSS −25.9%:

benchmark	wall Δ	peak RSS
luminal-llama	−31.1%	641 → 384 MiB (−40.1%)
hardboiled_conv1d_32	−21.6%	135 → 103 MiB (−23.7%)
eggcc-2mm-pass1	−20.0%	527 → 348 MiB (−33.9%)
pointer-analysis-small	−19.7%	at RSS floor
herbie	−19.0%	at RSS floor
math-microbenchmark	+3.8%	1108 → 899 MiB (−19.0%)
suite	−19.4%	2618 → 1940 MiB

Most of the win is program construction, charged outside rulesets: −1.71 s of eggcc-2mm's −2.0 s, −2.53 s of luminal-llama's −2.56 s. That is the deleted tables and the declare-on-first-use scaffolding shrinking the generated program.

math-microbenchmark is a genuine regression, reproduced in both passes and outside the noise floor. Phase attribution: Apply +615 ms, Merge −391 ms — the branch moves work out of merge into apply on this workload for ~150 ms net. Its RSS still improves 19%.

Native backend — neutral. Suite +0.2%/+0.3% against an A/A control of −0.2%; every per-file delta inside the floor, peak RSS identical.

Known limitation

Programs that were accepted under proofs are now rejected. A value the query computed has no row to project an anchor out of, and there is no congruence route to introduce its term. This only bites where a premise actually reads that anchor — a fact's premise composes Sym(left) with right and drops whichever side is reflexive, so the right-hand anchor is read exactly when the left-hand proof is itself reflexive. Two new ProofEncodingUnsupportedReasons cover it: ContainerCreatedInQueryProvedAbout (an eq-sort element read out of a container the query built) and EqSortPrimitiveResultWithoutContainer (an eq-sort value a primitive produced with no container to have read it out of). One test file moved to the unsupported list (container-query-built-read.egg); base-sorted reads (vec-length and friends) over query-built containers are unaffected. A head that mints no row reads no premise either, but proof support does not model that and rejects those rules too.

Notes for review

• No CHANGELOG.md entry, deliberately — this is a follow-up arc and the entry belongs to the release that ships it.
• Two independent implementations of the anchor gate remain (BodyAnchorScan in the support check, BodyAnchors in the encoder). They reason about the same alias classes over different value representations and can drift; only an assert! catches it. Worth a follow-up.

🤖 Generated with Claude Code

[oflatt-claude]

Superseded by saulshanabrook#48, opened against upstream.