Module MBAexpr

Require Export Integers.
Require Import Coqlib.
Require Import Coq.Program.Wf.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import BooleanDecomposition.
Require Import BooleanSemanticTable.

Opaque Z.mul.

Definition of a Mixed Boolean-Arithmetic expression type

Inductive Bexpr : Type :=
| Zero : Bexpr
| MOne : Bexpr
| X : Bexpr
| Y : Bexpr
| And : Bexpr -> Bexpr -> Bexpr
| Or : Bexpr -> Bexpr -> Bexpr
| Xor : Bexpr -> Bexpr -> Bexpr
| Not : Bexpr -> Bexpr.

Inductive MBAexpr : Type :=
| Mul : Z -> Bexpr -> MBAexpr
| Add : MBAexpr -> MBAexpr -> MBAexpr.


First semantics of MBAexpr : transform a MBAexpr into a function.

Fixpoint Bexpr_to_Z (bex: Bexpr) : Z -> Z -> Z :=
  match bex with
  | Zero => fun x y => 0
  | MOne => fun x y => (-1)
  | X => fun x y => x
  | Y => fun x y => y
  | And bex1 bex2 => fun x y => Z.land (Bexpr_to_Z bex1 x y) (Bexpr_to_Z bex2 x y)
  | Or bex1 bex2 => fun x y => Z.lor (Bexpr_to_Z bex1 x y) (Bexpr_to_Z bex2 x y)
  | Xor bex1 bex2 => fun x y => Z.lxor (Bexpr_to_Z bex1 x y) (Bexpr_to_Z bex2 x y)
  | Not bex' => fun x y => Z.lnot (Bexpr_to_Z bex' x y)
  end.

Fixpoint MBAexpr_to_Z (mba: MBAexpr) : Z -> Z -> Z :=
  match mba with
  | Mul z bex => fun x y => Z.mul z (Bexpr_to_Z bex x y)
  | Add mba1 mba2 => fun x y => Z.add (MBAexpr_to_Z mba1 x y) (MBAexpr_to_Z mba2 x y)
  end.



Fixpoint Bexpr_to_Int (bex: Bexpr) : int -> int -> int :=
  match bex with
  | Zero => fun x y => Int.repr 0
  | MOne => fun x y => Int.repr (-1)
  | X => fun x y => x
  | Y => fun x y => y
  | And bex1 bex2 => fun x y => Int.and (Bexpr_to_Int bex1 x y) (Bexpr_to_Int bex2 x y)
  | Or bex1 bex2 => fun x y => Int.or (Bexpr_to_Int bex1 x y) (Bexpr_to_Int bex2 x y)
  | Xor bex1 bex2 => fun x y => Int.xor (Bexpr_to_Int bex1 x y) (Bexpr_to_Int bex2 x y)
  | Not bex' => fun x y => Int.not (Bexpr_to_Int bex' x y)
  end.

Fixpoint MBAexpr_to_Int (mba: MBAexpr) : int -> int -> int :=
  match mba with
  | Mul z bex => fun x y => Int.mul (Int.repr z) (Bexpr_to_Int bex x y)
  | Add mba1 mba2 => fun x y => Int.add (MBAexpr_to_Int mba1 x y) (MBAexpr_to_Int mba2 x y)
  end.

Second semantics of MBAexpr : transform a MBAexpr into a truth table.

Fixpoint Bexpr_to_TT (bex: Bexpr) : TT :=
  match bex with
  | Zero => fun xb yb => false
  | MOne => fun xb yb => true
  | X => fun xb yb => xb
  | Y => fun xb yb => yb
  | And bex1 bex2 => TT_and (Bexpr_to_TT bex1) (Bexpr_to_TT bex2)
  | Or bex1 bex2 => TT_or (Bexpr_to_TT bex1) (Bexpr_to_TT bex2)
  | Xor bex1 bex2 => TT_xor (Bexpr_to_TT bex1) (Bexpr_to_TT bex2)
  | Not bex' => TT_not (Bexpr_to_TT bex')
  end.

