Repository navigation
The emission ratchet gates nothing: design its enrolment as an OBSERVATION with an executing consumer and a discriminating red — do not land it as a merge-blocking baseline - #9345
Closed
briansrls wants to merge 8 commits into
Conversation
… consumer, and a discriminating red The emit-subject clean ratchet gates nothing. Measured on origin/main at 730d226 and re-confirmed at e1f65b3: `git grep -l emit_subject_clean` returns exactly three files -- the frontier module, the runner tool, and their one witness -- and the path-fragment search returns the same three, which closes the argv-assembled-entry-path case a module-name grep would miss. No workflow, no required phase, no module names either of them. This is not a defect in the ratchet. The enrolment wall was a genuine construction: it refused every enrolment while the universe carried a single denominator. What changed is that #9231 made the permitting arm producible, and the wall then answered PERMITTED about a carrier that must still not gate -- it asked one question from one fact, and that fact is no longer the only disqualifier. ENROLMENT IS TWO QUESTIONS, SO THE MODE IS A PARAMETER. `EmitRatchetGatingAdmission` is deleted at the root and replaced by `emit_ratchet_enrolment_admission(enrolment, r)` over `EnrolledAsObservation | EnrolledAsGate`. Preconditions are derived from the fold, never asserted about it: BOTH a non-empty universe -- a fold over no subjects is a discovery failure, and rendering one as an observation of nothing is the empty-observation narrow at the point where the observation is taken. GATE ONLY the dual denominator, for the reason the previous wall gave verbatim. GATE ONLY every roster subject EVALUATED. A subject that reached NOT-EVALUATED or was never measured has no verdict about its cleanliness, and a gate whose universe contains such subjects decides a closed-universe question over an open one. This is hole 3 arriving at the enrolment seam. The asymmetry is deliberate rather than lenient: an observation is NOT refused by a single denominator or by unevaluated subjects, because those are its CONTENT. Refusing to look because the looking is imperfect is the same narrow one level up. What a weak universe disqualifies is DECIDING. EXECUTION PROVENANCE IS STRUCTURAL, NOT CHECKED. `EmitRatchetObservation = ObservationTaken { roster, standing } | ObservationNotTaken { cause }`. The not-taken arm holds NO standing field, so there is no spelling in which a fold that never happened reads as a fold that found nothing wrong. The report reaches the standing only THROUGH the observation and prints the gate admission beside it, so a reading cannot be quoted as a gate verdict. On the host side `attempt_emit_subject_clean_ratchet` separates never-attempted (roster unreadable, source root unlistable) from folded, before the difference stops being knowable. The new `observe` verb exits SUCCESS on a refusing standing -- the observation succeeded and the news is bad, which belongs in the report a human reads -- and FAILURE only when the observation could not be taken. `check` now routes through the gate admission and refuses to be a gate. THE THIRD STATE: HAS NOT RUN YET vs WILL NEVER RUN HERE. Both render as an absent report and only the second is terminal. The vocabulary is BORROWED rather than minted: `std.witness_admission` already separates a row with an executing consumer from one nothing claims from one whose cadence has no scheduled route. `emit_ratchet_runner_cadence = NoConsumer` derives `UnexecutedDeferredWitness`, and the derivation is not constant -- handed a cadence with a route it returns the covered arm. NOTHING ENROLS. No workflow, no required phase, no CI authority is touched, and no import reaches the runner from anything the floor folds. Enrolment is a floor-cut re-add and requires its own operator agreement; this gets the mechanism to where that is a one-line change someone with the authority can approve. EVIDENCE, BY EXECUTION on BuildBuddy (arm64 session, amd64 runner, build and run in one dispatch): control 10/10 claims PASS; `gunbc compile --entry dag/tools/emit_subject_clean_ratchet.dag` -> 0 blocking, 949 advisory, 152 files emitted. mutation 1 gate ignores unevaluated subjects (the pre-change wall restored): FAIL a_gate_refuses_a_dual_denominator_fold_whose_subjects_were_never_evaluated FAIL an_unevaluated_subject_is_observed_rather_than_suppressed four unrelated claims stay PASS -- targeted, not a broad break. mutation 2 empty universe no longer refuses enrolment: FAIL an_observation_that_was_not_taken_holds_no_standing FAIL the_report_distinguishes_an_untaken_observation_from_a_clean_one restored control green before and after. Every claim pairs its refusing input with a control differing in exactly one field, and `the_ratchet_runner_has_no_executing_consumer_today` is green BECAUSE nothing runs the runner -- it goes red the day a cadence is agreed, which is what forces it and the block it mirrors to be rewritten together. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ce that could not fail
Two review findings, both fixed at the root rather than in the row that surfaced them.
THE NOT-TAKEN ARM HELD A RENDERING WHERE IT SHOULD HAVE HELD THE FACT.
`ObservationNotTaken { cause: String }` flattened the typed refusal into prose at the moment it was
stored -- the anemic leaf DESIGN §2 names, a String hiding parts that already existed one function
away. The cost landed exactly where it hurts most: every claim about WHY an observation was not
taken had to be a substring match, so the one artifact a reader would cite as proof of this
carrier's strongest property was a change detector -- red on a wording edit, green on any text
carrying the phrase. It now carries `admission: EmitRatchetEnrolmentAdmission`, and the rendering
becomes a projection derived at the edge, never the record.
AND THE ROW THAT COULD NOT FAIL IS DELETED, NOT REPAIRED.
`an_observation_that_was_not_taken_holds_no_standing` had four conjuncts: one structural, three
substring matches. Worse, the property its NAME asserted is unauthorable at BOTH §4b boundaries --
no fixture can construct a variant field that does not exist -- which is precisely the case where
the right answer is no check at all, because a permanently-green check is worse than absent for
being cited as coverage. It is replaced by `an_empty_dual_fold_yields_no_observation`, which asserts
only what can fail for the right reason: which ARM an unobservable fold dispatches to, and which
REFUSAL it carries, both as variant matches. The structural property survives in the type and is
stated in the module header, where the header also records that no witness asserts it and why.
The report row IS legitimately a renderer claim, so it stays -- but its expected rows are now
COMPOSED from the renderer instead of hand-written. A literal fragment there pins one authority's
wording into another's claim, which is §3's fork arriving as a test fixture.
THE QUADRATIC FOLD IS FIXED, AND NOT AS A NIT.
`ratchet_unevaluated_subjects` accumulated with `concat(acc, [e])` per hit. DESIGN §6's standing
bare-minimum-cost ruling is explicit that a copied accumulator or a quadratic fold is ALWAYS fixed
regardless of the realized n, because "n is small here" is not a time-stable fact -- and this
roster is the whole discovered corpus, so the mitigating premise was weak on its own terms. It is
now a total `emit_ratchet_verdict_evaluated` predicate plus filter-then-map, which also states the
question the whole not-evaluated wall turns on ONCE instead of inlining it in a selection loop.
This module's peer accumulators predate the change and are untouched; pricing this cut against
pre-existing corpus defects would be the wrong denominator.
EVIDENCE, BY EXECUTION (BuildBuddy, build and run in one dispatch), controls green either side:
filter rewrite control 8/8 PASS. Mutating the EXTRACTED predicate (NotEvaluated reads as
evaluated) reds exactly the two gate claims -- so the wall moved with the code
rather than out from under it, which is the specific risk in extracting it.
typed admission control 8/8 PASS.
mutation A, empty universe permits so the fold routes to TAKEN
-> FAIL an_empty_dual_fold_yields_no_observation
mutation B, the not-taken arm carries the WRONG refusal identity
-> FAIL an_empty_dual_fold_yields_no_observation
Both conjuncts load-bearing; six unrelated claims PASS throughout.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… citation to a symbol this branch deletes
REVIEW 56173, FINDING 1 -- FIXED. `ratchet_roster_is_empty` is gone; `emit_ratchet_enrolment_admission`
matches `r.roster` directly, as the wall it replaced did. The reviewer's instinct is right even though
the citation is not: `grep -c` for the named predicate-dissolution rule in DESIGN.md returns 0. The
real precedent is in the corpus -- `std.witness_admission` `witness_admission_predicate_dissolution_note`
records two predicates dissolved (review 39760) BY MAKING CONSUMERS MATCH THE COPRODUCT, and
`v2.std.witness_execution_routing` records three more. Same direction, so the change stands on its
merits rather than on the rule as cited.
REVIEW 56173, FINDING 2 -- DECLINED, three reasons, the third deciding.
1. `filter` takes a Bool by construction, so dissolving `emit_ratchet_verdict_evaluated` means
returning to a fold that appends -- the quadratic accumulator review 56160 and DESIGN §6's
bare-minimum-cost ruling had just removed. The two findings would cancel.
2. `emit_ratchet_verdict_holds` sits ten lines above it: same coproduct, same `-> Bool`, same total
match, pre-existing and untouched here. That IS the module's idiom.
3. It is not a second accessor for one answer, which is what the duplicated-shape objection needs.
`RatchetRegressed` discriminates them: holds=false, evaluated=TRUE. A regression is a verdict the
fold ESTABLISHED and then refused. Collapsing the two would make an evaluated failure
indistinguishable from a subject nobody could measure -- the distinction this carrier exists for.
A STALE CITATION TO A SYMBOL THIS BRANCH DELETES, found via gentle-bee-495 rather than by review.
The `RosterDenominators` note cited `emit_ratchet_gating_admission` -- deleted by this very PR -- and
it would have shipped, in the module that argues for cited-symbol hygiene. Repaired, and widened,
because the sentence carried a second defect of the same family: it ended "when the file inventory
lands, the field changes and enrolment becomes possible", true of the wall as it stood and falsified
the moment gunbc#9231 landed. A dual denominator now makes a gate ELIGIBLE, not admissible, and an
observation does not consult the field at all. A stale citation wrapped around a stale claim.
THE GATE'S PERMIT IS UNOCCUPIED ON THE LIVE CORPUS, AND THAT IS NOT UNREACHABLE (gentle-bee-495,
2026-08-26). Hole 3's bounded-tail reader means a talkative subject arrives NOT-EVALUATED, so over a
realistic roster the any-unevaluated condition refuses essentially always and nothing RECEIVES the
permit. Recorded as occupancy rather than reachability, because only the second reading licenses
deleting the arm: DESIGN puts that test at the FIXTURE boundary, and the witness authors the permit
today as the one-field control beside the unevaluated refusal. Yes / yes / zero is a healthy guard
being quiet. The arm is NOT relaxed to tolerate unevaluated subjects -- that converts the
instrument's blindness into a green, the absorbing fallback arriving as a kindness to a roster that
is not ready. The relayed sample is carried as a SHAPE and not a rate; no proportion is stated.
EVIDENCE, controls green either side, every arm printing an explicit VOID fallback:
control after dissolution 8/8 PASS
C: gate permits without consulting FAIL ×3, including the substring-free `_permits_none`
denominator or verdicts PASS an_empty_dual_fold (a different question, correctly green)
E: empty-roster arm permits FAIL an_empty_dual_fold_yields_no_observation
restored PASS
Two earlier attempts at C were VOID rather than passing: forcing the arm by inventing a variant name
does not compile, and zero verdict lines greps identically to zero failures.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… one-arm version smart-ram-730 re-derived the holds/evaluated disagreement against this branch and found TWO arms disagreeing, not one. Re-measured here and confirmed: variant holds evaluated RatchetCleanHeld true true RatchetDebtHeld true true RatchetRegressed FALSE TRUE <-- disagree RatchetFrontierStale FALSE TRUE <-- disagree RatchetNotEvaluated false false RatchetSubjectUnmeasured false false WHY TWO IS STRONGER THAN ONE, and it is the reason this note changed rather than a citation being added to it: a single disagreeing variant is dismissible as an accident of how that one case is treated, which is exactly how the declined review finding would have read it. Two disagreeing in the SAME DIRECTION show the functions answer different questions by construction. AND THE READING IS THE PART THAT SURVIVES. Both disagreeing arms are cases where the fold DID establish a verdict and then refused it -- a regression is a subject measured and found dirty, a stale frontier row is a subject measured and found CLEAN while its admission row says otherwise. Neither is a subject nobody could measure. That is the entire content of the split, and collapsing the two questions would make an evaluated failure indistinguishable from an unevaluated subject: the state-space conflation this carrier exists to refuse, committed inside the machinery refusing it. Comment-only, and verified anyway rather than assumed -- this corpus refuses annotations in the wrong position, so "it is only a comment" is not evidence. PASS_COUNT=8 over the eight claims. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…, with the divergence class named
Review 56204 raised the predicate duplication a second time and rejected both my reasons. It is right,
and the part I got wrong is worth stating exactly: I argued the two predicates have DISTINCT SEMANTICS
and that `filter` needs a `Bool`. Both true, and neither answers the objection. Two total matches over
six variants are two places holding the coproduct's shape, and the compiler forcing both to be total
does not make them ONE AUTHORITY. Distinct semantics and duplicated shape knowledge can both be true
at once; my reply treated the first as refuting the second.
THE FIX GIVES BOTH QUESTIONS ONE SOURCE RATHER THAN DELETING A PREDICATE. `VerdictStanding` is the
real semantic axis and `emit_ratchet_verdict_standing` is now the only function reading the verdict
vocabulary's shape for classification:
VerdictHeld established, and the ratchet holds
VerdictEstablishedAndRefused established, and then REFUSED
VerdictUnestablished no verdict about this subject exists at all
`holds` and `evaluated` are projections over that, not over storage. Measured after the change --
variant mentions: standing 6, holds 0, evaluated 0. One place fails to compile when a variant lands.
(`emit_ratchet_verdict_entry` and `_row` still match six: they extract per-variant PAYLOADS, a field
and a rendering, which is not classification knowledge.)
AND IT IS A BETTER MODEL THAN EITHER POSITION IN THE ARGUMENT. The divergence between the two
questions used to be EMERGENT -- two independent matches that happened to disagree on two arms,
discoverable only by measuring them against each other, which is literally how it surfaced. Now it
is a named class. `VerdictEstablishedAndRefused` IS the population where the fold established a
verdict and then refused it: a regression is a subject measured and found dirty, a stale frontier row
is a subject measured and found CLEAN while its admission row disagrees.
TWO NEW CLAIMS PIN THE RELATION, and they fail for different reasons:
holding_a_verdict_entails_having_established_it -- the ratchet cannot hold over a subject nobody
measured; a failure means some arm reports a verdict it never established.
an_established_verdict_that_refuses_is_what_separates_the_two_questions -- the converse set is
NON-EMPTY (2). If it were empty the split would be a decoration and `evaluated` deletable.
EVIDENCE: control 10/10 PASS. Mutating the classifier to call a regression UNESTABLISHED reds exactly
the divergence claim and nothing else -- the entailment claim correctly stays green, since collapsing
that class creates no holds-without-evaluated case. Restored 10/10.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
# Conflicts: # dag/gunbc/emit_subject_clean_frontier.dag # dag/test/claim/emit_subject_clean_frontier_witness_test.dag
…flict sides The #9238 absorption left two files unparseable. Both sides' content survived intact; what did not was MY closing braces, and the cause is worth recording because the resolution looked correct by every check I ran. WHAT HAPPENED. Both conflicts were append/append at the file tails. I resolved by concatenating the two sides. But git had factored the SHARED TRAILING BRACE out of both sides as common context -- both blocks ended identically, so the closing `}` appeared ONCE, after the conflict region. Concatenating two bodies then left one brace closing two functions: emit_subject_clean_frontier.dag emit_ratchet_runner_execution_standing lost its `else` and function close; emit_outcome_under_membership was lexically swallowed by the still-open else ..._witness_test.dag an_established_verdict_that_refuses... lost its close; fn membership_with_candidates was swallowed the same way WHAT ALMOST LET IT THROUGH, which is the reusable part. I verified the merge by checking that both sides' SYMBOLS AND CLAIMS WERE PRESENT. All of them were. PRESENCE IS NOT WELL-FORMEDNESS -- every grep reported a clean merge while neither file parsed. WHAT CAUGHT IT was PASS_COUNT=0 on both lanes with no FAIL and no ERROR: the neither-verdict signal. A parse refusal is not a verdict, so a filter written for PASS/FAIL is blind to it, and zero verdict lines greps identically to zero failures. Raw output said it plainly: `module index refused: 2 unparseable .dag source(s)`. Review 56291 independently found the frontier half and prescribed the same fix; it named only that file, so applying the review alone would have left the witness test unparseable -- and the witness file is where the evidence lives, so the module would have compiled with its claims silently absent. VERIFIED BY EXECUTION, both lanes, because a merge can break either side: MINE 10/10 PASS THEIRS 3/3 PASS (gentle-bee-495's boundary claims -- the ones a careless merge destroys) runner tool compile 0 blocking, 154 files emitted frontier module 0 blocking, 148 files emitted The branch now also carries #9273 (d31fa86), so these claims pass against a tree where a truncated capture has its own refusal rather than being read as a compiler scoping failure. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…the instrument failed on
A roster subject arriving at the fold with no reading was RatchetSubjectUnmeasured whether the
run had asked about it or not. The two facts share nothing but their silence and have opposite
remedies -- fix the instrument, or widen the run -- so a reader handed one UNMEASURED count
could not tell which they were looking at.
This module already draws exactly this distinction correctly one axis over: an admission row
naming a subject the roster lacks is reported as an ORPHAN rather than as a missing measurement,
in its own words "because the two have opposite owners". The selection axis is the same shape and
did not get the same treatment.
WHAT LANDS
SubjectSelection = SelectionWholeRoster | SelectionSubset { entries }
A coproduct rather than a bare List<String>, deliberately: an empty list would mean both "a subset
naming nothing" and "no subsetting at all", which is the state-space conflation the type exists to
remove, reintroduced in the type that removes it.
RatchetSubjectNotSelected joins the verdict vocabulary and is threaded through the four total
matches over it. Both silences remain VerdictUnestablished, so a gate still refuses over either --
this splits OWNERS without promoting scope into evidence. The runner derives one selection and
reads it twice (the measured list and the classified selection come from the same value), because
two independent derivations could disagree and the disagreement would render as an UNMEASURED
subject the run had in fact measured.
EVIDENCE, and the reds are the point
The pair is a ONE-FIELD control: identical roster, admissions and readings, only the selection
differs. Mutated on BuildBuddy in both directions:
A, selection ignored (the pre-change behavior): a_subject_the_run_never_selected... FAILS alone
B, selection inverted: the two selected-side claims FAIL, that one passes
restored: all four pass
So claim A is the regression control for precisely the defect repaired here.
Stated rather than counted: neither_silence_establishes_a_verdict passes in every arm. It guards a
different property -- that neither silence is promoted to evidence -- and is NOT discriminating on
the selection axis.
a_partial_run_refuses_and_names_the_subjects_it_did_not_measure pinned the old UNMEASURED row text
and is updated with it; it stays red under both mutations.
Measured: 4 new/changed claims pass, the 12 pre-existing pass unchanged, and the runner compiles
0 blocking / 951 advisory.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
|
Closing as a duplicate: #9345 and #9346 are the same branch (session/loyal-lark-254-selection) at the same head, auto-created here while I was opening #9346 by hand. Keeping #9346 because its BASE is correct. This branch is stacked on #9315, so against main the diff carries #9315's commits too and a reviewer is shown the wrong subject; #9346 is based on session/loyal-lark-254 and shows only the 142-line change it makes. Two PRs on one branch also split review -- a finding on one is invisible to the other, and this change's whole content is a discriminating red I would rather have read once, in the right place. Work continues on #9346. -- sent from loyal-lark-254 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Auto-opened by session-dashboard for session
loyal-lark-254.Pushing to
session/loyal-lark-254-selectionadvances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan