aver-lang 0.25.0

//! Int-wrapper algebraic-law detectors (commutative / associative /
//! identity / anti-commutative / unary-equals-binary) and their
//! private AST matchers.
//!
//! Split from `proof_lower.rs` — see the module docs in [`super`].

use super::*;

/// Stage 8 of #232: detect `wrapper(g) == other(g)` where `wrapper`
/// is a `ModulePattern::WrapperOverRecursion` and the inner fn has a
/// monoidal-accumulator shape we know how to emit Dafny support
/// theorems for. Returns the typed strategy carrying enough payload
/// for the backend to emit the aux acc-decomposition lemma without
/// re-walking the AST.
pub(super) fn detect_wrapper_over_recursion(
    law: &crate::ast::VerifyLaw,
    fn_name: &str,
    inputs: &ProofLowerInputs,
) -> Option<crate::ir::ProofStrategy> {
    use crate::analysis::shape::ModulePattern;
    use crate::ast::{BinOp, Expr, Stmt};

    // Pre-pipeline AST has `Expr::Ident(n)`; post-pipeline the
    // resolver rewrites local/param idents to `Expr::Resolved { name }`.
    // Both forms identify the same surface name.
    fn ident_name(e: &Spanned<Expr>) -> Option<&str> {
        match &e.node {
            Expr::Ident(n) => Some(n.as_str()),
            Expr::Resolved { name, .. } => Some(name.as_str()),
            _ => None,
        }
    }

    let shape = inputs.program_shape?;

    // Only handle single-given laws — the template is parameterized
    // by one universal `xs`.
    if law.givens.len() != 1 {
        return None;
    }
    let given_name = &law.givens[0].name;

    // Read the loop fn + its fold step from the shared `AccumulatorFold` pattern
    // (recognized once by `analysis::shape`, consumed by both this strategy and
    // the `--discover` lemma chains) — no bespoke inner-body re-walk for the OP.
    // The monoidal strategy needs an additive/multiplicative inline step and an
    // identity finish (the nil arm returns the accumulator).
    let (inner_fn, combine_op) = shape.patterns.iter().find_map(|p| match p {
        ModulePattern::AccumulatorFold {
            wrapper_fn,
            loop_fn,
            step_op: Some(op),
            finish_fn: None,
            ..
        } if wrapper_fn == fn_name && matches!(op, BinOp::Add | BinOp::Mul) => {
            Some((loop_fn.clone(), *op))
        }
        _ => None,
    })?;
    let wrapper_fn = fn_name.to_string();

    // Law shape: `wrapper(g) == other(g)` (either side).
    let extract = |expr: &Spanned<crate::ast::Expr>| -> Option<String> {
        let Expr::FnCall(callee, args) = &expr.node else {
            return None;
        };
        let name = ident_name(callee)?;
        if args.len() != 1 {
            return None;
        }
        if ident_name(&args[0])? != given_name {
            return None;
        }
        Some(name.to_string())
    };
    let lhs_call = extract(&law.lhs);
    let rhs_call = extract(&law.rhs);
    let other_fn = match (lhs_call, rhs_call) {
        (Some(l), Some(r)) if l == wrapper_fn && r != wrapper_fn => r,
        (Some(l), Some(r)) if r == wrapper_fn && l != wrapper_fn => l,
        _ => return None,
    };

    // Wrapper body must be `inner(<given>, neutral)` where neutral is
    // 0 for Add and 1 for Mul. Verify against the fn def to be sure.
    let wrapper_fd = inputs.find_fn_def_by_call_name(&wrapper_fn)?;
    let wstmts = wrapper_fd.body.stmts();
    if wstmts.len() != 1 {
        return None;
    }
    let Stmt::Expr(wbody) = &wstmts[0] else {
        return None;
    };
    let (wcallee_name, wargs) = match &wbody.node {
        Expr::FnCall(c, a) => (ident_name(c)?, a.clone()),
        Expr::TailCall(td) => (td.target.as_str(), td.args.clone()),
        _ => return None,
    };
    if wcallee_name != inner_fn {
        return None;
    }
    if wargs.len() != 2 {
        return None;
    }
    let expected_neutral: i64 = match combine_op {
        BinOp::Add | BinOp::Sub => 0,
        BinOp::Mul => 1,
        _ => return None,
    };
    let neutral_matches = matches!(
        &wargs[1].node,
        Expr::Literal(crate::ast::Literal::Int(n)) if *n == expected_neutral
    );
    if !neutral_matches {
        return None;
    }

    Some(crate::ir::ProofStrategy::WrapperOverRecursion {
        wrapper_fn,
        inner_fn,
        other_fn,
        combine_op,
    })
}

