From 9983c52b654525bb8e8f430483624dfdf3ca6255 Mon Sep 17 00:00:00 2001 From: Dmitrii Fedorov Date: Thu, 15 Oct 2026 12:51:46 -0300 Subject: [PATCH 1/3] spec(port): inject crypto host results into random keypair (Closes #9635) (cherry picked from commit a66fd2987b9f7bff1bf0574796d63c053f2b2ef8) --- .../crates/trios-mesh-node/src/crypto.t27 | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/specs/port/trios/crates/trios-mesh-node/src/crypto.t27 b/specs/port/trios/crates/trios-mesh-node/src/crypto.t27 index d088806ae5..3730bca1c2 100644 --- a/specs/port/trios/crates/trios-mesh-node/src/crypto.t27 +++ b/specs/port/trios/crates/trios-mesh-node/src/crypto.t27 @@ -398,10 +398,12 @@ module port::trios_mesh_node_crypto { // crypto.rs lines 41-50: rand fills 32 bytes and they become the secret // directly -- no stretching, unlike from_seed. The OS randomness is the // parameter here; everything after it is the derivation from_seed tails - // with. - pub fn MeshKeypair_random(entropy: [32]u8) -> MeshKeypair { - const public: [32]u8 = pubkey_from_secret(entropy); - const digest: [32]u8 = sha256_32(public); + // with. The X25519 public key of the entropy and the SHA-256 of that public key + // are the host's results (the header: primitives are declared, never called by a + // test), so they arrive as parameters like the entropy; a body that called the + // undefined primitives read bytes nothing wrote, which t27b's interpreter refuses + // and Zig only hides by filling them. + pub fn MeshKeypair_random(entropy: [32]u8, public: [32]u8, digest: [32]u8) -> MeshKeypair { return keypair_from_public(entropy, public, digest); } @@ -600,8 +602,15 @@ module port::trios_mesh_node_crypto { // lines 43-45: the raw 32 random bytes ARE the secret -- no 0xA3 // layout, no stretching; only from_seed does that. const e: [32]u8 = stretch_seed(6); - const kp: MeshKeypair = MeshKeypair_random(e); + const p: [32]u8 = stretch_seed(7); + const d: [32]u8 = stretch_seed(8); + const kp: MeshKeypair = MeshKeypair_random(e, p, d); assert(arr32_eq(kp.secret, e)); + assert(arr32_eq(kp.public, p)); + assert(kp.secret[0] == 6); + assert(kp.public[0] == 7); + assert(kp.dest_hash[0] == 8); + assert(kp.dest_hash[1] == 0xA3); } test b64_alphabet_table { From 31b384cf09d1614e93a2c6ec092efdfb63ae2d76 Mon Sep 17 00:00:00 2001 From: Dmitrii Fedorov Date: Thu, 15 Oct 2026 16:36:45 -0300 Subject: [PATCH 2/3] spec(t27b): avoid rust_convert CSE hoist and seal crypto (Refs #9632, #9635) --- .../src_port::trios_mesh_node_crypto.json | 28 +++++++++++++++++++ .trinity/seals/t27o_T27oRust.json | 14 +++++----- gen/rust/tools/t27o/rust_convert.rs | 7 +++-- specs/tools/t27o/rust_convert.t27 | 7 +++-- 4 files changed, 44 insertions(+), 12 deletions(-) create mode 100644 .trinity/seals/src_port::trios_mesh_node_crypto.json diff --git a/.trinity/seals/src_port::trios_mesh_node_crypto.json b/.trinity/seals/src_port::trios_mesh_node_crypto.json new file mode 100644 index 0000000000..55f02c9e8e --- /dev/null +++ b/.trinity/seals/src_port::trios_mesh_node_crypto.json @@ -0,0 +1,28 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+cd8a65666", + "closure": [], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:1e74b996ade22e83796910c9b4e244b1cc04f6253a35505054198be62254e853", + "gen_hash_rust": "sha256:ea7c338992c88064b5375c0b5462bb4868f244384f01a344780f025452123335", + "gen_hash_verilog": "sha256:fc2816200338199bc3a3553bfd5fa97ddc9ec7e707af61b23ec096758d38e309", + "gen_hash_zig": "sha256:11c4e273387ec011bd4e7c6a27d1a0217fc821c5c58f1abb7e225a95d9eee469", + "module": "port::trios_mesh_node_crypto", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-15T19:35:12Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:d1d3ed152196c59afbafb1b1c08af5ef6e270fd7e354dc4f101e5bc9dcf212d7", + "spec_path": "specs/port/trios/crates/trios-mesh-node/src/crypto.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 23, + "total": 23, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/.trinity/seals/t27o_T27oRust.json b/.trinity/seals/t27o_T27oRust.json index 4b9ba5d329..30f1e81513 100644 --- a/.trinity/seals/t27o_T27oRust.json +++ b/.trinity/seals/t27o_T27oRust.json @@ -1,17 +1,17 @@ { - "built_by": "t27c-bootstrap@0.5.2+e7fbc2639", + "built_by": "t27c-bootstrap@0.5.2+cd8a65666", "closure": [], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:5ced192099954e788bc953c0973428c9f278751b7610f050e07758a9a6611a14", - "gen_hash_rust": "sha256:ae84f2ed194de288b42f9dfeb10b6a965c65f99ca992ef82aaf971082aaca512", - "gen_hash_verilog": "sha256:130434cc65aee3c2c38a14354c010aedbfd11c6e2e565a2da72448ca8a471d17", - "gen_hash_zig": "sha256:a3aee0b8ec566bb21157cb64c6330e87ffcb44ce765a2bf150beb95dd0c9b2ab", + "gen_hash_c": "sha256:93076da93a404ea49f455526fa1d25dfc8b6040dda6f2972dcb747074eb755a3", + "gen_hash_rust": "sha256:d912c313830e2ec4ba390adcf66baabba71cecd6f720246e1a619a95b0964334", + "gen_hash_verilog": "sha256:2b7550a7c7d5e0f989df3e4a00597c788e5abc0671043978bef8bd4cfd40aa9c", + "gen_hash_zig": "sha256:a47e14e956324ccd1ff1d9f521f2761b659ee6e61623c53365af62043c731264", "module": "T27oRust", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-12T10:09:28Z", + "sealed_at": "2026-10-15T19:29:34Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:f4ee9bcc7818621bf5d591d8d74f6cb41ef6fcac3e558e550af6dc45d549aec5", + "spec_hash": "sha256:690282a6a0c834606de0def8b4b05499c1a0e415bc270ffac2d908bc3ca5abbf", "spec_path": "specs/tools/t27o/rust_convert.t27", "tests": { "failed": 0, diff --git a/gen/rust/tools/t27o/rust_convert.rs b/gen/rust/tools/t27o/rust_convert.rs index 199a90f884..99102edd9f 100644 --- a/gen/rust/tools/t27o/rust_convert.rs +++ b/gen/rust/tools/t27o/rust_convert.rs @@ -7262,7 +7262,7 @@ pub fn out_format(src: &[u8], st: &mut [usize], out: &mut [u8], a: usize, ret: b } let fq: usize = quoted_end(src, f); let mut p: usize = (f + 1); - let mut piece: usize = (f + 1); + let mut piece: usize = p; let mut arg: usize = skip_ws(src, fq); if tok_is(src, arg, b",") { arg = skip_ws(src, tok_end(src, arg)); @@ -7310,8 +7310,9 @@ pub fn out_format(src: &[u8], st: &mut [usize], out: &mut [u8], a: usize, ret: b refuse(st, R_STRUSE, a, a, fe); return (); } - if ((fq - 1) > piece) { - put_out_piece(src, st, out, piece, (fq - 1)); + let tail_end: usize = (fq - 1); + if (tail_end > piece) { + put_out_piece(src, st, out, piece, tail_end); newline(st, out); } st[(P) as usize] = skip_ws(src, rp); diff --git a/specs/tools/t27o/rust_convert.t27 b/specs/tools/t27o/rust_convert.t27 index 170da2ed90..46e6de8a35 100644 --- a/specs/tools/t27o/rust_convert.t27 +++ b/specs/tools/t27o/rust_convert.t27 @@ -6206,8 +6206,10 @@ pub fn out_format(src: []const u8, st: []usize, out: []u8, a: usize, ret: bool) const f : usize = skip_ws(src, lp + 1); if (!str_tok(src, f)) { refuse(st, R_STRUSE, a, a, fe); return; } const fq : usize = quoted_end(src, f); + // `f + 1` is spelled once: repeated, it became a `_cse` temporary that t27c writes above `const f` + // (t27b: FnDecl(reference CSE hoist), #9632). var p : usize = f + 1; - var piece : usize = f + 1; + var piece : usize = p; // the arguments start after the format string's comma: format!(FMT, a0, a1, ..) var arg : usize = skip_ws(src, fq); if (tok_is(src, arg, ",")) { arg = skip_ws(src, tok_end(src, arg)); } @@ -6240,7 +6242,8 @@ pub fn out_format(src: []const u8, st: []usize, out: []u8, a: usize, ret: bool) refuse(st, R_STRUSE, a, a, fe); return; } - if (fq - 1 > piece) { put_out_piece(src, st, out, piece, fq - 1); newline(st, out); } + const tail_end : usize = fq - 1; + if (tail_end > piece) { put_out_piece(src, st, out, piece, tail_end); newline(st, out); } st[P] = skip_ws(src, rp); if (ret) { puts(st, out, "return t27o_w;"); } } From d8229d9fafe5d78b6a49f4fc91213f2fd91c225b Mon Sep 17 00:00:00 2001 From: Dmitrii Fedorov Date: Thu, 15 Oct 2026 16:36:54 -0300 Subject: [PATCH 3/3] ci(t27b): distinguish PR ledger lag from runtime defects (Refs #9600) --- .github/workflows/t27b-native.yml | 6 +- .trinity/seals/t27b_T27bSteward.json | 19 ++--- gen/c/tri/t27b/steward.c | 102 ++++++++++++++++++++++++++- scripts/tri_loop/t27b.py | 26 ++++--- scripts/tri_loop/t27b_rules.py | 8 +-- specs/tri/t27b/steward.t27 | 68 ++++++++++++++++++ 6 files changed, 199 insertions(+), 30 deletions(-) diff --git a/.github/workflows/t27b-native.yml b/.github/workflows/t27b-native.yml index 75bad76bf6..85f7c5efc1 100644 --- a/.github/workflows/t27b-native.yml +++ b/.github/workflows/t27b-native.yml @@ -260,11 +260,13 @@ jobs: - name: tri t27b ratchet against the ledger id: ratchet + env: + PR_FLAG: ${{ github.event_name == 'pull_request' && '--pr' || '' }} run: | set +e - ./scripts/tri t27b ratchet --run run.json --json > ratchet.json 2> ratchet.err + ./scripts/tri t27b ratchet --run run.json $PR_FLAG --json > ratchet.json 2> ratchet.err code=$? - ./scripts/tri t27b ratchet --run run.json > ratchet.txt 2>&1 + ./scripts/tri t27b ratchet --run run.json $PR_FLAG > ratchet.txt 2>&1 cat ratchet.txt cat ratchet.err echo "exit=$code" >> "$GITHUB_OUTPUT" diff --git a/.trinity/seals/t27b_T27bSteward.json b/.trinity/seals/t27b_T27bSteward.json index 203ff7016f..e717f77278 100644 --- a/.trinity/seals/t27b_T27bSteward.json +++ b/.trinity/seals/t27b_T27bSteward.json @@ -1,24 +1,25 @@ { - "built_by": "t27c-bootstrap@0.5.2+0d573722c", + "built_by": "t27c-bootstrap@0.5.2+cd8a65666", "closure": [], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:c699bc3ab8e8e01af1729ea96725a3abc2a8e6a85c88d5644fe30978e2fa57ee", - "gen_hash_rust": "sha256:0c6fe0756c745a0ff553e141c197f6535107ce71d8f8f556d70b31a6b04a11db", - "gen_hash_verilog": "sha256:eb7f9f6aecff876331ea1ad8fbdf9d32d55af1bef22d379eff01216d98adef76", - "gen_hash_zig": "sha256:db0e1e6532a57d2ba0c6559f001812827cfc8fc677876747c84848068af60b7e", + "gen_hash_c": "sha256:042f0a9f08534cdde91942cc7c3c0e8ce94134e6e9f6ceacf1aaadcb29f91de9", + "gen_hash_rust": "sha256:5d4af985fc5c471ad4e3bba71643067ccd7cb93de1372cdc9a2c3cca73dd13f6", + "gen_hash_verilog": "sha256:a9ba4ed46258687262c9e17669107da71c184e27f71ef73e65f1679da4b10d63", + "gen_hash_zig": "sha256:4eb8cadfd3dfc70296f06b8ca4f34c4a9ef9600fc262354fdb1fe5c5a0426fe7", "module": "T27bSteward", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-09T21:34:31Z", + "sealed_at": "2026-10-15T19:29:16Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:70867c8cd8a8155d82f352b6833168f04c846a736413d6b2420d54774994123e", + "spec_hash": "sha256:e302b1c3cb8c988982f01fb092a62758ca68996a61bb64f6b437b336b486e23f", "spec_path": "specs/tri/t27b/steward.t27", "tests": { "failed": 0, "failing": [], "forced": false, - "passed": 128, - "total": 128 + "passed": 137, + "total": 137, + "vacuous": 0 }, "toolchain": { "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", diff --git a/gen/c/tri/t27b/steward.c b/gen/c/tri/t27b/steward.c index 634b91362e..770218af93 100644 --- a/gen/c/tri/t27b/steward.c +++ b/gen/c/tri/t27b/steward.c @@ -28,6 +28,7 @@ bool unlisted(uint8_t reference, bool listed); bool over_cap(uint32_t not_pass, uint32_t cap, bool has_cap); bool ratchet_is_red(uint8_t code); bool is_unimplemented(uint8_t v); +bool ratchet_red(uint8_t code, uint8_t got, bool pr); uint8_t bless_reason(uint8_t got, uint8_t kept); bool cap_rises(uint32_t not_pass, uint32_t old_cap, bool has_old); bool lab_stale(uint32_t age_min, uint32_t limit_min); @@ -222,6 +223,34 @@ bool is_unimplemented(uint8_t v) { return false; } +bool ratchet_red(uint8_t code, uint8_t got, bool pr) { + if ((pr == false)) { + return ratchet_is_red(code); + } + if ((code == 2)) { + return true; + } + if ((code == 8)) { + return true; + } + if ((code == 9)) { + return true; + } + if ((code > 9)) { + return true; + } + if ((code == 7)) { + if (is_pass(got)) { + return false; + } + if (is_unimplemented(got)) { + return false; + } + return true; + } + return false; +} + uint8_t bless_reason(uint8_t got, uint8_t kept) { if ((kept != 0)) { return kept; @@ -469,6 +498,14 @@ uint32_t with_tests(uint32_t reference, uint32_t vacuous) { /* invariant: no_total_in_the_ledger_header */ /* invariant no_total_in_the_ledger_header is not a C constant expression: (header_stored(5) == false) */ +/* invariant: strict_ratchet_red_is_ratchet_is_red */ +/* invariant strict_ratchet_red_is_ratchet_is_red is not a C constant expression: (ratchet_red(0, 6, false) == ratchet_is_red(0)) */ +/* invariant strict_ratchet_red_is_ratchet_is_red is not a C constant expression: (ratchet_red(2, 0, false) == ratchet_is_red(2)) */ +/* invariant strict_ratchet_red_is_ratchet_is_red is not a C constant expression: (ratchet_red(3, 0, false) == ratchet_is_red(3)) */ +/* invariant strict_ratchet_red_is_ratchet_is_red is not a C constant expression: (ratchet_red(5, 0, false) == ratchet_is_red(5)) */ +/* invariant strict_ratchet_red_is_ratchet_is_red is not a C constant expression: (ratchet_red(7, 0, false) == ratchet_is_red(7)) */ +/* invariant strict_ratchet_red_is_ratchet_is_red is not a C constant expression: (ratchet_red(8, 0, false) == ratchet_is_red(8)) */ + /* invariant: gained_never_red */ /* invariant gained_never_red is not a C constant expression: (delta_is_red(delta_code(0, 0, 2, 0, 0, 1)) == false) */ @@ -613,6 +650,60 @@ void test_ratchet_red_codes(void) { assert((ratchet_is_red(6) == false)); } +void test_pr_lag_is_pending(void) { + assert((ratchet_red(7, 0, true) == false)); + assert((ratchet_red(7, 1, true) == false)); + assert((ratchet_red(7, 2, true) == false)); + assert((ratchet_red(7, 3, true) == false)); + assert((ratchet_red(7, 4, true) == false)); + assert((ratchet_red(3, 0, true) == false)); + assert((ratchet_red(4, 2, true) == false)); + assert((ratchet_red(5, 0, true) == false)); + assert((ratchet_red(1, 1, true) == false)); + assert((ratchet_red(6, 0, true) == false)); + assert((ratchet_red(0, 0, true) == false)); +} + +void test_negative_pr_unlisted_mismatch_is_red(void) { + assert(ratchet_red(7, 6, true)); +} + +void test_negative_pr_unlisted_crash_is_red(void) { + assert(ratchet_red(7, 7, true)); +} + +void test_negative_pr_unlisted_fail_is_red(void) { + assert(ratchet_red(7, 5, true)); +} + +void test_negative_pr_unlisted_timeout_is_red(void) { + assert(ratchet_red(7, 8, true)); +} + +void test_negative_pr_unlisted_not_run_is_red(void) { + assert(ratchet_red(7, 9, true)); +} + +void test_negative_pr_unlisted_missing_is_red(void) { + assert(ratchet_red(7, 10, true)); +} + +void test_negative_pr_regression_is_red(void) { + assert(ratchet_red(2, 2, true)); + assert(ratchet_red(2, 0, true)); + assert(ratchet_red(8, 0, true)); + assert(ratchet_red(9, 0, true)); + assert(ratchet_red(10, 0, true)); +} + +void test_master_and_the_lab_stay_strict(void) { + assert(ratchet_red(7, 0, false)); + assert(ratchet_red(7, 6, false)); + assert(ratchet_red(3, 0, false)); + assert(ratchet_red(5, 0, false)); + assert((ratchet_red(4, 2, false) == false)); +} + void test_bless_keeps_a_written_reason(void) { assert_eq(bless_reason(5, 2), 2); } @@ -1048,6 +1139,15 @@ int main(void) { test_ratchet_unlisted(); test_ratchet_cap(); test_ratchet_red_codes(); + test_pr_lag_is_pending(); + test_negative_pr_unlisted_mismatch_is_red(); + test_negative_pr_unlisted_crash_is_red(); + test_negative_pr_unlisted_fail_is_red(); + test_negative_pr_unlisted_timeout_is_red(); + test_negative_pr_unlisted_not_run_is_red(); + test_negative_pr_unlisted_missing_is_red(); + test_negative_pr_regression_is_red(); + test_master_and_the_lab_stay_strict(); test_bless_keeps_a_written_reason(); test_bless_unimplemented(); test_bless_refuses_a_defect(); @@ -1145,7 +1245,7 @@ int main(void) { test_ledger_stores_where_it_came_from(); test_ledger_derives_its_counts(); test_ledger_stores_no_unknown_field(); - printf("All %d tests passed.\n", 128); + printf("All %d tests passed.\n", 137); return 0; } #endif /* T27_TEST_MAIN */ diff --git a/scripts/tri_loop/t27b.py b/scripts/tri_loop/t27b.py index 53a05a62bf..2d1289ebdb 100644 --- a/scripts/tri_loop/t27b.py +++ b/scripts/tri_loop/t27b.py @@ -190,12 +190,10 @@ (`unimplemented` | `reference-bug` | `n/a`). `ratchet` diffs one lab run (latest.json shape) against it: - UNEXPECTED FAILURE a ledger pass that is not a pass now (a pass that turned - vacuous included); a ledger pass_vacuous that no longer - passes at all + UNEXPECTED FAILURE a ledger pass that is not a pass now (vacuous included); + a ledger pass_vacuous that no longer passes at all UNEXPECTED PASS a ledger non-pass that passes now; a pass_vacuous that - is a real pass now. Red too: an improvement nobody - blesses leaves slack for the next regression + is a real pass now. Red: an unblessed gain leaves slack UNLISTED the reference passes a spec the ledger does not name STALE a ledger spec the reference now fails, or that is gone OVER CAP more non-pass entries than `max_not_pass`, which only @@ -203,17 +201,16 @@ BAD REASON a non-pass entry whose reason is not one of the three -- not red -- MOVED still not a pass, but the first blocker changed - UNJUDGED the reference could not judge the spec in this run - (lab_error, timeout, skip): no verdict either way - VACUITY MEASURED a ledger pass blessed from a run that did not count - asserts (source.asserts_counted false) is pass_vacuous - in a run that does: a first measurement, not a - regression. Bless to record it + UNJUDGED the reference gave no verdict (lab_error, timeout, skip) + VACUITY MEASURED a ledger pass blessed before asserts were counted is + pass_vacuous in a run that counts: a first measurement, + not a regression. Bless to record it tri t27b ratchet # latest lab run vs the ledger tri t27b ratchet --run runs/.json # a saved run (path or URL) tri t27b ratchet --bless # rewrite the ledger from the run tri t27b ratchet --json # the verdict, machine-readable + tri t27b ratchet --pr # a PR: lag pending, a defect red Exit 0 green, 1 red (or a refused bless), 2 usage or an unreadable input. """ @@ -876,7 +873,7 @@ def ratchet(run, ledger): """ r = rules() found = [] - add = lambda kind, path, what: found.append({"kind": kind, "path": path, "what": what}) # noqa: E731 + add = lambda kind, path, what, t27b=None: found.append({"kind": kind, "path": path, "what": what, "t27b": t27b}) # noqa: E731 by_path = {x.get("file"): x for x in run["results"]} entries = {e["path"]: e for e in ledger.get("entries", [])} # A ledger blessed from a run without assert counts cannot tell pass from @@ -916,7 +913,7 @@ def ratchet(run, ledger): if r.unlisted(rec.get("reference") or "missing", path in entries): got, blocker = observed(rec) add("UNLISTED", path, f"the reference passes it and the ledger does not name it (t27b {got}" - + (f": {blocker})" if blocker else ")")) + + (f": {blocker})" if blocker else ")"), got) not_pass = sum(1 for e in entries.values() if not r.is_pass(e.get("t27b") or "missing")) cap = ledger.get("max_not_pass") if r.over_cap(not_pass, cap): @@ -1020,6 +1017,7 @@ def ratchet_main(argv): ap.add_argument("--bless", action="store_true", help="rewrite the ledger from the run") ap.add_argument("--accept-new", action="store_true", help="bless: let the cap rise by exactly the non-pass specs new to the ledger") + ap.add_argument("--pr", action="store_true", help="a pull request: lag is pending, a runtime defect stays red") ap.add_argument("--json", action="store_true") try: args = ap.parse_args(argv) @@ -1059,7 +1057,7 @@ def ratchet_main(argv): try: found = ratchet(run, old) counts = {k: sum(1 for f in found if f["kind"] == k) for k in KINDS} - red = sum(v for k, v in counts.items() if rules().ratchet_is_red(k)) + red = sum(1 for f in found if rules().ratchet_is_red(f["kind"], f["t27b"] or "pass", args.pr)) except Exception as e: # noqa: BLE001 -- RulesUnavailable lives in a lazily imported module if type(e).__name__ != "RulesUnavailable": raise diff --git a/scripts/tri_loop/t27b_rules.py b/scripts/tri_loop/t27b_rules.py index bfdf997b6f..7f500eb209 100644 --- a/scripts/tri_loop/t27b_rules.py +++ b/scripts/tri_loop/t27b_rules.py @@ -94,8 +94,8 @@ def _build(): so.unlisted.restype = ctypes.c_bool so.over_cap.argtypes = [ctypes.c_uint32, ctypes.c_uint32, ctypes.c_bool] so.over_cap.restype = ctypes.c_bool - so.ratchet_is_red.argtypes = [ctypes.c_uint8] - so.ratchet_is_red.restype = ctypes.c_bool + so.ratchet_red.argtypes = [ctypes.c_uint8, ctypes.c_uint8, ctypes.c_bool] + so.ratchet_red.restype = ctypes.c_bool so.bless_reason.argtypes = [ctypes.c_uint8, ctypes.c_uint8] so.bless_reason.restype = ctypes.c_uint8 so.cap_rises.argtypes = [ctypes.c_uint32, ctypes.c_uint32, ctypes.c_bool] @@ -189,8 +189,8 @@ def over_cap(not_pass, cap): return bool(lib().over_cap(not_pass, cap if has else 0, has)) -def ratchet_is_red(kind): - return bool(lib().ratchet_is_red(RATCHETS.index(kind))) +def ratchet_is_red(kind, t27b="pass", pr=False): + return bool(lib().ratchet_red(RATCHETS.index(kind), verdict(t27b), bool(pr))) def bless_reason(got, kept): diff --git a/specs/tri/t27b/steward.t27 b/specs/tri/t27b/steward.t27 index 62682107a9..7b430f6206 100644 --- a/specs/tri/t27b/steward.t27 +++ b/specs/tri/t27b/steward.t27 @@ -149,6 +149,29 @@ pub fn is_unimplemented(v: u8) -> bool { return false; } +// Is one ratchet finding red? `got` is t27b's verdict on that spec (the lab's code; 0 when the +// finding has none). `pr` false is ratchet_is_red: master and the lab stay strict, because the +// steward job starts only from a red master ratchet (ledger_steward.t27 run_starts_job). +// `pr` true is a pull request, as specs/ci/derived_data.t27 ledger_code_verdict reads it (#9600): +// lag is pending, not red -- UNEXPECTED PASS (3), MOVED (4), STALE (5) and an UNLISTED spec t27b +// passes or cannot compile yet (is_pass, is_unimplemented) -- because the refresh bot owes the row. +// A runtime defect is never lag: an UNLISTED spec t27b fails, mismatches, crashes or times out on +// (the steward refuses it too, ledger_steward.t27 RR_DEFECT) stays red, and so do UNEXPECTED +// FAILURE (2), OVER CAP (8), BAD REASON (9) and a code this file does not know. +pub fn ratchet_red(code: u8, got: u8, pr: bool) -> bool { + if (pr == false) { return ratchet_is_red(code); } + if (code == 2) { return true; } + if (code == 8) { return true; } + if (code == 9) { return true; } + if (code > 9) { return true; } + if (code == 7) { + if (is_pass(got)) { return false; } + if (is_unimplemented(got)) { return false; } + return true; + } + return false; +} + // The reason bless writes for a non-pass entry: the one a human wrote, else // UNIMPLEMENTED for a construct t27b rejects, else NONE (bless refuses). pub fn bless_reason(got: u8, kept: u8) -> u8 { @@ -418,6 +441,41 @@ test ratchet_red_codes { assert(ratchet_is_red(4) == false); assert(ratchet_is_red(6) == false); } +// A pull request (#9600): lag is pending, a runtime defect is red. got: 0 pass, 1 pass_vacuous, +// 2 blocked, 3 frontend, 4 codegen, 5 fail, 6 mismatch, 7 crash, 8 timeout, 9 not run, 10 missing. +test pr_lag_is_pending { + assert(ratchet_red(7, 0, true) == false); + assert(ratchet_red(7, 1, true) == false); + assert(ratchet_red(7, 2, true) == false); + assert(ratchet_red(7, 3, true) == false); + assert(ratchet_red(7, 4, true) == false); + assert(ratchet_red(3, 0, true) == false); + assert(ratchet_red(4, 2, true) == false); + assert(ratchet_red(5, 0, true) == false); + assert(ratchet_red(1, 1, true) == false); + assert(ratchet_red(6, 0, true) == false); + assert(ratchet_red(0, 0, true) == false); +} +test negative_pr_unlisted_mismatch_is_red { assert(ratchet_red(7, 6, true)); } +test negative_pr_unlisted_crash_is_red { assert(ratchet_red(7, 7, true)); } +test negative_pr_unlisted_fail_is_red { assert(ratchet_red(7, 5, true)); } +test negative_pr_unlisted_timeout_is_red { assert(ratchet_red(7, 8, true)); } +test negative_pr_unlisted_not_run_is_red { assert(ratchet_red(7, 9, true)); } +test negative_pr_unlisted_missing_is_red { assert(ratchet_red(7, 10, true)); } +test negative_pr_regression_is_red { + assert(ratchet_red(2, 2, true)); + assert(ratchet_red(2, 0, true)); + assert(ratchet_red(8, 0, true)); + assert(ratchet_red(9, 0, true)); + assert(ratchet_red(10, 0, true)); +} +test master_and_the_lab_stay_strict { + assert(ratchet_red(7, 0, false)); + assert(ratchet_red(7, 6, false)); + assert(ratchet_red(3, 0, false)); + assert(ratchet_red(5, 0, false)); + assert(ratchet_red(4, 2, false) == false); +} test bless_keeps_a_written_reason { assert_eq(bless_reason(5, 2), 2); } test bless_unimplemented { assert_eq(bless_reason(3, 0), 1); } test bless_refuses_a_defect { assert_eq(bless_reason(6, 0), 0); } @@ -546,6 +604,16 @@ invariant no_total_in_the_ledger_header { assert(header_stored(5) == false); } +// The strict reading never changes under pr=false, whatever t27b said. +invariant strict_ratchet_red_is_ratchet_is_red { + assert(ratchet_red(0, 6, false) == ratchet_is_red(0)); + assert(ratchet_red(2, 0, false) == ratchet_is_red(2)); + assert(ratchet_red(3, 0, false) == ratchet_is_red(3)); + assert(ratchet_red(5, 0, false) == ratchet_is_red(5)); + assert(ratchet_red(7, 0, false) == ratchet_is_red(7)); + assert(ratchet_red(8, 0, false) == ratchet_is_red(8)); +} + invariant gained_never_red { assert(delta_is_red(delta_code(0, 0, 2, 0, 0, 1)) == false); }