Moving away from `abstract`

Background

F* currently (as of 8th April 2019) supports two abstraction mechanisms:

• An abstract qualifier on definitions, and
• Interfaces

The intended behavior of the abstract qualifier is that, if a module A.fst contains an abstract definition abstract let f ..., then the clients of A are allowed to see only the type of f -- the definition of f is abstract to them. In other words, clients cannot make any assumption about how f is implemented.

However, the abstract qualifier implementation in F* has always been leaky. For example, F* allows this kind of definitions:

module A

abstract type t : Type0 =
  | C : x:int -> t

let f (x:t) : (n:int{n == x.x}) = x.x

Even though the type t is marked abstract, F* allows the expression x.x in the type of f. Thus the type of f leaks that t is a record with at least an int type field x.

Here is another instance:

module A

abstract type t : Type0 =
  | C : x:int -> t

module Test

open A

let test () = hasEq t

Even though A.t is abstract, Test can observe that it has decidable equality. Arguably, this is an implementation bug that's easy to fix, but it shows how fickle the implementation of abstract can be.

Interfaces, on the other hand, are rock-solid. When a programmer writes A.fsti and A.fst, for verification purposes, the clients only see A.fsti, and hence all the implementation details are hidden by construction. So our first example, when using interfaces, does not even typecheck:

//A.fsti:

module A

val t : Type0

let f (x:t) : (n:int{n == x.x}) = x.x  //Type error

Similarly, for the second example, if the interface of A only has val t : Type0, clients can't observe whether t has decidable equality.

use_extracted_interfaces

Some time back we tried to fix the abstract keyword implementation in the typechecker by implementing a scheme to automatically extract an interface from a .fst file, typecheck the interface to make sure that it verifies, and then use it for verifying the clients. In principle, it fixes the above two problems. The scheme is implemented under an F* option, --use_extracted_interfaces.

However, we had a hard time making this flag the default. While the algorithm to extract and verify the interface itself was quite easy, integrating it with rest of the typechecker (desugaring, extraction, etc.) turned out to be a challenge. In addition, creating interfaces is really a design problem, F* can use some heuristics to generate one from an implementation, but it is a good practice to think about what should be exported to clients in an interface.

And so, we are moving away from abstract

in favor of interfaces being the only mechanism to enforce abstraction.

Rest of the document contains a guide to how to migrate your .fst that may have some definitions marked abstract, to use interfaces instead. The only objective function of this guide is to have least impact on the clients.

Converting .fst with abstract to use interfaces instead

Copy the .fst to .fsti, then for each definition:

• If the definition is pure or ghost (Tot, Pure, PURE, GTot, Ghost, GHOST, ...) and is not marked abstract, keep the definition in the interface.

• If the definition is a Lemma, marking it abstract is unnecessary. You may want to keep only the val in the interface, while having the implementation in the .fst file. Note that in some cases, you may have to do it anyway, since the proof of the lemma may not typecheck in the interface (after removing some abstract definitions, as below).

• If the definition is pure or ghost, and is marked abstract, keep only the val in the interface, moving the body to the .fst.

• If the definition is effectful (non pure and ghost), Lemma guideline above applies (abstract is unnecessary, you may want to keep only the val in the interface etc.).

• If the definition is marked inline_for_extraction, and you are not using --cmi, it must be kept in the interface, even if it is effectful (I am yet to see a case where a pure or ghost function is marked inline_for_extraction as well as abstract, in which case we need to rethink).

In the above, type definitions fall into the pure or ghost category.

Now taking this interface as the .fsti, tweak the original .fst accordingly so that it typechecks as per the interface.

Tip: Suppose there was a definition of the following form in the original .fst:

val incr (x:int) : int = x + 1
let incr x = x + 1

Since this is not marked abstract, as per the guidelines above, we would like to keep this definition in the interface. However, since an interface cannot have both val and let, we would need to combine them in the .fsti as:

let incr (x:int) : int = x + 1

while the definition goes away from the .fst.