D13 (b2): dependency-demand census — demand-census verb and //gunbc/instruments:dependency-demand-census

[gunbai-bot]

Step (b2) of D13 (node adhoc-62cc5494-886). Stacked on #12985 (b1, the reducer).

What it adds

• v2.compiler.dependency_demand_census:
  • The census-only strip. Each fn's uses clause shell is replaced by grammar_empty_node, which is what the parser leaves when the clause is absent. The authored rows are recorded from the same parse.
  • The fact reader over resolved trees. Each declaration's callees are its declaration references (a declared over-approximation). A path under a declared resource is demand for that resource. An Arrow with no body is an operation, and its requirement is read from its requires edge.
  • Verdicts scoped to the audited vocabulary (Network): Equal / Mismatch / Undecided-by-cause / Unobserved-by-reason. Filesystem and Clock rows are out of vocabulary and never a Mismatch.
  • The report lines, including a count of functions that agree on Filesystem, to size the next audit.
• v2.compiler.compile native_demand_census_report / _output:
  • It folds the whole ingest phase by phase (tokenize, parse, strip, normalize), then absorbs through the same native_test_context_absorb the production fold uses.
  • It resolves every module and reduces with dependency_demand_of over the whole closure.
  • The context never leaves the route: the result is rows, never a tree, so nothing can reach infer, eval or emit.
• The demand-census command word:
  • in NativeDriverVerb and its parse;
  • the rendered main arm in v1.compiler.emit_rust, with the stage0 mirror regenerated;
  • the producer DependencyDemandCensusProducer, the label //gunbc/instruments:dependency-demand-census, the host arm, and a seed-growth row.
• It is on no CI lane, per the lane ruling. (b3) executes it at its own head as required evidence.

Controls (floor claims over a supplied 4-module ingest, real route):

• Count conservation: 6 uses fns produce 6 rows, emitted by a different fold than the one that counted them.
• One claim per verdict: equal (direct and transitive), mismatch RED, opaque-undecided RED, and alias-used-is-never-a-restatement RED.
• Deletable rows: 2 (Network only); Filesystem-agreeing count: 1.
• Production control: native_test_context_from_ingest over the SAME ingest still refuses both uses files with body_lowering_reason_uses_clause_unmodeled.

Numbers: the executed census numbers will be reported once the instrument runs on this head.

Boundaries:

• v2.compiler.effect_demand is a different concept: host primitive realization keyed by PrimitiveIdentity. No fork.
• No carrier is built for the authored row (operator D13).

🤖 Generated with Claude Code

[gunbai-bot]

Review 74228, all three findings addressed in the head above:

1. Arrow predicate. demand_census_is_arrow is deleted. An operation is now v2.compiler.eval eval_node_is_arrow plus v2.std.node_query find_arrow_body_child refusing (no body).
2. Counts by variant. Counts are a DemandCensusTally built by matching verdict and cause variants. The words are print-only.
3. No spelled vocabulary. Resources are no longer dotted strings. The audited vocabulary is derived: the set of resources declared in operations' requires edges, read off the resolved tree. Out-of-vocabulary resources are reported per resource ([demand-census-out-of-vocabulary] resource=… rows=… agreeing_functions=…), which replaces the Filesystem-specific count.

Also in this push, from the floor's first real run of these claims:

• Containment rule. The fact walk now follows symbol_index_fill's containment rule: it unwraps the spine at every Conj and descends parse-projection edges without extending the path. Before, every fn read as function_not_declared.
• Production control cost. The control now reads one source through the same front end v2.test.claim.parse.uses_clause uses, as a warm nullary producer. The old version cost 818k eval steps against the 72k new-witness budget.

— sent from sleek-boar-665

[briansrls]

HOLD at exact head cc2af669e5c5af29ac42dd31fbf6351c7b8298c3.

The census-only strip, rows-only return boundary, production-lowering control, resolved authored-type reading, audited-vocabulary derivation, and whole-closure reducer integration otherwise look coherent. Four blockers remain before this can be the evidence b3 consumes.

