Commit 3c5f8cc4 authored by Martin Clochard's avatar Martin Clochard

(wip) mini-compiler: variation with backward simulation

parent 861b2d3f
(*Imp to ImpVm compiler *)
(**************************************************************************)
module Compile_aexpr
use import int.Int
use import list.List
use import list.Length
use import list.Append
use import imp.Imp
use import vm.Vm
use import vm.VMClock
use import state.State
use import logic.Compiler_logic
use import specs.VM_instr_spec
function aexpr_post (a:aexpr) (len:pos) : post 'a =
\x p ms ms'. let VMC _ s m c = ms in
let VMC p' s' m' c' = ms' in
p' = p + len /\ s' = push (aeval m a) s /\ m' = m /\ c' >= c
meta rewrite_def function aexpr_post
let rec compile_aexpr (a:aexpr) : hl 'a
ensures { result.pre = trivial_pre /\ hl_correctness result }
ensures { result.post = aexpr_post a result.code.length }
variant { a }
= let c = match a with
| Anum n -> $ iconstf n
| Avar x -> $ ivarf x
| Aadd a1 a2 -> $ compile_aexpr a1 ~ $ compile_aexpr a2 ~ $ iaddf ()
| Asub a1 a2 -> $ compile_aexpr a1 ~ $ compile_aexpr a2 ~ $ isubf ()
| Amul a1 a2 -> $ compile_aexpr a1 ~ $ compile_aexpr a2 ~ $ imulf ()
end in
hoare trivial_pre c (aexpr_post a c.wcode.length)
end
module Compile_bexpr
use import int.Int
use import list.List
use import list.Length
use import list.Append
use import imp.Imp
use import vm.Vm
use import vm.VMClock
use import state.State
use import logic.Compiler_logic
use import specs.VM_instr_spec
use import Compile_aexpr
function bexpr_post (b:bexpr) (cond: bool) (out_t:pos) (out_f:pos) : post 'a =
\x p ms ms'. let VMC _ s m c = ms in
let VMC p' s' m' c' = ms' in
s' = s /\ m' = m /\ c' >= c /\
if beval m b = cond then p' = p + out_t else p' = p + out_f
meta rewrite_def function bexpr_post
function exec_cond (b1:bexpr) (cond:bool) : pre 'a =
\x p ms. let VMC _ _ m _ = ms in beval m b1 = cond
meta rewrite_def function exec_cond
let rec compile_bexpr (b : bexpr) (cond: bool) (ofs: pos) : hl 'a
ensures { result.pre = trivial_pre /\ hl_correctness result }
ensures { result.post =
bexpr_post b cond (result.code.length + ofs) result.code.length }
variant { b }
= let c = match b with
| Btrue -> $ if cond then ibranchf ofs else inil ()
| Bfalse -> $ if cond then inil () else ibranchf ofs
| Bnot b1 -> $ compile_bexpr b1 (not cond) ofs
| Band b1 b2 ->
let c2 = $ compile_bexpr b2 cond ofs % exec_cond b1 true in
let ofs = if cond then length c2.wcode else ofs + length c2.wcode in
$ compile_bexpr b1 false ofs ~ c2
| Beq a1 a2 -> $ compile_aexpr a1 ~ $ compile_aexpr a2 ~
$ if cond then ibeqf ofs else ibnef ofs
| Ble a1 a2 -> $ compile_aexpr a1 ~ $ compile_aexpr a2 ~
$ if cond then iblef ofs else ibgtf ofs
end in
let ghost post = bexpr_post b cond (c.wcode.length + ofs) c.wcode.length in
hoare trivial_pre c post
end
module Compile_com
use import int.Int
use import list.List
use import list.Length
use import list.Append
use import imp.Imp
use import vm.Vm
use import vm.VMClock
use import state.State
use import logic.Compiler_logic
use import specs.VM_instr_spec
use import Compile_aexpr
use import Compile_bexpr
function com_post (cmd:com) (len:pos) : post 'a =
\x p ms ms'. let VMC _ s m c = ms in
let VMC p' s' m' c' = ms' in
p' = p + len /\ s' = s /\ ceval m cmd m' /\ c' >= c
meta rewrite_def function com_post
function exec_cond_old (b1:bexpr) (cond:bool) : pre ('a,clock_state) =
\x p ms. let VMC _ _ m _ = snd x in beval m b1 = cond
meta rewrite_def function exec_cond_old
function loop_invariant (c:com) : pre ('a,clock_state) =
\x p msi. let VMC _ s0 m0 c0 = snd x in
let VMC pi si mi ci = msi in
pi = p /\ s0 = si /\ ci >= c0 /\
(forall mf. ceval mi c mf -> ceval m0 c mf)
meta rewrite_def function loop_invariant
function loop_post (c : com) (len: pos) : pre ('a,clock_state) =
\x p msf. let VMC _ s0 m0 c0 = snd x in let VMC pf sf mf cf = msf in
pf = p + len /\ s0 = sf /\ cf >= c0 /\ ceval m0 c mf
meta rewrite_def function loop_post
let rec compile_com (cmd: com) : hl 'a
ensures { result.pre = trivial_pre /\ hl_correctness result }
ensures { result.post = com_post cmd result.code.length }
variant { cmd }
= let res = match cmd with
| Cskip -> $ inil ()
| Cassign x a -> $ compile_aexpr a ~ $ isetvarf x
| Cseq cmd1 cmd2 -> $ compile_com cmd1 ~ $ compile_com cmd2
| Cif cond cmd1 cmd2 -> let code_false = compile_com cmd2 in
let code_true = $ compile_com cmd1 ~ $ ibranchf code_false.code.length in
$ compile_bexpr cond false code_true.wcode.length ~
(code_true % exec_cond cond true) ~
($ code_false % exec_cond_old cond false)
| Cwhile test body -> let code_body = compile_com body in
let body_length = length code_body.code + 1 in
let code_test = compile_bexpr test false body_length in
let ofs = length code_test.code + body_length in
let wp_while = $ code_test ~
($ code_body ~ $ ibranchf (- ofs)) % exec_cond test true in
let ghost inv = loop_invariant cmd in
let ghost post = loop_post cmd ofs in
let hl_while = hoare inv wp_while (loop_preservation inv post) in
$ inil () ~ $ make_loop_hl hl_while inv post
end in
hoare trivial_pre res (com_post cmd res.wcode.length)
let compile_program (prog:com) : code
ensures { forall mi mf:state,p s.
vm_stuck result (VMS 0 Nil mi) (VMS p s mf) ->
s = Nil /\ codeseq_at result p ihalt /\ ceval mi prog mf }
= let res = compile_com prog : hl unit in
let res' = res.code ++ ihalt in
assert { codeseq_at res' 0 res.code &&
forall mi pf sf mf.
(forall ms'. not transition res' (VMS pf sf mf) ms') ->
forall p' s' m'.
("induction" transition_star res' (VMS p' s' m') (VMS pf sf mf)) ->
forall c'.
let init = VMC 0 Nil mi 0 in
let post = com_post prog res.code.length () 0 init in
trivial_pre () 0 init ->
C.transition_star (res',post) init (VMC p' s' m' c') ->
("stop_split" sf = Nil /\ pf = res.code.length /\ ceval mi prog mf) };
assert { forall mi mf, p s.
vm_stuck res' (VMS 0 Nil mi) (VMS p s mf) ->
let init = VMC 0 Nil mi 0 in
let post = com_post prog res.code.length () 0 init in
C.transition_star (res',post) init init &&
p = res.code.length &&
s = Nil /\ codeseq_at res' p ihalt /\ ceval mi prog mf };
res'
(*
(* Execution test: compile a simple factorial program, e.g
X := 1; WHILE NOT (Y <= 0) DO X := X * Y; Y := Y - 1 DONE
(why3 execute -L . compiler.mlw Compile_com.test) *)
let test () : code =
let x = Id 0 in
let y = Id 1 in
let cond = Bnot (Ble (Avar y) (Anum 0)) in
let body1 = Cassign x (Amul (Avar x) (Avar y)) in
let body2 = Cassign y (Asub (Avar y) (Anum 1)) in
let lp = Cwhile cond (Cseq body1 body2) in
let code = Cseq (Cassign x (Anum 1)) lp in
compile_program code
let test2 () : code =
compile_program (Cwhile Btrue Cskip)*)
end
(*
Local Variables:
compile-command: "why3 ide -L . compiler.mlw"
End:
*)
(* *)
(*
(res.wp p post) ms ->
(exists ms' : machine_state. (post ms')
/\ contextual_irrelevance res.wcode p ms ms')
*)
(*
(res.wp p post) ms
exists ms'
-----------------------------------------------
(post ms') /\ contextual_irrelevance res.wcode p ms ms')
*)
(*condition suffisante ? *)
(* trouver un ms' qui vérifie :
((s2.wp (p + s1.wcode.length) post) ms') /\ contextual_irrelevance res.wcode p ms ms' *)
(*
(res.wp p post) ms
exists ms'
-----------------------------------------------
(post ms') /\ contextual_irrelevance res.wcode p ms ms') *)
theory Imp
use import state.State
use import bool.Bool
use import int.Int
(* ************************ SYNTAX ************************ *)
type aexpr =
| Anum int
| Avar id
| Aadd aexpr aexpr
| Asub aexpr aexpr
| Amul aexpr aexpr
type bexpr =
| Btrue
| Bfalse
| Band bexpr bexpr
| Bnot bexpr
| Beq aexpr aexpr
| Ble aexpr aexpr
type com =
| Cskip
| Cassign id aexpr
| Cseq com com
| Cif bexpr com com
| Cwhile bexpr com
(* ************************ SEMANTICS ************************ *)
function aeval (st:state) (e:aexpr) : int =
match e with
| Anum n -> n
| Avar x -> st[x]
| Aadd e1 e2 -> aeval st e1 + aeval st e2
| Asub e1 e2 -> aeval st e1 - aeval st e2
| Amul e1 e2 -> aeval st e1 * aeval st e2
end
function beval (st:state) (b:bexpr) : bool =
match b with
| Btrue -> true
| Bfalse -> false
| Bnot b' -> notb (beval st b')
| Band b1 b2 -> andb (beval st b1) (beval st b2)
| Beq a1 a2 -> aeval st a1 = aeval st a2
| Ble a1 a2 -> aeval st a1 <= aeval st a2
end
inductive ceval state com state =
(* skip *)
| E_Skip : forall m. ceval m Cskip m
(* assignement *)
| E_Ass : forall m a x. ceval m (Cassign x a) m[x <- aeval m a]
(* sequence *)
| E_Seq : forall cmd1 cmd2 m0 m1 m2.
ceval m0 cmd1 m1 -> ceval m1 cmd2 m2 -> ceval m0 (Cseq cmd1 cmd2) m2
(* if then else *)
| E_IfTrue : forall m0 m1 cond cmd1 cmd2. beval m0 cond ->
ceval m0 cmd1 m1 -> ceval m0 (Cif cond cmd1 cmd2) m1
| E_IfFalse : forall m0 m1 cond cmd1 cmd2. not beval m0 cond ->
ceval m0 cmd2 m1 -> ceval m0 (Cif cond cmd1 cmd2) m1
(* while *)
| E_WhileEnd : forall cond m body. not beval m cond ->
ceval m (Cwhile cond body) m
| E_WhileLoop : forall mi mj mf cond body. beval mi cond ->
ceval mi body mj -> ceval mj (Cwhile cond body) mf ->
ceval mi (Cwhile cond body) mf
lemma ceval_deterministic_aux : forall c mi mf1. ceval mi c mf1 ->
forall mf2. ("inversion" ceval mi c mf2) -> mf1 = mf2
lemma ceval_deterministic : forall c mi mf1 mf2.
ceval mi c mf1 -> ceval mi c mf2 -> mf1 = mf2
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<file name="../imp.why">
<theory name="Imp" sum="d47e4ca50e2ba0ffa18970b5b9819d30">
<goal name="ceval_deterministic_aux">
<transf name="induction_pr">
<goal name="ceval_deterministic_aux.1" expl="1.">
<transf name="inversion_pr">
<goal name="ceval_deterministic_aux.1.1" expl="1.">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="ceval_deterministic_aux.1.2" expl="2.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.1.3" expl="3.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.1.4" expl="4.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.1.5" expl="5.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.1.6" expl="6.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.1.7" expl="7.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.2" expl="2.">
<transf name="inversion_pr">
<goal name="ceval_deterministic_aux.2.1" expl="1.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.2" expl="2.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.3" expl="3.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.4" expl="4.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.5" expl="5.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.6" expl="6.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.2.7" expl="7.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.3" expl="3.">
<transf name="inversion_pr">
<goal name="ceval_deterministic_aux.3.1" expl="1.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.2" expl="2.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.3" expl="3.">
<proof prover="0"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.4" expl="4.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.5" expl="5.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.6" expl="6.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.3.7" expl="7.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.4" expl="4.">
<transf name="inversion_pr">
<goal name="ceval_deterministic_aux.4.1" expl="1.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.2" expl="2.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.3" expl="3.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.4" expl="4.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.5" expl="5.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.6" expl="6.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.4.7" expl="7.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.5" expl="5.">
<transf name="inversion_pr">
<goal name="ceval_deterministic_aux.5.1" expl="1.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.5.2" expl="2.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.5.3" expl="3.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.5.4" expl="4.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.5.5" expl="5.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.5.6" expl="6.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.5.7" expl="7.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.6" expl="6.">
<transf name="inversion_pr">
<goal name="ceval_deterministic_aux.6.1" expl="1.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6.2" expl="2.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6.3" expl="3.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6.4" expl="4.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6.5" expl="5.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6.6" expl="6.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="ceval_deterministic_aux.6.7" expl="7.">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic_aux.7" expl="7.">
<transf name="inversion_pr">
<goal name="ceval_deterministic_aux.7.1" expl="1.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.7.2" expl="2.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.7.3" expl="3.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.7.4" expl="4.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.7.5" expl="5.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.7.6" expl="6.">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="ceval_deterministic_aux.7.7" expl="7.">
<proof prover="0"><result status="valid" time="0.07"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="ceval_deterministic">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
</file>
</why3session>
module Compiler_logic
use import int.Int
use import list.List
use import list.Length
use import list.Append
use import vm.Vm
use import vm.VMClock
use import state.State
use import HighOrd
function fst (p: ('a,'b)) : 'a = let (x,_) = p in x
meta rewrite_def function fst
function snd (p: ('a,'b)) : 'b = let (_,y) = p in y
meta rewrite_def function snd
(* Unary predicates over machine states *)
type pred = clock_state -> bool
(* Binary predicates over machine states *)
type rel = clock_state -> pred
(* pre/post-conditions types, as parameterized unary/binary predicates. *)
type pre 'a = 'a -> pos -> pred
type post 'a = 'a -> pos -> rel
(* Hoare triples with explicit pre & post *)
type hl 'a =
{ code: code;
ghost pre : pre 'a;
ghost post: post 'a }
(* Predicate transformer type. *)
type wp_trans 'a = 'a -> pos -> pred -> pred
(* Code with weakest precondition wp_correctness. *)
type wp 'a =
{ wcode : code;
ghost wp : wp_trans 'a }
(* Correctness for hoare triple:
If starting from precondition,
never get stuck before reaching the postcondition. *)
predicate hl_correctness (cs:hl 'a) =
forall x:'a,c_glob p mc mc'. cs.pre x p mc ->
codeseq_at c_glob p cs.code ->
let post = cs.post x p mc in
C.transition_star (c_glob,post) mc mc' /\ not post mc' ->
let VMC p s m _ = mc' in
exists ms''. transition c_glob (VMS p s m) ms''
(* Invariant for code with WP wp_correctness. *)
predicate wp_correctness (code:wp 'a) =
forall x:'a,c_glob p post mc mc'. code.wp x p post mc ->
codeseq_at c_glob p code.wcode ->
C.transition_star (c_glob,post) mc mc' /\ not post mc' ->
let VMC p s m _ = mc' in
exists ms''. transition c_glob (VMS p s m) ms''
(* WP combinator for sequence. *)
(*** Technical: Why3 refuse the logic call in program,
so we cannot define it in function of (wp 'a) arguments only. *)
function seq_wp (l1:int) (w1:wp_trans 'a)
(w2:wp_trans ('a,clock_state)) : wp_trans 'a =
\x p q mc. w1 x p (w2 (x,mc) (p+l1) q) mc
lemma seq_wp_lemma :
forall l1,w1: wp_trans 'a,w2 x p q mc.
seq_wp l1 w1 w2 x p q mc = w1 x p (w2 (x,mc) (p+l1) q) mc
meta rewrite prop seq_wp_lemma
(* Code combinator for sequence, with wp. *)
let (~) (s1 : wp 'a) (s2 : wp ('a, clock_state)) : wp 'a
requires { wp_correctness s1 /\ wp_correctness s2 }
ensures { result.wcode.length = s1.wcode.length + s2.wcode.length }
ensures { result.wp = seq_wp s1.wcode.length s1.wp s2.wp }
ensures { wp_correctness result }
= let code = s1.wcode ++ s2.wcode in
let res = { wcode = code; wp = seq_wp s1.wcode.length s1.wp s2.wp } in
assert { forall x:'a,c_glob p post mc mc' mc''.
C.transition_star (c_glob,post) mc' mc'' ->
not post mc'' -> codeseq_at c_glob p code -> res.wp x p post mc ->
let post2 = s2.wp (x,mc) (p+s1.wcode.length) post in
C.transition_star (c_glob,post2) mc mc' ->
not post2 mc' ->
let VMC p s m _ = mc'' in
exists ms. transition c_glob (VMS p s m) ms
};
assert { forall x:'a,c_glob p post mc mc'.
C.transition_star (c_glob,post) mc mc' -> not post mc' ->
codeseq_at c_glob p code -> res.wp x p post mc ->
let post2 = s2.wp (x,mc) (p+s1.wcode.length) post in
C.transition_star (c_glob,post2) mc mc &&
let VMC p s m _ = mc' in
exists ms. transition c_glob (VMS p s m) ms };
res
function fork_wp (w:wp_trans 'a) (cond:pre 'a) : wp_trans 'a =
\x p q ms. (not cond x p ms -> q ms) /\ (cond x p ms -> w x p q ms)
lemma fork_wp_lemma: forall w:wp_trans 'a,cond x p q ms.
fork_wp w cond x p q ms =
((not cond x p ms -> q ms) /\ (cond x p ms -> w x p q ms))
meta rewrite prop fork_wp_lemma
(* Code combinator for sequence, with wp. *)
let (%) (s:wp 'a) (ghost cond:pre 'a) : wp 'a
requires { wp_correctness s }
ensures { result.wp = fork_wp s.wp cond }
ensures { result.wcode.length = s.wcode.length /\ wp_correctness result }
= { wcode = s.wcode; wp = fork_wp s.wp cond }
(* WP transformer for hoare triples. *)
function towp_wp (pr:pre 'a) (ps:post 'a) : wp_trans 'a =
\x p q ms. pr x p ms && (forall ms'. ps x p ms ms' -> q ms')
lemma towp_wp_lemma:
forall pr ps, x:'a, p q ms. towp_wp pr ps x p q ms =
(pr x p ms && (forall ms'. ps x p ms ms' -> q ms'))
meta rewrite prop towp_wp_lemma
(* Unwrap code with hoare triple into code with wp.
Analogous to function call/abstract block. *)
let ($_) (c:hl 'a) : wp 'a
requires { hl_correctness c }
ensures { result.wcode.length = c.code.length }
ensures { result.wp = towp_wp c.pre c.post /\ wp_correctness result }
= { wcode = c.code; wp = towp_wp c.pre c.post }
(* Equip code with pre/post-condition. That is here that proof happen.
(P -> wp (c,Q)). Anologous to checking function/abstract block
specification. *)
let hoare (ghost pre:pre 'a) (c:wp 'a) (ghost post:post 'a) : hl 'a
requires { wp_correctness c }
requires { forall x p ms. pre x p ms -> (c.wp x p (post x p ms)) ms }
ensures { result.pre = pre /\ result.post = post }
ensures { result.code.length = c.wcode.length /\ hl_correctness result}
= { code = c.wcode ; pre = pre; post = post }
function trivial_pre : pre 'a = \x p ms. let VMC p' _ _ _ = ms in p = p'
meta rewrite_def function trivial_pre
function loop_preservation (inv post:pre 'a) : post 'a =
\x p ms ms'. (inv x p ms' /\ ms <> ms') \/ post x p ms'
meta rewrite_def function loop_preservation
function forget_old (post:pre 'a) : post 'a =
\x p ms . post x p