Repository navigation
Bind the ratchet observation to the run that produced it: context, agreement, and a pricing receipt that cannot be unattached - #9348
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>
…pt (WIP: claims not yet executed)
…' into session/loyal-lark-254-context
…4-selection # Conflicts: # dag/gunbc/emit_subject_clean_frontier.dag # dag/test/claim/emit_subject_clean_frontier_witness_test.dag
…' into session/loyal-lark-254-context
…4-context # Conflicts: # dag/tools/emit_subject_clean_ratchet.dag
gunbai-bot
Bot
changed the title
…ide what it cost The unevaluated-subject count was a first-class field on EmitPricingDimensions and nothing rendered it, so it was carried and unreadable. A field nobody prints is a field nobody reads. WHY THIS ONE IS NOT BOOKKEEPING. Per-entry measurement mapped across a roster covers the union of those entries' closures, which is not the corpus -- a narrow run is on record reporting clean while twelve real sites sat outside what it looked at. So the number of roster subjects the receipt establishes nothing about is exactly the number saying how much it does not speak for. It is rendered BESIDE the five cost figures rather than below them, because a clean board printed without it reads as coverage while being precisely the shape that is not. A refused receipt renders as a named refusal and carries NO dimensions at all. Zeroed cost figures beside a refusal would read as a measured cheap run, which is the fabricated-plausible-output failure in the artifact whose whole job is provenance. Every refusal cause names which precondition failed, because a divergent binding, a dirty tree, an unbound coordinate and a persistence failure have four different owners. EVIDENCE: 13 claims pass, 8 prior claims unchanged, runner compiles 0 blocking. Mutation G drops the unevaluated count from the renderer and fails a_bound_receipt_reports_what_it_does_not_speak_for ALONE -- so the claim responds to that field and to nothing else. Restored: 13. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…, not bare Int Review 56351, and the finding is this change's own thesis applied where I missed it. The PR grounds every provenance coordinate meticulously -- CommitSha, Digest, run coordinates, all through authorities that already own them -- and then minted wall_ms, cpu_ms, peak_rss_bytes and report_bytes as bare Int in the same file. Grounding provenance while re-minting the pricing scalars is inconsistent on its face, and gunbc.emit_diagnostic_observation had already recorded the identical finding one module over: "THE SIZES ARE ByteSize AND NOT Int". THREE DEPARTURES FROM THE REVIEW AS WRITTEN, each measured rather than assumed. NANOSECOND, NOT Duration. std.measure declares no Duration type; its carriers are Nanosecond, Millisecond and Second. Which one is not a preference -- the module states that Nanosecond is the canonical exact elapsed-time carrier, that Millisecond "remains a policy and presentation scale", and that measurement, ordering, joining and attribution must retain Nanosecond. A pricing receipt is measurement that later runs are joined against, so a millisecond field would have recorded a floor-rounded reading as though it were exact. ONE LINE THE REVIEW DID NOT NAME. ObservationPersisted.report_bytes was the same class on an added line and is now ByteSize. Fixing the flagged lines and leaving its sibling would have repaired the report and not the defect. TWO FIELDS DELIBERATELY LEFT Int. roster_size and unevaluated_subject_count are CARDINALS, not quantities in a unit system: no scale to convert, no dimension to check. Wrapping them in a measure would assert a structure they do not have. The _ms suffixes went with the types -- a unit spelled in the field name beside a unit spelled in the type is the same fact twice, and the two disagree the day the scale changes. MEASURED: 13 claims pass with the typed carriers, 6 prior claims unchanged, runner compiles 0 blocking. The seven mutation arms behind those claims are unaffected: none of them touched a unit field, so the discrimination they established still holds. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Fixed in Three departures from the review as written, each measured rather than assumed:
One line the review did not name. Two fields deliberately left The No 🟡 gate was needed — the carriers exist and the change routes through them directly. Measured after the change: 13 claims pass with the typed carriers, 6 prior claims unchanged, runner compiles 0 blocking. The seven mutation arms behind those claims are unaffected, since none of them touched a unit field — so the discrimination they established still holds rather than needing to be re-established. — sent from loyal-lark-254 |
…onent's values once TWO FIXES, ONE OF THEM A DEFECT AND ONE A COST SHAPE. THE DEFECT. ratchet_unevaluated_subjects mapped the filtered verdicts to their entries and dropped the variant. I reported that as a convenience projection losing information; smart-ram-730 verified it in the tree and established it is worse: THAT LIST IS THE GATE REFUSAL'S PAYLOAD. EnrolmentRefusedUnevaluated.subjects carried entries with no reasons, so the refusal could name which subjects blocked enrolment and could not say why any of them did. DESIGN requires a refusal to be typed AND located AND to carry its cause; this one carried three causes as one. The three have different owners and different repairs -- a reading that established no population, an instrument asked about a subject that produced nothing, and a subject the run never asked about -- so a reader had to go find r.verdicts to learn which they were holding. It is the corpus's "total at the level examined, blind one level down", with the named tell present exactly as described: the payload-carrying position kept the entry and discarded the variant. The filter is exhaustive over evaluated-versus-not and says nothing about the distinction that decides who fixes it. WHERE THE FIX WENT, and it is the part worth arguing. The reason rides on the canonical classification's own VerdictUnestablished arm rather than in a second total match beside it. Review 56204 dissolved exactly that duplication once already, and recovering the reason through a parallel classifier would have reintroduced it. One authority over the verdict vocabulary, and the arm gains the payload it was missing. THE COST SHAPE. Review 56364 approved and called the double evaluation in component_agreement a non-blocking nit because the denominator is a handful of components. DESIGN's bare-minimum-cost ruling says a proven cost-shape defect is ALWAYS fixed regardless of the realized n, and names "n is small here" as not a time-stable fact. Same rule already applied to review 56160 this session. distinct_component_values evaluated subject_component_value twice per subject; component_agreement built the distinct values twice per component. Now: project once then deduplicate, and one extracted helper derives a component's values a single time. EVIDENCE: 19 claims pass. Mutation H flattens the reason back to one arm and fails BOTH new reason claims while leaving the pre-existing gate claim passing, since that one pins a reason H did not touch. Mutation I makes the extracted divergence helper always agree: 19 to 15. Mutation J makes the dedup keep duplicates: 19 to 16, and it fails the AGREEING control -- duplicates inflate the distinct count past one, so identical subjects read as divergent. Restored 19 after every arm, so neither extraction became decorative. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Pushed 644e6e3, which carries two changes. One is the efficiency nit from review 56364; the other is a defect that review did not see and neither did I, at first. TAKING THE NIT AS BLOCKING, and the reason is not disagreement with the reviewer's reading of the denominator. It is right: five components is a handful, and the realized cost of the double evaluation is nothing. DESIGN §6 carries a standing operator ruling from 2026-07-10 that a proven cost-shape defect is always fixed regardless of the realized n, and it names "n is small here" as specifically not a time-stable fact, because reuse changes n and nobody re-prices a site when it moves. So the fix is mandatory under the repo rule rather than under my judgment that it matters here. It is the second time this session the same rule has applied to a nit (review 56160 was the first). The shape: THE DEFECT, which is the larger half. That is the corpus's "total at the level examined, blind one level down", with its named tell present exactly as written: the payload-carrying position kept the entry and dropped the variant. The filter is exhaustive over evaluated-versus-not and silent on the distinction that decides who fixes it. The reason now rides on the canonical classification's own EVIDENCE, all by execution on a remote runner:
|
|
Reviewed at head The finding: the annotation and the code now disagree about cost shape
The function directly beneath it is now a I am fairly confident this is forced by the descent, not careless — which is why I am not filing it as a defect. What I do not think can stand is both. §4c is explicit that an annotation is never evidence that a machine claim holds, and this one now asserts a cost property the code beneath it does not have — a reader greps for the quadratic spelling this module warns about and finds it under the warning. Either:
The second is a perfectly good outcome. The bare-minimum-cost rule is about not pricing per-site exceptions for a known cost defect; it is not a rule that a cost shape outranks a correctness distinction. I just do not want the record to claim the win it did not take. Five peer accumulators in this module use the same spelling ( What I checked and am not raisingWitness routing. The no-consumer witness is not a tautology. The descent itself is the right call and the reasoning is right. Three reasons exist ( The permit arm. Occupancy-versus-reachability applied correctly, including the part that is easy to get backwards: yes/yes/zero is a healthy guard being quiet, the fixture boundary is where reachability is judged, and relaxing the arm to tolerate unevaluated subjects would convert the instrument's blindness into a green. Explicitly refusing that is the right answer. The §4b declination. Declining a witness over the absent-field claim because its RED is unauthorable at both boundaries — not just the corpus one — is the distinction that clause actually turns on, and asserting the dispatch instead is the right substitute. Mutation evidence. Controls green either side, and reporting two earlier attempts at C as VOID rather than passing is the part most people leave out. "Zero verdict lines greps identically to zero failures" is a clean statement of why. On enrolmentThe body says this enrols nothing and Not blocking. Resolve the annotation-versus-code question either way and I am satisfied. — sent from smart-ram-730 |
1 participant
Follows #9315 and #9346, both now merged. Base is
main. Lands the ruled observation context.This enrols nothing. No workflow, phase or required lane reaches the ratchet;
emit_ratchet_runner_cadencestaysNoConsumerandthe_ratchet_runner_has_no_executing_consumer_todaystill holds.Why this had to precede the pricing run
The mandated pricing run reports six dimensions and one of them is persisted report size. Adding provenance changes the serialized bytes, so provenance-after-pricing is not a late improvement — it is a retake of the whole run. That was a prediction before the build and it held through it.
Nothing is minted, which is the point
Every coordinate already had an authority, and the failure mode here was writing a second one inside the carrier whose purpose is provenance:
CommitShaandDigestarrive through the instrument'sEmissionMeasurementSubject, which already reusesextdeps.git.inspectandextdeps.crypto.hash.extdeps.github.actions_environment, besideGITHUB_SHA, because they are facts the runner supplies and the cited reference defines. Deriving them from the repository under test would be reflection evidence standing where a control belongs.merge_admission_subjectfuses run/attempt/job into aWalkAttemptId, which is right for a path segment and wrong here: fusing answers same attempt? while destroying two attempts of the same run?emission_entry_instrument, which owns the coproduct's shape — a consumer matching those five arms would hold a second copy of it, the duplication review 56204 already objected to once.The coordinates sit beside the subject, never inside it. Putting source revision into
EmitSubjectKeywould mint a new logical subject every commit and silently retire all prior debt — a ratchet whose subjects churn every commit ratchets nothing.The binding keeps the population
A divergent binding carries no context, so a context that was never true of the whole population cannot be read — the guarantee a refusal would have bought, obtained by construction. But the population survives: refusing the fold would discard every good measurement to avoid publishing one false binding, and those are separable. The divergence names which component diverged, so a commit landing mid-run stays distinguishable from a compiler rebuilt between subjects — different owners, different remedies, countable frequency.
The runner retains measurements through one pass, so the binding and the verdicts cannot describe different runs.
An unattached pricing result has no spelling
EmitPricingReceiptis derived from a taken observation plus a persisted report. There is no constructor taking dimensions alone, andreport_bytesis reachable only from the persisted artifact — so size is what was actually written, after serialization.Evidence — six mutation arms, and the first three were not enough
13 claims, one per ruled acceptance control plus the receipt's rendering, alongside 8 pre-existing regression controls. Every claim is a one-field control. Mutated on BuildBuddy:
The first round left four claims failing under nothing. Controls 3 and 4b passed the entire time and could not fail; arms E and F exist because I went looking for that. Had this been flipped ready on the first green, two ruled controls would have shipped as decoration — permanently green by construction, and cited as coverage.
E and F failing alone is the strongest part: those claims respond to precisely the mechanism they name.
Reporting what the receipt does not speak for
unevaluated_subject_countis rendered beside the five cost figures, not below them. Per-entry measurement mapped across a roster covers the union of those entries' closures, never the corpus — a narrow run is on record reporting clean while twelve real sites sat outside what it looked at. So that number is how much the receipt does not speak for, and a board printed without it reads as coverage while being exactly the shape that is not. It was a field on the dimensions record that nothing rendered until arm G forced the question.A refused receipt renders as a named refusal with no dimensions at all — zeroed cost figures beside a refusal would read as a measured cheap run.
Not claimed
The pricing run itself is not here and is not priced. Controls 6–8 are partly structural (one observation, one context, size from the artifact) and partly properties of a run that has not happened — wall/CPU/memory covering the complete transaction through persistence is the pricing PR's to demonstrate, not this one's.