Caching verified modules

The flag --cache_checked_modules enables caching of verified modules.

For each file A.fst(i), the cache is written to file A.fst(i).checked.

The .checked file is an OCaml serialization of the type-checked AST of a module together with some meta-data, described below. As such, it has a strong dependence on the version of OCaml used to generate it.

In what follows, consider module A depending on module B; B depending on C.

Metadata in a .checked file

1. An internal version number of the F* AST. This version number is incremented in F* at our discretion, each time we make a semantic change.

2. Hashes encoding the dependence graph.

   • A.fst.checked contains a hash of A.fst and a hash of B.fst.checked
   • B.fst.checked contains a hash of B.fst and a hash of C.fst.checked etc.

Reading and writing .checked files

If you invoke fstar --cache_checked_modules A.fst, this will at most write A.fst.checked.

A few things happen along the way:

1. We build the dependence graph by scanning A.fst and its dependences.

A.fst.checked: A.fst B.fst.checked
B.fst.checked: B.fst C.fst.checked
...

Which is to say that in order to produce A.fst.checked, we depend on the A.fst and B.fst.checked.

We obtain from this analysis a linear ordering of all the files to be checked, in this case C.fst, B.fst, A.fst

2. For each file in the dependences of A.fst, F* proceeds in linear order looking for the corresponding .checked file (TODO: more details on where it looks for the file)

For each file, it validates the hashes. If the hashes are not valid, F* prints a message noting a stale cache file and falls back to verifying the sources of all remaining files.

Otherwise, it loads the .checked file and populates its internal state and continues.

3. If all the dependences were up to date, then F* looks for A.fst.checked. If it is also up to date, F* loads it and continues (e.g., to extraction, if requested), printing a message Verified module: A (0 ms). Otherwise it verified A.fst and if that succeeds write out A.fst.checked.

Options not yet documented

• .checked.lax, produced when --lax is given
• --cache_dir, controls where the .checked files go
• options like --admit_smt_queries, which when set from the command line can result in a .checked file being produced even though the file was not verified.