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;

Modules

detect

Proof-mode recursion classifier.

Structs

ProofModeIssue

A diagnostic surfaced when a recursive fn falls outside the supported patterns. Proof backends translate this into a warning and emit the fn through a partial/axiom fallback (or skip it entirely).

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).

Functions

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.

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).