v2: a resource declaration parses and lowers; the index marks it a declared resource (D13 step a0)

[gunbai-bot]

Built on #12863 (landed); main is merged in, so the diff is this change only.

Why

D13's prerequisite (gunbc.rung_drop network_requirement_unrepresented_after_uses_cut) needs an operation to declare the resources it reaches, checked at resolve against a resource declaration. v2 had no resource declaration: dag/std/resources.dag did not parse in v2. This is step (a0); step (a), the requires contract edge, builds on it.

What

• Grammar (v2.extdeps.languages.dag): resource Name { .. }, with one production per entry: kind:, mode:, expires:, capability name { input/output }, acquire { [hermetic] }, release {}. Anything else is a located parse refusal. v1's parse_resource_entries skips acquire and release bodies token by token; v2 does not. The bare and parenthesized capability forms are not admitted, and the corpus authors neither.
• Homes (std.resources): ResourceKind = Capability | Observation and ResourceMode = Read | ReadWrite. This retires three ActiveDebt rows in floor_unimported_bare_provider_debt_roster (ImportsFixed: the file now declares the names).
• Lowering (body_lower_resource_decl): capabilities lower through the one operation reader (body_lower_operation), so a resource has a service's Conj { Name: payload } shape. Kind, mode, expires and acquire are read against their homes (v2.std.resource_declaration) into a DeclaredResourceContract on a new DeclaredTypeKind arm, DeclaredResource. It is captured at normalize, as a record's kind is. A repeated, unknown or missing entry refuses at the entry, under 4 new reasons.
• Index: SymbolIndex.declared_resources, read by symbol_index_declares_resource_at, filled from the captured names. Those names ride on ModuleBindingSource / CensusTree / LocatedModuleRoot resource_declarations beside record_declarations. Emission refuses a resource member as unsupported.

Deviations from the agreed shape (reported to the lane owner)

• The contract facts are not edges on the node. symbol_index_fill indexes every Named payload edge as a member path, so an edge there would be a name nobody declared.
• DeclaredPayloadKind was not reused. It means "is a constructor payload" (resolve_path_is_declared_payload), and a resource is not one.
• decl_index ItemKind is unchanged. Its producer is a host seam, so a ResourceItem arm would have no producer.
• No compile_door_cause_ownership rows, with the evidence stated at its real strength. The four new reasons are body_lowering_reason_resource_entry_unread, _resource_entry_repeated, _resource_value_unknown and _resource_entry_missing. Each fires only on a malformed resource declaration. The corpus has exactly 5 resource declarations, all in dag/std/resources.dag, and each authors exactly the entry forms the grammar admits (read off the file). On CI run 36849662743 (head 818a0e2), none of the four reasons appears in the floor, emit-build or witnesses logs. Those lanes do NOT lower dag/std/resources.dag through v2, though: the emitted compiler's closure no longer reaches std.resources. So the zero means no executed route reached them; it is not a measurement that all 5 declarations lower cleanly. That measurement belongs to the native-route census. If it ever reports one of these reasons on a real module, the row is owed then.

Evidence (executed)

CI run 36849662743 on 818a0e2: floor, emit-build, generated and witnesses are all green. Every claim in v2.test.claim.normalize.resource_declaration_lowering passed in the floor:

• census admits a resource and marks only its path (59,984 eval steps);
• the full door admits a resource with every property entry (47,324 steps);
• the capture names the resource and only it;
• 4 REDs: an unknown kind, a repeated kind, a missing mode, and an acquire body other than hermetic;
• the supplied-stream fidelity claims.

Review 73658 (§3c) is addressed. Only the name is carried, the index mark declares its step (a) consumer, and the validated-but-not-carried contract is declared as gunbc.recurring_failure_mode resource_contract_validated_but_not_carried.

🤖 Generated with Claude Code

[gunbai-bot]

Addressing review 73658 (§3c, no production consumer) in a040310. The finding was correct.

• Index mark (SymbolIndex.declared_resources / symbol_index_declares_resource_at): it now carries a declared 3c frontier beside the type. The production reader is D13 step (a), the resolve check that each requires member of an operation's ^arrow_resource_requirements_edge names a declared resource. The trigger is that step (a) calls the accessor; if step (a) is abandoned, the field, mark, accessor and resource_declarations carrier are deleted.
• Contract (kind/mode/expires/acquire): no consumer reads it, so it is no longer carried. DeclaredResource is { name } only. Every entry is still read against its home and refuses at the entry when unknown, repeated or missing. The values are validated and not carried, and that gap is declared as gunbc.recurring_failure_mode resource_contract_validated_but_not_carried. Its trigger is the first consumer of those facts (for example provider admission), which also carries the contract. The lane owner chose this over a frontier with no scheduled change behind it.

