v1: an operation body parses requires R, .. and carries it on the operation (D13 step b0)

[gunbai-bot]

Why

D13 step (b) derives a function's resource demand partly from the requires edge of the service operations it calls (#12911). That edge has to be authored on real extdeps operations, a ~500-op Network audit the lane owner dispatches next. But the corpus is compiled by the v1 seed, and v1 did not parse requires, so no operation could author it. This is that v1 parse change, ruled as a separate small PR: v1 parses requires on operations and carries it, with no other v1 behaviour change.

What

• v1.compiler.parse parse_op_body_entries gains a requires arm. parse_op_requires_members reads a comma list of type expressions (parse_type_expr) and turns each member into one requires property whose value is the parsed type, carried beside the modifier properties.
• No other v1 behaviour reads it. Every v1 consumer of an operation's properties selects by name or prefix (idempotent/readonly/hermetic, response_, exit_, mock_). The one generic reader is compile.dag's property serializer, which dumps every property and only matters once an operation authors requires. No corpus operation does yet.
• The seed's generated Rust (src/v1/stage0/src/v1_compiler_parse.rs) is regenerated per the recipe CI's generated-artifact phase prints. (If that file is not yet in the diff, it follows in the next commit.)

Controls (test.claim.v1_operation_requires_parse_witness_test)

Accepted (through the real seed compile, compile_dag_rust_emit_check): one member, and two members, compile clean.

Refused:

• A non-type member (requires 123).
• An empty requires written as the LAST entry, right before }, so the member reader meets the brace. It is paired with the identical operation without the line, which compiles clean.

Carried, not only accepted. v1.compiler.parse operation_requires_members is the one .dag reader of an operation's parsed members, in order. Its production consumer is D13 step (c) (§3c). The seed query compile_dag_operation_requires(source, service, operation) parses with the seed's own parser and reads through that reader. A parse error, a missing service or a missing operation refuses; none answers an empty list. Controls:

• one member gives exactly ["Net"];
• two members give ["Net", "Fs"], in order;
• an operation without the clause gives [].

Filed with it:

• the builtin signature (04_method.dag);
• the std.primitives roster and the interpreter primitive surface row (dispatch projection);
• a primitive-egress SeedQuery disposition row;
• a seed-growth justification for the one hand host function (gunbc.operation_requires_query_seed_growth).

The stage0 mirrors were regenerated with claim_executor --required-regen.

Noticed, not changed

parse_op_body_entries already accepts an unknown name: expr entry in an operation body and drops it (its last ShIdent arm). That is a silent drop, but it predates this change and is out of scope here; reported to the lane owner.

🤖 Generated with Claude Code

[gunbai-bot]

On review 73858's residual risk (whether every v1 consumer of an operation's properties selects them by name or prefix). I checked this before writing that comment; the readers on this base, found by grepping .properties |> filter|map across src/v1/*.dag:

• 05_emit_rust.dag: mock_props via has_mock_prefix, response_200 by name, response_props via has_response_prefix, exit_props via has_exit_prefix. 05_emit_core_support.dag: has_mock_prefix.
• 00_core.dag: admit_callers by name, and two type-node property filters (not operation nodes).
• 04_resolve.dag, 05_emit.dag, 05_emit_rust.dag: the field from key, on field nodes, not operations.
• 04_infer.dag: head_erasing_properties, on type nodes.
• The one generic reader: compile.dag's JSON serializer emits every property. A requires entry would appear there once an operation authors one. No corpus operation does yet, and the PR body says so.

So none of them can select a requires property except that serializer.

One weakness in my own controls. a_requires_with_no_member_refuses refuses, but probably not for the reason its name gives: parse_type_expr skips newlines and reads the next line's output as the type, and the parse then fails at {. It is still a refusal, never an acceptance, but it does not discriminate an empty member list specifically. I'll tighten it if a reviewer wants a dedicated empty-list refusal.

— sent from sleek-boar-665

[briansrls]

HOLD at exact head 83725b0723efb95a228254a166183a65a5f3cc41.

Two bounded test findings; the parser change itself otherwise looks coherent, the stage0 mirror is regenerated, and all exact-head checks are green.

P1 — the empty-requires control refuses for the wrong reason

The disclosed weakness is blocking. In the current fixture, parse_type_expr skips the newline and reads the next entry's output identifier as the purported requirement type. The parse then fails at that entry's {. Therefore a_requires_with_no_member_refuses would remain green even if the requires parser had no nonempty-list rule at all; it proves only that the resulting token stream eventually fails.

A refusal control must discriminate the rule it names. Use an otherwise-valid operation where requires is the final entry immediately before }, so the next token cannot begin a type expression, and pair it with the same operation without that line compiling cleanly. Alternatively inspect a parser result/error at the requires member boundary. Merely asserting !compiles(...) on a fixture that fails later is insufficient.

P1 — acceptance does not prove the members are carried

Both positive controls would still pass if the new arm parsed and consumed requires R, .. but discarded r.properties instead of concatenating them into modifier_props. That is especially important here because the PR correctly states that no ordinary v1 semantic consumer reads requires; compile success therefore cannot observe the central "carried as one property per member" claim.

Add one discriminating control at the parser or the existing generic property serializer showing:

• one member yields exactly one requires property whose value is that parsed type expression; and
• two members yield two such properties in order.

The code currently appears to do this (concat(modifier_props, r.properties) and one minted property per recursion), but the behavior needs an executable observer because carrying—not merely accepting the spelling—is the purpose of step b0.

Exact-head floor, generated, emit-build, and witnesses pass. This hold is solely the two non-discriminating coverage gaps; no direct merge or check bypass.

[briansrls]

APPROVE-MERGE at exact head 2800067ac7234b55e9e11cf7bd8ec763ab9cb9ca.

This supersedes my CHANGES_REQUESTED review 5384774721. No findings.

Both held P1s are resolved:

• The empty-requires discriminator now puts requires last, directly before the operation's }, so parse_op_requires_members meets the closer where a type expression must begin. The paired source differs only by removing that line and compiles cleanly. The negative can no longer stay green by consuming a following operation entry and failing incidentally later.
• Carry is now observed, not inferred from compile acceptance. v1.compiler.parse.operation_requires_members is the one .dag reader of the parsed requires properties and preserves their authored order. compile_dag_operation_requires parses through the seed's tokenizer/parser, finds the named service and operation, and delegates to that reader; parse failure, missing service, and missing operation are refusals rather than empty results. The controls require exactly [Net], [Net, Fs], and [] for one, two, and absent clauses, so dropping, reordering, or fabricating the carried members is discriminated.
• The reader has an honest DESIGN §3c standing: D13 step (c) is the named production consumer. The hand host exposure is bounded by a filed seed-growth justification and primitive-egress disposition, and the signature, primitive roster, authored dispatch surface, generated dispatch projection, and stage0 mirrors move together.
• Service children are the parser's operations population, so the host lookup cannot satisfy the operation name with an unrelated service member.

Exact-head floor, generated, emit-build, and witnesses all pass. GitHub reports the PR open, non-draft, clean, and mergeable.

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