/// Return `Some(op)` iff `fn_name` resolves to a 2-arg Int wrapper
/// `fn f(p1: Int, p2: Int) -> Int :- p1 <op> p2`. The op family
/// covers `Add` / `Mul` (commutative + associative lemmas) and
/// `Sub` (anti-commutative + right-identity); other ops fall back
/// to `BackendDispatch`.
pub(super) fn wrapper_binop(fn_name: &str, inputs: &ProofLowerInputs) -> Option<crate::ast::BinOp> {
    use crate::ast::{BinOp, Expr};

    let fd = inputs.find_fn_def_by_call_name(fn_name)?;
    if fd.params.len() != 2 || fd.return_type != "Int" {
        return None;
    }
    let (p1, t1) = &fd.params[0];
    let (p2, t2) = &fd.params[1];
    if t1 != "Int" || t2 != "Int" {
        return None;
    }
    let expr = body_terminal_expr(fd.body.as_ref())?;
    let Expr::BinOp(op, left, right) = &expr.node else {
        return None;
    };
    if !matches_ident_expr(left, p1) || !matches_ident_expr(right, p2) {
        return None;
    }
    matches!(op, BinOp::Add | BinOp::Mul | BinOp::Sub).then_some(*op)
}

pub(super) fn detect_wrapper_commutative(
    law: &crate::ast::VerifyLaw,
    fn_name: &str,
    _op: crate::ast::BinOp,
) -> bool {
    if law.givens.len() != 2 || law.givens.iter().any(|g| g.type_name != "Int") {
        return false;
    }
    let a = &law.givens[0].name;
    let b = &law.givens[1].name;
    matches_binary_call(&law.lhs, fn_name, a, b) && matches_binary_call(&law.rhs, fn_name, b, a)
        || matches_binary_call(&law.lhs, fn_name, b, a)
            && matches_binary_call(&law.rhs, fn_name, a, b)
}

pub(super) fn detect_wrapper_associative(
    law: &crate::ast::VerifyLaw,
    fn_name: &str,
    _op: crate::ast::BinOp,
) -> bool {
    if law.givens.len() != 3 || law.givens.iter().any(|g| g.type_name != "Int") {
        return false;
    }
    let a = &law.givens[0].name;
    let b = &law.givens[1].name;
    let c = &law.givens[2].name;
    let nested = |side| matches_assoc_nested(side, fn_name, a, b, c);
    let flat = |side| matches_assoc_flat(side, fn_name, a, b, c);
    (nested(&law.lhs) && flat(&law.rhs)) || (nested(&law.rhs) && flat(&law.lhs))
}

/// Detect a unary↔binary wrapper equivalence shape:
/// outer side: `outer(g)` where `fn outer(p) -> p <op> K`
/// other side: `inner(g, K)` or `inner(K, g)` where `fn inner(a, b) -> a <op> b`
/// Both sides must agree on op + constant + var-position.
/// Returns the inner fn's source name, or `None` if no match.
pub(super) fn detect_wrapper_unary_equivalence(
    law: &crate::ast::VerifyLaw,
    fn_name: &str,
    inputs: &ProofLowerInputs,
) -> Option<String> {
    if law.givens.len() != 1 || law.givens[0].type_name != "Int" {
        return None;
    }
    let unary = unary_int_wrapper(fn_name, inputs)?;
    let g = &law.givens[0].name;

    let try_side = |call_side: &Spanned<crate::ast::Expr>,
                    other_side: &Spanned<crate::ast::Expr>|
     -> Option<String> {
        if !matches_unary_call(call_side, fn_name, g) {
            return None;
        }
        let (callee_name, var_first, lit) = binary_call_var_const(other_side, g)?;
        if lit != unary.constant || var_first != unary.var_first {
            return None;
        }
        let inner_op = wrapper_binop(&callee_name, inputs)?;
        if inner_op != unary.op {
            return None;
        }
        Some(callee_name)
    };
    try_side(&law.lhs, &law.rhs).or_else(|| try_side(&law.rhs, &law.lhs))
}

#[derive(Debug, Clone, Copy)]
pub(super) struct UnaryIntWrapper {
    op: crate::ast::BinOp,
    constant: i64,
    var_first: bool,
}

