assura 0.4.2

//! Encode simple Rust function bodies as Assura Implementation IR for check-rust.
//!
//! Supports int/bool arith, abs/min/max/clamp/saturating(+neg/abs)/abs_diff/signum,
//! is_positive/negative/zero, `is_multiple_of`, PartialOrd methods, logical `&&`/`||`,
//! unary `-`/`!`/`*`/`&`, identity ops (`into`/`as` lossless/`clone`/`copied`/`as_ref`/
//! `not`), `default` and integer MIN/MAX, small `pow`, multi-let (incl. ref/cast folds),
//! if/match (incl. guards and plain ident binds rewritten as `_` + scrutinee
//! subst), and Bool comparisons. Body text via `syn` (co-publish-safe).
//!
//! Peeps: wrapping `+0`/`-0`/`*1`/`*0`/`sub(x,x)`; shift/rotate by 0;
//! `is_multiple_of(±1)`; same-path `abs_diff`/`min`/`max`/`clamp(_,y,y)`;
//! `abs`/`saturating_abs` `.is_negative()` → false; const `is_power_of_two` /
//! `count_ones` / `count_zeros` / `trailing_zeros` / `leading_zeros` /
//! `trailing_ones` / `leading_ones` / `reverse_bits` / `swap_bytes` for
//! unsigned and signed path params ≤64 (signed via bit-pattern map;
//! ones via NOT+zeros product; bit products for reverse/swap).
//! Unsigned wrapping_* / shl/shr/rotate via mod 2^w (#1010). Signed
//! wrapping_add/sub/mul/div/rem (and `wrapping_{add,sub}_{signed,unsigned}` aliases)
//! and wrapping_shl via double-mod+reinterpret for i8..i64 (i64 modulus is
//! synthetic `(2^32)*(2^32)`). `wrapping_pow` const exp ≤4.
//! Signed rotate via bit-pattern map. Signed wrapping_shr via floor div by 2^k.
//! Top-level signed `wrapping_neg` (multi-block if); nested signed via modular
//! (0-x) mod 2^w + reinterpret. `wrapping_abs` → `if x >= 0 { x } else { wrapping_neg }`.
//! `wrapping_div`/`wrapping_rem` with nonzero const or positive path-param
//! divisor (MIN/-1 wraps; `/0` stays BNM). Variable wrapping_shl/shr case-sum
//! for bits≤64 (i64 and u64/usize use synthetic 2^64 modulus; 2^63 factor is
//! 2^32*2^31). Variable rotate_left/right case-sum for bits≤64. Variable
//! BitAnd/Or/Xor: const mask (unsigned/signed ≤64; signed via bit-pattern map)
//! or both-variable signed/unsigned ≤64. Variable bitwise `!x` for fixed-width
//! ints ≤64 (`(2^w-1)-u`, synthetic 2^64 for i64/u64). Variable is_power_of_two
//! via pot enum (≤64 exponents incl. u64/usize). Variable `ilog2`/`ilog10`,
//! `next_power_of_two`, and `isqrt` for unsigned path params ≤64.
//! `checked_next_power_of_two`/`checked_shl`/`checked_shr`(const).`unwrap_or` /
//! `unwrap_or_default` (→ `unwrap_or(0)`) and
//! `checked_{add,sub,mul,div,rem,neg,abs,ilog*,npot,pow,shl,shr}(…).is_some()`/`.is_none()`
//! → overflow-bound bools;
//! `overflowing_{add,sub,mul,div,rem,neg,shl,shr,pow}(…).0` → wrapping_* (pow const exp ≤4; div/rem nonzero);
//! `overflowing_*(…).1` → same overflow bool as `checked_*(…).is_none()` (const where required; div/rem refuse 0).
//! `u64`/`usize`
//! `MAX`/`MIN` associated consts. Saturating ops clamp to width (u64 via
//! synthetic max). Literal `/0`, `%0`, `is_multiple_of(0)` BNM. `signum`
//! nestable clamp (#1032). rem_euclid/div_euclid/div_ceil/next_multiple_of with
//! positive const or NonZeroU* path-param divisor (`.get()` peels; signed Euclidean).
//!
//! Multi-block if IR must use **unique temp slots across sibling blocks**.
//! `eval_ir_block` clones parent slots into each block; reusing `$1`/`$2` for
//! temps collides with the condition/`if` result and makes SMT unsound
//! (false Verified). Match `Clamp.ir`: params `$0..$n-1` are shared; temps
//! monotonically increase (see shared `next` in `emit_value_blocks`).

use assura_rust_analyzer::ParamInfo;
use std::cell::{Cell, RefCell};
use std::collections::HashMap;
use syn::spanned::Spanned;

thread_local! {
    /// Saturating op bounds for the current encode (set from return type).
    static SAT_BOUNDS: Cell<Option<(i64, i64)>> = const { Cell::new(None) };
    /// Param name → integer bounds (for methods that need width, e.g. is_power_of_two).
    static PARAM_BOUNDS: RefCell<HashMap<String, (i64, i64)>> = RefCell::new(HashMap::new());
}

use quote::ToTokens;

// Layout (issue #1187):
// - bitops: BitAnd/Or/Xor, bit counts, reverse, ilog, next_power_of_two
// - width: wrap_width, pot exponents, path/receiver bounds, rotl, emit_pow2
// - tests: unit coverage for try_ir_from_rust_body
// - this file: extract/body fold, multi-block if/match, encode_syn_expr dispatch
mod bitops;
mod width;
use bitops::*;
use width::*;

/// Extract a simple trailing return expression for `fn_name` from Rust source.
pub(crate) fn extract_body_return(source: &str, fn_name: &str) -> Option<String> {
    clear_fold_residual();
    let file = syn::parse_file(source).ok()?;
    for item in &file.items {
        match item {
            syn::Item::Fn(func) if func.sig.ident == fn_name => {
                return body_return_from_block(&func.block);
            }
            syn::Item::Impl(imp) => {
                for impl_item in &imp.items {
                    if let syn::ImplItem::Fn(method) = impl_item
                        && method.sig.ident == fn_name
                    {
                        return body_return_from_block(&method.block);
                    }
                }
            }
            _ => {}
        }
    }
    None
}

fn body_return_from_block(block: &syn::Block) -> Option<String> {
    match block.stmts.as_slice() {
        [syn::Stmt::Expr(syn::Expr::Return(ret), _)] => ret.expr.as_ref().map(|e| expr_source(e)),
        [syn::Stmt::Expr(expr, _)] => Some(expr_source(expr)),
        stmts => fold_simple_lets(stmts).map(|e| expr_source(&e)),
    }
}

// Last residual reason when fold fails on a known construct (line-specific BNM).
thread_local! {
    static FOLD_RESIDUAL: RefCell<Option<String>> = const { RefCell::new(None) };
}

/// Reason for the most recent body fold failure (if any). Cleared on success.
pub(crate) fn take_fold_residual() -> Option<String> {
    FOLD_RESIDUAL.with(|c| c.borrow_mut().take())
}

fn set_fold_residual(reason: impl Into<String>) {
    FOLD_RESIDUAL.with(|c| *c.borrow_mut() = Some(reason.into()));
}

fn clear_fold_residual() {
    FOLD_RESIDUAL.with(|c| *c.borrow_mut() = None);
}

/// Fold simple statement sequences into a single expression via substitution
/// (linear SSA + branch-local join for if/match mutation; not full loop SSA).
///
/// Supported:
/// - `let a = e1; let b = a + 1; b` (pure lets; `mut` ok without reassignment)
/// - `let mut y = x; y += 1; y` / `y = y + 1; y` (linear reassignment)
/// - `let mut y = x; if c { y += 1; } y` / if-else / match arm mutation (CFG join)
/// - Final stmt: path / return / expression referencing prior binds
///
/// Not supported (returns None → body_not_modeled): loops with mutation,
/// multi-LHS patterns, type ascriptions on lets, bare mid-block expressions
/// that are not assignments / if / match.
fn fold_simple_lets(stmts: &[syn::Stmt]) -> Option<syn::Expr> {
    clear_fold_residual();
    if stmts.len() < 2 {
        return None;
    }
    let (last, prefix) = stmts.split_last()?;
    // name → current expression (already substituted for earlier names)
    let mut env: Vec<(String, syn::Expr)> = Vec::new();
    let mut assigned = std::collections::HashSet::new();
    for stmt in prefix {
        apply_stmt_to_env(stmt, &mut env, &mut assigned)?;
    }
    let mut final_expr: syn::Expr = match last {
        syn::Stmt::Expr(syn::Expr::Return(ret), _) => (*ret.expr.as_ref()?.as_ref()).clone(),
        syn::Stmt::Expr(e, _) => e.clone(),
        _ => return None,
    };
    for (name, init) in env.into_iter().rev() {
        final_expr = substitute_ident_expr(final_expr, &name, &init);
    }
    // Lift if out of binary operands: `(if c { a } else { b }) + 1` →
    // `if c { a + 1 } else { b + 1 }` so multi-block encode works.
    clear_fold_residual();
    Some(distribute_if_binary(paren_if_match_operands(final_expr)))
}

type SsaEnv = Vec<(String, syn::Expr)>;
type AssignedSet = std::collections::HashSet<String>;

/// Apply one statement to the SSA env (local bind, assign, or if/match join).
///
/// `assigned` records names mutated via `=` / `+=` / … so CFG join does not
/// treat a shadowing `let y = e` as mutation of outer `y`.
fn apply_stmt_to_env(
    stmt: &syn::Stmt,
    env: &mut Vec<(String, syn::Expr)>,
    assigned: &mut AssignedSet,
) -> Option<()> {
    match stmt {
        syn::Stmt::Local(local) => {
            let name = match &local.pat {
                syn::Pat::Ident(id) if id.by_ref.is_none() && id.subpat.is_none() => {
                    id.ident.to_string()
                }
                _ => {
                    set_fold_residual("multi-pattern or typed let not modeled in body SSA");
                    return None;
                }
            };
            let init = local.init.as_ref()?;
            if init.diverge.is_some() {
                return None;
            }
            let mut init_expr = (*init.expr).clone();
            for (n, e) in env.iter().rev() {
                init_expr = substitute_ident_expr(init_expr, n, e);
            }
            // Shadow / rebind for in-scope uses; does NOT count as assignment.
            if let Some((_, slot)) = env.iter_mut().find(|(n, _)| n == &name) {
                *slot = init_expr;
            } else {
                env.push((name, init_expr));
            }
            Some(())
        }
        syn::Stmt::Expr(expr, _) => apply_effect_expr(expr, env, assigned),
        _ => {
            set_fold_residual("unsupported statement form in body SSA");
            None
        }
    }
}

/// Mid-block effect: assignment or if/match mutation join (not loops).
fn apply_effect_expr(
    expr: &syn::Expr,
    env: &mut Vec<(String, syn::Expr)>,
    assigned: &mut AssignedSet,
) -> Option<()> {
    if matches!(expr, syn::Expr::Assign(_))
        || matches!(expr, syn::Expr::Binary(b) if assign_op_to_bin_op(b.op).is_some())
    {
        return apply_linear_assignment(expr, env, assigned).or_else(|| {
            set_fold_residual(format!(
                "assignment to unbound or unsupported LHS (line ~{})",
                expr_approx_line(expr)
            ));
            None
        });
    }
    match expr {
        syn::Expr::If(if_e) => apply_cfg_if(if_e, env, assigned),
        syn::Expr::Match(m) => apply_cfg_match(m, env, assigned),
        syn::Expr::While(_) | syn::Expr::ForLoop(_) | syn::Expr::Loop(_) => {
            set_fold_residual(format!(
                "loop control flow not modeled (line ~{}): rewrite without loop or supply co-located .ir",
                expr_approx_line(expr)
            ));
            None
        }
        syn::Expr::Paren(p) => apply_effect_expr(&p.expr, env, assigned),
        syn::Expr::Group(g) => apply_effect_expr(&g.expr, env, assigned),
        _ => {
            set_fold_residual(format!(
                "mid-block expression not modeled as assignment/if/match (line ~{})",
                expr_approx_line(expr)
            ));
            None
        }
    }
}

fn expr_approx_line(expr: &syn::Expr) -> usize {
    let line = expr.span().start().line;
    if line == 0 { 1 } else { line }
}

/// Apply every statement in a block as env effects (mutation arms).
fn apply_block_to_env(
    block: &syn::Block,
    env: &mut Vec<(String, syn::Expr)>,
    assigned: &mut AssignedSet,
) -> Option<()> {
    for stmt in &block.stmts {
        apply_stmt_to_env(stmt, env, assigned)?;
    }
    Some(())
}

/// Substitute current env into `expr` (names → expressions).
fn subst_env(expr: syn::Expr, env: &[(String, syn::Expr)]) -> syn::Expr {
    let mut out = expr;
    for (n, e) in env.iter().rev() {
        out = substitute_ident_expr(out, n, e);
    }
    out
}

/// Build `if cond { then } else { else }` as a value expression.
fn make_if_value(cond: syn::Expr, then_e: syn::Expr, else_e: syn::Expr) -> syn::Expr {
    syn::Expr::If(syn::ExprIf {
        attrs: Vec::new(),
        if_token: Default::default(),
        cond: Box::new(cond),
        then_branch: syn::Block {
            brace_token: Default::default(),
            stmts: vec![syn::Stmt::Expr(then_e, None)],
        },
        else_branch: Some((
            Default::default(),
            Box::new(syn::Expr::Block(syn::ExprBlock {
                attrs: Vec::new(),
                label: None,
                block: syn::Block {
                    brace_token: Default::default(),
                    stmts: vec![syn::Stmt::Expr(else_e, None)],
                },
            })),
        )),
    })
}

/// Join parent env after if/else mutation arms (phi-style).
/// Only names in then/else `assigned` sets take arm values (not shadowing lets).
fn join_env_after_if(
    cond: syn::Expr,
    then_env: &[(String, syn::Expr)],
    then_assigned: &AssignedSet,
    else_env: &[(String, syn::Expr)],
    else_assigned: &AssignedSet,
    env: &mut [(String, syn::Expr)],
) {
    for (name, parent_val) in env.iter_mut() {
        let then_val = if then_assigned.contains(name) {
            then_env
                .iter()
                .find(|(n, _)| n == name)
                .map(|(_, e)| e.clone())
                .unwrap_or_else(|| parent_val.clone())
        } else {
            parent_val.clone()
        };
        let else_val = if else_assigned.contains(name) {
            else_env
                .iter()
                .find(|(n, _)| n == name)
                .map(|(_, e)| e.clone())
                .unwrap_or_else(|| parent_val.clone())
        } else {
            parent_val.clone()
        };
        if expr_source(&then_val) == expr_source(&else_val) {
            *parent_val = then_val;
        } else {
            *parent_val = make_if_value(cond.clone(), then_val, else_val);
        }
    }
}

/// CFG join for `if cond { …mut… } [else …]`.
fn apply_cfg_if(
    if_e: &syn::ExprIf,
    env: &mut [(String, syn::Expr)],
    parent_assigned: &mut AssignedSet,
) -> Option<()> {
    let cond = subst_env((*if_e.cond).clone(), env);
    let mut then_env: SsaEnv = env.to_vec();
    let mut then_assigned = AssignedSet::new();
    apply_block_to_env(&if_e.then_branch, &mut then_env, &mut then_assigned)?;

    let mut else_env: SsaEnv = env.to_vec();
    let mut else_assigned = AssignedSet::new();
    if let Some((_, else_box)) = &if_e.else_branch {
        match else_box.as_ref() {
            syn::Expr::Block(eb) => {
                apply_block_to_env(&eb.block, &mut else_env, &mut else_assigned)?
            }
            syn::Expr::If(nested) => apply_cfg_if(nested, &mut else_env, &mut else_assigned)?,
            other => apply_effect_expr(other, &mut else_env, &mut else_assigned)?,
        }
    }

    join_env_after_if(
        cond,
        &then_env,
        &then_assigned,
        &else_env,
        &else_assigned,
        env,
    );
    for n in then_assigned.union(&else_assigned) {
        parent_assigned.insert(n.clone());
    }
    Some(())
}

/// CFG join for match with lit / trailing-irrefutable arms that only mutate env.
fn apply_cfg_match(
    m: &syn::ExprMatch,
    env: &mut [(String, syn::Expr)],
    parent_assigned: &mut AssignedSet,
) -> Option<()> {
    if m.arms.is_empty() {
        set_fold_residual("empty match not modeled in body SSA");
        return None;
    }
    let scrut = subst_env((*m.expr).clone(), env);

    // (optional lit eq, env after arm, names assigned in arm)
    let mut arm_results: Vec<(Option<syn::Expr>, SsaEnv, AssignedSet)> = Vec::new();
    let mut saw_irrefutable = false;
    for arm in &m.arms {
        if saw_irrefutable {
            set_fold_residual(format!(
                "match arm after irrefutable pattern not modeled (line ~{})",
                expr_approx_line(&m.expr)
            ));
            return None;
        }
        if matches!(&arm.pat, syn::Pat::Guard(_)) {
            set_fold_residual(format!(
                "match guard mutation not modeled (line ~{})",
                expr_approx_line(&m.expr)
            ));
            return None;
        }
        let (lit_pat, bind_name): (Option<syn::Expr>, Option<String>) = match &arm.pat {
            syn::Pat::Wild(_) => {
                saw_irrefutable = true;
                (None, None)
            }
            syn::Pat::Lit(pl) => (
                Some(syn::Expr::Lit(syn::ExprLit {
                    attrs: Vec::new(),
                    lit: pl.lit.clone(),
                })),
                None,
            ),
            syn::Pat::Ident(id)
                if id.by_ref.is_none() && id.mutability.is_none() && id.subpat.is_none() =>
            {
                // Irrefutable bind: like wild + subst bind → scrut (value-match policy).
                saw_irrefutable = true;
                (None, Some(id.ident.to_string()))
            }
            _ => {
                set_fold_residual(format!(
                    "match pattern not modeled for mutation join (line ~{})",
                    expr_approx_line(&m.expr)
                ));
                return None;
            }
        };
        let mut arm_env: SsaEnv = env.to_vec();
        let mut arm_assigned = AssignedSet::new();
        if let Some(bind) = &bind_name {
            arm_env.push((bind.clone(), scrut.clone()));
        }
        match arm.body.as_ref() {
            syn::Expr::Block(eb) => apply_block_to_env(&eb.block, &mut arm_env, &mut arm_assigned)?,
            other => apply_effect_expr(other, &mut arm_env, &mut arm_assigned)?,
        }
        if let Some(bind) = &bind_name {
            arm_assigned.remove(bind);
        }
        arm_results.push((lit_pat, arm_env, arm_assigned));
    }

    for (name, parent_val) in env.iter_mut() {
        let mut nest: Option<syn::Expr> = None;
        for (lit, arm_env, arm_assigned) in arm_results.iter().rev() {
            let arm_val = if arm_assigned.contains(name) {
                arm_env
                    .iter()
                    .find(|(n, _)| n == name)
                    .map(|(_, e)| e.clone())
                    .unwrap_or_else(|| parent_val.clone())
            } else {
                parent_val.clone()
            };
            nest = Some(match (lit, nest) {
                (None, None) => arm_val,
                (None, Some(_)) => arm_val, // unreachable: arms after irrefutable rejected
                (Some(lit_e), None) => {
                    let cond = make_binary(scrut.clone(), syn::parse_quote!(==), lit_e.clone());
                    make_if_value(cond, arm_val, parent_val.clone())
                }
                (Some(lit_e), Some(else_e)) => {
                    let cond = make_binary(scrut.clone(), syn::parse_quote!(==), lit_e.clone());
                    make_if_value(cond, arm_val, else_e)
                }
            });
        }
        if let Some(joined) = nest {
            *parent_val = joined;
        }
    }
    for (_, _, arm_assigned) in &arm_results {
        for n in arm_assigned {
            parent_assigned.insert(n.clone());
        }
    }
    Some(())
}

