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.

• Native tactics and plugins cannot deal with arbitrary types. Concretely, consider the following module:

module Plugin
open FStar.Tactics
type foo =
  | Bar: foo
[@plugin]
let plug () : Tac foo =
    Bar

Extracting this module will result in the error "(Error 238) Plugin plug can not run natively because Embedding not defined for type Plugin.foo".

When you extract a tactic, say t : foo -> foo, you produce some OCaml binary, which internally works over values that have a native representation.

However, consider the following call to the compiled tactic t: t (id Bar). In this case, the argument is actually the F* term Application (Name "id") (Name "Bar").

To effectively get a b out of t (id Bar), F* normalizes id Bar: in this case we are lucky and we get easily the normal form Bar... which is still a F* term, something like Name "Bar".

The actual native function t excepts a native representation for the value Bar of your type foo. Since foo is isomorphic to unit, let's suppose OCaml compiler flattened out foo into unit, that is, let's suppose the native t expects units as input and produces units.

F* requires a bridge between your F* foo datatype and the native unit, so that F* can feed the F* term Bar to t as (). The same process, in backward, exists for the return value.

These bridges are called embeddings, and are defined in F*'s sources, in the modules FStar.Reflection.Embeddings FStar.Syntax.Embeddings and some others. These modules define embeddings for common types, such as integers, strings, lists, tuples, etc.