How to Comfortably use F*

1 How to Comfortably use F*

F* is a dependently typed language based off of Hoare Type Theory, refinement types, a SMT solver and features an effect system.

All these features culminate in a high level language that excels at verifying and generating low level code. Although F* has been used to achieve wondrous results, actually learning the language and becoming comfortable in it is quite challenging.

This post thus seeks out to remedy common gotchas I came across while learning F*. Future posts will be dedicated to explaining various parts of the STDLib and how the OCaml extraction works.

1.1 Prerequisites

  • I would read the introduction section of the tutorial to get a good feel for the language.
    • Great thing about this tutorial, is that it already has an editor setup for verifying code.
  • I would also suggest getting familiar with OCaml, at least enough to be able to read.
  • I would then install F*.
    • Opam is the easiest, however you will also need to install Z3 for your system as well
    • This requires a working version of OCaml between 4.04 and 4.08 ([4.04, 4.08)).
  • Then setup your editor This post will assume you are using emacs as that has the most mature editing mode.
    • I also suggest playing around with the listed keybindings.
  • Be comfortable with Emacs bindings, in this post I will often say C-cb to mean Control-c Control-b

1.2 Into the Deep End

Great, Now that F* is now installed on your system, we can begin to explore various pain points surrounding development and learning.

1.2.1 Tutorial Issues

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

1.2.2 Emacs Mode Issues And Tips

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.

1.2.3 Sharing OCaml and F* code

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.

1.2.4 Build Scripts and Environments

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.

1.3 Final Words

F* is a rather fun language, however it has a lot of unique quirks that must be programmed around. Hopefully this blog post has helped you avoid some of them.

Happy Hacking!

Written by Jeremy Ornelas, core developer and researcher at Metastate.

Metastate has ceased its activities on the 31st of January 2021. The team members have joined a new company and working on a new project. If you're interested in programming language theory, functional programming, type theory, formal verification, or compiler engineering positions, check out the open positions at Heliax.

If you have any feedback or questions on this article, please do not hesitate to contact us: hello@heliax.dev.