/// Apply `x = e` or `x += e` (etc.) to the linear env. Name must already be bound.
fn apply_linear_assignment(
    expr: &syn::Expr,
    env: &mut [(String, syn::Expr)],
    assigned: &mut AssignedSet,
) -> Option<()> {
    match expr {
        syn::Expr::Assign(a) => {
            let name = expr_simple_ident_name(&a.left)?;
            let mut rhs = (*a.right).clone();
            for (n, e) in env.iter().rev() {
                rhs = substitute_ident_expr(rhs, n, e);
            }
            let (_, slot) = env.iter_mut().find(|(n, _)| n == &name)?;
            *slot = rhs;
            assigned.insert(name);
            Some(())
        }
        syn::Expr::Binary(b) => {
            let plain = assign_op_to_bin_op(b.op)?;
            let name = expr_simple_ident_name(&b.left)?;
            let mut rhs = (*b.right).clone();
            for (n, e) in env.iter().rev() {
                rhs = substitute_ident_expr(rhs, n, e);
            }
            let cur = env.iter().find(|(n, _)| n == &name)?.1.clone();
            let combined = syn::Expr::Binary(syn::ExprBinary {
                attrs: Vec::new(),
                left: Box::new(cur),
                op: plain,
                right: Box::new(rhs),
            });
            let (_, slot) = env.iter_mut().find(|(n, _)| n == &name)?;
            *slot = combined;
            assigned.insert(name);
            Some(())
        }
        _ => None,
    }
}

fn expr_simple_ident_name(expr: &syn::Expr) -> Option<String> {
    match expr {
        syn::Expr::Path(p) if p.path.segments.len() == 1 && p.qself.is_none() => {
            Some(p.path.segments[0].ident.to_string())
        }
        syn::Expr::Paren(p) => expr_simple_ident_name(&p.expr),
        _ => None,
    }
}

fn assign_op_to_bin_op(op: syn::BinOp) -> Option<syn::BinOp> {
    match op {
        syn::BinOp::AddAssign(_) => Some(syn::parse_quote!(+)),
        syn::BinOp::SubAssign(_) => Some(syn::parse_quote!(-)),
        syn::BinOp::MulAssign(_) => Some(syn::parse_quote!(*)),
        syn::BinOp::DivAssign(_) => Some(syn::parse_quote!(/)),
        syn::BinOp::RemAssign(_) => Some(syn::parse_quote!(%)),
        syn::BinOp::BitXorAssign(_) => Some(syn::parse_quote!(^)),
        syn::BinOp::BitAndAssign(_) => Some(syn::parse_quote!(&)),
        syn::BinOp::BitOrAssign(_) => Some(syn::parse_quote!(|)),
        syn::BinOp::ShlAssign(_) => Some(syn::parse_quote!(<<)),
        syn::BinOp::ShrAssign(_) => Some(syn::parse_quote!(>>)),
        _ => None,
    }
}

/// Lift if/match out of binary/unary/method so multi-block encode can fire.
/// `(if c { a } else { b }) ⊕ r` → `if c { a ⊕ r } else { b ⊕ r }` (and right/match/unary).
fn distribute_if_binary(expr: syn::Expr) -> syn::Expr {
    match expr {
        syn::Expr::Binary(b) => {
            let left = unwrap_paren(distribute_if_binary(*b.left));
            let right = unwrap_paren(distribute_if_binary(*b.right));
            // (if c { t } else { e }) ⊕ r  →  if c { t ⊕ r } else { e ⊕ r }
            if let Some(lifted) = try_lift_if_left(left.clone(), b.op, right.clone()) {
                return distribute_if_binary(lifted);
            }
            // l ⊕ (if c { t } else { e })  →  if c { l ⊕ t } else { l ⊕ e }
            if let Some(lifted) = try_lift_if_right(left.clone(), b.op, right.clone()) {
                return distribute_if_binary(lifted);
            }
            // (match …) ⊕ r / l ⊕ (match …)
            if let Some(lifted) = try_lift_match_left(left.clone(), b.op, right.clone()) {
                return distribute_if_binary(lifted);
            }
            if let Some(lifted) = try_lift_match_right(left.clone(), b.op, right.clone()) {
                return distribute_if_binary(lifted);
            }
            syn::Expr::Binary(syn::ExprBinary {
                attrs: b.attrs,
                left: Box::new(left),
                op: b.op,
                right: Box::new(right),
            })
        }
        // -(if c { t } else { e }) → if c { -t } else { -e }
        syn::Expr::Unary(u) => {
            let inner = unwrap_paren(distribute_if_binary(*u.expr));
            if let Some(lifted) = try_lift_if_unary(u.op, inner.clone()) {
                return distribute_if_binary(lifted);
            }
            if let Some(lifted) = try_lift_match_unary(u.op, inner.clone()) {
                return distribute_if_binary(lifted);
            }
            syn::Expr::Unary(syn::ExprUnary {
                attrs: u.attrs,
                op: u.op,
                expr: Box::new(inner),
            })
        }
        // (if c { t } else { e }).abs() → if c { t.abs() } else { e.abs() }
        syn::Expr::MethodCall(m) => {
            let recv = unwrap_paren(distribute_if_binary(*m.receiver));
            let args: Vec<syn::Expr> = m.args.into_iter().map(distribute_if_binary).collect();
            if let Some(lifted) = try_lift_if_method(
                recv.clone(),
                m.method.clone(),
                &args,
                &m.turbofish,
                m.attrs.clone(),
            ) {
                return distribute_if_binary(lifted);
            }
            if let Some(lifted) = try_lift_match_method(
                recv.clone(),
                m.method.clone(),
                &args,
                &m.turbofish,
                m.attrs.clone(),
            ) {
                return distribute_if_binary(lifted);
            }
            // recv.m(if c { a } else { b }) → if c { recv.m(a) } else { recv.m(b) }
            if let Some(lifted) = try_lift_if_in_single_method_arg(
                recv.clone(),
                m.method.clone(),
                &args,
                &m.turbofish,
                m.attrs.clone(),
            ) {
                return distribute_if_binary(lifted);
            }
            syn::Expr::MethodCall(syn::ExprMethodCall {
                attrs: m.attrs,
                receiver: Box::new(recv),
                dot_token: m.dot_token,
                method: m.method,
                turbofish: m.turbofish,
                paren_token: m.paren_token,
                args: args.into_iter().collect(),
            })
        }
        // (if c { t } else { e }) as T → if c { t as T } else { e as T }
        syn::Expr::Cast(c) => {
            let inner = unwrap_paren(distribute_if_binary(*c.expr));
            if let Some(lifted) = try_lift_if_cast(inner.clone(), c.ty.clone()) {
                return distribute_if_binary(lifted);
            }
            if let Some(lifted) = try_lift_match_cast(inner.clone(), c.ty.clone()) {
                return distribute_if_binary(lifted);
            }
            syn::Expr::Cast(syn::ExprCast {
                attrs: c.attrs,
                expr: Box::new(inner),
                as_token: c.as_token,
                ty: c.ty,
            })
        }
        syn::Expr::If(mut if_e) => {
            // Distribute inside then/else so nested if⊕if settles.
            if_e.then_branch = map_block_expr(if_e.then_branch, distribute_if_binary);
            if let Some((tok, else_box)) = if_e.else_branch.take() {
                let else_e = distribute_if_binary(*else_box);
                if_e.else_branch = Some((tok, Box::new(else_e)));
            }
            syn::Expr::If(if_e)
        }
        syn::Expr::Match(mut m) => {
            m.arms = m
                .arms
                .into_iter()
                .map(|mut arm| {
                    arm.body = Box::new(distribute_if_binary(*arm.body));
                    arm
                })
                .collect();
            syn::Expr::Match(m)
        }
        // else-branches and arm bodies are often `Expr::Block { binary… }`.
        syn::Expr::Block(mut eb) => {
            eb.block = map_block_expr(eb.block, distribute_if_binary);
            syn::Expr::Block(eb)
        }
        syn::Expr::Paren(mut p) => {
            *p.expr = distribute_if_binary(*p.expr);
            syn::Expr::Paren(p)
        }
        other => other,
    }
}

fn unwrap_paren(expr: syn::Expr) -> syn::Expr {
    match expr {
        syn::Expr::Paren(p) => unwrap_paren(*p.expr),
        other => other,
    }
}

fn block_inner_expr(block: &syn::Block) -> syn::Expr {
    block_as_expr_owned(block).unwrap_or_else(|| {
        syn::Expr::Block(syn::ExprBlock {
            attrs: Vec::new(),
            label: None,
            block: block.clone(),
        })
    })
}

fn else_inner_expr(else_box: &syn::Expr) -> syn::Expr {
    match else_box {
        syn::Expr::Block(eb) => block_inner_expr(&eb.block),
        other => other.clone(),
    }
}

fn make_binary(left: syn::Expr, op: syn::BinOp, right: syn::Expr) -> syn::Expr {
    syn::Expr::Binary(syn::ExprBinary {
        attrs: Vec::new(),
        left: Box::new(left),
        op,
        right: Box::new(right),
    })
}

fn try_lift_if_left(left: syn::Expr, op: syn::BinOp, right: syn::Expr) -> Option<syn::Expr> {
    let syn::Expr::If(mut if_e) = left else {
        return None;
    };
    let (else_tok, else_box) = if_e.else_branch.take()?;
    let then_inner = block_inner_expr(&if_e.then_branch);
    let else_inner = else_inner_expr(&else_box);
    if_e.then_branch = expr_as_block(make_binary(then_inner, op, right.clone()));
    if_e.else_branch = Some((
        else_tok,
        Box::new(syn::Expr::Block(syn::ExprBlock {
            attrs: Vec::new(),
            label: None,
            block: expr_as_block(make_binary(else_inner, op, right)),
        })),
    ));
    Some(syn::Expr::If(if_e))
}

fn try_lift_if_right(left: syn::Expr, op: syn::BinOp, right: syn::Expr) -> Option<syn::Expr> {
    let syn::Expr::If(mut if_e) = right else {
        return None;
    };
    let (else_tok, else_box) = if_e.else_branch.take()?;
    let then_inner = block_inner_expr(&if_e.then_branch);
    let else_inner = else_inner_expr(&else_box);
    if_e.then_branch = expr_as_block(make_binary(left.clone(), op, then_inner));
    if_e.else_branch = Some((
        else_tok,
        Box::new(syn::Expr::Block(syn::ExprBlock {
            attrs: Vec::new(),
            label: None,
            block: expr_as_block(make_binary(left, op, else_inner)),
        })),
    ));
    Some(syn::Expr::If(if_e))
}

fn try_lift_match_left(left: syn::Expr, op: syn::BinOp, right: syn::Expr) -> Option<syn::Expr> {
    let syn::Expr::Match(mut m) = left else {
        return None;
    };
    m.arms = m
        .arms
        .into_iter()
        .map(|mut arm| {
            let body = match arm.body.as_ref() {
                syn::Expr::Block(eb) => block_inner_expr(&eb.block),
                other => other.clone(),
            };
            arm.body = Box::new(make_binary(body, op, right.clone()));
            arm
        })
        .collect();
    Some(syn::Expr::Match(m))
}

fn try_lift_match_right(left: syn::Expr, op: syn::BinOp, right: syn::Expr) -> Option<syn::Expr> {
    let syn::Expr::Match(mut m) = right else {
        return None;
    };
    m.arms = m
        .arms
        .into_iter()
        .map(|mut arm| {
            let body = match arm.body.as_ref() {
                syn::Expr::Block(eb) => block_inner_expr(&eb.block),
                other => other.clone(),
            };
            arm.body = Box::new(make_binary(left.clone(), op, body));
            arm
        })
        .collect();
    Some(syn::Expr::Match(m))
}

fn make_unary(op: syn::UnOp, expr: syn::Expr) -> syn::Expr {
    syn::Expr::Unary(syn::ExprUnary {
        attrs: Vec::new(),
        op,
        expr: Box::new(expr),
    })
}

fn try_lift_if_unary(op: syn::UnOp, inner: syn::Expr) -> Option<syn::Expr> {
    let syn::Expr::If(mut if_e) = inner else {
        return None;
    };
    let (else_tok, else_box) = if_e.else_branch.take()?;
    let then_inner = block_inner_expr(&if_e.then_branch);
    let else_inner = else_inner_expr(&else_box);
    if_e.then_branch = expr_as_block(make_unary(op, then_inner));
    if_e.else_branch = Some((
        else_tok,
        Box::new(syn::Expr::Block(syn::ExprBlock {
            attrs: Vec::new(),
            label: None,
            block: expr_as_block(make_unary(op, else_inner)),
        })),
    ));
    Some(syn::Expr::If(if_e))
}

fn try_lift_match_unary(op: syn::UnOp, inner: syn::Expr) -> Option<syn::Expr> {
    let syn::Expr::Match(mut m) = inner else {
        return None;
    };
    m.arms = m
        .arms
        .into_iter()
        .map(|mut arm| {
            let body = match arm.body.as_ref() {
                syn::Expr::Block(eb) => block_inner_expr(&eb.block),
                other => other.clone(),
            };
            arm.body = Box::new(make_unary(op, body));
            arm
        })
        .collect();
    Some(syn::Expr::Match(m))
}

fn make_method(
    recv: syn::Expr,
    method: syn::Ident,
    args: &[syn::Expr],
    turbofish: &Option<syn::AngleBracketedGenericArguments>,
    attrs: Vec<syn::Attribute>,
) -> syn::Expr {
    syn::Expr::MethodCall(syn::ExprMethodCall {
        attrs,
        receiver: Box::new(recv),
        dot_token: Default::default(),
        method,
        turbofish: turbofish.clone(),
        paren_token: Default::default(),
        args: args.iter().cloned().collect(),
    })
}

fn try_lift_if_method(
    recv: syn::Expr,
    method: syn::Ident,
    args: &[syn::Expr],
    turbofish: &Option<syn::AngleBracketedGenericArguments>,
    attrs: Vec<syn::Attribute>,
) -> Option<syn::Expr> {
    let syn::Expr::If(mut if_e) = recv else {
        return None;
    };
    let (else_tok, else_box) = if_e.else_branch.take()?;
    let then_inner = block_inner_expr(&if_e.then_branch);
    let else_inner = else_inner_expr(&else_box);
    if_e.then_branch = expr_as_block(make_method(
        then_inner,
        method.clone(),
        args,
        turbofish,
        attrs.clone(),
    ));
    if_e.else_branch = Some((
        else_tok,
        Box::new(syn::Expr::Block(syn::ExprBlock {
            attrs: Vec::new(),
            label: None,
            block: expr_as_block(make_method(else_inner, method, args, turbofish, attrs)),
        })),
    ));
    Some(syn::Expr::If(if_e))
}

fn try_lift_match_method(
    recv: syn::Expr,
    method: syn::Ident,
    args: &[syn::Expr],
    turbofish: &Option<syn::AngleBracketedGenericArguments>,
    attrs: Vec<syn::Attribute>,
) -> Option<syn::Expr> {
    let syn::Expr::Match(mut m) = recv else {
        return None;
    };
    m.arms = m
        .arms
        .into_iter()
        .map(|mut arm| {
            let body = match arm.body.as_ref() {
                syn::Expr::Block(eb) => block_inner_expr(&eb.block),
                other => other.clone(),
            };
            arm.body = Box::new(make_method(
                body,
                method.clone(),
                args,
                turbofish,
                attrs.clone(),
            ));
            arm
        })
        .collect();
    Some(syn::Expr::Match(m))
}

fn try_lift_if_in_single_method_arg(
    recv: syn::Expr,
    method: syn::Ident,
    args: &[syn::Expr],
    turbofish: &Option<syn::AngleBracketedGenericArguments>,
    attrs: Vec<syn::Attribute>,
) -> Option<syn::Expr> {
    if args.len() != 1 {
        return None;
    }
    let arg = unwrap_paren(args[0].clone());
    let syn::Expr::If(mut if_e) = arg else {
        return None;
    };
    let (else_tok, else_box) = if_e.else_branch.take()?;
    let then_inner = block_inner_expr(&if_e.then_branch);
    let else_inner = else_inner_expr(&else_box);
    if_e.then_branch = expr_as_block(make_method(
        recv.clone(),
        method.clone(),
        &[then_inner],
        turbofish,
        attrs.clone(),
    ));
    if_e.else_branch = Some((
        else_tok,
        Box::new(syn::Expr::Block(syn::ExprBlock {
            attrs: Vec::new(),
            label: None,
            block: expr_as_block(make_method(recv, method, &[else_inner], turbofish, attrs)),
        })),
    ));
    Some(syn::Expr::If(if_e))
}

fn make_cast(expr: syn::Expr, ty: Box<syn::Type>) -> syn::Expr {
    syn::Expr::Cast(syn::ExprCast {
        attrs: Vec::new(),
        expr: Box::new(expr),
        as_token: Default::default(),
        ty,
    })
}

fn try_lift_if_cast(inner: syn::Expr, ty: Box<syn::Type>) -> Option<syn::Expr> {
    let syn::Expr::If(mut if_e) = inner else {
        return None;
    };
    let (else_tok, else_box) = if_e.else_branch.take()?;
    let then_inner = block_inner_expr(&if_e.then_branch);
    let else_inner = else_inner_expr(&else_box);
    if_e.then_branch = expr_as_block(make_cast(then_inner, ty.clone()));
    if_e.else_branch = Some((
        else_tok,
        Box::new(syn::Expr::Block(syn::ExprBlock {
            attrs: Vec::new(),
            label: None,
            block: expr_as_block(make_cast(else_inner, ty)),
        })),
    ));
    Some(syn::Expr::If(if_e))
}

