Layered DSLs for Stateful Programming

Overview

The goal of this effort is to derive certified low-level F★ code, in particular code written in the Low★ subset of F★, from high-level purely functional code.

The effectful low-level programs operate on the F★'s model of C memory. The high-level program operates on an "abstract", purely-functional view of the low-level memory, which is more amenable to formal verification. We can transfer between the two representations of the state using a lens following ideas from biderectional programming.

High Level

At the high-level end we have functional programs written in a monadic style, that operate on a specific state representation. Right now the high level state is a pair of machine integers (type state = mint * mint) but we intent to generalize it.

High-level computations are programs written in the state monad, indexed by a wp:

type comp_wp 'a (wp : hwp_mon 'a) = s0:state -> PURE ('a * state) (wp s0)

As with the high-level state. we provide a set of low-level combinators.

We provide a set of high-level combinators and we also define the High effect to facilitate coding in the high-level DSL.

return_elab (#a:Type) (x : a) : comp_wp a (return_wp x)
bind_elab #a #b #f_w ($f:comp_wp a f_w) #g_w ($g:(x:a) -> comp_wp b (g_w x)) : Tot (comp_wp b (bind_wp f_w g_w))
hread_elab (i:nat) : comp_wp mint (read_wp i)
hwrite_elab (i:nat) (v:mint) : comp_wp unit (write_wp i v)
ite_elab (#a:Type) (b : bool) (#wp1 : hwp_mon a) (c1:comp_wp a wp1) (#wp2 : hwp_mon a) (c2:comp_wp a wp2) : comp_wp a (ite_wp b wp1 wp2)
for_elab' (inv : state -> int -> Type) (f : (i:int) -> comp_p unit (requires (fun h0 -> inv h0 i))
                                                                   (ensures (fun h0 _ h1 -> inv h1 (i + 1)))) 
          (lo : int) (hi : int{lo <= hi}) :
          (comp_p unit (requires (fun h0 -> inv h0 lo)) (ensures (fun h0 _ h1 -> inv h1 hi)))

Low Level

At the low-level end we have computations written in the Stack effect. The low-level state is the part of memory that corresponds to the high-level view (type lstate = pointer mint * pointer mint). Low-level computations are indexed by a high-level computation (and its WP) and their type ensures that they refine the high-level program.

More specifically, the high-level and low-level state define a lens with the following transformation functions (for which we prove the lens laws):

val lstate_as_state : HS.mem -> lstate -> GTot state

val state_as_lstate : h:HS.mem -> ls:lstate{well_formed h ls} -> state -> GTot (h':HS.mem{well_formed h' ls})

The type of low-level computations can then be defined as follows:

let lcomp_wp (a:Type) (wp : hwp_mon a) (c : comp_wp a wp) =
  ls:lstate ->
  Stack a
     (requires (fun h -> well_formed h ls /\ (let s0 = lstate_as_state h ls in wp s0 (fun _ -> True))))
     (ensures  (fun h r h' ->
                  well_formed h' ls /\
                  (let s0 = lstate_as_state h ls in
                   let (x, s1) = c s0 in
                   h' == state_as_lstate h ls s1 /\ x == r )))

That is, running the low-level computation on the low state is the same as running the high computation in the high-level view of the low state and then applying the resulting view to the low-level state.

Again, we provide a set of combinators.

lreturn (#a:Type) (x:a) : lcomp_wp a (return_wp x) (return_elab x)
lbind (#a:Type) (#b:Type)(#wp1: hwp_mon a) (#fwp2 : (a -> hwp_mon b))
  (#c1:comp_wp a wp1) (#c2:(x:a -> comp_wp b (fwp2 x)))
  (m: lcomp_wp a wp1 c1) (f: (x:a) -> lcomp_wp b (fwp2 x) (c2 x)) :
  lcomp_wp b (bind_wp wp1 fwp2) (bind_elab c1 c2)
lwrite : i:nat{ i < 2 } -> v:mint -> lcomp_wp unit (write_wp i v) (hwrite_elab i v)
lread : i:nat{ i < 2 } -> lcomp_wp mint (read_wp i) (hread_elab i)
lfor' : (inv : state -> int -> Type0) (fh : (i:int) -> comp_p unit  (fun h0 -> inv h0 i) (fun h0 _ h1 -> inv h1 (i + 1)))
              (f : (i:int) -> lcomp unit (fun h0 -> inv h0 i) (fun h0 _ h1 -> inv h1 (i + 1)) (fh i)) 
              (lo : int) (hi : int{lo <= hi}) :
         lcomp unit (requires (fun h0 -> inv h0 lo))
                    (ensures (fun h0 _ h1 -> inv h1 hi))
                    (for_elab' inv fh lo hi)) (decreases (hi - lo))

From High to Low

Eventually, given a high-level computation, we want to obtain an efficient low-level computation that refines it. Every high-level computation gives rise to a trivial, low-level computation, by transforming the initial low state to its high-level view, running the high computation, and applying the resulting view to the initial low-level state. This low-level computation has the expected observable behavior, but it's not expressed with the low level DSL, does not uses efficient Stack updates and accesses, and it's not written in the Low★ fragment, meaning that it does not enjoy a translation to C.

let morph (#a:Type) (wp:hwp_mon a) (c:comp_wp a wp) : lcomp_wp a wp c =
    fun (b1, b2) ->
      let s1 = b1.(0ul) in
      let s2 = b2.(0ul) in
      let (x, (s1', s2')) = run_high c (s1, s2) in
      b1.(0ul) <- s1';
      b2.(0ul) <- s2';
      x

Typing Inversion Axioms

Meetings

TODOs

• Generalize the state
• Tactic rewriting

Related Work

possibly related work includes:

• qhasm
• jasmin
• cryptol