Executing programs

Producing an OCaml library

To extract OCaml code from a F* program use the command-line options, as shown below:

fstar --codegen OCaml --extract Part1.Quicksort --odir out Part1.Quicksort.Generic.fst

• The --codegen option tells F* to produce OCaml code

• The --extract option tells F* to only extract all modules in the given namespace, i.e., in this case, all modules in Part1.Quicksort

• The --odir option tells F* to put all the generated files into the specified directory; in this case out

• The last argument is the source file to be checked and extracted

The resulting OCaml code is in the file Part1_Quicksort_Generic.ml, where the F* dot-separated name is transformed to OCaml’s naming convention for modules. The generated code is here

Some points to note about the extracted code:

• F* extracts only those definitions that correspond to executable code. Lemmas and other proof-only aspects are erased. We’ll learn more about erasure in a later chapter.

• The F* types are translated to OCaml types. Since F* types are more precise than OCaml types, this translation process necessarily involves a loss in precision. For example, the type of total orders in Part1.Quicksort.Generic.fst is:

  let total_order_t (a:Type) = f:(a -> a -> bool) { total_order f }
  

  Whereas in OCaml it becomes

  type 'a total_order_t = 'a -> 'a -> Prims.bool
  

  This means that you need to be careful when calling your extracted F* program from unverified OCaml code, since the OCaml compiler will not complain if you pass in some function that is not a total order where the F* code expects a total order.

Compiling an OCaml library

Our extracted code provides several top-level functions (e.g., sort) but not main. So, we can only compile it as a library.

For simple uses, one can compile the generated code into a OCaml native code library (a cmxa file) with ocamlbuild, as shown below

OCAMLPATH=$FSTAR_HOME/lib ocamlbuild -use-ocamlfind -pkg batteries -pkg fstar.lib Part1_Quicksort_Generic.cmxa

Some points to note:

• You need to specify the variable OCAMLPATH which OCaml uses to find required libraries. For F* projects, the OCAMLPATH should include the bin directory of the FStar release bundle.

• The -use-ocamlfind option enables a utility to find OCaml libraries.

• Extracted F* programs rely on two libraries: batteries and fstar.lib, which is what the -pkg options say.

• Finally, Part1_Quicksort_Generic.cmxa references the name of the corresponding .ml file, but with the .cmxa extension to indicate that we want to compile it as a library.

Your can use the resulting .cmxa file in your other OCaml projects.

Adding a ‘main’

We have focused so far on programming and proving total functions. Total functions have no side effects, e.g., they cannot read or write state, they cannot print output etc. This makes total functions suitable for use in libraries, but to write a top-level driver program that can print some output (i.e., a main), we need to write functions that actually have some effects.

We’ll learn a lot more about F*’s support for effectful program in a later section, but for now we’ll just provide a glimpse of it by showing (below) a main program that calls into our Quicksort library.

module Part1.Quicksort.Main
module Q = Part1.Quicksort.Generic

//Printing the elements of an integer list, using the FStar.Printf library
let string_of_int_list l =
  Printf.sprintf "[%s]"
    (String.concat "; " (List.Tot.map (Printf.sprintf "%d") l))

//A main program, which sorts a list and prints it before and after
let main () =
  let orig = [42; 17; 256; 94] in
  let sorted = Q.sort ( <= ) orig in
  let msg =
    Printf.sprintf "Original list = %s\nSorted list = %s\n"
      (string_of_int_list orig)
      (string_of_int_list sorted)
  in
  FStar.IO.print_string msg

//Run ``main ()`` when the module loads
#push-options "--warn_error -272"
let _ = main ()
#pop-options

There are few things to note here:

• This time, rather than calling Q.sort from unverified OCaml code, we are calling it from F*, which requires us to prove all its preconditions, e.g., that the comparison function ( <= ) that we are passing in really is a total order—F* does that automatically.

• FStar.IO.print_string is a library function that prints a string to stdout. Its type is string -> ML unit, a type that we’ll look at in detail when we learn more about effects. For now, keep in mind that functions with the ML label in their type may have observable side effects, like IO, raising exceptions, etc.

• The end of the file contains let _ = main (), a top-level term that has a side-effect (printing to stdout) when executed. In a scenario where we have multiple modules, the runtime behavior of a program with such top-level side-effects depends on the order in which modules are loaded. When F* detects this, it raises the warning 272. In this case, we intend for this program to have a top-level effect, so we suppress the warning using the --warn_error -272 option.

To compile this code to OCaml, along with its dependence on Part1.Quicksort.Generic, one can invoke:

fstar --codegen OCaml --extract Part1.Quicksort --odir out Part1.Quicksort.Main.fst

This time, F* extracts both Part1.Quicksort.Generic.fst (as before) and Part1.Quicksort.Main.fst to OCaml, producing Part1_Quicksort_Main.ml to OCaml.

You can compile this code in OCaml to a native executable by doing:

OCAMLPATH=$FSTAR_HOME/lib ocamlbuild -use-ocamlfind -pkg batteries -pkg fstar.lib Part1_Quicksort_Main.native

And, finally, you can execute Part1_Quicksort_Main.native to see the following output:

$ ./Part1_Quicksort_Main.native
Original list = [42; 17; 256; 94]
Sorted list = [17; 42; 94; 256]