Function analyze_plans_in_scope 

pub fn analyze_plans_in_scope(
    inputs: &ProofLowerInputs<'_>,
    scope: Option<&str>,
    global_view: bool,
) -> (HashMap<String, RecursionPlan>, Vec<ProofModeIssue>)

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.

Consumers should not call this directly. After Step 18 / 20 the only caller is proof_lower::populate_fn_contracts, which translates the output into ProofIR.fn_contracts and ProofIR.unclassified_fns. Backends read those fields instead. The fn stays pub only because the diff test (tests/proof_ir_diff.rs) cross-checks ProofIR against the legacy classifier output — that test is itself slated for rationalisation once the migration is fully bedded down. Scope-aware classifier. scope = None runs against entry only, Some(prefix) against one dep module. Aver’s module DAG invariant rules out cross-module recursion SCCs, so per-scope classification is the canonical view and avoids two same-bare-name fns from different modules colliding in the SCC analyser’s HashMap<name, _>. The global_view flag keeps the legacy “chain all fns, classify globally” behaviour for tests/proof_ir_diff.rs cross-check tests; production callers always pass global_view = false and walk scopes themselves.