Skip to content

Model the exact Symbol-to-Rust representation binding and eliminate bare String capture - #9689

Merged
gunbai-bot[bot] merged 10 commits into
mainfrom
session/lively-seal-506
Aug 30, 2026
Merged

gunbai-bot[bot] merged 10 commits into
mainfrom
session/lively-seal-506

Conversation

@briansrls

@briansrls briansrls commented Aug 29, 2026 •

Copy link
Copy Markdown
Contributor

Part of #9664.

E0308 does not move in this PR. The ~2400-site capture subset empties only when XL-0B threads DeclarationRef into the checkpoint-spelling callers of 05_emit_rust.dag and asks rust_lookup_exact_binding first; this PR lands the authority, the deletion, the verdicts and the acceptance roster that commit is measured against. Until then, any live caller that renders a reference to v2.std.node Symbol through the spelling-keyed arm of type_realization_decision hits a loud, typed refusal (line-stop), not the prior Realized{String} and not a silent fallback — the seed's generated modules carry no such reference (measured: only hand-retained pilot files spell it), and on the freeze emit path that refusal is the census XL-0B reads.

What

XL-0's first self-host typeck run (#9665 freeze) reported 2799 refusals; ~2400 were one defect: v2.std.node type Symbol (opaque) was projected by the bare-name rust_type_checkpoints row to the bare token String, and every module also importing v2.std.text { String } (structural FreeMonoid<Char>) captured that token via its use-line — so fn f(identity: Symbol) expected Rc<im::Vector<i64>> while callers passed the host string. Two independent faults in one row: keyed on a spelling, and carrying a spelling a use-line can shadow. Both are closed here at the authority layer (DESIGN §2/§3, model before implement).

Model

  • std.target_representation — the three identities one TypeCheckpoint row fused, separated by owner: SourceTypeTargetBinding<R> (exact DeclarationRef → representation, corpus-owned), RepresentationSpelling<R> (representation → fully qualified reference/grounding spelling, target-owned), ExactBindingResolution (Resolved | Absent | Ambiguous | SourceIdentityUnavailable — no bare-name fallback; only Resolved yields a table spelling), and CheckpointRowDisposition (MigratedToExactBinding | ProvenUniqueKernelBinding | StillBareNameDebt).
  • extdeps.languages.rust.representation — RustRepresentation and its realizations, fully qualified (std::string::String, std::vec::Vec<u8>, …). RustSymbolNewtype / RustInternedSymbol are representable but carry no realization row, so a binding to either refuses at spelling time. rust_exact_type_checkpoint synthesizes the TypeCheckpoint the emitter and std.reference_realization already consume.
  • gunbc.rust_source_type_bindings — the exact rows (v2.std.node.Symbol → RustStdString, plus every declaration the bare table answered for), a verdict on every bare row (Symbol migrated + deleted; String/Bool/Unit proven-unique kernel with the shadowing-identity proof; Int/Float/Bytes/Secret/Json declared debt with capability-grain triggers), and the capture acceptance roster by declarer identity (23 declarers; instrument named, counts not transcribed).
  • std.symbol_semantics + gunbc.symbol_identity_census — consumer census at exact identity (13 rows, each citing the symbol read), the decision split in two claims — value semantics LexemeBacked (equality/order/hash/serialization by lexeme, no intern table, bijective identity seams) and nominality standing NominalityNotEnforced (the source checker admits Symbol→String/NonEmptyStr flows and the chosen representation erases them; restoration trigger = the ruled six-step chain (a)–(f), nominality true in .dag first, then by construction in the target) — and the representation ruling: std::string::String, with struct Symbol(std::string::String) the named next rung, triggered by the .dag checker distinguishing Symbol from String. Not the newtype now because the erasure is exploited at the source with the checker's blessing (content_hash_atom(value: NonEmptyStr) receives Symbols corpus-wide; v1.compiler.types types ^x as string_type): a newtype would make rustc refuse programs the source Accepts — a divergence, not a wall.
  • v1.compiler.coercion — rust_lookup_exact_binding / rust_exact_realization_decision (the exact path), and type_realization_decision now refuses a Migrated name that reaches the spelling-keyed arm without a DeclarationRef. The bare Symbol row is deleted; the kernel ^x literal never needed it (its suffix comes from the String row, matching its kernel type).

Evidence

24 witnesses executing on the remote corpus (dag/test/claim/symbol_identity_binding_witness_test.dag, src/v2/test/claim/symbol_identity_semantics_test.dag): exact resolution; another module's type Symbol receives no binding; missing identity refuses; two rows refuse as ambiguous; no realization spells the bare token; every bare row carries a verdict and migrated names are absent from the table; decision coherence (Eq/Hash/Ord law); symbol_lexeme ∘ symbol_intern_lexeme round trip, lexical equality/ordering/hash on the live substrate. Control run: restoring the Symbol row reds exactly w_migrated_names_are_absent_from_the_bare_table and w_every_bare_row_carries_a_verdict, nothing else.

