Every build checked
Two checks are only worth something if they run on the kernel that ships. The gate builds sysk's kernel through sysi, runs sysi refine and sysi validate on that same build, and keeps the kernel only if both pass.
What the gate does
make sysk-gate runs tools/sysk-gate.sh on the sysk checkout beside this one (../sysk, or SYSK=...). The script never touches that checkout: it copies sysk into build/sysk-gate/sysk and builds there, with a sysp whose build command is sysi asm --as-c. sysk's own Makefile then runs as usual, and the kernel it links is sysi's. Step through it; the lines of the script that do each step are marked.
The last gate
The last line each check printed, the last time the gate ran in this checkout before the docs were built (build/sysk-gate/refine.txt and validate.txt keep each check's whole report):
With specs/011 the gate passed on sysk again, as it did through specs/008: every one of sysk 061's 574 functions refined, and validate accepted the kernel, in six and a half minutes on a quiet machine (the build, refine with eight functions side by side, validate). On sysk 063, run while other work kept the machine at a load average of about 110, the two functions nearest z3's limits did not make them, because the limits were wall-clock. Since specs/012 they count z3's work: the gate above passes on sysk 063's 585 functions in six minutes, and refine gives the same answer at a load average near 200, in 48. Since specs/013 a function found to refine is kept by everything its check reads: a second gate with nothing changed takes all 585 from the store and passes in 48 seconds, refine 7 of them. Between, sysi lowered more of sysk than it could check: specs/009 added sysp's newer forms, specs/010 bounded refine's memory so the gate ran to the end, and specs/011 took the functions left, drivers, the file server and the shell's largest, none of which was a wrong lowering. refine says what changed.
When refine says no
sysi refine sorts every function into one of three outcomes: checked, failed (a goal z3 could not prove, or an error), or too slow (over --budget-s, which the gate sets to BUDGET, 300 seconds unless given: the work z3 does in that many seconds on a quiet machine, counted query by query, with a wall-clock backstop ten times as long; specs/012). Since specs/025 every sysp form is in scope (a cell-swap was the last one out). It exits 0 only when every function was checked. A function that was too slow has not failed, but it has not been shown to refine either, so the gate does not pass. Try it:
The scripts
Each says what it does in its first lines (quoted from the files as they are now):
The three single-check scripts and the gate share sysk_build from tools/sysk-build.sh, so they build the kernel exactly as the gate does, each in its own directory under build/, and as sysk's own check builds it: by sysk's rule for its sysi kernel, with the arguments sysk gives sysi (specs/047). tools/sysk-check.sh is the odd one out: it writes its own wrapper, and runs those of sysk's test files that build a kernel (the others never reach sysi; eight side by side, as sysk's own make test runs them) with every kernel they build going through sysi, as RV64 assembly by default or as sysi's C with BACKEND=c. It needs QEMU; the gate does not run it.
Both checks lower the program again. sysi refine and sysi validate each take the sources and the build's arguments, not the build's output files: each lowers the sources itself, and validate compiles the result again to get the allocator's map, then checks the ELF the build linked against it. If validate's module were not the one the build compiled, the ELF would not match and validate would fail. What joins the two checks is that both lower the same files with the same arguments: the module refine checks is the one validate checks the machine code against.