Skip to content

Split the checkpoint row's two spelling roles: what a reference renders and what a declaration grounds in - #8788

Merged
briansrls merged 8 commits into
mainfrom
session/sharp-carp-197-checkpoint-split
Aug 21, 2026
Merged

briansrls merged 8 commits into
mainfrom
session/sharp-carp-197-checkpoint-split

Conversation

@briansrls

@briansrls briansrls commented Aug 21, 2026 •

Copy link
Copy Markdown
Contributor

Provenance note. This branch was attached to a work item whose (immutable) title names the lambda/bare-name-roster investigation that preceded this change; the dashboard seeded that title onto the PR on attach and it has been corrected. Nothing here touches emit_typed_call or that roster — that half landed separately as #8772, and its measured null is what re-diagnosed this half as a two-role defect in the checkpoint row rather than a second bare-name bypass. If the seeded title reappears, this diff is the authority, not the title.

Summary

A TypeCheckpoint row was answering two different questions with one field, and the six facts of this change are:

  1. A row now carries two spelling roles — target_type, what a reference renders, and grounding_type, what a declaration's right-hand side is grounded in.
  2. Across all 37 rows in five language tables, Rust's String is the only row where they differ (String vs std::string::String) — the one self-referencing shape.
  3. The compensating item_text == "String" arm in emit_typed_item is deleted, not guarded, along with its helper.
  4. Production callers are three reference readers and one grounding reader, each naming its question through rust_scalar_checkpoint_reference_base / _grounding_base over one shared identity-keyed body.
  5. The shared helper stays public and reachable, which is why the claim stops at mechanically preventable rather than structurally impossible.
  6. The stage0 mirrors were regenerated, not hand-written: the sequence reached a repeatable candidate with no hand edits to any generated file.

Test plan

  • Witness rows, green by execution. Three rows added to v1.tests.claim.checkpoint_identity_keying_witness_test, run via cargo test -p v1-compiler: test result: ok.
  • Discriminating RED. With rust_scalar_checkpoint_grounding_base flipped to read target_type, the run fails at the grounding assertion specifically while both reference assertions before it still pass. Collapsing the split reds exactly one row, whichever field survives.
  • Caller census. The shared body's only direct callers are the two wrappers, in the authority and in the emitted seed alike.
  • Regen. claim_executor --required-regen: round 1 first_generation_equal=false, adopt candidate, rebuild, round 2 true. All eight changed mirrors md5-verified byte-identical to what the emitter produced.
  • CI: witnesses (parse, regen, floor).

Coverage boundary: the witness rows execute, but they are not enrolled

Stated here rather than left implied, because the obvious reading of a green run is stronger than the instrument.

The required-CI invocation is claim_executor --required-ci --source-root dag --source-root src/v2. The three rows this PR adds live in src/v1/tests/claim/, outside that envelope. They were run directly during authoring — green, plus the discriminating RED — and that is evidence the assertions hold; it is not evidence that CI runs them. So §4b(4), which keeps the discriminating RED enrolled as the executing evidence that a rung stays real, does not yet hold for these rows. Trigger: src/v1 witnesses reachable from the required-CI envelope.

Re-homing them to the dag/ sibling is not the fix and was not done. These rows import v1.compiler.emit_rust and read the function's answer directly; the dag/ sibling can only observe the emitter black-box through compile_dag_rust_emit_check, which sees rendered output rather than the function's answer. Moving them would trade a real instrument for an enrolled weaker one.

Related, and the reason this section exists: a floor pass covers the routed roster, not the discovered one — this branch's run reported offered=11609 routed=10253, so 1362 discovered sites are declined by home policy before the fold sees them. A green floor is a claim about the witnesses that ran.

Why the two questions cannot share one field

The recorded framing of this gap was wrong, and correcting it is the change. checkpoint_table_bypasses_identity_note called the String declaration-site arm a second bare-name bypass to delete. Deleting it alone emits pub type String = String; — self-referential — because the checkpoint's target_type for String is the bare spelling and the declaration site used it as the alias's right-hand side. The arm was compensating, not bypassing.

So the defect was not a wrong value in the row; it was one field carrying two roles. Whichever spelling it held, one consumer was wrong, and the arm was the visible cost of making it try. (Earlier revisions of this description called that an arity defect. That word already means type-parameter count in this exact area — rust_checkpoint_scalar_arity_note sits a few lines away — so the durable wording is two spelling roles, or two projections.)

