Module recursion 

Shared proof-mode recursion analysis.

Classifies each recursive pure fn into a RecursionPlan that tells the proof backends (Lean, Dafny) how to emit a fuel-guarded helper plus a wrapper with an appropriate fuel metric. The same classifier feeds both backends so supported shapes stay consistent.

Emission is backend-specific (syntax, termination-proof mechanism, default-value for fuel exhaustion), but the recognition pass and the AST transform that rewrites recursive calls into helper calls are shared.

Re-exports

pub use detect::analyze_plans_in_scope;

pub use crate::codegen::common::substitute_ident_in_expr;

Modules

detect

Proof-mode recursion classifier.

Structs

ProofModeIssue

Classifier-side diagnostic: a recursive fn whose shape falls outside every supported pattern. proof_lower::populate_fn_ contracts translates these into ProofIR.unclassified_fns — consumers should read ctx.proof_ir.unclassified_fns (typed Vec<UnclassifiedFn>) instead of reaching for this type.

Enums

RecursionPlan

Classification for a single recursive fn (or a whole mutual-recursion SCC, in which case every fn in the SCC gets its own plan from the same family).

Constants

OMEGA_PROOF_SENTINEL

Sentinel identifier injected as an extra synthetic argument at every recursive callsite inside an IntCountdownGuarded body. Lean’s expr emitter recognises this name and renders it as (by omega); Dafny’s codegen never sees it because Dafny discharges preconditions via auto-inference at the existing fn-def emit path.

Functions

expr_references_ident

True iff expr (recursively) mentions name as an Ident/ Resolved reference. Used by the caller-guard extractor to filter out enclosing predicates that don’t constrain the variable passed at the countdown-param position — those predicates name caller locals that aren’t in scope inside the callee.

flip_comparison_binop

Flip a comparison BinOp to its logical negation so a caller’s match (a OP b) { false -> ... } arm normalises into a positive predicate. Returns None for non-comparison operators (Add, Sub, etc.) — those can’t legally land as a match … { Bool -> ... } subject anyway. Used by the issue-84 caller-guard extractor so every collected predicate is the same Spanned<Expr> shape opaque types and verify when already use, avoiding a parallel (expr, negated) representation.

fuel_helper_name

Canonical suffix for a fuel-guarded helper fn. Deliberately contains only lowercase ASCII + underscores so both Lean and Dafny accept it as an identifier without renaming.

native_aux_name

Suffix for the native-emit auxiliary fn that carries the explicit precondition parameter. Mirrors fuel_helper_name’s ASCII-only shape so Lean accepts it verbatim.

rewrite_native_guarded_calls_body

Body-level wrapper around rewrite_native_guarded_calls_expr.

rewrite_native_guarded_calls_expr

Walk expr and rewrite every recursive call to fn_name into a call to aux_name carrying an extra OMEGA_PROOF_SENTINEL ident at the end of the argument list. Used by the proof-mode IntCountdownGuarded lowering — the synthetic argument lets Lean discharge the precondition at every recursive site without touching the original Aver source.

rewrite_native_guarded_calls_resolved_expr

ResolvedExpr mirror of rewrite_native_guarded_calls_expr. The proof-mode IntCountdownGuarded shape stores the rewritten arms on ProofIR (now resolved), so the rewriter that lifts fn(args) to aux_name(args, OMEGA_PROOF_SENTINEL) works in resolved space too.

rewrite_recursive_calls_body

Body-level wrapper around rewrite_recursive_calls_expr.

rewrite_recursive_calls_expr

AST transform: walk expr and replace every recursive call to a fn in targets with fn__fuel(fuel_var, …args). Inter-fn mutual calls in the same SCC are rewritten identically (the fuel parameter is threaded through the whole group).