sysi, in levels
sysi is the compiler between sysp and the machine: an intermediate representation, a lowering into it, and backends out of it to RISC-V and C. It also checks itself: for each function of each build, sysi checks that its output means what the sysp program means, and that the machine code means what its sysi means. So what sysp proves about a program also holds for the bits the core runs.
make testFive levels
Read the stack from the top: a program is written at the top and runs at the bottom. Each arrow between levels is a translation, and each translation is checked by a tool on the right, either once for all programs or again for every program it translates. Select a level to see what lives there and who vouches for it.
What checks each step
One function, through every level
The docs' example is sum, the total of a buffer's bytes (the tour runs it). Here is everything that happens to it on its way down, with what each step printed when the docs were last built. Step through it, or play it.
The ideas behind sysi
Proving a compiler correct once is a large project. Checking that each of its outputs means what its input means (translation validation) is a much smaller one, and it covers the assembler and linker too.
The lowering marks each loop head and says which sysi values hold each sysp variable there. Searching for that correspondence is the hard part of translation validation. A wrong hint can only make a check fail.
The machine-code check reads what an instruction does from isa.sysr, the same file the sysr core is proven against. No second model of RISC-V has to be trusted, except for division and remainder, which isa.sysr leaves out and the validator takes from the RISC-V manual.
One kind of value (a 64-bit word), explicit memory, blocks with parameters instead of phi nodes. Each instruction is easy to give a meaning, and each meaning is short.
How to read these docs
If you want to see sysi work, start with the tour: it takes one small program from sysp to a validated executable, with real output. To see where sysi sits among sysp, sysk and sysr, and what is still trusted, read How the stack fits. The two checks have a page each, and the checker, tested shows how the model of sysp they rely on is tested against running code. Every page ends with In the source: the files it explains, as they are in the code today. Words you don't know are in the Glossary.