Cross module Inlining

It sometimes happens that one enforces modular abstractions during typechecking (e.g., the abstraction enforces some semantic property; or, hides from the verifier needless details about the implementation), even though these abstractions are unnecessary, or worse, harmful for executable code.

In such cases, one may mark the declarations of a symbol with the inline_for_extraction qualifier, even when that declaration appears in a module's interface. This instructs F* to specialize clients of the module with respect to a particular implementation of that module (whichever implementation is found on the include path) by inlining the definition of that symbol during extraction.

A basic example: examples/extraction/cmi/0

In an interface file A.fsti we have:

inline_for_extraction
val id : #a:Type -> a -> a

And in a corresponding implementation A.fst we have:

let id #a x = x

In a client module, B.fst we have:

type t =
  | T
let test_id_T = A.id T

We would like test_id_T to be extracted simply as let test_id_T = T, specializing the code with respect to the definition of A.id in A.fst. However, verification of B.fst should be only with respect to the interface A.fsti.

By providing the --cmi flag to F* during both dependency scanning (--dep full) and on --codegen invocations, this produces the desired behavior. See /examples/extraction/cmi/Makefile.common.

Note, the --cmi flag is transitionary: the flag will be removed and inlining implementations across interface boundaries will be the default behavior for all symbols marked inline_for_extraction in an interface.

Some downsides

This feature intentionally breaks separate compilation for modules that interact via inline_for_extraction interfaces.