Primitive Effect Refinements

Note

This chapter provides some background on Floyd-Hoare logic and weakest-precondition-based verification condition generation. This is necessary if you want to understand a bit about how F* infers the logical constraints needed to prove the correctness of a program. It is also useful background for more advanced material in subsequent chapters about defining custom effects in F*, e.g., effects to model state, exceptions, or concurrency.

Refinement types x:t{p} refine value types t and allow us to make more precise assertions about the values in the program. For example, when we have v : x:int{x >= 0}, then not only we know that v is an int, but also that v >= 0.

In a similar manner, F* allows refining computation types with specifications that describe some aspects of a program’s computational behavior. These effect refinements can, in general, be defined by the user in a reasoning system of their choosing, e.g., the refinements may use separation logic, or they may count computation steps.

However, F* has built-in support for refining the specification of pure programs with effect refinements that encode the standard reasoning principles of Floyd-Hoare Logic and weakest precondition-based calculi. Foreshadowing what’s about to come in this chapter, we can write the following specification for the factorial function:

open FStar.Mul
let rec factorial (x:int)
  : Pure int (requires x >= 0) (ensures fun r -> r >= 1)
  = if x = 0
    then 1
    else x * factorial (x - 1)

Intuitively, this type states that factorial x is a computation defined only when x >= 0 and always terminates returning a value r >= 1. In a way, this type is closely related to other, more familiar, types we have given to factorial so far, e.g., nat -> pos, and, indeed, factorial can be used at this type.

let fact (x:nat) : pos = factorial x

Actually, in all the code we’ve seen so far, what’s happening under the covers is that F* infers a type for a pure program similar to Pure t pre post and then checks that that type can be subsumed to a user-provided specification of the form Tot t'.

In this chapter, we look into how these Pure specifications work, starting with a primer on Floyd-Hoare Logic and weakest precondition calculi. If the reader is familiar with these, they may safely skip the next subsections, though even if you are an expert, if may be of interest to see how such program logics can be formalized in F*.

A Primer on Floyd-Hoare Logic and Weakest Preconditions

Floyd-Hoare Logic is a system of specifications and rules to reason about the logical properties of programs, introduced by Robert Floyd in a paper titled Assigning Meaning to Programs and by Tony Hoare in An axiomatic basis for computer programming. The notation used in most modern presentations (called Hoare triples) is due to Hoare. An algorithm to compute Hoare triples was developed by Edsger Dijkstra presented first in this paper , using a technique called weakest preconditions. All of them received Turing Awards for their work on these and other related topics.

For an introduction to these ideas, we’ll develop a small imperative language with global variables, presenting

An operational semantics for the language, formalized as an interpreter.
A Floyd-Hoare program logic proven sound with respect to the operational semantics.
And, finally, an algorithm to compute weakest preconditions proved sound against the Floyd-Hoare logic.

Our language has the following abstract syntax:

let var = nat

type expr =
  | EConst : int -> expr                           // constants: ..., -1, 0, 1, ...
  | EVar   : var -> expr                           // global variables
  | EAdd   : expr -> expr -> expr                  // arithmetic: e1 + e2
  
type program = 
  | Assign : var -> expr -> program                // x := e
  | Seq    : program -> program -> program         // p1; p2
  | If     : expr -> program -> program -> program // if e then p1 else p2
  | Repeat : expr -> program -> program            // repeat n { p }

Expressions includes integer constants, global variables (represented just as natural numbers), and some other forms, e.g., arithmetic expressions like addition.

A program includes:

Assignments, EAssign x e, representing the assignment of the result of an expression e to a global variable x, i.e., x := e
Seq, to compose programs sequentially
If to compose programs conditionally
And Repeat n p, which represents a construct similar to a for-loop (or primitive recursion), where the program p is repeated n times, where n evaluates to a non-negative integer.

Our language does not have while loops, whose semantics are a bit more subtle to develop. We will look at a semantics for while in a subsequent chapter.

Operational Semantics

Our first step in giving a semantics to programs is to define an interpreter for it to run a program while transforming a memory that stores the values of the global variables.

To model this memory, we use the type state shown below:

// The state of a program is a map from global variable to integers
let state = var -> int
let read (s:state) (i:var) : int = s i
let write (s:state) (i:var) (v:int)
  : state
  = fun j -> if i=j then v else read s j

