[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 "Universes.ma". |
---|
[224] | 9 | |
---|
[246] | 10 | include "Vector.ma". |
---|
| 11 | include "List.ma". |
---|
| 12 | include "Nat.ma". |
---|
| 13 | include "Bool.ma". |
---|
[240] | 14 | |
---|
[236] | 15 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 16 | (* Common synonyms. *) |
---|
| 17 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 18 | |
---|
[228] | 19 | ndefinition BitVector ≝ λn: Nat. Vector Bool n. |
---|
[263] | 20 | ndefinition Bit ≝ Bool. |
---|
[230] | 21 | ndefinition Nibble ≝ BitVector (S (S (S (S Z)))). |
---|
| 22 | ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))). |
---|
| 23 | ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))). |
---|
| 24 | ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))). |
---|
[271] | 25 | ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S Z))))))))))). |
---|
[224] | 26 | |
---|
[236] | 27 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
[240] | 28 | (* Lookup. *) |
---|
| 29 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 30 | |
---|
[337] | 31 | ndefinition get_index_bv ≝ |
---|
[240] | 32 | λn: Nat. |
---|
| 33 | λb: BitVector n. |
---|
| 34 | λm: Nat. |
---|
[266] | 35 | λp: m < n. |
---|
| 36 | get_index Bool n b m p. |
---|
[240] | 37 | |
---|
| 38 | interpretation "BitVector get_index" 'get_index b n = (get_index ? b n). |
---|
| 39 | |
---|
[337] | 40 | ndefinition set_index_bv ≝ |
---|
[240] | 41 | λn: Nat. |
---|
| 42 | λb: BitVector n. |
---|
| 43 | λm: Nat. |
---|
[266] | 44 | λp: m < n. |
---|
| 45 | λc: Bool. |
---|
[314] | 46 | set_index Bool n b m c. |
---|
[240] | 47 | |
---|
| 48 | ndefinition drop ≝ |
---|
| 49 | λn: Nat. |
---|
| 50 | λb: BitVector n. |
---|
| 51 | λm: Nat. |
---|
| 52 | drop Bool n b m. |
---|
| 53 | |
---|
| 54 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
[236] | 55 | (* Creating bitvectors from scratch. *) |
---|
| 56 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 57 | |
---|
[228] | 58 | ndefinition zero ≝ |
---|
| 59 | λn: Nat. |
---|
[260] | 60 | ((replicate Bool n false): BitVector n). |
---|
[228] | 61 | |
---|
[236] | 62 | ndefinition max ≝ |
---|
| 63 | λn: Nat. |
---|
[260] | 64 | ((replicate Bool n true): BitVector n). |
---|
[236] | 65 | |
---|
[237] | 66 | ndefinition append ≝ |
---|
| 67 | λm, n: Nat. |
---|
| 68 | λb: BitVector m. |
---|
| 69 | λc: BitVector n. |
---|
| 70 | append Bool m n b c. |
---|
[240] | 71 | |
---|
[237] | 72 | ndefinition pad ≝ |
---|
| 73 | λm, n: Nat. |
---|
| 74 | λb: BitVector n. |
---|
[260] | 75 | let padding ≝ replicate Bool m false in |
---|
[237] | 76 | append Bool m n padding b. |
---|
[240] | 77 | |
---|
| 78 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 79 | (* Other manipulations. *) |
---|
| 80 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
[237] | 81 | |
---|
[240] | 82 | ndefinition reverse ≝ |
---|
| 83 | λn: Nat. |
---|
| 84 | λb: BitVector n. |
---|
| 85 | reverse Bool n b. |
---|
| 86 | |
---|
| 87 | ndefinition length ≝ |
---|
| 88 | λn: Nat. |
---|
| 89 | λb: BitVector n. |
---|
| 90 | length Bool n b. |
---|
| 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 | |
---|
[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. |
---|
| 154 | |
---|
[236] | 155 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
| 156 | (* Conversions to and from lists and natural numbers. *) |
---|
| 157 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
[232] | 158 | |
---|
[237] | 159 | ndefinition list_of_bitvector ≝ |
---|
| 160 | λn: Nat. |
---|
| 161 | λb: BitVector n. |
---|
| 162 | list_of_vector Bool n b. |
---|
[236] | 163 | |
---|
[237] | 164 | ndefinition bitvector_of_list ≝ |
---|
| 165 | λl: List Bool. |
---|
| 166 | vector_of_list Bool l. |
---|
[234] | 167 | |
---|
[235] | 168 | nlet rec bitvector_of_nat_aux (n: Nat) on n ≝ |
---|
[237] | 169 | let divrem ≝ divide_with_remainder n (S (S Z)) in |
---|
| 170 | let div ≝ first Nat Nat divrem in |
---|
| 171 | let rem ≝ second Nat Nat divrem in |
---|
[235] | 172 | match div with |
---|
| 173 | [ Z ⇒ |
---|
| 174 | match rem with |
---|
| 175 | [ Z ⇒ Empty Bool |
---|
[260] | 176 | | S r ⇒ ? (true :: (bitvector_of_nat_aux Z)) |
---|
[235] | 177 | ] |
---|
| 178 | | S d ⇒ |
---|
| 179 | match rem with |
---|
[260] | 180 | [ Z ⇒ ? (false :: (bitvector_of_nat_aux (S d))) |
---|
| 181 | | S r ⇒ ? (true :: (bitvector_of_nat_aux (S d))) |
---|
[235] | 182 | ] |
---|
[236] | 183 | ]. |
---|
[237] | 184 | //. |
---|
| 185 | nqed. |
---|
[236] | 186 | |
---|
[315] | 187 | ndefinition eq_bv ≝ |
---|
| 188 | λn: Nat. |
---|
| 189 | λb, c: BitVector n. |
---|
| 190 | eq_v Bool n (λd, e. |
---|
| 191 | if inclusive_disjunction (conjunction d e) (conjunction (negation d) |
---|
| 192 | (negation e)) then |
---|
| 193 | true |
---|
| 194 | else |
---|
| 195 | false) b c. |
---|
| 196 | |
---|
[273] | 197 | nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝ |
---|
| 198 | let biglist ≝ reverse ? (bitvector_of_nat_aux m) in |
---|
| 199 | let size ≝ length ? biglist in |
---|
| 200 | let bitvector ≝ bitvector_of_list biglist in |
---|
| 201 | let difference ≝ n - size in |
---|
| 202 | match greater_than_b size n with |
---|
| 203 | [ true ⇒ max n |
---|
| 204 | | false ⇒ ? (pad difference size bitvector) |
---|
| 205 | ]. |
---|
| 206 | nnormalize. |
---|
| 207 | nrewrite > (plus_minus_inverse_right n ?). |
---|
| 208 | #H. |
---|
| 209 | nassumption. |
---|
| 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 |
---|
[260] | 218 | ]. |
---|
[313] | 219 | |
---|
| 220 | naxiom full_add: |
---|
| 221 | ∀n: Nat. |
---|
| 222 | ∀b, c: BitVector n. |
---|
| 223 | ∀d: Bit. |
---|
| 224 | Bool × (BitVector n). |
---|
[320] | 225 | |
---|
| 226 | ndefinition half_add ≝ |
---|
| 227 | λn: Nat. |
---|
| 228 | λb, c: BitVector n. |
---|
| 229 | full_add n b c false. |
---|