Supercompiler — a unified optimization pass that subsumes constant folding,
propagation, dead code elimination, and compile-time function evaluation
in a single framework.
EXODIA Phase 1’s DELIVERY layer: a product fact for every expression
occurrence at its program point, keyed by ARENA ADDRESS (stable for the
analyzed snapshot — record facts immediately before consuming them, and
never across a pass that re-allocates expressions). Shared subtrees that
appear at several program points JOIN their facts (sound; precision is
lost exactly where sharing occurs).
A variable’s program-wide PROVEN facts — the statically-verified summary the
debugger shows beside its live value (distinct from the dynamic, observed-this-run
invariants). All fields are sound over-approximations: present ⇒ proven.
Run the Oracle’s rich abstract interpretation, returning the (unchanged)
statements together with the per-variable abstract facts.
The scalar kinds downstream consumers (typed bytecode, JIT guard
elision) act on.
Begin recording which optimizations fire AND which they preempt for the
current compile. Resets both accumulators; pair with end_fired_trace /
end_preempted_trace.
Render an affine capacity LinExpr as a Rust i64 expression string — used to
size a dense map’s direct-addressed array (with_bounds(0, (cap) + 1)) at its
constructor site. None if any coefficient or the constant is non-integer (no
clean rendering), in which case the dense gate declines and the map stays a
hash table. Terms are emitted in symbol-index order for determinism.
Record that winner took precedence over loser here — the exact spot the
code skips one optimization for another (the conflict, traced at its source,
the same way mark_fired traces firing). No-op when no trace is active, so
the normal compile path and the benchmark scripts pay nothing. Self-gated on
BOTH being enabled in the current config: a preemption is only meaningful when
the two genuinely contest an instance — so toggling either off cleanly stops
the edge from being reported.
Lighter optimization for Futamura P1: fold + propagate + PE + CTFE.
Skips DCE, abstract interpretation, supercompilation, and structural
transforms (LICM, closed-form, deforestation) that eliminate branches
or restructure control flow. The residual preserves the program’s
original control-flow structure while still folding constants,
propagating values, specializing functions, and evaluating CTFE.
The RUN-PATH pipeline (EXODIA D1): the Futamura residual — fold,
propagate, polyvariant PE, CTFE, GVN, LICM, closed-form, deforestation,
interval analysis, DCE — everything except supercompilation (whose
driving cost is unbounded; it stays AOT-only). Budgeted: programs beyond
the statement gate run raw, and LOGOS_RUN_OPT=0 kills the pass
entirely. Optimizer time lands inside the measured run, so the budget is
part of the contract.
The run-path optimizer, gated by the unit’s hotness tier (HOTSWAP §4). Every
pass runs in the SAME order as the un-tiered pipeline; tier decides WHICH passes
run (via admits_pinned, a single cost comparison, with hs’s per-opt pins
applied) and how many PE-fixpoint iterations to pay for. Tier::T3 with an all-on
config and no pins reproduces optimize_for_run exactly — the compatibility +
soundness anchor.
The AOT optimizer — ONE pipeline. The Futamura residual (fold, propagate,
polyvariant PE, CTFE) then the ARCHITECT: equality saturation over a
kernel-certified e-graph, Oracle facts gating the conditional rewrites
(value facts suppressed for loop-mutated variables — see egraph::convert);
then defunctionalization, deforestation, interval analysis, DCE, and
supercompilation. GVN/LICM/closed-form STILL run after the e-graph until it
subsumes their cross-statement and loop-recurrence reach (the EG waves).
oracle_analyze with the interner, enabling declared-parameter type
seeds inside function bodies. Used by every NON-AOT consumer (VM bytecode,
copy-and-patch JIT, e-graph, UI) — these get NO entry-guard precondition, so
the partition’s accesses stay behind a runtime RegionBoundsGuard rather
than being statically elided on a precondition the bytecode never enforces.
oracle_analyze_with for the largo build AOT codegen ONLY. Enables the
recursive-1-based-partition entry-guard precondition (1 <= lo,
hi <= len) and alias length_def propagation — sound here because the AOT
codegen emits the matching runtime assert! at the function entry. The
VM/JIT path emits no such assert, so it must use oracle_analyze_with.