# source:src/ASM/Arithmetic.ma@1404

Last change on this file since 1404 was 1404, checked in by boender, 9 years ago
• added an axiom to arithmetic, but should be provable
File size: 12.0 KB
Line
1include "ASM/BitVector.ma".
2include "ASM/Util.ma".
3
4definition nat_of_bool ≝
5  λb: bool.
6    match b with
7      [ false ⇒ O
8      | true ⇒ S O
9      ].
10
11definition carry_of : bool → bool → bool → bool ≝
12λa,b,c. match a with [ false ⇒ b ∧ c | true ⇒ b ∨ c ].
13
14definition 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. *)
28definition borrow_of : bool → bool → bool → bool ≝
29λa,b,c. match a with [ false ⇒ b ∨ c | true ⇒ b ∧ c ].
30
31definition 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
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/
59qed.
60
61definition 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/
75qed.
76
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 *)
82qed.
83
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 *)
90qed.
91
92(* dpm: needed for assembly proof *)
93definition 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
98qed.
99
100definition 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 *)
105qed.
106
107definition 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 *)
113qed.
114
115definition increment ≝
116  λn: nat.
117  λb: BitVector n.
118    \fst (add_with_carries n b (zero n) true).
119
120definition decrement ≝
121  λn: nat.
122  λb: BitVector n.
123    \fst (sub_with_borrows n b (zero n) true).
124
125let 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
131definition bitvector_of_nat : ∀n:nat. nat → BitVector n ≝
132  λn,m. bitvector_of_nat_aux n m (zero n).
133
134let rec nat_of_bitvector_aux (n,m:nat) (v:BitVector n) on v : nat ≝
135match 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
140definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝
141  λn,v. nat_of_bitvector_aux n O v.
142
143axiom bitvector_of_nat_ok:
144  ∀n,x,y.bitvector_of_nat (S n) x = bitvector_of_nat (S n) y → x = y.
145(* if anyone wants to prove this... *)
146
147definition two_complement_negation ≝
148  λn: nat.
149  λb: BitVector n.
150    let new_b ≝ negation_bv n b in
151      increment n new_b.
152
154  λn: nat.
155  λb, c: BitVector n.
156    let 〈res,flags〉 ≝ add_with_carries n b c false in
157      res.
158
159definition subtraction ≝
160  λn: nat.
161  λb, c: BitVector n.
162    addition_n n b (two_complement_negation n c).
163
164let rec mult_aux (m,n:nat) (b:BitVector m) (c:BitVector (S n)) (acc:BitVector (S n)) on b : BitVector (S n) ≝
165match b with
166[ VEmpty ⇒ acc
167| VCons m' hd tl ⇒
168    let acc' ≝ if hd then addition_n ? c acc else acc in
169    mult_aux m' n tl (shift_right_1 ?? c false) acc'
170].
171
172definition multiplication : ∀n:nat. BitVector n → BitVector n → BitVector (n + n) ≝
173  λn: nat.
174  match n return λn.BitVector n → BitVector n → BitVector (n + n) with
175  [ O ⇒ λ_.λ_.[[ ]]
176  | S m ⇒
177    λb, c : BitVector (S m).
178    let c' ≝ pad (S m) (S m) c in
179      mult_aux ?? b (shift_left ?? m c' false) (zero ?)
180  ].
181
182(* Division:  001...000 divided by 000...010
183     Shift the divisor as far left as possible,
184                                  100...000
185      then try subtracting it at each
186      bit position, shifting left as we go.
187              001...000 - 100...000 X ⇒ 0
188              001...000 - 010...000 X ⇒ 0
189              001...000 - 001...000 Y ⇒ 1 (use subtracted value as new quotient)
190              ...
191      Then pad out the remaining bits at the front
192         00..001...
193*)
194inductive fbs_diff : nat → Type[0] ≝
195| fbs_diff' : ∀n,m. fbs_diff (S (n+m)).
196
197let rec first_bit_set (n:nat) (b:BitVector n) on b : option (fbs_diff n) ≝
198match b return λn.λ_. option (fbs_diff n) with
199[ VEmpty ⇒ None ?
200| VCons m h t ⇒
201    if h then Some ? (fbs_diff' O m)
202    else match first_bit_set m t with
203         [ None ⇒ None ?
204         | Some o ⇒ match o return λx.λ_. option (fbs_diff (S x)) with [ fbs_diff' x y ⇒ Some ? (fbs_diff' (S x) y) ]
205         ]
206].
207
208let rec divmod_u_aux (n,m:nat) (q:BitVector (S n)) (d:BitVector (S n)) on m : BitVector m × (BitVector (S n)) ≝
209match m with
210[ O ⇒ 〈[[ ]], q〉
211| S m' ⇒
212    let 〈q',flags〉 ≝ add_with_carries ? q (two_complement_negation ? d) false in
213    let bit ≝ head' … flags in
214    let q'' ≝ if bit then q' else q in
215    let 〈tl, md〉 ≝ divmod_u_aux n m' q'' (shift_right_1 ?? d false) in
216    〈bit:::tl, md〉
217].
218
219definition divmod_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n) × (BitVector (S n))) ≝
220  λn: nat.
221  λb, c: BitVector (S n).
222
223    match first_bit_set ? c with
224    [ None ⇒ None ?
225    | Some fbs' ⇒
226        match fbs' return λx.λ_.option (BitVector x × (BitVector (S n))) with [ fbs_diff' fbs m ⇒
227          let 〈d,m〉 ≝ (divmod_u_aux ? (S fbs) b (shift_left ?? fbs c false)) in
228          Some ? 〈switch_bv_plus ??? (pad ?? d), m〉
229        ]
230    ].
231
232definition division_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
233λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\fst p) ].
234
235definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
236  λn.
237    match n with
238    [ O ⇒ λb, c. None ?
239    | S p ⇒ λb, c: BitVector (S p).
240        let b_sign_bit ≝ get_index_v ? ? b O ? in
241        let c_sign_bit ≝ get_index_v ? ? c O ? in
242        match b_sign_bit with
243        [ true ⇒
244          let neg_b ≝ two_complement_negation ? b in
245          match c_sign_bit with
246          [ true ⇒
247              (* I was worrying slightly about -2^(n-1), whose negation can't
248                 be represented in an n bit signed number.  However, it's
249                 negation comes out as 2^(n-1) as an n bit *unsigned* number,
250                 so it's fine. *)
251              division_u ? neg_b (two_complement_negation ? c)
252          | false ⇒
253              match division_u ? neg_b c with
254              [ None ⇒ None ?
255              | Some r ⇒ Some ? (two_complement_negation ? r)
256              ]
257          ]
258        | false ⇒
259          match c_sign_bit with
260          [ true ⇒
261              match division_u ? b (two_complement_negation ? c) with
262              [ None ⇒ None ?
263              | Some r ⇒ Some ? (two_complement_negation ? r)
264              ]
265          | false ⇒ division_u ? b c
266          ]
267        ]
268   ].
269    //
270qed.
271
272definition modulus_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
273λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\snd p) ].
274
275definition modulus_s ≝
276  λn.
277  λb, c: BitVector n.
278    match division_s n b c with
279      [ None ⇒ None ?
280      | Some result ⇒
281          let 〈high_bits, low_bits〉 ≝ split bool ? n (multiplication n result c) in
282            Some ? (subtraction n b low_bits)
283      ].
284
285definition lt_u ≝
286  fold_right2_i ???
287    (λ_.λa,b,r.
288      match a with
289      [ true ⇒ b ∧ r
290      | false ⇒ b ∨ r
291      ])
292    false.
293
294definition gt_u ≝ λn, b, c. lt_u n c b.
295
296definition lte_u ≝ λn, b, c. ¬(gt_u n b c).
297
298definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
299
300definition lt_s ≝
301  λn.
302  λb, c: BitVector n.
303    let 〈result, borrows〉 ≝ sub_with_borrows n b c false in
304    match borrows with
305    [ VEmpty ⇒ false
306    | VCons _ bwn tl ⇒
307      match tl with
308      [ VEmpty ⇒ false
309      | VCons _ bwpn _ ⇒
310        if exclusive_disjunction bwn bwpn then
311          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
312        else
313          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
314      ]
315    ].
316
317definition gt_s ≝ λn,b,c. lt_s n c b.
318
319definition lte_s ≝ λn,b,c. ¬(gt_s n b c).
320
321definition gte_s ≝ λn. λb, c. ¬(lt_s n b c).
322
323alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
324
325definition max_u ≝ λn,a,b. if lt_u n a b then b else a.
326definition min_u ≝ λn,a,b. if lt_u n a b then a else b.
327definition max_s ≝ λn,a,b. if lt_s n a b then b else a.
328definition min_s ≝ λn,a,b. if lt_s n a b then a else b.
329
330definition bitvector_of_bool:
331      ∀n: nat. ∀b: bool. BitVector (S n) ≝
332  λn: nat.
333  λb: bool.
334   (pad n 1 [[b]])⌈n + 1 ↦ S n⌉.
335  //
336qed.
337
339  λn: nat.
340  λb, c: BitVector n.
341  λd: Bit.
342    fold_right2_i ? ? ? (
343      λn.
344       λb1, b2: bool.
345        λd: Bit × (BitVector n).
346        let 〈c1,r〉 ≝ d in
347          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
348           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
349     〈d, [[ ]]〉 ? b c.
350
352  λn: nat.
353  λb, c: BitVector n.
354    full_add n b c false.
355
356definition sign_bit : ∀n. BitVector n → bool ≝
357λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
358
359definition sign_extend : ∀m,n. BitVector m → BitVector (n+m) ≝
360λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
361
362definition zero_ext : ∀m,n. BitVector m → BitVector n ≝
363λm,n.
364  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
365  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (pad … v)
366  | nat_eq n' ⇒ λv. v
367  | nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v))
368  ].
369
370definition sign_ext : ∀m,n. BitVector m → BitVector n ≝
371λm,n.
372  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
373  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (sign_extend … v)
374  | nat_eq n' ⇒ λv. v
375  | nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v))
376  ].
377
Note: See TracBrowser for help on using the repository browser.