Skip to content

Faithful String element Nat->Char: de-double FreeMonoid<Char>, single application - #5532

Merged
briansrls merged 2 commits into
mainfrom
emitter/faithful-carrier-single-application
Jun 22, 2026
Merged

briansrls merged 2 commits into
mainfrom
emitter/faithful-carrier-single-application

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Jun 22, 2026

Copy link
Copy Markdown
Contributor

Faithful String element: Nat→Char de-double (single application)

The faithful Rust carrier (corpus_repr=FaithfulFreeMonoid) baked String's element as Nat — an unauthorized emitter-side Char→Nat grounding shortcut contradicting the declared std alias (std/string_type.dag: String = FreeMonoid<Char>, "the free monoid over Char"). This rendered String leaves as FreeMonoid<Nat> and applied sites as the double FreeMonoid<Nat><Char> (base baked <Nat> and the resolved Char child appended).

Fix (emit-side, faithful-guarded)

Per quick-seal's ruling — this removes a grounding shortcut, it does not add one. Render String's declared element Char uniformly, single application:

  • rust_named_type_base: leaf base FreeMonoid<Nat> → FreeMonoid<Char>
  • render_rust_text_carrier: FreeMonoid<Nat> → FreeMonoid<Char>
  • new rust_applied_type_base: bare FreeMonoid base for the applied path, so the resolved Char child drives the single application (no element literal → no double)
  • render_rust_applied_type / render_rust_decl_type: applied sites use the bare base

The leaf Char is a time-bounded scaffold (a leaf type-node carries no resolved type-arg, so the element cannot be read from the node). Dissolve-on: when resolve attaches the element to String leaf nodes uniformly (resolve-side), the literal + the String special-case delete — String then expands as an ordinary closed alias.

Char→Nat reduction is not touched (the operator-parked algebra thread): Char emits as its own branded-Int form (type Char = i64); FreeMonoid<Char> compiles clean.

Proven by execution

Full-crate cargo-green is deferred behind the ~150-gap import lane — this fix owns the double-generic class, not the full-crate green:

  • census (re-emit faithful dsl corpus): FreeMonoid<Nat> 2315→0, FreeMonoid<Char> 2315 at leaf+applied, double-applications 72→0
  • render-witness (faithful_string_element_char_witness_test, RED-on-revert): leaf, text-carrier, bare applied base, single-application, + host control — 5/5 green
  • Char-compiles: FreeMonoid<Char>=FreeMonoid<i64> well-formed (unbounded FreeMonoid<T>)
  • host-seed byte-identical: fixed vs pristine emitter on the host corpus → no diff (faithful-only)

Scope honesty

