From ca2a9ea2412b4a5cd4e6e886c3add03310c3d1a5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 26 Aug 2026 06:27:37 +0000 Subject: [PATCH 1/7] Enrol the emission ratchet as an OBSERVATION: two modes, an executing consumer, and a discriminating red The emit-subject clean ratchet gates nothing. Measured on origin/main at 730d2269527 and re-confirmed at e1f65b3650: `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) --- dag/gunbc/emit_subject_clean_frontier.dag | 278 ++++++++++++++++-- ...it_subject_clean_frontier_witness_test.dag | 228 ++++++++++++-- dag/tools/emit_subject_clean_ratchet.dag | 183 +++++++++--- 3 files changed, 600 insertions(+), 89 deletions(-) diff --git a/dag/gunbc/emit_subject_clean_frontier.dag b/dag/gunbc/emit_subject_clean_frontier.dag index c774543bd6f..4a8035f7ce4 100644 --- a/dag/gunbc/emit_subject_clean_frontier.dag +++ b/dag/gunbc/emit_subject_clean_frontier.dag @@ -4,6 +4,14 @@ import std.types { Bool, Int, String, NonEmptyStr } import std.materialization_ladder { string_list_contains } import std.content_hash { Fnv1a64Structural, content_hash_atom } import std.dissolution { DissolutionCondition } +import std.witness_admission { + WitnessConsumerCadence, + NoConsumer, + WitnessExecutionStanding, + WitnessHasExecutingConsumer, + UnexecutedDeferredWitness, + witness_cadence_has_scheduled_route +} import std.roster_frontier { FrontierRow, frontier_row_path, @@ -1026,51 +1034,219 @@ fn emit_ratchet_standing_text(standing: EmitRatchetStanding) -> String { // function of rows the report also prints in full, so a reader can reconstruct it and no consumer // has to trust it. Nothing above admits or refuses on one. // --------------------------------------------------------------------------------------------- -// THE ENROLMENT WALL. -// -// Any consumer that would let a merge decision ride on this carrier routes through here first, and -// today it always refuses, because hole 2 is open: a universe discovered from the declaration index -// alone drops a file it cannot CLASSIFY instead of blocking it, so a gate reading it would report -// IMPROVEMENT when ingest regresses. That is fabricated plausible output with merge authority -// behind it. -// -// THIS IS A CONSTRUCTION, NOT A NOTE, AND THE DIFFERENCE IS THE POINT. The same rule written as -// prose is enforced only by the next author reading a paragraph and correctly believing it applies -// to them; written here it is a typed refusal naming the missing denominator. When the module -// inventory lands, the field changes, this permits, and there is no sentence anyone has to remember -// to delete. -// -// BOTH ARMS ARE REACHABLE TODAY — the permitting arm is authorable by handing the fold the dual -// denominator, which is why this is a wall rather than a decoration that could only ever refuse. -type EmitRatchetGatingAdmission - = GatingPermitted - | GatingRefusedDenominator { missing: String } - -fn emit_ratchet_gating_admission(r: EmitSubjectCleanRatchet) -> EmitRatchetGatingAdmission { +// THE ENROLMENT WALL, AND WHY ENROLMENT IS TWO QUESTIONS RATHER THAN ONE. +// +// The wall that stood here answered ONE question -- may a merge decision ride on this carrier -- +// and answered it from ONE fact, the denominators the universe was discovered under. That was the +// only fact it needed while hole 2 was open, because a single-denominator universe disqualifies +// every enrolment at once. Hole 2 closed, the permitting arm became producible, and the wall then +// permitted a carrier that must still not gate: the question it asks is now too narrow for the +// answer it gives. +// +// SO THE ENROLMENT MODE IS A PARAMETER, NOT AN ASSUMPTION. An OBSERVATION reports what it measured +// and decides nothing; a GATE stops a merge. They are different claims about the same fold, they +// have different preconditions, and collapsing them is what would let a first live run be adopted +// as a baseline. DESIGN §5 is explicit that a population measured from the tree being judged is not +// an oracle -- and the first live run of this ratchet over a corpus nobody has measured produces +// exactly such a population. Enrolled as an observation it is a reading; enrolled as a gate it is a +// snapshot with merge authority, and the refusal below is what keeps the second from being reachable +// by wiring alone. +// +// THE PRECONDITIONS, PER MODE, AND EACH ONE IS DERIVED FROM THE FOLD RATHER THAN ASSERTED ABOUT IT: +// +// BOTH -- the universe is non-empty. A fold over no subjects is a discovery failure, and a +// discovery failure rendered 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 and which is +// unchanged. +// +// GATE ONLY -- every roster subject was EVALUATED. A subject that reached NOT-EVALUATED or was +// never measured has no verdict about its cleanliness at all, and a gate whose universe contains +// such subjects is deciding a closed-universe question over an open one. This is hole 3 arriving +// at the enrolment seam: while the instrument cannot recover entry scope for a talkative subject, +// a realistic universe folds to a wall of not-evaluated rows, and the honest consequence is that +// the carrier may be READ and may not GATE. +// +// AND THE ASYMMETRY IS DELIBERATE RATHER THAN LENIENT. An observation is NOT refused by a single +// denominator or by unevaluated subjects, because those are the observation's CONTENT: refusing to +// look because the looking is imperfect is the same narrow the empty-universe arm refuses, committed +// one level up. What the observation may not do is be quoted as a gate, and that is not a property +// of the reading -- it is the question this admission answers. +// +// BOTH ARMS OF EVERY REFUSAL ARE AUTHORABLE, which is what makes this a wall rather than a +// decoration: the witness beside this module produces each refusing input and its one-field control. +// --------------------------------------------------------------------------------------------- +type EmitRatchetEnrolment + = EnrolledAsObservation + | EnrolledAsGate + +fn emit_ratchet_enrolment_text(enrolment: EmitRatchetEnrolment) -> String { + match enrolment { + EnrolledAsObservation => "observation" + EnrolledAsGate => "gate" + } +} + +type EmitRatchetEnrolmentAdmission + = EnrolmentPermitted { enrolment: EmitRatchetEnrolment } + | EnrolmentRefusedNoUniverse { enrolment: EmitRatchetEnrolment } + | EnrolmentRefusedDenominator { enrolment: EmitRatchetEnrolment, missing: String } + | EnrolmentRefusedUnevaluated { enrolment: EmitRatchetEnrolment, subjects: List } + +fn ratchet_roster_is_empty(r: EmitSubjectCleanRatchet) -> Bool { match r.roster { - RosterEmpty { policy: _, denominators: dn } => emit_ratchet_gating_admission_of(denominators: dn) - RosterIdentified { policy: _, denominators: dn, subject_count: _, digest: _ } => - emit_ratchet_gating_admission_of(denominators: dn) + RosterEmpty { policy: _, denominators: _ } => true + RosterIdentified { policy: _, denominators: _, subject_count: _, digest: _ } => false } } -fn emit_ratchet_gating_admission_of(denominators: RosterDenominators) -> EmitRatchetGatingAdmission { - match denominators { - DeclarationIndexAndModuleInventory => GatingPermitted +fn ratchet_denominators(r: EmitSubjectCleanRatchet) -> RosterDenominators { + match r.roster { + RosterEmpty { policy: _, denominators: dn } => dn + RosterIdentified { policy: _, denominators: dn, subject_count: _, digest: _ } => dn + } +} + +// THE UNEVALUATED SUBJECTS, BY NAME. A count would be the wrong shape for the same reason every +// other count in this module is display only: the refusal has to tell an operator WHICH subjects +// have no verdict, because that list is the work that closes the gap. +fn ratchet_unevaluated_subjects(r: EmitSubjectCleanRatchet) -> List { + fold( + r.verdicts, + init: [], + f: (acc, v) => + match v { + RatchetCleanHeld { entry: _ } => acc + RatchetDebtHeld { entry: _, cause: _ } => acc + RatchetRegressed { entry: _, cause: _ } => acc + RatchetFrontierStale { entry: _ } => acc + RatchetNotEvaluated { entry: e, on_frontier: _, cause: _ } => concat(acc, [e]) + RatchetSubjectUnmeasured { entry: e, on_frontier: _ } => concat(acc, [e]) + } + ) +} + +fn emit_ratchet_gate_admission(r: EmitSubjectCleanRatchet) -> EmitRatchetEnrolmentAdmission { + match ratchet_denominators(r: r) { DeclarationIndexOnly => - GatingRefusedDenominator { + EnrolmentRefusedDenominator { + enrolment: EnrolledAsGate, missing: "file inventory — a universe discovered from the declaration index alone loses a file the index cannot CLASSIFY (a fragment, a header preceded by non-comment text, an empty module name) instead of blocking it, so a gate over it reports improvement when such a file drops out of classification" } + DeclarationIndexAndModuleInventory => { + let unevaluated = ratchet_unevaluated_subjects(r: r) + if count(unevaluated) == 0 { + EnrolmentPermitted { enrolment: EnrolledAsGate } + } else { + EnrolmentRefusedUnevaluated { enrolment: EnrolledAsGate, subjects: unevaluated } + } + } + } +} + +fn emit_ratchet_enrolment_admission( + enrolment: EmitRatchetEnrolment, + r: EmitSubjectCleanRatchet +) -> EmitRatchetEnrolmentAdmission { + if ratchet_roster_is_empty(r: r) { + EnrolmentRefusedNoUniverse { enrolment: enrolment } + } else { + match enrolment { + EnrolledAsObservation => EnrolmentPermitted { enrolment: enrolment } + EnrolledAsGate => emit_ratchet_gate_admission(r: r) + } + } +} + +fn emit_ratchet_enrolment_admission_text(admission: EmitRatchetEnrolmentAdmission) -> String { + match admission { + EnrolmentPermitted { enrolment: e } => + concat("permitted as ", emit_ratchet_enrolment_text(enrolment: e)) + EnrolmentRefusedNoUniverse { enrolment: e } => + concat( + concat("refused as ", emit_ratchet_enrolment_text(enrolment: e)), + " — the fold discovered no subject, so there is nothing to report and nothing to decide" + ) + EnrolmentRefusedDenominator { enrolment: e, missing: m } => + concat( + concat(concat("refused as ", emit_ratchet_enrolment_text(enrolment: e)), " — missing "), + m + ) + EnrolmentRefusedUnevaluated { enrolment: e, subjects: ss } => + concat( + concat( + concat("refused as ", emit_ratchet_enrolment_text(enrolment: e)), + " — no verdict was established for: " + ), + join(ss, ", ") + ) } } +// --------------------------------------------------------------------------------------------- +// THE OBSERVATION, AND ITS EXECUTION PROVENANCE. +// +// A standing and a fold that could not be taken must not render alike, and the coproduct is what +// makes that structural rather than checked. DESIGN's execution-provenance-loss row states the test +// exactly: if a count of zero and an unreached stage produce the same output, the number is not an +// observation. `ObservationNotTaken` is therefore not a standing with no failing rows -- it holds no +// standing at all, so there is no spelling in which a fold that never happened reads as a fold that +// found nothing wrong. +// +// AND A REFUSING STANDING IS A TAKEN OBSERVATION. That is the whole distinction this carrier exists +// to hold: the observation succeeded and the news is bad. Its consumer reports it and does not stop +// the line on it; what stops the line is being unable to observe at all. +// --------------------------------------------------------------------------------------------- +type EmitRatchetObservation + = ObservationTaken { roster: RosterIdentity, standing: EmitRatchetStanding } + | ObservationNotTaken { cause: String } + +fn emit_ratchet_observation(r: EmitSubjectCleanRatchet) -> EmitRatchetObservation { + let admission = emit_ratchet_enrolment_admission(enrolment: EnrolledAsObservation, r: r) + match admission { + EnrolmentPermitted { enrolment: _ } => + ObservationTaken { roster: r.roster, standing: emit_ratchet_standing(r: r) } + EnrolmentRefusedNoUniverse { enrolment: _ } => + ObservationNotTaken { cause: emit_ratchet_enrolment_admission_text(admission: admission) } + EnrolmentRefusedDenominator { enrolment: _, missing: _ } => + ObservationNotTaken { cause: emit_ratchet_enrolment_admission_text(admission: admission) } + EnrolmentRefusedUnevaluated { enrolment: _, subjects: _ } => + ObservationNotTaken { cause: emit_ratchet_enrolment_admission_text(admission: admission) } + } +} + +fn emit_ratchet_observation_text(observation: EmitRatchetObservation) -> String { + match observation { + ObservationTaken { roster: _, standing: s } => + concat("taken — ", emit_ratchet_standing_text(standing: s)) + ObservationNotTaken { cause: c } => concat("NOT TAKEN — ", c) + } +} + +// THE REPORT CARRIES THE OBSERVATION, NEVER A BARE STANDING. A row reading `standing\theld over 0 +// subject(s)` and a row reading `standing\t...` written by a run that never folded anything are the +// same bytes, and DESIGN's execution-provenance test is exactly that: if a count of zero and an +// unreached stage produce the same output, the number is not an observation. So the standing is +// reachable on this report only THROUGH the observation, whose not-taken arm holds no standing to +// print. The gate admission is printed beside it because a reader of an observation report must be +// able to see, on the artifact itself, that it is not a gate verdict. fn emit_ratchet_report_rows(r: EmitSubjectCleanRatchet) -> List { concat( concat( roster_identity_rows(identity: r.roster), [ concat("admission_rows\t", to_string(r.admission_count)), - concat("standing\t", emit_ratchet_standing_text(standing: emit_ratchet_standing(r: r))) + concat( + "observation\t", + emit_ratchet_observation_text(observation: emit_ratchet_observation(r: r)) + ), + concat( + "enrolment_gate\t", + emit_ratchet_enrolment_admission_text( + admission: emit_ratchet_enrolment_admission(enrolment: EnrolledAsGate, r: r) + ) + ) ] ), concat( @@ -1100,3 +1276,47 @@ fn emit_ratchet_report_text(r: EmitSubjectCleanRatchet) -> String { // empty roster that greened would be the absorbing fallback; one that refuses is a debt roster with // nothing yet admitted to it. data emit_subject_clean_admissions: List = [] + +// --------------------------------------------------------------------------------------------- +// WHO RUNS THIS, TODAY: NOBODY, AND THAT IS A DECLARED FACT RATHER THAN A GAP SOMEONE HAS TO NOTICE. +// +// THE DISTINCTION THIS CLOSES is not "did the fold succeed" -- the observation above answers that -- +// but the one a reader of an absent report actually needs: HAS THE RATCHET NOT RUN YET, or WILL IT +// NEVER RUN HERE. They render identically as absence and only the second is terminal, so a consumer +// that reports both as "no report" strands whoever is waiting on the first. +// +// THE VOCABULARY IS BORROWED, NOT MINTED. `std.witness_admission` already separates a row with an +// executing consumer from a row nothing claims from a row whose named cadence has no scheduled +// route, and it already carries the mechanical per-cadence realization gate. Minting a second +// "does anything run this" vocabulary beside it would be the §3 nicknaming violation, in the exact +// place this carrier is arguing that a name without a mechanism is worthless. +// +// TODAY'S ANSWER IS `NoConsumer`, and it is measured rather than assumed: no workflow, no phase and +// no module in the tree names `tools.emit_subject_clean_ratchet` or this module. So the derived +// standing is UnexecutedDeferredWitness -- nothing claims the runner -- whose remedy the admission +// authority states as naming a cadence or deleting the witness. Neither is available from inside a +// PR: enrolment is a floor-cut re-add and DESIGN requires each of those to be re-derived under its +// own operator agreement, which is not a thing a diff can author. +// +// AND THIS FUNCTION IS NOT CONSTANT, which is what keeps the declaration from being a decoration: +// handed a cadence that HAS a scheduled route it returns the covered arm, and the witness beside +// this module asserts both directions. The day enrolment is agreed, the cadence row below changes, +// the claim naming today's answer goes RED, and it is that red -- not a paragraph -- that forces +// this block to be rewritten. +// --------------------------------------------------------------------------------------------- +data emit_ratchet_runner_entry: String = "dag/tools/emit_subject_clean_ratchet.dag" + +data emit_ratchet_runner_observe_function: String = "observe" + +data emit_ratchet_runner_cadence: WitnessConsumerCadence = NoConsumer + +fn emit_ratchet_runner_execution_standing(cadence: WitnessConsumerCadence) -> WitnessExecutionStanding { + if witness_cadence_has_scheduled_route(cadence: cadence) { + WitnessHasExecutingConsumer { cadence: cadence } + } else { + UnexecutedDeferredWitness { + entry: emit_ratchet_runner_entry, + function: emit_ratchet_runner_observe_function + } + } +} diff --git a/dag/test/claim/emit_subject_clean_frontier_witness_test.dag b/dag/test/claim/emit_subject_clean_frontier_witness_test.dag index bc82b72d4f4..e898d49e6d6 100644 --- a/dag/test/claim/emit_subject_clean_frontier_witness_test.dag +++ b/dag/test/claim/emit_subject_clean_frontier_witness_test.dag @@ -475,36 +475,178 @@ test fn an_upstream_mask_refuses_rather_than_reading_as_improvement() -> Bool { && fixture_standing_holds(roster: fixture_roster, admissions: [], readings: fixture_both_clean()) } -// THE ENROLMENT WALL, BOTH ARMS. The refusing arm is the live one: a single-denominator carrier -// cannot be gated on, and the refusal names the missing denominator rather than answering a bare -// false. The permitting arm is authored here to prove this is a WALL and not a decoration that -// could only ever refuse — if the permitting arm were unreachable, the refusal would carry no -// information and would be worse than absent for being counted as coverage. -test fn a_single_denominator_carrier_refuses_enrolment_and_names_what_is_missing() -> Bool { - match emit_ratchet_gating_admission_of(denominators: DeclarationIndexOnly) { - GatingPermitted => false - GatingRefusedDenominator { missing: m } => string_contains(s: m, pattern: "file inventory") +// --------------------------------------------------------------------------------------------- +// THE ENROLMENT WALL, PER MODE. +// +// The wall used to answer one question from one fact, and the witness beneath it proved both arms of +// that one fact reachable. That is no longer enough, and the reason is a change in the tree rather +// than a change of mind: while the denominator was the only disqualifier, permitting on it was +// permitting on everything. Hole 2 closed, dual-denominator folds became producible, and the same +// wall then said PERMITTED about a carrier whose subjects have no verdicts at all. +// +// So these claims are written against the fact that DISCRIMINATES the two modes, not against the +// mode label. Each pairs a refusing input with a control differing in exactly one field, so a green +// cannot be an accident of the fixture, and each names WHICH mode it refuses -- an observation that +// refuses for a gate's reasons would be the empty-observation narrow, and a gate that permits for an +// observation's reasons is the merge-blocking baseline this lane exists to prevent. +// --------------------------------------------------------------------------------------------- + +fn fixture_empty_dual_fold() -> EmitSubjectCleanRatchet { + fold_emit_subject_clean_ratchet_over_readings( + universe: DualUniverse { policy: fixture_policy(), entries: [], inventory: [] }, + admissions: [], + readings: [] + ) +} + +fn fixture_one_unevaluated() -> List { + [ + fixture_reading(entry: fixture_alpha, outcome: EmitSubjectClean), + fixture_reading(entry: fixture_beta, outcome: EmitSubjectNotEvaluated { cause: ExtentUnestablished }) + ] +} + +fn fixture_one_regressed() -> List { + [ + fixture_reading(entry: fixture_alpha, outcome: EmitSubjectClean), + fixture_reading(entry: fixture_beta, outcome: EmitSubjectBlocked { cause: BlockingDiagnostics { blocking: 1 } }) + ] +} + +fn fixture_gate_admission(r: EmitSubjectCleanRatchet) -> EmitRatchetEnrolmentAdmission { + emit_ratchet_enrolment_admission(enrolment: EnrolledAsGate, r: r) +} + +fn fixture_observation_admission(r: EmitSubjectCleanRatchet) -> EmitRatchetEnrolmentAdmission { + emit_ratchet_enrolment_admission(enrolment: EnrolledAsObservation, r: r) +} + +fn fixture_admission_permits(admission: EmitRatchetEnrolmentAdmission) -> Bool { + match admission { + EnrolmentPermitted { enrolment: _ } => true + EnrolmentRefusedNoUniverse { enrolment: _ } => false + EnrolmentRefusedDenominator { enrolment: _, missing: _ } => false + EnrolmentRefusedUnevaluated { enrolment: _, subjects: _ } => false } - && match emit_ratchet_gating_admission_of(denominators: DeclarationIndexAndModuleInventory) { - GatingPermitted => true - GatingRefusedDenominator { missing: _ } => false - } } -// AND THE WALL READS THE CARRIER, not just a bare argument: a fold that produced a standing carries -// the denominators it was folded over, so the enrolment question is answered from the artifact -// rather than from whatever the caller says about it. -test fn the_enrolment_wall_reads_the_denominators_the_carrier_was_folded_over() -> Bool { - match emit_ratchet_gating_admission( - r: fixture_fold_of(roster: fixture_roster, admissions: [], readings: fixture_both_clean()) - ) { - GatingPermitted => false - GatingRefusedDenominator { missing: _ } => true +// RED: a single-denominator carrier still cannot be gated on, and the refusal still names the +// missing denominator rather than answering a bare false. The control is the SAME readings under a +// dual denominator, so the refusal is about the universe's provenance and not about the fixture. +test fn a_single_denominator_carrier_refuses_a_gate_and_names_what_is_missing() -> Bool { + match fixture_gate_admission(r: fixture_fold_of(roster: fixture_roster, admissions: [], readings: fixture_both_clean())) { + EnrolmentRefusedDenominator { enrolment: _, missing: m } => string_contains(s: m, pattern: "file inventory") + EnrolmentPermitted { enrolment: _ } => false + EnrolmentRefusedNoUniverse { enrolment: _ } => false + EnrolmentRefusedUnevaluated { enrolment: _, subjects: _ } => false } - && match emit_ratchet_gating_admission(r: fixture_dual_fold(inventory: fixture_roster, readings: fixture_both_clean())) { - GatingPermitted => true - GatingRefusedDenominator { missing: _ } => false - } + && fixture_admission_permits( + admission: fixture_gate_admission(r: fixture_dual_fold(inventory: fixture_roster, readings: fixture_both_clean())) + ) +} + +// AND THE SAME CARRIER IS AN ADMISSIBLE OBSERVATION. This is the claim that makes the two modes +// different questions rather than one question with a label: refusing to LOOK because the universe +// was discovered under one denominator is the narrow, committed at the point where the reading is +// taken. What a single denominator disqualifies is DECIDING, and the report prints its denominators +// so the reading cannot be quoted wider than it was taken. +test fn a_single_denominator_carrier_is_still_an_admissible_observation() -> Bool { + fixture_admission_permits( + admission: fixture_observation_admission(r: fixture_fold_of(roster: fixture_roster, admissions: [], readings: fixture_both_clean())) + ) + && !fixture_admission_permits( + admission: fixture_gate_admission(r: fixture_fold_of(roster: fixture_roster, admissions: [], readings: fixture_both_clean())) + ) +} + +// RED, AND IT IS THE ONE THE OLD WALL COULD NOT PRODUCE: a DUAL-denominator fold — everything the +// previous wall consulted, answered in the permitting direction — whose roster contains a subject +// with no verdict at all. Gating on it would decide a closed-universe question over an open one, so +// it refuses and NAMES the subjects that have no verdict, because that list is the work that closes +// the gap. The control differs in exactly one field: the same fold with that one reading clean +// permits, which is what makes this a wall over the verdicts rather than a second denominator check. +test fn a_gate_refuses_a_dual_denominator_fold_whose_subjects_were_never_evaluated() -> Bool { + match fixture_gate_admission(r: fixture_dual_fold(inventory: fixture_roster, readings: fixture_one_unevaluated())) { + EnrolmentRefusedUnevaluated { enrolment: _, subjects: ss } => ss == [fixture_beta] + EnrolmentPermitted { enrolment: _ } => false + EnrolmentRefusedNoUniverse { enrolment: _ } => false + EnrolmentRefusedDenominator { enrolment: _, missing: _ } => false + } + && fixture_admission_permits( + admission: fixture_gate_admission(r: fixture_dual_fold(inventory: fixture_roster, readings: fixture_both_clean())) + ) +} + +// AND AN UNEVALUATED SUBJECT DOES NOT STOP THE OBSERVATION. It is the observation's CONTENT: hole 3 +// says a realistic universe folds to a wall of not-evaluated rows today, and a reading that refuses +// to be taken because its subjects are unmeasured reports nothing about the very population it was +// built to expose. The standing still refuses inside it — this claim is about who may be told, not +// about the news being good. +test fn an_unevaluated_subject_is_observed_rather_than_suppressed() -> Bool { + fixture_admission_permits( + admission: fixture_observation_admission(r: fixture_dual_fold(inventory: fixture_roster, readings: fixture_one_unevaluated())) + ) + && !fixture_admission_permits( + admission: fixture_gate_admission(r: fixture_dual_fold(inventory: fixture_roster, readings: fixture_one_unevaluated())) + ) +} + +// --------------------------------------------------------------------------------------------- +// EXECUTION PROVENANCE: the observation that was not taken, and the observation whose news is bad. +// +// DESIGN's test is stated as an equality between renderings: if a count of zero and an unreached +// stage produce the same output, the number is not an observation. These two claims are that test +// run in both directions, and the pair is the point — either alone is satisfiable by a carrier that +// simply always refuses or always permits. +// --------------------------------------------------------------------------------------------- + +// RED: a fold that discovered nothing holds NO STANDING. There is no field to read a standing out +// of, so no consumer can render it as one — the distinction is structural rather than checked. The +// control is a fold that WAS taken over the same shape of universe, whose rendering says `held`, and +// the claim asserts that word is absent from the not-taken rendering. +test fn an_observation_that_was_not_taken_holds_no_standing() -> Bool { + match emit_ratchet_observation(r: fixture_empty_dual_fold()) { + ObservationTaken { roster: _, standing: _ } => false + ObservationNotTaken { cause: c } => string_contains(s: c, pattern: "discovered no subject") + } + && !string_contains( + s: emit_ratchet_observation_text(observation: emit_ratchet_observation(r: fixture_empty_dual_fold())), + pattern: "held" + ) + && string_contains( + s: emit_ratchet_observation_text( + observation: emit_ratchet_observation(r: fixture_dual_fold(inventory: fixture_roster, readings: fixture_both_clean())) + ), + pattern: "held over 2 subject(s)" + ) +} + +// AND THE OTHER DIRECTION, which is the half a carrier that always refuses would fail: an entry that +// STOPPED being clean is a TAKEN observation carrying a REFUSING standing. The observation succeeded; +// the corpus is what is wrong. Collapsing this into the not-taken arm would be the mirror defect — +// bad news rendered as no news — and it is what would make an observation-first enrolment worthless. +test fn a_refusing_standing_is_a_taken_observation_and_not_a_missing_one() -> Bool { + match emit_ratchet_observation(r: fixture_dual_fold(inventory: fixture_roster, readings: fixture_one_regressed())) { + ObservationTaken { roster: _, standing: s } => + match s { + EmitRatchetRefused { failing_rows: rows } => + count(filter(rows, row => string_contains(s: row, pattern: "REGRESSED\tdag/fixture/beta.dag"))) == 1 + EmitRatchetHeld { subject_count: _ } => false + } + ObservationNotTaken { cause: _ } => false + } +} + +// AND THE REPORT INHERITS THE SPLIT RATHER THAN RE-DERIVING IT. A reader of the artifact — which is +// the only thing that survives the run — must be able to tell the two apart on the bytes, and must +// be able to see that what they are holding is not a gate verdict. +test fn the_report_distinguishes_an_untaken_observation_from_a_clean_one() -> Bool { + let taken = emit_ratchet_report_rows(r: fixture_dual_fold(inventory: fixture_roster, readings: fixture_both_clean())) + let untaken = emit_ratchet_report_rows(r: fixture_empty_dual_fold()) + count(filter(taken, row => string_contains(s: row, pattern: "observation\ttaken — held over 2 subject(s)"))) == 1 + && count(filter(untaken, row => string_contains(s: row, pattern: "observation\tNOT TAKEN"))) == 1 + && count(filter(untaken, row => string_contains(s: row, pattern: "observation\ttaken"))) == 0 + && count(filter(taken, row => string_contains(s: row, pattern: "enrolment_gate\tpermitted as gate"))) == 1 } // A ZERO-FILE TREE IS NOT A CLEAN ENTRY. @@ -541,3 +683,37 @@ test fn the_three_not_evaluated_causes_are_not_collapsed() -> Bool { == EmitSubjectNotEvaluated { cause: ExtentUnestablished } ) } + + +// --------------------------------------------------------------------------------------------- +// WHO RUNS THE RUNNER: the third state, which is neither a good fold nor a bad one. +// +// "The ratchet has not run yet" and "the ratchet will never run here" render identically as an +// absent report, and only the second is terminal. The first is a fold that was attempted; the +// second is a carrier with no scheduled route at all, and it is the state this ratchet is in today. +// The claim asserts today's answer and its control in one breath, so the derivation cannot be a +// constant wearing a standing's name. +// --------------------------------------------------------------------------------------------- + +// RED-ON-ENROLMENT BY CONSTRUCTION: this claim is green because the runner has NO consumer, and it +// goes red on the day one is agreed and the cadence row changes. That inversion is deliberate and it +// is the only mechanism that forces this claim and the block it mirrors to be rewritten together — +// a declaration that survives its own falsification is the rung inflation DESIGN calls worse than +// sitting low. +test fn the_ratchet_runner_has_no_executing_consumer_today() -> Bool { + match emit_ratchet_runner_execution_standing(cadence: emit_ratchet_runner_cadence) { + UnexecutedDeferredWitness { entry: e, function: f } => + e == "dag/tools/emit_subject_clean_ratchet.dag" && f == "observe" + WitnessHasExecutingConsumer { cadence: _ } => false + LegacyFrozenPathDeferral { entry: _, function: _ } => false + UnclassifiedPathDeferral { entry: _, function: _ } => false + DeclaredCadenceUnrealized { cadence: _, entry: _, function: _ } => false + } + && match emit_ratchet_runner_execution_standing(cadence: DiscoverySelection) { + WitnessHasExecutingConsumer { cadence: c } => c == DiscoverySelection + UnexecutedDeferredWitness { entry: _, function: _ } => false + LegacyFrozenPathDeferral { entry: _, function: _ } => false + UnclassifiedPathDeferral { entry: _, function: _ } => false + DeclaredCadenceUnrealized { cadence: _, entry: _, function: _ } => false + } +} diff --git a/dag/tools/emit_subject_clean_ratchet.dag b/dag/tools/emit_subject_clean_ratchet.dag index d2b9fccafee..5bbe5a2bb2b 100644 --- a/dag/tools/emit_subject_clean_ratchet.dag +++ b/dag/tools/emit_subject_clean_ratchet.dag @@ -19,11 +19,25 @@ import gunbc.emit_subject_clean_frontier { EmitRatchetStanding, EmitRatchetHeld, EmitRatchetRefused, + EmitRatchetEnrolment, + EnrolledAsGate, + EmitRatchetEnrolmentAdmission, + EnrolmentPermitted, + EnrolmentRefusedNoUniverse, + EnrolmentRefusedDenominator, + EnrolmentRefusedUnevaluated, + EmitRatchetObservation, + ObservationTaken, + ObservationNotTaken, RosterDiscoveryPolicy, DeclarationIndexUnderRoots, emit_subject_clean_admissions, emit_ratchet_report_text, emit_ratchet_standing, + emit_ratchet_observation, + emit_ratchet_observation_text, + emit_ratchet_enrolment_admission, + emit_ratchet_enrolment_admission_text, fold_emit_subject_clean_ratchet } @@ -157,55 +171,156 @@ fn run_emit_subject_clean_ratchet( } // --------------------------------------------------------------------------------------------- -// THE CLI SURFACE. +// THE ATTEMPT, WHICH IS WHERE THE HOST HALF'S EXECUTION PROVENANCE LIVES. +// +// Two things can go wrong before a fold exists at all: the roster cannot be read, or a source root +// cannot be listed. Neither is a standing about the corpus and neither may be folded into one -- a +// run that never reached the fold and a run that folded and found nothing are the two states DESIGN +// says must not render alike, and here they are separated at the point where the difference is +// still knowable. Below this line every consumer holds a fold or a typed cause, never a silence. +// --------------------------------------------------------------------------------------------- +type RatchetRunAttempt + = RatchetRunFolded { ratchet: EmitSubjectCleanRatchet } + | RatchetRunUnattempted { cause: String } + +fn attempt_emit_subject_clean_ratchet(entries: String) -> RatchetRunAttempt { + match emit_ratchet_roster() { + EmitRatchetRosterUnreadable { cause: c } => + RatchetRunUnattempted { cause: concat("the entry roster could not be read — ", c) } + EmitRatchetRosterEntries { entries: roster } => + match module_inventory(roots: witness_layer_roots) { + ModuleInventoryUnreadable { root: rt, cause: c } => + RatchetRunUnattempted { + cause: concat( + concat("the file inventory could not list ", rt), + concat( + " — refusing rather than folding an unreadable root into an empty one: ", + c + ) + ) + } + ModuleInventoryFiles { paths: inventory } => + RatchetRunFolded { + ratchet: run_emit_subject_clean_ratchet( + entries: entries, + roster: roster, + inventory: inventory + ) + } + } + } +} + +fn write_ratchet_report(report: String, r: EmitSubjectCleanRatchet) -> Bool { + Filesystem.Write(path: report, content: emit_ratchet_report_text(r: r)).success +} + +// --------------------------------------------------------------------------------------------- +// THE CLI SURFACE: TWO VERBS, BECAUSE ENROLMENT IS TWO QUESTIONS. // // gunbc run --source-root dag --source-root src/v2 \ -// --entry dag/tools/emit_subject_clean_ratchet.dag --function check \ +// --entry dag/tools/emit_subject_clean_ratchet.dag --function observe \ // --arg entries=dag/std/logic.dag --arg report=/tmp/ratchet.tsv // // The report is WRITTEN rather than returned for the same reason the instrument's is: `gunbc run` // maps a returned value to an exit status and has no value-printing verb. // -// THE EXIT STATUS REPORTS THE RATCHET, and unlike the instrument beneath it that is a statement -// about the SUBJECT: a refusing standing is a refusing entry, an orphaned admission row, or a run -// that did not measure its whole roster. An instrument that could not run reaches the fold as -// RatchetNotEvaluated and refuses there, so a broken instrument and a dirty corpus are -// both nonzero -- and the report says which, per subject, on its own row. +// `observe` REPORTS AND DOES NOT JUDGE THE CORPUS. Its exit status answers one question and it is +// not the one a reader expects: did the observation happen. A refusing standing -- a regressed +// entry, a stale admission row, a subject with no verdict -- exits SUCCESS, because the observation +// succeeded and its content is bad news that belongs in the report a human reads. What exits +// FAILURE is being unable to observe: the roster unreadable, a source root unlistable, the report +// unwritable, or a universe of no subjects. That is the split DESIGN's execution-provenance row +// demands, placed on the one channel a CI step actually reads. +// +// `check` IS THE GATE VERB AND IT REFUSES TO BE ONE TODAY. It routes through the enrolment +// admission first, so a consumer that wires it into a merge decision receives a typed refusal +// naming what disqualifies the carrier -- a single denominator, or roster subjects with no verdict +// at all -- rather than a verdict computed over a universe the fold could not evaluate. The +// refusal is a construction rather than a note precisely because no `Accepted` program can read a +// note, and the note is what this repository has already watched fail. +// --------------------------------------------------------------------------------------------- +fn observe(entries: String, report: String) -> ProcessExit { + if report == "" { + exit_failure(reason: "observe: --arg report= is required — the observation is written, not printed") + } else { + match attempt_emit_subject_clean_ratchet(entries: entries) { + RatchetRunUnattempted { cause: c } => + exit_failure(reason: concat("observe: the observation was not taken — ", c)) + RatchetRunFolded { ratchet: r } => + if !write_ratchet_report(report: report, r: r) { + exit_failure( + reason: concat( + "observe: the observation was taken and could not be written to ", + report + ) + ) + } else { + match emit_ratchet_observation(r: r) { + ObservationTaken { roster: _, standing: _ } => ExitSuccess + ObservationNotTaken { cause: c } => + exit_failure(reason: concat("observe: the observation was not taken — ", c)) + } + } + } + } +} + fn check(entries: String, report: String) -> ProcessExit { if report == "" { exit_failure(reason: "check: --arg report= is required — the standing is written, not printed") } else { - match emit_ratchet_roster() { - EmitRatchetRosterUnreadable { cause: c } => - exit_failure(reason: concat("check: the entry roster could not be read — ", c)) - EmitRatchetRosterEntries { entries: roster } => - match module_inventory(roots: witness_layer_roots) { - ModuleInventoryUnreadable { root: rt, cause: c } => - exit_failure( - reason: concat( - concat("check: the file inventory could not list ", rt), - concat(" — refusing rather than folding an unreadable root into an empty one: ", c) + match attempt_emit_subject_clean_ratchet(entries: entries) { + RatchetRunUnattempted { cause: c } => + exit_failure(reason: concat("check: ", c)) + RatchetRunFolded { ratchet: r } => + if !write_ratchet_report(report: report, r: r) { + exit_failure(reason: concat("check: could not write the standing to ", report)) + } else { + match emit_ratchet_enrolment_admission(enrolment: EnrolledAsGate, r: r) { + EnrolmentPermitted { enrolment: _ } => check_standing(r: r, report: report) + EnrolmentRefusedNoUniverse { enrolment: e } => + exit_failure( + reason: concat( + "check: this carrier may not decide a merge — ", + emit_ratchet_enrolment_admission_text( + admission: EnrolmentRefusedNoUniverse { enrolment: e } + ) + ) ) - ) - ModuleInventoryFiles { paths: inventory } => { - let r = run_emit_subject_clean_ratchet(entries: entries, roster: roster, inventory: inventory) - let write = Filesystem.Write(path: report, content: emit_ratchet_report_text(r: r)) - if !write.success { - exit_failure(reason: concat("check: could not write the standing to ", report)) - } else { - match emit_ratchet_standing(r: r) { - EmitRatchetHeld { subject_count: _ } => ExitSuccess - EmitRatchetRefused { failing_rows: rows } => - exit_failure( - reason: concat( - concat("check: the emit-subject clean ratchet refused — ", to_string(count(rows))), - concat(" row(s), named in ", report) - ) + EnrolmentRefusedDenominator { enrolment: e, missing: m } => + exit_failure( + reason: concat( + "check: this carrier may not decide a merge — ", + emit_ratchet_enrolment_admission_text( + admission: EnrolmentRefusedDenominator { enrolment: e, missing: m } ) - } - } + ) + ) + EnrolmentRefusedUnevaluated { enrolment: e, subjects: ss } => + exit_failure( + reason: concat( + "check: this carrier may not decide a merge — ", + emit_ratchet_enrolment_admission_text( + admission: EnrolmentRefusedUnevaluated { enrolment: e, subjects: ss } + ) + ) + ) } } } } } + +fn check_standing(r: EmitSubjectCleanRatchet, report: String) -> ProcessExit { + match emit_ratchet_standing(r: r) { + EmitRatchetHeld { subject_count: _ } => ExitSuccess + EmitRatchetRefused { failing_rows: rows } => + exit_failure( + reason: concat( + concat("check: the emit-subject clean ratchet refused — ", to_string(count(rows))), + concat(" row(s), named in ", report) + ) + ) + } +} From 34b13697a061636b999fdda65d451da80c618266 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 26 Aug 2026 06:56:25 +0000 Subject: [PATCH 2/7] Carry the typed admission on the not-taken arm, and delete the evidence that could not fail MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- dag/gunbc/emit_subject_clean_frontier.dag | 68 ++++++++++++------ ...it_subject_clean_frontier_witness_test.dag | 72 +++++++++++++------ dag/tools/emit_subject_clean_ratchet.dag | 9 ++- 3 files changed, 104 insertions(+), 45 deletions(-) diff --git a/dag/gunbc/emit_subject_clean_frontier.dag b/dag/gunbc/emit_subject_clean_frontier.dag index 4a8035f7ce4..0650ff1724b 100644 --- a/dag/gunbc/emit_subject_clean_frontier.dag +++ b/dag/gunbc/emit_subject_clean_frontier.dag @@ -1108,22 +1108,35 @@ fn ratchet_denominators(r: EmitSubjectCleanRatchet) -> RosterDenominators { } } +// WHETHER A VERDICT ESTABLISHED ANYTHING, asked as its own total question rather than inline. The +// two arms that answer NO are the two the whole not-evaluated wall exists for, and stating the +// predicate separately is what lets the selection below be a filter instead of an accumulator. +fn emit_ratchet_verdict_evaluated(v: EmitRatchetVerdict) -> Bool { + match v { + RatchetCleanHeld { entry: _ } => true + RatchetDebtHeld { entry: _, cause: _ } => true + RatchetRegressed { entry: _, cause: _ } => true + RatchetFrontierStale { entry: _ } => true + RatchetNotEvaluated { entry: _, on_frontier: _, cause: _ } => false + RatchetSubjectUnmeasured { entry: _, on_frontier: _ } => false + } +} + // THE UNEVALUATED SUBJECTS, BY NAME. A count would be the wrong shape for the same reason every // other count in this module is display only: the refusal has to tell an operator WHICH subjects // have no verdict, because that list is the work that closes the gap. +// +// SELECTED, NOT ACCUMULATED. The obvious spelling is a fold appending `concat(acc, [e])` per hit, +// which copies the accumulator on every append and is quadratic in the roster. DESIGN's bare-minimum- +// cost rule is explicit that a proven cost shape is fixed regardless of the realized n, because "n is +// small here" is not a time-stable fact -- and the roster here is the whole corpus, so it is not even +// small. filter-then-map says the same thing in the shape that does not copy. (This module's peer +// accumulators predate this change and are not touched by it; pricing an unrelated cut against them +// would be the wrong denominator.) fn ratchet_unevaluated_subjects(r: EmitSubjectCleanRatchet) -> List { - fold( - r.verdicts, - init: [], - f: (acc, v) => - match v { - RatchetCleanHeld { entry: _ } => acc - RatchetDebtHeld { entry: _, cause: _ } => acc - RatchetRegressed { entry: _, cause: _ } => acc - RatchetFrontierStale { entry: _ } => acc - RatchetNotEvaluated { entry: e, on_frontier: _, cause: _ } => concat(acc, [e]) - RatchetSubjectUnmeasured { entry: e, on_frontier: _ } => concat(acc, [e]) - } + map( + filter(r.verdicts, v => !emit_ratchet_verdict_evaluated(v: v)), + v => emit_ratchet_verdict_entry(v: v) ) } @@ -1194,25 +1207,39 @@ fn emit_ratchet_enrolment_admission_text(admission: EmitRatchetEnrolmentAdmissio // standing at all, so there is no spelling in which a fold that never happened reads as a fold that // found nothing wrong. // +// AND NO WITNESS ASSERTS THAT LAST SENTENCE, DELIBERATELY. The absent field is unauthorable at BOTH +// §4b boundaries -- not in the corpus, and not in a fixture either, since no fixture can construct a +// variant field that does not exist -- so a check over it would be permanently green BY CONSTRUCTION +// and worse than absent for being cited as coverage. What the witness asserts instead is the thing +// that CAN fail: that an unobservable fold DISPATCHES to this arm rather than to the taken one. +// // AND A REFUSING STANDING IS A TAKEN OBSERVATION. That is the whole distinction this carrier exists // to hold: the observation succeeded and the news is bad. Its consumer reports it and does not stop // the line on it; what stops the line is being unable to observe at all. // --------------------------------------------------------------------------------------------- +// THE NOT-TAKEN ARM CARRIES THE ADMISSION, NOT ITS RENDERING, and that is a correction rather than a +// preference. It held a `cause: String` -- the typed refusal flattened into prose at the moment it +// was stored -- which is DESIGN §2's anemic leaf: a String hiding named parts that already exist one +// function away. The cost was immediate and was caught in review: every claim about WHY an +// observation was not taken had to be a substring match over rendered text, so the evidence for this +// carrier's strongest property was a change detector that reds on a wording edit and greens on any +// prose containing the phrase. Storing the admission makes the same question structural, and the +// rendering becomes what it should have been -- a projection, derived at the edge, never the record. type EmitRatchetObservation = ObservationTaken { roster: RosterIdentity, standing: EmitRatchetStanding } - | ObservationNotTaken { cause: String } + | ObservationNotTaken { admission: EmitRatchetEnrolmentAdmission } fn emit_ratchet_observation(r: EmitSubjectCleanRatchet) -> EmitRatchetObservation { let admission = emit_ratchet_enrolment_admission(enrolment: EnrolledAsObservation, r: r) match admission { EnrolmentPermitted { enrolment: _ } => ObservationTaken { roster: r.roster, standing: emit_ratchet_standing(r: r) } - EnrolmentRefusedNoUniverse { enrolment: _ } => - ObservationNotTaken { cause: emit_ratchet_enrolment_admission_text(admission: admission) } - EnrolmentRefusedDenominator { enrolment: _, missing: _ } => - ObservationNotTaken { cause: emit_ratchet_enrolment_admission_text(admission: admission) } - EnrolmentRefusedUnevaluated { enrolment: _, subjects: _ } => - ObservationNotTaken { cause: emit_ratchet_enrolment_admission_text(admission: admission) } + EnrolmentRefusedNoUniverse { enrolment: e } => + ObservationNotTaken { admission: EnrolmentRefusedNoUniverse { enrolment: e } } + EnrolmentRefusedDenominator { enrolment: e, missing: m } => + ObservationNotTaken { admission: EnrolmentRefusedDenominator { enrolment: e, missing: m } } + EnrolmentRefusedUnevaluated { enrolment: e, subjects: ss } => + ObservationNotTaken { admission: EnrolmentRefusedUnevaluated { enrolment: e, subjects: ss } } } } @@ -1220,7 +1247,8 @@ fn emit_ratchet_observation_text(observation: EmitRatchetObservation) -> String match observation { ObservationTaken { roster: _, standing: s } => concat("taken — ", emit_ratchet_standing_text(standing: s)) - ObservationNotTaken { cause: c } => concat("NOT TAKEN — ", c) + ObservationNotTaken { admission: a } => + concat("NOT TAKEN — ", emit_ratchet_enrolment_admission_text(admission: a)) } } diff --git a/dag/test/claim/emit_subject_clean_frontier_witness_test.dag b/dag/test/claim/emit_subject_clean_frontier_witness_test.dag index e898d49e6d6..278b7fecc87 100644 --- a/dag/test/claim/emit_subject_clean_frontier_witness_test.dag +++ b/dag/test/claim/emit_subject_clean_frontier_witness_test.dag @@ -600,25 +600,36 @@ test fn an_unevaluated_subject_is_observed_rather_than_suppressed() -> Bool { // simply always refuses or always permits. // --------------------------------------------------------------------------------------------- -// RED: a fold that discovered nothing holds NO STANDING. There is no field to read a standing out -// of, so no consumer can render it as one — the distinction is structural rather than checked. The -// control is a fold that WAS taken over the same shape of universe, whose rendering says `held`, and -// the claim asserts that word is absent from the not-taken rendering. -test fn an_observation_that_was_not_taken_holds_no_standing() -> Bool { +// RED: a fold that discovered nothing DISPATCHES TO THE NOT-TAKEN ARM, and it names the refusal +// STRUCTURALLY rather than by matching prose. +// +// WHAT THIS ROW DELIBERATELY DOES NOT ASSERT, because the first shape of it did and the assertion +// could not fail: that the not-taken arm holds no standing. That is true, and it is true BY +// CONSTRUCTION -- the variant has no such field, so the violating state is unauthorable in the +// corpus AND in a fixture, which §4b names as exactly the case where the right answer is no check +// at all. Three of that row's four conjuncts were substring matches over rendered text, so the one +// artifact a reader would have cited as proof of execution provenance was a change detector: red on +// any wording edit, green on any cause carrying the phrase. The property survives in the type; only +// its fake evidence is gone. +// +// WHAT REMAINS IS THE PART THAT CAN FAIL FOR THE RIGHT REASON: which arm an unobservable fold routes +// to, and which refusal it carries. Both halves are now variant matches, so a prose edit moves +// nothing here and a dispatch change reds it. +test fn an_empty_dual_fold_yields_no_observation() -> Bool { match emit_ratchet_observation(r: fixture_empty_dual_fold()) { + ObservationNotTaken { admission: a } => + match a { + EnrolmentRefusedNoUniverse { enrolment: e } => e == EnrolledAsObservation + EnrolmentPermitted { enrolment: _ } => false + EnrolmentRefusedDenominator { enrolment: _, missing: _ } => false + EnrolmentRefusedUnevaluated { enrolment: _, subjects: _ } => false + } ObservationTaken { roster: _, standing: _ } => false - ObservationNotTaken { cause: c } => string_contains(s: c, pattern: "discovered no subject") } - && !string_contains( - s: emit_ratchet_observation_text(observation: emit_ratchet_observation(r: fixture_empty_dual_fold())), - pattern: "held" - ) - && string_contains( - s: emit_ratchet_observation_text( - observation: emit_ratchet_observation(r: fixture_dual_fold(inventory: fixture_roster, readings: fixture_both_clean())) - ), - pattern: "held over 2 subject(s)" - ) + && match emit_ratchet_observation(r: fixture_dual_fold(inventory: fixture_roster, readings: fixture_both_clean())) { + ObservationTaken { roster: _, standing: s } => s == EmitRatchetHeld { subject_count: 2 } + ObservationNotTaken { admission: _ } => false + } } // AND THE OTHER DIRECTION, which is the half a carrier that always refuses would fail: an entry that @@ -633,20 +644,35 @@ test fn a_refusing_standing_is_a_taken_observation_and_not_a_missing_one() -> Bo count(filter(rows, row => string_contains(s: row, pattern: "REGRESSED\tdag/fixture/beta.dag"))) == 1 EmitRatchetHeld { subject_count: _ } => false } - ObservationNotTaken { cause: _ } => false + ObservationNotTaken { admission: _ } => false } } // AND THE REPORT INHERITS THE SPLIT RATHER THAN RE-DERIVING IT. A reader of the artifact — which is // the only thing that survives the run — must be able to tell the two apart on the bytes, and must // be able to see that what they are holding is not a gate verdict. +// +// THE EXPECTED ROWS ARE COMPOSED FROM THE RENDERER, never hand-written. A literal fragment here +// would pin the renderer's current wording into an unrelated claim, so an edit to one authority +// would red the other — the fork §3 forbids, arriving as a test fixture. What is asserted is that +// the report CARRIES the observation's own rendering and that the two renderings DIFFER, which is +// the distinction the row is named for and the only one it should own. +fn fixture_observation_row(r: EmitSubjectCleanRatchet) -> String { + concat("observation\t", emit_ratchet_observation_text(observation: emit_ratchet_observation(r: r))) +} + test fn the_report_distinguishes_an_untaken_observation_from_a_clean_one() -> Bool { - let taken = emit_ratchet_report_rows(r: fixture_dual_fold(inventory: fixture_roster, readings: fixture_both_clean())) - let untaken = emit_ratchet_report_rows(r: fixture_empty_dual_fold()) - count(filter(taken, row => string_contains(s: row, pattern: "observation\ttaken — held over 2 subject(s)"))) == 1 - && count(filter(untaken, row => string_contains(s: row, pattern: "observation\tNOT TAKEN"))) == 1 - && count(filter(untaken, row => string_contains(s: row, pattern: "observation\ttaken"))) == 0 - && count(filter(taken, row => string_contains(s: row, pattern: "enrolment_gate\tpermitted as gate"))) == 1 + let clean = fixture_dual_fold(inventory: fixture_roster, readings: fixture_both_clean()) + let empty = fixture_empty_dual_fold() + count(filter(emit_ratchet_report_rows(r: clean), row => row == fixture_observation_row(r: clean))) == 1 + && count(filter(emit_ratchet_report_rows(r: empty), row => row == fixture_observation_row(r: empty))) == 1 + && !(fixture_observation_row(r: clean) == fixture_observation_row(r: empty)) + && count( + filter( + emit_ratchet_report_rows(r: clean), + row => row == concat("enrolment_gate\t", emit_ratchet_enrolment_admission_text(admission: fixture_gate_admission(r: clean))) + ) + ) == 1 } // A ZERO-FILE TREE IS NOT A CLEAN ENTRY. diff --git a/dag/tools/emit_subject_clean_ratchet.dag b/dag/tools/emit_subject_clean_ratchet.dag index 5bbe5a2bb2b..a9a74407854 100644 --- a/dag/tools/emit_subject_clean_ratchet.dag +++ b/dag/tools/emit_subject_clean_ratchet.dag @@ -258,8 +258,13 @@ fn observe(entries: String, report: String) -> ProcessExit { } else { match emit_ratchet_observation(r: r) { ObservationTaken { roster: _, standing: _ } => ExitSuccess - ObservationNotTaken { cause: c } => - exit_failure(reason: concat("observe: the observation was not taken — ", c)) + ObservationNotTaken { admission: a } => + exit_failure( + reason: concat( + "observe: the observation was not taken — ", + emit_ratchet_enrolment_admission_text(admission: a) + ) + ) } } } From 9db13fd8a06decfd991abbb4ce52f6365f24419f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 26 Aug 2026 07:32:14 +0000 Subject: [PATCH 3/7] Dissolve the roster predicate into a direct match, and repair a stale citation to a symbol this branch deletes MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- dag/gunbc/emit_subject_clean_frontier.dag | 77 ++++++++++++++----- ...it_subject_clean_frontier_witness_test.dag | 24 ++++-- 2 files changed, 78 insertions(+), 23 deletions(-) diff --git a/dag/gunbc/emit_subject_clean_frontier.dag b/dag/gunbc/emit_subject_clean_frontier.dag index 0650ff1724b..3053eea357a 100644 --- a/dag/gunbc/emit_subject_clean_frontier.dag +++ b/dag/gunbc/emit_subject_clean_frontier.dag @@ -313,10 +313,14 @@ type RosterDiscoveryPolicy // them. That is exactly the failure this carrier exists to remove, committed by the carrier itself. // // So the rule "nothing may gate on a single-denominator universe" is carried by -// `emit_ratchet_gating_admission` below, which REFUSES on this field. Enrolling a single-denominator -// carrier is then a typed refusal naming the missing denominator, not a missed paragraph — and when -// the file inventory lands, the field changes and enrolment becomes possible with no note for -// anyone to remember. +// `emit_ratchet_gate_admission` below, which REFUSES on this field. Enrolling a single-denominator +// carrier as a GATE is then a typed refusal naming the missing denominator, not a missed paragraph. +// +// AND THE FIELD NO LONGER DECIDES ENROLMENT BY ITSELF, which is the correction this sentence needed +// rather than a widening of it. It used to end "when the file inventory lands, the field changes and +// enrolment becomes possible" -- true of the wall as it then stood, and false the moment that landed: +// a dual denominator makes a gate ELIGIBLE, not admissible, because a gate additionally requires that +// every roster subject was evaluated. Enrolment as an OBSERVATION does not consult this field at all. type RosterDenominators = DeclarationIndexOnly | DeclarationIndexAndModuleInventory @@ -1076,6 +1080,27 @@ fn emit_ratchet_standing_text(standing: EmitRatchetStanding) -> String { // // BOTH ARMS OF EVERY REFUSAL ARE AUTHORABLE, which is what makes this a wall rather than a // decoration: the witness beside this module produces each refusing input and its one-field control. +// +// AND THE GATE'S PERMITTING ARM IS UNOCCUPIED ON THE LIVE CORPUS TODAY, WHICH IS A DIFFERENT FACT +// FROM BEING UNREACHABLE -- the distinction decides whether this arm is a quiet wall or a decoration, +// and only one of those readings licenses deleting it. Hole 3 above: the instrument reads compiler +// stderr through a bounded TAIL while the entry-scope marker prints near the HEAD, so a talkative +// subject loses its marker and arrives NOT-EVALUATED. Over a realistic roster under `dag` that means +// the any-unevaluated condition refuses essentially always, so nothing currently RECEIVES the permit +// (relayed from gentle-bee-495, 2026-08-26, on the measuring lane's nine sized specimens -- a SHAPE +// and not a rate, since nine chosen entries are not a census, and no proportion is stated here or in +// hole 3). +// +// THAT IS OCCUPANCY, NOT REACHABILITY. DESIGN's reachability-read-as-occupancy row puts the test at +// the FIXTURE boundary rather than the corpus one, and the permit is authorable there -- the witness +// authors it, as the one-field control beside the unevaluated refusal, and it goes red if the arm +// stops permitting. Yes / yes / zero is a healthy guard being quiet. So this arm is not relaxed to +// tolerate unevaluated subjects, which would convert the instrument's blindness into a green: the +// absorbing fallback exactly, arriving as a kindness to a roster that is not ready. +// +// WHAT THE PERMIT ACTUALLY WAITS ON is therefore not this module and not the admission roster: it is +// a typed entry-scope output the reader does not reconstruct from prose. No tail size closes it -- +// the marker is bounded from the head and the window from the tail, so the two never meet by tuning. // --------------------------------------------------------------------------------------------- type EmitRatchetEnrolment = EnrolledAsObservation @@ -1094,13 +1119,6 @@ type EmitRatchetEnrolmentAdmission | EnrolmentRefusedDenominator { enrolment: EmitRatchetEnrolment, missing: String } | EnrolmentRefusedUnevaluated { enrolment: EmitRatchetEnrolment, subjects: List } -fn ratchet_roster_is_empty(r: EmitSubjectCleanRatchet) -> Bool { - match r.roster { - RosterEmpty { policy: _, denominators: _ } => true - RosterIdentified { policy: _, denominators: _, subject_count: _, digest: _ } => false - } -} - fn ratchet_denominators(r: EmitSubjectCleanRatchet) -> RosterDenominators { match r.roster { RosterEmpty { policy: _, denominators: dn } => dn @@ -1111,6 +1129,15 @@ fn ratchet_denominators(r: EmitSubjectCleanRatchet) -> RosterDenominators { // WHETHER A VERDICT ESTABLISHED ANYTHING, asked as its own total question rather than inline. The // two arms that answer NO are the two the whole not-evaluated wall exists for, and stating the // predicate separately is what lets the selection below be a filter instead of an accumulator. +// +// THIS ONE IS A PREDICATE AND STAYS ONE, for two reasons that do not apply to the roster above. +// `filter` takes a `Bool` by construction, so dissolving this into a direct match means going back +// to a fold that appends -- the quadratic accumulator this very change removed. And it is NOT a +// second accessor for an existing answer: `emit_ratchet_verdict_holds` beside it answers a DIFFERENT +// question over the same coproduct, and `RatchetRegressed` is the row that proves it -- holds=false, +// evaluated=TRUE. A regression is a verdict the fold established and then refused; collapsing the two +// questions would make an evaluated failure indistinguishable from a subject nobody could measure, +// which is the distinction this entire carrier exists to hold. fn emit_ratchet_verdict_evaluated(v: EmitRatchetVerdict) -> Bool { match v { RatchetCleanHeld { entry: _ } => true @@ -1158,17 +1185,23 @@ fn emit_ratchet_gate_admission(r: EmitSubjectCleanRatchet) -> EmitRatchetEnrolme } } +// THE ROSTER COPRODUCT IS MATCHED DIRECTLY, not through a Bool. A `roster_is_empty` predicate would +// be a second place holding the same shape knowledge, and the repository has already dissolved that +// exact pattern twice -- `std.witness_admission` `witness_admission_predicate_dissolution_note` +// (review 39760) and `v2.std.witness_execution_routing` -- in both cases by making the CONSUMER match +// the coproduct instead. `RosterEmpty` carries the discovery failure, so reading it here is reading +// the authority rather than a derived answer about it. fn emit_ratchet_enrolment_admission( enrolment: EmitRatchetEnrolment, r: EmitSubjectCleanRatchet ) -> EmitRatchetEnrolmentAdmission { - if ratchet_roster_is_empty(r: r) { - EnrolmentRefusedNoUniverse { enrolment: enrolment } - } else { - match enrolment { - EnrolledAsObservation => EnrolmentPermitted { enrolment: enrolment } - EnrolledAsGate => emit_ratchet_gate_admission(r: r) - } + match r.roster { + RosterEmpty { policy: _, denominators: _ } => EnrolmentRefusedNoUniverse { enrolment: enrolment } + RosterIdentified { policy: _, denominators: _, subject_count: _, digest: _ } => + match enrolment { + EnrolledAsObservation => EnrolmentPermitted { enrolment: enrolment } + EnrolledAsGate => emit_ratchet_gate_admission(r: r) + } } } @@ -1326,6 +1359,14 @@ data emit_subject_clean_admissions: List = [] // PR: enrolment is a floor-cut re-add and DESIGN requires each of those to be re-derived under its // own operator agreement, which is not a thing a diff can author. // +// WHEN A CADENCE IS AGREED, THE ROW AND ITS WITNESS MOVE IN ONE DIFF. Changing +// `emit_ratchet_runner_cadence` without replacing or inverting +// `the_ratchet_runner_has_no_executing_consumer_today` in the SAME change leaves a known-false +// declaration standing green -- which is this carrier's own third-state defect arriving from the +// other side: there, an absent report could not say whether it would ever be produced; here, a +// declaration would keep asserting nobody runs the runner after somebody does. The claim is written +// to red on that change rather than to survive it, and the enrolment diff is expected to carry both. +// // AND THIS FUNCTION IS NOT CONSTANT, which is what keeps the declaration from being a decoration: // handed a cadence that HAS a scheduled route it returns the covered arm, and the witness beside // this module asserts both directions. The day enrolment is agreed, the cadence row below changes, diff --git a/dag/test/claim/emit_subject_clean_frontier_witness_test.dag b/dag/test/claim/emit_subject_clean_frontier_witness_test.dag index 278b7fecc87..651c7d46484 100644 --- a/dag/test/claim/emit_subject_clean_frontier_witness_test.dag +++ b/dag/test/claim/emit_subject_clean_frontier_witness_test.dag @@ -530,12 +530,15 @@ fn fixture_admission_permits(admission: EmitRatchetEnrolmentAdmission) -> Bool { } } -// RED: a single-denominator carrier still cannot be gated on, and the refusal still names the -// missing denominator rather than answering a bare false. The control is the SAME readings under a +// RED: a single-denominator carrier still cannot be gated on, and WHICH refusal it receives is +// asserted as a VARIANT rather than as a substring of the refusal's prose. The refusal does still +// name the missing denominator -- that is what `missing` carries -- but the naming is REPORT +// RENDERING and this row's declared subject is the semantic admission, so pinning the wording here +// would red this claim on an edit to a different authority. The control is the SAME readings under a // dual denominator, so the refusal is about the universe's provenance and not about the fixture. -test fn a_single_denominator_carrier_refuses_a_gate_and_names_what_is_missing() -> Bool { +test fn a_single_denominator_carrier_refuses_a_gate_and_permits_none() -> Bool { match fixture_gate_admission(r: fixture_fold_of(roster: fixture_roster, admissions: [], readings: fixture_both_clean())) { - EnrolmentRefusedDenominator { enrolment: _, missing: m } => string_contains(s: m, pattern: "file inventory") + EnrolmentRefusedDenominator { enrolment: e, missing: _ } => e == EnrolledAsGate EnrolmentPermitted { enrolment: _ } => false EnrolmentRefusedNoUniverse { enrolment: _ } => false EnrolmentRefusedUnevaluated { enrolment: _, subjects: _ } => false @@ -641,7 +644,18 @@ test fn a_refusing_standing_is_a_taken_observation_and_not_a_missing_one() -> Bo ObservationTaken { roster: _, standing: s } => match s { EmitRatchetRefused { failing_rows: rows } => - count(filter(rows, row => string_contains(s: row, pattern: "REGRESSED\tdag/fixture/beta.dag"))) == 1 + count( + filter( + rows, + row => + row == emit_ratchet_verdict_row( + v: RatchetRegressed { + entry: fixture_beta, + cause: BlockingDiagnostics { blocking: 1 } + } + ) + ) + ) == 1 EmitRatchetHeld { subject_count: _ } => false } ObservationNotTaken { admission: _ } => false From ef5e42d27d82160cc8f39db22f1064814fc6d032 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 26 Aug 2026 08:34:20 +0000 Subject: [PATCH 4/7] Carry the two-arm measurement behind the surviving predicate, not the 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) --- dag/gunbc/emit_subject_clean_frontier.dag | 23 +++++++++++++++++++---- 1 file changed, 19 insertions(+), 4 deletions(-) diff --git a/dag/gunbc/emit_subject_clean_frontier.dag b/dag/gunbc/emit_subject_clean_frontier.dag index 3053eea357a..aacc86d89b0 100644 --- a/dag/gunbc/emit_subject_clean_frontier.dag +++ b/dag/gunbc/emit_subject_clean_frontier.dag @@ -1134,10 +1134,25 @@ fn ratchet_denominators(r: EmitSubjectCleanRatchet) -> RosterDenominators { // `filter` takes a `Bool` by construction, so dissolving this into a direct match means going back // to a fold that appends -- the quadratic accumulator this very change removed. And it is NOT a // second accessor for an existing answer: `emit_ratchet_verdict_holds` beside it answers a DIFFERENT -// question over the same coproduct, and `RatchetRegressed` is the row that proves it -- holds=false, -// evaluated=TRUE. A regression is a verdict the fold established and then refused; collapsing the two -// questions would make an evaluated failure indistinguishable from a subject nobody could measure, -// which is the distinction this entire carrier exists to hold. +// question over the same coproduct, and the disagreement is measurable rather than argued -- +// +// variant holds evaluated +// RatchetCleanHeld true true +// RatchetDebtHeld true true +// RatchetRegressed FALSE TRUE <-- disagree +// RatchetFrontierStale FALSE TRUE <-- disagree +// RatchetNotEvaluated false false +// RatchetSubjectUnmeasured false false +// +// TWO ARMS DISAGREE, AND THAT IS STRONGER THAN ONE. A single disagreeing variant could be dismissed +// as an accident of how that one case is treated; two disagreeing in the SAME DIRECTION show the +// functions are answering different questions by construction. Both 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. Collapsing the two questions would make an evaluated +// failure indistinguishable from an unevaluated subject, which is the state-space conflation this +// entire carrier exists to refuse -- committed inside the machinery that refuses it. +// (Two-arm measurement: smart-ram-730, 2026-08-26, independently re-derived against this branch.) fn emit_ratchet_verdict_evaluated(v: EmitRatchetVerdict) -> Bool { match v { RatchetCleanHeld { entry: _ } => true From f3d5c810973d97f3c6966ab65fe3e1fb72516e27 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 26 Aug 2026 09:08:09 +0000 Subject: [PATCH 5/7] Give both verdict questions one authority: a canonical classification, 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) --- dag/gunbc/emit_subject_clean_frontier.dag | 97 +++++++++++-------- ...it_subject_clean_frontier_witness_test.dag | 47 +++++++++ 2 files changed, 103 insertions(+), 41 deletions(-) diff --git a/dag/gunbc/emit_subject_clean_frontier.dag b/dag/gunbc/emit_subject_clean_frontier.dag index aacc86d89b0..5d1bc1e10d8 100644 --- a/dag/gunbc/emit_subject_clean_frontier.dag +++ b/dag/gunbc/emit_subject_clean_frontier.dag @@ -800,14 +800,54 @@ fn emit_ratchet_verdict_entry(v: EmitRatchetVerdict) -> String { } } -fn emit_ratchet_verdict_holds(v: EmitRatchetVerdict) -> Bool { +// --------------------------------------------------------------------------------------------- +// THE CANONICAL CLASSIFICATION, and it is the ONE place that reads the verdict vocabulary's shape. +// +// Two questions are asked of a verdict -- did the ratchet HOLD, and was the subject EVALUATED AT ALL +// -- and they were answered by two independent total matches. Review 56204 is right that this +// duplicates the coproduct's shape knowledge across two authorities, and right that distinct +// semantics do not exempt it: both facts can be true at once, which is what neither of my earlier +// answers said. Two matches over six variants is two places to edit when a variant lands, and the +// compiler forcing both to be total does not make them one authority. +// +// SO THE FIX IS NOT TO DELETE A PREDICATE BUT TO GIVE BOTH ONE SOURCE. The three-way classification +// below is the real semantic axis, and naming it turns the disagreement the two predicates exhibited +// into a CONSTRUCT rather than an emergent difference someone has to measure to discover: +// +// VerdictHeld the fold established a verdict and the ratchet holds +// VerdictEstablishedAndRefused 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 +// VerdictUnestablished no verdict about this subject exists at all +// +// That middle class IS the population where the two questions diverge: holds=false, evaluated=true. +// It previously had to be discovered by comparing two functions arm by arm; now it has a name, and +// a new verdict variant fails to compile in exactly one place instead of two. +type VerdictStanding + = VerdictHeld + | VerdictEstablishedAndRefused + | VerdictUnestablished + +fn emit_ratchet_verdict_standing(v: EmitRatchetVerdict) -> VerdictStanding { match v { - RatchetCleanHeld { entry: _ } => true - RatchetDebtHeld { entry: _, cause: _ } => true - RatchetRegressed { entry: _, cause: _ } => false - RatchetFrontierStale { entry: _ } => false - RatchetNotEvaluated { entry: _, on_frontier: _, cause: _ } => false - RatchetSubjectUnmeasured { entry: _, on_frontier: _ } => false + RatchetCleanHeld { entry: _ } => VerdictHeld + RatchetDebtHeld { entry: _, cause: _ } => VerdictHeld + RatchetRegressed { entry: _, cause: _ } => VerdictEstablishedAndRefused + RatchetFrontierStale { entry: _ } => VerdictEstablishedAndRefused + RatchetNotEvaluated { entry: _, on_frontier: _, cause: _ } => VerdictUnestablished + RatchetSubjectUnmeasured { entry: _, on_frontier: _ } => VerdictUnestablished + } +} + +// BOTH PREDICATES ARE NOW PROJECTIONS OVER THE CLASSIFICATION, never over the storage shape. They +// stay predicates because `filter` takes a `Bool`, but that is now a question about the CONSUMER's +// interface rather than a reason to duplicate variant knowledge -- which is the distinction the +// earlier defence of them missed. +fn emit_ratchet_verdict_holds(v: EmitRatchetVerdict) -> Bool { + match emit_ratchet_verdict_standing(v: v) { + VerdictHeld => true + VerdictEstablishedAndRefused => false + VerdictUnestablished => false } } @@ -1126,41 +1166,16 @@ fn ratchet_denominators(r: EmitSubjectCleanRatchet) -> RosterDenominators { } } -// WHETHER A VERDICT ESTABLISHED ANYTHING, asked as its own total question rather than inline. The -// two arms that answer NO are the two the whole not-evaluated wall exists for, and stating the -// predicate separately is what lets the selection below be a filter instead of an accumulator. -// -// THIS ONE IS A PREDICATE AND STAYS ONE, for two reasons that do not apply to the roster above. -// `filter` takes a `Bool` by construction, so dissolving this into a direct match means going back -// to a fold that appends -- the quadratic accumulator this very change removed. And it is NOT a -// second accessor for an existing answer: `emit_ratchet_verdict_holds` beside it answers a DIFFERENT -// question over the same coproduct, and the disagreement is measurable rather than argued -- -// -// variant holds evaluated -// RatchetCleanHeld true true -// RatchetDebtHeld true true -// RatchetRegressed FALSE TRUE <-- disagree -// RatchetFrontierStale FALSE TRUE <-- disagree -// RatchetNotEvaluated false false -// RatchetSubjectUnmeasured false false -// -// TWO ARMS DISAGREE, AND THAT IS STRONGER THAN ONE. A single disagreeing variant could be dismissed -// as an accident of how that one case is treated; two disagreeing in the SAME DIRECTION show the -// functions are answering different questions by construction. Both 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. Collapsing the two questions would make an evaluated -// failure indistinguishable from an unevaluated subject, which is the state-space conflation this -// entire carrier exists to refuse -- committed inside the machinery that refuses it. -// (Two-arm measurement: smart-ram-730, 2026-08-26, independently re-derived against this branch.) +// WHETHER A VERDICT ESTABLISHED ANYTHING -- the second projection over the same classification, and +// the one the not-evaluated wall turns on. `VerdictEstablishedAndRefused` answering TRUE here while +// answering FALSE in `holds` is the whole content of the split: an evaluated failure must never be +// indistinguishable from a subject nobody could measure, which is the state-space conflation this +// carrier exists to refuse. fn emit_ratchet_verdict_evaluated(v: EmitRatchetVerdict) -> Bool { - match v { - RatchetCleanHeld { entry: _ } => true - RatchetDebtHeld { entry: _, cause: _ } => true - RatchetRegressed { entry: _, cause: _ } => true - RatchetFrontierStale { entry: _ } => true - RatchetNotEvaluated { entry: _, on_frontier: _, cause: _ } => false - RatchetSubjectUnmeasured { entry: _, on_frontier: _ } => false + match emit_ratchet_verdict_standing(v: v) { + VerdictHeld => true + VerdictEstablishedAndRefused => true + VerdictUnestablished => false } } diff --git a/dag/test/claim/emit_subject_clean_frontier_witness_test.dag b/dag/test/claim/emit_subject_clean_frontier_witness_test.dag index 651c7d46484..ea30bedb250 100644 --- a/dag/test/claim/emit_subject_clean_frontier_witness_test.dag +++ b/dag/test/claim/emit_subject_clean_frontier_witness_test.dag @@ -757,3 +757,50 @@ test fn the_ratchet_runner_has_no_executing_consumer_today() -> Bool { DeclaredCadenceUnrealized { cadence: _, entry: _, function: _ } => false } } + +// --------------------------------------------------------------------------------------------- +// THE TWO VERDICT QUESTIONS ARE PROJECTIONS OF ONE CLASSIFICATION, and the relation between them is +// asserted rather than left to be rediscovered by comparing two functions arm by arm. +// +// WHY THIS ROW EXISTS AT ALL: the divergence between `holds` and `evaluated` was previously an +// EMERGENT fact -- two independent matches that happened to disagree on two arms, discoverable only +// by measuring them against each other, which is exactly how it came up in review. Routing both +// through `emit_ratchet_verdict_standing` makes the divergence a named class, and this claim pins +// the two properties that make the split load-bearing rather than decorative. +data every_verdict_shape: List = [ + RatchetCleanHeld { entry: fixture_alpha }, + RatchetDebtHeld { entry: fixture_alpha, cause: BlockingDiagnostics { blocking: 1 } }, + RatchetRegressed { entry: fixture_alpha, cause: BlockingDiagnostics { blocking: 1 } }, + RatchetFrontierStale { entry: fixture_alpha }, + RatchetNotEvaluated { entry: fixture_alpha, on_frontier: false, cause: ExtentUnestablished }, + RatchetSubjectUnmeasured { entry: fixture_alpha, on_frontier: false } +] + +// A HELD VERDICT IS ALWAYS AN EVALUATED ONE -- the ratchet cannot hold over a subject nobody +// measured. If this ever fails, some arm is reporting a verdict it never established. +test fn holding_a_verdict_entails_having_established_it() -> Bool { + count( + filter( + every_verdict_shape, + v => emit_ratchet_verdict_holds(v: v) && !emit_ratchet_verdict_evaluated(v: v) + ) + ) == 0 +} + +// AND THE CONVERSE MUST NOT HOLD, which is the half that makes the two questions distinct rather +// than one question spelled twice. An ESTABLISHED-AND-REFUSED verdict is evaluated and does not +// hold; if this set were empty the split would be a decoration and `evaluated` could be deleted. +test fn an_established_verdict_that_refuses_is_what_separates_the_two_questions() -> Bool { + count( + filter( + every_verdict_shape, + v => emit_ratchet_verdict_evaluated(v: v) && !emit_ratchet_verdict_holds(v: v) + ) + ) == 2 + && count( + filter( + every_verdict_shape, + v => emit_ratchet_verdict_standing(v: v) == VerdictEstablishedAndRefused + ) + ) == 2 +} From 73429aa66ed3bab9f742dce57012c64d2ac2cecb Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 26 Aug 2026 15:45:15 +0000 Subject: [PATCH 6/7] Repair the merge: git factored a shared closing brace out of both conflict 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 (d31fa86382), 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) --- dag/gunbc/emit_subject_clean_frontier.dag | 2 ++ dag/test/claim/emit_subject_clean_frontier_witness_test.dag | 2 ++ 2 files changed, 4 insertions(+) diff --git a/dag/gunbc/emit_subject_clean_frontier.dag b/dag/gunbc/emit_subject_clean_frontier.dag index a6ad2439b3e..6e5005222c8 100644 --- a/dag/gunbc/emit_subject_clean_frontier.dag +++ b/dag/gunbc/emit_subject_clean_frontier.dag @@ -1431,6 +1431,8 @@ fn emit_ratchet_runner_execution_standing(cadence: WitnessConsumerCadence) -> Wi entry: emit_ratchet_runner_entry, function: emit_ratchet_runner_observe_function } + } +} // --------------------------------------------------------------------------------------------- // A MEASUREMENT OVER A SUBJECT WHOSE BOUNDARY DID NOT HOLD IS NOT A MEASUREMENT OF THAT SUBJECT. diff --git a/dag/test/claim/emit_subject_clean_frontier_witness_test.dag b/dag/test/claim/emit_subject_clean_frontier_witness_test.dag index 9c2ce291b43..31271fe5ec7 100644 --- a/dag/test/claim/emit_subject_clean_frontier_witness_test.dag +++ b/dag/test/claim/emit_subject_clean_frontier_witness_test.dag @@ -803,6 +803,8 @@ test fn an_established_verdict_that_refuses_is_what_separates_the_two_questions( v => emit_ratchet_verdict_standing(v: v) == VerdictEstablishedAndRefused ) ) == 2 +} + fn membership_with_candidates(candidates: List, closure: List) -> SubjectMembership { SubjectMembership { resolution_candidates: MembershipObserved { members: candidates }, From 619a532ac24308fb1e95352b39d71f1e171fbea3 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 26 Aug 2026 16:57:32 +0000 Subject: [PATCH 7/7] One silence, two owners: split a subject nobody asked about from one 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, 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) --- dag/gunbc/emit_subject_clean_frontier.dag | 65 ++++++++++++++++++- ...it_subject_clean_frontier_witness_test.dag | 62 +++++++++++++++++- dag/tools/emit_subject_clean_ratchet.dag | 28 +++++--- 3 files changed, 142 insertions(+), 13 deletions(-) diff --git a/dag/gunbc/emit_subject_clean_frontier.dag b/dag/gunbc/emit_subject_clean_frontier.dag index 6e5005222c8..bbc4c8036cb 100644 --- a/dag/gunbc/emit_subject_clean_frontier.dag +++ b/dag/gunbc/emit_subject_clean_frontier.dag @@ -802,6 +802,7 @@ type EmitRatchetVerdict | RatchetFrontierStale { entry: String } | RatchetNotEvaluated { entry: String, on_frontier: Bool, cause: EmitNotEvaluatedCause } | RatchetSubjectUnmeasured { entry: String, on_frontier: Bool } + | RatchetSubjectNotSelected { entry: String, on_frontier: Bool } fn emit_ratchet_verdict_entry(v: EmitRatchetVerdict) -> String { match v { @@ -811,6 +812,7 @@ fn emit_ratchet_verdict_entry(v: EmitRatchetVerdict) -> String { RatchetFrontierStale { entry: e } => e RatchetNotEvaluated { entry: e, on_frontier: _, cause: _ } => e RatchetSubjectUnmeasured { entry: e, on_frontier: _ } => e + RatchetSubjectNotSelected { entry: e, on_frontier: _ } => e } } @@ -850,6 +852,7 @@ fn emit_ratchet_verdict_standing(v: EmitRatchetVerdict) -> VerdictStanding { RatchetFrontierStale { entry: _ } => VerdictEstablishedAndRefused RatchetNotEvaluated { entry: _, on_frontier: _, cause: _ } => VerdictUnestablished RatchetSubjectUnmeasured { entry: _, on_frontier: _ } => VerdictUnestablished + RatchetSubjectNotSelected { entry: _, on_frontier: _ } => VerdictUnestablished } } @@ -891,7 +894,12 @@ fn emit_ratchet_verdict_row(v: EmitRatchetVerdict) -> String { RatchetSubjectUnmeasured { entry: e, on_frontier: f } => concat( concat(concat("UNMEASURED\t", e), concat("\ton_frontier\t", to_string(f))), - "\tthe fold was handed no measurement for this roster subject — a partial run cannot answer a closed-universe claim" + "\tthe instrument was asked about this subject and produced no reading for it — a deficit in the run, not its scope" + ) + RatchetSubjectNotSelected { entry: e, on_frontier: f } => + concat( + concat(concat("NOT-SELECTED\t", e), concat("\ton_frontier\t", to_string(f))), + "\tthis run measured a subset and never asked about this subject — scope rather than a deficit, and still not a verdict" ) } } @@ -952,9 +960,56 @@ fn lookup_subject_reading(readings: List, entry: String) -> ) } -fn emit_ratchet_verdict_for(entry: String, on_frontier: Bool, readings: List) -> EmitRatchetVerdict { +// --------------------------------------------------------------------------------------------- +// THE SELECTION, WHICH IS WHY "NO VERDICT" IS TWO FACTS AND NOT ONE. +// +// A roster subject can arrive at the fold with no reading for two reasons that share nothing but +// their silence. Either the run ASKED about it and the instrument produced nothing -- a deficit in +// the run -- or the run never asked, because `entries` named a subset. The owners are opposite: +// the first is an instrument to fix, the second is a run to widen, and a reader handed one +// UNMEASURED count cannot tell which they are 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, +// because the two have opposite owners. The selection axis is the same shape and did not get the +// same treatment, so it is given one here. +// +// THE CARRIER IS A COPRODUCT AND NOT A LIST, deliberately. A bare `List` would make the +// empty list mean both a subset naming nothing and no subsetting at all -- the state-space +// conflation this type exists to remove, reintroduced in the type that removes it. +type SubjectSelection + = SelectionWholeRoster + | SelectionSubset { entries: List } + +fn subject_was_selected(selection: SubjectSelection, entry: String) -> Bool { + match selection { + SelectionWholeRoster => true + SelectionSubset { entries: es } => string_list_contains(xs: es, wanted: entry) + } +} + +// The subjects an instrument should be invoked over, which is the SAME value the classification +// above reads. A caller deriving this list independently of the selection is how the two drift. +fn subject_selection_entries(selection: SubjectSelection, roster: List) -> List { + match selection { + SelectionWholeRoster => roster + SelectionSubset { entries: es } => es + } +} + +fn emit_ratchet_verdict_for( + entry: String, + on_frontier: Bool, + selection: SubjectSelection, + readings: List +) -> EmitRatchetVerdict { match lookup_subject_reading(readings: readings, entry: entry) { - SubjectReadingAbsent => RatchetSubjectUnmeasured { entry: entry, on_frontier: on_frontier } + SubjectReadingAbsent => + if subject_was_selected(selection: selection, entry: entry) { + RatchetSubjectUnmeasured { entry: entry, on_frontier: on_frontier } + } else { + RatchetSubjectNotSelected { entry: entry, on_frontier: on_frontier } + } SubjectReadingFound { reading: reading } => emit_ratchet_verdict_of_outcome( entry: entry, @@ -982,6 +1037,7 @@ type EmitSubjectCleanRatchet { fn fold_emit_subject_clean_ratchet_over_readings( universe: RatchetUniverse, admissions: List, + selection: SubjectSelection, readings: List ) -> EmitSubjectCleanRatchet { let keys = map(admissions, a => emit_debt_admission_entry(admission: a)) @@ -995,6 +1051,7 @@ fn fold_emit_subject_clean_ratchet_over_readings( emit_ratchet_verdict_for( entry: entry, on_frontier: string_list_contains(xs: keys, wanted: entry), + selection: selection, readings: all_readings ) ), @@ -1020,11 +1077,13 @@ fn fold_emit_subject_clean_ratchet_over_readings( fn fold_emit_subject_clean_ratchet( universe: RatchetUniverse, admissions: List, + selection: SubjectSelection, measurements: List ) -> EmitSubjectCleanRatchet { fold_emit_subject_clean_ratchet_over_readings( universe: universe, admissions: admissions, + selection: selection, readings: map(measurements, m => emit_subject_reading(m: m)) ) } diff --git a/dag/test/claim/emit_subject_clean_frontier_witness_test.dag b/dag/test/claim/emit_subject_clean_frontier_witness_test.dag index 31271fe5ec7..d75d3b012b6 100644 --- a/dag/test/claim/emit_subject_clean_frontier_witness_test.dag +++ b/dag/test/claim/emit_subject_clean_frontier_witness_test.dag @@ -57,6 +57,7 @@ fn fixture_fold_of( fold_emit_subject_clean_ratchet_over_readings( universe: IndexOnlyUniverse { policy: fixture_policy(), entries: roster }, admissions: admissions, + selection: SelectionWholeRoster, readings: readings ) } @@ -105,6 +106,7 @@ fn fixture_dual_fold( inventory: inventory }, admissions: [], + selection: SelectionWholeRoster, readings: readings ) } @@ -269,7 +271,7 @@ test fn a_partial_run_refuses_and_names_the_subjects_it_did_not_measure() -> Boo let readings = [fixture_reading(entry: fixture_alpha, outcome: EmitSubjectClean)] !fixture_standing_holds(roster: fixture_roster, admissions: [], readings: readings) && fixture_failing_rows(roster: fixture_roster, admissions: [], readings: readings) - == ["UNMEASURED\tdag/fixture/beta.dag\ton_frontier\tfalse\tthe fold was handed no measurement for this roster subject — a partial run cannot answer a closed-universe claim"] + == ["UNMEASURED\tdag/fixture/beta.dag\ton_frontier\tfalse\tthe instrument was asked about this subject and produced no reading for it — a deficit in the run, not its scope"] } // RED: an admission row naming a subject the discovered roster does not contain is a row to delete, @@ -451,6 +453,7 @@ test fn a_measurement_cannot_overwrite_an_unclassified_files_classification() -> inventory: [fixture_alpha, fixture_beta, hidden] }, admissions: [], + selection: SelectionWholeRoster, readings: concat(fixture_both_clean(), [fixture_reading(entry: hidden, outcome: EmitSubjectClean)]) ) count( @@ -495,6 +498,7 @@ fn fixture_empty_dual_fold() -> EmitSubjectCleanRatchet { fold_emit_subject_clean_ratchet_over_readings( universe: DualUniverse { policy: fixture_policy(), entries: [], inventory: [] }, admissions: [], + selection: SelectionWholeRoster, readings: [] ) } @@ -767,13 +771,67 @@ test fn the_ratchet_runner_has_no_executing_consumer_today() -> Bool { // by measuring them against each other, which is exactly how it came up in review. Routing both // through `emit_ratchet_verdict_standing` makes the divergence a named class, and this claim pins // the two properties that make the split load-bearing rather than decorative. + +// --------------------------------------------------------------------------------------------- +// THE SELECTION SPLIT: ONE SILENCE, TWO OWNERS. +// +// A roster subject with no reading used to render as UNMEASURED whether the run had asked about it +// or not. The two facts have opposite remedies -- fix the instrument, or widen the run -- so a +// reader handed one count could not tell which they were looking at. The pair below is the whole +// evidence for the split, and it is a ONE-FIELD control: the roster, the admissions and the +// readings are IDENTICAL across both claims and only the selection differs. A green that survived +// collapsing the two arms would therefore have to be an accident of the selection alone. +// --------------------------------------------------------------------------------------------- + +fn fixture_beta_verdict_under(selection: SubjectSelection) -> List { + filter( + fold_emit_subject_clean_ratchet_over_readings( + universe: IndexOnlyUniverse { policy: fixture_policy(), entries: fixture_roster }, + admissions: [], + selection: selection, + readings: [fixture_reading(entry: fixture_alpha, outcome: EmitSubjectClean)] + ).verdicts, + v => emit_ratchet_verdict_entry(v: v) == fixture_beta + ) +} + +// RED: a subject the run never asked about must not be reported as one the instrument failed on. +// If the classifier stops consulting the selection, this arm collapses into the one below. +test fn a_subject_the_run_never_selected_is_scope_rather_than_a_deficit() -> Bool { + fixture_beta_verdict_under(selection: SelectionSubset { entries: [fixture_alpha] }) + == [RatchetSubjectNotSelected { entry: fixture_beta, on_frontier: false }] +} + +// RED: the same silence, from a run that DID ask, is a deficit and keeps its old name. This is the +// control that makes the claim above discriminating rather than a rename. +test fn a_subject_the_run_selected_and_could_not_measure_is_still_a_deficit() -> Bool { + fixture_beta_verdict_under(selection: SelectionWholeRoster) + == [RatchetSubjectUnmeasured { entry: fixture_beta, on_frontier: false }] +} + +// NEITHER IS A VERDICT. The split names two owners; it does not promote scope into evidence, and a +// gate must still refuse over both. If the new arm were ever classified as established, a subset +// run would start answering a closed-universe question it never asked. +test fn neither_silence_establishes_a_verdict() -> Bool { + count( + filter( + [ + RatchetSubjectNotSelected { entry: fixture_beta, on_frontier: false }, + RatchetSubjectUnmeasured { entry: fixture_beta, on_frontier: false } + ], + v => emit_ratchet_verdict_evaluated(v: v) || emit_ratchet_verdict_holds(v: v) + ) + ) == 0 +} + data every_verdict_shape: List = [ RatchetCleanHeld { entry: fixture_alpha }, RatchetDebtHeld { entry: fixture_alpha, cause: BlockingDiagnostics { blocking: 1 } }, RatchetRegressed { entry: fixture_alpha, cause: BlockingDiagnostics { blocking: 1 } }, RatchetFrontierStale { entry: fixture_alpha }, RatchetNotEvaluated { entry: fixture_alpha, on_frontier: false, cause: ExtentUnestablished }, - RatchetSubjectUnmeasured { entry: fixture_alpha, on_frontier: false } + RatchetSubjectUnmeasured { entry: fixture_alpha, on_frontier: false }, + RatchetSubjectNotSelected { entry: fixture_alpha, on_frontier: false } ] // A HELD VERDICT IS ALWAYS AN EVALUATED ONE -- the ratchet cannot hold over a subject nobody diff --git a/dag/tools/emit_subject_clean_ratchet.dag b/dag/tools/emit_subject_clean_ratchet.dag index a9a74407854..a67235f5e65 100644 --- a/dag/tools/emit_subject_clean_ratchet.dag +++ b/dag/tools/emit_subject_clean_ratchet.dag @@ -31,6 +31,10 @@ import gunbc.emit_subject_clean_frontier { ObservationNotTaken, RosterDiscoveryPolicy, DeclarationIndexUnderRoots, + SubjectSelection, + SelectionWholeRoster, + SelectionSubset, + subject_selection_entries, emit_subject_clean_admissions, emit_ratchet_report_text, emit_ratchet_standing, @@ -138,15 +142,15 @@ fn module_inventory(roots: List) -> ModuleInventoryRead { ) } -fn selected_entries(entries: String, roster: List) -> List { +// An empty `entries` is WHOLE-ROSTER and not an empty subset. That is the one place the two could +// have been conflated, and the coproduct is what keeps them apart all the way to the report. +fn subject_selection(entries: String, roster: List) -> SubjectSelection { if entries == "" { - roster + SelectionWholeRoster } else { - fold( - split(s: entries, delimiter: ","), - init: [], - f: (acc, e) => if e == "" { acc } else { concat(acc, [e]) } - ) + SelectionSubset { + entries: filter(split(s: entries, delimiter: ","), e => e != "") + } } } @@ -154,11 +158,16 @@ fn measure_selected(selection: List) -> List { map(selection, entry => measure_entry_emission(entry: entry)) } +// ONE SELECTION, READ TWICE. The list the instrument is invoked over and the selection the fold +// classifies against are derived from the same value rather than computed twice from `entries` -- +// two derivations could disagree, and a disagreement here would render as an UNMEASURED subject +// the run had in fact measured, which is the precise confusion the selection carrier removes. fn run_emit_subject_clean_ratchet( entries: String, roster: List, inventory: List ) -> EmitSubjectCleanRatchet { + let selection = subject_selection(entries: entries, roster: roster) fold_emit_subject_clean_ratchet( universe: DualUniverse { policy: emit_subject_clean_roster_policy, @@ -166,7 +175,10 @@ fn run_emit_subject_clean_ratchet( inventory: inventory }, admissions: emit_subject_clean_admissions, - measurements: measure_selected(selection: selected_entries(entries: entries, roster: roster)) + selection: selection, + measurements: measure_selected( + selection: subject_selection_entries(selection: selection, roster: roster) + ) ) }