aver-lang 0.26.0

/// Heuristics for auto-proving `verify law` theorems in Lean output.
///
/// This module is intentionally isolated from `toplevel.rs` so all heuristic
/// matching and proof-shape logic lives in one place.
mod decimal;
mod floor_window;
mod induction;
mod sampled;
mod shared;
mod spec;
mod suffix_roundtrip;

use super::VerifyEmitMode;
use super::expr::aver_name_to_lean;
use super::recursive_pure_fn_names;
use crate::ast::{VerifyBlock, VerifyLaw};
use crate::codegen::CodegenContext;
use crate::verify_law::{collect_missing_helper_law_hints, missing_helper_law_message};
use sampled::emit_guarded_domain_law;

/// Cross-file law pool — EMIT-side gate (re-exported for `transpile`):
/// the `(module_prefix, theorem_base)` dep-law theorems some consumer law
/// admits, so the emitter writes ONLY those into the build.
pub(crate) use induction::admitted_dep_law_theorems;

/// `emit_verify_law_block` reads this to decide whether a `when`-law's theorem
/// statement should drop its sampled-domain disjunctions (`omit_domain`) and be
/// emitted in TRUE-universal form — exactly when the conditional
/// comparison-bridge emit will close it. Re-exported so the statement builder
/// and the proof emitter stay in lockstep.
pub(in crate::codegen::lean) use induction::recognize_conditional_comparison_bridge;

/// Generic conditional-inductive close (the decomposition path: list induction
/// threading the premise, then `simp_all` over the fn defs and the laws-as-
/// lemmas pool). Also feeds the `omit_domain` statement driver, kept in
/// lockstep with the emit.
pub(in crate::codegen::lean) use induction::recognize_conditional_inductive_generic;

/// `aver proof --explain` residual probe: turn an emitted main law theorem's
/// source lines into a normalization-only twin so Lean reports its residual
/// (`unsolved goals`). Re-exported up to `codegen::lean` for the `--check`
/// harness in the `aver` binary; see [`induction::residual_probe_body`].
pub use induction::residual_probe_body;

pub struct AutoProof {
    pub support_lines: Vec<String>,
    /// The proof body as a structured tactic tree (`:= by` block). Built by
    /// each rung; rendered to lines by the consumer. Proofs not yet structured
    /// into `First` portfolios wrap their lines via [`tactic_ir::Tactic::raw`]
    /// (a no-op on output). `--minimize` collapses the `First` nodes here.
    pub body: super::tactic_ir::Tactic,
    /// When true, the main theorem statement is already included in `support_lines`
    /// and should not be emitted separately by the caller.
    pub replaces_theorem: bool,
}

/// Look up the strategy `proof_lower::populate_law_theorems` pinned
/// on `(fn_name, law_name)`. Returns `None` when no contract was
/// lowered (LawLower disabled or the verify block wasn't a Law).
fn law_strategy_for(
    ctx: &CodegenContext,
    fn_name: &str,
    law_name: &str,
) -> Option<crate::ir::ProofStrategy> {
    // Scope-aware: a dep module's law is keyed by its dep-scope `FnId`
    // (cross-file law pool), so resolve `fn_name` through the active
    // module scope rather than assuming entry.
    let fn_id = ctx.law_target_fn_id(fn_name)?;
    ctx.proof_ir
        .law_theorems
        .iter()
        .find(|t| t.fn_id == fn_id && t.law_name == law_name)
        .map(|t| t.strategy.clone())
}

pub fn emit_verify_law_forall_auto_proof(
    vb: &VerifyBlock,
    law: &VerifyLaw,
    ctx: &CodegenContext,
    verify_mode: VerifyEmitMode,
    theorem_base: &str,
    quant_params: &str,
    theorem_prop: &str,
) -> Option<AutoProof> {
    let inner = emit_verify_law_forall_auto_proof_inner(
        vb,
        law,
        ctx,
        verify_mode,
        theorem_base,
        quant_params,
        theorem_prop,
    )?;
    // ADDITIVE, SHAPE-GATED `grind` outright-closer rung — prepended at
    // the TOP of the ladder, but ONLY for laws whose goal is
    // grind-amenable (algebraic / ring / order / comparison identity, NOT
    // a structural-induction theorem). `grind` (Lean 4.31 core, no
    // Mathlib) is a saturation solver with commutative-ring (+ring), AC,
    // and order/linarith subsolvers — it closes flat arithmetic goals
    // (like the nonlinear NR polynomial identity in nr_wall) WITHOUT
    // induction, but it CANNOT perform the structural induction the
    // recursive monoid/order laws (append-assoc, rev-involution,
    // count-rev) require. Emitting it on those inductive goals only burns
    // ~1.2s per proof for a guaranteed fall-through. The rung is admitted
    // iff BOTH gates pass: the SHAPE gate (`grind_is_shape_amenable` — the
    // law's unfold cone has NO user-recursive pure fn the proof would
    // induct over) AND the FRONTIER gate (the proof ends in an honest
    // `sorry`, so grind can do NEW work — guaranteed closers like
    // `omega`/`rfl` are left byte-identical).
    Some(maybe_wrap_with_grind_rung(vb, law, ctx, inner))
}

/// Whether the additive `grind` rung is SHAPE-AMENABLE for this law:
/// the goal is a flat algebraic / ring / order / comparison identity
/// that `grind`'s quantifier-free ring/AC/order subsolvers can close
/// outright, NOT a structural-induction theorem over a user-recursive
/// def (which needs `induction`/`fun_induction` first — something
/// `grind` does not perform).
///
/// The discriminating signal is the law's unfold cone (`law_simp_defs`,
/// the same transitively-reached pure-fn set the simp rungs source)
/// intersected with `recursive_pure_fn_names` (the recursion classifier's
/// set of user-recursive pure fns). When the cone touches ANY recursive
/// pure fn, the law routes to the structural-induction path
/// (`mk_arms`/list-induction/`fun_induction`) and `grind` cannot close
/// it — SKIP. When the cone is entirely non-recursive, the goal is flat
/// arithmetic/ring (like `nrNewErrNum = nrOldErrSq`) — ADMIT.
///
/// Also requires a non-empty cone: a law with no user fns in its cone is
/// a pure builtin/arith goal the existing IR-pinned rungs (omega /
/// RingIdentity) already own; a bare `grind` adds nothing there.
fn grind_is_shape_amenable(ctx: &CodegenContext, vb: &VerifyBlock, law: &VerifyLaw) -> bool {
    // Cone by SOURCE name (pre-`aver_name_to_lean`), so it can be matched
    // directly against `recursive_pure_fn_names`' bare source names.
    let cone = shared::law_simp_source_names(ctx, vb, law);
    if cone.is_empty() {
        return false;
    }
    let recursive = recursive_pure_fn_names(ctx);
    // A user-recursive pure fn anywhere in the cone => the law inducts;
    // `grind` cannot close it. Skip the rung (no waste on inductive goals).
    !cone.iter().any(|name| recursive.contains(name))
}

/// Wrap an already-emitted [`AutoProof`] with the additive top-of-ladder
/// `grind` rung when the law is shape-amenable (see
/// [`grind_is_shape_amenable`]) AND the proof body has the canonical
/// `intro <givens>; <body>` shape. Returns the proof unchanged otherwise
/// — the rung is purely additive (a non-closing `grind` ends in `done`
/// and `first` falls through to the existing body byte-for-byte).
fn maybe_wrap_with_grind_rung(
    vb: &VerifyBlock,
    law: &VerifyLaw,
    ctx: &CodegenContext,
    proof: AutoProof,
) -> AutoProof {
    // `replaces_theorem` proofs carry their OWN theorem statement +
    // bespoke support stack (RingIdentity, floor-window, decimal /
    // string roundtrips) — there is no plain `intro <givens>; <tactic>`
    // body to prepend a `grind` arm onto, and the RingIdentity family
    // already runs `grind` internally. Leave them untouched.
    if proof.replaces_theorem {
        return proof;
    }
    // A `when`-premised law introduces extra hypotheses (`h_when`, …)
    // whose Subtype/`by_cases` handling the existing rungs are written
    // around; a bare `grind` over the premise shape risks an
    // introduced-but-unused hypothesis stall. The plain unconditional
    // laws are exactly grind's wheelhouse, so restrict the rung to them.
    if law.when.is_some() {
        return proof;
    }
    // A proof body that ALREADY leads with `grind` owns its own grind
    // rung (the `RingIdentity` family emits `first | (grind [<cone>]; …`
    // internally). Re-wrapping it would emit a redundant outer `grind`
    // arm — pure waste (a second grind saturation on the same goal). Skip.
    let lines = proof.body.render();
    if lines.iter().any(|l| l.contains("grind")) {
        return proof;
    }
    // SHAPE GATE: only wrap a grind-amenable (flat algebraic/ring/order)
    // goal — never an inductive law over a user-recursive def.
    if !grind_is_shape_amenable(ctx, vb, law) {
        return proof;
    }
    // FRONTIER GATE: only wrap a proof whose body ends in an honest
    // `sorry` floor (a `first | … | sorry` fallback that might NOT
    // close). A proof with a GUARANTEED closer (no trailing `sorry`: the
    // IR-pinned `Reflexive`/`Commutative`/`LinearArithmetic`/… rungs that
    // end in `rfl`/`omega`/`simp …`) already closes cheaply and reliably;
    // prepending `grind` there only (a) churns the byte-for-byte golden
    // exports for zero benefit and (b) risks running `grind` to a
    // potential `maxHeartbeats` build error `first` cannot catch on a goal
    // `omega` decides instantly. The shape gate already restricts to flat
    // goals; pairing it with the frontier gate means `grind` is emitted
    // ONLY where it can do NEW work — exactly the open flat laws (like the
    // nonlinear ring identity the simp package no longer normalizes).
    let ends_in_sorry = lines
        .iter()
        .rev()
        .find(|l| !l.trim().is_empty())
        .is_some_and(|l| l.trim_end().ends_with("sorry") || l.trim_end().ends_with("sorry)"));
    if !ends_in_sorry {
        return proof;
    }
    // The proof must be the canonical `intro <givens>` + body shape
    // (the first proof line, post-indent, is the `intro`). Anything
    // else is left as-is rather than guessing where to splice the arm.
    let Some(first_line) = lines.first() else {
        return proof;
    };
    if !first_line.trim_start().starts_with("intro ") {
        return proof;
    }
    // The unfold cone (Lean names, law subject first) the same way the
    // simp rungs source it. `grind` does NOT unfold user `def`s on its
    // own (the same lesson as the RingIdentity rung), so it is handed the
    // cone as `grind [<cone>]`. The shape gate already guaranteed a
    // non-empty, recursion-free cone.
    let cone: Vec<String> = shared::law_simp_defs(ctx, vb, law).into_iter().collect();
    if cone.is_empty() {
        return proof;
    }
    // Structured grind rung:
    //
    // ```text
    // intro <givens>
    // first
    // | (grind [<cone>]; done)
    // | (<existing body>)
    // ```
    //
    // Built as a real [`tactic_ir::Tactic::First`] (not a flattened string) so
    // `--minimize` can collapse it to its winning branch — almost always the
    // existing body, since `grind` is a shape-gated frontier closer admitted
    // only where the body already ends in an honest `sorry`. The `grind` arm
    // ends in `done`, so a `grind` that leaves a residual goal THROWS and
    // `first` falls to the existing body; the rung is purely additive and adds
    // no axioms beyond grind's whitelisted set ({propext, Classical.choice,
    // Quot.sound}).
    //
    // The body branch keeps the EXISTING body tree (intro removed) rather than
    // its rendered string, so a structured inner portfolio (a converted
    // `first | … | sorry`) stays a real `First` the minimizer can also collapse
    // — not flattened back to opaque text. Render is byte-identical either way
    // (the inner `First` prints inline). The intro-shape gate above guarantees
    // step 0 of the body sequence is the `intro`.
    use crate::codegen::lean::tactic_ir::Tactic;
    let support_lines = proof.support_lines;
    let body = match proof.body {
        Tactic::Seq(mut steps) if !steps.is_empty() => {
            let intro = steps.remove(0);
            Tactic::Seq(vec![
                Tactic::Leaf(intro.render().join("\n").trim().to_string()),
                Tactic::First(vec![
                    Tactic::Leaf(format!("grind [{}]; done", cone.join(", "))),
                    Tactic::Seq(steps),
                ]),
            ])
        }
        // A non-sequence body is unreachable given the intro-shape gate; leave
        // it untouched rather than guess where the `grind` arm would splice.
        other => other,
    };
    AutoProof {
        support_lines,
        body,
        replaces_theorem: false,
    }
}

