Start · the four projects

How the stack fits

sysi is one of four projects that together take a program from a verified source to the bits a RISC-V core runs. Each step on the way is proven once, checked again for every program, or trusted. This page shows the steps, which tool covers each, and what is still taken on trust.

Four projects

They are checked out side by side, and each finds the others by a relative path (sysi reads ../sysp and ../sysr; its sysk tools default to ../sysk).

sysp

The language and its verifier. Every index, every arithmetic operation and every contract is proven with z3, or the program is rejected. It also has a C backend.

sysi uses sysp's checker as it is (sysi/sysp.rkt requires it from ../sysp). README

sysk

A kernel written in sysp: preemptive tasks in user mode behind PMP, channels, a deadlock check. Its assembly is its trusted base.

sysi's main customer: the gate builds and checks it. sysk docs

sysi

The compiler between them: an IR, a lowering from sysp, backends to RV64 assembly and C, and two checks of its own output.

These docs. sysi, in levels

sysr

A hardware description language, and an RV64IM core written in it whose execute stage, ALUs, multiplier, load/store unit and PMP are proven against cores/rv64im/isa.sysr.

sysi reads the same isa.sysr to know what an instruction does. sysr docs

From a source to the bits, and who vouches for each step

Follow the chain from top to bottom. The grey boxes are what exists between steps (a file, an executable); each card is a step that turns one into the next. Select a step to see what does it, what checks it, what that check assumes, and where to read more. The buttons above the chain pick out the steps of one kind.

proven, or checked for each program trusted: assumed, not checked a tool whose output is checked, so not trusted

What is still trusted

Between a verified sysp program and the bits sysr's core runs, these are taken on trust. Everything else on the chain above is either proven once for all programs or checked again for each build. Tools whose output is checked (sysi's own lowering and backend, clang as an assembler, ld.lld) are not on this list: if one of them is wrong, a check fails.

Trusted	Why it matters, and what keeps it honest	Read

A check can be vacuous. If the facts a check assumes contradict each other, every goal is "proven". sysi refine asks z3 whether the facts its proofs used are satisfiable (reference §8: "The facts proofs used are checked not to contradict each other"), and both checks are tested the other way round: tests/refine-test.rkt and tests/validate-test.rkt corrupt one instruction at a time and require every mutant to be rejected, or to run exactly as the original on sysr's instruction-set simulator.

Where each check runs

sysp's verifier runs inside sysi: sysi lower, asm, refine and validate all call sysp's checker on the sources first and stop if the program does not verify (lower-files in sysi/main.rkt; --no-verify skips it, for experiments only). sysi refine and sysi validate run on every build of sysk through the gate; the last gate here reported:

sysr's proofs run in sysr, once for the core (sysr check), not per program. sysk runs its own checks before its kernel is built: the deadlock check (tools/model.rkt), the check that tasks name only what kernel/interface.sysk lists (tools/interface.rkt), and afterwards its test suite in QEMU, which make sysk-check runs with every kernel built through sysi (Commands, build, tests).