What is verified, what is extracted?

(This page is accurate for F* versions after January 9th, 2017.)

Consider the following situation:

• Main.fst has an interface Main.fsti
• Main.fsti depends on Lib
• Lib.fst has an interface Lib.fsti
• everything depends on Prims which only has Prims.fst

The complete, non-transitive dependency graph (minus Prims) is:

Lib.fsti <- Main.fsti
   ^      ↙    ^
   |    ↙      |
Lib.fst     Main.fst

The partial, non-transitive dependency graph (minus Prims) is:

Lib.fsti <- Main.fsti
   ^           ^
   |           |
Lib.fst     Main.fst

Verification

• By default, only modules passed on the command-line are verified. By default, the dependency graph is partial and does not take dependencies on implementations.

  Example: fstar Main.fst performs a partial dependency discovery that stops at Lib.fsti. F* lax-checks Prims and Lib (interface only), then interleaves Main.fst with Main.fsti and verifies Main. (Note: F* then drops the interleaving, and verifies the interface only, then stops.)

• The --verify_module option overrides the verification behavior but does not change the discovery behavior. Only the specified modules are verified, but the dependency discovery is still partial.

  Example: fstar Main.fsti --verify_module Lib performs a partial dependency discovery that stops at Lib.fsti. F* lax-checks Prims, verifies Lib (still interface only). (Note: F* then lax-checks Main, interface only.)

  Example: fstar Main.fsti Lib.fst --verify_module Lib performs a partial dependency discover that includes Lib.fst. F* lax-checks Prims, interleaves Lib.fst with Lib.fsti, then verifies Lib. (Note: F* then drops the interleaving, verifies Lib.fsti alone, then moves on and lax-checks Main.fsti.)

• The --verify_all option overrides both the verification behavior and the discovery dependency behavior. All the modules are verified, and the dependency discovery visits implementations too.

  Example: fstar Main.fsti --verify_all performs a complete dependency discovery that discovers Lib.fst. F* verifies Prims, interleaves Lib.fst with Lib.fsti, then verifies Lib; F* drops the interleaving, then verifies Lib.fsti alone; finally, F* verifies Main (interface only).

  Example: fstar Main.fst --verify_all performs a complete dependency discovery that discovers Lib.fst. F* verifies Prims, interleaves Lib.fst with Lib.fsti, then verifies Lib; F* drops the interleaving, then verifies Lib.fsti alone; F* verifies the interleaving of Main.fst and Main.fsti; F* drops the interleaving, then verifies Main.fsti alone.

Note: --verify_module and --verify_all are mutually exclusive.

Extraction

Extraction is triggered by the presence of a --codegen flag.

• By default, the dependency discovery is partial. All the modules in the dependency graph are extracted. All the extracted modules are written out to disk.

  Example: fstar --codegen OCaml Main.fsti will write to disk the interleaving of Lib.fsti and Lib.fstasLib.mland the extracted interfaceMain.fstiasMain.ml-- most likely,Main.mlwill contain a bunch offailwith "Not implemented"`

• --extract_all controls the dependency discovery; when present, F* performs a complete dependency discovery that takes dependencies on implementations too, as above.

  Example: fstar --codegen OCaml Main.fst will write to disk the interleaving of Lib.fsti and Lib.fstasLib.mland the interleaving ofMain.fstiandMain.fstasMain.ml`

• --no_extract M affects which modules are written out to disk; it just instructs F* to skip writing out a specific file to disk.

  Example: fstar --codegen OCaml --no_extract Lib Main.fst will only write to disk the interleaving of Main.fsti and Main.fst as Main.ml. Note: there is always an implicit --no_extract Prims.

• --extract_module affects which modules are written out to disk; it instructs F* to only extract modules that are specified with --extract_module.

  Example: fstar --codegen OCaml --extract_module Main Main.fst will only write to disk the interleaving of Main.fsti and Main.fst as Main.ml.

Note: --no_extract and --extract_module are mutually exclusive, while (--no_extract or --extract_module) and --extract_all are not mutually exclusive.

Note: there is no way to skip the in-memory extraction of a module in the dependency graph; it does not make sense, as it would create unbound references (in the in-memory extracted code) that are required for extracting later modules. We could devise a lax-extraction mode that only brings into the extraction environment the types of top-level declarations without actually extracting their bodies, but this is for later.