KreMLin is a tool for extracting low-level F* programs to readable C code
Pull request Compare This branch is 10 commits ahead, 297 commits behind FStarLang:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
.ci
book
include
kremlib
lib
misc
parser
runtime
src
test
.clang-format
.gitattributes
.gitignore
.gitmodules
.merlin
.odocl
.travis.yml
Changes.md
DESIGN.md
LICENSE
Makefile
README.md
Tests.ml
_tags
myocamlbuild.ml

README.md

KreMLin

このリポジトリはKreMLinに関するドキュメントの日本語訳置き場です。 翻訳文書はhttp://fstar-ja.metasepi.org/doc/kremlin-book/で公開しています。

元のREADME

Build Status

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

We have written 20,000 lines of low-level F* code, implementing the TLS 1.3 record layer. As such, KreMLin 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 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 make test.

File a bug if things don't work!

Documentation

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

$ ./krml --help

License

Kremlin is released under the Apache 2.0 license; see LICENSE for more details.