Home

Awesome

KaRaMeL

Linux
Build and Deploy

KaRaMeL (formerly known as KReMLin) is a tool that extracts an F* program to readable C code: K&R meets ML!

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 KaRaMeL will turn it into C.

The best way to learn about KaRaMeL is its work-in-progress tutorial. Pull requests and feedback are welcome!

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.

We have written 120,000 lines of Low* code, implementing the TLS 1.3 record layer. As such, KaRaMeL is a key component of Project Everest.

Trying out KaRaMeL

KaRaMeL requires OCaml (>= 4.10.0), OPAM, and a recent version of GNU make.

Regarding GNU make: On OSX, this may require you to install a recent GNU make via homebrew, and invoke gmake instead of make.

Regarding OCaml: Install OPAM via your package manager, then:

$ opam install ppx_deriving_yojson zarith pprint "menhir>=20161115" sedlex process fix "wasm>=2.0.0" visitors ctypes-foreign ctypes uucp

Next, 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 and FSTAR_HOME should point to the directory where F* is installed.

To build just run make from this directory.

Note: on OSX, KaRaMeL 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 KaRaMeL test suite by doing make test.

Installing through OPAM

KaRaMeL is also available on OPAM, by running opam install karamel.

If you installed the latest version of F* through OPAM, using opam pin add fstar --dev-repo, you can also install the most up-to-date version of KaRaMeL by running opam pin add karamel --dev-repo.

File a bug if things don't work!

Documentation

The --help flag contains a substantial amount of information.

$ ./krml --help

License

KaRaMeL is released under the Apache 2.0 license and MIT license; see LICENSE-* for more details.