Repository navigation
Stage0 emission boundary as a target profile, and the crate partition named before native bootstrap - #10886
Conversation
…pected_red note's producer The add-slice roster note in v2.workflow.floor_expected_red carried a dated receipt (main 3a8344b: infer accepts dag_add_emitted_root; the infer-then-translate composition refuses headed by infer_grounding_not_derived) and named its own next-rung trigger: a .dag entry returning the per-stage verdicts for one root, so the paragraph can name a producer instead of a commit. v2.compiler.self_host.candidate_generation_stage_verdicts is that entry, parameterized over root and target: the receipt's verdict vocabulary (infer_accepted / infer_rejected; candidate_accepted or the rejection head reason) plus the carried-reasons lists -- the half the verdict symbols cannot say, namely that infer accepts while carrying the frontier diagnostic on its accepted path, so the enrolled witness's d == None conjunct fails even where the composition reaches acceptance. v2.test.execution.self_host_candidate_generation_stage_verdicts binds the instrument to the slice's own fixture, with add_slice_stage_verdicts_entry the runnable gunbc run --function form (ExitSuccess only when infer accepts clean and the composition accepts clean). Two witnesses: infer-accepts as a permanent positive control, and the frontier-state pin that is expected to red the day the add-slice stall's trigger lands, flipping to a permanent regression control in the same change that removes the roster row (DESIGN 4b(4)). Measured by execution on this branch: the entry exits 1 printing infer=infer_accepted, infer_carried=[infer_grounding_not_derived x10], composition=infer_grounding_not_derived, composition_carried=[x11] -- the receipt reproduced, with bind_outcome's pending-plus-gate chain counted. Both witnesses PASS; the enrolled semantic witness still fails as enrolled. Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
…nd-to-end infer gains the declared-inhabitant membership derivation: a node declared in the dag language authority's declared-inhabitants roster derives its grounding by lookup, with the roster as evidence -- the namespacing answer to the atom authority question, at specimen scope. The add slice's ten type-spine nodes (Arrow, Conj, Atom) are all roster members, so: - candidate_generation_translate_self_emit_dag_add_slice_holds passes; its floor_expected_red roster row and per-row note delete per the roster's own stale-quarantine arm - the dag same-language ingest path compiles end-to-end: cross_language_compile accepts, byte-equal to the authority's own serialization, no carried diagnostics - the add-slice stall narrows to its four python/typescript round-trip members; the original trigger's causal clause was refuted by execution and is restated against the grammar parse-product population - the instrument's frontier guard flips to add_slice_composition_accepts_holds (DESIGN 4b(4): frontier guard to permanent regression control) - five manual witnesses flip with it: two root flips rewritten to assert the green state, three transitive conjunctions updated The kinds stay frontier: non-member Arrow/Conj/Atom specimens carry GroundingNotDerived exactly as before, and all fourteen enrolled refusal/acceptance controls pass unchanged. The door's production path still reds inside rust emission, untouched by this rule. Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
…joins binding to inhabitant once The resolver already binds the surface spelling Int to the canonical binding symbol dag_binding_type_int; what that binding DENOTES is the Int inhabitant declared at dag_declared_inhabitants_core. Every hand-rolled fixture facts lookup re-authored that join (dag_add_canonical_grounding_for, record_construct_canonical_grounding_for). The language authority now declares it once as dag_binding_denotation, and infer_node_facts consumes it: an Atom whose identity is a canonical dag binding with a declared denotation derives with that denotation as its grounding evidence. Direct-rust-door specimen census: 14 underived -> 10 underived (the four dag_binding_type_int atoms derive; grammar-production atoms, algebra atoms, bare operand atoms, and the arrow/conj spine stay on the frontier unchanged). Specimen-scope interim in the same frame as infer_node_declared_in_dag_inhabitants: both delete in favor of consuming resolution output when the resolver hands infer declaration-resolved identities directly (the namespace migration's completed state). Witness: v2.test.execution.dag_binding_denotation — all four Int binding atoms in the door specimen derive with dag_int_inhabitant_node() as structural evidence, and the two bare operand atoms stay GroundingNotDerived (boundary control). Refusal suite 14/14, ingest bridge 7/7, add-slice instruments 2/2 green; every remaining red in the at-risk population reproduces identically on the pre-change tree and is enrolled in floor_expected_red. Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
…ntract A point-in-time orientation that defers to the existing authorities (DESIGN section 7, the four-wave self-host program, the roadmap node chain, the three frontier carriers, the guarantee-stall roster, XL-N) rather than restating them: state is re-derived by the named instruments, never transcribed here. Sequences the remaining work in roadmap order (door, parse-product grounding, first behavioral module, XL-N milestones, native bootstrap, fixed point, v1 deletion) and states which decisions stay operator-gated. Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
The sixth and seventh kind rules: a non-roster Conj or Arrow whose every child carries DerivedGrounding derives, its evidence the same shape re-formed over the children's grounding evidence (a fresh OccurrenceSynthetic node, never the source — the self-evidence wall holds by construction). A product with any frontier or absent child stays on the frontier with its typed diagnostic; a childless product has no evidence to compose and stays frontier. Roster members keep their roster evidence. Measured on the direct-rust-door specimen (scratch probe, uncommitted): 10 underived of 15 -> 6. The parameter conj, the module-structure conjs, and the bodied add arrow derive; what remains is the algebra atoms from the + operation (AlgebraPrimitive, ring_field_add), the module atom (dag_surface_module), the parameter references (x, y), and the grammar-projection root conj that cascades once they land. Enrolled witnesses (src/v2/test/claim/execution/infer_product_introduction_test.dag): - product_introduction_derives_fully_evidenced_products_holds — census: 4 Conj (3 derived, 1 frontier-by-frontier-child) + 1 Arrow (derived). - product_introduction_composed_evidence_carries_child_groundings_holds — the params conj's evidence is a Conj whose x/y children target the dag authority's Int inhabitant. - product_introduction_leaves_childless_conj_on_the_frontier_holds — boundary control via direct infer over a hand-built childless Conj. Flip census (pre- and post-change, zero unexpected flips): translate_underived_refusal 14/14, infer_self_grounding_wall 12/12, branch_infer_if_then_else 2/2, compile_eval_thesis_proof 6/6, ingest_bridge 9/9, cross_language_add_python_to_typescript 4/4, inhabitant_neutralization 6/6 + e2e 6/6, emit_host_classical_not 14/14, dag_binding_denotation 2/2, stage-verdicts instrument 2/2, dag_add_emit_round_trip 4/6 (the 2 enrolled reds unchanged), door production group still enrolled-red (unchanged). Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
…roster membership Two more specimen-scope derivations in infer_node_facts, both lookups into declared authorities, never inventions: - Canonical-operations roster (target_model.dag): every CanonicalOperation the target-model authority declares, rendered by target_model_canonical_operation_wire_node and gathered under one Conj root. The resolver canonicalizes surface operators (e.g. +) to those declared operations, so the wire atoms -- the operation discriminant and its field references -- derive by membership with the roster root as evidence. General over all 14 declared operations, not add-narrow. - Grammar-productions roster (dag.dag): every production in dag_grammar_root() projected to its emitted surface atom under one Conj root keyed by production name. The bridge projects a production's parse into (identity atom, captured content) pairs, so the identity atom (dag_surface_module) derives by membership with the roster root as evidence. The roster derives from the grammar root, so a production added to the grammar joins by construction. Both roster roots are Conj nodes, never structurally equal to any member atom, so the self-evidence wall holds by construction (the first attempt at the operations rule used the wire node itself as evidence and was refused by grounding_evidence_is_source -- the wall doing its work). Measured on the direct-rust-door specimen (scratch probe, uncommitted): 6 underived of 15 -> 2 (only the operand atoms x and y remain; the grammar-projection root conj cascades once the module atom grounds). Enrolled witnesses (infer_atom_grounding_rules_test.dag): each roster rule pins derivation + evidence identity + census; a boundary control pins that a bare atom with no authority membership stays frontier; the closing control pins the 2-of-15 state. Flip census: the product-introduction census witness updates 3->4 derived conjs (the top conj now cascades) and gains a hand-built partially-evidenced boundary control to replace the in-specimen one the cascade consumed. Full battery otherwise unchanged: refusal suite 14/14, grounding wall 12/12, instrument 2/2, binding-denotation 2/2, round-trips, bridge, cross-language, neutralization, emit-host all green; enrolled reds unchanged. Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
…aration The fifth specimen-scope derivation, closing the direct-rust-door specimen's inference frontier: an Atom whose binding an enclosing arrow's domain declares derives with the declared domain type as its evidence -- the declaration-site annotation, itself derived (x: Int grounds the x reference). This is the same lookup the branch-operand path already performs (infer_find_arrow_domain_type_in_tree), now written to the operand atom's own facts; it is scope-naive (whole-tree, first match), recorded in the frontier note, and deletes with the other specimen-scope rules when the resolver hands infer declaration-resolved identities. The tree is threaded through the fold's init chain to reach infer_node_facts; the helper had exactly one caller. Measured on the door specimen (scratch probe, uncommitted): 2 underived of 15 -> 0. The specimen's inference frontier is fully closed, and the production observation advances from InferenceRejected (infer_grounding_not_derived) to EmissionRejected (target_use_site_ownership_lookup_miss) -- a new, typed, located deficit in the emitter, the next gate on the path. Flip census (all three rewrites verified by execution): - dag_binding_denotation_leaves_unbound_operand_atoms_on_the_frontier_holds -> dag_binding_denotation_declares_no_denotation_for_operand_bindings_holds: the boundary moves to the authority itself (the denotation table returns Absent for x/y), true regardless of infer's other rules. - The three emit_host classical-not refusal guards (canonical, staging, staging-swapped) flip to acceptance witnesses pinning the emitted text's shape -- the real-infer tree now fully derives, and the emission is the same one the equals-eval witness proves behaviorally correct. The translate-refuses-underived behavior stays enrolled on hand-staged fixtures in translate_underived_refusal_test.dag (14/14 green). The renames are carried into the commit_workflow and witness_deferral_freeze rosters. - New witnesses: binding_reference_derives_parameter_atoms_holds (evidence is the domain's Int binding atom, census 2) and door_specimen_fully_derives_holds (0 frontier of 15). Full battery at this state: refusal suite 14/14, grounding wall 12/12, instrument 2/2, binding-denotation 2/2, product-introduction 4/4, atom-rules 5/5, emit_host 14/14, round-trips 4/6 (2 enrolled reds unchanged), bridge 9/9, cross-language 4/4, neutralization 6/6 + e2e 6/6, branch 2/2, eval-thesis 6/6; door production group still enrolled-red (unchanged). Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
…osition and decode canonical operator wires
The door specimen's inference frontier is fully closed, so its production
observation now reaches the emission stage. Two defects surfaced there, both
fixed here:
Emission composition. generate_rust_emission_candidate served two lanes with
one root shape: the door's production path (a dag module shell) and a fixture
lane (a bare rust Arrow). The translate ownership gate queried the module
atom's ownership at a struct-field use site and refused with
target_use_site_ownership_lookup_miss, because the module's grammar-projection
conj was misread as a type record. The door's real composition is the
produced-decl path: collect declaration conjuncts from the inferred tree and
emit via emit_produced_decl. A new generate_rust_module_emission_candidate does
exactly that, enforcing an exactly-one-declaration admission policy
(rust_module_emission_decl_absent / _ambiguous). The observation and production
mint paths switch to it; the fixture-lane candidate is retained with a note
that it is fixture-only. A pure collector, produced_decl_conjs_in_tree, finds
nodes of produced-decl shape (a Conj whose first child is a Named edge to an
Arrow). Its decl-head match routes through a declared FreeMonoid<Edge>
parameter because the v1 seed stamps pattern variables from a declared
parameter type, not from a field-access scrutinee.
Operator decode. With composition fixed, source fidelity still refused: the
door emitted fn add(x: i32, y: i32) -> i32 { AlgebraPrimitive(x, y) } instead
of { x + y }. Resolution canonicalizes a surface operator atom into a
canonical-operation wire node, so a production tree's transform operator
position carries the wire, while fixture trees that bypass resolution still
carry the surface token atom. translate_project_transform_in_arrow_scope only
knew the surface-token table, so the wire missed and fell to callable apply,
rendering the discriminant identity. The projection now tries the wire decode
first (canonical_operation_from_wire_node) and only on a wire miss falls to
the surface-token table, then to callable apply; the arms are disjoint, so the
dispatch adds no fallback widening. target_transform_operator_child extracts
the operator child safely.
The door's closing expectation now greens by execution, so its known_red_probe
row in explicit_witness_admission is deleted per its own dissolution condition,
and the roadmap authority note, the door contract note, and the direct-path
plan are updated to record the green state. realized_closure_for_v2_direct_
rust_door_emit_run's module list reflects the produced-decl route.
Verified by execution: the door witness greens; the fixture, containment,
algebra, produced-decl, add-slice, and classical-not witnesses stay green;
claim_executor required-ci lanes build and witnesses both exit 0; cargo fmt and
clippy --all-targets -D warnings are clean. One pre-existing red,
witness_projection_is_active_only in the floor_cost_debt containment roster,
reproduces on the base revision and is unrelated to this change.
Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
… membership to the closed ingest set The declared-inhabitant roster-membership derivation in 04_infer generalized from the dag roster to the closed ingest set (dag, python, typescript): infer_node_declared_in_language_inhabitants returns the declaring authority's roster root as evidence, with deep subtree membership so a declared inhabitant's leaf fact atoms derive exactly as the inhabitant node itself. Measured: the python fixture's 19-node frontier and the typescript fixture's 28-node frontier both close to zero; all four add-slice stall population round-trip witnesses green; the python->typescript cross-language compile accepts, byte-identical to ts_source_text. Section 4b(4) flips (expecting-red probes becoming permanent regression controls for the acceptances): - cross_language_compile_refuses_canonical_underived_holds -> cross_language_compile_python_to_typescript_round_trip_holds - inhabitant_neutralization_emit_after_neutralize / same_flavor_python / go_int64_to_ts refusal helpers -> round-trip controls - inhabitant_neutralization_python_to_ts_cross_language_compile (e2e) -> round-trip control; python->go members stay refusal guards (go is outside the closed ingest set) - cross_language_emit_inhabitant_neutralization_refuses_underived_holds -> round-trip control; the python->typescript emit-matrix row reads ChainProven The add-slice stall's next-rung trigger fired, so it retired per DESIGN 4b(4): removed from all_guarantee_stalls, row file deleted, witnesses stay enrolled. Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
…ess for the emitted add crate
First InterpreterRetained -> SelfEmittedNative promotion after classical_not,
executing the v2-emitter-first-behavioral-module first slice at the
coverage-frontier grain: the add family (fewest dependencies — integer
literals plus one canonical operation) now carries a native-only verdict
witness, so its behavior is established by the emitted crate's own stdout
with eval() unreachable from the verdict path.
- emit_host_native_only_add_holds: real emit -> cargo build -> native run,
stdout pinned to the family's expected octet, sharing the kernel family's
one-build cache key exactly as the classical_not arm shares its family's
key (no duplicated cold build).
- emit_host_native_only_add_wrong_octet_mismatch_detected_holds: the broken
control — a no-eval verdict has no oracle leg to break, so the expectation
side breaks (an octet the run never produces must not match); program-side
discrimination stays with the family's equals_eval primitive-five/six pair.
- The add coverage row flips disposition with its backing citation enrolled
by construction (the verdict entry is file-grain enrolled in
falsifier_self_host_wet_template_entries).
- Frontier census tests updated at identity grain: natives are exactly
{classical_not, add}; split 2/13.
Verified by execution: all six native-only verdict tests green locally
(real wet legs — compile_skipped receipts show cold builds and native runs);
all eight emit_coverage_frontier tests green, including the unbacked-claim
RED control.
Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
…rounding-frontier-3100 # Conflicts: # dag/gunbc/guarantee_stall/roster.dag # src/v2/compiler/self_host/candidate_generation_stage_verdicts.dag # src/v2/test/claim/execution/self_host_candidate_generation_stage_verdicts_test.dag # src/v2/workflow/floor_expected_red.dag
…fication The row classified candidate_generation_translate_self_emit_dag_add_slice_holds as RealDefect/CompilerBehaviourRefusal with measured evidence that translate refuses infer_grounding_not_derived. The owner lane (v2 self-host) repaired the subject: the declared-inhabitant roster-membership derivation grounds the slice's type spine by lookup, and the witness passes under claim_batch --hermetic on the merged tree. The dated classification is kept verbatim; the disposition flips RoutedToOwner -> RepairedInThisChange with the repair measurement appended to the evidence, so the routing carrier stops dispatching a fixed defect. Structural witnesses (count 13, no NotReproduced, exact partition) are untouched and pass.
Main's annotation-placement wall (source annotations admit only standalone leading blocks attached to module-scope declarations; in-body forms refuse) reached this branch through the merge and refused 8 blocking errors on the 00_compile closure: the add-family promotion note inside the emit_coverage_frontier_roster list and the python->typescript row note inside the cross_language_emit_matrix list. Both blocks move above their enclosing declarations, rephrased to name their subject row. Measured: gunbc compile of src/v2/compiler/00_compile.dag now emits 172 files with 0 blocking errors; both files' suites stay green (8/8 and 4/4).
…ct witness for the emitted logic family crate The complement family's native execution runs family-grain per the witness_family_build_grain_ruling (one crate for meet + join + complement, argv-dispatched), so the native-only arm emits the logic family crate and runs the complement member through the family dispatcher, sharing the family witness's one-build cache key. The verdict is decided solely by the emitted native run's stdout (expected octet 0, complement(True) = False); the broken control flips the expectation side (octet 1 can never match), with the comparator pinned by the stdout mock pair. Program-side discrimination stays with the equals_eval agreement pair and the family witness's all-alt leg. The frontier row's backing citation lands in the already file-grain-enrolled native-only verdict entry, so it is enrolled by construction; the roster comment is rephrased to cover both 2026-09-07 promotions (add and complement). The frontier test's split and native membership assertions move to 3 native / 12 retained. Verified by execution: claim_batch --hermetic on emit_host_native_only_verdict_test.dag passes all 8 witnesses (the two new complement arms included), and emit_coverage_frontier_test.dag passes all 8.
…ling is_host_text_carrier_type answered true for any type expression whose authored name reads "String", including references to the structural alias v2.std.text.String (type String = FreeMonoid<Char>) that the namespace lane (gunbc#9907) requalified the v2 corpus's text-carrier fields to. The emitter rendered every one of those references as the host String while value-position consumers rendered the structure -- the E0308 family dominating the self-host compile-phase frontier (41 of 64 in v2_compiler_tokenize.rs on the post-merge board). The String arm now consults the resolved declaration's provenance against v1.compiler.coercion structural_declaration_modules_for -- the same roster type_realization_decision reads -- so the legacy arm and the strict decision cannot diverge on one node (DESIGN section 3, and gunbc.recurring_failure_mode alias_resolution_collides_with_kernel_spelling). Kernel mints and unresolved references keep the host answer exactly as before. Regen: the only drifted stage0 mirror is v1_compiler_emit_rust.rs itself (no module in the stage0 closure references a structurally declared String -- verified by the whole-population candidate tree), installed from target/stage0-regen-candidate after the priced round's partitioned rebuild refused MirrorHasNoOwningPackage on the emitter (the emitter is monolith-shell, not partition-owned). Fixed point verified by execution: claim_executor --required-regen on the rebuilt seed reports first_generation_equal=true over 158 adjudicated mirrors.
… -> 28 errors A field authored v2.std.text.String reached the Rust emitter as an overlay-less resolved reference leaf and rendered the bare terminal name, which binds the prelude String cross-module (#9813: kernel names are never overridden by imports, so the use-line is dropped) while every value position renders the structural carrier Rc<Vec<i64>> -- the v2_compiler_tokenize.rs E0308 family, 41 of 72 errors on the XL-N phase board. The new rust_overlayless_alias_leaf_requires_peel arm in render_rust_type_without_applied_binding detects the population (overlay-less zero-parameter alias leaf, qualified spelling, String terminal segment, closed_alias_peel_verdict agrees) and renders the alias declaration's resolved right-hand side, projecting the same realization the fn-signature positions already produce. The qualified gate is load-bearing: inside the declaring module the bare name is the correct render (the emitted module carries the alias declaration), and the local binding's resolved_type drops the RHS type argument, so an ungated peel rendered Rc<FreeMonoid> there (E0107 x13, E0282 x2 on the probe). Bare String keeps denoting the kernel scalar through the host-carrier arm. Measured: probe specimen (qualified/bare/direct-FreeMonoid/container/variant/ local-alias positions) compiles clean; XL-N compiler closure cargo check 72 -> 28 errors with the residual census dominated by the declared text_boundary_identity_wall class (kernel String vs structural carrier at bare-authored boundaries, 17 of 20 E0308s); v1-corpus fixed point holds (first_generation_equal=true, 158/158 adjudicated).
…rsions + witness_violates helper Four clusters, all measured non-hop additions between receipt_1 (155) and the post-peel census (28); the live gate now measures 15 with zero unadmitted regressions: - integer.dag: integer_string_to_decimal_digits_step takes v2.std.text.String; the public boundary converts with chars() (text_boundary_identity_wall specimen discharged at this site). - 01_tokenize.dag: Token/UnboundSourceAnnotation lexemes convert structural -> host String with chars_to_string() at construction, mirroring the v1 tokenizer's host-lexeme carrier. - target_model.dag + bash.dag: EmitSpellingEscape.from/to and apply_emit_spelling_escapes go structural (v2.std.text.String); the EmitSpellingQuote arm converts host->structural->host at its boundary; bash's escape rows wrap their kernel String literals with chars(). - witness.dag + 3 call sites (collection list_nth, provenance span_index_resolve_textual_locus_from_ids, compile outcome_with_diagnostics): new witness_violates<C> helper puts Violates constructions in a Witness-headed position so the emitter resolves the carrier type argument; dissolves once inference records per-call substitutions. Verified: 48 targeted claim witnesses green (tokenize behavioral, shell conformance, string brace escape, string length, map-lookup violates, source text ingress, bash materialize x12, int literal smoke x6, provenance span index x2).
…nsus at 6676531 The census at the XL-N lane tip: 155 -> 15 net, credited to the qualified-alias peel (60cbd7b, 72 -> 28) and the twelve-error source cluster (6676531, 28 -> 15). The epoch changes on the instrument's target pinning (found by review on gunbc#9857), admitted with receipt_1's board as the reclassified predecessor under the identity map. Nine added identities are hop relocations admitted by the hop index; four sit in python/typescript modules newly entered into the emitted closure, admitted as ExposedByNewEmittedModule. Validated: all 36 self_host_compile_phase_frontier_witness claims PASS, including current_persisted_compile_phase_frontier_holds.
Inference substitutes the resolved declaration into a data annotation's type-argument position, so BooleanAlgebra<v2.std.logic.Bool> reaches the emitter with the arg BEING the type Bool = True | False declaration itself (Disj connective, ident_span in src/v2/std/logic.dag, no Resolved wrapper). type_reference_provenance_in_env's bare-leaf arm re-resolved that leaf in the REFERENCING module's scope, where post-#9813 a kernel-shadowed spelling answers the kernel declaration -- so the structural enum rendered as host bool against a value of BooleanAlgebra<Bool> (the python.rs:328 / typescript.rs:177 E0308 pair on the XL-N compile-phase frontier). The connective is the discriminator: a reference node is a bare name (NoConnective); a node carrying Conj/Disj structure IS the declaration, and type_reference_provenance's own-span fallback already answers that shape correctly. The guard routes declaration-shaped nodes there directly, bypassing the scope lookup that #9813 makes answer the kernel. Mirror regenerated via the regen round; fixed-point verified (claim_executor --required-regen PASS).
…s at the boundaries The receipt_2 census's fifteen identities, resolved at their sources: - lexing.dag, dag.dag, python.dag, typescript.dag: LexPattern.text is the structural carrier (v2.std.text.String); the construction sites held host Strings. Convert at construction with chars() -- the #9907 ingress pattern. - python.dag / typescript.dag bool groundings: qualify the annotation as BooleanAlgebra<v2.std.logic.Bool>; with the emitter's substituted- declaration provenance guard the qualified arg now renders structural. - target_model.dag: target_lex_rule_literal_step returns the host carrier (chars_to_string over the structural pattern text); TargetText.source converts at the is_empty boundary; the unicode-scalar symbol intern converts its single-codepoint list to the host carrier. - qualified_name.dag: qualified_name_from_dotted_string uses the host-carrier emptiness check (string_length == 0) instead of routing through the structural string_is_empty. - 02_parse.dag: parse_looks_like_match_arm_start rewritten on host-carrier operations (string_length, char_at, code_point) rather than converting to the structural carrier for a two-character lookahead; parse_char_is_arm_pattern_lead takes the codepoint Int directly. - v1_interpreter_primitive_surface.dag row_key: the concat pipeline lowered to a .concat() method call on std::string::String (E0599); rewritten as nested concat calls. Measured: the 00_compile closure emits 172 files and cargo check reports cargo_clean=true, cargo_error_population=0 under the pinned 1.93.0 toolchain.
The cargo half runs with cwd = a fresh mktemp directory; with no rust-toolchain.toml there, rustup resolves the host's DEFAULT toolchain, so a census under cargo 1.83 and one under cargo 1.93 would compare as equal epochs while different compilers did the measuring -- the fabricated comparability the target pin (gunbc#9857) excludes, one level up. Measured 2026-09-07: a host default of 1.83.0 met a crates.io index whose freshly published dependency manifests require edition2024, resolution failed before any diagnostic existed, and the zero-diagnostic refusal fired on an unmeasured tree. The pin is propagated by copying the repo's rust-toolchain.toml into out_dir: the file remains the sole in-repo channel authority (its header forbids a second pinned literal), and the copy makes the measured channel true by construction on any host. The gate's read_live_toolchain observes the same channel because every documented actuator invokes from the repository root, which the same file governs.
… closure's cargo census is empty Measured at 5ee4892 by the one-entry instrument: the 172-file emitted crate reports zero cargo error diagnostics, so the board attributes every phase a count of zero and furthest_phase_reached stands at Borrowck. The fifteen removals against receipt_2 need no disposition; nothing was added. The epoch does not change: the cargo half now pins the toolchain channel by copying the repo's rust-toolchain.toml into the scratch crate, and every recorded comparison field is identical to receipt_2 (whose census the fingerprint evidence shows the same 1.93.0 toolchain already compiled), so the same-epoch arm carries no reclassified predecessor. The frontier-state pin flips per DESIGN 4b(4): the_published_frontier_standing_does_not_claim_typeck_or_borrowck_passed becomes the_published_frontier_standing_claims_typeck_and_borrowck_passed, the permanent regression control over the green state. Validated: all 36 self_host_compile_phase_frontier_witness claims PASS, including current_persisted_compile_phase_frontier_holds.
Ledger-Repair-Judged: docs/design-failure-modes.md Ledger-Repair-Judged: docs/design-rung-drops.md
…e rosters First native-parity divergence class found by running the emitted closure on a discriminating fixture: the algebra inhabitant rosters still carried PointwisePower after its authority row was cut, so the emitted compiler panicked at 12 record-shaped carrier sites while the interpreted seed refused cleanly. The roster rows are removed in rust/python/go/typescript types.dag, the derived coercion assertions in compiler_tests.rs regenerate without them, and two witnesses pin the boundary: the record shape constructs its structural carrier, and FinitePowerSet still refuses while its row stands. Mirrors regenerated by a converged regen round (fixed point Reached, stage-1 PromoteGenerationInputs over the three language types mirrors).
The admitted side of run_built_seed_regen carries the executable-digest spelling (current_exe_digest, next_pass_executable_digest) while the observed side hashed the file through path_digest, which prepends the fnv1a64: tag. Same bytes, two spellings, so the gate could never pass -- unpassable since fa2d403 (#9771). Factor current_exe_on_disk as the single path authority and read the observed digest through current_exe_digest so both sides spell the same bytes the same way.
A regen round whose only stage-2 drift was compiler_tests.rs (the PointwisePower roster removal rewrote its derived coercion assertions) refused the rebuild MirrorHasNoOwningPackage: the mirror is owned by no partition package, because every item it defines is #[cfg(test)] and no release unit elaborates it. The refusal conflated two different states -- unowned (a coverage hole) and excluded from the release build by construction (a precise empty scope). The model now names the class: rebuild_scope_release_excluded_mirrors rosters its members (compiler_tests.rs, cited to emit_compiler_tests_module), the decision answers ReleaseScopeEmpty when the whole change set is excluded, and the actuation shape is actuatable with an empty package closure and every partition package excluded -- the build still runs as verification, and a compiled partition package refuses the stage. The host admits the empty closure only when the new stage0_partition_rebuild_release_scope_empty_today query answers true; any other empty closure still refuses. A mixed change set scopes on its release-visible members alone. Verified by execution: the 2026-09-08 round converged (fixed point Reached) with stage-2 installing compiler_tests.rs alone; cargo recompiled the shell crate on its fingerprint (the outer mod line is ungated, so rustc reads the file) while the produced executable was byte-identical -- stage input seed digest == output seed digest. Four new witnesses pin the arm, its actuation shape, the mixed set, and the host-facing query's two arms; the boundary witness (unowned cli_run.rs still refuses) keeps the roster from decaying into the absorbing fallback.
The receipt's partition-rebuild line is rendered by the model over receipt.installed_mirrors, which the host populated from the stages' projected_paths -- full paths -- while the partition rows and rosters key on basenames. Every drifted round's receipt therefore rendered a spurious RebuildScopeRefused MirrorHasNoOwningPackage line naming a full path, a false claim on the round's own receipt. Route the projection through emit_path_basename, the module's single path-to-basename bridge, so the field carries the mirror names the model's vocabulary means.
The ReleaseScopeEmpty modeling commit placed three // blocks inside declaration bodies (stage0_partition_rebuild_is_actuatable, stage0_partition_rebuild_decision, stage0_partition_rebuild_excluded_today). The .dag realization admits annotations at module-item grain only, so the floor lane's parse phase refused the file with 12 located errors and the run ended floor refused. The prose is unchanged; each block now sits above the declaration it describes.
…d realization The witness added with the fossil-row removal excluded the bare spelling "BTreeSet", but every emitted file's preamble imports OrdSet as BTreeSet, so the row could never green. The exclusion's subject is the finite-set REALIZATION the fossil row would have asserted; spell it applied (BTreeSet<i64), which the preamble's import line does not contain.
The second native-parity divergence class, measured 2026-09-08 on the
native run of the emitted 00_compile closure: emit_data_value_json spelled
EVERY record literal as a JSON map, including the zero-field record, while
emit_struct_from_children renders that same declaration as a Rust unit
struct (pub struct BoolEncodingFact;). serde's derived unit-struct
Deserialize reads null and rejects {}, so the emitted compiler panicked at
first touch of v2.std.logic's bool_primitive_facts: "invalid type: map,
expected unit struct BoolEncodingFact". The JSON spelling of a data value
must deserialize into the Rust type the same declaration emitted; the
record arm now spells the zero-field value null and keeps the map spelling
for non-empty records.
The mirror is taken from the required-regen candidate, not hand-edited.
Two witnesses enroll: the discriminating red (zero-field record spells
null, never {}) and the boundary control (a record with fields keeps the
map spelling).
…s for the twelve ceiling-band native-only verdict claims Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
…ge0-boundary emissions The floor refused this branch's first head two ways, and both are cost, not content. Fixed at the cause rather than by raising a line. FIRST: twelve of #10692's native-only rows tipped 6-118ms over the 500ms per-claim ceiling. They sit deliberately just under it -- the parent's last two commits are about keeping them there -- and this branch had re-parameterized rust_binding_spellings, which every one of them evaluates. The profile now OVERLAYS the single key it changes (map_insert over the Rust map) instead, so the base map is byte-for-byte what it was and every claim already sharing one evaluation of it keeps sharing exactly that one. A profile's delta belongs to the profile; charging every other witness for it was the defect. SECOND: this branch's own three claims were INTERRUPTED BEFORE VERDICT at ~1200ms each -- a full ingest-assemble-infer-emit walk per claim. Split by an ingest-only/assemble-only probe pair, the disk read and its content-hash verification cost 0ms and assembly costs 878ms, so the recompute was assembly, three times, of a pure function of one file's content. Two repairs, both the roster's own named one: The emission claims now run over direct_rust_door_specimen_resolved, the already-warm-enrolled producer of a resolved add-shaped module. A second producer for a specimen of the same shape would have been the duplication that roster exists to end. The two emissions themselves (profile target, base target) are nullary producers enrolled warm, the same shape as produced_add_module_source. Each claim is then a string comparison, and infer+emit is evaluated once at preparation rather than three times inside three budgets. THE READ IS CLAIMED SEPARATELY, because it is a separate fact and it is free (0-5ms): the committed fixture reaches source_ref_for_observed_storage_path and source_root_ingest_from_source_refs, whose content-hash verification is the seam no enrolled claim covered -- the door's specimen carries its module source inline. The assertion is a containment, not a whole-text golden, so editing the fixture's prose is not a test failure (a change detector, not a check). claim_batch over the entry: 5/5 PASS. The emission claims read the door specimen, so the expected sources name its declaration (`add`) rather than the fixture's. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011X5tyxfVrw3chDNbQ3sVD3
…ontier-3100' into session/lively-gull-662 # Conflicts: # src/v2/workflow/floor_pure_producer_share.dag
Review 62939 is right, and the gap is exactly where it says: the fixture's own annotation still described the enrolled fact as disk -> ingest -> assemble -> infer -> emit. That was true when written and stopped being true one commit later, when the three emission claims moved onto the door's warm-shared resolved specimen to fit the floor's per-claim ceiling. An annotation describing a route no claim executes is DESIGN section 5's specification-without-execution, and it is worse than absent because it reads as coverage. The file now states what it is the subject of -- the storage-read seam, claimed by the two read claims over the bytes actually on disk -- and says outright that no claim ingests, assembles, infers or emits it, with the reason the split happened. The two facts stay separate on purpose: the READ is claimed over a real file, the two target-profile SELECTIONS over the shared specimen, and neither claim covers the other. No behavior changes; the claims are unchanged and still PASS. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011X5tyxfVrw3chDNbQ3sVD3
|
Fixed in The file now states the seam it is actually the subject of — the storage read, claimed by the two read claims over the bytes on disk — and says outright that no claim ingests, assembles, infers or emits it, with the reason the split happened. The PR body is rewritten to match: the two facts are claimed separately (selections over the shared specimen, read over the committed file) and neither claim covers the other. I did not take the other arm you offered (re-enrolling a warm shared disk→emit producer). I tried it first: a nullary producer whose body performs the read did not serve — the fill was charged to the claim rather than stored — so the claims stayed ~1.2s and would have kept blocking the floor. The split is therefore the honest evidence rather than a preference, and it is now what the source says. — sent from lively-gull-662 |
…ops transcribing it Review 62942 caught the drift as it happened. The same measurement -- these three claims against the per-claim ceiling -- was transcribed twice in one diff, into the test file and into the enrolment row, and the two copies already disagreed (713-805 against 713-834). DESIGN section 6 forbids exactly this: name the producer that re-derives a measurement, never copy its numbers into prose, because a transcribed number is unreachable from the run that owns it and rots without either end being touched. The disagreement is that rot arriving on day zero. The figures now live once, at the enrolment row in v2.workflow.floor_pure_producer_share, which is where the ceiling arithmetic is argued and where every neighbouring row already argues its own. The test file names the instrument -- claim_batch's [witness] receipt over this entry, with the ingest-only / assemble-only probe pair that splits the pipeline -- and states the shape of the fact (unshared, each claim costs multiples of the ceiling; the read pair is the cheapest in the file) without restating a number beside it. Claims unchanged: 5/5 PASS. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011X5tyxfVrw3chDNbQ3sVD3
|
Fixed in The figures now live once, at the enrolment row in Claims unchanged, 5/5 PASS. Required floor is green on this branch by — sent from lively-gull-662 |
Review 62944 is right on both halves, and they compound. The arm asserted that
the ingested source did not contain "fn probe_add(x: Int) -> Int {" -- an arity-1
declaration authorable nowhere the check runs, over a fixed committed file no
fixture varies -- and it was additionally green on total refusal, because the
helper collapsed Rejected and Empty into a text sentinel that contains no marker.
So a broken read passed it. DESIGN section 4b: a check whose forbidden state
cannot be expressed where it runs is not a weak wall but a decoration,
permanently green by construction and worse than absent because it is cited as
coverage.
Two repairs, one per half.
The refusal is its own arm now. Stage0BoundaryRead carries Refused, Empty and
Carried separately, so a claim about content cannot be satisfied by a refusal and
a claim about refusal cannot be satisfied by content. The sentinel that made the
two indistinguishable is gone from this route.
The control forbids a writable state: a path no file occupies must REFUSE rather
than answer. The path is an ordinary String this module supplies, so the red is
authorable exactly where section 4b says it must be -- in the fixture surface --
and I verified it by execution rather than by argument: pointing that String at
the committed probe file turns the claim FAIL, and pointing it back turns it
PASS. That is the discrimination the predecessor never had.
claim_batch over the entry: both read claims PASS, and the emission trio is
unchanged.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011X5tyxfVrw3chDNbQ3sVD3
|
Fixed in Two repairs, one per half. Refusal is its own arm. The control now forbids a writable state: a path no file occupies must REFUSE rather than answer. The path is an ordinary Both read claims PASS; the emission trio is unchanged. — sent from lively-gull-662 |
# Conflicts: # docs/design-rung-drops.md # src/v2/workflow/floor_pure_producer_share.dag
…rebuild itself The compiler the new generator emits is written out today as ONE package: one manifest, one crate root, and the whole reachable closure beneath it (emitted_closure_compile_host requires exactly one src/lib.rs per crate dir). That is a reasonable probe while native and interpreted divergences are being burned down, and it is not a build topology anyone intends to keep -- but nothing in the sequence forced it to change, so it would have become one by default. The machinery is not missing. v2.std.compilers.compilation_unit already separates a language MODULE from a separately-compiled UNIT, derives cross-unit dependencies, closes interfaces over by-value type definitions, and refuses a split SCC, a unit-graph cycle and an unrepresentable by-value cycle. v2.workflow.rust_crate_partition already generates manifests and crate roots for a real seven-package split. What is missing is the join: nothing projects the compiler's own resolved closure through that model, and the policy resolver that would select a split from a target count is deliberately unimplemented -- a count is a placeholder, not a policy. So this is one edge, not a plan: the split is named as its own step between the first real module flip and the two-round native bootstrap. The placement is the whole point. Crate boundaries decide which declarations need visibility outside their own file, whether unit interfaces are actually complete, what a leaf edit rebuilds, and a build's peak memory -- so a self-rebuild proven over a one-package artifact is proven for a shape that will not ship, and the failures it hides are the first ones the real shape surfaces. This lane already met that class from the other end: the stage0 profile in this same PR exists because a module crossing a crate boundary needs `pub`, which a single crate never asks for. The node's RED control is deliberately stronger than "more than one crate": a module owned by two units or none refuses, a cycle between units refuses, a deliberately broken cross-unit export must fail the build rather than be papered over by wildcard re-exports, and a leaf edit must be shown to rebuild its own dependents rather than the whole compiler. Deliberately NOT added: a SingleClosureProbeCrate disposition type. Nothing would read it today, and a carrier with no consumer is the dangling modeling DESIGN section 3c refuses. The active roadmap row IS the carrier that cannot be quietly kept: it is read every session and cannot be accepted while the artifact is one package. roadmap_authority_test: both affected chain witnesses PASS. ROADMAP.md regenerated; the artifact gate agrees. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011X5tyxfVrw3chDNbQ3sVD3
# Conflicts: # ROADMAP.md
…as emitted Review 62979 found the last place a refusal could pass for an answer, and the annotation that claimed otherwise. stage0_visibility_selection_is_load_bearing asked only that the base emission DIFFER from the profile's expected text, and the refusal sentinel differs from everything -- so the arm the file billed as the discriminating visibility control was green on total pipeline failure. It was also strictly implied by its sibling's equality, so it carried no information even when the pipeline worked. DESIGN section 4b: a check permanently green on the failure it names is worse than absent, because it is cited as coverage. And section 4c: an annotation is never evidence a machine claim holds, which is exactly what "every arm reds on a route that stopped" was doing. The sentinel is gone. Stage0BoundaryEmission carries Refused and Produced as separate arms, and every claim requires a produced emission before it asks anything about the text, so a route that stops reds all three rather than satisfying one for free. The control now asks the question its name promises. Instead of "differs from the profile's text" -- a fact about the other target -- it asserts that the base target, which selects no visibility, emits no visibility keyword. The profile's side of the same fact is the positive claim, whose expected text leads with that keyword. Verified by execution, not argument: pointing the base producer at the profile target turns it FAIL, pointing it back turns it PASS. claim_batch over the entry: 5/5 PASS. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011X5tyxfVrw3chDNbQ3sVD3
|
Fixed in
The sentinel is gone from this route. The control now asks the question its name promises: the base target, which selects no visibility, emits no visibility keyword — a fact about this capability class, not about the other target's text. Verified by execution: pointing the base producer at the profile target turns it FAIL, pointing it back turns it PASS. 5/5 PASS. Also since the last round: — sent from lively-gull-662 |
…on is actually installed Review 62986 is right, and the defect is mine twice over. long_home_prefixes is an EXCLUSION from the required floor, not an opt-in to a bigger budget. I moved this module to v2.test.long. to get its claims out of the 500ms interrupt while their cost was being fixed, which took them off the merge path altogether -- so the green floor that followed said nothing about them. That is specification-without-execution with a green tick beside it, and it is exactly what this PR spent three rounds removing from the claims themselves. It also made the enrolment incoherent. floor_cross_claim_pure_producers_warm is installed and force-warmed by the required floor; enrolling two producers whose only callers were excluded from that floor buys a preparation-time fill no planned claim reads -- a cache with an empty consumer set on the one route that warms it (DESIGN sections 2 and 3c). Both halves resolve the same way: the module is v2.test.self_host again, homed where its name says, and the enrolment rows follow it. The cost problem the move was avoiding is what the enrolment is FOR -- the floor fills both emissions once at preparation, outside every per-claim budget, and each claim is then a comparison over a value it did not compute. claim_batch does not install the roster, so its receipt still shows the unshared recompute; the floor is where the serve happens and where this now has to hold. Stated plainly because it is a real risk and not a hope: if the fill does not serve on the lane, these claims will be interrupted and the floor will red. That is the correct failure -- visible, on the route that matters -- and strictly better than the silence I had bought by hiding them in the long home. claim_batch over the entry: 5/5 PASS. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011X5tyxfVrw3chDNbQ3sVD3
|
Fixed in
It also made the enrolment incoherent, which is the half you led with: Both halves resolve together. The module is Stated plainly rather than hoped: if the fill does not serve on the lane, these claims will be interrupted and the floor will red. That is the correct failure — visible, on the route that matters — and strictly better than the silence I had bought by hiding them in the long home. 5/5 PASS locally. — sent from lively-gull-662 |
Review 62990: the annotation still cited v2.test.long.stage0_production_target, a module that no longer exists -- the consumer moved back to v2.test.self_host.stage0_production_target in the previous commit, and grep for the old name returned exactly this one line. A citation naming a symbol that resolves to nothing is decidable and enforceable (DESIGN section 3), and it is the third time in this PR that this file's prose has described a route the code had moved off, which is the class rather than the instance. Two lines, not one. The same paragraph also still described the sibling read claim as asserting the source does not contain a declaration it never held -- that arm was replaced with the absent-path refusal control two commits ago, precisely because the old one forbade a state authorable nowhere. It now says what the pair actually does, including the property that makes this file safe to edit: its content is not the discriminating claim's subject, so changing the prose around the declaration cannot break the control. Both read claims PASS. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011X5tyxfVrw3chDNbQ3sVD3
|
Fixed in Two lines, not the one you offered. The same paragraph still described the sibling read claim as asserting the source does not contain a declaration it never held — that arm was replaced by the absent-path refusal control two commits ago, precisely because the old one forbade a state authorable nowhere. It now says what the pair actually does, and adds the property that makes the file safe to edit: its content is not the discriminating claim's subject, so changing the prose around the declaration cannot break the control. Both read claims PASS. — sent from lively-gull-662 |
|
The floor answered the risk I flagged, by execution rather than argument. Required-witnesses-floor run 34368368314 (green) receipt: Three things that were open are now measured on the merge path rather than asserted: both fills land at preparation with — sent from lively-gull-662 |
The produced-declaration type-reference route renders ^dag_binding_type_int through binding_spellings and never consults rust_target_atom_realization_catalog. So what this profile selects is the spelling that route emits, not Rust's realization of the language's Int -- the catalog owns that proposition and did not produce this result. The annotations said "INTEGER CARRIER" and "a Rust realization picks a primitive", which credits an authority that never ran, and the test file described the second control as a carrier control. Vocabulary only; no behaviour changes. The debt is now stated where the overlay is authored: binding_spellings is a second, weaker home for a fact the atom catalog owns (the duplicate Rust `bool` spelling is the same fork from the other side, and an unspelled atom prints its symbol lexeme instead of refusing), and the repair -- produced-declaration type references resolving through TargetAtomRealization, missing realization a typed refusal, neither binding_spellings nor a symbol lexeme admitted as a fallback in a type position -- is its own emission lane. All five claims rerun and PASS. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011X5tyxfVrw3chDNbQ3sVD3
The second capability class had no arm that isolated it. Its only evidence
was a whole-text equality against "fn add(x: i32, y: i32) -> i32 { x + y }",
which is satisfied by the visibility fact and the spelling fact TOGETHER:
adding `pub ` to the base output reddened it and the visibility control at
once, so the annotation's claim that the two controls fail for their own
reasons was not established by the implementation.
stage0_base_target_stays_private_and_i32_holds is replaced by
stage0_integer_spelling_selection_is_load_bearing_holds, which asks only
what the base target spells at the three type positions the stage0 ABI
fixes ("(x: i32, y: i32) -> i32" present, "i64" absent) over a produced
emission. Claim count and the shared-producer consumer set are unchanged;
the exact-output pin that remains is the profile's, in the positive claim,
where a golden is a fixture rather than one class's only witness.
Verified by executing both single-axis mutations against the base target,
one component of the profile at a time:
lex + produced-decl rows from the profile, base spellings
-> visibility control FAIL, spelling control PASS
base lex + rows, binding_spellings from the profile
-> visibility control PASS, spelling control FAIL
Unmutated: all five claims PASS.
rust.dag's ^dag_binding_type_int annotation carried the same overclaim this
branch removed elsewhere -- "which Rust integer CARRIES the language's Int"
-- and now says what was measured: the row is the spelling one emission
route reads, a second and weaker home for a fact
rust_target_atom_realization_catalog owns.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011X5tyxfVrw3chDNbQ3sVD3
#10886 landed the stage0 target profile and enrolled two of its own emissions on floor_cross_claim_pure_producers_warm for exactly the reason this branch enrolled seven: a ~700ms nullary fill cannot complete inside a 500ms claim. Both row sets and both carrier notes are kept -- the conflict was additive on both sides, with no disagreement about the mechanism. Worth recording, because it independently confirms a call made on this branch: #10886's note states that enrolling a producer whose only callers declare v2.test.long. would buy a preparation-time fill no planned claim reads, and that homing its claims there "took them off the merge path altogether and made a green floor mean nothing about them". That is the same reason this branch refused the long-home escape for its own arms rather than taking it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QbNFKK8mf6wBeVaCr22iNV
…ual to one Merging #10886 surfaced two regressions this branch caused, both real and both invisible to every witness that existed before that PR landed. Measured against origin/main to establish they are mine and not pre-existing: all three of v2.test.self_host.stage0_production_target's emission claims are GREEN on origin/main and RED with this branch's collector change. FIRST, the join produced the wrong representation of a string. emit_produced_module folded with list_append over an `Empty` FreeMonoid seed, so its result carried the CONS-LIST SPELLING of a string rather than the native one. `==` and `concat` behave identically on it -- which is why every golden over this fold has been green since it was written, and why this branch's own eight arms, which compare with `==`, could not see it either. A builtin that requires a native string refuses it: `split expects a string, got Variant`, from the two stage0 contains-controls, the first consumers ever to read this fold's output through `split`. Nothing on the production door reached the fold until this branch routed every nonempty population through it, so the defect was latent rather than new, and equality-only readers could never have found it. The join is now `concat` over a "" seed. One representation for one concept (DESIGN section 3). The first attempt at this fix changed only the seed and left list_append, and it did not work -- the measurement said so, and it is the reason the diagnosis above names the JOIN rather than the seed. SECOND, the trailing separator moved a golden this branch could not have known about. stage0_boundary_expected_source pinned "pub fn add(x: i64, y: i64) -> i64 { x + y }" against the door's output, which now terminates its last declaration because the door routes through the module authority. The expected text gains the separator, composed from emit_module_decl_separator rather than transcribed, so a future change to the module convention reds there instead of drifting silently. The declaration text stays a literal: it is the fixture golden that claim exists to pin, and reading it from the profile under test would stop it discriminating. Verified on the merged tree: all five stage0_production_target claims, this branch's eight population arms, produced_decl_module_folds_declarations_in_order, produced_decl_unwired_target_still_refuses, produced_module_two_distinct_fns_assemble and direct_rust_door_production_group_closing_expectation_holds. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QbNFKK8mf6wBeVaCr22iNV
… was silently truncating them (#10907) * The v2 production door was not refusing multi-declaration modules; it was silently truncating them The lane's premise was that generate_rust_module_emission_candidate's exactly-one-declaration ceiling was the admission wall keeping real corpus modules out, and that removing it meant routing every nonempty population through emit_produced_module. Execution says the ceiling was never the wall. produced_decl_conjs_in_tree asked whether a node was a Conj whose FIRST child is a Named edge into an Arrow, and stopped descending there. A resolved .dag module carries one Named-into-Arrow edge PER DECLARATION on a single shell Conj, so the SHELL satisfied that predicate: the walk recorded it as one declaration, and emit_produced_decl -- which reads children[0] -- emitted declaration 1 and dropped 2..N while reporting Accepted. Measured through observe_provenanced_rust_emission_from_ingest on a two-declaration module: ArtifactProduced, carrying exactly the first declaration. The rust_module_emission_decl_ambiguous surplus arm above it was therefore unreachable from any real module -- the collector never produced a surplus to refuse -- so relaxing the ceiling alone would have widened a silent truncation, not opened a door. This is DESIGN section 5's forbidden case, not a rung. The repair moves the predicate onto the edge that carries the role: a declaration IS the named edge into an arrow, and no per-declaration node exists in the tree to collect. The walk is edge-driven, records one declaration per declaration edge in source order, and never descends into one. The composition above keeps its typed zero-declaration refusal and sends every nonempty population through emit_produced_module. Evidence, green by execution over REAL INGESTED modules rather than planted decl nodes (v2.test.claim.self_host.rust_module_emission_population): the count arm reads 2 for a two-declaration module and 1 for one, measured one stage before emission; both declarations emit in source order and the swapped order is refused; a declarationless module still refuses at emission; a two-declaration module against an unwired target refuses WHOLE, with the same module on a wired target as its positive control. Every existing witness over this fold stayed green through the entire silent-drop period because each handed the fold a declaration list it had built itself -- which is why the specimens here are ingested modules. direct_rust_door_expected_source gains the module authority's declared separator, composed from rust_source_text and emit_module_decl_separator rather than transcribed: a one-declaration module is still a module, and emit_produced_module terminates every declaration including the last, exactly as emit_module does. The direct-door production group closing expectation, the two-target module fold and the produced-module golden all remain green. Class filed at gunbc.recurring_failure_mode.shape_predicate_reads_only_the_head_so_a_container_passes_as_its_element. No production regen selector, workflow/CI routing, roadmap acceptance or native bootstrap touched. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QbNFKK8mf6wBeVaCr22iNV * Carry each specimen's production walk once, so the floor's per-claim ceiling can reach a verdict required-witnesses-floor run 34392489718 refused seven of the eight new arms INTERRUPTED-BEFORE-VERDICT at cpu_at_least=501-507ms against the lane's 500ms per-claim CPU ceiling. The eighth, the declarationless refusal, completed at ~341ms -- it is the one specimen whose walk stops at the collector's empty population. The cost is not incidental setup that could be rewritten away: each arm is one ingest -> assemble -> infer -> collect -> emit production walk over one specimen module, and that walk IS what the arms assert over. Two arms walked three specimens to compose their expected text from the single-declaration emissions. So the repair is DESIGN section 2's -- one computation serving several demands is carried once at their shared ancestor rather than recomputed per demand -- using the mechanism v2.workflow.floor_pure_producer_share already models: nullary pure producers, warm-enrolled, forced during strict preparation OUTSIDE every per-claim budget, with each claim serving the landed fill. The production walk is not shortcut by this. The producers ARE the production observation, one per specimen, and their cost is paid in full; what changes is how many times it is paid. The share points are String and Bool, fully portable. Grounds for enrollment stated on the carrier, because three of the seven serve exactly one claim and would fail this roster's cross-claim sharing conjunct if read against it: these earn their rows on the FILL-THAT-CANNOT-LAND ground the roster already records for dag_prepared_grammar -- a fill costing more than one claim's budget can never complete from an in-fold first touch, and sharing is not the question. NOT verified locally, and the carrier says so: the warm path runs at strict preparation, which is the required-floor recipe's step and not a plain claim_batch --entry run. Measured after the refactor, the arms' claim_batch costs are unchanged at 341-1545ms, exactly as expected when the fill is not being forced. The deciding instrument is the required floor's own [floor-shared-fill] ledger: these fills must land at preparation with disposition=Stored and the seven former INTERRUPTED arms must serve hits. All eight arms remain green by execution on their verdicts. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QbNFKK8mf6wBeVaCr22iNV * A module's joined text is a String, not a FreeMonoid that compares equal to one Merging #10886 surfaced two regressions this branch caused, both real and both invisible to every witness that existed before that PR landed. Measured against origin/main to establish they are mine and not pre-existing: all three of v2.test.self_host.stage0_production_target's emission claims are GREEN on origin/main and RED with this branch's collector change. FIRST, the join produced the wrong representation of a string. emit_produced_module folded with list_append over an `Empty` FreeMonoid seed, so its result carried the CONS-LIST SPELLING of a string rather than the native one. `==` and `concat` behave identically on it -- which is why every golden over this fold has been green since it was written, and why this branch's own eight arms, which compare with `==`, could not see it either. A builtin that requires a native string refuses it: `split expects a string, got Variant`, from the two stage0 contains-controls, the first consumers ever to read this fold's output through `split`. Nothing on the production door reached the fold until this branch routed every nonempty population through it, so the defect was latent rather than new, and equality-only readers could never have found it. The join is now `concat` over a "" seed. One representation for one concept (DESIGN section 3). The first attempt at this fix changed only the seed and left list_append, and it did not work -- the measurement said so, and it is the reason the diagnosis above names the JOIN rather than the seed. SECOND, the trailing separator moved a golden this branch could not have known about. stage0_boundary_expected_source pinned "pub fn add(x: i64, y: i64) -> i64 { x + y }" against the door's output, which now terminates its last declaration because the door routes through the module authority. The expected text gains the separator, composed from emit_module_decl_separator rather than transcribed, so a future change to the module convention reds there instead of drifting silently. The declaration text stays a literal: it is the fixture golden that claim exists to pin, and reading it from the profile under test would stop it discriminating. Verified on the merged tree: all five stage0_production_target claims, this branch's eight population arms, produced_decl_module_folds_declarations_in_order, produced_decl_unwired_target_still_refuses, produced_module_two_distinct_fns_assemble and direct_rust_door_production_group_closing_expectation_holds. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QbNFKK8mf6wBeVaCr22iNV --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
What this is
Not the regen-grain flip, and not the full production-compatibility prerequisite either. It is the part of that prerequisite that is finished, plus the measurement that says what the rest of it costs.
Per the ruling: the flip's presumptive subject (
std.integer) is not producible by the v2 generator, and neither is any other real corpus mirror. Of the 152 committed stage0 mirrors joined to their.dagsources, exactly one module carries a single declaration — the shape the production composition admits —gunbc.rust_decl_type_overlay, and its body stops emission.Landed: the two boundary selections (ruling classes 1 and 2)
Rust owns what Rust is.
v2.compiler.self_host.stage0_production_targetowns what the stage0 seed crate requires of a module emitted into it:pub, because the crate calls across module boundaries (gunbc_rust_decl_type_overlay's function is called fromv1_compiler_emit_rust). The.dagsource spells no visibility and Rust emission in general must not — a private item is correct at a boundary with no external consumer. The keyword is a Rust row (rust_visibility_public_lex_rule); the selection is the profile's. Not "all emitted Rust is always public".^dag_binding_type_intthroughbinding_spellings. The stage0 profile overrides that route fromi32toi64, yielding the signature the committed stage0 crate requires; the direct-door fixtures stay organized aroundi32. The profile overlays the one key it changes (map_insertoverrust_binding_spellings()), leaving the base map byte-identical — so this selection charges no other witness an evaluation. This is a bounded compatibility overlay, not the canonical Rust atom-realization selection:produced_decl_type_ref_tokensdoes not consultrust_target_atom_realization_catalog, so calling it an integer-carrier or target-representation selection would credit an authority that did not produce the result. The debt is stated at the overlay itself, and the repair (produced-declaration type references resolving throughTargetAtomRealization, a missing realization a typed refusal, neitherbinding_spellingsnor a symbol lexeme admitted as a fallback in a type position) is its own emission lane — not a merge criterion here.Evidence — five claims, all PASS, and what each one covers
claim_batch --entry src/v2/test/claim/self_host/stage0_production_target_test.dag— 5/5 PASS. The two facts are claimed separately, and neither claim covers the other:The selections, over
direct_rust_door_specimen_resolved(the already-warm-enrolled resolved add-shaped module):stage0_production_target_emits_boundary_compatible_source_holds— the profile emitspub fn add(x: i64, y: i64) -> i64 { x + y }.stage0_visibility_selection_is_load_bearing_holds/stage0_integer_spelling_selection_is_load_bearing_holds— over a produced base emission, the base target emits nopub, and spells(x: i32, y: i32) -> i32with noi64. One discriminating control per capability class, and each really is isolated to its class: verified by executing both single-axis mutations of the base target, one component of the profile at a time — profilelex+ produced-decl rows with base spellings reddens the visibility control alone; base lex + rows with the profile'sbinding_spellingsreddens the spelling control alone. The predecessor of the second was a whole-text equality satisfied by both facts together, so apubregression reddened both controls at once and the spelling class had no arm of its own; the only exact-output golden that remains is the profile's positive claim above.The read, over a committed file:
stage0_boundary_committed_module_reads_through_the_storage_route_holds/stage0_boundary_absent_path_refuses_rather_than_answering_holds— a committed path returns content carrying the expected declaration, while a path no file occupies refuses rather than answering. The route issource_ref_for_observed_storage_path→source_root_ingest_from_source_refs, which nothing else in the corpus exercises over a file actually on disk (the door's specimen carries its module source inline). The wrong-hash refusal is part of that route's contract and this pair does not claim it. Containment, not a whole-file golden, so editing the fixture's prose is not a test failure.The emission claims ran the full disk→emit walk in the first commit and cost ~1.2s each — over the floor's 500ms per-claim ceiling, three times, recomputing an 878ms assembly of one file's content. They now read the shared specimen, and the two emissions are themselves warm-enrolled nullary producers. Review 62939 caught that the fixture's annotation still described the old composed route; it now states the seam it is actually the subject of.
The remainder (ruling class 3), measured per form rather than predicted
x > ytarget_value_expr_reason_transform_shape_invalid, at the first operand, not the operator!ax + 1infer_grounding_not_derived— integer literals areValue-kind, no rulelet z = …infer_grounding_not_derived—Bind-kind, no rulev: Int?Atomshapesmatch v { Present … }resolve_reason_unbound_symbola && bandx + yemit fine, so this is not "complex expressions".04_infer'snode_grounding_frontier_notestates it: six of twelve node kinds derive, "Transform add-shape only". So a production-compatible corpus module is gated on that open inference frontier — and>failing while&&passes is a resolution/layout question, sinceop_gtis already in the canonicalization table.Noted, not fixed: an unspelled type binding prints its symbol lexeme (
bool_node_symbol) instead of refusing, and Rust'sboolspelling exists twice (aTargetAtomRealizationand a binding-spellings row). The repair is produced-decl type refs consulting the atom realization catalog.Roadmap
v2-emitter-production-compatible-corpus-moduleadded between the door and the flip,v2-emitter-first-behavioral-modulere-parented under it, so the flip node keeps its own fact: that production regeneration actually selected v2 and could not reach the old generator.ROADMAP.mdregenerated;generated_artifact_gate mainagrees.Also in this PR: the crate partition, named as a step
Added after the mega-crate analysis, verified against the tree rather than taken on report:
emitted_closure_compile_hostrequires exactly onesrc/lib.rsper crate dir, and00_compile.dag's closure is ~170 modules beneath it.v2.std.compilers.compilation_unitseparates a language module from a separately-compiled unit, derives cross-unit dependencies, closes interfaces over by-value type definitions, and refuses a split SCC / unit cycle / unrepresentable by-value cycle.v2.workflow.rust_crate_partitionalready generates manifests and crate roots for a real seven-package split.PolicyResolverUnimplementedis what the count-only policy resolver returns.So this adds one edge, not a plan:
v2-emitter-native-crate-partitionbetweenv2-emitter-first-behavioral-moduleandv2-emitter-native-bootstrap. Its RED control is deliberately stronger than "crate count > 1" — a module owned by two units or none refuses, a unit cycle refuses, a deliberately broken cross-unit export must fail the build rather than be papered over by wildcard re-exports, and a leaf edit must be shown to rebuild only its own dependents.This lane met that class from the other end already: the stage0 profile above exists because a module crossing a crate boundary needs
pub, which a single crate never asks for.Deliberately not added: a
SingleClosureProbeCratedisposition type. Nothing would read it today, and a carrier with no consumer is §3c's dangling modeling. The active roadmap row is the carrier that cannot be quietly kept — it is read every session and cannot be accepted while the artifact is one package.mainis merged in;roadmap_authority_test's two affected chain witnesses PASS;ROADMAP.mdregenerated and the artifact gate agrees.Test plan
claim_batch … stage0_production_target_test.dag— 5/5 PASS, plus the two single-axis mutation runs above.claim_batch … roadmap_authority_test.dag --functions witness_new_generator_precedes_fixed_point_and_old_generator_deletion— PASS.gunbc run … generated_artifact_gate --function main— agrees.pull_requestCI on this head — the PR targetsmain, sowitnesses.ymlruns normally and the exact-head run is the evidence.cargo fmt --all --checkclean via the pre-push hook.This branch started from #10692, which has since merged; the PR targets
mainandmainis merged in.🤖 Generated with Claude Code
https://claude.ai/code/session_011X5tyxfVrw3chDNbQ3sVD3