Enum RecursionContract 

pub enum RecursionContract {
    Fuel {
        fuel_metric: FuelMetric,
    },
    LinearRecurrence2,
    Native {
        precondition: Vec<Predicate>,
        measure: Measure,
        preservation: PreservationProof,
        decrease: DecreaseProof,
        body: NativeIntCountdownBody,
    },
    WellFoundedToNat {
        param: String,
        floor_div: Option<FloorDivShrink>,
    },
}

Recursion-shape decision. Each variant carries everything its emit needs AND the side-conditions the lowerer proved to choose it. The variants intentionally cannot be constructed without their side-conditions — backends cannot render Native without the lowerer having proved preservation + decrease.

Variants

Fuel

Fuel-encoded fallback. No side-conditions to prove; works for any shape the classifier accepted as recursive.

Fields

fuel_metric: FuelMetric

Symbolic measure feeding the wrapper (natAbs n + 1, |xs| + 1, etc.). Backends translate per target.

LinearRecurrence2

Affine second-order linear recurrence on Int, shape f(n) = a*f(n-1) + b*f(n-2) with literal 0/1 base cases and an n < 0 guard. Lowered to a private Nat pair-state worker (Lean / Dafny both emit native structural recursion on the Nat counter, no fuel). The lowerer doesn’t carry the shape coefficients yet — backends still pattern-match the fn body via lean::recurrence::detect_second_order_int_ linear_recurrence. Step N+1 could materialise them here.

Native

Native recursion with explicit precondition. Lowerer proved both preservation (rec args stay in domain) and decrease (measure strictly drops) before constructing this variant. Currently specialised to the IntCountdown-literal-zero shape (match p { 0 -> BASE; _ -> rec(p-1, ...) }); other native- recursion shapes (e.g. linear recurrence on a pair-state worker) will land as additional RecursionContract variants.

Fields

precondition: Vec<Predicate>

Conjunction of precondition clauses, kept as a vector so backends can render one requires per clause (Dafny) or fold into a single && chain (Lean). Empty means “no caller-derived precondition” — the backend synthesises a fibTR-style default (param ≥ 0) at emit time.

measure: Measure

Symbolic measure (e.g. natAbs(n)). Backends render per target language (Int.natAbs n on Lean, n with a requires n >= 0 clause on Dafny).

preservation: PreservationProof

Side-condition tag: lowerer attests the recursive args preserve the precondition. Empty enum payload — its existence in the type is the proof, not its content.

decrease: DecreaseProof

Same for the decreasing measure.

body: NativeIntCountdownBody

Body decomposition for the IntCountdown-literal-zero shape: the literal int that selects the base arm, the base arm’s body, and the wildcard arm’s body. Carried so backends can render the if h : p = <lit> then base else rec(p-1, ...) switch without re-walking the source AST. The literal is always 0 today — the IntCountdownLiteralZero preservation marker attests it; carrying the value as data keeps the IR shape forward-compatible with future preservation proofs that admit other literals.

WellFoundedToNat

Well-founded native def on param.toNat — graduates a fn out of the fuel/partial encoding so it stays kernel-transparent (Lean: termination_by param.toNat + a decreasing_by the kernel re-checks; Dafny: decreases if param >= 0 then param else 0 with NO synthesized requires, so total callers stay wellformed). Two validated sources:

• floor_div: Some(..) — every self-call shrinks param by a literal-divisor floor division (Result.withDefault(Int.div(p, k), d) with literal k >= 2, possibly through a unary wrapper fn), and the classifier verified the guard chain enclosing every self-call site implies p >= 1 — so p / k < p and the measure strictly drops. Never guessed: a fn whose guards don’t justify the shrink keeps its prior (partial/opaque) emission.
• floor_div: None — guard-protected subtractive countdown (p - k, literal k >= 1, guards imply p >= 1), graduated out of fuel on demand by the floor-division window law family, whose proof templates need the fn’s defining equations and functional-induction principle.

Fields

param: String

The decreasing Int parameter (source name).

floor_div: Option<FloorDivShrink>

Some for the floor-division shrink; None for the guarded subtractive countdown.

Trait Implementations

impl Clone for RecursionContract

fn clone(&self) -> RecursionContract

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for RecursionContract

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

Formats the value using the given formatter.