Three things that could not fail or could not be seen: duplicate agreement, seal coverage, and 348 specs that do not compile

.claude/skills/ci-gates/SKILL.md

@@ -128,6 +128,48 @@ The workflow's `name:` may change freely. `jobs.<id>:` may not.
 When `repos/:owner/:repo/branches/master/protection` returns nothing useful, read the
 contexts off a recently merged PR: `gh pr checks <N> | awk '{print $1}' | sort -u`.
 
+## 7. When a scan says something alarming, re-derive it a second way before writing it down
+
+Four times in one session an anomaly came from the instrument rather than the thing
+measured. Every one would have been reported as a fact about the repository.
+
+| what the instrument said | what was true | why it lied |
+|---|---|---|
+| "two of four optima are not identified" | the opposite — all four narrow, mutually incompatible | `depth` measured the gap to the nearest **grid point**, so it ranked the grids |
+| "`tmul` has diverged across the BitNet family" | all 15 copies are one function | a regex ending at `\n}` swallowed five definitions in a spec written on one line; and `if(ta==1)` vs `if (ta == 1)` hash differently |
+| Verilog arm silently narrower than C and Rust | caught before it ran | the testbench generator sliced every argument `[7:0]`, hardcoded, while `sign0` takes `i16` |
+| "73 seals reference specs that never existed" | **15** | `git log --diff-filter=D -- <exact path>` only sees a deletion recorded at that path; by basename across all history the count is a fifth of that |
+
+None was caught by reasoning. Three were caught by a **negative control** — plant the
+fault, run, read the output — and one by re-deriving the same number a different way.
+
+**The rule.** A scan that reports something bad about the tree is a claim like any
+other, and the first version of it is usually a claim about the scan. Before writing it
+down: derive it a second way, and prefer a way that shares no code with the first.
+`tools/check_seal_coverage.py` does this in-line — `_ever_existed` asks git twice, by
+path and by basename, because the one-way version overstated fivefold.
+
+**The corollary about severity.** The more alarming the finding, the more likely it is
+yours. "Seals reference specs that never existed" and "the backends diverge" are
+accusations; "a spec has a typo" and "a regex is wrong" are not. The session's four
+false alarms were all in the first category, and all four true causes were in the
+second.
+
+## 8. Name the kinds of a failure separately when their fixes differ
+
+`check_seal_coverage.py` first reported 89 **dangling** seals. Splitting by whether the
+spec ever existed gives two problems that share nothing but a symptom:
+
+* **74 dangling** — the spec was committed and later deleted, 16 of them by one
+  identifiable commit. Fix: remove the seal with the spec, or restore both.
+* **15 phantom** — the spec appears in no commit and is nowhere on disk. Its
+  `spec_hash` and four `gen_hash_*` name a file nobody can fetch, so the record has no
+  checkable content. For four of them the seal file is the **only** trace of the module
+  anywhere in the tree. Fix: find the spec, or drop the seal.
+
+One word for both would have sent a reader to the wrong repair for 15 of 89 cases. A
+gate's vocabulary is part of its output.
+
 ---
 
 ## Writing a gate here

.github/workflows/emit-bitexact-gate.yml

@@ -21,7 +21,10 @@ on:
       - "bootstrap/**"
       - "cli/**"
       - "tools/check_specs_parse.py"
+      - "tools/check_specs_generate.py"
+      - "specs/**"
       - "tools/verify_exhaustive.py"
+      - "tools/check_duplicate_agreement.py"
       - "specs/ternary/**"
       - "tools/gft_backprop_microcode.py"
       - "tools/verify_emit_bitexact.py"
@@ -66,6 +69,15 @@ jobs:
       - name: Required specs parse
         run: python3 tools/check_specs_parse.py
 
+      # 348 of 1114 specs do not generate with ANY backend -- 31.2% of what the
+      # constitution calls the single source of truth. Not one is a backend mismatch:
+      # on a 25-spec sample, zero generated with any of the four. They are recorded as
+      # debt so this holds the line, and the number can only go down.
+      - name: Every spec still generates (negative control)
+        run: python3 tools/check_specs_generate.py --self-check
+      - name: Every spec still generates
+        run: python3 tools/check_specs_generate.py
+
       # Ternary primitives have input spaces small enough to enumerate: a full adder
       # over three trits-in-a-byte is 16,777,216 inputs, about a second of CPU. A space
       # you can exhaust needs neither a sample nor a prover, and docs/POSITIONING.md
@@ -76,6 +88,15 @@ jobs:
       - name: Exhaustive cross-target agreement
         run: python3 tools/verify_exhaustive.py
 
+      # tmul is defined in 14 specs, dot27 in 9, quantize in 7. Nothing checked that
+      # the copies still compute the same thing, and copies drift. Compares BEHAVIOUR,
+      # not text: hashing the source reported three "divergences" that were all
+      # artefacts of the comparison rather than facts about the tree.
+      - name: Duplicated functions agree (negative control)
+        run: python3 tools/check_duplicate_agreement.py --self-check
+      - name: Duplicated functions agree
+        run: python3 tools/check_duplicate_agreement.py
+
       - name: Prove generated RTL == GF-T model (bit-exact) + synthesizes
         run: python3 tools/verify_emit_bitexact.py
 

.github/workflows/seal-coverage.yml

@@ -1,17 +1,51 @@
-name: SEAL Coverage
+name: Seal Coverage
+
+# This workflow is named a required check in docs/BRANCH-PROTECTION.md and its entire
+# body used to be:
+#
+#     echo "Running SEAL coverage analysis..."
+#
+# A required check that cannot fail reads as coverage and is worse than none.
+#
+# A seal records spec_path, spec_hash, and the sha256 of each generated target at the
+# moment of sealing. Its invariant is therefore: the spec it names still exists, and
+# still hashes to what was recorded. If the spec changed, the four gen_hashes no longer
+# describe what it produces and the seal asserts something false.
+#
+# Establishing that took two attempts. The first scored coverage by matching seal
+# FILENAMES against spec filenames and produced "1668 orphans of 1714" -- a finding
+# about the assumption, not the tree. Seals are keyed by MODULE name; the spec is named
+# inside the file.
+#
+# 207 seals do not hold today (89 dangling, 113 stale, 5 without a spec_path). They are
+# recorded in tools/seal_baseline.txt as debt so this gate holds the line without
+# demanding they all be fixed at once.
+#
+# The job id below is the status-check CONTEXT branch protection matches on. Renaming it
+# makes the required context stop reporting and the PR goes BLOCKED with every visible
+# check green -- learned the hard way in #2191.
 
 on:
   pull_request:
     branches: [master]
   push:
     branches: [master]
+  workflow_dispatch:
 
 jobs:
   coverage:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v6
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
+
+      # A gate nobody has seen fail is not a gate: this plants a stale seal and a
+      # dangling one in a temp tree and proves both are reported while a good one
+      # stays silent.
+      - name: Negative control
+        run: python3 tools/check_seal_coverage.py --self-check
 
-      - name: Run coverage
-        run: |
-          echo "Running SEAL coverage analysis..."
+      - name: Every seal still describes its spec
+        run: python3 tools/check_seal_coverage.py

.trinity/seals/VSACore.json

@@ -1,11 +1,11 @@
 {
-  "gen_hash_c": "sha256:41b888af77ad3a8f9f2434c9b18feffc710edd4628588aee2cb40916ee94e200",
-  "gen_hash_rust": "sha256:a22e87123a83dfe4229b7ebf46b33a8935c947f453ea307eab1ec6ac34f0e321",
-  "gen_hash_verilog": "sha256:dadf74db46fbd4139f0ad4f980d0505437ea4d54dc5531d19be88a279e1db035",
-  "gen_hash_zig": "sha256:df0d8a85e90abe88a781b2325ba09f5602321c0f720c113dc4bf19698e47dcaf",
-  "module": "VSACore",
-  "ring": 12,
-  "sealed_at": "2026-04-14T06:32:49Z",
-  "spec_hash": "sha256:de8f6deee5853e59dd20b0ded47f90ce2fbe810fe01b35181df1e1a452ed62c4",
-  "spec_path": "specs/vsa/core.t27"
+ "gen_hash_c": "sha256:41b888af77ad3a8f9f2434c9b18feffc710edd4628588aee2cb40916ee94e200",
+ "gen_hash_rust": "sha256:a22e87123a83dfe4229b7ebf46b33a8935c947f453ea307eab1ec6ac34f0e321",
+ "gen_hash_verilog": "sha256:dadf74db46fbd4139f0ad4f980d0505437ea4d54dc5531d19be88a279e1db035",
+ "gen_hash_zig": "sha256:df0d8a85e90abe88a781b2325ba09f5602321c0f720c113dc4bf19698e47dcaf",
+ "module": "VSACore",
+ "ring": 12,
+ "sealed_at": "2026-04-14T06:32:49Z",
+ "spec_hash": "sha256:de8f6deee5853e59dd20b0ded47f90ce2fbe810fe01b35181df1e1a452ed62c4",
+ "spec_path": "specs/test_framework/core.t27"
 }

.trinity/seals/vsa_VSACore.json

@@ -1,11 +1,11 @@
 {
-  "gen_hash_c": "sha256:41b888af77ad3a8f9f2434c9b18feffc710edd4628588aee2cb40916ee94e200",
-  "gen_hash_rust": "sha256:a22e87123a83dfe4229b7ebf46b33a8935c947f453ea307eab1ec6ac34f0e321",
-  "gen_hash_verilog": "sha256:3b65c336199877d860dac1127b70045667a26c2bae31050520b7cb40ad15bb75",
-  "gen_hash_zig": "sha256:df0d8a85e90abe88a781b2325ba09f5602321c0f720c113dc4bf19698e47dcaf",
-  "module": "VSACore",
-  "ring": 12,
-  "sealed_at": "2026-04-11T16:57:38Z",
-  "spec_hash": "sha256:e6ee5037438a5a35d64894d726e66881658f21fe67066f14c52b5dfc5db3bd50",
-  "spec_path": "specs/vsa/core.t27"
+ "gen_hash_c": "sha256:41b888af77ad3a8f9f2434c9b18feffc710edd4628588aee2cb40916ee94e200",
+ "gen_hash_rust": "sha256:a22e87123a83dfe4229b7ebf46b33a8935c947f453ea307eab1ec6ac34f0e321",
+ "gen_hash_verilog": "sha256:3b65c336199877d860dac1127b70045667a26c2bae31050520b7cb40ad15bb75",
+ "gen_hash_zig": "sha256:df0d8a85e90abe88a781b2325ba09f5602321c0f720c113dc4bf19698e47dcaf",
+ "module": "VSACore",
+ "ring": 12,
+ "sealed_at": "2026-04-11T16:57:38Z",
+ "spec_hash": "sha256:e6ee5037438a5a35d64894d726e66881658f21fe67066f14c52b5dfc5db3bd50",
+ "spec_path": "specs/test_framework/core.t27"
 }

bootstrap/src/compiler.rs

@@ -203,6 +203,14 @@ pub enum TokenKind {
     ShiftLeft,
     ShiftRight,
     PlusEquals,
+    // Only += existed. -=, *=, |=, &=, ^= lexed as two tokens and the parser died
+    // on the bare '='. Among the 348 specs that do not generate, 6 use -=, 4 use *=
+    // and 1 uses |= -- including specs/base/types.t27 at pack_trit line 172.
+    MinusEquals,
+    StarEquals,
+    PipeEquals,
+    AmpEquals,
+    CaretEquals,
     PlusPercent,
     MinusPercent,
     StarPercent,
@@ -597,6 +605,61 @@ impl Lexer {
                 };
             }
 
