source:src/ASM/Arithmetic.ma@1928

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

Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should rightfully be in another file. Added a new file, ASM/UtilBranch.ma for code that should rightfully be in ASM/Util.ma but is incomplete (i.e. daemons).

File size: 17.2 KB
Line
1include "ASM/BitVector.ma".
2include "ASM/Util.ma".
3
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
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
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
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
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
164lemma bitvector_of_nat_ok:
165  ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y.
166 #n elim n -n
167 [ #x #y #Hx #Hy #Heq <(le_n_O_to_eq ? (le_S_S_to_le ?? Hx)) <(le_n_O_to_eq ? (le_S_S_to_le ?? Hy)) @refl
168 | #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *)
169 ]
170qed.
171
172lemma bitvector_of_nat_abs:
173  ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y).
174 #n #x #y #Hx #Hy #Heq @notb_elim
175 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)))
176 cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %);
177 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H / by I/
178 | #H / by I/
179 ]
180qed.
181
182axiom nat_of_bitvector_bitvector_of_nat_inverse:
183  ∀n: nat.
184  ∀b: nat.
185    b < 2^n → nat_of_bitvector n (bitvector_of_nat n b) = b.
186
187axiom bitvector_of_nat_inverse_nat_of_bitvector:
188  ∀n: nat.
189  ∀b: BitVector n.
190    bitvector_of_nat n (nat_of_bitvector n b) = b.
191
192lemma nat_of_bitvector_aux_injective:
193  ∀n: nat.
194  ∀l, r: BitVector n.
195  ∀acc_l, acc_r: nat.
196    nat_of_bitvector_aux n acc_l l = nat_of_bitvector_aux n acc_r r →
197      acc_l = acc_r ∧ l ≃ r.
198  #n #l
199  elim l #r
200  [1:
201    #acc_l #acc_r normalize
202    >(BitVector_O r) normalize /2/
203  |2:
204    #hd #tl #inductive_hypothesis #r #acc_l #acc_r
205    normalize normalize in inductive_hypothesis;
206    cases (BitVector_Sn … r)
207    #r_hd * #r_tl #r_refl destruct normalize
208    cases hd cases r_hd normalize
209    [1:
210      #relevant
211      cases (inductive_hypothesis … relevant)
212      #acc_assm #tl_assm destruct % //
213      lapply (injective_plus_l ? ? ? acc_assm)
214      -acc_assm #acc_assm
215      change with (2 * acc_l = 2 * acc_r) in acc_assm;
216      lapply (injective_times_r ? ? ? ? acc_assm) /2/
217    |4:
218      #relevant
219      cases (inductive_hypothesis … relevant)
220      #acc_assm #tl_assm destruct % //
221      change with (2 * acc_l = 2 * acc_r) in acc_assm;
222      lapply(injective_times_r ? ? ? ? acc_assm) /2/
223    |2:
224      #relevant
225      change with ((nat_of_bitvector_aux r (2 * acc_l + 1) tl) =
226        (nat_of_bitvector_aux r (2 * acc_r) r_tl)) in relevant;
227      cases (eqb_decidable … (2 * acc_l + 1) (2 * acc_r))
228      [1:
229        #eqb_true_assm
230        lapply (eqb_true_to_refl … eqb_true_assm)
231        #refl_assm
232        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
233      |2:
234        #eqb_false_assm
235        lapply (eqb_false_to_not_refl … eqb_false_assm)
236        #not_refl_assm cases not_refl_assm #absurd_assm
237        cases (inductive_hypothesis … relevant) #absurd
238        cases (absurd_assm absurd)
239      ]
240    |3:
241      #relevant
242      change with ((nat_of_bitvector_aux r (2 * acc_l) tl) =
243        (nat_of_bitvector_aux r (2 * acc_r + 1) r_tl)) in relevant;
244      cases (eqb_decidable … (2 * acc_l) (2 * acc_r + 1))
245      [1:
246        #eqb_true_assm
247        lapply (eqb_true_to_refl … eqb_true_assm)
248        #refl_assm
249        lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm)
250        -refl_assm #refl_assm
251        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
252      |2:
253        #eqb_false_assm
254        lapply (eqb_false_to_not_refl … eqb_false_assm)
255        #not_refl_assm cases not_refl_assm #absurd_assm
256        cases (inductive_hypothesis … relevant) #absurd
257        cases (absurd_assm absurd)
258      ]
259    ]
260  ]
261qed.
262
263lemma nat_of_bitvector_destruct:
264  ∀n: nat.
265  ∀l_hd, r_hd: bool.
266  ∀l_tl, r_tl: BitVector n.
267    nat_of_bitvector (S n) (l_hd:::l_tl) = nat_of_bitvector (S n) (r_hd:::r_tl) →
268      l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl.
269  #n #l_hd #r_hd #l_tl #r_tl
270  normalize
271  cases l_hd cases r_hd
272  normalize
273  [4:
274    /2/
275  |1:
276    #relevant
277    cases (nat_of_bitvector_aux_injective … relevant)
278    #_ #l_r_tl_refl destruct /2/
279  |2,3:
280    #relevant
281    cases (nat_of_bitvector_aux_injective … relevant)
282    #absurd destruct(absurd)
283  ]
284qed.
285
286lemma BitVector_cons_injective:
287  ∀n: nat.
288  ∀l_hd, r_hd: bool.
289  ∀l_tl, r_tl: BitVector n.
290    l_hd = r_hd → l_tl = r_tl → l_hd:::l_tl = r_hd:::r_tl.
291  #l #l_hd #r_hd #l_tl #r_tl
292  #l_refl #r_refl destruct %
293qed.
294
295lemma refl_nat_of_bitvector_to_refl:
296  ∀n: nat.
297  ∀l, r: BitVector n.
298    nat_of_bitvector n l = nat_of_bitvector n r → l = r.
299  #n
300  elim n
301  [1:
302    #l #r
303    >(BitVector_O l)
304    >(BitVector_O r)
305    #_ %
306  |2:
307    #n' #inductive_hypothesis #l #r
308    lapply (BitVector_Sn ? l) #l_hypothesis
309    lapply (BitVector_Sn ? r) #r_hypothesis
310    cases l_hypothesis #l_hd #l_tail_hypothesis
311    cases r_hypothesis #r_hd #r_tail_hypothesis
312    cases l_tail_hypothesis #l_tl #l_hd_tl_refl
313    cases r_tail_hypothesis #r_tl #r_hd_tl_refl
314    destruct #cons_refl
315    cases (nat_of_bitvector_destruct n' l_hd r_hd l_tl r_tl cons_refl)
316    #hd_refl #tl_refl
317    @BitVector_cons_injective try assumption
318    @inductive_hypothesis assumption
319  ]
320qed.
321
322definition two_complement_negation ≝
323  λn: nat.
324  λb: BitVector n.
325    let new_b ≝ negation_bv n b in
326      increment n new_b.
327
329  λn: nat.
330  λb, c: BitVector n.
331    let 〈res,flags〉 ≝ add_with_carries n b c false in
332      res.
333
334definition subtraction ≝
335  λn: nat.
336  λb, c: BitVector n.
337    addition_n n b (two_complement_negation n c).
338
339let rec mult_aux (m,n:nat) (b:BitVector m) (c:BitVector (S n)) (acc:BitVector (S n)) on b : BitVector (S n) ≝
340match b with
341[ VEmpty ⇒ acc
342| VCons m' hd tl ⇒
343    let acc' ≝ if hd then addition_n ? c acc else acc in
344    mult_aux m' n tl (shift_right_1 ?? c false) acc'
345].
346
347definition multiplication : ∀n:nat. BitVector n → BitVector n → BitVector (n + n) ≝
348  λn: nat.
349  match n return λn.BitVector n → BitVector n → BitVector (n + n) with
350  [ O ⇒ λ_.λ_.[[ ]]
351  | S m ⇒
352    λb, c : BitVector (S m).
353    let c' ≝ pad (S m) (S m) c in
354      mult_aux ?? b (shift_left ?? m c' false) (zero ?)
355  ].
356
357(* Division:  001...000 divided by 000...010
358     Shift the divisor as far left as possible,
359                                  100...000
360      then try subtracting it at each
361      bit position, shifting left as we go.
362              001...000 - 100...000 X ⇒ 0
363              001...000 - 010...000 X ⇒ 0
364              001...000 - 001...000 Y ⇒ 1 (use subtracted value as new quotient)
365              ...
366      Then pad out the remaining bits at the front
367         00..001...
368*)
369inductive fbs_diff : nat → Type[0] ≝
370| fbs_diff' : ∀n,m. fbs_diff (S (n+m)).
371
372let rec first_bit_set (n:nat) (b:BitVector n) on b : option (fbs_diff n) ≝
373match b return λn.λ_. option (fbs_diff n) with
374[ VEmpty ⇒ None ?
375| VCons m h t ⇒
376    if h then Some ? (fbs_diff' O m)
377    else match first_bit_set m t with
378         [ None ⇒ None ?
379         | Some o ⇒ match o return λx.λ_. option (fbs_diff (S x)) with [ fbs_diff' x y ⇒ Some ? (fbs_diff' (S x) y) ]
380         ]
381].
382
383let rec divmod_u_aux (n,m:nat) (q:BitVector (S n)) (d:BitVector (S n)) on m : BitVector m × (BitVector (S n)) ≝
384match m with
385[ O ⇒ 〈[[ ]], q〉
386| S m' ⇒
387    let 〈q',flags〉 ≝ add_with_carries ? q (two_complement_negation ? d) false in
388    let bit ≝ head' … flags in
389    let q'' ≝ if bit then q' else q in
390    let 〈tl, md〉 ≝ divmod_u_aux n m' q'' (shift_right_1 ?? d false) in
391    〈bit:::tl, md〉
392].
393
394definition divmod_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n) × (BitVector (S n))) ≝
395  λn: nat.
396  λb, c: BitVector (S n).
397
398    match first_bit_set ? c with
399    [ None ⇒ None ?
400    | Some fbs' ⇒
401        match fbs' return λx.λ_.option (BitVector x × (BitVector (S n))) with [ fbs_diff' fbs m ⇒
402          let 〈d,m〉 ≝ (divmod_u_aux ? (S fbs) b (shift_left ?? fbs c false)) in
403          Some ? 〈switch_bv_plus ??? (pad ?? d), m〉
404        ]
405    ].
406
407definition division_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
408λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\fst p) ].
409
410definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
411  λn.
412    match n with
413    [ O ⇒ λb, c. None ?
414    | S p ⇒ λb, c: BitVector (S p).
415        let b_sign_bit ≝ get_index_v ? ? b O ? in
416        let c_sign_bit ≝ get_index_v ? ? c O ? in
417        match b_sign_bit with
418        [ true ⇒
419          let neg_b ≝ two_complement_negation ? b in
420          match c_sign_bit with
421          [ true ⇒
422              (* I was worrying slightly about -2^(n-1), whose negation can't
423                 be represented in an n bit signed number.  However, it's
424                 negation comes out as 2^(n-1) as an n bit *unsigned* number,
425                 so it's fine. *)
426              division_u ? neg_b (two_complement_negation ? c)
427          | false ⇒
428              match division_u ? neg_b c with
429              [ None ⇒ None ?
430              | Some r ⇒ Some ? (two_complement_negation ? r)
431              ]
432          ]
433        | false ⇒
434          match c_sign_bit with
435          [ true ⇒
436              match division_u ? b (two_complement_negation ? c) with
437              [ None ⇒ None ?
438              | Some r ⇒ Some ? (two_complement_negation ? r)
439              ]
440          | false ⇒ division_u ? b c
441          ]
442        ]
443   ].
444    //
445qed.
446
447definition modulus_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
448λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\snd p) ].
449
450definition modulus_s ≝
451  λn.
452  λb, c: BitVector n.
453    match division_s n b c with
454      [ None ⇒ None ?
455      | Some result ⇒
456          let 〈high_bits, low_bits〉 ≝ split bool ? n (multiplication n result c) in
457            Some ? (subtraction n b low_bits)
458      ].
459
460definition lt_u ≝
461  fold_right2_i ???
462    (λ_.λa,b,r.
463      match a with
464      [ true ⇒ b ∧ r
465      | false ⇒ b ∨ r
466      ])
467    false.
468
469definition gt_u ≝ λn, b, c. lt_u n c b.
470
471definition lte_u ≝ λn, b, c. ¬(gt_u n b c).
472
473definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
474
475definition lt_s ≝
476  λn.
477  λb, c: BitVector n.
478    let 〈result, borrows〉 ≝ sub_with_borrows n b c false in
479    match borrows with
480    [ VEmpty ⇒ false
481    | VCons _ bwn tl ⇒
482      match tl with
483      [ VEmpty ⇒ false
484      | VCons _ bwpn _ ⇒
485        if xorb bwn bwpn then
486          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
487        else
488          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
489      ]
490    ].
491
492definition gt_s ≝ λn,b,c. lt_s n c b.
493
494definition lte_s ≝ λn,b,c. ¬(gt_s n b c).
495
496definition gte_s ≝ λn. λb, c. ¬(lt_s n b c).
497
498alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
499
500definition max_u ≝ λn,a,b. if lt_u n a b then b else a.
501definition min_u ≝ λn,a,b. if lt_u n a b then a else b.
502definition max_s ≝ λn,a,b. if lt_s n a b then b else a.
503definition min_s ≝ λn,a,b. if lt_s n a b then a else b.
504
505definition bitvector_of_bool:
506      ∀n: nat. ∀b: bool. BitVector (S n) ≝
507  λn: nat.
508  λb: bool.
509   (pad n 1 [[b]])⌈n + 1 ↦ S n⌉.
510  //
511qed.
512
514  λn: nat.
515  λb, c: BitVector n.
516  λd: Bit.
517    fold_right2_i ? ? ? (
518      λn.
519       λb1, b2: bool.
520        λd: Bit × (BitVector n).
521        let 〈c1,r〉 ≝ d in
522          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
523           (xorb (xorb b1 b2) c1) ::: r〉)
524     〈d, [[ ]]〉 ? b c.
525
527  λn: nat.
528  λb, c: BitVector n.
529    full_add n b c false.
530
531definition sign_bit : ∀n. BitVector n → bool ≝
532λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
533
534definition sign_extend : ∀m,n. BitVector m → BitVector (n+m) ≝
535λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
536
537definition zero_ext : ∀m,n. BitVector m → BitVector n ≝
538λm,n.
539  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
540  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (pad … v)
541  | nat_eq n' ⇒ λv. v
542  | nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v))
543  ].
544
545definition sign_ext : ∀m,n. BitVector m → BitVector n ≝
546λm,n.
547  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
548  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (sign_extend … v)
549  | nat_eq n' ⇒ λv. v
550  | nat_gt m' n' ⇒ λv. \snd (split … (switch_bv_plus … v))
551  ].
552
Note: See TracBrowser for help on using the repository browser.