fn try_lift_match_cast(inner: syn::Expr, ty: Box<syn::Type>) -> Option<syn::Expr> {
    let syn::Expr::Match(mut m) = inner else {
        return None;
    };
    m.arms = m
        .arms
        .into_iter()
        .map(|mut arm| {
            let body = match arm.body.as_ref() {
                syn::Expr::Block(eb) => block_inner_expr(&eb.block),
                other => other.clone(),
            };
            arm.body = Box::new(make_cast(body, ty.clone()));
            arm
        })
        .collect();
    Some(syn::Expr::Match(m))
}

fn map_block_expr(block: syn::Block, f: impl Fn(syn::Expr) -> syn::Expr) -> syn::Block {
    match block.stmts.as_slice() {
        [syn::Stmt::Expr(e, semi)] => {
            let e2 = f(e.clone());
            syn::Block {
                brace_token: block.brace_token,
                stmts: vec![syn::Stmt::Expr(e2, *semi)],
            }
        }
        _ => block,
    }
}

fn expr_as_block(expr: syn::Expr) -> syn::Block {
    syn::Block {
        brace_token: Default::default(),
        stmts: vec![syn::Stmt::Expr(expr, None)],
    }
}

/// Wrap if/match subexpressions that appear as operands so `expr_source` round-trips.
fn paren_if_match_operands(expr: syn::Expr) -> syn::Expr {
    match expr {
        syn::Expr::Binary(mut b) => {
            *b.left = paren_if_match_leaf(paren_if_match_operands(*b.left));
            *b.right = paren_if_match_leaf(paren_if_match_operands(*b.right));
            syn::Expr::Binary(b)
        }
        syn::Expr::Unary(mut u) => {
            *u.expr = paren_if_match_leaf(paren_if_match_operands(*u.expr));
            syn::Expr::Unary(u)
        }
        syn::Expr::MethodCall(mut m) => {
            *m.receiver = paren_if_match_leaf(paren_if_match_operands(*m.receiver));
            let args: Vec<syn::Expr> = m
                .args
                .into_iter()
                .map(|a| paren_if_match_leaf(paren_if_match_operands(a)))
                .collect();
            m.args = args.into_iter().collect();
            syn::Expr::MethodCall(m)
        }
        syn::Expr::Call(mut c) => {
            *c.func = paren_if_match_operands(*c.func);
            let args: Vec<syn::Expr> = c
                .args
                .into_iter()
                .map(|a| paren_if_match_leaf(paren_if_match_operands(a)))
                .collect();
            c.args = args.into_iter().collect();
            syn::Expr::Call(c)
        }
        syn::Expr::Paren(mut p) => {
            *p.expr = paren_if_match_operands(*p.expr);
            syn::Expr::Paren(p)
        }
        other => other,
    }
}

fn paren_if_match_leaf(expr: syn::Expr) -> syn::Expr {
    match expr {
        syn::Expr::If(_) | syn::Expr::Match(_) => syn::Expr::Paren(syn::ExprParen {
            attrs: Vec::new(),
            paren_token: Default::default(),
            expr: Box::new(expr),
        }),
        other => other,
    }
}

/// Replace free path `name` with `replacement` (structural, supported expr kinds).
fn substitute_ident_expr(expr: syn::Expr, name: &str, replacement: &syn::Expr) -> syn::Expr {
    match expr {
        syn::Expr::Path(ref p) if p.path.segments.len() == 1 => {
            if p.path.segments[0].ident == name {
                replacement.clone()
            } else {
                expr
            }
        }
        syn::Expr::Paren(mut p) => {
            *p.expr = substitute_ident_expr(*p.expr, name, replacement);
            syn::Expr::Paren(p)
        }
        syn::Expr::Group(mut g) => {
            *g.expr = substitute_ident_expr(*g.expr, name, replacement);
            syn::Expr::Group(g)
        }
        syn::Expr::Unary(mut u) => {
            *u.expr = substitute_ident_expr(*u.expr, name, replacement);
            syn::Expr::Unary(u)
        }
        syn::Expr::Reference(mut r) => {
            *r.expr = substitute_ident_expr(*r.expr, name, replacement);
            syn::Expr::Reference(r)
        }
        syn::Expr::Cast(mut c) => {
            *c.expr = substitute_ident_expr(*c.expr, name, replacement);
            syn::Expr::Cast(c)
        }
        syn::Expr::Binary(mut b) => {
            *b.left = substitute_ident_expr(*b.left, name, replacement);
            *b.right = substitute_ident_expr(*b.right, name, replacement);
            syn::Expr::Binary(b)
        }
        syn::Expr::MethodCall(mut m) => {
            *m.receiver = substitute_ident_expr(*m.receiver, name, replacement);
            let args: Vec<syn::Expr> = m
                .args
                .into_iter()
                .map(|a| substitute_ident_expr(a, name, replacement))
                .collect();
            m.args = args.into_iter().collect();
            syn::Expr::MethodCall(m)
        }
        syn::Expr::Call(mut c) => {
            *c.func = substitute_ident_expr(*c.func, name, replacement);
            let args: Vec<syn::Expr> = c
                .args
                .into_iter()
                .map(|a| substitute_ident_expr(a, name, replacement))
                .collect();
            c.args = args.into_iter().collect();
            syn::Expr::Call(c)
        }
        // CFG join leaves if/match trees that still mention bound names.
        syn::Expr::If(mut if_e) => {
            *if_e.cond = substitute_ident_expr(*if_e.cond, name, replacement);
            if_e.then_branch = map_block_expr(if_e.then_branch, |e| {
                substitute_ident_expr(e, name, replacement)
            });
            if let Some((tok, else_box)) = if_e.else_branch.take() {
                let else_e = substitute_ident_expr(*else_box, name, replacement);
                if_e.else_branch = Some((tok, Box::new(else_e)));
            }
            syn::Expr::If(if_e)
        }
        syn::Expr::Match(mut m) => {
            *m.expr = substitute_ident_expr(*m.expr, name, replacement);
            m.arms = m
                .arms
                .into_iter()
                .map(|mut arm| {
                    arm.body = Box::new(substitute_ident_expr(*arm.body, name, replacement));
                    arm
                })
                .collect();
            syn::Expr::Match(m)
        }
        syn::Expr::Block(mut eb) => {
            eb.block = map_block_expr(eb.block, |e| substitute_ident_expr(e, name, replacement));
            syn::Expr::Block(eb)
        }
        other => other,
    }
}

fn expr_source(expr: &syn::Expr) -> String {
    // Parenthesize if/match so `if c { a } else { b } + 1` re-parses as binary
    // after let-fold (ToTokens does not insert precedence parens).
    let raw = expr
        .to_token_stream()
        .to_string()
        .split_whitespace()
        .collect::<Vec<_>>()
        .join(" ");
    if matches!(expr, syn::Expr::If(_) | syn::Expr::Match(_)) {
        format!("({raw})")
    } else {
        raw
    }
}

/// Build IR text for a function if `body_return` is a simple supported shape.
pub(crate) fn try_ir_from_rust_body(
    item_name: &str,
    params: &[ParamInfo],
    return_ty: Option<&str>,
    body_return: &str,
) -> Option<String> {
    let ret_assura = return_ty
        .map(assura_codegen::type_map::rust_type_to_assura)
        .unwrap_or_else(|| "Int".to_string());
    if !matches!(ret_assura.as_str(), "Int" | "Nat" | "Bool") {
        return None;
    }
    let sat = rust_int_bounds(return_ty.map(str::trim).unwrap_or(""));
    SAT_BOUNDS.set(sat);

    let mut pbounds: HashMap<String, (i64, i64)> = HashMap::new();
    for p in params.iter().filter(|p| p.name != "self") {
        if let Some(b) = rust_int_bounds(p.ty.trim()) {
            pbounds.insert(p.name.clone(), b);
        }
    }
    PARAM_BOUNDS.with(|c| *c.borrow_mut() = pbounds);

    let param_names: Vec<&str> = params
        .iter()
        .filter(|p| p.name != "self")
        .map(|p| p.name.as_str())
        .collect();
    if param_names.is_empty() {
        return None;
    }

    for p in params.iter().filter(|p| p.name != "self") {
        let ty = assura_codegen::type_map::rust_type_to_assura(&p.ty);
        if !matches!(ty.as_str(), "Int" | "Nat" | "Bool") {
            return None;
        }
    }

    let mut expr: syn::Expr = syn::parse_str(body_return).ok()?;
    // wrapping_abs → if >=0 id else wrapping_neg (before wrapping_neg expand).
    if let Some(e) = expand_wrapping_abs_method(&expr) {
        expr = e;
    }
    // Top-level wrapping_neg → multi-block if (MIN stays MIN). Nested signed uses
    // modular encode in the method arm (same bit pattern).
    if let Some(e) = expand_wrapping_neg_method(&expr) {
        expr = e;
    }
    if let Some(e) = expand_checked_binop_unwrap_or(&expr) {
        expr = e;
    }
    if let Some(e) = expand_checked_is_some_none(&expr) {
        expr = e;
    }
    if let Some(e) = expand_overflowing_binop_tuple0(&expr) {
        expr = e;
    }
    if let Some(e) = expand_overflowing_binop_tuple1(&expr) {
        expr = e;
    }
    // `(if c { a } else { b }) + 1` → `if c { a + 1 } else { b + 1 }` for multi-block.
    expr = distribute_if_binary(paren_if_match_operands(expr));
    // `expr_source` parenthesizes top-level if/match; strip so multi-block match hits.
    // Also peel identity `&` / `*` layers (`*& (if …)`).
    loop {
        expr = match expr {
            syn::Expr::Paren(p) => *p.expr,
            syn::Expr::Reference(r) => *r.expr,
            syn::Expr::Unary(u) if matches!(u.op, syn::UnOp::Deref(_)) => *u.expr,
            other => {
                expr = other;
                break;
            }
        };
    }

    let mut sig_parts = Vec::new();
    for (i, p) in params.iter().filter(|p| p.name != "self").enumerate() {
        let ty = assura_codegen::type_map::rust_type_to_assura(&p.ty);
        sig_parts.push(format!("${i}: {ty}"));
    }
    let sig = sig_parts.join(", ");

    // If / match (including nested): multi-block IR (Clamp.ir style).
    if matches!(expr, syn::Expr::If(_) | syn::Expr::Match(_)) {
        return try_ir_from_if_tree(item_name, &sig, &ret_assura, &param_names, &expr);
    }

    let mut lines = Vec::new();
    let mut next = param_names.len();
    let result_slot = encode_syn_expr(&expr, &param_names, &mut lines, &mut next)?;
    let result_ty = if ret_assura == "Bool" { "Bool" } else { "Int" };
    lines.push(format!("$result = load ${result_slot} : {result_ty}"));

    let mut ir = String::new();
    ir.push_str(&format!("module {item_name} {{\n"));
    ir.push_str(&format!("  fn #0 : ({sig}) -> {ret_assura} ! pure\n"));
    ir.push_str("  {\n");
    for line in lines {
        ir.push_str("    ");
        ir.push_str(&line);
        ir.push('\n');
    }
    ir.push_str("  }\n");
    ir.push_str("}\n");
    Some(ir)
}

/// Flatten if/else-if tree into numbered IR functions with unique temp slots.
fn try_ir_from_if_tree(
    item_name: &str,
    sig: &str,
    ret_assura: &str,
    param_names: &[&str],
    root: &syn::Expr,
) -> Option<String> {
    let mut blocks: Vec<(usize, Vec<String>)> = Vec::new();
    let mut next_block = 0usize;
    // Shared across all blocks: params 0..n-1 stay shared; temps never reuse.
    let mut next_slot = param_names.len();
    let entry = emit_value_blocks(
        root,
        param_names,
        ret_assura,
        &mut blocks,
        &mut next_block,
        &mut next_slot,
    )?;
    if entry != 0 {
        return None;
    }

    let mut ir = String::new();
    ir.push_str(&format!("module {item_name} {{\n"));
    for (id, lines) in &blocks {
        let fn_sig = if *id == 0 {
            format!("({sig}) -> {ret_assura}")
        } else {
            format!("() -> {ret_assura}")
        };
        ir.push_str(&format!("  fn #{id} : {fn_sig} ! pure\n  {{\n"));
        for line in lines {
            ir.push_str("    ");
            ir.push_str(line);
            ir.push('\n');
        }
        ir.push_str("  }\n");
    }
    ir.push_str("}\n");
    Some(ir)
}

/// Emit IR for a value expression that may be a nested if/match. Returns block id.
fn emit_value_blocks(
    expr: &syn::Expr,
    param_names: &[&str],
    ret_assura: &str,
    blocks: &mut Vec<(usize, Vec<String>)>,
    next_block: &mut usize,
    next_slot: &mut usize,
) -> Option<usize> {
    match expr {
        syn::Expr::If(if_expr) => {
            let else_expr = if_expr.else_branch.as_ref()?.1.as_ref();
            let then_expr = block_as_expr_owned(&if_expr.then_branch)?;
            let else_expr = match else_expr {
                syn::Expr::Block(b) => block_as_expr_owned(&b.block)?,
                other => other.clone(),
            };

            let this_id = *next_block;
            *next_block += 1;
            // Reserve this block slot (filled after children so ids are sequential-ish)
            blocks.push((this_id, Vec::new()));

            let then_id = emit_value_blocks(
                &then_expr,
                param_names,
                ret_assura,
                blocks,
                next_block,
                next_slot,
            )?;
            let else_id = emit_value_blocks(
                &else_expr,
                param_names,
                ret_assura,
                blocks,
                next_block,
                next_slot,
            )?;

            let mut main_lines = Vec::new();
            let cond_slot =
                encode_syn_expr(&if_expr.cond, param_names, &mut main_lines, next_slot)?;
            let if_out = *next_slot;
            *next_slot += 1;
            main_lines.push(format!(
                "${if_out} = if ${cond_slot} then #{then_id} else #{else_id} : {ret_assura}"
            ));
            main_lines.push(format!("$result = load ${if_out} : {ret_assura}"));

            if let Some((_, lines)) = blocks.iter_mut().find(|(id, _)| *id == this_id) {
                *lines = main_lines;
            }
            Some(this_id)
        }
        syn::Expr::Match(m) => {
            // Prefer identity-guard rewrite to if-tree (#999); else lit/_ match (#993).
            if let Some(if_tree) = match_identity_guards_to_if(m) {
                return emit_value_blocks(
                    &if_tree,
                    param_names,
                    ret_assura,
                    blocks,
                    next_block,
                    next_slot,
                );
            }
            if m.arms.is_empty() {
                return None;
            }
            let this_id = *next_block;
            *next_block += 1;
            blocks.push((this_id, Vec::new()));

            let mut arm_specs: Vec<(String, usize)> = Vec::new();
            for arm in &m.arms {
                // syn 3: match guards are Pat::Guard, not Arm.guard
                if matches!(&arm.pat, syn::Pat::Guard(_)) {
                    return None;
                }
                // Plain `n => body`: rewrite as `_ => body[n:=scrut]` (IR match has no binds).
                let (pat, body_expr) = if let syn::Pat::Ident(id) = &arm.pat {
                    if id.by_ref.is_some() || id.mutability.is_some() || id.subpat.is_some() {
                        return None;
                    }
                    let name = id.ident.to_string();
                    let raw_body = match arm.body.as_ref() {
                        syn::Expr::Block(b) => block_as_expr_owned(&b.block)?,
                        other => other.clone(),
                    };
                    let body = substitute_ident_expr(raw_body, &name, m.expr.as_ref());
                    ("_".into(), body)
                } else {
                    let pat = match_pattern_ir(&arm.pat)?;
                    let body = match arm.body.as_ref() {
                        syn::Expr::Block(b) => block_as_expr_owned(&b.block)?,
                        other => other.clone(),
                    };
                    (pat, body)
                };
                let arm_id = emit_value_blocks(
                    &body_expr,
                    param_names,
                    ret_assura,
                    blocks,
                    next_block,
                    next_slot,
                )?;
                arm_specs.push((pat, arm_id));
            }

            let mut main_lines = Vec::new();
            let scrut = encode_syn_expr(&m.expr, param_names, &mut main_lines, next_slot)?;
            let arms_joined = arm_specs
                .iter()
                .map(|(p, id)| format!("{p} => #{id}"))
                .collect::<Vec<_>>()
                .join(", ");
            let out = *next_slot;
            *next_slot += 1;
            main_lines.push(format!(
                "${out} = match ${scrut} {{ {arms_joined} }} : {ret_assura}"
            ));
            main_lines.push(format!("$result = load ${out} : {ret_assura}"));

            if let Some((_, lines)) = blocks.iter_mut().find(|(id, _)| *id == this_id) {
                *lines = main_lines;
            }
            Some(this_id)
        }
        other => {
            let this_id = *next_block;
            *next_block += 1;
            let mut lines = Vec::new();
            let slot = encode_syn_expr(other, param_names, &mut lines, next_slot)?;
            let ty = if ret_assura == "Bool" { "Bool" } else { "Int" };
            lines.push(format!("$result = load ${slot} : {ty}"));
            blocks.push((this_id, lines));
            Some(this_id)
        }
    }
}

/// IR match pattern text for a simple arm (int/bool/wildcard only).
fn match_pattern_ir(pat: &syn::Pat) -> Option<String> {
    match pat {
        syn::Pat::Wild(_) => Some("_".into()),
        syn::Pat::Lit(lit) => match &lit.lit {
            syn::Lit::Int(n) => {
                let _ = n.base10_digits().parse::<i64>().ok()?;
                Some(n.base10_digits().to_string())
            }
            syn::Lit::Bool(b) => Some(if b.value {
                "true".into()
            } else {
                "false".into()
            }),
            _ => None,
        },
        // `true` / `false` as path patterns
        syn::Pat::Path(p) if p.path.segments.len() == 1 => {
            let name = p.path.segments[0].ident.to_string();
            if name == "true" || name == "false" {
                Some(name)
            } else {
                None
            }
        }
        _ => None,
    }
}

/// Rewrite `match x { n if cond(n) => body, _ => e }` into nested if-tree (#999).
/// Binding + guard arms: substitute the scrutinee for the bind in guard and body.
/// Final arm must be `_` without guard. No plain bindings without guards.
fn match_identity_guards_to_if(m: &syn::ExprMatch) -> Option<syn::Expr> {
    if m.arms.len() < 2 {
        return None;
    }
    let mut nest: Option<String> = None;
    for arm in m.arms.iter().rev() {
        let body = match arm.body.as_ref() {
            syn::Expr::Block(b) => block_as_expr_owned(&b.block)?,
            other => other.clone(),
        };
        match &arm.pat {
            syn::Pat::Wild(_) => {
                if nest.is_some() {
                    return None;
                }
                nest = Some(format!("( {} )", expr_source(&body)));
            }
            // syn 3: `n if cond => body` is Pat::Guard wrapping Pat::Ident
            syn::Pat::Guard(g)
                if let syn::Pat::Ident(id) = g.pat.as_ref()
                    && id.by_ref.is_none()
                    && id.mutability.is_none() =>
            {
                let bind = id.ident.to_string();
                let guard_sub = substitute_ident_expr((*g.guard).clone(), &bind, &m.expr);
                let body_sub = substitute_ident_expr(body, &bind, &m.expr);
                let cond_src = expr_source(&guard_sub);
                let then_src = expr_source(&body_sub);
                let else_src = nest?;
                nest = Some(format!(
                    "if {cond_src} {{ {then_src} }} else {{ {else_src} }}"
                ));
            }
            _ => return None,
        }
    }
    let tree = nest?;
    syn::parse_str(&tree).ok()
}

