recurrence

Documentation

Overview

Package recurrence solves the standard recurrence families of self-recursive functions. A bound is returned only when the recursion's measure provably strictly decreases toward a base — a wrong answer here is a wrong bound on (possibly non-terminating) code, the highest-severity bug class.

Index

• func IsSelfRecursive(fn *ssa.Function) bool
• func MutualPartner(fn *ssa.Function) (*ssa.Function, bool)
• func ProvablyExponential(fn *ssa.Function) (a int, ok bool)
• func Solve(fn *ssa.Function, model engine.CostModel) (work bound.Bound, depth bound.Bound, ok bool)
• func SolvePair(fn, partner *ssa.Function, model engine.CostModel) (bound.Bound, bound.Bound, bool)

Functions

func IsSelfRecursive

func IsSelfRecursive(fn *ssa.Function) bool

IsSelfRecursive reports whether fn calls itself directly (a static call whose callee is fn). Mutual recursion is out of scope and reads as false.

func MutualPartner

func MutualPartner(fn *ssa.Function) (*ssa.Function, bool)

MutualPartner returns the unique two-cycle partner of fn, if any: the same- package function g such that fn statically calls g, g statically calls fn, neither is self-recursive, and no other function also forms a two-cycle with fn. A second distinct partner makes the SCC larger than two, which is out of scope, so the result is (nil, false).

func ProvablyExponential

func ProvablyExponential(fn *ssa.Function) (a int, ok bool)

ProvablyExponential reports whether fn is a directly self-recursive function whose recurrence is provably exponential: Θ(aⁿ) for branching factor a ≥ 2. This is the positive smell claim SM8 makes on unannotated code — the exact family the solver *rejects for bounding* in solveSubtractive (a ≥ 2 subtractive). It must be at least as strict as the solver's rejection: everything the extractor cannot positively classify returns false.

ok only when all of:

• fn is directly self-recursive (selfCalls non-empty);
• no self-call sits inside an enclosing size loop (constant multiplicity);
• a measure parameter exists whose every self-call steps subtractively (stepsFor returns all stepSub, at least one strict step);
• the termination guard holds (terminates) — a proved base, so the claim is on terminating code, not a runaway;
• the branching factor (selfCallMult) is ≥ 2 (a=1 is linear, not exponential).

a is the branching factor (e.g. naive Fibonacci → a=2). Everything else — divisive steps (binary search solves), mutual recursion, unguarded recursion, a=1 countdowns — returns false.

func Solve

func Solve(fn *ssa.Function, model engine.CostModel) (work bound.Bound, depth bound.Bound, ok bool)

Solve returns the solved asymptotic time bound (work) and the recursion-tree height (depth) of a self-recursive function in its own canonical size variables, or ok=false when no recurrence family applies (the caller falls back to ⊤). Depth is the true peak stack the space slice needs; work is the time bound every existing caller consumes.

func SolvePair

func SolvePair(fn, partner *ssa.Function, model engine.CostModel) (bound.Bound, bound.Bound, bool)

SolvePair solves the two-function cycle fn↔partner as a virtual self-recurrence in fn's measure vocabulary, routing the composed recurrence through the shipped solvers (solveWork/depthOf) — no new solver math. ok=false (⊤) when extraction fails a soundness precondition or the composed recurrence is out of the solvers' representable families (e.g. a≥2 subtractive).