Two named entry points, not one function with a position argument: an argument is a discriminator a caller can get wrong, and nothing stops the next caller passing the one that compiles rather than the one that is true. Naming the question makes the wrong selection require visibly calling the wrong function.

The honest rung, and what a green regen does not establish

The class sits at mechanically preventable, not structurally impossible, and an earlier revision of the annotation claimed otherwise. rust_scalar_checkpoint_spelling is reachable and carries the grounding Bool — exactly the discriminator the two surfaces exist to remove — so a caller can still select the wrong spelling by calling the shared body directly, and nothing refuses it. What the entry points buy is that every production caller goes through a question-named surface: a fact about the current call graph, not a property of the API. The caller census is the standing evidence that keeps that claim checkable rather than merely modest.

Ceiling, not a defect left unfixed: .dag has no function-privacy concept, so the shared body cannot be made unreachable however it is written — measured on the emitted emitter: 665 pub fn, zero non-pub, and no privacy keyword in the parser. Next-rung trigger: a module-private function boundary in the language.

A note on the regen evidence, because the obvious reading of it is wrong: first_generation_equal=false beside fixed_point_equal=true establishes only that emission is repeatable, not that it is correct — a deterministic wrong emitter reproduces its wrong output forever. What those two readings together rule out is unstable or non-converging emission; correctness is established by the witness execution and the discriminating RED above, never by a green regen.

Pre-empting the redundancy objection: the field is not optional, and must not become so

Eight of the nine Rust rows carry grounding_type identical to target_type, and every other language table is identical throughout. That reads as redundancy, and the natural suggestion is to make the field optional and default it to target_type when absent. That suggestion undoes this change and should be declined.

A default is a rule about what a row means when it stays silent — which is precisely the compensation this PR deletes. It does not remove the ambiguity, it moves it from the declaration site into the row's absence arm, where it is harder to see and nothing executes over it. The eight coincidences are not one fact written twice; they are two facts that happen to agree for those types. The value of the full field is that the next name colliding with its own host spelling cannot be added without someone deciding both answers. Optional-with-default lets exactly that name be added silently and wrong.

The numeric witness row exists for the same reason: it states by execution that grounding equals reference where the two coincide, so the coincidence is asserted rather than assumed — which is the honest version of what a default would have papered over.

…g spelling are two facts

emit_typed_item's type-alias arm special-cased `item_text == "String"` and emitted
`pub type String = std::string::String;` unconditionally, never consulting the
identity-keyed authority every reference already routed through, so a module
declaring `type String = FreeMonoid<Char>` could disagree with its own references
inside one emitted file.

The recorded framing called that a second bare-name bypass to be deleted. It was
not. The arm was COMPENSATING: deleting it alone emits `pub type String = String;`,
self-referential, because the checkpoint's target_type for String is the bare
spelling and the declaration site used target_type as the alias's right-hand side.
The defect was the ROW'S ARITY -- one field answering two questions, what a
REFERENCE renders and what a DECLARATION is GROUNDED IN. Whichever spelling the
single field carried, one consumer was wrong.

TypeCheckpoint now carries both spellings. rust_scalar_checkpoint_reference_base
and rust_scalar_checkpoint_grounding_base are two named entry points over one
shared identity-keyed body, so a caller states which question it asks rather than
passing a position argument a caller can get wrong; three reference callers read
the reference spelling, the single declaration-RHS caller reads grounding, and the
arm is deleted rather than guarded. Grounding differs from reference only where
dag_name == target_type -- the one self-referencing shape -- which is Rust's String
row alone across all 37 rows in five language tables.

EVIDENCE BY EXECUTION, with a discriminating red. Three rows land in
v1.tests.claim.checkpoint_identity_keying_witness_test: the same body called with
the same name and the same decl_file must answer `String` at a reference and
`std::string::String` at a declaration -- a pair no single field can satisfy -- plus
a numeric row pinning grounding to the reference spelling where the two coincide,
so the new field is not read as a second authority free to drift row by row.
GREEN: all rows pass. RED CONTROL: with the grounding entry point flipped to read
target_type, the run fails at the grounding assertion specifically while both
reference assertions still pass. Collapsing the split reds exactly one row,
whichever field survives.

