From 07f326c977af65cb8ea57267b7321ed3f270f1d0 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Tue, 18 Aug 2026 20:17:32 +0700 Subject: [PATCH 1/2] docs(skills): record how a gate lies, six confirmed cases Six distinct ways a CI gate produced a wrong signal, all confirmed in this repository on 2026-08-18 with paths, across #2185 #2187 #2189 #2191 #2193. cannot fail two required checks were one echo; a third asserted phi**2 + phi**-2 == 3, true of an empty repository green because under-scoped the withdrawal gate scanned 975 documents and could not see formats_catalog.t27, which still carried the withdrawn number swallows the tool's message 27 sites took stdout or returncode and dropped stderr; a parse error surfaced as 'the C backend failed to build' crash as disagreement run(binary).stdout with no exit check turns signal 11 into a numeric mismatch partial repair, reported done twice; a regex matches a form, not a meaning renaming a job MERGEABLE + BLOCKED, every check green, the required context simply stops reporting Plus the construction rules: 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, which were ten days apart in the case that started this; baselines keyed to the line rather than the file, since keying to the file silences every future occurrence in an append-only document; and reporting what could not be established rather than inventing it. Closes #2195 Co-Authored-By: Claude Opus 5 --- .claude/skills/ci-gates/SKILL.md | 151 +++++++++++++++++++++++++++++++ docs/NOW.md | 10 ++ 2 files changed, 161 insertions(+) create mode 100644 .claude/skills/ci-gates/SKILL.md 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..bd4bd30f37 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,3 +1,13 @@ +# 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 From e0906d2c164fb1dbb298fb5cbf68fb1954b9ddf3 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Tue, 18 Aug 2026 20:31:57 +0700 Subject: [PATCH 2/2] verify: make ternary_mul exhaustive, and say where the others are samples Read what the alternatives do rather than assuming, then measured what this repository actually proves. Both axes of 'one spec, four targets, bit-exact' are occupied. Chisel elaborates to FIRRTL and CIRCT lowers it to Verilog AND a C++ cycle-accurate simulator from one source; HLS has gone C->RTL for two decades. Equivalence between an RTL design and a C model is industrial practice -- HECTOR for sequential EC, and the ACL2/RAC line translating Verilog->C++->ACL2 for mechanically checked proofs over ALL inputs. Emitting several targets is table stakes; formal EC is stronger than randomised differential testing. What we prove, before this commit: ternary_mul(a: i8, w) space 256 x 256 = 65,536 800 sampled ternary_mac(acc: i32, ..) space ~2.8e14 800 sampled gft_smul / gft_sadd space ~4.3e9 600 sampled (1.4e-7) ternary_mul was sampling a domain it could enumerate -- 800 draws from 65,536, missing about 22% of it by chance, when enumeration costs milliseconds. It is now exhaustive: C and Rust each sweep every (a, code) pair and match the model's FNV-1a digest 6b2724c5. Perturbing the model at exactly one input out of 65,536 is caught by both backends, so the check has full resolution over the domain. The other arms stay sampled and the verdict lines now say so, with the reason -- ternary_mac carries an i32 accumulator, which is what makes its space 2.8e14. Also recorded: the 11 Coq developments under coq/ are real and gated against Admitted, but they concern the kernel and phi, not backend equivalence, and must not be cited as if they did. docs/POSITIONING.md states what is occupied, what is proven here precisely, and the three things genuinely less occupied: the target set, a path with no vendor licence, and the one place the ternary choice buys a verification advantage rather than an area claim -- small domains make complete cross-target agreement affordable where a 32-bit float datapath forces sampling or a prover. Closes #2197 Co-Authored-By: Claude Opus 5 --- docs/NOW.md | 13 +++++ docs/POSITIONING.md | 82 +++++++++++++++++++++++++++++ tools/verify_igla_race.py | 107 +++++++++++++++++++++++++++++++++++++- 3 files changed, 200 insertions(+), 2 deletions(-) create mode 100644 docs/POSITIONING.md diff --git a/docs/NOW.md b/docs/NOW.md index bd4bd30f37..929cc9e4f1 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,3 +1,16 @@ +# 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 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)