Struct ProofIR 

pub struct ProofIR {
    pub refined_types: HashMap<TypeId, RefinedTypeDecl>,
    pub fn_contracts: HashMap<FnId, FnContract>,
    pub law_theorems: Vec<LawTheorem>,
    pub unclassified_fns: Vec<UnclassifiedFn>,
}

Output of the proof_lower pipeline stage. Every decision the proof backends will make is materialised here; backends become pure renderers.

ProofIR is intentionally NOT a closed superset of the AST — it only carries facts that proof export needs. Source-faithful emission of plain fns / verify cases still flows through the untyped AST path, same as runtime backends (VM, Rust, WASM).

Fields

refined_types: HashMap<TypeId, RefinedTypeDecl>

Every refinement-lifted user type, keyed by opaque TypeId from the symbol table. Same-bare-name refined records in two modules (A.Natural vs B.Natural) get distinct IDs, so their predicates never merge. Includes types declared in the entry items and in dependent modules; name resolution happens once in populate_refined_types, consumers look up directly by id through ctx.symbol_table.

fn_contracts: HashMap<FnId, FnContract>

Per-pure-fn contract describing what proof artifact the fn lowers to (native / fuel / structural / linear recurrence). Keyed by opaque FnId from the symbol table — name resolution happens once in populate_fn_contracts; consumers thereafter use ctx.symbol_table to resolve &FnDef → FnId and look up directly. Cross-module same-bare-name fns get distinct IDs, so the lookup is unambiguous without per-call-site scope plumbing.

law_theorems: Vec<LawTheorem>

Per-verify-law theorem decomposed into quantifiers, premises, and claim with all wrapper-strip / val-projection / drop-vs- keep decisions baked in, plus the pinned proof strategy.

unclassified_fns: Vec<UnclassifiedFn>

Recursive pure fns whose shape fell outside every recognised pattern. Surfaced as diagnostics (“recursive function ‘foo’ is outside proof subset (…)”) and steers the consumer to either skip the fn or emit it as a partial/axiom fallback. Carried in ProofIR so consumers don’t re-run the classifier just to see what failed.

Trait Implementations

impl Clone for ProofIR

fn clone(&self) -> ProofIR

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ProofIR

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for ProofIR

fn default() -> ProofIR

Returns the “default value” for a type.