Fixpoint MBAexpr_to_BST (mba: MBAexpr) : BST Z :=
  match mba with
  | Mul z bex => BST_unop (fun x => z * Z.b2z x) (Bexpr_to_TT bex)
  | Add mba1 mba2 => BST_add (MBAexpr_to_BST mba1) (MBAexpr_to_BST mba2)
  end.

Definition of equivalence relations for MBAexpr.

Definition MBA_equiv_BST (mba1 mba2: MBAexpr) :=
  forall xb yb, MBAexpr_to_BST mba1 xb yb = MBAexpr_to_BST mba2 xb yb.

Definition MBA_equiv_Z (mba1 mba2: MBAexpr) :=
  MBAexpr_to_Z mba1 = MBAexpr_to_Z mba2.

Definition MBA_equiv_Z_modulo (n: Z) (mba1 mba2: MBAexpr) :=
  forall x y, (MBAexpr_to_Z mba1 x y) mod n = (MBAexpr_to_Z mba2 x y) mod n.

Definition MBA_equiv_Int (mba1 mba2: MBAexpr) :=
  MBAexpr_to_Int mba1 = MBAexpr_to_Int mba2.

Notation "A <==BST==> B" := (MBA_equiv_BST A B) (at level 80, right associativity).
Notation "A <==Z==> B" := (MBA_equiv_Z A B) (at level 80, right associativity).
Notation "A <==Z/ N Z==> B " := (MBA_equiv_Z_modulo N A B) (at level 80, right associativity).
Notation "A <==I==> B" := (MBA_equiv_Int A B) (at level 80, right associativity).

Specification of MBAexpr_to_BST

Lemma Bexpr_to_TT_spec_aux:
  forall (bex: Bexpr),
    (forall (xb yb : bool) (x y : Z),
        Bexpr_to_Z bex (2 * x + Z.b2z xb) (2 * y + Z.b2z yb) =
        2 * Bexpr_to_Z bex x y + Bexpr_to_Z bex (0 + Z.b2z xb) (0 + Z.b2z yb) -
                                 2 * Bexpr_to_Z bex 0 0) /\
    (forall xb yb : bool,
        Bexpr_to_Z bex (0 + Z.b2z xb) (0 + Z.b2z yb) =
        2 * Bexpr_to_Z bex 0 0 + Z.b2z (Bexpr_to_TT bex xb yb)).
Proof.
  intros bex.
  
  assert(Hswap: forall a b c, a + (b + c) - b = a + c) by (intros; omega).
  induction bex.
  - split; auto.
  - split; auto.
  - split; intros; simpl; omega.
  - split; intros; simpl; omega.
  - destruct IHbex1 as [IHbex1_local IHbex1_BST].
    destruct IHbex2 as [IHbex2_local IHbex2_BST].
    simpl in *.
    split.
    + intros.
      specialize (IHbex1_BST xb yb).
      specialize (IHbex2_BST xb yb).
      rewrite IHbex1_BST.
      rewrite IHbex2_BST.
      bool_decomp.
      rewrite Hswap.
      rewrite <- and_decomp.
      rewrite IHbex1_local.
      rewrite IHbex2_local.
      f_equal; omega.
    + intros.
      unfold TT_and.
      unfold BST_binop.
      rewrite <- and_decomp.
      f_equal; auto.
  - destruct IHbex1 as [IHbex1_local IHbex1_BST].
    destruct IHbex2 as [IHbex2_local IHbex2_BST].
    simpl in *.
    split.
    + intros.
      specialize (IHbex1_BST xb yb).
      specialize (IHbex2_BST xb yb).
      rewrite IHbex1_BST.
      rewrite IHbex2_BST.
      bool_decomp.
      rewrite Hswap.
      rewrite <- or_decomp.
      rewrite IHbex1_local.
      rewrite IHbex2_local.
      f_equal; omega.
    + intros.
      unfold TT_or.
      unfold BST_binop.
      rewrite <- or_decomp.
      f_equal; auto.
  - destruct IHbex1 as [IHbex1_local IHbex1_BST].
    destruct IHbex2 as [IHbex2_local IHbex2_BST].
    simpl in *.
    split.
    + intros.
      specialize (IHbex1_BST xb yb).
      specialize (IHbex2_BST xb yb).
      rewrite IHbex1_BST.
      rewrite IHbex2_BST.
      bool_decomp.
      rewrite Hswap.
      rewrite <- xor_decomp.
      rewrite IHbex1_local.
      rewrite IHbex2_local.
      f_equal; omega.
    + intros.
      unfold TT_xor.
      unfold BST_binop.
      rewrite <- xor_decomp.
      f_equal; auto.
  - destruct IHbex as [IHbex_local IHbex_BST].
    simpl in *.
    split.
    + intros.
      specialize (IHbex_BST xb yb).
      rewrite IHbex_BST.
      bool_decomp.
      rewrite Hswap.
      rewrite <- not_decomp.
      rewrite IHbex_local.
      f_equal; omega.
    + intros.
      unfold TT_not.
      unfold BST_unop.
      rewrite <- not_decomp.
      f_equal; auto.
