Caching verified modules
--cache_checked_modules enables caching of verified modules.
For each file
A.fst(i), the cache is written to file
.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 depending on
Metadata in a .checked file
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.
Hashes encoding the dependence graph.
A.fst.checkedcontains a hash of
A.fstand a hash of
B.fst.checkedcontains a hash of
B.fstand a hash of
Reading and writing .checked files
If you invoke
fstar --cache_checked_modules A.fst, this will at most write
A few things happen along the way:
- 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
We obtain from this analysis a linear ordering of all the files to be checked, in this case
C.fst, B.fst, A.fst
- 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.
- 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.fstand 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.