How a gate lies (skill), and where t27 actually stands (positioning + exhaustive ternary_mul)

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

@@ -0,0 +1,151 @@
+---
+name: ci-gates
+description: How a CI gate lies. Six confirmed cases from one day in this repository — gates that cannot fail, gates blind to the files that matter, wrappers that swallow the tool's own message, and a crash reported as a numeric disagreement. Read before writing a gate, before trusting a green one, and before believing a failure message about which subsystem broke.
+---
+
+# How a gate lies
+
+Every rule below is a specific failure found in this repository on 2026-08-18, with the
+path. None is a principle someone liked.
+
+The day's arithmetic: **one missing brace cost four days of a red gate**, and the four days
+were spent because three layers of diagnostics each named a different subsystem and only
+the innermost one was right.
+
+---
+
+## 1. A gate that cannot fail reads as coverage, and is worse than none
+
+`docs/BRANCH-PROTECTION.md` named five required checks. Two had a body of exactly one
+`echo`:
+
+```yaml
+- run: echo "Running SEAL coverage analysis..."      # seal-coverage.yml, 17 lines
+- run: echo "Validating JSON schemas..."             # schema-validation.yml, 15 lines
+```
+
+A third, described in that same table as **"Main test suite"**, asserted
+
+```python
+assert abs(phi**2 + phi**-2 - 3) < 1e-10
+```
+
+which is a truth about arithmetic and holds for an empty repository.
+
+**The test:** for each gate you rely on, write down the change that should make it fail.
+If you cannot name one, the gate is decoration and the row in the required-checks table is
+a claim that isn't true.
+
+Replacing one `echo` with *does every tracked JSON parse* — the weakest question worth
+asking, chosen because it carries no theory that could itself be wrong — immediately found
+`clara-bridge/audit-trail/experience-schema.json` with a literal `...` on line 40, which
+`clara-bridge/tests/run_tests.py:152` loads with `json.load()`. **3 of its 11 tests were
+failing** and no workflow ran that suite at all.
+
+## 2. A gate is green until proven otherwise — check its SCOPE separately from its result
+
+`tools/check_withdrawn_live.py` shipped scanning `.md`/`.tex`/`.rst` and printed
+`OK … 975 documents scanned`. It was green **because it could not see** the file that
+mattered: `specs/numeric/formats_catalog.t27:228`, the canonical CATALOG row that feeds
+the published dataset, still carried the withdrawn number. So did the metrics CSV and two
+self-citations in a `.t27` benchmark.
+
+Widening to `.t27`/`.csv`/`.json` took the scan from 975 to **4435** documents and found
+seven live occurrences.
+
+**A gate green because it is under-scoped is the same failure it was built to kill.**
+Print what the gate covered — file count, extensions, exclusions — beside its verdict, and
+read that number as carefully as the verdict.
+
+## 3. Ask the exit code. Print what the tool said.
+
+Two patterns, both found by AST scan over `tools/*.py`:
+
+| pattern | what it does | sites found |
+|---|---|---|
+| `run(..., capture_output=True).returncode` | reads the exit code, discards the message | 9 |
+| `run(..., capture_output=True).stdout` | reads neither the exit code nor stderr | 18 |
+
+The second is worse. When `t27c gen-c` failed to *parse* a spec, `.stdout` was `""`, the
+empty string flowed downstream, and the failure surfaced as
+
+```
+FAIL: C backend failed to build/run
+```
+
+naming a subsystem that had never been reached. The compiler's own message named the file,
+the function, the line and the token — and `capture_output` collected it so it could be
+thrown away.
+
+**A diagnostic that names the wrong subsystem costs more than no diagnostic.** "The C and
+Rust backends diverge" is a far more alarming claim than "a spec has a typo", and it is
+where the four days went.
+
+**Rule: any wrapper that captures a tool's output must print it on a non-zero exit.**
+
+## 4. A crash is not a disagreement
+
+`run(built_binary).stdout` without an exit-code check turns a **dead program** into a
+**numeric mismatch between targets** — the most alarming reading a verification harness can
+produce, and the wrong one. A program that died on signal 11 did not disagree about
+arithmetic.
+
+Same shape one layer out: a simulator that hits its own timeout yields a short output list,
+reported as `step count RTL=0 PY=80`, which reads as *the RTL emitted nothing* — a design
+fault. The testbench was printing `TIMEOUT` into the very stdout the script parsed, and
+nothing looked for it.
+
+**Distinguish, in the message: did not run / did not finish / ran and disagreed.** Three
+different bugs, three different owners.
+
+## 5. Re-scan after a pattern fix, before claiming the pattern is gone
+
+Two partial repairs in a row, same day:
+
+* fixed the wrong 9 sites (the `.returncode` ones) and the output **did not change at all**,
+  because the failure was upstream in the `.stdout` calls the scan had not been written to
+  find;
+* fixed 6 sites in one file, reported the pattern handled — a re-scan found **12 more**,
+  the same call in a multi-line form the regex missed, plus 8 binary invocations.
+
+Both were caught by a **negative control** — plant the original fault, run, read the output
+— not by reasoning and not by the scan.
+
+**A regex matches a form, not a meaning.** Scan by AST, and run the scan *after* the fix as
+well as before.
+
+## 6. Renaming a CI job silently breaks branch protection
+
+Replacing a gate's body and renaming its job from `validate` to `schema-validation` sent
+the PR to **`mergeable: MERGEABLE`, `mergeStateStatus: BLOCKED`** with every visible check
+green and no required review outstanding.
+
+Branch protection matches on the **job id**, which is the status-check context. A renamed
+required context does not report as failing — **it stops reporting**, and nothing says so.
+
+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`.
+
+---
+
+## Writing a gate here
+
+1. **Negative control first, as its own CI step.** Plant the fault the gate exists to catch
+   and prove it fires; prove it stays silent on a clean input. A gate nobody has seen fail
+   is not a gate. Every gate added on 2026-08-18 carries `--self-check`, and the controls
+   caught three of the author's own mistakes before merge.
+2. **Data, not code, for the rule set.** `tools/withdrawn.txt` holds one regex per withdrawn
+   number, so a row is added the moment a number is withdrawn rather than when the document
+   is finally fixed — those two events were **ten days** apart.
+3. **Baselines keyed to the line, not the file.** `path | pattern | sha1(line)` — keying on
+   the file would silence every future occurrence in it, which for an append-only document
+   like `docs/NOW.md` widens with every entry.
+4. **Report what you could not establish.** `.trinity/seals/` holds 1714 files keyed on
+   *type* names; scoring "seal coverage" against spec names produced "1668 orphans of 1714",
+   a finding about the assumption rather than the repository. Neither a check nor a deletion
+   was written, and the PR said so.
+5. **Say what the gate does not cover.** `external/` is excluded from the JSON gate because
+   tsconfig is JSONC by convention — flagging it would be the gate making the mistake it
+   exists to catch.

docs/NOW.md

@@ -1,3 +1,26 @@
+# NOW -- one arm is exhaustive now, and the other three say they are samples (2026-08-18)
+
+Last updated: 2026-08-18
+
+## verify: make ternary_mul exhaustive, and state where t27 actually stands (Closes #2197)
+
+- **Both axes of "one spec, four targets, bit-exact" are occupied.** Chisel/FIRRTL/CIRCT emits Verilog *and* a C++ simulator from one source; HLS has done C→RTL for twenty years. Equivalence between an RTL design and a C model is industrial practice -- HECTOR, and the ACL2/RAC line producing mechanically checked proofs over **all** inputs. Multi-target emission is table stakes and formal equivalence is stronger than what we do
+- **`ternary_mul` was sampling a domain it could enumerate**: 800 random draws from a space of 256 x 256 = 65,536, missing about 22 % of it by chance, when enumeration costs milliseconds. It is now exhaustive -- C and Rust each sweep all 65,536 `(a, code)` pairs and match the model's FNV-1a digest `6b2724c5`
+- **Negative control has full resolution:** perturbing the model at exactly one input out of 65,536 is caught by both backends
+- `ternary_mac` stays sampled and now says so -- its i32 accumulator puts the space at ~2.8e14. `gft_smul`/`gft_sadd` sample 600 of ~4.3e9, which is 1.4e-7 of it
+- **The Coq work is real and is about something else.** 11 developments under `coq/`, gated against `Admitted`, concerning the kernel and phi -- **not** backend equivalence, and not to be cited as if they were
+- `docs/POSITIONING.md`: what is occupied, what we prove precisely, and the three things that are not occupied -- the target *set* (no one else emits a standalone Rust or Zig library from the same source as the RTL), a path with no vendor licence, and the one place ternary buys a **verification** advantage rather than an area claim: small domains make complete cross-target agreement affordable
+
+# NOW -- how a gate lies, written down (2026-08-18)
+
+Last updated: 2026-08-18
+
+## skills: six confirmed ways a CI gate produces a wrong signal (Closes #2195)
+
+- **The day's arithmetic: one missing brace cost four days of a red gate**, and the days went to three layers of diagnostics each naming a different subsystem, only the innermost right
+- Six ways recorded with paths: a gate that **cannot fail** (two required checks were one `echo`; a third asserted `phi**2 + phi**-2 == 3`); a gate green because **under-scoped** (975 documents scanned, blind to the canonical catalog row); a wrapper that **swallows the tool's message** (27 sites); a **crash reported as a numeric disagreement**; a **partial repair reported as complete**, twice; and **renaming a job silently breaking branch protection**
+- Construction rules alongside: negative control as its own CI step; the rule set as data, so a row is added when a number is withdrawn rather than when the document is fixed -- ten days apart in the case that started this; baselines keyed to the **line** rather than the file, since an append-only document widens the hole every entry; and reporting what could not be established instead of inventing it
+- `.claude/skills/ci-gates/SKILL.md`
 # NOW -- a dead simulator is not a design that emitted nothing (2026-08-18)
 
 Last updated: 2026-08-18

docs/POSITIONING.md

@@ -0,0 +1,82 @@
+# Where t27 actually stands
+
+Written 2026-08-18 after reading what the alternatives do, rather than assuming. The point of
+this document is to name what is occupied, so effort goes where something is not.
+
+## The claim, as the tools state it
+
+The verification scripts print lines like `ALL TARGETS BIT-EXACT` and describe themselves as
+closing *"one spec → any target, bit-exact"* across {Verilog, C, Rust, model}. That phrasing
+invites two readings, and only one is supported.
+
+## What is already occupied
+
+**Multi-target generation from one source — occupied.** Chisel elaborates to FIRRTL and CIRCT
+lowers it to Verilog *and* to a C++ cycle-accurate simulator from the same source; this is the
+standard flow, not a frontier. High-level synthesis has gone C/C++/SystemC → RTL for two
+decades. A language that emits more than one target is not, by itself, a position.
+
+**Proving target-to-target equivalence — occupied, and by stronger methods than ours.** Formal
+equivalence checking between an RTL design and a C model is industrial practice: Synopsys HECTOR
+does sequential equivalence checking; the ACL2/Restricted-Algorithmic-C line translates Verilog
+to C++ to ACL2 and produces mechanically checked proofs against architectural specifications,
+in production use for floating-point datapaths. Those are proofs over *all* inputs.
+
+## What this repository actually proves, precisely
+
+Two different strengths, and until 2026-08-18 the output line did not distinguish them:
+
+| function | input space | what is checked |
+|---|---|---|
+| `ternary_mul(a: i8, w)` | 256 × 256 = **65,536** | **every input**, C and Rust against the model, FNV-1a digest `6b2724c5` |
+| `ternary_mac(acc: i32, …)` | 256 × 256 × 2³² ≈ 2.8 × 10¹⁴ | 800 sampled vectors, edge cases included |
+| `gft_smul` / `gft_sadd` | ~4.3 × 10⁹ | 600 sampled operands — 1.4 × 10⁻⁷ of the space |
+| `systolic_ternary_pe` | i16 accumulator | 800 sampled vectors |
+
+So one arm is exhaustive and the rest are **randomised differential testing**. That is a real
+technique with a real name, and it is weaker than formal equivalence checking. The verdict lines
+now say which is which.
+
+The repository does carry genuine formal work — 11 Coq developments under `coq/`, with a CI gate
+that rejects any `Admitted` proof. They are about the kernel and φ, **not** about backend
+equivalence, and should not be cited as if they were.
+
+## What is genuinely less occupied
+
+Three things, and they are narrower than the slogan:
+
+1. **The target set.** Chisel emits Verilog and a C++ *simulator*. HLS goes C → RTL. Neither
+   emits a standalone **Rust** or **Zig** library from the same source as the RTL. t27 does.
+2. **No vendor licence anywhere in the path.** The flow is `t27c` → Yosys → nextpnr → prjxray,
+   reproducible from a pinned container digest. HECTOR and the commercial EC tools are the
+   opposite of that.
+3. **Exhaustive verification is reachable here, and is not for the alternatives' targets.**
+   A ternary primitive over an 8-bit operand and a 2-bit weight has 65,536 inputs. Enumerating
+   that costs milliseconds. Small ternary domains make *complete* cross-target agreement
+   affordable, where a 32-bit float datapath forces you to either sample or invoke a prover.
+   That is the one place where the ternary choice buys a verification advantage rather than
+   an area claim.
+
+## What to stop saying
+
+- **"bit-exact across targets"** without a qualifier, when three of four arms are sampled.
+  Say *exhaustive* where it is exhaustive and *sampled over N* where it is not.
+- Anything implying the Coq proofs cover the backends. They do not.
+- Treating multi-target emission as the differentiator. It is table stakes; the target *set*
+  and the licence-free path are the differences.
+
+## What would strengthen the position, in order of cost
+
+1. Push exhaustive coverage up the datapath wherever the domain allows it — every ternary
+   primitive whose input space is under ~2²⁴ can be enumerated rather than sampled.
+2. For the arms that cannot be exhausted, state the sampled fraction next to the result, as the
+   table above does. A reader can then judge it.
+3. If a proof over all inputs is wanted for the wide arms, that is an equivalence-checking or
+   theorem-proving problem with existing literature, not something to reinvent.
+
+## Sources
+
+- [Chisel](https://www.chisel-lang.org/) and [chipsalliance/chisel](https://github.com/chipsalliance/chisel) — single source to Verilog and a C++ simulator via FIRRTL/CIRCT
+- [Formal Verification of Arithmetic RTL: Translating Verilog to C++ to ACL2](https://arxiv.org/pdf/2009.13761) — mechanically checked proofs against architectural specs
+- [Automated Formal Equivalence Verification of Pipelined Nested Loops in Datapath Designs](https://arxiv.org/pdf/1712.09818) — industrial sequential equivalence checking (HECTOR)
+- [Translation Validation for an Optimizing Compiler](https://people.eecs.berkeley.edu/~necula/Papers/tv_pldi00.pdf) — the source-to-target equivalence framing