fn emit_verify_law_forall_auto_proof_inner(
    vb: &VerifyBlock,
    law: &VerifyLaw,
    ctx: &CodegenContext,
    verify_mode: VerifyEmitMode,
    theorem_base: &str,
    quant_params: &str,
    theorem_prop: &str,
) -> Option<AutoProof> {
    if verify_mode != VerifyEmitMode::NativeDecide {
        return None;
    }

    let intro_names: Vec<String> = law
        .givens
        .iter()
        .map(|g| aver_name_to_lean(&g.name))
        .collect();
    let proof_intro_names = extend_intro_names_with_premises(law, &intro_names);

    // Conditional comparison-bridge laws (the `prop_70 leSucc` family):
    // `when <R1(..)> -> <R2(..)> = true` over canonical Peano relations
    // (`≤`/`<`/`=`). Tried BEFORE the pinned-strategy dispatch because
    // `classify_law_strategy` never pins `Induction` on a `when`-law (it routes
    // them to `LinearArithmetic` / `BackendDispatch`), so this is the only point
    // a conditional law reaches a genuine universal closer. For exactly this
    // recognized shape `emit_verify_law_block` emits the unbounded
    // `∀ givens, when = true -> claim` statement (see
    // `recognize_conditional_comparison_bridge`); every other conditional shape
    // declines here and falls through to the bounded guarded-domain proof.
    if law.when.is_some()
        && let Some(proof) =
            induction::emit_conditional_comparison_bridge_law(vb, law, ctx, &intro_names)
    {
        return Some(proof);
    }

    // Generic conditional-inductive close: any `when`-law that recurses on a
    // list given with an equational conclusion, proved by list induction +
    // premise threading + `simp_all` over the fn defs AND the laws-as-lemmas
    // pool (earlier `verify ... law` helper blocks). This is the DECOMPOSITION
    // path — a figure's algebraic content (e.g. zip-reverse's snoc-distribution)
    // lives as Aver helper laws, not a hardcoded Lean template. Tried last among
    // the conditional arms; the bespoke recognizers above decline into it.
    if law.when.is_some()
        && let Some(proof) =
            induction::emit_conditional_inductive_generic_law(vb, law, ctx, &intro_names)
    {
        return Some(proof);
    }

    // Structural induction — IR-pinned `ProofStrategy::Induction`
    // wins first. The legacy chain ran induction at this position
    // unconditionally; the IR-pin path keeps that priority while
    // making the decision visible in `proof_ir.law_theorems`.
    // Falls through to the legacy emit_structural_induction_law
    // (still called for BackendDispatch laws that the lowerer
    // hasn't classified — shouldn't trigger for canonical recursive-
    // ADT shapes after Step 31).
    //
    // `SimpOverLemmas(names)` (the discovery feedback loop — the CLI
    // re-pins an `Induction` law when committed discovered lemmas are
    // in-scope) routes to the SAME induction emit with the lemma
    // names threaded through: the emit embeds the lemma texts, adds
    // the names to the simp sets, and tries a lemma-first fast path
    // before inducting.
    let pinned = law_strategy_for(ctx, &vb.fn_name, &law.name);
    let discovered: Vec<String> = match &pinned {
        Some(crate::ir::ProofStrategy::SimpOverLemmas(names)) => names.clone(),
        _ => Vec::new(),
    };
    if matches!(
        pinned,
        Some(crate::ir::ProofStrategy::Induction { .. })
            | Some(crate::ir::ProofStrategy::SimpOverLemmas(_))
    ) && let Some(proof) = induction::emit_structural_induction_law(
        vb,
        law,
        ctx,
        &intro_names,
        theorem_base,
        quant_params,
        theorem_prop,
        &discovered,
    ) {
        return Some(proof);
    }
    // IR-pinned `FloorDivWindow` — the floor-division window family.
    // The renderer emits a self-contained support stack (power
    // algebra by functional induction, the binary-exponent window
    // characterization, the core ediv bridges) plus the law theorem
    // in TRUE universal form, so it replaces the bounded statement
    // entirely (`replaces_theorem`). The caller's law-class marker
    // recognizes the pin and classes the statement `universal`;
    // crediting stays fail-closed behind the `#print axioms`
    // whitelist.
    if let Some(proof) =
        floor_window::emit_floor_window_law(vb, law, ctx, theorem_base, quant_params)
    {
        return Some(proof);
    }
    // IR-pinned `TailRecFixedBaseFold` (TIP prop_35, `exp x y = qexp x y one`).
    // Like `FloorDivWindow`, it renders its own TRUE-universal statement plus the
    // accumulator-generalization support lemma (`replaces_theorem`); the caller's
    // law-class marker classes it `universal`, fail-closed behind `#print axioms`.
    if let Some(crate::ir::ProofStrategy::TailRecFixedBaseFold {
        spec_fn,
        loop_fn,
        combine_fn,
        combine_op,
        ..
    }) = law_strategy_for(ctx, &vb.fn_name, &law.name)
        && let Some(proof) = spec::emit_tailrec_fixed_base_fold_law(
            law,
            ctx,
            theorem_base,
            &spec_fn,
            &loop_fn,
            &combine_fn,
            combine_op,
        )
    {
        return Some(proof);
    }
    // IR-pinned strategies. The lowerer's decision wins over the
    // ad-hoc detection chain that follows; backend just renders the
    // tactic the IR selected. Each variant has a fixed Lean shape;
    // the IR's `BinOp` payload maps to a specific lemma name here.
    if let Some(strategy) = law_strategy_for(ctx, &vb.fn_name, &law.name) {
        use crate::ast::BinOp;
        use crate::ir::ProofStrategy;
        let fn_lean = aver_name_to_lean(&vb.fn_name);
        let proof_lines = match strategy {
            ProofStrategy::Reflexive => Some(vec!["rfl".to_string()]),
            ProofStrategy::Commutative { op } => match op {
                BinOp::Add => Some(vec![format!("simp [{}, Int.add_comm]", fn_lean)]),
                BinOp::Mul => Some(vec![format!("simp [{}, Int.mul_comm]", fn_lean)]),
                _ => None,
            },
            ProofStrategy::Associative { op } => match op {
                BinOp::Add => Some(vec![format!("simp [{}, Int.add_assoc]", fn_lean)]),
                BinOp::Mul => Some(vec![format!("simp [{}, Int.mul_assoc]", fn_lean)]),
                _ => None,
            },
            ProofStrategy::IdentityElement { .. } => {
                // Add → `simp [fn]` collapses `a + 0` / `0 + a`;
                // Mul → same against `a * 1` / `1 * a`; Sub →
                // `simp [fn]` reduces `a - 0` to `a` (one-sided —
                // detector enforces shape). Op-agnostic emit:
                // unfold the wrapper and simp closes via Lean's
                // built-in identity lemmas.
                Some(vec![format!("simp [{}]", fn_lean)])
            }
            ProofStrategy::UnaryEqualsBinary { ref inner_fn } => {
                // `outer(a) = inner(a, K)` (or `inner(K, a)`) —
                // simp unfolds both fns to the same underlying op
                // expression on each side.
                Some(vec![format!(
                    "simp [{}, {}]",
                    fn_lean,
                    aver_name_to_lean(inner_fn)
                )])
            }
            ProofStrategy::AntiCommutative { neg_on_rhs, .. } => {
                // `Int.neg_sub b a : -(b - a) = a - b`. `.symm` flip
                // when the user's law puts the negation on rhs.
                let a = aver_name_to_lean(&law.givens[0].name);
                let b = aver_name_to_lean(&law.givens[1].name);
                let step = if neg_on_rhs {
                    format!("simpa [{}] using (Int.neg_sub {} {}).symm", fn_lean, b, a)
                } else {
                    format!("simpa [{}] using (Int.neg_sub {} {})", fn_lean, b, a)
                };
                Some(vec![step])
            }
            // LinearArithmetic runs at its position in the chain
            // (below spec_equivalence + maps) — falls through here
            // and emits in the dedicated arm further down.
            ProofStrategy::LinearArithmetic { .. } => None,
            _ => None,
        };
        if let Some(lines) = proof_lines {
            return Some(AutoProof {
                support_lines: Vec::new(),
                body: crate::codegen::lean::tactic_ir::Tactic::raw(intro_then(
                    &proof_intro_names,
                    lines,
                )),
                replaces_theorem: false,
            });
        }
    }

    // IR-pinned `SpecEquivalence` — the lowerer validated impl and
    // spec fns have syntactically-identical bodies; backend closes
    // via `simpa [<unfolds>]` (impl + spec + transitively-reached
    // helpers). Falls through to the legacy spec dispatch when IR
    // didn't pin (other spec sub-shapes are still backend-driven).
    if let Some(crate::ir::ProofStrategy::SpecEquivalence { ref extra_unfolds }) =
        law_strategy_for(ctx, &vb.fn_name, &law.name)
    {
        let lean_names: Vec<String> = extra_unfolds.iter().map(|n| aver_name_to_lean(n)).collect();
        return Some(AutoProof {
            support_lines: Vec::new(),
            body: crate::codegen::lean::tactic_ir::Tactic::raw(intro_then(
                &proof_intro_names,
                vec![format!("simpa [{}]", lean_names.join(", "))],
            )),
            replaces_theorem: false,
        });
    }

    // IR-pinned `EnumConstantFold` — the lowerer validated the law
    // pins every non-Int param to a constructor literal and the call
    // tree is non-recursive, so the goal is a ground equality. Unfold
    // the fn + transitively-reached callees with `simp only`, then
    // close each residual branch with a `split`/`rfl`/`decide` cascade.
    // The `first | ... ` tries the cheapest closer first; the kernel
    // re-checks whichever fires, and a goal the cascade can't close
    // surfaces honestly (the law would then need a hand proof) rather
    // than a false `sorry`-free claim.
    if let Some(crate::ir::ProofStrategy::EnumConstantFold { ref unfold_fns }) =
        law_strategy_for(ctx, &vb.fn_name, &law.name)
    {
        let lean_names: Vec<String> = unfold_fns.iter().map(|n| aver_name_to_lean(n)).collect();
        return Some(AutoProof {
            support_lines: Vec::new(),
            body: crate::codegen::lean::tactic_ir::Tactic::raw(intro_then(
                &proof_intro_names,
                vec![format!(
                    "simp only [{}] <;> (first | (split <;> rfl) | rfl | decide)",
                    lean_names.join(", ")
                )],
            )),
            replaces_theorem: false,
        });
    }

    // IR-pinned `FiniteDomainCases` — every given ranges over a closed
    // finite domain (Bool or an all-fieldless user enum, ≤ 16 total
    // combinations), so exhaustive `cases` enumeration yields one
    // closed ground goal per combination. Fuel-wrapped callees compute
    // through (constant-measure constructor args), which is why the
    // detector has no call-shape / recursion gate. Per-leaf cascade:
    // `rfl` first (the workhorse — kernel defeq computes ground
    // terms), then `decide` (kernel-rechecked; can be weak on derived
    // DecidableEq over nested ADTs), then the iron guard — an HONEST
    // `sorry`. A non-closing leaf must surface as a caught sorry,
    // NEVER a build error and NEVER `native_decide` (which would
    // inject `Lean.ofReduceBool` and silently kill `universal:true`).
    if let Some(crate::ir::ProofStrategy::FiniteDomainCases { ref givens }) =
        law_strategy_for(ctx, &vb.fn_name, &law.name)
    {
        let cascade = givens
            .iter()
            .map(|g| format!("cases {}", aver_name_to_lean(g)))
            .collect::<Vec<_>>()
            .join(" <;> ");
        return Some(AutoProof {
            support_lines: Vec::new(),
            body: crate::codegen::lean::tactic_ir::Tactic::raw(intro_then(
                &proof_intro_names,
                vec![format!("{cascade} <;> (first | rfl | decide | sorry)")],
            )),
            replaces_theorem: false,
        });
    }

    // IR-pinned `IntDecimalRoundtrip` — the lowerer validated the
    // ENTIRE canonical decimal-parser shape (head-char dispatch arms,
    // single recognized string-pos scanner with the synthesized
    // `__fuel_scan` companion, slice + `Int.fromString` leaf), so the
    // backend renders the fixed sign-split skeleton ported from the
    // verified json hand proof. Wrapped in `first | (…; done) | sorry`
    // — a non-closing case degrades to a caught honest sorry.
    if let Some(crate::ir::ProofStrategy::IntDecimalRoundtrip {
        ref parse_fn,
        ref neg_fn,
        ref pos_fn,
        ref sign_fn,
        ref scanner_fn,
        ref predicate_fn,
        ref finish_fn,
        ref finish_int_fn,
        ref serializer_fn,
    }) = law_strategy_for(ctx, &vb.fn_name, &law.name)
        && let Some(proof) = decimal::emit_int_decimal_roundtrip_law(
            law,
            ctx,
            theorem_base,
            parse_fn,
            neg_fn,
            pos_fn,
            sign_fn,
            scanner_fn,
            predicate_fn,
            finish_fn,
            finish_int_fn,
            serializer_fn,
        )
    {
        return Some(proof);
    }

    // IR-pinned `StringEscapeRoundtrip` — the lowerer validated the
    // ENTIRE escaped-string roundtrip pair (scanner SCC arm shapes,
    // producer classifier table aligned with the consumer's escape
    // dispatcher, control-escape prefix, threshold agreement), so the
    // backend renders the suffix-invariant proof skeleton ported from
    // the verified json hand proof. Every synthesized lemma and the
    // law proof itself carry `first | (…; done) | sorry` floors — a
    // non-closing template degrades to caught honest sorries, never a
    // build error.
    if let Some(crate::ir::ProofStrategy::StringEscapeRoundtrip(ref pin)) =
        law_strategy_for(ctx, &vb.fn_name, &law.name)
        && let Some(proof) =
            suffix_roundtrip::emit_string_escape_roundtrip_law(law, ctx, theorem_base, pin)
    {
        return Some(proof);
    }

    // IR-pinned `LinearIntSpecEquivalence` — Step 40: lowerer
    // validated substituted bodies are pure linear arithmetic over
    // Int givens. Backend emits `change <impl> = <spec> ; omega`.
    if let Some(crate::ir::ProofStrategy::LinearIntSpecEquivalence {
        ref unfolded_impl,
        ref unfolded_spec,
    }) = law_strategy_for(ctx, &vb.fn_name, &law.name)
    {
        return Some(AutoProof {
            support_lines: Vec::new(),
            body: crate::codegen::lean::tactic_ir::Tactic::raw(intro_then(
                &proof_intro_names,
                vec![
                    format!(
                        "change {} = {}",
                        super::expr::emit_expr(unfolded_impl, ctx),
                        super::expr::emit_expr(unfolded_spec, ctx)
                    ),
                    "omega".to_string(),
                ],
            )),
            replaces_theorem: false,
        });
    }

    // IR-pinned `SpecEquivalenceSimpNormalized` — Step 39 broaden:
    // impl and spec bodies aren't syntactically identical but
    // normalize to the same expression under arg substitution +
    // algebraic identity folding (`a + 0`, `a * 1`, `a * 0`).
    // Backend closes via `simp [<unfolds>]`; the simp normalization
    // discharges the residual arithmetic identities.
    if let Some(crate::ir::ProofStrategy::SpecEquivalenceSimpNormalized { ref extra_unfolds }) =
        law_strategy_for(ctx, &vb.fn_name, &law.name)
    {
        let lean_names: Vec<String> = extra_unfolds.iter().map(|n| aver_name_to_lean(n)).collect();
        return Some(AutoProof {
            support_lines: Vec::new(),
            body: crate::codegen::lean::tactic_ir::Tactic::raw(intro_then(
                &proof_intro_names,
                vec![format!("simp [{}]", lean_names.join(", "))],
            )),
            replaces_theorem: false,
        });
    }

    // IR-pinned `EffectfulSpecEquivalence` — Oracle Lift normalised
    // both sides; lowerer matched the canonical `impl(args) ==
    // spec(args)` shape post-rewrite. Backend emits `simp [impl,
    // spec]`; both definitions unfold to the same oracle call.
    if let Some(crate::ir::ProofStrategy::EffectfulSpecEquivalence {
        ref impl_fn,
        ref spec_fn,
    }) = law_strategy_for(ctx, &vb.fn_name, &law.name)
    {
        return Some(AutoProof {
            support_lines: Vec::new(),
            body: crate::codegen::lean::tactic_ir::Tactic::raw(intro_then(
                &proof_intro_names,
                vec![format!(
                    "simp [{}, {}]",
                    aver_name_to_lean(impl_fn),
                    aver_name_to_lean(spec_fn)
                )],
            )),
            replaces_theorem: false,
        });
    }

    // IR-pinned `LinearRecurrence2SpecEquivalence` — lowerer
    // validated impl as tail-rec wrapper, spec as direct second-order
    // recurrence, helper as their shared affine worker. Dispatches
    // to the existing emit which renders the Nat-helper + shift
    // lemma + helper-seed bridge (heavy ~50-line support_lines stay
    // in the legacy module). The IR pin makes the algebraic decision
    // observable in `proof_ir.law_theorems` and provides the integration
    // point for a future Dafny consumer (issue #116).
    if matches!(
        law_strategy_for(ctx, &vb.fn_name, &law.name),
        Some(crate::ir::ProofStrategy::LinearRecurrence2SpecEquivalence { .. })
    ) && let Some(proof) = spec::emit_second_order_linear_recurrence_spec_equivalence_law(
        vb,
        law,
        ctx,
        &proof_intro_names,
    ) {
        return Some(proof);
    }

    // Stage 8b of #232 — `ResultPipelineChain`. Unfold both fns +
    // every step fn, then `repeat split` peels off match layers
    // until structural equality remains.
    if let Some(crate::ir::ProofStrategy::ResultPipelineChain {
        chain_qm_fn,
        chain_manual_fn,
        step_fns,
    }) = law_strategy_for(ctx, &vb.fn_name, &law.name)
        && let Some(proof) = spec::emit_result_pipeline_chain_law(
            vb,
            law,
            ctx,
            &chain_qm_fn,
            &chain_manual_fn,
            &step_fns,
        )
    {
        return Some(proof);
    }

    // Stage 8 of #232 — `WrapperOverRecursion` support stack.
    // Aux acc-decomposition lemma + main universal lemma. The `List`-fold
    // additive case closes in core Lean 4 (`omega`); the Peano-`Nat`
    // multiplicative case (`factTR`) bridges the user monoid fn to `Nat.*`
    // and closes with the core `Nat.mul_*` lemmas — still no Mathlib.
    if let Some(crate::ir::ProofStrategy::WrapperOverRecursion {
        wrapper_fn,
        inner_fn,
        other_fn,
        combine_op,
        driver,
        combine_fn,
    }) = law_strategy_for(ctx, &vb.fn_name, &law.name)
        && let Some(proof) = spec::emit_wrapper_over_recursion_law(
            vb,
            law,
            ctx,
            &wrapper_fn,
            &inner_fn,
            &other_fn,
            combine_op,
            &driver,
            combine_fn.as_deref(),
        )
    {
        return Some(proof);
    }

    spec::emit_spec_function_equivalence_law(vb, law, ctx, &proof_intro_names)
        .or_else(|| {
            // IR-pinned Map library axiom (has_set_self / get_set_self).
            // The lowerer detected the canonical shape and captured the
            // (m, k, v) args; backend just renders the Lean simpa.
            if let Some(crate::ir::ProofStrategy::LibraryAxiom {
                ref axiom,
                ref args,
            }) = law_strategy_for(ctx, &vb.fn_name, &law.name)
                && matches!(axiom.as_str(), "Map.has_set_self" | "Map.get_set_self")
                && args.len() == 3
            {
                let lemma = match axiom.as_str() {
                    "Map.has_set_self" => "AverMap.has_set_self",
                    "Map.get_set_self" => "AverMap.get_set_self",
                    _ => unreachable!(),
                };
                let atom_arg = |e: &crate::ast::Spanned<crate::ir::hir::ResolvedExpr>| {
                    let rendered = super::expr::emit_expr(e, ctx);
                    if rendered.contains(' ') && !rendered.starts_with('(') {
                        format!("({rendered})")
                    } else {
                        rendered
                    }
                };
                return Some(AutoProof {
                    support_lines: Vec::new(),
                    body: crate::codegen::lean::tactic_ir::Tactic::raw(intro_then(
                        &proof_intro_names,
                        vec![format!(
                            "simpa using {} {} {} {}",
                            lemma,
                            atom_arg(&args[0]),
                            atom_arg(&args[1]),
                            atom_arg(&args[2]),
                        )],
                    )),
                    replaces_theorem: false,
                });
            }
            None
        })
        .or_else(|| {
            // IR-pinned `MapUpdatePostcondition` — the lowerer
            // validated the outer fn's "inspect get, set in every
            // arm" body shape and captured the law's (map, key)
            // args + the helper-fn unfold set. Backend renders the
            // 2-line `simp [outer (, extras)] ; cases h : AverMap.get
            // m k <;> simp [AverMap.<axiom> (, extras)]` tactic.
            if let Some(crate::ir::ProofStrategy::MapUpdatePostcondition {
                ref outer_fn,
                kind,
                ref map_arg,
                ref key_arg,
                ref extra_unfolds,
            }) = law_strategy_for(ctx, &vb.fn_name, &law.name)
            {
                let outer_lean = aver_name_to_lean(outer_fn);
                let extras_lean: Vec<String> =
                    extra_unfolds.iter().map(|n| aver_name_to_lean(n)).collect();
                let atom_render = |e: &crate::ast::Spanned<crate::ir::hir::ResolvedExpr>| {
                    let rendered = super::expr::emit_expr(e, ctx);
                    if rendered.contains(' ') && !rendered.starts_with('(') {
                        format!("({rendered})")
                    } else {
                        rendered
                    }
                };
                let (axiom_lemma, prefix_extras): (&str, Vec<String>) = match kind {
                    crate::ir::MapUpdatePostconditionKind::HasAfter => {
                        ("AverMap.has_set_self", Vec::new())
                    }
                    crate::ir::MapUpdatePostconditionKind::GetAfter => {
                        ("AverMap.get_set_self", extras_lean.clone())
                    }
                };
                let simp_first: String = {
                    let mut items = vec![outer_lean.clone()];
                    items.extend(prefix_extras);
                    format!("simp [{}]", items.join(", "))
                };
                let simp_second: String = {
                    let mut items = vec![axiom_lemma.to_string()];
                    if matches!(kind, crate::ir::MapUpdatePostconditionKind::GetAfter) {
                        items.push(outer_lean.clone());
                        items.extend(extras_lean.iter().cloned());
                    }
                    format!(
                        "cases h : AverMap.get {} {} <;> simp [{}]",
                        atom_render(map_arg),
                        atom_render(key_arg),
                        items.join(", ")
                    )
                };
                return Some(AutoProof {
                    support_lines: Vec::new(),
                    body: crate::codegen::lean::tactic_ir::Tactic::raw(intro_then(
                        &proof_intro_names,
                        vec![simp_first, simp_second],
                    )),
                    replaces_theorem: false,
                });
            }
            None
        })
        .or_else(|| {
            // IR-pinned `MapKeyTrackedIncrement` — the lowerer
            // validated the outer fn's "tracked counter" body
            // template (Some(n) -> n + 1, None -> 1) and matched the
            // law against the `Option.withDefault`-defaulted shape.
            // Backend renders the 2-line `simp [outer] ; cases h :
            // AverMap.get m k <;> simp [AverMap.get_set_self, h]`
            // tactic.
            if let Some(crate::ir::ProofStrategy::MapKeyTrackedIncrement {
                ref outer_fn,
                ref map_arg,
                ref key_arg,
            }) = law_strategy_for(ctx, &vb.fn_name, &law.name)
            {
                let outer_lean = aver_name_to_lean(outer_fn);
                let atom_render = |e: &crate::ast::Spanned<crate::ir::hir::ResolvedExpr>| {
                    let rendered = super::expr::emit_expr(e, ctx);
                    if rendered.contains(' ') && !rendered.starts_with('(') {
                        format!("({rendered})")
                    } else {
                        rendered
                    }
                };
                let lines = vec![
                    format!("simp [{}]", outer_lean),
                    format!(
                        "cases h : AverMap.get {} {} <;> simp [AverMap.get_set_self, h]",
                        atom_render(map_arg),
                        atom_render(key_arg),
                    ),
                ];
                return Some(AutoProof {
                    support_lines: Vec::new(),
                    body: crate::codegen::lean::tactic_ir::Tactic::raw(intro_then(
                        &proof_intro_names,
                        lines,
                    )),
                    replaces_theorem: false,
                });
            }
            None
        })
        .or_else(|| {
            // Pure builtin `Int.abs` identities (`Int.abs(Int.abs x) =
            // Int.abs x`, `Int.abs(x*y) = Int.abs x * Int.abs y`,
            // `Int.abs x >= 0 = true`). Placed BEFORE the LinearArithmetic
            // rung: idempotence/non-negativity otherwise route there and its
            // `simp only [cone] <;> omega` can't see through the `Int.natAbs`
            // cast (and, with no sorry floor, hard-fails the build), while the
            // `*`-distribution law falls through to a bare sorry. Dafny's Z3
            // proves all three. Shape-driven on `Int.abs` in the law sides, so
            // it leaves every non-abs LinearArithmetic law untouched.
            emit_int_abs_identity_law(law, &proof_intro_names)
        })
        .or_else(|| {
            // IR-pinned SimpOmegaUnfold takes precedence over the
            // legacy detection here — the lowerer already ran the
            // same shape check and captured `unfold_fns`,
            // `wrapper_return`, `smart_guard`. When the IR didn't
            // pin (BackendDispatch), fall through to the legacy
            // detector below.
            if let Some(crate::ir::ProofStrategy::LinearArithmetic {
                ref unfold_fns,
                wrapper_return,
                ref smart_guard,
                lifted,
            }) = law_strategy_for(ctx, &vb.fn_name, &law.name)
            {
                // `when`-premise + wrapper-return: DECLINE. The
                // sign-split `by_cases <;> simp` chain this arm
                // renders cannot consume a `when` premise (the
                // hypothesis is introduced but never used), and the
                // pre-fix emission even cased over the introduced
                // HYPOTHESIS names (`by_cases h_h_a : h_a >= 0` where
                // `h_a : Prop`) — an application-type-mismatch BUILD
                // ERROR, not a caught sorry. Falling through reaches
                // `emit_guarded_domain_law`, which closes the bounded
                // guarded statement by domain case-split +
                // `native_decide`.
                if wrapper_return && !lifted && law.when.is_some() {
                    return None;
                }
                // Lifted laws use base intro names — the Subtype
                // lift incorporates the `when` premise into the
                // theorem's quantifier types, so the user-side
                // hypotheses (`h_a`, `h_b`, `h_when`) aren't
                // available in the proof goal. Non-lifted paths
                // keep premise expansion for by_cases hypotheses.
                let chosen_intro: &[String] = if lifted {
                    &intro_names
                } else {
                    &proof_intro_names
                };
                let uses_max_min = linear_arith_uses_max_min(unfold_fns, ctx);
                return Some(AutoProof {
                    support_lines: Vec::new(),
                    body: emit_simp_omega_from_ir(
                        unfold_fns,
                        wrapper_return,
                        smart_guard.as_ref(),
                        lifted,
                        chosen_intro,
                        &intro_names,
                        law.when.is_some(),
                        uses_max_min,
                        ctx,
                    ),
                    replaces_theorem: false,
                });
            }
            None
        })
        .or_else(|| {
            emit_guarded_domain_law(law).map(|proof_lines| AutoProof {
                support_lines: Vec::new(),
                body: crate::codegen::lean::tactic_ir::Tactic::raw(proof_lines),
                replaces_theorem: false,
            })
        })
        .or_else(|| {
            // Pure builtin empty-map facts (`Map.get(empty, k) = None`,
            // `Map.has(empty, k) = false`, `Map.len(empty) = 0`). Placed
            // BEFORE the prelude rung: such a law is stated through its
            // subject fn (`getE(k) => None`), so `SimpOverPreludeLemmas`
            // claims it but its minimal `simp [cone, Int.add_sub_cancel]`
            // can't reduce the `AverMap.*` accessor and parks it on a sorry.
            // This rung's bounded `simp only [cone, AverMap.*, []-lemmas]`
            // closes it. The recognizer is empty-map-precise (the accessor's
            // map arg must be a `{}` literal or a const fn returning `{}`),
            // so it never steals a Map law the prelude rung could close.
            emit_map_empty_fact_law(vb, law, ctx, &proof_intro_names)
        })
        .or_else(|| {
            // `Map.len(Map.set(m, k, v)) >= 1 => true` — `set` always yields a
            // non-empty map. Unlike the empty-map facts this needs real
            // induction (`set.go` length is `>= 1`), so it leans on the
            // hand-proved prelude lemma `AverMap.len_set_ge_one` (stated in the
            // exact lowered goal shape); the rung just `exact`s it. Shape-driven
            // on the `Map.len(Map.set(…)) >= 1` lhs, so it claims nothing else.
            emit_map_len_set_positive_law(law, &proof_intro_names)
        })
        .or_else(|| {
            // IR-pinned `RingIdentity` — rendered (like the prelude
            // rung below) after every legacy ad-hoc fallback, so it
            // fires only where the chain used to fall through. The
            // emit carries the strategy-scoped AC-ring package; see
            // `emit_ring_identity_law`.
            emit_ring_identity_law(vb, law, ctx, &proof_intro_names)
        })
        .or_else(|| {
            // IR-pinned `SimpOverPreludeLemmas` — after every legacy
            // ad-hoc fallback above: it must fire only where the chain
            // used to return `None` and the caller emitted a
            // bare-`sorry` universal. The simp set is kept minimal
            // (cone + fuel + registry hits + the single baked-in
            // `Int.add_sub_cancel` rewrite the archived hand-proofs
            // needed) — a fat set risks a simp LOOP, and a
            // maxHeartbeats blow-up is a build error `first` cannot
            // catch. `done` forces closure: simp succeeding but
            // leaving a residual goal must fall to the honest `sorry`,
            // never surface as an "unsolved goals" build error.
            emit_simp_over_prelude_lemmas_law(vb, law, ctx, &proof_intro_names)
        })
        .or_else(|| {
            // Pure builtin String-length additivity (`String.len(a + b)
            // = String.len(a) + String.len(b)`). The law statement is
            // over builtins alone, so every cone-anchored rung above has
            // already declined and the strategy stayed `BackendDispatch`
            // — Dafny's Z3 already discharges the sequence-length axiom,
            // and this is the Lean-only twin that closes it instead of a
            // bare `sorry`. Shape-driven (not IR-pinned), so it fires
            // exactly where the cascade returned `None`.
            emit_string_length_additive_law(law, &proof_intro_names)
        })
        .or_else(|| {
            // Pure builtin String-concat monoid identities (`s + "" = s`,
            // `"" + s = s`, `(a + b) + c = a + (b + c)`) — the
            // no-`String.len`-wrapper sibling of the rung above. Same
            // class (bare String equality, no user fn → BackendDispatch →
            // Dafny proves, Lean used to sorry); last-in-cascade and
            // shape-driven, so it cannot perturb any existing proof.
            emit_string_append_monoid_law(law, &proof_intro_names)
        })
        .or_else(|| {
            // Last-resort universal close for a no-`when` EQUATIONAL law that no
            // strategy above claimed — typically a no-list-given rewrite with no
            // induction variable (`rev [z] = [z]`: `z : Int`, so there is nothing
            // to induct on, and every pin/recognizer declined). Unfold the law's
            // own def cone and let `simp` discharge the goal. `done` forces
            // closure, so a goal `simp` cannot close falls to the honest `sorry`
            // floor — never an unsolved-goals build error. Shape-driven and LAST
            // in the cascade, reached only where the result would otherwise be a
            // bare `sorry`, so it can only turn a would-be sorry into a kernel
            // close and never perturbs a proof an earlier rung produced. Loop-safe:
            // the simp set is the fn DEFS alone (no commutativity lemmas), which
            // unfold structurally and cannot reduce a match on a free variable.
            if law.when.is_some() {
                return None;
            }
            let defs: Vec<String> = shared::law_simp_defs(ctx, vb, law).into_iter().collect();
            if defs.is_empty() {
                return None;
            }
            Some(AutoProof {
                support_lines: Vec::new(),
                body: crate::codegen::lean::tactic_ir::Tactic::raw(intro_then(
                    &proof_intro_names,
                    vec![format!(
                        "first | (simp [{}] <;> done) | sorry",
                        defs.join(", ")
                    )],
                )),
                replaces_theorem: false,
            })
        })
}

