[698] | 1 | include "ASM/BitVector.ma". |
---|
| 2 | include "ASM/Util.ma". |
---|
[475] | 3 | |
---|
| 4 | definition nat_of_bool ≝ |
---|
| 5 | λb: bool. |
---|
| 6 | match b with |
---|
| 7 | [ false ⇒ O |
---|
| 8 | | true ⇒ S O |
---|
| 9 | ]. |
---|
[697] | 10 | |
---|
| 11 | definition carry_of : bool → bool → bool → bool ≝ |
---|
| 12 | λa,b,c. match a with [ false ⇒ b ∧ c | true ⇒ b ∨ c ]. |
---|
| 13 | |
---|
| 14 | definition add_with_carries : ∀n:nat. BitVector n → BitVector n → bool → |
---|
| 15 | BitVector n × (BitVector n) ≝ |
---|
| 16 | λn,x,y,init_carry. |
---|
| 17 | fold_right2_i ??? |
---|
| 18 | (λn,b,c,r. |
---|
| 19 | let 〈lower_bits, carries〉 ≝ r in |
---|
| 20 | let last_carry ≝ match carries with [ VEmpty ⇒ init_carry | VCons _ cy _ ⇒ cy ] in |
---|
| 21 | let bit ≝ exclusive_disjunction (exclusive_disjunction b c) last_carry in |
---|
| 22 | let carry ≝ carry_of b c last_carry in |
---|
| 23 | 〈bit:::lower_bits, carry:::carries〉 |
---|
| 24 | ) |
---|
| 25 | 〈[[ ]], [[ ]]〉 n x y. |
---|
| 26 | |
---|
| 27 | (* Essentially the only difference for subtraction. *) |
---|
| 28 | definition borrow_of : bool → bool → bool → bool ≝ |
---|
| 29 | λa,b,c. match a with [ false ⇒ b ∨ c | true ⇒ b ∧ c ]. |
---|
| 30 | |
---|
| 31 | definition sub_with_borrows : ∀n:nat. BitVector n → BitVector n → bool → |
---|
| 32 | BitVector n × (BitVector n) ≝ |
---|
| 33 | λn,x,y,init_borrow. |
---|
| 34 | fold_right2_i ??? |
---|
| 35 | (λn,b,c,r. |
---|
| 36 | let 〈lower_bits, borrows〉 ≝ r in |
---|
| 37 | let last_borrow ≝ match borrows with [ VEmpty ⇒ init_borrow | VCons _ bw _ ⇒ bw ] in |
---|
| 38 | let bit ≝ exclusive_disjunction (exclusive_disjunction b c) last_borrow in |
---|
| 39 | let borrow ≝ borrow_of b c last_borrow in |
---|
| 40 | 〈bit:::lower_bits, borrow:::borrows〉 |
---|
| 41 | ) |
---|
| 42 | 〈[[ ]], [[ ]]〉 n x y. |
---|
[475] | 43 | |
---|
| 44 | definition add_n_with_carry: |
---|
[697] | 45 | ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. n ≥ 5 → |
---|
| 46 | (BitVector n) × (BitVector 3) ≝ |
---|
[475] | 47 | λn: nat. |
---|
| 48 | λb: BitVector n. |
---|
| 49 | λc: BitVector n. |
---|
| 50 | λcarry: bool. |
---|
[697] | 51 | λpf:n ≥ 5. |
---|
| 52 | |
---|
| 53 | let 〈result, carries〉 ≝ add_with_carries n b c carry in |
---|
| 54 | let cy_flag ≝ get_index_v ?? carries 0 ? in |
---|
| 55 | let ov_flag ≝ exclusive_disjunction cy_flag (get_index_v ?? carries 1 ?) in |
---|
| 56 | let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *) |
---|
| 57 | 〈result, [[ cy_flag; ac_flag; ov_flag ]]〉. |
---|
| 58 | // @(transitive_le … pf) /2/ |
---|
| 59 | qed. |
---|
[475] | 60 | |
---|
[697] | 61 | definition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. n ≥ 5 → |
---|
| 62 | (BitVector n) × (BitVector 3) ≝ |
---|
[475] | 63 | λn: nat. |
---|
| 64 | λb: BitVector n. |
---|
| 65 | λc: BitVector n. |
---|
| 66 | λcarry: bool. |
---|
[697] | 67 | λpf:n ≥ 5. |
---|
| 68 | |
---|
| 69 | let 〈result, carries〉 ≝ sub_with_borrows n b c carry in |
---|
| 70 | let cy_flag ≝ get_index_v ?? carries 0 ? in |
---|
| 71 | let ov_flag ≝ exclusive_disjunction cy_flag (get_index_v ?? carries 1 ?) in |
---|
| 72 | let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *) |
---|
| 73 | 〈result, [[ cy_flag; ac_flag; ov_flag ]]〉. |
---|
| 74 | // @(transitive_le … pf) /2/ |
---|
| 75 | qed. |
---|
| 76 | |
---|
[712] | 77 | definition add_8_with_carry ≝ |
---|
| 78 | λb, c: BitVector 8. |
---|
| 79 | λcarry: bool. |
---|
| 80 | add_n_with_carry 8 b c carry ?. |
---|
| 81 | @le_S @le_S @le_S @le_n (* ugly: fix using tacticals *) |
---|
| 82 | qed. |
---|
[475] | 83 | |
---|
[712] | 84 | definition add_16_with_carry ≝ |
---|
| 85 | λb, c: BitVector 16. |
---|
| 86 | λcarry: bool. |
---|
| 87 | add_n_with_carry 16 b c carry ?. |
---|
| 88 | @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S |
---|
| 89 | @le_S @le_S @le_n (* ugly: fix using tacticals *) |
---|
| 90 | qed. |
---|
| 91 | |
---|
| 92 | definition sub_8_with_carry ≝ |
---|
| 93 | λb, c: BitVector 8. |
---|
| 94 | λcarry: bool. |
---|
| 95 | sub_n_with_carry 8 b c carry ?. |
---|
| 96 | @le_S @le_S @le_S @le_n (* ugly: fix using tacticals *) |
---|
| 97 | qed. |
---|
| 98 | |
---|
| 99 | definition sub_16_with_carry ≝ |
---|
| 100 | λb, c: BitVector 16. |
---|
| 101 | λcarry: bool. |
---|
| 102 | sub_n_with_carry 16 b c carry ?. |
---|
| 103 | @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S |
---|
| 104 | @le_S @le_S @le_n (* ugly: fix using tacticals *) |
---|
| 105 | qed. |
---|
| 106 | |
---|
[475] | 107 | definition increment ≝ |
---|
| 108 | λn: nat. |
---|
| 109 | λb: BitVector n. |
---|
[697] | 110 | \fst (add_with_carries n b (zero n) true). |
---|
[475] | 111 | |
---|
| 112 | definition decrement ≝ |
---|
| 113 | λn: nat. |
---|
| 114 | λb: BitVector n. |
---|
[697] | 115 | \fst (sub_with_borrows n b (zero n) true). |
---|
[724] | 116 | |
---|
| 117 | let rec bitvector_of_nat_aux (n,m:nat) (v:BitVector n) on m : BitVector n ≝ |
---|
| 118 | match m with |
---|
| 119 | [ O ⇒ v |
---|
| 120 | | S m' ⇒ bitvector_of_nat_aux n m' (increment n v) |
---|
| 121 | ]. |
---|
| 122 | |
---|
| 123 | definition bitvector_of_nat : ∀n:nat. nat → BitVector n ≝ |
---|
| 124 | λn,m. bitvector_of_nat_aux n m (zero n). |
---|
| 125 | |
---|
| 126 | let rec nat_of_bitvector_aux (n,m:nat) (v:BitVector n) on v : nat ≝ |
---|
| 127 | match v with |
---|
| 128 | [ VEmpty ⇒ m |
---|
| 129 | | VCons n' hd tl ⇒ nat_of_bitvector_aux n' (if hd then 2*m +1 else 2*m) tl |
---|
| 130 | ]. |
---|
| 131 | |
---|
| 132 | definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝ |
---|
| 133 | λn,v. nat_of_bitvector_aux n O v. |
---|
| 134 | |
---|
[475] | 135 | definition two_complement_negation ≝ |
---|
| 136 | λn: nat. |
---|
| 137 | λb: BitVector n. |
---|
| 138 | let new_b ≝ negation_bv n b in |
---|
| 139 | increment n new_b. |
---|
| 140 | |
---|
| 141 | definition addition_n ≝ |
---|
| 142 | λn: nat. |
---|
| 143 | λb, c: BitVector n. |
---|
[697] | 144 | let 〈res,flags〉 ≝ add_with_carries n b c false in |
---|
[475] | 145 | res. |
---|
| 146 | |
---|
| 147 | definition subtraction ≝ |
---|
| 148 | λn: nat. |
---|
| 149 | λb, c: BitVector n. |
---|
| 150 | addition_n n b (two_complement_negation n c). |
---|
[744] | 151 | |
---|
| 152 | let rec mult_aux (m,n:nat) (b:BitVector m) (c:BitVector (S n)) (acc:BitVector (S n)) on b : BitVector (S n) ≝ |
---|
| 153 | match b with |
---|
| 154 | [ VEmpty ⇒ acc |
---|
| 155 | | VCons m' hd tl ⇒ |
---|
| 156 | let acc' ≝ if hd then addition_n ? c acc else acc in |
---|
| 157 | mult_aux m' n tl (shift_right_1 ?? c false) acc' |
---|
| 158 | ]. |
---|
| 159 | |
---|
| 160 | definition multiplication : ∀n:nat. BitVector n → BitVector n → BitVector (n + n) ≝ |
---|
[475] | 161 | λn: nat. |
---|
[744] | 162 | match n return λn.BitVector n → BitVector n → BitVector (n + n) with |
---|
| 163 | [ O ⇒ λ_.λ_.[[ ]] |
---|
| 164 | | S m ⇒ |
---|
| 165 | λb, c : BitVector (S m). |
---|
| 166 | let c' ≝ pad (S m) (S m) c in |
---|
| 167 | mult_aux ?? b (shift_left ?? m c' false) (zero ?) |
---|
| 168 | ]. |
---|
| 169 | |
---|
| 170 | (* Division: 001...000 divided by 000...010 |
---|
| 171 | Shift the divisor as far left as possible, |
---|
| 172 | 100...000 |
---|
| 173 | then try subtracting it at each |
---|
| 174 | bit position, shifting left as we go. |
---|
| 175 | 001...000 - 100...000 X ⇒ 0 |
---|
| 176 | 001...000 - 010...000 X ⇒ 0 |
---|
| 177 | 001...000 - 001...000 Y ⇒ 1 (use subtracted value as new quotient) |
---|
| 178 | ... |
---|
| 179 | Then pad out the remaining bits at the front |
---|
| 180 | 00..001... |
---|
| 181 | *) |
---|
| 182 | inductive fbs_diff : nat → Type[0] ≝ |
---|
| 183 | | fbs_diff' : ∀n,m. fbs_diff (S (n+m)). |
---|
| 184 | |
---|
| 185 | let rec first_bit_set (n:nat) (b:BitVector n) on b : option (fbs_diff n) ≝ |
---|
| 186 | match b return λn.λ_. option (fbs_diff n) with |
---|
| 187 | [ VEmpty ⇒ None ? |
---|
| 188 | | VCons m h t ⇒ |
---|
| 189 | if h then Some ? (fbs_diff' O m) |
---|
| 190 | else match first_bit_set m t with |
---|
| 191 | [ None ⇒ None ? |
---|
| 192 | | Some o ⇒ match o return λx.λ_. option (fbs_diff (S x)) with [ fbs_diff' x y ⇒ Some ? (fbs_diff' (S x) y) ] |
---|
| 193 | ] |
---|
| 194 | ]. |
---|
| 195 | |
---|
| 196 | let rec divmod_u_aux (n,m:nat) (q:BitVector (S n)) (d:BitVector (S n)) on m : BitVector m × (BitVector (S n)) ≝ |
---|
| 197 | match m with |
---|
| 198 | [ O ⇒ 〈[[ ]], q〉 |
---|
| 199 | | S m' ⇒ |
---|
| 200 | let 〈q',flags〉 ≝ add_with_carries ? q (two_complement_negation ? d) false in |
---|
| 201 | let bit ≝ head' … flags in |
---|
| 202 | let q'' ≝ if bit then q' else q in |
---|
| 203 | let 〈tl, md〉 ≝ divmod_u_aux n m' q'' (shift_right_1 ?? d false) in |
---|
| 204 | 〈bit:::tl, md〉 |
---|
| 205 | ]. |
---|
| 206 | |
---|
| 207 | definition divmod_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n) × (BitVector (S n))) ≝ |
---|
[475] | 208 | λn: nat. |
---|
[744] | 209 | λb, c: BitVector (S n). |
---|
| 210 | |
---|
| 211 | match first_bit_set ? c with |
---|
| 212 | [ None ⇒ None ? |
---|
| 213 | | Some fbs' ⇒ |
---|
| 214 | match fbs' return λx.λ_.option (BitVector x × (BitVector (S n))) with [ fbs_diff' fbs m ⇒ |
---|
| 215 | let 〈d,m〉 ≝ (divmod_u_aux ? (S fbs) b (shift_left ?? fbs c false)) in |
---|
| 216 | Some ? 〈switch_bv_plus ??? (pad ?? d), m〉 |
---|
| 217 | ] |
---|
[475] | 218 | ]. |
---|
[744] | 219 | |
---|
| 220 | definition division_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝ |
---|
| 221 | λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\fst p) ]. |
---|
[475] | 222 | |
---|
[697] | 223 | definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝ |
---|
[475] | 224 | λn. |
---|
| 225 | match n with |
---|
| 226 | [ O ⇒ λb, c. None ? |
---|
| 227 | | S p ⇒ λb, c: BitVector (S p). |
---|
| 228 | let b_sign_bit ≝ get_index_v ? ? b O ? in |
---|
| 229 | let c_sign_bit ≝ get_index_v ? ? c O ? in |
---|
[744] | 230 | match b_sign_bit with |
---|
| 231 | [ true ⇒ |
---|
| 232 | let neg_b ≝ two_complement_negation ? b in |
---|
| 233 | match c_sign_bit with |
---|
[475] | 234 | [ true ⇒ |
---|
[744] | 235 | (* I was worrying slightly about -2^(n-1), whose negation can't |
---|
| 236 | be represented in an n bit signed number. However, it's |
---|
| 237 | negation comes out as 2^(n-1) as an n bit *unsigned* number, |
---|
| 238 | so it's fine. *) |
---|
| 239 | division_u ? neg_b (two_complement_negation ? c) |
---|
[475] | 240 | | false ⇒ |
---|
[744] | 241 | match division_u ? neg_b c with |
---|
| 242 | [ None ⇒ None ? |
---|
| 243 | | Some r ⇒ Some ? (two_complement_negation ? r) |
---|
| 244 | ] |
---|
[475] | 245 | ] |
---|
[744] | 246 | | false ⇒ |
---|
| 247 | match c_sign_bit with |
---|
| 248 | [ true ⇒ |
---|
| 249 | match division_u ? b (two_complement_negation ? c) with |
---|
| 250 | [ None ⇒ None ? |
---|
| 251 | | Some r ⇒ Some ? (two_complement_negation ? r) |
---|
| 252 | ] |
---|
| 253 | | false ⇒ division_u ? b c |
---|
| 254 | ] |
---|
[475] | 255 | ] |
---|
[744] | 256 | ]. |
---|
[475] | 257 | // |
---|
| 258 | qed. |
---|
| 259 | |
---|
[744] | 260 | definition modulus_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝ |
---|
| 261 | λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\snd p) ]. |
---|
[475] | 262 | |
---|
| 263 | definition modulus_s ≝ |
---|
| 264 | λn. |
---|
| 265 | λb, c: BitVector n. |
---|
| 266 | match division_s n b c with |
---|
| 267 | [ None ⇒ None ? |
---|
| 268 | | Some result ⇒ |
---|
| 269 | let 〈high_bits, low_bits〉 ≝ split bool ? n (multiplication n result c) in |
---|
| 270 | Some ? (subtraction n b low_bits) |
---|
| 271 | ]. |
---|
| 272 | |
---|
| 273 | definition lt_u ≝ |
---|
[697] | 274 | fold_right2_i ??? |
---|
| 275 | (λ_.λa,b,r. |
---|
| 276 | match a with |
---|
| 277 | [ true ⇒ b ∧ r |
---|
| 278 | | false ⇒ b ∨ r |
---|
| 279 | ]) |
---|
| 280 | false. |
---|
[475] | 281 | |
---|
| 282 | definition gt_u ≝ λn, b, c. lt_u n c b. |
---|
| 283 | |
---|
| 284 | definition lte_u ≝ λn, b, c. ¬(gt_u n b c). |
---|
| 285 | |
---|
| 286 | definition gte_u ≝ λn, b, c. ¬(lt_u n b c). |
---|
[697] | 287 | |
---|
[475] | 288 | definition lt_s ≝ |
---|
| 289 | λn. |
---|
| 290 | λb, c: BitVector n. |
---|
[697] | 291 | let 〈result, borrows〉 ≝ sub_with_borrows n b c false in |
---|
| 292 | match borrows with |
---|
| 293 | [ VEmpty ⇒ false |
---|
| 294 | | VCons _ bwn tl ⇒ |
---|
| 295 | match tl with |
---|
| 296 | [ VEmpty ⇒ false |
---|
| 297 | | VCons _ bwpn _ ⇒ |
---|
| 298 | if exclusive_disjunction bwn bwpn then |
---|
| 299 | match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ] |
---|
| 300 | else |
---|
| 301 | match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ] |
---|
| 302 | ] |
---|
| 303 | ]. |
---|
| 304 | |
---|
[475] | 305 | definition gt_s ≝ λn,b,c. lt_s n c b. |
---|
| 306 | |
---|
| 307 | definition lte_s ≝ λn,b,c. ¬(gt_s n b c). |
---|
| 308 | |
---|
| 309 | definition gte_s ≝ λn. λb, c. ¬(lt_s n b c). |
---|
| 310 | |
---|
| 311 | alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop". |
---|
| 312 | |
---|
| 313 | definition bitvector_of_bool: |
---|
| 314 | ∀n: nat. ∀b: bool. BitVector (S n) ≝ |
---|
| 315 | λn: nat. |
---|
| 316 | λb: bool. |
---|
| 317 | (pad n 1 [[b]])⌈n + 1 ↦ S n⌉. |
---|
| 318 | // |
---|
| 319 | qed. |
---|
| 320 | |
---|
| 321 | definition full_add ≝ |
---|
| 322 | λn: nat. |
---|
| 323 | λb, c: BitVector n. |
---|
| 324 | λd: Bit. |
---|
| 325 | fold_right2_i ? ? ? ( |
---|
| 326 | λn. |
---|
| 327 | λb1, b2: bool. |
---|
| 328 | λd: Bit × (BitVector n). |
---|
| 329 | let 〈c1,r〉 ≝ d in |
---|
| 330 | 〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)), |
---|
| 331 | (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉) |
---|
| 332 | 〈d, [[ ]]〉 ? b c. |
---|
| 333 | |
---|
| 334 | definition half_add ≝ |
---|
| 335 | λn: nat. |
---|
| 336 | λb, c: BitVector n. |
---|
| 337 | full_add n b c false. |
---|