Enum RecursionPlan 

pub enum RecursionPlan {
    IntCountdown {
        param_index: usize,
    },
    IntCountdownGuarded {
        param_index: usize,
        base_arm_literal: i64,
        base_arm_body: Spanned<Expr>,
        wildcard_arm_body: Spanned<Expr>,
        precondition: Vec<Spanned<Expr>>,
    },
    IntAscending {
        param_index: usize,
        bound: Spanned<Expr>,
    },
    IntFloorDivCountdown {
        param_index: usize,
        divisor: i64,
        helper_fn: Option<String>,
    },
    LinearRecurrence2,
    ListStructural {
        param_index: usize,
    },
    SizeOfStructural,
    StringPosAdvance,
    MutualIntCountdown,
    MutualStringPosAdvance {
        rank: usize,
    },
    MutualSizeOfRanked {
        rank: usize,
    },
}

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

Eq is deliberately omitted — IntAscending holds an AST expression which only implements PartialEq (float literals inside it are partially ordered). PartialEq still works for the uses this enum sees (pattern matching, matches!, equality via .eq).

Variants

IntCountdown

Single-fn recursion where an Int parameter decreases by 1. The wrapper supplies n.natAbs + 1 fuel so the helper terminates.

Fields

param_index: usize

IntCountdownGuarded

Same shape as IntCountdown but body is match p { 0 -> BASE; _ -> rec(p-1, ...) } and the fn is closed-world: every external callsite either passes a non-negative literal or sits in a guard branch that proves p ≥ 0. Proof backends emit a native def with an injected p ≥ 0 precondition plus a wrapper handling the p < 0 case from the source’s 0 arm, skipping fuel entirely so Lean can decide / unfold for symbolic proofs. Carries both arm bodies so the Lean emitter can switch the elaborated shape to if h_zero : p = 0 then BASE else REC — needed because Lean’s match elaborator does not expose the case-split hypothesis to omega for the recursive callsite’s p - 1 ≥ 0 discharge.

Fields

param_index: usize

base_arm_literal: i64

Literal int from the body’s literal-match arm — the value the if h_zero : p = L then base else rec(p-1, ...) aux splits on.

base_arm_body: Spanned<Expr>

wildcard_arm_body: Spanned<Expr>

precondition: Vec<Spanned<Expr>>

Path-constraint chain extracted from the single external caller’s surrounding match (Bool) { true/false -> CALL ... } (and if/then/else) guards. Already normalised to positive form by flipping the comparison BinOp on false-arm guards (Lt ↔ Gte, Gt ↔ Lte, Eq ↔ Neq), so every clause is a plain Aver Bool expression. Substituted into callee’s variable space (caller’s arg-binding renamed to callee’s param name). Conjunction of all clauses is the aux’s precondition.

Empty means “no single external caller in ctx”: the Lean emitter falls back to (h_dom : p ≥ 0) so a free-standing fibTR-shape (no caller in the proof artifact) keeps the legacy precondition. Same Spanned<Expr>-as-predicate representation as opaque types’ smart-constructor predicate (refinement_info_for) and verify-law when clauses — the three sources differ only in where the predicate comes from.

IntAscending

Single-fn recursion where an Int param increases by 1 up to a bound. The bound is kept as an Aver AST expression so each backend renders it in its own idiom; the wrapper supplies (bound - n).natAbs + 1 fuel.

Fields

param_index: usize

bound: Spanned<Expr>

IntFloorDivCountdown

Single-fn recursion where an Int parameter shrinks by a literal-divisor floor division at every self-call — Result.withDefault(Int.div(p, k), d) with literal k >= 2, either inlined at the call site or through a unary wrapper fn (half(p)) whose body is exactly that expression. Validated, never guessed: the classifier additionally proves that the guard chain enclosing every self-call site implies p >= 1 (so p / k < p and p.toNat strictly decreases). Backends emit a native well-founded def — Lean termination_by p.toNat (kernel re-checks the measure), Dafny decreases if p >= 0 then p else 0 with no synthesized requires.

Fields

param_index: usize

divisor: i64

The literal divisor (>= 2).

helper_fn: Option<String>

Some(name) when the shrink goes through a unary wrapper fn; None for the inlined form.

LinearRecurrence2

Affine second-order recurrence like fib(n) = fib(n-1) + fib(n-2) with 0 / 1 bases and an n < 0 guard. Emitted through a private Nat helper (pair-state), not a fuel helper.

ListStructural

Single-fn structural recursion on a List<_> parameter; proof backends emit as structural recursion directly (no fuel).

Fields

param_index: usize

SizeOfStructural

Single-fn structural recursion on a recursive user ADT; proof backends emit through a sizeOf-guarded fuel helper.

StringPosAdvance

Single-fn recursion where the first String is preserved and the second Int position parameter strictly advances (pos + k, k ≥ 1). Wrapper fuel is derived from s.length - pos.

MutualIntCountdown

Mutual recursion SCC where the first Int parameter decreases by 1 across every inter-fn call.

MutualStringPosAdvance

Mutual recursion SCC where the first String is preserved and the second Int either advances or stays the same across rank-decreasing edges.

Fields

rank: usize

MutualSizeOfRanked

Generic mutual recursion SCC using sizeOf on structural parameters plus rank for same-measure edges.

Fields

rank: usize

Trait Implementations

impl Clone for RecursionPlan

fn clone(&self) -> RecursionPlan

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for RecursionPlan

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for RecursionPlan

fn eq(&self, other: &RecursionPlan) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for RecursionPlan