How a gate lies (skill), and where t27 actually stands (positioning + exhaustive ternary_mul) - #2196
Merged
Conversation
Contributor
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
gHashTag
changed the title
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 <noreply@anthropic.com>
…ples 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 <noreply@anthropic.com>
gHashTag
force-pushed
the
loop/t27-skill-gates
branch
from
August 18, 2026 13:39
3d8a075 to
e0906d2
Compare
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-18 13:39:28 UTC
Summary
Seal Status
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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. The arithmetic of the day: one missing brace cost four days of a red gate, and those days were spent because three layers of diagnostics each named a different subsystem and only the innermost was right.
echo; a third assertedphi**2 + phi**-2 == 3, true of an empty repoformats_catalog.t27, which still carried the withdrawn numberrun(binary).stdoutwith no exit check turns signal 11 into a numeric mismatch between targetsMERGEABLE+BLOCKED, every visible check green, required context simply stops reportingPlus the construction rules that came out of it: 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 here); baselines keyed to the line, 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 —
.trinity/seals/is keyed on type names, and scoring coverage against spec names produced "1668 orphans of 1714", a finding about the assumption.Goes in
.claude/skills/ci-gates/. Refs #2193Read what the alternatives do, rather than assuming, and then measured what this repository actually proves.
Occupied, both axes of the slogan:
What we actually prove:
ternary_mul(a: i8, w)ternary_mac(acc: i32, …)gft_smul/gft_saddternary_mulwas sampling a domain it could enumerate. 800 random draws from 65,536, missing ~22 % of the space by chance, when enumerating it costs milliseconds.This PR makes that arm exhaustive. C and Rust each sweep all 65,536
(a, code)pairs and produce an FNV-1a digest compared against the model:6b2724c5. Negative control — perturbing the model at exactly one input out of 65,536 — is caught by both backends, so the check has full resolution and is not vacuous.Verdict lines now distinguish exhaustive from sampled over N, and name why the sampled arms cannot be exhausted (
ternary_maccarries an i32 accumulator).Also corrected: the 11 Coq developments under
coq/are real and gated againstAdmitted, but they concern the kernel and φ — not backend equivalence — and must not be cited as if they did.docs/POSITIONING.mdrecords what is occupied, what this repository proves precisely, and the three things that are genuinely less occupied: the target set (nobody else emits a standalone Rust or Zig library from the same source as the RTL), a path with no vendor licence anywhere in it, and — the one place the ternary choice buys a verification advantage rather than an area claim — that small ternary domains make complete cross-target agreement affordable where a 32-bit float datapath forces sampling or a prover.Refs #2195
Closes #2195
Closes #2197
🤖 Generated with Claude Code