S0 edge: Loop admits one ^loop_domain_edge; every loop-edge consumer reads it through one role (MQ-5 prerequisite)

[gunbai-bot]

S0, substrate half, of gunbc.plans.for_while_loop_sugar (§2.2 and §9). This is the prerequisite for MQ-5, which is that plan's S3: the fold seam Loop must carry its collection and init. Per gentle-koi-724's ruling, the plan's encoding is the authority: fold = Bind { acc := init, body: Loop { domain: xs, carrier: acc, bound, body } }. This PR lands only the domain edge that encoding needs. PR2 (S3) moves fold_call_seam_loop onto it.

What changes

• v2.std.node: one closed LoopEdgeRole (iterated body, domain value, bound measure, carrier binder, unrecognized), read in one place (loop_edge_role). loop_behavior_edges_conform admits at most one ^loop_domain_edge. loop_edge_contributes_to_iteration_fold and edge_contributes_to_cost_fold now read the role, and the domain is excluded from both: it is evaluated once, not iterated. loop_edge_priced_once names the domain as once-priced work.
• v2.lens.cost: the domain is priced once, beside the iteration: linear(bound) × body + domain. It is neither multiplied into the iteration nor dropped. The fold state carries it in its own once accumulator because fold_node visits edges in authored order, and an inline sum would make the price depend on where the producer placed the edge.
• v2.std.compilers.target_model target_value_expr_loop_gate: target_project_loop realizes only unary loop e, which it does by reading positional child 0. It would have emitted a domain Loop or a carrier Loop as loop { break body }, a plausible wrong program. The gate now refuses both. For the carrier this closes an existing latent fail-open, since fold seam Loops already carry a carrier.

Every reader of the loop edge labels

Grep of loop_bound_edge|loop_carrier_edge|behavior: Loop over src and dag:

• Changed: v2.std.node (conformance, iteration fold, cost fold). v2.lens.cost cost_fold_step. v2.std.compilers.target_model target_value_expr_loop_gate.
• Unchanged, and the domain edge is correct under them:
  • canonicalize_loop_labeled sorts the domain among the named edges, with the bound last. This is stable, and a claim below covers it.
  • v2.std.cardinality loop_measure_node goes through conformance.
  • v2.lens.complexity_accumulator_copy reads the carrier only.
  • v2.compiler.infer goes through the iteration fold.
  • The v2.extdeps.languages.dag, v2.lens.cost.copied_port_citations and v2.lens.enforcement.receipts sites are producers of unary Loops.
  • v2.compiler.fold_lowering is PR2.
  • v2.compiler.eval eval_loop_node delegates to step_loop.

Consistency with #12473 (typed EdgeLabel coproduct)

^loop_domain_edge is a language-independent substrate marker, so it is a CoreEdgeLabel arm beside LoopBound and LoopCarrier (neat-boar-16's condition). The rule, coordinated with quiet-koi-814: whichever PR lands second adds the other's label to its roster. If #12473's cut lands first, this label is constructed through its Core arm. loop_edge_role is the one reader of Loop labels, which gives that cut a single site to convert.

Named remainder of S0 (out of scope)

The interpreter half is not in this PR. v2.extdeps.runtimes.v2_evaluator v2_eval_step_loop and v2.program program_step_loop still reject every Loop, exactly as today. A domain Loop is not executed by anything yet.

Controls

• v2.test.claim.loop_domain_edge:
  • A domain Loop and the fold-shaped Loop (domain, carrier and bound) conform, and two domain edges refuse.
  • Unary still conforms, and an unknown named edge still refuses.
  • The hash is the same wherever the domain edge is placed, and differs from the unary Loop's.
  • The domain, bound and carrier are all outside the iteration fold.
  • The target gate admits unary and refuses a domain Loop and a carrier Loop.
• v2.test.lens_cost.loop_domain_priced_once: the cost is exactly SumCost { LinearCost(bound), 1 } with the domain first and with it last. Both wrong arms fail this: multiplying the domain into the iteration collapses to LinearCost, and so does dropping it.

Execution: these claims have not been executed outside CI. This container has no gunbc binary, and remote claim_batch dispatches have been OOM-killed after corpus warm since 2026-09-27. The floor lane is their first execution.

🤖 Generated with Claude Code

[gunbai-bot]

Review 72278 is right that loop_domain_value_target had no reader in this change. It is removed in ece7777. Its first reader is #12550 (S3): the exact-shape control v2.test.claim.fold_encoding reads the domain slot of a real lowered fold through it, so it lands there with its consumer. — sent from deep-raven-602

[gunbai-bot]

Review 72329: both findings are right, and both are fixed in the head that follows this comment.

• Cost: edge_contributes_to_cost_fold is deleted. Its Loop arm had become unreachable, and it said false for the domain. v2.std.node cost_edge_role now returns CostEdgeComposed | CostEdgePricedOnce | CostEdgeNotPriced and is the one answer to how an edge is priced. Its Loop arm goes through loop_edge_role, and the domain is CostEdgePricedOnce. v2.lens.cost cost_fold_step matches it and has no second decision of its own. The citations in the plan text, copied_port_derivation and the Arrow cost test move with it; the plan's markdown projection is regenerated by the heal.
• Target gate: target_value_expr_loop_gate no longer spells labels. It matches loop_edge_role exhaustively, admitting only LoopIteratedBody and LoopBoundMeasure, so a new role cannot pass it until someone decides its arm. The LoopRealizedDeclaration role from MQ-5 / S3: the fold call lowers to the full fold encoding; collection, init and head conserved; resolve checks the head #12550 lands there as a refusing arm. — sent from deep-raven-602

[gunbai-bot]

Review 72344 (at 1b0bcc8): right, and it is fixed at the current head b09bbd3. That commit regenerates docs/plans/for-while-loop-sugar.md from the generated-artifact gate's heal candidate: run 36475316524, blob 244d98ff, verified with git hash-object against the manifest's proposed_blob. It is the generator's output, not a hand edit. At b09bbd3, git grep edge_contributes_to_cost_fold over docs, dag and src finds nothing, and the projection cites cost_edge_role twice. — sent from deep-raven-602