source: src/ASM/Arithmetic.ma @ 2222

Last change on this file since 2222 was 2192, checked in by sacerdot, 7 years ago

Shuffling around.

File size: 24.3 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〉 ≝ vsplit … 8 8 pc in
8  let 〈n1, n2〉 ≝ vsplit … 4 4 pc_upper in
9  let 〈b123, b〉 ≝ vsplit … 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
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 bitvector_of_nat_exp_zero: ∀n.bitvector_of_nat n (2^n) = zero n.
183
184axiom nat_of_bitvector_bitvector_of_nat_inverse:
185  ∀n: nat.
186  ∀b: nat.
187    b < 2^n → nat_of_bitvector n (bitvector_of_nat n b) = b.
188
189axiom bitvector_of_nat_inverse_nat_of_bitvector:
190  ∀n: nat.
191  ∀b: BitVector n.
192    bitvector_of_nat n (nat_of_bitvector n b) = b.
193
194axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n.
195
196axiom eq_bitvector_of_nat_to_eq:
197 ∀n,n1,n2.
198  n1 < 2^n → n2 < 2^n →
199   bitvector_of_nat n n1 = bitvector_of_nat n n2 → n1=n2.
200
201lemma nat_of_bitvector_aux_injective:
202  ∀n: nat.
203  ∀l, r: BitVector n.
204  ∀acc_l, acc_r: nat.
205    nat_of_bitvector_aux n acc_l l = nat_of_bitvector_aux n acc_r r →
206      acc_l = acc_r ∧ l ≃ r.
207  #n #l
208  elim l #r
209  [1:
210    #acc_l #acc_r normalize
211    >(BitVector_O r) normalize /2/
212  |2:
213    #hd #tl #inductive_hypothesis #r #acc_l #acc_r
214    normalize normalize in inductive_hypothesis;
215    cases (BitVector_Sn … r)
216    #r_hd * #r_tl #r_refl destruct normalize
217    cases hd cases r_hd normalize
218    [1:
219      #relevant
220      cases (inductive_hypothesis … relevant)
221      #acc_assm #tl_assm destruct % //
222      lapply (injective_plus_l ? ? ? acc_assm)
223      -acc_assm #acc_assm
224      change with (2 * acc_l = 2 * acc_r) in acc_assm;
225      lapply (injective_times_r ? ? ? ? acc_assm) /2/
226    |4:
227      #relevant
228      cases (inductive_hypothesis … relevant)
229      #acc_assm #tl_assm destruct % //
230      change with (2 * acc_l = 2 * acc_r) in acc_assm;
231      lapply(injective_times_r ? ? ? ? acc_assm) /2/
232    |2:
233      #relevant 
234      change with ((nat_of_bitvector_aux r (2 * acc_l + 1) tl) =
235        (nat_of_bitvector_aux r (2 * acc_r) r_tl)) in relevant;
236      cases (eqb_decidable … (2 * acc_l + 1) (2 * acc_r))
237      [1:
238        #eqb_true_assm
239        lapply (eqb_true_to_refl … eqb_true_assm)
240        #refl_assm
241        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
242      |2:
243        #eqb_false_assm
244        lapply (eqb_false_to_not_refl … eqb_false_assm)
245        #not_refl_assm cases not_refl_assm #absurd_assm
246        cases (inductive_hypothesis … relevant) #absurd
247        cases (absurd_assm absurd)
248      ]
249    |3:
250      #relevant 
251      change with ((nat_of_bitvector_aux r (2 * acc_l) tl) =
252        (nat_of_bitvector_aux r (2 * acc_r + 1) r_tl)) in relevant;
253      cases (eqb_decidable … (2 * acc_l) (2 * acc_r + 1))
254      [1:
255        #eqb_true_assm
256        lapply (eqb_true_to_refl … eqb_true_assm)
257        #refl_assm
258        lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm)
259        -refl_assm #refl_assm
260        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
261      |2:
262        #eqb_false_assm
263        lapply (eqb_false_to_not_refl … eqb_false_assm)
264        #not_refl_assm cases not_refl_assm #absurd_assm
265        cases (inductive_hypothesis … relevant) #absurd
266        cases (absurd_assm absurd)
267      ]
268    ]
269  ]
270qed.
271
272lemma nat_of_bitvector_destruct:
273  ∀n: nat.
274  ∀l_hd, r_hd: bool.
275  ∀l_tl, r_tl: BitVector n.
276    nat_of_bitvector (S n) (l_hd:::l_tl) = nat_of_bitvector (S n) (r_hd:::r_tl) →
277      l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl.
278  #n #l_hd #r_hd #l_tl #r_tl
279  normalize
280  cases l_hd cases r_hd
281  normalize
282  [4:
283    /2/
284  |1:
285    #relevant
286    cases (nat_of_bitvector_aux_injective … relevant)
287    #_ #l_r_tl_refl destruct /2/
288  |2,3:
289    #relevant
290    cases (nat_of_bitvector_aux_injective … relevant)
291    #absurd destruct(absurd)
292  ]
293qed.
294
295lemma BitVector_cons_injective:
296  ∀n: nat.
297  ∀l_hd, r_hd: bool.
298  ∀l_tl, r_tl: BitVector n.
299    l_hd = r_hd → l_tl = r_tl → l_hd:::l_tl = r_hd:::r_tl.
300  #l #l_hd #r_hd #l_tl #r_tl
301  #l_refl #r_refl destruct %
302qed.
303
304lemma refl_nat_of_bitvector_to_refl:
305  ∀n: nat.
306  ∀l, r: BitVector n.
307    nat_of_bitvector n l = nat_of_bitvector n r → l = r.
308  #n
309  elim n
310  [1:
311    #l #r
312    >(BitVector_O l)
313    >(BitVector_O r)
314    #_ %
315  |2:
316    #n' #inductive_hypothesis #l #r
317    lapply (BitVector_Sn ? l) #l_hypothesis
318    lapply (BitVector_Sn ? r) #r_hypothesis
319    cases l_hypothesis #l_hd #l_tail_hypothesis
320    cases r_hypothesis #r_hd #r_tail_hypothesis
321    cases l_tail_hypothesis #l_tl #l_hd_tl_refl
322    cases r_tail_hypothesis #r_tl #r_hd_tl_refl
323    destruct #cons_refl
324    cases (nat_of_bitvector_destruct n' l_hd r_hd l_tl r_tl cons_refl)
325    #hd_refl #tl_refl
326    @BitVector_cons_injective try assumption
327    @inductive_hypothesis assumption
328  ]
329qed.
330
331definition two_complement_negation ≝
332  λn: nat.
333  λb: BitVector n.
334    let new_b ≝ negation_bv n b in
335      increment n new_b.
336   
337definition addition_n ≝
338  λn: nat.
339  λb, c: BitVector n.
340    let 〈res,flags〉 ≝ add_with_carries n b c false in
341      res.
342   
343definition subtraction ≝
344  λn: nat.
345  λb, c: BitVector n.
346    addition_n n b (two_complement_negation n c).
347
348let rec mult_aux (m,n:nat) (b:BitVector m) (c:BitVector (S n)) (acc:BitVector (S n)) on b : BitVector (S n) ≝
349match b with
350[ VEmpty ⇒ acc
351| VCons m' hd tl ⇒
352    let acc' ≝ if hd then addition_n ? c acc else acc in
353    mult_aux m' n tl (shift_right_1 ?? c false) acc'
354].
355
356definition multiplication : ∀n:nat. BitVector n → BitVector n → BitVector (n + n) ≝
357  λn: nat.
358  match n return λn.BitVector n → BitVector n → BitVector (n + n) with
359  [ O ⇒ λ_.λ_.[[ ]]
360  | S m ⇒
361    λb, c : BitVector (S m).
362    let c' ≝ pad (S m) (S m) c in
363      mult_aux ?? b (shift_left ?? m c' false) (zero ?)
364  ].
365
366definition short_multiplication : ∀n:nat. BitVector n → BitVector n → BitVector n ≝
367λn,x,y. (\snd (vsplit ??? (multiplication ? x y))).
368
369(* Division:  001...000 divided by 000...010
370     Shift the divisor as far left as possible,
371                                  100...000
372      then try subtracting it at each
373      bit position, shifting left as we go.
374              001...000 - 100...000 X ⇒ 0
375              001...000 - 010...000 X ⇒ 0
376              001...000 - 001...000 Y ⇒ 1 (use subtracted value as new quotient)
377              ...
378      Then pad out the remaining bits at the front
379         00..001...
380*)
381inductive fbs_diff : nat → Type[0] ≝
382| fbs_diff' : ∀n,m. fbs_diff (S (n+m)).
383
384let rec first_bit_set (n:nat) (b:BitVector n) on b : option (fbs_diff n) ≝
385match b return λn.λ_. option (fbs_diff n) with
386[ VEmpty ⇒ None ?
387| VCons m h t ⇒
388    if h then Some ? (fbs_diff' O m)
389    else match first_bit_set m t with
390         [ None ⇒ None ?
391         | Some o ⇒ match o return λx.λ_. option (fbs_diff (S x)) with [ fbs_diff' x y ⇒ Some ? (fbs_diff' (S x) y) ]
392         ]
393].
394
395let rec divmod_u_aux (n,m:nat) (q:BitVector (S n)) (d:BitVector (S n)) on m : BitVector m × (BitVector (S n)) ≝
396match m with
397[ O ⇒ 〈[[ ]], q〉
398| S m' ⇒
399    let 〈q',flags〉 ≝ add_with_carries ? q (two_complement_negation ? d) false in
400    let bit ≝ head' … flags in
401    let q'' ≝ if bit then q' else q in
402    let 〈tl, md〉 ≝ divmod_u_aux n m' q'' (shift_right_1 ?? d false) in
403    〈bit:::tl, md〉
404].
405
406definition divmod_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n) × (BitVector (S n))) ≝
407  λn: nat.
408  λb, c: BitVector (S n).
409
410    match first_bit_set ? c with
411    [ None ⇒ None ?
412    | Some fbs' ⇒
413        match fbs' return λx.λ_.option (BitVector x × (BitVector (S n))) with [ fbs_diff' fbs m ⇒
414          let 〈d,m〉 ≝ (divmod_u_aux ? (S fbs) b (shift_left ?? fbs c false)) in
415          Some ? 〈switch_bv_plus ??? (pad ?? d), m〉
416        ]
417    ].
418
419definition division_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
420λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\fst p) ].
421     
422definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
423  λn.
424    match n with
425    [ O ⇒ λb, c. None ?
426    | S p ⇒ λb, c: BitVector (S p).
427        let b_sign_bit ≝ get_index_v ? ? b O ? in
428        let c_sign_bit ≝ get_index_v ? ? c O ? in
429        match b_sign_bit with
430        [ true ⇒
431          let neg_b ≝ two_complement_negation ? b in
432          match c_sign_bit with
433          [ true ⇒
434              (* I was worrying slightly about -2^(n-1), whose negation can't
435                 be represented in an n bit signed number.  However, it's
436                 negation comes out as 2^(n-1) as an n bit *unsigned* number,
437                 so it's fine. *)
438              division_u ? neg_b (two_complement_negation ? c)
439          | false ⇒
440              match division_u ? neg_b c with
441              [ None ⇒ None ?
442              | Some r ⇒ Some ? (two_complement_negation ? r)
443              ]
444          ]
445        | false ⇒
446          match c_sign_bit with
447          [ true ⇒
448              match division_u ? b (two_complement_negation ? c) with
449              [ None ⇒ None ?
450              | Some r ⇒ Some ? (two_complement_negation ? r)
451              ]
452          | false ⇒ division_u ? b c
453          ]
454        ]
455   ].
456    //
457qed.
458
459definition modulus_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
460λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\snd p) ].
461           
462definition modulus_s ≝
463  λn.
464  λb, c: BitVector n.
465    match division_s n b c with
466      [ None ⇒ None ?
467      | Some result ⇒
468          let 〈high_bits, low_bits〉 ≝ vsplit bool ? n (multiplication n result c) in
469            Some ? (subtraction n b low_bits)
470      ].
471     
472definition lt_u ≝
473  fold_right2_i ???
474    (λ_.λa,b,r.
475      match a with
476      [ true ⇒ b ∧ r
477      | false ⇒ b ∨ r
478      ])
479    false.
480     
481definition gt_u ≝ λn, b, c. lt_u n c b.
482
483definition lte_u ≝ λn, b, c. ¬(gt_u n b c).
484
485definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
486
487definition lt_s ≝
488  λn.
489  λb, c: BitVector n.
490    let 〈result, borrows〉 ≝ sub_with_borrows n b c false in
491    match borrows with
492    [ VEmpty ⇒ false
493    | VCons _ bwn tl ⇒
494      match tl with
495      [ VEmpty ⇒ false
496      | VCons _ bwpn _ ⇒
497        if xorb bwn bwpn then
498          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
499        else
500          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
501      ]
502    ].
503   
504definition gt_s ≝ λn,b,c. lt_s n c b.
505
506definition lte_s ≝ λn,b,c. ¬(gt_s n b c).
507
508definition gte_s ≝ λn. λb, c. ¬(lt_s n b c).
509     
510alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
511
512definition max_u ≝ λn,a,b. if lt_u n a b then b else a.
513definition min_u ≝ λn,a,b. if lt_u n a b then a else b.
514definition max_s ≝ λn,a,b. if lt_s n a b then b else a.
515definition min_s ≝ λn,a,b. if lt_s n a b then a else b.
516
517definition bitvector_of_bool:
518      ∀n: nat. ∀b: bool. BitVector (S n) ≝
519  λn: nat.
520  λb: bool.
521   (pad n 1 [[b]])⌈n + 1 ↦ S n⌉.
522  //
523qed.
524
525definition full_add ≝
526  λn: nat.
527  λb, c: BitVector n.
528  λd: Bit.
529    fold_right2_i ? ? ? (
530      λn.
531       λb1, b2: bool.
532        λd: Bit × (BitVector n).
533        let 〈c1,r〉 ≝ d in
534          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
535           (xorb (xorb b1 b2) c1) ::: r〉)
536     〈d, [[ ]]〉 ? b c.
537   
538definition half_add ≝
539  λn: nat.
540  λb, c: BitVector n.
541    full_add n b c false.
542
543definition add ≝
544  λn: nat.
545  λl, r: BitVector n.
546    \snd (half_add n l r).
547
548lemma half_add_carry_Sn:
549  ∀n: nat.
550  ∀l: BitVector n.
551  ∀hd: bool.
552    \fst (half_add (S n) (hd:::l) (false:::(zero n))) =
553      andb hd (\fst (half_add n l (zero n))).
554  #n #l elim l
555  [1:
556    #hd normalize cases hd %
557  |2:
558    #n' #hd #tl #inductive_hypothesis #hd'
559    whd in match half_add; normalize nodelta
560    whd in match full_add; normalize nodelta
561    normalize in ⊢ (??%%); cases hd' normalize
562    @pair_elim #c1 #r #c1_r_refl cases c1 %
563  ]
564qed.
565
566lemma half_add_zero_carry_false:
567  ∀m: nat.
568  ∀b: BitVector m.
569    \fst (half_add m b (zero m)) = false.
570  #m #b elim b try %
571  #n #hd #tl #inductive_hypothesis
572  change with (false:::(zero ?)) in match (zero ?);
573  >half_add_carry_Sn >inductive_hypothesis cases hd %
574qed.
575
576axiom half_add_true_true_carry_true:
577  ∀n: nat.
578  ∀hd, hd': bool.
579  ∀l, r: BitVector n.
580    \fst (half_add (S n) (true:::l) (true:::r)) = true.
581
582lemma add_Sn_carry_add:
583  ∀n: nat.
584  ∀hd, hd': bool.
585  ∀l, r: BitVector n.
586    add (S n) (hd:::l) (hd':::r) =
587      xorb (xorb hd hd') (\fst (half_add n l r)):::add n l r.
588  #n #hd #hd' #l elim l
589  [1:
590    #r cases hd cases hd'
591    >(BitVector_O … r) normalize %
592  |2:
593    #n' #hd'' #tl #inductive_hypothesis #r
594    cases (BitVector_Sn … r) #hd''' * #tl' #r_refl destruct
595    cases hd cases hd' cases hd'' cases hd'''
596    whd in match (xorb ??);
597    cases daemon
598  ]
599qed.
600 
601lemma add_zero:
602  ∀n: nat.
603  ∀l: BitVector n.
604    l = add n l (zero …).
605  #n #l elim l try %
606  #n' #hd #tl #inductive_hypothesis
607  change with (false:::zero ?) in match (zero ?);
608  >add_Sn_carry_add >half_add_zero_carry_false
609  cases hd <inductive_hypothesis %
610qed.
611
612axiom most_significant_bit_zero:
613  ∀size, m: nat.
614  ∀size_proof: 0 < size.
615    m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false.
616  normalize in size_proof; normalize @le_S_S assumption
617qed.
618   
619axiom zero_add_head:
620  ∀m: nat.
621  ∀tl, hd.
622    (hd:::add m (zero m) tl) = add (S m) (zero (S m)) (hd:::tl).
623
624lemma zero_add:
625  ∀m: nat.
626  ∀b: BitVector m.
627    add m (zero m) b = b.
628  #m #b elim b try %
629  #m' #hd #tl #inductive_hypothesis
630  <inductive_hypothesis in ⊢ (???%);
631  >zero_add_head %
632qed.
633
634axiom bitvector_of_nat_one_Sm:
635  ∀m: nat.
636    ∃b: BitVector m.
637      bitvector_of_nat (S m) 1 ≃ b @@ [[true]].
638
639axiom increment_zero_bitvector_of_nat_1:
640  ∀m: nat.
641  ∀b: BitVector m.
642    increment m b = add m (bitvector_of_nat m 1) b.
643
644axiom add_associative:
645  ∀m: nat.
646  ∀l, c, r: BitVector m.
647    add m l (add m c r) = add m (add m l c) r.
648
649lemma bitvector_of_nat_aux_buffer:
650  ∀m, n: nat.
651  ∀b: BitVector m.
652    bitvector_of_nat_aux m n b = add m (bitvector_of_nat m n) b.
653  #m #n elim n
654  [1:
655    #b change with (? = add ? (zero …) b)
656    >zero_add %
657  |2:
658    #n' #inductive_hypothesis #b
659    whd in match (bitvector_of_nat_aux ???);
660    >inductive_hypothesis whd in match (bitvector_of_nat ??) in ⊢ (???%);
661    >inductive_hypothesis >increment_zero_bitvector_of_nat_1
662    >increment_zero_bitvector_of_nat_1 <(add_zero m (bitvector_of_nat m 1))
663    <add_associative %
664  ]
665qed.
666
667definition sign_extension: Byte → Word ≝
668  λc.
669    let b ≝ get_index_v ? 8 c 1 ? in
670      [[ b; b; b; b; b; b; b; b ]] @@ c.
671  normalize
672  repeat (@le_S_S)
673  @le_O_n
674qed.
675
676lemma bitvector_of_nat_sign_extension_equivalence:
677  ∀m: nat.
678  ∀size_proof: m < 128.
679    sign_extension … (bitvector_of_nat 8 m) = bitvector_of_nat 16 m.
680  #m #size_proof whd in ⊢ (??%?);
681  >most_significant_bit_zero
682  [1:
683    elim m
684    [1:
685      %
686    |2:
687      #n' #inductive_hypothesis whd in match bitvector_of_nat; normalize nodelta
688      whd in match (bitvector_of_nat_aux ???);
689      whd in match (bitvector_of_nat_aux ???) in ⊢ (???%);
690      >(bitvector_of_nat_aux_buffer 16 n')
691      cases daemon
692    ]
693  |2:
694    assumption
695  ]
696qed.
697
698axiom add_commutative:
699  ∀n: nat.
700  ∀l, r: BitVector n.
701    add … l r = add … r l.
702
703axiom nat_of_bitvector_add:
704 ∀n,v1,v2.
705  nat_of_bitvector n v1 + nat_of_bitvector n v2 < 2^n →
706   nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2.
707
708axiom add_bitvector_of_nat:
709 ∀n,m1,m2.
710  bitvector_of_nat n (m1 + m2) =
711   add n (bitvector_of_nat n m1) (bitvector_of_nat n m2).
712
713(* CSC: corollary of add_bitvector_of_nat *)
714axiom add_overflow:
715 ∀n,m,r. m + r = 2^n →
716  add n (bitvector_of_nat n m) (bitvector_of_nat n r) = zero n.
717
718example add_SO:
719  ∀n: nat.
720  ∀m: nat.
721    add n (bitvector_of_nat … m) (bitvector_of_nat … 1) = bitvector_of_nat … (S m).
722 cases daemon.
723qed.
724
725axiom add_bitvector_of_nat_plus:
726  ∀n,p,q:nat.
727    add n (bitvector_of_nat ? p) (bitvector_of_nat ? q) = bitvector_of_nat ? (p+q).
728   
729lemma add_bitvector_of_nat_Sm:
730  ∀n, m: nat.
731    add … (bitvector_of_nat … 1) (bitvector_of_nat … m) =
732      bitvector_of_nat n (S m).
733 #n #m @add_bitvector_of_nat_plus
734qed.
735
736axiom le_to_le_nat_of_bitvector_add:
737  ∀n,v,m1,m2.
738    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 ≤ m2 →
739      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) ≤
740      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
741
742lemma lt_to_lt_nat_of_bitvector_add:
743  ∀n,v,m1,m2.
744    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 →
745      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) <
746      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
747#n #v #m1 #m2 #m2_ok #bounded #H
748lapply (le_to_le_nat_of_bitvector_add n v (S m1) m2 ??) try assumption
749#K @(transitive_le … (K H))
750cases daemon (*CSC: TRUE, complete*)
751qed.
752
753definition sign_bit : ∀n. BitVector n → bool ≝
754λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
755
756definition sign_extend : ∀m,n. BitVector m → BitVector (n+m) ≝
757λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
758
759definition zero_ext : ∀m,n. BitVector m → BitVector n ≝
760λm,n.
761  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
762  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (pad … v)
763  | nat_eq n' ⇒ λv. v
764  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
765  ].
766
767definition sign_ext : ∀m,n. BitVector m → BitVector n ≝
768λm,n.
769  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
770  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (sign_extend … v)
771  | nat_eq n' ⇒ λv. v
772  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
773  ].
774
775example sub_minus_one_seven_eight:
776  ∀v: BitVector 7.
777  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
778  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
779 cases daemon.
780qed.
781
782axiom sub16_with_carry_overflow:
783  ∀left, right, result: BitVector 16.
784  ∀flags: BitVector 3.
785  ∀upper: BitVector 9.
786  ∀lower: BitVector 7.
787    sub_16_with_carry left right false = 〈result, flags〉 →
788      vsplit bool 9 7 result = 〈upper, lower〉 →
789        get_index_v bool 3 flags 2 ? = true →
790          upper = [[true; true; true; true; true; true; true; true; true]].
791  //
792qed.
793
794axiom sub_16_to_add_16_8_0:
795 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
796  get_index' ? 2 0 flags = false →
797  sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 →
798   v1 = add ? v2 (sign_extension (false:::v3)).
799
800axiom sub_16_to_add_16_8_1:
801 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
802  get_index' ? 2 0 flags = true →
803  sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 →
804   v1 = add ? v2 (sign_extension (true:::v3)).
Note: See TracBrowser for help on using the repository browser.