Just using `check` as a prefix to various keywords would lead to too many ambiguities in the parser (notably in contracts, where you can have an empty requires list followed by `check ensures ...` or a `check requires ...`. With a lookahead of 1, it's difficult for the parser see which rule should apply. Hence, the lexer will perform itself the lookahead and emit a proper token (`CHECK_ENSURES` or `CHECK_REQUIRES` respectively).
This directory contains the kernel backend.
It is low-level files which are internally used by other parts of the kernel, in particular to build the AST from the annotated C input files into an AST.
It should not contain any useful APIs for the plug-in developers, except for very low-level interactions and corner cases.