Module detect 

Proof-mode recursion classifier.

Backend-neutral pattern matching over the Aver AST that decides, for each recursive pure fn (or mutual-recursion SCC), which RecursionPlan variant applies — or emits a ProofModeIssue when the shape falls outside the supported set.

Lean and Dafny consume the same plans through [crate::codegen::recursion::analyze_plans]; a couple of helpers that depend on AST queries tied to Lean’s toplevel (pure-fn predicate, recursive-type-def predicate, type-def name) still live in crate::codegen::lean and are re-used here through pub(crate) exports. That could move to a neutral AST helper module in a later pass.

Functions

analyze_plans_in_scope

Classify every recursive pure fn in inputs. The returned map assigns each supported function a RecursionPlan; anything that falls outside the recognised shapes becomes a ProofModeIssue.

scc_has_growing_accumulator

True iff some intra-SCC call passes a non-trivially-shrinking expression into a callee’s sizeOf parameter — tail-recursive accumulator patterns like [x] + acc / List.prepend(x, acc) / acc + [x], plus arbitrary FnCall(...) results we can’t statically prove shrink. These all fail termination-by-measure even though fuel encoding handles them fine; backends fall back to fuel for those SCCs.

sizeof_measure_param_indices

SizeOf-measure param indices for a fn — every non-scalar param position contributes a term to the structural measure. Matches the picks made for the Lean termination_by clause and the Dafny native decreases tuple so the same params drive measure inference on both backends.