WHAT THIS DOES NOT CLOSE, filed as its own row rather than folded in:
lookup_checkpoint's first arm answers straight from the bare-name table when
decl_file is empty, so identity is not consulted at all at any site that never
threads it. The split governs what a row may SAY once identity is known; that
bypass governs whether identity is consulted. gunbc.empty_decl_file_checkpoint_bypass
states it at mitigatable, lists the one instance that was measured rather than
reasoned, and declares its population UncountedNoSweepRun with no estimate offered.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review August 21, 2026 17:40
@gunbai-bot gunbai-bot Bot changed the title Bare-name roster root, declaration-consulting half (NOT held by the contains ruling): emit_typed_call binds a lambda argument's params only if the callee's bare name is one of four literals - consult the resolved callee from lookup_item instead Split the checkpoint row's arity: what a reference renders and what a declaration grounds in are two facts Aug 21, 2026
Brian Searls and others added 3 commits August 21, 2026 19:32
…body is reachable

The annotation over the two entry points claimed the discrimination lives in the
structure rather than in author care, and that a new caller must say which
position it is in before it can compile at all. Neither holds, and the overclaim
is corrected in place rather than softened.

rust_scalar_checkpoint_spelling is reachable and carries the grounding Bool --
exactly the discriminator the two surfaces exist to remove -- so a caller can
still select the wrong spelling by calling the shared body directly, and nothing
refuses it. What the entry points buy is that every PRODUCTION caller goes
through a question-named surface, which is a fact about the current call graph
rather than a property of the API.

RUNG: mechanically preventable, not structurally impossible. The evidence that
makes the narrower claim checkable rather than merely modest is the caller
census -- the shared body's only direct callers are the two wrappers, in the
authority and in the emitted seed alike, so a third direct caller appearing is
the regression the annotation now makes visible.

CEILING RATHER THAN A DEFECT LEFT UNFIXED: .dag has no function-privacy concept,
so the body cannot be made unreachable however it is written -- measured on the
emitted emitter, 665 pub fn and zero non-pub, against a parser with no privacy
keyword. NEXT-RUNG TRIGGER: a module-private function boundary in the language.

Also states what target_type now means and nothing broader. It is the
reference-position spelling, not the general answer to what a type is in the
target; the name survives only because renaming reaches every target table, so
it is the one-name-two-meanings shape this split removed from the field's VALUE
still standing in its NAME, and a reader must not take it for the universal
answer.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ritten approximation

required-regen reported first_generation_equal=false with drift confined to
v1_compiler_emit_rust.rs and v1_tests_claim_checkpoint_identity_keying_witness_test.rs
-- the two surfaces this branch changed -- while regen-fixed-point reported TRUE.
Read together those two facts are the diagnosis, not two symptoms: a wrong
emitter fails to reproduce ITSELF, so a candidate that is its own fixed point is
internally consistent and merely differs from what is committed.

The mechanism is the emitter emitting itself. The committed mirrors were produced
by the emitter as it stood BEFORE this branch, so they cannot contain the output
of the emitter as it stands after; the converging sequence is install candidate,
REBUILD, regenerate. Measured: round 1 false, adopt, rebuild, round 2 TRUE.

The bytes are adopted wholesale rather than hand-patched toward green. Editing a
generated .rs to make the comparison pass produces a hybrid no generator emitted,
and it survives exactly one regeneration before returning. Verified by md5 that
every one of the eight files installed here is byte-identical to what the emitter
produced, rather than merely close enough to apply -- an earlier attempt to carry
the change across as a diff was refused, because a diff computed on the remote
runner is relative to the RUNNER'S base commit and not to this branch.

What the emitter writes that I had approximated: the two checkpoint imports as
one merged use, the narrowed ceiling note, and `grounding.clone()` at the field
selection.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot gunbai-bot Bot changed the title Split the checkpoint row's arity: what a reference renders and what a declaration grounds in are two facts Split the checkpoint row's two spelling roles: what a reference renders and what a declaration grounds in Aug 21, 2026
Brian Searls and others added 4 commits August 21, 2026 21:11
…ter count here

The defect these carriers describe was being called an ARITY defect, and that
word is taken. In this exact area it already means type-parameter count --
v1.compiler.emit_rust carries AliasDeclArityVerdict and
rust_checkpoint_scalar_declared_arity_guard_note, the latter a few declarations
from the text doing the borrowing. A durable artifact that reuses a live term for
a different meaning is a nickname pointed the wrong way: it does not create a
second name for one concept, it creates a second concept under one name, which
is worse to read and impossible to grep apart.

