Repository navigation
fan_tach_health binds to std.goal_assessment, discharging the frontier that named it - #10926
Conversation
…rontier std.goal_assessment declared GoalAssessmentRefused a section 3c frontier whose trigger was a NAMED CONSUMER rather than a date: "product.fan_tach_health already computes exactly this fact -- FanTachRefused over DuplicateExpectedHeader, DuplicateObservedHeader and HostIdentityMismatch, each of them an ill-formed question set rather than an unhealthy fan -- and the arm is discharged when that module is bound to this algebra." This is that binding. The seven-arm FanTachVerdict splits into FanTachHealthy, FanTachDeviation and FanTachUnknown. That is not cosmetic: GoalDiverged carries FreeSemigroup<Deviation>, so handing it the undivided verdict would let a divergence list hold RotationObserved -- a healthy reading filed as a mismatch, which is the edit that algebra's own annotation says nothing in the type would stop. One FanTachJudgement fold keeps the per-header classification a single authority; the three extractors are projections of it, not second folds. ONE ARM CHANGES ANSWER RATHER THAN LABEL. An expected header the collector never answered for was a verdict beside the others, so a host carrying one still read as assessed. Nothing about that fan was established, so it is now an unknown and the host is indeterminate -- which assess_by_deviations_and_unknowns ranks above any proved deviation, for the reason that algebra states: remediating a subject whose state is partly unread is licensed by an answer nobody has. EVIDENCE, AND IT IS EXECUTED. dag/test/claim/fan_tach_assessment_witness_test.dag carries 8 witnesses, 4 of them controls that exist to keep the other 4 honest -- a satisfied host so the divergence is not vacuous, a fully-read host so the indeterminate arm is not universal, a well-formed question so the three refusals are not an assessment that refuses everything. Two mutations were run: missing observation reclassified as a deviation turns the omitted-window witness red with both controls green, and disabling the host-identity check turns the cross-host refusal red with both controls green. The refusal arm is therefore reachable on a real input, so the frontier is discharged by execution and not by assertion. The wet witness gains no new evidence here: fleet_fan_tach_expectation cannot be emitted (filter in branch condition, unprojectable), which reproduces byte-identical on clean main with this change stashed. The claim witness is the executing path. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PUtSkZTNvpWQv58Lk9cGzg
… module goes gunbc.fleet_fan_tach_health_witness was referenced by NOTHING -- absent from v2.workflow.local_repo_wet_terminal local_repo_wet_schedule (46 identities, none of them fan_tach), named by no lane, no roster and no CI step. A corpus grep returned only the file's own two self-references. Its claims had therefore never run on any merge path, which makes it the section 5 case that is worse than an absent witness: a file that reads as coverage while being permanently inert. WHAT NEARLY WENT WRONG. Discovering it could not be emitted, I was about to write a section 4b(3) declared rung drop for the lost wet evidence. That would have declared a regression against a baseline that never existed. Checking enrolment before writing the drop is what caught it -- no rung was held, so none was lost, and the real finding is older and worse than the one I set out to record. Deleting it outright would have discarded five claims the new claim witness did not cover: an intermittent zero is not a fault (the conjunct that makes the RATE load-bearing rather than decorative), an unwired endpoint is nominal rather than a missing rotation, a header outside the roster is an authority gap, srv3 and srv4 differ by identity rather than arity, and srv1's three healthy endpoints beside its two degraded ones. So this is the second half of a replacement migration: the claims move to where they execute, and only then does the inert module die -- rather than surviving as an attractor a later reader mistakes for a safety net (DESIGN section 3, delete-first, and its rule that the minimum Y must preserve every required refusal). They fold the judgements rather than the assessment, because "two degraded endpoints AND three healthy ones" is a statement about five headers and the algebra carries evidence on the satisfied arm alone. EXECUTED, NOT ASSERTED. 13 witnesses green. Mutating the judgement to key on any zero instead of the rate floor -- the exact defect the dropout control exists to prevent -- turns both rate-dependent claims red while the roster-identity claim stays green, so the mutation isolates rather than flattens. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PUtSkZTNvpWQv58Lk9cGzg
gunbai-bot
Bot
changed the title
…alse Review 63076, three findings, all confirmed against the code. GoalAssessmentRefused was constructed at three sites and absent from the import list. Both sibling bindings import it explicitly, so this was also a section 3 inconsistency. One correction to the finding's severity, which does not change the fix: it is an `unlisted import use` ADVISORY rather than an unresolved symbol, which is why 13 witnesses and the whole closure compiled over it. THE FRONTIER ROW IS RETIRED, and this is the finding worth the diff. The note in std.goal_assessment still read "AND IT HAS NO CONSTRUCTOR TODAY", still described the discharge as pending, and still cited FanTachRefused -- a symbol this PR deletes. So the PR body claimed the frontier was discharged while the carrier mark said otherwise and pointed at a dead name (section 4b(4): a climb retires the machinery it obsoletes; section 3: cite a symbol that resolves). Two things the old note had right are kept rather than lost with it: that repo_ruleset and the realization-selection witness reach the arm never, which is a property of THEIR SUBJECTS and not of the arm -- a parameter instantiated at Never is a binding declaring the arm unreachable for itself, which is the honest use of it -- and the section 5 reason the arm would deserve to exist with no consumer at all, because "the world differs" and "the question was malformed" have different owners. The rotating_floor annotation cited the wet witness as its reason for existing, in the same PR that deletes that witness. It now grounds the literal instead: srv2's healthy endpoints sit at 16-20 and srv1's bad ones at 4 and 9, so 12 is chosen inside the separating gap rather than measured off the current tree, and it lives with the caller because fan_tach_health takes the floor as a goal parameter -- a shared constant would be the fork that parameter prevents. BOTH OF THE LAST TWO ARE THE SAME DEFECT: an annotation asserting a state this same diff invalidated. It is the class this session briefed another lane about, found twice here, and did not catch by re-reading. 13 witnesses green; the four pre-existing suites unchanged at 12/6/6/18. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PUtSkZTNvpWQv58Lk9cGzg
|
Addressed review 63076 in 1. 2. The frontier row must be retired in the same diff — fixed, and this was the one worth the diff. The note still read "AND IT HAS NO CONSTRUCTOR TODAY", still described the discharge as pending, and still cited Two things the old note had right are kept rather than deleted along with it: that 3. Findings 2 and 3 are the same defect — an annotation asserting a state this same diff invalidated — which is the class I briefed another lane about this session and then committed twice here. CI is red for a reason outside this PR. The 17 parse errors are all in 13 witnesses green; four pre-existing suites unchanged at 12/6/6/18. — sent from sleek-newt-698 |
…ever read zero Review 63089, two findings. They turned out to be one defect, and fixing it one way fixes both. rotation_anomaly_count and expectation_drift_count were left dangling: their only consumer was the wet witness this PR deletes, and the replacement imported three of the five counters. Section 3c red, and pointedly so in a PR whose framing is that it retires inert code -- leaving two newly-inert functions behind is the same defect one level down. Separately the witness projected the closed FanTachJudgement sum onto ad-hoc string tags and counted them by equality. That re-minted counting the module already owns as typed folds (section 2), and -- the part that matters -- it made three assertions unfalsifiable: "no-rotation" was ONLY EVER asserted at zero, so any drift in the literal, or a rename of the arm behind it, left them permanently green. That is section 4b's decoration rather than a wall, and it is the same class this PR's own controls were written to avoid. So the tags are deleted and every count goes through the module's folds, which makes a renamed arm a compile error rather than a silent pass. The two orphans are consumed rather than deleted, because they were exactly the tools the string comparisons were standing in for. All seven judgement arms now have one typed counter in one authority; the two healthy arms gained theirs here. FOUR NEW CONJUNCTS PIN WHAT ONLY READ ZERO. A rotor read twenty times that never turned, an expected header whose sensor published nothing -- the same verdict arm reached by the other absence, so a migration collapsing the two causes is visible here rather than in a postmortem -- a not-expected header spinning anyway, and the matching zero on the unmodified fleet so the drift control proves more than that the counter can reach one. The live fleet exhibits none of these, which is precisely why the old assertions could not be falsified; the fixtures REPLACE a window rather than adding one, so the roster and denominator stay as declared and only the reading is under test. 17 witnesses green. Two further mutations, each predicted-red with green controls: collapsing an unpublished expected header into correctly-absent reds the publishing-nothing conjunct while the stopped-rotor one stays green, so the two absences are independently pinned; disabling UnexpectedRotation reds the drift conjunct alone. Five mutation cycles now stand behind this PR. No counter is dangling: consumers 6/6/3/3/3/2/2 across the seven. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PUtSkZTNvpWQv58Lk9cGzg
|
Addressed review 63089 in Finding 1 — two counters left dangling. Confirmed: Finding 2 — string tags over a closed sum. Also confirmed, and this is the one that mattered. The fix is one change. All string tags are deleted; every count now goes through the module's typed folds, so a renamed arm is a compile error rather than a silent pass. The two orphans are consumed rather than deleted, because they were exactly the tools the string comparisons were standing in for. All seven judgement arms now have one typed counter in one authority (the two healthy arms gained theirs here). Four new conjuncts pin what previously only read zero: a rotor read twenty times that never turned; an expected header whose sensor published nothing — the same verdict arm reached by the other absence, so a migration collapsing the two causes shows up here rather than in a postmortem; a not-expected header spinning anyway; and the matching zero on the unmodified fleet, so the drift control proves more than that the counter can reach one. The live fleet exhibits none of these conditions, which is exactly why the old assertions couldn't be falsified. The fixtures replace a window rather than adding one, so the roster and denominator stay as the fleet declares them and only the reading is under test. Evidence: 17 witnesses green. Two further mutations, each predicted-red with green controls — collapsing an unpublished expected header into correctly-absent reds the publishing-nothing conjunct while the stopped-rotor one stays green (so the two absences are independently pinned); disabling CI remains red for a cause outside this PR. All 17 parse errors are in — sent from sleek-newt-698 |
… its own evidence Review 63108, two findings, both confirmed. FanTachSubject packed a `host` beside expectation.host with nothing constraining them to agree, while the note on that very declaration claimed invalid assembly was unwritable. It was not: a mismatched pair was constructible, inspect_fan_tach labelled the receipt from the subject's copy and assess_fan_tach joined windows against the expectation's, so an inspection could be filed under a host that was never assessed. The field is deleted and the inspection subject derived from expectation.host -- one fact in one place (section 3), by construction rather than an equality check bolted on afterwards (section 4b). The fail-open control dropped FAN4 and asserted one degradation survived. FAN4 is one of srv1's TWO degraded endpoints -- 9 rotations in 20 beside FAN5's 4 -- so the arithmetic was right and established nothing the annotation claimed: it could not tell "the deviations survive the unknown" from "one of them was the header I removed". It now omits FAN1, which is healthy at 20 of 20, and asserts both degradations survive. THE PATTERN IS THE FINDING. This is the third annotation in this PR to assert a state the code does not hold -- after one citing FanTachRefused past its deletion and one citing the wet witness past its deletion. All three are prose written to describe an intention and never re-read against what the code ended up doing. Review is catching them; the author is not. Seven mutation cycles now stand behind this PR, and the seventh exists because the sixth was wrong. Emptying deviations at the call site reds the omitted-window conjunct AND the divergence conjunct, because with no deviations and no unknowns srv1 falls through to GoalSatisfied -- too broad to isolate the claim, and reported as a confirmation it would have been the same overclaim as the three above. Emptying known_deviations inside GoalIndeterminate alone reds the target with both controls green, which is the evidence the annotation actually needs. 59 witnesses green: 17 fan-tach, and 12/6/6/18 across the pre-existing suites, re-run because the narrow mutation touched std.goal_assessment, an authority five bindings share. Both mutated files restored byte-identical. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PUtSkZTNvpWQv58Lk9cGzg
|
Addressed review 63108 in Finding 2 — Finding 1 — the fail-open control overclaims. Also right. srv1/FAN4 is The pattern is worth naming. This is the third annotation in this PR to assert a state the code doesn't hold, after one citing On the evidence, including a correction. Seven mutation cycles now stand behind this PR, and the seventh exists because the sixth was wrong. Emptying 59 witnesses green: 17 fan-tach plus 12/6/6/18 across the pre-existing suites, re-run because the narrow mutation touched CI is red for a cause outside this PR, and I have verified it by filename rather than by inference. Extracting the parse failures from run — sent from sleek-newt-698 |
…8-observed-collision
1 participant
Finishes the convergence consolidation:
product.fan_tach_healthwas the lastmodule computing an observe/assess judgement with its own hand-rolled vocabulary
instead of
std.goal_assessment.Why this module, and why now
This is not a migration I picked the shape of.
std.goal_assessmentalreadydeclared
GoalAssessmentRefuseda §3c declared frontier and named itstrigger as a consumer rather than a date:
This is that binding. The frontier is now discharged, and discharged by
execution: three witnesses reach
GoalAssessmentRefusedon real fleet inputs,and disabling the host-identity check turns one of them red.
The type split is not cosmetic
GoalDivergedcarriesFreeSemigroup<Deviation>. Handing that parameter theundivided seven-arm
FanTachVerdictwould let a divergence list holdRotationObserved-- a healthy reading filed as a mismatch, which is exactly theedit that algebra's own annotation says nothing in the type would stop. So the
verdict splits into
FanTachHealthy/FanTachDeviation/FanTachUnknown,with one
FanTachJudgementfold keeping the per-header classification a singleauthority and three projections off it (§4b: construction over validation).
One arm changes the answer, not the label
An expected header the collector never answered for used to be a verdict beside
the others, so a host carrying one still read as assessed. Nothing about that
fan was established, so it is now an unknown and the host is indeterminate --
which
assess_by_deviations_and_unknownsranks above any proved deviation, forthe reason that algebra states: remediating a subject whose state is partly unread
is licensed by an answer nobody has.
This is the only behavioural change in the PR, and it is the one the witnesses
work hardest on.
A witness that had never run
While verifying,
gunbc.fleet_fan_tach_health_witnessturned out to bereferenced by nothing -- absent from
local_repo_wet_schedule(46identities, none of them fan_tach), named by no lane, roster or CI step, with a
corpus grep returning only its own two self-references. Its claims had never
executed on any merge path.
What nearly went wrong: on finding it could not be emitted, I was about to
write a §4b(3) declared rung drop for the lost wet evidence. That would have
declared a regression against a baseline that never existed. Checking enrolment
before writing the drop is what caught it.
Deleting it outright would have discarded five claims the new witness did not
cover -- among them "an intermittent zero is not a fault", the conjunct that makes
the rotation rate load-bearing rather than decorative. So the claims moved to
where they execute first, and only then did the inert module die (§3 delete-first,
and its rule that the minimum Y preserves every required refusal).
Evidence
13 witnesses in
dag/test/claim/fan_tach_assessment_witness_test.dag, five ofwhich exist to keep the others honest: a satisfied host so the divergence is not
vacuous, a fully-read host so the indeterminate arm is not universal, a
well-formed question so the three refusals are not an assessment that refuses
everything, and a roster-identity claim untouched by rate logic.
Three mutation cycles, each predicted-red with green controls:
an_omitted_window_is_an_unknown_not_an_assessed_hostone_host_expectation_against_another_hosts_windows_refuses42 pre-existing witnesses (fabric switch 12, cable plant 6, goal assessment 6,
realization selection 18) unchanged. Namespace wave
ADMITTED, 2 deltas, bothauto-admitted, no admission rows required.
Stated plainly, because it bears on how this PR was scoped
I opened this branch to fix a four-way
Observednaming fork, having claimed itbroke the
repo_rulesetclosure and blocked its verification. That claim wasfalse.
repo_rulesettype-checks clean -- frontend, normalize, reconcile andanalyses all pass, with zero occurrences of
Observedin the output, and it doesnot import any of the colliding modules. It refuses at emit, for an unrelated
modelled reason (
shelltransport has no rust realization forgunbc.WitnessBin.Run). I have retracted the claim and briefed the cleanup lanenot to repeat it; the
Observedde-fork landed separately on its §3 merits in#10915.
fleet_fan_tach_expectationlikewise refuses at emit (filterin branchcondition, unprojectable). Verified pre-existing: byte-identical diagnostic on
clean
mainwith this change stashed. That is why the executing evidence here isa claim witness (interpreted) rather than the wet path.
Follow-up worth its own lane
If one witness module could sit unenrolled and unnoticed since it was written,
the open question is how many others do -- an unrun witness is indistinguishable
from a passing one from the outside. A census of witness modules against the
schedules that actually run them is a lens-shaped question, and it is the
difference between "we found one" and "we know the number."
🤖 Generated with Claude Code
https://claude.ai/code/session_01PUtSkZTNvpWQv58Lk9cGzg