Qed.




Theorem Bexpr_to_TT_spec:
  forall (bex: Bexpr), isLocal (Bexpr_to_Z bex) /\
                         BST_unop Z.b2z (Bexpr_to_TT bex) =
                         BST_of_local (Bexpr_to_Z bex).
Proof.
  intros bex.
  unfold BST_unop.
  unfold BST_of_local.
  unfold isLocal.
  unfold T.
  unfold isConstant.
  split.
  - intros xb yb x y.
    replace (2 * 0) with 0 by omega.
    pose proof (Bexpr_to_TT_spec_aux bex) as [H _].
    specialize (H xb yb x y).
    simpl in *.
    omega.
  - apply functional_extensionality; intros xb.
    apply functional_extensionality; intros yb.
    replace (2 * 0) with 0 by omega.
    pose proof (Bexpr_to_TT_spec_aux bex) as [_ H].
    specialize (H xb yb).
    simpl in *.
    omega.
Qed.


Theorem MBAexpr_to_BST_spec:
  forall (mba: MBAexpr), isLocal (MBAexpr_to_Z mba) /\
                         MBAexpr_to_BST mba =
                         BST_of_local (MBAexpr_to_Z mba).
Proof.
  intros mba.
  split.
  - intros xb yb x y.
    induction mba; simpl.
    + pose proof Bexpr_to_TT_spec b as [Hlocal _].
      specialize (Hlocal xb yb x y).
      unfold T in *.
      replace (2 * 0) with 0 in * by omega.
      simpl in *.
      rewrite !(Z.mul_shuffle3 2 z).
      rewrite <- !Z.mul_sub_distr_l.
      rewrite Hlocal.
      reflexivity.
    + unfold T in *.
      omega.
  - induction mba; simpl.
    + rewrite BST_of_local_homogeneity; auto.
      unfold BST_mul.
      pose proof Bexpr_to_TT_spec b as [_ HBST].
      rewrite <- HBST.
      auto.
    + rewrite BST_of_local_additivity; auto.
      rewrite IHmba1, IHmba2.
      auto.
Qed.

Specification of MBAexpr_to_Int

Theorem Bexpr_to_Int_spec : forall (b: Bexpr) (x y: int),
    Bexpr_to_Int b x y = Int.repr (Bexpr_to_Z b (Int.unsigned x) (Int.unsigned y) mod Int.modulus).
Proof.
  intros b x y.

  induction b; simpl; Int.bit_solve;
    try (rewrite IHb1, IHb2);
    try (rewrite IHb);
    replace Int.modulus with (2^Int.zwordsize) by auto;
    rewrite !Int.testbit_repr; auto;
      rewrite !Z.mod_pow2_bits_low; try omega;
        symmetry.
  - apply Int.Ztestbit_m1. omega.
  - reflexivity.
  - reflexivity.
  - apply Z.land_spec.
  - apply Z.lor_spec.
  - apply Z.lxor_spec.
  - apply Z.lnot_spec.
    omega.
Qed.

Lemma Inteq_eq : forall x y: int,
    Int.eq x y = true -> x = y.
