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

Last change on this file since 981 was 961, checked in by campbell, 10 years ago

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File size: 11.6 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
143definition 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
150  λn: nat.
151  λb, c: BitVector n.
152    let 〈res,flags〉 ≝ add_with_carries n b c false in
153      res.
154
155definition subtraction ≝
156  λn: nat.
157  λb, c: BitVector n.
158    addition_n n b (two_complement_negation n c).
159
160let rec mult_aux (m,n:nat) (b:BitVector m) (c:BitVector (S n)) (acc:BitVector (S n)) on b : BitVector (S n) ≝
161match 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
168definition 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*)
190inductive fbs_diff : nat → Type[0] ≝
191| fbs_diff' : ∀n,m. fbs_diff (S (n+m)).
192
193let rec first_bit_set (n:nat) (b:BitVector n) on b : option (fbs_diff n) ≝
194match 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
204let rec divmod_u_aux (n,m:nat) (q:BitVector (S n)) (d:BitVector (S n)) on m : BitVector m × (BitVector (S n)) ≝
205match 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
215definition 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
228definition 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
231definition 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    //
266qed.
267
268definition 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
271definition 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
281definition 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
290definition gt_u ≝ λn, b, c. lt_u n c b.
291
292definition lte_u ≝ λn, b, c. ¬(gt_u n b c).
293
294definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
295
296definition 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
313definition gt_s ≝ λn,b,c. lt_s n c b.
314
315definition lte_s ≝ λn,b,c. ¬(gt_s n b c).
316
317definition gte_s ≝ λn. λb, c. ¬(lt_s n b c).
318
319alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
320
321definition 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  //
327qed.
328
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
343  λn: nat.
344  λb, c: BitVector n.
345    full_add n b c false.
346
347definition sign_bit : ∀n. BitVector n → bool ≝
348λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
349
350definition sign_extend : ∀m,n. BitVector m → BitVector (n+m) ≝
351λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
352
353definition zero_ext : ∀m,n. BitVector m → BitVector n ≝
354λm,n.
355  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
356  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (pad … v)
357  | nat_eq n' ⇒ λv. v
358  | nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v))
359  ].
360
361definition sign_ext : ∀m,n. BitVector m → BitVector n ≝
362λm,n.
363  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
364  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (sign_extend … v)
365  | nat_eq n' ⇒ λv. v
366  | nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v))
367  ].
368
Note: See TracBrowser for help on using the repository browser.