/// Resolve `fn outer(p: Int) -> Int :- p <op> K` or `K <op> p`.
/// Returns the op + literal + which side carries the param.
pub(super) fn unary_int_wrapper(
    fn_name: &str,
    inputs: &ProofLowerInputs,
) -> Option<UnaryIntWrapper> {
    use crate::ast::{Expr, Literal};

    let fd = inputs.find_fn_def_by_call_name(fn_name)?;
    if fd.params.len() != 1 || fd.return_type != "Int" {
        return None;
    }
    let (param, param_ty) = &fd.params[0];
    if param_ty != "Int" {
        return None;
    }
    let expr = body_terminal_expr(fd.body.as_ref())?;
    let Expr::BinOp(op, left, right) = &expr.node else {
        return None;
    };
    let lit_of = |e: &Spanned<Expr>| -> Option<i64> {
        match &e.node {
            Expr::Literal(Literal::Int(n)) => Some(*n),
            _ => None,
        }
    };
    if matches_ident_expr(left, param) {
        let n = lit_of(right)?;
        return Some(UnaryIntWrapper {
            op: *op,
            constant: n,
            var_first: true,
        });
    }
    if matches_ident_expr(right, param) {
        let n = lit_of(left)?;
        return Some(UnaryIntWrapper {
            op: *op,
            constant: n,
            var_first: false,
        });
    }
    None
}

pub(super) fn matches_unary_call(
    expr: &Spanned<crate::ast::Expr>,
    fn_name: &str,
    arg: &str,
) -> bool {
    use crate::ast::Expr;
    let Expr::FnCall(callee, args) = &expr.node else {
        return false;
    };
    args.len() == 1 && callee_matches_name(callee, fn_name) && matches_ident_expr(&args[0], arg)
}

/// `inner(var, K)` or `inner(K, var)` shape. Returns
/// `(callee_name, var_first, K)` on match.
/// **syntax-discovery-only** (epic #170 Phase 7). Detects a
/// 2-arg fn call whose first arg is `Ident(var_name)` and second
/// is an `Int` literal (or symmetric). Returns the callee's dotted
/// name + the literal — caller dispatches on the name string. Used
/// only against builtin namespace methods (`Int.add`, etc.); the
/// returned name string is not stored or used for identity past
/// the dispatch site.
pub(super) fn binary_call_var_const(
    expr: &Spanned<crate::ast::Expr>,
    var_name: &str,
) -> Option<(String, bool, i64)> {
    use crate::ast::{Expr, Literal};
    let Expr::FnCall(callee, args) = &expr.node else {
        return None;
    };
    if args.len() != 2 {
        return None;
    }
    let callee_name = expr_to_dotted_name(&callee.node)?;
    match (&args[0].node, &args[1].node) {
        (Expr::Ident(v) | Expr::Resolved { name: v, .. }, Expr::Literal(Literal::Int(n)))
            if v == var_name =>
        {
            Some((callee_name, true, *n))
        }
        (Expr::Literal(Literal::Int(n)), Expr::Ident(v) | Expr::Resolved { name: v, .. })
            if v == var_name =>
        {
            Some((callee_name, false, *n))
        }
        _ => None,
    }
}

pub(super) fn detect_wrapper_sub_right_identity(
    law: &crate::ast::VerifyLaw,
    fn_name: &str,
) -> bool {
    if law.givens.len() != 1 || law.givens[0].type_name != "Int" {
        return false;
    }
    let g = &law.givens[0].name;
    matches_sub_right_identity_side(&law.lhs, &law.rhs, fn_name, g)
        || matches_sub_right_identity_side(&law.rhs, &law.lhs, fn_name, g)
}

/// Detect `sub(a, b) => -sub(b, a)` or the swapped arrangement.
/// Returns `Some(neg_on_rhs)` — `true` when the negation is on the
/// rhs (canonical direction); `false` when swapped (call on rhs,
/// negation on lhs). `None` when the shape doesn't fit.
pub(super) fn detect_wrapper_sub_anti_commutative(
    law: &crate::ast::VerifyLaw,
    fn_name: &str,
) -> Option<bool> {
    if law.givens.len() != 2 || law.givens.iter().any(|g| g.type_name != "Int") {
        return None;
    }
    let a = &law.givens[0].name;
    let b = &law.givens[1].name;
    if matches_binary_call(&law.lhs, fn_name, a, b)
        && matches_neg_binary_call(&law.rhs, fn_name, b, a)
    {
        return Some(true);
    }
    if matches_binary_call(&law.rhs, fn_name, a, b)
        && matches_neg_binary_call(&law.lhs, fn_name, b, a)
    {
        return Some(false);
    }
    None
}

