Library Asm.Bitvector.BArith

Two's-complement arithmetic

Require Import Arith Bool Bvector ZArith.

Require Import Asm.Util.ArithUtil.
Require Import Asm.Util.Mod.
Require Import Asm.Util.Tactics.

Require Import Asm.Bitvector.Bitwise.
Require Import Asm.Bitvector.Convert.
Require Import Asm.Bitvector.Defs.
Require Import Asm.Bitvector.Tactics.

Set Implicit Arguments.

Preliminary definitions
Used to check for the absense of overflow
Inductive belowMax (len : nat) (v : Bvector len) (n : nat) : Prop :=
  | belowMax_rule :
    bvec_to_nat v < pow2 len - n
    -> belowMax v n.

Theorem belowMax_dec : forall len (v : Bvector len) n,
  belowMax v n
  -> forall m, m < n
    -> belowMax v m.

Hint Resolve belowMax_dec : asm.

Zero


Lemma bzero_btn : forall len,
  bvec_to_nat (bzero len) = 0.

Lemma bzero_neg : forall len,
  bneg (bzero len) = bzero len.

Increment

Conversion to nat


Lemma binc_btn : forall len (v : Bvector len),
  eqMod (pow2 len) (bvec_to_nat (binc v)) (S (bvec_to_nat v)).

Hint Resolve binc_btn : asm.

Lemma binc2_btn : forall len (v : Bvector len),
  eqMod (pow2 len) (bvec_to_nat (binc2 v)) (S (S (bvec_to_nat v))).

Lemma binc3_btn : forall len (v : Bvector len),
  eqMod (pow2 len) (bvec_to_nat (binc3 v)) (S (S (S (bvec_to_nat v)))).

Lemma binc4_btn : forall len (v : Bvector len),
  eqMod (pow2 len) (bvec_to_nat (binc4 v)) (S (S (S (S (bvec_to_nat v))))).

Disequalities


Theorem binc_neq : forall len (v : Bvector (S len)),
  binc v <> v.

Theorem binc2_neq : forall len (v : Bvector (S (S len))),
  binc2 v <> v.

Theorem binc3_neq : forall len (v : Bvector (S (S len))),
  binc3 v <> v.

Theorem binc_neq' : forall len (v : Bvector (S len)),
  binc v = v -> False.

Theorem binc2_neq' : forall len (v : Bvector (S (S len))),
  binc (binc v) = v -> False.

Theorem binc3_neq' : forall len (v : Bvector (S (S len))),
  binc (binc (binc v)) = v -> False.

Alternate bvec_to_nat versions, for use when we know that incrementing won't overflow
Pattern common to lemmas about different numbers of incrementations
Ltac binc_btn_below func lemma :=
  match goal with
    [ |- forall len (v : Bvector len), _ ] =>
    let Hbound := fresh "Hbound" in let Hbound2 := fresh "Hbound" in
      (intros len v Hbelow; destruct Hbelow; destruct (eqMod_nat (lemma len v)) as [x];
        add Hbound (btn_upper v); add Hbound2 (btn_upper (func len v));
        assert (x > 0 -> x * pow2 len >= pow2 len); [intros; induction x; simpl; intuition | destruct x; omega])
  end.

Theorem binc_btn_belowMax : forall len (v : Bvector len),
  belowMax v 1
  -> bvec_to_nat (binc v) = S (bvec_to_nat v).

Theorem binc2_btn_belowMax : forall len (v : Bvector len),
  belowMax v 2
  -> bvec_to_nat (binc2 v) = S (S (bvec_to_nat v)).

Theorem binc3_btn_belowMax : forall len (v : Bvector len),
  belowMax v 3
  -> bvec_to_nat (binc3 v) = S (S (S (bvec_to_nat v))).

Theorem binc4_btn_belowMax : forall len (v : Bvector len),
  belowMax v 4
  -> bvec_to_nat (binc4 v) = S (S (S (S (bvec_to_nat v)))).

??


Ltac binc_btn_below_inc func lemma :=
  match goal with
    [ |- forall len (v : Bvector len) n, _ ] =>
    let Hbound := fresh "Hbound" in let Hbound2 := fresh "Hbound" in
      (intros len v n Hbelow; destruct Hbelow; destruct (eqMod_nat (lemma len v)) as [x];
        add Hbound (btn_upper v); add Hbound2 (btn_upper (func len v));
        assert (x > 0 -> x * pow2 len >= pow2 len); [intros; induction x; simpl; intuition | destruct x; split; omega])
  end.

Theorem belowMax_binc_dec : forall len (v : Bvector len) n,
  belowMax v (S n)
  -> belowMax (binc v) n.

Theorem belowMax_binc2_dec : forall len (v : Bvector len) n,
  belowMax v (S (S n))
  -> belowMax (binc2 v) n.

Theorem belowMax_binc3_dec : forall len (v : Bvector len) n,
  belowMax v (S (S (S n)))
  -> belowMax (binc3 v) n.

Hint Resolve belowMax_binc_dec belowMax_binc2_dec belowMax_binc3_dec : asm.

Decrement


Lemma bdec_btn' : forall len (v : Bvector len),
  bvec_to_nat v > 0
  -> bvec_to_nat (bdec v) = pred (bvec_to_nat v).

Lemma bdec2_btn' : forall len (v : Bvector len),
  bvec_to_nat v > 1
  -> bvec_to_nat (bdec2 v) = pred (pred (bvec_to_nat v)).

Lemma bdec3_btn' : forall len (v : Bvector len),
  bvec_to_nat v > 2
  -> bvec_to_nat (bdec3 v) = pred (pred (pred (bvec_to_nat v))).

Lemma bdec4_btn' : forall len (v : Bvector len),
  bvec_to_nat v > 3
  -> bvec_to_nat (bdec4 v) = pred (pred (pred (pred (bvec_to_nat v)))).

Lemma bdec_btn : forall len (v : Bvector len),
  bvec_to_nat v > 0
  -> bvec_to_nat (bdec v) = bvec_to_nat v - 1.

Lemma bdec2_btn : forall len (v : Bvector len),
  bvec_to_nat v > 1
  -> bvec_to_nat (bdec2 v) = bvec_to_nat v - 2.

Lemma bdec3_btn : forall len (v : Bvector len),
  bvec_to_nat v > 2
  -> bvec_to_nat (bdec3 v) = bvec_to_nat v - 3.

Lemma bdec4_btn : forall len (v : Bvector len),
  bvec_to_nat v > 3
  -> bvec_to_nat (bdec4 v) = bvec_to_nat v - 4.

Negation


Theorem bneg_btn : forall len (v : Bvector len),
  eqMod (pow2 len) (bvec_to_nat (bneg v)) (pow2 len - bvec_to_nat v).

Theorem bneg_btn_sub : forall len (v : Bvector len) n,
  bvec_to_nat v <= n
  -> eqMod (pow2 len) (n - bvec_to_nat v) (n + bvec_to_nat (bneg v)).

Theorem bneg_btn_double : forall len (v : Bvector len),
  bneg (bneg v) = v.

Addition


Lemma badd_zero' : forall len (v : Bvector len),
 badd (bzero len) v = v.

Subtraction


Theorem bsub_btn : forall len (v1 v2 : Bvector len),
  eqMod (pow2 len) (bvec_to_nat (bsub v1 v2))
  (pow2 len + bvec_to_nat v1 - bvec_to_nat v2).

Theorem bsub_btn_neg : forall len (v1 v2 : Bvector len),
  eqMod (pow2 len) (bvec_to_nat (bneg (bsub v1 v2)))
  (bvec_to_nat (bsub v2 v1)).

