KreMLin is a tool that extracts an F* program to readable C code. If the F* program verifies against a low-level memory model that talks about the stack and the heap; if it is first-order; if it obeys certain restrictions (e.g. non-recursive data types) then KreMLin will turn it into C.
The best way to learn about KreMLin is its work-in-progress tutorial. Pull requests and feedback are welcome!
- DESIGN.md has a technical overview of the different transformation passes performed by KreMLin, and is slightly out of date.
This work has been formalized on paper. We state that the compilation of such F* programs to C preserves semantics. We start from Low*, a subset of F*, and relate its semantics to CompCert's Clight.
- the ICFP 2017 Paper provides an overview of KreMLin as well as a paper formalization of our compilation toolchain
- HACL*, our High Assurance Crypto Library, provides numerous cryptographic primitives written in F*; these primitives enjoy memory safety, functional correctness, and some degree of side-channel resistance -- they extract to C via KreMLin.
Trying out KreMLin
KreMLin requires OCaml (> 4.04.0) and OPAM.
$ opam install ppx_deriving_yojson zarith pprint menhir ulex process fix wasm visitors
Then, make sure you have an up-to-date F*, and that you ran
make in the
ulib/ml directory of F*. The
fstar.exe executable should be on your PATH.
To build just run
make from this directory.
Note: on OSX, KreMLin is happier if you have
greadlink installed (
brew install coreutils).
If you have the right version of F* and
fstar.exe is in your
PATH then you
can run the KreMLin test suite by doing
File a bug if things don't work!
--help flag contains a substantial amount of information.
$ ./krml --help
Kremlin is released under the Apache 2.0 license; see
LICENSE for more details.