Commit 20e00b94 authored by Léon Gondelman's avatar Léon Gondelman
Browse files

mini-compiler:new version of compiler with aexpr proverd

parent 8921730c
......@@ -7,6 +7,17 @@ module Compiler_logic
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 = machine_state -> bool
......@@ -14,15 +25,15 @@ module Compiler_logic
type post = machine_state -> pred
(* Hoare triples with explicit pre & post *)
type hl =
type hl 'a =
{ code: code;
ghost pre : pos -> pred;
ghost post: pos -> post }
ghost pre : 'a -> pos -> pred;
ghost post: 'a -> pos -> post }
(* Code with weakest precondition wp_correctness. *)
type wp =
type wp 'a =
{ wcode : code;
ghost wp : pos -> pred -> pred }
ghost wp : 'a -> pos -> pred -> pred }
(* Machine transition independence for a piece of code with respect
to the rest of the code. *)
......@@ -32,48 +43,50 @@ module Compiler_logic
transition_star c_global ms1 ms2
(* (Total) correctness for hoare triple. *)
predicate hl_correctness (cs : hl) =
forall p: pos, ms : machine_state. cs.pre p ms ->
predicate hl_correctness (cs : hl 'a) =
forall x:'a, p: pos, ms : machine_state. cs.pre x p ms ->
exists ms' : machine_state.
cs.post p ms ms' /\ contextual_irrelevance cs.code p ms ms'
cs.post x p ms ms' /\ contextual_irrelevance cs.code p ms ms'
(* Invariant for code with WP wp_correctness. *)
predicate wp_correctness (code : wp) =
forall p: pos, post : pred, ms: machine_state.
(code.wp p post) ms ->
predicate wp_correctness (code : wp 'a) =
forall x:'a, p: pos, post : pred, ms: machine_state.
(code.wp x p post) ms ->
exists ms' : machine_state.
(post ms') /\ contextual_irrelevance code.wcode p ms ms'
(* WP combinator for sequence. *)
function seq_wp (s1 s2: wp) : pos -> pred -> pred =
\p q . s1.wp p (s2.wp (p + s1.wcode.length) q)
function seq_wp (s1 : wp 'a) (s2: wp ('a, machine_state)) : 'a -> pos -> pred -> pred =
\x p q ms. s1.wp x p (s2.wp (x,ms) (p + s1.wcode.length) q) ms
lemma seq_wp_lemma :
forall s1 s2 p q.
seq_wp s1 s2 p q = s1.wp p (s2.wp (p + s1.wcode.length) q)
forall s1: wp 'a, s2 x p q ms.
seq_wp s1 s2 x p q ms = s1.wp x p (s2.wp (x,ms) (p + s1.wcode.length) q) ms
meta rewrite prop seq_wp_lemma
(* Code combinator for sequence, with wp. *)
let (~) (s1 s2 : wp) : wp
let (~) (s1 : wp 'a) (s2 : wp ('a, machine_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 s2 /\ wp_correctness result }
= let wcode = s1.wcode ++ s2.wcode in
let res =
{ wcode = wcode ;
wp = any pos -> pred -> pred ensures {result = seq_wp s1 s2 } }
wp = any 'a -> pos -> pred -> pred ensures {result = seq_wp s1 s2 } }
in assert {
forall p: pos, post : pred, ms: machine_state. (res.wp p post) ms ->
forall x: 'a, p: pos, post : pred, ms: machine_state. (res.wp x p post) ms ->
not ( exists ms' : machine_state. (post ms')
/\ contextual_irrelevance res.wcode p ms ms') ->
(forall ms' : machine_state.
((s2.wp (p + s1.wcode.length) post) ms')
((s2.wp (x,ms) (p + s1.wcode.length) post) ms')
/\ contextual_irrelevance res.wcode p ms ms' -> false)
&& false };
res
(*
function fork_wp (s2: wp) (exn: pos -> pred) : pos -> pred -> pred =
\p q ms.
(exn p ms -> q ms) /\
......@@ -87,49 +100,50 @@ module Compiler_logic
(* Code combinator for sequence, with wp. *)
let (%) (s: wp) (exn: pos -> pred) : wp
requires { wp_correctness s }
ensures { result.wp = fork_wp s exn /\ result.wcode.length = s.wcode.length }
ensures { wp_correctness result }
= { wcode = s.wcode ;
wp = any pos -> pred -> pred ensures {result = fork_wp s exn } }
wp = any pos -> pred -> pred ensures {result = fork_wp s exn } } *)
(* WP transformer for hoare triples. *)
function towp_wp (c : hl) : pos -> pred -> pred =
\p q ms. c.pre p ms && (forall ms'. c.post p ms ms' -> q ms')
function towp_wp (c : hl 'a) : 'a -> pos -> pred -> pred =
\ x p q ms. c.pre x p ms && (forall ms'. c.post x p ms ms' -> q ms')
lemma towp_wp_lemma:
forall c p q ms. towp_wp c p q ms =
(c.pre p ms && (forall ms'. c.post p ms ms' -> q ms'))
forall c, x:'a, p q ms. towp_wp c x p q ms =
(c.pre x p ms && (forall ms'. c.post 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) : wp
let ($_) (c: hl 'a) : wp 'a
requires { hl_correctness c }
ensures { result.wcode.length = c.code.length /\ result.wp = towp_wp c}
ensures { wp_correctness result }
= { wcode = c.code;
wp = any pos -> pred -> pred ensures {result = towp_wp c}}
wp = any 'a -> pos -> pred -> pred ensures {result = towp_wp c}}
(* 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: pos -> pred) (c: wp) (ghost post: pos -> post) : hl
let hoare (ghost pre: 'a -> pos -> pred) (c: wp 'a) (ghost post: 'a -> pos -> post) : hl 'a
requires { wp_correctness c }
requires { forall p ms. pre p ms -> (c.wp p (post p ms)) ms }
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 : pos -> pred = \p ms.
function trivial_pre : 'a -> pos -> pred = \x p ms.
match ms with
| VMS p' _ _ -> p = p'
end
lemma trivial_pre_lemma:
forall p ms. trivial_pre p ms =
forall x:'a, p ms. trivial_pre x p ms =
match ms with
| VMS p' _ _ -> p = p'
end
......@@ -148,7 +162,7 @@ module Builtin_spec
use import HighOrd
use import Compiler_logic
(*
function inil_post : pos -> post =
\p ms ms'. ms = ms'
......@@ -160,31 +174,31 @@ module Builtin_spec
let inil () : hl
ensures { result.pre = trivial_pre /\ result.post = inil_post }
ensures { result.code.length = 0 /\ hl_correctness result }
= { pre = trivial_pre; code = Nil; post = inil_post }
= { pre = trivial_pre; code = Nil; post = inil_post } *)
function iconst_post (n:int) : pos -> post =
\p ms ms'. forall s m.
function iconst_post (n:int) : 'a -> pos -> post =
\x p ms ms'. forall s m.
ms = VMS p s m ->
ms' = VMS (p+1) (push n s) m
lemma iconst_post_lemma:
forall n p ms ms'.
iconst_post n p ms ms' =
forall x:'a, n p ms ms'.
iconst_post n x p ms ms' =
forall s m.
ms = VMS p s m ->
ms' = VMS (p+1) (push n s) m
meta rewrite prop iconst_post_lemma
let iconstf (n: int) : hl
let iconstf (n: int) : hl 'a
ensures { result.pre = trivial_pre /\ result.post = iconst_post n }
ensures { result.code.length = 1 /\ hl_correctness result }
= let res =
{ pre = trivial_pre; code = iconst n; post = iconst_post n } in
assert {
forall p ms. res.pre p ms ->
not (exists ms' : machine_state. res.post p ms ms' /\
forall x p ms. res.pre x p ms ->
not (exists ms' : machine_state. res.post x p ms ms' /\
contextual_irrelevance res.code p ms ms') ->
match ms with
| VMS p' s m -> p' = p &&
......@@ -193,28 +207,28 @@ module Builtin_spec
| _ -> false end && false };
res
function ivar_post (x:id) : pos -> post =
\p ms ms'. forall s m.
function ivar_post (x:id) : 'a -> pos -> post =
\a p ms ms'. forall s m.
ms = VMS p s m ->
ms' = VMS (p+1) (push m[x] s) m
lemma ivar_post_lemma:
forall x p ms ms'.
ivar_post x p ms ms' =
forall x, a:'a, p ms ms'.
ivar_post x a p ms ms' =
forall s m.
ms = VMS p s m ->
ms' = VMS (p+1) (push m[x] s) m
meta rewrite prop ivar_post_lemma
let ivarf (x: id) : hl
let ivarf (x: id) : hl 'a
ensures { result.pre = trivial_pre /\ result.post = ivar_post x }
ensures { result.code.length = 1 /\ hl_correctness result }
= let res =
{ pre = trivial_pre; code = ivar x; post = ivar_post x } in
assert {
forall p ms. res.pre p ms ->
not (exists ms' : machine_state. res.post p ms ms' /\
forall a p ms. res.pre a p ms ->
not (exists ms' : machine_state. res.post a p ms ms' /\
contextual_irrelevance res.code p ms ms') ->
match ms with
| VMS p' s m -> p' = p &&
......@@ -224,7 +238,7 @@ module Builtin_spec
res
(*
constant isetvar_pre : pos -> pred =
\p ms . exists n s m. ms = VMS p (push n s) m
......@@ -262,35 +276,35 @@ constant isetvar_pre : pos -> pred =
let ms' = VMS (p+1) s m[x<-n] in
contextual_irrelevance res.code p ms ms' && false
| _ -> false end && false };
res
res *)
type binop = int -> int -> int
constant ibinop_pre : pos -> pred =
\p ms . exists n1 n2 s m. ms = VMS p (push n2 (push n1 s)) m
constant ibinop_pre : 'a -> pos -> pred =
\x p ms . exists n1 n2 s m. ms = VMS p (push n2 (push n1 s)) m
lemma ibinop_pre_lemma:
forall p ms. ibinop_pre p ms =
forall x:'a, p ms. ibinop_pre x p ms =
exists n1 n2 s m. ms = VMS p (push n2 (push n1 s)) m
meta rewrite prop ibinop_pre_lemma
function ibinop_post (op : binop) : pos -> machine_state -> pred =
\p ms ms'. forall n1 n2 s m.
function ibinop_post (op : binop) : 'a -> pos -> machine_state -> pred =
\x p ms ms'. forall n1 n2 s m.
ms = VMS p (push n2 (push n1 s)) m ->
ms' = VMS (p + 1) (push (op n1 n2) s) m
lemma ibinop_post_lemma:
forall op p ms ms'.
ibinop_post op p ms ms' =
forall op, x:'a, p ms ms'.
ibinop_post op x p ms ms' =
forall n1 n2 s m.
ms = VMS p (push n2 (push n1 s)) m ->
ms' = VMS (p + 1) (push (op n1 n2) s) m
meta rewrite prop ibinop_post_lemma
let create_binop (code_binop: code) (ghost op : binop) : hl
let create_binop (code_binop: code) (ghost op : binop) : hl 'a
requires {
forall c: code, p: pos.
codeseq_at c p code_binop ->
......@@ -302,8 +316,8 @@ constant isetvar_pre : pos -> pred =
ensures { result.code = code_binop /\ 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' /\
forall x p ms. res.pre x p ms ->
not (exists ms' : machine_state. res.post x p ms ms' /\
contextual_irrelevance res.code p ms ms') ->
match ms with
| VMS p' (Cons n2 (Cons n1 s)) m -> p' = p &&
......@@ -324,24 +338,24 @@ constant isetvar_pre : pos -> pred =
lemma mul_lemma: forall x y. mul x y = x * y
meta rewrite prop mul_lemma
let iaddf () : hl
let iaddf () : hl 'a
ensures { result.pre = ibinop_pre /\ result.post = ibinop_post plus }
ensures { result.code.length = 1 /\ hl_correctness result}
= create_binop iadd plus
let isubf () : hl
let isubf () : hl 'a
ensures { result.pre = ibinop_pre /\ result.post = ibinop_post sub }
ensures { result.code.length = 1 /\ hl_correctness result}
= create_binop isub sub
let imulf () : hl
let imulf () : hl 'a
ensures { result.pre = ibinop_pre /\ result.post = ibinop_post mul }
ensures { result.code.length = 1 /\ hl_correctness result}
= create_binop imul mul
(********************************************************************)
(********************************************************************)
(*
function ibranch_post (ofs: pos) : pos -> post =
\p ms ms'. forall s m. ms = VMS p s m -> ms' = VMS (p + 1 + ofs) s m
......@@ -453,6 +467,7 @@ let ibgtf (ofs : pos) : hl
ensures { result.code.length = 1 /\ hl_correctness result }
= create_cjump (ibgt ofs) bgt ofs
*)
end
......@@ -472,15 +487,15 @@ module Compile_aexpr
(* arithmetic expression compiler. *)
function aexpr_post (a:aexpr) (len:pos) : pos -> post =
\ p ms ms'.
function aexpr_post (a:aexpr) (len:pos) : 'a -> pos -> post =
\ x p ms ms'.
match ms with
| VMS _ s m -> ms' = VMS (p + len) (push (aeval m a ) s) m
end
lemma aexpr_post_lemma:
forall a len p ms ms'.
aexpr_post a len p ms ms' =
forall a len, x: 'a, p ms ms'.
aexpr_post a len x p ms ms' =
match ms with
| VMS _ s m -> ms' = VMS (p + len) (push (aeval m a ) s) m
end
......@@ -488,7 +503,7 @@ module Compile_aexpr
meta rewrite prop aexpr_post_lemma
let rec compile_aexpr (a : aexpr) : hl
let rec compile_aexpr (a : aexpr) : hl 'a
variant { a }
ensures { result.pre = trivial_pre }
ensures { result.post = aexpr_post a result.code.length }
......@@ -510,12 +525,14 @@ module Compile_aexpr
transition_star c
(VMS p s m)
(VMS (p + length result) (push (aeval m a) s) m) }
= let res = (compile_aexpr a) in
assert { forall p s m. res.pre p (VMS p s m) };
= let res = (compile_aexpr a) : hl unit in
assert { forall p s m. res.pre () p (VMS p s m) };
res.code
end
(*
module Compile_bexpr
use import int.Int
......@@ -667,7 +684,7 @@ module Compile_com
end
*)
(*
Local Variables:
......
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