Module proof_lower 

Build ProofIR from a CodegenContext.

The lowering producer: types live in src/ir/proof_ir.rs, this file fills them in from a typechecked + analysed codegen context. Output lands in CodegenContext.proof_ir; both proof backends read from the same field, so any classifier-side decision flows consistently to Lean and Dafny without each backend re-running shape detection.

Populates three IR sections: refined_types (refinement-via- opaque records → Lean Subtype / Dafny subset type), fn_contracts (per-pure-fn recursion shape: native / sized-fuel / linear recurrence), and law_theorems (per-verify- law strategy + quantifier decomposition + claim shape, with Oracle-Lift’d impl-spec calls for effectful equivalence).

tests/proof_ir_diff.rs pins the producer’s output for each canonical source pattern — divergence between the classifier and the IR populator surfaces there.

Epic #170 Phase 7 invariant — AST discovery + typed identity

This module is the last consumer of raw crate::ast::Expr patterns in the codegen layer. That is intentional, not migration debt.

What’s AST-shaped (syntax-discovery-only)

Detector helpers in this file (detect_*, walk_for_*, callee_matches_name, call_named_args, binary_call_var_const, matches_ident_expr) walk ast::Expr directly. They are pattern matchers over source shape — they look for things like match n { 0 -> base; _ -> rec(n - 1) } or Map.has(outer(m, k), k) to decide which ProofStrategy / RecursionPlan variant lowers a given fn or law. The pattern belongs in source-shape; rewriting them on ResolvedExpr would be the same logic spelled in a different enum, no extra safety.

Every detector helper carries a syntax-discovery-only comment at its definition.

What’s identity-sensitive (typed IDs)

Decisions that depend on which fn / type / ctor a name refers to (not just “does this name appear”) MUST go through SymbolTable or ProofIR.refined_types (TypeId-keyed) / ProofIR.fn_contracts (FnId-keyed). Examples:

• Refinement-carrier lookups go through find_refined_type / resolve_refined_type_in_with_key, both of which canonicalise the name through the symbol table before reaching the IR map.
• Fn-contract lookups go through find_fn_contract_for_fn — pointer-eq scope on &FnDef resolves to the right FnId.
• The Lean native-guarded rewriter pins target by FnId via rewrite_native_guarded_calls_resolved_expr (PR 169).

What stays raw-AST as a documented identity exception

Builtin matchers (callee_is X for X ∈ {"Bool.and", "Map.set", …}) compare against the canonical builtin namespace, which is global by spec — no per-scope identity to leak. Verify-law callsites all walk vb.fn_name (entry-only by parser grammar); the EntryFnIndex newtype in verify_law.rs pins the entry-only contract at the type level (PR 177).

Full ResolvedProofLowerView + semantic matcher API (callee_is_builtin, callee_is_fn(FnId), ctor_is, ident_name, int_lit) deferred per project_phase_e_scope_b_deferred memory until a real trigger lands (module-scoped verify, dotted law targets, LSP rename, cross-scope inliner).

Structs

ProofLowerInputs

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.

Functions

lower

Run every proof-export lowering in one shot — convenience for callers that want a fully-populated ProofIR. The pipeline calls the three populate_* fns directly so it can run them as independent stages and short-circuit on typecheck failure.

populate_fn_contracts

Walk analyze_plans(inputs) and populate ProofIR.fn_contracts.

populate_law_theorems

Walk every verify block, lift VerifyKind::Law entries into ProofIR.law_theorems.

populate_refined_types

Refinement-via-opaque lift. Walks every type definition (entry + dep modules), classifies the records that pair a single carrier field with a validating smart constructor, and emits RefinedTypeDecl entries into ir.refined_types. Backends (Lean → Subtype, Dafny → subset type) render these directly.