Writing a small evaluator for expressions is easy:

let rec eval_expr (e:expr) (s:state)
  : int
  = match e with
    | EConst v ->
      v
      
    | EVar x ->
      read s x
      
    | EAdd e1 e2 ->
      eval_expr e1 s + eval_expr e2 s

The interpreter for programs itself takes a bit more work, since programs can both read and write the state. To structure our interpreter, we’ll introduce a simple state monad st a. We’ve seen this construction before in a previous chapter—so, look there if the state monad is unfamiliar to you. Recall that F* has support for monadic let operators: the let! provides syntactic sugar to convenient compose st terms.

let st (a:Type) = state -> (a & state)

let get : st state = fun s -> (s, s)

let put (s:state) : st unit = fun _ -> ((), s)

let (let!) #a #b (f:st a) (g: a -> st b) : st b = 
  fun s -> let v, s' = f s in g v s'

let return #a (x:a) : st a = fun s -> (x, s)

Now, the interpreter itself is a total, recursive function run which interprets a program p as a state-passing function of type st unit, or state -> unit & state.

let rec run (p:program)
  : Tot (st unit)
        (decreases %[p;0])
  = match p with
    | Assign x e -> 
      let! s = get in
      let v = eval_expr e s in
      put (write s x v)

    | Seq p1 p2 -> 
      run p1;!
      run p2

    | If e p1 p2 ->
      let! s = get in
      let n = eval_expr e s in
      if n <> 0 then run p1 else run p2
      
    | Repeat e p ->
      let! s = get in
      let n = eval_expr e s in
      if n <= 0 then return ()
      else run_repeat p n

and run_repeat (p:program) (n:nat)
  : Tot (st unit)
        (decreases %[p; 1; n])
  = if n = 0 then return ()
    else ( run p ;! run_repeat p (n - 1) )

Let’s look at its definition in detail:

Assign x e: Evaluate e in the current state and then update the state with a new value of x.

Seq p1 p2: Simply run p1 and then run p2, where ;! is syntactic sugar for let! _ = run p1 in run p2.

If e p1 p2: Evaluate e in the current state, branch on its result and run either p1 or p2

Repeat e p: Evaluate e to n, and if n is greater than zero, call the mutually recursive run_repeat n p. Most of the subtlety here is in convincing F* that this mutually recursive function terminates, but this is fairly straightforward once you know how—we discussed termination proofs for mutually recursive functions earlier.

These operational semantics are the ground truth for our programming language—it defines how programs execute. Now that we have that settled, we can look at how a Floyd-Hoare logic makes it possible to reason about programs in a structured way.

Floyd-Hoare Logic

The goal of a Floyd-Hoare logic is to provide a way to reason about a program based on the structure of its syntax, rather than reasoning directly about its operational semantics. The unit of reasoning is called a Hoare triple, a predicate of the form {P} c {Q}, where P and Q are predicates about the state of the program, and c is the program itself.

We can define Hoare triples for our language by interpreting them as an assertion about the operational semantics, where triple p c q represents, formally, the Hoare triple { p } c { q }.

let triple (pre:state -> prop)
           (c:program)
           (post:state -> prop)
  = forall s0. pre s0 ==> post (snd (run c s0))

The predicate triple p c q is valid, if when executing c in a state that satisfies p results in a state that satisfies q. The predicates p and q are also called precondition and postcondition of c, respectively.

For each syntactic construct of our language, we can prove a lemma that shows how to build an instance of the triple predicate for that construct. Then, to build a proof of program, one stitches together these lemmas to obtain a triple p main q, a statement of correctess of the main program.

Assignment

Our first rule is for reasoning about variable assignment:

let assignment (x:var) (e:expr) (post:state -> prop)
  : Lemma (triple (fun s0 -> post (write s0 x (eval_expr e s0)))
                  (Assign x e)
                  post)
  = ()

This lemma says that post holds after executing x := e in the initial state s0, if post holds on the initial state updated at x with the value of e.

