Interfaces

Look through the F* standard libary (in the ulib folder) and you’ll find many files with .fsti extensions. Each of these is an interface file that pairs with a module implementation in a corresponding .fst file.

An interface (.fsti) is very similar to a module implementation (.fst): it can contain all the elements that a module can, including inductive type definitions; let and let rec definitions; val declarations; etc. However, unlike module implementations, an interface is allowed to declare a symbol val f : t without any corresponding definition of f. This makes f abstract to the rest of the interface and all client modules, i.e., f is simply assumed to have type t without any definition. The definition of f is provided in the .fst file and checked to have type t, ensuring that a client module’s assumption of f:t is backed by a suitable definition.

To see how interfaces work, we’ll look at the design of the bounded integer modules FStar.UInt32, FStar.UInt64, and the like, building our own simplified versions by way of illustration.

Bounded Integers

The F* primitive type int is an unbounded mathematical integer. When compiling a program to, say, OCaml, int is compiled to a “big integer”, implemented by OCaml’s ZArith package. However, the int type can be inefficient and in some scenarios (e.g., when compiling F* to C) one may want to work with bounded integers that can always be represented in machine word. FStar.UInt32.t and FStar.UInt64.t are types from the standard library whose values can always be represented as 32- and 64-bit unsigned integers, respectively.

Arithmetic operations on 32-bit unsigned integers (like addition) are interpreted modulo 2^32. However, for many applications, one wants to program in a discipline that ensures that there is no unintentional arithmetic overflow, i.e., we’d like to use bounded integers for efficiency, and by proving that their operations don’t overflow we can reason about bounded integer terms without using modular arithmetic.

Note

Although we don’t discuss them here, F*’s libraries also provide signed integer types that can be compiled to the corresponding signed integters in C. Avoiding overflow on signed integer arithmetic is not just a matter of ease of reasoning, since signed integer overflow is undefined behavior in C.

Interface: UInt32.fsti

The interface UInt32 begins like any module with the module’s name. Although this could be inferred from the name of the file (UInt32.fsti, in this case), F* requires the name to be explicit.

module UInt32

val t : eqtype

UInt32 provides one abstract type val t : eqtype, the type of our bounded integer. Its type says that it supports decidable equality, but no definition of t is revaled in the interface.

The operations on t are specified in terms of a logical model that relates t to bounded mathematical integers, in particular u32_nat, a natural number less than pow2 32.

let n = 32
let min : nat = 0
let max : nat = pow2 n - 1
let u32_nat = n:nat{ n <= max }

Note

Unlike interfaces in languages like OCaml, interfaces in F* can include let and let rec definitions. As we see in UInt32, these definitions are often useful for giving precise specifications to the other operations whose signatures appear in the interface.

To relate our abstract type t to u32_nat, the interface provides two coercions v and u that go back and forth between t and u32_nat. The lemma signatures vu_inv and uv_inv require v and u to be mutually inverse, meaning that t and u32_nat are in 1-1 correspondence.

val v (x:t) : u32_nat
val u (x:u32_nat) : t

val uv_inv (x : t) : Lemma (u (v x) == x)
val vu_inv (x : u32_nat) : Lemma (v (u x) == x)

Modular addition and subtraction

Addition and subtraction on t values are defined modulo pow2 32. This is specified by the signatures of add_mod and sub_mod below.

(** Addition modulo [2^n]

    Unsigned machine integers can always be added, but the postcondition is now
    in terms of addition modulo [2^n] on mathematical integers *)
val add_mod (a:t) (b:t) 
  : y:t { v y = (v a + v b) % pow2 n } 

(** Subtraction modulo [2^n]

    Unsigned machine integers can always be subtracted, but the postcondition is now
    in terms of subtraction modulo [2^n] on mathematical integers *)
val sub_mod (a:t) (b:t) 
  : y:t { v y = (v a - v b) % pow2 n }

Bounds-checked addition and subtraction

Although precise, the types of add_mod and sub_mod aren’t always easy to reason with. For example, proving that add_mod (u 2) (u 3) == u 5 requires reasoning about modular arithmetic—for constants like 2, 3, and 5 this is easy enough, but proofs about modular arithmetic over symbolic values will, in general, involve reasoning about non-linear arithmetic, which is difficult to automate even with an SMT solver. Besides, in many safety critical software systems, one often prefers to avoid integer overflow altogether.

So, the UInt32 interface also provides two additional operations, add and sub, whose specification enables two t values to be added (resp. subtracted) only if there is no overflow (or underflow).

First, we define an auxiliary predicate fits to state when an operation does not overflow or underflow.

let fits (op: int -> int -> int)
         (x y : t)
  = min <= op (v x) (v y) /\
    op (v x) (v y) <= max

Then, we use fits to restrict the domain of add and sub and the type ensures that the result is the sum (resp. difference) of the arguments, without need for any modular arithmetic.

(** Bounds-respecting addition

    The precondition enforces that the sum does not overflow,
    expressing the bound as an addition on mathematical integers *)
val add (a:t) (b:t { fits (+) a b }) 
  : y:t{ v y == v a + v b }

(** Bounds-respecting subtraction

    The precondition enforces that the difference does not underflow,
    expressing the bound as an subtraction on mathematical integers *)
val sub (a:t) (b:t { fits (fun x y -> x - y) a b }) 
  : y:t{ v y == v a - v b }

Note

Although the addition operator can be used as a first-class function with the notation (+), the same does not work for subtraction, since (-) resolves to unary integer negation, rather than subtraction—so, we write fun x y -> x - y.

Comparison

