Skip to content

Give the v2.* argument-type class a home before its deletion PR closes: three probes, one expected-red row, one 4b row - #8902

Merged
briansrls merged 2 commits into
mainfrom
session/silent-badger-817-evidence
Aug 22, 2026
Merged

briansrls merged 2 commits into
mainfrom
session/silent-badger-817-evidence

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 22, 2026 •

Copy link
Copy Markdown
Contributor

Give the v2.* argument-type class a home before its deletion PR closes: three probes, one expected-red row, one 4b row

The lane that measured module_skips_direct_call_arg_check is closing without
deleting it -- the deletion (gunbc#8886) is blocked behind a resolve change that
was DECLINED at the layer that would own it. This lands the evidence so the
class stays countable, because closing that PR with its probes inside would make
the class INVISIBLE AGAIN, which is strictly worse than never having measured
it: the corpus would not know what we now know is there. That is how this
exemption survived years in the first place.

WHAT LANDS:

  1. THREE ENROLLED PROBES under a new direct-call-argument-type class in the
    guarantee probe corpus, and their asymmetry IS the class's shape:

    • a v2.-named module, Int formal, String actual, expecting a
      TypeMismatch refusal. THE DISCRIMINATING RED. It CANNOT pass while the
      exemption stands, and it PASSES measured on a tree with the arm deleted --
      so it is a satisfiable assertion held open by a named cause, not an
      aspiration and not a broken witness.
    • the BYTE-IDENTICAL source under an ordinary module name. Passes today, on
      main, with the exemption in place, because the exemption never covered it.
      This is the paired nonzero, and without it a red on the v2 row cannot be
      distinguished from a harness that reds on anything.
    • a CORRECT call in a v2.-named module. Passes today. Without it, a seam
      refusing every argument in a v2.* module would satisfy both reds.
  2. THE DISCRIMINATING RED ROSTERED in v2.workflow.floor_expected_red with its
    trigger named. DESIGN §4b(4) keeps a climb's evidence enrolled when the climb
    COMPLETES; the same reasoning holds when it is BLOCKED, and the roster is what
    makes a blocked class countable rather than forgotten. The day the exemption
    is deleted it flips to a permanent regression control and comes OFF the
    roster -- green while still rostered is a coherence failure, which the
    expected-red coherence witness catches.

  3. A §4b ROW recording the measured, blocked stop: rung below floor (unchanged --
    the judgment still does not run for any v2.* caller), ceiling R2, and the
    next trigger stated WITH its disposition -- "a formal parameter declared as an
    applied generic carries its applied form through resolution rather than
    reaching the comparison seam as the bare constructor: DECLINED 2026-08-22". A
    declined trigger is a legitimate §4b state; a blocked class with no row is not.

WHAT THE ROW RECORDS AND WHAT IT REFUSES TO RECORD. Deleting the arm produces
285+k blocking diagnostics, and 67+k with gunbc#8873 merged, for k >= 1
unmeasured -- ROSTER-RESOLVED counts, not corpus counts.
src/v2/extdeps/formatters/lean4_format.dag:184 is the proof: a live site,
structurally identical to eight that refused, contributing zero to BOTH arms and
therefore invisible to their difference. Zero genuine call-site defects were
found in the residue; every diagnostic examined was a deficit in the type
judgment, which is why no call sites were edited -- 67 mechanical edits would
have cemented three compiler deficits permanently. The per-mechanism split of
that residue is deliberately ABSENT: it was published as 48/11/8 and retracted
when the rule the 48 were attributed to was found to admit nothing in this
corpus.

THE COUNTEREXAMPLE THAT RETRACTED IT IS PRESERVED, because it will bite the next
person who reaches for a name-keyed alias relation: type Float = Float64 is
declared in BOTH dag/std/float.dag:18 and src/v2/std/float.dag:33, spelling the
target identically -- but dag/std/float.dag:16 has Float64 = Real64 while
src/v2/std/float.dag:30 has Float64 as a RECORD. Two declarations agreeing on a
SPELLING and disagreeing on a TYPE. Found by still-carp-717 before it shipped.

Co-Authored-By: Claude Opus 5 (1M context) noreply@anthropic.com
Claude-Session: https://claude.ai/code/session_01NcKYMt7nRBEYqnZv5rXkxb


THE PROBES WERE ENROLLED AND INERT, AND THE FLOOR CAUGHT IT

The first push of this PR rostered the discriminating red and CI refused with
ExpectedRedIdentityDidNotExecute. The roster was right; the HOME was wrong.
dag/test/claim/guarantee_probe_corpus_witness_test.dag declares ReadsLiveTree
-- correctly, it reads harness source off disk to compute a measurement revision
-- and a live home is DECLINED by the required floor's home policy before the
fold ever sees it. Measured, not inferred: on run 32570670086 a grep of the whole
run log names that module exactly TWICE, both times inside the refusal message.
Not one witness in that file executed.

So the three probes as first authored were enrolled and inert -- the
specification-without-execution state §5 names, wearing the costume of a
populated probe corpus. They are now MOVED (not copied) into
test.claim.direct_call_argument_type_witness_test, which declares
SubstrateInputsOnly and needs no live read, and the roster names the new
module. The registry rows in gunbc.guarantee_probe_corpus are untouched: which
module holds an assertion is a different fact from what the corpus registers.

This is the second time in this lane that an instrument reported nothing and
the nothing read as fine.
The floor's refusal is the reason it did not this
time -- ExpectedRedIdentityDidNotExecute exists precisely to make "the witness
you rostered never ran" loud, and it is the only mechanism in the sequence that
could tell an unexecuted probe from a passing one.

NOT CLAIMED, AND LARGER THAN THIS PR: the fix here covers three probes. The
rest of guarantee_probe_corpus_witness_test -- the enrolled executing evidence
for the bare-none, call-shape, method-surface, declared-conformance,
sole-constructor and v2-frontier guarantee classes -- still does not execute in
the required floor. Every §4b rung that cites those probes as its executing
evidence is therefore citing something CI does not run. That is a rung-honesty
question about the guarantee-recovery evidence base, not this class's to repair,
and it is reported rather than quietly swept in beside a class row.

ONE STATED MEASUREMENT GAP

The corroboration run against still-carp-717's current head (verify/with-8873-head,
pushed to settle their 19-vs-67 reading against mine) NEVER EXECUTED: witness CI
runs on PRs and main, and that branch has no PR, so it has no run. The 67 in this
PR is my own measurement from this lane's own required-ci; the corroboration is
absent, and I am not opening a throwaway PR to obtain it at lane close. Their
19 reading was separately shown not to hold -- the relation they thought my
mirror had lost is present in all four files of the tree I measured -- but that
is an argument, not the second measurement.

