Running tactics natively (and plugins)

A quick guide on how to a run a tactic (or other functions) natively, in order to make typechecking/verification faster.

First of all, make sure you have compiled and installed the tactics library binary

$ make -C ulib/ install-fstar-tactics

Suppose we have two modules Plug and Call:

module Plug

open FStar.Tactics

let rec cd (i:int) : Tac unit =
    if i > 0
    then cd (i-1)
    else ()

let tau () : Tac unit =
    dump "Begin";
    cd 1000000;
    dump "End"

module Call

open FStar.Tactics
open Plug

let _ = assert True by (tau ())

On my machine, verifying Call takes about 8 seconds of tactic runtime:

$ ./bin/fstar.exe Call.fst --tactics_info 
proof-state: State dump @ depth 1 (Begin):
Location: Plug.fst(12,4-12,16)
Goal 1/1:
 |- _ : Prims.squash Prims.l_True

proof-state: State dump @ depth 0 (End):
Location: Plug.fst(14,4-14,14)
Goal 1/1:
 |- _ : Prims.squash Prims.l_True

Tactic fun _ ->
  [@ FStar.Pervasives.inline_let ]let _ = () in
  Plug.tau () ran in 7808 ms (Call)
Verified module: Call
All verification conditions discharged successfully

What we can do instead is mark tau as a native plugin, extract it, and then re-verify Call with the plugin loaded.

The first step is accomplished by adding the plugin attribute to tau.

...

[@plugin]
let tau () : Tac unit =
...

This means that calls to tau will instead be performed natively. Importantly, functions called by tau (such as cd) will also be run natively. Extraction is "deep", in a sense. However, standalone calls to cd will not switch to its native version unless cd itself is marked as a plugin.

Now, we can extract Plug as such:

$ ./bin/fstar.exe Plug.fst --codegen Plugin

This will generate a Plug.ml file (alongside others). You can check that Plug.ml contains a register_tactic call for tau (if it does not, perhaps you forgot the plugin attribute).

Now we can verify Call asking it to load the plugin like this (--tactics_info is there just to get timing info):

$ ./bin/fstar.exe Call.fst --load Plug --tactics_info
findlib: [WARNING] Interface main.cmi occurs in several directories: /home/guido/r/fstar/guido_tactics/bin/fstar-compiler-lib, /home/guido/.opam/4.05.0/lib/ocaml/compiler-libs
findlib: [WARNING] Interface topdirs.cmi occurs in several directories: /home/guido/.opam/4.05.0/lib/ocaml/compiler-libs, /home/guido/.opam/4.05.0/lib/ocaml
cmxs file: Plug.cmxs
proof-state: State dump @ depth 1 (Begin):
Location: Plug.fst(12,4-12,16)
Goal 1/1:
 |- _ : Prims.squash Prims.l_True

proof-state: State dump @ depth 0 (End):
Location: Plug.fst(14,4-14,14)
Goal 1/1:
 |- _ : Prims.squash Prims.l_True

Tactic fun _ ->
  [@ FStar.Pervasives.inline_let ]let _ = () in
  Plug.tau () ran in 8 ms (Call)
Verified module: Call
All verification conditions discharged successfully

The first two lines are output from ocamlopt being called to compile Plug.ml into Plug.cmxs. Note that the tactic now ran in 8ms.

This can also be performed in a single file, but the purpose is rather lost since the extraction call will need to verify the entire file without having the relevant plugins loaded, so tau would run slowly that first time.

Adding a module to fstartaclib

fstartaclib contains some modules that are auto laoded into F* on every run so their tactics are run natively. Notably: typeclasses are included here. To add a new module, simply add it to the EXTRACT_MDOULES variable in the fstartaclib.mgen rule in ulib/Makefile.

See for instance this example https://github.com/FStarLang/FStar/commit/83b8bb3cb83d68e9c2c9023bf43dbbebc1a5f616. The second change, to the FSTAR_FILES variable, is needed only since Steel.* modules are filtered out by default, but should not be usually needed.

Gotchas

• F* will not detect changes in the plugin's ML file and recompile. I would advise to just rm *.cmxs before each run when debugging.