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

Last change on this file since 2657 was 2311, checked in by garnier, 8 years ago

Some more cleaning of switchRemoval ...

File size: 36.3 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
512(* Some properties of addition_n *)
514#n elim n
515[ 1: #a #b #carry
516     lapply (BitVector_O … a) lapply (BitVector_O … b) #H1 #H2 destruct @refl
517| 2: #n' #Hind #a #b #carry
518     lapply (BitVector_Sn … a) lapply (BitVector_Sn … b)
519     * #bhd * #btl #Heqb
520     * #ahd * #atl #Heqa destruct
521     lapply (Hind atl btl carry)
522     whd in match (add_with_carries ????) in ⊢ ((??%%) →  (??%%));
523     normalize in match (rewrite_l ??????);
524     normalize nodelta
525     #Heq >Heq
526     generalize in match (fold_right2_i ????????); * #res #carries
527     normalize nodelta
528     cases ahd cases bhd @refl
529] qed.
530
532#n #a #b whd in match (addition_n ???) in ⊢ (??%%); >commutative_add_with_carries
533@refl
534qed.
535
536(* -------------------------------------------------------------------------- *)
537(* Associativity proof for addition_n. The proof relies on the observation
538 * that the two carries (inner and outer) in the associativity equation are not
539 * independent. In fact, the global carry can be encoded in a three-valued bits
540 * (versus 2 full bits, i.e. 4 possibilites, for two carries). I seriously hope
541 * this proof can be simplified, but now it's proved at least. *)
542
543inductive ternary : Type[0] ≝
544| Zero_carry : ternary
545| One_carry : ternary
546| Two_carry : ternary.
547
548definition carry_0 ≝ λcarry.
549    match carry with
550    [ Zero_carry ⇒ 〈false, Zero_carry〉
551    | One_carry ⇒ 〈true, Zero_carry〉
552    | Two_carry ⇒ 〈false, One_carry〉 ].
553
554definition carry_1 ≝ λcarry.
555    match carry with
556    [ Zero_carry ⇒ 〈true, Zero_carry〉
557    | One_carry ⇒ 〈false, One_carry〉
558    | Two_carry ⇒ 〈true, One_carry〉 ].
559
560definition carry_2 ≝ λcarry.
561    match carry with
562    [ Zero_carry ⇒ 〈false, One_carry〉
563    | One_carry ⇒ 〈true, One_carry〉
564    | Two_carry ⇒ 〈false, Two_carry〉 ].
565
566definition carry_3 ≝ λcarry.
567    match carry with
568    [ Zero_carry ⇒ 〈true, One_carry〉
569    | One_carry ⇒ 〈false, Two_carry〉
570    | Two_carry ⇒ 〈true, Two_carry〉 ].
571
572(* Count the number of true bits in {xa,xb,xc} and compute the new bit along the new carry,
573   according to the last one. *)
574definition ternary_carry_of ≝ λxa,xb,xc,carry.
575if xa then
576  if xb then
577    if xc then
578      carry_3 carry
579    else
580      carry_2 carry
581  else
582    if xc then
583      carry_2 carry
584    else
585      carry_1 carry
586else
587  if xb then
588    if xc then
589      carry_2 carry
590    else
591      carry_1 carry
592  else
593    if xc then
594      carry_1 carry
595    else
596      carry_0 carry.
597
598let rec canonical_add (n : nat) (a,b,c : BitVector n) (init : ternary) on a : (BitVector n × ternary) ≝
599match a in Vector return λsz.λ_. BitVector sz → BitVector sz → (BitVector sz × ternary) with
600[ VEmpty ⇒ λ_,_. 〈VEmpty ?, init〉
601| VCons sz' xa tla ⇒ λb',c'.
602  let xb ≝ head' … b' in
603  let xc ≝ head' … c' in
604  let tlb ≝ tail … b' in
605  let tlc ≝ tail … c' in
606  let 〈bits, last〉 ≝ canonical_add ? tla tlb tlc init in
607  let 〈bit, carry〉 ≝ ternary_carry_of xa xb xc last in
608  〈bit ::: bits, carry〉
609] b c.
610
611(* convert the classical carries (inner and outer) to ternary) *)
612definition carries_to_ternary ≝ λcarry1,carry2.
613  if carry1
614  then if carry2
615       then Two_carry
616       else One_carry
617  else if carry2
618       then One_carry
619       else Zero_carry.
620
621(* Copied back from Clight/casts.ma *)
623  add_with_carries n x y c = fold_right2_i ????? n x y.
624// qed.
625
627  add_with_carries (S n) (a_hd ::: a_tl) (b_hd ::: b_tl) carry =
628   (let 〈lower_bits,carries〉 ≝ add_with_carries n a_tl b_tl carry in
629    let last_carry ≝
630    match carries in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with
631    [VEmpty⇒carry
632    |VCons (sz:ℕ) (cy:bool) (tl:(Vector bool sz))⇒cy]
633    in
634    if last_carry then
635      let bit   ≝ xorb (xorb a_hd b_hd) true in
636      let carry ≝ carry_of a_hd b_hd true in
637      〈bit:::lower_bits,carry:::carries〉
638    else
639      let bit ≝ xorb (xorb a_hd b_hd) false in
640      let carry ≝ carry_of a_hd b_hd false in
641      〈bit:::lower_bits,carry:::carries〉).
642#n #a_hd #a_tl #b_hd #b_tl #carry
644normalize nodelta
646cases (add_with_carries n a_tl b_tl carry)
647#lower_bits #carries normalize nodelta
648elim n in a_tl b_tl lower_bits carries;
649[ 1: #a_tl #b_tl #lower_bits #carries
650     >(BitVector_O … carries) normalize nodelta
651     cases carry normalize nodelta
652     cases a_hd cases b_hd //
653| 2: #n' #Hind #a_tl #b_tl #lower_bits #carries
654     lapply (BitVector_Sn … carries) * #carries_hd * #carries_tl
655     #Heq >Heq normalize nodelta
656     cases carries_hd cases a_hd cases b_hd normalize nodelta
657     //
658] qed.
659
660(* Correction of [canonical_add], left side. Note the invariant on carries. *)
662  let 〈res_ab,flags_ab〉 ≝ add_with_carries n a b carry1 in
663  let 〈res_ab_c,flags_ab_c〉 ≝ add_with_carries n res_ab c carry2 in
664  let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c (carries_to_ternary carry1 carry2) in
665  res_ab_c = res_canonical
666  ∧ (match n return λx. BitVector x → BitVector x → Prop with
667     [ O ⇒ λ_.λ_. True
668     | S _ ⇒ λflags_ab',flags_ab_c'. carries_to_ternary (head' … flags_ab') (head' … flags_ab_c') = last_carry
669     ] flags_ab flags_ab_c).
670#n elim n
671[ 1: #carry1 #carry2 #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try //
672| 2: #n' #Hind #carry1 #carry2 #a #b #c
673     elim (BitVector_Sn … a) #xa * #a' #Heq_a
674     elim (BitVector_Sn … b) #xb * #b' #Heq_b
675     elim (BitVector_Sn … c) #xc * #c' #Heq_c
676     lapply (Hind … carry1 carry2 a' b' c') -Hind
678     elim (add_with_carries … a' b' carry1) #Hres_ab #Hflags_ab normalize nodelta
679     lapply Hflags_ab lapply Hres_ab lapply c' lapply b' lapply a'
680     -Hflags_ab -Hres_ab -c' -b' -a'
681     cases n'
682     [ 1: #a' #b' #c' #Hres_ab #Hflags_ab normalize nodelta
683          >(BitVector_O … a') >(BitVector_O … b') >(BitVector_O … c')
684          >(BitVector_O … Hres_ab) >(BitVector_O … Hflags_ab)
685          normalize nodelta #_
686          cases carry1 cases carry2 cases xa cases xb cases xc normalize @conj try //
687     | 2: #n' #a' #b' #c' #Hres_ab #Hflags_ab normalize nodelta
688          elim (BitVector_Sn … Hflags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab
689          normalize nodelta
690          elim (BitVector_Sn … Hres_ab) #hd_res_ab * #tl_res_ab #Heq_res_ab >Heq_res_ab
691          cases hd_flags_ab in Heq_flags_ab; #Heq_flags_ab normalize nodelta
693          elim (add_with_carries (S n') (hd_res_ab:::tl_res_ab) c' carry2) #res_ab_c #flags_ab_c
694          normalize nodelta
695          elim (BitVector_Sn … flags_ab_c) #hd_flags_ab_c * #tl_flags_ab_c #Heq_flags_ab_c >Heq_flags_ab_c
696          normalize nodelta
697          cases hd_flags_ab_c in Heq_flags_ab_c; #Heq_flags_ab_c
698          normalize nodelta
699          whd in match (canonical_add (S (S ?)) ? ? ? ?);
700          whd in match (tail ???); whd in match (tail ???);
701          elim (canonical_add (S n') a' b' c' (carries_to_ternary carry1 carry2)) #res_canonical #last_carry normalize
702          * #Hres_ab_is_canonical #Hlast_carry <Hlast_carry normalize
703          >Hres_ab_is_canonical
704          cases xa cases xb cases xc try @conj try @refl
705     ]
706] qed.
707
708(* Symmetric. The two sides are most certainly doable in a single induction, but lazyness
709   prevails over style.  *)
711  let 〈res_bc,flags_bc〉 ≝ add_with_carries n b c carry1 in
712  let 〈res_a_bc,flags_a_bc〉 ≝ add_with_carries n a res_bc carry2 in
713  let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c (carries_to_ternary carry1 carry2) in
714  res_a_bc = res_canonical
715  ∧ (match n return λx. BitVector x → BitVector x → Prop with
716     [ O ⇒ λ_.λ_. True
717     | S _ ⇒ λflags_bc',flags_a_bc'. carries_to_ternary (head' … flags_bc') (head' … flags_a_bc') = last_carry
718     ] flags_bc flags_a_bc).
719#n elim n
720[ 1: #carry1 #carry2 #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try //
721| 2: #n' #Hind #carry1 #carry2 #a #b #c
722     elim (BitVector_Sn … a) #xa * #a' #Heq_a
723     elim (BitVector_Sn … b) #xb * #b' #Heq_b
724     elim (BitVector_Sn … c) #xc * #c' #Heq_c
725     lapply (Hind … carry1 carry2 a' b' c') -Hind
727     elim (add_with_carries … b' c' carry1) #Hres_bc #Hflags_bc normalize nodelta
728     lapply Hflags_bc lapply Hres_bc lapply c' lapply b' lapply a'
729     -Hflags_bc -Hres_bc -c' -b' -a'
730     cases n'
731     [ 1: #a' #b' #c' #Hres_bc #Hflags_bc normalize nodelta
732          >(BitVector_O … a') >(BitVector_O … b') >(BitVector_O … c')
733          >(BitVector_O … Hres_bc) >(BitVector_O … Hflags_bc)
734          normalize nodelta #_
735          cases carry1 cases carry2 cases xa cases xb cases xc normalize @conj try //
736     | 2: #n' #a' #b' #c' #Hres_bc #Hflags_bc normalize nodelta
737          elim (BitVector_Sn … Hflags_bc) #hd_flags_bc * #tl_flags_bc #Heq_flags_bc >Heq_flags_bc
738          normalize nodelta
739          elim (BitVector_Sn … Hres_bc) #hd_res_bc * #tl_res_bc #Heq_res_bc >Heq_res_bc
740          cases hd_flags_bc in Heq_flags_bc; #Heq_flags_bc normalize nodelta
742          elim (add_with_carries (S n') a' (hd_res_bc:::tl_res_bc) carry2) #res_a_bc #flags_a_bc
743          normalize nodelta
744          elim (BitVector_Sn … flags_a_bc) #hd_flags_a_bc * #tl_flags_a_bc #Heq_flags_a_bc >Heq_flags_a_bc
745          normalize nodelta
746          cases (hd_flags_a_bc) in Heq_flags_a_bc; #Heq_flags_a_bc
747          whd in match (canonical_add (S (S ?)) ????);
748          whd in match (tail ???); whd in match (tail ???);
749          elim (canonical_add (S n') a' b' c' (carries_to_ternary carry1 carry2)) #res_canonical #last_carry normalize
750          * #Hres_bc_is_canonical #Hlast_carry <Hlast_carry normalize
751          >Hres_bc_is_canonical
752          cases xa cases xb cases xc try @conj try @refl
753     ]
754] qed.
755
756
757(* Note that we prove a result more general that just associativity: we can vary the carries. *)
759  ∀n,carry1,carry2,a,b,c.
760  (\fst (add_with_carries n a (let 〈res,flags〉 ≝ add_with_carries n b c carry1 in res) carry2))
761   =
762  (\fst (add_with_carries n (let 〈res,flags〉 ≝ add_with_carries n a b carry1 in res) c carry2)).
763#n cases n
764[ 1: #carry1 #carry2 #a #b #c
765      >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c)
766      normalize try @refl
767| 2: #n' #carry1 #carry2 #a #b #c
768     lapply (canonical_add_left … carry1 carry2 a b c)
769     lapply (canonical_add_right … carry1 carry2 a b c)
770     normalize nodelta
771     elim (add_with_carries (S n') b c carry1) #res_bc #flags_bc
772     elim (add_with_carries (S n') a b carry1) #res_ab #flags_ab
773     normalize nodelta
774     elim (add_with_carries (S n') a res_bc carry2) #res_a_bc #flags_a_bc
775     normalize nodelta
776     elim (add_with_carries (S n') res_ab c carry2) #res_ab_c #flags_ab_c
777     normalize nodelta
778     cases (canonical_add ? a b c (carries_to_ternary carry1 carry2)) #canonical_bits #last_carry
779     normalize nodelta
780     * #HA #HB * #HC #HD destruct @refl
781] qed.
782
783(* This closes the proof of associativity for bitvector addition. *)
784
786#n #a #b #c
787whd in match (addition_n ???) in ⊢ (??%%);
788whd in match (addition_n n b c);
789whd in match (addition_n n a b);
790lapply (associative_add_with_carries … false false a b c)
791elim (add_with_carries n b c false) #bc_bits #bc_flags
792elim (add_with_carries n a b false) #ab_bits #ab_flags
793normalize nodelta
794elim (add_with_carries n a bc_bits false) #a_bc_bits #a_bc_flags
795elim (add_with_carries n ab_bits c false) #ab_c_bits #ab_c_flags
796normalize
797#H @H
798qed.
799
800
801
802definition max_u ≝ λn,a,b. if lt_u n a b then b else a.
803definition min_u ≝ λn,a,b. if lt_u n a b then a else b.
804definition max_s ≝ λn,a,b. if lt_s n a b then b else a.
805definition min_s ≝ λn,a,b. if lt_s n a b then a else b.
806
807definition bitvector_of_bool:
808      ∀n: nat. ∀b: bool. BitVector (S n) ≝
809  λn: nat.
810  λb: bool.
811   (pad n 1 [[b]])⌈n + 1 ↦ S n⌉.
812  //
813qed.
814
816  λn: nat.
817  λb, c: BitVector n.
818  λd: Bit.
819    fold_right2_i ? ? ? (
820      λn.
821       λb1, b2: bool.
822        λd: Bit × (BitVector n).
823        let 〈c1,r〉 ≝ d in
824          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
825           (xorb (xorb b1 b2) c1) ::: r〉)
826     〈d, [[ ]]〉 ? b c.
827
829  λn: nat.
830  λb, c: BitVector n.
831    full_add n b c false.
832
834  λn: nat.
835  λl, r: BitVector n.
836    \snd (half_add n l r).
837
839  ∀n: nat.
840  ∀l: BitVector n.
841  ∀hd: bool.
842    \fst (half_add (S n) (hd:::l) (false:::(zero n))) =
843      andb hd (\fst (half_add n l (zero n))).
844  #n #l elim l
845  [1:
846    #hd normalize cases hd %
847  |2:
848    #n' #hd #tl #inductive_hypothesis #hd'
849    whd in match half_add; normalize nodelta
850    whd in match full_add; normalize nodelta
851    normalize in ⊢ (??%%); cases hd' normalize
852    @pair_elim #c1 #r #c1_r_refl cases c1 %
853  ]
854qed.
855
857  ∀m: nat.
858  ∀b: BitVector m.
859    \fst (half_add m b (zero m)) = false.
860  #m #b elim b try %
861  #n #hd #tl #inductive_hypothesis
862  change with (false:::(zero ?)) in match (zero ?);
863  >half_add_carry_Sn >inductive_hypothesis cases hd %
864qed.
865
867  ∀n: nat.
868  ∀hd, hd': bool.
869  ∀l, r: BitVector n.
870    \fst (half_add (S n) (true:::l) (true:::r)) = true.
871
873  ∀n: nat.
874  ∀hd, hd': bool.
875  ∀l, r: BitVector n.
876    add (S n) (hd:::l) (hd':::r) =
877      xorb (xorb hd hd') (\fst (half_add n l r)):::add n l r.
878  #n #hd #hd' #l elim l
879  [1:
880    #r cases hd cases hd'
881    >(BitVector_O … r) normalize %
882  |2:
883    #n' #hd'' #tl #inductive_hypothesis #r
884    cases (BitVector_Sn … r) #hd''' * #tl' #r_refl destruct
885    cases hd cases hd' cases hd'' cases hd'''
886    whd in match (xorb ??);
887    cases daemon
888  ]
889qed.
890
892  ∀n: nat.
893  ∀l: BitVector n.
894    l = add n l (zero …).
895  #n #l elim l try %
896  #n' #hd #tl #inductive_hypothesis
897  change with (false:::zero ?) in match (zero ?);
899  cases hd <inductive_hypothesis %
900qed.
901
902axiom most_significant_bit_zero:
903  ∀size, m: nat.
904  ∀size_proof: 0 < size.
905    m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false.
906  normalize in size_proof; normalize @le_S_S assumption
907qed.
908
910  ∀m: nat.
911  ∀tl, hd.
912    (hd:::add m (zero m) tl) = add (S m) (zero (S m)) (hd:::tl).
913
915  ∀m: nat.
916  ∀b: BitVector m.
917    add m (zero m) b = b.
918  #m #b elim b try %
919  #m' #hd #tl #inductive_hypothesis
920  <inductive_hypothesis in ⊢ (???%);
922qed.
923
924axiom bitvector_of_nat_one_Sm:
925  ∀m: nat.
926    ∃b: BitVector m.
927      bitvector_of_nat (S m) 1 ≃ b @@ [[true]].
928
929axiom increment_zero_bitvector_of_nat_1:
930  ∀m: nat.
931  ∀b: BitVector m.
932    increment m b = add m (bitvector_of_nat m 1) b.
933
935  ∀m: nat.
936  ∀l, c, r: BitVector m.
938
939lemma bitvector_of_nat_aux_buffer:
940  ∀m, n: nat.
941  ∀b: BitVector m.
942    bitvector_of_nat_aux m n b = add m (bitvector_of_nat m n) b.
943  #m #n elim n
944  [1:
945    #b change with (? = add ? (zero …) b)
947  |2:
948    #n' #inductive_hypothesis #b
949    whd in match (bitvector_of_nat_aux ???);
950    >inductive_hypothesis whd in match (bitvector_of_nat ??) in ⊢ (???%);
951    >inductive_hypothesis >increment_zero_bitvector_of_nat_1
952    >increment_zero_bitvector_of_nat_1 <(add_zero m (bitvector_of_nat m 1))
954  ]
955qed.
956
957definition sign_extension: Byte → Word ≝
958  λc.
959    let b ≝ get_index_v ? 8 c 1 ? in
960      [[ b; b; b; b; b; b; b; b ]] @@ c.
961  normalize
962  repeat (@le_S_S)
963  @le_O_n
964qed.
965
966lemma bitvector_of_nat_sign_extension_equivalence:
967  ∀m: nat.
968  ∀size_proof: m < 128.
969    sign_extension … (bitvector_of_nat 8 m) = bitvector_of_nat 16 m.
970  #m #size_proof whd in ⊢ (??%?);
971  >most_significant_bit_zero
972  [1:
973    elim m
974    [1:
975      %
976    |2:
977      #n' #inductive_hypothesis whd in match bitvector_of_nat; normalize nodelta
978      whd in match (bitvector_of_nat_aux ???);
979      whd in match (bitvector_of_nat_aux ???) in ⊢ (???%);
980      >(bitvector_of_nat_aux_buffer 16 n')
981      cases daemon
982    ]
983  |2:
984    assumption
985  ]
986qed.
987
989  ∀n: nat.
990  ∀l, r: BitVector n.
992
994 ∀n,v1,v2.
995  nat_of_bitvector n v1 + nat_of_bitvector n v2 < 2^n →
996   nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2.
997
999 ∀n,m1,m2.
1000  bitvector_of_nat n (m1 + m2) =
1001   add n (bitvector_of_nat n m1) (bitvector_of_nat n m2).
1002
1003(* CSC: corollary of add_bitvector_of_nat *)
1005 ∀n,m,r. m + r = 2^n →
1006  add n (bitvector_of_nat n m) (bitvector_of_nat n r) = zero n.
1007
1009  ∀n: nat.
1010  ∀m: nat.
1011    add n (bitvector_of_nat … m) (bitvector_of_nat … 1) = bitvector_of_nat … (S m).
1012 cases daemon.
1013qed.
1014
1016  ∀n,p,q:nat.
1017    add n (bitvector_of_nat ? p) (bitvector_of_nat ? q) = bitvector_of_nat ? (p+q).
1018
1020  ∀n, m: nat.
1021    add … (bitvector_of_nat … 1) (bitvector_of_nat … m) =
1022      bitvector_of_nat n (S m).
1024qed.
1025
1027  ∀n,v,m1,m2.
1028    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 ≤ m2 →
1029      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) ≤
1030      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
1031
1033  ∀n,v,m1,m2.
1034    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 →
1035      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) <
1036      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
1037#n #v #m1 #m2 #m2_ok #bounded #H
1038lapply (le_to_le_nat_of_bitvector_add n v (S m1) m2 ??) try assumption
1039#K @(transitive_le … (K H))
1040cases daemon (*CSC: TRUE, complete*)
1041qed.
1042
1043definition sign_bit : ∀n. BitVector n → bool ≝
1044λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
1045
1046definition sign_extend : ∀m,n. BitVector m → BitVector (n+m) ≝
1047λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
1048
1049definition zero_ext : ∀m,n. BitVector m → BitVector n ≝
1050λm,n.
1051  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
1052  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (pad … v)
1053  | nat_eq n' ⇒ λv. v
1054  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
1055  ].
1056
1057definition sign_ext : ∀m,n. BitVector m → BitVector n ≝
1058λm,n.
1059  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
1060  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (sign_extend … v)
1061  | nat_eq n' ⇒ λv. v
1062  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
1063  ].
1064
1065example sub_minus_one_seven_eight:
1066  ∀v: BitVector 7.
1067  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
1068  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
1069 cases daemon.
1070qed.
1071
1072axiom sub16_with_carry_overflow:
1073  ∀left, right, result: BitVector 16.
1074  ∀flags: BitVector 3.
1075  ∀upper: BitVector 9.
1076  ∀lower: BitVector 7.
1077    sub_16_with_carry left right false = 〈result, flags〉 →
1078      vsplit bool 9 7 result = 〈upper, lower〉 →
1079        get_index_v bool 3 flags 2 ? = true →
1080          upper = [[true; true; true; true; true; true; true; true; true]].
1081  //
1082qed.
1083