Compiling tactics

Summary of a discussion between NS, Guido and JP on 05/05.

Compiling tactics

A reminder on OCaml file extensions.

• .cmi interface binary description
• .cmo bytecode object file
• .cma byte archive (several .cmo)
• .cmx native object
• .cmxa native archive (several .cmx and .o)
• .cmxs dynamically-loadable native object file (see https://caml.inria.fr/pub/docs/manual-ocaml/libref/Dynlink.html)

fstar.exe contains several .cmx's: FStar_Tactic.cmx, FStar_Util.cmx, NativeTactics.cmx.

To compile a tactic, one needs to:

• extract it into mytactic.ml
• using ocamlopt -shared -I ..., compile it against the .cmx's, .mli's and .cmi's above to obtain mytactic.cmxs

The steps above may be automated by fstar.exe itself, but we can assume that they are performed manually for now.

Then, the resulting .cmxs shall be loaded into fstar.exe. Again, this may be performed automatically, but we may assume as a temporary stopgap that the user calls fstar.exe -load mytactic.cmxs; the tactic references several modules such as FStar_Tactic; the dynamic loader resolves this against the corresponding .cmx already present in fstar.exe and everyone is happy.

Naturally, one should not screw things up, and the cmxs used for the build of mytactic.cmxs shall be exactly those linked into fstar.exe

One thing to note is that the Dynlink module does not provide a "lookup function by name" feature; instead, we suggest the following NativeTactics.mli:

val register_prim_step: string -> int -> (list term -> option term) -> unit
val register_tactic: string -> int -> (list term -> tactic term) -> unit
val find: string -> (list term -> option term) option

Then, NativeTactics.cmx is linked into fstar.exe, and at tactic-extraction time, fstar.exe appends to the generated mytactic.ml a few calls to NativeTactics.register_....

Embeddings, two-way communication between normalizer and native tactics

Consider a parameterized tactic val f: nat -> Tac term. When the user writes by_tactic (f 2), a type-checking time, a VC is generated which contains a tactic sub-term of the form Tm_app (Tm_fvar "f", Tm_constant "2"). F* then:

• deeply embeds the environment as a term
• calls the normalize to reduce the term above applied to the environment
• gets back a list of sub-goals to process, along with an updated environment which is de-embedded.

The gist of the issue is that the natively-compiled f present in mytactic.cmxs has type val f: Prims.nat -> (env -> goal -> (env * goal list) option) (roughly), but the F* typechecker manipulates terms, meaning that one has to de-embed and re-embed when crossing the boundary between the F* typechecker and the compiled code.

Conceptually (doesn't type-check)

We want, at tactic-extraction time, to generate the embeddings and de-embeddings. For instance:

... contents of mytactic.ml ... definition of f ...
NativeTactics.register "f" (embed (Arrow Nat, ...) f
                                   ^^^^^^^^^
                                   a "dyn" type that describes the type of `f`, written
                                   out by F*'s extraction

This doesn't work, however, because i) register would have to use a lot of Obj.magic's (no way to refine the type of f based on the dynamic type and ii) it doesn't work for the function case because we need to call back into the normalizer.

Symbolically evaluating embed

Instead, we symbolically evaluate the embed function and generate specialized bits of code for each f and its type.

We assume f fits within the Hindley-Milner type system (prenex polymorphism). Then,

embed_fun (dembed_a: term -> a) (embed_b: b -> term) (f: a -> b): term -> term =
  fun x ->
    embed_b (f (dembed_a x))
embed_nat (n: nat): term =
  Tm_constant (string_of_nat n)
embed_bool (b: bool) =
  ...
embed_var (x: term): term = x

dembed_fun (embed_a: a -> term) (dembed_b: term -> b) (f: term) =
  fun (x: a) ->
    dembed_b (normalize (Tm_app (f, embed_a)))
dembed_nat (n: term): nat =
  match n with Tm_constant (Const_int n) -> int_of_string n | _ -> assert false
dembed_bool (b: term): bool =
  ...
dembed_var (x: term): term = x

The "var" case is the most interesting. It corresponds to a tactic that has type, say:

val g: #a -> a -> (a -> bool) -> Tac term

a is a type variable; we don't know how to embed/dembed it! But, by parametricity, g ought to be able to deal with any such a (remember that g is in the Hindley-Milner subset, this wouldn't work with dependent types, as g may refine the a based on the value of some other parameter). We pick a = term which generates the identity embedding/de-embedding.