/// Fixed core AC-ring lemma package for the `RingIdentity` rung —
/// `Init.Data.Int.Lemmas` names only (core + Std, NO Mathlib, no
/// `ring` tactic). Mechanism: `Int.mul_add`/`Int.add_mul` fully
/// distribute products over sums, the mul/add `comm`/`left_comm`/
/// `assoc` triples AC-sort monomials and sums (simp's ordered
/// rewriting terminates on permutational lemmas), and
/// `Int.sub_eq_add_neg`/`Int.zero_sub`/`Int.neg_mul` push `-` into
/// the same normal form. An unconditional ring identity then has
/// identical monomial multisets on both sides — no coefficient
/// collection needed — and the default simp set (`beq_iff_eq`,
/// `Int.mul_one`, `Int.add_zero`, …) finishes.
///
/// SCOPED TO THIS RUNG ONLY: the permutational rewrites loop or
/// destroy the normal forms other strategies' simp sets rely on, so
/// they are never merged into the shared prelude registry
/// (`prelude_spec_lemmas_for_builtins`) or any other strategy's set.
///
/// Known boundary (measured): identities that need coefficient
/// collection (`t + t` vs `2 * t`) or cancellation
/// (`x + (-x) = 0` nested inside products) stay outside — the
/// `first | … | sorry` alternation degrades them to an honest
/// caught sorry.
const RING_NORMALIZATION_LEMMAS: [&str; 11] = [
    "Int.mul_add",
    "Int.add_mul",
    "Int.mul_comm",
    "Int.mul_left_comm",
    "Int.mul_assoc",
    "Int.add_comm",
    "Int.add_left_comm",
    "Int.add_assoc",
    "Int.sub_eq_add_neg",
    "Int.zero_sub",
    "Int.neg_mul",
];