Seam (agreed with bold-carp-449 / XL-0)

05_emit_rust.dag is untouched. XL-0B's first commit threads DeclarationRef (from typed_modules' module nodes, no path convention) into the checkpoint-spelling callers and asks rust_lookup_exact_binding first; the (dag_name, decl_file) arm stays as the declared residue with its own count. Acceptance is by failing-site identity on the freeze instrument: the symbol_capture_declarers subset empty, no declarer reappearing under another class. The import-collision fixture source is specified beside the witness for that instrument.

Note for the parent: Symbol in the declarer modules resolves only by namespace-only resolution (DESIGN's open thread), not a resolver defect — the identity XL-0B threads must come from the resolver's binding (Resolved { node }), not the import list.

🤖 Generated with Claude Code

https://claude.ai/code/session_016PAyJ8DfoCKPfA7NEBLZBG

Brian Searls and others added 5 commits August 29, 2026 19:36
…d Rust bindings with fully qualified spellings; the bare Symbol checkpoint row deleted

The first self-host typeck run (XL-0, #9665 freeze) reported 2799 refusals, ~2400 of them one defect: v2.std.node `type Symbol` (opaque) was projected by the bare-name rust_type_checkpoints row to the bare token `String`, and every module also importing v2.std.text { String } (a structural FreeMonoid<Char>) captured that token, so `fn f(identity: Symbol)` expected Rc<im::Vector<i64>> while callers passed the host string. Two independent faults in one row: keyed on a spelling, and carrying a spelling a use-line can shadow.

Model (DESIGN section 2/3, model before implement):
- std.target_representation: SourceTypeTargetBinding<R> (DeclarationRef -> representation, corpus-owned), RepresentationSpelling<R> (representation -> qualified reference/grounding spelling, target-owned), ExactBindingResolution (Resolved | Absent | Ambiguous | SourceIdentityUnavailable; no bare-name fallback), CheckpointRowDisposition (MigratedToExactBinding | ProvenUniqueKernelBinding | StillBareNameDebt).
- extdeps.languages.rust.representation: RustRepresentation and its realizations, fully qualified (std::string::String, std::vec::Vec<u8>, ...); RustSymbolNewtype / RustInternedSymbol representable but unrealized, so a binding to them refuses.
- gunbc.rust_source_type_bindings: the exact rows (v2.std.node Symbol -> RustStdString, plus every declaration the bare table answered for), a verdict on every bare row, and the capture acceptance roster by declarer identity (instrument: the freeze's emit + cargo check).
- std.symbol_semantics + gunbc.symbol_identity_census: consumer census at exact identity; decision LexemeBackedNominal (equality/order/hash/serialization by lexeme, no intern table, bijective identity seams); Rust representation std::string::String, with struct Symbol(std::string::String) the named next rung, triggered by the .dag checker distinguishing Symbol from String (the erasure is exploited at the source today: content_hash_atom(value: NonEmptyStr) receives Symbols with v1.compiler.types' blessing, so a newtype would refuse Accepted programs).
- v1.compiler.coercion: rust_lookup_exact_binding / rust_exact_realization_decision (the exact path, composing with std.reference_realization), and type_realization_decision refuses a Migrated name that reaches the spelling-keyed arm without a DeclarationRef. The bare Symbol row is deleted; the kernel `^x` literal never needed it (typed string_type, suffix from the String row).

Witnesses (24, all executing on the remote corpus): exact resolution, another-module Symbol receives no binding, missing identity refuses, ambiguity refuses, spellings never the bare token, every bare row carries a verdict and migrated names are absent from the table (control: restoring the row reds exactly those two), decision coherence, round trip and Eq/Hash/Ord laws on the live substrate. Renderer threading of DeclarationRef is XL-0B's first commit by agreement with bold-carp-449; the byte-level fixture is specified beside the witness for that instrument.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016PAyJ8DfoCKPfA7NEBLZBG
…match in symbol_consumer_class_blocks_decision (nfr roster)

required-regen refused with 'emitted surface has no committed mirror' for extdeps_languages_rust_representation.rs, gunbc_rust_source_type_bindings.rs and std_target_representation.rs; installed from the srv1 candidate tree along with the four drifted mirrors (lib.rs, emitted_population.rs, extdeps_languages_rust_types.rs, v1_compiler_coercion.rs) -- every changed line is the new modules' registration or the .dag change's projection. cli_run::nfr_tests::nfr_roster_receipt flagged the one wildcard arm as an unrostered non-fold residue; the match is now exhaustive over SymbolConsumerClass.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016PAyJ8DfoCKPfA7NEBLZBG
…heckpoint answer now assert its migration

coercion_rust_checkpoint_resolves_primitives and coercion_is_copy_from_checkpoint asserted Symbol -> "String" / Some(false) at the spelling-keyed arm; with the row migrated to gunbc.rust_source_type_bindings the arm answers no checkpoint, so they now assert the fall-through spelling and None -- the incumbent evidence recorded as the deletion's positive control.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016PAyJ8DfoCKPfA7NEBLZBG
…(cited-declaration gate); revert the hand edit to the generated compiler_tests.rs

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016PAyJ8DfoCKPfA7NEBLZBG
…py assertions no longer carry the migrated Symbol row (regen fixed point after the mirror install)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016PAyJ8DfoCKPfA7NEBLZBG
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review August 29, 2026 21:36
@gunbai-bot gunbai-bot Bot changed the title Symbol identity: v2.std.node Symbol / kernel String / v2.std.text.String are one concept under three names -- model the authority in std/ before XL-0 resumes (2400 of 2799 typeck errors) Model the exact Symbol-to-Rust representation binding and eliminate bare String capture Aug 29, 2026
Brian Searls and others added 2 commits August 30, 2026 01:19
…cked) and SymbolNominalityStanding (NominalityNotEnforced, six-step trigger); total consumer-evidence classifier

Per bright-ram-778's ruling on #9689: the fused LexemeBackedNominal said nominal while the source checker and the chosen representation both erase, and the coherence law never inspected text_operations_permitted_on_symbol. The value claim and the nominality claim are now two carriers, the law checks each half over its own fields, and two witnesses mutate each half alone to prove independence. The newtype trigger is the ruled ordered chain (a)-(f), nominality true in .dag first. The census states that the identity bridges support LexemeBacked and do not prove the erasure permanently correct. Review 57460: the one-true/ten-false predicate is replaced by a total SymbolConsumerEvidenceStatus classifier the census folds.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016PAyJ8DfoCKPfA7NEBLZBG
gunbai-bot Bot added a commit that referenced this pull request Aug 30, 2026
…dissolved on #9665 merging (#9705)

Every pull_request build now has ecdeb49 (or later) as its base, so base and merge
head both carry the hoist, no run can produce those six deltas, and the rows report
stale -- refusing every open PR (measured on #9689 @ bfd9524: 0 unadjudicated,
6 stale). Removed by their own dissolve-on trigger; the roster is empty and empty is
not permissive.


Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU

Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot merged commit 24fc4a3 into main Aug 30, 2026
4 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/lively-seal-506 branch August 30, 2026 02:43
briansrls pushed a commit that referenced this pull request Aug 30, 2026
…, and the required build lane gains the partition crates as the wall (#9711)

* Stage0 partition roster: the three modules #9689 added, the phantom row, and the required gate that can see them

The authority edits only; generated artifacts follow in the next commit.

- v2.workflow.rust_crate_partition: std_target_representation into the std-core
  unit, extdeps_languages_rust_representation into the extdeps-languages unit,
  and gunbc_rust_source_type_bindings into the v1-infer unit through its own
  named list, because its layer is neither the v1_compiler pipeline nor the
  extdeps one and the grouping is physical rather than nominal. Placement is
  forced by each module's own crate:: references, not chosen.
- The same authority drops std_lens_verdict, which named a file stage0 lib.rs
  deliberately does not declare (has_pub_mod false in the crate-layout
  registration), so the partition crates were compiling a module the monolith
  does not. The FILE's disposition is deliberately not settled here.
- gunbc.repo_self_build gains repo_self_build_partition_crates_command, whose
  package list is read from the partition roster rather than restated, and the
  build lane runs it beside the all-bins build. That is the executing wall for
  the E0432 class, with rustc as the oracle.
- One witness for the class a hermetic join CAN reach, with its discriminating
  RED authored as a fixture because the live corpus cannot express the refused
  state once the phantom row is gone.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RTvKD3J3pnUzXmUascawfQ

* Move the roster witness inside the required gate's prefix; convert the v1-infer count literal to an identity join

Run 33290382542 measured both of these rather than my guessing at them.

- The new witness sat at `test.claim.stage0_partition_roster_layout_join_witness`,
  which matches none of v2.workflow.required_floor required_gate_prefixes, so the
  floor discovered it, classified it DeclinedOutsideRequiredGate and never ran it
  -- while it was RED on the live corpus. A wall that reds and is declined is an
  inert lens, so the module path is part of the wall and the file now lives at
  v2.test.claim.*, which the `v2.test.` prefix admits.
- witness_v1_infer_unit_members_holds was the run's single unexpected failure:
  `(unit.members |> count) == 9`, stale the moment the roster gained a module. It
  is now an identity join between the declared roster and what came back through
  the assignment map and partition_fold, so it cannot be repaired by retyping a
  number. Its blind spot -- an error in the roster itself -- is stated in place
  and belongs to the build lane, where rustc is the oracle.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RTvKD3J3pnUzXmUascawfQ

* Sixth admission shrink: the two RequiredCiLane rows dissolved on #9698 merging -- this refuses EVERY pull request, not just this one

Not this lane's subject, taken because it stands between every branch and a
green. #9698 (fa03a01) moved BuildLane and WitnessesLane from
gunbc.required_ci_host_verdict_census to the new gunbc.required_ci_phase_roster.
The two TransitionAdmission rows that adjudicated that move were authored with
the trigger "they go STALE the moment #9698 merges and MUST be removed then" --
their own words -- and #9698 is merged, so no pull_request build can produce the
deltas they name and the phase refuses on the stale rows alone.

Measured, run 33292088803: FAILED PHASE namespace-wave-admission (0 unadjudicated
delta(s), 2 stale admission(s)), naming both rows. This branch's own namespace
delta -- the gunbc.repo_self_build -> gunbc.stage0_crate_partition_generated
import the roster fix adds -- was adjudicated ExplicitlyEvaluatedZeroDelta and
passed, so the refusal is entirely the two stale rows.

Emptying the array to &[] is the proven form: the fourth shrink (#9705) did
exactly that and shipped green. That shrink was a standalone PR and that remains
the normal shape; it rides here only because main was already red.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RTvKD3J3pnUzXmUascawfQ

* Regenerated: the partition roster, its stage0 mirror, the three crate lib.rs files, and the build lane that now compiles them

Produced by the generators, not by hand. main_wet (dag/gunbc/instruments/
generated_artifact_gate.dag) rewrote exactly two artifacts -- the generated
partition .dag and .github/workflows/witnesses.yml -- and nothing else in the
corpus moved. --required-regen then reported one drifted mirror,
gunbc_stage0_crate_partition_generated.rs, and --emit-partition-crates rendered
14 files and wrote 3: the std-core, extdeps-languages and v1-infer lib.rs, which
are precisely the three crates the roster change touches.

The emitted build step, read off the emitted bytes rather than assumed:

    run: |
      cargo build --release -p v1-compiler --bins
      cargo build --release -p v1-stage0-runtime -p v1-stage0-std-core ...

Both commands under one literal block scalar, the package list derived from the
partition roster rather than restated, so a crate added to the partition joins
the gate with no edit at the gate.

REGEN NOTE FOR THE NEXT AUTHOR: main_wet is OOM-killed on a BuildBuddy runner
under the default budget (SIGKILL, rc=137). /sys/fs/cgroup/memory.max and
memory.high are unreadable there, so memory_governor read_host_budget_bytes
falls through to MemAvailable -- which reports the HOST's memory, not the slot's
-- and caps at the 15 GiB declared slot line, which can exceed what the slot
actually has. Setting GUNBC_MEMORY_BUDGET_BYTES explicitly (10 GiB used here,
peak RSS 7.7 GiB) makes it complete. The kill is silent through a `cmd | grep |
tail` pipeline, because the pipeline reports the last stage's status.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RTvKD3J3pnUzXmUascawfQ

---------

Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot gunbai-bot Bot mentioned this pull request Aug 30, 2026
gunbai-bot Bot pushed a commit that referenced this pull request Sep 12, 2026
Three corrections to the dissolution record, none to the deletion.

THE FILE ALREADY RULES ON THIS AND I ARGUED IT FROM CONVENTION INSTEAD. Its own
words: "the phase refused every unrelated change, so the shrink is the fix, not
housekeeping", and "each transition adds its rows here and removes them when its
subject lands". So the deletion is this roster's documented dissolution rather
than unrelated cleanup riding a route-facts diff, and it is the same motion as
the two shrinks already recorded here.

STALE AND CONSUMED ARE TWO FRAMES FOR ONE ROW AND THEY BLOCK DIFFERENTLY. The
dissolution records say consumed -- satisfied at the base, a typed receipt. The
floor said stale -- an UnmatchedAdmission refusal, which fires whether or not
anyone touched the roster. That is why this PR refused on a file byte-identical
to main's, and why a record saying only "consumed" would not explain the red
that forced the edit. Both are named now.

AND SHRINKING EARLY CANNOT FAIL OPEN, which is the argument for not waiting on
the row's owner: the file rules that empty does not mean permissive -- with no
rows, a real delta refuses as UNADJUDICATED. The worst case of an eager deletion
is a loud refusal naming the delta, never a silent admission.

Also recorded: this is at least the fourth occurrence of the shape, not a
novelty -- 53 rows once outlived their subject, a later state had 314 stale,
#9689 measured six, tonight one.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01AQGTwRrSBe8r3bmR3epQsL
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