pub(super) fn detect_wrapper_identity(
    law: &crate::ast::VerifyLaw,
    fn_name: &str,
    op: crate::ast::BinOp,
) -> bool {
    if law.givens.len() != 1 || law.givens[0].type_name != "Int" {
        return false;
    }
    let identity = match op {
        crate::ast::BinOp::Add => 0,
        crate::ast::BinOp::Mul => 1,
        _ => return false,
    };
    let g = &law.givens[0].name;
    matches_identity_side(&law.lhs, &law.rhs, fn_name, g, identity)
        || matches_identity_side(&law.rhs, &law.lhs, fn_name, g, identity)
}

// ── AST matchers — ported from `lean::law_auto::shared` ─────────
//
// Kept private to proof_lower to preserve layering (proof_lower
// must not reach into lean codegen). The shapes are backend-neutral
// — pure AST pattern matching — so the duplication is local-cost
// only. A future cleanup could consolidate these into a shared
// `codegen::ast_match` module.

pub(super) fn body_terminal_expr(body: &crate::ast::FnBody) -> Option<&Spanned<crate::ast::Expr>> {
    use crate::ast::Stmt;
    match body.stmts() {
        [Stmt::Expr(expr)] => Some(expr),
        _ => None,
    }
}

/// Fold the algebraic identities that survive a body-substitution
/// pass with a literal-int arg: `a + 0 == a`, `0 + a == a`,
/// `a - 0 == a`, `a * 1 == a`, `1 * a == a`, `a * 0 == 0`,
/// `0 * a == 0`. Recursive over BinOp / Neg / Attr / FnCall. Used
/// by `detect_spec_equivalence` so impl bodies like `n + 0` and
/// spec bodies like `n` are recognised as equivalent under arg
/// substitution. Matches the legacy `simp_normalized` shape.
pub(super) fn simplify_identity_expr(
    expr: &Spanned<crate::ast::Expr>,
) -> Spanned<crate::ast::Expr> {
    use crate::ast::{BinOp, Expr, Literal};
    let line = expr.line;
    let int_lit = |e: &Expr| -> Option<i64> {
        match e {
            Expr::Literal(Literal::Int(n)) => Some(*n),
            _ => None,
        }
    };
    let new_node = match &expr.node {
        Expr::BinOp(op, left, right) => {
            let left = simplify_identity_expr(left);
            let right = simplify_identity_expr(right);
            match op {
                BinOp::Add => {
                    if int_lit(&left.node) == Some(0) {
                        return right;
                    } else if int_lit(&right.node) == Some(0) {
                        return left;
                    } else {
                        Expr::BinOp(*op, Box::new(left), Box::new(right))
                    }
                }
                BinOp::Sub => {
                    if int_lit(&right.node) == Some(0) {
                        return left;
                    } else {
                        Expr::BinOp(*op, Box::new(left), Box::new(right))
                    }
                }
                BinOp::Mul => {
                    if int_lit(&left.node) == Some(0) || int_lit(&right.node) == Some(0) {
                        Expr::Literal(Literal::Int(0))
                    } else if int_lit(&left.node) == Some(1) {
                        return right;
                    } else if int_lit(&right.node) == Some(1) {
                        return left;
                    } else {
                        Expr::BinOp(*op, Box::new(left), Box::new(right))
                    }
                }
                _ => Expr::BinOp(*op, Box::new(left), Box::new(right)),
            }
        }
        Expr::Neg(inner) => Expr::Neg(Box::new(simplify_identity_expr(inner))),
        Expr::Attr(base, field) => {
            Expr::Attr(Box::new(simplify_identity_expr(base)), field.clone())
        }
        Expr::FnCall(callee, args) => Expr::FnCall(
            Box::new(simplify_identity_expr(callee)),
            args.iter().map(simplify_identity_expr).collect(),
        ),
        Expr::Match { subject, arms } => Expr::Match {
            subject: Box::new(simplify_identity_expr(subject)),
            arms: arms
                .iter()
                .map(|arm| crate::ast::MatchArm {
                    pattern: arm.pattern.clone(),
                    body: Box::new(simplify_identity_expr(&arm.body)),
                    binding_slots: arm.binding_slots.clone(),
                })
                .collect(),
        },
        other => other.clone(),
    };
    Spanned::new(new_node, line)
}

/// **syntax-discovery-only** (epic #170 Phase 7). Returns true iff
/// `expr` is a bare `Ident(name)` / `Resolved { name }` matching
/// the given name. Used by shape detectors to recognise "the
/// callsite mentions this binder" — no identity lookup, just
/// source-name shape.
pub(super) fn matches_ident_expr(expr: &Spanned<crate::ast::Expr>, name: &str) -> bool {
    use crate::ast::Expr;
    matches!(&expr.node, Expr::Ident(n) | Expr::Resolved { name: n, .. } if n == name)
}

