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 A.fsti.checked and A.fsti.auto-generated, the latter being 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.

1. abstract val f : t is retained in the interface as val f : t.

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

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

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

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

6. 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)

7. 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.

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

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

10. 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).