F★ Interfaces (simple version)

This describes the simple scenario where fsti means "realized module, no code generation" and fst files include visibility modifiers to provide abstraction. If you insist on having a separate notion of interfaces that match against an implementation, see F★ interfaces (split-file, more complicated version).

Interfaces as realized modules

In this scenario, an .fsti file indicates a series of definitions that will be automatically assumed by F*; a .fsti file generates no code at extraction-time. You have to provide, say, an OCaml implementation of the specified interface. For instance, FStar.IO.fsti generates no code; we provide an OCaml-specific implementation of it in lib/ml/FStar_IO.ml.

Digression on realized modules that are modelized in an fst

Some modules are written as .fst's; however, they are meant to be replaced at extraction-time by more efficient implementations. For these modules, you have to pass the --no-extract flag to make sure no code is generated at extraction-time. For instance, FStar.List.fst is replaced by Batteries' more efficient functions at extraction-time.

In the specific case of F*'s standard library, the following modules are implemented as .fst's but then realized: All Heap List Set. Furthermore, for convenience, we provide a single .cmxa for all the OCaml-implemented modules. Therefore, in your Makefile, you should do:

STDLIB_REALIZED=All Heap List Set
FSTARFLAGS=--codegen OCaml $(addprefix --no-extract ,$(STDLIB_REALIZED))

all: $(FSTFILES)
  $(FSTAR) $(FSTARFLAGS) $^
  $(MAKE) -C $(FSTAR_HOME)/lib/ml
  $(OCAML) $(FSTAR_HOME)/lib/ml/fstarlib.cmxa $(FSTFILES:.fst=.ml)

Note: ulib/ml/Makefile.include does this for you. Use it! (See examples/hello)

Modularity and visibility using modifiers in fst files

In this scenario, an fst contains a val for each exported top-level declaration. The val may come with modifiers, such as abstract or private (see Abstraction%2C-reduction-and-visibility-of-type-definitions). You never have both the fst and the fsti!

Possible workflow:

• Step 1: write out a series of assume val definitions in your file; this is the interface that other people in the project will program against.
• Step 2: play around; perhaps write a series of experimental functions in the same file.
• Step 3: once the playground stabilizes, start matching the interface that has been exposed earlier in the file. When a function verifies and matches against its val declaration, remove the assume keyword.

Here are a series of representative use-cases.

Use-case 1: I want to agree on an interface, then play around while others write code against said interface. Answer: use scenario above.

Use-case 2: We agreed on an interface, I have a partial implementation that --lax type-checks, but I still want others to be able to carry on with their lives. Answer: use val and let (no assume) but tell other people who depend on your module to use the --verify-module TheirModule argument so that your module is lax type-checked.

Use-case 3: TheirModule does not verify anymore but you want to carry on with your life and keep working on YourModule. Answer: revert their commit.

Use-case 4: I want to commit a sketch of ideas that doesn't even parse or lax type-check. Answer: use a text file.

Examples

private type int32' =
  | Int32 : i:int{within_int32 i} -> int32'

type int32 = int32'

In this scenario, clients of the module can refer to the type int32; however, they cannot refer to the type int32' or the constructor Int32, meaning that the modelization of 32-bit integers is indeed private. This allows swapping them with a more efficient representation (actual machine integers) at extraction-time.

The SMT-solver, however, is aware of the definition of int32', meaning the SMT-solver can still verify that clients of the module respect the pre-condition of the + operation, i.e. that it does not overflow.

Using abstract wouldn't work, because for client code, the SMT-solver would be unaware of the definition of int32.

abstract type int32 =
  | Int32: ...