Link between MBAexpr and Clight expressions
Require Import Clight.
Require Import Cop.
Require Import Ctypes.
Require Import Values.
Require Export Coqlib.
Require Import EvalDeterminism.
Require Import MBAexpr.
Transform a MBAexpr into a Clight expression
Fixpoint Bexpr_to_expr (
bex:
Bexpr) (
x y:
expr)
t :
expr :=
match bex with
|
Zero =>
Econst_int (
Int.repr 0)
t
|
MOne =>
Econst_int (
Int.repr (-1))
t
|
X =>
x
|
Y =>
y
|
And bex1 bex2 =>
Ebinop Oand (
Bexpr_to_expr bex1 x y t) (
Bexpr_to_expr bex2 x y t)
t
|
Or bex1 bex2 =>
Ebinop Oor (
Bexpr_to_expr bex1 x y t) (
Bexpr_to_expr bex2 x y t)
t
|
Xor bex1 bex2 =>
Ebinop Oxor (
Bexpr_to_expr bex1 x y t) (
Bexpr_to_expr bex2 x y t)
t
|
Not bex' =>
Eunop Onotint (
Bexpr_to_expr bex'
x y t)
t
end.
Fixpoint MBAexpr_to_expr (
mba:
MBAexpr) (
x y:
expr)
t :
expr :=
match mba with
|
Mul z bex =>
Ebinop Omul (
Econst_int (
Int.repr z)
type_int32s) (
Bexpr_to_expr bex x y t)
t
|
Add mba1 mba2 =>
Ebinop Oadd (
MBAexpr_to_expr mba1 x y t) (
MBAexpr_to_expr mba2 x y t)
t
end.
Preservation of types
Lemma Bexpr_to_expr_typeof:
forall bex x y t,
typeof x =
t ->
typeof y =
t ->
typeof (
Bexpr_to_expr bex x y t) =
t.
Proof.
intros bex x y t Htx Hty.
induction bex; auto.
Qed.
Lemma MBAexpr_to_expr_typeof:
forall mba x y t,
typeof x =
t ->
typeof y =
t ->
typeof (
MBAexpr_to_expr mba x y t) =
t.
Proof.
intros mba x y t Htx Hty.
induction mba; auto.
Qed.
Specification of the transformation
Theorem Bexpr_to_expr_spec :
forall (
ge :
genv) (
e :
env) (
le :
temp_env) (
m :
Memory.Mem.mem),
forall (
bex:
Bexpr) (
x y:
expr),
forall valx valy,
typeof x =
type_int32s ->
typeof y =
type_int32s ->
eval_expr ge e le m x (
Vint valx) ->
eval_expr ge e le m y (
Vint valy) ->
eval_expr ge e le m (
Bexpr_to_expr bex x y type_int32s) (
Vint (
Bexpr_to_Int bex valx valy)).
Proof.
Theorem MBAexpr_to_expr_spec :
forall (
ge :
genv) (
e :
env) (
le :
temp_env) (
m :
Memory.Mem.mem),
forall (
mba:
MBAexpr) (
x y:
expr),
forall valx valy,
typeof x =
type_int32s ->
typeof y =
type_int32s ->
eval_expr ge e le m x (
Vint valx) ->
eval_expr ge e le m y (
Vint valy) ->
eval_expr ge e le m (
MBAexpr_to_expr mba x y type_int32s) (
Vint (
MBAexpr_to_Int mba valx valy)).
Proof.
Theorem MBAexpr_to_expr_spec' :
forall (
ge :
genv) (
e :
env) (
le :
temp_env) (
m :
Memory.Mem.mem),
forall (
mba:
MBAexpr) (
x y:
expr),
forall valx valy v,
typeof x =
type_int32s ->
typeof y =
type_int32s ->
eval_expr ge e le m x (
Vint valx) ->
eval_expr ge e le m y (
Vint valy) ->
v = (
MBAexpr_to_Int mba valx valy) ->
eval_expr ge e le m (
MBAexpr_to_expr mba x y type_int32s) (
Vint v).
Proof.
intros ge e le m mba x y.
intros valx valy v Htx Hty Hx Hy Hv.
rewrite Hv.
apply MBAexpr_to_expr_spec;
auto.
Qed.
Link with the equivalence relation over truth tables
Theorem MBA_equiv_BST_to_expr :
forall mba1 mba2,
mba1 <==
BST==>
mba2 ->
forall (
ge :
genv) (
e :
env) (
le :
temp_env) (
m :
Memory.Mem.mem),
forall x y valx valy val1 val2,
typeof x =
type_int32s ->
typeof y =
type_int32s ->
eval_expr ge e le m x (
Vint valx) ->
eval_expr ge e le m y (
Vint valy) ->
eval_expr ge e le m (
MBAexpr_to_expr mba1 x y type_int32s) (
Vint val1) ->
eval_expr ge e le m (
MBAexpr_to_expr mba2 x y type_int32s) (
Vint val2) ->
val1 =
val2.
Proof.
Theorem MBA_equiv_BST_to_expr' :
forall mba1 mba2,
mba1 <==
BST==>
mba2 ->
forall (
ge :
genv) (
e :
env) (
le :
temp_env) (
m :
Memory.Mem.mem),
forall x y valx valy v,
typeof x =
type_int32s ->
typeof y =
type_int32s ->
eval_expr ge e le m x (
Vint valx) ->
eval_expr ge e le m y (
Vint valy) ->
eval_expr ge e le m (
MBAexpr_to_expr mba1 x y type_int32s) (
Vint v) ->
eval_expr ge e le m (
MBAexpr_to_expr mba2 x y type_int32s) (
Vint v).
Proof.