The same commit also fixes the floor's budget refusal on two claims, which were over the new-witness eval-step budget: they now read smaller fixtures.

— sent from sleek-boar-665

[briansrls]

HOLD / REQUEST_CHANGES at exact head 818a0e2cb9422346cd7879dc08e24d6748a918da.

[P1] body_lowering_reason_resource_entry_unread is reachable from a grammar-admitted resource capability, so the PR's claim that all four new reasons fire only on malformed resource declarations is false.

dag_grammar_capability_expr reuses the ordinary input_block / output_block productions. Their shared I/O field grammar admits the existing optional tail forms, including from "key" and = default. body_lower_operation therefore returns a nonempty set_aside for such a field. body_lower_resource_with_capability maps every nonempty op.set_aside to the new fatal body_lowering_reason_resource_entry_unread at the whole capability entry.

So a shape such as:

resource R {
  kind: Capability
  mode: Read
  capability get {
    input { page: Int = 1 }
  }
}

parses under this grammar and then reaches the supposedly malformed-only cause. An output from "key" has the same route. This is a valid-but-unmodeled interface/realization fact, not an unread malformed resource entry. The new RFM covers kind/mode/expires/acquire contract values, not this capability-member gap, and the controls exercise only a tail-free capability.

Bounded correction: either (a) give resource capabilities a tail-free I/O grammar until the binder-default and realization carriers exist, making these forms unwriteable here and adding negative parse controls, or (b) keep the shared grammar and preserve a specific located frontier with an ownership row/trigger for each admitted tail class. Do not collapse an admitted default or wire projection into generic resource_entry_unread while leaving that fatal cause unowned.

The name-only declared_resources index mark, its DESIGN §3c standing, the reuse of operation lowering, and the validated-but-not-carried resource-contract RFM otherwise look coherent. Exact-head CI is green, but it does not cover this route. Return with a corrected exact head for merge-queue-only review; no direct merge or check bypass.

[gunbai-bot]

Addressing GitHub review 5378770924 in 8aba6f6. The finding was correct: a capability's well-formed from "key" or = expr io tail was refused as the generic resource_entry_unread, and the positive fixture had no tail to catch it.

Taken as option (B), with no grammar fork. The capability arm now refuses exactly as a service with a set-aside member does on a route past the census: the owned fatal cause body_lowering_reason_service_realization_unreachable at the capability, with body_lowering_reason_interface_member_unmodeled pending at each tail (the reason body_lower_operation already assigns both tail forms). New controls: a_default_tail_refuses_as_a_service_set_aside_RED and a_wire_key_tail_refuses_as_a_service_set_aside_RED, each asserting that fatal, that pending cause, and the absence of resource_entry_unread, plus supplied-stream fidelity claims. resource_entry_unread is now reached only by a malformed entry.

One difference from the brief: services file both tails under interface_member_unmodeled; default_value_unmodeled is used only for fn parameter defaults on main. So I reused the service's actual causes rather than splitting them.

— sent from sleek-boar-665

[briansrls]

APPROVE-MERGE at exact head 8aba6f63be3549413c88b7864aacc9f61aa32bb5.

No findings. This supersedes my CHANGES_REQUESTED review 5378770924.

The held route is repaired without weakening the shared I/O grammar:

• A well-formed resource-capability I/O tail no longer becomes body_lowering_reason_resource_entry_unread. body_lower_resource_with_capability preserves the existing ServiceSetAside diagnostics and refuses fatally as body_lowering_reason_service_realization_unreachable, the same fail-closed class used when an operation carries an unmodeled default or wire projection.
• The existing ownership/retirement trigger applies to the actual facts in this set-aside population: the one-binder default representation removes = expr; the realization binding removes from "key". resource_entry_unread is therefore left for malformed or unreadable resource entries only.
• New default-tail and wire-key-tail controls require the owned fatal cause, require pending interface_member_unmodeled, and explicitly exclude resource_entry_unread. Either control is red on the held head by construction, whose fatal was resource_entry_unread.
• Both supplied token streams are paired with tokenizer-fidelity controls, so the specimens exercise forms the real grammar admits rather than hand-built-only trees.
• The corrective head is one two-file commit after the main merge: production classification plus the two discriminating controls.

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

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