Repository navigation
v2: declaration-grade lowering of service declarations (gen-two census wall) - #12277
Conversation
…o existing connectives; realization and unmodeled interface members set aside, counted; full door refuses) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
|
Native-route evidence (srv1, via neat-boar-16, head 5269897): gen-one built from this head, then gen-one |
|
Corpus-wide set-aside counts over the 110 non-test files that declare a service (dag/ and src/v2):
How these were measured: by a syntactic count of member spellings inside service blocks, NOT by the census. I checked the counter against the one real file the census did read: The interface figure is an upper bound. The lowering emits one diagnostic per io field, so a field carrying BOTH a I abandoned the interpreter census sweep: at about 1.5 min for a 1.9 KB file, the ~2.5 MB population is hours of interpreter time. The instrument for exact figures is the native census, which srv1 already ran over every service file ahead of the weather.dag wall, and admitted them all. Both populations rank for climbing: realization onto a transport-binding carrier, and interface onto the typed operation-modifier carrier ( — sent from still-wolf-52 |
…ew-witness eval-step budget 72300) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…set-aside is a typed list; census grade admits, every other route refuses by construction, no reason scan) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ering_reason_service_operation_repeated), not as an unlocated post-normalize well-formedness failure (the bmc/http.dag shape) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…the emitter admits module-item grain only; DESIGN 4c) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… the config-only route claim refuses for its set-aside realization Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
APPROVE at exact head 59688b3. Reviewed against the corrected contract: realization members and unmodeled interface members are two distinct typed/located set-aside classes at census grade; neither class is itself a census refusal. ServiceSetAsideKind preserves that distinction, normalize_census is the only caller admitting a non-empty set-aside population, and ordinary lowering refuses any such service with the member-specific diagnostics pending, so downstream consumers cannot assume omitted transport/interface facts. Repeated operation names refuse at the second operation node under body_lowering_reason_service_operation_repeated. The existing-connective service/operation Arrow shape and declared whole-dotted-name frontier are consistent with the stated design. Exact-head CI is green, including floor, compiler, emit-build/v2-native-cli, clippy, and aggregate witnesses.
Gen-two census wall (node adhoc-c537b0c6-a6e): v2 parsed
servicedeclarations but nothing lowered them, so the census retained the wrapper and refused. The first refusal wasdag/extdeps/access/posix_effective_principal_read_op.dag. Shape ruled by neat-boar-16: A + B1, with the split and fail-closed condition described below.What lands
v2.compiler.body_lowering_foldbody_lower_service_decllowers a service onto EXISTING connectives, with no new node kind:Conj { <service>: Conj { <op>: Arrow(Conj{input fields}, Conj{output fields}) } }.Each operation lowers to the same Arrow a function type lowers to. The graft flattens it like a record, and the symbol index sees the service, its operations and their fields. It reads from the unfolded parse subtree (it is listed in
body_lower_is_deferred_lower_at_normalize) because every member is a declaration fact, not a body.body_lowering_reason_realization_member_set_aside: transport, service-levelconfig(it binds the transport's endpoint and authentication; parsed since G0 grammar: service-level config blocks over v1's closed field set #12286), exit, response and mock_response. These are realization per DESIGN §3.body_lowering_reason_interface_member_unmodeled:readonly/idempotent/hermetic, plus an io field'sfrom "key"/= defaulttail. These ARE interface facts, and they rank for modeling on the new RFM rowservice_interface_member_has_no_carrier, whose trigger is a typed operation-modifier carrier.BodyLowering; there is no reason scan). The lowering builds its set-aside population as a typed list (ServiceSetAside). At census grade (normalize_census, whose carrier has no route past the symbol index) the service lowers, with each member as a located advisory. On every other routebody_lower_service_declREFUSES the service asbody_lowering_reason_service_realization_unreachable, with each member's own located diagnostic pending, so no stage can assume a default transport. That cause has acompile_door_cause_ownershiprow.normalized_tree.dagis unchanged by this PR.body_lowering_reason_service_member_unread), and an unreadable name retains the shell. An operation that declaresinput(oroutput) twice refuses located asbody_lowering_reason_service_io_block_repeated. A service that declares an operation name twice refuses at the second declaration asbody_lowering_reason_service_operation_repeated, rather than as an unlocatedpost_normalize_not_well_formedat the module root. The first full gen-two census found exactly that shape indag/extdeps/bmc/http.dag, whereGetManageris declared twice. The source fix is its own PR.v2.extdeps.languages.dag):io_blockis split intoinput_block/output_block. A literal terminal is captured by token class alone, so one io_block over a choice of the two words could not say which one it matched. The production identity now carries that.Declared frontier: the service name
The name is ONE label carrying the whole declared spelling (
shell.Find), not a per-segment spine. A spine collides at the module level:dag/extdeps/shell.daghas 16 services undershell, and 9 other files share a prefix. Fixing that needs a prefix merge innamespace_graft, which is load-bearing.The cost: a dotted label hides its named parts (DESIGN §2), and a dotted reference to it does not resolve. Trigger: v2 resolving service CALLS. At that point the spine plus the graft prefix merge becomes required, and this label migrates in one transition. This is recorded on the RFM row.
Evidence
v2.test.claim.normalize.service_declaration_lowering: 10 claims, all PASS locally. Each runs from a supplied token stream and stays within the 72,300-step new-witness budget (38k–56k eval steps). Three fidelity claims pin each supplied stream to what the real tokenizer produces.m.'a.P'.R;s.F,s.E, the shell.dag shape) both admit with distinct labels;v2.test.parse.g0_service_decl_parse_probe: the old route claim ("a parsed service is refused for retention") flipped, as intended. Per §4b(4) it is kept as two permanent controls: an empty service is admitted, and a transport-only service is refused by full normalize asservice_realization_unreachable. All 19 claims in the file PASS locally.Real file: an interpreter census of the real
dag/extdeps/access/posix_effective_principal_read_op.daggives ADMIT, realization=3, unmodeled-interface=5.Corpus-wide counts over the 110 non-test service files are pending. An interpreter sweep is running and I'll post the result as a comment.
Native route (srv1, head 5269897): gen-one
emit --entry v2.compiler.compilegets the census pastposix_effective_principal_read_op.dagand every other service file ahead of the next wall. Neither service-levelconfignor any other service file is the first wall. The new fatal isbody_lowering_reason_call_argument_unreadatdag/examples/weather/weather.dagbytes 1015..1016: a fn literal passed as a call argument (#12210's class), withparse_grammar_choice_overlap_residuein the chain. That is outside this PR.🤖 Generated with Claude Code