ADR-0020: B0 Structural Node Identity and Intraprocedural Judgment

Status: accepted
Date: 2026-07-25

Context

B0-A binds analysis to a verified P1V0 request. B0-B must identify every analyzed Core term, rvalue, and operand independently of Rust layout, source names, formatting, or allocation addresses. It must also establish the first conservative data/control dependency judgment without prematurely introducing the interprocedural fixed point reserved for B0-C.

Options considered

Option	Benefit	Cost
Surface source span	Familiar diagnostics	Core may be generated and has no authoritative Surface span
Rust address or traversal ordinal	Cheap	Unstable under allocation and traversal changes
Hash each subtree	Content-addressed	Identical subtrees collide without parent context; expensive to inspect
`FunctionId + canonical structural path`	Stable, local, independently reconstructible	Requires a versioned grammar tag table

Decision

Use a node identity consisting of:

FunctionId + ordered structural-path segments
segment = U8 field tag + U32 big-endian index

The function-body term has an empty path. Non-sequence fields use index 0. Tags in Node Identity Encoding v1 are:

Tag	Field
0	`LetValue`
1	`LetNext`
2	`IfCondition`
3	`IfThen`
4	`IfElse`
5	`CaseScrutinee`
6	`CaseArm`
7	`ReturnOperand`
8	`UseOperand`
9	`TupleElement`
10	`ProjectTuple`
11	`ConstructField`
12	`PrimitiveArgument`
13	`CallArgument`
14	`TailCallArgument`

Canonical node bytes are domain-separated. Judgments are ordered lexicographically by node identity, which places the root before descendants and grammar fields in tag/index order.

B0-B analyzes only the validated entry function:

literals are Static;
locals use the entry, pattern, or let environment;
rvalues join their operand dependencies;
dynamic if/case control contaminates both branch computations;
case payload bindings conservatively inherit the scrutinee binding time;
checked integer operations and array indexing are not eligible for default static execution because they can produce typed errors;
dynamic nodes and any node containing denied work are Denied;
direct and tail calls fail closed as UnsupportedInterprocedural;
node-budget exhaustion returns no analysis result.

B0-B reports dependency and eligibility but executes no Core operation.

Rationale

An independent verifier can rebuild paths from canonical Core alone.
Empty-root plus field tags avoids redundant function-body metadata.
Lexicographic order is deterministic without relying on insertion order.
Rejecting calls keeps the first judgment small and prevents an unreviewed approximation from becoming the B0-C recursion policy.

Trade-offs

Tag changes require a new domain/version or explicit migration.
One binding time per sum value loses field-sensitive precision.
Dynamic control contamination is conservative even when both branches return equivalent static values.
Entry-only analysis ignores unreachable helper functions until B0-C.
Checked operations remain non-executable at specialization time even when their operands are static; a later proven typed-error policy may refine this.

Consequences

Positive: B0-C receives stable nodes and a tested intraprocedural transfer function.

Negative: B0-B cannot analyze the recursive lighthouse interpreter yet.

Mitigation: CallArgument and TailCallArgument tags are reserved now, while their semantics remain fail closed until B0-C.

Revisit trigger

Add field-sensitive partially static domains only when P1 evidence shows that whole-value conservatism leaves material interpreter structure unresolved.