/// **syntax-discovery-only** (epic #170 Phase 7). Compares the
/// callee's dotted source name against a target string for shape
/// recognition. EXACT MATCH ONLY — the previous suffix-match clause
/// (`name.rsplit('.').next() == Some(target)`) was an identity leak:
/// it accepted `Foo.helper` as a match for target `"helper"`. Bounded
/// today by the parser invariant (`vb.fn_name` is bare entry-only),
/// but the suffix clause stayed live as dead code that any future
/// module-scoped verify would silently exercise.
pub(super) fn callee_matches_name(expr: &Spanned<crate::ast::Expr>, target: &str) -> bool {
    let Some(name) = expr_to_dotted_name(&expr.node) else {
        return false;
    };
    name == target
}

pub(super) fn call2_args<'a>(
    expr: &'a Spanned<crate::ast::Expr>,
    fn_name: &str,
) -> Option<(&'a Spanned<crate::ast::Expr>, &'a Spanned<crate::ast::Expr>)> {
    use crate::ast::Expr;
    let Expr::FnCall(callee, args) = &expr.node else {
        return None;
    };
    if args.len() != 2 || !callee_matches_name(callee, fn_name) {
        return None;
    }
    Some((&args[0], &args[1]))
}

pub(super) fn matches_binary_call(
    expr: &Spanned<crate::ast::Expr>,
    fn_name: &str,
    a: &str,
    b: &str,
) -> bool {
    let Some((x, y)) = call2_args(expr, fn_name) else {
        return false;
    };
    matches_ident_expr(x, a) && matches_ident_expr(y, b)
}

pub(super) fn matches_assoc_nested(
    expr: &Spanned<crate::ast::Expr>,
    fn_name: &str,
    a: &str,
    b: &str,
    c: &str,
) -> bool {
    let Some((ab, z)) = call2_args(expr, fn_name) else {
        return false;
    };
    let Some((x, y)) = call2_args(ab, fn_name) else {
        return false;
    };
    matches_ident_expr(x, a) && matches_ident_expr(y, b) && matches_ident_expr(z, c)
}

pub(super) fn matches_assoc_flat(
    expr: &Spanned<crate::ast::Expr>,
    fn_name: &str,
    a: &str,
    b: &str,
    c: &str,
) -> bool {
    let Some((x, bc)) = call2_args(expr, fn_name) else {
        return false;
    };
    let Some((y, z)) = call2_args(bc, fn_name) else {
        return false;
    };
    matches_ident_expr(x, a) && matches_ident_expr(y, b) && matches_ident_expr(z, c)
}

pub(super) fn matches_sub_right_identity_side(
    call_side: &Spanned<crate::ast::Expr>,
    ident_side: &Spanned<crate::ast::Expr>,
    fn_name: &str,
    given_name: &str,
) -> bool {
    use crate::ast::{Expr, Literal};
    if !matches_ident_expr(ident_side, given_name) {
        return false;
    }
    let Some((x, y)) = call2_args(call_side, fn_name) else {
        return false;
    };
    matches_ident_expr(x, given_name)
        && matches!(&y.node, Expr::Literal(Literal::Int(n)) if *n == 0)
}

pub(super) fn matches_neg_binary_call(
    expr: &Spanned<crate::ast::Expr>,
    fn_name: &str,
    a: &str,
    b: &str,
) -> bool {
    use crate::ast::Expr;
    match &expr.node {
        Expr::Neg(inner) => matches_binary_call(inner, fn_name, a, b),
        _ => false,
    }
}

pub(super) fn matches_identity_side(
    call_side: &Spanned<crate::ast::Expr>,
    ident_side: &Spanned<crate::ast::Expr>,
    fn_name: &str,
    given_name: &str,
    identity: i64,
) -> bool {
    use crate::ast::{Expr, Literal};
    if !matches_ident_expr(ident_side, given_name) {
        return false;
    }
    let Some((x, y)) = call2_args(call_side, fn_name) else {
        return false;
    };
    let is_int_lit = |e: &Spanned<Expr>, n: i64| -> bool {
        matches!(&e.node, Expr::Literal(Literal::Int(m)) if *m == n)
    };
    (matches_ident_expr(x, given_name) && is_int_lit(y, identity))
        || (is_int_lit(x, identity) && matches_ident_expr(y, given_name))
}