# Effectful Verification with the Dijkstra monad

#### Cătălin Hriţcu (Inria Paris)

Type Systems for Security Verification Lecture

Saarland University

Thursday, 19 March 2015

## Swap

  wlp (Z:=X; X:=Y; Y:=Z) (X=y /\ Y=x)= wlp (Z:=X; X:=Y)       (X=y /\ Z=x)= wlp (Z:=X)             (Y=y /\ Z=x)=                        (Y=y /\ X=x)

## Max

  wlp (if X < Y then Z:=Y else Z:=X) ((Z=X \/ Z=Y) /\ Z>=X /\ Z>=Y)= if (X<Y) then wlp (Z:=Y) ((Z=X \/ Z=Y) /\ Z>=X /\ Z>=Y)           else wlp (Z:=X) ((Z=X \/ Z=Y) /\ Z>=X /\ Z>=Y) = if (X<Y) then ((Y=X \/ Y=Y) /\ Y>=X /\ Y>=Y)           else ((X=X \/ X=Y) /\ X>=X /\ X>=Y)

## Reduce to Zero

wlp (WHILE X â‰  0 DO X ::= X - 1 END) (X = 0)= if X != 0 then wlp (X ::= X - 1) True else (X = 0)= wlp (X ::= X - 1) True= True

## Finding Square Roots

      { X=m }  â‡¾      { X=m âˆ§ 0Ã—0 â‰¤ m }    Z ::= 0;      { X=m âˆ§ ZÃ—Z â‰¤ m }    while (Z+1)*(Z+1) â‰¤ X do        { X=m âˆ§ ZÃ—Zâ‰¤m âˆ§ (Z+1)*(Z+1)â‰¤X }  â‡¾        { X=m âˆ§ (Z+1)*(Z+1)â‰¤m }      Z ::= Z+1        { X=m âˆ§ ZÃ—Zâ‰¤m }    end      { X=m âˆ§ ZÃ—Zâ‰¤m âˆ§ X<(Z+1)*(Z+1) }  â‡¾      { ZÃ—Zâ‰¤m âˆ§ m<(Z+1)*(Z+1) }

Homework - 1p

## Wrap up: we want both!

• Hoare logic
• great for specification and manual verification
• exploits human intuition, but does not scale
• Weakest precondition (aka. predicate transformers)
• great for scaling up to interesting code
• exploits computation and automatic theorem proving (SMT)
• lots of tools based on this: Dafny, Boogie, Frama-C, Spec#, VCC, Why3
• all of them for imperative programming languages

## Why is this hard?

### Why are effectful functional programs trickier to verify than programs in While or C?

• expressions can both perform side-effects and return results
• higher-order functions
• higher-order state (functions in the heap)
• effects often interact badly with fancy types:
• polymorphism (ML value restrictions story)
• dependent types, abstract types, etc.

• weakest preconditions for effectful functional programs
• generic algorithm that works for all effects of F* (integrated with typing)
• works well with higher-order features and fancy types
• intuitive Hoare-like specs (Pure, Div, Exn, St, All)
• automation that scales well in practice
• produces simple, first-order VCs that work well with SMT

## Lattice of effects

• Customizable; the default one:
• M ::= PURE | DIV | EXN | STATE | ALL
• M parameterized by type and predicate transformer (M t wp)
• shape of the wp depends on the effect: PURE simple, ALL complex
• type of wp depends on t: M.WP t = M.Post -> M.Pre

## Desugaring what we know and love

Pure  a (requires pre) (ensures post) =PURE  a (fun p -> pre /\ forall x. post x ==> p x)Exn   a (requires pre) (ensures post) =EXN   a (fun p -> pre /\ forall x. post x ==> p x)St    a (requires pre) (ensures post) =STATE a (fun p h0 -> pre h0 /\ forall x h1. post h0 x h1 ==> p x h1)All   a (requires pre) (ensures post) =ALL   a (fun p h0 -> pre h0 /\ forall x h1. post h0 x h1 ==> p x h1)

## PURE

