source: src/ASM/Arithmetic.ma @ 1646

Last change on this file since 1646 was 1646, checked in by mulligan, 8 years ago

finished the block_costs computation, and propagated the changes forward, subject to closing two axioms (an elimination principle, and a lemma on subvectors). moved some code around to its rightful place.

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