[475] | 1 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 2 | (* BitVector.ma: Fixed length bitvectors, and common operations on them. *) |
---|
| 3 | (* Most functions are specialised versions of those found in *) |
---|
| 4 | (* Vector.ma as a courtesy, or boolean functions lifted into *) |
---|
| 5 | (* BitVector variants. *) |
---|
| 6 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 7 | |
---|
| 8 | include "arithmetics/nat.ma". |
---|
| 9 | |
---|
[985] | 10 | include "ASM/FoldStuff.ma". |
---|
[698] | 11 | include "ASM/Vector.ma". |
---|
[475] | 12 | |
---|
| 13 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 14 | (* Common synonyms. *) |
---|
| 15 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 16 | |
---|
| 17 | definition BitVector ≝ λn: nat. Vector bool n. |
---|
| 18 | definition Bit ≝ bool. |
---|
| 19 | definition Nibble ≝ BitVector 4. |
---|
| 20 | definition Byte7 ≝ BitVector 7. |
---|
| 21 | definition Byte ≝ BitVector 8. |
---|
| 22 | definition Word ≝ BitVector 16. |
---|
| 23 | definition Word11 ≝ BitVector 11. |
---|
| 24 | |
---|
| 25 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
[985] | 26 | (* Inversion *) |
---|
| 27 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 28 | |
---|
| 29 | lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool. |
---|
[1516] | 30 | #v lapply (refl … 0) cases v in ⊢ (??%? → ?%%??); // |
---|
[990] | 31 | #n #hd #tl #abs @⊥ destruct (abs) |
---|
[985] | 32 | qed. |
---|
| 33 | |
---|
| 34 | lemma BitVector_Sn: ∀n.∀v:BitVector (S n). |
---|
| 35 | ∃hd.∃tl.v ≃ VCons bool n hd tl. |
---|
[1516] | 36 | #n #v lapply (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))); |
---|
[990] | 37 | [ #abs @⊥ destruct (abs) |
---|
[985] | 38 | | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ] |
---|
| 39 | qed. |
---|
| 40 | |
---|
| 41 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
[475] | 42 | (* Lookup. *) |
---|
| 43 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 44 | |
---|
| 45 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 46 | (* Creating bitvectors from scratch. *) |
---|
| 47 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 48 | |
---|
| 49 | definition zero: ∀n:nat. BitVector n ≝ |
---|
| 50 | λn: nat. replicate bool n false. |
---|
[2006] | 51 | |
---|
| 52 | alias id "bv_zero" = "cic:/matita/cerco/ASM/BitVector/zero.def(2)". |
---|
| 53 | |
---|
[475] | 54 | definition maximum: ∀n:nat. BitVector n ≝ |
---|
| 55 | λn: nat. replicate bool n true. |
---|
| 56 | |
---|
| 57 | definition pad ≝ |
---|
| 58 | λm, n: nat. |
---|
[744] | 59 | λb: BitVector n. pad_vector ? false m n b. |
---|
[1890] | 60 | |
---|
| 61 | (* jpb: we already have bitvector_of_nat and friends in the library, maybe |
---|
| 62 | * we should unify this in some way *) |
---|
[1635] | 63 | let rec nat_to_bv (n : nat) (k : nat) on n : BitVector n ≝ |
---|
| 64 | match n with |
---|
| 65 | [ O ⇒ VEmpty ? |
---|
| 66 | | S n' ⇒ |
---|
| 67 | eqb (k mod 2) 1 ::: nat_to_bv n' (k ÷ 2) |
---|
| 68 | ]. |
---|
| 69 | |
---|
| 70 | let rec bv_to_nat (n : nat) (b : BitVector n) on b : nat ≝ |
---|
| 71 | match b with |
---|
| 72 | [ VEmpty ⇒ 0 |
---|
| 73 | | VCons n' x b' ⇒ (if x then 1 else 0) + bv_to_nat n' b' * 2]. |
---|
| 74 | |
---|
[475] | 75 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 76 | (* Other manipulations. *) |
---|
| 77 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 78 | |
---|
| 79 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 80 | (* Logical operations. *) |
---|
| 81 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 82 | |
---|
| 83 | definition conjunction_bv: ∀n. ∀b, c: BitVector n. BitVector n ≝ |
---|
| 84 | λn: nat. |
---|
| 85 | λb: BitVector n. |
---|
| 86 | λc: BitVector n. |
---|
| 87 | zip_with ? ? ? n (andb) b c. |
---|
| 88 | |
---|
| 89 | interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c). |
---|
| 90 | |
---|
| 91 | definition inclusive_disjunction_bv ≝ |
---|
| 92 | λn: nat. |
---|
| 93 | λb: BitVector n. |
---|
| 94 | λc: BitVector n. |
---|
| 95 | zip_with ? ? ? n (orb) b c. |
---|
| 96 | |
---|
| 97 | interpretation "BitVector inclusive disjunction" |
---|
| 98 | 'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c). |
---|
| 99 | |
---|
| 100 | definition exclusive_disjunction_bv ≝ |
---|
| 101 | λn: nat. |
---|
| 102 | λb: BitVector n. |
---|
| 103 | λc: BitVector n. |
---|
[1599] | 104 | zip_with ? ? ? n xorb b c. |
---|
[475] | 105 | |
---|
| 106 | interpretation "BitVector exclusive disjunction" |
---|
[1599] | 107 | 'exclusive_disjunction b c = (xorb b c). |
---|
[475] | 108 | |
---|
| 109 | definition negation_bv ≝ |
---|
| 110 | λn: nat. |
---|
| 111 | λb: BitVector n. |
---|
| 112 | map bool bool n (notb) b. |
---|
| 113 | |
---|
| 114 | interpretation "BitVector negation" 'negation b c = (negation_bv ? b c). |
---|
| 115 | |
---|
| 116 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 117 | (* Rotates and shifts. *) |
---|
| 118 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 119 | |
---|
| 120 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 121 | (* Conversions to and from lists and natural numbers. *) |
---|
| 122 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 123 | |
---|
[868] | 124 | definition eq_b ≝ |
---|
| 125 | λb, c: bool. |
---|
| 126 | if b then |
---|
| 127 | c |
---|
| 128 | else |
---|
| 129 | notb c. |
---|
| 130 | |
---|
[2121] | 131 | lemma eq_b_refl: |
---|
| 132 | ∀b. |
---|
| 133 | eq_b b b = true. |
---|
| 134 | #b cases b // |
---|
| 135 | qed. |
---|
| 136 | |
---|
[985] | 137 | lemma eq_b_eq: |
---|
| 138 | ∀b, c. |
---|
| 139 | eq_b b c = true → b = c. |
---|
| 140 | #b #c |
---|
| 141 | cases b |
---|
| 142 | cases c |
---|
| 143 | normalize // |
---|
| 144 | qed. |
---|
| 145 | |
---|
[475] | 146 | definition eq_bv ≝ |
---|
| 147 | λn: nat. |
---|
| 148 | λb, c: BitVector n. |
---|
[868] | 149 | eq_v bool n eq_b b c. |
---|
[475] | 150 | |
---|
[726] | 151 | lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y. |
---|
[697] | 152 | (x = y → P true) → |
---|
| 153 | (x ≠ y → P false) → |
---|
| 154 | P (eq_bv n x y). |
---|
[1516] | 155 | #P #n #x #y #Ht #Hf whd in ⊢ (?%); @(eq_v_elim … Ht Hf) |
---|
[697] | 156 | #Q * *; normalize /3/ |
---|
| 157 | qed. |
---|
[961] | 158 | |
---|
| 159 | lemma eq_bv_true: ∀n,v. eq_bv n v v = true. |
---|
| 160 | @eq_v_true * @refl |
---|
| 161 | qed. |
---|
| 162 | |
---|
| 163 | lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false. |
---|
| 164 | #n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ] |
---|
| 165 | qed. |
---|
[985] | 166 | |
---|
| 167 | lemma eq_bv_refl: |
---|
| 168 | ∀n,v. eq_bv n v v = true. |
---|
| 169 | #n #v |
---|
| 170 | elim v |
---|
| 171 | [ // |
---|
| 172 | | #n #hd #tl #ih |
---|
| 173 | normalize |
---|
| 174 | cases hd |
---|
| 175 | [ normalize |
---|
| 176 | @ ih |
---|
| 177 | | normalize |
---|
| 178 | @ ih |
---|
| 179 | ] |
---|
| 180 | ] |
---|
| 181 | qed. |
---|
| 182 | |
---|
| 183 | lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1. |
---|
| 184 | #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/] |
---|
| 185 | qed. |
---|
| 186 | |
---|
| 187 | lemma eq_eq_bv: |
---|
| 188 | ∀n, v, q. |
---|
| 189 | v = q → eq_bv n v q = true. |
---|
| 190 | #n #v |
---|
| 191 | elim v |
---|
| 192 | [ #q #h <h normalize % |
---|
| 193 | | #n #hd #tl #ih #q #h >h // |
---|
| 194 | ] |
---|
| 195 | qed. |
---|
| 196 | |
---|
| 197 | lemma eq_bv_eq: |
---|
| 198 | ∀n, v, q. |
---|
| 199 | eq_bv n v q = true → v = q. |
---|
[1516] | 200 | #n #v #q generalize in match v; |
---|
[985] | 201 | elim q |
---|
| 202 | [ #v #h @BitVector_O |
---|
| 203 | | #n #hd #tl #ih #v' #h |
---|
| 204 | cases (BitVector_Sn ? v') |
---|
| 205 | #hd' * #tl' #jmeq >jmeq in h; |
---|
| 206 | #new_h |
---|
[1521] | 207 | change with ((andb ? ?) = ?) in new_h; |
---|
[985] | 208 | cases(conjunction_true … new_h) |
---|
| 209 | #eq_heads #eq_tails |
---|
| 210 | whd in eq_heads:(??(??(%))?); |
---|
| 211 | cases(eq_b_eq … eq_heads) |
---|
| 212 | whd in eq_tails:(??(?????(%))?); |
---|
[1521] | 213 | change with (eq_bv ??? = ?) in eq_tails; |
---|
[985] | 214 | <(ih tl') // |
---|
| 215 | ] |
---|
| 216 | qed. |
---|
| 217 | |
---|
[1928] | 218 | corollary refl_iff_eq_bv_true: |
---|
| 219 | ∀n: nat. |
---|
| 220 | ∀x: BitVector n. |
---|
| 221 | ∀y: BitVector n. |
---|
| 222 | eq_bv n x y = true ↔ x = y. |
---|
| 223 | #n #x #y whd in match iff; normalize nodelta |
---|
| 224 | @conj /2/ |
---|
| 225 | qed. |
---|
| 226 | |
---|
[2126] | 227 | lemma bitvector_3_cases: |
---|
| 228 | ∀w: BitVector 3. |
---|
| 229 | ∃b0,b1,b2: bool. |
---|
| 230 | w ≃ [[b0;b1;b2]]. |
---|
| 231 | #w |
---|
| 232 | repeat (cases (BitVector_Sn … w) #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w) |
---|
| 233 | >(BitVector_O … w) % |
---|
[2122] | 234 | qed. |
---|
| 235 | |
---|
[2126] | 236 | lemma bitvector_11_cases: |
---|
| 237 | ∀w: BitVector 11. |
---|
| 238 | ∃b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10: bool. |
---|
| 239 | w ≃ [[b0;b1;b2;b3;b4;b5;b6;b7;b8;b9;b10]]. |
---|
| 240 | #w |
---|
| 241 | repeat (cases (BitVector_Sn … w) #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w) |
---|
| 242 | >(BitVector_O … w) % |
---|
| 243 | qed. |
---|
| 244 | |
---|
[2124] | 245 | lemma bitvector_3_elim_prop: |
---|
| 246 | ∀P: BitVector 3 → Prop. |
---|
| 247 | P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] → |
---|
| 248 | P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] → |
---|
| 249 | P [[true;true;false]] → P [[true;true;true]] → ∀v. P v. |
---|
| 250 | #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 |
---|
| 251 | cases (bitvector_3_cases … H9) #l #assm cases assm |
---|
| 252 | -assm #c #assm cases assm |
---|
| 253 | -assm #r #assm cases assm destruct |
---|
| 254 | cases l cases c cases r assumption |
---|
[2601] | 255 | qed. |
---|