Proof.
  intros x y.
  intros H1.
  pose proof Int.eq_spec x y as H2.
  rewrite H1 in H2.
  apply H2.
Qed.

Theorem MBAexpr_to_Int_spec : forall (mba: MBAexpr) (x y: int),
    MBAexpr_to_Int mba x y = Int.repr ((MBAexpr_to_Z mba (Int.unsigned x) (Int.unsigned y)) mod Int.modulus).
Proof.
  intros mba x y.

  assert(H: Int.modulus > 0).
  { apply two_power_nat_pos. }
  
  induction mba; simpl.
  - rewrite Bexpr_to_Int_spec.
    apply Inteq_eq.
    unfold Int.eq.
    unfold Int.mul.
    rewrite !Int.unsigned_repr_eq.
    rewrite <- !Zmult_mod.
    rewrite Z.mul_mod_idemp_r; try omega.
    rewrite !Z.mod_mod; try omega.
    apply zeq_true.
  - rewrite IHmba1, IHmba2.
    apply Inteq_eq.
    unfold Int.eq.
    unfold Int.add.
    rewrite !Int.unsigned_repr_eq.
    rewrite <- !Zdiv.Zplus_mod.
    rewrite Z.mod_mod; try omega.
    apply zeq_true.
Qed.

Proofs of implications between equivalence relations.

Theorem MBA_equiv_BST_to_Z: forall (mba1 mba2: MBAexpr),
    mba1 <==BST==> mba2 -> mba1 <==Z==> mba2.
Proof.
  unfold MBA_equiv_Z.
  unfold MBA_equiv_BST.
  intros mba1 mba2 H.
  apply BST_of_local_injective.
  - apply MBAexpr_to_BST_spec.
  - apply MBAexpr_to_BST_spec.
  - pose proof MBAexpr_to_BST_spec mba1 as [_ HBST1].
    pose proof MBAexpr_to_BST_spec mba2 as [_ HBST2].
    rewrite <- HBST1.
    apply functional_extensionality.
    intros xb.
    apply functional_extensionality.
    intros yb.
    rewrite H.
    rewrite HBST2.
    reflexivity.
Qed.

Theorem MBA_equiv_Z_to_BST: forall (mba1 mba2: MBAexpr),
    mba1 <==Z==> mba2 -> mba1 <==BST==> mba2.
Proof.
  intros mba1 mba2 H x y.
  pose proof MBAexpr_to_BST_spec mba1 as [_ HBST1].
  pose proof MBAexpr_to_BST_spec mba2 as [_ HBST2].
  rewrite HBST1, HBST2.
  rewrite H.
  reflexivity.
Qed.

Theorem MBA_equiv_Z_to_Z_modulo : forall mba1 mba2 n,
    mba1 <==Z==> mba2 -> mba1 <==Z/ n Z==> mba2.
Proof.
  intros mba1 mba2 n.
  intros H.
  intros x y.
  unfold MBA_equiv_Z in H.
  rewrite H.
  reflexivity.
Qed.

Theorem MBA_equiv_Z_modulo_to_Int : forall mba1 mba2,
    mba1 <==Z/(Int.modulus)Z==> mba2 -> mba1 <==I==> mba2.
Proof.
  intros mba1 mba2.
  intros H.
  apply functional_extensionality.
  intros y.
  apply functional_extensionality.
  intros x.
  rewrite !MBAexpr_to_Int_spec.
  rewrite H.
  reflexivity.
Qed.


Theorem MBA_equiv_Z_to_Int : forall mba1 mba2,
    mba1 <==Z==> mba2 -> mba1 <==I==> mba2.
Proof.
  intros mba1 mba2 H.
  apply MBA_equiv_Z_modulo_to_Int.
  apply MBA_equiv_Z_to_Z_modulo.
  auto.
Qed.


Theorem MBA_equiv_BST_to_Int : forall mba1 mba2,
    mba1 <==BST==> mba2 -> mba1 <==I==> mba2.
Proof.
  intros mba1 mba2 H; apply MBA_equiv_Z_to_Int.
  apply MBA_equiv_BST_to_Z; auto.
Qed.




Generated by coq2html