Not a §7 fixpoint; the seed mirror is a hand-synced mirror (the two standing drifts re-applied). The ~150-gap full-crate cargo-green remains the deferred regen-fixpoint lane (node://adhoc-80af9ff8-40f).

🤖 Generated with Claude Code

briansrls and others added 2 commits June 22, 2026 14:59
… application

The faithful Rust carrier (corpus_repr=FaithfulFreeMonoid) baked String's element as
Nat -- an unauthorized emitter-side Char->Nat grounding shortcut contradicting the
declared std alias (std/string_type.dag: String = FreeMonoid<Char>, "the free monoid
over Char"). This rendered leaves as FreeMonoid<Nat> and applied sites as the double
FreeMonoid<Nat><Char> (the base baked <Nat> AND the resolved Char child appended).

Fix (emit-side, faithful-guarded; quick-seal ruling -- removing a grounding shortcut,
not adding one): render String's DECLARED element Char uniformly, single application.
- rust_named_type_base: leaf base FreeMonoid<Nat> -> FreeMonoid<Char>
- render_rust_text_carrier: FreeMonoid<Nat> -> FreeMonoid<Char>
- new rust_applied_type_base: bare FreeMonoid base for the applied path, so the
  resolved Char child drives the single application (no element literal -> no double)
- render_rust_applied_type / render_rust_decl_type: applied sites use the bare base

The leaf Char is a time-bounded scaffold (a leaf type-node carries no resolved
type-arg, so the element cannot be read from the node). DISSOLVE-ON: when resolve
attaches the element to String leaf nodes uniformly (resolve-side), both the literal
and the String special-case delete -- String then expands as an ordinary closed alias.

Char->Nat reduction is NOT touched (the operator-parked algebra thread): Char emits
as its own branded-Int form (type Char = i64), FreeMonoid<Char> compiles clean.

Proven by execution (full-crate cargo-green DEFERRED behind the ~150-gap import lane;
this fix owns the double-generic CLASS, not the full-crate green):
- census: re-emit faithful dsl corpus -> FreeMonoid<Nat> 2315->0, FreeMonoid<Char>
  2315 present at leaf+applied, double-applications 72->0
- render-witness (faithful_string_element_char_witness_test, RED-on-revert): leaf,
  text-carrier, bare applied base, single-application, + host control
- Char-compiles: FreeMonoid<Char>=FreeMonoid<i64> well-formed (unbounded FreeMonoid<T>)
- host-seed byte-identical: fixed vs pristine emitter on the host corpus -> no diff

Seed mirror v1_compiler_emit_rust.rs regenerated + the two standing hand-sync drifts
re-applied (inline cargo header, no extdeps_cargo_version orphan import).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…review)

The import added in #5481 (extdeps.version.semver { SemVerConstraint }) is unused in
cargo.dag -- the only occurrence was the import line itself. Flagged by review on #5481,
deferred to this PR.

Separate witness from the faithful-String fix: re-emitting the faithful dsl corpus after
the drop is clean (416 files, 0 diagnostics; FreeMonoid<Nat>=0 / FreeMonoid<Char>=2315
unchanged) -- the import is genuinely dead, the drop reds nothing.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Jun 22, 2026

Copy link
Copy Markdown
Contributor Author

Manager sign — PASS by execution (emission/medium lane), on head bf59aaae39. Faithful-carrier double-generic emit fix.

What this signs. The faithful Rust target emitted String (declared FreeMonoid<Char>, std/string_type.dag) two ways wrong: the leaf base hard-coded FreeMonoid<Nat> (an unauthorized emitter-side element grounding contradicting the declared alias), and applied sites concatenated leaf-base + resolved child → the double FreeMonoid<Nat><Char>. The fix renders the declared element uniformly: leaf base → FreeMonoid<Char>, applied base → bare FreeMonoid + the single resolved child. This is faithful alias-expansion (emit-side), not the parked Char→Nat grounding thread — it removes an emitter-side grounding rather than deciding one.

Load-bearing proof — render-witness, re-run by me on this exact head (5/5 green, not carried forward): faithful_string_element_char_witness_test — leaf_base/text_carrier = FreeMonoid<Char> (each with the discriminating assert_ne against the old Nat); applied_base = bare FreeMonoid (no <); applied_single_application_not_doubled (FreeMonoid<Char> ≠ FreeMonoid<Nat><Char>); host_string_unchanged_by_faithful_fix (the host control — HostNative String never contains FreeMonoid, so the fix is faithful-only via the corpus_repr_is_faithful guard). These execute the actual render helpers; each asserts both the new value and the old-wrong value's absence.

Census-0 by construction (sign-bar a — stronger than a corpus grep). I enumerated every FreeMonoid emit site in the Rust emitter and traced its dispatch: the leaf base (rust_named_type_base, 05_emit_rust.dag:333) is the single authority producing every String leaf instance (swift-bee's 2315), the applied base (rust_applied_type_base:346) is the single authority for every applied String (the 72 doubles), and both now render Char/single — so the reported 2315→0 / 72→0 is the mechanical consequence of two single-authority functions each flipping Nat→Char, each witness-exercised. The text carrier (:244) already emits FreeMonoid<Char>. The only other FreeMonoid literals (FreeMonoid<K>/<V>, :360/:362) are PartialFunction/Map container coercion on Map K/V params — not String's Char element — correctly untouched. No fourth String-emit path exists.

Residual-risk routing (cleared). "Does FreeMonoid<Char> compile without Char→Nat reduction?" — verified CLEAN (Char = Int where unicode_scalar brand, so FreeMonoid<Char> is well-formed FreeMonoid<i64>); parent affirmed the emit-side ruling and holds the FreeMonoid grounding cluster if it ever fired. It didn't.

Honest naming (no overclaim). This signs the double-generic emit CLASS as fixed (render-witness + single-authority census). Full-crate faithful cargo-green is DEFERRED behind the pre-existing ~150-gap duplicate-import lane (~150 ∩ this fix = ∅); that lane aborts name-resolution before type-check, so a literal corpus-compile census is unreachable today — the render-witness + construction census carry the sign, named as such.

Dissolve-on verified. The Char literal is a marked §3 time-bounded second-representation scaffold (a leaf type-node carries no resolved type-arg, so the element can't be read at the leaf); the dissolution trigger — resolve-side uniform-element attachment so the applied path's single-child mechanism covers the leaf too — is named at the carrier. Correct.

Contribution clean. merge-base b44684a8cc is a clean ancestor; the real delta is the 5 faithful-carrier files (the extras in origin/main..head are stale-base reverse-deltas of intervening merges). mergeable=MERGEABLE confirms no conflict.

Merge-ready under the relaxed 1-bar on CI green (BLOCKED is CI IN_PROGRESS, 0 failing). Relaying to the operator queue on green.

— sent from quick-seal-137

@briansrls
briansrls merged commit 630ac96 into main Jun 22, 2026
1 check passed
@briansrls
briansrls deleted the emitter/faithful-carrier-single-application branch June 22, 2026 17:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant