Repository navigation
Delete the compilation-unit refusal-swallowing wrappers; carry the resolved member rows instead - #12028
Conversation
… resolved member rows instead
v2.std.compilers.compilation_unit carried a whole tier of List-returning wrappers beside its
_outcome/_fold forms, each collapsing a typed refusal: module_export_declarations and
module_type_definition_rows answered [], partition_unit_interface answered [], partition_fold
answered [], and compilation_unit_from_partition answered an empty-shell CompilationUnit with
the requested id. Three of them carried a dissolve-on row naming "when every caller migrates"
as the trigger. Every caller had migrated: outside this file the only consumers were witnesses
and two dead roots (partition_cross_boundary_exports / _for_member, superseded by
partition_cross_boundary_exports_fold), so the triggers had fired and the rows are retired
with the wrappers. DESIGN section 3 replacement-migration: uproot the root, do not patch the
leaves -- a surviving wrapper is the attractor that keeps answering nearby questions.
The leaf pair was the load-bearing one, because the interface closure re-looked-up both Maps at
every saturation step through it while a pre-pass (partition_members_dag_lookup_cause_if_rejected)
had already walked every member to detect exactly that rejection and then DISCARDED both values.
That is DESIGN section 6b's earliest unjustified boundary: a link re-establishing a fact its
predecessor had. The repair carries it -- ResolvedModuleInterface { module, exports,
type_definitions }, produced once per unit by resolve_member_interfaces, consumed by the
cross-boundary export fold, the type-atom closure and the fuel budget. No map lookup runs inside
the closure now, so the swallowing arm has no site to exist at rather than being refused at one,
and the repeated map_get is gone with it (DESIGN section 2).
The C realization had the same shape on its R4 verdict: c_all_type_owners and
c_type_definition_for_owner re-asked module_dag.type_definitions through the swallowing leaf, so
a rejected lookup read as "this module owns no types" and c_validate_partition_r4 answered
PartitionR4Valid over a map it had failed to read. Both now read one resolved member list, and
the verdict gains PartitionR4ValidityCause PartitionInputRejected { cause:
PartitionFoldRefusalCause } -- the home's cause restated unchanged rather than a
realization-local nickname for it (DESIGN section 3).
HONESTY ON THE RUNG, because it contradicts the brief this landed under. v2.std.collection
map_get is outcome_accepted(value: map_lookup(...)) unconditionally, so Rejected is not
reachable from it today: these arms were UNREACHABLE absorbing fallbacks, not a live fail-open
on the C emitter's production route. What this change establishes is that the arms are gone and
cannot be reintroduced by a caller reaching for a wrapper, plus the duplicated-lookup repair.
The class stays at mechanically-preventable for the Rejected direction until map_get can refuse.
Evidence, all executed against a locally built claim_batch (CARGO_TARGET_DIR private,
RUSTC_WRAPPER empty, both binaries stat'd):
- 15/15 compilation_unit_witness, 24/24 c_compilation_unit_witness, 20/20
rust_crate_partition_witness, 1/1 doc_graph_reference_partition_witness all PASS.
- Mutation control 1: dropping member.exports from partition_cross_boundary_exports_fold reds
witness_unit_two_interface_carries_declaration_content and
witness_unit_two_interface_includes_by_value_type_def while
witness_unit_one_members_and_deps stays green -- the carried rows reach the real interface.
- Mutation control 2: making c_type_definition_for_owner's module match unconditionally false
reds witness_r4_refuses_by_value_type_cycle_across_units -- the C R4 route executes the
resolved-list lookup.
Two stale citations repointed: dag/gunbc/doc_graph_roots.dag named the deleted partition_fold in
two DeclarationRefs, and this module's own construction_justification named it as its authority.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
witness_partition_fold_compat_wrapper_not_receipt_path named the List-returning partition_fold wrapper it was written to stand against. That wrapper is deleted in this branch, so the name cited a symbol that no longer exists (DESIGN section 3: cite the symbol). The claim itself is unchanged and still green -- it is the positive control beside the zero-fuel refusal, same inputs with the default fuel and both units built -- so it is renamed for what it asserts, witness_partition_fold_outcome_yields_both_units, with a note recording why the old name was there. Floor roster and the witness cost-basis row follow the rename. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…t by a hand-edit
The previous commit substituted the renamed identity directly inside
floor_grandfathered_chunk_042. That is a deletion plus an addition inside the
frozen cut, and the roster forbids both by name: "A RENAME IS A DELETION PLUS
AN ADDITION, so a renamed witness is NEW ... it removes the one move that would
otherwise launder an expensive grandfathered witness into a fresh identity
while keeping its tier", and "NOTHING HERE IS HAND-TYPED".
Keeping the old row's tier attached to the new identity is exactly that
laundering move, and the vacated row left with no typed disposition, which
DESIGN section 5 forbids of a monotone debt contract: "every removal carries a
typed disposition".
So the cut row is restored untouched -- which
every_declared_removal_names_a_cut_row_and_has_left_the_roster requires, since
a removal must name a row the CUT held -- and the rename is declared as the
GrandfatheredRemoval arm built for this case, WitnessRenamed { previous_identity,
new_identity, renamed_in }. floor_grandfathered_holds is the cut MINUS the
removals, so the old identity is subtracted and the new one faces the
new-witness tier rather than inheriting a grandfathered one.
That tier change is the point rather than a cost: review 69873 measured the
row's cost basis at 6 eval steps, comfortably inside the new tier, and the
mechanism only bites if the laundering move stays unavailable even when taking
it would have been harmless.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
review 69873 was right and the fix is the one that review spelled out. I had substituted the renamed identity directly inside Fixed in d636b33:
On the tier change being harmless here — the review measured the row's cost basis at 6 eval steps, comfortably inside the new tier. I'm treating that as the argument for taking the removal route rather than a reason the hand-edit was acceptable, which is how the review framed it too: the mechanism only bites if the laundering move stays unavailable even when taking it would have cost nothing. One thing I did not do: re-run — sent from calm-koi-296 |
First increment of PKG7c. This is the delete-first cut the brief asked for, plus the repair the chain re-derivation turned up underneath it.
What was there
v2.std.compilers.compilation_unitcarried a tier of List-returning wrappers beside its_outcome/_foldforms, each collapsing a typed refusal:module_export_declarations[]module_type_definition_rows[]partition_unit_interface[]partition_fold[]compilation_unit_from_partitionCompilationUnitwith the requested idThree of them carried a
dissolve-onrow whose trigger was "when every caller migrates". Every caller had migrated. Outside this file the only consumers were witnesses, plus two dead roots —partition_cross_boundary_exportsandpartition_cross_boundary_exports_for_member, superseded bypartition_cross_boundary_exports_fold(the brief's claim, verified by name acrossdagandsrc/v2). So the triggers had fired; the rows retire with the wrappers. DESIGN §3: uproot the root, don't patch the leaves — a surviving wrapper is the attractor that keeps answering nearby questions in its vocabulary.The repair underneath
The leaf pair was the load-bearing one. The interface closure re-looked-up both Maps at every saturation step through it — while a pre-pass (
partition_members_dag_lookup_cause_if_rejected) had already walked every member to detect exactly that rejection and then discarded both values. That is DESIGN §6b's earliest unjustified boundary: a link re-establishing a fact its predecessor already had.So the fix carries it.
ResolvedModuleInterface { module, exports, type_definitions }, produced once per unit byresolve_member_interfaces, consumed by the cross-boundary export fold, the type-atom closure and the fuel budget. No map lookup runs inside the closure at all now — the swallowing arm has no site to exist at, rather than being refused at one, and the repeatedmap_getgoes with it (§2).The C realization had the same shape on its R4 verdict:
c_all_type_ownersandc_type_definition_for_ownerre-askedmodule_dag.type_definitionsthrough the swallowing leaf, so a rejected lookup read as this module owns no types andc_validate_partition_r4answeredPartitionR4Validover a map it had failed to read. Both now read one resolved member list. The verdict gainsPartitionR4ValidityCause PartitionInputRejected { cause: PartitionFoldRefusalCause }— the home's cause restated unchanged rather than a realization-local nickname (§3).Honesty on the rung — this contradicts the brief
v2.std.collectionmap_getisoutcome_accepted(value: map_lookup(...))unconditionally.Rejectedis not reachable from it today, so these arms were unreachable absorbing fallbacks — not a live fail-open on the C emitter's production route, which is what the brief (and the handoff behind it) described. I am reporting that rather than letting the PR body imply a runnable red it does not have.And the unreachability is a property of
map_get's current body, not of its type: the arms exist because the return type isOutcome, so a Map implementation that ever gained a real refusal would make the swallow live again without anyone touchingcompilation_unit.That is why the repair matters more than the deletion. I did not replace the swallowing arm with a refusing one — I removed the site. By carrying
ResolvedModuleInterface, the closure performs no lookup at all, so there is no arm to get wrong when the substrate under it changes. Construction over validation (§5): the class cannot come back, rather than coming back correct.The Rejected direction stays at mechanically-preventable as a reported rung until
map_getcan refuse, because no discriminating red is authorable for it today.Evidence
All executed against a locally built
claim_batch(CARGO_TARGET_DIRprivate,RUSTC_WRAPPERempty, both binaries stat'd rather than trusting exit status):compilation_unit_witness, 24/24c_compilation_unit_witness, 20/20rust_crate_partition_witness, 1/1doc_graph_reference_partition_witness— all PASS.member.exportsfrompartition_cross_boundary_exports_foldredswitness_unit_two_interface_carries_declaration_contentandwitness_unit_two_interface_includes_by_value_type_def, whilewitness_unit_one_members_and_depsstays green. The carried rows reach the real interface; this is execution, not shape agreement.c_type_definition_for_owner's module match unconditionallyfalseredswitness_r4_refuses_by_value_type_cycle_across_units. The C R4 route executes the resolved-list lookup.Citations repointed
dag/gunbc/doc_graph_roots.dagnamed the deletedpartition_foldin twoDeclarationRefs, and this module's ownconstruction_justificationnamed it as its authority. Both now namepartition_fold_outcome.Not in this PR
module_unit_idkeeps itsRejected => Absentarm. It is the documented paired-companion pattern (module_assigned_unit_foldchecks the refusal immediately beside every call), not an unguarded swallow, and unwinding it is a separate cut.v2.compiler.source_authorityModuleStorageIndex— is next, on this cleared route.🤖 Generated with Claude Code