Skip to content

The bodyless-type exposed subset is four names of 66, 1045 of it Symbol — and a nullary alias rendered with an applied type argument - #9888

Merged
gunbai-bot[bot] merged 2 commits into
mainfrom
session/vivid-deer-102
Sep 1, 2026
Merged

gunbai-bot[bot] merged 2 commits into
mainfrom
session/vivid-deer-102

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 1, 2026

Copy link
Copy Markdown
Contributor

The headline is four names, not sixty-nine

#9879 filed the third inhabitance seam — any bodyless type X admits any argument in parameter position, silently — and stated that the exposed subset was smaller than the syntactic population and unmeasured. This measures it.

4 of 66 distinct names are reachable in parameter position, where a non-inhabiting value can actually flow in:

name module parameter sites
Symbol v2.std.node 1045
SourceSpan v2.lens.application 129
Bytes std.types 4
ConfigPatchRecord v2.std.patch 1

33 names appear only in field position. 27 appear in no parameter, field, or return position at all. So the class is small and its exposure is dominated by a single declaration — Symbol, the substrate's own identity field — by an order of magnitude over everything else combined. A census reported as "69 exposed positions" would bury that.

The two censuses join at identity, not at count

Re-derived independently at origin/main 6741a3953, per #9879's own instruction to re-derive rather than quote either number: 69 declarations / 66 distinct names, which agrees with that row's 69 exactly.

The reconciliation is the part worth keeping. A first pass matching ^type X$ found 62. The missing 7 are parameterized bodyless declarations — Compose<carrier, dimension>, MachineWidth<bits> (twice), ReferenceModel<T>, CppTargetDataModel<…>, CppTargetProfile<…>, ConfigPatchRecord<Config>. 62 + 7 = 69, so the two lanes agree on membership, not merely on a total.

Compose and MachineWidth turn out to be unexposed: type constructors applied as type arguments, never parameter types. Adding all 7 to the population moves the exposure count by one.

The naive count reproduces the broken instrument. Matching ^type X$ without reading the following line returns 5194 — within 1.5% of tools.opaque_realization_census's 5269 — because 5132 declarations carry = … or | … on the next line. I hit this before catching it by reading the hits, which is independent corroboration of that instrument's defect by accident rather than by design. Repairing the instrument is a separate PR (different subject; the prefix-boundary bug ranks first since it survives a fix of the other).

The ceiling is not one value

