Commit e3c4a040 authored by Martin Clochard's avatar Martin Clochard
Browse files

Proof of aexpr_natural

parent 3cb17d16
......@@ -285,6 +285,36 @@ let imulf () : hl
ensures { result.code.length = 1 /\ hl_correctness result}
= create_binop imul mul
(*type cond = int -> int -> bool
function icjump_post (cond : cond) : pos -> machine_state -> pred =
\p ms ms'. forall n1 n2 s m.
ms = VMS p (push n2 (push n1 s)) m ->
(cond n1 n2 -> ms' = VMS (p+ofs+1) s m) /\
(not cond n1 n2 -> ms' = VMS (p+1) s m)
let make_cjump (code_cond:code) (ghost cond:cond) (ghost ofs:pos) : hl
requires { forall c: code, p1, n1 n2: int.
codeseq_at c p1 cjmp ->
let p2 = (if cond n1 n2 then p1 + 1 + ofs else p1 + 1) in
forall s:stack, m: state.
transition c
(VMS p1 (push n2 (push n1 s)) m)
(VMS p2 s m) }
ensures { result.pre = ibinop_pre /\ result.post = icjump_post cond }
ensures { result.code = code_cond /\ hl_correctness result }
= let res = {code = code_binop; pre = ibinop_pre ; post = ibinop_post op }
in assert {
forall p ms. res.pre p ms ->
not (exists ms' : machine_state. res.post p ms ms' /\
contextual_irrelevance res.code p ms ms') ->
match ms with
| VMS p' (Cons n2 (Cons n1 s)) m -> p' = p &&
if cond n1 n2
then let ms' = VMS (p+ofs+1) (push (cond n1 n2) s) m in
contextual_irrelevance res.code p ms ms' && false
| _ -> false end && false };
res*)
end
......@@ -305,7 +335,7 @@ module Compile_aexpr
(* arithmetic expression compiler. *)
function aexpr_post (a:aexpr) (len:pos) : pos -> machine_state -> pred =
function aexpr_post (a:aexpr) (len:pos) : pos -> post =
\ p ms ms'.
match ms with
| VMS _ s m -> ms' = VMS (p + len) (push (aeval m a ) s) m
......@@ -338,7 +368,6 @@ module Compile_aexpr
any pos -> post ensures { result = aexpr_post a c.wcode.length }
in hoare pre c post
let compile_aexpr_natural (a: aexpr) : code
ensures { forall c p s m.
codeseq_at c p result ->
......@@ -348,6 +377,25 @@ module Compile_aexpr
=
(compile_aexpr a).code
(*function bexpr_post (b:bexpr) (out_t:pos) (out_f:pos) : pos -> post =
\p ms ms' -> match ms with
| VMS _ s m -> if beval b m
then ms' = VMS (p+out_t) s m
else ms' = VMS (p+out_f) s m
end
lemma bexpr_post_def : forall b out_t out_f p ms ms'.
bexpr_post b out_t out_f p ms ms' =
match ms with
| VMS _ s m -> if beval b m
then ms' = VMS (p+out_t) s m
else ms' = VMS (p+out_f) s m
end
meta rewrite prop bexpr_post_def*)
end
......@@ -376,4 +424,4 @@ end
(res.wp p post) ms
exists ms'
-----------------------------------------------
(post ms') /\ contextual_irrelevance res.wcode p ms ms') *)
\ No newline at end of file
(post ms') /\ contextual_irrelevance res.wcode p ms ms') *)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment