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.cmx; the tactic references several modules such as FStar_Tactic; the dynamic loader resolves this against the .cmx already present in fstar.exe and everyone is happy.

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.