P1 — the operator-approved fleet route cannot select this instrument

#12998's closed choice is authored by instrument_dispatch_labels(), which currently contains only //gunbc/instruments:dag-emit-real-grammar-round-trips. This PR adds dependency-demand-census to gunbc.instrument_targets, but it changes neither gunbc.instrument_dispatch_workflow nor the generated workflow YAML. Roster membership is necessary but does not add an option to the dispatch choice.

After #12998 lands, merge it here, add dependency_demand_census_label() to instrument_dispatch_labels(), regenerate the workflow, and add a control that the generated choice contains the exact census label. Until then, the route the operator selected is not reachable at this head.

P1 — count conservation can be true while a uses-bearing file is completely missing

In native_demand_census_read, a tokenize/parse rejection is absorbed while both authored and file_refused remain unchanged. Authored functions are recorded only after parse succeeds. Later, uses_functions is computed solely from those two lists, and demand_census_conserved compares that observed count with emitted rows.

Therefore a malformed file containing a uses function can disappear from both sides of the equality: file_refusals increases, but conservation remains true and native_demand_census_exit still returns 0. That is not one row per uses function; it is one row per uses function the route got far enough to see.

Make pre-authorship front-end refusal a typed incomplete-population/no-observation state that b3 cannot consume—most simply, a report with any such refusal exits 2—or carry an independently complete population authority. Add a malformed uses-bearing file control whose census cannot hold.

P1 — the real route can never produce FunctionValueCalled

Every FunctionFact built by demand_fact_declaration hard-codes calls_function_value: false. The reducer and report retain FunctionValueCalled, but no resolved-tree fact reader can set it, so that undecided cause is dead on the production census route.

A function that both reaches a known Network operation and calls a function-valued parameter can consequently read CensusEqual instead of undecided: the known operation supplies Network while the dynamic call is invisible. Inspect call positions and set the flag whenever the callee is not a statically resolved declaration. Add a real-route control in which the direct Network call would otherwise mask the missing function-value cause.

P1 — OutOfVocabulary is prose/aggregation, not a typed row verdict

DemandCensusVerdict has only Equal, Mismatch, Undecided and Unobserved. demand_census_verdict filters authored and derived sets to the audited vocabulary before comparison, so the Filesystem control intentionally receives CensusEqual; its out-of-vocabulary status exists only in a separate aggregate report line/count.

That is unsafe for the declared b3 interface: the module comment says b3 deletes a row where the census reads Equal, but the same typed arm currently covers both deletable Network rows and non-deletable Filesystem rows. demand_census_deletable_rows is only a count and identifies no source row.

Carry a per-authored-row standing—or a typed list of exact deletable row identities—that distinguishes InVocabularyEqual, mismatch and OutOfVocabulary by construction. Include a mixed Network + Filesystem function so b3 cannot accidentally treat a function-level Equal as permission to delete both rows.

Exact-head floor, generated, emit-build and witnesses are green; this hold is semantic and integration-related, not CI-related. No direct merge or check bypass.

[briansrls]

HOLD at exact head cebd330392fc52d0d9ff51352b6b244a89dc6874.

Three of the four P1s from review 5396343031 are resolved:

• the generated fleet dispatcher now offers the exact dependency-demand census label and has a generated-choice control;
• a tokenize/parse refusal before authored rows are readable increments unreadable_files, makes the census exit 2, and has a malformed uses-bearing-file discriminator;
• each authored row now carries a typed standing, and DeletableUsesRow { function, resource } identifies only in-vocabulary rows of Equal functions; the mixed Network/Filesystem control prevents function-level Equal from licensing both rows.

Remaining P1 — a named function-valued parameter is still silently omitted

demand_fact_is_value_call sets the flag only when both:

1. eval_transform_has_callee_reference(node) is true; and
2. the first child is a lexical_reference_label_optional.

That reaches the new let g = t.app.restates; g(...) control, because a let-bound name is lexical. It does not reach a call through a named function parameter.