/// Render the `RingIdentity` rung:
/// `intro <givens>; first | (simp [<cone>, <AC-ring package>]; done) | sorry`.
///
/// Simp-set assembly: the unfold cone (law subject first — source
/// names via `aver_name_to_lean`; record-field projections unfold by
/// themselves), then the fixed [`RING_NORMALIZATION_LEMMAS`] package.
/// `done` forces closure — a simp that fails OR leaves a residual
/// goal falls to the honest caught `sorry`, never an "unsolved
/// goals" build error and never `native_decide`.
fn emit_ring_identity_law(
    vb: &VerifyBlock,
    law: &VerifyLaw,
    ctx: &CodegenContext,
    proof_intro_names: &[String],
) -> Option<AutoProof> {
    let Some(crate::ir::ProofStrategy::RingIdentity { unfold_fns }) =
        law_strategy_for(ctx, &vb.fn_name, &law.name)
    else {
        return None;
    };
    // Cone unfold fns, mapped to their Lean names. `grind` does NOT
    // unfold user `def`s on its own, so the same cone the simp set
    // leads with is handed to `grind [<cone>]` as its unfold bracket;
    // without it `grind` stalls on the opaque `sameValue …` goal.
    let grind_cone: Vec<String> = unfold_fns.iter().map(|f| aver_name_to_lean(f)).collect();
    let simp_set: Vec<String> = grind_cone
        .iter()
        .cloned()
        .chain(RING_NORMALIZATION_LEMMAS.iter().map(|s| s.to_string()))
        .collect();
    Some(AutoProof {
        support_lines: Vec::new(),
        // Rung order, cheapest genuine closer first: `grind [<cone>]`
        // (Lean 4.31 core, no Mathlib) carries the multi-variable
        // nonlinear ring identities the hand-rolled AC-ring simp
        // package stopped normalizing at 4.31 (`minus.equalsPlusNegate`);
        // the simp package stays as the fallback rung, then the honest
        // caught `sorry`. Every alternation arm ends in `done`, so a
        // tactic that leaves a residual goal falls through rather than
        // raising an "unsolved goals" build error.
        body: intro_then_first(
            proof_intro_names,
            vec![
                format!("grind [{}]; done", grind_cone.join(", ")),
                format!("simp [{}]; done", simp_set.join(", ")),
            ],
        ),
        replaces_theorem: false,
    })
}

