The other four concepts make claims. This one is about which of them you are allowed to believe, and it is last for a reason: a cross-check is the part that says which of the others are real, and putting it first would mean asking you to trust it before you know what it costs to build one.
The reason it needs its own concept, rather than a paragraph at the end, is this collection’s history. The AArch64 data-path course found its own cross-check reporting 0 disagreements over a corpus where 85 instructions genuinely disagreed — and not one of the four bugs printed a wrong word. They all made the comparison VACUOUS. A wrong word is visible; a vacuous comparison is believed, and believing it is worse than being wrong.
So this concept does four things a cross-check which agrees perfectly does not do. It prints how many instructions it compared. It prints how many times each of its 47 normalisation rules fired, because a rule that matches nothing is the exact shape of that bug. It classifies every disagreement it finds by kind. And it runs four poisons, each of which must move the number it claims to test.
The artifact is rvdec.py. Part one of it imports os, re, struct and sys and nothing else, and that is a claim a reader can check by reading four lines rather than taking a promise. ELF64 section headers are read by hand with struct.unpack_from — e_shoff at 0x28, e_shentsize/e_shnum/e_shstrndx at 0x3a, 64 bytes per entry — and .text is found by NAME.
The reason is not purity. A decoder that shells out to a disassembler is a disassembler with a hardcoded path in it. The reader is a dependency of the claim, not a convenience: if the decoder asked llvm-objdump what a word meant, the cross-check would be comparing llvm-objdump with itself.
One more check the decoder makes, and it is not decoration. It refuses any file whose e_machine is not 243 (EM_RISCV). About a quarter of all x86-64 opcodes have bits[1:0] == 0b11, so the length rule would step four bytes at a time through an x86-64 object and produce a stream of entirely plausible wrong lengths. Nothing in the DECODE would look wrong; the WALK would be wrong, and the walk is what every other measurement is taken against.
26 instruction models for the 32-bit encodings and one handler for the whole 16-bit space. The subset is a subset of NAMES, and — unlike the AArch64 course and unlike x86-64 — an unmodelled word here still has a LENGTH, because the length is a two-bit RULE and not a table. A word no model claims is printed and counted, never dropped:
$ python3 rvdec.py --run | sed -n '/Of the 1082/,/^$/p'
Of the 1082 instructions in the corpus:
1047 named by a model in this file
0 UNDEFINED by the architecture (not by this file)
0 RESERVED compressed code points
4 HINTs -- DEFINED, and they do nothing
35 unmodelled: the vector data path, and a few rows
Those are five DIFFERENT numbers and the cross-check depends on the distinction. An undefined encoding, a reserved encoding, a hint and an unmodelled word all print something that is not a plain mnemonic, and a two-reader check that reported the last of them as a failure would be reporting its own declared scope as a bug.
Every instruction in every corpus object, decoded by this file and by llvm-objdump-21 --triple=riscv64, and the two canonicalised and compared:
$ python3 rvdec.py --run | sed -n '/THE CROSS-CHECK, over every/,/^$/p'
THE CROSS-CHECK, over every corpus object:
1082 instructions the second reader printed
1047 of them this file NAMES
35 of them this file does not model (counted, not dropped)
1047 AGREE after normalisation
0 DISAGREE
0 where the two readers disagree on the LENGTH alone
Zero disagreements, and that is exactly what a broken cross-check looks like. Which is why the four things after it exist. And the honest sentence is the one about where this came from: the first run of this file reported 354 agree and 701 disagree of 1,055, and the difference between that and this is not a decoder that got better in the abstract. It is:
r_mul and r_mulw sit above r_alu and r_shiftw in the dispatch and neither checked funct7, so they claimed every opcode-0x33 and 0x3b word before the model that owns them was asked. add, sub, sll, slt, sltu, xor, srl, or, and, addw, sllw, srlw all reported as mul, mulh, div, rem and friends. Nothing about the output looked wrong: three plausible operands, a real register, a real instruction name.i_alu_imm raised Undefined for funct3 = 1 and 5, which belong to i_shift_imm, the model directly below it. Undefined STOPS the dispatch, so slli, srli and srai — three of the commonest instructions in the corpus — all reported as undefined by the architecture, when nothing about them was undefined.c.mv was UNREACHABLE because the compressed CR cell was dispatched on rs1 == 0, which is not a bit of that cell; the bit is inst[12]. And the same mistake reported c.jalr as c.jr, which is a decoder that turns every indirect call into an indirect jump.inst[8] was mapped into imm[0]. A B-type displacement is always even; a decoder that produces an odd target is producing a target no RISC-V instruction can encode, and 26 of them looked like addresses.fcvt rows with the source and destination swapped.701 was not one number. It was seven different things counted together, and the single verdict — “this decoder disagrees with llvm-objdump about 67 per cent of the corpus” — is a statement about a comparison, not about a decoder. The zero above is zero because the seven hundred were fixed one at a time and each fix is a numbered retraction in the artifact. Retracting a number is not the same as retracting the work: the work is the seven hundred.
Nearly every disagreement above was a printing convention: the reader says li where this file says addi rd, x0, imm; the reader says mv for a zero immediate; the reader prints the BASE mnemonic for a compressed word; the reader prints 0x5 where this file prints 5. Reconciling them is a normaliser’s job, and this one has 47 rules.
And the design decision every rule rests on is stated as a rule of the course, because getting it wrong is the bug this collection has already shipped:
EVERY rule EXPANDS. None of them deletes an operand.
A normaliser that DELETES an operand makes two readers agree by
deleting the same operand, and the agreement is then evidence
about the normaliser rather than about either decoder.
So `c.add a0, a1` becomes `add x10, x10, x11` and `add a0, a0, a1`
becomes `add x10, x10, x11` -- both sides GAIN the implicit rd, and a
decoder that read the wrong register produces a different canonical
form and is caught.
Four of the 47 rules were dead on the first run of the new normaliser, and every one of them was dead for the same reason: the pattern was anchored with ^mnemonic and the text has a SPACE there. Forty-one rules, zero substitutions, and a cross-check that reported its number anyway. That is the AArch64 bug reproduced in a new file by a rewrite that had read the lesson and still got it wrong.
The fix for reporting it is structural and it is worth copying: the counter is pre-seeded with every rule name at zero, so a rule that never fires is a ROW WITH A ZERO rather than an absence. The first version of this file created the entries lazily, which is a third instance of the same class — the reporting structure could not represent the failure it existed to report.
$ python3 rvdec.py --run | sed -n '/rules, .* fired/p'
47 rules, 47 fired, 0 matched nothing.
A control that cannot move the number it measures is a comment that says the word POISONED. Each of these must move its number, and a poison that does not prints [POISON FAILED] rather than a verdict.
The control is the sharpest of the four, because the first version of it could not move its own number, and diagnosing why is the most useful thing on this page. It picked its victim by counting each model’s footprint with that model alone in the dispatch table. That measures what the model’s guards would claim if nothing above it got there first — and it is the wrong quantity, because a model is only responsible for the words the dispatch actually gives it:
$ python3 rvdec.py --run | sed -n '/The dispatch, as CONFIGURED/,/^$/p'
The dispatch, as CONFIGURED, attributes the corpus like this.
rvc 284 named words
i_alu_imm 188 named words
i_jalr 101 named words
b_branch 91 named words
r_alu 88 named words
i_load 81 named words
...
i_alu_imm names 472 words ALONE and 188 in the dispatch.
The gap is the compressed extension: 284 of the 1,082 instructions are two bytes and are decoded by the 16-bit handler, which is not in that table at all. So the model that names the most words alone is not the model that owns the most words, and a poison that picks its victim by the wrong number picks a model whose words are somebody else’s, removes it, watches nothing move, and reports [POISON FAILED] — which is the correct verdict about a control that cannot move and the wrong verdict about this decoder.
So the victims are now chosen from the data, by in-dispatch ownership, and there are three of them rather than one:
VICTIM i_alu_imm owns 188 corpus words in the dispatch
BEFORE the poison: 1047 agree, 0 disagree, of 1047 named
AFTER the poison: 859 agree, 159 disagree, of 1018 named
and again, with the model restored: 1047 agree, 0 disagree
VERDICT: POISON 1 FIRED on all 3 victims.
deltas: i_alu_imm=188, r_shiftw=6, i_fp_ldst=1
And the 159 is the interesting part: removing i_alu_imm does not make its words unmodelled, it makes them fall through to a different model that decodes them wrongly. The delta equals the victim’s own footprint exactly, which is what makes it evidence rather than a coincidence — a model that owns N words and a control that moves N numbers are not two pieces of evidence, they are one number counted twice, and their agreeing is what makes the number mean something.
Bit 12, which is the sign bit of every base immediate, the compressed extension’s sign bit, and the high bit of a U-type immediate. One flip moves words between formats and changes immediate signs, and a classifier that is not reading the bits cannot survive it. Total movement: 326 instructions changed format, across 3 format values, and the same flip takes the cross-check from 1,047 agreements to 1 — which is the expected result: the words are no longer what the assembler emitted.
“Four if the offset is a multiple of four, else two” — wrong for every 2-byte instruction that happens to sit at a 4-aligned offset, and there are many. 1,082 instructions become 939. The guess found FEWER, which is exactly what a desynchronised walk does: it steps four bytes over a two-byte instruction and loses the one in between. The length rule is load-bearing, the counts in concepts 1 and 2 are real, and a decoder that guesses lengths gets a plausible smaller number.
This one is the fourth because it poisons the CHECK rather than the decoder, and a decoder bug is found by reading the output while a check bug is found only by trying to break the check. The first version of it got the argument backwards, and the way it got it backwards is worth more than the poison:
STEP 1. One operand of every `addi` in the corpus is changed
to x0 -- a real decode difference, planted on purpose, in the
TEXT the cross-check compares and nowhere else:
the cross-check with the bug planted: 879 agree, 168 disagree
CAUGHT. The check compares operands.
STEP 2. The same bug, AND the AArch64 bug: a normaliser rule
that DELETES the last operand:
the cross-check with BOTH: 926 agree, 121 disagree
DELTA: 47 of the 168 planted disagreements DISAPPEARED when the
normaliser was given the rule that deletes an operand. That
is the AArch64 failure reproduced on purpose and MEASURED.
The first version broke the normaliser and asserted the agreement count would then go up. It did not move, and the poison printed [POISON FAILED]. The [POISON FAILED] was CORRECT and the ASSERTION was wrong: you cannot raise an agreement count that is already at 100 per cent, because there is nothing left to agree about. The poison was asking the number to move in a direction that was not available to it. The corrected version plants a real disagreement first, so there is something for the bug to hide — and then shows that 47 of 168 real disagreements vanish under the AArch64 rule.
One more trap in writing this poison, and it is the easiest to repeat: a normaliser is a function of one string, and the first version corrupted it from inside the normaliser — which runs on BOTH sides. So it corrupted the reader’s text as well as this file’s, the two corrupted identically, and the cross-check reported 1,047 agreements with a real disagreement planted in the middle of them. The fix is to corrupt where only one side’s text exists.
rvdec.py, delete the if bits(i.word, 31, 25) != 0x01: raise Bad() from r_mul and re-run. Expect the section 10 agreement count to fall by roughly 116 and the poison-1 delta for i_alu_imm to change. Then put it back and confirm the count returns — a decoder change you cannot undo is not an experiment.)^mv\s+(\w+),(\w+)$ rule and delete the \s+, so the pattern is ^mv(\w+),(\w+)$ again. Expect the agreement count to fall by 108, and expect the fire table to show mv alias at zero rather than absent — which is the whole reason the counter is pre-seeded. A reader who saw only a fire table that listed what fired would not know the rule was there.)python3 crosscheck.py rvdec.out — 128 checks, and every one of them re-asks a claim in the recorded output rather than re-measuring it. Note what it asserts as a shape rather than a value: the -march comparison is asserted as “rv64i GAINS three and LOSES four” rather than as counts, because a count there moves with the compiler and a shape does not. A check whose threshold is a bare number is a check that fails on a busier machine and teaches its reader to ignore it.)Backwards, this concept is the check on all four. Concept 2’s three-bit rd' trap — every register seven too small, nothing malformed — is findable by exactly one of these mechanisms, because it is a bug in the decoding and both readers would have to be wrong in the same way to hide it.
Across, the same shape appears in a64-verify and in exe-verify, and the vocabulary is deliberately identical across all three: a poison, a delta, a [POISON FAILED]. A reader who has learned what a poisoned control is can read the verification section of any course in this collection, and the vocabulary being shared is the point.
And the limitation belongs here rather than at the end, because it bounds everything above. The two readers share an assembler.clang assembled the corpus and llvm-objdump-21 disassembled it, so both ultimately depend on one LLVM tree. An independent second assembler does not exist on this host. What this concept establishes is that this decoder and one other piece of software agree on what the bytes mean — not that either agrees with silicon, and there is no silicon here to agree with.