The resolver's carrier partition is explicit: a named fn's parameter is minted as parameter_reference_node keyed by <fn path>.<label>; lexical references are for lets, match arms, and lambdas. The evaluator likewise tests parameter_reference_path_optional separately, while eval_node_is_callee_reference admits only an Arrow, an Atom, or a lexical reference. Therefore a callee such as g in:

fn via_param(g: fn(Bool) -> Bool, p: Bool) -> Bool uses net: Network {
  let r = t.http.H.Get()
  g(p: p)
}

is a parameter reference. eval_transform_has_callee_reference returns false, the census never sets calls_function_value, and the direct Network call can still make this function read Equal. That is the exact masked-function-value case the earlier hold named; the current control substitutes a different carrier.

The comment in dependency_demand_census.dag also says a lexical reference names a "local or parameter", which disagrees with the parameter-reference authority and its executing route claims.

Please classify a parameter reference in callee position as FunctionValueCalled—either by extending the shared call-head predicate coherently or by handling parameter_reference_path_optional at the census call boundary—and add the direct-Network-plus-function-valued-parameter real-route control. Keep the existing lexical control; it proves a distinct dynamic-call inhabitant.

Exact-head floor, generated, emit-build, and witnesses are green. This is the only remaining finding; the hold is semantic and no direct merge or check bypass is authorized.

[briansrls]

APPROVE for merge-queue landing at exact head 9259ca23f08eaec7752136f91fbe9195d45f8048.

No findings. This supersedes my CHANGES_REQUESTED review 5398216986 at cebd330392fc52d0d9ff51352b6b244a89dc6874.

The remaining P1 is resolved:

• The existing lexical-reference inhabitant remains governed by eval_transform_has_callee_reference plus lexical_reference_label_optional.
• A named function parameter is handled as its distinct resolver carrier: only a Transform whose first edge is Positional and whose target satisfies parameter_reference_path_optional is classified as the additional function-value call. The exhaustive Behavior match prevents this from becoming a wildcard over every computation node.
• The real-route via_param fixture directly calls t.http.H.Get (which would otherwise derive Network and make the row Equal) and also calls its function-valued parameter g. The assertion requires CensusUndecided { FunctionValueCalled { function: t.valued.via_param } }, so the direct Network call cannot mask a missed dynamic call.
• The prior let-bound lexical control remains, and the inaccurate “local or parameter” comment is corrected.

