Generalizing tactics to customize the behavior of F*

(Summary of a discussion between JP and NS.)

Tactics as a way to customize the behavior of F*

Tactics enable user-defined behavior in order to solve one specific problem: rewriting proof obligations by applying trusted terms, in order to, hopefully, end up with True. In essence, tactics provide an extension point where the user can plug in a general term-rewriting function... while still dealing with a crafted API that prevents unsoundness.

Tactics are thus a specific instance of a general pattern where the user plugs in custom behavior tailored to their application domain.

Extraction tactics

Another such instance is extraction, wherein the user might want to provide custom behavior to rewrite some terms before, say, they are extracted to C. The programmer should be provided with "safe" combinators that implement reduction rules from our EMF* formalization. These "extraction tactics" would be another entry point in F* for the user to provide custom behavior.

Inlining

For instance, the user might want to inspect a term, and rewrite things such as:

load32_le b

into:

    int8_to_int32 b.(0ul)
    |^ int8_to_int32 b.(1ul) <<^ 8ul
    |^ int8_to_int32 b.(2ul) <<^ 16ul
    |^ int8_to_int32 b.(3ul) <<^ 24ul

One way to perform this in a safe manner is to provide a set of combinators, say:

lookup: term -> term // replace a name with its definition
beta: term -> term // beta-reduction when the arguments are values

then, the "extraction tactic" would rewrite:

App (FVar "load32_le", Name b)

by matching onto the term:

match t with
| App (head, args) when should_inline head ->
    let let_bindings = List.map (fun arg ->
      if not (is_value arg) then
        let name = fresh_name () in
        Some (name, arg), Name name
      else
        None, arg
    in
    let args = snd (List.split let_bindings) in
    let let_bindings = List.filter_some (fst (List.split let_bindings)) in
    Let (let_bindings, beta (App (lookup head, args)))

There are numerous advantages:

• we could list in a library the rewriting rules that are legal per the EMF* formalization
• all of the custom hackish rewriting behavior could be moved out of the normalizer into a library (say, lowstar.cmxs) that would contain all of the rewriting tactics for low-level code
• things such as "determining what gets inlined" would be moved out of F*; the inline_for_extraction and [@"substitute"] syntax would be definitely moved out of F* and [@"inline"] would just get a special, user-defined interpretation... one could also implement a policy that any function from the Inline module gets inlined, or that anything that has the shape (load|store)(32|64)_(le|be) would be inlined... this is much more flexible and allows for much experimentation
• this potentially serves more use-cases as we need to customize more and more the behavior of extraction.

Vale

More generally, this enables a much better meta-programming pattern, wherein the user controls very precisely what kind of meta-programming happens, and can potentially perform much more powerful rewritings.

One could even imagine, for instance, that instead of doing two executions of Vale/F* programs, one to print the .S ASM file, and another one to extract to C, the programmer would just run F* once, relying on a custom extraction technique to replace:

let f x =
  embed [ MovDQL ... ]

with

assume val f: int -> unit

while writing out the .S file for the deeply embedded syntax.

Pre-processing tactics

Another case where we might want to perform meta-programming is to generate definitions for data types. For instance, one might want to do "show_deriving", where a universal printer is generated for each datatype. The tactic would then return a new set of toplevel definitions, to be inserted into the program.

This may require operating on the surface syntax of terms; this may also need to happen before desugaring.