Commit 253b4a7b authored by Léon Gondelman's avatar Léon Gondelman

mini-compiler:bisect

parent 13585337
(* 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.
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).
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
(* Why3 assumption *)
Inductive id :=
| Id : Z -> id.
Axiom id_WhyType : WhyType id.
Existing Instance id_WhyType.
(* 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.
(* 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))).
Axiom ceval_deterministic : forall (c:com) (mi:(map id Z)) (mf1:(map id Z))
(mf2:(map id Z)), (ceval mi c mf1) -> ((ceval mi c mf2) -> (mf1 = mf2)).
(* 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 : 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 *)
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).
Parameter transition_star: (list instr) -> machine_state -> machine_state ->
Prop.
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.
Parameter infix_at: forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, (func a b) -> a -> b.
(* Why3 assumption *)
Inductive hl
(a:Type) :=
| mk_hl : (list instr) -> (func a (func Z (func machine_state bool))) ->
(func a (func Z (func machine_state (func machine_state bool)))) -> hl
a.
Axiom hl_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (hl a).
Existing Instance hl_WhyType.
Implicit Arguments mk_hl [[a]].
(* Why3 assumption *)
Definition post {a:Type} {a_WT:WhyType a} (v:(hl a)): (func a (func Z (func
machine_state (func machine_state bool)))) :=
match v with
| (mk_hl x x1 x2) => x2
end.
(* Why3 assumption *)
Definition pre {a:Type} {a_WT:WhyType a} (v:(hl a)): (func a (func Z (func
machine_state bool))) := match v with
| (mk_hl x x1 x2) => x1
end.
(* Why3 assumption *)
Definition code {a:Type} {a_WT:WhyType a} (v:(hl a)): (list instr) :=
match v with
| (mk_hl x x1 x2) => x
end.
(* Why3 assumption *)
Definition contextual_irrelevance (c:(list instr)) (p:Z) (ms1:machine_state)
(ms2:machine_state): Prop := forall (c_global:(list instr)), (codeseq_at
c_global p c) -> (transition_star c_global ms1 ms2).
(* Why3 assumption *)
Definition hl_correctness {a:Type} {a_WT:WhyType a} (cs:(hl a)): Prop :=
forall (x:a) (p:Z) (ms:machine_state),
((infix_at (infix_at (infix_at (pre cs) x) p) ms) = true) ->
exists ms':machine_state,
((infix_at (infix_at (infix_at (infix_at (post cs) x) p) ms)
ms') = true) /\ (contextual_irrelevance (code cs) p ms ms').
Parameter com_pre: forall {a:Type} {a_WT:WhyType a}, com -> (func a (func Z
(func machine_state bool))).
Axiom com_pre_def : forall {a:Type} {a_WT:WhyType a}, forall (cmd:com) (x:a)
(p:Z) (ms:machine_state),
((infix_at (infix_at (infix_at (com_pre cmd: (func a (func Z (func
machine_state bool)))) x) p) ms) = true) <->
match ms with
| (VMS p' _ m) => (p = p') /\ exists m':(map id Z), (ceval m cmd m')
end.
Parameter com_post: forall {a:Type} {a_WT:WhyType a}, com -> Z -> (func a
(func Z (func machine_state (func machine_state bool)))).
Axiom com_post_def : forall {a:Type} {a_WT:WhyType a}, forall (cmd:com)
(len:Z) (x:a) (p:Z) (ms:machine_state) (ms':machine_state),
((infix_at (infix_at (infix_at (infix_at (com_post cmd len: (func a (func Z
(func machine_state (func machine_state bool))))) x) p) ms)
ms') = true) <-> match (ms,
ms') with
| ((VMS p1 s m), (VMS p' s' m')) => (p' = (p1 + len)%Z) /\ ((s' = s) /\
(ceval m cmd m'))
end.
(* Why3 goal *)
Theorem WP_parameter_compile_com_natural : forall (com1:com),
forall (res:(list instr)) (res1:(func unit (func Z (func machine_state
bool)))) (res2:(func unit (func Z (func machine_state (func machine_state
bool))))), ((res1 = (com_pre com1: (func unit (func Z (func machine_state
bool))))) /\ ((res2 = (com_post com1 (list.Length.length res): (func unit
(func Z (func machine_state (func machine_state bool)))))) /\
(hl_correctness (mk_hl res res1 res2)))) -> ((forall (p:Z) (s:(list Z))
(m:(map id Z)) (m':(map id Z)), (ceval m com1 m') ->
((infix_at (infix_at (infix_at res1 tt) p) (VMS p s m)) = true)) ->
forall (c:(list instr)) (p:Z) (s:(list Z)) (m:(map id Z)) (m':(map id Z)),
(ceval m com1 m') -> ((codeseq_at c p res) -> (transition_star c (VMS p s
m) (VMS (p + (list.Length.length res))%Z s m')))).
(* Why3 intros com1 res res1 res2 (h1,(h2,h3)) h4 c p s m m' h5 h6. *)
intros com1 res res1 res2 (h1,(h2,h3)) h4 c p s m m' h5 h6.
unfold hl_correctness in *.
remember h5 as h7 eqn:eqn;clear eqn.
apply (h4 p s) in h5.
apply h3 in h5.
Require Import Why3.
simpl in *.
subst.
destruct h5.
rewrite com_post_def in H.
why3 "Alt-Ergo,0.95.2,".
Qed.
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