Reporting a single ceiling would overstate the row, because the population splits and the parts differ:

  • (a) Declared-abstract by ruling — Symbol, Unit. The attainable ceiling is not structural impossibility via arms; it is a construction discipline at the boundary, values entering only through a declared minting authority. symbol_intern_lexeme is such an authority, which is why XL-0-INFER: classify and repair inference-failure survivors #9854's repair of target_value_expression_char_unicode_scalar has the right shape where minting a host String via from_code_point did not. R3 at sites that go through one, R2 corpus-wide.
  • (b) The 27 type-level tags (cpp_abi widths, std.measure rate units, std.constructors' Product/Coproduct/Phantom). Nullary markers used as type arguments, not value carriers. Hole unreachable, honest ceiling no climb needed — filing them as exposure would inflate the class and bury the one member that matters.
  • (c) SourceSpan and Bytes — genuinely exposed, unruled, recorded so they stay countable rather than forgotten.

Class rung is the minimum across parts: below floor. The trigger names a capability, per §4b(3) — a bodyless declared type can be inhabited only through a declared minting authority, and the direct-call inhabitance judgment consults that authority. #9854's witness char_unicode_scalar_expression_carries_a_symbol_identity is a wall for one site and does not retire this row; the invalid state stays writable at the other 1044 Symbol parameter sites.

Method limits, carried in the row rather than left to be discovered: parameter sites are counted only on lines beginning fn /func , so multi-line signatures are undercounted; the field-position figure uses a looser match and may over-count. Both are bounds. The shape — four exposed names, Symbol dominating — is robust to both errors.

Second change: a new class

A nullary alias rendered with its body's type argument applied to it. Two instances, different aliases, one shape:

  • type LexText = FreeMonoid<Char> is nullary, yet a refusal at a LexText-declared parameter printed expected 'Node(LexText<Product(Char)>)'.
  • A repair to is_host_text_carrier_type emitted pub fn string_is_empty(s: String<i64>) into v2_std_text.rs — not valid Rust.

The harm is not the malformed spelling; it is that the malformed type reads as a real refusal. The LexText arm produced 129 refusals across three files where the qualified-spelling arm produced 30, and that 129 was reported and endorsed as a stricter wall over a larger population before the diagnostic text was read closely enough to notice the alias cannot take an argument. A population inflated by a printer defect is worse than a missing measurement, because it gets quoted.

It is distinct from the neighbouring non-confluence rows: those are two authorities disagreeing in two places; this is two decisions inside one rendered type expression — base name from one authority, type argument from another — which is why it survives every emitter-vs-resolver question currently open. It reaches both a resolve-stage diagnostic and an emitted Rust signature, so it is not confined to reporting.

The row deliberately does not name a repair site. The defect is in the type applier or the diagnostic printer, three lanes are converging on 05_emit_rust.dag, and naming a site would create a second authority for a fix nobody has scoped.

Provenance

Both instances reproduced on a binary built from a pristine origin/main export (6741a3953, modified-mirror-files=0, the is_host_text_carrier_type repair verified absent from the compiled mirror), each arm carrying a firing positive control — so neither is an artifact of the measuring tree. Earlier figures from this lane were produced by a binary built with that repair in the compiled mirror and were re-run before any of this was treated as a fact about main.

Neither row is enrolled: no probe asserts either, so nothing reds if the applier or the exemption changes. Both say so.

gunbc-ci-auto-heal and others added 2 commits September 1, 2026 04:59
… nullary-alias-applied-argument class

TWO CHANGES TO docs/plans/compiler-guarantee-recovery-gap-analysis.md, both building on
the third-inhabitance-seam row landed by #9879 rather than beside it.

1. THE EXPOSED SUBSET, which #9879's row explicitly left unmeasured.

Re-derived independently over dag/, src/v1/ and src/v2/ at origin/main 6741a39,
per that row's own instruction to re-derive rather than quote:

  69 bodyless declarations / 66 distinct names -- JOINING #9879's 69 at identity grain,
  not merely at count. A first pass matching ^type X$ found 62; the missing 7 are the
  PARAMETERIZED bodyless declarations (Compose<carrier, dimension>, MachineWidth<bits>
  twice, ReferenceModel<T>, CppTargetDataModel<...>, CppTargetProfile<...>,
  ConfigPatchRecord<Config>). 62 + 7 = 69, so the two censuses agree on membership.

Reachability in PARAMETER position -- where a non-inhabiting value can actually flow in:

  Symbol            (v2.std.node)          1045 parameter sites
  SourceSpan        (v2.lens.application)   129
  Bytes             (std.types)               4
  ConfigPatchRecord (v2.std.patch)            1

and nothing else. 33 names appear only in field position; 27 appear in no parameter,
field or return position at all. Compose and MachineWidth are among the unexposed --
type CONSTRUCTORS applied as type arguments, never parameter types.

So the headline is not 69: the exposure is dominated by ONE declaration, Symbol, the
substrate's own identity field, by an order of magnitude.

CEILING SPLIT THREE WAYS, because one value would overstate the row:
  (a) declared-abstract by ruling (Symbol, Unit) -- construction discipline at the
      boundary through a minting authority, NOT arms. R3 at such sites, R2 corpus-wide.
  (b) the 27 type-level tags -- hole unreachable, no climb needed. Filing them as
      exposure would inflate the class and bury the member that matters.
  (c) SourceSpan and Bytes -- genuinely exposed, unruled, recorded so they are countable.

Class rung is the minimum across parts: below floor. Trigger names the CAPABILITY per
4b(3) -- a bodyless declared type inhabitable only through a declared minting authority,
AND the direct-call inhabitance judgment consulting it. #9854's witness is a wall for
ONE SITE and does not retire the row.

METHOD LIMITS carried in the row: single-line fn matching undercounts multi-line
signatures; field position over-counts. Bounds, not exact counts; the shape is robust.

2. A NEW CLASS: a nullary alias rendered with its body's type argument applied to it.

Two instances, different aliases, one shape: a refusal at a LexText-declared parameter
printed expected 'Node(LexText<Product(Char)>)' though type LexText = FreeMonoid<Char>
is nullary; and a repair to is_host_text_carrier_type emitted
pub fn string_is_empty(s: String<i64>), which is not valid Rust.

The harm is that a malformed type READS AS A REAL REFUSAL: the LexText arm produced 129
refusals against the qualified spelling's 30, and the 129 was reported and endorsed as a
stricter wall over a larger population before the diagnostic text was read closely enough
to notice the alias cannot take an argument. A population inflated by a printer defect is
worse than a missing measurement, because it gets quoted.

Both instances reproduced on a binary built from a pristine origin/main export with the
is_host_text_carrier_type repair verified absent from the compiled mirror, each arm
carrying a firing positive control. The row deliberately does NOT name a repair site --
three lanes are converging on 05_emit_rust.dag.

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

eager-hawk-376 challenged the exclusion and they were right. DESIGN 4b judges
reachability BY WHAT A FIXTURE MAY AUTHOR, not by what the accepted corpus contains,
so "never used in parameter position in the corpus" is not grammar-absence.

Measured in an ordinary (non-v2.*) module, so seam (1)'s exemption is not in play,
against the pristine origin/main binary:

  fn vd_takes_phantom(x: Phantom) -> Int   fed "abc"  -> resolves clean, EXECUTES, returns 1
  fn vd_takes_persecond(x: PerSecond) -> Int fed 7    -> resolves clean, EXECUTES, returns 2
  planted positive control length(xs: n) on Int        -> REFUSES

The control is what makes the silence a measurement rather than a judgment that never
ran, and reaching the body makes this admission proven by execution rather than by a
silent compile.

So the 27 are CORPUS-UNOCCUPIED, not grammar-absent: exposure-on-first-use, acquiring
exposure the moment anyone writes the construct with nothing to refuse them. Filing them
as inert was the bounded-population-reads-as-progress trap.

Two of the 27 are measured, from two different declaring modules; the other 25 are the
same shape and are recorded by class rather than each by receipt, which the row says.

The exposure split is now three-way: exposed now (4 names, Symbol dominating),
exposure-on-first-use (27), grammar-absent (none found). Population, Symbol
concentration, below-floor rung and capability-grain trigger all unchanged.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019o3436yxdGdYZa53YopdQH
@gunbai-bot
gunbai-bot Bot merged commit d0009ca into main Sep 1, 2026
6 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/vivid-deer-102 branch September 1, 2026 05:42
gunbai-bot Bot pushed a commit that referenced this pull request Sep 1, 2026
…-gap census

#9888 edited the same row while this PR was open, so the merge is a real
resolution rather than a pick. Both sides survive:

- their exposed-subset measurement and the 69 / 66 reconciliation are kept
  VERBATIM, including the figures. Removing them to satisfy review 58065 would
  have been wrong: that review condemns transcribing a one-off with no producer,
  and their join is the opposite -- two lanes deriving the same population
  independently and reconciling it at IDENTITY GRAIN against a named ref, which
  is the re-derivation §6 asks for. Their "which JOINS THIS ROW'S 69 EXACTLY"
  also depends on the 69 upstream of it, so deleting the number would have left
  their sentence dangling.

- my own figures stay removed, because they are the case the review actually
  named: one-off scans with no committed producer.

The row now says which of the two treatments applies and why, so the next reader
does not read the asymmetry as an oversight, and records that both censuses
still owe the same committed producer.

The scope-gap census (ten of twelve positions have no obligation producer) is
carried through unchanged.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013wJU7jqGAEk8rj4UwpHdox
gunbai-bot Bot pushed a commit that referenced this pull request Sep 1, 2026
The conflict is one table region in docs/plans/compiler-guarantee-recovery-gap-analysis.md,
and resolving it is not a choice between two authors: #9868 was authored from a base
predating #9888 and #9889, so its squash silently reverted both of their rows while adding
its own. Verified by `git log -S` on the file: the scope-gap census text is added by
a7c72f0 (#9889) and removed by 8f82b55 (#9868), and the nullary-alias row goes the
same way via d0009ca (#9888).

Resolution keeps all three, because none contradicts another:
- the long inhabitance row (this branch), carrying the bodyless-type exposure split and the
  TEN-OF-TWELVE obligation scope census;
- the nullary-alias diagnostic row (#9888), re-inserted at its original position after the
  container-element row — git auto-merged main's deletion of it silently, outside the
  conflict region, which is exactly how the clobber propagates unnoticed;
- the sealed-carrier row (#9868), taken from main unchanged.

Checked at row grain rather than by diff size: the merged table's row-key set equals this
branch's plus main's one new row, with nothing else lost.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016CGc3k4QXMEdRqtPsSfmTv
gunbai-bot Bot added a commit that referenced this pull request Sep 1, 2026
…9943)

* File two failure classes found while repairing a stale-base clobber

Both come out of gunbc#9937 and neither is about that PR's content.

restored_bytes_reviewed_as_authorship — a clobber repair returns bytes a prior
PR already merged and a prior reviewer already accepted, but a diff cannot say
so: the restored lines are ADDED lines, so a reviewer attributes them to the
repairing PR. Review 58203 filed REQUEST_CHANGES against a §6 defect in bytes
character-for-character identical to #9888's merged row. The second-order effect
is why it is a class: it makes clobber repairs expensive to land, which biases
the fleet toward leaving clobbers standing. Recognition is decidable — added
lines byte-identical to a prior merged blob, answered by cmp against
`git show <sha>:<path>`.

review_summary_inverts_roles_and_affirms_the_join — review 58215 named files
that all exist, gave each the wrong role, and closed by asserting the one
property it was uniquely positioned to test ("diff is narrow and matches the PR
title") in the exact PR where that property failed. Distinct from a hallucinated
subject: an invention is refutable by grep, whereas here every noun is present
and only the relations are wrong, so checking that the cited things exist returns
all-clear.

The rows are single-line by deliberate reuse of this carrier's own
merge_region_excludes_shared_tail row, which states that the repair for its class
is a one-line appended unit; a multi-line row here would hand the next two lanes
exactly the conflict that row documents.

The backstop question is answered honestly in the second row rather than
comfortably: the required build lane's generated-artifact phase would have
refused the leak by construction, but that lane was CANCELLED on the leaked sha
when the next push superseded it, so it never ran and the author caught it. A row
claiming the gate held would assert an execution that did not happen.

DESIGN.md and docs/design-ledgers.md are projections of the roster and are
updated here to match; the required generated-artifact phase compares both
against their authority, so it is the executing check on that claim.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016CGc3k4QXMEdRqtPsSfmTv

* Both rows: the routing sentence was licence to merge a defect, and both now carry rung, ceiling and trigger (review 58220)

FINDING 1 IS CORRECT AND THE WORDING WAS THE DEFECT. The row said a finding
against restored bytes "belongs in its own diff", which reads as provenance
exempting the destination bytes from review — DESIGN §5's hard reject, and
inverted, since a restoration is precisely the motion that puts those bytes back
on main.

What the specimen actually established is the opposite, and the row now says it:
the §6 finding was correct, the repairing lane argued for routing it elsewhere,
the owning manager OVERRULED that, and the defect was repaired inside the
restoration under a ruling. Routing decides WHO answers and in which diff;
it never decides WHETHER. The row records its own wrong reading as refused,
because the earlier revision is the specimen for how the class gets misused.

FINDING 2: complied with, and worth stating what the honest answers are rather
than filling three cells. Both classes are mitigatable today. Both ceiling at
mechanically preventable and no higher, for the same reason stated differently:
nothing can make a restoration unwritable, and whether a summary describes a diff
correctly is undecidable — but the decidable part of each is what does the damage,
so the trigger names it. For the restoration class: the review surface
distinguishes restored bytes without the author asserting it, since an
author-supplied notice is exactly what a tired or adversarial diff omits. For the
review class: no verdict is admissible until a changed-file-set join against the
declared scope has executed — not a reviewer instructed to check it, which is the
same assertion that already failed, and not a lint on summary wording, which
would ratchet the prose while leaving the join undone.

docs/design-ledgers.md re-projected from the amended rows.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016CGc3k4QXMEdRqtPsSfmTv

---------

Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
briansrls pushed a commit that referenced this pull request Sep 2, 2026
…d transport in the present tense — decide and land its disposition (#9967)

* File two failure classes found while repairing a stale-base clobber

Both come out of gunbc#9937 and neither is about that PR's content.

restored_bytes_reviewed_as_authorship — a clobber repair returns bytes a prior
PR already merged and a prior reviewer already accepted, but a diff cannot say
so: the restored lines are ADDED lines, so a reviewer attributes them to the
repairing PR. Review 58203 filed REQUEST_CHANGES against a §6 defect in bytes
character-for-character identical to #9888's merged row. The second-order effect
is why it is a class: it makes clobber repairs expensive to land, which biases
the fleet toward leaving clobbers standing. Recognition is decidable — added
lines byte-identical to a prior merged blob, answered by cmp against
`git show <sha>:<path>`.

review_summary_inverts_roles_and_affirms_the_join — review 58215 named files
that all exist, gave each the wrong role, and closed by asserting the one
property it was uniquely positioned to test ("diff is narrow and matches the PR
title") in the exact PR where that property failed. Distinct from a hallucinated
subject: an invention is refutable by grep, whereas here every noun is present
and only the relations are wrong, so checking that the cited things exist returns
all-clear.

The rows are single-line by deliberate reuse of this carrier's own
merge_region_excludes_shared_tail row, which states that the repair for its class
is a one-line appended unit; a multi-line row here would hand the next two lanes
exactly the conflict that row documents.

The backstop question is answered honestly in the second row rather than
comfortably: the required build lane's generated-artifact phase would have
refused the leak by construction, but that lane was CANCELLED on the leaked sha
when the next push superseded it, so it never ran and the author caught it. A row
claiming the gate held would assert an execution that did not happen.

DESIGN.md and docs/design-ledgers.md are projections of the roster and are
updated here to match; the required generated-artifact phase compares both
against their authority, so it is the executing check on that claim.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016CGc3k4QXMEdRqtPsSfmTv

* Both rows: the routing sentence was licence to merge a defect, and both now carry rung, ceiling and trigger (review 58220)

FINDING 1 IS CORRECT AND THE WORDING WAS THE DEFECT. The row said a finding
against restored bytes "belongs in its own diff", which reads as provenance
exempting the destination bytes from review — DESIGN §5's hard reject, and
inverted, since a restoration is precisely the motion that puts those bytes back
on main.

What the specimen actually established is the opposite, and the row now says it:
the §6 finding was correct, the repairing lane argued for routing it elsewhere,
the owning manager OVERRULED that, and the defect was repaired inside the
restoration under a ruling. Routing decides WHO answers and in which diff;
it never decides WHETHER. The row records its own wrong reading as refused,
because the earlier revision is the specimen for how the class gets misused.

FINDING 2: complied with, and worth stating what the honest answers are rather
than filling three cells. Both classes are mitigatable today. Both ceiling at
mechanically preventable and no higher, for the same reason stated differently:
nothing can make a restoration unwritable, and whether a summary describes a diff
correctly is undecidable — but the decidable part of each is what does the damage,
so the trigger names it. For the restoration class: the review surface
distinguishes restored bytes without the author asserting it, since an
author-supplied notice is exactly what a tired or adversarial diff omits. For the
review class: no verdict is admissible until a changed-file-set join against the
declared scope has executed — not a reviewer instructed to check it, which is the
same assertion that already failed, and not a lint on summary wording, which
would ratchet the prose while leaving the join undone.

docs/design-ledgers.md re-projected from the amended rows.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016CGc3k4QXMEdRqtPsSfmTv

---------

Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

0 participants