Struct CodegenContext 

pub struct CodegenContext {

    pub items: Vec<TopLevel>,
    pub type_defs: Vec<TypeDef>,
    pub fn_defs: Vec<FnDef>,
    pub project_name: String,
    pub modules: Vec<ModuleInfo>,
    pub module_prefixes: HashSet<String>,
    pub policy: Option<ProjectConfig>,
    pub emit_replay_runtime: bool,
    pub runtime_policy_from_env: bool,
    pub guest_entry: Option<String>,
    pub emit_self_host_support: bool,
    pub extra_fn_defs: Vec<FnDef>,
    pub mutual_tco_members: HashSet<FnId>,
    pub recursive_fns: HashSet<FnId>,
    pub buffer_build_sinks: HashMap<String, BufferBuildShape>,
    pub buffer_fusion_sites: Vec<FusionSite>,
    pub synthesized_buffered_fns: Vec<FnDef>,
    pub proof_ir: ProofIR,
    pub symbol_table: SymbolTable,
    pub resolved_fn_defs: Vec<ResolvedFnDef>,
    pub current_module_scope: RefCell<Option<String>>,
    pub resolved_module_fn_defs: Vec<Vec<ResolvedFnDef>>,
    pub resolved_program: ResolvedProgramView,
    pub program_shape: Option<ProgramShape>,
    pub mir_program: Option<MirProgram>,
    pub bare_i64: BareI64Facts,
    pub discovered_lemmas: Vec<CommittedLemma>,
    pub sample_expected: HashMap<(String, usize), String>,
    pub allow_mathlib: bool,
    pub hand_proofs: HashMap<(String, String), String>,
}

Collected context from the Aver program, shared across all backends.

Invariant (epic #170 Phase 2)

resolved_program is the primary backend input. Every identity-sensitive decision (call/ctor/type lookup, fn-by-id dispatch, mutual-SCC analysis) belongs to that view; the pipeline produced it once and build_context projects it through.

The legacy AST-shape fields below — items, fn_defs, type_defs, resolved_fn_defs, resolved_module_fn_defs — are source metadata / migration caches, not independent sources of truth:

• items, fn_defs, type_defs retain source-shape spans and diagnostics; backends mid-migration still walk them. They are NOT the place to add new identity-sensitive logic.
• resolved_fn_defs / resolved_module_fn_defs are projections of resolved_program kept for callsites that don’t yet route through the FnId index. New code should reach resolved_program.fn_by_id(fn_id) instead.

Subsequent epic phases migrate backends (Rust, Lean, Dafny, wasm-gc) to iterate the view directly. New code in backends should default to the view. AST consumption requires a clear category in a code comment: diagnostic-only, syntax-discovery-only, backend-link-stage, display-only, or temporary-migration-bridge.

Fields

items: Vec<TopLevel>

All top-level items (post-TCO transform, post-typecheck).

Source metadata — kept for span / diagnostic / syntax discovery access. Backends iterating fn bodies should reach resolved_program.entry_fns() instead.

type_defs: Vec<TypeDef>

User-defined type definitions (for struct/enum generation).

Source metadata. Type-id-keyed lookups go through symbol_table (see Self::symbol_table); fn bodies that need a resolved type reach it via Type::Named(TypeId, _) after the typechecker stamps. This list stays for ergonomic iteration over user-declared types in syntax-discovery sites (e.g. cataloguing all enum declarations for the proof pipeline’s refinement detection).

fn_defs: Vec<FnDef>

User-defined function definitions.

Source metadata. Backends mid-migration walk this for fn-signature shape; new identity-sensitive code reaches resolved_program.entry_fns() / fn_by_id(fn_id) instead. Synthesized FnDefs (TCO hoists) appended after the pipeline ran live here too; the on-demand resolver (Self::resolve_fn_def) lifts them through the symbol table.

project_name: String

Project/binary name.

modules: Vec<ModuleInfo>

Dependent modules loaded for inlining.

module_prefixes: HashSet<String>

Set of module prefixes for qualified name resolution (e.g. “Models.User”).

policy: Option<ProjectConfig>

Embedded runtime policy from aver.toml for generated code.

emit_replay_runtime: bool

Emit generated scoped runtime support (replay and/or runtime-loaded policy).

runtime_policy_from_env: bool

Load runtime policy from the active module root instead of embedding it.

guest_entry: Option<String>

Explicit guest entry boundary for scoped replay/policy.

emit_self_host_support: bool

Emit extra generated helpers needed only by the cached self-host helper.

extra_fn_defs: Vec<FnDef>

Extra fn_defs visible during current module emission (not in fn_defs or modules). Set temporarily by the Rust backend when emitting a dependent module so that find_fn_def_by_name can resolve same-module calls.

mutual_tco_members: HashSet<FnId>

Functions that are part of a mutual-TCO SCC group (emitted as trampoline + wrappers). Functions NOT in this set but with TailCalls are emitted as plain self-TCO loops. Keyed by opaque crate::ir::FnId from the symbol table — entry-module fns and dep-module fns with the same bare name can’t accidentally merge under bare-name keying.

recursive_fns: HashSet<FnId>

Functions that call themselves directly or transitively. Set- form union of entry_analysis.recursive_fns plus each module’s analysis.recursive_fns. Keyed by opaque crate::ir::FnId — same disambiguation guarantee as mutual_tco_members. Used by codegen sites that previously called call_graph::find_recursive_fns ad-hoc.

buffer_build_sinks: HashMap<String, BufferBuildShape>

Buffer-build sink fns (List.prepend/reverse builders consumed by String.join). The Rust backend emits a <fn>__buffered variant alongside each entry; the WASM backend rewrites bodies to call rt_buffer_* helpers. Detection lives in ir::buffer_build.

buffer_fusion_sites: Vec<FusionSite>

Fusion sites detected for String.join(<sink>(...), sep) calls. Each entry pairs an enclosing fn + line + sink fn name; the emitter rewrites these call expressions to use buffered variants in place of the producer + consumer chain.

synthesized_buffered_fns: Vec<FnDef>

Synthesized <fn>__buffered variants for every buffer-build sink, produced by ir::synthesize_buffered_variants. These are real FnDefs with proper body AST; backends iterate over them alongside fn_defs so they reach codegen through the same pipeline (TCO / no-alloc / mutual-recursion all apply identically). Empty when no sinks are detected.

proof_ir: ProofIR

Proof-export decision IR populated by proof_lower::lower during build_context. Backends (Lean, Dafny) read from here to decide refinement-record lift, recursion contracts, law-theorem shape, etc. Single source of truth — both backends see the same decisions so cross-backend drift becomes impossible at the shape level. Step 2: only refined_types is populated; backends still consume legacy refinement_info_for for now. Step 3+ migrates backends.

symbol_table: SymbolTable

Resolved-identity table (#138 phase E). Always populated: pipeline::run builds it unconditionally and threads it through build_context. Consumers (proof IR lookups, backend FnId/TypeId resolution) read it directly — no Option wrapper to unwrap at each callsite.

resolved_fn_defs: Vec<ResolvedFnDef>

Resolved-HIR forms of every entry-scope fn in fn_defs, in the same source order.

Compatibility projection of resolved_program.entry_fns() (epic #170 Phase 1). Position-aligned with the entry slice of resolved_program.entry_items. New code should prefer resolved_program.entry_fns() / fn_by_id(fn_id) so the FnId index is the lookup mechanism. This vec stays for callsites that haven’t yet been migrated to the view; it will be retired once Phase 3-6 migrate all backends.

current_module_scope: RefCell<Option<String>>

Module scope currently active for name resolution. Set by a backend dispatcher before emitting a dep-module’s fns so that legacy resolve-on-demand adapters (e.g. Lean’s emit_expr_legacy) thread the right scope into resolve_expr / resolve_stmt instead of defaulting to entry. Empty by default. Set with Self::with_module_scope in a scoped manner.

resolved_module_fn_defs: Vec<Vec<ResolvedFnDef>>

Per-dep resolved fn defs, parallel to modules.

Compatibility projection of resolved_program.modules[i].fn_defs (epic #170 Phase 1). Position-aligned with modules for callsites that index by modules[i]. New code should prefer resolved_program.module_fns(prefix) or the global fn_by_id(fn_id) index — that’s where cross-module bare-name disambiguation happens for free. Retired alongside resolved_fn_defs once Phase 3-6 migrate the remaining backends.

resolved_program: ResolvedProgramView

Canonical resolved-program view of the whole codegen input — entry items (post-pipeline NameResolve) + per-dep-module resolved fn defs + FnId-keyed lookup.

Epic #170 Phase 1 invariant. resolved_program is the primary source of truth for backend codegen — fn_defs, type_defs, items, resolved_fn_defs, and resolved_module_fn_defs remain available as projection / source metadata / migration cache, but consumers should reach the view first when an FnId / TypeId is in hand. Subsequent phases (#170 Phase 3+) migrate backends to iterate the view as their primary input; this field is the foundation those PRs build on.

program_shape: Option<ProgramShape>

Whole-program shape facts — typed Archetype labels + call-graph SCC per FnId. Computed once per compilation by analyze_program at build_context time. Stage 5+ of #232 (0.23 “Shape”) migrates ad-hoc fn-shape detectors in proof codegen to read this instead of rewalking the AST. None only for tests that assemble the ctx by hand without calling build_context; downstream callers should treat that as opt-out (preserve legacy detection path).

mir_program: Option<MirProgram>

Optimized Core MIR for the whole codegen input (entry + dep module fns), FnId-keyed. Built once at build_context from the resolved program — the same lowering + optimizer pass the VM / wasm-gc / wasip2 backends run. The Rust backend reads fn_by_id(fn_id) here to drive its sole codegen path (from_mir::emit_mir_fn_body_routed): the MIR walker owns all runtime codegen after the HIR walker’s deletion (W6/Stage-3). None for hand-assembled test contexts that skip build_context.

bare_i64: BareI64Facts

Per-(FnId, LocalId) bare-i64 representation facts for the Int “unboxing” optimization, computed from mir_program by bare_i64::analyze. The Rust backend reads a per-fn slice at signature + body emit to select native i64 vs the default aver_rt::AverInt for provably-bounded, non-escaping Int values. Fail-closed: empty (all-Boxed) for hand-assembled test contexts and for dependency-module fragments (callers unseen).

discovered_lemmas: Vec<CommittedLemma>

Kernel-proved lemmas parsed back from a committed DiscoveredLemmas.lean (the --discover artifact), set by the CLI on a normal aver proof run when the discovery-surface hash still matches. The Lean backend embeds each pinned lemma’s text before the first law theorem that uses it (re-proving it in the same build) and simps over its name (ProofStrategy::SimpOverLemmas). Empty unless the CLI wired it — discovery feedback is strictly opt-in.

sample_expected: HashMap<(String, usize), String>

VM-computed ground-truth values for verify cases, keyed by (common::verify_block_counter_key(vb), global_case_index) → aver_repr_literal rendering of the case’s expected (right-side) value. Set by the CLI on aver proof --backend lean from a Declared- mode aver verify run over the entry items; empty everywhere else. The Lean emitter literalizes the expected side of bounded sample checks from this table (model-vs-ground-truth) so that fuel exhaustion — where panic! returns default and a model-vs-model equation becomes vacuously true under native_decide — cannot kernel-certify a false equation. Entries exist only for cases that PASSED aver verify; failing/skipped cases keep the source RHS.

allow_mathlib: bool

aver proof --allow-mathlib (Lean only, opt-in): permit a generic Mathlib break-glass closing arm on laws the core strategies cannot claim. When false (the default) the Lean backend is BYTE-IDENTICAL to before — no Mathlib import, no break-glass arm, same tiers. When true a walling when-law is emitted in true-universal form with a domain- blind Mathlib tactic portfolio (aver_mathlib, keyed on Int.ediv_ediv_of_nonneg / pow_add / positivity / nlinarith / …) under a first | (trace "AVER_MATHLIB:fn.law"; …) | sorry floor. The post-emit step (setup_mathlib_for_project) wires the cached Mathlib into the generated lake project; the build-log trace marker drives the per-law mathlib credit. Axiom whitelist is UNCHANGED — Mathlib lemmas are kernel-clean {propext, Classical.choice, Quot.sound}.

hand_proofs: HashMap<(String, String), String>

Hand-proof sidecars, keyed by (fn_name, law_name) → the proof BODY (the tactic text after Lean’s := by, or the Dafny lemma body between { and }). Loaded by the CLI from a project’s source-controlled proofs/<lean|dafny>/<fn>__<law>.{lean,dfy} sidecar dir for the active backend; empty everywhere else. When an entry exists for a law, the codegen splices the body into that law’s emitted theorem/lemma and lets the kernel (lake / dafny verify) re-check it — a WRONG body fails the build loudly and the law is denied universal credit. A law with NO sidecar is byte-identical to before. The genuinely-hard lemmas the generic engine cannot find (trunc-sticky composition, sticky-plus) live here as LABELED, kernel-checked hand proofs (manifest credit hand).

Implementations

impl CodegenContext

pub fn with_module_scope<R>( &self, scope: Option<&str>, f: impl FnOnce() -> R, ) -> R

Set current_module_scope for the duration of f. Backends wrap their per-module emit calls with this so legacy resolve-on-demand adapters see the correct prefix.

pub fn active_module_scope(&self) -> Option<String>

Snapshot of the active module scope. Cloned so callers may pass as_deref() into resolver/emitter APIs without holding the RefCell borrow.

pub fn law_target_fn_id(&self, fn_name: &str) -> Option<FnId>

Resolve a verify-law’s target fn name to its [FnId] under the active module scope: FnKey::in_module(scope, name) when a dep module is in scope (cross-file law pool — the dep law’s LawTheorem is keyed by its dep-scope id), else FnKey::entry(name). The entry key is tried as a fallback so an entry law emitted with a stale scope still resolves. Drives the proof_ir.law_theorems strategy lookup so a dep law gets the SAME auto-proof strategy an entry law of that shape would.

pub fn fn_def_by_name(&self, name: &str, scope: Option<&str>) -> Option<&FnDef>

Identity-keyed lookup from a bare fn name + scope to the matching &FnDef in fn_defs / modules[i].fn_defs. Resolves the name through the symbol table to an FnId first, then recovers the AST FnDef via fn_id_for_decl pointer-eq scope matching — so two same-bare-name fns across modules can’t cross-resolve.

Epic #170 Phase 5 helper. Replaces the ctx.fn_defs.iter().find(|fd| fd.name == name) pattern that proof-mode law / verify rewriters used pre-migration. Backends that still need a &FnDef (rather than the resolved twin — e.g. rewrite_effectful_calls_in_law consumes AST shape) reach this method instead of walking by bare name.

Returns None when the symbol table doesn’t know the name under the given scope, or when the resolved FnId doesn’t match any &FnDef in that scope (synthetic FnDefs added post-pipeline fall through here — callers can fallback to a bare-name walk over extra_fn_defs etc. when that matters).

impl CodegenContext

pub fn refresh_facts(&mut self)

Test-only bridge: recompute every derived fact (mutual_tco_members, recursive_fns, proof_ir, resolved_program) from the current items and modules. Used exclusively by unit tests that construct a CodegenContext piecewise — pushing synthetic FnDefs straight into the items list rather than going through the parser and pipeline. Production code never needs this: every derived fact is populated by the pipeline stages (analyze, proof_lower) and propagated through build_context. Calling refresh_facts on a production-built ctx is redundant work that produces the same answer — leave it off the hot path.

Single-source-of-truth invariant (epic #170 Phase 1+2): rebuilds resolved_program once from the freshly-resolved items, then derives resolved_fn_defs / resolved_module_fn_defs as projections of that view. There is no parallel resolve path here.

pub fn resolve_fn_def<'a>( &'a self, fd: &'a FnDef, scope: Option<&str>, ) -> Cow<'a, ResolvedFnDef>

Look up the resolved-HIR mirror of a source-shape FnDef previously stashed in resolved_fn_defs / resolved_module_fn_defs. Falls back to a fresh per-call resolver lift against the entry’s crate::ir::SymbolTable when neither path covers fd — this happens for synthetic FnDefs inserted between build_context and emit (TCO hoist rewrites, test fixtures) which the resolver hasn’t lifted upfront.

scope is the owning module prefix when fd came from a dependency module’s module.fn_defs, None when fd is part of the entry’s ctx.fn_defs. Lookup keys by crate::ir::FnKey through the crate::ir::SymbolTable so two modules that share a bare fn name (e.g. Util.format and Other.format) resolve to their own crate::ir::FnId without bare-name collisions. Pre-PR-9.3a this matched by rfd.name == fd.name against a flat search of every resolved table — fragile the moment flatten changes (or doesn’t run) and two scopes share a name.

Phase E shared lookup boundary — Rust codegen (PR 8) already consumes this through rust::toplevel::resolved_fn_def_for; wasm-gc / Lean / Dafny / self-host backends pick it up in their follow-up PRs.

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

Resolve a source-shape Spanned<Expr> on demand using the entry’s resolver context. Used by emit helpers that still walk Expr (TCO hoisting, mutual TCO, verify blocks, follow-up backends pre-migration) and need to feed the resolved shape into the migrated emitter. The returned Spanned<ResolvedExpr> carries the same line + type stamp as the input.

scope is the owning module prefix when the caller knows which dep module the expression lives in, None for entry- scope code. Required for cross-module name resolution — e.g., a call site in module A referring to Val.ValOk declared in module B only resolves to ResolvedCtor::User when the resolver’s current_module matches the call site’s owning scope. Pre-PR-9.4 the helper used the entry module name uniformly, which broke cross-module ctor / fn classification for the legacy emit paths (mutual TCO trampolines, TCO hoist — they walked dep-module fn bodies but the resolver context said “you’re in the entry module”; the self-host regen surfaced the gap when same-name shadowing across modules was no longer an option).

pub fn resolve_stmt(&self, stmt: &Stmt, scope: Option<&str>) -> ResolvedStmt

Same as Self::resolve_expr but for whole statements (Binding(name, ty_ann, expr) or Expr(expr)).

pub fn resolve_pattern( &self, pat: &Pattern, scope: Option<&str>, ) -> ResolvedPattern

Resolve a source-shape crate::ast::Pattern to its resolved HIR form. Wraps the pattern in a synthetic match arm + drops it through resolve_stmt_external, since the resolver doesn’t expose a standalone pattern lifter — same workaround rust/toplevel.rs used pre-PR-9.

Trait Implementations

impl FnSigOracle for CodegenContext

fn fn_sig(&self, name: &str) -> Option<FnSigInfo>