diff --git a/.claude/skills/ci-gates/SKILL.md b/.claude/skills/ci-gates/SKILL.md new file mode 100644 index 0000000000..c2495366c1 --- /dev/null +++ b/.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.:` may not. + +When `repos/:owner/:repo/branches/master/protection` returns nothing useful, read the +contexts off a recently merged PR: `gh pr checks | 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. diff --git a/docs/NOW.md b/docs/NOW.md index c1d378de56..929cc9e4f1 100644 --- a/docs/NOW.md +++ b/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 diff --git a/docs/POSITIONING.md b/docs/POSITIONING.md new file mode 100644 index 0000000000..5e243ef88d --- /dev/null +++ b/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 diff --git a/tools/verify_igla_race.py b/tools/verify_igla_race.py index 703bceb918..8b54f4a8fb 100644 --- a/tools/verify_igla_race.py +++ b/tools/verify_igla_race.py @@ -109,6 +109,27 @@ def ref_mul(a, code): def ref_mac(acc, a, code): return i32(i32(acc) + ref_mul(a, code)) +def exhaustive_mul_digest(): + """FNV-1a over ternary_mul(a, code) for EVERY (a, code) pair. + + The input space of ternary_mul is 256 x 256 = 65,536 -- small enough to + enumerate. gen_vectors() samples 800 triples from it, which is a subsample of + a space that can be covered completely, and "agree on 800 random operands" is + a strictly weaker statement than "agree on every possible input" when the + latter costs milliseconds. + + ternary_mac is NOT exhaustible: its accumulator is i32, so the space is + 256 x 256 x 2^32 ~ 2.8e14. It stays sampled, with its edge cases, and the + verdict line says which of the two it is. + """ + h = 2166136261 + for a in range(-128, 128): + for c in range(256): + v = ref_mul(a, c) & 0xFF + h = ((h ^ v) * 16777619) & 0xFFFFFFFF + return h + + def gen_vectors(): r = random.Random(7777) A = [-128, -1, 0, 1, 127]; C = [0, 1, 2, 3, 255]; ACC = [0, (1 << 31) - 1, -(1 << 31), 1000000] @@ -204,6 +225,69 @@ def _core_rust(t27c): return "#[derive(Clone, Copy)]\n" + st + "\n" + "\n".join(blocks) +def exhaustive_c(t27c, wd): + """ternary_mul over EVERY (a, code) pair, in C. 256 x 256 = 65,536 inputs. + + gen_vectors() samples 800 triples out of that space. Sampling a space you can + enumerate is a weaker statement than enumerating it, and here enumeration costs + milliseconds -- so this is not a sample, it is the whole domain. + + ternary_mac is deliberately NOT covered this way: its accumulator is i32, so its + space is 256 x 256 x 2^32 ~ 2.8e14. It stays sampled, and the verdict says so. + """ + core = _core_c(t27c) + if core is None: + return None + main = [ + "int main(void){", + " unsigned h = 2166136261u;", + " for (int a = -128; a < 128; a++) {", + " for (int c = 0; c < 256; c++) {", + " TernaryWeight w; w.code = (uint8_t)c;", + " unsigned v = (unsigned)((int)ternary_mul((int8_t)a, w) & 0xFF);", + " h = (h ^ v) * 16777619u;", + " }", + " }", + ' printf("%08x\\n", h);', + " return 0;", + "}", + ] + src = core + "\n" + "\n".join(main) + "\n" + f = os.path.join(wd, "exh.c") + open(f, "w").write(src) + if not _build(["cc", "-O2", "-o", os.path.join(wd, "exhc"), f], wd, "exhaustive C"): + return None + out = _run_bin(os.path.join(wd, "exhc"), "exhaustive C run") + return None if out is None else out.strip() + + +def exhaustive_rust(t27c, wd): + """The same whole-domain sweep, in Rust.""" + core = _core_rust(t27c) + if core is None: + return None + main = [ + "fn main(){", + " let mut h: u32 = 2166136261;", + " for a in -128i32..128 {", + " for c in 0u32..256 {", + " let w = TernaryWeight { code: c as u8 };", + " let v = ((ternary_mul(a as i8, w) as i32) & 0xFF) as u32;", + " h = (h ^ v).wrapping_mul(16777619);", + " }", + " }", + ' println!("{:08x}", h);', + "}", + ] + src = core + "\n" + "\n".join(main) + "\n" + f = os.path.join(wd, "exh.rs") + open(f, "w").write(src) + if not _build(["rustc", "-A", "warnings", "-O", "-o", os.path.join(wd, "exhr"), f], wd, "exhaustive Rust"): + return None + out = _run_bin(os.path.join(wd, "exhr"), "exhaustive Rust run") + return None if out is None else out.strip() + + def run_c(t27c, vecs, wd): core = _core_c(t27c) if core is None: @@ -341,7 +425,25 @@ def main(): print(f"FAIL: {tgt} != ref in {len(mism)}/{len(ref)}; first vec {vecs[i]} ref={r} {tgt}={g}") ok = False else: - print(f"OK ternary_mul/mac: {tgt} == reference BIT-EXACT over {len(ref)} vectors (edges incl.)") + print(f"OK ternary_mul/mac: {tgt} == reference over {len(ref)} SAMPLED vectors " + f"(edge cases included; ternary_mac's i32 accumulator makes its space " + f"~2.8e14, so this arm is a sample and says so)") + + # ternary_mul alone has a space of 256 x 256 = 65,536 -- small enough to enumerate. + # Sampling a domain you can exhaust is a weaker claim than exhausting it, and here + # exhausting it costs milliseconds. This arm is therefore not a sample. + want = f"{exhaustive_mul_digest():08x}" + for tgt, runner in (("C", exhaustive_c), ("Rust", exhaustive_rust)): + got = runner(t27c, wd) + if got is None: + print(f"FAIL: exhaustive {tgt} failed to build/run"); ok = False; continue + if got != want: + print(f"FAIL: exhaustive {tgt} digest {got} != model {want} -- the two disagree " + f"on at least one of the 65,536 possible (a, code) inputs") + ok = False + else: + print(f"OK ternary_mul: {tgt} == reference on ALL 65,536 possible inputs " + f"(exhaustive, FNV-1a digest {got})") # systolic PE: extends the check up the datapath (ternary_mac -> systolic PE) if os.path.exists(os.path.join(ROOT, SYS_SPEC)): print("NOTE systolic_ternary imports ternary_mul but the import is NOT emitted " @@ -362,7 +464,8 @@ def main(): ok = False else: print(f"OK systolic_ternary_pe: {tgt} == reference BIT-EXACT over {len(pref)} vectors (i16 psum, edges)") - print("IGLA RACE ternary MAC + systolic PE BIT-EXACT ACROSS TARGETS (C + Rust + model)" if ok else "IGLA RACE CROSS-TARGET MISMATCH") + print("IGLA RACE: ternary_mul EXHAUSTIVE over all 65,536 inputs; mac + systolic PE agree on " + "sampled vectors (C + Rust + model)" if ok else "IGLA RACE CROSS-TARGET MISMATCH") sys.exit(0 if ok else 1)