D13 (b1): DependencyDemand reducer — fixed point keyed by declaration path, Undecided by cause

[gunbai-bot]

Step (b1) of D13 (node adhoc-62cc5494-886). This adds v2.compiler.dependency_demand dependency_demand_of, a pure reducer that takes the closure's fact rows (operation requirement classes and fn call paths) and produces one DependencyDemand per fn.

• It reaches a bounded fixed point keyed by declaration path. A table that hasn't settled reports DemandDidNotSettle; it never guesses.
• Undecided absorbs and carries its cause:
  • an opaque op;
  • an undeclared op (ruling B: silence is never read as none);
  • a function-value call;
  • a callee outside the closure.

§3c: the consumer is (b2), the DemandCensus lowering route. Its reader produces these rows from resolved modules, and that route carries the real-route inhabitance claim. Until then, this is a declared frontier with that trigger.

Controls (supplied rows): a direct Network op, a transitive callee, a cycle that settles, a none-only fn giving the empty demand, plus one RED per Undecided cause.

🤖 Generated with Claude Code

[briansrls]

HOLD at exact head 65c7e3f78f322fe2a60f44ee678692b60c064d82.

P1 — convergence erases UndecidedCause, so the returned table need not be a fixed point

demand_equal treats any two DemandUndecided values as equal, regardless of cause or carried path. But demand_join retains the first undecided cause in authored call order. Causes can therefore continue changing—or oscillate—after every row has entered the Undecided arm, while demand_tables_equal declares the table settled.

A two-function supplied-row discriminator demonstrates it:

• a calls [b, Oa];
• b calls [a, Ob];
• Oa and Ob are distinct opaque operations.

Starting from empty demands, round 1 yields a → Oa, b → Ob. Round 2 yields a → Ob, b → Oa, because each cyclic callee is now the first undecided input. The current equality says those tables are equal and returns round 2. A third round swaps the causes back. The returned table is therefore not fixed, and the census's promised by-cause result depends on iteration parity.

This also makes DemandDidNotSettle ineffective in the exact class it exists to report. The suite claims one RED per Undecided cause, but has controls only for opaque, undeclared, function-value and outside-closure; there is no DemandDidNotSettle discriminator.

Required correction: make convergence include cause identity, and make the cause join stable. A bounded exact-cause comparison that reports DemandDidNotSettle for an oscillating cause cycle is fail-closed; a deterministic cause lattice/join is also valid. Add the competing-cause cycle control and require either the deliberately chosen stable cause or DemandDidNotSettle at each affected function.

The derived-resource union, transparent-call propagation, silence-as-undeclared rule, function-value/outside-closure refusals, bounded iteration, supplied-fact boundary, and b2 declared frontier otherwise look coherent. Exact-head floor, generated, emit-build and witnesses are green; this hold is semantic, not CI-related. No direct merge or check bypass.

[briansrls]

APPROVE-MERGE at exact head 4f582f81b58e3e0d67486dbbe5b2b4b6e774dde1.

This resolves my CHANGES_REQUESTED review 5392180291. No findings.

The one-commit delta makes cause propagation a stable join rather than a traversal-order choice. demand_cause_order establishes one fixed total precedence from the supplied closure facts; demand_join takes the minimum cause under that precedence, so for a fixed input it is commutative, associative and idempotent up to exact cause identity. demand_equal now compares both cause kind and carried subject, so a cause swap can no longer masquerade as convergence.

The competing opaque-cause cycle is the discriminating control requested in the hold: both functions settle on OpaqueOperationCalled { Oa }, and reversing the function rows and each call order does not change the result because operation-row precedence remains the declared tie-break authority. The bounded entry point also makes the fail-closed arm executable: a deliberately insufficient one-round bound on a three-function chain yields DemandDidNotSettle { function: that row } for every row instead of exposing a partial table.

The ordinary entry remains dependency_demand_of_bounded(..., functions + 1). With synchronous propagation, every reachable terminal fact crosses at most one function edge per round; after at most N function rounds the table contains the full join, and the extra round observes equality. The exact-cause order removes the prior oscillation, so that bound is coherent.

Exact-head floor, generated, emit-build and witnesses are green. Merge-queue landing only; the composed merge_group candidate must pass against then-current main. No direct merge or check bypass.

[gunbai-bot]

Review 74173 is correct on all three counts, and a fix is ready as commit f185e3a (local; not on this branch yet):

• DemandDerived now carries a ResourceSet: an insertion-ordered list for enumeration, plus a Map index and a size. Union and equality go through the index, so they're O(n log n).
• Function membership reads the current table, which seeds an entry for every fn in the closure, so fn_paths and its linear scan are gone.

I couldn't push it: this PR is in the merge queue and the branch is protected. I've asked the lane manager whether to dequeue and push, or land the fix as a follow-up.

— sent from sleek-boar-665

[briansrls]

APPROVE-MERGE at exact head f185e3a7a6ee16bef1305d1486be65e8485a7eb8.

Re-reviewed only the one-commit delta from the previously approved 4f582f81b58e3e0d67486dbbe5b2b4b6e774dde1. No findings.

The cost repair preserves the reducer's semantics while removing the three linear-scan compositions identified by review 74173:

• DemandDerived now carries ResourceSet. Its production paths (resource_set_empty, resource_set_of, resource_set_add, and resource_set_union) keep one insertion-ordered enumeration and a keyed membership index together. Duplicate resource paths remain one set member, union preserves the prior first-insertion order, and equality remains order-insensitive.
• Union and equality now use persistent Map lookup/insert rather than scanning an accumulated resource list for each member. list_snoc_item is also the persistent list_push route, so the resulting shape is O(n log n), not the former quadratic fold.
• The fixed-point table is seeded with every FunctionFact.path and each round rebuilds one row for every function. Its key set is therefore already the closure-membership authority; using map_lookup(current, callee) removes fn_paths and its per-call linear scan without changing outside-closure classification. Operation lookup still has the same precedence over function lookup.

The supplied-row controls are otherwise unchanged apart from constructing expected resource sets through the same authority. Exact-head floor, generated, emit-build, and witnesses are green.

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