From 5ee66a9a2787b9872125cc4ed2781537027a205e Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 11:13:48 +0700 Subject: [PATCH] spec(ci): suite ledger steward -- what the corpus ledger bot applies and refuses (Closes #10204) specs/ci/suite_ledger_steward.t27 decides, per corpus-ledger row and per master run, what a steward may write to docs/reports/suite_expectations.json: DROP a row whose spec passes, REPIN a discard pin that fell, lower the gate-failure pin and the cap to the count. It refuses a new failure, a moved or expired row, any rise, a missing reading, an unpinned or self-inconsistent row, a cap rise and a drop flood. A refused row stays as master has it and the rest is applied (#10192's rule). Tests pinned on #10172, #8345, #7804, #6437, #9281, #8823 and #5497. specs/jobs/suite_ledger_steward.t27 is the job card. Seals written by t27c on the Railway lab. Co-Authored-By: Claude Opus 5.5 --- .trinity/seals/ci_SuiteLedgerSteward.json | 33 ++ .../seals/jobs_JobSuiteLedgerSteward.json | 28 ++ specs/ci/suite_ledger_steward.t27 | 438 ++++++++++++++++++ specs/jobs/suite_ledger_steward.t27 | 153 ++++++ 4 files changed, 652 insertions(+) create mode 100644 .trinity/seals/ci_SuiteLedgerSteward.json create mode 100644 .trinity/seals/jobs_JobSuiteLedgerSteward.json create mode 100644 specs/ci/suite_ledger_steward.t27 create mode 100644 specs/jobs/suite_ledger_steward.t27 diff --git a/.trinity/seals/ci_SuiteLedgerSteward.json b/.trinity/seals/ci_SuiteLedgerSteward.json new file mode 100644 index 0000000000..f618d37b73 --- /dev/null +++ b/.trinity/seals/ci_SuiteLedgerSteward.json @@ -0,0 +1,33 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+c0f6076", + "closure": [ + { + "spec": "specs/ci/derived_data.t27", + "spec_hash": "sha256:7fe9ca15a493a13f0b0f54d354a2cd08d51f0945bf70185a899315f6ad4fc64a" + } + ], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:d571832e1c7ef30dd1e23dcbaf7894b82c2812b38dd29735007aa9291ec4ce30", + "gen_hash_rust": "sha256:8093eb8b837cc85f0777ba4fb18b01a2d4f62dd11fb0f343311ed0e7aaabcbdd", + "gen_hash_verilog": "sha256:07fa21e636186e463fc6a400e32c3983e19fe35eca2c0b3298ccc5af6cdd6c81", + "gen_hash_zig": "sha256:563755a63c5b8d4c7757c5c1d77df607540b7c1899ea2cfb92cffa61a75be2eb", + "module": "SuiteLedgerSteward", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-18T04:17:45Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:c64efdf85fb9c17278df8bf9f0f428761cf03b58873556b4dceae17aae1f2969", + "spec_path": "specs/ci/suite_ledger_steward.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 11, + "total": 11, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/.trinity/seals/jobs_JobSuiteLedgerSteward.json b/.trinity/seals/jobs_JobSuiteLedgerSteward.json new file mode 100644 index 0000000000..b0fd4d4693 --- /dev/null +++ b/.trinity/seals/jobs_JobSuiteLedgerSteward.json @@ -0,0 +1,28 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+c0f6076", + "closure": [], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:3b51a3a922afee5d27aecbdd27ab8814d74aca8db44c982190914fd121253eb7", + "gen_hash_rust": "sha256:9535b63c202997d5b528ea05a41046a542d6ef18030c65af9c437c1c3edf9e2e", + "gen_hash_verilog": "sha256:c97958b17eb22ea2e01d387ca3b16cb1951f0bb2a48600603e35374e3d88514f", + "gen_hash_zig": "sha256:bfbb9f8d2ad0eec5ae8b6b3c40a9157df14a2a5636d38095838ce0ed516e755f", + "module": "JobSuiteLedgerSteward", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-18T04:17:47Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:4692c9ab3e179f1e73bec6c87848ef5011872d0ae03e69454e2692b8944b7c61", + "spec_path": "specs/jobs/suite_ledger_steward.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 2, + "total": 2, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/specs/ci/suite_ledger_steward.t27 b/specs/ci/suite_ledger_steward.t27 new file mode 100644 index 0000000000..dad798f170 --- /dev/null +++ b/specs/ci/suite_ledger_steward.t27 @@ -0,0 +1,438 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/ci/suite_ledger_steward.t27 -- which corpus-ratchet findings on a master run the suite ledger +; steward applies by itself, and which it refuses and leaves to a person. +; docs/reports/suite_expectations.json is the corpus ledger: one row per (spec, first failing phase), +; a discard pin on every parse-no-discard row, the gate-failure pin max_gate_failures, and the cap +; max_entries. `t27c suite --ratchet --corpus-only` (bootstrap/src/suite.rs ratchet_compare) is red +; for a fall as well as for a rise: an UNEXPECTED PASS (the spec now passes every phase) and a +; DISCARD IMPROVED (fewer tokens lost than pinned) fail the check until the ledger says so. Each one +; turned `Corpus ratchet` red on master, and every PR inherited the red until someone wrote a hand PR. +; #10172 is the latest: 8 rows dropped (seven igla/coder specs from #10101, nn/attention from #10095), +; bench_proxy 738 -> 696 and prm 521 -> 520 re-pinned, the cap 81 -> 73. The same shape is in #7804 +; (3 rows, 77 -> 74), #6437 (4 rows, 113 -> 109) and #8345 (one pin 386 -> 349, cap 74 -> 71). +; specs/ci/derived_data.t27 says lag is PENDING and one bot re-derives it on master. This file is +; that bot's decision for the corpus ledger, the counterpart of specs/tri/t27b/ledger_steward.t27. +; The job card is specs/jobs/suite_ledger_steward.t27. +; What the steward applies, per ledger row and per run: +; DROP the row's spec fails no phase in the run: the row goes (an UNEXPECTED PASS) +; REPIN a parse-no-discard row whose total fell and whose channels each held or fell: the pin +; becomes the run's total and split (DISCARD IMPROVED, DISCARD CHANNEL) +; the gate-failure pin falls to the run's count +; the cap max_entries becomes the composed ledger's row count, which only falls +; What it refuses, so a person reads it (derived_data.t27 rule 4: the bot never writes a cap rise or +; a non-pass reason): +; a NEW FAILURE (a spec failing with no row: a regression, or a ported spec that needs a reason); +; a MOVED row (the spec fails another phase now: the reason must be rewritten); an EXPIRED row; +; a discard total that ROSE, a channel that rose while the total held or fell, a pinned row the +; run took NO READING of, a row with no total or no split (UNPINNED), a row whose split does not sum +; to its total (the ledger disagrees with itself); a gate-failure count that rose or has no pin; +; a cap rise (the composed ledger still over max_entries); and more drops in one run than +; DROP_LIMIT (a broken run looks like a corpus where everything passes). +; A rise is never applied, not even a small one with a good story. #10172 raised benchmark 315 -> 319 +; by hand, with the reason in _why_entries_rose; suite.rs's bless says a worsened pin is raised +; "ONLY by a human running bless and reviewing the diff". On #10172's run the steward applies the +; other ten changes and leaves benchmark as master has it, listed in its PR. +; A refused row stays as master has it and the rest of the run is applied (#10192's rule): only a run +; with nothing to apply, a cap rise or a drop flood is refused as a whole. +; ASCII only (L3). +; phi^2 + 1/phi^2 = 3 | TRINITY + +module SuiteLedgerSteward; + +use ci::derived_data::bot_may_bless; + +/// What the steward does with one ledger row, the gate-failure pin, or one run failure with no row. +/// KEEP the row holds, or there is nothing to do +/// DROP the row's spec passes every phase: the row goes +/// REPIN the discard (or gate-failure) pin fell: it becomes the run's number +/// REFUSE a person reads it: the row stays as master has it and the PR lists it +pub const ACT_KEEP : u8 = 0; +pub const ACT_DROP : u8 = 1; +pub const ACT_REPIN : u8 = 2; +pub const ACT_REFUSE : u8 = 3; + +/// Why something was refused, as the PR table or the issue words it. +pub const RR_NONE : u8 = 0; +pub const RR_NEW_FAILURE : u8 = 1; +pub const RR_MOVED : u8 = 2; +pub const RR_EXPIRED : u8 = 3; +pub const RR_DISCARD_ROSE : u8 = 4; +pub const RR_CHANNEL_ROSE : u8 = 5; +pub const RR_NO_READING : u8 = 6; +pub const RR_UNPINNED : u8 = 7; +pub const RR_LEDGER_SELF : u8 = 8; +pub const RR_GATE_ROSE : u8 = 9; +pub const RR_GATE_UNPINNED : u8 = 10; +pub const RR_CAP_RISE : u8 = 11; +pub const RR_DROP_FLOOD : u8 = 12; + +/// The run's verdict, as ledger_steward.t27 has it. +/// NOTHING no finding: the ratchet is green, no job +/// APPLY something is the steward's: compose the ledger from it, one PR, auto-merge; a refused +/// row stays as master has it and is listed in the PR +/// REFUSE nothing to apply but a person's finding, or the run as a whole is refused (a cap rise, +/// a drop flood): one issue for the run, no PR +/// SKIP not a run the steward reads (run_stewardable) +pub const RV_NOTHING : u8 = 0; +pub const RV_APPLY : u8 = 1; +pub const RV_REFUSE : u8 = 2; +pub const RV_SKIP : u8 = 3; + +/// More rows dropped in one run than this says the run is broken, not the corpus better: a suite +/// that stopped early observes few failures, and every row it did not reach reads as a pass. The +/// hand batches dropped 8 (#10172), 4 (#6437), 3 (#7804) and 2 (#6186); #5497 dropped 51 after a +/// parser change, and a person reading one issue for that is the cheap side of the mistake. +pub const DROP_LIMIT : u32 = 16; + +/// The effects a steward job may run, by the job card's effect steps (ledger_steward.t27's numbering). +pub const EF_REFUSAL_ISSUE : u8 = 0; +pub const EF_COMPOSE : u8 = 1; +pub const EF_LEDGER_ISSUE : u8 = 2; +pub const EF_PULL_REQUEST : u8 = 3; +pub const EF_AUTO_MERGE : u8 = 4; + +/// Why one row (or one run failure) is refused, from where the run and the ledger put its spec. +/// in_ledger the ledger has a row for this spec +/// run_fails the run observed the spec failing some phase (its first failing phase) +/// same_phase that phase is the row's phase +/// expired the row's `expires` date is before the run's day +pub fn row_refusal(in_ledger: bool, run_fails: bool, same_phase: bool, expired: bool) -> u8 { + if (in_ledger == false) { + if (run_fails) { return RR_NEW_FAILURE; } + return RR_NONE; + } + if (run_fails == false) { return RR_NONE; } + if (same_phase == false) { return RR_MOVED; } + if (expired) { return RR_EXPIRED; } + return RR_NONE; +} + +/// The steward's action on one row by its phase alone. A row whose spec passes is dropped even when +/// its date ran out: there is nothing left to renew. +pub fn row_action(in_ledger: bool, run_fails: bool, same_phase: bool, expired: bool) -> u8 { + if (row_refusal(in_ledger, run_fails, same_phase, expired) != RR_NONE) { return ACT_REFUSE; } + if (in_ledger and run_fails == false) { return ACT_DROP; } + return ACT_KEEP; +} + +/// Why a parse-no-discard row's pin is refused. +/// consistent the pinned split sums to the pinned total +/// pinned the row has both a total and a split +/// has_reading the run measured the spec (no reading is not zero: suite.rs) +/// old, seen the pinned and the measured totals +/// channels_rose how many channels the run saw above their pin (a channel absent counts as 0) +pub fn discard_refusal(consistent: bool, pinned: bool, has_reading: bool, old: u32, seen: u32, channels_rose: u32) -> u8 { + if (pinned == false) { return RR_UNPINNED; } + if (consistent == false) { return RR_LEDGER_SELF; } + if (has_reading == false) { return RR_NO_READING; } + if (seen > old) { return RR_DISCARD_ROSE; } + if (channels_rose > 0) { return RR_CHANNEL_ROSE; } + return RR_NONE; +} + +/// The steward's action on a parse-no-discard row that holds its phase. `channels_fell` is how many +/// channels the run saw below their pin; with no channel risen, a split can move only by falling. +pub fn discard_action(consistent: bool, pinned: bool, has_reading: bool, old: u32, seen: u32, channels_rose: u32, channels_fell: u32) -> u8 { + if (discard_refusal(consistent, pinned, has_reading, old, seen, channels_rose) != RR_NONE) { return ACT_REFUSE; } + if (seen < old) { return ACT_REPIN; } + if (channels_fell > 0) { return ACT_REPIN; } + return ACT_KEEP; +} + +/// One row's action: the phase decides first, and only a row that keeps its phase has its pin read. +/// A row of any other phase carries no pin, so its `discard` is KEEP. +pub fn entry_action(row: u8, discard: u8) -> u8 { + if (row != ACT_KEEP) { return row; } + return discard; +} + +/// The gate-failure pin: it falls with the run's count, and a rise or a missing pin is a person's. +pub fn gate_refusal(pinned: bool, old: u32, seen: u32) -> u8 { + if (pinned == false) { return RR_GATE_UNPINNED; } + if (seen > old) { return RR_GATE_ROSE; } + return RR_NONE; +} + +pub fn gate_action(pinned: bool, old: u32, seen: u32) -> u8 { + if (gate_refusal(pinned, old, seen) != RR_NONE) { return ACT_REFUSE; } + if (seen < old) { return ACT_REPIN; } + return ACT_KEEP; +} + +/// Folds over one run's actions, grouped by action with `n` rows in the group. +pub fn tally_refused(acc: u32, act: u8, n: u32) -> u32 { + if (act == ACT_REFUSE) { return acc + n; } + return acc; +} + +pub fn tally_applied(acc: u32, act: u8, n: u32) -> u32 { + if (act == ACT_DROP) { return acc + n; } + if (act == ACT_REPIN) { return acc + n; } + return acc; +} + +pub fn tally_drops(acc: u32, act: u8, n: u32) -> u32 { + if (act == ACT_DROP) { return acc + n; } + return acc; +} + +pub fn drop_flood(drops: u32) -> bool { + return drops > DROP_LIMIT; +} + +/// The composed ledger's row count: the steward only drops rows, so the count only falls. +pub fn rows_after(rows_before: u32, drops: u32) -> u32 { + if (drops > rows_before) { return 0; } + return rows_before - drops; +} + +/// The cap the composed ledger writes is its row count, and only when that holds or lowers the old +/// cap (derived_data.t27 bot_may_bless). A ledger still over its cap after the drops needs a cap rise, +/// which is a person's: the whole run is refused and the old cap stays. +pub fn cap_fits(rows: u32, old_cap: u32) -> bool { + return bot_may_bless(old_cap, rows); +} + +pub fn cap_after(rows: u32, old_cap: u32) -> u32 { + if (cap_fits(rows, old_cap)) { return rows; } + return old_cap; +} + +/// A run the steward reads: a master run, whose t27c was built from that same commit (a lab binary +/// older than master reported a false UNEXPECTED FAILURE on #10172's tree), whose ratchet reached its +/// verdict (a crash before the Ratchet section leaves nothing to read), and whose ledger is the one +/// master has now (otherwise its findings describe a file that is gone). +pub fn run_stewardable(is_master: bool, same_compiler: bool, ratchet_ran: bool, same_ledger: bool) -> bool { + if (is_master == false) { return false; } + if (same_compiler == false) { return false; } + if (ratchet_ran == false) { return false; } + if (same_ledger == false) { return false; } + return true; +} + +/// A refused row never holds back the steward's own: they are applied and the refused row stays. +pub fn run_verdict(stewardable: bool, refused: u32, applied: u32, drops: u32, cap_ok: bool) -> u8 { + if (stewardable == false) { return RV_SKIP; } + if (drop_flood(drops)) { return RV_REFUSE; } + if (cap_ok == false) { return RV_REFUSE; } + if (applied > 0) { return RV_APPLY; } + if (refused > 0) { return RV_REFUSE; } + return RV_NOTHING; +} + +/// The run-level reason the issue leads with when no single row was refused. +pub fn run_refusal(refused: u32, drops: u32, cap_ok: bool) -> u8 { + if (refused > 0) { return RR_NONE; } + if (drop_flood(drops)) { return RR_DROP_FLOOD; } + if (cap_ok == false) { return RR_CAP_RISE; } + return RR_NONE; +} + +/// Which effects a verdict runs: a refused run opens its issue and nothing else, an applied run its +/// PR and nothing else. +pub fn effect_wanted(verdict: u8, effect: u8) -> bool { + if (effect == EF_REFUSAL_ISSUE) { return verdict == RV_REFUSE; } + if (effect > EF_AUTO_MERGE) { return false; } + return verdict == RV_APPLY; +} + +/// A run starts a steward job when it is a master run whose ratchet is red and no job was started +/// for its commit yet. +pub fn run_starts_job(is_master: bool, ratchet_red: bool, commit_seen: bool) -> bool { + if (is_master == false) { return false; } + if (ratchet_red == false) { return false; } + if (commit_seen) { return false; } + return true; +} + +test pr_10172_applies_ten_rows_and_refuses_the_rise { + // #10172's run: seven igla/coder specs (#10101) and nn/attention (#10095) pass every phase + var drop : u8 = row_action(true, false, false, false); + assert drop == ACT_DROP; + // bench_proxy 738 -> 696: bdd-block-fallback 712 -> 696, stray-brace 1 -> 0, top-level-resync 25 -> 0 + var bench_proxy : u8 = entry_action(row_action(true, true, true, false), discard_action(true, true, true, 738, 696, 0, 3)); + assert bench_proxy == ACT_REPIN; + // prm 521 -> 520: stray-brace 1 -> 0, bdd-block-fallback held at 520 + var prm : u8 = entry_action(row_action(true, true, true, false), discard_action(true, true, true, 521, 520, 0, 1)); + assert prm == ACT_REPIN; + // benchmark 315 -> 319: bdd-block-fallback rose by 4; the hand PR raised the pin, the steward does not + var benchmark : u8 = entry_action(row_action(true, true, true, false), discard_action(true, true, true, 315, 319, 1, 0)); + assert benchmark == ACT_REFUSE; + assert discard_refusal(true, true, true, 315, 319, 1) == RR_DISCARD_ROSE; + var refused : u32 = tally_refused(0, benchmark, 1); + var applied : u32 = tally_applied(0, drop, 8); + applied = tally_applied(applied, bench_proxy, 1); + applied = tally_applied(applied, prm, 1); + var drops : u32 = tally_drops(0, drop, 8); + drops = tally_drops(drops, bench_proxy, 1); + assert refused == 1; + assert applied == 10; + assert drops == 8; + // 81 rows, 8 dropped: the cap follows the count down, 81 -> 73 + assert rows_after(81, drops) == 73; + assert cap_fits(73, 81) == true; + assert cap_after(73, 81) == 73; + assert run_verdict(run_stewardable(true, true, true, true), refused, applied, drops, cap_fits(73, 81)) == RV_APPLY; + assert effect_wanted(RV_APPLY, EF_PULL_REQUEST) == true; + assert effect_wanted(RV_APPLY, EF_REFUSAL_ISSUE) == false; +} + +test pr_10172_benchmark_alone_is_a_persons { + // after the steward's PR, benchmark's rise is the only finding left: one issue, no PR + var benchmark : u8 = discard_action(true, true, true, 315, 319, 1, 0); + var refused : u32 = tally_refused(0, benchmark, 1); + var applied : u32 = tally_applied(0, benchmark, 1); + assert run_verdict(true, refused, applied, 0, cap_fits(73, 73)) == RV_REFUSE; + assert effect_wanted(RV_REFUSE, EF_REFUSAL_ISSUE) == true; + assert effect_wanted(RV_REFUSE, EF_COMPOSE) == false; +} + +test pr_8345_repins_one_and_lowers_a_slack_cap { + // #8345: math/constants top-level-resync 37 -> 0, discard 386 -> 349; 71 rows under a cap of 74 + var constants : u8 = entry_action(row_action(true, true, true, false), discard_action(true, true, true, 386, 349, 0, 1)); + assert constants == ACT_REPIN; + var applied : u32 = tally_applied(0, constants, 1); + var drops : u32 = tally_drops(0, constants, 1); + assert drops == 0; + assert cap_after(rows_after(71, drops), 74) == 71; + assert run_verdict(true, 0, applied, drops, cap_fits(71, 74)) == RV_APPLY; +} + +test pr_7804_and_6437_drop_their_passes { + // #7804: three GoldenFloat lesson specs pass every phase, 77 -> 74 + var drops : u32 = tally_drops(0, row_action(true, false, false, false), 3); + assert rows_after(77, drops) == 74; + assert run_verdict(true, 0, tally_applied(0, ACT_DROP, 3), drops, cap_fits(74, 77)) == RV_APPLY; + // #6437: four rewritten specs, 113 -> 109 + drops = tally_drops(0, ACT_DROP, 4); + assert cap_after(rows_after(113, drops), 113) == 109; +} + +test night_tick_9281_is_refused { + // #9281: six ported specs fail codegen with no row, and the ledger already held 77 under a cap of 75 + var fresh : u8 = row_action(false, true, false, false); + assert fresh == ACT_REFUSE; + assert row_refusal(false, true, false, false) == RR_NEW_FAILURE; + var refused : u32 = tally_refused(0, fresh, 6); + assert refused == 6; + // the new rows are never written, so the count stays 77, and 77 over 75 is a cap rise + assert cap_fits(rows_after(77, 0), 75) == false; + assert cap_after(77, 75) == 75; + assert run_verdict(true, refused, 0, 0, false) == RV_REFUSE; +} + +test pr_8823_two_new_failures_are_refused { + // #8823: gen_w698 and railway fail gen-verilog with no row (72 -> 74 by hand) + var refused : u32 = tally_refused(0, row_action(false, true, false, false), 2); + assert refused == 2; + assert run_verdict(true, refused, 0, 0, cap_fits(72, 72)) == RV_REFUSE; + assert run_refusal(refused, 0, true) == RR_NONE; +} + +test pr_5497_is_a_drop_flood { + // #5497: 51 rows passed after a parser change, 6 moved one phase later, 33 ports failed with no row + var drops : u32 = tally_drops(0, ACT_DROP, 51); + var refused : u32 = tally_refused(0, row_action(true, true, false, false), 6); + refused = tally_refused(refused, row_action(false, true, false, false), 33); + assert row_refusal(true, true, false, false) == RR_MOVED; + assert drops == 51; + assert refused == 39; + assert drop_flood(drops) == true; + assert run_verdict(true, refused, 56, drops, cap_fits(rows_after(151, drops), 151)) == RV_REFUSE; + assert run_refusal(0, drops, true) == RR_DROP_FLOOD; + assert run_verdict(true, 0, DROP_LIMIT, DROP_LIMIT, true) == RV_APPLY; +} + +test the_steward_refuses_these { + // a discard rise, however small + assert discard_action(true, true, true, 220, 221, 1, 0) == ACT_REFUSE; + // a channel that rose while the total fell: one defect swapped for another + assert discard_refusal(true, true, true, 100, 90, 1) == RR_CHANNEL_ROSE; + assert discard_action(true, true, true, 100, 90, 1, 2) == ACT_REFUSE; + // a pinned row the run took no reading of: silence is not zero + assert discard_refusal(true, true, false, 52, 0, 0) == RR_NO_READING; + // no bound, or a bound that disagrees with itself + assert discard_refusal(true, false, true, 0, 30, 0) == RR_UNPINNED; + assert discard_refusal(false, true, true, 30, 30, 0) == RR_LEDGER_SELF; + // an expired row that still fails: renewing it needs a reason + assert row_refusal(true, true, true, true) == RR_EXPIRED; + assert row_action(true, true, true, true) == ACT_REFUSE; + // the gate-failure count + assert gate_refusal(true, 2, 3) == RR_GATE_ROSE; + assert gate_refusal(false, 0, 2) == RR_GATE_UNPINNED; + assert gate_action(true, 2, 3) == ACT_REFUSE; +} + +test the_steward_applies_these { + // a passing row is dropped even past its date: nothing is left to renew + assert row_action(true, false, false, true) == ACT_DROP; + assert row_refusal(true, false, false, true) == RR_NONE; + // a row that holds is kept, and a spec with no row that passes is no finding + assert row_action(true, true, true, false) == ACT_KEEP; + assert row_action(false, false, false, false) == ACT_KEEP; + assert discard_action(true, true, true, 52, 52, 0, 0) == ACT_KEEP; + // the gate-failure pin follows the count down + assert gate_action(true, 2, 1) == ACT_REPIN; + assert gate_action(true, 2, 2) == ACT_KEEP; + // the phase decides before the pin + assert entry_action(ACT_DROP, ACT_REFUSE) == ACT_DROP; + assert entry_action(ACT_REFUSE, ACT_REPIN) == ACT_REFUSE; + assert entry_action(ACT_KEEP, ACT_REPIN) == ACT_REPIN; + assert tally_applied(3, ACT_KEEP, 2) == 3; + assert tally_refused(3, ACT_REPIN, 2) == 3; +} + +test only_a_master_run_of_its_own_compiler_is_read { + assert run_stewardable(true, true, true, true) == true; + assert run_stewardable(false, true, true, true) == false; + // #10172's lab binary predated #10084 and saw verilog_odd_cast fail parse; CI's master build did not + assert run_stewardable(true, false, true, true) == false; + assert run_stewardable(true, true, false, true) == false; + assert run_stewardable(true, true, true, false) == false; + assert run_verdict(run_stewardable(true, false, true, true), 1, 10, 8, true) == RV_SKIP; + assert run_verdict(true, 0, 0, 0, true) == RV_NOTHING; + assert effect_wanted(RV_NOTHING, EF_COMPOSE) == false; + assert effect_wanted(RV_SKIP, EF_REFUSAL_ISSUE) == false; + assert effect_wanted(RV_APPLY, EF_AUTO_MERGE + 1) == false; + assert rows_after(3, 5) == 0; +} + +test a_red_master_run_starts_one_job { + assert run_starts_job(true, true, false) == true; + assert run_starts_job(true, true, true) == false; + assert run_starts_job(true, false, false) == false; + assert run_starts_job(false, true, false) == false; +} + +// derived_data.t27 rule 4: the bot never writes a cap rise. Its bot_may_bless and this cap agree. +invariant the_cap_never_rises { + assert cap_fits(74, 73) == false; + assert cap_after(74, 73) == 73; + assert cap_fits(73, 73) == true; + assert bot_may_bless(81, 73) == cap_fits(73, 81); + assert cap_after(0, 5) == 0; +} + +invariant a_rise_or_a_new_failure_is_never_applied { + assert row_action(false, true, false, false) == ACT_REFUSE; + assert row_action(false, true, true, false) == ACT_REFUSE; + assert row_action(true, true, false, false) == ACT_REFUSE; + assert discard_action(true, true, true, 0, 1, 0, 0) == ACT_REFUSE; + assert discard_action(true, true, true, 10, 10, 1, 1) == ACT_REFUSE; + assert gate_action(true, 0, 1) == ACT_REFUSE; + assert tally_applied(0, ACT_REFUSE, 9) == 0; +} + +invariant the_steward_codes_never_move { + assert ACT_KEEP == 0; + assert ACT_DROP == 1; + assert ACT_REPIN == 2; + assert ACT_REFUSE == 3; + assert RV_NOTHING == 0; + assert RV_APPLY == 1; + assert RV_REFUSE == 2; + assert RV_SKIP == 3; + assert RR_DROP_FLOOD == 12; + assert EF_AUTO_MERGE == 4; + assert DROP_LIMIT == 16; +} diff --git a/specs/jobs/suite_ledger_steward.t27 b/specs/jobs/suite_ledger_steward.t27 new file mode 100644 index 0000000000..4b6a879e0b --- /dev/null +++ b/specs/jobs/suite_ledger_steward.t27 @@ -0,0 +1,153 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/jobs/suite_ledger_steward.t27 -- the corpus (suite) ledger steward, as a job the Queen runs +; (specs/queen/jobs.t27). The counterpart of specs/jobs/t27b_ledger_steward.t27 for +; docs/reports/suite_expectations.json, the ledger behind the `Corpus ratchet` check. +; The steps are the ones a person ran by hand each time master's `Corpus ratchet` went red on a fall: +; read the run's findings, drop the rows whose specs now pass, re-pin the discard counts that fell, +; lower max_entries to the count, open an issue and a PR that closes it (#10172, #8345, #7804, #6437). +; What the steward may apply and what it refuses is decided in specs/ci/suite_ledger_steward.t27 +; (RULES), compiled to wasm like every card decision; this card names the steps. +; A job starts when master's CHECK job of WORKFLOW completes red and no job was started for its +; commit (suite_ledger_steward.t27 run_starts_job). The run's findings are read from its ARTIFACT: +; SUMMARY_FILE carries the RatchetVerdict under `ratchet` and the per-spec results (the first failing +; phase, the discard total and its channels); LOG_FILE is quoted in the issue and the PR. +; The job's parameters are the run (its Actions run id) and the run's commit. +; 0 CHECK steward-run the run is pinned as the subject: its ref is master, its t27c was +; built from that commit, the ratchet reached its verdict, and +; master's ledger is the ledger the run compared against +; (run_stewardable); otherwise the job fails as SKIP +; 1 EFFECT steward-refusals-issue when run_verdict is REFUSE: one issue for this run, listing each +; refused row with its reason (row_refusal, discard_refusal, +; gate_refusal, or run_refusal) and the rows the steward would have +; applied; otherwise PASS, nothing done +; 2 CHECK steward-appliable run_verdict is APPLY: some row is the steward's, the cap fits +; (cap_fits) and the drops are no flood (DROP_LIMIT); a refused row +; stays as master has it and is listed in the PR; REFUSE fails the +; job, pointing at the issue +; 3 EFFECT steward-ledger-issue the issue the ledger commit and the PR close (the Issue Gate: +; `Closes #N` in the commit and on line 1 of the PR body), +; labelled ISSUE_LABEL +; 4 EFFECT steward-compose compose the ledger from master's, row by row (entry_action: DROP +; removes the row, REPIN writes the run's discard_tokens and +; discard_by_channel; KEEP and REFUSE leave it); max_gate_failures by +; gate_action; max_entries = cap_after. It does NOT run +; `--bless-expectations`: bless drops the `_why_entries_*` notes and +; would write a rise. Rows stay in (path, phase) order, the notes +; stay, one line naming the run and this card is appended to +; `_why_entries_fell`, and the file keeps serde's pretty layout with +; a trailing newline. Push it as one commit to BRANCH_PREFIX + the +; run's commit (12 hex) +; 5 EFFECT steward-pull-request the PR from that branch to master, body line 1 `Closes #`, +; with a table of the rows by action and every refused row +; 6 EFFECT steward-auto-merge enable auto-merge with MERGE_METHOD while the checks are pending +; (GitHub refuses it once they finished with a non-required red) +; 7 WAIT steward-merged the PR merged; a day without it fails the job (jobs.t27) +; Every EFFECT goes through the effects journal (control.t27 section 7) under the key +; JOURNAL_PREFIX + the run's commit + ":" + its STEP_WHAT, so a Queen that restarts mid-step looks +; before she acts and never opens a second issue or PR for one run. STEP_EFFECT names the effect kind +; each step needs from the supervisor. +; Read at run time by the supervisor's vendored compiler wasm: the supervisor reads the constants; +; the two functions are only what the card's tests ask of them. +; Not wired yet: the trigger needs the supervisor (lab.py) to watch WORKFLOW, which is foreign code +; behind the owner-approved-foreign label; until then the card is the decision and nothing runs it. +; ASCII only (L3). +; phi^2 + 1/phi^2 = 3 | TRINITY + +module JobSuiteLedgerSteward; + +pub const JOB_NAME : str = "suite-ledger-steward"; +pub const REPO : str = "gHashTag/t27"; +pub const BASE_BRANCH : str = "master"; +pub const LEDGER : str = "docs/reports/suite_expectations.json"; +pub const RULES : str = "specs/ci/suite_ledger_steward.t27"; + +/// Where a master run is read: the corpus ratchet workflow, its job, and the artifact it uploads. +pub const TRIGGERS : [1]str = ["corpus-ratchet"]; +pub const WORKFLOW : str = "corpus-ratchet.yml"; +pub const CHECK : str = "Corpus ratchet (expected-failure ledger)"; +pub const ARTIFACT : str = "corpus-ratchet-log"; +pub const SUMMARY_FILE : str = "suite_summary.json"; +pub const LOG_FILE : str = "ratchet.log"; + +/// The two parameters a job of this card starts with. +pub const PARAMS : [2]str = ["run", "commit"]; + +/// What the steward writes. +pub const BRANCH_PREFIX : str = "steward/suite-ledger-"; +pub const ISSUE_LABEL : str = "suite-ledger-steward"; +pub const GENERATED_BY : str = "suite ledger steward (specs/jobs/suite_ledger_steward.t27)"; +pub const MERGE_METHOD : str = "squash"; +pub const JOURNAL_PREFIX : str = "suite-ledger:"; + +/// Step kinds by number (specs/queen/jobs.t27: CHECK 0, WAIT 1, EFFECT 2), and the executor each +/// step names. A name the supervisor does not know fails the step: it never guesses. +pub const STEP_COUNT : u32 = 8; +pub const STEP_KIND : [8]u8 = [0, 2, 0, 2, 2, 2, 2, 1]; +pub const STEP_WHAT : [8]str = [ + "steward-run", "steward-refusals-issue", "steward-appliable", "steward-ledger-issue", + "steward-compose", "steward-pull-request", "steward-auto-merge", "steward-merged" +]; + +/// The effect kind each step needs ("" for a CHECK or a WAIT). +pub const STEP_EFFECT : [8]str = ["", "issue", "", "issue", "push", "pull-request", "auto-merge", ""]; + +/// Which suite_ledger_steward.t27 effect code (EF_*) each EFFECT step is; 255 for a CHECK or a WAIT. +/// effect_wanted(run_verdict, code) says whether the step acts or answers PASS with nothing done. +pub const STEP_EF : [8]u8 = [255, 0, 255, 2, 1, 3, 4, 255]; + +/// The refusal issue is the only effect before the appliable CHECK; the ledger issue, the ledger and +/// its PR come only after it, so every check passed at the subject before the first of them +/// (jobs.t27 effect_may_run). +pub const REFUSAL_STEP : u32 = 1; +pub const APPLIABLE_STEP : u32 = 2; +pub const LEDGER_ISSUE_STEP : u32 = 3; +pub const COMPOSE_STEP : u32 = 4; + +/// Whether a step writes the steward's batch: an EFFECT after the appliable CHECK (the ledger issue, +/// the branch, the PR, auto-merge). The refusal issue before it only reports. +pub fn writes_the_repo(step: u32) -> bool { + if (step >= STEP_COUNT) { return false; } + if (STEP_KIND[step] != 2) { return false; } + return step > APPLIABLE_STEP; +} + +/// The suite_ledger_steward.t27 effect code of a step, 255 for a CHECK, a WAIT or a step past the end. +pub fn step_ef(step: u32) -> u8 { + if (step >= STEP_COUNT) { return 255; } + return STEP_EF[step]; +} + +test the_card_writes_the_ledger_only_after_its_checks { + assert writes_the_repo(0) == false; + assert writes_the_repo(REFUSAL_STEP) == false; + assert writes_the_repo(APPLIABLE_STEP) == false; + assert writes_the_repo(LEDGER_ISSUE_STEP) == true; + assert writes_the_repo(COMPOSE_STEP) == true; + assert writes_the_repo(5) == true; + assert writes_the_repo(6) == true; + assert writes_the_repo(7) == false; + assert writes_the_repo(STEP_COUNT) == false; + assert STEP_KIND[0] == 0; + assert STEP_KIND[APPLIABLE_STEP] == 0; + assert STEP_KIND[7] == 1; +} + +test every_effect_step_names_its_effect { + assert step_ef(REFUSAL_STEP) == 0; + assert step_ef(LEDGER_ISSUE_STEP) == 2; + assert step_ef(COMPOSE_STEP) == 1; + assert step_ef(5) == 3; + assert step_ef(6) == 4; + assert step_ef(0) == 255; + assert step_ef(APPLIABLE_STEP) == 255; + assert step_ef(7) == 255; + assert step_ef(STEP_COUNT) == 255; +} + +invariant the_steps_are_ordered { + assert REFUSAL_STEP == 1; + assert APPLIABLE_STEP == 2; + assert LEDGER_ISSUE_STEP == 3; + assert COMPOSE_STEP == 4; + assert COMPOSE_STEP < STEP_COUNT; +}