[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 | |
---|
[475] | 61 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 62 | (* Other manipulations. *) |
---|
| 63 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 64 | |
---|
| 65 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 66 | (* Logical operations. *) |
---|
| 67 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 68 | |
---|
| 69 | definition conjunction_bv: ∀n. ∀b, c: BitVector n. BitVector n ≝ |
---|
| 70 | λn: nat. |
---|
| 71 | λb: BitVector n. |
---|
| 72 | λc: BitVector n. |
---|
| 73 | zip_with ? ? ? n (andb) b c. |
---|
| 74 | |
---|
| 75 | interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c). |
---|
| 76 | |
---|
| 77 | definition inclusive_disjunction_bv ≝ |
---|
| 78 | λn: nat. |
---|
| 79 | λb: BitVector n. |
---|
| 80 | λc: BitVector n. |
---|
| 81 | zip_with ? ? ? n (orb) b c. |
---|
| 82 | |
---|
| 83 | interpretation "BitVector inclusive disjunction" |
---|
| 84 | 'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c). |
---|
| 85 | |
---|
| 86 | definition exclusive_disjunction_bv ≝ |
---|
| 87 | λn: nat. |
---|
| 88 | λb: BitVector n. |
---|
| 89 | λc: BitVector n. |
---|
[1599] | 90 | zip_with ? ? ? n xorb b c. |
---|
[475] | 91 | |
---|
| 92 | interpretation "BitVector exclusive disjunction" |
---|
[1599] | 93 | 'exclusive_disjunction b c = (xorb b c). |
---|
[475] | 94 | |
---|
| 95 | definition negation_bv ≝ |
---|
| 96 | λn: nat. |
---|
| 97 | λb: BitVector n. |
---|
| 98 | map bool bool n (notb) b. |
---|
| 99 | |
---|
| 100 | interpretation "BitVector negation" 'negation b c = (negation_bv ? b c). |
---|
| 101 | |
---|
| 102 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 103 | (* Rotates and shifts. *) |
---|
| 104 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 105 | |
---|
| 106 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 107 | (* Conversions to and from lists and natural numbers. *) |
---|
| 108 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 109 | |
---|
[868] | 110 | definition eq_b ≝ |
---|
| 111 | λb, c: bool. |
---|
| 112 | if b then |
---|
| 113 | c |
---|
| 114 | else |
---|
| 115 | notb c. |
---|
| 116 | |
---|
[2121] | 117 | lemma eq_b_refl: |
---|
| 118 | ∀b. |
---|
| 119 | eq_b b b = true. |
---|
| 120 | #b cases b // |
---|
| 121 | qed. |
---|
| 122 | |
---|
[985] | 123 | lemma eq_b_eq: |
---|
| 124 | ∀b, c. |
---|
| 125 | eq_b b c = true → b = c. |
---|
| 126 | #b #c |
---|
| 127 | cases b |
---|
| 128 | cases c |
---|
| 129 | normalize // |
---|
| 130 | qed. |
---|
| 131 | |
---|
[475] | 132 | definition eq_bv ≝ |
---|
| 133 | λn: nat. |
---|
| 134 | λb, c: BitVector n. |
---|
[868] | 135 | eq_v bool n eq_b b c. |
---|
[475] | 136 | |
---|
[726] | 137 | lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y. |
---|
[697] | 138 | (x = y → P true) → |
---|
| 139 | (x ≠ y → P false) → |
---|
| 140 | P (eq_bv n x y). |
---|
[1516] | 141 | #P #n #x #y #Ht #Hf whd in ⊢ (?%); @(eq_v_elim … Ht Hf) |
---|
[697] | 142 | #Q * *; normalize /3/ |
---|
| 143 | qed. |
---|
[961] | 144 | |
---|
| 145 | lemma eq_bv_true: ∀n,v. eq_bv n v v = true. |
---|
| 146 | @eq_v_true * @refl |
---|
| 147 | qed. |
---|
| 148 | |
---|
| 149 | lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false. |
---|
| 150 | #n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ] |
---|
| 151 | qed. |
---|
[985] | 152 | |
---|
| 153 | lemma eq_bv_refl: |
---|
| 154 | ∀n,v. eq_bv n v v = true. |
---|
| 155 | #n #v |
---|
| 156 | elim v |
---|
| 157 | [ // |
---|
| 158 | | #n #hd #tl #ih |
---|
| 159 | normalize |
---|
| 160 | cases hd |
---|
| 161 | [ normalize |
---|
| 162 | @ ih |
---|
| 163 | | normalize |
---|
| 164 | @ ih |
---|
| 165 | ] |
---|
| 166 | ] |
---|
| 167 | qed. |
---|
| 168 | |
---|
| 169 | lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1. |
---|
| 170 | #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/] |
---|
| 171 | qed. |
---|
| 172 | |
---|
| 173 | lemma eq_eq_bv: |
---|
| 174 | ∀n, v, q. |
---|
| 175 | v = q → eq_bv n v q = true. |
---|
| 176 | #n #v |
---|
| 177 | elim v |
---|
| 178 | [ #q #h <h normalize % |
---|
| 179 | | #n #hd #tl #ih #q #h >h // |
---|
| 180 | ] |
---|
| 181 | qed. |
---|
| 182 | |
---|
| 183 | lemma eq_bv_eq: |
---|
| 184 | ∀n, v, q. |
---|
| 185 | eq_bv n v q = true → v = q. |
---|
[1516] | 186 | #n #v #q generalize in match v; |
---|
[985] | 187 | elim q |
---|
| 188 | [ #v #h @BitVector_O |
---|
| 189 | | #n #hd #tl #ih #v' #h |
---|
| 190 | cases (BitVector_Sn ? v') |
---|
| 191 | #hd' * #tl' #jmeq >jmeq in h; |
---|
| 192 | #new_h |
---|
[1521] | 193 | change with ((andb ? ?) = ?) in new_h; |
---|
[985] | 194 | cases(conjunction_true … new_h) |
---|
| 195 | #eq_heads #eq_tails |
---|
| 196 | whd in eq_heads:(??(??(%))?); |
---|
| 197 | cases(eq_b_eq … eq_heads) |
---|
| 198 | whd in eq_tails:(??(?????(%))?); |
---|
[1521] | 199 | change with (eq_bv ??? = ?) in eq_tails; |
---|
[985] | 200 | <(ih tl') // |
---|
| 201 | ] |
---|
| 202 | qed. |
---|
| 203 | |
---|
[1928] | 204 | corollary refl_iff_eq_bv_true: |
---|
| 205 | ∀n: nat. |
---|
| 206 | ∀x: BitVector n. |
---|
| 207 | ∀y: BitVector n. |
---|
| 208 | eq_bv n x y = true ↔ x = y. |
---|
| 209 | #n #x #y whd in match iff; normalize nodelta |
---|
| 210 | @conj /2/ |
---|
| 211 | qed. |
---|
| 212 | |
---|
[2126] | 213 | lemma bitvector_3_cases: |
---|
| 214 | ∀w: BitVector 3. |
---|
| 215 | ∃b0,b1,b2: bool. |
---|
| 216 | w ≃ [[b0;b1;b2]]. |
---|
| 217 | #w |
---|
| 218 | repeat (cases (BitVector_Sn … w) #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w) |
---|
| 219 | >(BitVector_O … w) % |
---|
[2122] | 220 | qed. |
---|
| 221 | |
---|
[2126] | 222 | lemma bitvector_11_cases: |
---|
| 223 | ∀w: BitVector 11. |
---|
| 224 | ∃b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10: bool. |
---|
| 225 | w ≃ [[b0;b1;b2;b3;b4;b5;b6;b7;b8;b9;b10]]. |
---|
| 226 | #w |
---|
| 227 | repeat (cases (BitVector_Sn … w) #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w) |
---|
| 228 | >(BitVector_O … w) % |
---|
| 229 | qed. |
---|
| 230 | |
---|
[2124] | 231 | lemma bitvector_3_elim_prop: |
---|
| 232 | ∀P: BitVector 3 → Prop. |
---|
| 233 | P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] → |
---|
| 234 | P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] → |
---|
| 235 | P [[true;true;false]] → P [[true;true;true]] → ∀v. P v. |
---|
| 236 | #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 |
---|
| 237 | cases (bitvector_3_cases … H9) #l #assm cases assm |
---|
| 238 | -assm #c #assm cases assm |
---|
| 239 | -assm #r #assm cases assm destruct |
---|
| 240 | cases l cases c cases r assumption |
---|
[2601] | 241 | qed. |
---|