source: Deliverables/D3.3/id-lookup-branch/ASM/Arithmetic.ma @ 3033

Last change on this file since 3033 was 1311, checked in by campbell, 8 years ago

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

File size: 11.8 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   
44definition 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/
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
77definition 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 *)
82qed.
83
84definition 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 *)
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   
149definition 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   
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 max_u ≝ λn,a,b. if lt_u n a b then b else a.
322definition min_u ≝ λn,a,b. if lt_u n a b then a else b.
323definition max_s ≝ λn,a,b. if lt_s n a b then b else a.
324definition min_s ≝ λn,a,b. if lt_s n a b then a else b.
325
326definition bitvector_of_bool:
327      ∀n: nat. ∀b: bool. BitVector (S n) ≝
328  λn: nat.
329  λb: bool.
330   (pad n 1 [[b]])⌈n + 1 ↦ S n⌉.
331  //
332qed.
333
334definition full_add ≝
335  λn: nat.
336  λb, c: BitVector n.
337  λd: Bit.
338    fold_right2_i ? ? ? (
339      λn.
340       λb1, b2: bool.
341        λd: Bit × (BitVector n).
342        let 〈c1,r〉 ≝ d in
343          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
344           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
345     〈d, [[ ]]〉 ? b c.
346   
347definition half_add ≝
348  λn: nat.
349  λb, c: BitVector n.
350    full_add n b c false.
351
352definition sign_bit : ∀n. BitVector n → bool ≝
353λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
354
355definition sign_extend : ∀m,n. BitVector m → BitVector (n+m) ≝
356λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
357
358definition zero_ext : ∀m,n. BitVector m → BitVector n ≝
359λm,n.
360  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
361  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (pad … v)
362  | nat_eq n' ⇒ λv. v
363  | nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v))
364  ].
365
366definition sign_ext : ∀m,n. BitVector m → BitVector n ≝
367λm,n.
368  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
369  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (sign_extend … v)
370  | nat_eq n' ⇒ λv. v
371  | nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v))
372  ].
373
Note: See TracBrowser for help on using the repository browser.