F★ interfaces (split file, more complicated version)

You should only use this if the solution described in F★-Interfaces (simple version) doesn't work for you. This solution is more complicated, but also provides more flexibility. In particular, you can split the contents of your module over an fsti and an fst.

In a nutshell

Put the vals in A.fsti (the "partial module"), the lets in A.fst in the same order, then call fstar A.fsti A.fst. What happens is:

• F* verifies the concatenation of A.fsti and A.fst
• drops the environment
• then starts over with only A.fsti, where every val is now assume'd

In that setting, you don't need to put private on let-bindings because only those who have corresponding val's in the fsti will be visible outside of the current module.

Once you've verified that A.fst works against the partial module A.fsti, you can do something like fstar A.fsti B.fst. In that setting, you're making absolutely sure that B.fst is type-checked against the interface A.fsti.

But, for code generation, you will want to pass both the fst and the fsti, since the code is in the fst and F* won't fetch it automatically.

Note (04/05/2016): if you use --codegen and partial modules, then you must use --lax because of unfortunate implementation concerns.

Some use-cases

I need to define some Tot functions in the fsti for my "partial module", because I use them in the pre and post conditions my vals.

Consider using the new syntax for let-definitions. For instance:

T.fsti:

module T

val x: int

let y (z:int{z = x}): Lemma (requires true) (ensures true) = ()

T.fst:

module T

let x = 0

let z = x

Client.fst:

module Client

let main =
  T.y T.x

I want to hide the representation of an inductive type using an fsti

A.fsti:

val my_inductive: int -> Type0

A.fst:

type my_inductive' (x: int) =
  | MyInductive ...

let my_inductive = my_inductive'

Nitty-gritty

When passed both A.fsti and A.fst on the command-line, adjacent, in this exact order, then F* interleaves the two files in order to obtain a valid F* file according to the scoping rules. In particular, when F* hits a val x in the fsti, it includes every declaration from the fst up to let x. If another val is encountered in the fst before let x is hit, then this is an error. So, only use val if you intend to export the value.

See this for some known issues and workarounds when using interfaces in this manner.