For example, to prove that after executing z := y + 1 in s0, if we expect the value of z to be greater than zero`, then the assignment rule says that read s0 y + 1 > 0 should hold before the assignment, which is what we would expect.

Sequence

Our next lemma about triples stitches together triples for two programs that are sequentially composed:

let sequence (p1 p2:program)
             (pre pre_mid post:state -> prop)
  : Lemma 
    (requires 
      triple pre p1 pre_mid /\
      triple pre_mid p2 post)
    (ensures
      triple pre (Seq p1 p2) post)
  = ()

The lemma says that if we can derive the Hoare triples of the two statements such that postcondition of p1 matches the precondition of p2, then we can compose them.

Conditional

The lemma for conditionals is next:

let conditional (e:expr)
                (p1 p2:program)
                (pre post:state -> prop)
  : Lemma 
    (requires 
      triple (fun s -> pre s /\ eval_expr e s =!= 0) p1 post /\
      triple (fun s -> pre s /\ eval_expr e s == 0)  p2 post)
    (ensures
      triple pre (If e p1 p2) post)
  = ()

It says that to derive the postcondition post from the If e p1 p2, we should be able to derive it from each of the branches with the same precondition pre. In addition, since we know that p1 executes only when e is non-zero, we can add these facts to the preconditions of each branch.

Repeat

In all the cases so far, these lemmas are proved automated by F* and Z3. In the case of repeats, however, we need to do a little more work, since an inductive argument is involved.

The rule for repeat requires a loop invariant inv. The loop invariant is an assertion that holds before the loop starts, is maintained by each iteration of the loop, and is provided as the postcondition of the loop.

The lemma below states that if we can prove that triple inv p inv, then we can also prove triple inv (Repeat e p) inv.

// We need an auxilary lemma to prove it by induction for repeat_n
let rec repeat_n (p:program) (inv:state -> prop) (n:nat)
  : Lemma
    (requires triple inv p inv)
    (ensures (forall s0. inv s0 ==> inv (snd (run_repeat p n s0))))
 = if n = 0 then ()
   else repeat_n p inv (n - 1)

// Then, we use that auxiliary lemma to prove the main
// rule for reasoning about repeat using an invariant
let repeat (e:expr) (p:program) (inv:state -> prop)
  : Lemma
    (requires triple inv p inv)
    (ensures triple inv (Repeat e p) inv)
  = introduce forall s0. inv s0 ==> inv (snd (run (Repeat e p) s0)) with
    introduce _ ==> _  with
      inv_s0 . (
        let n = eval_expr e s0 in
        if n <= 0 then ()
        else repeat_n p inv n
    )

The auxiliary lemma repeat_n proves that run_repeat p n preserves inv, if p preserves inv.

To call this lemma from the main repeat lemma, we need to “get our hands on” the initial state s0, and the syntactic sugar to manipulate logical connectives makes this possible.

Consequence

The final lemma about our Hoare triples is called the rule of consequence. It allows strengthening the precondition and weakening the postcondition of a triple.

let consequence (p:program) (pre pre' post post':state -> prop)
  : Lemma
    (requires 
      triple pre p post /\
      (forall s. pre' s ==> pre s) /\
      (forall s. post s ==> post' s))
    (ensures
      triple pre' p post')
  = ()

A precondition of a program is an obligation before the statement is executed. So if p requires pre, we can always strengthen the precondition to pre', provided pre' ==> pre, i.e. it is logically valid to require more than necessary in the precondition. Similarly, postcondition is what a statement guarantees. So if p guarantees post, we can always weaken it to guarantee less, i.e. some post' where post ==> post'.

Weakest Preconditions

The rules of Floyd-Hoare logic provide an abstract way to reason about programs. However, the rules of the logic are presented declaratively. For example, to apply the sequence rule, one has derive triples for each component in a way that they prove exactly the same assertion (pre_mid) about the intermediate state. There may be many ways to do this, e.g., one could apply the rule of consequence to weaken the postcondition of the first component, or to strengthen the precondition of the second component.

Dijkstra’s system of weakest preconditions eliminates such ambiguity and provides an algorithm for computing valid Hoare triples, provided the invariants of all loops are given. This makes weakest preconditions the basis of many program proof tools, since given a program annotated with loop invariants, one can simply compute a logical formula (called a verification condition) whose validity implies the correctness of the program.

At the core of the approach is a function WP (c, Q), which computes a unique, weakest precondition P for the program c and postcondition Q. The semantics of WP is that WP (c, Q) is the weakest precondition that should hold before executing c for the postcondition Q to be valid after executing c. Thus, the function WP assigns meaning to programs as a transformer of postconditions Q to preconditions WP (s, Q).

The wp function for our small imperative language is shown below:

let rec wp (c:program) (post: state -> prop) 
  : state -> prop 
  = match c with
    | Assign x e -> 
      fun s0 -> post (write s0 x (eval_expr e s0))
      
    | Seq p1 p2 ->
      wp p1 (wp p2 post)

    | If e p1 p2 -> 
      fun s0 -> 
        (eval_expr e s0 =!= 0 ==> wp p1 post s0) /\
        (eval_expr e s0 == 0  ==> wp p2 post s0)
      
    | Repeat e p ->
      fun s0 ->
        (exists (inv:state -> prop). 
          inv s0 /\
          (forall s. inv s ==> post s) /\
          (forall s. inv s ==> wp p inv s))

The case of Assign is identical to the assignment lemma shown earlier.
The case of Seq sequentially composes the wp’s. That is, to prove the post after running p1 ;; p2 we need to prove wp p2 post after running p1. It may be helpful to read this case as the equivalent form fun s0 -> wp p1 (fun s1 -> wp p2 post s1) s0, where s0 is the initial state and s1 is the state that results after running just p1.
The If case computes the WPs for each branch and requires them to be proven under the suitable branch condition.
The Repeat case is most interesting: it involves an existentially quantified invariant inv, which is the loop invariant. That is, to reason about Repeat n p, one has to somehow find an invariant inv that is true initially, and implies both the WP of the loop body as well as the final postcondition.

The wp function is sound in the sense that it computes a sufficient precondition, as proven by the following lemma.

let rec wp_soundness (p:program) (post:state -> prop)
  : Lemma (triple (wp p post) p post)
  = match p with
    | Assign x e -> ()
    | Seq p1 p2 ->
      wp_soundness p2 post;
      wp_soundness p1 (wp p2 post)
    | If e p1 p2 ->
      wp_soundness p1 post;
      wp_soundness p2 post
    | Repeat e p ->
      introduce forall s0. wp (Repeat e p) post s0 ==> 
                      post (snd (run (Repeat e p) s0)) with
      introduce _ ==> _ with
        _ . ( 
          eliminate exists (inv:state -> prop).
                            inv s0 /\                      
                            (forall s. inv s ==> post s) /\
                            (forall s. inv s ==> wp p inv s)
          returns _
          with inv_props. (
            wp_soundness p inv;
            repeat e p inv
          )
      )

One could also prove that wp computes the weakest precondition, i.e., if triple p c q then forall s. p s ==> wp c q s, though we do not prove that formally here.

A Sample Program Proof

We now illustrate some sample proofs using our Hoare triples and wp function. To emphasize that Hoare triples provide an abstract way of reasoning about the execution of programs, we define the hoare p c q an alias for triple p c q marked with an attribute to ensure that F* and Z3 cannot reason directly about the underlying definition of triple—that would allow Z3 to find proofs by reasoning about the operational semantics directly, which we want to avoid , since it would not scale to larger programs. For more about the opaque_to_smt and reveal_opaque construct, please see this section on opaque definitions.

[@@"opaque_to_smt"]
let hoare p c q = triple p c q

let wp_hoare (p:program) (post:state -> prop)
  : squash (hoare (wp p post) p post)
  = reveal_opaque (`%hoare) hoare;
    wp_soundness p post

