Skip to content

V4.1 on GB10: 64-token kernel pages on SM12x, FlashInfer 0.7.1rc1, and FLASHINFER_VERSION passed to the build - #12954

Merged
briansrls merged 10 commits into
mainfrom
spark/v41-sm120-kernel-pages
Oct 2, 2026
Merged

briansrls merged 10 commits into
mainfrom
spark/v41-sm120-kernel-pages

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

What and why

The V4.1 Group A launch got to CUDA-graph capture and then failed on every rank (fleet-converge run 36921450575) with Assertion error (deepgemm-src/csrc/apis/attention.hpp:262): block_kv == 32 or block_kv == 64. The V4.1 backends declare 128-token kernel pages on anything that isn't SM90, so on GB10 (SM121) a ratio-1 indexer page held 128 states, and DeepGEMM's SM120 paged-MQA path only accepts 32 or 64. This is upstream vllm-project/vllm#56461 / #59203.

Upstream's fix has three parts. This PR adopts them:

Latent bug fixed: vllm_image_build_args now passes FLASHINFER_VERSION. The recipe's FlashInfer version was an input to the build key, but the build never read it.

The recipe is built through a new extdeps.vllm.source_build vllm_recipe_with_flashinfer, because VllmContainerBuildRecipe is sole_constructor.

Test plan

  • claim_batch --hermetic:
    • v41_runtime_candidate_witness_test: 24 pass, 2 fail. The same 2 fail on main (the hermetic route has no DigestFile arm).
    • v41_runtime_image_produce_witness_test: 7 pass. The verify-script claim now also pins the 0.7.1rc1 release URL.
  • Wet: image build from deploy/ds41-fabric-blob (which carries these commits). The source tree on srv8 was read back with all three kernel-page edits and flashinfer-*==0.7.1rc1 present. The first build died on a network timeout fetching the Rust toolchain; the rebuild is run 36934138860. The launch result will be added here.

🤖 Generated with Claude Code

