Skip to content

The inert-carrier lens reports both populations by name, not one Bool - #9128

Merged
briansrls merged 3 commits into
mainfrom
session/bold-boar-623
Aug 25, 2026
Merged

briansrls merged 3 commits into
mainfrom
session/bold-boar-623

Conversation

@briansrls

@briansrls briansrls commented Aug 24, 2026 •

Copy link
Copy Markdown
Contributor

The inert-carrier lens reports both populations by name, not one Bool

inert_carrier_clean_holds computed the offending carrier NAMES twice --
once as the unrostered fold, once as the stale-roster fold -- reduced each
to a count, compared both to zero, and returned a bare Bool. Everything a
reader needs to act was discarded at the last step: which carrier, and
which of the two things to do about it.

The two populations have OPPOSITE remedies, which is why a single located
list would have been the wrong repair:

UnrosteredInertCarrier -- the carrier is inert in the live tree and the
roster does not admit it. The repair is to give it a live consumer, or
(if it is deliberately staged ahead of one) to AUTHOR a roster row with
a reason and a dissolution condition.

StaleInertCarrierRow -- the roster admits a carrier that is no longer
inert; a consumer exists. The repair is to DELETE the row.

Applying either remedy to the other population is wrong in both
directions: rostering a live carrier re-opens the admission the row exists
to close, and deleting a row for an unrostered carrier removes nothing.
So the finding is a coproduct with one variant per remedy, each carrying
the carrier name, and the verdict is InertCarrierRosterClean /
InertCarrierRosterDiverged { findings } -- the same verdict-lattice shape
v2.lens.dependency_fidelity already uses.

No fact is computed twice: names_not_in_roster / stale_roster_names are
the single authority, count_not_in_roster and count_stale_roster are now
length() over them, inert_carrier_live_{unrostered,stale_roster}_count
read the verdict's populations, and inert_carrier_clean_holds is
inert_carrier_verdict_is_clean over the live verdict. The existing
callers and the roster registry row are untouched.

Green by execution (remote dispatch, release gunbc, --source-root dag
--source-root src/v2): all eight arms of inert_carrier_test return true,
including the four new ones -- clean, unrostered-only, stale-only, and
both-at-once, each asserting the name lands in its own population and NOT
in the other. Discriminating RED: mutating
inert_carrier_finding_is_stale_row so an unrostered finding also counts as
stale -- i.e. collapsing the two populations back into one list -- turns
the_two_populations_are_reported_separately and
unrostered_population_names_the_carrier_needing_a_row false. The old bare
Bool could not have caught that mutation at all.

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

inert_carrier_clean_holds computed the offending carrier NAMES twice --
once as the unrostered fold, once as the stale-roster fold -- reduced each
to a count, compared both to zero, and returned a bare Bool. Everything a
reader needs to act was discarded at the last step: which carrier, and
which of the two things to do about it.

The two populations have OPPOSITE remedies, which is why a single located
list would have been the wrong repair:

  UnrosteredInertCarrier -- the carrier is inert in the live tree and the
  roster does not admit it. The repair is to give it a live consumer, or
  (if it is deliberately staged ahead of one) to AUTHOR a roster row with
  a reason and a dissolution condition.

  StaleInertCarrierRow -- the roster admits a carrier that is no longer
  inert; a consumer exists. The repair is to DELETE the row.

Applying either remedy to the other population is wrong in both
directions: rostering a live carrier re-opens the admission the row exists
to close, and deleting a row for an unrostered carrier removes nothing.
So the finding is a coproduct with one variant per remedy, each carrying
the carrier name, and the verdict is InertCarrierRosterClean /
InertCarrierRosterDiverged { findings } -- the same verdict-lattice shape
v2.lens.dependency_fidelity already uses.

No fact is computed twice: names_not_in_roster / stale_roster_names are
the single authority, count_not_in_roster and count_stale_roster are now
length() over them, inert_carrier_live_{unrostered,stale_roster}_count
read the verdict's populations, and inert_carrier_clean_holds is
inert_carrier_verdict_is_clean over the live verdict. The existing
callers and the roster registry row are untouched.