let hoare_consequence (#p:program)
                     (#pre #post:state -> prop)
                     (pre_annot:state -> prop)
                     (_: squash (hoare pre p post))
                     (_: squash (forall s. pre_annot s ==> pre s))
  : squash (hoare pre_annot p post)
  = reveal_opaque (`%hoare) hoare

The lemmas above are just restatements of the wp_soundness and consequence lemmas that we’ve already proven. Now, these are the only two lemmas we have to reason about the hoare p c q predicate.

Next, we define some notation to make it a bit more convenient to write programs in our small language.

let ( := ) (x:var) (y:expr) = Assign x y

let add (e1 e2:expr) = EAdd e1 e2

let c (i:int) : expr = EConst i

let v (x:var) : expr = EVar x

let rec prog (p:list program { Cons? p }) 
  : program 
  = match p with
    | [c] -> c
    | c::cs -> Seq c (prog cs)

let x = 0
let y = 1
let z = 2

Finally, we can build proofs of some simple, loop-free programs automatically by computing their wp using wp_hoare and applying hoare_consequence to get F* and Z3 to prove that the inferred WP is implied by the annotated precondition.

let swap = prog [ z := v x; x := v y; y := v z]
let proof_swap (lx ly:int)
  : squash (hoare (fun s -> read s x = lx /\ read s y = ly) swap
                  (fun s -> read s x = ly /\ read s y = lx))
  = hoare_consequence _ (wp_hoare swap _) ()

This recipe of computing verification conditions using WPs and then checking the computed WP against the annotated specification using a solver like Z3 is a very common and powerful pattern. In fact, as we’ll see below, the methodology that we’ve developed here for our small imperative language is exactly what the F* typechecker does (at a larger scale and for the whole F* language) when checking an F* program.

The `PURE` Effect: A Dijkstra Monad for Pure Computations

F* provides a weakest precondition calculus for reasoning about pure computations. The calculus is based on a Dijkstra Monad, a construction first introduced in this paper. In this chapter, we will learn about Dijkstra Monad and its usage in specifying and proving pure programs in F*.

The first main difference in adapting the Hoare triples and weakest precondition computations that we saw earlier to the setting of F*’s functional language is that there are no global variables or mutable state (we’ll see about how model mutable state in F*’s effect system later). Instead, each pure expression in F*’s returns a value and the postconditions that we will manipulate are predicates about these values, rather than state predicates.

To illustrate, we sketch the definition of pure WPs below.

WP c Q                      = Q c
WP (let x = e1 in e2) Q     = WP e1 (fun x -> WP e2 Q)
WP (if e then e1 else e2) Q = (e ==> WP e1 Q) /\ (~e ==> WP e2 Q)

The WP of a constant c is just the postcondition Q applied to c.
The WP of a let binding is a sequential composition of WPs, applied to the values returned by each sub-expression
The WP of a condition is the WP of each branch, weakened by the suitable branch condition, as before.

The F* type system internalizes and generalizes this WP construction to apply it to all F* terms. The form this takes is as a computation type in F*, PURE a wp, where in prims.fst, PURE is defined as an F* primitive effect with a signature as shown below–we’ll see much more of the new_effect syntax as we look at user-defined effects in subsequent chapters; for now, just see it as a reserved syntax in F* to introduce a computation type constructor.

new_effect PURE (a:Type) (w:wp a) { ... }

where

let pre = Type0
let post (a:Type) = a -> Type0
let wp (a:Type) = post a -> pre

A program e of type PURE a wp is a computation which

Is defined only when wp (fun _ -> True) is valid

If wp post is valid, then e terminates without any side effects and returns a value v:a satisfying post v.

Notice that wp a is the type of a function transforming postconditions (a -> Type0) to preconditions (Type0). [1] The wp argument is also called an index of the PURE effect. [2]

The return operator for wp a is shown below: it is analogous to the WP c Q and WP x Q rules for variables and constants that we showed earlier:

let return_wp (#a:Type) (x:a) : wp a = fun post -> post x

The bind operator for wp a is analogous to the rule for sequencing WPs, i.e., the rule for WP (let x = e1 in e2) Q above:

let bind_wp (#a #b:Type) (wp1:wp a) (wp2:a -> wp b)
  : wp b
  = fun post -> wp1 (fun x -> wp2 x post)                

Finally, analogous to the WP rule for conditionals, one can write a combinator for composing wp a in a branch:

let if_then_else_wp (#a:Type) (b:bool) (wp1 wp2:wp a)
  : wp a
  = fun post -> if b then wp1 post else wp2 post

This is the essence of the Dijkstra monad construction for pure programs: the rule for computing weakest preconditions for a computation returning a value x is return_wp; the rule for computing the WP of the sequential composition of terms is the sequential composition of WPs using bind_wp; the rule for computing the WP of a conditional term is the conditional composition of WPs using if_then_else_wp.

If fact, if one thinks of pure computations as the identity monad, tot a as shown below:

let tot (a:Type) = a
let return_tot (#a:Type) (x:a) : tot a = x
let bind_tot (#a #b:Type) (x:tot a) (y:a -> tot b)
  : tot b
  = let v = x in y v

then the parallel between the tot monad and wp becomes even clearer—the WP analog of return_tot is return_wp and of bind_tot is bind_wp.

It turns out that wp a (for monotonic weakest preconditions) is itself a monad, as shown below by a proof of the monad laws:

(* A monotonic WP maps stronger postconditions to stronger preconditions *)
let monotonic (#a:Type) (wp:wp a) =
  forall (p q:post a). (forall x. p x ==> q x) ==> (wp p ==> wp q)

let mwp (a:Type) = w:wp a { monotonic w }

(* An equivalence relation on WPs *)
let ( =~= ) (#a:Type) (wp1 wp2:wp a)
  : prop
  = forall post. wp1 post <==> wp2 post

(* The three monad laws *)
let left_identity (a b:Type) (x:a) (wp:a -> mwp a)
  : Lemma (bind_wp (return_wp x) wp =~= wp x)
  = ()

let right_identity (a b:Type) (wp:mwp a)
  : Lemma (wp =~= (bind_wp wp return_wp))
  = ()

let associativity (a b c:Type) (wp1:mwp a) (wp2:a -> mwp b) (wp3:b -> mwp c)
  : Lemma (bind_wp wp1 (fun x -> bind_wp (wp2 x) wp3) =~=
           bind_wp (bind_wp wp1 wp2) wp3)
  = ()

`PURE` and `Tot`

When typechecking a program, F* computes a weakest precondition which characterizes a necessary condition for the program to satisfy all its typing constraints. This computed weakest precondition is usually hidden from the programmer, but if you annotate your program suitably, you can get access to it, as shown in the code snippet below:

let square (n:int) 
  : PURE nat (as_pure_wp #nat (fun q -> n*n >= 0 /\ q (n * n)))
  = n * n

The type says that square n is a pure function, which for any postcondition q:nat -> prop,

Is defined only when n * n >= 0 and when q (n * n) is valid

And returns a value m:nat satisfying q m

Let’s look at another example:

let maybe_incr (b:bool) (x:int)
  : PURE int (as_pure_wp (if_then_else_wp b
                                        (bind_wp (return_wp (x + 1)) (fun y -> return_wp y))
                                        (return_wp x)))
  = if b
    then let y = x + 1 in y
    else x

Notice how the wp index of PURE mirrors the structure of the computation itself—it starts with an if_then_else_wp, then in the first branch, uses a bind_wp followed by a return; and in the else branch it returns x.

As such, the wp-index simply “lifts” the computation into a specification in a form amenable to logical reasoning, e.g., using the SMT solver. For pure programs this may seem like overkill, since the pure term itself can be reasoned about directly, but when the term contains non-trivial typing constraints, e.g., such as those that arise from refinement type checking, lifting the entire program into a single constraint structures and simplifies logical reasoning.

Of course, one often writes specifications that are more abstract than the full logical lifting of the program, as in the example below, which says that to prove post of the return value, the precondition is to prove post on all y >= x. This is a valid, although weaker, characterization of the function’s return value.

let maybe_incr2 (b:bool) (x:int)
  : PURE int (as_pure_wp (fun post -> forall (y:int). y >= x ==> post y))
  = if b
    then let y = x + 1 in y
    else x

The PURE computation type comes with a built-in weakening rule. In particular, if a term is computed to have type PURE a wp_a and it is annotated to have type PURE b wp_b, then F* does the following:

It computes a constraint p : a -> Type0, which is sufficient to prove that a is a subtype of b, e.g., is a = int and b = nat, the constraint p is fun (x:int) -> x >= 0.
Next, it strengthens wp_a to assert that the returned value validates the subtyping constraints p x, i.e., it builds assert_wp wp_a p, where
let assert_wp (#a:Type) (w:wp a) (p: a -> Type0) 
  : wp (x:a{ p x })
  = fun post -> w (fun (x:a) -> p x /\ post x)
Finally, it produces the verification condition stronger_wp #b wp_b (assert_wp wp_a p), where stronger_wp is defined as shown below:
let stronger_wp (#a:Type) (wp1 wp2:wp a) : prop =
   forall post. wp1 post ==> wp2 post
That is, for any postcondition post, the precondition wp_b post implies the original precondition wp_a post as well as the subtyping constraint p x. This matches the intuition about preconditions that we built earlier: it is always sound to require more in the precondition.

Thus, when we have e:PURE a wp in F*, the wp is a predicate transformer for e, not necessarily the weakest one.

Of course, even maybe_incr2 is not particularly idiomatic in F*. One would usually annotate a program with a refinement type, such as the one below:

let maybe_incr_tot (b:bool) (x:int)
  : Tot (y:int { y >= x })
  = if b
    then let y = x + 1 in y
    else x

Internally to the compiler, F* treats Tot t as the following instance of PURE:

Tot t = PURE t (fun post -> forall (x:t). post x)

Once Tot t is viewed as just an instance of PURE, checking if a user annotation Tot t is stronger than the inferred specification of a term PURE a wp is just as explained before.

`Pure`: Hoare Triples for `PURE`

Although specification are easier to compute using WPs, they are more natural to read and write when presented as Hoare triples, with a clear separation between precondition and postconditions. Further, when specifications written as Hoare triples naturally induce monotonic WPs.

F* provides an effect abbreviation called Pure for writing and typechecking Hoare-style specifications for pure programs, and is defined as shown below in prims.fst:

effect Pure (a:Type) (req:Type0) (ens:a -> Type0) =
       PURE a (fun post -> req /\ (forall x. ens x ==> post x))

The signature of Pure is Pure a req ens, where req is the precondition and ens:a -> Type0 is the postcondition. Using Pure, we can write the factorial function we saw at the top of this chapter—F* infers a PURE a wp type for it, and relates it to the annotated Pure int req ens type, proving that the latter has a stronger precondition and weaker postcondition.

One may wonder when one should write specifications using the notation x:a -> Pure b req ens versus x:a{req} -> Tot (y:b { ens y }). The two styles are closely related and choosing between them is mostly a matter of taste. As you have seen, until this point in the book, we have not used Pure a req ens at all. However, when a function has many pre and postconditions, it is sometimes more convenient to use the Pure a req ens notation, rather than stuffing all the constraints in refinement types.

`GHOST` and `DIV`

Just as PURE is an wp-indexed refinement of Tot, F* provides two more primitive wp-indexed effects:

GHOST (a:Type) (w:wp a) is a refinement of GTot a

DIV (a:Type) (w:wp a) is a refinement of Dv a

That is, F* uses the GHOST effect to infer total correctness WPs for ghost computations, where, internally, GTot a is equivalent to GHOST a (fun post -> forall x. post x)

Likewise, F* uses the DIV effect to infer partial correctness WPs for potentially non-terminating computations, where, internally, Dv a is equivalent to DIV a (fun post -> forall x. post x).

As with Tot and PURE, F* automatically relates GTot and GHOST computations, and Dv and DIV computations. Further, the effect ordering Tot < Dv and Tot < GTot extends to PURE < DIV and PURE < GHOST as well.

The prims.fst library also provides Hoare-triple style abbreviations for GHOST and DIV, i.e.,

effect Ghost a req ens = GHOST a (fun post -> req /\ (forall x. ens x /\ post x))
effect Div a req ens = DIV a (fun post -> req /\ (forall x. ens x /\ post x))

These Hoare-style abbreviations are more convenient to use than their more primitive WP-based counterparts.

The tradeoffs of using Ghost vs. GTot or Div vs. Dv are similar to those for Pure vs Tot—it’s mostly a matter of taste. In fact, there are relatively few occurrences of Pure, Ghost, and Div in most F* codebases. However, there is one important exception: Lemma.

The `Lemma` abbreviation

We can finally unveil the definition of the Lemma syntax, which we introduced as a syntactic shorthand in an early chapter. In fact, Lemma is defined in prims.fst as follows:

effect Lemma (a: eqtype_u)
             (pre: Type)
             (post: (squash pre -> Type))
             (smt_pats: list pattern) =
       Pure a pre (fun r -> post ())

That is, Lemma is an instance of the Hoare-style refinement of pure computations Pure a req ens. So, when you write a proof term and annotate it as e : Lemma (requires pre) (ensures post), F* infers a specification for e : PURE a wp, and then, as with all PURE computations, F* tries to check that the annotated Lemma specification has a stronger WP-specification than the computed weakest precondition.

Of course, F* still includes syntactic sugar for Lemma, e.g., Lemma (requires pre) (ensures post) is desugared to Lemma unit pre (fun _ -> post) []. The last argument of a lemma, the smt_pats are used to introduce lemmas to the SMT solver for proof automation—a later chapter covers that in detail.

Finally, notice the type of the post, which assumes squash pre as an argument–this is what allows the ensures clause of a Lemma to assume that what was specified in the `requires clause.