The authored semantic fix is the two-file commit 8034225e60b57d66401cec21a7069f15c38c4cf2. The later main merges preserve it; the current PR diff contains no docs/design-rung-drops.md divergence, and the seed-growth conflict resolves as the union (the census import/roster row is added without deleting main's rows).

Exact-head generated, floor, emit-build, and witnesses checks all pass.

Non-blocking documentation note: the PR body still describes the earlier six-row fixture and earlier deletable/out-of-vocabulary counts; the current controlled fixture is nine uses functions, three deletable Network rows, and two Filesystem-agreeing functions.

Merge-queue landing only. The composed merge_group candidate must pass against then-current main; no direct merge or check bypass.

[briansrls]

APPROVE for merge-queue landing at exact head 402260f45fd708d4dae9028ff84ce4292192f177.

No findings. This rebinds my approval at 9259ca23f08eaec7752136f91fbe9195d45f8048.

I reviewed only the merge delta:

• the head is one merge commit whose parents are the approved head and main at 41de9a54a1c066f21242fd3b67265f5120d48a0e;
• src/v2/compiler/dependency_demand_census.dag and src/v2/test/claim/compiler/dependency_demand_census_test.dag retain exactly the approved blobs (66b1951c47dca2b0eb4e692e5180d4643a885082 and 8c1a567d4c9e4b0aa1f780cd3442bd971a3ebf7e);
• the approved-to-head delta contains no native_demand_census / demand-census edit. Main's 00_compile changes land outside the census route, while the final PR-vs-main patch still carries the complete route and verb;
• the two shared-roster resolutions are additive unions: seed_growth_admission adds only the census import and roster member, and floor_pure_producer_share adds only ddc_report and the production-refusal producer. Main's rows are retained;
• docs/design-rung-drops.md is main's regenerated artifact and is absent from the final PR-vs-main diff.

Exact-head generated, floor, emit-build, and witnesses checks all pass.

Merge-queue landing only. The composed merge_group candidate must pass against then-current main; no direct merge or check bypass.

[briansrls]

APPROVE for merge-queue landing at exact head cbf752b46a970621efd3f94e6801eabdcdbf8e58.

No findings. This rebinds my approval at 402260f45fd708d4dae9028ff84ce4292192f177.

I reviewed only the intervening merge/regeneration delta:

• the substantive merge commit de77122581d2a4be626a55681c083ee305f8b12f has parents 402260f45fd708d4dae9028ff84ce4292192f177 and current main 3433121b16e4f514b8c73796adde0dfd19650e9b;
• the authored census module and its complete real-route claim module retain exactly the previously approved blobs: dependency_demand_census.dag = 66b1951c47dca2b0eb4e692e5180d4643a885082, and dependency_demand_census_test.dag = 8c1a567d4c9e4b0aa1f780cd3442bd971a3ebf7e;
• the D13 census block in 00_compile.dag—strip/read, module resolution, report reduction and rows-only output—is textually unchanged. Newer-main edits in that file are outside this route;
• the shared-roster resolutions retain both sides: seed_growth_admission still imports and rosters dependency_demand_census_seed_growth_justification, and floor_pure_producer_share still carries ddc_report plus ddc_app_production_refuses_at_the_clause amid main's newer rows;
• the final head adds one generated follow-up commit after the merge, changing only one line in src/v1/stage0/src/v1_compiler_emit_rust.rs to regenerate the mirror on the composed tree. It is not an authored census semantic change.

Exact-head generated, floor, emit-build, and witnesses checks all pass. The PR is open, non-draft and mergeable at this SHA.

Merge-queue landing only. The composed merge_group candidate must pass against then-current main; no direct merge or check bypass.

[briansrls]

APPROVE for merge-queue landing at exact head 11de102f93fae28bb79af4637b584e61630d83a4.

No findings. This rebinds my approval at cbf752b46a970621efd3f94e6801eabdcdbf8e58.

I reviewed only the intervening merge and generated follow-up:

• the substantive merge commit 1eec9a8017329bde9c2cf6672d6f85969fa660e8 has parents cbf752b46a970621efd3f94e6801eabdcdbf8e58 and newer main 978fb0a566d540d82013775724385d3d947f3342;
• the authored census module and its real-route claim module retain exactly the approved blobs: dependency_demand_census.dag = 66b1951c47dca2b0eb4e692e5180d4643a885082, and dependency_demand_census_test.dag = 8c1a567d4c9e4b0aa1f780cd3442bd971a3ebf7e;
• the D13 block in 00_compile.dag—strip/read, scoped normalize, module resolution, fact collection, reduction and rows-only output—is textually unchanged; newer-main edits are outside that block;
• the dispatch-workflow resolution is the union: source authority and generated YAML retain dag-emit-real-grammar-round-trips and self-host-behavioral-equivalence and add dependency-demand-census, for exactly three choices;
• the final PR-vs-main patches in 05_emit_rust.dag, cli_run.rs, native_lane_runner.rs, and target_invocation_host.rs add only the census use, export, host runner, producer registry/dispatch and output mapping. Main's newer arms remain. The two host helpers are appended at the ends of their files, outside the shared append hot spots;
• the exact head's follow-up commit regenerates only .github/workflows/instrument-dispatch.yml and src/v1/stage0/src/v1_compiler_emit_rust.rs on the composed tree.

Exact-head generated, floor, emit-build, and witnesses checks all pass. The PR is open, non-draft and mergeable at this SHA.

Merge-queue landing only. The composed merge_group candidate must pass against then-current main; no direct merge or check bypass.