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.