The claim is unchanged -- one field was carrying two spelling roles, what a
REFERENCE renders and what a DECLARATION is grounded in -- and both carriers now
say so in those words, each stating the collision it is avoiding so the next
author does not reintroduce the term as an improvement.

The emitted mirror is regenerated rather than hand-edited: round 1 false, adopt,
rebuild, round 2 true, one file changed, md5-verified byte-identical to what the
emitter produced.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…g a side

The only conflict was checkpoint_table_bypasses_identity_note, edited on both
sides, and the two edits are about DIFFERENT halves of the same authority:

  - this branch closed the DECLARATION-site gap the note recorded, by splitting
    the row's two spelling roles and deleting the compensating arm;
  - main added royal-dove-436's REACHABILITY CORRECTION: a String-spelled
    reference in TYPE position never reaches lookup_checkpoint at all, because
    six renderers in this module short-circuit ahead of it.

Both survive, and a bridge paragraph states how they narrow each other -- because
either read alone overstates its half. The split makes the declaration site able
to consult the identity-keyed authority; the reachability finding says the
reference site is not yet reached. For String that is one authority with two
different reasons its consumers do not see it, not one gap: the declaration half
is closed and the reference half is unreachable. The split is therefore stated as
closing the arm it deletes, never as making every String position identity-keyed.