/// Branch/arm body as owned expression (return, single expr, multi-let fold).
fn block_as_expr_owned(block: &syn::Block) -> Option<syn::Expr> {
    match block.stmts.as_slice() {
        [syn::Stmt::Expr(syn::Expr::Return(ret), _)] => {
            Some((*ret.expr.as_ref()?.as_ref()).clone())
        }
        [syn::Stmt::Expr(e, _)] => Some(e.clone()),
        stmts => fold_simple_lets(stmts),
    }
}

/// `x.checked_*(…).is_some()` / `.is_none()` → overflow-bound bool.
/// Mirrors `unwrap_or` thresholds for the same checked surface (const where required).
/// Bounds come from the receiver (return type is often `bool`, so SAT_BOUNDS is empty).
fn expand_checked_is_some_none(expr: &syn::Expr) -> Option<syn::Expr> {
    let syn::Expr::MethodCall(outer) = expr else {
        return None;
    };
    let want_some = match outer.method.to_string().as_str() {
        "is_some" if outer.args.is_empty() => true,
        "is_none" if outer.args.is_empty() => false,
        _ => return None,
    };
    let syn::Expr::MethodCall(inner) = outer.receiver.as_ref() else {
        return None;
    };
    let method = inner.method.to_string();
    let (lo, hi) = wrap_bounds_for(&inner.receiver)?;
    let recv = expr_source(&inner.receiver);

    let some_tree = if matches!(method.as_str(), "checked_neg" | "checked_abs")
        && inner.args.is_empty()
    {
        if lo < 0 {
            let lo_src = if lo == i64::MIN {
                format!("-{} - 1", i64::MAX)
            } else {
                lo.to_string()
            };
            // None only at MIN for signed checked_neg/abs.
            format!("{recv} != ({lo_src})")
        } else {
            "true".to_string()
        }
    } else if matches!(method.as_str(), "checked_ilog2" | "checked_ilog10") && inner.args.is_empty()
    {
        // None for non-positive (matches unwrap_or peep).
        format!("{recv} > 0")
    } else if method == "checked_next_power_of_two" && inner.args.is_empty() {
        // Unsigned only; pot encode returns 0 on overflow.
        if lo != 0 {
            return None;
        }
        let (bits, _, _) = wrap_width(lo, hi)?;
        if bits == 0 || bits > 64 {
            return None;
        }
        format!("({recv}).next_power_of_two() != 0")
    } else if matches!(method.as_str(), "checked_shl" | "checked_shr") && inner.args.len() == 1 {
        let n = lit_int_i64(&inner.args[0])?;
        if n < 0 {
            return None;
        }
        let (bits, _, _) = wrap_width(lo, hi)?;
        if (n as u64) >= u64::from(bits) {
            "false".to_string()
        } else {
            "true".to_string()
        }
    } else if matches!(
        method.as_str(),
        "checked_add"
            | "checked_sub"
            | "checked_mul"
            | "checked_div"
            | "checked_rem"
            | "checked_pow"
    ) && inner.args.len() == 1
    {
        let c = lit_int_i64(&inner.args[0])?;
        match method.as_str() {
            "checked_add" => {
                if c == 0 {
                    "true".to_string()
                } else if c > 0 {
                    let thr = hi.checked_sub(c)?;
                    format!("{recv} <= ({thr})")
                } else {
                    let thr = lo.checked_sub(c)?;
                    format!("{recv} >= ({thr})")
                }
            }
            "checked_sub" => {
                if c == 0 {
                    "true".to_string()
                } else if c > 0 {
                    let thr = lo.checked_add(c)?;
                    format!("{recv} >= ({thr})")
                } else {
                    let thr = hi.checked_add(c)?;
                    format!("{recv} <= ({thr})")
                }
            }
            "checked_mul" => {
                if c == 0 || c == 1 {
                    "true".to_string()
                } else if c == -1 {
                    if lo < 0 {
                        let lo_src = if lo == i64::MIN {
                            format!("-{} - 1", i64::MAX)
                        } else {
                            lo.to_string()
                        };
                        format!("{recv} != ({lo_src})")
                    } else {
                        "true".to_string()
                    }
                } else if c == 2 {
                    let thr_hi = hi / 2;
                    let thr_lo = lo / 2;
                    format!("{recv} <= ({thr_hi}) && {recv} >= ({thr_lo})")
                } else {
                    return None;
                }
            }
            "checked_div" | "checked_rem" => {
                if c == 0 {
                    "false".to_string()
                } else if c == -1 && lo < 0 {
                    let lo_src = if lo == i64::MIN {
                        format!("-{} - 1", i64::MAX)
                    } else {
                        lo.to_string()
                    };
                    format!("{recv} != ({lo_src})")
                } else {
                    "true".to_string()
                }
            }
            "checked_pow" => {
                if !(0..=4).contains(&c) {
                    return None;
                }
                match c {
                    0 | 1 => "true".to_string(),
                    2 => {
                        let thr_hi = hi / 2;
                        let thr_lo = lo / 2;
                        format!("{recv} <= ({thr_hi}) && {recv} >= ({thr_lo})")
                    }
                    3 | 4 => {
                        let thr = match c {
                            3 => {
                                if hi >= i64::MAX / 2 {
                                    1290i64
                                } else {
                                    ((hi as f64).cbrt().floor() as i64).max(1)
                                }
                            }
                            _ => {
                                if hi >= i64::MAX / 2 {
                                    215i64
                                } else {
                                    ((hi as f64).sqrt().sqrt().floor() as i64).max(1)
                                }
                            }
                        };
                        format!("{recv} <= ({thr}) && {recv} >= 0")
                    }
                    _ => return None,
                }
            }
            _ => return None,
        }
    } else {
        return None;
    };

    let tree = if want_some {
        some_tree
    } else {
        format!("!({some_tree})")
    };
    syn::parse_str(&tree).ok()
}

/// `x.overflowing_add(y).0` → `x.wrapping_add(y)` (same for sub/mul/div/rem/neg/shl/shr/pow).
fn expand_overflowing_binop_tuple0(expr: &syn::Expr) -> Option<syn::Expr> {
    let syn::Expr::Field(f) = expr else {
        return None;
    };
    let syn::Member::Unnamed(idx) = &f.member else {
        return None;
    };
    if idx.index != 0 {
        return None;
    }
    let syn::Expr::MethodCall(m) = f.base.as_ref() else {
        return None;
    };
    let wrap = match m.method.to_string().as_str() {
        "overflowing_add" if m.args.len() == 1 => "wrapping_add",
        "overflowing_sub" if m.args.len() == 1 => "wrapping_sub",
        "overflowing_mul" if m.args.len() == 1 => "wrapping_mul",
        // Div/rem by 0 panics (not overflow); refuse literal 0 here.
        "overflowing_div" if m.args.len() == 1 && !is_lit_int_zero(&m.args[0]) => "wrapping_div",
        "overflowing_rem" if m.args.len() == 1 && !is_lit_int_zero(&m.args[0]) => "wrapping_rem",
        "overflowing_neg" if m.args.is_empty() => "wrapping_neg",
        "overflowing_shl" if m.args.len() == 1 => "wrapping_shl",
        "overflowing_shr" if m.args.len() == 1 => "wrapping_shr",
        // wrapping_pow supports const exp ≤4; larger exp stays BNM downstream.
        "overflowing_pow" if m.args.len() == 1 => "wrapping_pow",
        _ => return None,
    };
    let recv = expr_source(&m.receiver);
    let tree = if m.args.is_empty() {
        format!("{recv}.{wrap}()")
    } else {
        let arg = expr_source(&m.args[0]);
        format!("{recv}.{wrap}({arg})")
    };
    syn::parse_str(&tree).ok()
}

/// `x.overflowing_add(c).1` → overflow flag bool (dual of `checked_add(c).is_none()`).
/// Same method set / const limits as `expand_checked_is_some_none`.
/// Div/rem by 0 panics in Rust; refuse so we do not treat panic as overflow=true.
fn expand_overflowing_binop_tuple1(expr: &syn::Expr) -> Option<syn::Expr> {
    let syn::Expr::Field(f) = expr else {
        return None;
    };
    let syn::Member::Unnamed(idx) = &f.member else {
        return None;
    };
    if idx.index != 1 {
        return None;
    }
    let syn::Expr::MethodCall(m) = f.base.as_ref() else {
        return None;
    };
    let method = m.method.to_string();
    if matches!(method.as_str(), "overflowing_div" | "overflowing_rem")
        && m.args.len() == 1
        && is_lit_int_zero(&m.args[0])
    {
        return None;
    }
    let checked = match method.as_str() {
        "overflowing_add" if m.args.len() == 1 => "checked_add",
        "overflowing_sub" if m.args.len() == 1 => "checked_sub",
        "overflowing_mul" if m.args.len() == 1 => "checked_mul",
        "overflowing_div" if m.args.len() == 1 => "checked_div",
        "overflowing_rem" if m.args.len() == 1 => "checked_rem",
        "overflowing_neg" if m.args.is_empty() => "checked_neg",
        "overflowing_shl" if m.args.len() == 1 => "checked_shl",
        "overflowing_shr" if m.args.len() == 1 => "checked_shr",
        "overflowing_pow" if m.args.len() == 1 => "checked_pow",
        _ => return None,
    };
    let recv = expr_source(&m.receiver);
    let as_checked = if m.args.is_empty() {
        format!("{recv}.{checked}().is_none()")
    } else {
        let arg = expr_source(&m.args[0]);
        format!("{recv}.{checked}({arg}).is_none()")
    };
    let rewritten: syn::Expr = syn::parse_str(&as_checked).ok()?;
    expand_checked_is_some_none(&rewritten)
}

/// `x.checked_add(c).unwrap_or(alt)` → overflow-guarded if-tree (needs SAT_BOUNDS).
/// Const `c` only. Same for `checked_sub`.
/// `unwrap_or_default()` rewrites to `unwrap_or(0)` (integer Option default).
fn expand_checked_binop_unwrap_or(expr: &syn::Expr) -> Option<syn::Expr> {
    let syn::Expr::MethodCall(outer) = expr else {
        return None;
    };
    // Integer Option::default is 0; rewrite then fall through to unwrap_or path.
    if outer.method == "unwrap_or_default" && outer.args.is_empty() {
        let tree = format!("{}.unwrap_or(0)", expr_source(&outer.receiver));
        let rewritten: syn::Expr = syn::parse_str(&tree).ok()?;
        return expand_checked_binop_unwrap_or(&rewritten);
    }
    if outer.method != "unwrap_or" || outer.args.len() != 1 {
        return None;
    }
    let syn::Expr::MethodCall(inner) = outer.receiver.as_ref() else {
        return None;
    };
    let method = inner.method.to_string();
    // checked_neg() / checked_abs() are zero-arg
    if matches!(method.as_str(), "checked_neg" | "checked_abs") && inner.args.is_empty() {
        let (lo, _) = SAT_BOUNDS.get()?;
        let recv = expr_source(&inner.receiver);
        let alt = expr_source(&outer.args[0]);
        if lo < 0 {
            let lo_src = if lo == i64::MIN {
                format!("-{} - 1", i64::MAX)
            } else {
                lo.to_string()
            };
            let ok_body = if method == "checked_neg" {
                format!("-({recv})")
            } else {
                format!("({recv}).abs()")
            };
            let tree = format!("if {recv} == ({lo_src}) {{ {alt} }} else {{ {ok_body} }}");
            return syn::parse_str(&tree).ok();
        }
        // unsigned / nonneg: abs is id; neg still works
        let tree = if method == "checked_neg" {
            format!("-({recv})")
        } else {
            format!("({recv})")
        };
        return syn::parse_str(&tree).ok();
    }
    // checked_next_power_of_two (unsigned only): None when pot overflows width.
    // Encoded next_power_of_two returns 0 on overflow (a > 2^(bits-1)); a==0 → 1.
    if method == "checked_next_power_of_two" && inner.args.is_empty() {
        let (lo, hi) = SAT_BOUNDS.get()?;
        if lo != 0 {
            return None;
        }
        let (bits, _, _) = wrap_width(lo, hi)?;
        if bits == 0 || bits > 64 {
            return None;
        }
        let recv = expr_source(&inner.receiver);
        let alt = expr_source(&outer.args[0]);
        let tree = format!(
            "if ({recv}).next_power_of_two() == 0 {{ {alt} }} else {{ ({recv}).next_power_of_two() }}"
        );
        return syn::parse_str(&tree).ok();
    }
    // checked_shl/shr(const n): None only when n >= bit width (not value overflow).
    if matches!(method.as_str(), "checked_shl" | "checked_shr") && inner.args.len() == 1 {
        let n = lit_int_i64(&inner.args[0])?;
        if n < 0 {
            return None;
        }
        let (lo, hi) = SAT_BOUNDS.get()?;
        let (bits, _, _) = wrap_width(lo, hi)?;
        let recv = expr_source(&inner.receiver);
        let alt = expr_source(&outer.args[0]);
        if (n as u64) >= u64::from(bits) {
            let tree = format!("({alt})");
            return syn::parse_str(&tree).ok();
        }
        let wrap = if method == "checked_shl" {
            "wrapping_shl"
        } else {
            "wrapping_shr"
        };
        let tree = format!("({recv}).{wrap}({n})");
        return syn::parse_str(&tree).ok();
    }
    // checked_ilog2 / checked_ilog10: None only for 0 (and nonpos for signed).
    if matches!(method.as_str(), "checked_ilog2" | "checked_ilog10") && inner.args.is_empty() {
        let recv = expr_source(&inner.receiver);
        let alt = expr_source(&outer.args[0]);
        let peep = if method == "checked_ilog2" {
            "ilog2"
        } else {
            "ilog10"
        };
        let tree = format!("if {recv} <= 0 {{ {alt} }} else {{ ({recv}).{peep}() }}");
        return syn::parse_str(&tree).ok();
    }
    // checked_pow(const) for small exponents
    if method == "checked_pow" && inner.args.len() == 1 {
        let exp = lit_int_i64(&inner.args[0])?;
        if !(0..=4).contains(&exp) {
            return None;
        }
        let (lo, hi) = SAT_BOUNDS.get()?;
        let recv = expr_source(&inner.receiver);
        let alt = expr_source(&outer.args[0]);
        let tree = match exp {
            0 => "1".to_string(),
            1 => format!("({recv})"),
            2 => {
                let thr_hi = hi / 2;
                let thr_lo = lo / 2;
                format!(
                    "if {recv} > ({thr_hi}) || {recv} < ({thr_lo}) {{ {alt} }} else {{ {recv} * {recv} }}"
                )
            }
            3 | 4 => {
                // Conservative: only non-negative recv with thr for hi^(1/exp)
                let thr = match exp {
                    3 => {
                        // cube root of hi approx; use small thr for safety
                        if hi >= i64::MAX / 2 {
                            1290i64
                        } else {
                            ((hi as f64).cbrt().floor() as i64).max(1)
                        }
                    }
                    _ => {
                        if hi >= i64::MAX / 2 {
                            215i64
                        } else {
                            ((hi as f64).sqrt().sqrt().floor() as i64).max(1)
                        }
                    }
                };
                format!(
                    "if {recv} > ({thr}) || {recv} < 0 {{ {alt} }} else {{ {recv}.wrapping_pow({exp}) }}"
                )
            }
            _ => return None,
        };
        return syn::parse_str(&tree).ok();
    }
    let op = match method.as_str() {
        "checked_add" => "add",
        "checked_sub" => "sub",
        "checked_mul" => "mul",
        "checked_div" => "div",
        "checked_rem" => "rem",
        _ => return None,
    };
    if inner.args.len() != 1 {
        return None;
    }
    let c = lit_int_i64(&inner.args[0])?;
    let (lo, hi) = SAT_BOUNDS.get()?;
    let recv = expr_source(&inner.receiver);
    let alt = expr_source(&outer.args[0]);
    // Overflow thresholds for x ⊕ c within [lo, hi].
    let tree = match op {
        "add" => {
            if c == 0 {
                format!("({recv})")
            } else if c > 0 {
                // overflow when x > hi - c
                let thr = hi.checked_sub(c)?;
                format!("if {recv} > ({thr}) {{ {alt} }} else {{ {recv} + ({c}) }}")
            } else {
                // c < 0: overflow when x < lo - c
                let thr = lo.checked_sub(c)?;
                format!("if {recv} < ({thr}) {{ {alt} }} else {{ {recv} + ({c}) }}")
            }
        }
        "sub" => {
            // checked_sub(c): x - c
            if c == 0 {
                format!("({recv})")
            } else if c > 0 {
                // underflow when x < lo + c
                let thr = lo.checked_add(c)?;
                format!("if {recv} < ({thr}) {{ {alt} }} else {{ {recv} - ({c}) }}")
            } else {
                // c < 0: x - c = x + |c|; overflow when x > hi + c (c negative)
                let thr = hi.checked_add(c)?;
                format!("if {recv} > ({thr}) {{ {alt} }} else {{ {recv} - ({c}) }}")
            }
        }
        "mul" => {
            // Conservative: only const |c| <= 1 (identity/zero/neg) or c == 2 with mid bound.
            if c == 0 {
                "0".to_string()
            } else if c == 1 {
                format!("({recv})")
            } else if c == -1 {
                // overflow only at MIN for signed
                if lo < 0 {
                    let lo_src = if lo == i64::MIN {
                        format!("-{} - 1", i64::MAX)
                    } else {
                        lo.to_string()
                    };
                    format!("if {recv} == ({lo_src}) {{ {alt} }} else {{ -({recv}) }}")
                } else {
                    format!("-({recv})")
                }
            } else if c == 2 {
                // overflow when x > hi/2 or x < ceil(lo/2) (avoid lo-1 when lo==MIN)
                let thr_hi = hi / 2;
                let thr_lo = lo / 2; // floor; exact for even lo (MIN is even)
                format!(
                    "if {recv} > ({thr_hi}) || {recv} < ({thr_lo}) {{ {alt} }} else {{ {recv} * 2 }}"
                )
            } else {
                return None;
            }
        }
        "div" | "rem" => {
            // Div/rem by zero always fails → alt. MIN / -1 (or %) overflows signed.
            if c == 0 {
                format!("({alt})")
            } else if c == -1 && lo < 0 {
                let lo_src = if lo == i64::MIN {
                    format!("-{} - 1", i64::MAX)
                } else {
                    lo.to_string()
                };
                if op == "div" {
                    format!("if {recv} == ({lo_src}) {{ {alt} }} else {{ -({recv}) }}")
                } else {
                    // rem of ±1 is always 0 when defined
                    format!("if {recv} == ({lo_src}) {{ {alt} }} else {{ 0 }}")
                }
            } else if op == "div" {
                format!("{recv} / ({c})")
            } else {
                format!("{recv} % ({c})")
            }
        }
        _ => return None,
    };
    syn::parse_str(&tree).ok()
}