/// Render the `SimpOverPreludeLemmas` rung:
/// `intro <givens>; first | (simp [<set>]; done) | sorry`.
///
/// Simp-set assembly, in order: unfold fns (subject first — source
/// names via `aver_name_to_lean`), then per fuel fn the wrapper name +
/// `<fn>__fuel` + measure helpers (probed from the actual proof-mode
/// emission by `toplevel::law_fuel_simp_names` — a fuel fn that
/// graduated to native `termination_by` contributes its wrapper name
/// only, never a non-existent `__fuel` constant), then the prelude
/// spec lemmas the registry maps from the cone's builtin calls
/// (`lean::prelude_spec_lemmas_for_builtins` — the same names whose
/// mention makes the demand-driven prelude ship the lemma texts), then
/// `Int.add_sub_cancel`.
fn emit_simp_over_prelude_lemmas_law(
    vb: &VerifyBlock,
    law: &VerifyLaw,
    ctx: &CodegenContext,
    proof_intro_names: &[String],
) -> Option<AutoProof> {
    let Some(crate::ir::ProofStrategy::SimpOverPreludeLemmas {
        unfold_fns,
        fuel_fns,
        builtins,
    }) = law_strategy_for(ctx, &vb.fn_name, &law.name)
    else {
        return None;
    };
    let mut simp_set: Vec<String> = Vec::new();
    let push_unique = |set: &mut Vec<String>, name: String| {
        if !set.contains(&name) {
            set.push(name);
        }
    };
    for f in &unfold_fns {
        push_unique(&mut simp_set, aver_name_to_lean(f));
    }
    for f in &fuel_fns {
        push_unique(&mut simp_set, aver_name_to_lean(f));
        for name in super::toplevel::law_fuel_simp_names(f, ctx) {
            push_unique(&mut simp_set, name);
        }
    }
    for lemma in super::prelude_spec_lemmas_for_builtins(&builtins) {
        push_unique(&mut simp_set, lemma);
    }
    push_unique(&mut simp_set, "Int.add_sub_cancel".to_string());
    Some(AutoProof {
        support_lines: Vec::new(),
        body: intro_then_first(
            proof_intro_names,
            vec![format!("simp [{}]; done", simp_set.join(", "))],
        ),
        replaces_theorem: false,
    })
}

/// Pure builtin String-length additivity: `String.len(a + b) =
/// String.len(a) + String.len(b)` (and nested-concat / argument-swapped
/// variants). The law statement mentions no user fn — its lhs calls
/// builtins directly — so every cone-anchored rung declines: `Induction`
/// needs a recursive-ADT given, and `SimpOverPreludeLemmas` anchors its
/// unfold set on the subject fn appearing in the lhs. The strategy
/// therefore stays `BackendDispatch`, where Dafny's Z3 already discharges
/// the law via the sequence-length axiom (`|s + t| = |s| + |t|`) but the
/// Lean side fell to a bare `sorry`. This Lean-only rung closes it
/// without touching the IR strategy or the Dafny path.
///
/// Mechanism: Aver's `String +` is the custom `HAdd String` instance
/// (`⟨String.append⟩`); the prelude `rfl` lemma `String.add_eq_append :
/// s + t = s ++ t` (demand-shipped because the emitted tactic cites it)
/// rewrites `+ → ++`, the Lean-core `@[simp] String.length_append`
/// rewrites `(s ++ t).length → s.length + t.length`, and `omega` finishes
/// over the `(… : Int)` length coercions (it is cast-aware). The honest
/// `| sorry` floor means a non-additive law this happened to match simply
/// fails the tactic and degrades to the same caught sorry it had before —
/// the rung can never close a false law (`simp`/`omega` are sound).
fn emit_string_length_additive_law(
    law: &VerifyLaw,
    proof_intro_names: &[String],
) -> Option<AutoProof> {
    if law.when.is_some() {
        return None;
    }
    if !(law_expr_has_string_len_over_concat(&law.lhs)
        || law_expr_has_string_len_over_concat(&law.rhs))
    {
        return None;
    }
    Some(AutoProof {
        support_lines: Vec::new(),
        body: intro_then_first(
            proof_intro_names,
            vec!["simp only [String.add_eq_append, String.length_append] <;> omega".to_string()],
        ),
        replaces_theorem: false,
    })
}

