Primitive Effect Refinements

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.

// 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

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

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)

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 triple (pre:state -> prop)
           (c:program)
           (post:state -> prop)
  = forall s0. pre s0 ==> post (snd (run c s0))

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)
  = ()

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)
  = ()

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)
  = ()

// 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
    )

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')
  = ()

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))

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
          )
      )

[@@"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

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

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 _) ()

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)
  = ()

1

It is also possible to define post a = a -> prop and pre = prop. However, the F* libraries for pure WPs using Type0 instead of prop, so we remain faithful to that here.

2

Dijkstra monads are also related to the continuation monad. Continuation monad models Continuation Passing Style programming, where the control is passed to the callee explicitly in the form of a continuation. For a result type r, the continuation monad is defined as follows:

let cont (r:Type) (a:Type) = (a -> r) -> r  // (a -> r) is the continuation
let return #r (#a:Type) (x:a) : cont r a = fun k -> k x
let bind #r (#a #b:Type) (f:cont r a) (g:a -> cont r b)
  : cont r b
  =  fun k -> f (fun x -> g x k)

If we squint a bit, we can see that the wp monad we defined earlier, is nothing but a continuation into Type0, i.e., wp a = cont Type0 a (or cont prop a, if one prefers to use prop).

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:

1. 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.

2. 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)
   

3. 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.

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

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.