/// `x.wrapping_abs()` → `if x >= 0 { x } else { x.wrapping_neg() }` (MIN stays MIN).
fn expand_wrapping_abs_method(expr: &syn::Expr) -> Option<syn::Expr> {
    let syn::Expr::MethodCall(m) = expr else {
        return None;
    };
    if m.method != "wrapping_abs" || !m.args.is_empty() {
        return None;
    }
    let recv = expr_source(&m.receiver);
    let tree = format!("if {recv} >= 0 {{ {recv} }} else {{ ({recv}).wrapping_neg() }}");
    syn::parse_str(&tree).ok()
}

/// `x.wrapping_neg()` → if x == MIN { MIN } else { -x } (needs SAT_BOUNDS).
/// Signed only (multi-block if). Unsigned uses encode MethodCall mod path.
fn expand_wrapping_neg_method(expr: &syn::Expr) -> Option<syn::Expr> {
    let syn::Expr::MethodCall(m) = expr else {
        return None;
    };
    if m.method != "wrapping_neg" || !m.args.is_empty() {
        return None;
    }
    let (lo, _) = SAT_BOUNDS.get()?;
    // Unsigned: handled in encode_syn_expr via mod 2^w.
    if lo == 0 {
        return None;
    }
    let recv = expr_source(&m.receiver);
    // Avoid raw MIN literals that do not parse as i64 tokens (use -MAX-1).
    let lo_src = if lo == i64::MIN {
        format!("-{} - 1", i64::MAX)
    } else {
        lo.to_string()
    };
    let tree = format!("if {recv} == ({lo_src}) {{ ({lo_src}) }} else {{ -({recv}) }}");
    syn::parse_str(&tree).ok()
}

/// True when `expr` is integer literal 0 (after paren/group peels).
fn is_lit_int_zero(expr: &syn::Expr) -> bool {
    match expr {
        syn::Expr::Paren(p) => is_lit_int_zero(&p.expr),
        syn::Expr::Group(g) => is_lit_int_zero(&g.expr),
        syn::Expr::Lit(syn::ExprLit {
            lit: syn::Lit::Int(n),
            ..
        }) => n.base10_digits() == "0",
        _ => false,
    }
}

/// Integer value of a literal (optionally negated), after paren/group peels.
fn lit_int_i64(expr: &syn::Expr) -> Option<i64> {
    match expr {
        syn::Expr::Paren(p) => lit_int_i64(&p.expr),
        syn::Expr::Group(g) => lit_int_i64(&g.expr),
        syn::Expr::Unary(u) if matches!(u.op, syn::UnOp::Neg(_)) => {
            let v = lit_int_i64(&u.expr)?;
            v.checked_neg()
        }
        syn::Expr::Lit(syn::ExprLit {
            lit: syn::Lit::Int(n),
            ..
        }) => n.base10_parse().ok(),
        _ => None,
    }
}

fn is_lit_int_abs_one(expr: &syn::Expr) -> bool {
    match expr {
        syn::Expr::Paren(p) => is_lit_int_abs_one(&p.expr),
        syn::Expr::Group(g) => is_lit_int_abs_one(&g.expr),
        syn::Expr::Unary(u) if matches!(u.op, syn::UnOp::Neg(_)) => {
            matches!(
                u.expr.as_ref(),
                syn::Expr::Lit(syn::ExprLit {
                    lit: syn::Lit::Int(n),
                    ..
                }) if n.base10_digits() == "1"
            )
        }
        syn::Expr::Lit(syn::ExprLit {
            lit: syn::Lit::Int(n),
            ..
        }) => n.base10_digits() == "1",
        _ => false,
    }
}

/// Same single-segment path after paren/group peels (`x` vs `x`, not `x` vs `y`).
fn expr_same_simple_path(a: &syn::Expr, b: &syn::Expr) -> bool {
    fn path_name(expr: &syn::Expr) -> Option<String> {
        match expr {
            syn::Expr::Paren(p) => path_name(&p.expr),
            syn::Expr::Group(g) => path_name(&g.expr),
            syn::Expr::Path(p) if p.path.segments.len() == 1 => {
                Some(p.path.segments[0].ident.to_string())
            }
            _ => None,
        }
    }
    match (path_name(a), path_name(b)) {
        (Some(x), Some(y)) => x == y,
        _ => false,
    }
}

/// Clamp `val` slot into SAT_BOUNDS using max/min; returns result slot.
/// u64/usize: hi via synthetic `2^64 - 1` (cannot fit in i64 const).
fn emit_sat_clamp(val: usize, lines: &mut Vec<String>, next: &mut usize) -> Option<usize> {
    let (lo_v, hi_v) = SAT_BOUNDS.get()?;
    let lo = *next;
    *next += 1;
    lines.push(format!("${lo} = const {lo_v} : Int"));
    let hi = if is_u64_width_bounds(lo_v, hi_v) {
        emit_u64_max(lines, next)
    } else {
        let h = *next;
        *next += 1;
        lines.push(format!("${h} = const {hi_v} : Int"));
        h
    };
    let mx = *next;
    *next += 1;
    lines.push(format!("${mx} = call max (${val}, ${lo}) : Int"));
    let slot = *next;
    *next += 1;
    lines.push(format!("${slot} = call min (${mx}, ${hi}) : Int"));
    Some(slot)
}

pub(crate) fn is_identity_peel_method(name: &str) -> bool {
    matches!(
        name,
        "clone"
            | "to_owned"
            | "into"
            | "copied"
            | "cloned"
            | "as_ref"
            | "as_mut"
            | "borrow"
            | "borrow_mut"
            | "deref"
            | "deref_mut"
    )
}

/// Positive divisor for rem_euclid / div_euclid / next_multiple_of.
/// Accepts a positive const lit, or a path param with lower bound ≥ 1
/// (so zero and negative divisors stay BNM; they panic or are undefined
/// for rem_euclid in the unsigned encoding we use).
fn encode_positive_divisor(
    expr: &syn::Expr,
    param_names: &[&str],
    lines: &mut Vec<String>,
    next: &mut usize,
) -> Option<usize> {
    if let Some(v) = lit_int_i64(expr) {
        if v <= 0 {
            return None;
        }
        let slot = *next;
        *next += 1;
        lines.push(format!("${slot} = const {v} : Int"));
        return Some(slot);
    }
    let (lo, _hi) = path_param_bounds(expr)?;
    if lo < 1 {
        return None;
    }
    encode_syn_expr(expr, param_names, lines, next)
}