/// True when `e` contains a `String.len(arg)` call whose `arg`
/// syntactically involves a string `+` — the trigger shape for
/// [`emit_string_length_additive_law`]. `String.len` takes a `String`, so
/// an `Add` under it is necessarily the custom `HAdd String` concat (no
/// type lookup needed). Walks both law sides so an argument-swapped law
/// (`len(a) + len(b) => len(a + b)`) is recognised too.
fn law_expr_has_string_len_over_concat(e: &crate::ast::Spanned<crate::ast::Expr>) -> bool {
    use crate::ast::Expr;
    let here = matches!(&e.node, Expr::FnCall(callee, args)
        if args.len() == 1
            && crate::codegen::common::expr_to_dotted_name(&callee.node).as_deref()
                == Some("String.len")
            && expr_contains_add(&args[0]));
    here || law_expr_children_any(e, law_expr_has_string_len_over_concat)
}

/// True when `e` contains a `BinOp(Add, …)` at any depth.
fn expr_contains_add(e: &crate::ast::Spanned<crate::ast::Expr>) -> bool {
    use crate::ast::{BinOp, Expr};
    matches!(&e.node, Expr::BinOp(BinOp::Add, _, _)) || law_expr_children_any(e, expr_contains_add)
}

/// `true` if `f` holds on any direct child sub-expression of `e`. Covers
/// the compound `Expr` variants a `verify` law's lhs/rhs can hold;
/// leaf/irrelevant variants short-circuit to `false`.
fn law_expr_children_any(
    e: &crate::ast::Spanned<crate::ast::Expr>,
    f: fn(&crate::ast::Spanned<crate::ast::Expr>) -> bool,
) -> bool {
    use crate::ast::Expr;
    match &e.node {
        Expr::Attr(o, _) => f(o),
        Expr::FnCall(c, args) => f(c) || args.iter().any(f),
        Expr::BinOp(_, l, r) => f(l) || f(r),
        Expr::Neg(i) | Expr::ErrorProp(i) => f(i),
        Expr::Match { subject, arms } => f(subject) || arms.iter().any(|a| f(&a.body)),
        Expr::Constructor(_, Some(inner)) => f(inner),
        Expr::List(xs) | Expr::Tuple(xs) | Expr::IndependentProduct(xs, _) => xs.iter().any(f),
        Expr::MapLiteral(kvs) => kvs.iter().any(|(k, v)| f(k) || f(v)),
        Expr::RecordCreate { fields, .. } => fields.iter().any(|(_, v)| f(v)),
        Expr::RecordUpdate { base, updates, .. } => f(base) || updates.iter().any(|(_, v)| f(v)),
        Expr::TailCall(d) => d.args.iter().any(f),
        _ => false,
    }
}

/// Pure builtin String-concat monoid identities: `s + "" = s`, `"" + s =
/// s`, and `(a + b) + c = a + (b + c)`. Like [`emit_string_length_additive_law`]
/// these mention no user fn (the law is a bare String equality), so every
/// cone-anchored rung declines and the strategy stays `BackendDispatch` —
/// Dafny's Z3 discharges them, the Lean side fell to a bare `sorry`. This
/// is the no-`String.len`-wrapper sibling of that rung.
///
/// One unified tactic closes all three shapes: `String.add_eq_append`
/// (prelude rfl lemma, demand-shipped because the tactic cites it)
/// rewrites the custom `HAdd String` `+` to `++`, then the Lean-core
/// `String.append_empty` / `String.empty_append` / `String.append_assoc`
/// finish. The `| sorry` floor keeps it sound — a falsely-matched
/// non-identity (e.g. an `Int` reassociation that slipped past the earlier
/// arithmetic rungs) just fails the tactic and degrades to the same caught
/// sorry, never a false close (`simp` is kernel-checked).
fn emit_string_append_monoid_law(
    law: &VerifyLaw,
    proof_intro_names: &[String],
) -> Option<AutoProof> {
    if law.when.is_some() {
        return None;
    }
    let fires = law_expr_has_empty_string_concat(&law.lhs)
        || law_expr_has_empty_string_concat(&law.rhs)
        || is_concat_reassociation(&law.lhs, &law.rhs);
    if !fires {
        return None;
    }
    Some(AutoProof {
        support_lines: Vec::new(),
        body: intro_then_first(
            proof_intro_names,
            vec![
                "simp only [String.add_eq_append, String.append_empty, \
                 String.empty_append, String.append_assoc]"
                    .to_string(),
            ],
        ),
        replaces_theorem: false,
    })
}

/// `e` contains a `BinOp(Add, x, y)` where `x` or `y` is the empty String
/// literal `""` — the unambiguous String-`+` signal (`""` only types as a
/// String, so the `+` is the custom `HAdd String`). Triggers the
/// identity shapes of [`emit_string_append_monoid_law`].
fn law_expr_has_empty_string_concat(e: &crate::ast::Spanned<crate::ast::Expr>) -> bool {
    use crate::ast::{BinOp, Expr, Literal};
    let is_empty_str = |s: &crate::ast::Spanned<Expr>| matches!(&s.node, Expr::Literal(Literal::Str(t)) if t.is_empty());
    let here =
        matches!(&e.node, Expr::BinOp(BinOp::Add, l, r) if is_empty_str(l) || is_empty_str(r));
    here || law_expr_children_any(e, law_expr_has_empty_string_concat)
}

/// `lhs` is `(_ + _) + _` and `rhs` is `_ + (_ + _)` — a `+` reassociation
/// (the associativity shape). Operand types are not inspected: an `Int`
/// reassociation is closed by the earlier arithmetic rungs and never
/// reaches this last-in-cascade rung, so matching the shape alone is safe.
fn is_concat_reassociation(
    lhs: &crate::ast::Spanned<crate::ast::Expr>,
    rhs: &crate::ast::Spanned<crate::ast::Expr>,
) -> bool {
    use crate::ast::{BinOp, Expr};
    let left_nested = matches!(&lhs.node, Expr::BinOp(BinOp::Add, l, _) if matches!(l.node, Expr::BinOp(BinOp::Add, _, _)));
    let right_nested = matches!(&rhs.node, Expr::BinOp(BinOp::Add, _, r) if matches!(r.node, Expr::BinOp(BinOp::Add, _, _)));
    left_nested && right_nested
}

/// Pure builtin `Int.abs` identities — idempotence (`Int.abs(Int.abs x) =
/// Int.abs x`), multiplicativity (`Int.abs(x*y) = Int.abs x * Int.abs y`),
/// and non-negativity (`Int.abs x >= 0 = true`). `Int.abs` lowers to the
/// Int-honest `((… : Int).natAbs : Int)`, so these are facts about the
/// `Nat.cast` of a `natAbs`; the cone is already inlined in the goal, so no
/// def unfold is needed. One tactic closes all three: `Int.natAbs_natCast`
/// collapses `(↑n).natAbs = n` (idempotence), `Int.natAbs_mul` +
/// `Int.natCast_mul` push the product through the cast (multiplicativity),
/// and the full-`simp` fallback discharges the Bool `… >= 0 = true` wrapper
/// (non-negativity). The `| sorry` floor keeps it sound — `simp`/`omega` are
/// kernel-checked, so it can never close a false law.
fn emit_int_abs_identity_law(law: &VerifyLaw, proof_intro_names: &[String]) -> Option<AutoProof> {
    if law.when.is_some() || !(law_expr_calls_int_abs(&law.lhs) || law_expr_calls_int_abs(&law.rhs))
    {
        return None;
    }
    Some(AutoProof {
        support_lines: Vec::new(),
        body: intro_then_first(
            proof_intro_names,
            vec![
                "simp only [Int.natAbs_natCast, Int.natAbs_mul, Int.natCast_mul] <;> omega"
                    .to_string(),
                "simp [Int.natAbs_natCast, Int.natAbs_mul, Int.natCast_mul]".to_string(),
            ],
        ),
        replaces_theorem: false,
    })
}

/// `e` contains an `Int.abs(...)` builtin call at any depth — the trigger
/// for [`emit_int_abs_identity_law`].
fn law_expr_calls_int_abs(e: &crate::ast::Spanned<crate::ast::Expr>) -> bool {
    use crate::ast::Expr;
    let here = matches!(&e.node, Expr::FnCall(callee, _)
        if crate::codegen::common::expr_to_dotted_name(&callee.node).as_deref() == Some("Int.abs"));
    here || law_expr_children_any(e, law_expr_calls_int_abs)
}

/// Pure builtin empty-map facts: `Map.get(empty, k) = None`,
/// `Map.has(empty, k) = false`, `Map.len(empty) = 0`. The subject fn body
/// reduces to a `Map.get`/`has`/`len` over a provably empty map; Dafny's Z3
/// discharges these, but the Lean generic grind rung can't reduce the
/// `AverMap.*` accessor on `[]` and parks the law on a caught sorry.
///
/// This rung unfolds the law's cone (subject fn + the empty-map source fn)
/// together with the accessor defs and the `[]` lemmas, which collapses the
/// goal: `AverMap.get [] k = none`, `AverMap.has [] k = false` (via
/// `List.any_nil`), `((AverMap.len []) : Int) = 0` (via `List.length_nil` +
/// `Int.ofNat_zero`). One unified `simp only` set closes any of the three;
/// the `| sorry` floor keeps it sound — a Map law whose argument is NOT
/// empty simply fails the `; done` and degrades to the same caught sorry it
/// had before. Last-in-cascade and shape-driven, so it cannot perturb an
/// existing proof (a Map law another rung already owns is handled earlier).
fn emit_map_empty_fact_law(
    vb: &VerifyBlock,
    law: &VerifyLaw,
    ctx: &CodegenContext,
    proof_intro_names: &[String],
) -> Option<AutoProof> {
    if law.when.is_some() || !subject_fn_accesses_empty_map(vb, ctx) {
        return None;
    }
    let mut simp_set: Vec<String> = shared::law_simp_defs(ctx, vb, law).into_iter().collect();
    simp_set.extend(
        [
            "AverMap.get",
            "AverMap.has",
            "AverMap.len",
            "List.any_nil",
            "List.length_nil",
            "Int.ofNat_zero",
        ]
        .iter()
        .map(|s| s.to_string()),
    );
    Some(AutoProof {
        support_lines: Vec::new(),
        body: intro_then_first(
            proof_intro_names,
            vec![format!("simp only [{}] ; done", simp_set.join(", "))],
        ),
        replaces_theorem: false,
    })
}

