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

Last change on this file since 1632 was 1599, checked in by sacerdot, 8 years ago

Start of merging of stuff into the standard library of Matita.

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