source: src/ASM/Arithmetic.ma @ 2154

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

Code shuffled around.

File size: 24.0 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
366(* Division:  001...000 divided by 000...010
367     Shift the divisor as far left as possible,
368                                  100...000
369      then try subtracting it at each
370      bit position, shifting left as we go.
371              001...000 - 100...000 X ⇒ 0
372              001...000 - 010...000 X ⇒ 0
373              001...000 - 001...000 Y ⇒ 1 (use subtracted value as new quotient)
374              ...
375      Then pad out the remaining bits at the front
376         00..001...
377*)
378inductive fbs_diff : nat → Type[0] ≝
379| fbs_diff' : ∀n,m. fbs_diff (S (n+m)).
380
381let rec first_bit_set (n:nat) (b:BitVector n) on b : option (fbs_diff n) ≝
382match b return λn.λ_. option (fbs_diff n) with
383[ VEmpty ⇒ None ?
384| VCons m h t ⇒
385    if h then Some ? (fbs_diff' O m)
386    else match first_bit_set m t with
387         [ None ⇒ None ?
388         | Some o ⇒ match o return λx.λ_. option (fbs_diff (S x)) with [ fbs_diff' x y ⇒ Some ? (fbs_diff' (S x) y) ]
389         ]
390].
391
392let rec divmod_u_aux (n,m:nat) (q:BitVector (S n)) (d:BitVector (S n)) on m : BitVector m × (BitVector (S n)) ≝
393match m with
394[ O ⇒ 〈[[ ]], q〉
395| S m' ⇒
396    let 〈q',flags〉 ≝ add_with_carries ? q (two_complement_negation ? d) false in
397    let bit ≝ head' … flags in
398    let q'' ≝ if bit then q' else q in
399    let 〈tl, md〉 ≝ divmod_u_aux n m' q'' (shift_right_1 ?? d false) in
400    〈bit:::tl, md〉
401].
402
403definition divmod_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n) × (BitVector (S n))) ≝
404  λn: nat.
405  λb, c: BitVector (S n).
406
407    match first_bit_set ? c with
408    [ None ⇒ None ?
409    | Some fbs' ⇒
410        match fbs' return λx.λ_.option (BitVector x × (BitVector (S n))) with [ fbs_diff' fbs m ⇒
411          let 〈d,m〉 ≝ (divmod_u_aux ? (S fbs) b (shift_left ?? fbs c false)) in
412          Some ? 〈switch_bv_plus ??? (pad ?? d), m〉
413        ]
414    ].
415
416definition division_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
417λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\fst p) ].
418     
419definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
420  λn.
421    match n with
422    [ O ⇒ λb, c. None ?
423    | S p ⇒ λb, c: BitVector (S p).
424        let b_sign_bit ≝ get_index_v ? ? b O ? in
425        let c_sign_bit ≝ get_index_v ? ? c O ? in
426        match b_sign_bit with
427        [ true ⇒
428          let neg_b ≝ two_complement_negation ? b in
429          match c_sign_bit with
430          [ true ⇒
431              (* I was worrying slightly about -2^(n-1), whose negation can't
432                 be represented in an n bit signed number.  However, it's
433                 negation comes out as 2^(n-1) as an n bit *unsigned* number,
434                 so it's fine. *)
435              division_u ? neg_b (two_complement_negation ? c)
436          | false ⇒
437              match division_u ? neg_b c with
438              [ None ⇒ None ?
439              | Some r ⇒ Some ? (two_complement_negation ? r)
440              ]
441          ]
442        | false ⇒
443          match c_sign_bit with
444          [ true ⇒
445              match division_u ? b (two_complement_negation ? c) with
446              [ None ⇒ None ?
447              | Some r ⇒ Some ? (two_complement_negation ? r)
448              ]
449          | false ⇒ division_u ? b c
450          ]
451        ]
452   ].
453    //
454qed.
455
456definition modulus_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
457λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\snd p) ].
458           
459definition modulus_s ≝
460  λn.
461  λb, c: BitVector n.
462    match division_s n b c with
463      [ None ⇒ None ?
464      | Some result ⇒
465          let 〈high_bits, low_bits〉 ≝ vsplit bool ? n (multiplication n result c) in
466            Some ? (subtraction n b low_bits)
467      ].
468     
469definition lt_u ≝
470  fold_right2_i ???
471    (λ_.λa,b,r.
472      match a with
473      [ true ⇒ b ∧ r
474      | false ⇒ b ∨ r
475      ])
476    false.
477     
478definition gt_u ≝ λn, b, c. lt_u n c b.
479
480definition lte_u ≝ λn, b, c. ¬(gt_u n b c).
481
482definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
483
484definition lt_s ≝
485  λn.
486  λb, c: BitVector n.
487    let 〈result, borrows〉 ≝ sub_with_borrows n b c false in
488    match borrows with
489    [ VEmpty ⇒ false
490    | VCons _ bwn tl ⇒
491      match tl with
492      [ VEmpty ⇒ false
493      | VCons _ bwpn _ ⇒
494        if xorb bwn bwpn then
495          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
496        else
497          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
498      ]
499    ].
500   
501definition gt_s ≝ λn,b,c. lt_s n c b.
502
503definition lte_s ≝ λn,b,c. ¬(gt_s n b c).
504
505definition gte_s ≝ λn. λb, c. ¬(lt_s n b c).
506     
507alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
508
509definition max_u ≝ λn,a,b. if lt_u n a b then b else a.
510definition min_u ≝ λn,a,b. if lt_u n a b then a else b.
511definition max_s ≝ λn,a,b. if lt_s n a b then b else a.
512definition min_s ≝ λn,a,b. if lt_s n a b then a else b.
513
514definition bitvector_of_bool:
515      ∀n: nat. ∀b: bool. BitVector (S n) ≝
516  λn: nat.
517  λb: bool.
518   (pad n 1 [[b]])⌈n + 1 ↦ S n⌉.
519  //
520qed.
521
522definition full_add ≝
523  λn: nat.
524  λb, c: BitVector n.
525  λd: Bit.
526    fold_right2_i ? ? ? (
527      λn.
528       λb1, b2: bool.
529        λd: Bit × (BitVector n).
530        let 〈c1,r〉 ≝ d in
531          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
532           (xorb (xorb b1 b2) c1) ::: r〉)
533     〈d, [[ ]]〉 ? b c.
534   
535definition half_add ≝
536  λn: nat.
537  λb, c: BitVector n.
538    full_add n b c false.
539
540definition add ≝
541  λn: nat.
542  λl, r: BitVector n.
543    \snd (half_add n l r).
544
545lemma half_add_carry_Sn:
546  ∀n: nat.
547  ∀l: BitVector n.
548  ∀hd: bool.
549    \fst (half_add (S n) (hd:::l) (false:::(zero n))) =
550      andb hd (\fst (half_add n l (zero n))).
551  #n #l elim l
552  [1:
553    #hd normalize cases hd %
554  |2:
555    #n' #hd #tl #inductive_hypothesis #hd'
556    whd in match half_add; normalize nodelta
557    whd in match full_add; normalize nodelta
558    normalize in ⊢ (??%%); cases hd' normalize
559    @pair_elim #c1 #r #c1_r_refl cases c1 %
560  ]
561qed.
562
563lemma half_add_zero_carry_false:
564  ∀m: nat.
565  ∀b: BitVector m.
566    \fst (half_add m b (zero m)) = false.
567  #m #b elim b try %
568  #n #hd #tl #inductive_hypothesis
569  change with (false:::(zero ?)) in match (zero ?);
570  >half_add_carry_Sn >inductive_hypothesis cases hd %
571qed.
572
573axiom half_add_true_true_carry_true:
574  ∀n: nat.
575  ∀hd, hd': bool.
576  ∀l, r: BitVector n.
577    \fst (half_add (S n) (true:::l) (true:::r)) = true.
578
579lemma add_Sn_carry_add:
580  ∀n: nat.
581  ∀hd, hd': bool.
582  ∀l, r: BitVector n.
583    add (S n) (hd:::l) (hd':::r) =
584      xorb (xorb hd hd') (\fst (half_add n l r)):::add n l r.
585  #n #hd #hd' #l elim l
586  [1:
587    #r cases hd cases hd'
588    >(BitVector_O … r) normalize %
589  |2:
590    #n' #hd'' #tl #inductive_hypothesis #r
591    cases (BitVector_Sn … r) #hd''' * #tl' #r_refl destruct
592    cases hd cases hd' cases hd'' cases hd'''
593    whd in match (xorb ??);
594    cases daemon
595  ]
596qed.
597 
598lemma add_zero:
599  ∀n: nat.
600  ∀l: BitVector n.
601    l = add n l (zero …).
602  #n #l elim l try %
603  #n' #hd #tl #inductive_hypothesis
604  change with (false:::zero ?) in match (zero ?);
605  >add_Sn_carry_add >half_add_zero_carry_false
606  cases hd <inductive_hypothesis %
607qed.
608
609axiom most_significant_bit_zero:
610  ∀size, m: nat.
611  ∀size_proof: 0 < size.
612    m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false.
613  normalize in size_proof; normalize @le_S_S assumption
614qed.
615   
616axiom zero_add_head:
617  ∀m: nat.
618  ∀tl, hd.
619    (hd:::add m (zero m) tl) = add (S m) (zero (S m)) (hd:::tl).
620
621lemma zero_add:
622  ∀m: nat.
623  ∀b: BitVector m.
624    add m (zero m) b = b.
625  #m #b elim b try %
626  #m' #hd #tl #inductive_hypothesis
627  <inductive_hypothesis in ⊢ (???%);
628  >zero_add_head %
629qed.
630
631axiom bitvector_of_nat_one_Sm:
632  ∀m: nat.
633    ∃b: BitVector m.
634      bitvector_of_nat (S m) 1 ≃ b @@ [[true]].
635
636axiom increment_zero_bitvector_of_nat_1:
637  ∀m: nat.
638  ∀b: BitVector m.
639    increment m b = add m (bitvector_of_nat m 1) b.
640
641axiom add_associative:
642  ∀m: nat.
643  ∀l, c, r: BitVector m.
644    add m l (add m c r) = add m (add m l c) r.
645
646lemma bitvector_of_nat_aux_buffer:
647  ∀m, n: nat.
648  ∀b: BitVector m.
649    bitvector_of_nat_aux m n b = add m (bitvector_of_nat m n) b.
650  #m #n elim n
651  [1:
652    #b change with (? = add ? (zero …) b)
653    >zero_add %
654  |2:
655    #n' #inductive_hypothesis #b
656    whd in match (bitvector_of_nat_aux ???);
657    >inductive_hypothesis whd in match (bitvector_of_nat ??) in ⊢ (???%);
658    >inductive_hypothesis >increment_zero_bitvector_of_nat_1
659    >increment_zero_bitvector_of_nat_1 <(add_zero m (bitvector_of_nat m 1))
660    <add_associative %
661  ]
662qed.
663
664definition sign_extension: Byte → Word ≝
665  λc.
666    let b ≝ get_index_v ? 8 c 1 ? in
667      [[ b; b; b; b; b; b; b; b ]] @@ c.
668  normalize
669  repeat (@le_S_S)
670  @le_O_n
671qed.
672
673lemma bitvector_of_nat_sign_extension_equivalence:
674  ∀m: nat.
675  ∀size_proof: m < 128.
676    sign_extension … (bitvector_of_nat 8 m) = bitvector_of_nat 16 m.
677  #m #size_proof whd in ⊢ (??%?);
678  >most_significant_bit_zero
679  [1:
680    elim m
681    [1:
682      %
683    |2:
684      #n' #inductive_hypothesis whd in match bitvector_of_nat; normalize nodelta
685      whd in match (bitvector_of_nat_aux ???);
686      whd in match (bitvector_of_nat_aux ???) in ⊢ (???%);
687      >(bitvector_of_nat_aux_buffer 16 n')
688      cases daemon
689    ]
690  |2:
691    assumption
692  ]
693qed.
694
695axiom add_commutative:
696  ∀n: nat.
697  ∀l, r: BitVector n.
698    add … l r = add … r l.
699
700axiom nat_of_bitvector_add:
701 ∀n,v1,v2.
702  nat_of_bitvector n v1 + nat_of_bitvector n v2 < 2^n →
703   nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2.
704
705axiom add_bitvector_of_nat:
706 ∀n,m1,m2.
707  bitvector_of_nat n (m1 + m2) =
708   add n (bitvector_of_nat n m1) (bitvector_of_nat n m2).
709
710example add_SO:
711  ∀n: nat.
712  ∀m: nat.
713    add n (bitvector_of_nat … m) (bitvector_of_nat … 1) = bitvector_of_nat … (S m).
714 cases daemon.
715qed.
716
717axiom add_bitvector_of_nat_plus:
718  ∀n,p,q:nat.
719    add n (bitvector_of_nat ? p) (bitvector_of_nat ? q) = bitvector_of_nat ? (p+q).
720   
721lemma add_bitvector_of_nat_Sm:
722  ∀n, m: nat.
723    add … (bitvector_of_nat … 1) (bitvector_of_nat … m) =
724      bitvector_of_nat n (S m).
725 #n #m @add_bitvector_of_nat_plus
726qed.
727
728axiom le_to_le_nat_of_bitvector_add:
729  ∀n,v,m1,m2.
730    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 ≤ m2 →
731      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) ≤
732      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
733
734lemma lt_to_lt_nat_of_bitvector_add:
735  ∀n,v,m1,m2.
736    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 →
737      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) <
738      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
739#n #v #m1 #m2 #m2_ok #bounded #H
740lapply (le_to_le_nat_of_bitvector_add n v (S m1) m2 ??) try assumption
741#K @(transitive_le … (K H))
742cases daemon (*CSC: TRUE, complete*)
743qed.
744
745definition sign_bit : ∀n. BitVector n → bool ≝
746λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
747
748definition sign_extend : ∀m,n. BitVector m → BitVector (n+m) ≝
749λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
750
751definition zero_ext : ∀m,n. BitVector m → BitVector n ≝
752λm,n.
753  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
754  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (pad … v)
755  | nat_eq n' ⇒ λv. v
756  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
757  ].
758
759definition sign_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 … (sign_extend … v)
763  | nat_eq n' ⇒ λv. v
764  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
765  ].
766
767example sub_minus_one_seven_eight:
768  ∀v: BitVector 7.
769  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
770  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
771 cases daemon.
772qed.
773
774axiom sub16_with_carry_overflow:
775  ∀left, right, result: BitVector 16.
776  ∀flags: BitVector 3.
777  ∀upper: BitVector 9.
778  ∀lower: BitVector 7.
779    sub_16_with_carry left right false = 〈result, flags〉 →
780      vsplit bool 9 7 result = 〈upper, lower〉 →
781        get_index_v bool 3 flags 2 ? = true →
782          upper = [[true; true; true; true; true; true; true; true; true]].
783  //
784qed.
785
786axiom sub_16_to_add_16_8_0:
787 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
788  get_index' ? 2 0 flags = false →
789  sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 →
790   v1 = add ? v2 (sign_extension (false:::v3)).
791
792axiom sub_16_to_add_16_8_1:
793 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
794  get_index' ? 2 0 flags = true →
795  sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 →
796   v1 = add ? v2 (sign_extension (true:::v3)).
Note: See TracBrowser for help on using the repository browser.