requires none / requires opaque in both seeds; an absent requirements edge is undeclared, not none (D13 ruling B)

[gunbai-bot]

Stacked on #12911 (v2 requires edge) and #12937 (v1 requires parse), both in the merge queue. Until they land this diff contains their commits.

Why

D13 step (b) derives a function's demand from the operations it calls. With #12911's reading (absent edge = "no requirements"), every unaudited operation, and every one added later, silently reads as requiring nothing. That is the fail-open default DESIGN §5 forbids. The lane owner ruled B: every operation declares one of three forms, all on the one ^arrow_resource_requirements_edge, and an absent edge is undeclared, which step (b) reads as Undecided. The Network audit (loyal-crab-214) writes the rows: 236 NotNetwork ops get requires none, and 12 runtime-argv exec ops get requires opaque.

⚠️ Reversal of #12911, stated for deliberate review

#12911 said "no requirements has one form: the absent edge". This PR reverses that. docs/plans/arrow-contract-edges.md carries a section on the reversal, and it scopes requires none as none of the audited vocabulary (Network today), which is not a Filesystem/Clock/Entropy claim.

What

• v2 grammar: requires none and requires opaque are their own productions under op_requires, because a literal terminal stamps its class, not its word. They are whole clauses: a member after either refuses.
• v2 lowering: both lower onto the same edge as childless Atoms, ^requirements_declared_none and ^requirements_opaque. v2.std.arrow_contract admits exactly the three target shapes. Resolve walks only the member Conj and carries the Atoms unwalked.
• v1 parse: parse_op_requires_clause carries each word as ONE requires property whose value is the word as a string literal (matched by text, since none is a v1 keyword literal). It is the same property a resource member uses, and the reader tells the forms apart by the value's shape, because a property's name is read back from its span. A second requires clause on one operation refuses at parse (review 73995).
• v1 reader: operation_requires_members becomes the closed operation_requires_declaration = RequiresUndeclared | RequiresNone | RequiresOpaque | RequiresResources { members }, the answer D13 step (c) consumes. compile_dag_operation_requires reports the arm first (undeclared / none / opaque / resources, ..). The seed mirror is regenerated (claim_executor --required-regen).

Controls

v2 (v2.test.claim.normalize.operation_requires_edge):

• none and opaque lower to their Atoms;
• requires none, N refuses;
• the fidelity claims.

v1 (test.claim.v1_operation_requires_parse_witness_test):

• none and opaque are carried as their own forms;
• an operation without a clause is undeclared, not none;
• requires none, Net refuses;
• the member forms now report resources, ...

🤖 Generated with Claude Code

[gunbai-bot]

Addressing review 73995 in 43da08e. The finding was correct and blocking: v1's parse_op_body_entries accepted any number of requires entries, and operation_requires_declaration merged their members. So requires none plus a separate requires Filesystem read as RequiresNone, discarding the declared demand (and opaque plus Network read as RequiresOpaque). v2 already refused the repeat at lowering (body_lowering_reason_operation_requires_repeated), so the two seeds disagreed.

Fix, construction over validation: v1 now refuses a SECOND requires clause at parse, so the conflicting state can never be carried, and the reader never sees two clauses to arbitrate. The comment at the clause parser now states both rules: one clause per operation, and a member after a whole-clause word refuses. New REDs in test.claim.v1_operation_requires_parse_witness_test: a_second_requires_clause_after_none_refuses and a_second_requires_clause_after_opaque_refuses. The single-clause positives are unchanged, so each RED differs only by the second clause. The seed mirror is regenerated.

— sent from sleek-boar-665

[briansrls]

APPROVE-MERGE at exact head 43da08efcbdb2905c8faff99d42767ab17819230.

No findings.

The deliberate #12911 reversal is modeled coherently and fail-closed in both seeds:

• The one ^arrow_resource_requirements_edge has exactly three declared target forms: a nonempty resource-reference Conj, the childless ^requirements_declared_none Atom, or the childless ^requirements_opaque Atom. An absent edge is not reinterpreted as an empty target; it remains the distinguishable undeclared state that D13 step (b) must map to DemandUndecided.
• v2 gives none and opaque discriminable productions ahead of the general type-list arm. Lowering projects all three source forms onto the same edge, the contract wall admits only the two exact childless markers or a nonempty Conj, and resolve walks only the Conj while carrying the prevalidated marker Atoms unwalked.
• v1 exposes one closed OperationRequiresDeclaration answer (RequiresUndeclared | RequiresNone | RequiresOpaque | RequiresResources). The parser prevents the conflicting population rather than asking that reader to arbitrate it: requires none, R / requires opaque, R refuse, and any second requires clause refuses before it can be carried. Thus neither none nor opaque can silently dominate a separately declared resource demand.
• The seed query now reports the arm before any resources, so the controls distinguish undeclared, declared-none, opaque, and ordered resources rather than conflating absence with an empty list. The generated stage0 mirror moves with the source.
• The committed design explicitly scopes requires none to the audited vocabulary (Network today), preserving direct capability-derived Filesystem/Clock/Entropy demand rather than turning none into a universal effect assertion.

The approved #12911 and #12937 exact heads are ancestors of this head, and the later changes preserve their boundary evidence while adding the closed declaration forms and the one-clause construction wall.

Ordering remains binding: D13 step (b) must not land until #12965's Network population and the 236 requires none / 12 requires opaque rows are complete. This PR makes absence fail-closed; it does not itself complete that population.

Non-blocking PR-description note: the v1 implementation no longer uses separately named requires_none / requires_opaque properties. It carries one requires property whose value identifies the word, then the closed reader decodes it. Updating that bullet would make the PR body match the landed representation.

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