• (e : PURE t wp) if forall (p:PURE.Post) for which (wp p) holds we have that e evaluates (v:t) for which (p v) holds
PURE.Pre = TypePURE.Post (a:Type) = a -> TypePURE.WP (a:Type) = Post a -> Pre
• For example:
val factorial: x:int -> Pure int (requires (x >= 0)) (ensures (fun y -> y>=1))
val factorial: x:int -> PURE int (fun p -> x>=0 /\ forall y. y>=1 ==> p y)
• this reads as follows: forall p:PURE.Post int for which (x >= 0 /\forall y. y>=1 ==> p y) holds we have that (factorial x) evaluates to a value (v:int) for which (p v) holds

## STATE

• (STATE t wp) is the type of a computation which, when run in heap h0 for which (wp p h0) is valid (for any p : STATE.Post), may read or write the state, and diverges or returns a value (v:t) in heap h1 satisfying (p v h1).

• The STATE effect

kind Pre = heap -> Typekind Post (a:Type) = a -> heap -> Typekind WP   (a:Type) = Post a -> Pre

type return (a:Type) (x:a) : PURE.WP a = fun p -> p xtype bind (a:Type) (wp1:PURE.WP a) (wp2:a->PURE.WP b) : PURE.WP b =    fun p -> wp1 (fun x -> wp2 x p)
• Note: effects are primitive, monads only at specification level

• STATE (looks the same because of partial application)
type return (a:Type) (x:a) : STATE.WP a = fun p -> p xtype bind (a:Type) (wp1:STATE.WP a) (wp2:a->STATE.WP b) : STATE.WP b =  fun p -> wp1 (fun x -> wp2 x p)
• without partial application:
type return (a:Type) (x:a) : STATE.WP a = fun p h -> p x htype bind (a:Type) (wp1:STATE.WP a) (wp2:a->STATE.WP b) : STATE.WP b =  fun p h -> wp1 (fun x h' -> wp2 x p h') h

## Specifying effectful primitives

• Using predicate transformers

assume val read: r:ref int -> STATE int (fun p h -> p (sel h r) h)assume val write: r:ref int -> v:int -> STATE unit (fun p h -> p () (upd h r v))
• or Hoare triples

assume val read: r:ref int -> St int (requires (fun h -> True))                                   (ensures (fun h x h' -> h=h' /\ x=sel h r))assume val write: r:ref int -> v:int -> St unit (requires (fun h -> True)                                        (ensures (fun h x h' -> h'=upd h r v))

## Swap in detail

val swap : #a:Type -> r1:ref a -> r2:ref a -> St unit      (requires (fun h' -> contains h' r1 /\ contains h' r2))      (ensures (fun h' _ h ->                  let x1 = sel h' r1 in                  let x2 = sel h' r2 in                  equal h (upd (upd h' r1 x2) r2 x1)))let swap r1 r2 =  let tmp = read r1 in  let _   = write r1 (read r2) in  write r2 tmp

## Other possible simple examples

• factorial (pure)
val factorial n = if n <= 1 then 1 else n * (factorial (n-1))
• increment (assignment)
let incr r = r := !r + 1
• max (if-then-else)
if !r1 < !r2 then r := !r2 else r := !r1
• twice (higher-order)
val twice: a b wp f:(x:a -> STATE b (wp x)) -> y:a       -> STATE b (fun p. wp y (fun x. wp y p))let twice f x = f (f x)

## Typing rule for if-then-else

M.ite : #a:Type -> M.WP(int) -> M.WP(a) -> M.WP(a) -> M.WP(a)M.ite a wp0 wp1 wp2 = M.bind wp0 (fun b -> (M.up      b  ==>_M wp1) /\_M                                           (M.up (not b) ==>_M wp2))PURE.up  a t p   = tSTATE.up a t p h = t

## Lifting / sub-effecting

• Sub-effects: Lifting PURE to STATE
 type lift : a:Type -> PURE.WP a -> STATE.WP a =   fun (a:Type) (wp:PURE.WP a) (p:STATE.Post a) (h:heap) -> wp (fun x -> p x h)

## References

Semantic Purity and Effects Reunited in F* (Draft, March 2015)

There's lots of interesting things I didn't cover

## Homework

• Square roots wlp - 1p
• Stateful ACLs (sections 1 and 8.1 in tutorial, ex 8a) - 1p
• Pure insertion sorting for ints - 2p
• Pure insertion sorting for anything - 2p
• Optional: pure merge sort - 2p