/// Encode `expr` into IR lines; returns the slot holding the value.
fn encode_syn_expr(
    expr: &syn::Expr,
    param_names: &[&str],
    lines: &mut Vec<String>,
    next: &mut usize,
) -> Option<usize> {
    match expr {
        syn::Expr::Paren(p) => encode_syn_expr(&p.expr, param_names, lines, next),
        syn::Expr::Group(g) => encode_syn_expr(&g.expr, param_names, lines, next),
        syn::Expr::Reference(r) => encode_syn_expr(&r.expr, param_names, lines, next),
        syn::Expr::Unary(u) if matches!(u.op, syn::UnOp::Deref(_)) => {
            encode_syn_expr(&u.expr, param_names, lines, next)
        }
        syn::Expr::Path(path) if path.path.segments.len() == 1 => {
            let name = path.path.segments[0].ident.to_string();
            param_names.iter().position(|n| *n == name)
        }
        // i64::MIN / i64::MAX / u8::MAX (fits i64) as Int consts;
        // u64/usize::MAX = synthetic 2^64 - 1 (does not fit i64).
        syn::Expr::Path(path) if path.path.segments.len() == 2 => {
            let ty = path.path.segments[0].ident.to_string();
            let name = path.path.segments[1].ident.to_string();
            if matches!(ty.as_str(), "u64" | "usize") && name == "MAX" {
                return Some(emit_u64_max(lines, next));
            }
            let val: Option<i64> = match (ty.as_str(), name.as_str()) {
                ("i8", "MIN") => Some(i8::MIN as i64),
                ("i8", "MAX") => Some(i8::MAX as i64),
                ("i16", "MIN") => Some(i16::MIN as i64),
                ("i16", "MAX") => Some(i16::MAX as i64),
                ("i32", "MIN") => Some(i32::MIN as i64),
                ("i32", "MAX") => Some(i32::MAX as i64),
                ("i64", "MIN") | ("isize", "MIN") => Some(i64::MIN),
                ("i64", "MAX") | ("isize", "MAX") => Some(i64::MAX),
                ("u8", "MAX") => Some(u8::MAX as i64),
                ("u16", "MAX") => Some(u16::MAX as i64),
                ("u32", "MAX") => Some(u32::MAX as i64),
                ("u8" | "u16" | "u32" | "u64" | "usize", "MIN") => Some(0),
                _ => None,
            };
            let v = val?;
            let slot = *next;
            *next += 1;
            lines.push(format!("${slot} = const {v} : Int"));
            Some(slot)
        }
        syn::Expr::Lit(syn::ExprLit {
            lit: syn::Lit::Int(n),
            ..
        }) => {
            let val = n.base10_digits();
            let _ = val.parse::<i64>().ok()?;
            let slot = *next;
            *next += 1;
            lines.push(format!("${slot} = const {val} : Int"));
            Some(slot)
        }
        syn::Expr::Lit(syn::ExprLit {
            lit: syn::Lit::Bool(b),
            ..
        }) => {
            let val = if b.value { 1 } else { 0 };
            let slot = *next;
            *next += 1;
            lines.push(format!("${slot} = const {val} : Bool"));
            Some(slot)
        }
        syn::Expr::Unary(u) if matches!(u.op, syn::UnOp::Neg(_)) => {
            let zero = *next;
            *next += 1;
            lines.push(format!("${zero} = const 0 : Int"));
            let inner = encode_syn_expr(&u.expr, param_names, lines, next)?;
            let slot = *next;
            *next += 1;
            lines.push(format!("${slot} = arith sub ${zero} ${inner} : Int"));
            Some(slot)
        }
        syn::Expr::Unary(u) if matches!(u.op, syn::UnOp::Not(_)) => {
            // Typed integer lit: bitwise NOT (ones' complement within width).
            if let Some((v, bits)) = lit_int_i64_bits(&u.expr)
                && v >= 0
            {
                let mask = if bits == 64 {
                    u64::MAX
                } else {
                    (1u64 << bits) - 1
                };
                let notv = (!(v as u64)) & mask;
                let slot = *next;
                *next += 1;
                lines.push(format!("${slot} = const {notv} : Int"));
                return Some(slot);
            }
            // Variable integer bitwise NOT (bits ≤64): !x ≡ (2^w-1) - u(x).
            // Integer-typed receivers must not fall through to bool logical not.
            if let Some((lo, hi)) = path_param_bounds(&u.expr).or_else(|| SAT_BOUNDS.get()) {
                let (bits, modulus_i64, signed) = wrap_width(lo, hi)?;
                if bits == 0 || bits > 64 {
                    return None;
                }
                let a = encode_syn_expr(&u.expr, param_names, lines, next)?;
                let mslot = emit_signed_modulus_slot(modulus_i64, lines, next);
                let one = *next;
                *next += 1;
                lines.push(format!("${one} = const 1 : Int"));
                let ones = *next;
                *next += 1;
                lines.push(format!("${ones} = arith sub ${mslot} ${one} : Int"));
                let u_in = emit_to_unsigned_bits(a, mslot, lines, next);
                let not_u = *next;
                *next += 1;
                lines.push(format!("${not_u} = arith sub ${ones} ${u_in} : Int"));
                if signed {
                    return Some(emit_from_unsigned_bits(not_u, mslot, hi, lines, next));
                }
                return Some(not_u);
            }
            // Bool / general: logical not as eq 0.
            let zero = *next;
            *next += 1;
            lines.push(format!("${zero} = const 0 : Bool"));
            let inner = encode_syn_expr(&u.expr, param_names, lines, next)?;
            let slot = *next;
            *next += 1;
            lines.push(format!("${slot} = cmp eq ${inner} ${zero} : Bool"));
            Some(slot)
        }
        syn::Expr::Binary(b) => {
            // Const-fold bitops when both sides are integer lits (partial #1034 bitops).
            if let (Some(l), Some(r)) = (lit_int_i64(&b.left), lit_int_i64(&b.right)) {
                let folded = match &b.op {
                    syn::BinOp::BitAnd(_) if l >= 0 && r >= 0 => Some((l as u64 & r as u64) as i64),
                    syn::BinOp::BitOr(_) if l >= 0 && r >= 0 => Some((l as u64 | r as u64) as i64),
                    syn::BinOp::BitXor(_) if l >= 0 && r >= 0 => Some((l as u64 ^ r as u64) as i64),
                    syn::BinOp::Shl(_) if l >= 0 && (0..63).contains(&r) => {
                        Some(((l as u64) << (r as u32)) as i64)
                    }
                    syn::BinOp::Shr(_) if l >= 0 && (0..63).contains(&r) => {
                        Some(((l as u64) >> (r as u32)) as i64)
                    }
                    _ => None,
                };
                if let Some(val) = folded {
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = const {val} : Int"));
                    return Some(slot);
                }
            }
            // Variable BitAnd/Or/Xor: const mask (signed/unsigned) or both-var ≤64.
            if let Some(kind) = match &b.op {
                syn::BinOp::BitAnd(_) => Some(BitOpKind::And),
                syn::BinOp::BitOr(_) => Some(BitOpKind::Or),
                syn::BinOp::BitXor(_) => Some(BitOpKind::Xor),
                _ => None,
            } {
                let sides: Option<(&syn::Expr, i64)> =
                    match (lit_int_i64(&b.left), lit_int_i64(&b.right)) {
                        (Some(m), None) => Some((&b.right, m)),
                        (None, Some(m)) => Some((&b.left, m)),
                        _ => None,
                    };
                if let Some((var_e, mask_i)) = sides {
                    let bounds = path_param_bounds(var_e).or_else(|| SAT_BOUNDS.get());
                    if let Some((lo, hi)) = bounds
                        && let Some((bits, modulus_i64, signed)) = wrap_width(lo, hi)
                        && bits > 0
                        && bits <= 64
                        && (signed || mask_i >= 0)
                    {
                        let mask = mask_bits_u64(mask_i, bits);
                        let a = encode_syn_expr(var_e, param_names, lines, next)?;
                        if !signed {
                            return encode_unsigned_bitop_var_const(
                                a, mask, kind, bits, lines, next,
                            );
                        }
                        // Signed: map to unsigned bit pattern, bitop, reinterpret
                        // (i64 via synthetic 2^64).
                        let mslot = emit_signed_modulus_slot(modulus_i64, lines, next);
                        let u_in = emit_to_unsigned_bits(a, mslot, lines, next);
                        let u_out =
                            encode_unsigned_bitop_var_const(u_in, mask, kind, bits, lines, next)?;
                        return Some(emit_from_unsigned_bits(u_out, mslot, hi, lines, next));
                    }
                } else if lit_int_i64(&b.left).is_none() && lit_int_i64(&b.right).is_none() {
                    // Both variable: unsigned or signed (bit-pattern map) for bits ≤64
                    // (i64 via synthetic 2^64 modulus).
                    let info = path_param_bounds(&b.left)
                        .or_else(|| path_param_bounds(&b.right))
                        .or_else(|| SAT_BOUNDS.get())
                        .and_then(|(lo, hi)| {
                            let (bits, modulus_i64, signed) = wrap_width(lo, hi)?;
                            if bits == 0 || bits > 64 {
                                return None;
                            }
                            Some((bits, modulus_i64, signed, hi))
                        });
                    if let Some((bits, modulus_i64, signed, hi)) = info {
                        let lhs = encode_syn_expr(&b.left, param_names, lines, next)?;
                        let rhs = encode_syn_expr(&b.right, param_names, lines, next)?;
                        if !signed {
                            return encode_unsigned_bitop_var_var(
                                lhs, rhs, kind, bits, lines, next,
                            );
                        }
                        // Signed: map both to unsigned bit patterns, bitop, reinterpret.
                        // i64 uses synthetic 2^64 (same as reverse_bits / const-mask path).
                        let mslot = emit_signed_modulus_slot(modulus_i64, lines, next);
                        let u_l = emit_to_unsigned_bits(lhs, mslot, lines, next);
                        let u_r = emit_to_unsigned_bits(rhs, mslot, lines, next);
                        let u_out =
                            encode_unsigned_bitop_var_var(u_l, u_r, kind, bits, lines, next)?;
                        return Some(emit_from_unsigned_bits(u_out, mslot, hi, lines, next));
                    }
                }
            }
            if let Some(cmp) = match &b.op {
                syn::BinOp::Lt(_) => Some("lt"),
                syn::BinOp::Gt(_) => Some("gt"),
                syn::BinOp::Le(_) => Some("le"),
                syn::BinOp::Ge(_) => Some("ge"),
                syn::BinOp::Eq(_) => Some("eq"),
                syn::BinOp::Ne(_) => Some("ne"),
                _ => None,
            } {
                let lhs = encode_syn_expr(&b.left, param_names, lines, next)?;
                let rhs = encode_syn_expr(&b.right, param_names, lines, next)?;
                let slot = *next;
                *next += 1;
                lines.push(format!("${slot} = cmp {cmp} ${lhs} ${rhs} : Bool"));
                return Some(slot);
            }
            // Bool 0/1: a && b → mul; a || b → (a+b) != 0 (matches ir_generate)
            if matches!(b.op, syn::BinOp::And(_)) {
                let lhs = encode_syn_expr(&b.left, param_names, lines, next)?;
                let rhs = encode_syn_expr(&b.right, param_names, lines, next)?;
                let slot = *next;
                *next += 1;
                lines.push(format!("${slot} = arith mul ${lhs} ${rhs} : Bool"));
                return Some(slot);
            }
            if matches!(b.op, syn::BinOp::Or(_)) {
                let lhs = encode_syn_expr(&b.left, param_names, lines, next)?;
                let rhs = encode_syn_expr(&b.right, param_names, lines, next)?;
                let sum = *next;
                *next += 1;
                lines.push(format!("${sum} = arith add ${lhs} ${rhs} : Bool"));
                let zero = *next;
                *next += 1;
                lines.push(format!("${zero} = const 0 : Bool"));
                let slot = *next;
                *next += 1;
                lines.push(format!("${slot} = cmp ne ${sum} ${zero} : Bool"));
                return Some(slot);
            }
            let ir_op = match &b.op {
                syn::BinOp::Add(_) => "add",
                syn::BinOp::Sub(_) => "sub",
                syn::BinOp::Mul(_) => "mul",
                syn::BinOp::Div(_) => "div",
                syn::BinOp::Rem(_) => "mod",
                _ => return None,
            };
            // Refuse zero divisors (Rust panic / UB); do not give SMT a free
            // div-by-zero term that can pass ensures spuriously.
            if matches!(ir_op, "div" | "mod") {
                if is_lit_int_zero(&b.right) {
                    return None;
                }
                // Non-literal divisor: only encode when bounds prove lo >= 1
                // (e.g. NonZeroU*). Zero-including ranges stay BNM.
                if lit_int_i64(&b.right).is_none() {
                    let (lo, _) = path_param_bounds(&b.right)?;
                    if lo < 1 {
                        return None;
                    }
                }
            }
            let lhs = encode_syn_expr(&b.left, param_names, lines, next)?;
            let rhs = encode_syn_expr(&b.right, param_names, lines, next)?;
            let slot = *next;
            *next += 1;
            lines.push(format!("${slot} = arith {ir_op} ${lhs} ${rhs} : Int"));
            Some(slot)
        }
        syn::Expr::MethodCall(m) => {
            let method = m.method.to_string();
            match (method.as_str(), m.args.len()) {
                ("abs" | "unsigned_abs", 0) => {
                    // unsigned_abs is |x| as unsigned magnitude; SMT Int uses abs.
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = call abs (${a}) : Int"));
                    Some(slot)
                }
                // Integer signum ≡ clamp to [-1, 1] via min/max (nestable; #1032).
                // max(min(x, 1), -1) matches x.signum() for all Int values.
                ("signum", 0) => {
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let lo = *next;
                    *next += 1;
                    lines.push(format!("${lo} = const -1 : Int"));
                    let hi = *next;
                    *next += 1;
                    lines.push(format!("${hi} = const 1 : Int"));
                    let mx = *next;
                    *next += 1;
                    lines.push(format!("${mx} = call max (${a}, ${lo}) : Int"));
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = call min (${mx}, ${hi}) : Int"));
                    Some(slot)
                }
                ("is_positive", 0) => {
                    // abs_diff(x, x).is_positive() is always false
                    if let syn::Expr::MethodCall(inner) = m.receiver.as_ref()
                        && inner.method == "abs_diff"
                        && inner.args.len() == 1
                        && expr_same_simple_path(&inner.receiver, &inner.args[0])
                    {
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const 0 : Bool"));
                        return Some(slot);
                    }
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let z = *next;
                    *next += 1;
                    lines.push(format!("${z} = const 0 : Int"));
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = cmp gt ${a} ${z} : Bool"));
                    Some(slot)
                }
                ("is_negative", 0) => {
                    // abs/saturating_abs(...).is_negative() is always false
                    if let syn::Expr::MethodCall(inner) = m.receiver.as_ref()
                        && matches!(inner.method.to_string().as_str(), "abs" | "saturating_abs")
                        && inner.args.is_empty()
                    {
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const 0 : Bool"));
                        return Some(slot);
                    }
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let z = *next;
                    *next += 1;
                    lines.push(format!("${z} = const 0 : Int"));
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = cmp lt ${a} ${z} : Bool"));
                    Some(slot)
                }
                ("is_zero", 0) => {
                    // abs_diff(x, x).is_zero() is always true
                    if let syn::Expr::MethodCall(inner) = m.receiver.as_ref()
                        && inner.method == "abs_diff"
                        && inner.args.len() == 1
                        && expr_same_simple_path(&inner.receiver, &inner.args[0])
                    {
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const 1 : Bool"));
                        return Some(slot);
                    }
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let z = *next;
                    *next += 1;
                    lines.push(format!("${z} = const 0 : Int"));
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = cmp eq ${a} ${z} : Bool"));
                    Some(slot)
                }
                // Const lit peep, or pot enum over path/nested expr bounds (#1034).
                // Nested: `(x+1).is_power_of_two()` uses expr_int_bounds(x).
                ("is_power_of_two", 0) => {
                    if let Some(v) = lit_int_i64(&m.receiver) {
                        let pot = v > 0 && (v as u64).is_power_of_two();
                        let slot = *next;
                        *next += 1;
                        lines.push(format!(
                            "${slot} = const {} : Bool",
                            if pot { 1 } else { 0 }
                        ));
                        return Some(slot);
                    }
                    let (lo, hi) = expr_int_bounds(&m.receiver)?;
                    let n_exp = pot_exponents(lo, hi)?;
                    // Cap IR size: u64 uses 64 OR-chain steps (2^63 via emit_pow2_factor).
                    if n_exp > 64 {
                        return None;
                    }
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let mut acc: Option<usize> = None;
                    for e in 0..n_exp {
                        // e==63 needs synthetic 2^63 (1i64<<63 is negative)
                        let c = emit_pow2_factor(e, lines, next)?;
                        let eq = *next;
                        *next += 1;
                        lines.push(format!("${eq} = cmp eq ${a} ${c} : Bool"));
                        acc = Some(match acc {
                            None => eq,
                            Some(prev) => {
                                let sum = *next;
                                *next += 1;
                                lines.push(format!("${sum} = arith add ${prev} ${eq} : Bool"));
                                let zero = *next;
                                *next += 1;
                                lines.push(format!("${zero} = const 0 : Bool"));
                                let or_s = *next;
                                *next += 1;
                                lines.push(format!("${or_s} = cmp ne ${sum} ${zero} : Bool"));
                                or_s
                            }
                        });
                    }
                    acc
                }
                // count_ones: const peep, or path-param bit-sum (≤64; signed via bit pattern).
                ("count_ones", 0) => {
                    if let Some(v) = lit_int_i64(&m.receiver) {
                        // Signed and unsigned lits: use two's complement width from suffix when present.
                        if let Some((vv, bits)) = lit_int_i64_bits(&m.receiver) {
                            let mask = if bits >= 64 {
                                u64::MAX
                            } else {
                                (1u64 << bits) - 1
                            };
                            let ones = ((vv as u64) & mask).count_ones();
                            let slot = *next;
                            *next += 1;
                            lines.push(format!("${slot} = const {ones} : Int"));
                            return Some(slot);
                        }
                        if v < 0 {
                            return None;
                        }
                        let ones = (v as u64).count_ones();
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const {ones} : Int"));
                        return Some(slot);
                    }
                    let (lo, hi) = path_param_bounds(&m.receiver)?;
                    let (bits, modulus_i64, signed) = wrap_width(lo, hi)?;
                    if bits == 0 || bits > 64 {
                        return None;
                    }
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    if !signed {
                        return encode_bit_sum_count_ones(a, bits, lines, next);
                    }
                    let mslot = emit_signed_modulus_slot(modulus_i64, lines, next);
                    let u_in = emit_to_unsigned_bits(a, mslot, lines, next);
                    encode_bit_sum_count_ones(u_in, bits, lines, next)
                }
                // trailing_ones: const peep, or path ≤64 via NOT + trailing_zeros.
                ("trailing_ones", 0) => {
                    if let Some((v, bits)) = lit_int_i64_bits(&m.receiver) {
                        let mask = if bits >= 64 {
                            u64::MAX
                        } else {
                            (1u64 << bits) - 1
                        };
                        let t = ((v as u64) & mask).trailing_ones();
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const {t} : Int"));
                        return Some(slot);
                    }
                    if let Some(v) = lit_int_i64(&m.receiver) {
                        if v < 0 {
                            return None;
                        }
                        let t = (v as u64).trailing_ones();
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const {t} : Int"));
                        return Some(slot);
                    }
                    let (lo, hi) = path_param_bounds(&m.receiver)?;
                    let (bits, modulus_i64, signed) = wrap_width(lo, hi)?;
                    if bits == 0 || bits > 64 {
                        return None;
                    }
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let u_in = if signed {
                        let mslot = emit_signed_modulus_slot(modulus_i64, lines, next);
                        emit_to_unsigned_bits(a, mslot, lines, next)
                    } else {
                        a
                    };
                    encode_unsigned_trailing_ones(u_in, bits, lines, next)
                }
                // leading_ones: typed lit or path ≤64 via NOT + leading_zeros.
                ("leading_ones", 0) => {
                    if let Some((v, bits)) = lit_int_i64_bits(&m.receiver) {
                        let mask = if bits >= 64 {
                            u64::MAX
                        } else {
                            (1u64 << bits) - 1
                        };
                        let u = (v as u64) & mask;
                        let lo = match bits {
                            8 => (u as u8).leading_ones(),
                            16 => (u as u16).leading_ones(),
                            32 => (u as u32).leading_ones(),
                            64 => u.leading_ones(),
                            _ => return None,
                        };
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const {lo} : Int"));
                        return Some(slot);
                    }
                    let (lo, hi) = path_param_bounds(&m.receiver)?;
                    let (bits, modulus_i64, signed) = wrap_width(lo, hi)?;
                    if bits == 0 || bits > 64 {
                        return None;
                    }
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let u_in = if signed {
                        let mslot = emit_signed_modulus_slot(modulus_i64, lines, next);
                        emit_to_unsigned_bits(a, mslot, lines, next)
                    } else {
                        a
                    };
                    encode_unsigned_leading_ones(u_in, bits, lines, next)
                }
                // Typed width: count_zeros = bits - count_ones.
                // Path params ≤64: unsigned direct; signed via bit-pattern map.
                ("count_zeros", 0) => {
                    if let Some((v, bits)) = lit_int_i64_bits(&m.receiver) {
                        let mask = if bits >= 64 {
                            u64::MAX
                        } else {
                            (1u64 << bits) - 1
                        };
                        let zeros = bits - ((v as u64) & mask).count_ones();
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const {zeros} : Int"));
                        return Some(slot);
                    }
                    let (lo, hi) = path_param_bounds(&m.receiver)?;
                    let (bits, modulus_i64, signed) = wrap_width(lo, hi)?;
                    if bits == 0 || bits > 64 {
                        return None;
                    }
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let u_in = if signed {
                        let mslot = emit_signed_modulus_slot(modulus_i64, lines, next);
                        emit_to_unsigned_bits(a, mslot, lines, next)
                    } else {
                        a
                    };
                    let ones = encode_bit_sum_count_ones(u_in, bits, lines, next)?;
                    let bits_c = *next;
                    *next += 1;
                    lines.push(format!("${bits_c} = const {bits} : Int"));
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = arith sub ${bits_c} ${ones} : Int"));
                    Some(slot)
                }
                // Typed width lit (incl. negative via mask); path params ≤64
                // unsigned direct or signed via bit-pattern map.
                ("trailing_zeros", 0) => {
                    if let Some((v, bits)) = lit_int_i64_bits(&m.receiver) {
                        let mask = if bits >= 64 {
                            u64::MAX
                        } else {
                            (1u64 << bits) - 1
                        };
                        let u = (v as u64) & mask;
                        let tz = if u == 0 { bits } else { u.trailing_zeros() };
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const {tz} : Int"));
                        return Some(slot);
                    }
                    if let Some(v) = lit_int_i64(&m.receiver) {
                        if v <= 0 {
                            return None;
                        }
                        let tz = (v as u64).trailing_zeros();
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const {tz} : Int"));
                        return Some(slot);
                    }
                    let (lo, hi) = path_param_bounds(&m.receiver)?;
                    let (bits, modulus_i64, signed) = wrap_width(lo, hi)?;
                    if bits == 0 || bits > 64 {
                        return None;
                    }
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let u_in = if signed {
                        let mslot = emit_signed_modulus_slot(modulus_i64, lines, next);
                        emit_to_unsigned_bits(a, mslot, lines, next)
                    } else {
                        a
                    };
                    encode_unsigned_trailing_zeros(u_in, bits, lines, next)
                }
                // Typed lit (incl. negative via mask); path params ≤32
                // unsigned direct or signed via bit-pattern map.
                ("leading_zeros", 0) => {
                    if let Some((v, bits)) = lit_int_i64_bits(&m.receiver) {
                        let mask = if bits >= 64 {
                            u64::MAX
                        } else {
                            (1u64 << bits) - 1
                        };
                        let u = (v as u64) & mask;
                        let lz = if u == 0 {
                            bits
                        } else {
                            u.leading_zeros() - (64 - bits)
                        };
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const {lz} : Int"));
                        return Some(slot);
                    }
                    let (lo, hi) = path_param_bounds(&m.receiver)?;
                    let (bits, modulus_i64, signed) = wrap_width(lo, hi)?;
                    if bits == 0 || bits > 64 {
                        return None;
                    }
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let u_in = if signed {
                        let mslot = emit_signed_modulus_slot(modulus_i64, lines, next);
                        emit_to_unsigned_bits(a, mslot, lines, next)
                    } else {
                        a
                    };
                    encode_unsigned_leading_zeros(u_in, bits, lines, next)
                }
                // Typed lit (incl. signed) or path-param bit reverse (≤64;
                // signed via bit-pattern map + reinterpret; i64 synthetic 2^64).
                ("reverse_bits", 0) => {
                    if let Some((v, bits, signed)) = lit_int_i64_bits_signed(&m.receiver) {
                        let rev = match (bits, signed) {
                            (8, true) => (v as u8).reverse_bits() as i8 as i64,
                            (8, false) => (v as u8).reverse_bits() as i64,
                            (16, true) => (v as u16).reverse_bits() as i16 as i64,
                            (16, false) => (v as u16).reverse_bits() as i64,
                            (32, true) => (v as u32).reverse_bits() as i32 as i64,
                            (32, false) => (v as u32).reverse_bits() as i64,
                            (64, _) => (v as u64).reverse_bits() as i64,
                            _ => return None,
                        };
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const {rev} : Int"));
                        return Some(slot);
                    }
                    let (lo, hi) = path_param_bounds(&m.receiver)?;
                    let (bits, modulus_i64, signed) = wrap_width(lo, hi)?;
                    if bits == 0 || bits > 64 {
                        return None;
                    }
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    if !signed {
                        return encode_unsigned_reverse_bits(a, bits, lines, next);
                    }
                    let mslot = emit_signed_modulus_slot(modulus_i64, lines, next);
                    let u_in = emit_to_unsigned_bits(a, mslot, lines, next);
                    let u_out = encode_unsigned_reverse_bits(u_in, bits, lines, next)?;
                    Some(emit_from_unsigned_bits(u_out, mslot, hi, lines, next))
                }
                ("swap_bytes", 0) => {
                    if let Some((v, bits, signed)) = lit_int_i64_bits_signed(&m.receiver) {
                        let sw = match (bits, signed) {
                            (8, _) => v, // no-op
                            (16, true) => (v as u16).swap_bytes() as i16 as i64,
                            (16, false) => (v as u16).swap_bytes() as i64,
                            (32, true) => (v as u32).swap_bytes() as i32 as i64,
                            (32, false) => (v as u32).swap_bytes() as i64,
                            (64, _) => (v as u64).swap_bytes() as i64,
                            _ => return None,
                        };
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const {sw} : Int"));
                        return Some(slot);
                    }
                    // Path params ≤32: reverse byte order; signed via bit-pattern map.
                    let (lo, hi) = path_param_bounds(&m.receiver)?;
                    let (bits, modulus_i64, signed) = wrap_width(lo, hi)?;
                    if bits == 0 || bits > 64 || !bits.is_multiple_of(8) {
                        return None;
                    }
                    let nbytes = bits / 8;
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    if nbytes == 1 {
                        return Some(a); // i8/u8 identity
                    }
                    let (u_in, mslot) = if signed {
                        let mslot = emit_signed_modulus_slot(modulus_i64, lines, next);
                        (emit_to_unsigned_bits(a, mslot, lines, next), Some(mslot))
                    } else {
                        (a, None)
                    };
                    let b256 = *next;
                    *next += 1;
                    lines.push(format!("${b256} = const 256 : Int"));
                    let zero = *next;
                    *next += 1;
                    lines.push(format!("${zero} = const 0 : Int"));
                    let mut acc = zero;
                    for i in 0..nbytes {
                        // byte_i = (u_in / 256^i) % 256
                        let mut div = u_in;
                        for _ in 0..i {
                            let d = *next;
                            *next += 1;
                            lines.push(format!("${d} = arith div ${div} ${b256} : Int"));
                            div = d;
                        }
                        let byte = *next;
                        *next += 1;
                        lines.push(format!("${byte} = arith mod ${div} ${b256} : Int"));
                        // place at 256^(nbytes-1-i)
                        let mut placed = byte;
                        for _ in 0..(nbytes - 1 - i) {
                            let m = *next;
                            *next += 1;
                            lines.push(format!("${m} = arith mul ${placed} ${b256} : Int"));
                            placed = m;
                        }
                        let sum = *next;
                        *next += 1;
                        lines.push(format!("${sum} = arith add ${acc} ${placed} : Int"));
                        acc = sum;
                    }
                    if let Some(mslot) = mslot {
                        Some(emit_from_unsigned_bits(acc, mslot, hi, lines, next))
                    } else {
                        Some(acc)
                    }
                }
                // Const peep (ilog2(0) panics → BNM). Variable: unsigned path ≤64;
                // signed path ≤64 with a>0 math log (a<=0 modeled as 0; Rust panics).
                ("ilog2", 0) => {
                    if let Some(v) = lit_int_i64(&m.receiver) {
                        if v <= 0 {
                            return None;
                        }
                        let log = (v as u64).ilog2();
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const {log} : Int"));
                        return Some(slot);
                    }
                    let (lo, hi) = path_param_bounds(&m.receiver)?;
                    let (bits, _, signed) = wrap_width(lo, hi)?;
                    if bits == 0 || bits > 64 {
                        return None;
                    }
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    if !signed {
                        return encode_unsigned_ilog2(a, bits, lines, next);
                    }
                    // Math log for a>0. Non-positive: model 0 (panic honesty, like 0u.ilog2).
                    let zero = *next;
                    *next += 1;
                    lines.push(format!("${zero} = const 0 : Int"));
                    let one = *next;
                    *next += 1;
                    lines.push(format!("${one} = const 1 : Int"));
                    let a_pos = *next;
                    *next += 1;
                    lines.push(format!("${a_pos} = call max (${a}, ${one}) : Int"));
                    let raw = encode_unsigned_ilog2(a_pos, bits, lines, next)?;
                    let gt = *next;
                    *next += 1;
                    lines.push(format!("${gt} = cmp gt ${a} ${zero} : Bool"));
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = arith mul ${gt} ${raw} : Int"));
                    Some(slot)
                }
                // Const peep; variable unsigned path ≤32 via threshold sum;
                // signed path with a>0 math log (a<=0 modeled as 0).
                ("ilog10", 0) => {
                    if let Some(v) = lit_int_i64(&m.receiver) {
                        if v <= 0 {
                            return None;
                        }
                        let log = (v as u64).ilog10();
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const {log} : Int"));
                        return Some(slot);
                    }
                    let (lo, hi) = path_param_bounds(&m.receiver)?;
                    if hi <= 0 && !is_u64_width_bounds(lo, hi) {
                        return None;
                    }
                    let signed = lo != 0;
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let thr_hi = if is_u64_width_bounds(lo, hi) {
                        -1 // full u64 domain (encode builds 10^k through 10^19)
                    } else {
                        hi
                    };
                    if !signed {
                        return encode_unsigned_ilog10(a, thr_hi, lines, next);
                    }
                    let zero = *next;
                    *next += 1;
                    lines.push(format!("${zero} = const 0 : Int"));
                    let one = *next;
                    *next += 1;
                    lines.push(format!("${one} = const 1 : Int"));
                    let a_pos = *next;
                    *next += 1;
                    lines.push(format!("${a_pos} = call max (${a}, ${one}) : Int"));
                    let raw = encode_unsigned_ilog10(a_pos, thr_hi, lines, next)?;
                    let gt = *next;
                    *next += 1;
                    lines.push(format!("${gt} = cmp gt ${a} ${zero} : Bool"));
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = arith mul ${gt} ${raw} : Int"));
                    Some(slot)
                }
                // Const peep; variable unsigned path ≤64 (overflow → 0, like wrap).
                ("next_power_of_two", 0) => {
                    if let Some(v) = lit_int_i64(&m.receiver) {
                        if v < 0 {
                            return None;
                        }
                        let pot = (v as u64).next_power_of_two();
                        // Keep result in i64 (next_power_of_two of values near 2^63 overflows)
                        if pot > i64::MAX as u64 {
                            return None;
                        }
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const {pot} : Int"));
                        return Some(slot);
                    }
                    let (lo, hi) = path_param_bounds(&m.receiver)?;
                    if lo != 0 {
                        return None;
                    }
                    let bits = if is_u64_width_bounds(lo, hi) {
                        64
                    } else {
                        let modulus_u = (hi as u64).checked_add(1)?;
                        if !modulus_u.is_power_of_two() {
                            return None;
                        }
                        modulus_u.trailing_zeros()
                    };
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    encode_unsigned_next_power_of_two(a, bits, lines, next)
                }
                // Const peep or variable unsigned path ≤64 (overflow → 0).
                // Manual: stable API; unstable wrapping_next_power_of_two not used.
                ("wrapping_next_power_of_two", 0) => {
                    if let Some((v, bits)) = lit_int_i64_bits(&m.receiver) {
                        if v < 0 {
                            return None;
                        }
                        let vu = v as u64;
                        let pot = if vu == 0 {
                            1u64
                        } else {
                            let n = vu.next_power_of_two();
                            // If next power does not fit in `bits`, wrap to 0.
                            if bits < 64 && n >= (1u64 << bits) {
                                0
                            } else if bits == 64 && n < vu {
                                // u64 overflow wraps to 0
                                0
                            } else {
                                n
                            }
                        };
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const {pot} : Int"));
                        return Some(slot);
                    }
                    let (lo, hi) = path_param_bounds(&m.receiver)?;
                    if lo != 0 {
                        return None;
                    }
                    let bits = if is_u64_width_bounds(lo, hi) {
                        64
                    } else {
                        let modulus_u = (hi as u64).checked_add(1)?;
                        if !modulus_u.is_power_of_two() {
                            return None;
                        }
                        modulus_u.trailing_zeros()
                    };
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    encode_unsigned_next_power_of_two(a, bits, lines, next)
                }
                // Const peep; variable unsigned path ≤64 (ladder ≤16; binsearch 17..=64).
                ("isqrt", 0) => {
                    if let Some(v) = lit_int_i64(&m.receiver) {
                        if v < 0 {
                            return None;
                        }
                        let root = (v as u64).isqrt();
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const {root} : Int"));
                        return Some(slot);
                    }
                    let (lo, hi) = path_param_bounds(&m.receiver)?;
                    if lo != 0 {
                        return None;
                    }
                    let bits = if is_u64_width_bounds(lo, hi) {
                        64
                    } else {
                        let modulus_u = (hi as u64).checked_add(1)?;
                        if !modulus_u.is_power_of_two() {
                            return None;
                        }
                        modulus_u.trailing_zeros()
                    };
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    encode_unsigned_isqrt(a, bits, lines, next)
                }
                ("default", 0) => {
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = const 0 : Int"));
                    Some(slot)
                }
                ("lt" | "le" | "gt" | "ge" | "eq" | "ne", 1) => {
                    let cmp = method.as_str();
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let b = encode_syn_expr(&m.args[0], param_names, lines, next)?;
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = cmp {cmp} ${a} ${b} : Bool"));
                    Some(slot)
                }
                (name, 0) if is_identity_peel_method(name) => {
                    encode_syn_expr(&m.receiver, param_names, lines, next)
                }
                // NonZeroU*/I*::get() unwraps to the positive integer (lo >= 1).
                ("get", 0) => {
                    let (lo, _) = path_param_bounds(&m.receiver)?;
                    if lo < 1 {
                        return None;
                    }
                    encode_syn_expr(&m.receiver, param_names, lines, next)
                }
                ("not", 0) => {
                    let zero = *next;
                    *next += 1;
                    lines.push(format!("${zero} = const 0 : Bool"));
                    let inner = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = cmp eq ${inner} ${zero} : Bool"));
                    Some(slot)
                }

                ("is_multiple_of", 1) => {
                    // Rust panics on divisor 0; refuse zero-including divisors so we
                    // do not model mod-by-zero as a free SMT fact (false Verified).
                    if is_lit_int_zero(&m.args[0]) {
                        return None;
                    }
                    // is_multiple_of(±1) is always true for integers.
                    if is_lit_int_abs_one(&m.args[0]) {
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const 1 : Bool"));
                        return Some(slot);
                    }
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    // Const nonzero (any sign) or NonZeroU* / lo>=1 path param.
                    let b = if let Some(v) = lit_int_i64(&m.args[0]) {
                        if v == 0 {
                            return None;
                        }
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const {v} : Int"));
                        slot
                    } else {
                        encode_positive_divisor(&m.args[0], param_names, lines, next)?
                    };
                    let rem = *next;
                    *next += 1;
                    lines.push(format!("${rem} = arith mod ${a} ${b} : Int"));
                    let z = *next;
                    *next += 1;
                    lines.push(format!("${z} = const 0 : Int"));
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = cmp eq ${rem} ${z} : Bool"));
                    Some(slot)
                }
                // div_ceil for non-neg receiver + positive divisor: (a+b-1)/b.
                // Divisor: positive const or NonZeroU* path param (lo >= 1).
                // Receiver must be non-negative: path param with lo>=0, or non-neg lit.
                ("div_ceil", 1) => {
                    let nonneg = if let Some(v) = lit_int_i64(&m.receiver) {
                        v >= 0
                    } else if let Some((lo, _)) = path_param_bounds(&m.receiver) {
                        lo >= 0
                    } else {
                        false
                    };
                    if !nonneg {
                        return None;
                    }
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let b = encode_positive_divisor(&m.args[0], param_names, lines, next)?;
                    let one = *next;
                    *next += 1;
                    lines.push(format!("${one} = const 1 : Int"));
                    let bm1 = *next;
                    *next += 1;
                    lines.push(format!("${bm1} = arith sub ${b} ${one} : Int"));
                    let sum = *next;
                    *next += 1;
                    lines.push(format!("${sum} = arith add ${a} ${bm1} : Int"));
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = arith div ${sum} ${b} : Int"));
                    Some(slot)
                }
                // rem_euclid with positive divisor: ((a mod b) + b) mod b
                // (works for signed a; non-neg reduces to a mod b).
                // Divisor: positive const, or path param with lo >= 1.
                ("rem_euclid", 1) => {
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let b = encode_positive_divisor(&m.args[0], param_names, lines, next)?;
                    let t1 = *next;
                    *next += 1;
                    lines.push(format!("${t1} = arith mod ${a} ${b} : Int"));
                    let t2 = *next;
                    *next += 1;
                    lines.push(format!("${t2} = arith add ${t1} ${b} : Int"));
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = arith mod ${t2} ${b} : Int"));
                    Some(slot)
                }
                // div_euclid with positive divisor ≡ floor div (SMT Int).
                ("div_euclid", 1) => {
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let b = encode_positive_divisor(&m.args[0], param_names, lines, next)?;
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = arith div ${a} ${b} : Int"));
                    Some(slot)
                }
                // next_multiple_of with positive m: a - rem + m*[rem!=0]
                // where rem = rem_euclid(a,m). Works for signed a.
                ("next_multiple_of", 1) => {
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let mv = encode_positive_divisor(&m.args[0], param_names, lines, next)?;
                    // rem = ((a mod m) + m) mod m
                    let t1 = *next;
                    *next += 1;
                    lines.push(format!("${t1} = arith mod ${a} ${mv} : Int"));
                    let t2 = *next;
                    *next += 1;
                    lines.push(format!("${t2} = arith add ${t1} ${mv} : Int"));
                    let rem = *next;
                    *next += 1;
                    lines.push(format!("${rem} = arith mod ${t2} ${mv} : Int"));
                    let zero = *next;
                    *next += 1;
                    lines.push(format!("${zero} = const 0 : Int"));
                    let is_zero = *next;
                    *next += 1;
                    lines.push(format!("${is_zero} = cmp eq ${rem} ${zero} : Bool"));
                    let one = *next;
                    *next += 1;
                    lines.push(format!("${one} = const 1 : Int"));
                    let not_zero = *next;
                    *next += 1;
                    lines.push(format!("${not_zero} = arith sub ${one} ${is_zero} : Int"));
                    let m_if = *next;
                    *next += 1;
                    lines.push(format!("${m_if} = arith mul ${mv} ${not_zero} : Int"));
                    let a_m_rem = *next;
                    *next += 1;
                    lines.push(format!("${a_m_rem} = arith sub ${a} ${rem} : Int"));
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = arith add ${a_m_rem} ${m_if} : Int"));
                    Some(slot)
                }
                ("pow", 1) => {
                    let syn::Expr::Lit(syn::ExprLit {
                        lit: syn::Lit::Int(n),
                        ..
                    }) = &m.args[0]
                    else {
                        return None;
                    };
                    let exp: u32 = n.base10_parse().ok()?;
                    if exp > 4 {
                        return None;
                    }
                    let base = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    if exp == 0 {
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const 1 : Int"));
                        return Some(slot);
                    }
                    let mut acc = base;
                    for _ in 1..exp {
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = arith mul ${acc} ${base} : Int"));
                        acc = slot;
                    }
                    Some(acc)
                }
                // wrapping_pow with small const exp: mul chain + mod 2^w (≤64).
                ("wrapping_pow", 1) => {
                    let syn::Expr::Lit(syn::ExprLit {
                        lit: syn::Lit::Int(n),
                        ..
                    }) = &m.args[0]
                    else {
                        return None;
                    };
                    let exp: u32 = n.base10_parse().ok()?;
                    if exp > 4 {
                        return None;
                    }
                    let (lo, hi) = wrap_bounds_for(&m.receiver)?;
                    let (_bits, modulus_i64, signed) = wrap_width(lo, hi)?;
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    if exp == 0 {
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const 1 : Int"));
                        return Some(slot);
                    }
                    let mslot = emit_signed_modulus_slot(modulus_i64, lines, next);
                    let base_u = if signed {
                        emit_to_unsigned_bits(a, mslot, lines, next)
                    } else {
                        a
                    };
                    let mut acc = base_u;
                    for _ in 1..exp {
                        let prod = *next;
                        *next += 1;
                        lines.push(format!("${prod} = arith mul ${acc} ${base_u} : Int"));
                        // ((prod mod m) + m) mod m
                        let t1 = *next;
                        *next += 1;
                        lines.push(format!("${t1} = arith mod ${prod} ${mslot} : Int"));
                        let t2 = *next;
                        *next += 1;
                        lines.push(format!("${t2} = arith add ${t1} ${mslot} : Int"));
                        let u = *next;
                        *next += 1;
                        lines.push(format!("${u} = arith mod ${t2} ${mslot} : Int"));
                        acc = u;
                    }
                    if !signed {
                        return Some(acc);
                    }
                    Some(emit_from_unsigned_bits(acc, mslot, hi, lines, next))
                }

                ("min" | "max", 1) => {
                    if expr_same_simple_path(&m.receiver, &m.args[0]) {
                        return encode_syn_expr(&m.receiver, param_names, lines, next);
                    }
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let b = encode_syn_expr(&m.args[0], param_names, lines, next)?;
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = call {method} (${a}, ${b}) : Int"));
                    Some(slot)
                }
                // midpoint: floor((a+b)/2); Int SMT is unbounded so no overflow.
                ("midpoint", 1) => {
                    if expr_same_simple_path(&m.receiver, &m.args[0]) {
                        return encode_syn_expr(&m.receiver, param_names, lines, next);
                    }
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let b = encode_syn_expr(&m.args[0], param_names, lines, next)?;
                    let sum = *next;
                    *next += 1;
                    lines.push(format!("${sum} = arith add ${a} ${b} : Int"));
                    let two = *next;
                    *next += 1;
                    lines.push(format!("${two} = const 2 : Int"));
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = arith div ${sum} ${two} : Int"));
                    Some(slot)
                }
                // x.clamp(lo, hi) ≡ min(max(x, lo), hi)
                ("clamp", 2) => {
                    // clamp(x, b, b) ≡ b for any x
                    if expr_same_simple_path(&m.args[0], &m.args[1]) {
                        return encode_syn_expr(&m.args[0], param_names, lines, next);
                    }
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let lo = encode_syn_expr(&m.args[0], param_names, lines, next)?;
                    let hi = encode_syn_expr(&m.args[1], param_names, lines, next)?;
                    let mx = *next;
                    *next += 1;
                    lines.push(format!("${mx} = call max (${a}, ${lo}) : Int"));
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = call min (${mx}, ${hi}) : Int"));
                    Some(slot)
                }
                ("abs_diff", 1) => {
                    if expr_same_simple_path(&m.receiver, &m.args[0]) {
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = const 0 : Int"));
                        return Some(slot);
                    }
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let b = encode_syn_expr(&m.args[0], param_names, lines, next)?;
                    let d = *next;
                    *next += 1;
                    lines.push(format!("${d} = arith sub ${a} ${b} : Int"));
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = call abs (${d}) : Int"));
                    Some(slot)
                }
                ("saturating_neg", 0) => {
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let zero = *next;
                    *next += 1;
                    lines.push(format!("${zero} = const 0 : Int"));
                    let neg = *next;
                    *next += 1;
                    lines.push(format!("${neg} = arith sub ${zero} ${a} : Int"));
                    emit_sat_clamp(neg, lines, next)
                }
                // saturating_abs: abs then clamp to MAX (i64::MIN → MAX, not |MIN|).
                ("saturating_abs", 0) => {
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let ab = *next;
                    *next += 1;
                    lines.push(format!("${ab} = call abs (${a}) : Int"));
                    let (_, hi_v) = SAT_BOUNDS.get()?;
                    let hi = *next;
                    *next += 1;
                    lines.push(format!("${hi} = const {hi_v} : Int"));
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = call min (${ab}, ${hi}) : Int"));
                    Some(slot)
                }
                // saturating_add/sub: clamp arith to i64 range (#1007; needs param
                // range requires from check_rust for soundness on unbounded Int).
                ("saturating_add" | "saturating_sub" | "saturating_mul", 1) => {
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let b = encode_syn_expr(&m.args[0], param_names, lines, next)?;
                    let op = match method.as_str() {
                        "saturating_add" => "add",
                        "saturating_sub" => "sub",
                        "saturating_mul" => "mul",
                        _ => return None,
                    };
                    let sum = *next;
                    *next += 1;
                    lines.push(format!("${sum} = arith {op} ${a} ${b} : Int"));
                    emit_sat_clamp(sum, lines, next)
                }
                // wrapping_* peeps for identity constants (before general mod 2^w path):
                // wrapping_add(x, 0) / wrapping_sub(x, 0) ≡ x; wrapping_mul(x, 1) ≡ x;
                // wrapping_mul(x, 0) ≡ 0; wrapping_sub(x, x) ≡ 0.
                // Same for wrapping_{add,sub}_{signed,unsigned} (modular Int is sign-agnostic).
                (
                    "wrapping_add"
                    | "wrapping_sub"
                    | "wrapping_add_signed"
                    | "wrapping_sub_signed"
                    | "wrapping_add_unsigned"
                    | "wrapping_sub_unsigned",
                    1,
                ) if is_lit_int_zero(&m.args[0]) => {
                    encode_syn_expr(&m.receiver, param_names, lines, next)
                }
                ("wrapping_sub" | "wrapping_sub_signed" | "wrapping_sub_unsigned", 1)
                    if expr_same_simple_path(&m.receiver, &m.args[0]) =>
                {
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = const 0 : Int"));
                    Some(slot)
                }
                ("wrapping_mul", 1) if is_lit_int_zero(&m.args[0]) => {
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = const 0 : Int"));
                    Some(slot)
                }
                ("wrapping_mul", 1)
                    if matches!(
                        &m.args[0],
                        syn::Expr::Lit(syn::ExprLit {
                            lit: syn::Lit::Int(n),
                            ..
                        }) if n.base10_digits() == "1"
                    ) =>
                {
                    encode_syn_expr(&m.receiver, param_names, lines, next)
                }
                // Shift/rotate by 0 is identity (signed or unsigned).
                ("wrapping_shl" | "wrapping_shr" | "rotate_left" | "rotate_right", 1)
                    if is_lit_int_zero(&m.args[0]) =>
                {
                    encode_syn_expr(&m.receiver, param_names, lines, next)
                }
                // wrapping_shl/shr by const or variable amount (#1010/#1145/#1151/#1160).
                // Unsigned: shl (x * 2^k) mod 2^w; shr floor x / 2^k.
                // Signed: wrapping_shl via mul+double-mod+reinterpret; wrapping_shr
                // via floor div by 2^k. Variable k: case-sum over k%bits for bits<=64.
                // u64/usize use synthetic 2^64 (bounds sentinel (0,-1)).
                ("wrapping_shl" | "wrapping_shr", 1) => {
                    let (lo, hi) = wrap_bounds_for(&m.receiver)?;
                    let (bits, modulus_i64, signed) = wrap_width(lo, hi)?;
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    // Const shift amount (fast path)
                    if let Some(k) = lit_int_i64(&m.args[0]) {
                        if k < 0 {
                            return None;
                        }
                        let k_eff = (k as u64) % (bits as u64);
                        if k_eff == 0 {
                            return Some(a);
                        }
                        let f = emit_pow2_factor(k_eff as u32, lines, next)?;
                        if method == "wrapping_shr" {
                            let slot = *next;
                            *next += 1;
                            lines.push(format!("${slot} = arith div ${a} ${f} : Int"));
                            return Some(slot);
                        }
                        let raw = *next;
                        *next += 1;
                        lines.push(format!("${raw} = arith mul ${a} ${f} : Int"));
                        let mslot = emit_signed_modulus_slot(modulus_i64, lines, next);
                        let t1 = *next;
                        *next += 1;
                        lines.push(format!("${t1} = arith mod ${raw} ${mslot} : Int"));
                        let t2 = *next;
                        *next += 1;
                        lines.push(format!("${t2} = arith add ${t1} ${mslot} : Int"));
                        let u = *next;
                        *next += 1;
                        lines.push(format!("${u} = arith mod ${t2} ${mslot} : Int"));
                        if !signed {
                            return Some(u);
                        }
                        let his = *next;
                        *next += 1;
                        lines.push(format!("${his} = const {hi} : Int"));
                        let gt = *next;
                        *next += 1;
                        lines.push(format!("${gt} = cmp gt ${u} ${his} : Bool"));
                        let adj = *next;
                        *next += 1;
                        lines.push(format!("${adj} = arith mul ${gt} ${mslot} : Int"));
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = arith sub ${u} ${adj} : Int"));
                        return Some(slot);
                    }
                    // Variable shift: case-sum over k%bits (bits<=64, incl. signed i64).
                    if bits > 64 {
                        return None;
                    }
                    let k_slot = encode_syn_expr(&m.args[0], param_names, lines, next)?;
                    // Require non-neg path param for shift amount when available.
                    if let Some((klo, _)) = path_param_bounds(&m.args[0])
                        && klo < 0
                    {
                        return None;
                    }
                    let bits_c = *next;
                    *next += 1;
                    lines.push(format!("${bits_c} = const {bits} : Int"));
                    // k_eff = k mod bits (k non-neg)
                    let t1 = *next;
                    *next += 1;
                    lines.push(format!("${t1} = arith mod ${k_slot} ${bits_c} : Int"));
                    let t2 = *next;
                    *next += 1;
                    lines.push(format!("${t2} = arith add ${t1} ${bits_c} : Int"));
                    let k_eff = *next;
                    *next += 1;
                    lines.push(format!("${k_eff} = arith mod ${t2} ${bits_c} : Int"));
                    let mslot = emit_signed_modulus_slot(modulus_i64, lines, next);
                    let zero = *next;
                    *next += 1;
                    lines.push(format!("${zero} = const 0 : Int"));
                    let mut acc = zero;
                    for e in 0..bits {
                        let e_c = *next;
                        *next += 1;
                        lines.push(format!("${e_c} = const {e} : Int"));
                        let eq = *next;
                        *next += 1;
                        lines.push(format!("${eq} = cmp eq ${k_eff} ${e_c} : Bool"));
                        let f = emit_pow2_factor(e, lines, next)?;
                        let case_val = if method == "wrapping_shr" {
                            let d = *next;
                            *next += 1;
                            lines.push(format!("${d} = arith div ${a} ${f} : Int"));
                            d
                        } else {
                            let raw = *next;
                            *next += 1;
                            lines.push(format!("${raw} = arith mul ${a} ${f} : Int"));
                            let s1 = *next;
                            *next += 1;
                            lines.push(format!("${s1} = arith mod ${raw} ${mslot} : Int"));
                            let s2 = *next;
                            *next += 1;
                            lines.push(format!("${s2} = arith add ${s1} ${mslot} : Int"));
                            let u = *next;
                            *next += 1;
                            lines.push(format!("${u} = arith mod ${s2} ${mslot} : Int"));
                            if !signed {
                                u
                            } else {
                                let his = *next;
                                *next += 1;
                                lines.push(format!("${his} = const {hi} : Int"));
                                let gt = *next;
                                *next += 1;
                                lines.push(format!("${gt} = cmp gt ${u} ${his} : Bool"));
                                let adj = *next;
                                *next += 1;
                                lines.push(format!("${adj} = arith mul ${gt} ${mslot} : Int"));
                                let slot = *next;
                                *next += 1;
                                lines.push(format!("${slot} = arith sub ${u} ${adj} : Int"));
                                slot
                            }
                        };
                        let term = *next;
                        *next += 1;
                        lines.push(format!("${term} = arith mul ${eq} ${case_val} : Int"));
                        let sum = *next;
                        *next += 1;
                        lines.push(format!("${sum} = arith add ${acc} ${term} : Int"));
                        acc = sum;
                    }
                    Some(acc)
                }
                // rotate_left/right by const or variable k.
                // Unsigned: rotl ≡ (x*2^k + x/2^(bits-k)) mod 2^w.
                // Signed: map to unsigned bit pattern, rotate, reinterpret.
                // Variable: case-sum over k%bits for bits<=64 (same budget as shifts).
                ("rotate_left" | "rotate_right", 1) => {
                    let (lo, hi) = wrap_bounds_for(&m.receiver)?;
                    let (bits, modulus_i64, signed) = wrap_width(lo, hi)?;
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let mslot = emit_signed_modulus_slot(modulus_i64, lines, next);
                    let wrap = RotWrap {
                        bits,
                        mslot,
                        signed,
                        hi,
                    };
                    // Unsigned bit pattern: ((a mod m) + m) mod m
                    let t1 = *next;
                    *next += 1;
                    lines.push(format!("${t1} = arith mod ${a} ${mslot} : Int"));
                    let t2 = *next;
                    *next += 1;
                    lines.push(format!("${t2} = arith add ${t1} ${mslot} : Int"));
                    let u_in = *next;
                    *next += 1;
                    lines.push(format!("${u_in} = arith mod ${t2} ${mslot} : Int"));

                    // Const shift amount (fast path)
                    if let Some(k) = lit_int_i64(&m.args[0]) {
                        if k < 0 {
                            return None;
                        }
                        let k_eff = (k as u32) % bits;
                        if k_eff == 0 {
                            return Some(a);
                        }
                        // rotate_right(k) ≡ rotate_left(bits-k)
                        let k_left = if method == "rotate_left" {
                            k_eff
                        } else {
                            bits - k_eff
                        };
                        return emit_rotl_bits(u_in, k_left, &wrap, lines, next);
                    }

                    // Variable: case-sum over k%bits (bits<=64, matching wrapping_shl/shr).
                    if bits == 0 || bits > 64 {
                        return None;
                    }
                    let k_slot = encode_syn_expr(&m.args[0], param_names, lines, next)?;
                    if let Some((klo, _)) = path_param_bounds(&m.args[0])
                        && klo < 0
                    {
                        return None;
                    }
                    let bits_c = *next;
                    *next += 1;
                    lines.push(format!("${bits_c} = const {bits} : Int"));
                    let tm1 = *next;
                    *next += 1;
                    lines.push(format!("${tm1} = arith mod ${k_slot} ${bits_c} : Int"));
                    let tm2 = *next;
                    *next += 1;
                    lines.push(format!("${tm2} = arith add ${tm1} ${bits_c} : Int"));
                    let k_eff = *next;
                    *next += 1;
                    lines.push(format!("${k_eff} = arith mod ${tm2} ${bits_c} : Int"));
                    let zero = *next;
                    *next += 1;
                    lines.push(format!("${zero} = const 0 : Int"));
                    let mut acc = zero;
                    for e in 0..bits {
                        let e_c = *next;
                        *next += 1;
                        lines.push(format!("${e_c} = const {e} : Int"));
                        let eq = *next;
                        *next += 1;
                        lines.push(format!("${eq} = cmp eq ${k_eff} ${e_c} : Bool"));
                        // For rotate_right, case e means rotl by (bits-e)%bits
                        let k_left = if method == "rotate_left" {
                            e
                        } else if e == 0 {
                            0
                        } else {
                            bits - e
                        };
                        let case_val = if k_left == 0 {
                            if signed {
                                emit_rotl_bits(u_in, 0, &wrap, lines, next)?
                            } else {
                                u_in
                            }
                        } else {
                            emit_rotl_bits(u_in, k_left, &wrap, lines, next)?
                        };
                        let term = *next;
                        *next += 1;
                        lines.push(format!("${term} = arith mul ${eq} ${case_val} : Int"));
                        let sum = *next;
                        *next += 1;
                        lines.push(format!("${sum} = arith add ${acc} ${term} : Int"));
                        acc = sum;
                    }
                    Some(acc)
                }
                // wrapping_* via mod 2^w (#1010).
                // Unsigned (lo==0): result in [0, 2^w).
                // Signed: double-mod to [0, 2^w) then reinterpret as two's complement.
                // Double-mod ((raw mod m) + m) mod m works for large |raw| (signed mul)
                // without a 2^(2w-1) offset that may not fit in i64.
                // i64 modulus is 2^64: emit as (2^32)*(2^32) (const 2^64 is not i64).
                (
                    "wrapping_add"
                    | "wrapping_sub"
                    | "wrapping_mul"
                    | "wrapping_add_signed"
                    | "wrapping_sub_signed"
                    | "wrapping_add_unsigned"
                    | "wrapping_sub_unsigned",
                    1,
                ) => {
                    // Prefer return-type bounds; fall back to receiver width for nested
                    // uses like `x.wrapping_add(1).is_power_of_two()` (bool return).
                    // wrapping_{add,sub}_{signed,unsigned} are the same modular add/sub
                    // in SMT Int (arg sign is only a Rust type-system distinction).
                    let (lo, hi) = wrap_bounds_for(&m.receiver)?;
                    let (_bits, modulus_i64, signed) = wrap_width(lo, hi)?;
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let b = encode_syn_expr(&m.args[0], param_names, lines, next)?;
                    let raw = *next;
                    *next += 1;
                    let op = match method.as_str() {
                        "wrapping_add" | "wrapping_add_signed" | "wrapping_add_unsigned" => "add",
                        "wrapping_sub" | "wrapping_sub_signed" | "wrapping_sub_unsigned" => "sub",
                        "wrapping_mul" => "mul",
                        _ => return None,
                    };
                    lines.push(format!("${raw} = arith {op} ${a} ${b} : Int"));
                    let mslot = emit_signed_modulus_slot(modulus_i64, lines, next);
                    // ((raw mod m) + m) mod m → [0, m) for any raw (truncating or Euclidean)
                    let t1 = *next;
                    *next += 1;
                    lines.push(format!("${t1} = arith mod ${raw} ${mslot} : Int"));
                    let t2 = *next;
                    *next += 1;
                    lines.push(format!("${t2} = arith add ${t1} ${mslot} : Int"));
                    let u = *next;
                    *next += 1;
                    lines.push(format!("${u} = arith mod ${t2} ${mslot} : Int"));
                    if !signed {
                        return Some(u);
                    }
                    // Reinterpret u ∈ [0, 2^w) as signed: u - 2^w * (u > hi)
                    let his = *next;
                    *next += 1;
                    lines.push(format!("${his} = const {hi} : Int"));
                    let gt = *next;
                    *next += 1;
                    lines.push(format!("${gt} = cmp gt ${u} ${his} : Bool"));
                    let adj = *next;
                    *next += 1;
                    lines.push(format!("${adj} = arith mul ${gt} ${mslot} : Int"));
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = arith sub ${u} ${adj} : Int"));
                    Some(slot)
                }
                // wrapping_neg: (0 - x) mod 2^w; signed reinterprets into [lo, hi].
                // Nested signed works in single-block IR (no top-level expand required).
                ("wrapping_neg", 0) => {
                    let (lo, hi) = wrap_bounds_for(&m.receiver)?;
                    let (_bits, modulus_i64, signed) = wrap_width(lo, hi)?;
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    let zero = *next;
                    *next += 1;
                    lines.push(format!("${zero} = const 0 : Int"));
                    let raw = *next;
                    *next += 1;
                    lines.push(format!("${raw} = arith sub ${zero} ${a} : Int"));
                    let mslot = emit_signed_modulus_slot(modulus_i64, lines, next);
                    // rem_euclid into [0, m)
                    let t1 = *next;
                    *next += 1;
                    lines.push(format!("${t1} = arith mod ${raw} ${mslot} : Int"));
                    let t2 = *next;
                    *next += 1;
                    lines.push(format!("${t2} = arith add ${t1} ${mslot} : Int"));
                    let u = *next;
                    *next += 1;
                    lines.push(format!("${u} = arith mod ${t2} ${mslot} : Int"));
                    if !signed {
                        return Some(u);
                    }
                    let his = *next;
                    *next += 1;
                    lines.push(format!("${his} = const {hi} : Int"));
                    let gt = *next;
                    *next += 1;
                    lines.push(format!("${gt} = cmp gt ${u} ${his} : Bool"));
                    let adj = *next;
                    *next += 1;
                    lines.push(format!("${adj} = arith mul ${gt} ${mslot} : Int"));
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = arith sub ${u} ${adj} : Int"));
                    Some(slot)
                }
                // wrapping_div / wrapping_rem: nonzero const or positive path-param
                // divisor only (Rust panics on /0). Sole wrap case: signed MIN / -1
                // → MIN (≡ wrapping_neg); MIN % -1 → 0.
                ("wrapping_div" | "wrapping_rem", 1) => {
                    if is_lit_int_zero(&m.args[0]) {
                        return None;
                    }
                    let a = encode_syn_expr(&m.receiver, param_names, lines, next)?;
                    if let Some(c) = lit_int_i64(&m.args[0]) {
                        if c == 0 {
                            return None;
                        }
                        // rem ±1 is always 0 when defined (including MIN % -1 wrap).
                        if method == "wrapping_rem" && (c == 1 || c == -1) {
                            let slot = *next;
                            *next += 1;
                            lines.push(format!("${slot} = const 0 : Int"));
                            return Some(slot);
                        }
                        // wrapping_div by -1 ≡ wrapping_neg (MIN stays MIN).
                        if method == "wrapping_div" && c == -1 {
                            let (lo, hi) = wrap_bounds_for(&m.receiver)?;
                            let (_bits, modulus_i64, signed) = wrap_width(lo, hi)?;
                            let zero = *next;
                            *next += 1;
                            lines.push(format!("${zero} = const 0 : Int"));
                            let raw = *next;
                            *next += 1;
                            lines.push(format!("${raw} = arith sub ${zero} ${a} : Int"));
                            let mslot = emit_signed_modulus_slot(modulus_i64, lines, next);
                            let t1 = *next;
                            *next += 1;
                            lines.push(format!("${t1} = arith mod ${raw} ${mslot} : Int"));
                            let t2 = *next;
                            *next += 1;
                            lines.push(format!("${t2} = arith add ${t1} ${mslot} : Int"));
                            let u = *next;
                            *next += 1;
                            lines.push(format!("${u} = arith mod ${t2} ${mslot} : Int"));
                            if !signed {
                                return Some(u);
                            }
                            let his = *next;
                            *next += 1;
                            lines.push(format!("${his} = const {hi} : Int"));
                            let gt = *next;
                            *next += 1;
                            lines.push(format!("${gt} = cmp gt ${u} ${his} : Bool"));
                            let adj = *next;
                            *next += 1;
                            lines.push(format!("${adj} = arith mul ${gt} ${mslot} : Int"));
                            let slot = *next;
                            *next += 1;
                            lines.push(format!("${slot} = arith sub ${u} ${adj} : Int"));
                            return Some(slot);
                        }
                        let b = *next;
                        *next += 1;
                        lines.push(format!("${b} = const {c} : Int"));
                        let ir_op = if method == "wrapping_div" {
                            "div"
                        } else {
                            "mod"
                        };
                        let slot = *next;
                        *next += 1;
                        lines.push(format!("${slot} = arith {ir_op} ${a} ${b} : Int"));
                        return Some(slot);
                    }
                    // Non-literal: only positive path params (e.g. NonZeroU*).
                    let (lo, _) = path_param_bounds(&m.args[0])?;
                    if lo < 1 {
                        return None;
                    }
                    let b = encode_syn_expr(&m.args[0], param_names, lines, next)?;
                    let ir_op = if method == "wrapping_div" {
                        "div"
                    } else {
                        "mod"
                    };
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = arith {ir_op} ${a} ${b} : Int"));
                    Some(slot)
                }
                _ => None,
            }
        }
        // `x as T` identity only for lossless targets (i64/isize/bool).
        // Narrowing (`i64 as i32`) stays unencoded — both map to Int in Assura
        // and would silently drop high bits.
        syn::Expr::Cast(c) => {
            let ty_tokens = c.ty.to_token_stream().to_string().replace(' ', "");
            if !matches!(ty_tokens.as_str(), "i64" | "isize" | "bool") {
                return None;
            }
            encode_syn_expr(&c.expr, param_names, lines, next)
        }
        syn::Expr::Call(c) => {
            let syn::Expr::Path(path) = c.func.as_ref() else {
                return None;
            };
            // Free `abs`/`min`/`max` or associated `i64::max` / `i32::min`.
            let name = path.path.segments.last()?.ident.to_string();
            if path.path.segments.len() > 2 {
                return None;
            }
            match (name.as_str(), c.args.len()) {
                ("abs", 1) => {
                    let a = encode_syn_expr(&c.args[0], param_names, lines, next)?;
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = call abs (${a}) : Int"));
                    Some(slot)
                }
                // i64::saturating_abs(x) associated form
                ("saturating_abs", 1) if path.path.segments.len() == 2 => {
                    let a = encode_syn_expr(&c.args[0], param_names, lines, next)?;
                    let ab = *next;
                    *next += 1;
                    lines.push(format!("${ab} = call abs (${a}) : Int"));
                    let (_, hi_v) = SAT_BOUNDS.get()?;
                    let hi = *next;
                    *next += 1;
                    lines.push(format!("${hi} = const {hi_v} : Int"));
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = call min (${ab}, ${hi}) : Int"));
                    Some(slot)
                }
                ("min" | "max", 2) => {
                    if expr_same_simple_path(&c.args[0], &c.args[1]) {
                        return encode_syn_expr(&c.args[0], param_names, lines, next);
                    }
                    let a = encode_syn_expr(&c.args[0], param_names, lines, next)?;
                    let b = encode_syn_expr(&c.args[1], param_names, lines, next)?;
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = call {name} (${a}, ${b}) : Int"));
                    Some(slot)
                }
                ("from", 1) if path.path.segments.len() == 2 => {
                    // i64::from(x) identity for integer-like
                    encode_syn_expr(&c.args[0], param_names, lines, next)
                }
                ("default", 0) => {
                    let slot = *next;
                    *next += 1;
                    lines.push(format!("${slot} = const 0 : Int"));
                    Some(slot)
                }
                _ => None,
            }
        }
        _ => None,
    }
}

/// Params / return type from an annotated item Function.
pub(crate) fn function_params_return(
    kind: &assura_rust_analyzer::AnnotatedItemKind,
) -> Option<(&[ParamInfo], Option<&str>)> {
    match kind {
        assura_rust_analyzer::AnnotatedItemKind::Function {
            params,
            return_type,
            ..
        } => Some((params.as_slice(), return_type.as_deref())),
        _ => None,
    }
}

#[cfg(test)]
mod tests;