Struct OracleFacts 

pub struct OracleFacts { /* private fields */ }

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).

Implementations

impl OracleFacts

pub fn hoist_descs_for(&self, loop_ptr: usize) -> &[HoistDesc]

Region-entry bounds hoists for the loop at loop_ptr (the While/ Repeat statement’s arena address). The compiler lowers each to a RegionBoundsGuard at the loop head.

pub fn index_is_speculative(&self, index: &Expr<'_>) -> bool

Is this index sub-expression proven in bounds only SPECULATIVELY (needs a region-entry guard)? The compiler elides it solely when it emitted that guard.

pub fn expr_scalar(&self, e: &Expr<'_>) -> Option<ScalarKind>

The proven scalar kind of this expression occurrence, if concrete.

pub fn expr_int_range(&self, e: &Expr<'_>) -> Option<(i64, i64)>

The finite integer range proven for this occurrence, if both bounds are finite.

pub fn expr_proven_nonneg(&self, e: &Expr<'_>) -> bool

Is this occurrence PROVEN non-negative — its abstract interval’s LOWER bound is a finite >= 0? Unlike Self::expr_int_range this ignores the upper bound, so it holds even when the value’s magnitude is unbounded above (the LCG seed * 1103515245 + 12345 dividend: both factors non-negative, so lo = 0, but the product’s hi may saturate). This is the soundness gate for x % 2^k → x & (2^k - 1), whose identity needs only x >= 0, not a finite ceiling.

pub fn expr_int_range_addr(&self, addr: usize) -> Option<(i64, i64)>

As Self::expr_int_range, keyed by the expression’s arena address (the form the i32-narrowing gate collects its key/value sites in).

pub fn summarize_variables( &self, stmts: &[Stmt<'_>], ) -> Vec<(Symbol, VarProvenFacts)>

Debugger-only by-name rollup: walk stmts and JOIN every Identifier(sym) occurrence’s already-recorded abstract value into one proven summary per variable. Sound by construction (joining widens), so a returned int_range of [0, 9] means the variable was within it at every use — a program-wide proven invariant.

This re-reads the facts that the production walk already computed; it adds NOTHING to record_expr/oracle_analyze, so it is zero cost unless the debugger calls it (no production path does). Reused from the same module so it can read exprs.

pub fn has_dense_map_capacity(&self, map: Symbol) -> bool

Does this Map of Int to Int have a recorded invariant affine capacity (the precondition for any dense-key proof against it)?

pub fn map_cap_lin(&self, map: Symbol) -> Option<&LinearExpr>

The recorded invariant affine capacity for a dense map — the bound every key was proven <= cap against. Codegen renders it (see lin_to_rust) to size the direct-addressed array with_bounds(0, cap + 1).

pub fn dense_map_key_proven(&self, key: &Expr<'_>, map: Symbol) -> bool

Was this key occurrence PROVEN within [0, capacity(map)] (so a direct-addressed array of capacity + 1 slots indexes it safely)?

pub fn dense_map_key_proven_addr(&self, key_addr: usize, map: Symbol) -> bool

As Self::dense_map_key_proven, keyed by the expression’s arena address directly (the form the dense gate collects its key sites in).

pub fn dense_map_has_full_coverage(&self, map: Symbol) -> bool

Does this dense map’s single insert loop provably cover a contiguous range fully (the structural precondition for presence elision)?

pub fn dense_key_covered_addr(&self, key_addr: usize, map: Symbol) -> bool

Was this key occurrence PROVEN inside its map’s fully-covered insert range (so the key was definitely written, and get may skip the presence bit)?

pub fn expr_is_tracked_collection(&self, e: &Expr<'_>) -> bool

Is this occurrence PROVEN collection-kinded? Seeded at collection creations and preserved through growth, shrinkage and calls — kind is a binding-level fact only rebinding can erase.

pub fn loop_handles_definitely_distinct( &self, loop_stmt: &Stmt<'_>, a: Symbol, b: Symbol, ) -> bool

PROOF that two handles denote distinct allocations at every iteration of loop_stmt (a While/Repeat analyzed to convergence). This is the soundness gate for borrow hoisting: true only when both handles have fully tracked provenance and their may-alias components do not meet at the loop invariant — including loop-CARRIED edges. Anything else (tainted handle, non-converged loop, unknown statement, concurrent context) refuses.

pub fn expr_len_range(&self, e: &Expr<'_>) -> Option<(i64, i64)>

Finite proven LENGTH bounds for this collection occurrence.

pub fn index_proven_relational(&self, index: &Expr<'_>) -> bool

True when index is proven in bounds RELATIONALLY (multi-variable LIA / SCEV / entry-guard), as opposed to a plain interval bound. The swap peephole uses this to keep partition swaps (quicksort’s i/j, related by i <= j < hi <= len) as the unchecked indexed form instead of downgrading them to a bounds-checked .swap(); literal-index swaps (interval-proven) still become .swap()/__swap_tmp.

pub fn index_provably_in_bounds( &self, collection: &Expr<'_>, index: &Expr<'_>, ) -> bool

The guard-elision query (EXODIA 1.3): is index PROVABLY within the 1-based bounds of collection at this program point? True only when the index interval sits inside [1, len.lo].

pub fn index_positivity_guards(&self, index: &Expr<'_>) -> &[Symbol]

The % m divisors whose m >= 1 precondition an elision of this exact index relied on (empty for a purely affine/interval elision). Codegen emits assert!(m > 0) for each at the access, discharging the symbolic element bound’s precondition so the elision is sound for every input.

Trait Implementations

impl Default for OracleFacts

fn default() -> OracleFacts

Returns the “default value” for a type.