Equality Saturation And Superoptimization

Equality saturation and superoptimization are bounded research lanes for

discovering optimizer candidates. They are not default compiler behavior.

research output is separated from default compilation until a candidate is

promoted into an ordinary deterministic compiler rule with validation,

differential, benchmark, ADR/RFC, and documentation evidence.

Run the bounded evidence gate with:

make eqsat-superoptimization-check

This gate validates source-owned rewrite domains, e-graph budgets, extraction

cost models, candidate equivalence, offline proposal intake, promotion

evidence, diagnostics, negative fixtures, and release reports. It does not run

heavy compiler builds, self-hosting, remote deployment, broad benchmark suites,

or online model calls.

Domains

Supported research domains live in eqsat-superopt/domains.tsv:

• arithmetic-bitmanip;
• late-lir-peephole;
• vectorization-candidates;
• dsl-fragment.

Each domain is disabled by default and names an explicit target surface:

HIR, MIR, LIR, or MachineIR.

Rewrite And Extraction Budgets

Rewrite sets live in eqsat-superopt/rewrite-sets.tsv. Each set must declare:

• max e-graph nodes;
• max iterations;
• max elapsed milliseconds;
• deterministic limits;
• a release report.

Extraction costs live in eqsat-superopt/extraction-costs.tsv. Cost models

must have stable objectives and source-order tie breaking.

Candidate Validation

Candidate fixtures use 0x0-eqsat-candidate-v1 JSON and are checked by:

python3 tools/eqsat_candidate_eval.py --candidate eqsat-superopt/fixtures/valid-add-zero.json

The evaluator exhaustively checks the finite input domain for supported

candidate expressions and rejects:

• unsupported domains or operators;
• over-budget searches;
• non-equivalent expressions;
• candidates whose extracted expression is not cheaper.

Proposal Intake

LLM-guided proposals are allowed only as offline candidate generation. Online

LLM calls are not allowed in compiler, release, or gate paths. Proposal intake

lives in eqsat-superopt/llm-proposal-intake.tsv.

Promotion

A validated candidate is not a production compiler rule by itself. Promotion

requires:

• ordinary deterministic compiler implementation;
• ADR and RFC evidence;
• translation validation;
• differential testing;
• benchmark evidence;
• release note;
• public documentation.

The current promoted candidate is arith-add-zero, because the deterministic

optimizer-fold-int-identity rule already exists in compiler/main.0x0.

Other validated candidates remain research-only.

Release Evidence

Release evidence lives in:

• release/eqsat-superopt-rewrite-report.tsv;
• release/eqsat-superopt-extraction-report.tsv;
• release/eqsat-superopt-candidate-report.tsv;
• release/eqsat-superopt-validation-report.tsv;
• release/eqsat-superopt-differential-report.tsv;
• release/eqsat-superopt-benchmark-report.tsv;
• release/eqsat-superopt-proposal-report.tsv;
• release/eqsat-superopt-promotion-report.tsv;
• release/eqsat-superopt-diagnostics-report.tsv;
• perf/eqsat-superopt-performance.tsv;
• compat/eqsat-superoptimization-contract.tsv.

Diagnostics

The gate reports stable diagnostics:

• EQS_DOMAIN_MISSING;
• EQS_BUDGET_EXCEEDED;
• EQS_NON_EQUIVALENT;
• EQS_COST_MODEL;
• EQS_LLM_ONLINE;
• EQS_PROMOTION_EVIDENCE;
• EQS_DEFAULT_PATH.

Negative fixtures under eqsat-superopt/fixtures/ prove fail-closed behavior

for non-equivalence, budget excess, bad extraction cost, online LLM intake, and

promotion without evidence.