/// True when the law's subject fn body accesses a PROVABLY EMPTY map via
/// `Map.get`/`Map.has`/`Map.len` — the precise trigger for
/// [`emit_map_empty_fact_law`]. Requiring emptiness (not just any Map
/// accessor) keeps the rung from stealing a non-empty Map law the prelude
/// rung might close.
fn subject_fn_accesses_empty_map(vb: &VerifyBlock, ctx: &CodegenContext) -> bool {
    let Some(fd) = ctx.fn_def_by_name(&vb.fn_name, None) else {
        return false;
    };
    fd.body.stmts().iter().any(|stmt| {
        let e = match stmt {
            crate::ast::Stmt::Binding(_, _, e) | crate::ast::Stmt::Expr(e) => e,
        };
        expr_accesses_empty_map(e, ctx)
    })
}

/// `e` contains a `Map.get`/`Map.has`/`Map.len` call whose map argument is a
/// provably empty map (see [`expr_is_empty_map`]), at any depth.
fn expr_accesses_empty_map(
    e: &crate::ast::Spanned<crate::ast::Expr>,
    ctx: &CodegenContext,
) -> bool {
    use crate::ast::Expr;
    if let Expr::FnCall(callee, args) = &e.node
        && !args.is_empty()
        && matches!(
            crate::codegen::common::expr_to_dotted_name(&callee.node).as_deref(),
            Some("Map.get") | Some("Map.has") | Some("Map.len")
        )
        && expr_is_empty_map(&args[0], ctx)
    {
        return true;
    }
    // Recurse into the compound `Expr` variants a law subject's body holds.
    match &e.node {
        Expr::Attr(o, _) => expr_accesses_empty_map(o, ctx),
        Expr::FnCall(c, args) => {
            expr_accesses_empty_map(c, ctx) || args.iter().any(|a| expr_accesses_empty_map(a, ctx))
        }
        Expr::BinOp(_, l, r) => expr_accesses_empty_map(l, ctx) || expr_accesses_empty_map(r, ctx),
        Expr::Neg(i) | Expr::ErrorProp(i) => expr_accesses_empty_map(i, ctx),
        Expr::Match { subject, arms } => {
            expr_accesses_empty_map(subject, ctx)
                || arms.iter().any(|a| expr_accesses_empty_map(&a.body, ctx))
        }
        Expr::Constructor(_, Some(inner)) => expr_accesses_empty_map(inner, ctx),
        Expr::List(xs) | Expr::Tuple(xs) | Expr::IndependentProduct(xs, _) => {
            xs.iter().any(|x| expr_accesses_empty_map(x, ctx))
        }
        _ => false,
    }
}

/// A provably empty map: the `{}` literal, or a zero-arg call to a user fn
/// whose body is exactly `{}`.
fn expr_is_empty_map(e: &crate::ast::Spanned<crate::ast::Expr>, ctx: &CodegenContext) -> bool {
    use crate::ast::{Expr, Stmt};
    match &e.node {
        Expr::MapLiteral(entries) => entries.is_empty(),
        Expr::FnCall(callee, args) if args.is_empty() => {
            crate::codegen::common::expr_to_dotted_name(&callee.node)
                .and_then(|n| ctx.fn_def_by_name(&n, None))
                .is_some_and(|fd| {
                    let stmts = fd.body.stmts();
                    stmts.len() == 1
                        && matches!(&stmts[0],
                            Stmt::Expr(b) if matches!(&b.node, Expr::MapLiteral(es) if es.is_empty()))
                })
        }
        _ => false,
    }
}

/// `Map.len(Map.set(m, k, v)) >= 1 => true` — `set` always yields a
/// non-empty map. Unlike the empty-map facts this is not a definitional
/// unfold: it needs induction on `m` (`set.go` length is `>= 1`). The
/// hand-proved prelude lemma `AverMap.len_set_ge_one` carries that induction
/// and is stated in the exact lowered goal shape, so the rung discharges the
/// law with a bare `exact AverMap.len_set_ge_one _ _ _` (the placeholders
/// unify the map/key/value from the goal). Citing the lemma demand-ships it.
/// The `| sorry` floor keeps it sound.
fn emit_map_len_set_positive_law(
    law: &VerifyLaw,
    proof_intro_names: &[String],
) -> Option<AutoProof> {
    if law.when.is_some() || !law_is_map_len_set_ge_one(law) {
        return None;
    }
    Some(AutoProof {
        support_lines: Vec::new(),
        body: intro_then_first(
            proof_intro_names,
            vec!["exact AverMap.len_set_ge_one _ _ _".to_string()],
        ),
        replaces_theorem: false,
    })
}

/// True for a law whose lhs is `Map.len(Map.set(_, _, _)) >= 1` — the trigger
/// for [`emit_map_len_set_positive_law`].
fn law_is_map_len_set_ge_one(law: &VerifyLaw) -> bool {
    use crate::ast::{BinOp, Expr, Literal};
    let Expr::BinOp(BinOp::Gte, left, right) = &law.lhs.node else {
        return false;
    };
    let is_one = matches!(&right.node, Expr::Literal(Literal::Int(1)));
    let len_over_set = matches!(&left.node, Expr::FnCall(callee, args)
        if crate::codegen::common::expr_to_dotted_name(&callee.node).as_deref() == Some("Map.len")
            && args.len() == 1
            && matches!(&args[0].node, Expr::FnCall(set_callee, _)
                if crate::codegen::common::expr_to_dotted_name(&set_callee.node).as_deref()
                    == Some("Map.set")));
    is_one && len_over_set
}

/// Try `simp [fn_names...] ; omega` for laws on Int-domain functions.
///
/// Works when the function is a non-recursive match on Int args
/// (e.g. `computeScore(0, level) => 0`). `simp` unfolds the function,
/// `omega` closes the linear arithmetic goal.
/// Render the simp+omega tactic from IR-pinned data. Mirrors the
/// emit body of the legacy `emit_simp_omega_law` (kept as fallback
/// for `BackendDispatch`) but sources `unfold_fns` / `wrapper_
/// return` / `smart_guard` from `ProofIR.law_theorems[*].strategy`.
/// Core (no-Mathlib) lemma package that normalises a Bool-valued Int
/// comparison identity so `omega` can finish: `Bool.beq_comm` orders the
/// `==`, `Bool.or_eq_true`/`Bool.and_eq_true`/`decide_eq_true_eq` strip the
/// `= true` / `&&` / `||` Bool wrappers to the underlying decidable props,
/// `decide_eq_decide` reduces `decide p = decide q` to `p ↔ q`, `← decide_not`
/// turns `!decide p` into `decide ¬p`, and `ge_iff_le`/`gt_iff_lt` rewrite
/// `≥`/`>` to `≤`/`<` — leaving a pure linear-order goal `omega` decides.
/// Used only as a `first`-alternative after the sign-split in the
/// `wrapper_return` arm of [`emit_simp_omega_from_ir`].
const COMPARISON_NORMALIZERS: &[&str] = &[
    "Bool.beq_comm",
    "Bool.or_eq_true",
    "Bool.and_eq_true",
    "decide_eq_decide",
    "decide_eq_true_eq",
    "← decide_not",
    "ge_iff_le",
    "gt_iff_lt",
];

#[allow(clippy::too_many_arguments)]
fn emit_simp_omega_from_ir(
    unfold_fns: &[String],
    wrapper_return: bool,
    smart_guard: Option<&crate::ir::SmartGuard>,
    lifted: bool,
    intro_names: &[String],
    given_names: &[String],
    has_when: bool,
    uses_max_min: bool,
    ctx: &CodegenContext,
) -> super::tactic_ir::Tactic {
    use super::tactic_ir::Tactic;
    let lean_names: Vec<String> = unfold_fns.iter().map(|n| aver_name_to_lean(n)).collect();
    if lifted && wrapper_return {
        // Subtype/subset lift carries the smart-constructor
        // invariant in the type — the law-quantified vars are
        // already `Natural` (etc.) in the theorem statement, so
        // by_cases case-split is unnecessary. Plain unfold + simp
        // with arithmetic lemmas closes via Lean's built-in
        // commutativity normalisation.
        Tactic::raw(intro_then(
            intro_names,
            vec![
                format!("unfold {}", lean_names.join(" ")),
                "simp [Int.add_comm, Int.mul_comm]".to_string(),
            ],
        ))
    } else if wrapper_return {
        // Case ONLY over the law's actual Int-typed given variables —
        // NEVER the introduced premise-hypothesis names. `intro_names`
        // carries `h_a` / `h_when` for `when`-laws, and casing over
        // those (`by_cases h_h_a : h_a >= 0` where `h_a : Prop`) is an
        // application-type-mismatch build error. (The `when`+wrapper
        // combination is declined before this arm is reached; the
        // given-name restriction here is the structural guarantee.)
        let by_cases_clauses: Vec<String> = given_names
            .iter()
            .map(|n| {
                let predicate = match smart_guard {
                    Some(g) => {
                        let substituted = crate::codegen::common::substitute_ident_in_resolved_expr(
                            &g.predicate,
                            &g.param,
                            n,
                        );
                        super::expr::emit_expr(&substituted, ctx)
                    }
                    None => format!("{n} ≥ 0"),
                };
                format!("by_cases h_{n} : {predicate}")
            })
            .collect();
        let by_cases_chain = by_cases_clauses.join(" <;> ");
        let simp_hyps: Vec<String> = given_names
            .iter()
            .map(|n| format!("h_{n}"))
            .chain(["Int.add_comm".to_string(), "Int.mul_comm".to_string()])
            .collect();
        let simp_args = simp_hyps.join(", ");
        // The sign-split `by_cases … <;> simp [Int.add_comm, Int.mul_comm]`
        // closes wrapper-return arithmetic identities, but a Bool-valued
        // COMPARISON identity (`(a == b) = (b == a)`, `!(a < b) = (a >= b)`,
        // `(a <= b) || (b <= a) = true`, `(a < b) = (b > a)`) leaves it with
        // "simp made no progress" — and with no `first | … | sorry` wrapper
        // that hard-failed the whole module build. After the `unfold`, try the
        // sign-split FIRST (so every law that closed before is byte-identical),
        // then a comparison-normalising `simp only [<COMPARISON_NORMALIZERS>]
        // <;> omega` (which closes the Bool-comparison shapes Dafny's Z3 already
        // proves), and floor on `sorry` so anything still open degrades to a
        // caught sorry instead of an uncatchable build error. The comparison
        // rung is inert when the sign-split already closed (it is never
        // reached), and `simp`/`omega` are sound, so it can never close a false
        // law.
        let cmp = format!(
            "simp only [{}] <;> omega",
            COMPARISON_NORMALIZERS.join(", ")
        );
        // `unfold` then a structured `first | (sign-split) | (comparison) | sorry`
        // (was a flat string) so `--minimize` can collapse it to its winner.
        intro_prefix_then_first(
            intro_names,
            vec![format!("unfold {}", lean_names.join(" "))],
            vec![format!("{by_cases_chain} <;> simp [{simp_args}]"), cmp],
        )
    } else {
        // A `when` premise is introduced as a hypothesis (`h_when`).
        // `simp_all` simplifies it — e.g. a nested Bool `match` lowered to
        // an `if/then/else` — so `omega` can use the premise; for an
        // unsatisfiable premise it derives the contradiction and closes
        // the (vacuously-true) law. Plain `simp only` leaves the Bool
        // premise opaque and `omega` fails ("no usable constraints"),
        // wrongly rejecting a valid law. Without a `when`, keep the
        // conservative `simp only` — there is no premise to simplify.
        if uses_max_min {
            // `Int.max`/`Int.min` lower to core `max`/`min`, which
            // `omega` treats as opaque atoms (it has no `max`/`min`
            // theory). Unfolding `Int.max_def`/`Int.min_def` exposes
            // the underlying `if a ≤ b then …` so `split` peels each
            // branch into a linear goal `omega` can close. `try split`
            // (not bare `split`) keeps this safe when the unfold leaves
            // nothing to split — a bare `split` on a split-free goal is
            // an error. `simp_all` discharges the residual `if`/premise
            // shape before `omega`. GATED: only laws whose unfold chain
            // actually calls `Int.max`/`Int.min` take this path; every
            // other linear-arithmetic law stays byte-identical to the
            // `simp only [...] <;> omega` / `simp_all [...] <;> omega`
            // forms below so no existing law regresses.
            let lemmas: Vec<String> = lean_names
                .iter()
                .cloned()
                .chain(["Int.max_def".to_string(), "Int.min_def".to_string()])
                .collect();
            // `<;> omega` alone closes the unfolded min/max if-nest —
            // `omega` case-splits the `Int.min_def`/`Int.max_def`
            // conditionals itself, which the legacy `(try split) <;>
            // simp_all` chain did NOT for a 3-way `min` nest: it left
            // unsolved goals and, with no `first | … | sorry` wrapper,
            // hard-failed the WHOLE module build (poisoning every other
            // law in the file, not just this one). Try the clean `omega`
            // form first, keep the legacy chain as a fallback so no
            // min/max law that closed before can regress, and floor on
            // `sorry` so a still-open case degrades to a caught sorry
            // instead of an uncatchable build error.
            let l = lemmas.join(", ");
            // Structured `first | (omega) | (split…omega) | sorry` so a minimizer
            // can drop the legacy fallback rung when the clean `omega` form wins.
            intro_then_first(
                intro_names,
                vec![
                    format!("simp only [{l}] <;> omega"),
                    format!("simp only [{l}] <;> (try split) <;> simp_all <;> omega"),
                ],
            )
        } else if has_when {
            Tactic::raw(intro_then(
                intro_names,
                vec![format!("simp_all [{}] <;> omega", lean_names.join(", "))],
            ))
        } else {
            Tactic::raw(intro_then(
                intro_names,
                vec![format!("simp only [{}] <;> omega", lean_names.join(", "))],
            ))
        }
    }
}

