Module proof_lower

Expand description

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§

carrier_eligibility_demotions: ETAP-2 carrier-i64 SLICE 2b FOLLOW-UP: the fail-closed eligibility tightening. The bare carrier interval (carrier_interval_table) proves only that the smart-constructor’s invariant fits_i64; it does NOT prove that every value of the carrier type actually went through that gate, nor that the carrier’s codegen is exercised only in positions the i64 erasure supports. This scan removes a carrier from the eligible set when either assumption is violated, so the carrier stays boxed ($AverInt) — the safe, pre-slice representation that the VM and the boxed wasm-gc path agree on.
carrier_interval_table: ETAP-2 SLICE 0+1: derive, per refinement-via-opaque type in scope, the constant interval its smart-constructor invariant proves over the carrier. The table is keyed by the opaque type’s bare Aver name (e.g. "IntRange"). The bare-i64 MIR pass matches a carrier parameter/local/return slot against this key — it extracts the bare name from the slot’s MirParam.ty (which the lowerer fills with the Debug form Named { id: …, name: "IntRange" }, NOT the bare name; see bare_named_type in bare_i64) and seeds the slot with the proven bound.
field_carrier_eligible_intervals: ETAP-2 multi-field carrier-i64: the per-(record, field) ELIGIBLE map — field_carrier_interval_table tightened the same way the single-field path tightens its proven-bound set. An entry survives only when its bound is recognized AND fits_i64 AND the owning record is NOT demoted by any whole-program scan ([multi_field_record_demotions]):
field_carrier_interval_table: ETAP-2 multi-field carrier-i64: derive, per (record-type, Int-field) pair in scope, the constant interval a MULTI-ARG smart constructor’s guard proves over that field. This generalizes carrier_interval_table from the single-value-field carrier TYPE to a multi-field record whose 2+-arg smart constructor bounds each field independently.
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.