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.

0. If both val and let are present for a let binding, then only val declaration is retained in the interface.

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