Large scale separate verification & compilation

This is a summary of a lengthly discussion between Cédric Fournet, (jet-lagged) Tahina Ramananandro, and Jonathan Protzenko (current author).

Problem statement

With Project Everest making steady progress, we are now facing the problem of large-scale F* developments, and how to achieve some degree of modularity. This is important for:

• performance (parsing and lax-checking a huge dependency graph can make verifying even a standalone file difficult)
• collaboration (we want people working on, say, HACL/lib, to be independent from people working on, say, miTLS)
• proofs (we want to say that we can verify miTLS without having access to any of the low-level modules from HACL/lib).

The running example is miTLS, which wants to verify against HACL/lib (née low-level/crypto), but really only uses a handful of functions, not the whole pyramid of modules.

A look at the dependency graph

Ideally, we want the following dependency graph:

`-,
   \              Crypto.fsti   <----   miTLS
C1  `-,  <--,     |
       \     \    v
  C2    | <-- Crypto.fst
        |    ____ |
  C3   /  <-'    /
C4  ,-'  <------'
   /
  |
,-'

• miTLS only needs a handful of functions exported by Crypto.fsti;
• Crypto.fsti does NOT depend on any of the crypto modules C1 ...C4; rather, it uses a combination of abstract types and type abbreviations to expose a standalone cryptographic interface
• the implementation of Crypto.fsti, that is, Crypto.fst, provides concrete functions and contains a myriad of dependencies of each of the crypto modules C1 through C4.

This means that we can split verification, extraction and build in two steps:

• verify C1 .. C4, Crypto.fst and Crypto.fsti together
• verify miTLS against Crypto.fsti ONLY.

The latter step is a net improvement, because:

• the dependency graph is cut off (the arrow from Crypto.fsti to Crypto.fst is gone), meaning that we ignore all the C1 .. C4 files
• we have a bulletproof argument that miTLS won't traverse the abstraction to use some unsafe low-level crypto primitive (F* doesn't even read the files)
• people can work on C1 .. C4 separately.

Achieving modularity

Right now, when faced with both Crypto.fst and Crypto.fsti, F* generates a dependency on both files. We introduce a new option, --partial, that controls whether the arrow from Crypto.fsti to Crypto.fst exists in the dependency graph or not.

Verification

We have:

• --verify_all: this implies NOT(--partial), because we want to verify all the project
• --verify_module Mi: this implies --partial, because we're only interested in specific modules Mi; the dependency graph may have several connected components, but each Mi MUST be in the graph (JP: check that this is indeed a hard error)
• default behavior: verify modules passed on the command-line only; rely on the user-provided --partial to determine whether to follow dependency arrows from interfaces to implementations

Implementation note: this is a two-liner because the code for --partial is still there with a note saying that this is the --stratified behavior.

Extraction