/// Detect whether the LinearArithmetic unfold chain calls
/// `Int.max` / `Int.min`. Drives the gated `Int.max_def`/`Int.min_def`
/// split tactic in [`emit_simp_omega_from_ir`] — only laws that
/// actually involve min/max take the split path; everything else stays
/// on the byte-identical `simp only`/`simp_all` + `omega` forms.
///
/// Walks the *bodies* of every fn named in `unfold_fns` (the same fns
/// the tactic will `simp only [...]`-unfold), so an `Int.max` buried in
/// a helper that the law transitively unfolds is still caught. Resolves
/// each name via the symbol table (entry scope, then every dep module),
/// matching how the unfold list itself is sourced.
fn linear_arith_uses_max_min(unfold_fns: &[String], ctx: &CodegenContext) -> bool {
    unfold_fns.iter().any(|name| {
        let fd = ctx.fn_def_by_name(name, None).or_else(|| {
            ctx.modules
                .iter()
                .find_map(|m| ctx.fn_def_by_name(name, Some(&m.prefix)))
        });
        fd.is_some_and(|fd| fn_body_calls_max_min(&fd.body))
    })
}

/// True when `body` contains a call to `Int.max` or `Int.min`.
fn fn_body_calls_max_min(body: &crate::ast::FnBody) -> bool {
    body.stmts().iter().any(|stmt| match stmt {
        crate::ast::Stmt::Binding(_, _, e) | crate::ast::Stmt::Expr(e) => expr_calls_max_min(e),
    })
}

fn expr_calls_max_min(expr: &crate::ast::Spanned<crate::ast::Expr>) -> bool {
    use crate::ast::Expr;
    match &expr.node {
        Expr::FnCall(f, args) => {
            let is_max_min = crate::codegen::common::expr_to_dotted_name(&f.node)
                .is_some_and(|n| n == "Int.max" || n == "Int.min");
            is_max_min || args.iter().any(expr_calls_max_min)
        }
        Expr::BinOp(_, l, r) => expr_calls_max_min(l) || expr_calls_max_min(r),
        Expr::Neg(inner) | Expr::Attr(inner, _) | Expr::ErrorProp(inner) => {
            expr_calls_max_min(inner)
        }
        Expr::Match { subject, arms } => {
            expr_calls_max_min(subject) || arms.iter().any(|arm| expr_calls_max_min(&arm.body))
        }
        Expr::Constructor(_, Some(inner)) => expr_calls_max_min(inner),
        Expr::List(items) | Expr::Tuple(items) | Expr::IndependentProduct(items, _) => {
            items.iter().any(expr_calls_max_min)
        }
        Expr::MapLiteral(entries) => entries
            .iter()
            .any(|(k, v)| expr_calls_max_min(k) || expr_calls_max_min(v)),
        Expr::RecordCreate { fields, .. } => fields.iter().any(|(_, e)| expr_calls_max_min(e)),
        Expr::RecordUpdate { base, updates, .. } => {
            expr_calls_max_min(base) || updates.iter().any(|(_, e)| expr_calls_max_min(e))
        }
        Expr::TailCall(boxed) => boxed.args.iter().any(expr_calls_max_min),
        _ => false,
    }
}

pub fn emit_verify_law_support_theorems(
    vb: &VerifyBlock,
    _law: &VerifyLaw,
    ctx: &CodegenContext,
    _theorem_base: &str,
) -> Vec<String> {
    collect_missing_helper_law_hints(&ctx.items, ctx)
        .into_iter()
        .find(|hint| hint.line == vb.line && hint.fn_name == vb.fn_name)
        .map(|hint| {
            vec![
                format!("-- hint: {}", missing_helper_law_message(&hint)),
                "-- hint: the main theorem can stay generic, but it still needs those helper laws as intermediate theorems".to_string(),
            ]
        })
        .unwrap_or_default()
}

pub(super) fn intro_then(intro_names: &[String], steps: Vec<String>) -> Vec<String> {
    let mut lines = Vec::new();
    if !intro_names.is_empty() {
        lines.push(format!("intro {}", intro_names.join(" ")));
    }
    lines.extend(steps);
    indent_lines(lines, 2)
}

/// Build a proof body `intro <givens>; first | (b₀) | (b₁) | … | sorry` as a
/// STRUCTURED portfolio: each branch a [`Tactic`] leaf, a bare `sorry` floor
/// appended, under one [`tactic_ir::Tactic::First`]. This is the minimizable
/// twin of `Tactic::raw(intro_then(names, vec![format!("first | (b₀) | … |
/// sorry")]))` — `render_body` emits it INLINE and byte-for-byte identically
/// (so the emitted proof is unchanged), but `--minimize` can now collapse the
/// portfolio to its winning branch. `branches` are the alternative tactic
/// texts WITHOUT their wrapping parens (the renderer re-adds them) and WITHOUT
/// the trailing `| sorry` (added here). Each branch must be a single complete
/// tactic that runs on ONE goal — never the right-hand side of `<;>`.
fn intro_then_first(intro_names: &[String], branches: Vec<String>) -> super::tactic_ir::Tactic {
    intro_prefix_then_first(intro_names, Vec::new(), branches)
}

/// As [`intro_then_first`] but with `prefix` tactic steps emitted (each its own
/// line) between the `intro` and the `first` portfolio — e.g. an `unfold …`
/// that must run before the alternation. Renders
/// `intro <givens>; <prefix…>; first | (b₀) | … | sorry`, inline + byte-for-byte
/// like the legacy `intro_then(names, [<prefix…>, "first | … | sorry"])`.
fn intro_prefix_then_first(
    intro_names: &[String],
    prefix: Vec<String>,
    branches: Vec<String>,
) -> super::tactic_ir::Tactic {
    use super::tactic_ir::Tactic;
    let mut steps = Vec::new();
    if !intro_names.is_empty() {
        steps.push(Tactic::Leaf(format!("intro {}", intro_names.join(" "))));
    }
    steps.extend(prefix.into_iter().map(Tactic::Leaf));
    let mut alts: Vec<Tactic> = branches.into_iter().map(Tactic::Leaf).collect();
    alts.push(Tactic::Sorry);
    steps.push(Tactic::First(alts));
    Tactic::Seq(steps)
}

/// Render a SUPPORT theorem — a helper lemma emitted (as one multi-line string)
/// alongside the main law — from its `:= by` header line plus a structured
/// proof `body`. The body renders through [`super::tactic_ir::Tactic::render_body`],
/// so a `first | … | sorry` portfolio inside the support theorem is now a real
/// `First` the `--minimize` pass collapses (the producer runs inside the
/// minimize re-emit passes). Byte-for-byte identical to the legacy hand-written
/// `format!("theorem … := by\n  …")` string when no pass is active.
pub(super) fn support_theorem(header: &str, body: super::tactic_ir::Tactic) -> String {
    let mut out = String::from(header);
    for line in body.render_body() {
        out.push('\n');
        out.push_str(&line);
    }
    out
}

fn extend_intro_names_with_premises(law: &VerifyLaw, intro_names: &[String]) -> Vec<String> {
    let mut names = intro_names.to_vec();
    if law.when.is_some() {
        names.extend(intro_names.iter().map(|name| format!("h_{name}")));
        names.push("h_when".to_string());
    }
    names
}

pub(super) fn indent_lines(lines: Vec<String>, spaces: usize) -> Vec<String> {
    let pad = " ".repeat(spaces);
    lines
        .into_iter()
        .map(|line| format!("{pad}{line}"))
        .collect()
}