# 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
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 conditionallyAnd

`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-expressionThe 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 validIf

`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 validAnd 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`

, wherelet 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 postThat 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.