KaRaMeL
| Linux | Windows |
|---|---|
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!
- DESIGN.md has a technical overview of the different transformation passes performed by KaRaMeL, 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 KaRaMeL as well as a paper formalization of our compilation toolchain
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.
- [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 KaRaMeL.
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
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; see LICENSE for more details.