Executing F* code (original) (raw)

By default F* only verifies the input code, it does not compile or execute it. To execute F* code one needs to translate for instance to OCaml or F#, using F*'s code extraction facility---this is invoked using the command line argument --codegen OCaml or --codegen FSharp. Code written in a C-like shallowly embedded DSL can be extracted toCor WASMby the KreMLin tool, and code written in an ASM-like deeply embedded DSL can be extracted to ASM by the Vale tool, but none of that is not discussed on this page. Also since F# extraction is plagued by some bugs and lags quite a bit behind OCaml extraction (eg. #1096,#1087 andmore), the rest of this page is really only about OCaml extraction.

The OCaml extractor will produce <ModuleName>.ml files for each F* module in the code; whereas the F# version will emit <ModuleName>.fs. These files will be located in the directory specified with --odir; if no output directory is specified, the files are written out in the current directory.

The extracted code often relies on a support library, providing, for example, implementations of various primitive functions provided by F*'s standard library. The sources for this support library are inulib/ml (for OCaml) and ulib/fs (for F#). To build and install the support library for OCaml, run the following command in the F* directory:

To compile the extracted code further and obtain an executable, you will need to link it with the support library.

This also means that some modules (e.g. FStar.List) should not be extracted (because we provide an optimized implementation written in ML that uses, say, Batteries). For that purpose, a --no-codegen FStar.List flag should be passed when extracting.

To simplify things, a generic Makefile is provided in ulib/ml/Makefile.include; it provides a pre-set invocation of F* where all the --no-codegen flags have been added. Furthermore, to speed up build times, make -C ulib/ml now builds a .cmxa file in addition to the individual .cmx files. You may want to link against that to simplify your build scripts, rather than copying ml files. The examples/hello directory provides an example.

Several examples of how this process works can be found in the repository.Reminder: run make -C ulib/ml before proceeding to any of the OCaml extraction examples.

examples/hello provides hello.fst and a Makefile that compiles and executes a hello world program in OCaml. You can try that out via:

$ make -C examples/hello hello

(There is also an attempt to extract this to F# and run it, but it doesn't currently work.)

doc/tutorial/code/exercises provides a simplistic example of access control on files in Ex1a.fstThe make target Ex01a-ocaml illustrates how to extract this to OCaml and run it:

$ make -C doc/tutorial/code/exercises Ex01a-ocaml

examples/crypto provides RPC.fst and CntProtocol.fst and a Makefile with therpc-test and cnt-test targets providing a way to run a small, verified example of remote procedure calls in OCaml (while linking with OpenSSL). This example relies on ucontrib/Platform/ml which only works with OCaml 4.05.

$ opam switch 4.05.0  
$ eval $(opam env)  
$ make -C examples/crypto rpc-test  
$ make -C examples/crypto cnt-test

If the last commands fail because of errors in ucontrib/CoreCrypto/ml then read theINSTALL.md file there on how to install dependencies like OpenSSL on various platforms. Anyway, building this is not for the faint of heart.

src/ocaml-output provides a Makefile which we use to bootstrap the F* compiler in OCaml.

Advanced:

By default, Foo.Bar.fst gets extracted as a module Foo_Bar.ml; references to Foo.Bar become ML references to Foo_Bar. If you provide an F* interface for Foo.Bar via an .fsti only, then there will be no Foo_Bar.ml generated, you're expected to provide your own realization. So far, so good.

It may be the case that you have both Foo.Bar.fsti and Foo.Baz.fsti, which share the same namespace Foo. In order to simplify your life, --codegen-lib Foo will ensure that references to Foo.Bar are extracted as references to Foo.Bar (instead of Foo_Bar) and references to Foo.Baz are extracted to Foo.Baz (instead of Foo_Baz), so that you can use OCaml's module system to encapsulate your realized modules.