Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
27 commits
Select commit Hold shift + click to select a range
3dac9fb
File the class: a correct detector promoted to an actuator predicate
Sep 4, 2026
d695b3a
chore: regenerate drifted generated artifacts (ci auto-heal)
Sep 4, 2026
699fee8
Merge remote-tracking branch 'origin/main' into work/detector-promote…
Sep 4, 2026
db67cc6
chore: regenerate drifted generated artifacts (ci auto-heal)
Sep 4, 2026
5351302
Merge remote-tracking branch 'origin/main' into work/detector-promote…
Sep 4, 2026
1140a1d
Reclassify the reporting specimen as a neighbour, not an instance (re…
Sep 4, 2026
fb31798
chore: regenerate drifted generated artifacts (ci auto-heal)
Sep 4, 2026
ed700c9
Withdraw a syntactic ceiling justification and ground the trigger (re…
Sep 4, 2026
64a0490
Merge remote-tracking branch 'origin/main' into work/detector-promote…
Sep 4, 2026
0307a8c
chore: regenerate drifted generated artifacts (ci auto-heal)
Sep 4, 2026
047fa80
Require the permit's constructor to be EXCLUSIVE, not merely closed t…
Sep 4, 2026
27fba86
Merge remote-tracking branch 'origin/work/detector-promoted-to-actuat…
Sep 4, 2026
a9a1917
chore: regenerate drifted generated artifacts (ci auto-heal)
Sep 4, 2026
68535a8
Merge remote-tracking branch 'origin/main' into work/detector-promote…
Sep 4, 2026
e84a114
chore: regenerate drifted generated artifacts (ci auto-heal)
Sep 4, 2026
5aa4b1b
Merge remote-tracking branch 'origin/main' into work/detector-promote…
Sep 4, 2026
14b5912
chore: regenerate drifted generated artifacts (ci auto-heal)
Sep 4, 2026
9578e1e
Merge remote-tracking branch 'origin/main' into work/detector-promote…
Sep 4, 2026
6486b8f
chore: regenerate drifted generated artifacts (ci auto-heal)
Sep 4, 2026
b8c109e
Merge remote-tracking branch 'origin/main' into work/detector-promote…
Sep 5, 2026
3e1e4b2
chore: regenerate drifted generated artifacts (ci auto-heal)
Sep 5, 2026
fc35954
Merge remote-tracking branch 'origin/main' into work/detector-promote…
Sep 5, 2026
b9cd74a
chore: regenerate drifted generated artifacts (ci auto-heal)
Sep 5, 2026
f836879
Merge remote-tracking branch 'origin/main' into work/detector-promote…
Sep 5, 2026
66c8679
chore: regenerate drifted generated artifacts (ci auto-heal)
Sep 5, 2026
a0418d9
Merge main: ordered-union the authored roster, take base for the gene…
Sep 5, 2026
f368a74
chore: regenerate drifted generated artifacts (ci auto-heal)
Sep 5, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
module gunbc.recurring_failure_mode.detector_promoted_to_an_actuator_predicate

import std.types { NonEmptyStr }
import gunbc.recurring_failure_mode { RecurringFailureMode }

data detector_promoted_to_an_actuator_predicate: RecurringFailureMode = RecurringFailureMode {
identity: "detector_promoted_to_an_actuator_predicate" as NonEmptyStr,

receipts: [
"**a correct detector is wired to a side effect that is only valid on a subset of what it detects** (INVALID STATE: a predicate that TRULY and COMPLETELY describes a condition is promoted to select the population an ACTUATOR runs over, without the additional clause that separates the members needing the action from the members for which the same condition is the CORRECT and HEALTHY state. The detection is not wrong at any point. The promotion is. ",

"**WHAT MAKES IT DANGEROUS IS AN ASYMMETRY BETWEEN READING AND ACTING, and it is the whole reason the classes must be kept apart: OBSERVING a member the predicate correctly returns costs nothing, and ACTING on it can be destructive.** So a predicate can be perfectly validated as a description and still be unsafe as a trigger, and no amount of confirming the DESCRIPTION discovers it. ",

"**THE RECOGNITION RULE, and it is checkable in one question before any code changes: WAS THE PREDICATE VALIDATED AGAINST THE SPECIMEN THAT PROMPTED IT, OR AGAINST THE POPULATION IT WILL ACT ON?** These are different sets and the second is the only one that matters. The prompting specimen is by construction a member needing the action -- that is why it prompted -- so it can never expose the healthy majority. Nobody asks a detector what ELSE it returns, because it was built from the one thing it was supposed to return. ",

"**SPECIMEN WITH A RECEIPT, 2026-09-04, gunbc CI sweep, and both halves are mine.** A fleet sweep for parked workflow runs filtered on `status == completed AND conclusion == action_required`. A peer found a THIRD parked shape that filter could not reach -- `conclusion == cancelled` with an empty job list on a live head -- and correctly diagnosed the cause: the population was selected by a CONTAINER FIELD, so it admitted only the shape already seen. That is `population_selector_that_cannot_admit_a_counterexample`, committed inside the sweep whose author had relayed that row hours earlier. The proposed repair was to drop the conclusion predicate and filter on TERMINAL AND ZERO JOBS, which is a true and complete description of the parked state. ",

"**AND IT WOULD HAVE BEEN CATASTROPHIC AS A TRIGGER.** Run at member grain over the last 100 runs it returns TWENTY-ONE hits across ELEVEN branches, all `conclusion=cancelled` -- and roughly twenty are SUPERSEDED HEADS, cancelled before scheduling because the author pushed again. Zero jobs is exactly CORRECT for those: the run was killed as obsolete. The branch clustering shows the healthy population is the BULK and not an edge -- four runs on one branch, three on another, two on a third. Rerunning them would resurrect dead heads, register checks against commits nobody is trying to land, and spend runner capacity in a queue already measured at eighty-plus minutes deep. **n=1 CONFIRMING, n=20 REFUTING, AND THE TWENTY WERE NEVER QUERIED.** ",

"**THE MISSING CLAUSE IS LIVENESS, AND IT IS A DISCRIMINATOR RATHER THAN A HEURISTIC: `terminal AND zero jobs AND head_sha == the CURRENT head of an OPEN pull request`.** A superseded run fails the third clause BY CONSTRUCTION -- being superseded is precisely what made its head stale -- so the clause separates the two populations structurally rather than by threshold or confidence. Detect at member grain; GATE THE ACTUATOR ON LIVENESS; then branch on the conclusion only to choose the instrument, since `approve` releases an existing run and `rerun` starts a new attempt. ",

"**THE CONTROL THAT MADE THE CORRECTED SWEEP'S ZERO READABLE, recorded because the sweep returned zero and a zero is the value a broken join also returns.** After adding the liveness clause the sweep found no parked runs on live heads. That zero was checked by running the head-matcher against a KNOWN-LIVE head -- the author's own open PR -- and confirming it returned one. Without that control the result is indistinguishable from a join that matches nothing, which is `absent_reads_identically_to_never_looked`. ",

"**A NEIGHBOURING DEFECT, NOT THIS ONE, FOUND IN THE SAME HOUR AND RECORDED HERE ONLY TO SEPARATE THEM.** The sweep's author had been reporting `the fleet is clear` all night. That was true of the population the filter owned -- no runs AWAITING APPROVAL -- and was stated as the wider claim, no PARKED runs. A summary is a predicate too, and it inherits the narrowness of the query beneath it while its WORDS name the wider set. THIS ROW IS NOT ITS AUTHORITY: there is no actuator and no side effect in a status summary, so the distinguishing fact below -- detection and actuation having different admissible populations -- does not obtain, and filing it here would widen this class past its own boundary and fork an authority that already exists. It belongs to `green_reported_over_a_population_the_instrument_does_not_own`, whose subject is exactly an instrument reporting over a population it does not own. Recorded as a neighbour because the two were discovered together and a later reader tracing this specimen should be sent there rather than back here. ",

"**THE BOUNDARIES, since three roster rows sit adjacent and none covers this.** `population_selector_that_cannot_admit_a_counterexample`: there the QUERY IS WRONG and cannot return the negative; here the query is RIGHT and returns the whole population faithfully. `repair_enumerates_its_own_blast_radius_by_inspection`: there a COUNT of affected sites is stated with no decidable search behind it; here the search is decidable, executed, and correct, and the count is not in dispute. `guard_precondition_discharged_by_the_route_that_uses_it`: there a check stops discriminating because its precondition moved; here nothing has moved and the check discriminates exactly as designed. `green_reported_over_a_population_the_instrument_does_not_own`: there a REPORT names a wider population than the query beneath it owns, with no effect anywhere in it; here the report is not at issue and the defect is an EFFECT admitted on the wrong population. The distinguishing fact for this row is that DETECTION AND ACTUATION HAVE DIFFERENT ADMISSIBLE POPULATIONS and one predicate was used for both. ",

"**RUNG: 1 (mitigatable)** -- caught by asking the recognition question before wiring a predicate to an effect. ",

"**CEILING: 4 (structurally impossible), AND THE ROUTE TO IT IS NOT A STATIC SHAPE TEST.** An earlier draft of this row justified its ceiling by saying the property is decidable from the modeled call graph -- whether a predicate reaching an effectful operation carries a clause the pure-observation path does not. That justification is withdrawn: it is SYNTACTIC, and an arbitrary or irrelevant conjunct satisfies it while preserving the invalid state exactly. A check satisfiable by editing the declaration while the realization still lies is the validation-standing-where-construction-was-available tell of DESIGN section 5, so the shape test establishes no rung above 2. What it can honestly do is ENUMERATE CANDIDATES -- effect paths carrying no additional clause at all -- which is a useful lens and not a wall. ",

"**NEXT-RUNG TRIGGER, the capability and not an artifact, stated so that satisfying it entails the guarantee.** The actuator must DECLARE ITS ADMISSIBLE POPULATION as a predicate over the member, and the effect constructor must require a witness produced by EVALUATING THAT DECLARED PREDICATE on the member being acted on -- so that a detection result has no constructor into the effect at all, and the promotion fails to construct rather than being caught by a reviewer who thought to ask. EXCLUSIVITY IS THE WHOLE OF IT AND EXCLUDING THE DETECTION RESULT ALONE IS NOT ENOUGH: a successful evaluation must be the ONLY constructor of the permit, so that a caller-authored receipt, a bare member, or a true boolean cannot inhabit it either. A permit type carries no safety property of its own -- the property lives entirely in an exclusive constructor that proves the actuator's declared policy over the EXACT subject acted upon, and any additional constructor silently returns the class to rung 1 while the type name still reads as coverage. Both halves are load-bearing and a trigger naming only the second is the grain mismatch section 4b(3) names as its own review tell: a receipt type whose constructor does not require that evaluation is vacuously inhabitable, claims admissibility that no constructor entails, and leaves the class exactly where it was while reading as coverage. The receipt must be grounded in the actuator's own policy or it is decoration, and this trigger is retired by nothing less.",
],

evidence: [],
}
2 changes: 2 additions & 0 deletions dag/gunbc/recurring_failure_mode/roster.dag
Original file line number Diff line number Diff line change
Expand Up @@ -135,6 +135,7 @@ import gunbc.recurring_failure_mode.witness_that_fails_to_compile_is_absent_rath
import gunbc.recurring_failure_mode.instruction_and_subject_resolved_from_different_revisions { instruction_and_subject_resolved_from_different_revisions }
import gunbc.recurring_failure_mode.reported_required_refusal_does_not_precondition_landing { reported_required_refusal_does_not_precondition_landing }
import gunbc.recurring_failure_mode.corroboration_without_an_independent_derivation_axis { corroboration_without_an_independent_derivation_axis }
import gunbc.recurring_failure_mode.detector_promoted_to_an_actuator_predicate { detector_promoted_to_an_actuator_predicate }

data recurring_failure_mode_roster: List<RecurringFailureMode> = [
a_type_name_asserts_an_algebra_the_arithmetic_does_not_carry,
Expand Down Expand Up @@ -261,4 +262,5 @@ data recurring_failure_mode_roster: List<RecurringFailureMode> = [
instruction_and_subject_resolved_from_different_revisions,
reported_required_refusal_does_not_precondition_landing,
corroboration_without_an_independent_derivation_axis,
detector_promoted_to_an_actuator_predicate,
]
Loading
Loading