F* IMT Spec: Meta-F* Spec extraction

Motivation

As mentioned in #20, the goal is to extract a function's pre and post-conditions from its definitions. Concretely, given the definition:

val foo : x:T{P1 x} -> Pure T' (requires (P2 x)) (ensures (fun y -> Q x y))
let foo x = ...

We would like to define a Meta-F* tactic that generates the following code:

let foo_pre x = P1 x && P2 x
let foo_post x y = Q x y

With these, generating the QCheck tests should be straightforward.

Architecture

The tactics used to achieve this goal are defined in the SpecExtraction module. The entry point tactic is make_pre_post, which should be called after the function definition with a splice: definition:

val foo : x:T{P1 x} -> Pure T' (requires (P2 x)) (ensures (fun y -> Q x y))
let foo x = ...
%splice[] (make_pre_post (`%foo))

This tactic invokes pre_post, where most of the work is done. The algorithm for retrieving the pre and post-conditions is the following:

  1. Given the function's id (a string), look for its type in the environment.
  2. Collect the arguments of this (function) type, extracting from each of them the binder, type, and potential refinement. For instance, for a type x1:T1{P1 x1} -> x2:T2{P2 x1 x2} -> C, collect_args will compute the list: [(x1;T1; fun x1 -> P1 x1); (x2;T2; fun x1 x2 -> P2 x1 x2)]. For each refinement we abstract all the previous binders. For now, we leave the final computation C untouched.
  3. Join the arguments' refinements to get the function's implicit pre-condition along with its type.
  4. Retrieve from the final computation type C the post-condition (both from an ensures clause and the return type's refinement) and potential explicit pre-condition (requires clause). When there is an explicit pre-condition, join it with the computed implicit pre-condition. There's special treatment for lemmas, as in that case the post-condition doesn't require an extra argument.

Stumbling blocks

Binder unification

Usually, an F* function type follows the pattern: x:(v:T{P v}) -> .... Here, for the first argument, we have two binders: x (from the abstraction) and v (from the refinement). As explained in the previous section, we want to extract the refinement as fun x -> P x, so we need to unify x and v. To do so, we first extract the refinement as fun v -> P v, to then convert it to fun x -> (fun v -> P v) x.

Type synonym resolution

To capture all pre and post-conditions, we need to unfold type synonym definitions. For instance, we need to turn nat into n:int{n >= 0} so that the non-negative condition is considered.

I haven't found yet an elegant way to determine if a free var is a type (to make sure we don’t unfold arbitrary definitions). For now, I'm just checking if its return type is Type or Type0.

  • Correctly determine if an fv is a type.

Nested refinements

We also had to deal with nested refinements, like x:(v:T{P1 v}){P2 x}, generally as a result of the type synonym resolution. To do so, when faced with a refinement x:T{P} the get_refinement tactic recurses on T to retrieve the inner refinement. Then, the binders are unified as previously explained.

logical vs. bool

Our goal is to extract boolean predicates, to use with QCheck. However, F* refinements are of type logical (synonym of Type0). Boolean expressions are lifted to logical using the b2t function.

For now, our approach is to simply write purely boolean refinements and then remove the b2t calls when extracting the specs. It would be nice to define a different DM that deals with bool predicates only, to have the typechecker ensure that the extraction is possible.

visit_tm tactic

Throughout this module, we use the visit_tm tactic provided by the FStar.Tactics.Derived module. However, this tactic definition is incorrect, as it fails to visit the refinements' bound variable's type. Nik confirmed this is a bug.

  • Create a PR to fix this.

Mutually recursive let binding support in sigelt_view

The sigelt_view type, which is used for inspecting top-level declarations, currently doesn't support mutually recursive let bindings. This is a big deal because insert_list's definition is mutually recursive. I've added support for them in my F* fork, but need to ask about some decisions and open a PR.

  • [x] Add mrec support in my F* fork.
  • Open a PR to add mrec let support.

Lemma extraction

As mentioned in the previous section, a lemma's extracted spec differs from one extracted from a regular function in that the former's post-condition doesn’t require the additional argument (which in the latter represents the function's return value). This means that lemmas will need some special treatment when generating tests.

Another little quirk in lemma extraction is that post-conditions are thunked (as a fix for this issue). For now, I just unthunk them by applying unit.

Polymorphic spec extraction

Something weird is happening with the extracted spec of a polymorphic function. For example, take the function:

assume val poly : T.tree 'a 'b -> int
%splice[] (make_pre_post (`%poly))

The extracted spec is:

let poly_pre : 'a . unit -> ('a, Obj.t) Tree.tree -> Prims.bool =
  fun _'b -> fun uu___ -> true
let poly_post : 'a . unit -> ('a, Obj.t) Tree.tree -> Prims.int -> Prims.bool
  = fun _'b -> fun uu___ -> fun r0 -> true

Here, we would expect both type arguments to be extracted as implicit type arguments, but that's not the case. For some reason, 'b becomes a unit argument (I think this is due to Type extracting to unit).

I think this is caused by how F*'s AST encodes arrow types. There seems to be an ambiguity: the type x:X -> y:Y -> Z can be represented both as Tm_arrow [x, y] (Tot Z) and as Tm_arrow [x] (Tot (Tm_arrow [y] (Tot Z))) . In this particular case, poly's type is parsed in the former's style, but the predicates types generated by pack are encoded with the latter. This seems to break F*'s extraction. In the function extract_lb_sig from the FStar.Extraction.ML.Term module, type arguments are only erased if they belong to the flat binder list. Otherwise, they are replaced by a unit argument (which we see in the example).

Opened issue 2290 to address this. I found a quick fix, which I implemented on my fork.

eqtype resolution and extraction

A special case for type synonym resolution is eqtype, as it refines Type with a non-boolean condition.

  • Avoid resolving eqtype synonym.

The obvious problem regarding its extraction is that OCaml doesn’t support eqtype. This is related to the previous point, if we just instantiate all polymorphic types, this wouldn’t be an issue.

Edited by Antonio Locascio