Repository navigation
ALERT-4: the falsifier alert's decision as a pure function over sixteen terminal arms - #7935
Conversation
…n terminal arms Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…t only the PR Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ent state Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Fixed in The part worth more than the fix. The claim in the review that this "will not typecheck" is the reasonable expectation, and it is not what happened — that is the finding. The broken signature typechecked clean and all 18 witnesses passed, both before and after the correction, with an identical So my evidence did not catch this and could not have. Every witness in the suite exercises behavior, and the behavior was right the whole time; what was wrong was a declared type that no consumer checked. This is a below-floor gap in the sense DESIGN §4b names — "values inhabit declared types" is the ordinary compiler floor, and a diff that lands a declaration the substrate does not enforce is not compensated by the higher-order properties above it. I am not fixing that here; it is well outside this PR. But recording it plainly matters more than the one-line correction, because the natural reading of "18/18 green" is that the module typechecks in the sense a reader assumes, and on this seam it does not. Review found it by reading. That is the internal/external division DESIGN names — my witnesses find missing behavior, a reader finds missing checks — and it landed on exactly the class where execution evidence is blind. — sent from calm-fox-748 |
…riven witnesses Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Acted on the non-blocking remark in review 49651, because the charitable reading in it does not hold. Landed in The review read the overlap between Deleted, with the §4b(4) distinction observed: the redundant production machinery goes, the evidence does not. Its six payload-driven witnesses carried coverage the ALERT-4 suite genuinely lacked — they reach the arms through One of the six failed on the move, and the failure was worth keeping. Written as "an empty payload opens a first red", it red: an empty string is not valid JSON, so it decodes to I kept it as a claim rather than a corrected mistake because the tempting repair is on the wrong side. Mapping an empty payload to review 49654 raised nothing actionable; no change owed there. — sent from calm-fox-748 |
…production caller may use them Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
review 49672 raised nothing blocking, but its reasoning about the The review is right that That is the entire justification, and nothing held it. One future call site — an effect plan branching on The note states it as a convention and says so plainly, because nothing in the substrate distinguishes a witness caller from a production one today. It names the check that would catch a violation: if the effect plan ever imports this module, the import list is where to look. Not a wall, and not described as one. — sent from calm-fox-748 |
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
review 49673 (REQUEST_CHANGES on Deleting the forked throttle left eleven import-only symbols in Both suites re-run after the removal: decision 24/24, migration 46/46, PASS-counted against roster. If review 49673 was pointing at something else, I would like to see it — the artifact link in the tally is the only reference I have and it does not resolve from here. Happy to act on it once the body lands. Worth flagging that neither the dead imports nor the earlier signature defect (review 49641) produced any compiler complaint. That is the same gap I recorded on this PR: the substrate is not checking these declarations, so unused-import and parameter-type errors both pass silently and review is currently the only thing catching them. — sent from calm-fox-748 |
- component index is a Nat read by a strict numeric decoder, not text - outcome and failure_mode carry the existing typed authorities, unmodelled wire refuses - unsuccessful rows identity-join the complete population in both directions - component_count requires a number; the event numeric decoder names its two consumers Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ns policy - issue observation un-fused from the state marker (duplicate/never-closed) - notifications carry a handle; undeclared escalation refuses - incident identity is a sorted typed set, label-free, read back structurally - every writing arm carries its complete next state - routings exact-join the failing set by index - non-success conclusions no longer read as a green corpus Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Operator verdict addressed — all five corrections plus the conclusions ruling, in P0-1 — issue observation un-fused from the state marker. P0-2 — the mention is now structural, and you were right that it was not. The old independence claim asserted that such a notification carried no mention — it passed, and it was measuring the wrong thing. It now asserts the refusal. P0-3 — identity is a typed sorted set. P0-4 — every writing arm carries its complete next state, with the policy stated once. First red sets both clocks to now; heartbeat preserves P1-5 — routings exact-join the failing set by index, the same identity the signature is keyed on. Missing, surplus and duplicate each refuse with the offending indices named. Accept-and-join rather than deriving inside the decision, so the lane roster does not get a second copy inside the alert. Conclusions policy. Not in this PR, per your sequencing: the — sent from calm-fox-748 |
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
review 49807 is right — fixed in Cause was mine and worth naming since it is a pattern rather than a slip: I added the new symbols by appending fresh import blocks while satisfying unresolved-type errors one at a time, and the compiler accepted the duplicates, so nothing pushed back. That is the third time on this stack that a declaration-level rule turned out to be unenforced — after the Suite re-run after the change: 44/44, PASS-counted against roster. — sent from calm-fox-748 |
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
review 49830 found no defect, but its parenthetical — "11-arm (actually 15, counting all refuse arms)" — was a real catch about my prose, so I checked it. Fixed in Counted against the live coproduct: sixteen arms, eight of them refusals. Two of my own notes were stale:
Both corrected against the coproduct rather than from memory, and I kept the incident in the note rather than silently renumbering, because this is the same class three times on this stack — a name-level claim sitting false beside a mechanism that stayed correct. The previous two were caught by reviewers (the The specific hazard is worth stating: a count in prose decays every time the coproduct grows, silently, without anyone touching the sentence. It is DESIGN's positional-citation problem in a different coordinate — a claim about the shape of something the containment tree already knows exactly. The durable fix is not to write counts at all, and where the count IS the point (as it is here — "eight different investigations" is the argument for not collapsing them), it needs re-checking whenever the arms move. Suite re-run: 44/44, PASS-counted. — sent from calm-fox-748 |
…ut, strict natural decode Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…tanding, complete writing instructions - FirstRedStanding on the marker; an adopted issue no longer fabricates first_red = now - observer-unavailable decided before a receipt is required (a timed-out run has none) - OpenObserverIncident / RefreshObserverIncident carry issue, next state and throttle - NotifyAlertControllerUnavailable reports trusted internal failures instead of silence - review 49873: marker index readback goes through strict_natural_of_lexeme Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Operator live-head items 1–4 plus review 49873, in 3 — observer-unavailable now runs BEFORE the receipt is required. This was the sharpest of the four. A run that timed out or failed at startup produced no receipt — that is what those conclusions mean — so demanding a decoded, subject-matched receipt first sent every one of them to 2 — an adopted issue no longer claims to know when the incident started. That change surfaced a smaller one worth naming. My first version detected the null by string-matching the number reader's diagnostic prose, which would have made a marker's meaning depend on the wording of an error message — reading state out of prose, which is exactly the practice this module deleted when it dropped the 4 — the observer arms are complete writing instructions, split into 4 — trusted internal failures now notify. review 49873 / item 1 (partial) — the marker index readback now goes through Also still open by sequence: #7928 item A (gaining PR body updated separately — it still described the eleven-arm shape. — sent from calm-fox-748 |
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
review 49908 found a real single-authority defect I introduced. Fixed in I declared Worth naming rather than fixing quietly: this is the §3 fork on the very carrier Cause was the same one as the duplicate imports earlier on this stack: I added the type where I needed it while satisfying an unresolved-name error, and nothing pushed back. That is now four declaration-level defects on this stack caught by readers and none by execution — parameter type, bare cross-module references, duplicate imports, and now a duplicate type declaration. All four had correct behaviour and a wrong declaration, which is precisely the class witnesses cannot see. Suite re-run: 52/52, PASS-counted. PR body and title also updated — they still described the eleven-arm shape from before the operator verdict; it is sixteen arms, eight refusals. — sent from calm-fox-748 |
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
review 49927 is correct. Fixed in The reviewer's reasoning about why it matters is the right one and worth restating: the whole point of The prediction that "the module will not typecheck" is again the part worth reporting. It did. That is the fifth declaration-level defect on this stack found by a reader and the fifth not caught by execution: parameter type (review 49641), bare cross-module references (review 49774), duplicate imports (review 49807), duplicate type declaration (review 49908), and now a field type. Every one had correct behaviour and a wrong declaration. I am not treating the passing suite as evidence about declarations any more, and I have said as much rather than quietly re-running it. One note on process: the first re-run after this change reported 0/52, which was — sent from calm-fox-748 |
…es match it Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
review 49947 is right on all four findings, and they are one defect. Fixed in The defect: two representations of one failure. When the operator verdict moved controller failures from silent refusals to All six are deleted. One case moved as part of collapsing rather than being mechanically renamed: an unparseable stored signature was still returning the silent The two stale notes are the same failure in prose, and both are corrected. I kept the incidents in both notes rather than silently rewriting. This is now six declaration-or-prose defects on this stack caught by readers: five declaration-level and this pair of stale authority paragraphs. The pattern is consistent — behaviour correct, description wrong — and prose is the half no witness can ever check. Suite re-run: 52/52, PASS-counted. — sent from calm-fox-748 |
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
review 49971 is correct on both. Fixed in This one was a verification gap, not just an oversight, and that is the part worth reporting. When It would have redded loudly rather than silently: the interpreter's cross-representation equality guard raises on exactly this comparison, which is how the same class surfaced elsewhere on this branch. So this is a case where the substrate does catch the defect at runtime — unlike the six declaration-level ones — and my process simply never put the two together in one place. Migration suite on this branch after the fix: 65/65. Decision suite: 52/52. Both PASS-counted against roster. One thing I checked rather than assumed while doing it: the migration roster is 65 here against 71 on the base, and I did not take that on faith. The six absent claims are exactly the payload-driven ones moved onto — sent from calm-fox-748 |
|
Recording a merge conflict, not resolving it — the head stays where the two approvals are until the operator decides to spend the round. State. #7928 merged as squash
Measured read-only with This refutes the prediction the retarget was priced on. The plan held that retargeting after #7928 merged would need no rebase, the base change alone collapsing the diff. That is true for a fast-forward base and false for a squash-merged one. One round was the right call; "no conflict resolution in it" was not. Why I am not pushing. Both approvals sit on Resolution recipe when it is authorized (merge commit, not rebase, per repo merge policy): The witness file needs care specifically. Its diff against main is |
…alert4 # Conflicts: # dag/gunbc/falsifier_alert_state.dag # dag/test/claim/falsifier_alert_migration_witness_test.dag
…k refused Run 31219557841's regen job refused on the pre-plan witness naming walk: red_receipt_other_class is a plain fn in a *_test.dag unreachable from every test fn, which is silent de-enrollment. Deleted rather than promoted. It has zero call sites, and the changed-signature claim it looks like it should carry is already covered on the correct side -- the receipt stays red_receipt (the current run) while the STORED STATE's signature varies via signature_of_fixture(component: other_failing_component). Varying the receipt would exercise the wrong half of the comparison. So this is a dead scaffold, not a missing witness. Worth naming because a local run cannot find this class: claim_batch executes the roster handed to it, built by grepping `test fn`, so a plain fn no test reaches is outside that denominator by construction. The suite reported 52/52 before and after -- true both times, and silent on exactly the thing that failed to enroll. Decision suite 52/52 after the deletion, PASS-counted against roster. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…red path alert_decision_observer_unavailable's IncidentCurrent arm returned RefreshObserverIncident unconditionally -- it never compared the heartbeat window, and never compared the stored signature either. On the four-hourly falsifier cadence a permanently timed-out observer therefore paged every four hours, which is the notification spam this module exists to end. Two notes a few lines apart asserted the guard existed. The code was wrong and the prose was right, which is the worse orientation: an auditor reading the policy would have found it documented, coherent and untrue. The witness was holding it in place. a_repeated_observer_outage_refreshes_the_ same_incident asked the repeat case at last=5000 now=6000 -- a one-second gap inside a twenty-hour window -- and asserted RefreshObserverIncident, pinning the spam as the contract. That is why 52/52 was green over it, and why the correct fix would have read as a regression. New RefreshObserverIncidentWithoutNotification arm; the observer path now mirrors the red path. The two notifying cases share one arm because they produce the same effect -- the red path splits its two only because their MESSAGES differ, a distinction in what gets said rather than whether to say it. The suppressed arm carries last_notification_at UNCHANGED. Advancing it to now looks right (the run did just observe the incident) but restarts the window every cadence, so the elapsed comparison can never fire and the heartbeat goes silent permanently -- converting a spam defect into a strictly worse silence defect that nothing observes. The field records when we last SPOKE, never when we last LOOKED. Adding the arm broke alert_decision_notifies and alert_decision_notification as non-exhaustive, so the closed coproduct made it structurally impossible to add a suppressing arm while leaving a predicate claiming it notifies. Roster 52 -> 55, 55/55 PASS-counted. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… main (#8035) * WIP: Stop-line: separate direct_rust expected-red standing from long-lane exe * WIP: Stop-line: separate direct_rust expected-red standing from long-lane exe * Separate expected-red standing from execution budget: three independent witness axes Cadence, eval budget and expected verdict were carried on one axis (WitnessConsumerCadence), so a witness that is both expensive and known-red was inexpressible. The eval ceiling was armed only for a batch whose entries intersected the long-lane batch roster, so such a root earned its budget by ALSO joining that batch: two schedule occurrences, the second on a batch that expects green, which paged the operator once per heartbeat window for a witness that is red BY DESIGN (#7737). Expectation itself was batch-wide and matched on entry PATHS, so file placement and batch homogeneity decided polarity. std.witness_admission gains WitnessExecutionBudget and WitnessExpectedVerdict as independent axes; ExplicitWitnessAdmission carries all three per row, and explicit_witness_admission_is_known_red now reads the EXPECTATION rather than the cadence. The scheduler ceiling reads witness_long_eval_budget_entries — the union of the long-lane batch roster and rows declaring their own long budget — so batch membership no longer confers time. The direct_rust duplicate long-lane row deletes; its paired schedule-multiplicity admission deletes with it, its dissolve_on having fired. claim_executor matches every executed witness against its own row: still-red is agreement, unexpected green is a typed StaleKnownRedRefusal naming the rows to un-quarantine. The refusal is derived from roster membership joined against per-witness outcomes and carried as data, so it reaches the component receipt as its own StaleKnownRed mode (-> Refused) instead of falling through the substring classifier's WitnessRed arm, where an un-quarantine and a regression would share one alert signature with opposite remedies. The batch-wide predicate survives only for a corpus resolve refuse, which has no per-witness outcomes, and only in its narrow all-entries form. * WIP: Stop-line: separate direct_rust expected-red standing from long-lane exe * Delete the path-grain hermetic known-red field, and refuse an unaccounted failure Function-grain expectation replaced hermetic_known_red_entry_paths outright, so it is deleted rather than left beside its successor (-D dead_code caught it as the CI build error). The wet twin survives because it still scopes a WALL budget, a different fact from polarity. The still-red arm now passes only when every failure in the summary is matched by an agreement, instead of reading an empty unexpected-failure list as 'nothing failed'. Outcomes and failures are pushed in lockstep today so the counts agree; if one ever arrives without a per-witness identity the arm refuses rather than narrowing an unmatchable failure into a pass. * Receipt-layer witness: StaleKnownRed is a refusal, not a WitnessRed and not Done Both directions asserted. It must not collapse into WitnessRed (an un-quarantine and a regression would share one alert class signature with opposite remedies), and it must not read as success (an expected-red row that silently went green would accumulate on a roster nobody revisits — the fail-open this mode closes). Also fixes the two fixture helpers in the admission witness that still called known_red_probe without the now-required budget. * Name the lane-granularity consequence of the budget union One declared-long row raises the ceiling for every row in the batch carrying it, so the known-red probe batch now runs at the long ceiling. That is the pre-existing lane granularity rather than a new grain, and it narrows to per-row on the cost-envelope trigger already declared beside it — stated here rather than left for a reader to discover. * Agreement means the assertion RAN and was false; the budget roster is an identity set TWO DEFECTS FOUND IN REVIEW, both mine. (1) The classifier computed green = (outcome == Pass) and routed EVERY other outcome into the expected-red agreement arm. That blessed a budget kill, an interpreter fault, a non-Bool return and an unobserved row as though the business assertion had executed and returned false — the empty-observation conflation, in the one place that decides whether a red is real. It also contradicted a recorded ruling outright: BudgetExceeded is an interruption plus a measured lower bound on cost, never a semantic verdict on a witness, so a known-red witness that timed out reported its quarantine intact while its behaviour was unobserved. ExpectedRedDisposition now gives each outcome its own row. Only Fail is agreement. Pass is the stale quarantine. TimedOut is a budget failure and RuntimeError/NotBool an infrastructure-or-referent failure — both red the batch instead of being blessed. A rostered expected-red witness with no observation is EvidenceAbsent: counted and named on every path, never agreement and never a failure, because absent evidence is not a verdict. Refusal-before-evaluation shares the infrastructure arm today because run_claim formats the typed InterpError to a String before ClaimOutcome is built; that is declared on the variant with its trigger, not recovered by sniffing prose. (2) The ceiling roster concatenated its two inputs, so a witness reaching it through both would be listed twice. It is now an identity set joined on schedule_witness_entry_eq. The dedup control is worth naming, because the first one was a tautology: it read the live union, and the live inputs are disjoint, so deleting the membership check left it green — measured, not assumed. The fold is now exposed as witness_long_eval_budget_union_in and the control drives it with a planted overlap, which reds the moment the join stops using identity. * ALERT-3.5: strict input boundary before the decision algebra consumes it * Point the refused/fault collapse at the existing seam note, not a second ledger entry The collapse dissolves on the SAME trigger gunbc.witness_row_cost witness_cost_timed_out_seed_deferral_note already carries, because it is the same fact: the typed InterpError does not survive the marshalling of ClaimOutcome across the interpreter boundary. Realizing witness execution from .dag puts the typed error in hand at the point of judgement and splits the arm. One fact, one home — a new ledger entry for one cause is the parallel-ledger failure. Also promotes this PR's own tautology finding to a named tell in the body: a control that reads a live population can be vacuous whenever that population does not exhibit the property, and will stay green untouched. Found by mutation, not by reading. * review 49571: split the component-summary decoder so only index admits a number * review 49594: emit selection_degradation on every path so encode/decode round-trips * ALERT-4: the falsifier alert's decision as a pure function over eleven terminal arms Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * carry the guard-order divergence reasoning in the witness carrier, not only the PR Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * review 49641: alert_decision takes the decoding, not the peeled incident state Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * review 49651: delete the forked throttle decision, keep its payload-driven witnesses Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * review 49672: name the Bool helpers as a witness surface, and why no production caller may use them Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * drop import-only symbols left behind by the consolidation Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * operator verdict on #7928: type the decision-grain boundary - component index is a Nat read by a strict numeric decoder, not text - outcome and failure_mode carry the existing typed authorities, unmodelled wire refuses - unsuccessful rows identity-join the complete population in both directions - component_count requires a number; the event numeric decoder names its two consumers Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * review 49774: import the symbols the new claims call Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * operator verdict on #7935: the four missing facts, plus the conclusions policy - issue observation un-fused from the state marker (duplicate/never-closed) - notifications carry a handle; undeclared escalation refuses - incident identity is a sorted typed set, label-free, read back structurally - every writing arm carries its complete next state - routings exact-join the failing set by index - non-success conclusions no longer read as a green corpus Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * review 49807: fold the duplicated import blocks Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * correct the arm counts in prose against the live coproduct Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * operator live-head B and C: validate the outcome/mode pair, read output, strict natural decode Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * operator live-head 1-4 on #7935: observer-before-receipt, first-red standing, complete writing instructions - FirstRedStanding on the marker; an adopted issue no longer fabricates first_red = now - observer-unavailable decided before a receipt is required (a timed-out run has none) - OpenObserverIncident / RefreshObserverIncident carry issue, next state and throttle - NotifyAlertControllerUnavailable reports trusted internal failures instead of silence - review 49873: marker index readback goes through strict_natural_of_lexeme Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * CI: write out the wildcard arms the non-fold-residue lens counts Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * review 49908: FirstRedStanding has one authority, in the state module Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * review 49927: IncidentLegacy carries the standing, not a bare instant Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * review 49947: one representation for controller failures, and the notes match it Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * review 49971: the migration witness reads first_red as a standing Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Separate the known-red axes: two budget-homogeneous batches, and three fail-closed repairs Recut per operator ruling: the known-red lane carries two DERIVED budget-homogeneous discovery runnables instead of one mixed batch joined into the long lane for budget. Eval ceilings are per batch, so a mixed batch widened every sibling's budget; both populations are now derived from the admission authority by declared budget (known_red_probe_corpus_fast_budget_roster / known_red_probe_corpus_long_budget_roster), never a hard-coded singleton for direct_rust. Component indices are unchanged: components are per LANE, and LaneGates already carries a multi-runnable batch. FIX 1 - absent evidence is a COVERAGE REFUSAL, not a log line. ExpectationRefusal::ExpectedRedEvidenceAbsent refuses the batch on its own receipt mode (ModeExpectedRedEvidenceAbsent), so a rostered expected-red witness that stops executing can no longer pass admission. It stays out of hard_failures deliberately - it is a coverage fact, not a semantic verdict, and mixing it into the verdict population would corrupt the identity join. FIX 2 - a pre-verdict refusal needs its own DECLARED expectation. WitnessExpectedVerdict splits into ExpectWitnessHolds | ExpectAssertionFalse | ExpectTypedPreVerdictRefusal{phase, cause}. Only rows on known_red_pre_verdict_refusal_roster may admit a resolve-phase refusal, and the check is exact-entry-grained membership - no message sniffing. The observed cause is not yet matched against the declared one because run_claim formats the typed InterpError into a String before ClaimOutcome exists; the declaration GATES the inversion without VERIFYING it, disclosed as a bounded compatibility arm with dissolve-on the existing witness_cost_timed_out_seed_deferral_note seam. FIX 3 - completeness is an IDENTITY JOIN, not a count equality (operator oracle ruling, 2026-08-01). classified_non_pass carries identities; non_pass_join_is_complete requires every non-Pass outcome to appear in exactly one bucket by witness identity. The residual summary.failures count survives only as a guard over rendered diagnostic strings that carry no identity, explicitly not as admission authority, with its own dissolve-on. Shared membership helper schedule_witness_entry_roster_contains lifted into std.realization_schedule rather than forked a second time in ci_layer_roots. Green by execution: 8/8 executor unit witnesses including the discriminating pair (equal counts over different identities refuses; absence refuses on its own mode with an observed positive control), 17/17 exact_witness_admission, 17/17 floor_component_receipt, and the composed ci_floor_plan evaluates. * Add extdeps.linux.proc_self_cgroup parser substrate (#7887). Model /proc/self/cgroup unified-membership read with distinct missing, ambiguous, and malformed refusal states; enroll scope carrier; witness parser fixtures only (no production workflow or path_intent changes). Co-authored-by: Cursor <cursoragent@cursor.com> * Address #7887 substrate review: semantic subject, no inflated service. Ground ExternalModelScope on ProcPidCgroupMembershipRecord (not the citation authority), remove LinuxCgroup.CurrentMembership rung inflation, and require cgroup-v2 unified shape (0::path with empty controller field). Witness 0:cpu:/path is not accepted as unified membership. Co-authored-by: Cursor <cursoragent@cursor.com> * Recut cgroup membership + memory.peak ancestor vertical after #7887 review. Move bash membership realization into extdeps.linux.proc_self_cgroup (single parser authority; no grep -c/head -1/awk widen). Add NearestAncestorContaining search policy in std.path_intent with PathIntent start. Wire ci_floor_peak_emit through bash_orch_if lowering only. Add compile-time production witnesses plus executing shell fixtures enrolled in bin_witness_wet_entries; update emit goldens. Workflow yml drift deferred until merge train clears. Co-authored-by: Cursor <cursoragent@cursor.com> * Restrict NearestAncestorContaining.start to PathRefStart construction wall. Replace nearest_ancestor_walk_target's fabricated "d" fallback for PathLiteral/PathJoin with a PathRefStart field type so non-PathRef walk carriers are unwritable at construction (review 49936, non-blocking). Co-authored-by: Cursor <cursoragent@cursor.com> * Split bash cgroup membership lowering into v2.extdeps.languages.bash_proc_self_cgroup. extdeps.linux.proc_self_cgroup now owns only language-independent /proc/self/cgroup semantics; the foreign-executor shell spelling lives in a separate realization module per shell->intent Phase 1 layering. Co-authored-by: Cursor <cursoragent@cursor.com> * Regenerate the stage0 seed for the roster-membership addition `regen_verify_gate_passes` returned false on CI run 31153645062: the `.dag` admission-model changes on this branch emit a new `schedule_witness_entry_roster_contains` (and its note) into `std_realization_schedule.rs`, and the regenerated seed was never committed, so the self-host fixed point diverged. This is `regen_stage0`'s own output, not a hand edit: 133 generated files written, exactly one changed, 21 insertions and no deletions. Run by keen-ibex-349 on behalf of deep-otter-771, whose container could not complete the `v1-compiler` lib compile: two SIGKILLs with `memory.events max 0, oom 0, oom_kill 1` at a 2.68 GiB peak against a 31.27 GiB cap — the cgroup's own limit was never reached, so the kill arrived from an ancestor. A third identical kill reproduced in this container at 1-min load 34; this run succeeded at load 10.9. The `--remote` path executes regen but uploads no artifacts, so it cannot return the bytes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Pin the known-red lane's budget partition in the plan witness, not a singleton count The floor red on 7992dae is ci_floor_plan_witnesses returning false, and it is correct: the witness pinned the known-red probe lane to EXACTLY ONE runnable whose explicit_entries length equals the whole corpus roster. That is the shape the recut deliberately replaced, so the witness had to move with it. What replaces it is strictly stronger than the count it drops. Each runnable must match EXACTLY one derived budget roster by IDENTITY (schedule_witness_entry_roster_contains over every entry), not by length — so a same-sized wrong population refuses, and the two rosters cannot be swapped between runnables, which is the budget inversion the split could otherwise hide. The runnable count must equal the number of NONEMPTY rosters, so an empty side schedules no batch rather than an empty one. Every runnable independently keeps the lane's SelectionApplied / hermetic / no-host-compiler profile, which the single-runnable form only ever asserted once. And a coverage clause requires the two rosters to sum to the corpus roster, so the split cannot silently drop a row. Pinning only the total would permit the swap; pinning only the count would permit either side carrying the wrong rows. Both are asserted. NOT VERIFIED LOCALLY, and disclosed rather than implied: this container cannot build the interpreter (five SIGKILLs today compiling the v1-compiler lib, two of them at load 9-13, with memory.events max 0 / oom_kill 1 at a 2.68 GiB peak against a 31.27 GiB cap — the kill arrives from an ancestor cgroup, not this one), and CI's own release-bins binary will not run here (requires GLIBC_2.39, unavailable). CI is the only oracle currently reachable for this change. * Make the pre-verdict arm non-green, and make the roster join actually exact Two defects found in review, both real, both closed here. BLOCKER 1 — a DECLARATION was flipping the result green. The Err arm returned ok:true whenever every explicit entry merely DECLARED a typed pre-verdict refusal. No ClaimOutcome exists on that path and run_claim has already formatted the typed InterpError into a String, so the observed phase and cause cannot be matched against the declared ones — a row declaring PreVerdictResolve/UnboundImportedVariantConstructor was admitted when some entirely different pre-verdict fault occurred. Disclosing that did not make it sound: an unobserved fact must not be verdict-bearing. The arm is now NON-GREEN and the declaration only classifies WHY, via its own mode ExpectedRedPreVerdictUnverified, which floor_component_receipt maps to Refused alongside its two siblings. It is distinct from both by design: StaleKnownRed says an executed row passed (delete the admission), ExpectedRedEvidenceAbsent says a rostered row never ran (make it run), and this one says the row stopped as declared while nothing proves it stopped for the declared reason (carry the typed cause across the boundary). Dissolve-on: EXPECTED-RED-CAUSE-1. BLOCKER 2 — the identity join was not exact, and this one is worse than it looks because it falsified the PR's own thesis. known_red_probe_batch_ matches_roster asserted length equality plus ONE-WAY containment and the note called that an identity join. It is not: actual [A, A] against expected [A, B] satisfies both — lengths agree at 2, every actual entry is present — while B is dropped and A duplicated. A same-sized wrong population passed, which is exactly what the note claimed would refuse. Replaced with known_red_roster_set_eq: duplicate-free on BOTH sides plus containment in BOTH directions, which for identity-set rosters is set equality. covers_lane had the identical shape one line down (a bare count that two swapped rows or one duplicate per side both satisfy) and is fixed with the same move rather than left standing beside the repair. Why the earlier swap probe missed it, recorded in the note so the calibration survives: swapping the two rosters changes the ASSIGNMENT, and one-way containment does catch that, because a fast entry is genuinely absent from the long roster. Multiplicity is an orthogonal axis the swap never perturbs. Evidence that a clause is non-vacuous is not evidence that it is exact, and one discriminating RED establishes only the failure mode it actually drives. Witnesses: witness_known_red_roster_set_eq_is_exact_not_a_length_agreement drives [A,A] vs [A,B] in both directions plus the order-independence and subset cases; declared_pre_verdict_refusal_is_non_green_and_carries_its_own_ mode pins the mode string and its distinctness from both siblings; fcr_pre_verdict_unverified_is_a_refusal_distinct_from_both_siblings pins the receipt projection. Rust side 9/9 green by execution; the .dag side is unverified locally for the reasons the previous commit records. * Make the non-green regression control real, not a doc comment Found in review, and it is the same defect class as the identity join it sits beside: a stated discrimination wider than the one the test drives. declared_pre_verdict_refusal_is_non_green_and_carries_its_own_mode claimed "if someone restores the green arm, the first assertion here fails". It did not. All three assertions compared string constants to each other and to a literal; none observed ClaimResult.ok. run_discovery_batch_node has two call sites and neither is a test, so nothing executed the arm — flipping ok:false back to ok:true left the whole test green. The arm was non-green and the mode-distinctness half was genuine, but the regression control the comment promised did not exist. Repaired by construction rather than by weakening the sentence: the arm's ClaimResult is extracted to pre_verdict_unverified_claim_result, its single construction site, and the test now calls it and asserts ok == false. Restore the green arm and the test fails. It also pins that the typed mode and the located cause reach detail, that the entry count is carried, and that no per-witness population is fabricated on a path that observed no witness. Also worth stating because it is a real new refusal the previous commit did not advertise: covers_lane moved from a length sum to set_eq(concat(fast, long), corpus_roster), and duplicate-freedom over the CONCAT additionally forbids an entry appearing in BOTH budget rosters. The old form could not see that — 2 + 1 == 3 holds with one row double-counted and one missing. A row in both rosters would now refuse rather than pass. 9/9 executor unit witnesses green by execution. * Partition the known-red lane by expectation kind too, not budget alone cursor review 50216 requested changes and the finding is real. Verified against the code before acting: known_red_probe_corpus_{fast,long}_budget_ roster were derived from the whole corpus roster, so the three ExpectTypedPreVerdictRefusal rows sat in the same discovery batch as ExpectAssertionFalse rows. Those two kinds cannot share a batch. A pre-verdict row stops the batch at RESOLVE, so NO per-witness outcome exists for anyone in it, and the Err arm admits that stop only when EVERY entry declared a pre-verdict refusal. One pre-verdict row in a mixed batch therefore reds its siblings — witnesses that were holding quarantine correctly and that the stop says nothing about. That is the batch-wide coupling this whole PR exists to remove, reintroduced one axis over by the budget split itself. Splitting on budget alone was not enough, and the roster that would have caught it (known_red_pre_verdict_refusal_roster) was imported by the plan and never used to schedule anything. The lane now derives up to FOUR batches, one per (expectation kind, declared budget) pair, each homogeneous in both facts that govern it: the ceiling it needs and the fact that decides its verdict. Nothing is authored — a new admission routes itself, and an empty side schedules no batch rather than an empty one. Worth stating plainly: isolating the pre-verdict batches does NOT make them pass. They are non-green by construction until EXPECTED-RED-CAUSE-1 lands, because a declaration classifies a stop and does not verify it. The point is that their refusal stays THEIR refusal — located and countable — instead of being spread over rows it has nothing to say about. Witnesses moved with it. The partition claim is now four-way with per-row exactly-one-side membership (not a pairwise XOR, which cannot express four sides); a new no_batch_mixes_a_pre_verdict_row_with_an_assertion_false_row asserts the kinds are disjoint in both directions AND that the pre-verdict side is nonempty, so it cannot pass by the population being empty; budget homogeneity now covers all four rosters; and the plan witness pins batches to rosters IN ORDER, each by set equality, plus a union clause so the split can neither drop a row nor double-count one. The pairwise check is a fold with an index rather than recursion, to avoid a Loop with no descent evidence. Unverified locally: the cold full-lib rebuild still cannot complete here. * Respell six leading-plus continuations the parser does not accept 4fba338 did not parse. A leading '+' at the start of a continuation line is a parse error ("expected expression, found Plus"); the six sites were the new four-way partition arithmetic in exact_witness_admission_witness_test.dag. Operators moved to the end of the preceding line. No logic changes. Proved on minimal three-line fixtures rather than inferred from the file: let a = 1 \n + 2 \n + 3 -> parse error let a = true \n && false \n && true -> parses let a = 1 + 2 + 3 -> parses So '+' cannot BEGIN a continuation line, '&&' can, and '+' mid-line is fine. Corpus census: leading-'&&' occurs 9,570 times tree-wide, leading-'+' occurred exactly 6 times and all 6 were these. This commit wrote the first uses of a form the grammar does not admit, which is why no prior file caught it. Two things worth knowing beyond the respelling, neither fixed here. The panic is FATAL TO THE WHOLE SOURCE ROOT rather than to the offending entry: while that file was in the tree, any dag-rooted claim_batch run died on it, including runs parsing unrelated fixtures in other directories. So it would not have presented as a localized witness failure. And the asymmetry itself - '&&' admitting leading-operator continuation while '+' does not - is a language-layer gap with no evident reason, whose diagnostic names the token without saying that the POSITION is what is wrong. Both are filed to the operator rather than chased here. I had already hit this exact class earlier in this branch on '==', '!=' and '<' and did not generalize it to arithmetic. The general rule is: in .dag, a binary operator may not start a line. * Carry the pre-verdict mode structurally, so the receipt stops saying WitnessRed cursor review 50221 requested changes and the finding is real. Verified against the code: pre_verdict_unverified_claim_result set expectation_refusal: None and put ExpectedRedPreVerdictUnverified only in `function` and `detail`. batch_failure_mode_and_detail reads expectation_refusal off the VALUE and otherwise falls through to falsifier_failure_mode, whose fallback arm is "WitnessRed". So those batches reached the floor receipt as WitnessRed -> Failed, while the .dag vocabulary this same PR added said ModeExpectedRedPreVerdictUnverified -> Refused. The arm was half-wired: non-green result and receipt vocabulary present, the classification path missing. And the shape of the miss is the one this PR exists to remove — one fact in two representations, the second recovered by substring-matching prose. StaleKnownRed already avoids it by travelling as an ExpectationRefusal; pre-verdict now does the same. ExpectationRefusal gains PreVerdictUnverified { declared_entries, cause }, the constructor sets it, and detail() is the single place the message is built rather than a second format! beside the carrier. The enum's doc now states why it is the ONLY structural route to a typed mode, so the next arm does not repeat this. The test was extended to assert the receipt, not the constant: it calls batch_failure_mode_and_detail and requires the mode to equal the pre-verdict mode and NOT to be WitnessRed. The previous version asserted mode-string distinctness and would have passed against this defect untouched — the same too-narrow-assertion class as the earlier identity-join and regression-control findings, three for three in this PR. Unverified locally: two more equivalent SIGKILLs on the cold full-lib rebuild, so I stopped per the two-kill rule. Two things a compile would have caught were checked by reading instead: ClaimResult has no Clone derive (so the record is built from a second constructor call, not r.clone()), and the matches! borrows &r.expectation_refusal rather than moving it. * Add permanent cross-realization fixture law for cgroup membership. Parser and bash runtime scan must agree on all four fixture outcomes; mutation sketches on both sides prove drift reds without shipping defects. Co-authored-by: Cursor <cursoragent@cursor.com> * delete the dead red_receipt_other_class helper the naming-hygiene walk refused Run 31219557841's regen job refused on the pre-plan witness naming walk: red_receipt_other_class is a plain fn in a *_test.dag unreachable from every test fn, which is silent de-enrollment. Deleted rather than promoted. It has zero call sites, and the changed-signature claim it looks like it should carry is already covered on the correct side -- the receipt stays red_receipt (the current run) while the STORED STATE's signature varies via signature_of_fixture(component: other_failing_component). Varying the receipt would exercise the wrong half of the comparison. So this is a dead scaffold, not a missing witness. Worth naming because a local run cannot find this class: claim_batch executes the roster handed to it, built by grepping `test fn`, so a plain fn no test reaches is outside that denominator by construction. The suite reported 52/52 before and after -- true both times, and silent on exactly the thing that failed to enroll. Decision suite 52/52 after the deletion, PASS-counted against roster. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Extend the fifth site: the pair-agreement match inside the split module regen refused on b73bead with a located non-exhaustive match: floor_component_receipt_document.dag:443:7 — missing variant(s) ModeStaleKnownRed, ModeExpectedRedEvidenceAbsent, ModeExpectedRedPreVerdictUnverified My merge commit enumerated FOUR places a mode must appear and extended all four. There were FIVE. The fifth is component_outcome_agrees_with_failure_mode, inside floor_component_receipt_document.dag — the module the #7928 split CREATED. That is not a different mistake from the one the merge was guarding against; it is the same one, one module further along: I enumerated the consumer roster visible from the module I started in, and the split had moved consumers as well as declarations. Fixed by enumerating rather than counting. A scan for every match over the coproduct corpus-wide finds four (two of which are the outer/inner halves of this one nested match), and re-running it after the fix reports zero remaining non-exhaustive sites. Verified further by parity: all eight modes now appear at exactly six structural sites each, in lockstep — type, seed reader, tag table, wire reader, outcome_of_mode, pair agreement. ModeUnrecorded's five is correct and not an omission: it is deliberately absent from the seed reader, which never observes "no mode was recorded", and failure_mode_wire_reader_note already records why. The three new arms delegate to outcome_matches_implied_mode exactly as the other non-Unrecorded arms do, so the pair check stays derived from floor_component_outcome_of_mode rather than restating which pairs are valid. No wildcard: a catch-all here would have suppressed precisely the refusal that located this, and five of six arms being identical is what makes that tempting. Worth stating because it is the good outcome, not the bad one: the arms are real and that match was genuinely non-exhaustive without them, so the typechecker refused and named both the variants and the line. A count-based check would have said nothing. * review 50351: throttle the observer path with the same window as the red path alert_decision_observer_unavailable's IncidentCurrent arm returned RefreshObserverIncident unconditionally -- it never compared the heartbeat window, and never compared the stored signature either. On the four-hourly falsifier cadence a permanently timed-out observer therefore paged every four hours, which is the notification spam this module exists to end. Two notes a few lines apart asserted the guard existed. The code was wrong and the prose was right, which is the worse orientation: an auditor reading the policy would have found it documented, coherent and untrue. The witness was holding it in place. a_repeated_observer_outage_refreshes_the_ same_incident asked the repeat case at last=5000 now=6000 -- a one-second gap inside a twenty-hour window -- and asserted RefreshObserverIncident, pinning the spam as the contract. That is why 52/52 was green over it, and why the correct fix would have read as a regression. New RefreshObserverIncidentWithoutNotification arm; the observer path now mirrors the red path. The two notifying cases share one arm because they produce the same effect -- the red path splits its two only because their MESSAGES differ, a distinction in what gets said rather than whether to say it. The suppressed arm carries last_notification_at UNCHANGED. Advancing it to now looks right (the run did just observe the incident) but restarts the window every cadence, so the elapsed comparison can never fire and the heartbeat goes silent permanently -- converting a spam defect into a strictly worse silence defect that nothing observes. The field records when we last SPOKE, never when we last LOOKED. Adding the arm broke alert_decision_notifies and alert_decision_notification as non-exhaustive, so the closed coproduct made it structurally impossible to add a suppressing arm while leaving a predicate claiming it notifies. Roster 52 -> 55, 55/55 PASS-counted. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix #7978 CI drift, stale citations, and golden brace escapes. Remove merge-appended trailing blank lines from generated workflows (heal artifact), update DESIGN shell→intent citations to the landed cgroup vertical symbols, and escape literal braces in ci_floor_peak emit goldens so dag interpolation does not corrupt expected bytes. Co-authored-by: Cursor <cursoragent@cursor.com> * chore: regenerate drifted generated artifacts (ci auto-heal) * Fix workflow drift: add cgroup locate scaffold comments to pre/post steps. Heal could not push author-commit-required workflow paths; CI projected scaffold dissolve-on lines for ci_floor_peak pre/post pipelines that were missing from the committed ci.yml and falsifier.yml. Co-authored-by: Cursor <cursoragent@cursor.com> * Roster unified_membership_outcome_tag_eq for non-fold residue gate. The cross-realization tag equality fold in extdeps.linux.proc_self_cgroup uses structural off-variant wildcard arms; enroll it in non_fold_residue so non_fold_residue_no_unrostered_or_stale passes on the floor. Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: Cursor <cursoragent@cursor.com> Co-authored-by: Brian Searls <11205878+briansrls@users.noreply.github.com>
ALERT-4. The whole alert decision as one pure function — no GitHub calls, no clock read, no issue read. Every fact arrives as a parameter, so the arms hardest to reach in production are the cheapest to prove.
alert_decision(admission, receipt, observation, now, escalation, routings) -> AlertDecision, total over sixteen terminal arms, eight of them refusals.Guard order is the algebra
Trust → escalation recipient → observer availability → receipt decodability → subject match → state readability → verdict.
Observer availability sits before the receipt deliberately: a run that timed out or failed at startup produced no receipt, so requiring one first reported "the floor's writer is broken" for the case where the floor never ran. Trust sits first because this program holds issue-write capability and an unadmitted run's receipt must never be decoded.
The facts each arm carries
first_red; silent refresh moves neither; changed class preservesfirst_red(restarting it would erase how long the observer has been broken, precisely when the incident worsened).FirstRedStanding— an adopted issue does not fabricatefirst_red = now. Declared once, ingunbc.falsifier_alert_state, andnullon the wire rather than a sentinel instant.AlertNotification.escalation_handle: NonEmptyStr; the undeclared case isRefuseEscalationRecipientUndeclared, reached before any notifying arm can be built.OpenObserverIncident/RefreshObserverIncidentcarry issue, next state andsilent_for, with their own signature so a timeout after a startup failure is a changed class.NotifyAlertControllerUnavailablereplaces silent refusals for a trusted run with a bad receipt, corrupt marker, or non-joining routings — previously the workflow completed successfully while the alert had done nothing. It never renders receipt content and never overwrites the marker. Untrusted events stay silent, so the wall cannot be used to page an operator on demand.Identity
IncidentSignatureis a sorted set ofComponentIncidentIdentity { index, outcome_tag, failure_mode_tag }. The label is out of the identity — it was the delimiter hazard — and the stored marker is read back structurally, with its index through the samestrict_natural_of_lexemethe receipt decoder uses.Routing
Routings exact-join the failing set by index; missing, surplus and duplicate each refuse with the indices named.
Conclusions
TimedOut/StartupFailure→ observer incident.Skipped/Neutral/ActionRequired→RunPreventedByConfiguration, countable and distinct from green.Cancelled→CancellationUnexplained, deliberately unresolved: theworkflow_runenvelope does not say who cancelled a run or why.Evidence
52 witnesses, PASS-counted. Discriminating REDs per arm, each with a control that stayed green under the same mutation — receipts in
falsifier_alert_decision_red_receipts_note.Not in scope
The trust wall is not wired (ALERT-6, whose acceptance must prove both enforcement points). The
AlertDecision -> AlertEffectPlanprojection comes before shadow mode. Item 1's remaining half — typing marker members via the shared closed tag readers — waits on #7928.Stacked on #7928; rebases onto it when that merges.