TRI-NET: three boards, ten families, and four numbers that were wrong - #355
Open
gHashTag wants to merge 186 commits into
Open
TRI-NET: three boards, ten families, and four numbers that were wrong#355gHashTag wants to merge 186 commits into
gHashTag wants to merge 186 commits into
Conversation
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>
Applying the gate audit to CI found three of nineteen workflows whose entire job body was an echo statement -- seal-coverage, schema-validation, check-now-freshness -- each reporting green on every PR. The README cited one of them as evidence that conformance vectors were validated. That row was backed by an echo. This is the terminal form of the claimed-vs-tested gap: not a weak proxy but no test at all, wearing the name of one, and invisible from every angle except opening the file. grep -L for workflows whose steps run nothing but echo finds the class in seconds. Two repair rules recorded. Do not make a hollow gate blocking on the same commit that makes it real: seal-coverage was wired to a checker returning 0 of 496, so it went in non-blocking with the enforcing flip named as the next step -- a gate that blocks on a number nobody has agreed to is a new outage. And never hollow a gate out to make it pass; delete it instead, since a missing gate is visible in the workflow list and an empty one reports green. Separately: two derivations of one path is a bug even when every test passes. Seal files are <parent-dir>_<module-name>.json from the spec's module declaration; the gate guessed basename. It flagged a correctly sealed spec as missing, and "passed" another only because an unrelated GF16.json collided case-insensitively on macOS -- on Linux it would not have. Case-insensitive filesystems conceal naming disagreements until CI or a differently-configured contributor hits them. The fix is to delete the guess, not correct it: when a shell script and a compiled tool must agree on a derived path, the script calls the tool. Refs gHashTag/t27#1956 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A campaign of audits produced a findings document, and write-up time is where observations get rounded up into theorems. Two could not survive it. A seal-path function was committed as "injective by construction". It is not: the encoding flattens / to _, and _ is legal inside a path component, so specs/a_b/c.t27 and specs/a/b_c.t27 collide. What was true and sufficient is that it is injective on this corpus -- 496 specs, 496 distinct images, measured. The general claim was never needed; it was reached for because it sounded finished. Propositions now carry an evidence class: PROVED (machine-checked), MEASURED (reproducible over a stated domain), CONJECTURE. That forces the domain into the sentence, and the domain is where these claims break. Three habits recorded. Write the counterexample into a test that asserts the limitation holds, not a TODO comment -- a limitation pinned by a passing test is maintained, one pinned by prose is not. A partial invariant plus a guard at the mutation site beats a total invariant nobody re-checks: the predecessor scheme had a stronger-sounding rule, no guard, and silently destroyed a seal that stayed broken for months. And validate a checking pipeline in both directions before trusting it -- a yosys recipe was confirmed on a true property (exit 0) and a false one (exit 1), because a pipeline that only reports success is indistinguishable from one that checks nothing. Separately: six arXiv ids were assembled from memory for a related-work table. Fetching each citation_title showed one, recalled confidently as a numerics paper, was actually about pandemic concern extraction on Twitter. Identifiers feel retrievable and are not. One request per entry, and not optional in a document whose whole value is that its claims are checkable. Refs gHashTag/t27#1963 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… check The plan was to preprocess SystemVerilog with sv2v so Yosys could read the project's assertions. sv2v's README: "Assertions are also supported, but are simply dropped during conversion." Supported means parsed without error, not preserved. Measured on 0.0.13 -- property block and assert property in, zero assertions out, exit 0, no warning. Wired up, sv2v -> yosys -> sby would have run green while proving nothing. Worse than the broken state it replaced, which at least failed at parse. A pipeline can be built entirely from real, well-regarded tools and still be theater. Two rules. Read a tool's stated limitations before adopting it and unpack the word "supported" -- one README line saved a green meaningless CI job, and the install came after the README, empirical confirmation after that. And when a transform can silently reduce your inputs, measure the output population, not the exit code: the CI job now counts $check cells and fails at zero, validated both ways (real emitter 2, sv2v 0). Exit 0 over an empty set is the most expensive kind of pass, because nothing downstream can tell it from success. Separately: when a tool refuses your input, consider changing the input. Two waves went into Yosys not accepting named property blocks. It does accept immediate assertions, and nearly the whole property set maps onto them -- a |-> b is assert(!(a) || (b)), a |-> ##N b is assert(!($past(a,N)) || (b)). Meeting the tool where it is removed a dependency instead of adding one. Riders: name what does not survive translation in the artefact itself (s_eventually is liveness and cannot be an immediate assertion; it is reported in-file), because a partial translation that hides its coverage is the vacuity failure one level up. And let the prover correct you -- the first delayed-implication guard was rst_n alone, and the counterexample (one cycle after reset the antecedent's history predates the reset) was a design error found for free. Refs gHashTag/t27#1965 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…wn answer Formal verification found a lost-interrupt race in generated RTL. Two unit tests covered exactly that code and both passed -- they asserted the literal emitted text, so they passed for precisely as long as the bug existed and failed the moment it was fixed. They were not testing the design, they were holding it still. A string-match against emitted code asserts "the generator still produces what it produced yesterday", which is a snapshot, not a property. If a test would fail when the code is corrected, it is pinning the bug rather than guarding against it. Second lesson: prove the mechanism, not just the counterexample. A refutation says a bad state exists, which is easy to file as "can occasionally misbehave". Stating the failure as a property and proving it -- $past(inference_done) && $past(status_read) |-> irq_status[0] == 0, PROVED -- shows the event is always lost, not sometimes, and that is what justified changing RTL instead of adding a caveat. Supporting habits: make the experiment discriminating (two properties differing by one guard, one proving and one refuting, isolate the cause), and validate a regression harness against the broken version, since a harness only ever run against a fixed design might pass because its properties are vacuous. Third: when a property that cannot fail fails, the harness is wrong. Three properties came back refuted including a tautology; the cause was yosys sat refusing to run with more than one module selected, whose error reads exactly like a refutation. Keep one property per harness whose answer you already know -- it converts a class of silent harness faults into an obvious contradiction, the same instrument as "a clean 0%/100% is a harness fault" applied to a prover. Refs gHashTag/t27#1967 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Five properties checked against an AXI-Lite slave, three refuted, two real. The third -- bresp == 2'b00 -- was an artifact: bresp is only ever assigned 2'b00, so it cannot be violated in any reachable state. sat -tempinduct may begin its base case from an unreachable state. From a reachable start it proves; both genuine defects refuted under both settings. Rule recorded: cross-check every refutation against a reachable start before believing it. A real bug survives a change of proof method, an induction artifact does not. More generally, a model checker answers a question about a model, and the model includes assumptions about which states can occur -- when a result is surprising the first suspect is the state space, not the design. This is the reachability twin of the existing rules: a tautology that fails means a broken harness, a refutation from an impossible state means a mis-scoped one. And a false bug report is more expensive than a missed one, because it gets acted on -- someone would have "fixed" a correct reset value. Second lesson: count what must balance, not what should look right. The AXI handshakes were shaped correctly and VALID-stability proved on the buggy design; every shape-based check passed. The defect was arithmetic -- ready never dropped while one response register existed per channel, so two accepted transactions shared one response beat. Counting exposed it: outstanding <= outstanding + accepted - completed; assert (outstanding <= 1). When a design promises a conservation law, assert the balance directly. Shape properties check each event looks right; a balance checks none went missing, and the second is what hangs a bus. A counter also makes the violating state concrete, so the refutation resists dismissal as an artifact. Both RTL defects this campaign were missing events -- a lost interrupt and a lost response -- in modules whose per-event logic was individually correct. Refs gHashTag/t27#1968 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A master-side property was refuted -- "beats consumed must not exceed beats requested" -- and was not filed as a defect, because rvalid was a free input and the prover could have the slave deliver beats nobody asked for. A misbehaving environment is indistinguishable from a defect in the unit under test, and only assumptions tell them apart. Adding a minimal slave model made a different property meaningful and it caught a real bug; the over-read property stayed refuted after the fixes and was recorded as inconclusive rather than claimed. Three rules. An unconstrained input is an adversary, not a wire: any property about a unit's response to its environment is a property about that environment's contract too, so state the contract or state that you did not. Report inconclusive as inconclusive -- the pressure at write-up is to sort every result into bug or non-bug, and a third category names the next piece of work precisely. And the assume list belongs in the artefact, since a harness with hidden assumptions overstates coverage exactly the way a hollow gate does. Separately: the test's name can be the bug report. One test holding a defect in place was called dma_burst_length_is_max, asserting a fixed 256-beat burst on every transfer while the RTL abandoned the burst early. Its name asserted the defect as the contract, so an auditor reading the test list would take it for a design decision. Another asserted `if (m_axi_rlast || bytes_remaining <= 32'd8)` -- that || was the bug. Eight such tests were rewritten this campaign and all four RTL defects had one. Not a coincidence: a defect that survives review usually does so because something in the repo asserts it is correct. Read test names as claims about intent -- *_is_max, *_always_*, *_never_* are assertions about the specification, worth checking against it. Refs gHashTag/t27#1970 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…anomalies A formal environment model is code and has bugs. Wrong permissively it lets defects through; wrong restrictively it manufactures them, which is worse because it looks like a finding. An AXI4 slave model asserted rather than assumed its single-burst precondition, and that precondition refuted. Read naively: the master overlaps bursts. Checked instead with properties using only the unit's own ports -- !(arvalid && rready), no back-to-back AR handshakes -- both proved, locating the fault in the model, which cleared burst_active from its own counter rather than from the master-visible rlast. Port-only properties are the arbiter because they involve no model at all. When a modelled property and a port-only property disagree, the model is the newer, less-tested artefact. Two habits: assert a model's preconditions and never assume them, since an assumption that the unit behaves is exactly the assumption that hides misbehaviour; and key model state off signals the unit drives rather than a parallel count, because two counters that should agree are two things that can disagree. Second lesson: record the anomaly instead of picking a story. The same wave ended with arlen == 0 refuting at the address handshake while the hand-trace said it must hold. Two tidy stories were available -- a fifth defect, or a harness artifact -- both writable confidently, one of them wrong. It was recorded as an anomaly: named, reproduced, explicitly unclassified, with the dependent property marked open on the ground that a harness with one unexplained result cannot settle a second. The asymmetry that decides it: a false finding costs more than a missing one because it gets acted on -- someone edits correct RTL, or writes off a real bug as noise. There is a pull at write-up time, especially after a run with several real fixes, to make every thread end in a verdict. "Reproduced, unexplained, here is the exact command" is a complete deliverable. Refs gHashTag/t27#1972 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…e guards Yosys's sat ignores $assume cells unless -set-assumes is passed -- opt-in, no warning. A harness missing it still runs and still prints PROVED or REFUTED with every constraint doing nothing, so a property meant to hold given a compliant environment is quietly checked against an arbitrary one. That cost a wave: an anomaly recorded as unexplained and a dependent property left open, when the harness had never applied its own constraints. The catch is two lines -- assume(1'b0) plus assert(a == !a), which proves vacuously when assumptions are live and refutes when they are inert. It is now the first step of CI. Generalised: whenever a tool takes constraints, construct an input whose answer differs between constrained and unconstrained, and check which world you are in. Same shape for a linter config, a mock's expectations, a fixture's setup. Third instance of one instrument this campaign -- a tautology that fails means a broken harness, a gate that cannot fail is not a gate, constraints that constrain nothing are the same defect. Second: put assertions inside the module when you need a readable counterexample. A wrapper forces -flatten, which mangles every name and leaves VCDs full of $auto$async2sync internals. Appending the assertions to a copy of the module gives one module, no flatten, and a legible cycle-by-cycle table via -show. Hours went into reasoning about what the trace might contain; obtaining it took ten minutes. If a tool's diagnostic output is unusable, that is the bug to fix first -- everything downstream is speculation. Third: proving code unreachable is a reason to delete it, not to add it. A clamp for a counter wrap was written and reverted, because the same session had proved that state unreachable under contract, and the out-of-contract case underflows to a large value where the result is arithmetically correct. A defensive check whose trigger you just proved impossible implies a hazard that does not exist. And sometimes robustness against a lawless peer conflicts with correctness against the spec -- the spec wins, but say so, so the absent hardening reads as a decision rather than an oversight. Refs gHashTag/t27#1974 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…elete A passing property is compatible with two situations: the design is correct, or the property was never really evaluated. The second has two causes and neither reports anything unusual. Guard vacuity: G |-> P is free when G is unreachable. Exact oracle, no cover support needed -- replace the assertion body with assert(1'b0), keep the guard, and the run proves iff G is unreachable. Neutralise the file's other assertions first so each result speaks about one guard. Interesting-case vacuity: guard reachability is necessary but not sufficient, since assert(!A || B) is trivially satisfied whenever A is false. Probe the case the property exists to cover by asserting its negation; a refutation is the witness that the case occurs. The one that justified the exercise: a regression witness for a burst-abandonment bug needed a multi-beat burst to mean anything, and on single-beat bursts alone would have proved, stayed green, and silently stopped guarding its defect. Make witnesses permanent as runs that must fail. A CI step expecting refutation looks strange and is exactly right. Distinguish refutation from error by grepping the prover's failure text, since a syntax error also exits non-zero. Recurring shape, now found in five places: a check that cannot fail is indistinguishable from no check -- a shell gate that always errored and got bypassed, a CI job that was one echo, a validator matching the wrong shape, constraints the prover ignored, and properties whose antecedents might never occur. Same instrument each time: include a case whose answer you know. Separately, two mechanical traps that both presented as "the tool is broken". Deleting assertions to isolate one left dangling if-statements and nineteen tool errors; substituting assert(1'b1) keeps syntax intact and semantics inert. And an insertion offset computed before a regex substitution was applied after it, landing the probe past endmodule -- recompute positions after any length-changing edit. Refs gHashTag/t27#1976 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Two modules failed to terminate when a count parameter was zero: a terminator written `index == count - 1` compares against all-ones and never matches. Non-termination is liveness, and immediate assertions -- the only form the open-source prover accepts -- cannot express one. The instinct is to escalate tooling; unnecessary, because a loop that never ends almost always has a counter or index leaving its legitimate range, and that is pure safety. `valid |-> neuron_id < num_neurons` and `writes <= num_words` both refuted before the fix and proved after. Look for the safety shadow before escalating. "It runs forever" is hard; "this index exceeds its bound" is a one-line assertion a bounded model checker settles in seconds. Same substitution for deadlock (queue depth exceeds capacity), livelock (retry counter exceeds limit), leaks (allocation balance goes negative). An unbounded property often has a bounded consequence, and the consequence is the one worth asserting. Second: when siblings disagree, the odd one out is a bug rather than a contract. A zero-count defect could always be intentional -- maybe callers must pass non-zero. Nothing in the module says. But layer_sequencer already guarded `num_chunks == 0` and did not do the same for neurons, and the adjacent multilayer_sequencer guards `num_layers > 0`. A module that guards one of its own two counts and not the other is not expressing a contract, it is inconsistent with itself. Before deciding an omission is deliberate, look at how the same question is answered next door. A convention followed in three places and broken in one is an oversight; a rule broken everywhere may be the real convention. This settles bug-or-design without finding the author, and makes the report hard to wave away since the counter-example is the author's own code. The sweep is cheap: grep a family for how each member handles the degenerate input and line the answers up -- divergence in the column is the finding. Refs gHashTag/t27#1977 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…grated A design question rode nine waves as the deferred recommendation: "BitNet v2 moves the binding constraint from weight width to activation width -- is a ternary-weight datapath still right?" Fetching the abstract took one request. BitNet v2 keeps 1-bit weights; its contribution is a Hadamard transform making 4-bit activations viable. The premise was validated by the paper, not threatened by it, and the question as phrased had no answer because it presupposed something false. A question repeated across sessions accumulates authority it never earned -- each carry forward makes it look like settled context rather than a claim. Before doing the work a long-standing question implies, spend one request checking the sentence it rests on. Especially when the question came from your own earlier summary: restating your own inference back to yourself is how an inference becomes a premise. The corollary made the wave worth it. Answering properly meant reading what the system actually does, and that is where the finding was: the paper said weights were fine, the RTL said activations were ternary too -- more aggressive than any published variant on the axis the field finds hardest. Nobody had asked that, because everybody was asking the other question. Second lesson: "N of N emitted" is not "N of N integrated". A README row read "RTL pipeline · GREEN · 9/9 modules". Nine are emitted, so it is true. The top level instantiates three; the MAC, weight memory, DMA, bus slave and interrupt block are never instantiated, the memory port is tied to zero, one input is declared and never used. A count of artefacts presented where a reader infers a count of working parts -- a proxy metric arriving in a status table instead of a CI job. Two mechanical checks: for any "N components" claim, grep the top level for instantiations and compare; and ask what the verification ranges over, since module-scoped properties cannot imply system behaviour. When a project reports progress as a count, find out what the denominator counts -- modules that exist, compile, are reachable from the top, or are exercised are four different denominators, and the gap between first and last is where the real state hides. Refs gHashTag/t27#1979 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… the property Wiring a MAC to a memory with one cycle of read latency needs the control delayed by one cycle. The property written for it -- mac_valid_q == $past(layer_valid) -- is true and provable and useless: it constrains the register, not the consumer. Rewiring the MAC's valid_in straight to layer_valid, reintroducing exactly the hazard, left it PROVING, because the register still existed and nothing tied it to the MAC. The repair phrases the property over the consumer's own output, which can only be what it is if the consumer saw the intended input. Correct build proves, unskewed build refutes. When asserting that A drives B, phrase it over something only B can produce -- a property naming only signals upstream of the connection cannot see the connection. This is the integration-level form of vacuity: not an unreachable guard, but a true statement about the wrong side of a wire. Two carry-overs. Composition bugs are invisible to module-scoped verification by construction: sequencer correct, memory correct, MAC correct, assembly wrong. And the rule that caught it was already written down -- validate a regression harness against the broken version. Two minutes, and the only reason eight green properties were not shipped with one certifying nothing. A harness only run against a correct design has not been tested, it has been demonstrated. Separately: reduce the model, not the property, when the prover cannot handle a construct. sat cannot model $mem_v2, so a 4096-entry BRAM errors. Shrinking it is correct because the properties never read memory contents, so chparam -set DEPTH 4 plus memory_map changes nothing they observe and the claim proved is the same claim. Weakening the property would silently narrow what was verified; reducing the model narrows only what is simulated, and is auditable. State which you did -- "proved with reduced memory depth, because no property reads memory" is a complete disclosure, "proved" is not. Refs gHashTag/t27#1980 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…onditions A design question sat open for ten waves -- ternary activations or 4-bit -- and could not be answered because the choice had no address. It lived in the absence of a module: nothing said "activations are ternary", the datapath simply had no layer boundary and the assumption leaked in through whatever the neighbouring ports happened to be. Building the missing module changed the question's status without answering it; the width is now one output port, and a 4-bit variant is a diff. An unmade decision with no interface is untrackable. Before agonising over an open architectural question, check whether the artefact that would embody it exists -- if not, building it is usually worth more than deciding. And an assumption implied by an absence is the hardest kind to audit: grep finds a wrong constant, nothing finds a missing stage. Second: prefer a total function to a documented precondition. A negative threshold makes two comparisons overlap; as parallel comparisons that is a don't-care, and in a design whose output alphabet has a reserved invalid code a don't-care is silent corruption with no error path downstream. A priority chain costs one ternary operator and is legal for every input. A precondition is a promise made by code you do not control. Any enum with an unused encoding deserves a proof it is unreachable, not a comment. Third: a substring ban catches the documentation that justifies it. Three times now -- 8'hFF, 2'b11, FORMAT-SPEC -- a test forbidding a literal failed on the comment explaining the ban, and once on the assertion enforcing it. Narrow to the syntactic context: strip comments, skip assertion lines, match an assignment rather than an occurrence. The tell is a test failing on the very commit that adds the safeguard. Fourth: a test whose name contains a number gets renamed every time the system grows. bundle_order_has_twelve_entries and two entries[9]/entries[10] lookups broke on adding one file. The invariants they should have carried -- len() == declared count, last entry is the manifest, lookup by filename -- survive growth untouched. If a test's name must change when the system grows correctly, it is asserting the wrong thing. Refs gHashTag/t27#1981 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…s its own class A double-buffer controller computed a ping-pong decision, the top declared a wire and connected it, and nothing read it -- the activation memory had wr_en tied to 1'b0, so there was no path from a layer's output to the next layer's input. The whole thing was visible in one number: grep -c gave 2, meaning a declaration and a connection with no consumer. Three or more means something reads it. Count uses of each signal crossing a seam and look at every one with a count of two. Same for a module whose outputs go nowhere and an output assigned from a constant. A tie-off is a deferred decision, invisible in any view that does not span the boundary it sits on. Second: check the rate, not just the name, when reusing an address. The double-buffer controller already produced write_addr, so wiring it looked obvious -- and was wrong by 27x, because write_addr counts neurons and the requantizer emits one packed word per 27 neurons. When connecting two stages, compare their rates before their names: packing, batching and serialisation all introduce a divisor a plausible name hides. Third: integration defects are a distinct class and cannot be front-loaded. Three consecutive waves found a latency skew, an absent stage and a dead control signal -- every module had properties, every property proved, and the composition was wrong in three different ways. Module-level verification bounds its own claim, and saying so is part of reporting honestly: "28 properties proved" implies far more than it delivers if the modules are not wired together. The seam has to exist before you can assert across it, so expect the first assertions across a new seam to find something. Refs gHashTag/t27#1983 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ed decisions Wiring a prefetch controller to a shared memory produced a property that refuted -- the prefetcher could write an address the compute stage was reading -- and it still refuted with the environment constrained, so it was not an artefact. Three options existed: ship the failing assertion, weaken it until it passes, or record the gap. Option three, every time. Shipping a failing assertion turns a finding into an outage. Weakening it is deliberate vacuity, the exact failure catalogued elsewhere in this file, committed knowingly -- and it is worse than a missing assertion because it actively certifies the thing it stopped checking. The pressure at the end of a session is to leave everything green, and a weakened assertion looks exactly like a solved problem. When recording, state three things: the property as written, that it was reproduced under a constrained environment, and that it is not asserted. That turns "we did not finish" into a precise starting point. Second: count the tie-offs, they are decisions someone deferred. Every structural gap in three waves of integration announced itself as a constant -- prefetch_done = 1'b1, mem_addr = 32'd0, mem_rd_en = 1'b0, and wr_en(1'b0) on both memories, meaning the weight memory in an ML accelerator had never been loaded. Only the first carried a comment saying why. A tie-off is a deferred decision wearing the costume of a design choice. They are trivially greppable and each one bounds what any test above it can be checking -- an engine whose memories are tied to zero still passes every property about its sequencers. So grep for constant port connections before believing an integration is complete, and when writing one, put the removal condition in the comment: "tied off until X is wired" is a to-do with an owner, while a bare 1'b0 is indistinguishable from intent. Refs gHashTag/t27#1984 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…less output A property refuted, the trace identified a stale completion flag, the flag was fixed, and the property still refuted. The pull at that moment is to conclude the diagnosis was wrong and revert. It was correct and incomplete: a second independent defect sat in a different module, a level-triggered handshake sampled one cycle too early, and each defect would have been masked by the other's correctness. Re-read the trace instead of reverting. If a fix changes the counterexample, it addressed something real; a fix that leaves the counterexample identical is the one that missed. Composition defects cluster -- two modules each individually correct can disagree at their seam, and when two seams are broken at once, fixing either alone changes nothing at the top. Treat "still failing" as a request for the next trace, not a verdict on the last one. Second: the recorded gap is what made the fix possible. A previous session left the property reproduced, documented and not asserted, rather than weakening it. A softened assertion would have shipped two real defects under a green check and nobody would have taken the trace. An honestly recorded failure is a work item; a weakened assertion is a lie with a maintenance cost. Leaving something visibly unfinished costs discomfort and preserves the information; papering over it costs nothing now and destroys the information permanently. Third: ask the tool for the signals you named, not for a dump. Two waves were lost to -dump_vcd after -flatten producing files full of mangled auto-generated names. Top-level names survive flattening, so naming them with -show gives a clean table, and two independent defects were visible in one reading of it. When a diagnostic dump is unusable, ask for less rather than more -- a named projection of the signals you suspect is legible by construction, and it is usually one flag away. Refs gHashTag/t27#1985 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…obsoleted An AXI-Lite slave was instantiated to replace top-level config ports with CSRs. Instantiation is easy to verify by eye and easy to get wrong in a way nothing notices -- a previous wave left a double-buffer controller connected to a wire no consumer read, dead for four waves. So the properties name the connection, not the module: start == reg_ctrl[0], and reg_status reflecting busy and done. Both would be vacuously true if the slave were instantiated and ignored, since start would simply be something else. When integrating a component, assert an equality that spans the boundary -- "the module is instantiated" is greppable and means little, while "this internal signal equals that register bit" cannot hold unless the wire exists. Cheap version: the grep-count rule. Strong version: a property that fails if the connection is removed. Second: tests named for an interface break when the interface improves, and the fix is often to invert them. Replacing the config bundle broke three tests, none wrong about the old design, all asserting an incident of it. The rewrite renamed them and inverted them -- they now assert the absence of the old ports as well as the presence of the new ones. When a change makes a test obsolete, ask whether the negation is now the interesting claim: often what you just removed is exactly what must not come back, and inverting converts a broken test into a regression guard for free. Related smell seen repeatedly: a test asserting a string containing formatting breaks when a declaration is realigned. Match the semantic part or normalise whitespace -- a test that fails on changes invisible to git diff -w is measuring the wrong thing. Refs gHashTag/t27#1987 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A double-buffer invariant said never write the buffer being read. Correct, proved, and it had guarded a real defect. Then a second writer arrived -- an input DMA whose whole purpose is to fill the buffer about to be read, because that is where the first layer's input belongs -- and the invariant flagged the correct new code as a violation. The reflex when a proved property starts failing on a change you believe is right is to weaken or delete it. Neither was right: the property was always about the requantizer writing into a buffer under active read, and that scope was implicit only while there was one writer to be confused about. Adding a producer to a shared resource is the moment to re-read every invariant about that resource -- not to relax them, but to make explicit the domain they were always about. Same for a second caller of a function, a second writer to a table, a second scheduler on a queue. Corollary: if scoping an invariant makes it vacuous, it was the wrong invariant. Here the scoped version still bites, which is the check that the scoping was honest rather than a way of switching it off. Second lesson: busy was a decode, not a state. An interlock needed "is the engine running?" and the available signal was busy = (current_layer != 0) || layer_start -- a decode of a counter, false during the entire first layer, so the interlock has a hole exactly where the first inference happens. This is the proxy failure the campaign kept finding in gates, arriving in RTL instead of CI. When something needs a state, give it a register. Deriving it from whatever is nearby costs nothing and produces a signal right in the common case and wrong at the edges -- the worst distribution for a safety interlock. And before keying safety logic off an existing signal, read its definition rather than its name: busy, ready, done and active all invite the assumption that someone maintained them as state. Refs gHashTag/t27#1989 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… partial closes A DMA and a compute engine shared a buffer and must never run together. The guard blocked the DMA while compute was active, and nothing blocked compute while the DMA was active -- a host starting the DMA then requesting inference walked straight through. Mutual exclusion is symmetric by definition, and a guard for it is naturally written from whichever side you were thinking about when the hazard occurred to you. Write the second direction at the same time, or the guard encodes the order in which you imagined the failure. Mechanical test: for "A may not start while B runs", ask whether "B may not start while A runs" exists. Second: when a change invalidates a property, ask whether it becomes two. An interlock broke a property asserting start == ctrl[0], correct before and deliberately false once the interlock fires. Deleting or relaxing it are the obvious moves; splitting is better. The general form allows the interlock, and the original is kept under if (!dma_busy) -- pinning down that the change did exactly what was intended and nothing more. Relaxing the original would silently permit any future condition to suppress a start too. A property invalidated by an intentional change usually splits into "the new behaviour" and "nothing else changed", and the second half is the one that catches the next unintended broadening. Third: two fixes, neither sufficient -- report that, not the last one. A state signal that was actually a decode, and a one-directional guard on a symmetric constraint, both genuinely fixed, and the property still refutes. The temptation is to describe the wave by its last action or keep going until something is green. What is true: the property is the sole remaining failure, confirmed by neutralising it alone and watching everything else pass; the residual cause is bounded to a timing relationship; both fixes are independently worth having. A partially-closed gap, precisely bounded, is a better deliverable than an unbounded-but-green one. Refs gHashTag/t27#1990 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
One property refused to close across three waves. Each attempt was real and each narrowed the window: a status signal that was a decode became a state register, a one-directional guard on a symmetric constraint became symmetric, and the guard was extended across three more pipeline valids. All correct, none sufficient -- and the pattern, each fix narrows and none closes, is itself the diagnostic. The fourth attempt was spent on a trace instead, and it showed why: the supervisor being gated runs its own state machine and does not stop when the host clears the request bit. The signal the gate keyed off tracked a request, not a state. Quiescence lived inside a submodule and was not observable from where the gate was written. When successive guards each narrow a window without closing it, stop adding conditions and ask what the guard cannot see. Accumulating terms at the observation point is the signature of a missing observable, and the fix is usually one output port on the module that actually knows rather than a fifth conjunct on the module that does not. The corollary that made stopping right: the diagnosis is a better deliverable than a fourth narrowing. Naming the change converts an open bug into a scoped task and leaves the accumulated conditions replaceable by one that answers the right question, rather than entrenched as four that nearly do. Same distinction as request-versus-acknowledge in a handshake, one level up -- a supervisor that can be asked to stop is not one that has stopped. Refs gHashTag/t27#1992 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… lost time A four-condition interlock was replaced by one better condition -- the module's own idle state, exported so the guard could ask the right question. The new guard was more principled, shorter, and still wrong: seq_idle subsumed three of the four old terms but not !reg_ctrl[0], which existed for a different hazard, a host setting two control bits in the same write. At that instant the sequencer genuinely is idle, so the new condition permits exactly the case the dropped term blocked. Before replacing a compound guard, write down what each term was for. A replacement covering three of four leaves a hole precisely where the fourth was, and it is harder to see than the original mess because the new guard looks derived from first principles. The tell: the failure survived a fix that was independently correct -- same signal as elsewhere, a refutation surviving a real fix means another cause, and here the cause was something the fix removed. Second: time spent understanding why a fix fails is not lost from fixing it. One property stayed open four waves -- recorded rather than weakened, then two narrowings that shrank the window without closing it, then a wave that produced a diagnosis instead of a fix, then a five-line change. Waves two and three look like failure and were not: they bounded the problem until it could be said why no top-level fix could work. The temptation throughout is to weaken the property so the run goes green. Each wave offered that exit, and each refusal is why the final fix was five lines in the right place rather than a fifth condition in the wrong one. When successive fixes each narrow without closing, spend the next attempt on a trace rather than a fix -- the pattern is diagnostic. And a diagnosis naming a concrete change is a complete deliverable, since the person acting on it may be you next session with no memory of the reasoning. Refs gHashTag/t27#1993 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Four consecutive sessions were spent adding interlocks, each narrowing what a system may do, each correct, and every safety property passed at the end. That is exactly when a green result means least: an over-tight guard makes every safety property hold by making the system do nothing, and no safety property can distinguish "the bad thing cannot happen" from "nothing happens". So the next session audited instead of extending. Six probes, each asserting an activity is impossible, where a refutation is the evidence it still occurs -- the DMA can still start, compute can still run -- paired with the inverse, that the two are never concurrent, which must prove. That pair is what carries the claim: a safety property and a liveness witness together say something neither says alone, since "this combination is impossible" is only interesting once "each of these is possible" is established. Two habits. Order matters -- audit before extending, because a new property built on a stalled system proves trivially and the error compounds into everything after it; one session of checking bought certainty for all the work that follows. And write the liveness witnesses as CI rather than as a one-off, since the hazard is not that today's guard is too tight but that tomorrow's will be, while every safety property keeps passing. Applies well beyond hardware: after tightening validation, rate limits, permissions or retry conditions, the tests that still pass are not evidence the system works -- they are evidence it does not do the forbidden thing, which an inert system also achieves. Add a check that the permitted thing still happens. Refs gHashTag/t27#1995 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Five lessons from the cross-layer wave in t27. A probe harness that reads a nonzero exit as "the probe refuted" cannot tell your property failing from something else failing. An obligation yosys generates itself began failing and every row of a liveness table silently flipped, reporting on a failure no probe caused -- three confident wrong attributions before the baseline run found it in one command. A reference placed above its declaration makes Verilog conjure an implicit net with the same name, so the code reads an undriven twin. In a generator the insertion point is a correctness property, not formatting. Completion is not evidence that work was done -- third instance of the zero-sized-job shape. An open finding needs a CI gate asserting it still refutes, or it rots. And a fix that does not fix the target while regressing the baseline should be withdrawn, however much work it cost. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Three lessons from the zero-sized-request sweep in t27. A generated file's comments are not evidence about the generated file. An emitter's comment said a zero-length request completes immediately; the code dropped it entirely. Reading the comment produced a published claim that was specifically wrong and propagated into a proposition, a README row, a commit and an issue before a sweep contradicted it. Grep for behaviour, not prose. When a defect shape appears twice, enumerate the class instead of fixing instances. One sweep found both remaining cases at once and surfaced a policy question no single-module investigation had: four modules disagreeing about the same degenerate input, where neither policy is wrong alone. The unobservable outcome is the dangerous one. A silently dropped request beats no ranking -- it is worse than a vacuous completion, because the caller waits forever for a result that was never coming. Prefer the outcome a caller can observe, and assert both halves: that it completes, and that it did no work. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Four lessons from auditing the t27 formal-foundations document. Two reproduce blocks were added that violated a rule recorded in the same file, by the same author, in the two waves right after that rule was written. Neither was ever executed. Writing a rule down does not apply it; only a check that fails when it is broken does. Documentation is evidence and should be audited like evidence. 14 of 19 shell-fenced blocks were transcripts wearing a command's clothes -- a reader cannot tell them apart. The fence is a type annotation. Then execute the runnable ones and check specifically for exit 127. Trace claims to gates mechanically, then check the misses by hand: of six claims whose identifiers matched nothing, four were false negatives of the extractor. A heuristic that produces a shortlist is working; treating its output as a verdict is how an audit becomes the thing it audits. And distinguish having a check from the check being sufficient -- recording that limit is what keeps an audit honest. 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>
…angerous half Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…us before publishing a ratio Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ber can be the symptom Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ss boundary Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ons coarser than the defect hide partial fixes Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…e warnings above the error Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…; ask Print Assumptions Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…structive checks need death-proof restores Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… cause the failure Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…n, do not read it Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…m or it recurs in one wave Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ge notes are a queue Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
gHashTag
force-pushed
the
trinet-fleet-truth
branch
from
August 19, 2026 20:21
94f042c to
fa6b480
Compare
A stale worktree 2399 commits behind master fabricated three findings in one session, including a red CI gate that was reverted 34 minutes after landing, and a rediscovery of a bug fixed two months earlier and presented as new. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…er reaches the code Three lessons measured this wave: - reachability, not depth: 406/485 functions have zero call sites, so deepening yosys flags 1 of 28 real defects and certifies 27 - a producer that annotates what it cannot lower and emits it anyway is a fail-open; the detector already exists, the edge to refusal does not - proximity in a file is not attribution: 489/618 belonged to a different cause and that repair had already landed Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…rately A both-lines mutant proved half of what it appeared to: the first assertion panics and aborts, leaving every later assertion unproven. Plant one mutant per guard and read which assertion fired. Two companions from the same pass: a pre-push gate that blocks you is a question (the file it wanted was tracked in git, merely missing from a sparse checkout) and a diff should carry only the defect it proved. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Restoring a hardcoded verdict flag failed to break any test, which reads as an uncaught fail-open. It was an equivalent mutant: every failure path bails before the verdict is computed, so the flag is unobservable. Composing it with a real 23-of-24 defect caught it. Companion: a vm_compute proof pins what it computes over, not every literal in its statement -- one side was uniquely determined, the other admitted three values, one of which passed coqchk. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ards nothing Mutation left the equivalent-mutant defence open. Copying the test body plus only the types it names into a file with no production logic settled it: before, 1 passed; after, 38 compile errors and no binary. Two companions: prove consumption with the built artefact (two binaries, stubbed gh, exit 1 vs exit 0), and never let an unreadable history share a representation with zero -- one 502 downgraded every finding. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ng one A deliberate fail-open hunt: 272 hits, 1 finding. Neither real result came from the patterns -- one from reading a file whole, one from a set difference (declarations vs assignments) that exposed a name never assigned. The fail-open family is disproportionately made of absences, and text search enumerates presences. Build two sets and diff them. Companion: the harness itself is in scope -- unquoted $PATHS under zsh returned zero for all seven patterns and nearly shipped as a clean sweep. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… pass Three tests printed SKIP and returned; libtest reported 173 passed, 0 ignored, and cargo swallowed the reason because passing tests' stdout is captured. Invisible twice over: in the count and in the log. Companions: a ratchet must baseline a set of name+reason pairs emitted by its own parser, and must say 'not evaluated' rather than zero when it cannot see; and an instrument never run against a non-defective 'before' has demonstrated nothing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…rtions executed Adds the copy_propagate finding (return result -> return undefined, valid Zig returning garbage), the bare expect() fix that unblocked 27 specs, and the packed-format defects in specs/base/types.t27 filed as #2677.
… without moving 39 Records the flat-harness defect (it resolved imports by basename, which is not how Zig resolves them) and the reverted relative-path attempt: Zig forbids a module from reaching above its root directory, so 92 absent siblings became 92 illegal paths while specs-that-run stayed at 39.
…ror, not the fix Records that yesterday's revert was wrong (Zig forbids leaving the module root, not '..'), the harness change that proved it, and the three distinct defects hiding behind one 'missing module' count.
Records the use-path split (149->150 valid, 1193->1159 errors, 41->15 absent imports) and the measurement that 35 of 55 import-blocked specs depend on a Rust-dialect module the emitter is not expected to parse.
…46 to 74 Records the math/constants conversion, the two constructs that failed silently (dropped 'as' casts, a Rust range loop that swallowed the rest of the function), and the numerical defect it exposed in pow(4.0, 0.5).
…alse-positive check Records the emitter deleting every 'x as T' (compiling code with different semantics, invisible to every instrument) and the correction from 645 to 639 after finding prose in the count-1 tail of the frequency table.
…ression VALID could not see Records that 6 of 12 cast sites are untested (so yesterday's zero difference proved less than it looked), the hyphen-as-path-separator rule verified against the tree, and the module-binding regression only the per-spec error delta caught.
…r read Records nearly rewriting the corpus for a compiler deficiency (the spec declares 'module tritype-base;' itself), the 281/237 declared-name count, and the third instrument added because both existing ones were structurally blind to it.
… that compared strings Records the 'using' keyword removal (39->35 unresolved imports, 110->106 gate events) and that the per-spec error delta I relied on for two iterations was comparing '2' > '14' lexicographically.
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