ADR-0021: B0 Deterministic Interprocedural Fixed Point

Status: accepted
Date: 2026-07-25

Context

B0-B deliberately rejects direct and tail calls. B0-C must propagate binding times through the recursive P1V0 call graph without making evaluation order, map iteration, host addresses, or an unbounded recursion strategy part of the result. It must also preserve the fail-closed resource contract established by B0-A.

A function can become dynamic through both its arguments and the control context of its call site. The latter is required even for a zero-argument constant function called beneath a dynamic branch.

Options considered

Decision

Use one context-insensitive summary per function:

reachable
parameter binding times
incoming control binding time
result binding time
static-evaluation eligibility

Static, EligiblePure, and unreachable form the initial bottom. The entry is seeded reachable with the request manifest and static incoming control.

Each synchronous round:

1. snapshots the complete summary map;
2. analyzes functions that were reachable in that snapshot in increasing FunctionId order;
3. reads callee results only from the snapshot;
4. joins argument binding times and caller control into next-round callee summaries;
5. joins analyzed results and eligibility into the next summary map.

Newly reachable functions are therefore analyzed in the following round. Analysis terminates only after a round leaves the summary map unchanged. Judgments from that stable round are the returned judgments.

Direct and tail calls use the same transfer:

• each argument contributes to the matching callee parameter;
• caller control contributes to callee incoming control;
• the call result is the snapshotted callee result joined with caller control;
• default static execution is eligible only when the result, every argument, and the callee summary are eligible.

All joins are monotone. Denied is absorbing for static-evaluation eligibility. A missing callee or an arity mismatch fails closed even though the verified Core boundary should already reject either condition.

Resource use is cumulative over every analyzed round:

• nodes counts every visited term, rvalue, and operand;
• call_edges counts every visited direct or tail call site;
• fixpoint_iterations counts every started synchronous round.

The relevant budget is checked before consuming each unit. Exhaustion returns an error and no partial analysis.

Rationale

• Synchronous snapshots make the least fixed point independent of incidental traversal effects.
• Increasing FunctionId order is easy for an independent verifier to reconstruct.
• Incoming control closes the zero-argument dynamic-control hole.
• Cumulative accounting binds the request to actual analysis work instead of merely bounding final output size.
• A single summary per function is the smallest useful interprocedural domain for the first P1 lighthouse.

Trade-offs

• A function called from static and dynamic contexts is summarized as dynamic, which can lose specialization opportunities.
• Synchronous rounds repeat work that a worklist could avoid.
• Budget usage can increase after harmless call-graph changes even when the final binding-time answer is unchanged.
• Returned judgments describe the stable context-insensitive summary, not individual call contexts.

Consequences

Positive: B0 can now analyze finite recursive P1V0 call graphs with a deterministic, bounded, inspectable least fixed point.

Negative: B0-C is analysis evidence only. It does not authorize static execution, residualization, P1 success, or Nauxogenesis claims.

Mitigation: B0-D must canonically encode the request, function summaries, judgments, and budget usage and verify them independently before the residualizer is opened.

Revisit trigger

Introduce a versioned context-sensitive domain only if P1 lighthouse evidence shows that context merging leaves material interpreter structure dynamic.