[236] | 1 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 2 | (* BitVector.ma: Fixed length bitvectors, and common operations on them. *) |
---|
[240] | 3 | (* Most functions are specialised versions of those found in *) |
---|
| 4 | (* Vector.ma as a courtesy, or Boolean functions lifted into *) |
---|
| 5 | (* BitVector variants. *) |
---|
[236] | 6 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 7 | |
---|
[246] | 8 | include "Vector.ma". |
---|
[240] | 9 | |
---|
[236] | 10 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 11 | (* Common synonyms. *) |
---|
| 12 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 13 | |
---|
[228] | 14 | ndefinition BitVector ≝ λn: Nat. Vector Bool n. |
---|
[263] | 15 | ndefinition Bit ≝ Bool. |
---|
[230] | 16 | ndefinition Nibble ≝ BitVector (S (S (S (S Z)))). |
---|
| 17 | ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))). |
---|
| 18 | ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))). |
---|
| 19 | ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))). |
---|
[271] | 20 | ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S Z))))))))))). |
---|
[224] | 21 | |
---|
[236] | 22 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
[240] | 23 | (* Lookup. *) |
---|
| 24 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 25 | |
---|
[362] | 26 | (* |
---|
[337] | 27 | ndefinition get_index_bv ≝ |
---|
[240] | 28 | λn: Nat. |
---|
| 29 | λb: BitVector n. |
---|
| 30 | λm: Nat. |
---|
[266] | 31 | λp: m < n. |
---|
[362] | 32 | get_index_bv Bool n b m p. |
---|
[240] | 33 | |
---|
| 34 | interpretation "BitVector get_index" 'get_index b n = (get_index ? b n). |
---|
| 35 | |
---|
[337] | 36 | ndefinition set_index_bv ≝ |
---|
[240] | 37 | λn: Nat. |
---|
| 38 | λb: BitVector n. |
---|
| 39 | λm: Nat. |
---|
[266] | 40 | λp: m < n. |
---|
| 41 | λc: Bool. |
---|
[314] | 42 | set_index Bool n b m c. |
---|
[240] | 43 | |
---|
| 44 | ndefinition drop ≝ |
---|
| 45 | λn: Nat. |
---|
| 46 | λb: BitVector n. |
---|
| 47 | λm: Nat. |
---|
| 48 | drop Bool n b m. |
---|
[362] | 49 | *) |
---|
[240] | 50 | |
---|
| 51 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
[236] | 52 | (* Creating bitvectors from scratch. *) |
---|
| 53 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 54 | |
---|
[362] | 55 | ndefinition zero: ∀n:Nat. BitVector n ≝ |
---|
| 56 | λn: Nat. replicate Bool n false. |
---|
[228] | 57 | |
---|
[362] | 58 | ndefinition max: ∀n:Nat. BitVector n ≝ |
---|
| 59 | λn: Nat. replicate Bool n true. |
---|
| 60 | |
---|
| 61 | (* |
---|
[237] | 62 | ndefinition append ≝ |
---|
| 63 | λm, n: Nat. |
---|
| 64 | λb: BitVector m. |
---|
| 65 | λc: BitVector n. |
---|
| 66 | append Bool m n b c. |
---|
[362] | 67 | *) |
---|
| 68 | |
---|
[237] | 69 | ndefinition pad ≝ |
---|
| 70 | λm, n: Nat. |
---|
| 71 | λb: BitVector n. |
---|
[260] | 72 | let padding ≝ replicate Bool m false in |
---|
[237] | 73 | append Bool m n padding b. |
---|
[240] | 74 | |
---|
| 75 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 76 | (* Other manipulations. *) |
---|
| 77 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
[237] | 78 | |
---|
[362] | 79 | (* |
---|
[240] | 80 | ndefinition reverse ≝ |
---|
| 81 | λn: Nat. |
---|
| 82 | λb: BitVector n. |
---|
| 83 | reverse Bool n b. |
---|
| 84 | |
---|
| 85 | ndefinition length ≝ |
---|
| 86 | λn: Nat. |
---|
| 87 | λb: BitVector n. |
---|
| 88 | length Bool n b. |
---|
[362] | 89 | *) |
---|
[240] | 90 | |
---|
[236] | 91 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 92 | (* Logical operations. *) |
---|
| 93 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 94 | |
---|
[343] | 95 | ndefinition conjunction_bv ≝ |
---|
[228] | 96 | λn: Nat. |
---|
| 97 | λb: BitVector n. |
---|
| 98 | λc: BitVector n. |
---|
[240] | 99 | zip_with Bool Bool Bool n conjunction b c. |
---|
| 100 | |
---|
| 101 | interpretation "BitVector conjunction" 'conjunction b c = (conjunction ? b c). |
---|
[237] | 102 | |
---|
[343] | 103 | ndefinition inclusive_disjunction_bv ≝ |
---|
[228] | 104 | λn: Nat. |
---|
| 105 | λb: BitVector n. |
---|
| 106 | λc: BitVector n. |
---|
[240] | 107 | zip_with Bool Bool Bool n inclusive_disjunction b c. |
---|
| 108 | |
---|
| 109 | interpretation "BitVector inclusive disjunction" |
---|
| 110 | 'inclusive_disjunction b c = (inclusive_disjunction ? b c). |
---|
[237] | 111 | |
---|
[343] | 112 | ndefinition exclusive_disjunction_bv ≝ |
---|
[228] | 113 | λn: Nat. |
---|
| 114 | λb: BitVector n. |
---|
| 115 | λc: BitVector n. |
---|
[240] | 116 | zip_with Bool Bool Bool n exclusive_disjunction b c. |
---|
[232] | 117 | |
---|
[240] | 118 | interpretation "BitVector exclusive disjunction" |
---|
| 119 | 'exclusive_disjunction b c = (exclusive_disjunction ? b c). |
---|
| 120 | |
---|
[337] | 121 | ndefinition negation_bv ≝ |
---|
[234] | 122 | λn: Nat. |
---|
| 123 | λb: BitVector n. |
---|
| 124 | map Bool Bool n (negation) b. |
---|
[240] | 125 | |
---|
| 126 | interpretation "BitVector negation" 'negation b c = (negation ? b c). |
---|
[238] | 127 | |
---|
| 128 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 129 | (* Rotates and shifts. *) |
---|
| 130 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 131 | |
---|
[362] | 132 | (* |
---|
[337] | 133 | ndefinition rotate_left_bv ≝ |
---|
| 134 | λn, m: Nat. |
---|
[238] | 135 | λb: BitVector n. |
---|
| 136 | rotate_left Bool n m b. |
---|
| 137 | |
---|
[337] | 138 | ndefinition rotate_right_bv ≝ |
---|
| 139 | λn, m: Nat. |
---|
[238] | 140 | λb: BitVector n. |
---|
[240] | 141 | rotate_right Bool n m b. |
---|
[236] | 142 | |
---|
[337] | 143 | ndefinition shift_left_bv ≝ |
---|
| 144 | λn, m: Nat. |
---|
[240] | 145 | λb: BitVector n. |
---|
| 146 | λc: Bool. |
---|
| 147 | shift_left Bool n m b c. |
---|
| 148 | |
---|
[337] | 149 | ndefinition shift_right_bv ≝ |
---|
| 150 | λn, m: Nat. |
---|
[240] | 151 | λb: BitVector n. |
---|
| 152 | λc: Bool. |
---|
| 153 | shift_right Bool n m b c. |
---|
[362] | 154 | *) |
---|
| 155 | |
---|
[236] | 156 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 157 | (* Conversions to and from lists and natural numbers. *) |
---|
| 158 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
[232] | 159 | |
---|
[362] | 160 | (* |
---|
[237] | 161 | ndefinition list_of_bitvector ≝ |
---|
| 162 | λn: Nat. |
---|
| 163 | λb: BitVector n. |
---|
| 164 | list_of_vector Bool n b. |
---|
[236] | 165 | |
---|
[237] | 166 | ndefinition bitvector_of_list ≝ |
---|
| 167 | λl: List Bool. |
---|
| 168 | vector_of_list Bool l. |
---|
[362] | 169 | *) |
---|
[234] | 170 | |
---|
[353] | 171 | nlet rec bitvector_of_nat_aux (n: Nat) (bound: Nat) on bound ≝ |
---|
| 172 | match bound with |
---|
| 173 | [ Z ⇒ Empty Bool (* IT WILL NOT HAPPEN *) |
---|
| 174 | | S bound ⇒ |
---|
| 175 | let divrem ≝ divide_with_remainder n (S (S Z)) in |
---|
| 176 | let div ≝ first Nat Nat divrem in |
---|
| 177 | let rem ≝ second Nat Nat divrem in |
---|
| 178 | match div with |
---|
| 179 | [ Z ⇒ |
---|
| 180 | match rem with |
---|
| 181 | [ Z ⇒ Empty Bool |
---|
| 182 | | S r ⇒ true :: (bitvector_of_nat_aux Z bound) |
---|
| 183 | ] |
---|
| 184 | | S d ⇒ |
---|
| 185 | match rem with |
---|
| 186 | [ Z ⇒ false :: (bitvector_of_nat_aux (S d) bound) |
---|
| 187 | | S r ⇒ true :: (bitvector_of_nat_aux (S d) bound) |
---|
| 188 | ] |
---|
| 189 | ]]. |
---|
[236] | 190 | |
---|
[315] | 191 | ndefinition eq_bv ≝ |
---|
| 192 | λn: Nat. |
---|
| 193 | λb, c: BitVector n. |
---|
| 194 | eq_v Bool n (λd, e. |
---|
| 195 | if inclusive_disjunction (conjunction d e) (conjunction (negation d) |
---|
| 196 | (negation e)) then |
---|
| 197 | true |
---|
| 198 | else |
---|
| 199 | false) b c. |
---|
| 200 | |
---|
[273] | 201 | nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝ |
---|
[353] | 202 | let biglist ≝ reverse ? (bitvector_of_nat_aux m m) in |
---|
[273] | 203 | let size ≝ length ? biglist in |
---|
[362] | 204 | let bitvector ≝ vector_of_list ? biglist in |
---|
[273] | 205 | let difference ≝ n - size in |
---|
[351] | 206 | less_than_or_equal_b_elim … |
---|
| 207 | (λH:size ≤ n. ((pad difference size bitvector)⌈BitVector n ↦ BitVector (difference+size)⌉)) |
---|
| 208 | (λH:¬(size ≤ n). max n). |
---|
| 209 | nnormalize; nrewrite > (plus_minus_inverse_right n ?); //; nassumption. |
---|
[273] | 210 | nqed. |
---|
| 211 | |
---|
[237] | 212 | nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b ≝ |
---|
| 213 | match b with |
---|
| 214 | [ Empty ⇒ Z |
---|
| 215 | | Cons o hd tl ⇒ |
---|
[260] | 216 | let hdval ≝ match hd with [ true ⇒ S Z | false ⇒ Z ] in |
---|
[248] | 217 | ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl |
---|
[349] | 218 | ]. |
---|