Lemma bsub_zero : forall len (v : Bvector len),
  bvec_to_nat (bsub v (bzero len)) = bvec_to_nat v.

Lemma mod2_bool_1 : mod2_bool 1 = true.

Lemma div2_1 : div2 1 = 0.

Lemma mod2_bool_0 : mod2_bool 0 = false.

Lemma div2_0 : div2 0 = 0.

Hint Rewrite mod2_bool_1 div2_1 mod2_bool_0 div2_0 : asm.

Lemma mod2_bool_add_S : forall n1 n2,
  mod2_bool (S (2 * n1 + S (2 * n2))) = false.

Lemma div2_add_S : forall n1 n2,
  div2 (S (2 * n1 + S (2 * n2))) = S (n1 + n2).

Lemma mod2_bool_add : forall n1 n2,
  mod2_bool (2 * n1 + S (2 * n2)) = true.

Lemma div2_add : forall n1 n2,
  div2 (2 * n1 + S (2 * n2)) = n1 + n2.

Hint Rewrite mod2_bool_add_S div2_add_S mod2_bool_add div2_add : asm.

Lemma zero_ntb : forall len,
  nat_to_bvec len 0 = bzero len.

Hint Rewrite zero_ntb : asm.

Lemma bnot_bzero_mod : forall len,
  eqMod (pow2 len) (bvec_to_nat (bnot (bzero len))) (pow2 len - 1).

Hint Resolve bnot_bzero_mod : asm.

Lemma bzero_S_sub : forall len n,
  eqMod (pow2 len) (S n + bvec_to_nat (bnot (bzero len))) n.

Lemma bdec_binc : forall len (v : Bvector len),
  bdec (binc v) = v.

Lemma binc_bdec : forall len (v : Bvector len),
  binc (bdec v) = v.

Lemma bzero_S_dec : forall len (v : Bvector len),
  bvec_to_nat v > 0
  -> eqMod (pow2 len) (bvec_to_nat v + bvec_to_nat (bnot (bzero len))) (bvec_to_nat (bdec v)).

Hint Resolve bzero_S_sub bzero_S_dec : asm.

Lemma bsub_bdec : forall len (v : Bvector len),
  bvec_to_nat v > 0
  -> bsub v (nat_to_bvec len 1) = bdec v.

Lemma eqMod_eq : forall m x1 x2,
  x1 = x2
  -> eqMod m x1 x2.

Lemma badd_btn_neg : forall len (v1 v2 : Bvector len),
  eqMod (pow2 len)
  (bvec_to_nat (bneg (nat_to_bvec len
    (bvec_to_nat v1 + bvec_to_nat v2))))
  (bvec_to_nat (bneg v1) + bvec_to_nat (bneg v2)).

Lemma bsub_btn_const : forall len (v1 : Bvector len) n1 n2,
  bsub v1 (nat_to_bvec len (n1 + n2))
  = bsub (bsub v1 (nat_to_bvec len n1)) (nat_to_bvec len n2).

Lemma bsub_bdec2 : forall len (v : Bvector len),
  bvec_to_nat v > 1
  -> bsub v (nat_to_bvec len 2) = bdec2 v.

Lemma bsub_bdec3 : forall len (v : Bvector len),
  bvec_to_nat v > 2
  -> bsub v (nat_to_bvec len 3) = bdec3 v.

Lemma bsub_bdec4 : forall len (v : Bvector len),
  bvec_to_nat v > 3
  -> bsub v (nat_to_bvec len 4) = bdec4 v.

Lemma badd_comm : forall len (v1 v2 : Bvector len),
  badd v1 v2 = badd v2 v1.

Lemma badd32_comm : forall v1 v2,
  badd32 v1 v2 = badd32 v2 v1.

Lemma badd32_swap_neg : forall v1 v2,
  badd32 v2 v1 = bsub32 v1 (bneg v2).
Index
This page has been generated by coqdoc