Module MBAtoClight

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.

  intros ge e le m bex x y.
  intros valx valy Htx Hty Hx Hy.
  induction bex; simpl.
  - constructor.
  - constructor.
  - apply Hx.
  - apply Hy.
  - apply eval_Ebinop with (Vint (Bexpr_to_Int bex1 valx valy))
                           (Vint (Bexpr_to_Int bex2 valx valy)).
    + apply IHbex1.
    + apply IHbex2.
    + rewrite !Bexpr_to_expr_typeof; auto.
  - apply eval_Ebinop with (Vint (Bexpr_to_Int bex1 valx valy))
                           (Vint (Bexpr_to_Int bex2 valx valy)).
    + apply IHbex1.
    + apply IHbex2.
    + rewrite !Bexpr_to_expr_typeof; auto.
  - apply eval_Ebinop with (Vint (Bexpr_to_Int bex1 valx valy))
                           (Vint (Bexpr_to_Int bex2 valx valy)).
    + apply IHbex1.
    + apply IHbex2.
    + rewrite !Bexpr_to_expr_typeof; auto.
  - apply eval_Eunop with (Vint (Bexpr_to_Int bex valx valy)).
    + apply IHbex.
    + rewrite !Bexpr_to_expr_typeof; auto.
Qed.

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.

  intros ge e le m mba x y.
  intros valx valy Htx Hty Hx Hy.
  induction mba; simpl.
  - apply eval_Ebinop with (Vint (Int.repr z))
                           (Vint (Bexpr_to_Int b valx valy)).
    + apply eval_Econst_int.
    + apply Bexpr_to_expr_spec; auto.
    + rewrite !Bexpr_to_expr_typeof; auto.

  - apply eval_Ebinop with (Vint (MBAexpr_to_Int mba1 valx valy))
                           (Vint (MBAexpr_to_Int mba2 valx valy)).
    + apply IHmba1.
    + apply IHmba2.
    + rewrite !MBAexpr_to_expr_typeof; auto.
Qed.

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.

  intros mba1 mba2 H.
  intros ge e le m.
  intros x y valx valy val1 val2.
  intros Htx Hty Hx Hy H1 H2.

  pose proof MBAexpr_to_expr_spec _ _ _ _ mba1 _ _ _ _ Htx Hty Hx Hy as H1'.
  pose proof MBAexpr_to_expr_spec _ _ _ _ mba2 _ _ _ _ Htx Hty Hx Hy as H2'.

  pose proof eval_expr_determ _ _ _ _ _ _ _ H1 H1' as Hv1.
  pose proof eval_expr_determ _ _ _ _ _ _ _ H2 H2' as Hv2.
  inversion Hv1.
  inversion Hv2.

  apply MBA_equiv_BST_to_Int in H.
  unfold MBA_equiv_Int in H.
  rewrite H.
  reflexivity.
Qed.

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.

  intros mba1 mba2 H.
  intros ge e le m.
  intros x y valx valy v.
  intros Htx Hty Hx Hy H1.

  pose proof MBAexpr_to_expr_spec _ _ _ _ mba1 _ _ _ _ Htx Hty Hx Hy as H1'.
  pose proof MBAexpr_to_expr_spec _ _ _ _ mba2 _ _ _ _ Htx Hty Hx Hy as H2'.

  pose proof eval_expr_determ _ _ _ _ _ _ _ H1 H1' as Hv1.
  rewrite Hv1.

  apply MBA_equiv_BST_to_Int in H.
  unfold MBA_equiv_Int in H.
  rewrite H.
  apply H2'.
Qed.