TRI-NET: three boards, ten families, and four numbers that were wrong - #355
Open
gHashTag wants to merge 85 commits into
Open
TRI-NET: three boards, ten families, and four numbers that were wrong#355gHashTag wants to merge 85 commits into
gHashTag wants to merge 85 commits into
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>
The fleet has been described as two boards since yesterday, with the third recorded as a wiring fault: configured, DONE=1, UART silent. That diagnosis was wrong, and the operator asking "why can't you see the third board?" is what prompted actually testing it instead of repeating it. It answers at 1124474 baud. The fleet was hardcoded to 1186267 — a 5.2% error, where a UART tolerates about 3. Swept, it verifies 32/32 immediately and then 6400/6400 across 100 independent runs, which makes it the equal of the best board in the fleet. The cause is physical and matters beyond this desk. CFGMCLK is an untrimmed RC oscillator, so its frequency belongs to the die: this fleet measures 71.18, 70.46 and 67.47 MHz, a 5.5% spread. Two boards had suggested 1.25% and that number is now known to be a two-sample artifact. No single host rate can serve this fleet, so Node.initFpgaAutoBaud asks each board its rate instead of being told. It scores six probes per candidate rather than trusting one, because the marginal board latched two different rates on consecutive runs from the same wire — one job is one coin flip. Statistical base, 100 independent runs of 64 jobs per board, port reopened each run (the FPGA frame parser survives the host process, so that matters): node0 6400/6400 100/100 perfect runs node1 6400/6400 100/100 perfect runs node2 6308/6400 42/100 perfect, min 60, p50 63 node2's loss is not the baud: swept to its own centre it scored slightly worse, 98.08% against 98.56%. That hypothesis is cleanly falsified and the marginal link stands. Report the minimum — a fleet is used at its worst run. Two more defects fell out of running all three: A KEYLESS VERIFIER WAS ACCUSING HONEST BOARDS. The fleet slashed node2 400 mTRI over a missing entry in the host's key file. With no key every keyed receipt looks equally unlike the expected tag, and the code read that as a lie. New Verdict.unverifiable: not accepted, and never an indictment. Holding the wrong key is a statement about the receipt; holding no key is a statement about us. BOARDS ON PUBLISHED KEYS NOW EARN NOTHING. The fleet drops the key of any board whose receipts verify under a key from the git history, so its work is unverifiable — no credit, and no slash either, because those boards are honest. With all three stale the ledger correctly refuses to dispatch at all, and the fleet now explains that instead of dying on error.NoEligibleNode. 180 tests pass across protocol, node, ledger, mesh, model and agent. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…nd a security fix that never reached the silicon The report now leads with what it got wrong rather than editing itself quietly. Four corrections: the fleet is three boards not two; the per-chip CFGMCLK spread is 5.5% not 1.25%; every board carries a published receipt key, so no receipt on this hardware is evidence of anything; and every jobs/s figure ever published divided by jobs attempted rather than verified and is withdrawn rather than restated. Adds W09-W11. W09 is the worst thing here: "fixed" meant the source changed and nobody checked the artifact. Records what running option C's falsifier returned. It came back opposite to the prediction — the cell is portable across ten families — and the recommendation to defer C still does not change, because C's real obstacles were never engineering. That distinction is now stated rather than implied. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Option B's action is one issue on TernaryCore with a concrete integration sketch; its falsifier is a 30-day silence. The draft is written and not sent. The pitch's strongest line would be "per-job verifiable receipts, demonstrated on silicon", and that line is not true today: all three boards carry receipt keys published in this repository, so the layer being offered has a hardware demonstration whose central security property is void. Sending now means either overstating it — which makes the falsifier meaningless, since a polite non-reply would then be the correct response — or opening with an apology. Send after the re-flash. About a day of work, and it gates the honest version of all three options. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…was split read_verilog listed only the wrapper and siphash; trinet_node_core.v has been the actual node since the portability split, so this workflow would have failed on the first push that touched it. Also sets USE_DNA 0. DNA_PORT places, routes, and returns zero for all 57 bits on this flow, so the node id comes from synthesis either way — the primitive and its read state machine are dead weight in every bitstream, and removing them makes the node id in simulation equal the one the hardware reports, which the DNA path made impossible. Records what BAUD_DIV=60 actually means now that there are three dies to compare: not one line rate but three (~1186, ~1174, ~1124 kbaud), because CFGMCLK is untrimmed and these chips are 5.5% apart where a UART tolerates 3. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ards CANDIDATE_RATES held only the rates a shared BAUD_DIV implies, which assumes every board runs the same clock. They do not. CFGMCLK is untrimmed and this fleet's dies measure 71.18, 70.46 and 67.47 MHz, so at BAUD_DIV=60 they speak 1186267, 1174399 and 1124474 baud — and the slowest answered none of the listed rates. That is why it was recorded as a wiring fault for a day. Both boards now enumerate, and the tool says out loud that they are at different line rates. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…dy can rotate is a key nobody rotates The committed-key defect was fixed in source on 2026-08-02 and never reached the silicon. Today's measurement found all three boards still signing with keys from this repository's git history, and the reason it stayed that way is structural rather than careless. Re-keying a baked-in key needs a place-and-route run the operator's machine cannot perform — an XC7A200T chipdb OOMs at Docker's 4 GB, and raising the limit to 6 GB on an 8 GB host stops Docker starting at all — plus 13 minutes of flashing, per board. That is roughly an hour per rotation on a good day and impossible on this desk. A design where the fix costs that much guarantees the fix does not happen. So the node now takes its key over the wire. op 0x02 carries 16 key bytes in the W and X operand fields, which keeps the request at 24 bytes and leaves the frame parser — and conformance/frame_alignment_check.py — untouched. Accepted exactly once per configuration and refused afterwards: a key that can be replaced at any time is not a key, because anyone reaching the wire could overwrite the operator's and every later receipt would verify under theirs. The trade is honest and worth stating. Whoever can reach this UART in the window after configuration can claim the node. They can also just re-flash it, so this concedes little that physical access did not already concede — and it buys rotation cheap enough to actually happen. A non-null RECEIPT_KEY still bakes a key in and locks it at reset, for anyone with a build machine who prefers the key never touch a wire. Cost: 1292 -> 1484 LC, +15% for the key register and the latch. Still 0 DSP48. The acknowledgement is signed with the key just installed, so the host can tell acceptance from an echo — a node that only echoed the request could produce the status byte but not that tag. Node.setKey checks the tag, not the status. Statuses 0x02/0x03/0x04 (key set / key locked / no key) all verify as Verdict.unverifiable rather than bad_status. A board that has not been provisioned yet is not misbehaving, and an unrecognised status is still chargeable — both are tested. formal/trinet_setkey_tb.v proves the four properties end to end over the real UART, 11/11: an unkeyed node computes but will not sign; the key installs and the ack is tagged with it; work then verifies; and a second key is refused while the first still signs. Golden tags come from tools/gen_setkey_golden.py driving the independent Python implementation, never from this RTL. 198 tests pass. Both static guards still pass. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…y baud rate Baud negotiation, the census and the probe's arithmetic column each tested `status == status_ok`. A node that has been flashed but not yet keyed answers status_no_key, and its dot products are perfectly real — so the negotiator would have rejected a correctly working board at all eight candidate rates, and the operator would have concluded the flash failed. Found by reading the new code against the boot sequence it creates, before spending a flash cycle on it. The three sites now share protocol.statusMeansComputed() so they cannot drift apart again: computed and signed are different questions, and only the second needs a key. A key-load acknowledgement carries no dot product and is correctly excluded, as is any status the protocol does not define. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The skill and the SSOT both described a procedure that no longer exists. The part worth keeping is not the new opcode but the reason for it: the committed-key fix never reached the silicon because rotating a baked-in key needs a place-and-route run this workstation cannot perform. A design whose fix costs an hour per board guarantees the fix does not happen. Also records that local place-and-route is impossible here, measured rather than assumed: 4 GB OOMs the chipdb build, 6 GB stops Docker starting on an 8 GB host. Any plan step assuming a local bitstream is dead on arrival. And that port names are not identity — '-1110' was node0 one hour and node1 the next, after a hub change. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Reported 180, then 198. Both were sums of overlapping suites: zig test on a file runs the tests of everything it imports, so protocol's 16 were counted again inside node, mesh, model and agent. The real number is 54 — one run of zig test src/trinet/agent.zig, which nests protocol(16), mesh(10), model(8), ledger(8), agent(6), node(4), net(2). Smaller than claimed and worth correcting, because the count is cited as evidence. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… finished That label was accurate when a bitstream without a baked key was a crippled build good only for routing and resource checks. The node now takes its key over the wire, so these are complete and deployable: flash, then trinet setkey. Leaving the label would send somebody looking for a 'real' keyed build that no longer exists — and, worse, might tempt them to bake a key back in to get one. Built and verified: three distinct bitstreams, sha256 matching what CI recorded, 1455-1475 LC, routed on the first seed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…first Three AL321 cables attached today, one reachable. The two on the host controller directly stalled in mpsse_flush() on every attempt; the one behind a USB2.1 hub answered with IDCODE 0x13636093 on every attempt, three times running. An hour went into reseating and retrying before the pattern was visible in ioreg. Also records how to pair a serial port with a programmer without flashing anything to find out: a CP2102N and a Digilent under the same hub are the same board. And that an unbounded JTAG probe wedges a cable — the first one ran ten minutes and the two cables it touched never recovered — so every probe now carries a hard timeout. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ly something to report node0 re-flashed and keyed over the wire: 6400/6400 dot products correct and 6400/6400 receipts authenticated under a key that was never published, across 100 independent runs with the port reopened each time. Until today that column would have been meaningless — every board carried a key from the git history — so census only counted arithmetic. It now counts both, and says which of three situations it is in: checked, no key file, or no key on file for this node's id. A zero that means 'not checked' is the kind of number that gets cited as if it meant 'checked and failed'. The write-once latch was tested against an adversary on silicon, not only in simulation: a second setkey carrying an attacker's key returned 0x03 KEY_LOCKED, and subsequent work still verified under the operator's key and not the attacker's. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Re-flashed from the CI artifact, came up unkeyed with correct arithmetic, took a key over the wire that has never been published: 6400/6400 correct and 6400/6400 authenticated across 100 independent runs. An attacker's second key was refused on silicon and later work still verified under the operator's key. Records the JTAG finding too, because it cost an hour and will cost it again: reachability is a bus property, not a cable property. Two cables on the host controller stalled every time; the one behind a USB2.1 hub worked every time. node1 and node2 remain on published keys. That is a bench problem, not a design problem, and the report says so rather than averaging it away. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… WE did not hold Verdict.unverifiable was added so a keyless verifier could not accuse. The ledger never asked. settle() named `.corrupt` as the one verdict that costs nothing and slashed everything else, so the new verdict went straight to the slash path — measured on hardware: node1 and node2 lost 600 mTRI each and were suspended, for the crime of holding keys the coordinator could not check. Same shape of defect three times in one session: a rule written in one place and enforced by enumerating cases somewhere else. So the fix is structural rather than another case. settle() now asks verdict.indictsTheNode(), and the mesh's outcome accounting is an exhaustive switch with no `else` — adding an outcome is a compile error until someone decides what it means. That catch-all had been printing "39 rejected as dishonest" beside "slashed: 0 mTRI". A summary that accuses and then charges nothing is either a lie or a bug and a reader cannot tell which. It was two: unverifiable receipts and jobs we declined to dispatch, both counted as dishonesty. New Outcome.unverifiable_not_charged, counted apart from corruption because corrupt is a claim about the link and unverifiable is a claim about the verifier. A node we cannot pay does stop receiving work after the tolerance — that is scheduling, not punishment, and no stake moves. On hardware now: 96 dispatched = 33 accepted + 48 unverifiable + 15 not dispatched, 0 rejected as dishonest, 0 slashed, all three stakes intact. Two regression tests, both of which fail against the old settle(). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ed process I recorded that JTAG reachability follows the USB bus: two cables on the host controller stalled in mpsse_flush() every time, one behind a hub worked every time, three consistent observations. Wrong cause. Two openocd processes from earlier probes were still alive as root, holding those two adapters — ps showed them at 1h17m. After the cables were replugged all three answered, including both that had 'always' stalled. The leak is the lesson. The probes were bounded with sudo -n openocd ... & P=$!; ( sleep 25; kill -9 $P ) & and $! is the sudo wrapper, not openocd. openocd runs as root beneath it, a user kill -9 cannot touch a root child, so the wrapper died, the timeout looked like it had worked, and the adapter stayed held. The timeout has to live inside the privileged process: sudo -n timeout -s KILL 25 openocd ... Three consistent observations of a correlation are not a cause, and this one cost an hour and produced a confident false entry in the skill that would have cost the next person the same hour. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…nally mean something All three boards re-flashed from CI artifacts and keyed over the wire with per-node keys that have never been published. node1 and node2 flashed in parallel on separate programmers: 778.755 s and 778.757 s, so 13 minutes for two rather than 26. 100 runs x 64 jobs per board, port reopened each run: node0 6400/6400 correct, 6400/6400 authenticated, 100/100 perfect node1 6400/6400 correct, 6400/6400 authenticated, 100/100 perfect node2 6245/6400 correct, 6235/6400 authenticated, 25/100 perfect, min 59 The agent's forward pass across all three: 96 of 96 accepted, 0 rejected as dishonest, 0 damaged, 0 slashed, 96 mTRI credited, all three nodes active. Every previous settlement in this programme rested on tags any reader of the git log could compute. This one does not. node2 is still the marginal board and the report says so rather than averaging it away — 97.6%, min 59 of 64. Its losses are the link, not the key: swept to its own centre rate it scored slightly worse. Also stops setkey from hiding a success behind a lossy cable. It counted a board as keyed only if 32/32 verification jobs then came back clean, so node2 was keyed and reported as not keyed. The acknowledgement's tag already proves installation — only a board holding the key can produce it — so the count now follows that, and the link quality is reported separately. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The leaked-process anti-pattern was written into the skill inside a ```bash fence — which renders with a Run button. It reads as an example of what not to do and clicks as an instruction. The operator ran it; the '...' placeholder expanded to ../.. and openocd exited immediately, which is the harmless failure mode, but the next placeholder might not be. The broken form is now described in prose and only the working command is runnable. Also records a second failure of the same kind as the first. 'sudo -n pkill -9 openocd' was reported three times as having cleared the leak. It never ran: the NOPASSWD rule covers /opt/homebrew/bin/openocd and nothing else, so pkill needs a password, and -n makes it fail silently instead of prompting. ps showed both processes alive 2h49m later. Checking the exit of the thing you ran is not the same as checking the state you claimed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…disbelieve Self-contained state: what the fleet is, what was measured, how the key works now, how to bring a board up, what the environment cannot do, and what is still open. Three things it deliberately leads with rather than buries. Every jobs/s figure this project published is withdrawn, not restated — they counted attempts, so a board answering nothing read as the fastest run ever recorded. There is still no power figure of any kind. And the port names, JTAG locations and line rates in its own tables are all unstable; only the node id is not. It also names the defect that recurred three times in one session: a rule written in one place and enforced by enumerating cases somewhere else. The fix is structural — ask the verdict, do not name the cases; exhaustive switch, no else — and the handoff asks that new code be tested against the same question: if someone adds a case tomorrow, does this default to safe or to accusing an honest operator? Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…be could not tell
node2 was written up as the marginal board of the fleet -- 97.6% correct, 25 of
100 perfect runs -- and the handoff's next action was to try a different cable
and a different hub port before believing the board. It is the same cable and
the same hub port. At 1144744 baud instead of 1186267 it returns 6400/6400.
The baud hypothesis had already been tested and recorded as refuted: re-run at
"its own centre rate" the board scored 98.08% against 98.56%, and half a percent
was read as a refutation. That rate was 1174399, from the BAUD_DIV=60 candidate
table -- and it is also outside node2's window. Every rate anyone tried came
from a list the wrong assumption had generated, so no test drawn from that list
could have escaped it. Sweeping is what breaks the circle.
Measured by sweeping the host rate in 0.5% steps, 64 jobs per step, a step
counting clean only when all eleven predictable response bytes were right on
every job:
node0 1121020..1227778 centre 1174399 +/-4.55% CFGMCLK 70.46 +/- 0.18 MHz
node1 1068248..1169444 centre 1118846 +/-4.52% CFGMCLK 67.13 +/- 0.18 MHz
node2 1121020..1168468 centre 1144744 +/-2.07% CFGMCLK 68.69 +/- 0.18 MHz
The spread is 4.97% and each board tolerates about +/-4.5%, so the windows
overlap and the claim that no single host rate can serve this fleet is wrong:
at 1144744 all three returned every job, 100 runs of 64 each, 19,200 jobs, zero
failures. Each board did the same at its own centre, and node2 twice, because
one clean run is an anecdote.
The instrument was the defect. trinet_baud_sweep.py asked six jobs per rate and
Node.initFpgaAutoBaud six probes per candidate, then took the first that passed.
A rate losing 2.4% of jobs passes six 86% of the time and one 97.6% of the time.
Neither check could fail the only case it existed to detect -- the same shape as
counting attempted jobs as throughput, and as a verdict enumeration that acquits
whatever it forgot to list.
* the sweep now runs 64 jobs per rate, checks every predictable byte, splits
failures by direction (a wrong product with an intact nonce is host->board;
a damaged nonce or identity is board->host), reports the centre of the clean
window, and prints each degradation shoulder separately rather than merging
them into one range with one misleading worst case.
* discover no longer trusts the first reply: it measures the rate it acquired
and refuses to report a board as found-and-fine at 63/64.
* auto-baud scores 64 jobs on every candidate that answers, does not stop at
the first that passes, and operates at the middle of the rates that were
perfect rather than the first of them. Verified on hardware: node0
negotiates 1174399, node1 and node2 1144744, 192/192 each.
Also fixed, found while reading the output: census printed "no published key
seen. Receipts from this fleet can be cited." whenever no run had been caught
with a published key -- including runs with no key loaded, where none could have
been seen. It now says which of the three things actually happened.
CFGMCLK figures carry the sweep step as their error bar. Printing six digits of
a number known to half a percent is how a measurement becomes a constant nobody
rechecks.
Open, and unexplained: node0 and node1 have hard window edges, one step out and
nothing comes back. node2 degrades gently instead, 96-98% clean over
1174399..1227778. Something costs that board its upper margin. It no longer
costs it any jobs, so this is a question, not a fault.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The next-actions list said "restate throughput with the corrected counter".
The command that does it has never been able to. `bench` never called
loadFleetKeys, so FleetNode.key was null on every path, verifyWithKey answered
`unverifiable` for every job, `verified` stayed 0 and the throughput line
printed 0.0 jobs/s -- on any machine, holding the correct key file or not. It
was invisible because nobody reads a bench that reports zero as a defect in the
bench.
Three more in the same function, all found by reading its output rather than
its code:
* it indexed the fleet table by a command-line slot instead of asking the
board its identity -- the identity-by-argument-order defect already fixed on
the fleet path, which hands node0's key to whichever port was typed first;
* it derived the compute ceiling from a hardcoded 71.18 MHz CFGMCLK, a figure
belonging to no board in this fleet (they measure 70.46, 67.13, 68.69). It
now comes from the negotiated rate times the divisor the bitstream ships
with, which is a measurement and cannot go stale;
* it printed the REQUESTED baud in the transport-ceiling line while computing
that ceiling from the NEGOTIATED one, so the label disagreed with its own
arithmetic.
bench also now defaults to negotiating the rate rather than to a fleet constant,
because a constant is what put the marginal board on the rate that lost it 2.4%
of its jobs.
Restated, 2000 jobs per board at each board's negotiated rate:
node0 1174399 baud 495.7 jobs/s batched x32 3843.6 78.5% of ceiling
node1 1144744 baud 483.7 jobs/s batched x32 3680.1 77.2% of ceiling
node2 1144744 baud 475.6 jobs/s batched x32 3678.6 77.1% of ceiling
2000/2000 whole on every board. NOT authenticated: the keys these boards hold
are not on this machine, so no receipt was checked. `whole` and `verified` are
counted separately and the headline says which one it is, because a transport
measurement read as verified compute is exactly the confusion this project keeps
paying for.
Batching buys 7.6-7.8x because the round trip is USB latency, 2.05 ms p50
against roughly 0.4 ms of wire time. What is left over is not the cell: the cell
is idle for all but ~30 of the ~200 clocks a job occupies and the derived
compute ceiling is 480x the transport. Any throughput claim about this node is
still a claim about a UART.
The handoff is updated where it is now wrong: node2's row measures a line rate
rather than a board, the "no single host rate serves this fleet" conclusion is
withdrawn, the lost key file and the missing sudoers rule are written down with
the one-line fix that needs a password, and the next-actions list no longer asks
for two things that are done.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
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>
The `portability` job installed yosys from apt. On ubuntu-latest that is 0.33,
and under 0.33 every synth_<family> pass returns without stats
portability_check.py can read — so the job printed "only 0 families
synthesised" and failed. Every run of this workflow since the day it was added,
on every branch, including the commit whose own message announced the
ten-family result.
The claim it guards was true the whole time. Reproduced today under both yosys
0.62 and 0.65: ten families agree at 1082 flip-flops, intel_alm at 1092 because
its register cell absorbs reset logic, and not one infers a multiplier. What was
broken is the gate. docs/TRI_NET_PORTABILITY.md cited it as "now checked rather
than remembered" while nothing had ever checked anything, and a real regression
would have arrived as one more red run on a workflow that was always red.
CI now runs the check inside the pinned regymm/openxc7 image, the way
ax7203-format-cost.yml already did after hitting this exact problem ("build
yosys 0.63 from source (not Ubuntu 0.9)"). The script prints the yosys version
alongside its results, because a portability number with no tool version
attached cannot be compared with the one before it.
Looking at the output found a second defect, in the check itself. A family that
synthesised but whose register cells the script could not name went into
`results` — counting toward "N families checked" — and was then dropped from the
flip-flop comparison by a truthiness filter, so it inflated the headline while
contributing nothing to the invariant that headline is about. analogdevices
under yosys 0.65 does exactly this: 2686 cells, zero recognised flip-flops, and
the run announced eleven families when ten had agreed. Such a family is now
named in the output and counted in neither direction, and the run says ten.
The tables in docs/TRI_NET_PORTABILITY.md are re-measured. They read 819 and
831, from before the receipt key started arriving over the wire and brought a
key register and its write-once latch with it. The design changed; the number
followed. The agreement did not, which is exactly why this check asserts the
spread rather than the value — and why the stale number was never a problem for
the check, only for the prose.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…o the wire The report's headline sentence and its results table both said 1313 LC. The handoff, three files away, said the setkey change took the cell 1292 -> 1484. Both cannot be true and the report is the document people read. Measured under yosys 0.62 with the chparams the fleet CI actually builds with (USE_DNA=0, FALLBACK_NODE_ID set, BAUD_DIV_P=60): 1480 LCs, 1046 flip-flops, no DSP48 and no DNA_PORT in the netlist. Synthesised with defaults instead it is 1499 LCs and DNA_PORT is present, which is the difference the chparams make and the reason the parameters belong next to the number. Also corrected in docs/outreach/ternarycore-issue-draft.md, which quoted 1313 in a paragraph that would have gone to a third party. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…as 0% clean
node0 was re-flashed today, came up correct and unkeyed, and both tools I
rewrote yesterday called it broken. They compared the response status against
0x01 exactly. A board between a re-flash and setkey answers 0x04 NO_KEY and
computes the dot product perfectly — discover printed "0.00% clean" and the
sweep would have found no clean window anywhere, at exactly the moment a fresh
board's rate has to be measured.
Written yesterday, in the session that fixed three other checks for treating a
legitimate state as a failure, against a handoff that says in so many words:
"An unkeyed board answers 0x04 NO_KEY with a real dot product. Anything
measuring arithmetic must call statusMeansComputed()."
Both now accept the statuses that mean the arithmetic is real, {0x01, 0x04},
and print which of the two the board is in — discover's line now reads "no key
yet" or "keyed" rather than leaving the reader to infer it from a percentage.
Recorded with it, from the same session:
* node0 re-flashed (778.76 s) and re-keyed with a key from openssl rand that
has never been printed anywhere. 100 runs x 64: 6400/6400 correct,
6400/6400 authenticated, 100/100 perfect, at its measured window centre of
1174399 baud. Throughput authenticated for the first time: 481.4 jobs/s one
at a time, 3788.0 batched x32, 77.4% of the transport ceiling, 2000/2000.
The write-once latch was re-confirmed on this configuration rather than
carried over from the last one.
* Every AL321 stalled in mpsse_flush() with no leaked process beforehand;
replugging fixed it. The locations were not at fault, and there is a control
that proves it in seconds: a bogus `adapter usb location 9-9.9` errors
instantly with "no device found", so a location that stalls is one that was
found and opened.
* The recipe on record for bounding a privileged probe, `sudo -n timeout -s
KILL 25 openocd`, cannot run here — there is no timeout and no gtimeout on
this machine. A foreground wrapper killed by an outer timeout leaves openocd
alive as root and a user-level kill cannot touch it. That cost two adapters
today until the operator ran `sudo pkill -9 openocd`. Start it in the
background and poll instead.
* Three "Digilent Adept" adapters appeared where two AX7203s had been. They
read IDCODE 0x23727093 — a Zynq-7020, not the 0x13636093 Artix-7 this
project flashes. Asking them, with init and shutdown and no pld load, is
what identified them; widening the config's device filter until something
answers is how a bitstream reaches a device nobody identified.
One board of three. node1 and node2 were not on the bus, so nothing here is a
fleet result.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…-to-head (#430) Research artifacts for the ternary-native GoldenFloat format family (GF-T), the publication material behind the arXiv:2606.05017 / 2606.09686 updates. - GFT16_BEATS_TEKUM16: GF-T16 vs tekum16 head-to-head (measured x3 mid-range, x5.5 far-range; uniform 9-bit mantissa vs tekum's tapered 4; no regime decode; exponent added natively in balanced ternary). Adder 461 LC / 0 DSP. - GF_T_GOLD_STANDARD_LADDER: full GF-T4..GF-T1024 ladder (Et trits per rung, adder LC, all 0 DSP). - GFTERNARY_vs_BALANCED_TERNARY_HW: GFTERNARY {-phi,0,+phi} is a 2-bit phi- alphabet on a float mul (2 DSP / 1191 LC), NOT ternary compute; the real ternary core is TF3 / trinet_mac32 (0 DSP / 398 LC). - XC7A200T_GF16_DATAPOINT: bare-core combinational Fmax (~323 MHz) vs routed Fmax; board reconciliation (XC7A200T-FBG484). - ARXIV_GFT16_SNIPPET / ARXIV_GFTERNARY_HW_SNIPPET: ready-to-paste LaTeX. - SUBMISSION_PACKAGE: index of the v4/v3 paper updates (author credentials required to actually submit; nothing here is a submission). Off-path conformance oracles (reference only, not on the codegen path): - conformance/gft16_ref.py : bit-exact GF-T16 encode/decode/add/mul. - conformance/gft_ref.py : parameterized GFTFormat(exp_trits, mant_bits), covers the whole GF-T4..1024 ladder. Co-authored-by: SSD DDD <ssdm4@MacBook-Pro.local> Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
A 100% failure rate is a broken harness until proven otherwise. A sweep reported "PARSE OK: 0 FAIL: 496" — read literally, the parser was dead. It was exit 127: cwd had reset and t27c builds to the workspace target dir, not bootstrap/target/release/. The tell was the shape, not the content — real breakage is ragged, a clean 0% or 100% means the measurement never reached the thing measured. True count was 496/496. A gate that is always bypassed is not a gate. scripts/tri was broken for every subcommand (--repo-root passed before the subcommand, but it is a per-subcommand clap option). It is pre-commit Gate 1/4, so it was not fixed, it was routed around with --no-verify — invisible in history. When a hook blocks you, read the hook before satisfying it; the block is a symptom. And run the fences in your own README: doc-sync passes edit prose and never execute the commands they ship. Ask who occupies the corner you claim to own. COMPETITORS.md was sourced and honest in tone, named five commercial NPUs it declined to race, then claimed the formal/assurance corner while naming nobody in it — a corner that holds Vericert, Kami, and Amaranth, all ahead on that axis. A competitive document is not honest because each sentence is true; it is honest when the omissions do not do the arguing. Refs gHashTag/t27#1951 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
validate-conformance printed "43 valid, 58 empty/skipped". That went into a report, a NOW.md entry, a GitHub issue, and a memory file as "the corpus is half-hollow", and became the next wave's headline recommendation: populate the empty files. Zero were empty. The validator used .as_array() and the corpus stores vectors both as arrays and as objects. 45 of the 58 were fully populated, 8 were schema files, 5 were benchmark reports. Among the false positives was FORMAT-SPEC-001.json -- the numeric SSOT the positioning rests on, reported as empty by its own repo's validator. Two rules recorded. When a count is about to become a plan, open the objects it counted -- sampling across categories, not depth, since the 58 held four distinct shapes and three files of one shape would have confirmed the wrong conclusion. And a gate with a high false-positive rate is worse than no gate: nobody reads warning 43 of 58, which is how a CLARA coverage file covering 7% of the corpus stayed hidden for months. This is the third instance of one failure mode in this campaign, now stated in general form: the defect is never a wrong number, it is an unexamined label. "FAIL: 496" meant binary-not-found. "58 empty" meant object-shaped. Both were accurate counts of something other than their word. Refs gHashTag/t27#1951 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Three consecutive waves each found one gate enforcing something weaker than its label. check-now claimed NOW freshness and tested nothing (broken wrapper, bypassed with --no-verify). validate-conformance claimed a populated corpus and tested array-shaped payloads only. Gate 2/4 claimed "seal coverage" and tested that a file exists -- while 730 seals verified zero, 480 of them written the same day as the commit that rewrote the specs they sealed. Presence is not integrity, and only presence was enforced, so the drift was structurally invisible. The audit that finds this class in one pass: for each gate, write down the property its name claims, then read it and write down the property it tests. The gap is the hole. Two riders. A gate that cannot fail teaches people to route around it -- the always-red Gate 1/4 produced --no-verify commits, which disabled the other three. And check file resolution, not just the predicate: Gate 2/4 resolved basename -> gf16.json while seal --verify reads a path-derived numeric_triformat-gf16.json, coinciding only because macOS is case-insensitive. Two naming schemes for one artefact is a defect even when every test passes. Separately: evidence citing a command nobody can run is not evidence. clara_spec_coverage.json carried "bash scripts/clara/demo.sh -> 20/20 passed" for four months; that path does not exist in the repo. There was no claim to narrow. Run an evidence file's own stated reproduction command before reading its numbers. Corollary on scope: regenerating a measurement is repair, rewriting a baseline is a decision. Re-running coverage was mechanical. Re-sealing 496 specs would canonicalise whatever current codegen emits with no oracle that it is right, so it was reported and left for a human. An audit that quietly re-baselines what it audits has destroyed the evidence it was sent to check. Refs gHashTag/t27#1954 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Three lessons from the gate-adequacy wave in t27. Redirect the vacuity oracle at the gates themselves: for each gate, apply a mutation that should violate the claim it guards and require it to go red. Three phases, and the first two make the third mean anything -- a baseline where the unmutated build passes everything, and a control with a semantically neutral edit where everything still passes. Skipping the control is the subtle failure, because a gate that fails unconditionally scores 100% on mutation testing. Include at least one mutation that makes the system inert rather than wrong. Stalling the system leaves every safety property true; only liveness notices. If no gate goes red when the feature is disabled entirely, the suite is measuring silence. And state the lower bound the method gives you, at the same prominence as the number. Mutation testing bounds from below, never from above. A result reported without its ceiling gets cited later as if it had none -- usually by whoever produced it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…lation is Four lessons from the maximum-size sweep in t27. A bounded check that cannot reach the counterexample reports success and establishes nothing -- two modules passed a wrap property whose violation needed 4096 writes against a 24-cycle bound. Scale the model until the counterexample fits, and state what scaling changed. Generalises to fuzzing, load tests and soak tests: a green result from a search that could not have found the bug is not evidence. When a correct fix does not make a property pass, there is a second cause. The most valuable defect of the wave was found that way; the temptation to revert the fix or weaken the property destroys the signal. An unconstrained input is an adversary -- two refutations were faults in my own harness and looked exactly like design defects. A refutation is a claim about the environment until the environment is pinned down. And stop patching after the second attempt: the next action is a counterexample read carefully, not a third patch. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…nobody fixed Three lessons from the write-pairing audit in t27. A regex for a defect shape returned zero candidates because both instances had just been repaired -- the scan measured my memory, not the code. Enumerate the class (every write port) rather than the symptom (a self-incremented address), and ask the semantic question. That found a third port never checked at all. A property a known defect would have passed is the wrong property. The first property only required the write address to increase, which permits skipping slot 0 -- exactly what the second defect did. At the moment you fix a defect, run your property against the pre-fix version; if it passes, you wrote a property describing the fix rather than the requirement. And do not diagnose with a tool that just contradicted itself: a trace showing the guard signal low throughout cannot violate a property guarded on it. Fix the instrument, validating it on a case whose answer you already know, before trusting it on one you don't. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…strument Four lessons from fixing the counterexample reader in t27. Two waves produced nothing on one finding, both concluding the design was subtle. The counterexample had never been parsed -- the trace showed a guard signal low throughout, which cannot violate a property guarded on it. Watch for a diagnosis that contradicts its own premise; that is the instrument reporting on itself. Validate a diagnostic reader against a known answer, in CI. Two concrete traps: a .json extension does not mean parseable (RTLIL names contain backslashes that break JSON escapes), and compressed formats need full expansion (WaveJSON's means repeat, and skipping it loses most of the trace while appearing to work). Query the trace rather than reading it -- encode the failing assertion as a predicate and let it find the row. Eyeballing a 30x90 table is how the earlier misreadings happened. And refine the rule on withdrawing fixes: withdraw one that misses its target when it costs something, keep it when it is independently correct. The test is not did it work but would I write this having seen the code fresh. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Four lessons from closing the DMA in t27. The defect that survived four waves: local_we was cleared in READ_DATA's else, which runs only while in that state. Every other state left it untouched, so a one-cycle pulse held high across transitions and kept writing at a stale address. Any signal meaning this cycle do X needs a default before the case, not a per-branch clear. Scale everything the scaled signal touches. Narrowing a DUT signal for tractability while the harness kept the old width left undriven bits, and x fails every comparison -- producing a confident refutation of an innocent design. Also: learn what your trace reader prints for x versus for no data. Report each property's discriminating power separately. Two properties proved after the fix; only one also refuted when the fix was reverted. A property that passes on both the fixed and broken design contributes zero information, and saying so is the difference between a result and a number. And judge a sweep by total defects found, not hit rate against its stated target: this one found five, four unrelated to what it was aimed at. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…n its own Four lessons from closing the last open defect in t27. Three fixes were withdrawn because each broke an unexplained baseline; the defect was recorded and gated rather than patched around. Eight waves later the same fix was re-applied unchanged and the baseline proved -- the blocker had gone away with three other defects fixed meanwhile. Unexplained blockers are often symptoms of defects not yet found. A global flag cannot answer a per-instance question. Three attempts gated on one input_loaded bit when the property asked about a specific buffer. The tell is an arity mismatch: if the property mentions a selector, the state backing it must be indexed by that selector. Prefer an observable error to a stall. Refusing to start deadlocks whenever the unsafe condition is legitimate, and a stalled system passes every safety property. Do not perform the unsafe operation, complete anyway, raise an error the caller can see -- then verify with liveness that work still happens. And an expected-refutation gate is how an open defect closes itself: CI asserts the property must still fail, so the fix turns the build red and asks for promotion. Pair it with a gate asserting no such guard remains. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…lish both Three lessons from measuring the scale ceiling in t27. All properties proved is not a property of a design; it is a property of the design paired with the bound the checker ran at. Measure the ceiling and publish it with the claim -- it buys headroom (does the claim hold above what CI runs) and cost shape (which axis is expensive). Raise the axes together at least once: each alone can pass while the combination does not. Undecided is a third verdict, not a shade of pass or fail. Four of five module suites extended to 4x their bound; one became intractable at 2x, so its proof is real at its own bound and nothing is known beyond it. That line names the one place a deeper defect could sit unseen, and collapsing it into either binary would have erased it. And check the ceiling on a schedule, failing both when a scale starts refuting and when it stops completing -- a refutation means a defect at depth, a new timeout means the claim quietly shrank. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Three lessons from splitting a formal suite in t27. A suite verified in one invocation returns one answer describing its worst member. The parts summed to under 90s while the whole exceeded 240 -- a combined instance can be superlinearly harder than its pieces -- and the single number concealed that two members were verified four times deeper than the third. Splitting bought a 2.9x deeper bound at the same wall time and named the failure. A limit attributed to the system may be a limit of the question. One module was recorded as the place a deeper defect could hide because its proof would not extend; re-asking one property at a time removed the limit entirely. The tell is a large gap between the cost of the whole and the sum of the parts. And replacing a global count with a local invariant is the right instinct, but establish the alignment first as its own measured question -- assert the relation at each candidate offset and see which proves. Guessing it inside a larger property makes every failure ambiguous between wrong offset and wrong idea. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…far it extends Three lessons from mapping a formal suite in t27. A wave spent measuring proof depth produced a careful table of ceilings, and two entries had no ceiling -- proved by k-induction, then re-measured with bounded checking and reported as proved to 8x the bound. Measuring the extent of a claim that has no extent produces a number worse than none, because it looks like a limit where none exists. Classify the result before quantifying it. The same parameter name means different things in different modes: -seq is a search bound under BMC and an induction depth under tempinduct, and raising it in the second case is pure cost. Key bulk edits on the mode flag, not on the parameter -- the edit that treats all call sites alike quietly does the wrong thing to a subset. And an aggregate can be uninformative in a way that looks informative: six green verdicts where two meant something categorically different and one was the minimum over members differing by two orders of magnitude in cost. A per-member map names the single genuinely shallow item, which is the only actionable part. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Three lessons from the engine-suite split in t27. Splitting one suite per-property bought a 2.9x deeper bound; the same move on another bought nothing. The difference is measurable in advance -- cheapest to dearest ratio 436x versus 1.08x. Where one member dominates, isolating it lifts the achievable depth; where the shared setup is the expense, splitting buys attribution only. The diagnostic is one run: time a trivially true member. A partition produced by a timeout is a partition of the timeout. A sweep reported 8 of 20 proved, inviting the false reading that those 8 are easier; all 20 proved given time. The tell was a tautology in the failing group -- put a known-trivial control in any cut-off run and check which side it lands on. And use the identifier a tool returned, never the one you predicted: a commit body said Closes #2012 when the issue created was #2014, and #2012 was an unrelated open issue the merge would have closed. Sequential-looking identifiers are the dangerous case, because a wrong guess is well-formed and points at something real. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… for it Two lessons from correcting a published scale ceiling in t27. Naming the error that a partition produced by a timeout is a partition of the timeout prompted a sweep of prior published numbers, which found a ceiling recorded one wave earlier as undecided at depth 80 that in fact proves in 396s against the 300s budget used. A newly understood failure mode is a query to run against everything already published, not just future measurements. And write the budget into the result -- undecided within 300s, never undecided -- so a later reader can tell a limit from a finding. Batch overhead tells you where the cost lives: one suite's batch was worse than the sum of its parts, so cost lives in the properties and splitting helps; the other's batch cost 1.4x a single member, so cost lives in the shared model and splitting cannot help. Time the batch, time one member, divide. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Four lessons from locating the solver cost in t27. Replacing a subsystem with a same-interface stub answered where the time goes in two runs, but under it all twenty properties failed including a tautology -- and the baseline check showed the stubbed build did not pass with no properties at all. Timings from a stub are usable; verdicts are not. First time this rule caught my own replacement rather than a change to the design. Cell count is a poor proxy for solving cost: the stub removed 31% of cells and 0.4% of flops and cut solve time 8x, because unrolling multiplies combinational logic once per step while state grows linearly. When a bounded proof is slow, look for wide combinational structures, not register count. A knob exists only if someone built one. Memory depth was scalable because it was already a parameter; the datapath width was a literal at 26 sites across six generators. Scalability for testing is a property of the code, not the tool. And do not start an invasive refactor to serve a measurement, late in a session. Measured and scoped leaves the next session a task with the full picture; a half-finished refactor trades a known cost for an unknown one. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Three lessons from adding read-side properties in t27. Fifteen waves rested on a baseline run -- the design compiled without its properties -- that never excluded a single one, because the tool's -formal flag predefines the FORMAL macro. One three-line module and two runs detect it: compare cell counts with and without the define, and identical means the guard is not a guard. The deeper cost was diagnostic: an earlier wave spent four rounds trying to separate a failing probe from a failing property when no flag existed that could. Distinguish the tool failing from the check failing. A harness reported REFUTED in 0.1s because an input file was missing. Parse the tool's own words for the specific outcome rather than trusting the exit code, and treat implausible timings as evidence -- a check that normally takes 40s and fails in 0.1 has not run. Third instance of this shape in one campaign. And add the mirror of every property you have. Forty propositions all constrained writes; the read path had no coverage and nobody noticed because the write properties kept finding real defects. Read your property set as a list of shapes and ask each one about the other direction. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Three lessons from a failed diagnosis in t27. To decide whether a property failed because of the design or because its operands were undefined, I asserted a == a. It proves, and it is meaningless: the optimiser folds algebraic identities to constant true before any value is considered. A probe whose result is determined by its own syntax tests nothing -- before trusting a diagnostic assertion, ask what input would make it fail. When a method turns out to be mis-specified, re-run what it touched rather than reasoning about the blast radius. Six witnesses, six re-runs, six identical verdicts: the claim is now measured instead of argued, and the re-run surfaced the precise condition under which it would have mattered. And the same folding trap sits inside property sets: a long-standing proved property is literally assert (bram_addr == bram_addr). Vacuity checking asks whether a guard is reachable; it does not ask whether the body is discharged by the optimiser. Both are ways a property can be free. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…t vacuity Three lessons from auditing a property set in t27. A suite gated itself on a check count, because a green run over an empty set proves nothing. Five properties had bodies of the form X == X, folded to constant true -- and each still emitted a check cell, so the padding was counted by the very gate meant to catch an all-vacuous set. Two notions of free are at play and typically only one is gated: an unreachable guard, and a body discharged by the optimiser. When a change appears to break something, reproduce the failure without the change. I attributed a refutation to my edit, then to a subtle interaction, and built a plausible theory for each; re-running the unchanged file refuted identically. The cost of skipping that run is not a wasted run, it is a confident documented wrong explanation. And a detector that searches text will match prose: classifying steps by searching for a flag reported two suites using an unbounded method when only one did, because the other step named the flag inside a comment explaining why it was not used. Match on structure, not substrings. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Three lessons from building a free-property gate in t27. The gate and its own control ship in one CI step: four injected free shapes must be flagged and a real property must not. The negative case matters most, because firing on everything scores perfectly on positives alone. A check that is not itself checked is an assumption wearing a green tick. A detector that produces false positives is worse than no detector. A stronger semantic version flagged six real properties -- common-subexpression elimination lets a genuine property add zero net cells -- so it was withdrawn rather than tuned. A gate that cries wolf on real work gets disabled by whoever hits it next, and takes the true positives with it. Four dead ends were written into the module instead, which costs nothing to carry and is worth more to the next attempt than a broken tool in the pipeline. And ship the smaller thing while stating what it does not do, in the same paragraph as its purpose. Every overstated claim in this campaign was overstated at the moment of writing, by someone who knew the limit and did not write it down. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…iscriminator Four lessons from attributing a failing check in t27. After two failed attempts to decide whether a failing check meant the system was wrong or the check was wrong, what worked was writing the same claim a second, structurally different way. Agreement exonerates the weaker formulation and implicates the system; disagreement implicates the approximation. It does not depend on reading tool output correctly, only on two checks agreeing. Validate a new instrument against what it must NOT say: assert the negation of what you expect and require a counterexample, which proves the instrument can move. Asserting the expected value proves nothing, and that was how two earlier attempts went wrong. A boolean is not a count. A defect was closed by tracking whether a buffer had been written; the finer defect was that nothing related how many slots a consumer reads to how many a producer wrote. When a guard answers did anything happen, ask what happens when less than enough happened. And $past(x)[1:0] is not legal Verilog -- part-selecting a system function call. Under a harness that reads any nonzero exit as a verdict it would have appeared as a refuted property; it appeared as a tool error only because that separation was already in place. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…enforce a per-cycle invariant Three lessons from a withdrawn fix in t27. A property required that at the moment of each read the slot be already written. The attempted fix gated the start of the operation on a count. It could never work: a start-time check says nothing about what happens during the operation, where a producer fills one buffer while a consumer drains another. The mismatch was not the threshold or an off-by-one, it was that a per-cycle claim needs a per-cycle guarantee. Before writing a guard, name when the claim must hold and check the guard is evaluated at the same rate. Withdraw on two counts, not one. The standing rule was withdraw a fix that misses its target and costs something; this hit both halves in one run, which made the decision immediate. The tempting failure is keeping a change that fails only one half -- it did not fix the bug but is harmless, or it broke one test but is the right direction. And record the eliminated shape where the next attempt will read it: in the file it would have changed, not only in a commit message. Three waves have gone into one defect, and that is progress only if the eliminations are visible from the code. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ories Three lessons from locating a long-open defect in t27. Six waves went into one failing check -- two inconclusive trace reads, an invalid discriminator, a withdrawn fix. What finally located it took three runs: unconstrained refutes, one added assumption proves. That is a bisection of the input space, and it is far more reliable than reading a counterexample, because each run answers a question you chose rather than requiring you to interpret a dump. Do it before reading traces, not after. A module-level guard does not travel to the paths that bypass it. A sequencer was proved in isolation to emit no work for a zero-sized job, and the engine performed a read anyway, because the address came from a counter and the valid from skew registers -- neither passing through the proved guard. Enumerate a guard's consumers and find the ones that derive the same information independently. And degenerate inputs deserve the same sweep on every side of a datapath. Recording that we swept zero-sized inputs without recording which surface leaves an impression of completeness; the honest form names the surface. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…nosis Three lessons from fixing a live-configuration defect in t27. A failing check was fixed by assuming a non-zero count, and the obvious conclusion -- the bug is the zero case -- was published and wrong. A weaker assumption also restored the proof: a stable count, including a stable zero. The necessary condition was the change, not the value. Every assumption that restores a proof describes a sufficient condition; only the weakest describes the cause, and the strong one is usually the first you think of. Configuration read live by a running state machine is a defect class. A sequencer compared its counter against a host-writable limit every cycle, so a write mid-run moved the terminator underneath work in flight. Latch the configuration at the start of the operation and run from the copy. Look for it wherever an operation has a duration. And ship a fix that is right on its own terms even if it does not close the case. The test: would I write this having seen the code fresh, with no knowledge of the open bug? If the only argument for it is the bug it failed to fix, withdraw it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… time Three lessons from closing an eight-wave defect in t27. An interlock was withdrawn with a conclusion that read like a law; three waves later the same interlock, unchanged, closed the defect. The conclusion was conditional on the design at that moment, and a separate fix removed the condition. What made the re-attempt cheap was recording the reason beside the code rather than only the verdict -- a verdict closes the door, a reason leaves it open for the day the condition stops holding. Some defects need several changes, none of which look like progress alone. Three changes over eight waves, each leaving the property still failing. Under a strict withdraw-anything-that-does-not-fix-the-target rule the first two would have been reverted and the third would never have worked. The rule that saved them: withdraw a fix that misses its target and costs something, keep one that is right on its own terms. And building the instrument is most of the work. The defect was one line of missing state; finding it took a trace reader, a free-property gate and an assumption-bisection method. When a bug resists two honest attempts, the next move is usually a first attempt at seeing it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…d have Three lessons from a clean read-side sweep in t27. A clean sweep and a broken sweep produce the same report. Three new properties proved and found no defect, which was worth nothing until each was shown capable of failing -- body replaced by assert(1'b0) under the same guard, all three refute. Without that, we looked and saw nothing is indistinguishable from we did not look. Derived state cannot drift; independent state does. Four write-side defects against one read-side defect was not attention bias: the write paths each carried their own counter and every defect was two of them disagreeing, while the read pointers were derived from a single source. When two registers track the same quantity, that is a defect site -- prefer deriving to duplicating, and when duplication is unavoidable the relation between copies is the property worth asserting. And state the surface a sweep covered, not just the class. We swept zero-sized inputs sounds complete; zero-sized inputs on the write paths is what made the read-side gap visible later. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…the stubbed thing costs Four lessons from killing a four-times-deferred refactor in t27. Stubbing a module made a proof 8x faster and justified a six-file refactor. The refactor was worth 1.5x. The 8x measured something else: removing the module's instantiation left its wide inputs unused, and the optimiser deleted the whole datapath feeding it. Removing a consumer removes its producers. Attribute cost by shrinking a component, not deleting it, and measure the change you actually intend on a small scale first. Cell count is a poor proxy for solving cost: two builds fourteen cells apart differed eleven times in solve time, and one with 161 fewer cells ran slower. Static size can suggest hypotheses, not rank them. Re-cost a deferred item before picking it up. Four deferrals carried the original estimate forward; when it reached the front of the queue it was stale and wrong by 5x, and re-costing closed it permanently. And git status is part of the verification: a file was modified but never committed for twenty waves, so local runs and CI used different inputs. It elaborated either way, so nothing went red, which is why it survived. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…cks that would catch it Three lessons from a census wave in t27. A property refuted, and the obvious fix was to constrain the environment more tightly. It worked, and it also pinned an input to zero forever, so two reachability witnesses stopped firing while every property still passed. An assumption is not a local edit: it removes behaviours from every property in the file, including the ones asserting that behaviours are reachable. When a fix is an added constraint, re-run the reachability checks; and prefer fixing the property, which is scoped to itself, over constraining the environment, which is scoped to everything. A suite composed entirely of things that must pass cannot detect its own over-constraint. Turn an explanation into a target list. The observation that independent state drifts and derived state cannot was converted into a census of every counter and derived copy, yielding three named pairs to attack and a demonstration that the rest of the design cannot hold that defect class. And a gate's own pattern list is where its false positives hide: an allowlist checker reports violations that are really gaps in the list, so it needs a known-good negative control of its own. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…hat behaviour remains Three lessons from auditing assumptions in t27. A campaign added reachability witnesses to its integration suite and never to the module suites, because the top level was where stalling was the visible risk. An over-constraint later appeared in a module file and was caught by a top-level witness -- coverage overlap, not design. The gap is structural: an assumption file with no reachability probe is a place where over-constraint is invisible by construction, because adding a constraint makes every property easier to prove and the symptom is everything getting greener. A no-findings sweep needs a control run every time. Twelve clean probes are indistinguishable from twelve broken probes until one is shown failing; reinstating a known-bad state from the campaign's own history is the cheapest control and the strongest evidence. And scope a negative result by what it cannot see: these probes check each module's main activity, so a constraint removing a rare interleaving would pass all twelve. That sentence belongs in the result, not in a follow-up when someone finds the gap. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ision, not a queue entry Three lessons from abandoning an invariant in t27. One property took three waves and never landed, each attempt ending one insight short -- the shape that keeps a task alive indefinitely. The fourth wave was not spent; the item was closed with written reasoning, because the pair it would constrain is already covered by two properties that did land. Carrying a nearly done item is not free: it occupies the queue, justifies the next attempt by the sunk cost of the last, and makes every plan slightly dishonest. The test is whether it would be worth doing if proposed fresh today with no history. Negative results are worth keeping only where the next attempt will look. Four measurements live as a comment in the file that would have to change, above the properties that did land -- not only in a commit message or an issue. A negative result filed where nobody looks is indistinguishable from never having run it. And before believing a refutation, check the probe is not simply too strict: a status output cleared in a terminal state lags its state register by a cycle, so properties asserting they move together fail on correct hardware. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ed underneath it Three lessons from re-measuring a scale ceiling in t27. A ceiling was measured, published and gated; ten defect fixes and six properties later, three of six configurations no longer completed. The claim had been false for some time and nothing reported it, because the gate only re-checked the scales it was given rather than whether those were still right. Put the re-measurement on the same schedule as the changes, not the calendar. Re-baselining is maintenance; say so, and distinguish it from weakening. A gate demanding scales that no longer complete would be a permanent red that people learn to skip. The test before relaxing any gate: can I state what changed in the world that makes the old expectation wrong? If the honest answer is nothing changed, it just fails now, that is a defect. And measure the verification apparatus separately from the system: the design alone proved in 5.5s, with its properties and their tracking state 126.7s. The scaffolding cost 23x the thing it verifies, so the slowdown blamed on new interlocks was mostly the properties added alongside them. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Three lessons from measuring a property set in t27. Four of 26 properties accounted for 75% of the proof time, because they needed ten pieces of dedicated tracking state that the other 22 did not. Removing just those four restored the verifiable depth from 40 to 80. The instinct when a check gets slow is to simplify the subject; the measurement said the apparatus was the problem, and inside it a small minority. Disable each check in turn and time the rest before optimising anything. Splitting a check set is not weakening it, so long as both groups run and the bound each is checked at rises or holds. The test: after the split, is any property checked less thoroughly than before? If no, it is a scheduling change. And two failed attempts at the same edit are a signal about the edit's shape, not about persistence. Both failures here had one root -- the things to be wrapped are scattered, not adjacent -- and the second failure established it. When the same edit fails twice for related reasons, characterise the structure before trying a third time. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… of the output Three lessons from landing a property-set split in t27. An edit adding ifdef-style guards can land correctly for the configuration you test and wrongly for the one you do not. Three checks caught it: every configuration elaborates, the partition is exactly what was intended measured by per-item guard depth in the output, and the guards balance. Checking it compiled would have passed the broken version. Scattered things look contiguous until you print their positions. Two attempts failed assuming four items and ten dependencies sat in one block; they form four regions with an unrelated item inside what looks like a fifth. The third attempt began by dumping line numbers and reading the region -- not more care in the edit, but establishing the structure before editing at all. And splitting work by cost rather than importance can raise every bound at once: four checks needing dedicated state cost 75% of the runtime, so isolating them let the other twenty-two run four times deeper while keeping their own depth. It only counts as free when every item's coverage rises or holds -- say so and check it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Wave 606's lessons. A reachability probe per activity does not cover the reachability of their combinations -- twelve probes each said the module does its job while a constraint removing a rare interleaving stayed invisible. Choose which interleavings to probe from defect history rather than combinatorics. Validate each probe by removing its own target, one at a time. The trap worth the most: a control that fails to remove the thing it targets tests nothing, and reads exactly like a blind probe. Suspect the control before the probe. Plus the tool wall -- $past inside an async-reset block is rejected by async2sync outright -- and the depth cost: an interleaving witness needs roughly double the seq bound of the activity witness it extends.
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.
Three commits. The first answers a question that was asked; the other two are
things found while trying to answer it, and they matter more.
The cell is portable, and that was the surprise
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.
Splitting
trinet_node_v2_ax7203.vfound exactly two Xilinx primitives —STARTUPE2for the clock,DNA_PORTfor the device identity — both boardconcerns, not node concerns. With those lifted into a wrapper, the core
synthesises with zero errors on ten families from eight vendors and no
inferred multiplier anywhere. Nine of the ten recover 819 flip-flops; Intel
ALM finds 831 because its register cell absorbs reset logic the others express
separately.
The wrapper instantiates the core rather than keeping a copy, so the claim
cannot rot while both files still build. CI asserts the invariant — sequential
state agrees, nobody infers a multiplier — not the numbers, which would fail on
a yosys upgrade for no reason.
This does not establish portability of product: synthesis is not P&R, no
non-Xilinx mapping has met timing, and only xc7 has run on silicon. It also does
not make anyone want the IP. The recommendation to defer option C does not
change — its real obstacles were never engineering.
Four numbers were wrong
Found by pointing the host at the boards and disbelieving the first thing it
printed.
The third board was never broken. It had been recorded for a day as a wiring
fault — configured,
DONE=1, UART silent. It answers at 1124474 baud against ahardcoded 1186267: a 5.2% error where a UART tolerates about 3. Swept, it scores
6400/6400 over 100 independent runs, equal to the best board in the fleet.
The cause generalises: CFGMCLK is an untrimmed RC oscillator, and these three
dies run at 71.18 / 70.46 / 67.47 MHz — a 5.5% spread, not the 1.25% that
two samples had suggested. Line rate is now negotiated per board.
Every board is running a receipt key published in this repository. W01 nulled
the keys in the source and never reached the silicon. node0 verifies 64/64 under
0x00..0x0f, node2 63/64 under0x20..0x2f. Every "keyed receipt verified onsilicon" result this project has reported is a tag any reader of the git log can
compute. A compromised key and a good key are indistinguishable to any test that
only asks whether the tag matches, so the suite stayed green. "Fixed" meant the
source changed and nobody checked the artifact.
Throughput counted jobs that failed.
jobs_per_sdivided by attempts. Aboard 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. Every published jobs/s figure is withdrawn rather than restated.
The host picked the wire format from its own config file. Response width came
from
key != null; the width belongs to the bitstream. A keyless host read 15bytes of a 19-byte response and offset every later read by four — a healthy board
reporting
MalformedResponseforever, and throughput defect's accomplice.Statistical base
100 independent runs × 64 jobs per board, port reopened every run (the FPGA frame
parser survives the host process, so that matters):
node2's loss is not the baud — swept to its own centre it scored slightly worse.
That hypothesis is cleanly falsified and the marginal link stands.
New laws and guards
Verdict.unverifiable— the fleet slashed an honest board 400 mTRI over amissing key-file entry. Holding the wrong key is a statement about the receipt;
holding no key is a statement about the verifier, and only the first costs stake.
protocol.publishedKeyUsed()— a board on a published key gets no credit andno slash. It is honest and useless at the same time.
conformance/key_default_check.py— null defaults in RTL, explicit keys intestbenches. Both rules were broken at once and neither failure was visible:
nulling the default silently disabled the testbench guarding the receipt, which
had failed 0/6 ever since. CI breaks each rule on purpose to prove the guard
still fails when it should.
180 tests pass across protocol, node, ledger, mesh, model and agent.
What this does not do
The boards are not re-flashed. Until they are, no receipt from this hardware is
evidence of anything, and the fleet correctly refuses to settle — it now explains
that instead of dying on
NoEligibleNode. That is one day of work and it gateseverything downstream.
🤖 Generated with Claude Code