Commit 43b24a6b authored by Léon Gondelman's avatar Léon Gondelman
Browse files

(WIP) mini-compiler proof in progress

parent 05c13646
module Compiler_logic
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 state.State
use import HighOrd
type pred = machine_state -> bool
type post = machine_state -> pred
(* Hoare triples with explicit pre & post *)
type codespec =
{ code: code;
ghost pre : pos -> pred;
ghost post: pos -> post }
(* Weakest Precondition Calculus *)
type wp =
{ wcode : code;
ghost wp : pos -> pred -> pred }
(*
function offset (ms : machine_state) (ofs: pos) : machine_state
= match ms
with (VMS p s m) -> (VMS (p + ofs) s m) end *)
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
predicate total_correctness (cs : codespec) =
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'
predicate transformer (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'
function seq_wp (s1 s2: wp) : pos -> pred -> pred =
\p q. s1.wp p (s2.wp (p + s1.wcode.length) q)
let (~) (s1 s2 : wp) : wp
requires { transformer s1 /\ transformer s2 }
ensures { transformer result }
ensures { result.wp = seq_wp s1 s2 }
ensures { result.wcode.length = s1.wcode.length + s2.wcode.length }
= 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
};
res
function towp_wp (c : codespec) : pos -> pred -> pred =
\p q ms. c.pre p ms && (forall ms'. c.post p ms ms' -> q ms')
let (!!) (c: codespec) : wp
requires { total_correctness c }
ensures { transformer 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 hoare (ghost pre: pos -> pred) (c: wp)
(ghost post: pos -> machine_state -> pred) : codespec
requires { transformer c }
requires { forall p ms. pre p ms -> (c.wp p (post p ms)) ms }
ensures { result.code = c.wcode }
ensures { total_correctness result }
ensures { result.pre = pre /\ result.post = post }
= { code = c.wcode ; pre = pre; post = post }
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 =
\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
let iaddf () : codespec
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 { total_correctness result }
= let res = {code = Cons Iadd Nil; pre = ibinop_pre ; post = iadd_post } 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 &&
let ms' = VMS (p+1) (push (n1 + n2) s) m in
contextual_irrelevance res.code p ms ms' && false
| _ -> false end && false };
res
end
(*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 state.State
use import Compiler_logic
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
function aexpr_pre : pos -> machine_state -> bool = \p ms.
match ms with
| VMS p' _ _ -> p = p'
end
let rec compile_aexpr (a : aexpr) : codespec
variant { a }
ensures { result.pre = aexpr_pre }
ensures { result.post = aexpr_post a result.code.length }
ensures {total_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
end
(* *)
\ No newline at end of file
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require list.List.
Require list.Length.
Require list.Mem.
Require map.Map.
Require bool.Bool.
Require list.Append.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
Axiom map : forall (a:Type) (b:Type), Type.
Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((get (set m a1 b1) a2) = b1).
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1: (map a b)) a1) = b1).
(* Why3 assumption *)
Inductive id :=
| Id : Z -> id.
Axiom id_WhyType : WhyType id.
Existing Instance id_WhyType.
(* Why3 assumption *)
Definition state := (map id Z).
(* Why3 assumption *)
Inductive aexpr :=
| Anum : Z -> aexpr
| Avar : id -> aexpr
| Aadd : aexpr -> aexpr -> aexpr
| Asub : aexpr -> aexpr -> aexpr
| Amul : aexpr -> aexpr -> aexpr.
Axiom aexpr_WhyType : WhyType aexpr.
Existing Instance aexpr_WhyType.
(* Why3 assumption *)
Inductive bexpr :=
| Btrue : bexpr
| Bfalse : bexpr
| Band : bexpr -> bexpr -> bexpr
| Bnot : bexpr -> bexpr
| Beq : aexpr -> aexpr -> bexpr
| Ble : aexpr -> aexpr -> bexpr.
Axiom bexpr_WhyType : WhyType bexpr.
Existing Instance bexpr_WhyType.
(* Why3 assumption *)
Inductive com :=
| Cskip : com
| Cassign : id -> aexpr -> com
| Cseq : com -> com -> com
| Cif : bexpr -> com -> com -> com
| Cwhile : bexpr -> com -> com.
Axiom com_WhyType : WhyType com.
Existing Instance com_WhyType.
(* Why3 assumption *)
Fixpoint aeval (st:(map id Z)) (e:aexpr) {struct e}: Z :=
match e with
| (Anum n) => n
| (Avar x) => (get st x)
| (Aadd e1 e2) => ((aeval st e1) + (aeval st e2))%Z
| (Asub e1 e2) => ((aeval st e1) - (aeval st e2))%Z
| (Amul e1 e2) => ((aeval st e1) * (aeval st e2))%Z
end.
Parameter beval: (map id Z) -> bexpr -> bool.
Axiom beval_def : forall (st:(map id Z)) (b:bexpr),
match b with
| Btrue => ((beval st b) = true)
| Bfalse => ((beval st b) = false)
| (Bnot b') => ((beval st b) = (Init.Datatypes.negb (beval st b')))
| (Band b1 b2) => ((beval st b) = (Init.Datatypes.andb (beval st
b1) (beval st b2)))
| (Beq a1 a2) => (((aeval st a1) = (aeval st a2)) -> ((beval st
b) = true)) /\ ((~ ((aeval st a1) = (aeval st a2))) -> ((beval st
b) = false))
| (Ble a1 a2) => (((aeval st a1) <= (aeval st a2))%Z -> ((beval st
b) = true)) /\ ((~ ((aeval st a1) <= (aeval st a2))%Z) -> ((beval st
b) = false))
end.
Axiom inversion_beval_t : forall (a1:aexpr) (a2:aexpr) (m:(map id Z)),
((beval m (Beq a1 a2)) = true) -> ((aeval m a1) = (aeval m a2)).
Axiom inversion_beval_f : forall (a1:aexpr) (a2:aexpr) (m:(map id Z)),
((beval m (Beq a1 a2)) = false) -> ~ ((aeval m a1) = (aeval m a2)).
(* Why3 assumption *)
Inductive ceval: (map id Z) -> com -> (map id Z) -> Prop :=
| E_Skip : forall (m:(map id Z)), (ceval m Cskip m)
| E_Ass : forall (m:(map id Z)) (a:aexpr) (n:Z) (x:id), ((aeval m
a) = n) -> (ceval m (Cassign x a) (set m x n))
| E_Seq : forall (cmd1:com) (cmd2:com) (m0:(map id Z)) (m1:(map id Z))
(m2:(map id Z)), (ceval m0 cmd1 m1) -> ((ceval m1 cmd2 m2) -> (ceval m0
(Cseq cmd1 cmd2) m2))
| E_IfTrue : forall (m0:(map id Z)) (m1:(map id Z)) (cond:bexpr) (cmd1:com)
(cmd2:com), ((beval m0 cond) = true) -> ((ceval m0 cmd1 m1) -> (ceval
m0 (Cif cond cmd1 cmd2) m1))
| E_IfFalse : forall (m0:(map id Z)) (m1:(map id Z)) (cond:bexpr)
(cmd1:com) (cmd2:com), ((beval m0 cond) = false) -> ((ceval m0 cmd2
m1) -> (ceval m0 (Cif cond cmd1 cmd2) m1))
| E_WhileEnd : forall (cond:bexpr) (m:(map id Z)) (body:com), ((beval m
cond) = false) -> (ceval m (Cwhile cond body) m)
| E_WhileLoop : forall (mi:(map id Z)) (mj:(map id Z)) (mf:(map id Z))
(cond:bexpr) (body:com), ((beval mi cond) = true) -> ((ceval mi body
mj) -> ((ceval mj (Cwhile cond body) mf) -> (ceval mi (Cwhile cond
body) mf))).
(* Why3 assumption *)
Definition pos := Z.
(* Why3 assumption *)
Definition stack := (list Z).
(* Why3 assumption *)
Inductive machine_state :=
| VMS : Z -> (list Z) -> (map id Z) -> machine_state.
Axiom machine_state_WhyType : WhyType machine_state.
Existing Instance machine_state_WhyType.
(* Why3 assumption *)
Inductive instr :=
| Iconst : Z -> instr
| Ivar : id -> instr
| Isetvar : id -> instr
| Ibranch_fwd : Z -> instr
| Ibranch_bwd : Z -> instr
| Iadd : instr
| Isub : instr
| Imul : instr
| Ibeq : Z -> instr
| Ibne : Z -> instr
| Ible : Z -> instr
| Ibgt : Z -> instr
| Ihalt : instr.
Axiom instr_WhyType : WhyType instr.
Existing Instance instr_WhyType.
(* Why3 assumption *)
Definition code := (list instr).
(* Why3 assumption *)
Inductive codeseq_at: (list instr) -> Z -> (list instr) -> Prop :=
| codeseq_at_intro : forall (c1:(list instr)) (c2:(list instr))
(c3:(list instr)) (pc:Z), (pc = (list.Length.length c1)) -> (codeseq_at
(Init.Datatypes.app (Init.Datatypes.app c1 c2) c3) pc c2).
Axiom codeseq_at_app_right : forall (c:(list instr)) (c1:(list instr))
(c2:(list instr)) (p:Z), (codeseq_at c p (Init.Datatypes.app c1 c2)) ->
(codeseq_at c (p + (list.Length.length c1))%Z c2).
Axiom codeseq_at_app_left : forall (c:(list instr)) (c1:(list instr))
(c2:(list instr)) (p:Z), (codeseq_at c p (Init.Datatypes.app c1 c2)) ->
(codeseq_at c p c1).
(* Why3 assumption *)
Definition iconst (n:Z): (list instr) :=
(Init.Datatypes.cons (Iconst n) Init.Datatypes.nil).
(* Why3 assumption *)
Definition ivar (x:id): (list instr) :=
(Init.Datatypes.cons (Ivar x) Init.Datatypes.nil).
(* Why3 assumption *)
Definition isetvar (x:id): (list instr) :=
(Init.Datatypes.cons (Isetvar x) Init.Datatypes.nil).
(* Why3 assumption *)
Definition ibeq (ofs:Z): (list instr) :=
(Init.Datatypes.cons (Ibeq ofs) Init.Datatypes.nil).
(* Why3 assumption *)
Definition ible (ofs:Z): (list instr) :=
(Init.Datatypes.cons (Ible ofs) Init.Datatypes.nil).
(* Why3 assumption *)
Definition ibne (ofs:Z): (list instr) :=
(Init.Datatypes.cons (Ibne ofs) Init.Datatypes.nil).
(* Why3 assumption *)
Definition ibgt (ofs:Z): (list instr) :=
(Init.Datatypes.cons (Ibgt ofs) Init.Datatypes.nil).
(* Why3 assumption *)
Definition ibranchf (ofs:Z): (list instr) :=
(Init.Datatypes.cons (Ibranch_fwd ofs) Init.Datatypes.nil).
(* Why3 assumption *)
Definition ibranchb (ofs:Z): (list instr) :=
(Init.Datatypes.cons (Ibranch_bwd ofs) Init.Datatypes.nil).
(* Why3 assumption *)
Inductive transition: (list instr) -> machine_state -> machine_state ->
Prop :=
| trans_const : forall (c:(list instr)) (p:Z) (n:Z), (codeseq_at c p
(iconst n)) -> forall (m:(map id Z)) (s:(list Z)), (transition c (VMS p
s m) (VMS (p + 1%Z)%Z (Init.Datatypes.cons n s) m))
| trans_var : forall (c:(list instr)) (p:Z) (x:id), (codeseq_at c p
(ivar x)) -> forall (m:(map id Z)) (s:(list Z)), (transition c (VMS p s
m) (VMS (p + 1%Z)%Z (Init.Datatypes.cons (get m x) s) m))
| trans_set_var : forall (c:(list instr)) (p:Z) (s:(list Z)) (x:id),
(codeseq_at c p (isetvar x)) -> forall (n:Z) (m:(map id Z)),
(transition c (VMS p (Init.Datatypes.cons n s) m) (VMS (p + 1%Z)%Z s
(set m x n)))
| trans_add : forall (c:(list instr)) (p:Z), (codeseq_at c p
(Init.Datatypes.cons Iadd Init.Datatypes.nil)) -> forall (n1:Z) (n2:Z)
(s:(list Z)) (m:(map id Z)), (transition c (VMS p
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m) (VMS (p + 1%Z)%Z
(Init.Datatypes.cons (n1 + n2)%Z s) m))
| trans_sub : forall (c:(list instr)) (p:Z), (codeseq_at c p
(Init.Datatypes.cons Isub Init.Datatypes.nil)) -> forall (n1:Z) (n2:Z)
(s:(list Z)) (m:(map id Z)), (transition c (VMS p
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m) (VMS (p + 1%Z)%Z
(Init.Datatypes.cons (n1 - n2)%Z s) m))
| trans_mul : forall (c:(list instr)) (p:Z), (codeseq_at c p
(Init.Datatypes.cons Imul Init.Datatypes.nil)) -> forall (n1:Z) (n2:Z)
(s:(list Z)) (m:(map id Z)), (transition c (VMS p
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m) (VMS (p + 1%Z)%Z
(Init.Datatypes.cons (n1 * n2)%Z s) m))
| trans_beq : forall (c:(list instr)) (p1:Z) (p2:Z) (ofs:Z) (n1:Z) (n2:Z),
(codeseq_at c p1 (ibeq ofs)) -> ((((n1 = n2) /\
(p2 = ((p1 + 1%Z)%Z + ofs)%Z)) \/ ((~ (n1 = n2)) /\
(p2 = (p1 + 1%Z)%Z))) -> forall (s:(list Z)) (m:(map id Z)),
(transition c (VMS p1
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m) (VMS p2 s m)))
| trans_bne : forall (c:(list instr)) (p1:Z) (p2:Z) (ofs:Z) (n1:Z) (n2:Z),
(codeseq_at c p1 (ibne ofs)) -> ((((n1 = n2) /\ (p2 = (p1 + 1%Z)%Z)) \/
((~ (n1 = n2)) /\ (p2 = ((p1 + 1%Z)%Z + ofs)%Z))) ->
forall (s:(list Z)) (m:(map id Z)), (transition c (VMS p1
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m) (VMS p2 s m)))
| trans_ble : forall (c:(list instr)) (p1:Z) (p2:Z) (ofs:Z) (n1:Z) (n2:Z),
(codeseq_at c p1 (ible ofs)) -> ((((n1 <= n2)%Z /\
(p2 = ((p1 + 1%Z)%Z + ofs)%Z)) \/ ((~ (n1 <= n2)%Z) /\
(p2 = (p1 + 1%Z)%Z))) -> forall (s:(list Z)) (m:(map id Z)),
(transition c (VMS p1
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m) (VMS p2 s m)))
| trans_bgt : forall (c:(list instr)) (p1:Z) (p2:Z) (ofs:Z) (n1:Z) (n2:Z),
(codeseq_at c p1 (ibgt ofs)) -> ((((n1 <= n2)%Z /\
(p2 = (p1 + 1%Z)%Z)) \/ ((~ (n1 <= n2)%Z) /\
(p2 = ((p1 + 1%Z)%Z + ofs)%Z))) -> forall (s:(list Z)) (m:(map id Z)),
(transition c (VMS p1
(Init.Datatypes.cons n2 (Init.Datatypes.cons n1 s)) m) (VMS p2 s m)))
| trans_branch_fwd : forall (c:(list instr)) (p:Z) (ofs:Z), (codeseq_at c p
(ibranchf ofs)) -> forall (m:(map id Z)) (s:(list Z)), (transition c
(VMS p s m) (VMS ((p + 1%Z)%Z + ofs)%Z s m))
| trans_branch_bwd : forall (c:(list instr)) (p:Z) (ofs:Z), (codeseq_at c p
(ibranchb ofs)) -> forall (m:(map id Z)) (s:(list Z)), (transition c
(VMS p s m) (VMS ((p + 1%Z)%Z - ofs)%Z s m)).
(* Why3 assumption *)
Inductive trans :=
| TransZero : trans
| TransOne : machine_state -> trans -> trans.
Axiom trans_WhyType : WhyType trans.
Existing Instance trans_WhyType.
(* Why3 assumption *)
Fixpoint transition_star_proof (p:(list instr)) (s1:machine_state)
(s3:machine_state) (pi:trans) {struct pi}: Prop :=
match pi with
| TransZero => (s1 = s3)
| (TransOne s2 pi') => (transition p s1 s2) /\ (transition_star_proof p s2
s3 pi')
end.
Parameter transition_star: (list instr) -> machine_state -> machine_state ->
Prop.
Axiom transition_star_def : forall (p:(list instr)) (s1:machine_state)
(s3:machine_state), (transition_star p s1 s3) <-> exists pi:trans,
(transition_star_proof p s1 s3 pi).
Axiom transZero : forall (p:(list instr)) (s:machine_state), (transition_star
p s s).
Axiom transOne : forall (p:(list instr)) (s1:machine_state)
(s2:machine_state) (s3:machine_state), (transition p s1 s2) ->
((transition_star p s2 s3) -> (transition_star p s1 s3)).
Axiom transition_star_one : forall (p:(list instr)) (s1:machine_state)
(s2:machine_state), (transition p s1 s2) -> (transition_star p s1 s2).
Axiom trans_star : forall (p:(list instr)) (s1:machine_state)
(s2:machine_state) (s3:machine_state) (pi:trans), ((transition_star_proof p
s1 s2 pi) /\ (transition_star p s2 s3)) -> (transition_star p s1 s3).
Axiom transition_star_transitive : forall (p:(list instr)) (s1:machine_state)
(s2:machine_state) (s3:machine_state), (transition_star p s1 s2) ->
((transition_star p s2 s3) -> (transition_star p s1 s3)).
(* Why3 assumption *)
Definition vm_terminates (c:(list instr)) (mi:(map id Z)) (mf:(map id
Z)): Prop := exists p:Z, (codeseq_at c p
(Init.Datatypes.cons Ihalt Init.Datatypes.nil)) /\ (transition_star c
(VMS 0%Z Init.Datatypes.nil mi) (VMS p Init.Datatypes.nil mf)).
Axiom func : forall (a:Type) (b:Type), Type.
Parameter func_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (func a b).
Existing Instance func_WhyType.
(* Why3 assumption *)
Definition pred (a:Type) := (func a bool).
Parameter infix_at: forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, (func a b) -> a -> b.
(* Why3 assumption *)
Definition pred1 := (func machine_state bool).
(* Why3 assumption *)
Definition post := (func machine_state (func machine_state bool)).
(* Why3 assumption *)
Inductive codespec :=
| mk_codespec : (list instr) -> (func Z (func machine_state bool)) -> (func
Z (func machine_state (func machine_state bool))) -> codespec.
Axiom codespec_WhyType : WhyType codespec.
Existing Instance codespec_WhyType.
(* Why3 assumption *)
Definition post1 (v:codespec): (func Z (func machine_state (func
machine_state bool))) := match v with
| (mk_codespec x x1 x2) => x2
end.
(* Why3 assumption *)
Definition pre (v:codespec): (func Z (func machine_state bool)) :=
match v with
| (mk_codespec x x1 x2) => x1
end.
(* Why3 assumption *)
Definition code1 (v:codespec): (list instr) :=
match v with
| (mk_codespec x x1 x2) => x
end.
(* Why3 assumption *)
Inductive wp :=