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