gunbc-ci-auto-heal and others added 2 commits August 22, 2026 11:34
…s: three probes, one expected-red row, one 4b row

The lane that measured `module_skips_direct_call_arg_check` is closing without
deleting it -- the deletion (gunbc#8886) is blocked behind a resolve change that
was DECLINED at the layer that would own it. This lands the evidence so the
class stays countable, because closing that PR with its probes inside would make
the class INVISIBLE AGAIN, which is strictly worse than never having measured
it: the corpus would not know what we now know is there. That is how this
exemption survived years in the first place.

WHAT LANDS:

1. THREE ENROLLED PROBES under a new `direct-call-argument-type` class in the
   guarantee probe corpus, and their asymmetry IS the class's shape:
   - a `v2.`-named module, `Int` formal, `String` actual, expecting a
     TypeMismatch refusal. THE DISCRIMINATING RED. It CANNOT pass while the
     exemption stands, and it PASSES measured on a tree with the arm deleted --
     so it is a satisfiable assertion held open by a named cause, not an
     aspiration and not a broken witness.
   - the BYTE-IDENTICAL source under an ordinary module name. Passes today, on
     main, with the exemption in place, because the exemption never covered it.
     This is the paired nonzero, and without it a red on the v2 row cannot be
     distinguished from a harness that reds on anything.
   - a CORRECT call in a `v2.`-named module. Passes today. Without it, a seam
     refusing every argument in a `v2.*` module would satisfy both reds.

2. THE DISCRIMINATING RED ROSTERED in `v2.workflow.floor_expected_red` with its
   trigger named. DESIGN §4b(4) keeps a climb's evidence enrolled when the climb
   COMPLETES; the same reasoning holds when it is BLOCKED, and the roster is what
   makes a blocked class countable rather than forgotten. The day the exemption
   is deleted it flips to a permanent regression control and comes OFF the
   roster -- green while still rostered is a coherence failure, which the
   expected-red coherence witness catches.

3. A §4b ROW recording the measured, blocked stop: rung below floor (unchanged --
   the judgment still does not run for any `v2.*` caller), ceiling R2, and the
   next trigger stated WITH its disposition -- "a formal parameter declared as an
   applied generic carries its applied form through resolution rather than
   reaching the comparison seam as the bare constructor: DECLINED 2026-08-22". A
   declined trigger is a legitimate §4b state; a blocked class with no row is not.

WHAT THE ROW RECORDS AND WHAT IT REFUSES TO RECORD. Deleting the arm produces
285+k blocking diagnostics, and 67+k with gunbc#8873 merged, for k >= 1
unmeasured -- ROSTER-RESOLVED counts, not corpus counts.
`src/v2/extdeps/formatters/lean4_format.dag:184` is the proof: a live site,
structurally identical to eight that refused, contributing zero to BOTH arms and
therefore invisible to their difference. Zero genuine call-site defects were
found in the residue; every diagnostic examined was a deficit in the type
judgment, which is why no call sites were edited -- 67 mechanical edits would
have cemented three compiler deficits permanently. The per-mechanism split of
that residue is deliberately ABSENT: it was published as 48/11/8 and retracted
when the rule the 48 were attributed to was found to admit nothing in this
corpus.

THE COUNTEREXAMPLE THAT RETRACTED IT IS PRESERVED, because it will bite the next
person who reaches for a name-keyed alias relation: `type Float = Float64` is
declared in BOTH dag/std/float.dag:18 and src/v2/std/float.dag:33, spelling the
target identically -- but dag/std/float.dag:16 has `Float64 = Real64` while
src/v2/std/float.dag:30 has `Float64` as a RECORD. Two declarations agreeing on a
SPELLING and disagreeing on a TYPE. Found by still-carp-717 before it shipped.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01NcKYMt7nRBEYqnZv5rXkxb
…ome, because their obvious home does not execute

CI on #8902 refused with ExpectedRedIdentityDidNotExecute for the rostered
identity. The cause is not the roster: dag/test/claim/guarantee_probe_corpus_witness_test.dag
declares ReadsLiveTree, and a live home is DECLINED by the required floor's
home policy before the fold sees it. Measured on run 32570670086 -- a grep of
the whole run log names that module exactly twice, both times inside the
refusal message. Not one witness in that file executed.

So the three probes were enrolled and inert: the specification-without-execution
state DESIGN 5 names, wearing the costume of a populated probe corpus. They are
MOVED (not copied) into test.claim.direct_call_argument_type_witness_test, which
declares SubstrateInputsOnly and needs no live read, so the rostered red actually
runs and the roster string now names the new module.

The registry rows in gunbc.guarantee_probe_corpus are untouched, and the three
probe ids stay in dag_native_v1_compile_probe_ids -- the corpus registry is a
different fact from which module holds the assertion.

NOT CLAIMED: this fixes only these three. That an entire enrolled guarantee
probe corpus does not execute in the required floor is a finding about the
guarantee-recovery evidence base, larger than this class, and is reported
rather than quietly repaired here.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01NcKYMt7nRBEYqnZv5rXkxb
@briansrls
briansrls merged commit 19f0be8 into main Aug 22, 2026
1 check passed
@briansrls
briansrls deleted the session/silent-badger-817-evidence branch August 22, 2026 16:30
gunbai-bot Bot pushed a commit that referenced this pull request Aug 22, 2026
One conflict, in the v2.* argument-type row of the guarantee-recovery gap
analysis. Both sides added a paragraph to the same table cell and the two
are complementary rather than competing:

  ours (#8870)  SEAM (2) gained a live production specimen --
                v2.std.materialize stores an Fnv1a64Structural payload
                into a field declared as the ContentHash union, proven by
                a PatternMatchFailure receipt against the module as it
                stands on main.

  main (#8902)  SEAM (1) was executed to a measured, blocked stop, with
                its next trigger DECLINED at the owning layer and its
                evidence enrolled so the class stays countable.

Kept both, in the order the row already reads: seam (2)'s specimen, then
the shared "the enumeration is unfinished" sentence that both sides carry
once, then seam (1)'s blocked-stop row, then the per-seam trigger list.
Neither paragraph is edited.

Merged rather than rebased, per the repo's merge policy: history is
flattened at squash-merge, so rebasing only buys a force-push.

Resolved at cell grain rather than by taking a side. First attempt spliced
whole cells and silently duplicated the 2122-character shared suffix --
both seam-(1) trigger lists, both ALIAS TRANSPARENCY paragraphs -- while
still producing a well-formed 7-cell row that read correctly at the join
it was inspected at. Caught by counting distinctive strings rather than by
reading the result. Rebuilt from the common prefix/suffix decomposition;
every distinctive string now appears exactly once and the table holds its
94 rows.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.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.

1 participant