Skip to content

GitLab

Commit 92211e8b authored by Léon Gondelman's avatar Léon Gondelman
Browse files

mini-compiler : fully automatic proof of compilation for arithmetic expressions

parent 1469c893
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 599 additions and 179 deletions
examples/in_progress/mini-compiler/compiler.mlw
View file @ 92211e8b
......@@ -3,16 +3,13 @@ module Compiler_logic
use import list.List
use import list.Length
use import list.Append
use import imp.Imp
use import vm.Vm
use import state.State
use import HighOrd
(* Unary predicates over machine states *)
type pred = machine_state -> bool
(* Postcondition type (first argument is old state) *)
type post = machine_state -> pred
......@@ -21,119 +18,274 @@ module Compiler_logic
{ code: code;
ghost pre : pos -> pred;
ghost post: pos -> post }
(* Code with weakest precondition wp_correctness. *)
type wp =
{ wcode : code;
ghost wp : pos -> pred -> pred }
(* Machine transition independence for a piece of code with respect
to the rest of the code. *)
predicate contextual_irrelevance (c : code) (p: pos) (ms1 ms2 : machine_state)
= forall c_global: code.
codeseq_at c_global p c ->
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 ->
exists ms' : machine_state. cs.post p ms ms'
/\ contextual_irrelevance cs.code p ms ms'
exists ms' : machine_state.
cs.post 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 ->
exists ms' : machine_state. (post ms')
/\ contextual_irrelevance code.wcode p ms 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)
lemma seq_wp_def : forall s1 s2 p q.
seq_wp s1 s2 p q = s1.wp p (s2.wp (p+s1.wcode.length) q)
meta rewrite prop seq_wp_def
\p q . s1.wp p (s2.wp (p + s1.wcode.length) q)
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)
meta rewrite prop seq_wp_lemma
(* Code combinator for sequence, with wp. *)
let (~) (s1 s2 : wp) : wp
requires { wp_correctness s1 /\ wp_correctness s2 }
ensures { wp_correctness result }
ensures { result.wp = seq_wp s1 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 } } in
assert {
forall p: pos, post : pred, ms: machine_state.
(res.wp 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')
/\ contextual_irrelevance res.wcode p ms ms' -> false) && false
};
let res =
{ wcode = wcode ;
wp = any pos -> pred -> pred ensures {result = seq_wp s1 s2 } }
in assert {
forall p: pos, post : pred, ms: machine_state. (res.wp 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')
/\ 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) /\
(not exn p ms -> s2.wp p q ms)
lemma fork_wp_lemma:
forall s2 exn p q ms.
fork_wp s2 exn p q ms = ((exn p ms -> q ms) /\ (not exn p ms -> s2.wp p q ms))
meta rewrite prop fork_wp_lemma
(* 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 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')
lemma towp_wp_def : forall c p q ms.
towp_wp c p q ms = (c.pre p ms && (forall ms'. c.post p ms ms' -> q ms'))
meta rewrite prop towp_wp_def
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'))
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
requires { hl_correctness c }
ensures { wp_correctness result }
ensures { result.wcode = c.code }
ensures { result.wp = towp_wp c }
= { wcode = c.code; wp = any pos -> pred -> pred ensures {result = towp_wp c}}
let ($_) (c: hl) : wp
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}}
(* 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 -> machine_state -> pred) : hl
requires { wp_correctness c }
requires { forall p ms. pre p ms -> (c.wp p (post p ms)) ms }
ensures { result.code = c.wcode }
ensures { hl_correctness result }
ensures { result.pre = pre /\ result.post = post }
let hoare (ghost pre: pos -> pred) (c: wp) (ghost post: pos -> post) : hl
requires { wp_correctness c }
requires { forall p ms. pre p ms -> (c.wp p (post 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 }
(* Specification of builtin binary operators. *)
function trivial_pre : pos -> pred = \p ms.
match ms with
| VMS p' _ _ -> p = p'
end
lemma trivial_pre_lemma:
forall p ms. trivial_pre p ms =
match ms with
| VMS p' _ _ -> p = p'
end
meta rewrite prop trivial_pre_lemma
end
(* Specification of builtin instructions. *)
module Builtin_spec
use import int.Int
use import list.List
use import list.Length
use import vm.Vm
use import state.State
use import HighOrd
use import Compiler_logic
function iconst_post (n:int) : pos -> post =
\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 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
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' /\
contextual_irrelevance res.code p ms ms') ->
match ms with
| VMS p' s m -> p' = p &&
let ms' = VMS (p+1) (push n s) m in
contextual_irrelevance res.code p ms ms' && false
| _ -> false end && false };
res
function ivar_post (x:id) : pos -> post =
\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 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
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' /\
contextual_irrelevance res.code p ms ms') ->
match ms with
| VMS p' s m -> p' = p &&
let ms' = VMS (p+1) (push m[x] s) m in
contextual_irrelevance res.code p ms ms' && false
| _ -> false end && false };
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
function iadd_post : pos -> machine_state -> pred =
lemma ibinop_pre_lemma:
forall p ms. ibinop_pre 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.
ms = VMS p (push n2 (push n1 s)) m ->
ms' = VMS (p + 1) (push (n1 + n2) s) m
ms = VMS p (push n2 (push n1 s)) m ->
ms' = VMS (p + 1) (push (op n1 n2) s) m
let iaddf () : hl
ensures { forall p ms. result.pre p ms <-> ibinop_pre p ms}
ensures { forall p ms ms'. result.post p ms ms' <-> iadd_post p ms ms' }
ensures { hl_correctness result }
ensures { result.code.length = 1 }
= let res = {code = Cons Iadd Nil; pre = ibinop_pre ; post = iadd_post } in
assert {
lemma ibinop_post_lemma:
forall op p ms ms'.
ibinop_post op 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
requires {
forall c: code, p: pos.
codeseq_at c p code_binop ->
forall n1 n2: int, s: stack, m: state.
transition c
(VMS p (push n2 (push n1 s)) m)
(VMS (p + 1) (push (op n1 n2) s) m) }
ensures { result.pre = ibinop_pre /\ result.post = ibinop_post op }
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' /\
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 &&
let ms' = VMS (p+1) (push (n1 + n2) s) m in
let ms' = VMS (p+1) (push (op n1 n2) s) m in
contextual_irrelevance res.code p ms ms' && false
| _ -> false end && false };
res
constant plus : binop = \x y. x + y
lemma plus_lemma: forall x y. plus x y = x + y
meta rewrite prop plus_lemma
constant sub : binop = \x y. x - y
lemma sub_lemma: forall x y. sub x y = x - y
meta rewrite prop sub_lemma
constant mul : binop = \x y. x * y
lemma mul_lemma: forall x y. mul x y = x * y
meta rewrite prop mul_lemma
let iaddf () : hl
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
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
ensures { result.pre = ibinop_pre /\ result.post = ibinop_post mul }
ensures { result.code.length = 1 /\ hl_correctness result}
= create_binop imul mul
end
......@@ -149,41 +301,69 @@ module Compile_aexpr
use import vm.Vm
use import state.State
use import Compiler_logic
use import Builtin_spec
(* arithmetic expression compiler. *)
function aexpr_post (a:aexpr) (len:pos) : pos -> machine_state -> pred =
\ p ms ms'.
match ms with
| VMS _ s m -> ms' = VMS (p + len) (push (aeval m a ) s) m
end
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' =
match ms with
| VMS _ s m -> ms' = VMS (p + len) (push (aeval m a ) s) m
end
meta rewrite prop aexpr_post_lemma
function aexpr_pre : pos -> machine_state -> bool = \p ms.
match ms with
| VMS p' _ _ -> p = p'
end
let rec compile_aexpr (a : aexpr) : hl
variant { a }
ensures { result.pre = aexpr_pre }
ensures { result.pre = trivial_pre }
ensures { result.post = aexpr_post a result.code.length }
ensures {hl_correctness result}
ensures { hl_correctness result}
= let c = match a with
| Anum n -> absurd (* iconst n *)
| Avar x -> absurd (* ivar x *)
| Aadd a1 a2 ->
!! (compile_aexpr a1) ~ !! (compile_aexpr a2) ~ !! (iaddf ())
| Asub a1 a2 -> absurd (* compile_aexpr a1 ~ compile_aexpr a2 ~ isubf () *)
| Amul a1 a2 -> absurd (* compile_aexpr a1 ~ compile_aexpr a2 ~ imulf () *)
end in
let ghost pre = aexpr_pre in
let ghost post = any pos -> machine_state -> pred
ensures { result = aexpr_post a c.wcode.length } in
hoare pre c post
| 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
let ghost pre = trivial_pre in
let ghost post =
any pos -> post ensures { result = aexpr_post a c.wcode.length }
in hoare pre c post
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') *)
\ No newline at end of file
examples/in_progress/mini-compiler/vm.mlw
View file @ 92211e8b
......@@ -81,8 +81,8 @@ theory Vm "Virtual Machine for IMP language"
| Iconst int (* push n on stack *)
| Ivar id (* push the value of variable *)
| Isetvar id (* pop an integer, assign it to variable *)
| Ibranch_fwd pos (* skip ofs instructions forward *)
| Ibranch_bwd pos (* skip ofs instructions backward *)
| Ibranch pos (* skip ofs instructions *)
(*| Ibranch_bwd pos (* skip ofs instructions backward *)*)
| Iadd (* pop two values, push their sum *)
| Isub (* pop two values, push their difference *)
| Imul (* pop two values, push their product *)
......@@ -123,8 +123,8 @@ theory Vm "Virtual Machine for IMP language"
function ible (ofs:int) : code = Cons (Ible ofs) Nil
function ibne (ofs:int) : code = Cons (Ibne ofs) Nil
function ibgt (ofs:int) : code = Cons (Ibgt ofs) Nil
function ibranchf (ofs: int) : code = Cons (Ibranch_fwd ofs) Nil
function ibranchb (ofs: int) : code = Cons (Ibranch_bwd ofs) Nil
function ibranch (ofs: int) : code = Cons (Ibranch ofs) Nil
(*function ibranchb (ofs: int) : code = Cons (Ibranch_bwd ofs) Nil*)
constant ihalt : code = (Cons Ihalt Nil)
(* The semantics of the virtual machine is given in small-step style,
......@@ -221,21 +221,21 @@ theory Vm "Virtual Machine for IMP language"
(VMS p2 s m)
| trans_branch_fwd:
| trans_branch:
forall c: code, p ofs: pos.
codeseq_at c p (ibranchf ofs) ->
codeseq_at c p (ibranch ofs) ->
forall m: state, s: stack.
transition c
(VMS p s m)
(VMS (p + 1 + ofs) s m)
| trans_branch_bwd:
(* | trans_branch_bwd:
forall c: code, p ofs: pos.
codeseq_at c p (ibranchb ofs) ->
forall m: state, s: stack.
transition c
(VMS p s m)
(VMS (p + 1 - ofs) s m)
(VMS (p + 1 - ofs) s m) *)
......
examples/in_progress/mini-compiler/vm/why3session.xml
View file @ 92211e8b
......@@ -6,28 +6,28 @@
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="2" name="Vampire" version="0.6" timelimit="5" memlimit="1000"/>
<file name="../vm.mlw" expanded="true">
<theory name="ReflTransClosure" expanded="true">
<goal name="transZero" sum="5f576931016c6e98a82af4eb636fe96b" expanded="true">
<theory name="ReflTransClosure" sum="858a40c1dde55e8befdaee8ae005e423">
<goal name="transZero">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="transOne" sum="82b3748ce6112311cfc4ad0fed4a6acb">
<goal name="transOne">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="transition_star_one" sum="38add69295b2304d8481416ed2bc245d">
<goal name="transition_star_one">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter trans_star" expl="VC for trans_star" sum="810b09de5d400a18ebdbff965c9e4a3b">
<goal name="WP_parameter trans_star" expl="VC for trans_star">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="transition_star_transitive" sum="4e21189c07ea29a045e6b2320a077ab7">
<goal name="transition_star_transitive">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="Vm" expanded="true">
<goal name="codeseq_at_app_right" sum="0b8a571ad0b8d9ed101bbce6ac5b93ed" expanded="true">
<theory name="Vm" sum="030cc7eb9172e9aca56370af11cf7236" expanded="true">
<goal name="codeseq_at_app_right">
<proof prover="2"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="codeseq_at_app_left" sum="43d50744644159935e1cbb0a6447b570" expanded="true">
<goal name="codeseq_at_app_left">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
......
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