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  ,-'  <------'
   /
  |
,-'