| Theorems about converting between bitvectors and naturals |
Require Import Arith Bool Bvector Euclid.
Require Import Asm.Util.ArithUtil.
Require Import Asm.Util.Mod.
Require Import Asm.Util.Tactics.
Require Import Asm.Bitvector.Defs.
Require Import Asm.Bitvector.Tactics.
Set Implicit Arguments.
Converting bitvectors to naturals |
Upper bounds |
| A bitvector can't translate to a natural number that requires more bits than the original did. |
Lemma btn_upper : forall len (v : Bvector len),
bvec_to_nat v < pow2 len.
Lemma btn_upper' : forall len (v : Bvector len),
bvec_to_nat v <= pow2 len - 1.
Lemma btn_upper'' : forall len (v : Bvector len),
bvec_to_nat v <= pow2 len.
Hint Immediate btn_upper btn_upper' : asm.
Lemma btn_diff_pos : forall len (v : Bvector len),
pow2 len - bvec_to_nat v > 0.
Hint Resolve btn_diff_pos : asm.
Theorem btn_inj : forall n (t1 t2 : Bvector n), bvec_to_nat t1 = bvec_to_nat t2 -> t1 = t2.
Theorem btn_invert : forall len (v : Bvector len),
nat_to_bvec len (bvec_to_nat v) = v.
Lemma S_minus_1_pow2 : forall len (v : Bvector len),
S (pow2 len - bvec_to_nat v) - 1 = S (pow2 len - bvec_to_nat v - 1).
Hint Rewrite S_minus_1_pow2 : asm.
Converting naturals to bitvectors |
Theorem ntb_mod : forall len n1 n2,
eqMod (pow2 len) n1 n2
-> nat_to_bvec len n1 = nat_to_bvec len n2.
Lemma mod2_div2 : forall n,
n = 2 * div2 n + mod2 n.
Lemma mod2_inj : forall n1 n2,
mod2_bool n1 = mod2_bool n2
-> mod2 n1 = mod2 n2.
Theorem ntb_mod' : forall len n1 n2,
nat_to_bvec len n1 = nat_to_bvec len n2
-> eqMod (pow2 len) n1 n2.
Theorem ntb_invert : forall len n,
n < pow2 len
-> bvec_to_nat (nat_to_bvec len n) = n.
Theorem ntb_invert_mod : forall len n,
eqMod (pow2 len) (bvec_to_nat (nat_to_bvec len n)) n.
Theorem ntb_add : forall len n1 n2,
eqMod (pow2 len) (n1 + n2)
(bvec_to_nat (nat_to_bvec len n1) + bvec_to_nat (nat_to_bvec len n2)).
Lemma ntb_invert_eqMod : forall len n1 n2 n k,
bvec_to_nat (nat_to_bvec len n) <= n1
-> n <= k * pow2 len
-> eqMod (pow2 len) (n1 + k * pow2 len - n) n2
-> eqMod (pow2 len) (n1 - bvec_to_nat (nat_to_bvec len n)) n2.