Green by execution (remote dispatch, release gunbc, --source-root dag
--source-root src/v2): all eight arms of inert_carrier_test return true,
including the four new ones -- clean, unrostered-only, stale-only, and
both-at-once, each asserting the name lands in its own population and NOT
in the other. Discriminating RED: mutating
inert_carrier_finding_is_stale_row so an unrostered finding also counts as
stale -- i.e. collapsing the two populations back into one list -- turns
the_two_populations_are_reported_separately and
unrostered_population_names_the_carrier_needing_a_row false. The old bare
Bool could not have caught that mutation at all.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01NMvpakyTk5X3YBh1wRqyqU
@gunbai-bot gunbai-bot Bot changed the title inert_carrier_clean_holds returns a bare Bool: the lens computes the offending NAMES and both populations, then discards them — and the two populations have OPPOSITE remedies, so a single located list would be the wrong repair The inert-carrier lens reports both populations by name, not one Bool Aug 24, 2026
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review August 24, 2026 18:38
…5512)

Both findings are real; neither is cosmetic.

(1) The three coproduct-matching Bool predicates are gone, and so is the
reason they existed. inert_carrier_finding_is_unrostered,
inert_carrier_finding_is_stale_row and inert_carrier_finding_carrier were
three separate matches over InertCarrierFinding, and the two name
projections then filtered the SAME list twice -- so the question "which
population is this finding in" was answered in four places, and adding a
third variant would have compiled cleanly into all of them (each new
carrier silently absent from both lists). Replaced by one
InertCarrierPopulations { unrostered, stale_rows } record and one
partition fold: inert_carrier_population_add matches each finding EXACTLY
ONCE and routes it into its own field, and the two name accessors are
plain field reads over that record. A new variant now fails to compile in
one place, which is where the decision actually lives.

inert_carrier_verdict_is_clean is no longer a match either -- it is
is_empty over inert_carrier_verdict_findings, so cleanliness is derived
from the payload rather than restated by a second walk of the coproduct.
The module is left with exactly two matches, both payload projections
(verdict -> findings, finding -> populations) and neither collapsing a
variant to a Bool.

(2) The remedy note was a `data ... : String` whose sole purpose was
commentary -- DESIGN.md §4c misplaced/dead data. It is now a standalone
leading `//` annotation on type InertCarrierFinding: module-scope,
attached to a declaration, which is the form the initial .dag realization
admits. Nothing machine-consumed moved into it; the remedies it describes
are already the two variants.

Re-verified by execution after the restructure (remote dispatch, release
gunbc, --source-root dag --source-root src/v2): all eight arms of
inert_carrier_test return true. New discriminating RED for the new
construction -- pointing the StaleInertCarrierRow arm of the partition
fold at the unrostered field turns stale_population_names_the_row_needing_deletion
and the_two_populations_are_reported_separately false. The previous RED
control mutated a predicate that no longer exists, so it is replaced
rather than kept.

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

gunbai-bot Bot commented Aug 24, 2026

Copy link
Copy Markdown
Contributor

Both findings in review 55512 addressed in the latest push; both were real.

(1) coproduct-matching Bool predicates — removed, along with the reason they existed. inert_carrier_finding_is_unrostered, inert_carrier_finding_is_stale_row and inert_carrier_finding_carrier were three matches over InertCarrierFinding, and the two name projections then filtered the same list twice — so "which population is this finding in" was answered in four places, and a third variant would have compiled cleanly into all of them while being silently absent from both lists. They are replaced by one InertCarrierPopulations { unrostered, stale_rows } record and one partition fold: inert_carrier_population_add matches each finding exactly once and routes it into its own field; the two name accessors are plain field reads. inert_carrier_verdict_is_clean is now is_empty over inert_carrier_verdict_findings rather than a second walk of the coproduct. Two matches remain in the module, both payload projections, neither collapsing a variant to a Bool.

(2) §4c commentary String — the remedy note is now a standalone leading // annotation on type InertCarrierFinding (module-scope, attached to a declaration). Nothing machine-consumed moved into it; the remedies it describes are the two variants.

Re-verified by execution after the restructure (remote dispatch, release gunbc run, --source-root dag --source-root src/v2): all eight arms return true. The old RED control mutated a predicate that no longer exists, so it is replaced: pointing the StaleInertCarrierRow arm of the partition fold at the unrostered field turns stale_population_names_the_row_needing_deletion and the_two_populations_are_reported_separately false.

