diff --git a/.trinity/seals/claw_ClawGates.json b/.trinity/seals/claw_ClawGates.json index 13c30cb979..9beed58429 100644 --- a/.trinity/seals/claw_ClawGates.json +++ b/.trinity/seals/claw_ClawGates.json @@ -7,23 +7,23 @@ } ], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:ce0738bca2f5180ee4534277adba4c639bfbcd3f996d67aed18f8b11c046f683", - "gen_hash_rust": "sha256:39159b221533f17be9fb1ff4eb4ce7354436fb594275513c4e435fd1b2824df2", - "gen_hash_verilog": "sha256:e41e2a573f0a4bab0fe16018391059a845bd636c600364c4fdb011aa2ae6f516", - "gen_hash_zig": "sha256:9b9d65386abd4c7eaffac3508cd2881b01863d0769d2f28066cc1cd51b892dfc", + "gen_hash_c": "sha256:723a598914ee23e57be303db50d42531cc4e060b0dc2f4cb56234e53ef1f545c", + "gen_hash_rust": "sha256:a959e6e61dbce9d00050932baed8e74633a5ce6e4a6dc376f9ee3c5494445473", + "gen_hash_verilog": "sha256:27185ecb4aa7e109f3c9fb7280863ac2fff7f4262bf8b02b9c3177612079580f", + "gen_hash_zig": "sha256:d96163a4182c592c121c7cf497d5770791f41fb7fb382300b2d79dee3ef3c79e", "module": "ClawGates", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T21:37:24Z", + "sealed_at": "2026-10-18T22:24:12Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:96a1d6b79b1832f7ee063270a9c851793fe1100b7981d6d3985c881b61e60bcb", + "spec_hash": "sha256:1976cf9af48f8799d5d7584648c3cca97ca35d0ccd31b5019b0a1fed909f1e90", "spec_path": "specs/claw/gates.t27", "tests": { "failed": 0, "failing": [], "forced": false, - "passed": 20, - "total": 20, + "passed": 23, + "total": 23, "vacuous": 0 }, "toolchain": { diff --git a/gen/c/claw/gates.c b/gen/c/claw/gates.c index 37b48b03c5..a1f4491a12 100644 --- a/gen/c/claw/gates.c +++ b/gen/c/claw/gates.c @@ -53,8 +53,11 @@ uint8_t class_of(const char* name, size_t name_len); bool is_blocking(const char* name, size_t name_len); const char* events_of(const char* name, size_t name_len); uint32_t count_class(uint8_t c); +bool rows_filled(const char* names[static 67], const char* events[static 67]); bool every_row_filled(void); +bool names_unique_in(const char* names[static 67], size_t lens[static 67]); bool all_names_unique(void); +bool classes_known(uint8_t cl[static 67]); bool all_classes_known(void); size_t line_len(uint8_t* dir_text, size_t dir_len, size_t start); bool line_eq_name(uint8_t* dir_text, size_t start, size_t len, const char* name, size_t name_len); @@ -104,22 +107,26 @@ uint32_t count_class(uint8_t c) { return n; } -bool every_row_filled(void) { +bool rows_filled(const char* names[static 67], const char* events[static 67]) { for (size_t i = 0; i < 67; i++) { - if ((NAMES[i] == "")) { + if ((names[i] == "")) { return false; } - if ((EVENTS[i] == "")) { + if ((events[i] == "")) { return false; } } return true; } -bool all_names_unique(void) { +bool every_row_filled(void) { + return rows_filled(NAMES, EVENTS); +} + +bool names_unique_in(const char* names[static 67], size_t lens[static 67]) { for (size_t i = 0; i < 67; i++) { for (size_t j = (i + 1); j < 67; j++) { - if (str_eq(NAMES[i], NAME_LENS[i], NAMES[j], NAME_LENS[j])) { + if (str_eq(names[i], lens[i], names[j], lens[j])) { return false; } } @@ -127,11 +134,15 @@ bool all_names_unique(void) { return true; } -bool all_classes_known(void) { +bool all_names_unique(void) { + return names_unique_in(NAMES, NAME_LENS); +} + +bool classes_known(uint8_t cl[static 67]) { for (size_t i = 0; i < 67; i++) { - if ((CLASSES[i] != G_BLOCKING)) { - if ((CLASSES[i] != G_SOFT)) { - if ((CLASSES[i] != G_REPORTING)) { + if ((cl[i] != G_BLOCKING)) { + if ((cl[i] != G_SOFT)) { + if ((cl[i] != G_REPORTING)) { return false; } } @@ -140,6 +151,10 @@ bool all_classes_known(void) { return true; } +bool all_classes_known(void) { + return classes_known(CLASSES); +} + size_t line_len(uint8_t* dir_text, size_t dir_len, size_t start) { size_t i = start; while ((i < dir_len)) { @@ -588,6 +603,63 @@ void test_coverage_report_lines_are_exact(void) { assert((buf_has(&out, w, "G_REPORTING n=2 blocking=false e.g. auto-merge-ready-prs, queen-publish\n", 72) == true)); } +void test_a_hole_in_either_column_fails_the_filled_check(void) { + assert((rows_filled(NAMES, EVENTS) == true)); + const char* n[67] = {0}; + for (size_t i = 0; i < 67; i++) { + n[i] = NAMES[i]; + } + n[66] = ""; + assert((rows_filled(n, EVENTS) == false)); + const char* e[67] = {0}; + for (size_t i = 0; i < 67; i++) { + e[i] = EVENTS[i]; + } + e[0] = ""; + assert((rows_filled(NAMES, e) == false)); +} + +void test_a_repeated_name_is_caught_wherever_it_sits(void) { + const char* n[67] = {0}; + for (size_t i = 0; i < 67; i++) { + n[i] = NAMES[i]; + } + size_t l[67] = {0}; + for (size_t i = 0; i < 67; i++) { + l[i] = NAME_LENS[i]; + } + n[5] = n[4]; + l[5] = l[4]; + assert((names_unique_in(n, l) == false)); + const char* m[67] = {0}; + for (size_t i = 0; i < 67; i++) { + m[i] = NAMES[i]; + } + size_t k[67] = {0}; + for (size_t i = 0; i < 67; i++) { + k[i] = NAME_LENS[i]; + } + m[66] = m[0]; + k[66] = k[0]; + assert((names_unique_in(m, k) == false)); +} + +void test_a_class_outside_the_three_is_unknown(void) { + assert((classes_known(CLASSES) == true)); + uint8_t c[67] = {0}; + for (size_t i = 0; i < 67; i++) { + c[i] = CLASSES[i]; + } + c[66] = G_UNKNOWN; + assert((classes_known(c) == false)); + c[66] = G_BLOCKING; + assert((classes_known(c) == true)); + c[66] = G_SOFT; + assert((classes_known(c) == true)); + c[66] = G_REPORTING; + assert((classes_known(c) == true)); +} + /* ------------------------------------------------------- Test runner (compile with -DT27_TEST_MAIN to execute) @@ -616,7 +688,10 @@ int main(void) { test_coverage_report_carries_every_class(); test_audit_tail_line_matches_the_count(); test_coverage_report_lines_are_exact(); - printf("All %d tests passed.\n", 20); + test_a_hole_in_either_column_fails_the_filled_check(); + test_a_repeated_name_is_caught_wherever_it_sits(); + test_a_class_outside_the_three_is_unknown(); + printf("All %d tests passed.\n", 23); return 0; } #endif /* T27_TEST_MAIN */ diff --git a/specs/claw/gates.t27 b/specs/claw/gates.t27 index f0b0256d33..1ede4a9be4 100644 --- a/specs/claw/gates.t27 +++ b/specs/claw/gates.t27 @@ -149,30 +149,42 @@ pub fn count_class(c: u8) -> u32 { return n; } -/// Every row has a name and a recorded trigger set. -pub fn every_row_filled() -> bool { +/// Every row of a table shaped like this one has a name and a recorded trigger set. The +/// columns are parameters so a test can hand in a copy with one hole: a check that only reads +/// the constant table can never fail, and no mutant of it can die (#10686). +pub fn rows_filled(names: [67]str, events: [67]str) -> bool { for i in 0..67 { - if NAMES[i] == "" { return false; } - if EVENTS[i] == "" { return false; } + if names[i] == "" { return false; } + if events[i] == "" { return false; } } return true; } -pub fn all_names_unique() -> bool { +/// Every row of the inventory has a name and a recorded trigger set. +pub fn every_row_filled() -> bool { + return rows_filled(NAMES, EVENTS); +} + +/// No name appears twice in a name column (with its length column). +pub fn names_unique_in(names: [67]str, lens: [67]usize) -> bool { for i in 0..67 { for j in (i + 1)..67 { - if str_eq(NAMES[i], NAME_LENS[i], NAMES[j], NAME_LENS[j]) { return false; } + if str_eq(names[i], lens[i], names[j], lens[j]) { return false; } } } return true; } -/// Every class literal in CLASSES is one of the three real classes. -pub fn all_classes_known() -> bool { +pub fn all_names_unique() -> bool { + return names_unique_in(NAMES, NAME_LENS); +} + +/// Every class in a class column is one of the three real classes. +pub fn classes_known(cl: [67]u8) -> bool { for i in 0..67 { - if CLASSES[i] != G_BLOCKING { - if CLASSES[i] != G_SOFT { - if CLASSES[i] != G_REPORTING { + if cl[i] != G_BLOCKING { + if cl[i] != G_SOFT { + if cl[i] != G_REPORTING { return false; } } @@ -181,6 +193,11 @@ pub fn all_classes_known() -> bool { return true; } +/// Every class literal in CLASSES is one of the three real classes. +pub fn all_classes_known() -> bool { + return classes_known(CLASSES); +} + // --------------------------------------------------------------------------- // The audit law (T2, Refs #9271): does the live .github/workflows directory // agree with this inventory? The runner the gate-topology workflow compiles @@ -597,3 +614,47 @@ test coverage_report_lines_are_exact { assert buf_has(&out, w, "G_SOFT n=3 blocking=false e.g. oracle-nightly, queen-doctor, rings-rust\n", 72) == true; assert buf_has(&out, w, "G_REPORTING n=2 blocking=false e.g. auto-merge-ready-prs, queen-publish\n", 72) == true; } + +test a_hole_in_either_column_fails_the_filled_check { + assert rows_filled(NAMES, EVENTS) == true; + var n : [67]str = undefined; + for i in 0..67 { n[i] = NAMES[i]; } + n[66] = ""; + assert rows_filled(n, EVENTS) == false; + var e : [67]str = undefined; + for i in 0..67 { e[i] = EVENTS[i]; } + e[0] = ""; + assert rows_filled(NAMES, e) == false; +} + +test a_repeated_name_is_caught_wherever_it_sits { + var n : [67]str = undefined; + for i in 0..67 { n[i] = NAMES[i]; } + var l : [67]usize = undefined; + for i in 0..67 { l[i] = NAME_LENS[i]; } + n[5] = n[4]; + l[5] = l[4]; + assert names_unique_in(n, l) == false; + var m : [67]str = undefined; + for i in 0..67 { m[i] = NAMES[i]; } + var k : [67]usize = undefined; + for i in 0..67 { k[i] = NAME_LENS[i]; } + m[66] = m[0]; + k[66] = k[0]; + assert names_unique_in(m, k) == false; +} + +test a_class_outside_the_three_is_unknown { + assert classes_known(CLASSES) == true; + var c : [67]u8 = undefined; + for i in 0..67 { c[i] = CLASSES[i]; } + c[66] = G_UNKNOWN; + assert classes_known(c) == false; + // Each of the three real classes passes on its own, so no one of the three checks is spare. + c[66] = G_BLOCKING; + assert classes_known(c) == true; + c[66] = G_SOFT; + assert classes_known(c) == true; + c[66] = G_REPORTING; + assert classes_known(c) == true; +}