[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. |
---|
| 31 | #v generalize in match (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. |
---|
| 37 | #n #v generalize in match (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. |
---|
| 52 | |
---|
| 53 | definition maximum: ∀n:nat. BitVector n ≝ |
---|
| 54 | λn: nat. replicate bool n true. |
---|
| 55 | |
---|
| 56 | definition pad ≝ |
---|
| 57 | λm, n: nat. |
---|
[744] | 58 | λb: BitVector n. pad_vector ? false m n b. |
---|
[475] | 59 | |
---|
| 60 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 61 | (* Other manipulations. *) |
---|
| 62 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 63 | |
---|
| 64 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 65 | (* Logical operations. *) |
---|
| 66 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 67 | |
---|
| 68 | definition conjunction_bv: ∀n. ∀b, c: BitVector n. BitVector n ≝ |
---|
| 69 | λn: nat. |
---|
| 70 | λb: BitVector n. |
---|
| 71 | λc: BitVector n. |
---|
| 72 | zip_with ? ? ? n (andb) b c. |
---|
| 73 | |
---|
| 74 | interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c). |
---|
| 75 | |
---|
| 76 | definition inclusive_disjunction_bv ≝ |
---|
| 77 | λn: nat. |
---|
| 78 | λb: BitVector n. |
---|
| 79 | λc: BitVector n. |
---|
| 80 | zip_with ? ? ? n (orb) b c. |
---|
| 81 | |
---|
| 82 | interpretation "BitVector inclusive disjunction" |
---|
| 83 | 'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c). |
---|
| 84 | |
---|
| 85 | definition exclusive_disjunction_bv ≝ |
---|
| 86 | λn: nat. |
---|
| 87 | λb: BitVector n. |
---|
| 88 | λc: BitVector n. |
---|
| 89 | zip_with ? ? ? n (exclusive_disjunction) b c. |
---|
| 90 | |
---|
| 91 | interpretation "BitVector exclusive disjunction" |
---|
| 92 | 'exclusive_disjunction b c = (exclusive_disjunction ? b c). |
---|
| 93 | |
---|
| 94 | definition negation_bv ≝ |
---|
| 95 | λn: nat. |
---|
| 96 | λb: BitVector n. |
---|
| 97 | map bool bool n (notb) b. |
---|
| 98 | |
---|
| 99 | interpretation "BitVector negation" 'negation b c = (negation_bv ? b c). |
---|
| 100 | |
---|
| 101 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 102 | (* Rotates and shifts. *) |
---|
| 103 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 104 | |
---|
| 105 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 106 | (* Conversions to and from lists and natural numbers. *) |
---|
| 107 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 108 | |
---|
[868] | 109 | definition eq_b ≝ |
---|
| 110 | λb, c: bool. |
---|
| 111 | if b then |
---|
| 112 | c |
---|
| 113 | else |
---|
| 114 | notb c. |
---|
| 115 | |
---|
[985] | 116 | lemma eq_b_eq: |
---|
| 117 | ∀b, c. |
---|
| 118 | eq_b b c = true → b = c. |
---|
| 119 | #b #c |
---|
| 120 | cases b |
---|
| 121 | cases c |
---|
| 122 | normalize // |
---|
| 123 | qed. |
---|
| 124 | |
---|
[475] | 125 | definition eq_bv ≝ |
---|
| 126 | λn: nat. |
---|
| 127 | λb, c: BitVector n. |
---|
[868] | 128 | eq_v bool n eq_b b c. |
---|
[475] | 129 | |
---|
[726] | 130 | lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y. |
---|
[697] | 131 | (x = y → P true) → |
---|
| 132 | (x ≠ y → P false) → |
---|
| 133 | P (eq_bv n x y). |
---|
| 134 | #P #n #x #y #Ht #Hf whd in ⊢ (?%) @(eq_v_elim … Ht Hf) |
---|
| 135 | #Q * *; normalize /3/ |
---|
| 136 | qed. |
---|
[961] | 137 | |
---|
| 138 | lemma eq_bv_true: ∀n,v. eq_bv n v v = true. |
---|
| 139 | @eq_v_true * @refl |
---|
| 140 | qed. |
---|
| 141 | |
---|
| 142 | lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false. |
---|
| 143 | #n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ] |
---|
| 144 | qed. |
---|
[985] | 145 | |
---|
| 146 | lemma eq_bv_refl: |
---|
| 147 | ∀n,v. eq_bv n v v = true. |
---|
| 148 | #n #v |
---|
| 149 | elim v |
---|
| 150 | [ // |
---|
| 151 | | #n #hd #tl #ih |
---|
| 152 | normalize |
---|
| 153 | cases hd |
---|
| 154 | [ normalize |
---|
| 155 | @ ih |
---|
| 156 | | normalize |
---|
| 157 | @ ih |
---|
| 158 | ] |
---|
| 159 | ] |
---|
| 160 | qed. |
---|
| 161 | |
---|
| 162 | lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1. |
---|
| 163 | #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/] |
---|
| 164 | qed. |
---|
| 165 | |
---|
| 166 | lemma eq_eq_bv: |
---|
| 167 | ∀n, v, q. |
---|
| 168 | v = q → eq_bv n v q = true. |
---|
| 169 | #n #v |
---|
| 170 | elim v |
---|
| 171 | [ #q #h <h normalize % |
---|
| 172 | | #n #hd #tl #ih #q #h >h // |
---|
| 173 | ] |
---|
| 174 | qed. |
---|
| 175 | |
---|
| 176 | lemma eq_bv_eq: |
---|
| 177 | ∀n, v, q. |
---|
| 178 | eq_bv n v q = true → v = q. |
---|
| 179 | #n #v #q generalize in match v |
---|
| 180 | elim q |
---|
| 181 | [ #v #h @BitVector_O |
---|
| 182 | | #n #hd #tl #ih #v' #h |
---|
| 183 | cases (BitVector_Sn ? v') |
---|
| 184 | #hd' * #tl' #jmeq >jmeq in h; |
---|
| 185 | #new_h |
---|
| 186 | change in new_h with ((andb ? ?) = ?); |
---|
| 187 | cases(conjunction_true … new_h) |
---|
| 188 | #eq_heads #eq_tails |
---|
| 189 | whd in eq_heads:(??(??(%))?); |
---|
| 190 | cases(eq_b_eq … eq_heads) |
---|
| 191 | whd in eq_tails:(??(?????(%))?); |
---|
| 192 | change in eq_tails with (eq_bv ??? = ?); |
---|
| 193 | <(ih tl') // |
---|
| 194 | ] |
---|
| 195 | qed. |
---|
| 196 | |
---|
[475] | 197 | axiom bitvector_of_string: |
---|
| 198 | ∀n: nat. |
---|
| 199 | ∀s: String. |
---|
| 200 | BitVector n. |
---|
| 201 | |
---|
| 202 | axiom string_of_bitvector: |
---|
| 203 | ∀n: nat. |
---|
| 204 | ∀b: BitVector n. |
---|
| 205 | String. |
---|