fix(research): half the intrinsic-invariant flags were signed zero, not a defect — 40 flags to 20 - #354
Merged
Merged
Conversation
…s a number for it Option C's falsifier was "port the cell to a non-Xilinx target and measure how much of it is 7-series-specific; if most of it is, there is no IP to sell." It was expected to kill the option. It did the opposite. Split trinet_node_v2_ax7203 into a board wrapper and fpga/portable/ trinet_node_core.v. The audit of what actually had to move found two primitives: STARTUPE2 for the clock and DNA_PORT for the device identity, both board concerns rather than node concerns. Nothing else was vendor-bound. The core then synthesised on ten families from eight vendors with zero errors and zero inferred multipliers -- and every one of them recovered 819 flip-flops, except Intel ALM at 831 because its register cell absorbs reset logic the others express separately. Ten synthesisers agreeing to the register is what portable RTL looks like. The LUT column varies 939..1737 and that is LUT width doing its job, so the CI check asserts the invariant rather than the numbers; asserting the numbers would fail on a yosys upgrade for no reason. The wrapper instantiates the core rather than keeping a copy. A copy would drift and the portability claim would stop being true while both files built. This does not establish portability of product. Synthesis is not place-and- route, no non-Xilinx mapping has met timing, and only the xc7 path has run on silicon. It also does not make anyone want the IP -- the report's real objections to option C (no measured power, no device-bound identity, no fab path) are untouched, and "C not this year" stands. What changed is that the reason is now about market access rather than about engineering. Also fixes a defect the split surfaced. formal/trinet_node_v2_tb.v failed 0/6 -- and failed identically on the pre-split design, which is what proved the split behaviour-preserving. The testbench passed no key and relied on the module default, so when W01 replaced the compromised default with a null one, its golden tags stopped matching anything the RTL could produce. The security fix disabled the test guarding the security property and nothing said so. Now passes the SipHash reference key explicitly, with goldens regenerated from the independent Python implementation rather than from the RTL: 6/6. conformance/key_default_check.py enforces both halves of that lesson -- null defaults in RTL, explicit keys in testbenches -- and CI deliberately breaks each rule to confirm the guard still fails when it should. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…od one Found while trying to build the statistical base a paper needs. None of them were visible from the code; all three came out of pointing the host at the boards and disbelieving the first number it printed. 1. THE FLEET IS RUNNING PUBLISHED KEYS. W01 replaced the committed receipt keys with a null default. That fixed the source and never reached the silicon. Measured today: node0 verifies 64/64 under 0x00..0x0f and node2 63/64 under 0x20..0x2f -- both keys published in this repository's history. Every "keyed receipt verified on silicon" result this project has reported rests on tags any reader of the git log can compute. A compromised key and a good key are indistinguishable to any test that only asks "does the tag match", which is why nothing noticed. protocol.zig now carries the published keys explicitly and publishedKeyUsed() checks every receipt against them; probe refuses the node with "a working node with worthless receipts. Do not pay it." The arithmetic is separately reported and is real -- 64/64 and 63/64 -- because a board can compute perfectly and prove nothing, and conflating those is the same mistake W03 was about. 2. THROUGHPUT COUNTED JOBS THAT FAILED. jobs_per_s divided by n, the number attempted, not by the number verified. A board answering nothing returns instantly, so total failure read as the fastest run ever recorded: 5409 jobs/s against a transport ceiling of 4942, with 0/64 verified. The ceiling caught it. Latency percentiles had the same shape -- failures wrote a zero into the array and dragged p50 to 0.00 ms. Now counts verified work only, takes percentiles over successful jobs only, and prints IMPOSSIBLE when the rate exceeds what the UART can carry. Every jobs/s figure published before today was computed the broken way and is restated. 3. THE HOST PICKED THE WIRE FORMAT FROM ITS OWN CONFIG FILE. Response width was inferred from `key != null`. But the width is a property of the flashed bitstream and the key is a property of the host's config -- so a keyless host reading a v2 board took 15 bytes of a 19-byte response, left four behind, and offset every later read by four. A healthy board reported MalformedResponse forever, and the benchmark read 15-byte slices of a stream at full line rate and called it throughput. That is defect 2's accomplice. The format is now asked of the wire on the first exchange and latched. The detection costs one timeout on a v1 board, once, and buys a host that cannot be misconfigured into a permanent desync. Also gives probe a baud argument, because the boards answer at 1186267 and the built-in default of 160000 could not reach them at all. 48/48 protocol+agent, 18 ledger, 34 mesh, 16 node, 42 model. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ot a defect Looking for a third place where a check compares in the wrong domain. This is it, and it was flagging 40 formats. verify_intrinsic_invariants.py reported "roundtrip VIOLATED" for binary16, bfloat16, gf16, fp8_e5m2 and 17 others. Opening the flags gave the same answer every time: binary16 1 failure of 65536 the negative-zero code bfloat16 1 failure of 65536 the negative-zero code gf16 1 failure of 65536 the negative-zero code fp8_e5m2 1 failure of 256 the negative-zero code fp6_e2m3 1 failure of 64 the negative-zero code The oracles carry values as Fraction, which cannot distinguish -0 from +0, so encode() returns the positive-zero code and the round trip closes on the wrong one. That is a property of the carrier, not of the format. The corpus already knows it -- crossval_ml_ dtypes.py prints "[2 zero-sign not carried by oracle]" for exactly this reason -- and this check turned it into a flag against 21 of 35 narrow formats. It also explains why the flag tracked width rather than correctness. Exhaustive enumeration always reaches the negative-zero code; the 4000-point stride sample used above 16 bits usually steps over it. Narrow formats looked worse because they were looked at harder. Signed zero is now counted apart from real round-trip failures. The flag list goes from 40 to 20, and binary16, bfloat16, gf16 and fp8_e5m2 read OK. The 20 that remain are the ones the file's own caveat was always about: bcd and decimal carry redundant representations by design, uint has no sign to negate, nf4 is a quantile table, and the VAX, IBM HFP, Microsoft MBF, Cray and PDP-11 entries are legacy formats with genuinely different rules. Those are leads. The 20 that left were not. This is the third instance of one class in four passes -- pass 156 in the negation check, pass 158 in crossval_libtakum, this one here. Each reported a healthy corpus as broken, at a scale of tens of thousands of codes or tens of formats, and each was a comparison made where the object does not live: the value domain for a logarithmic format, and a rational carrier for a sign-magnitude zero.
gHashTag
pushed a commit
that referenced
this pull request
Aug 3, 2026
main carried a squashed, earlier snapshot of this branch's own work (#354), so every conflict was this branch against its own past rather than against someone else's change. Resolved by inspection, not by rule: fpga/portable/trinet_node_core.v main's side is byte-identical to this branch at 6ba3634, before the key started arriving over the wire — ours src/trinet/protocol.zig main's side has no `.unverifiable`, the verdict added so a keyless verifier cannot accuse an honest board — ours src/trinet/node.zig main's side predates auto-baud — ours src/trinet/main.zig main's side predates per-board rate negotiation and the identity probe — ours specs/trinet/ternary_hw_verification.t27 ours, strictly a superset .github/workflows/trinet-portability.yml THEIRS: identical to ours except for a path entry main added afterwards, so that the job re-runs when the script it runs changes Verified after resolving rather than assumed: 56/56 tests, zig fmt clean, and on hardware — all three boards discovered at 1144744 baud 64/64 clean, node2 census 192/192 with the rate negotiated. Noted, not touched because it is neither this branch's nor this merge's: docs/ARCHITECTURE.md has 16 `<<<<<<< Updated upstream` markers committed into it on both sides. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
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.
Looking for a third place where a check compares in the wrong domain. This is it, and it was flagging 40 formats.
verify_intrinsic_invariants.pyreportedroundtrip VIOLATEDfor binary16, bfloat16, gf16, fp8_e5m2 and 17 others. Opening the flags gave the same answer every time:The oracles carry values as
Fraction, which cannot distinguish −0 from +0, soencode()returns the positive-zero code and the round trip closes on the wrong one. That is a property of the carrier, not of the format. The corpus already knows it —crossval_ml_dtypes.pyprints "[2 zero-sign not carried by oracle]" for exactly this reason — and this check turned it into a flag against 21 of 35 narrow formats.It also explains why the flag tracked width rather than correctness. Exhaustive enumeration always reaches the negative-zero code; the 4000-point stride sample used above 16 bits usually steps over it. Narrow formats looked worse because they were looked at harder.
Result
Flag list 40 → 20. binary16, bfloat16, gf16 and fp8_e5m2 read OK.
The 20 that remain are the ones the file's own caveat was always about:
bcdanddecimalcarry redundant representations by design,uinthas no sign to negate,nf4is a quantile table, and the VAX / IBM HFP / Microsoft MBF / Cray / PDP-11 entries are legacy formats with genuinely different rules. Those are leads. The 20 that left were not.Third instance of one class in four passes
Pass 156 in the negation check, pass 158 in
crossval_libtakum, this one here. Each reported a healthy corpus as broken, at a scale of tens of thousands of codes or tens of formats — and each was a comparison made where the object does not live: the value domain for a logarithmic format, and a rational carrier for a sign-magnitude zero.🤖 Generated with Claude Code