Struct ProofLowerInputs 

pub struct ProofLowerInputs<'a> {
    pub entry_items: &'a [TopLevel],
    pub dep_modules: &'a [ModuleInfo],
    pub module_prefixes: &'a HashSet<String>,
    pub recursive_fns: &'a HashSet<FnId>,
    pub symbol_table: &'a SymbolTable,
    pub program_shape: Option<&'a ProgramShape>,
}

Backend-neutral view of the data proof_lower needs. Built once per lowering call; lets the pipeline pass it through without requiring a fully-assembled CodegenContext (which only exists after build_context runs). Legacy callers still build the view from &CodegenContext via ProofLowerInputs::from_ctx.

All fields are borrows — the struct never owns memory; the pipeline and build_context both already own the data and just lend it.

Post-Step-7c: every helper the lowerer touches (refinement_info_for, analyze_plans, the detect.rs shape checkers) reads its inputs through this view. No more &CodegenContext reach-through — the struct stands on its own.

Fields

entry_items: &'a [TopLevel]

Entry-file top-level items, post-pipeline (TCO etc. applied).

dep_modules: &'a [ModuleInfo]

Dependent modules already split into type/fn defs.

module_prefixes: &'a HashSet<String>

Set of dep module prefix strings (e.g. "Models.User").

recursive_fns: &'a HashSet<FnId>

Recursive fn ids from the analyze pipeline stage. Keyed by opaque crate::ir::FnId so entry+module same-bare-name fns don’t merge. Per-scope helpers below project back to HashSet<String> for consumers that operate on a single scope (the DAG invariant keeps bare-name unambiguous within a scope).

symbol_table: &'a SymbolTable

Resolved-identity table (#138 phase E). When Some, the populate-side resolves FnKey / TypeKey to FnId / TypeId once at the IR boundary and keys ProofIR.fn_contracts / ProofIR.refined_types / LawTheorem.fn_id by the opaque IDs. Callers that haven’t wired in the symbol-table stage pass None and fall through to legacy key-typed maps (transitional during phase E migration).

program_shape: Option<&'a ProgramShape>

Optional ProgramShape substrate (Stage 6b of #232). When Some, refinement_info_for reads from the typed ModulePattern::RefinementSmartConstructor entries instead of re-walking the AST. None keeps the legacy walk path — preserved for test fixtures that build ProofLowerInputs by hand without going through the pipeline.

Implementations

impl<'a> ProofLowerInputs<'a>

pub fn from_ctx(ctx: &'a CodegenContext) -> Self

Build a view from a fully-assembled CodegenContext — used by refresh_facts (test helper) and by any caller that already owns a built context. Reads only the fields the lowerer actually needs.

pub fn pure_fns(&self) -> Vec<&'a FnDef>

All pure fn defs across entry items and dep modules, in walk order (entry first, then deps). is_pure_fn lives in the Lean toplevel module today; pure_fns reaches there since the pure-ness criterion is the same for every proof backend.

pub fn recursive_pure_fn_names(&self) -> HashSet<String>

Recursive pure fn names. Filters recursive_fns by pure-ness. Returns bare names (pure_fns view is the whole program here, so any FnId in recursive_fns that maps back to a pure fn gets its bare name surfaced for downstream classifiers).

pub fn pure_fns_in_scope(&self, scope: Option<&str>) -> Vec<&'a FnDef>

Pure fns restricted to a single scope: None = entry only, Some(prefix) = the dep module with that prefix only. Aver’s module DAG invariant rules out cross-module recursion SCCs, so per-scope classification is the canonical view — populate_fn_contracts walks this per scope to give each Module.fn its own canonical key in ir.fn_contracts instead of letting two same-bare-name fns silently merge.

pub fn recursive_pure_fn_names_in_scope( &self, scope: Option<&str>, ) -> HashSet<String>

Recursive pure fn names restricted to a single scope. Filters the FnId-keyed recursive_fns to the ones whose canonical scope matches scope, then projects back to bare names for scope-local consumers (DAG invariant keeps bare-name unambiguous within a single scope).

pub fn scopes(&self) -> Vec<Option<String>>

Iterator over (None = entry, Some(prefix) = each dep module) — drives populate_fn_contracts’s per-scope walk.

pub fn fn_owning_scope(&self, fd: &FnDef) -> Option<&'a str>

Scope of the dep module that owns fd, or None for entry module fns. Pointer-eq match against dep_modules, mirroring crate::codegen::common::fn_owning_scope_for but reading off the lowering view (which doesn’t carry a full CodegenContext).

pub fn resolve_expr( &self, expr: &Spanned<Expr>, scope: Option<&str>, ) -> Spanned<ResolvedExpr>

Resolve a raw-AST expression to its ResolvedExpr form under the given scope. ProofIR stores resolved expressions (Phase E PR 12 Scope A), so this helper is called at every producer site that lifts a Spanned<crate::ast::Expr> slice from the source into an IR field. Mirrors CodegenContext::resolve_expr but reads only the symbol_table carried on this view — proof lowering runs inside the pipeline, before a full CodegenContext exists.

pub fn recursive_type_names(&self) -> HashSet<String>

Names of every recursive user-defined type across entry + deps.

pub fn find_fn_def_by_call_name(&self, call_name: &str) -> Option<&'a FnDef>

Find a fn def by name across entry + deps. Falls back to the last segment of a dotted call (e.g. Module.fn resolves to fn when no exact-match candidate exists).

pub fn find_type_def(&self, type_name: &str) -> Option<&'a TypeDef>

Find a type def by bare name across entry + deps. None on miss or when the name resolves to a non-Product / non-Sum shape.