Everything in the last five concepts carries one of three labels, and on most pages you would be forgiven for not noticing. This page prints all of them, in one table, with the count.
The reason to do that is not fastidiousness. It is that this course is about a machine that does not exist on the machine that wrote it, and a course with that property has exactly one advantage over a course with hardware — it is forced to be explicit about which claims are which kind — and a course that does not take the advantage has thrown away the only thing it had that the x86-64 section did not. So this page is the concept that makes the other five trustworthy, and it is last for the same reason a64-verify is last in the encoding course and a64-unwind is last in the ABI course.
$ python3 a64sys.py --section 10 | tail -60
The whole course, one line per claim, with the label it carries
and the section that establishes it. 57 claims.
1 syscall
MEASURED-ON-BYTES the syscall number is a 16-bit unsigned field at sec 3, 4
MEASURED the assembler accepts 0..65535 and refuses both sec 3
MEASURED Linux puts the same number in x8, and clang uses sec 4
MEASURED x0-x7 receive the arguments in argument order sec 4
MEASURED the ninth argument is not a register sec 4
QUOTED a Linux syscall takes at most six arguments sec 2, 4
QUOTED __NR_write is 64 and __NR_read is 63 sec 2
QUOTED the SVC traps to EL1 and the kernel returns in x0 sec 2
...
6 evidence
MEASURED the two readers agree on every word of this corpus sec 9
MEASURED the check detects a poisoned guard sec 9B
MEASURED the inherited HINT guard is one bit too narrow sec 3
21 MEASURED, 5 MEASURED-ON-BYTES, 31 QUOTED, 57 total
54% of the claims in this course are QUOTED
That ratio is the finding, not a disclaimer. The subject of this course is a machine, and the machine is the one thing this host does not have, so a majority of the claims about the machine are quotations. What the course can measure — and does, twenty-six times — is the encoding, the compiler and the object file, and those are exactly the three things a learner writing a backend has to get right and exactly the three that do not need a CPU.
The distribution is also not random, and the shape is worth noticing: concept 5 is almost entirely measured, concept 3 is half measured, and concepts 2 and 4 are mostly quoted. That is a direct consequence of what each one is about. A descriptor format is a document; a relocation is a file.
$ python3 a64sys.py --section 1 | sed -n '1,40p'
==========================================================================
a64sys -- the artifact for "The AArch64 Machine: Modes, Memory and Faults"
==========================================================================
THE METHOD IS FORCED AND IT IS STATED FIRST:
there is no AArch64 machine on this host, no AArch64 emulator and
no AArch64 linker, so NOT ONE INSTRUCTION IN THIS COURSE HAS
BEEN RUN, and there are NO TIMINGS anywhere in this file or on any
of its six pages. The x86-64 section measured a 4.92x and a
27.65x; nothing here has a counterpart and nothing here fakes one.
...
aarch64-linux-gnu-ld ABSENT (AArch64 linker)
qemu-aarch64 ABSENT (AArch64 emulator)
aarch64-linux-gnu-as ABSENT (a SECOND AArch64 assembler)
aarch64-linux-gnu-gcc ABSENT (an AArch64 GCC)
Four absences, and the fourth is the one that is easy to forget: there is no second AArch64 assembler. Every refusal quoted anywhere in this course is a refusal by clang 21.1.8's integrated assembler and by nothing else, and both readers of the two-reader check come from one LLVM tree. So the check establishes that this decoder and one other piece of software agree on what the bytes mean — not that either agrees with silicon.
Six files, four optimisation levels, 1,516 instructions, 0 disagreements. And that number is worthless on its own, which is the entire reason section 9B exists.
$ python3 a64sys.py --section 9 | sed -n '/TOTAL/,/^$/p'
TOTAL 1516 instructions read, 1516 NAMED by reader 1, 0 DISAGREEMENTS.
[COVERAGE] reader 1 names 1516 of 1516 words, so 0 are unmodelled
[RECONCILED] the alias rules that fired, each with its count, because
[] a normalisation that is not counted is a fudge:
ldr -> ldr 320
adrp -> adrp 298
ret -> ret 208
...
movz -> mov 46
mrs -> mrs 44
...
[DISAGREE] ZERO true disagreements.
Then one guard, one bit, and the same loop again:
==========================================================================
9B THE POISON: one guard, one bit, and the same loop again
==========================================================================
[CLEAN] 1516 instructions read, 1516 named, 0 DISAGREEMENTS
[POISONED] with the poison in: 1459 named, 57 DISAGREEMENTS
the named count moved from 1516 to 1459 -- 57 instructions
the disagreement count moved from 0 to 57 -- 57 instructions
the first few, printed BY NAME so a reader can check them:
0xd5385208 reader 1: (op 0xd5385208) reader 2: mrs x8, ESR_EL1
0xd5384028 reader 1: (op 0xd5384028) reader 2: mrs x8, ELR_EL1
0xd5386008 reader 1: (op 0xd5386008) reader 2: mrs x8, FAR_EL1
0xd538c008 reader 1: (op 0xd538c008) reader 2: mrs x8, VBAR_EL1
0xd518c008 reader 1: (op 0xd518c008) reader 2: msr VBAR_EL1, x8
1,516 to 1,459 named, 0 to 57 disagreements, and every one of the 57 is an mrs or an msr printed by name. A check that has never been seen to fail is a check with no reason to be believed, and this one has now been seen to fail, which is the only property that makes the zero mean anything.
And the choice of which guard to poison is not arbitrary: mrs/msr is the family this course added, so poisoning it measures this course's contribution rather than the inherited decoder's. Poisoning an inherited guard would produce a larger number and a less informative one, because a reader could not tell how much of the movement was the poison and how much was the twenty-one models that arrived with the file.
Before the poison there was a retraction, and it is the most valuable thing in the course. The encoding course's decoder has a model whose own claim is "NOP, WFI, YIELD and the rest: 27 fixed bits and a 5-bit hint number", and whose guard is bits[31:5]:
hint word word >> 5 guard matches?
nop 0xd503201f 0x6a81900 YES
yield 0xd503203f 0x6a81901 no
wfe 0xd503205f 0x6a81902 no
wfi 0xd503207f 0x6a81903 no
sev 0xd503209f 0x6a81904 no
sevl 0xd50320bf 0x6a81905 no
dgh 0xd50320df 0x6a81906 no
bti 0xd503241f 0x6a81920 no
bti c 0xd503245f 0x6a81922 no
bti j 0xd503249f 0x6a81924 no
bti jc 0xd50324df 0x6a81926 no
ONE of ELEVEN.
The body of that model is correct — it reads the hint number and has the right eleven names — and the guard makes eight of them unreachable. And the reason it survived a whole course is the sentence that generalises further than anything else in this file:
And here is the number that makes the whole thing concrete. The same loop over the same corpus, with three different sets of models:
[MEASURED] what each course's models contribute to THIS corpus
dispatch read named coverage
the encoding course's 21 alone 1516 1374 90.6%
+ the ABI course's 6 1516 1385 91.4%
+ this course's 6 1516 1516 100.0%
[RESULT] the encoding course names 1374 of 1516 of this corpus
(90.6%), and the two later courses add 11 and 131
A coverage number means nothing on its own — it is a number about a corpus. So the same loop is run three times with three different sets of models, and that is what turns "100% named" from a boast into a number. 1374 of 1516 words of a corpus whose whole subject is the SYSTEM class, and 142 of the 33 models written by the two courses that came after the first.
Sixteen retractions, printed in full by the artifact in section 11 with a source for each, and asserted as text by the harness so that a retraction can be neither quietly dropped nor edited into being right. Here they are in one table, with what replaced what:
R1 "the syndrome is a 32-bit field: EC, IL, ISS"
-> it is 32 bits INSIDE a 64-bit register, bits 55:32
are ISS2, and a 32-bit mask throws it away
R2 "the syscall number is the immediate in the SVC"
-> BOTH are in the emitted code: the field is the
architectural half and x8 is the Linux half
R3 the inherited decoder covers the encoding well enough
-> it names FIVE words of the SYSTEM class, and every
instruction in this course is outside those five
R4 "NOP, WFI, YIELD and the rest"
-> NOP alone: the guard is one bit too narrow, and
matches 1 of 11 hints the assembler accepts
R5 one relocation per address reference, as SYSCALL does
-> TWO, always, for every reference on AArch64
R6 "x8 is the syscall-number register, so a compiler must
treat it as reserved"
-> clang uses it as a scratch in all four functions
that do not mention it, at all four levels
R7 the natural test is to shift the syndrome right by 26
-> clang does not shift, and does not need to: THREE
instructions, because 0x24 and 0x25 differ in one bit
R8 the table needs 16 x 0x80 and `.align 11` is the way
-> the size is right and the DIRECTIVE is only
necessary; both ends assemble with no diagnostic
R9 "`.align 11` and it is valid"
-> necessary and NOT SUFFICIENT, and nothing checks it
R10 "52-bit" means the high half is 52 bits of address
-> it means a REGION of 2^52, mapped at the TOP, with
TTBR1 = 0xffff000000000000
R11 a page table is an ordinary array, so nothing
distinguishes it
-> its ALIGNMENT does, and the alignment is a property
of the SECTION: 4096 without, 0x200000 with
R12 a page needs a PAIR because the adrp reach is 4 GiB
-> the reach is 4 GiB and IRRELEVANT; ADRP MASKS OFF
the low twelve bits of the target
R13 the four levels and the block sizes read as a MENU
-> 2^27 entries are needed for a 2 MiB block at L1
and a table has 512, so a 48-bit regime cannot use it
R14 100% two-reader agreement is the strongest evidence
-> it is not, and section 9B is the demonstration
R15 the two-reader check establishes the decoder is correct
-> it establishes AGREEMENT; a corpus chosen to suit
the decoder is the failure mode this course found
R16 a 30-bit virtual address space is configurable
-> T0SZ is FIVE bits and 64-30 = 34 does not fit; the
floor is 2^33 bytes
Seven of those sixteen were asserted before this course was written — in docs/aarch64-section-plan.md or in the brief this course was built from — and the artifact prints the source next to each one, because a retraction with no prior source is a course disagreeing with itself. Three of the sixteen were found by this course's own measurements against a draft it had already written, and they say so rather than claiming a prior source.
A course that reports ZERO retractions on a subject this
size has either not looked or has not been reading the
documents it cites. 16 retractions.
Fifteen of them, and the first two decide what every other one may say:
adrp+add → adr+nop relaxation — is quoted.Printed in the artifact, not in a footnote, because a limit that is a footnote is a limit that gets forgotten. This list is the honest end of the course and it is not a formality:
svc #0 traps, or to where, or that x8 is read.VBAR is honoured, or that the sixteen entries are in the quoted order.ADRP+ADD pair, because there is no AArch64 linker on this host.llvm-objdump agrees with the silicon. It does not have to: it is a second reader, and both readers come from one LLVM tree..s file on this disk.That is the shape of a course with no hardware: a small set of claims you can check with a hex editor, and a large set you have to take on the word of a document — and an exact statement of which is which. A course with hardware would have the second set too, labelled MEASURED, and would be worth more for the parts that need it.
python3 courses/a64sys/assets/samples/crosscheck.py. (Expect 210/210 checks passed, with no assembler, no linker, no emulator and no network. The harness reads the committed a64sys.out rather than re-measuring, on purpose: a course whose claims can only be verified by first rebuilding its own artifact is a course whose claims are only verifiable on the machine that wrote them, which is the same mistake as quoting a remembered number wearing a different hat.)m_sysreg from the dispatch and re-run. (Expect 1,459 named and 57 disagreements, all mrs/msr. Then delete m_hint_family instead and re-run: expect 1,391 named and 125 disagreements, and expect the 125 to include the eight hints from the R4 table. Two runs, two guards, two different numbers, and the difference between them is the seven hundred words those two guards together cover — which is a coverage measurement you made by breaking something rather than by reading a table.)Backwards, all five, and specifically: concept 5 is the one with the most measured content and therefore the one that most needs this page, because a page that is mostly measurements is exactly the page a reader is most likely to over-trust. Concept 3 contributed the largest absence in the course and this page is where the habit of printing an absence lives. Concept 1 is where the two-labels rule was first needed, because a field in an instruction and a value in a register are different kinds of claim and both are in the same line of assembly.
Sideways, the collection's own method. The encoding course's cross-check is the first application of the poison and it retracted its own 100% twice; the ABI course's unwinding concept is the second; this is the third, and R4 — a bug in an inherited artifact that survived a whole course because the corpus did not contain the words it was wrong about — is the first time the method has found a defect in a sibling course's file. The x86-64 course's boundary concept is the same idea applied to a course that did have hardware, and it proves an absence rather than asserting one — which is the harder case and the better precedent.
Outward, and the general form is the one the whole section has been converging on for six courses. Every claim in a course should be classifiable as reproducible-by-a-command, readable-in-a-file, or attributable-to-a-paragraph — and a claim that is none of the three is a claim nobody should act on. That is not a rule about courses without hardware; it is a rule about all of them, and a course with hardware is simply better at the second category and no better at the first or the third. The AArch64 section's contribution is that it has been forced to be explicit, and the reader who takes the habit out of here will apply it to a machine they can run — where the temptation is to treat a duration as a mechanism, and where the discipline costs nothing and saves a week.
And where this course ends. Sixteen retractions, fifteen limits, and a decoder with six models of its own that found a bug in its predecessor's and printed the arithmetic that killed a row in its own first draft. That is the whole of what a course about a machine you cannot run can honestly claim, and the two courses after this one in the section — the NEON register file and the weak memory model — are the ones where a reader should ask whether the same method would find as much, because the subject changes from control to data and the encodings get denser rather than sparser.