Skip to content

Declare the v2.* direct-call compat-arm exemption: one of two arms, measured at diagnostic identity - #9923

Merged
gunbai-bot[bot] merged 2 commits into
mainfrom
session/bold-carp-449-argseam-drop
Sep 1, 2026
Merged

gunbai-bot[bot] merged 2 commits into
mainfrom
session/bold-carp-449-argseam-drop

Conversation

@gunbai-bot

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

Copy link
Copy Markdown
Contributor

v1.compiler.infer module_skips_direct_call_arg_check returns true for
every module whose declared name begins with v2., and until this row that
exemption was declared nowhere in-tree. gunbc.doc_graph_roots already names
it as the one in-tree violation of the no-escape-hatch clause — the compiler
being bootstrapped is authored under weaker checks than ordinary source — and
records that its deletion (gunbc#8924) is CLOSED and held on a resolve-layer
seam whose repair was DECLINED on 2026-08-22 with no owner and no schedule.
That is an untracked stall wearing a trigger's costume (DESIGN §4b(2)): with
no row, there is no trigger, and a drop is retired BY ITS TRIGGER AND BY
NOTHING ELSE.

WHAT THE EXEMPTION SUPPRESSES, MEASURED RATHER THAN ARGUED FROM THE PREDICATE
NAME. One fixture authored twice, byte-identical but for its module line and a
renaming of every declaration so nothing resolves across the pair, run through
a gunbc built from this tree. Three arms each, all receiving a kernel String:
a local type Wrapped = FreeMonoid<Char> parameter, a cross-module
v2.std.text.String parameter, and an Int control.

non-v2. local alias ADMITTED, no diagnostic
declaration path REFUSED, inhabitance
Int control REFUSED twice: type mismatch + inhabitance
v2.* local alias ADMITTED, no diagnostic
declaration path REFUSED, inhabitance (same identity)
Int control REFUSED once: inhabitance ONLY

Exactly one diagnostic identity disappears across the pair — the type mismatch row — and every other identity is preserved. So this exemption
suppresses arg_compat_diags and nothing else. A count join would have been
defeated by the concat at 04_infer:5792 alone; identity is what makes the
difference attributable to the exemption rather than merely coincident with it.

THE LOSS IS NARROWER THAN THE PREDICATE'S NAME, AND THE FIRST DRAFT OF THIS
ROW GOT IT WRONG. arg_compat_diags is computed under the gate at :5769;
direct_call_argument_inhabitance_diags is called immediately after with NO
gate at :5780; both feed one concat. The inhabitance judgment therefore runs
inside v2.* exactly as it runs everywhere else (found by vivid-deer-102,
verified here at the source). A reader who takes argument checking to be off
in v2.* will misattribute every surviving refusal and every surviving
admission.

CONSEQUENTLY THIS ROW CLAIMS NO SELF-HOST HARM AND NAMES NONE. The specimen
anyone reaches for first — src/v2/std/integer.dag calling v2.std.text
string_head, whose emitted Rust rustc refuses — is NOT hidden by this
exemption: the surviving inhabitance arm judges that shape, and the fixture
shows the compat arm would not have refused it either. That shape belongs to
the already-standing text_boundary_identity_wall row. Citing it here would
be an unbacked execution claim.

The population is restated off the 9-declarations-under-formatters bound the
hold was priced against: the predicate's population is every module whose
declared name begins with v2., which includes the self-host emission
closure. The claim is not that the blast radius now exceeds 9 — it is that the
SUBJECT CHANGED and the old bound no longer describes what is being bought.

DESIGN.md and docs/design-ledgers.md are regenerated projections of
gunbc.rung_drop, not hand-edited.

The instrument

The fixture is described in the row in full rather than committed: two modules, byte-identical but for the module line, every declaration renamed so nothing resolves across the pair, three arms each, one gunbc run resolve per module against a gunbc built from this tree. It is re-derivable from the row's own text; committing a scratch probe with no final consumer would be §6 experimental residue.

What this does not do

🤖 Generated with Claude Code

https://claude.ai/code/session_01Vo22gFeUgs7vAVuhsmWqKk

gunbc-ci-auto-heal and others added 2 commits September 1, 2026 11:10
…easured at diagnostic identity

`v1.compiler.infer` `module_skips_direct_call_arg_check` returns true for
every module whose declared name begins with `v2.`, and until this row that
exemption was declared nowhere in-tree. `gunbc.doc_graph_roots` already names
it as the one in-tree violation of the no-escape-hatch clause — the compiler
being bootstrapped is authored under weaker checks than ordinary source — and
records that its deletion (gunbc#8924) is CLOSED and held on a resolve-layer
seam whose repair was DECLINED on 2026-08-22 with no owner and no schedule.
That is an untracked stall wearing a trigger's costume (DESIGN §4b(2)): with
no row, there is no trigger, and a drop is retired BY ITS TRIGGER AND BY
NOTHING ELSE.

WHAT THE EXEMPTION SUPPRESSES, MEASURED RATHER THAN ARGUED FROM THE PREDICATE
NAME. One fixture authored twice, byte-identical but for its module line and a
renaming of every declaration so nothing resolves across the pair, run through
a gunbc built from this tree. Three arms each, all receiving a kernel `String`:
a local `type Wrapped = FreeMonoid<Char>` parameter, a cross-module
`v2.std.text.String` parameter, and an `Int` control.

  non-`v2.`  local alias        ADMITTED, no diagnostic
             declaration path   REFUSED, inhabitance
             Int control        REFUSED twice: `type mismatch` + inhabitance
  `v2.*`     local alias        ADMITTED, no diagnostic
             declaration path   REFUSED, inhabitance (same identity)
             Int control        REFUSED once: inhabitance ONLY

Exactly one diagnostic identity disappears across the pair — the `type
mismatch` row — and every other identity is preserved. So this exemption
suppresses `arg_compat_diags` and nothing else. A count join would have been
defeated by the `concat` at 04_infer:5792 alone; identity is what makes the
difference attributable to the exemption rather than merely coincident with it.

THE LOSS IS NARROWER THAN THE PREDICATE'S NAME, AND THE FIRST DRAFT OF THIS
ROW GOT IT WRONG. `arg_compat_diags` is computed under the gate at :5769;
`direct_call_argument_inhabitance_diags` is called immediately after with NO
gate at :5780; both feed one `concat`. The inhabitance judgment therefore runs
inside `v2.*` exactly as it runs everywhere else (found by vivid-deer-102,
verified here at the source). A reader who takes argument checking to be off
in `v2.*` will misattribute every surviving refusal and every surviving
admission.

CONSEQUENTLY THIS ROW CLAIMS NO SELF-HOST HARM AND NAMES NONE. The specimen
anyone reaches for first — `src/v2/std/integer.dag` calling `v2.std.text`
`string_head`, whose emitted Rust rustc refuses — is NOT hidden by this
exemption: the surviving inhabitance arm judges that shape, and the fixture
shows the compat arm would not have refused it either. That shape belongs to
the already-standing `text_boundary_identity_wall` row. Citing it here would
be an unbacked execution claim.

The population is restated off the 9-declarations-under-formatters bound the
hold was priced against: the predicate's population is every module whose
declared name begins with `v2.`, which includes the self-host emission
closure. The claim is not that the blast radius now exceeds 9 — it is that the
SUBJECT CHANGED and the old bound no longer describes what is being bought.

DESIGN.md and docs/design-ledgers.md are regenerated projections of
`gunbc.rung_drop`, not hand-edited.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Vo22gFeUgs7vAVuhsmWqKk
…* (review 58154)

codex review 58154 found cross-path rung inflation in the row: PREVIOUS RUNG
claimed "mechanically preventable" for the compat arm INSIDE `v2.*` on the
strength of an OUTSIDE-`v2.*` fixture. The arm has never executed inside the
exemption, so no rung stood at the declared subject grain and none is now
claimed.

The row now says:

  - PREVIOUS RUNG at this row's own subject grain: NONE STOOD. The exemption
    predates the row; there is no rung it lowered.
  - What the fixture establishes is a DIFFERENT path — that the suppressed
    check operates OUTSIDE the exemption on the same tree and binary — which
    is what makes this a loss of an AVAILABLE guarantee rather than a check
    nobody has. The two paths are named separately and not averaged.
  - Because a class's rung is the MINIMUM across its in-scope paths, the
    temporary rung for this subject is UNGUARDED, not mitigatable. The
    mitigated emitted-Rust path is named only to bound where the loss is
    observable, never to raise the reported rung.
  - It is filed as a drop because the §4b(3) obligation — population, reason,
    and a trigger that can retire it — is exactly what an undeclared permanent
    exemption was escaping.

Same shape as `text_boundary_identity_wall`, which states "PREVIOUS RUNG,
STATED HONESTLY: none stood" for the same reason.

docs/design-ledgers.md is the regenerated projection of `gunbc.rung_drop`.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Vo22gFeUgs7vAVuhsmWqKk
@gunbai-bot
gunbai-bot Bot merged commit c137b62 into main Sep 1, 2026
6 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/bold-carp-449-argseam-drop branch September 1, 2026 12:10
@briansrls
briansrls restored the session/bold-carp-449-argseam-drop branch September 1, 2026 12:12
gunbai-bot Bot pushed a commit that referenced this pull request Sep 1, 2026
The generated-artifact merge driver refused DESIGN.md and docs/design-ledgers.md:
both sides changed them since the merge base, so neither side's bytes are the
projection of the merged authorities. Taking either side would have dropped the
other's authority-derived content with no conflict — the same silent deletion
that cost this branch a rung-drop row earlier today. Both are regenerated from
the merged authorities via the sanctioned actuator instead.

The .dag authorities merged clean. The three rows at risk were checked by
identity, not by eyeballing the diff: sealing_property_erases_structure and
merge_region_excludes_shared_tail in recurring_failure_mode, and
direct_call_arg_seam_v2_exemption in rung_drop — all present. That last row now
arrives from main via #9923, so this branch carries no rung-drop delta of its own.

Verified locally on the merged tree with a claim_executor rebuilt from it:
build lane regen first_generation_equal=true, generated-artifact 35/35 matched
0 drifted; witnesses lane 3 phases 0 failures, 4476 files parse-clean,
namespace-wave-admission ADMITTED.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9
@gunbai-bot
gunbai-bot Bot deleted the session/bold-carp-449-argseam-drop branch September 3, 2026 12:23
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