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