Finally, the interface also provides a comparison operator lt, as specified below:

(** Less than *)
val lt (a:t) (b:t) 
  : r:bool { r <==> v a < v b }

Implementation: UInt32.fst

An implementation of UInt32 must provide definitions for all the val declarations in the UInt32 interface, starting with a representation for the abstract type t.

There are multiple possible representations for t, however the point of the interface is to isolate client modules from these implementation choices.

Perhaps the easiest implementation is to represent t as a u32_nat itself. This makes proving the correspondence between t and its logical model almost trivial.

module UInt32

let t = n:nat { n <= pow2 32 - 1}

let v (x:t) = x
let u (x:u32_nat) = x

let uv_inv x = ()
let vu_inv x = ()

let add_mod a b = (a + b) % pow2 32
let sub_mod a b = (a - b) % pow2 32

let add a b = a + b
let sub a b = a - b

let lt (a:t) (b:t) = v a < v b

Another choice may be to represent t as a 32-bit vector. This is a bit harder and proving that it is correct with respect to the interface requires handling some interactions between Z3’s theory of bit vectors and uninterpreted functions, which we handle with a tactic. This is quite advanced, and we have yet to cover F*’s support for tactics, but we show the code below for reference.

open FStar.BV
open FStar.Tactics

let t = bv_t 32
let v (x:t) = bv2int x
let u x = int2bv x

let sym (#a:Type) (x y:a)
  : Lemma (requires x == y)
          (ensures y == x)
  = ()

let dec_eq (#a:eqtype) (x y:a)
  : Lemma (requires x = y)
          (ensures x == y)
  = ()

let uv_inv (x:t)
  = assert (u (v x) == x)
        by (mapply (`sym);
            mapply (`dec_eq);
            mapply (`inverse_vec_lemma))

let ty (x y:u32_nat)
  : Lemma (requires eq2 #(FStar.UInt.uint_t 32) x y)
          (ensures x == y)
  = ()

let vu_inv (x:u32_nat)
  = assert (v (u x) == x)
        by (mapply (`ty);
            mapply (`sym);
            mapply (`dec_eq);
            mapply (`inverse_num_lemma))

let add_mod a b =
  let y = bvadd #32 a b in
  assert (y == u (FStar.UInt.add_mod #32 (v a) (v b)))
     by  (mapply (`sym);
          mapply (`int2bv_add);
          pointwise
              (fun _ -> try mapply (`uv_inv) with | _ -> trefl());
          trefl());
  vu_inv ((FStar.UInt.add_mod #32 (v a) (v b)));
  y

let sub_mod a b =
  let y = bvsub #32 a b in
  assert (y == u (FStar.UInt.sub_mod #32 (v a) (v b)))
     by
         (mapply (`sym);
          mapply (`int2bv_sub);
          pointwise
              (fun _ -> try mapply (`uv_inv) with | _ -> trefl());
          trefl());
  vu_inv ((FStar.UInt.sub_mod #32 (v a) (v b)));
  y

let add a b =
  let y = add_mod a b in
  FStar.Math.Lemmas.modulo_lemma (v a + v b) (pow2 32);
  y

let sub a b =
  let y = sub_mod a b in
  FStar.Math.Lemmas.modulo_lemma (v a - v b) (pow2 32);
  y

let lt (a:t) (b:t) = v a < v b

Although both implementations correctly satisfy the UInt32 interface, F* requires the user to pick one. Unlike module systems in some other ML-like languages, where interfaces are first-class entities which many modules can implement, in F* an interface can have at most one implementation. For interfaces with multiple implementations, one must use typeclasses.

Interleaving: A Quirk

The current F* implementation views an interface and its implementation as two partially implemented halves of a module. When checking that an implementation is a correct implementation of an interface, F* attempts to combine the two halves into a complete module before typechecking it. It does this by trying to interleave the top-level elements of the interface and implementation, preserving their relative order.

This implementation strategy is far from optimal in various ways and a relic from a time when F*’s implementation did not support separate compilation. This implementation strategy is likely to change in the future (see this issue for details).

Meanwhile, the main thing to keep in mind when implementing interfaces is the following:

  • The order of definitions in an implementation much match the order of val declarations in the interface. E.g., if the interface contains val f : tf followed by val g : tg, then the implementation of f must precede the implementation of g.

Also, remember that if you are writing val declarations in an interface, it is a good idea to be explicit about universe levels. See here for more discussion.

Other issues with interleaving that may help in debugging compiler errors with interfaces:

Comparison with machine integers in the F* library

F*’s standard library includes FStar.UInt32, whose interface is similar, though more extensive than the UInt32 shown in this chapter. For example, FStar.UInt32 also includes multiplication, division, modulus, bitwise logical operations, etc.

The implementation of FStar.UInt32 chooses a representation for FStar.UInt32.t that is similar to u32_nat, though the F* compiler has special knowledge of this module and treats FStar.UInt32.t as a primitive type and compiles it and its operations in a platform-specific way to machine integers. The implementation of FStar.UInt32 serves only to prove that its interface is logically consistent by providing a model in terms of bounded natural numbers.

The library also provides several other unsigned machine integer types in addition to FStar.UInt32, including FStar.UInt8, FStar.UInt16, and FStar.UInt64. F* also has several signed machine integer types.

All of these modules are very similar, but not being first-class entities in the language, there is no way to define a general interface that is instantiated by all these modules. In fact, all these variants are generated by a script from a common template.

Although interfaces are well-suited to simple patterns of information hiding and modular structure, as we’ll learn next, typeclasses are more powerful and enable more generic solutions, though sometimes requiring the use of higher-order code.