What is verified, what is extracted? - FStarLang/FStar GitHub Wiki

(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.)

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.fst will write to disk the interleaving of Main.fsti and Main.fst as Main.ml and the extracted interface Lib.fsti as Lib.ml -- most likely, Lib.ml will contain a bunch of failwith "Not implemented"

  • --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.

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.