Taking either side wholesale would have silently deleted the other session's
measured finding, which is the failure mode a generated-artifact conflict makes
easy and a prose conflict makes invisible.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Prompted by a coverage correction from deep-ant-102: a floor pass covers the
ROUTED roster, not the DISCOVERED one (11609 offered, 10253 routed on this
branch's run), so "the floor passed" is a claim about the witnesses that ran.
Checking what that meant for THIS change surfaced something sharper than the
declined counts.

The required-CI invocation is
`claim_executor --required-ci --source-root dag --source-root src/v2`. The three
rows this branch added live in src/v1/tests/claim/, OUTSIDE that envelope. They
were executed directly during authoring -- green, plus a discriminating RED that
fails at the grounding assertion specifically while both reference assertions
still pass -- but direct execution is evidence the assertions HOLD, never
evidence that CI runs them. So DESIGN 4b(4), which keeps the discriminating RED
enrolled as the executing evidence that a rung stays real, does not hold for
these rows yet.

Declared here rather than left to be rediscovered, per 4b(2)'s no-untracked-stall
rule, with the trigger named: src/v1 witnesses reachable from the required-CI
envelope. Re-homing them to the dag/ sibling is explicitly NOT the fix and is not
done: these rows import v1.compiler.emit_rust and read the function's answer,
while the dag/ sibling can only observe the emitter black-box through
compile_dag_rust_emit_check. Moving them would silently downgrade what they
discriminate -- trading a real instrument for an enrolled weaker one.

Annotation only, so no regeneration cycle.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…at was refused

The trigger declared one commit ago -- src/v1 witnesses becoming reachable from
the required-CI envelope -- names an event the repo has already measured and
ruled out, so the row would have sat waiting on something that will not happen.
That is the untracked stall 4b(2) forbids wearing a trigger's clothes.

Corrected on two axes, per deep-ant-102 and verified against the carrier:

MECHANISM. These rows are not merely outside a live envelope. The consumer that
ran v1 claim entries -- the scoped witness batch, the only ScopedWitnessBatch
instance that ever existed -- was DELETED 2026-08-15
(gunbc.ci_layer_roots v1_claim_scoped_witness_batch_deleted_note, which carries
triage receipts for seventeen other v1 witness files retired for the same root).
Enrolled against a removed consumer is worse than outside a live envelope:
nothing refuses, because nothing is asking.

TRIGGER. Widening the envelope was refused with a re-measured reason (2026-08-19,
after the original went stale). The blocker is no longer cost but NAME
RESOLUTION: src/v1 and src/v2 collide on the LAST SEGMENT in twelve places, so
admitting src/v1 breaks bare cross-module references that resolve today by
pool-membership coincidence -- 532 typed diagnostics, 525 in src/v2, 7 in
dag/test, ZERO in src/v1. The damage is in what is already there. The real
condition is references binding BY CONTAINMENT, whose current vehicle is the
namespace cut (gunbc#8282).

Annotation only; no regeneration.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@briansrls
briansrls merged commit 183e50a into main Aug 21, 2026
1 check passed
@briansrls
briansrls deleted the session/sharp-carp-197-checkpoint-split branch August 21, 2026 23:43
gunbai-bot Bot pushed a commit that referenced this pull request Aug 22, 2026
…ually and restore two silent losses

MY OWN SURVEY HAD SEEN THESE AND MY CLASSIFICATION ABSORBED THEM. I reported "41
declarations on main and absent here", explained the bucket by naming four members
(class_b_import_closure_overlay, declared_import_closure_binding,
compile_clean_diagnostic_policy and their witnesses), and let the other thirty-seven
inherit that verdict. A count with four named members explains four; the rest are assumed.

Re-run at declaration grain against current main with the instrument corrected -- an
alias RHS is not a declaration, and qualification is normalized before diffing, which
takes a false 301 down to a real 107 -- and every member enumerated:

  95  import machinery the cut deletes by design (12 wholly-absent modules plus
      v1.compiler.resolve's 10 import-resolution decls and infer_env's 4 listed-import
      predicates), each now individually accounted rather than bucket-explained
   3  main's #8788 rust_scalar_checkpoint_* -- arriving in this merge
   5  deliberate branch decisions with their own commits (v2.std.collection.List
      de-forked as a nickname for std.types.List; ownership_movable retired with a receipt)
   2  REAL SILENT LOSSES, restored here:
        test.claim.runner_slot_provision.fixture_five_slot_deploy  (#8401, ancestor)
        test.claim.roadmap_belt_actuate_witness.live_tree_disposition  (#8804, ancestor)
   2  gunbc.non_fold_residue class_b rows, by design

Both losses came from take-one-side-whole resolutions on commits ALREADY in the branch,
so no merge would ever have re-offered them. Also reverted 141 further in-string
qualifications this pass introduced.

regen: exit 0, first_generation_equal=true, 131 modules.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Aug 24, 2026
…w was inert, now it refuses (#9096)

`copy_hand_maintained_support` iterated HAND_MAINTAINED_STAGE0_FILES and
HAND_MAINTAINED_STAGE0_DIRS with a bare `if exists` / `if is_dir` and no else, so a
declared crate-layout row naming a path that is not on disk was silently skipped. That
is an absorbing fallback in DESIGN §5's exact shape: the failure arm widened (copy what
resolves, ignore what does not) instead of refusing, so the deficit's frequency was zero
by construction.

WHAT IT MADE INERT, with a live specimen. On integration/namespace-cut,
dag/gunbc/stage0_crate_layout_generated.dag carries a stray `"rs",` row between
"shared_typecheck_store.rs" and "recorded_fixture.rs" — 37 entries against main's 36 —
introduced by merge commit ebda683 ("Integrate main (#8788)"), where a line split and
its tail survived as its own list element. Nothing named `rs` is on disk, so the copy
loop skipped it without a word, and because the emitted mirror faithfully reproduces the
corrupted authority, regen's fixed point reports green over it (that branch's own
6d9f239: "regen fixed point green (exit 0)"). Regen compares mirror to authority and
has no operand for whether the authority is right — but the authority CAN be joined to
the tree, every declared basename either resolves or does not, and this is the one place
that join already happened and its result was discarded.

BOTH LOOPS, and the second is not a copy of the first. The file loop's absence is absence
from disk, which is never legitimate. Note the contrast with `verify_hand_maintained`,
which iterates the same list and also continues on absence: its absence is absence from
the EMITTED population, the ordinary case for 35 of the 36 entries. Two functions, one
list, two different absences, and only one of them is normal.

EVIDENCE, per DESIGN §5 — green by execution plus a discriminating red. The new test
plants every declared row on disk and accepts, then removes exactly one file and one
directory, so control and refusal differ by a single row and the refusal must name it.
Verified red without the wall by two independently constructed controls (the impl arms
removed; and origin/main's body carrying only the new test), both failing with "a
declared row naming no file must refuse". Verified against main's live population first:
all 36 declared files and both declared dirs resolve on origin/main, so the wall is green
on main by measurement rather than by assumption.

Rung: mechanically preventable — `basename: String` and `List<String>` throughout, so
`"rs"` is a well-formed inhabitant and no type error is available. Next-rung trigger: a
Stage0Filename carrier minted only from a path that resolves, which would make the corrupt
row unwritable rather than refused.

v1 admission: the seed is semantics-frozen and maintenance-active, and this serves the v2
self-host program — a corrupt crate-layout authority silently accepted is a self-host
correctness gap. Same class as the bare-`Err(_)` arms swift-lynx-327 is converting in
gunbc#9087, ~14k lines away in this file.

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant