# source:src/ASM/Arithmetic.ma@2177

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

Tidy up multiplication.

File size: 24.1 KB
Line
1include "ASM/BitVector.ma".
2include "ASM/Util.ma".
3
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
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 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
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
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
539  λn: nat.
540  λb, c: BitVector n.
541    full_add n b c false.
542
544  λn: nat.
545  λl, r: BitVector n.
546    \snd (half_add n l r).
547
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
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
577  ∀n: nat.
578  ∀hd, hd': bool.
579  ∀l, r: BitVector n.
580    \fst (half_add (S n) (true:::l) (true:::r)) = true.
581
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
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 ?);
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
620  ∀m: nat.
621  ∀tl, hd.
622    (hd:::add m (zero m) tl) = add (S m) (zero (S m)) (hd:::tl).
623
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 ⊢ (???%);
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
645  ∀m: nat.
646  ∀l, c, r: BitVector m.
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)
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))
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
699  ∀n: nat.
700  ∀l, r: BitVector n.
702
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
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
714  ∀n: nat.
715  ∀m: nat.
716    add n (bitvector_of_nat … m) (bitvector_of_nat … 1) = bitvector_of_nat … (S m).
717 cases daemon.
718qed.
719
721  ∀n,p,q:nat.
722    add n (bitvector_of_nat ? p) (bitvector_of_nat ? q) = bitvector_of_nat ? (p+q).
723
725  ∀n, m: nat.
726    add … (bitvector_of_nat … 1) (bitvector_of_nat … m) =
727      bitvector_of_nat n (S m).
729qed.
730
732  ∀n,v,m1,m2.
733    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 ≤ m2 →
734      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) ≤
735      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
736
738  ∀n,v,m1,m2.
739    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 →
740      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) <
741      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
742#n #v #m1 #m2 #m2_ok #bounded #H
743lapply (le_to_le_nat_of_bitvector_add n v (S m1) m2 ??) try assumption
744#K @(transitive_le … (K H))
745cases daemon (*CSC: TRUE, complete*)
746qed.
747
748definition sign_bit : ∀n. BitVector n → bool ≝
749λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
750
751definition sign_extend : ∀m,n. BitVector m → BitVector (n+m) ≝
752λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
753
754definition zero_ext : ∀m,n. BitVector m → BitVector n ≝
755λm,n.
756  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
757  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (pad … v)
758  | nat_eq n' ⇒ λv. v
759  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
760  ].
761
762definition sign_ext : ∀m,n. BitVector m → BitVector n ≝
763λm,n.
764  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
765  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (sign_extend … v)
766  | nat_eq n' ⇒ λv. v
767  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
768  ].
769
770example sub_minus_one_seven_eight:
771  ∀v: BitVector 7.
772  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
773  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
774 cases daemon.
775qed.
776
777axiom sub16_with_carry_overflow:
778  ∀left, right, result: BitVector 16.
779  ∀flags: BitVector 3.
780  ∀upper: BitVector 9.
781  ∀lower: BitVector 7.
782    sub_16_with_carry left right false = 〈result, flags〉 →
783      vsplit bool 9 7 result = 〈upper, lower〉 →
784        get_index_v bool 3 flags 2 ? = true →
785          upper = [[true; true; true; true; true; true; true; true; true]].
786  //
787qed.
788