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)

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

Typing Inversion Axioms

Meetings

TODOs

• Generalize the state
• Tactic rewriting

Related Work

possibly related work includes:

• qhasm
• jasmin
• cryptol