-
Notifications
You must be signed in to change notification settings - Fork 232
Layered DSLs for Stateful Programming
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.
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)))
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))
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
We say that two low programs are when their wp's are precise, meaning that the fully characterize the result of the computation, and equi-satisfiable:
let lwp_eq #a (wp1:lwp a) (wp2:lwp a) =
precise wp1 /\
precise wp2 /\
(forall ls h0 post. wp1 ls h0 post <==> wp2 ls h0 post)
let l_eq #a (#wp1:hwp_mon a) (#c1:comp_wp a wp1) (lc1: lcomp_wp a wp1 c1)
(#wp2:hwp_mon a) (#c2:comp_wp a wp2) (lc2 : lcomp_wp a wp2 c2) =
lwp_eq (as_lwp c1) (as_lwp c2)
Where as_lwp is a coercion from high wp's to low wp's.
We add the following axiom (TODO revise to ensure consistency).
assume val l_eq_axiom : (#a:Type) -> (#wp1:hwp_mon a) -> (#c1:comp_wp a wp1) -> (lc1: lcomp_wp a wp1 c1) ->
(#wp2:hwp_mon a) -> (#c2:comp_wp a wp2) -> (lc2 : lcomp_wp a wp2 c2) ->
Lemma (requires (l_eq lc1 lc2)) (ensures (lc1 === lc2))
(from Nik's post on Oct 16th.)
Our intention is to provide rewrite lemmas of the following form for each pair of corresponding high/low combinators.
morph (return_wp x) (return_elab x) == lreturn x
We could use such lemmas to rewrite the low-level program morph c to the desired efficient low-level program. However, it turns out that this form of equalities does not quite work as the require the inferred wp for the high-level computation to exactly match the first argument of morph, which may not always be the case.
To circumvent that, we state the rewrite lemmas as follows.
let morph_return #a (wp : hwp_mon a) (c : comp_wp a wp) (x : a) :
Lemma
(requires (c === return_elab x))
(ensures (return_inv c x;
morph wp c == lreturn x))
let morph_bind #a #b (wp1 : hwp_mon a) (c1 : comp_wp a wp1)
(wp2 : a -> hwp_mon b) (c2 : (x:a) -> comp_wp b (wp2 x))
(wp : hwp_mon b) (c : comp_wp b wp) :
Lemma (requires (c === bind_elab c1 c2))
(ensures (morph wp c == lbind (morph wp1 c1) (fun x -> (morph (wp2 x) (c2 x))))) =
For the above rules to typecheck we need to know that the type of morph wp c is the same with the one of lbind (morph wp1 c1) (fun x -> (morph (wp2 x) (c2 x))). This need not be true in general, however we know that c === bind_elab c1 c2) and hence c is syntactically the same as bind_elab c1 c2. Therefore, its inferred wp has to be stronger than the weakest wp. We internalize this metatheoretical result by adding the following assumptions.
assume val return_inv (#a:Type) (#wp : hwp_mon a) (c : comp_wp a wp) (x:a):
Lemma (requires (c === return_elab x)) (ensures (subsumes (return_wp x) wp))
assume val write_inv (#wp : hwp_mon unit) (c : comp_wp unit wp) (i:nat) (v:mint) :
Lemma (requires (c === hwrite_elab i v)) (ensures (subsumes (write_wp i v) wp))
assume val bind_inv (#a:Type) (#b:Type) (#f_w : hwp_mon a) (f:comp_wp a f_w)
(#g_w: a -> hwp_mon b) (g:(x:a) -> comp_wp b (g_w x)) (#wp : hwp_mon b) (c:comp_wp b wp) :
Lemma (requires (c === bind_elab f g))
(ensures (subsumes (bind_wp f_w g_w) wp))
etc.
-
[10/16] First meeting
-
[10/23]
-
high-level overview of where we're going with this project (as requested by Danel, among others)
-
Rewriting terms with incomplete type information
-
Review progress since last meeting: equivalence relation of l_eq
-
-
[11/06]
- Lens typeclass. Q: What do we need to define a generic morph?
-
l_eq_axiominconsistent. Alternative: use equality on reified low computation (functional extensionality)
- Generalize the state
- Tactic rewriting
-
l_eq_axiominconsistent? - Fix
lforto use Low★'sforcombinator
possibly related work includes:
- qhasm
- jasmin
- cryptol