+        if two == [b'-', b'='] {
+                self.advance();
+                self.advance();
+                return Token {
+                    kind: TokenKind::MinusEquals,
+                    lexeme: String::from("-="),
+                    line: start_line,
+                    col: start_col,
+                };
+            }
+
+        if two == [b'*', b'='] {
+                self.advance();
+                self.advance();
+                return Token {
+                    kind: TokenKind::StarEquals,
+                    lexeme: String::from("*="),
+                    line: start_line,
+                    col: start_col,
+                };
+            }
+
+        if two == [b'|', b'='] {
+                self.advance();
+                self.advance();
+                return Token {
+                    kind: TokenKind::PipeEquals,
+                    lexeme: String::from("|="),
+                    line: start_line,
+                    col: start_col,
+                };
+            }
+
+        if two == [b'&', b'='] {
+                self.advance();
+                self.advance();
+                return Token {
+                    kind: TokenKind::AmpEquals,
+                    lexeme: String::from("&="),
+                    line: start_line,
+                    col: start_col,
+                };
+            }
+
+        if two == [b'^', b'='] {
+                self.advance();
+                self.advance();
+                return Token {
+                    kind: TokenKind::CaretEquals,
+                    lexeme: String::from("^="),
+                    line: start_line,
+                    col: start_col,
+                };
+            }
+
             if two == [b'+', b'%'] {
                 self.advance();
                 self.advance();
@@ -2027,15 +2090,24 @@ impl Parser {
         }
 
         // Check for += assignment
-        if self.current.kind == TokenKind::PlusEquals {
-            self.advance(); // consume +=
+        let compound_op = match self.current.kind {
+            TokenKind::PlusEquals => Some("+="),
+            TokenKind::MinusEquals => Some("-="),
+            TokenKind::StarEquals => Some("*="),
+            TokenKind::PipeEquals => Some("|="),
+            TokenKind::AmpEquals => Some("&="),
+            TokenKind::CaretEquals => Some("^="),
+            _ => None,
+        };
+        if let Some(cop) = compound_op {
+            self.advance(); // consume the compound operator
             let rhs = self.parse_expr()?;
             if self.current.kind == TokenKind::Semicolon {
                 self.advance();
             }
             let mut assign = Node::new(NodeKind::StmtAssign);
             assign.line = self.current.line as u32;
-            assign.extra_op = "+=".to_string();
+            assign.extra_op = cop.to_string();
             assign.children.push(expr);
             assign.children.push(rhs);
             return Ok(assign);
@@ -2671,6 +2743,21 @@ impl Parser {
             "bool", "u8", "i8", "u16", "i16", "u32", "i32", "u64", "i64", "usize",
         ];
         if !VALID_CAST_TYPES.contains(&base.as_str()) {
+            // f32/f64 parse in DECLARATIONS, so "unknown type" would be a lie here.
+            // The truth is narrower: no backend lowers float arithmetic -- the C
+            // generator emits the literal token `f32`, which is not a C type, and
+            // Verilog treats it as 32 plain bits. A cast that parses and then
+            // produces uncompilable C would be worse than this error, which is why
+            // f32/f64 are named here rather than added to the list.
+            if matches!(base.as_str(), "f32" | "f64") {
+                return Err(format!(
+                    "cast to `{}` is not supported: the language accepts float \
+                     declarations, but no backend lowers float arithmetic (the C \
+                     generator emits `{}` verbatim, which is not a C type). This spec \
+                     assumes a float-capable target that does not exist yet.",
+                    base, base
+                ));
+            }
             return Err(format!(
                 "unknown cast target type `{}`; expected one of {:?}",
                 base, VALID_CAST_TYPES
@@ -4120,8 +4207,8 @@ impl Codegen {
                 self.write_indent();
                 if node.children.len() >= 2 {
                     self.gen_expr(&node.children[0]);
-                    if node.extra_op == "+=" {
-                        self.write(" += ");
+                    if let Some(op) = compound_binop(&node.extra_op) {
+                        self.write(&format!(" {}= ", op));
                     } else {
                         self.write(" = ");
                     }
@@ -9523,10 +9610,10 @@ impl VerilogCodegen {
                         self.in_lvalue = true;
                         self.gen_verilog_expr(lhs);
                         self.in_lvalue = false;
-                        if node.extra_op == "+=" {
+                        if let Some(op) = compound_binop(&node.extra_op) {
                             self.write(asn);
                             self.gen_verilog_expr(lhs);
-                            self.write(" + ");
+                            self.write(&format!(" {} ", op));
                         } else {
                             self.write(asn);
                         }
@@ -11384,8 +11471,8 @@ impl CCodegen {
                         self.gen_c_expr(&node.children[1]);
                     } else {
                         self.gen_c_expr(&node.children[0]);
-                        if node.extra_op == "+=" {
-                            self.write(" += ");
+                        if let Some(op) = compound_binop(&node.extra_op) {
+                            self.write(&format!(" {}= ", op));
                         } else {
                             self.write(" = ");
                         }
@@ -12080,6 +12167,22 @@ fn resolve_import_path(
 // Compiler Interface
 // ============================================================================
 
+/// The binary operator inside a compound assignment: "|=" -> "|".
+/// All three backends tested `extra_op == "+="` and fell through to " = " otherwise,
+/// so accepting a new compound operator without touching them would have emitted
+/// `x = rhs` for `x |= rhs` -- a miscompilation rather than an error.
+fn compound_binop(extra_op: &str) -> Option<&'static str> {
+    match extra_op {
+        "+=" => Some("+"),
+        "-=" => Some("-"),
+        "*=" => Some("*"),
+        "|=" => Some("|"),
+        "&=" => Some("&"),
+        "^=" => Some("^"),
+        _ => None,
+    }
+}
+
 pub struct Compiler;
 
 #[allow(dead_code)]