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