Revised checking of a module's interface

There are two mechanisms by which F* enforces abstraction of a module's interface.

1. Type-checking the context of a module against that module's explicitly provided interface. i.e., when B uses A, check module B against A.fsti, if it exists.

2. In the absence of A.fsti, check B against the exported symbols of module A, where the exported symbols are determined by inspecting the qualifiers (like abstract etc.) that decorate the definitions in A.

Option 1 is much more robust. Option 2, in contrast, has been plagued by persistent problems in the check_exports function, like https://github.com/FStarLang/FStar/issues/1112. Since the goal of check_exports is to enforce the abstraction it plays a crucial role in modularity of verification, and where abstraction is relied upon for meta-properties like parametricity, it is also important for soundness.

This note suggests abandoning option 2 and instead automatically reducing all interface checking to Option 1.

General strategy

0. Remove check_exports altogether.

1. Define a simple syntactic procedure by which an interface can be extracted from a module

2. Every invocation of fstar.exe that triggers type-checking will be forced to contain only a single source file on the the command line: this is the only file that will be verified, and it will be verified against the interfaces of all its dependences.

The automatically extracted interface of a module will be fully verified, just like any hand-written .fsti

The main intended usage of this is in conjunction with separate compilation/verification.

Given A.fst used by B.fst, we expect verification to proceed as follows, which will be orchestrated by fstar --dep full, so if you use the template makefile, then make verify-all should do all this for you.

1. fstar A.fst: producing A.fst.checked
2. fstar --check_interface A.fst: producing A.fsti.checked
3. fstar B.fst: producing B.fst.checked while reading A.fsti.checked.
4. fstar --check_interface B.fst: producing B.fsti.checked.

Note, in the future, once we get fstar --indent to work reliably, we could expect fstar --check_interface A.fst to also emit A.fsti.auto-generated, a source representation of the computed interface.

Automatically extracting an interface from a module

A module implementation is a list of top-level "sigelts". For each sigelt, we decide whether to include it in the interface or not, based on its qualifiers and its annotated type, if any.

-- abstract val f : t is retained in the interface as val f : t. If both val and let are present for a let binding, then only val declaration is retained in the interface.

-- abstract let [rec] f1 : t1 = e ... and ... fn:tn = en is included in the interface as val f1 : t1 ... val fn : tn.

-- abstract type t1:k1 = ... and tn:kn = ... is retained in the interface as val t1 : k1 ... val tn : kn.

-- For any other qualifier, an inductive type definition is retained in the interface as is.

-- let f : (x:t) -> Lemma args = e is retained as val f: (x:t) -> Lemma args

-- For any other visibility qualifier q (i.e., private, irreducible, or nothing), q val f : t is retained in the interface as is.

-- irreducible let f : t = e is retained in the interface as irreducible val f : t. (Note, retaining the irreducible qualifier is important, since it controls the equations about f that may appear in a computed VC)

-- For any other qualifier, q, q let f [: t] = e, if:

a. the annotation `t` is not present (although we should continue to advocate annotating top-level types), then it is retained in the interface as is.

b. if `t` is nullary function with a type that is not a sub-singleton (e.g., unit, squash etc.); or is a function whose effect is `PURE, GHOST` with a non sub-singleton result type; or has some reifiable effect, then it is retained in the interface as is.

c. Otherwise, only `q val f : t` is retained in the interface.

-- Any top-level level assumption q assume Foo: t is retained in the interface, unless q is abstract.

-- Any effect definition or abbreviation is retained in the interface (they can't be marked abstract anyway)

-- An pragma, like #set-options or #reset-options, is retained in the interface.

Other qualifiers like unfold and inline_for_extraction are retained for a symbol in the interface only if that symbol's definition is also retained (since without a definition, these qualifiers do not make sense).