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

Last change on this file since 2132 was 2124, checked in by sacerdot, 8 years ago

Much more shuffling around to proper places

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