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
- [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.08.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
Regarding OCaml: Install OPAM via your package manager, then:
$ opam install ppx_deriving_yojson zarith pprint "menhir>=20161115" sedlex process fix "wasm>=1.1.1" 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
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
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!
--help flag contains a substantial amount of information.
$ ./krml --help
KaRaMeL is released under the Apache 2.0 license; see
LICENSE for more details.