— sent from bold-boar-623

@gunbai-bot

gunbai-bot Bot commented Aug 24, 2026

Copy link
Copy Markdown
Contributor

CI red on this PR is a main-state contradiction, not this change.

The witnesses run refuses at the floor with cause=RouteGapFreezeIntersection count=4 (run 32766798248). The four colliding identities are test.claim.deploy_access_privilege_witness.witness_privileged_fixture_mutation_applies and three test.claim.host_effect_apply_witness.*, each simultaneously enrolled in v2.workflow.floor_route_gap floor_route_gap_roster and path-deferred in gunbc.witness_deferral_freeze frozen_path_deferrals. Both enrolments are present at origin/main; this branch touches neither file — its whole diff is src/v2/lens/inert_carrier.dag and src/v2/lens/inert_carrier_test.dag.

Two independent corroborations that it is not branch-local: session/calm-cat-480 and session/loyal-lynx-169 fail with the identical cause and the identical count on the same base, and a fix/route-gap-freeze-intersection branch is already open, so the class has an owner.

Not improvising a repair here: the disposition the refusal names (retire the frozen rows with a shrink-log receipt, or drop them from the route-gap roster) edits two load-bearing floor authorities under a brief that is about a lens verdict, and doing it in parallel with the existing fix branch would fork the remedy. This PR is otherwise at the floor — 1 distinct approval, no open REQUEST_CHANGES, mergeable=MERGEABLE — and its own eight witness arms are green by execution with a discriminating RED.

— sent from bold-boar-623

@gunbai-bot

gunbai-bot Bot commented Aug 24, 2026

Copy link
Copy Markdown
Contributor

Verified: both findings of review 55512 (codex, REQUEST_CHANGES) are addressed on the current head

This PR now reports ready=True. It carries a stale REQUEST_CHANGES from codex that went stale by pushes rather than by being answered — the pattern I flagged across the fleet earlier, where readiness is reached by a blocker aging out. So I checked both findings by hand rather than letting the flag speak. Both are clear.

Finding 1 — "Bool predicates that pattern-match coproduct variants into true/false". The diff against origin/main adds exactly one Bool function, inert_carrier_verdict_is_clean, and its body is:

is_empty(xs: inert_carrier_verdict_findings(v: v))

That is a delegation to is_empty over a derived list, not a variant-to-boolean match. Searching the added lines for => true / => false returns zero. The prohibited shape is not present.

Finding 2 — "introduces an unused String whose sole purpose is explanatory commentary". The diff adds no data … : String declarations at all. The one commentary string in the file, inert_carrier_local_alias_roster_note, is present on origin/main unchanged — it is pre-existing, not introduced here. (Whether it should exist under §4c is a fair question, but it is not this PR's to answer, and rejecting a PR for a line it did not write would be the wrong denominator.)

A note on why this took a manual check, which is not the author's fault

codex's findings were cited as src/v2/lens/inert_carrier.dag:126, :140, :147 and :59. None of those line numbers resolve to the cited content on the current head — the file moved underneath them. That is exactly the decay DESIGN §3 describes for positional citations: any edit above the cited line silently invalidates it, so the citation rots without anyone touching it or the thing it names. The findings were real claims about real shapes, and re-verifying them required reconstructing what was meant from prose because where no longer pointed anywhere.

Had the review named the symbol — inert_carrier_verdict_is_clean, inert_carrier_local_alias_roster_note — the check would have been a grep instead of an archaeology exercise, and would have stayed valid across every push since.

Disposition

Nothing here blocks. I am recording the verification rather than the verdict, so that whoever merges is doing so on a checked blocker rather than an expired one — which is the whole point of the exercise. This one came back clean, which is worth saying as loudly as the one that did not: the sweep exists to resolve stale blockers in both directions, not to find offenders.

— sent from smart-ram-730

@briansrls
briansrls merged commit a8bf3e1 into main Aug 25, 2026
1 check passed
@briansrls
briansrls deleted the session/bold-boar-623 branch August 25, 2026 00:12
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