How to Comfortably use F*

The tutorial is the best place to learn F*, however the tutorial is far from perfect. Often the included code is outdated and will not verify properly.

This issue is most pronounced in section 2.3.2 which shows the following seemingly harmless piece of code

open FStar.All
open FStar.List.Tot
open FStar.Ref

val new_counter: int -> St (unit -> St int)
let new_counter init =
  let c = ST.alloc init in
  fun () -> c := !c + 1; !c

If you were to try to verify this code, they would get (Error) could not prove psot-condition. This is not because the type signature is incorrect but due to an issues which can be seen here, here, and here.

Other issues include having old type signatures or missing pieces of code, so if any example does not verify in your editor, I would highly suggest to scroll down to the nearest exercise and click Load in editor. These code snippets are up to date and should not fail at verification

Similarly to the tutorial, Emacs's Fstar-mode is the most mature mode for F* but has its own share of problems that one has to learn to work around

1. No longer allowed to import new modules

   • One issue I often face, is that I start to verify a buffer (I start this with C-cn [verify next statement!]) and add in new definitions. Starting to verify a new buffer causes fstar.exe to be a long living process. When this process starts, it starts to verify all imported libraries at the module name.

     What this means is that if you were to suddenly require a new dependency say FStar.HyperStack you would get the error Namespeace FStar.HyperStack cannot be found even though it is clearly in the standard library.

     This is fixed by simply pressing C-cx to kill the long living process and start a new none, re-verifying the entire buffer

     This isn't the most ideal solution, however this can be dramatically sped up by using verified cached modules.

2. Getting into an Invalid State

   • There are a few keys in the emacs mode that may cause the verifier to give an invalid state.

     One way I often triggered this was by pressing C-cl or C-c<enter>. These commands verify up until your cursor. If your cursor is in the middle of syntax this will likely cause a parse error. The best action is to only use these commands where you cursor is not in the way of any text and rely on C-cn instead to verify the next statement and C-cp to unverify the last statement

3. Invalid Verified Code
   • There are times when the Emacs mode will verify statements which may be invalid. For the sake of simplicity, put the 2.3.2 code in the Tutorial Issues section into a new blank files, and run C-cb or C-cl. Notice that the code verifies perfectly! A trick to get around this is either to C-cn the whole file (this may be time consuming), or to press C-c<enter> at the bottom of the file. These seem to not have the issues C-cl and C-cb have.
4. Running code without generating OCaml code

   • The emacs mode comes with the key combination C-cse, which allows the user to run any verified piece of code!

     This can come in handy if one doesn't feel like generating OCaml and running it in their file

5. Getting type definitions of unfinished definitions
   • One annoying thing about F* is that error messages tend to be opaque. So one trick I've found is to write a function, then put the hole admit () somewhere in the code and see what base signature it requires. This is gotten by C-csp. Note that this isn't always the nicest way to get type signatures as it expands ST into the full blown State which can be quite intimidating.

One of the nicer things about F*, is that the translation to OCaml is very straightforward.

However one issue Ι originally had was how does this work? a post on the F* wiki shows an easy way to achieve this. However, it wasn't clear if this was only for the F* ∩ OCaml ∩ F# subset of F*.

Thankfully, it turns out that this also works for just normal fst and fsti files.

1. Create a fsti file for an interface, say

   (* Getopt.fsti *)
   (* Taken from F* source code *)
   
   module Getopt
   
   open FStar.ST
   open FStar.All
   open FStar.Pervasives
   
   val noshort : Char.char
   
   val cmdline: unit -> list string
   
   

2. Create an OCaml or F# instantiation of this code, with ints replaced with Z.t

   (* GetOpt.ML *)
   
   let noshort = 0
   
   (* ... *)
   
   let cmdline () =
      Array.to_list (Sys.argv)
   

3. Write some F* code which relies on this interface

   (* Useage.fst *)
   
   module Useage
   
   open Getopt
   
   let test = cmdline
   

Now F* will happily verify and produce Useage.ml for you.

Note that a build script is very helpful for the above code, because by default F* generates .ml files for every single used library in the current directory. ★ This is not only slow, but it also clutters the directory. The wiki has a good post covering how to deal with this, however Ι could not get the build script it points to work.

So instead I made this bash script that can be augmented to allow STDLib caching among other improvements that can be made

fstar.exe $1 --codegen OCaml \
--no_extract FStar.Pervasives.Native \
--no_extract FStar.Pervasives \
--no_extract FStar.Mul \
--no_extract FStar.Preorder \
--no_extract FStar.Calc \
--no_extract FStar.StrongExcludedMiddle \
--no_extract FStar.List.Tot.Base \
--no_extract FStar.List.Tot.Properties \
--no_extract FStar.List.Tot \
--no_extract FStar.Seq.Base \
--no_extract FStar.Seq.Properties \
--no_extract FStar.Seq \
--no_extract FStar.Math.Lib \
--no_extract FStar.Math.Lemmas \
--no_extract FStar.BitVector \
--no_extract FStar.UInt \
--no_extract FStar.UInt32 \
--no_extract FStar.UInt64 \
--no_extract FStar.UInt8 \
--no_extract FStar.PropositionalExtensionality \
--no_extract FStar.PredicateExtensionality \
--no_extract FStar.TSet \
--no_extract FStar.Heap \
--no_extract FStar.ST \
--no_extract FStar.IO \
--no_extract FStar.All \
--no_extract FStar.Exn

Thus one can just run this shell script on a .fst file and get the outputted .ml file.

Another piece of data that is needed to run the outputted OCaml code, is to load this into a toplevel with #require "fstarlib";;. I simply put this line in my ~/.ocamlinit, but you could of course put this in the toplevel manually.