Repository navigation
Char codepoint atom identity minted through from_code_point: the source-to-target projection pair is inverse again - #9882
Closed
gunbai-bot[bot] wants to merge 161 commits into
Closed
gunbai-bot[bot] wants to merge 161 commits into
gunbai-bot[bot] wants to merge 161 commits into
Conversation
…nt, and a primitive with no realization refuses instead of inventing one Two roots behind 175 of the 260 rustc errors on the emitted v2 compiler closure (issue #9664, milestones 1 and 2): - 102 x E0425: the four DeclaredCallableIdentity constructions in v1.compiler.infer_lookup took decl_name from the AUTHORED spelling, so a qualified call carried the whole dotted path as the declaration name and emission rendered crate::v2_std_grammar::v2.std.grammar.f(..). - 73 x E0425: v2.std.algebra length is a ModeledProjection of the `length` primitive and rt_function_registry has no `length` row, so emission took rust_runtime_bridge_name's identity arm and wrote v1_rt::length -- a symbol the seed does not define. A primitive's identity and its per-target realization are two facts; CallTargetIdentity carried only the first, so every emitter had to ASSUME a bridge exists. RuntimePrimitiveCall now carries projected_from, the declaration the roster projected it from, and emit_rust routes to the bridge only when its own registry holds the primitive, falls back to the declaration otherwise, and refuses when neither exists. DeclaredCallableIdentity moves to v1.std.core so the target type can carry it without forking the pair. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
…ot checked tier0 method resolution resolves an ordinary fn-typed RECORD FIELD through lookup_field_in_product, so `algebra.step(..)` arrives as AlgebraMethodSemantics carrying the field node as its method_def. The fallback at the end of that arm hardcoded runtime_bridge: true, which emitted `v1_rt::step` -- and made emit_rust_generic_method_call's own callable-field arm, guarded on runtime_bridge == false, unreachable for the exact receiver it was written for. 65 E0425s on the emitted v2 compiler closure (member, apply, is_empty, step, init, allocate_literal, ...) were that one literal. It now passes the realization question keyed on the same registry as the plain-call seam, so a real bridge method still lowers to a bridge, a callable field lowers as a field, and a name that is neither reaches the existing loud refusal rather than a fabricated symbol. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
…y is a self-call, so falling back to it would emit a nonterminating function The declaration fallback is sound only where the declaration's body is real code. HostRealizedSeam means the body IS a self-call, so emitting it compiles and then loops forever -- silent wrongness, strictly worse than the unresolved symbol it would have replaced. A seam whose target has no realization has no honest lowering, so it carries nothing and reaches emission's refusal. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
…lared to be host seams
v2.std.compilers.lexing symbol_lexeme and symbol_intern_lexeme have self-call
bodies -- the HostRealizedSeam shape exactly -- and the interpreter has carried
real arms for both (v4_bridge.symbol_lexeme, v4_bridge.symbol_intern_lexeme).
With no projection roster row the resolver saw ordinary declarations, so Rust
emission emitted the declaration, and
pub fn symbol_lexeme(sym: String) -> String { symbol_lexeme(sym) }
COMPILES. The emitted closure carried two functions that type-check, pass every
gate we own, and diverge from the interpreter by not terminating. Unlike the
sibling seams (decl_facts and friends, which at least refuse loudly as
unresolved v1_rt symbols) nothing anywhere reported this one -- it is absent
from the E0425 census precisely because it is silent.
extdeps.languages.rust.types already declares Symbol's target type as String,
so on this target both bridges are the identity. That is a realization of the
declared row, not a second opinion about it.
Residue named, not closed: a self-call body is a DECIDABLE structural marker of
a host seam, so the compiler could refuse an unrealized one rather than emit it.
It does not yet; that check is the class's next-rung trigger.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
…round 2) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
…, with boundary controls Six rows over the three emitter defects plus the two symbol bridges. Each class's positive and negative assertion differ only in the fact the repair added, so no single edit satisfies both directions, and each repair carries a boundary control that would go red had it over-reached the other way (empty_map for the registry gate, a registered bridge method for the class-B gate). The symbol-bridge row is deliberately not an error-count assertion: that class COMPILED throughout the defect and diverged by not terminating, so a row asserting 'no error' would have been green the whole time. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
…never reaches the seam under repair count is answered by rust_simple_method_specs before the algebra fallback, so the row would have gone red while executing none of the code the repair touched. trim is in rt_function_registry and has no template, so it is one of the few names that actually reaches that fallback. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
The module index refused the file outright, so none of the six witnesses were discovered. .dag item declarations carry no terminator. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
…mitting compiling recursion A whole-body self-call is the decidable structural marker of a host seam. In the interpreter the shape is safe -- reaching it recurses to the evaluation-budget refusal -- but emitted to Rust the same shape COMPILES and returns to no caller. Nothing reported it: not the module index, not the compile-clean gate, not cargo check. That is why the two symbol bridges were invisible until someone read the emitted bytes. emit_fn_def now asks the realization registry -- the same authority the call sites ask, so the two cannot drift -- and suppresses the declaration when the seam is realized, refuses with a located message when it is not. Suppression rather than delegation is deliberate: a forwarding body would make this seam reconstruct signatures in target types, which is the cementing the existing suppressed-seam precedent avoids, and a realized primitive's calls all route to the bridge anyway. The predicate is whole-body identity, not 'contains a self-call'. Ordinary recursion has a match, an if or a let between the head and the call, so it never matches; expr_has_self_call walks children and would have refused most of the compiler. Both directions carry a fixture. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
…, not the declaration name Measured, not predicted: the wall refused six seams in the emitted closure and one of them -- v2.std.collection empty_map_primitive_delegate -- is realized. Its roster row names the empty_map primitive, whose bridge is rc_empty_map, but rt_function_registry holds 'empty_map' and the wall looked up 'empty_map_primitive_delegate'. A declaration's name and the primitive it realizes are two facts; the roster is the authority that joins them, and the declaration name is only the fallback for a seam nobody has rostered. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
…ession created 10 dangling imports Measured on the emitted closure with the wall finally in the mirror: removing a realized seam's item left 10 unresolved imports (E0432) for symbol_lexeme, symbol_intern_lexeme and resolve_type_node. Other modules import these declarations; the suppression created that breakage rather than finding it. And the reasoning that made suppression look safe is what makes it unnecessary. A realized seam's body IS a call to itself, and resolution already routes that call through the roster to the bridge -- so ordinary emission writes v1_rt::symbol_lexeme(sym) as the body without help. The wall's whole job is the UNREALIZED arm. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
…: rustc's denominator is larger than the demand denominator compile_error! fails the WHOLE crate, and that form silently assumes every seam it refuses is one somebody calls. It is not. rustc type-checks the entire emitted crate including declarations imported but never invoked, so the refusal denominator is strictly larger than the entry-reachable execution closure -- five unreachable seams took the crate down. The refusal is now a panic body with the declaration's real signature: dependent modules resolve, the crate compiles, and only an actual invocation fails loudly. That moves the refusal from the crate to the one declaration that earned it, and leaves reachability to a separate instrument. An entry-rooted pruner can replace the body later without revisiting this. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
…his change DETERMINISM DENOMINATOR (9 reach_witness rows red, including determinism_denominator_is_closed_on_declared_primitives, whose entire job is to notice this). v2.lens.determinism closes its denominator over primitive_declared_definitions, so adding two canonical names without traversal facts made the closure false. Both bridges are scalar -- symbol_lexeme maps one Symbol to its text and symbol_intern_lexeme is its inverse -- so there is no collection to walk and OrderFreeResult is the honest arm. HostUnspecifiedOrder would claim a real traversal whose order the host does not pin, fabricating a leak the primitive cannot have. NAMESPACE WAVE ADMISSION (6 unadjudicated deltas). Four are TargetChanged for DeclaredCallableIdentity moving v1.compiler.infer_sigs -> v1.std.core, which is what lets CallTargetIdentity carry the declaration a runtime target was projected from. infer_sigs imports v1.std.core, so the type could not stay put without a cycle. Four enumerated rows, one per binding site; the two membership deltas auto-admit as ExplicitlyEvaluatedZeroDelta. Dissolve-on: this PR merging, by the same trigger the three prior shrinks record. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
…er than the corpus The row FAILED while the mechanism was green. The probe used the qualified spelling without importing v2.std.collection, which resolves against the real 4261-module corpus but not against compile_dag_rust_emit_check's 2973-module witness pool. Measured both ways: emitted against the corpus the same probe produces crate::v2_std_collection::map_get(m.clone(), "key".to_string()), exactly what the row asserts. The import restores module presence and does not answer the call -- decl_name comes from the authored spelling at the call site regardless of imports -- so the negative assertion still discriminates. Falsifier 2 is what proves that rather than argues it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
…n it never had Before the class-B change, xs |> is_empty emitted v1_rt::is_empty, a symbol the seed does not define: 5 x E0425. After it, the same 5 sites became typed refusals -- correct in kind, still 5 errors. The class-B repair made the gap visible; it did not close it. is_empty is an algebra template over FreeMonoid whose Rust realization is Vec::is_empty, exactly as count's is Vec::len, so the fix is one row in rust_simple_method_specs beside count. Nothing in 05_emit_rust learns a new name: realization is a target fact and lives in the target's registry. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
…s B survived one layer up The requested is_empty negative control found a live hole rather than confirming a safe one. Both rust_method_templates lookups are keyed on the bare method spelling with no receiver check, so a fn-typed record field named is_empty was captured by the target template and emitted as recv.is_empty() instead of (recv.is_empty)(..). The class-B repair fixed the algebra FALLBACK and left the two tables sitting in front of it. The hole is not new and is not specific to is_empty: count, first, join, split, take, skip, last, chars and enumerate have carried it for as long as they have had templates. Adding is_empty made it urgent by putting the spelling most likely to name a predicate field in front of that table. One helper, consulted at the top of both arms before every name-keyed special case, so the two cannot drift. Two controls: the new spelling and a pre-existing one. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
v1.compiler.infer_sigs used to DECLARE DeclaredCallableIdentity, so its own two construction sites resolved locally and produced no delta. Now that the declaration lives in v1.std.core and infer_sigs imports it, those sites rebind exactly like the consumers in infer_lookup. An enumeration error on my part, not a second transition: same subject, same trigger, same dissolve. Floor is now green on this branch (passed=2754 failed=0) -- the OrderFreeResult traversal facts closed all nine determinism rows. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
# Conflicts: # src/v1/stage0/src/v1_compiler_emit_rust.rs # src/v1/stage0/src/v1_compiler_infer.rs
…domain, not the receiver's: 202 refusals on the first compile of the converged seed rust_receiver_has_callable_method_field asked rust_record_field_needs_fn_rc, which sweeps rust_struct_field_lookup_candidates -- and that list deliberately widens a receiver's name to its container template algebra. An algebra declares its operations as arrow-typed members, so under that widening every Map receiver "has a callable field" named map_keys, map_values, lookup or get, and the tier captured the very bridge calls it sits in front of. Measured at the first compile of the round-3 converged mirror: 202 rustc refusals, one class -- 164 E0609 (no field `map_keys` on Rc<im::HashMap<String, Rc<ItemInfo>>> and friends), 48 E0282, 4 E0615 on `get`. It is the same defect the tier was built to close, one level up: a name-keyed lookup consuming an identity domain that is not its own. The predicate now consults only the receiver's own declared record. w_map_receiver_operation_is_not_read_as_a_callable_field is the discriminating red: restore the candidate sweep and its must_not_contain clause fires. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
… point at round 3, six paths, each explained by an authority change Convergence transaction on srv1 (/tmp/xl0c.sh -> /tmp/xl0g.log), on 952ffa6 = main b726547 merged with the branch. Criterion is BYTE equality (sha256 over the whole candidate tree vs the whole installed tree), never first_generation_equal and never the changed-path list; the full workspace is rebuilt inside every round so a non-compiling mirror stops the line. round 1 cand e212fe74 inst 6f55cf3e installed, compiles round 2 cand 932b0543 inst e212fe74 drift = v1_rt.rs only (the two-hop: v1_rt.rs is rendered by the previously compiled rt_hash_ops) round 3 cand 932b0543 inst 932b0543 BYTE FIXED POINT -- produced by a compiler rebuilt from the round-2 installed tree Changed paths and their authority: extdeps_languages_rust_emit.rs <- rt_function_registry / rust_simple_method_specs rows std_primitive_projection.rs <- symbol_lexeme / symbol_intern_lexeme roster rows v1_compiler_emit_rust.rs <- 05_emit_rust.dag (seam wall, callable-field tier, class B/C) v1_compiler_infer.rs <- 04_infer.dag projected_from on RuntimePrimitiveCall v1_compiler_runtime_rust.rs <- runtime_rust.dag symbol bridges v1_rt.rs <- same, one hop later On these bytes: function_value_named_application_controls_witness PASSES (the d805243 / 952ffa6 rust-unit-tests red was the merge-driver-refused stale v1_compiler_infer.rs, not a semantic regression); emit 175 files; cargo check 15 errors: 9 E0425 (filesystem 2, V 2, K 2, Determinism 2, T 1), 2 E0728, 2 E0107, 1 E0391, 1 UNRESOLVED_CompilerError. No hand edit to any generated file. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
…a4e965ddb built from the committed mirror): v1_compiler_emit_rust.rs regenerated; candidate patch sha 05ce734c52890571
… installed ce959e40604ffdd5): std_algebra.rs, std_nat.rs -- arrow returns now render through the Rust renderer (Rc<Vec<K>> for List<K>, Nat preserved); candidate patch sha b5b409aeebbeb6c4
…fect shapes: the unconditioned route emitted 2790 refusals where 15 stood; fix the arrow probe's variant spelling
…bda's admission; F: a qualified type reference earns its use-line from the qualifier under export proof; both earlier cuts were measured non-events and are deleted
…at round 3, three paths, each explained by an authority change srv1 (/tmp/xl0e.sh -> /tmp/xl0j.log), criterion = every regen-population file byte-equal to installed; full workspace rebuilt as the gate each round. round 1 gunbc=1dc61ba198c6750b from installed 0479b0df9fc5598e -> v1_compiler_emit_rust.rs round 2 gunbc=909aa212f353bd03 from installed 8ebedc7445fadbaa -> std_algebra.rs, v1_compiler_trait_derive_emit.rs round 3 gunbc=0d0cd70ec5b20db9 from installed 8713cb43f8ad848c -> <none> BYTE FIXED POINT v1_compiler_emit_rust.rs <- 05_emit_rust.dag (gated arrow position, init turbofish admission, qualified-type use-lines) std_algebra.rs <- the gated arrow route restores the pre-e9900e2 spelling of the two arrow-typed fields v1_compiler_trait_derive_emit.rs <- one use-line synthesized for a qualified std.types.List reference under export proof Final installed tree 8713cb43f8ad848c. No hand edit to any generated file. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
…e variant arm; the qualified route synthesizes use-lines only for types the emitted source names Four regressions the 0773184 fixed point put on the closure, each with its discriminating row: - E0603 x16: the qualified-type route synthesized `pub use crate::v2_std_nat::Succ;` for every `v2.std.nat.Succ { prev: .. }` record literal. A qualified name reaches the surface walk in the same dotted spelling whether it is a type or a variant head; the route now asks the registry whether the leaf is a TYPE declared in the named qualifier, records each decision as a census row, and considers only leaves the emitted source actually names (it had also synthesized an unused `DeclarationRef` import from a variant payload). w_qualified_variant_head_earns_no_type_use_line. - `Outcome<compile_error!("UNRESOLVED_CompilerError")>` x3 and `Rc<Medium>` E0107: two cuts had each introduced a second per-position renderer for arrow types beside the one fn parameters use. An arrow's return is not a different kind of type from its parameter: both positions now render through render_rust_fn_sig_type, and render_rust_type_with_applied_binding -- which rebuilt its EmitGraphInfo with an empty generic scope, so a fn-scope `C` rendered `_` (E0121) -- carries the fn's generic names through that hop. The measured gate over the second renderer is deleted. w_generic_arrow_return_renders_the_fn_scope_generic; w_arrow_return_type_keeps_its_applied_binding (its fixture was an invalid program: Accepted lacked `diagnostics`). - v2.std.determinism E0425 x2: traced to the bare-name disposition, not the qualified route -- `Determinism` is a type in std.determinism and a variant of v2.lens.registry LensIdV0, and is_known_variant is corpus-wide by spelling, so a TYPE-position reference was delegated to an enum it never named. A name in one of the module's type positions never takes the variant arm. a_known_variant_spelling_in_a_type_position_takes_the_registry_arm (red by construction on the old arm); the harness row is a positive control and says so, because the witness harness refuses any pool carrying the colliding variant with NoSuchVariable. Verified on a test binary built from the self-emitted emitter (not a regeneration): witnesses 23/24 -> 24/24 after the harness row was reshaped; closure instrument 2799 -> 2779. The regeneration that binds these to the mirror follows as its own commit after the freeze merge. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
…ution mixed pre-main mirrors with main consumers of compile_sources_selected -- E0432 on round 1); hand-maintained interpreter arms re-inserted (4 ExprElaboratedLiteral arms, EXPR_VARIANT_COUNT 23) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qao5PDTLMpAjCGQDUELuiM
…s reference ExprElaboratedLiteral, which only regen adds to v1_std_core); the arms are re-inserted mid-convergence and land with the regen commit Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qao5PDTLMpAjCGQDUELuiM
… to the c7b8056-compatible three-hop state, recording each measured failure in place: leaf-name guard 108->174, terminal census hop ->569, module-binding rederivation ->437, one-authority renderer ->745. The shadowed-module class stays open under the boundary-lane declared drop with its fix shape on the class row; natively-coherence (destination census file) is kept Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qao5PDTLMpAjCGQDUELuiM
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qao5PDTLMpAjCGQDUELuiM
… census-file coherence read was deleted with the census hops and its consumer refused regen) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qao5PDTLMpAjCGQDUELuiM
…ated_binding_shadows_bare_render + surface_shorthand_preempts_resolved_identity); projections ours pending main_wet regen Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qao5PDTLMpAjCGQDUELuiM
…ines when the conflict markers were stripped mechanically -- both rows now well-formed (this parse error silently refused regen, which my capture filters then hid) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qao5PDTLMpAjCGQDUELuiM
…merged tree (rounds 2, 3 and the final rebuilt-binary check all equal); interpreter hand arms restored; DESIGN/design-ledgers projections carry both new recurring-failure class rows Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qao5PDTLMpAjCGQDUELuiM
…mirror set taken from main (self-consistent with the new assembly), regen re-derives this branch's authorities; projections re-derived by main_wet next round Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Qao5PDTLMpAjCGQDUELuiM
…longside main's stage0 mirror set (regen re-derives the literal-elaboration rows)
…bootstrap tree — literal-elaboration/operator-realization/structural-bindings mirrors re-derived and installed, partition lib rows and the four ExprElaboratedLiteral interpreter hand arms restored (EXPR_VARIANT_COUNT 23) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01R4A6MRdzeYxNr7dRbugcUC
# Conflicts: # dag/gunbc/structural_realization_bindings.dag # dag/std/literal_elaboration.dag # dag/std/operator_realization.dag # dag/test/claim/self_host_peano_literal_operator_realization_witness_test.dag # src/v1/00_core.dag # src/v1/04_env.dag # src/v1/04_infer.dag # src/v1/05_emit_rust.dag # src/v1/stage0/src/gunbc_structural_realization_bindings.rs # src/v1/stage0/src/std_literal_elaboration.rs # src/v1/stage0/src/std_operator_realization.rs # src/v1/stage0/src/v1_compiler_coercion.rs # src/v1/stage0/src/v1_compiler_compile.rs # src/v1/stage0/src/v1_compiler_complexity.rs # src/v1/stage0/src/v1_compiler_dag_collect_support.rs # src/v1/stage0/src/v1_compiler_emit.rs # src/v1/stage0/src/v1_compiler_emit_rust.rs # src/v1/stage0/src/v1_compiler_infer.rs # src/v1/stage0/src/v1_compiler_infer_env.rs # src/v1/stage0/src/v1_compiler_infer_resolve.rs # src/v1/stage0/src/v1_compiler_ownership.rs # src/v1/stage0/src/v1_std_core.rs # src/v2/test/claim/self_host/peano_nat_structural_realization_test.dag # src/v2/workflow/floor_expected_red.dag
…ree (round 2 equal) — the mirror delta vs main is exactly the four text-family files the re-added UnicodeScalarSequenceUnfold row touches Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01R4A6MRdzeYxNr7dRbugcUC
…tches in peano_nat_structural_realization_test over the re-added UnicodeScalarSequenceUnfold variant (both witnesses PASS scoped), and retire the XL-0N #9719 wave-admission row by its own dissolve-on trigger (base and head both carry the relocation; the run on bc74b2e reported it stale) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01R4A6MRdzeYxNr7dRbugcUC
# Conflicts: # src/v1/stage0/src/namespace_wave_admission.rs
…(declaration_ref_of_type_node with by-name + qualified-census fallback, scoped to the elaboration destination read; XL-0N's operand reader untouched), delete the resurrected name-keyed text op overrides and host_string_text seam arms from 05_emit_rust, restore the ExprElaboratedLiteral arm in data-value emission, and narrow the ops witness excludes to the overrides' exact receiver forms (bare .is_empty() red the structural Vec lowering — substring-oracle over-match). Text battery 11/11, peano 29/29, regen at byte fixed point Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01R4A6MRdzeYxNr7dRbugcUC
# Conflicts: # dag/gunbc/rung_drop.dag
… text_boundary_identity_wall row intact (the union regex had split on a '=======' line inside an authored string — parse error at the module index), retake main's stage0 set (the generated-artifact merge driver had left ours-bytes marker-less on namespace_wave_admission.rs), regen re-derives the six text-family mirrors to the byte fixed point (round 2 equal); text battery 11/11, peano 29/29 Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01R4A6MRdzeYxNr7dRbugcUC
# Conflicts: # src/v1/stage0/src/v1_compiler_emit_rust.rs
…curring_failure_mode rows) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01R4A6MRdzeYxNr7dRbugcUC
…t survives resolution (FreeMonoid+Char), natively reads the destination's own declaring file, witnesses re-anchor on the qualified boundary The #9813 kernel-precedence landing exposed that the text row was keyed on information resolution deliberately discards: String is a container-alias spelling, so every 'type X = FreeMonoid<Char>' boundary peels to the bare structural carrier and no module spelling survives to key on. The row now keys on that surviving structure — destination std.algebra.FreeMonoid with element std.types.Char (LiteralHomomorphism gains an element field, threaded through literal_homomorphism_for/elaborate_literal_at; peano and bool rows carry element: none). Second repair on the same boundary: destination_realizes_natively was read from the RESOLVED NODE's ident_span file, and a substituted alias RHS is a kernel-minted node whose pseudo-file <kernel:std.algebra.FreeMonoid> string-matched the '<kernel:' native-numeric roster row, so the peeled structural boundary answered natively=true and took DirectLiteral with the matching row present. natively is now read from the DESTINATION declaration's own census file (declaration_file_of in 04_env), per numeric_realization_identity_note's own rule that realization is a fact about the declaration. Witness battery re-anchored per the division ruling: the seven positive rows probe the QUALIFIED v2.std.text.String boundary (each probe imports string_is_empty so the harness's import-following closure loads the text module), and a new control pins bare String + text import = host, deterministically, under uniform kernel precedence. 12/12 text rows and 29/29 peano rows green by execution; stage0 mirrors regenerated to first-generation byte fixed point on the merged tree. Also: recurring_failure_mode row mistyped_body_radiates_nonlocal_diagnostics (the phantom-diagnostic specimen, layer stated), DESIGN.md and docs/design-ledgers.md regenerated via generated_artifact_gate main_wet_one, stale rust_host_string_seam_fn_emit comment fixed (review 57929). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01R4A6MRdzeYxNr7dRbugcUC
…current recurring_failure_mode rows; DESIGN.md and design-ledgers.md regenerated from the merged authority Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01R4A6MRdzeYxNr7dRbugcUC
…icted generated mirrors taken from main pending regeneration from the merged authority Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01R4A6MRdzeYxNr7dRbugcUC
…ring the inverse pair
target_value_expression_char_unicode_scalar placed a decoded Char directly into
Atom { identity: ... }. Connective::Atom declares identity: Symbol, and v2.std.node
declares `type Symbol` with NO ARMS -- an opaque nominal with no constructor -- so
nothing in the source language refused a branded Int there. The violation surfaced
only in the emitted target, as E0308 expected `String` found `i64` at
v2_std_compilers_target_model.rs:2606:15.
The identity is now minted with from_code_point(cp: codepoint), the declared inverse
of the code_point that source_atom_char_projection_from_node uses to read the value
back, so the projection pair is inverse again and the class is decidable at the .dag
layer rather than at rustc.
Measured on pristine origin/main (0e8c49d) with this change alone applied:
0 inhabitance errors, the closure resolves clean.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019o3436yxdGdYZa53YopdQH
Contributor
Author
|
Merged-tree receipt, closing the gap the PR body flags. The clean-resolve measurement in the description was taken at the pre-merge base Zero inhabitance errors on the composed tree, same arm reached. So the receipt holds post-merge, not only against the base I originally measured. |
Contributor
Author
|
Closing as SUPERSEDED, not resolving the conflict — the row this PR repairs no longer exists on main. Checked the row before touching the conflict, per the sequencing that matters here: resolving first would have produced a file that compiles and looks right either way, hiding the redundancy.
landed by #9854 ( Their repair is better than mine and I'd rather have theirs. What survives from this PR is in its body and worth keeping findable:
— sent from vivid-deer-102 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What this is
One two-line repair to
v2.std.compilers.target_model, closing the row routed to this lane asv2_std_compilers_target_model.rs:2606:15—E0308, expected String, found i64.target_value_expression_char_unicode_scalarplaced a decodedCharstraight intoAtom { identity: … }.Connective::Atomdeclaresidentity: Symbol, and the identity is now minted withfrom_code_point(cp: codepoint)— the declared inverse of thecode_pointthatsource_atom_char_projection_from_nodeuses to read the value back. The projection pair is inverse again, and the class becomes decidable at the.daglayer instead of at rustc.Why the violation was invisible
v2.std.nodedeclarestype Symbolwith no arms — an opaque nominal with no constructor — so nothing in the source language refused a brandedIntin aSymbol-typed field. The mismatch surfaced only after realization, as rustc spelling the two host types.Named candidate for the recurring-failure roster, not censused here: a zero-arm
type Xis inhabited by anything, so the floor guarantee "values inhabit declared types" is silently absent wherever one is used as a field type. Adjacent tosingle_arm_coproduct_is_a_type_alias, which breaks at the importer rather than the declaration. This row is one instance; nobody has counted the others.Evidence
Measured on pristine
origin/main(0e8c49ddee9) with this change alone applied,git reset --hardbefore the run, diffstat printed as a receipt:Zero inhabitance errors; the closure resolves clean and gets all the way to the roster refusal, which is a different arm and not this change's subject.
Scope held back, deliberately
This lane's carrier work — the
v2.std.compilers.lexingand01_tokenizerespelling, and a repair tov1.compiler.emit_rust is_host_text_carrier_type— is not in this PR, under an explicit manager ruling. Two reasons worth recording:lexing.dag's declaring side to the qualifiedv2.std.text.Stringmakes 29 host-Stringproducers inextdeps/languages/bash.dagcorrectly refuse. Those are revealed, not introduced — they were type-checking against aStringthat was never structural. Repairing them is not mechanical: 4 of the 8 enclosing functions take host-Stringparameters whose callers reach out ofextdepsintosrc/v2/workflow, andv2.std.texthas no host→structural conversion to stop the ripple at the boundary.is_host_text_carrier_typerepair closes the probe shape it was aimed at but emitspub fn string_is_empty(s: String<i64>)inv2_std_text.rs— not valid Rust. Held as defective.Two notes for whoever regenerates next
main_wet_oneis the wrong actuator forsrc/v1/stage0/src/v1_compiler_emit_rust.rs. It refuses withGeneratedArtifactPathUnrostered— the path is not among the 35committed_generated_artifactsrows. That mirror regenerates throughclaim_executor --required-regen.gunbc … | tailreports the pipeline's last stage, so aresolve failedrun reads as exit 0. Cost me a false "regen green" tonight. UsePIPESTATUSor redirect to a file.