gunbc-ci-auto-heal and others added 5 commits October 1, 2026 21:08
…fer 0.7.1rc1 (flashinfer#5197); pass FLASHINFER_VERSION to the build

The launch reached CUDA-graph capture and DeepGEMM's SM120 paged-MQA metadata asserted
block_kv == 32 or block_kv == 64 on every rank (fleet-converge run 36921450575): the V4.1
backends declare 128-token kernel pages off SM90, so a ratio-1 indexer page held 128 states.
Upstream's three-part fix (vllm#56461/#59203): 64-token pages on SM12x (#57292, adapted as
member sm120_64_token_kernel_pages), FlashInfer with runtime SM120 page sizes for the ratio-2
32-token extra pages (#5197, first released in 0.7.1rc1, operator-approved RC), and DeepGEMM
page32 on SM120 (already admitted by this image's DeepGEMM, per its assertion text).

Also: vllm_image_build_args now passes FLASHINFER_VERSION; the recipe's version was a build-key
input the build never read.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ainerBuildRecipe is sole_constructor; build run 36927694013 refused at resolve)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…t per-architecture providers

FlashInfer 0.7.x splits flashinfer-jit-cache into a shim whose METADATA requires one provider per
architecture; the candidate admitted exactly python, cubin and one jit-cache wheel, so the live
0.7.1rc1 population would have refused. The build-target gate now covers the whole family.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…M#14 ported to 8b1392b)

Launch run 36945738911 passed the indexer metadata (member 3) and then asserted in
fp8_fp4_paged_mqa_logits: SM12x FP8 caches admitted block_kv 64 only, and ratio-2 layers
take 32-state pages. The member ships #14's two host hunks and has deepgemm.cmake apply
them after FetchContent, idempotently, refusing a tree it cannot patch.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
POSIX_FADV_DONTNEED is advisory; on srv8 (2026-10-02) 135168 of 25345200678 bytes survived one
call, the rank refused, systemd restarted it into a rendezvous that had moved on, and the
four-rank launch hung. The release now retries up to 5 times 200 ms apart; residue that
survives every attempt still refuses, naming the attempt count.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@briansrls
briansrls marked this pull request as ready for review October 2, 2026 03:53
@chatgpt-codex-connector

Copy link
Copy Markdown

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review Status Commit Review trigger
📝 Code Review ✅ Completed 2026-10-02T03:55:53.164315Z 687e2ad Draft marked ready
ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

gunbc-ci-auto-heal and others added 5 commits October 2, 2026 03:56
…ed (floor RosterStale)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…nt the three GB10 members

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…(floor RosterStale)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@briansrls
briansrls added this pull request to the merge queue Oct 2, 2026
Merged via the queue into main with commit a12fe0f Oct 2, 2026
4 checks passed
@briansrls
briansrls deleted the spark/v41-sm120-kernel-pages branch October 2, 2026 06:29
gunbai-bot Bot pushed a commit that referenced this pull request Oct 2, 2026
…standing

Main (#12954) retired them after fixing those imports; a merge here had carried the older
ActiveDebt rows forward, which the floor refuses as RosterRetirementChanged.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls pushed a commit that referenced this pull request Oct 2, 2026
…icates as declarations) (#12969)

* v2: ground where-refinement predicates as declarations; resolve binds them

Each decidable where predicate is a total Bool declaration (std.types string_non_empty,
gt_zero, range; std.content_hash lower_hex_16/40/64/128) and brand a declared marker fn.
Lowering carries every predicate of a clause, with its arguments, at its own occurrence;
v2 resolve binds each by ordinary name lookup and refuses an unbound one as
resolve_reason_where_predicate_unbound. non_empty is respelled string_non_empty corpus-wide
(v1 parse/infer tables + stage0 regen) and the gate's non_empty_string consolidates onto it.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* v2: home the Char classifier in std.unicode.char_class; fix stale predicate homes; import filter

std.string_type pulled into the compiler closure broke self-host emission (string_lex_compare
E0308); the classifier moves to its own Unicode module instead. Comments naming std.integer as
the home of gt_zero/range now name std.types (review 71649). filesystem_io imports the bare
filter the floor refused once the file was touched.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* floor roster: retire filter rows discharged by filesystem_io's filter import

filesystem_io now imports v2.std.algebra filter, so every file importing filesystem_io
no longer carries its bare filter pair; the floor refused the touched one as RosterStale.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* floor roster: retire v2.std.algebra rows reached through filesystem_io

The import closure is module-grained: importing filesystem_io now reaches every
v2.std.algebra declaration, so skip/any/length rows on its importers are discharged too.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* where predicates: execute each declaration against the seed's probe values; stop overclaiming one authority

Until v1's tables can consult a declaration (feature:where-refinement-predicate-declaration-authority),
the declaration and the table are two representations. The vocabulary witness now executes each
grounded declaration on the probe value the compiler is observed to refuse, with boundary controls,
one claim per predicate; the comments state the fork instead of claiming one authority (review 71681).

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* stage0: restore main's v1_rt.rs (a stale-binary regen had reverted it)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* filesystem_io: drop the duplicate filter import (main added the same one; review 71725)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* MQ-1 PR-2 WIP: caret symbol lowers to a symbol literal

* MQ-1 PR-2: RFMs, conservation control, symbol-literal frontier control

* symbol literal payload read without a nested Edge pattern (emitted Rust holds the label in an Rc)

* caret lowering claims: list_snoc_item from v2.std.algebra; declare the generic-ident-class flip

* parse probe: caret-site claims read one warm-shared parse (caret_tree_atom_identities) instead of re-parsing each

* caret lowering witness: plain recursion instead of fn-lambda call arguments (the witness is about carets, not the lambda frontier)

* caret lowering witness: build lists with list literals/concat (seed types a bare Cons as FreeMonoid)

* reference_conservation_admission: drop the braces my merge resolution orphaned (floor/generated: unparseable at byte 6129)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* namecheap witnesses: rename the test helper response -> namecheap_api_response

#12421 declared a top-level fn response. The bare-reference scanner reads each
service operation's response { ... } block (42 files) as a reference to it, so
every PR touching one of those files is refused UnimportedBareProvider. The
scanner's missing keyword awareness is reported as its own finding.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* v2 resolve: a module's own `type Int` / `type Bool` shadows the kernel spelling instead of being captured

Body lowering rewrote every type atom spelled Int or Bool to the kernel binding before any scope
existed. A module that declared its own `type Int = | Mine` and wrote `let y: Int = 1` therefore
had its annotation replaced by the kernel Int, and infer judged the let matched.

The spelling table moves to its language authority (v2.extdeps.languages.dag
dag_kernel_type_binding_optional), and resolve_atom consults it only after the scope walk and the
symbol index. A hit declared in the referencing module binds that declaration. Imported, foreign,
ambiguous and unbound kernel spellings keep the kernel binding, unchanged.

Claims (v2.test.claim.body_let_annotation, 5c): the module-declared Int and Bool lets refuse at the
annotation, and the annotation is asserted not to be the kernel binding. An undeclared Int/Bool
still binds the kernel type. Both shadow rows are red on main 9ce0394 and green here.
The rfm row records the residual and its trigger.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* v2 resolve: an imported user Int refuses instead of binding the kernel Int

Resolve now reads a kernel spelling by the declaration a door selected.
v2.extdeps.languages.dag dag_kernel_type_declaration_binding_optional lists the declarations a
kernel spelling denotes. A hit on one of them takes the canonical binding, and the module's own
declaration shadows it. Any other declaration, reached through an import or another module,
refuses with resolve_reason_kernel_type_spelling_names_a_foreign_declaration. Unbound and
ambiguous names keep the spelling fallback.

Third RED: bla_imported_user_int_refuses_rather_than_binding_the_kernel_int (a two-module
fixture, p imports q's `type Int = | Mine`). All three REDs are F on main and T here, and the
controls are T on both. The new specimens are enrolled in floor_pure_producer_share. The rfm row now
states rung = refused, with the trigger at capability grain: declaration-keyed binding across every
door.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* v2 resolve: an ambiguous kernel spelling refuses unless every candidate is a kernel declaration

An ambiguous kernel spelling now binds the kernel type only when every candidate is a kernel
declaration of it: v2.std.integer Int beside std.integer Int is one kernel type. Otherwise it
refuses with the ordinary resolve_reason_ambiguous_symbol instead of defaulting to the kernel. An
unbound name keeps the kernel binding, which is the correct answer when no declaration is in scope.

New claims:
- RED bla_ambiguous_imported_int_refuses_rather_than_defaulting_to_the_kernel (p imports Int from
  q and r). F on main, T here.
- Control bla_ambiguous_kernel_declarations_bind_the_kernel_type. T on both.

The multi-module specimens now share one helper, bla_assemble_with_peers. The rfm residual is now
only the kernel-declaration path list. Its trigger is a mark on the kernel declarations themselves.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* wip: infer symbol-literal arm (DagCanonicalSymbolLiteral typed as v2.std.node Symbol)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* test.claim.parse_test_fn_decl_return_clause: lowering carries the authored return-type spelling

Three floor blockers on fa8c596. These claims read the positional return clause from body lowering
and expected the kernel binding (dag_binding_type_int, bool_node_symbol). Lowering used to produce
that binding by rewriting the spelling. That rewrite now happens in v2.compiler.resolve, after the
scope walk, so lowering carries `Int` and `Bool` as written, as the generic row already reads `T`.
Arm 1 still discriminates: the return type is Bool, not the parameter's Int.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* dag_canonical_literal_from_node: match the symbol-literal optional once

review 72280: the symbol arm tested dag_node_is_symbol_literal_atom and then recomputed
dag_symbol_literal_name_optional. That was the same optional twice, and the recomputation needed an
arm the predicate had already ruled out. The decision now matches the optional once. The remaining
Absent arm is a name payload with no atom identity, which is reachable.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* Dissolve dag_node_is_symbol_literal_atom: callers match dag_symbol_literal_name_optional directly (review 72280 on #12549)

* identity_captured_navigation: read a caret literal's name from the lexeme-stamped terminal; delete the span/source-text route and its prose note row (review 72294 on #12549)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* Delete the octet-to-scalar index and its lens-slice claims with the lens span route: nothing else consumed them

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* caret_symbol_has_no_lowered_form: the receipt states the literal's type as this PR derives it

review 72301: the receipt still said the symbol literal's type stays on the GroundingNotDerived
frontier. The arm in this PR makes that false. It now names the derivation route
(DagCanonicalSymbolLiteral, infer_literal_type_binding, v2.std.node symbol_type_node) and the two
body_let_annotation claims that execute it. Census trigger (a) stays open and the receipt says why:
it names the source checker v1.compiler.types, which still types LitSymbol as string_type.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* v2 resolve: the single-tree namespace binds the module's own declarations; ownership reads declared_in

GitHub review 5342739525 on #12540. The same-module test compared a declaration's path to
ctx.namespace.module_qn, but build_program_namespace (the plain normalize -> resolve route)
leaves module_qn Empty and records its owner in declared_in. namespace_owns_declaration now reads
declared_in, which is the owner on both namespace routes and the field root_binding_origin reads.

Measuring that route found the earlier boundary. build_program_namespace harvested only the root's
named edges, and a normalized module keeps its declarations under captured -> <module path>, so
none of them were bound. `type Myint` refused as unbound, and a module's own `type Int` fell
through to the kernel spelling and was silently bound to the kernel Int. The namespace now also
harvests the module body, which it finds by declared_in.

Controls on that route (v2.test.claim.body_let_annotation, enrolled share points):
- bla_single_tree_module_declared_int_and_bool_bind_the_local_declaration: F before, T now.
- bla_single_tree_undeclared_int_binds_the_kernel_type: T on both.
The foreign-import refusal and both ambiguity dispositions are unchanged and still hold.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* v2 resolve: select a grafted module body by the graft's mark, never by walking names

Review 5343957887 (P2 on b55b8a7). namespace_tree_module_body walked the module path's names and
restarted at the root on a missing step. Two leaks followed:
- `module m.t` with a root-level record `t` missed `m`, restarted, found `t`, and bound the record's
  field as a module binding.
- `module t` with a record `t` selected it at once.

The body is now selected by the producer's own mark. v2.compiler.namespace_graft
namespace_graft_module_body_optional descends the containment spine
(namespace_graft_spine_segment_edge_optional) until a step is not a segment, never restarts, and
answers only when that stop is the marked body (namespace_graft_node_is_module_body).
Header and flat representations have no grafted body, so they keep root-only harvesting.

The admission reader in v2.compiler.name_resolve already descended the same spine with its own
copy (admit_named_exports_body_root and _descend_spine). It now calls the one function in
namespace_graft (namespace_graft_module_body_root), so the spine has one reader.

Controls (v2.test.claim.resolve.single_tree_module_body): supplied emit-shaped roots, because
normalize always emits a well-formed graft and source text cannot author these shapes.
- a_record_matching_the_path_suffix_is_not_a_module_body_holds: F on b55b8a7, T here.
- a_record_named_like_a_flat_module_is_not_its_body_holds: F on b55b8a7, T here.
Each asserts `leaked` is not bound and `t` still is.

The local Int/Bool and undeclared-kernel controls still hold.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* v2 resolve: move build_program_namespace's rationale above the declaration

The parse phase refused a // annotation inside the fn body (DESIGN section 4c: only module-item
grain is modeled). This is the same text, placed above the declaration.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* RFM reference_conservation_population_omits_class_stamped_terminals: the caret WHY is past tense and names its helper as deleted (review 72492)

* v2 infer: a literal payload's facts derive for its own family

Review 5348050288. infer_literal_edge_diagnostics_derived decided which literal family owned a
payload edge, then dropped the family. infer_literal_payload_entries typed every payload atom as a
DecimalDigit, so a Symbol literal's name terminal was recorded as a digit.

The edge decision is now typed: infer_literal_edge_payload returns InferIntMagnitudePayload,
InferSymbolNamePayload or InferNotALiteralPayload, and the payload fold takes that family.
- Int magnitude members keep DecimalDigit / FreeMonoid<DecimalDigit>.
- A Symbol name payload is one childless atom and derives as v2.std.node Symbol (symbol_type_node).
- Any other shape stays on the frontier.

Controls read each payload node's recorded resolved_type (v2.test.claim.body_let_annotation 5e):
- bla_symbol_literal_payload_is_typed_symbol_not_digit: F at 87a29e4, T here.
- bla_int_literal_payload_digits_stay_decimal_digits: T on both (the integer family is unchanged).
Both require at least one payload to be seen, so neither can pass vacuously.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* body_let_annotation: share the payload verdicts, not the inferred trees

The floor refused at 92389ff: PureProducerShareWarmNotStored for bla_symbol_literal_as_symbol_tree,
because the cross-claim store cannot hold a closure (ServeCacheValueNotPortable, path
.value.facts.lookup). The shared producers now return the portable projection the claims inspect:
bla_symbol_literal_payload_verdict (the symbol-typed and digit-typed Bools) and
bla_int_literal_payload_digit_verdict. The trees are built inside those producers and never stored.
The claims and their discrimination are unchanged: the Symbol payload control is F without the
family-aware fold and T with it.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* 04_infer: the payload comment cites infer_literal_edge_payload, not the deleted predicate

Review 72579: the comment above infer_literal_payload_member_type still named
infer_literal_edge_diagnostics_derived, which this PR replaced. No definition or reference to it remains.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* Merge origin/main; bla_symbol_literal_as_int returns Outcome<ResolvedTree> (the #12432 assemble type)

* Import the std.disposition / v2.std.live_tree names two touched files use bare; retire their now-imported roster rows

Main newly declared Disposition and LiveTreeDisposition, so the gate refused
both files on this touch as UnimportedBareProvider. Importing the declaring
modules also covers SingleAuthority, RealizationDispatch and
SubstrateInputsOnly, whose ActiveDebt rows retire as ImportsFixed.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* roster_gate imports Finding (bare channel is off in a file that declares imports)

* reference_conservation_admission: KnownDropShape as a one-variant coproduct (leading |), not an alias to StatementLetBinder

With one arm left, '= StatementLetBinder' parsed as an alias, so the variant
did not exist and two importers refused IMPORT-MEMBER-ABSENT. The corpus form
for a one-variant coproduct is '= | Variant' (e.g. SdramSignalingFamily).

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* v2: the kernel host-text String, bound only where no String declaration is visible

neat-boar-16's ruling after #12549. It mirrors #12549's Symbol pair through the same mechanism.

- Declaration: v2.std.node declares the opaque kernel `String` beside Symbol (the kernel-types home),
  and owns its type node, host_text_type_node.
- Binding: v2.extdeps.languages.dag binds the spelling `String` to it, and the declaration table maps
  v2.std.node.String to it.
- Foreign declarations (decision A): String is the one kernel spelling the corpus already declares
  with another meaning (v2.std.text and std.string_type are FreeMonoid<Char>, imported by 470+
  modules), so dag_kernel_type_foreign_declaration types its foreign-declaration disposition as
  ForeignDeclarationBinds. v2.compiler.resolve then binds the declaration the author reached, and
  the kernel host text applies only in the unbound arm. Int, Bool and Symbol keep
  ForeignDeclarationRefuses.
- Literal: DagCanonicalStringLiteral is a fourth arm of the one literal decision, typed as host
  text. Every consumer that matches the literal decision handles it (infer's type binding, branch
  operand, match-arm body, Bool pattern classify, payload edge, and the undecidable-verdict lens).
- No implicit coercion: a host-text literal at a FreeMonoid<Char> position REFUSES. The declared
  unfold (literal_homomorphism_rows, UnicodeScalarSequenceUnfold) is not reachable yet, because the
  literal carries no value. That is filed as gunbc.recurring_failure_mode
  string_literal_lowers_to_one_class_stamped_atom (fix routed to gentle-koi-724's lane).

Claims (v2.test.claim.body_let_annotation 5f). The REDs are F with the behavior reverted and T here:
- bla_unimported_string_binds_kernel_host_text
- bla_string_literal_is_typed_host_text
- bla_string_literal_ascribed_int_refuses
- bla_host_text_literal_at_structural_string_refuses
Controls, T on both:
- bla_imported_structural_string_binds_its_declaration
- bla_host_text_value_at_structural_string_is_never_matched (no non-literal expression derives host
  text in v2 yet, so it pins "never a clean admit")
- bla_unknown_unimported_type_name_still_refuses

The Symbol and #12540 claims are unchanged and still hold.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* carrier_by_spelling: record the v1/v2 String fork and where it resolves (at the importers)

royal-newt-820 flagged it and neat-boar-16 ruled. Under decision A, v2 binds `import v2.std.text { String }`
to the structural carrier, while v1 keeps the kernel. The fork resolves at the importers:
- host-using importers drop String from their imports, in a separate PR ahead of #12760;
- structural-using importers are a declared divergence, recorded here, with #12760's census as the
  instrument.
The rung stays at the v1 minimum. Evidence: bla_imported_structural_string_binds_its_declaration.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* dag_canonical_literal_from_node: the string arm matches the atom inline; the is_* predicate is gone

Review 73119. dag_node_is_string_literal_atom was a sibling Bool predicate over Node storage, which
the literal coproduct exists to replace. That is the same dissolution as dag_node_is_symbol_literal_atom
(3fb5d6a, review 72280). The decision matches the atom identity inline. The claim reads
DagCanonicalStringLiteral from the decision, and the RFM row cites the decision.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* defork census: the String row names the kernel host-text String as a distinct concept

The generated check failed at d9cc153: docs/plans/dag-v2-defork-audit.md drifted, because the census
now finds v2.std.node String (#12760) among the String declarations. The derived file list was
right, but the authored reading still called every String '= FreeMonoid<Char>, one concept, two
declarations'. That is false for the opaque host text. The reading now separates the structural pair
from the host-text String, and the projection is regenerated with generated_artifact_gate main_wet.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* kernel String: read #12759's string value; realize v2.std.node String as the host string

#12759 landed, so a string literal now carries its decoded value as one named payload.
- DagCanonicalStringLiteral { value } reads it through dag_string_literal_value_symbol_optional. A
  payload-less string atom is now a malformed literal.
- The value edge is its own payload family (InferStringValuePayload), typed host text and never a
  digit, as #12549 did for the Symbol name. bla_string_literal_is_typed_host_text now also
  requires that.
- string_literal_lowers_to_one_class_stamped_atom records the climb by #12759. The remaining
  literal-at-FreeMonoid<Char> refusal is now blocked only by v2 infer not peeling an alias to its
  body.

emit-build failed at 9b7c07f: the opaque v2.std.node String was emitted as its own struct, so the
bare String in v2_std_node.rs (symbol_lexeme's return) stopped meaning the host string (E0308).
gunbc.rust_source_type_bindings gains the exact row v2.std.node String -> RustStdString beside
Symbol's, and the String checkpoint proof records that the kernel spelling now has one declaration
rendering the same carrier. The stage0 mirror is updated to match: claim_executor --required-regen
reports first_generation_equal=true over 161 files.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* carrier_by_spelling: the importer census is a named frontier, not an instrument this PR cites

Review 73214. The receipt called the importer census '#12760's census' and its instrument, but no
classification exists in the tree yet. It now says the population is described, not bounded; names
the census and deletion lane that will bound it; and states that #12760 is held as a draft until both
land, so the flip cannot precede the cutover. When the census lands, the receipt will cite it by
symbol.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* where_predicate_binding: assemble_program_from_ingest now returns Outcome<ResolvedTree> (#12629)

The binding claims inspect only accept/refuse, so they retype to
Outcome<ResolvedTree>; Node is no longer used.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* v1 emit_rust: an opaque declaration with an exact realization row emits an alias to that row

Ruled by deep-bee-18 for gunbc#12760. The emitter emitted every zero-parameter opaque declaration
as `pub struct X(PhantomData)` and ignored the declaration-keyed rows in
gunbc.rust_source_type_bindings. On #12760, v2.std.node String therefore became a struct, and the
kernel's bare `String` render inside v2_std_node.rs meant that struct (E0308 at symbol_lexeme).

The rule is general and declaration-keyed: rust_opaque_declaration_has_exact_row joins the existing
name-keyed kernel-alias route at all three sites that decide it. An exact row emits
`pub type X = <row spelling>`. An ambiguous row, or a row with no realization, renders the located
compile_error! that rust_exact_binding_spelling already produces, so there is no silent choice. The
phantom struct stays only where no row exists.

Stage0: v1_compiler_emit_rust.rs is regenerated. std_types.rs gains `pub type Unit = ();`, because
std.types Unit is a bare opaque declaration with an exact row (RustUnit) that the old emitter
emitted nothing for. claim_executor --required-regen reports first_generation_equal=true.

Controls (test.claim.opaque_exact_row_alias_witness_test, each read from the emitted text):
- std.types Unit, reached only by its row, emits `pub type Unit = ();` (absent before this rule);
- a row-less opaque declaration keeps its phantom struct;
- Symbol keeps its row alias.

v1 admission (gunbc.v1_maintenance_standing v1_seed_standing): this serves the v2 self-host
program, because the emitted compiler closure must build with the v2.std.node host-text String.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* 04_infer: bind the literal payload family once in the gather

Review 73303 on #12809 (finding 2) flagged the pattern this PR introduced: each family arm matched a
variant only to rebuild it for infer_gather_literal_payload_step. The gather now binds the family
once, with one arm for InferNotALiteralPayload and one for every family (DESIGN section 2).

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* carrier_by_spelling: cite the importer census by symbol, and its structural-using population

The census is gunbc#12840 (royal-lark-857). Instrument: v2.lens.text_string_importer_census
verdict_with_crossings, whose identity join closes (407 = 391 String importers + 16 non-members). The
structural-using population, the declared v1/v2 divergence, is 7 modules, named here. It is a lower
bound: 120 unclassified and 2 unmeasured importers stay open. #12760 stays a draft until #12840 and the
import-deletion PR land. The symbol is cited in prose only, and joins the evidence list once #12840
lands.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* carrier_by_spelling: the structural-using population is 15 (census revision 7b87f99)

After neat-boar-16's fixpoint ruling, #12840 classifies 15 structural-using modules. Eight of them
are structural only because they pass host text into a module that keeps its import. v2.compiler.tokenize
and v2.std.integer are named divergence sites (ruling 1), 10 parse-refused modules keep the import
(ruling 4), and 24 remain undecided. The second instrument, text_string_importer_fixpoint, is added.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* floor: the live-tree closure reads the process-shared index (one index for the environment and kernel-types closures)

closure_paths_of built a fresh MultiEntryIndex over the live dag root per
call. A diff touching std/types.dag asks for both the parse-environment and
kernel-types closures, so the same name set was indexed twice and #12765's
guard refused the floor (MultiEntryIndexBuiltTwiceForOneNameSet, both sites
namespace_baseline.rs closure_paths_of). The revision-tree index in
evaluate_owned_item_in is a distinct source set and is left as is.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* Carry one live-tree index to both closures instead of using the thread's shared slot

The shared slot holds the floor's own dag+src/v2 index; a dag-only demand
there evicted it and the floor refused SharedIndexRebuiltAfterEviction
(#12848's own floor). LiveDagIndex is built on first demand by the floor's
baseline reconstruction and passed to environment_agreement and
kernel_set_serves_both (-> kernel_names_at), so the two closures share one
build and the shared slot is untouched. The roundtrip test shares one too.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* string_literal RFM: the literal-at-structural refusal is a stopgap; #12809 is its trigger

neat-boar-16's ruling on #12760: since #12759 carries the literal's value, the lawful route is the
unfold. The row now cites gunbc#12809 (parked on #12726 PR2 and #12506) as the trigger that flips
bla_host_text_literal_at_structural_string_refuses to an unfold control.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* lexing: import unicode_char_code_point from std.unicode.char_class

This branch moved it out of std.unicode.types (to break the std.types cycle);
main's new v2.std.compilers.lexing imported it from the old module, so the
v2-native emit of 00_compile refused (emit-build).

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* WIP v2 resolve: lexical references keyed by occurrence; infer/eval/translate/emit read them

* legacy_repair_tap witness: import Present/Absent from v2.std.optional

The witness matched git_sha1_object_id's Optional result with bare Present/Absent.
v2.std.execution_surface also declares Absent | Present (a9388e4, the same
commit), so once a closure holds both, the four reads are ambiguous and the floor
refuses PureProducerShareRowModuleUnframeable (AmbiguousBareNameRead, sites=4).
The value variant Present { value } is v2.std.optional's; execution_surface's
carries no field.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* WIP: lift unscoped atom arm; flatten infer pattern

* WIP: argument may not begin after a newline

* WIP: walk-population fixture mints its bound references, as the parser does

* Restore main's text in the gap-analysis plan: its non_empty spellings record measurements taken on the old name (review 73826)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* v2 resolve: a loop carrier is a binder, kept as the atom it names, never a lexical reference

* Debt roster: retire (std/content_hash.dag, get) as NotAReference

The floor refused RosterStale: content_hash's get is the builtin get(xs:, index:),
whose pair came from the whole-pool fallback resolving it to an unrelated pool
fn get. be51d1f (bare loader asks per name) removed that, and retired the same
builtin-get pairs elsewhere (e.g. extdeps/bootloader/grub.dag) as NotAReference.
This branch touches content_hash.dag, so its row is the one this floor judges.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* Review 73872: drop the unused Char classifier; the gate checks its structural strings with v2.std.algebra non_empty

- std.unicode.char_class keeps only unicode_char_code_point (consumed by tokenize
  and lexing). CharClass and char_in_class had no consumer anywhere and are deleted
  rather than rehomed.
- gate's displaced_cost / mechanism_class are v2.std.text String = FreeMonoid<Char>.
  Passing them to std.types string_non_empty (host text) crossed representations
  with no declared unfold (DESIGN section 4). The gate now calls v2.std.algebra
  non_empty, the structural carrier's own check; main's private non_empty_string
  stays deleted.
- The vocabulary comment no longer claims String inhabits no FreeMonoid carrier.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* Arrow-body-form mutation mirrors place the lexical-reference arm, as production does

* Integration: real three-way merges of the generated stage0 files; name Filesystem's declaring module at its five bare readers

The five bare Filesystem reads (harness_cli, harness_turn, runner_microvm_boot_probe,
scm.repository_load, scm.repository_save) call Filesystem.Read/Write/List, the
extdeps.filesystem.filesystem_io service that v1.compiler.emit_rust emit_file_call binds,
so that module is the import. They were refused AmbiguousBareNameRead once #12381's
std.types edit brought them into the floor's prepared closure.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* Integration: thread #12947's lexical field through #12381's where-predicate walk

resolve_where_predicate_operator converts resolve_atom's Outcome through the existing
resolve_walk_of_outcome (a type's where clause has no lexical binders in scope, and
resolve_atom carries no lexical answer), and the unwalked where-set edge carries an
empty lexical list. With this, v2.test.claim.parameter_reference's five assembled-program
rows (the four the floor failed on #12947 plus pr_named_fn_parameter_is_a_parameter_reference_holds,
red on main) return true: #12381's where-predicate binding is what cures main's
resolve_unbound_name_is_declared_in_several_modules at the where clause.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* Revert "Merge #12760 (neat-ibex-696/kernel-string) into the integration branch (generated conflicts taken from ours; regenerated below)"

This reverts commit 2688462, reversing
changes made to d5446f3.

* Integration: take #12760 back out (operator option A); regenerate

#12760's own carrier_by_spelling row orders it after the String import-deletion
PR, which has not started. Its merge is reverted, the source-type binding row it
added is re-derived away by claim_executor --regen-round-cost (fixed point,
rebuild_packages=0), and the defork audit's String row returns to main's.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* Integration: #12947's occurrence matches take main's OccurrencePending (#12790)

A pending occurrence has no id yet, so it is read like a synthetic one:
resolved_tree_lexical_binding finds no binding (Absent), and resolve_lexical_reference
refuses it as unkeyed (resolve_reason_lexical_reference_unkeyed). emit-build and the
generated lane refused both matches as non-exhaustive on bc718d2.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* Integration: main's resolve_arrow_resource_requirements atom arm carries #12947's lexical field

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* Integration: name the declaring module at three bare reads the combined closure made ambiguous

extdeps.cloud.gcp.sts and extdeps.tailscale.acl_api read String bare, declared by both
std.string_type and v2.std.text; they import it from std.string_type, the dag/extdeps
convention (acl_api's std.types import of String bound nothing). gunbc.systemd_property_directive_overlap
reads Unit bare, declared by std.types and v2.std.cardinality; it imports std.types Unit.
The floor refused these as AmbiguousBareNameRead (CLAIM-SCOPE) on 430d11d.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* Integration: revert #12381's annotation-only edit in an excluded wet receipt; file the floor class it trips

The floor selects an annotation-only hunk as a changed witness, contrary to DESIGN section 4c,
and refused the head with ChangedWitnessOutsidePreparedSubject for
test.manual.command_runner_local_argv_receipt (on the hermetic exclusion list). The
annotation correction (non_empty -> string_non_empty) is reverted so the honest edit is not
what blocks the integration; the stale annotation and the capability that lets it be
restored are rostered as gunbc.recurring_failure_mode annotation_only_edit_selects_a_changed_witness.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* Integration: the two spark get rows keep main's Retired ImportsFixed standing

Main (#12954) retired them after fixing those imports; a merge here had carried the older
ActiveDebt rows forward, which the floor refuses as RosterRetirementChanged.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.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