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