source: src/ASM/Arithmetic.ma @ 2700

Last change on this file since 2700 was 2700, checked in by sacerdot, 7 years ago
  1. exponential function dropped in favour of standard library
  2. fixpoint computation and graph colouring abstracted in the back-end, axiomatized in the compiler
  3. minor speedups in Policy.ma
File size: 37.4 KB
Line 
1include "ASM/BitVector.ma".
2include "ASM/Util.ma".
3include "arithmetics/exp.ma".
4
5definition addr16_of_addr11: Word → Word11 → Word ≝
6  λpc: Word.
7  λa: Word11.
8  let 〈pc_upper, ignore〉 ≝ vsplit … 8 8 pc in
9  let 〈n1, n2〉 ≝ vsplit … 4 4 pc_upper in
10  let 〈b123, b〉 ≝ vsplit … 3 8 a in
11  let b1 ≝ get_index_v … b123 0 ? in
12  let b2 ≝ get_index_v … b123 1 ? in
13  let b3 ≝ get_index_v … b123 2 ? in
14  let p5 ≝ get_index_v … n2 0 ? in
15    (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b.
16  //
17qed.
18
19definition nat_of_bool ≝
20  λb: bool.
21    match b with
22      [ false ⇒ O
23      | true ⇒ S O
24      ].
25
26definition carry_of : bool → bool → bool → bool ≝
27λa,b,c. match a with [ false ⇒ b ∧ c | true ⇒ b ∨ c ].
28
29definition add_with_carries : ∀n:nat. BitVector n → BitVector n → bool →
30                                      BitVector n × (BitVector n) ≝
31  λn,x,y,init_carry.
32  fold_right2_i ???
33   (λn,b,c,r.
34     let 〈lower_bits, carries〉 ≝ r in
35     let last_carry ≝ match carries with [ VEmpty ⇒ init_carry | VCons _ cy _ ⇒ cy ] in
36      (* Next if-then-else just to avoid a quadratic blow-up of the whd of an application
37         of add_with_carries *)
38     if last_carry then
39      let bit ≝ xorb (xorb b c) true in
40      let carry ≝ carry_of b c true in
41       〈bit:::lower_bits, carry:::carries〉
42     else
43      let bit ≝ xorb (xorb b c) false in
44      let carry ≝ carry_of b c false in
45       〈bit:::lower_bits, carry:::carries〉     
46   )
47   〈[[ ]], [[ ]]〉 n x y.
48
49(* Essentially the only difference for subtraction. *)
50definition borrow_of : bool → bool → bool → bool ≝
51λa,b,c. match a with [ false ⇒ b ∨ c | true ⇒ b ∧ c ].
52
53definition sub_with_borrows : ∀n:nat. BitVector n → BitVector n → bool →
54                                      BitVector n × (BitVector n) ≝
55  λn,x,y,init_borrow.
56  fold_right2_i ???
57   (λn,b,c,r.
58     let 〈lower_bits, borrows〉 ≝ r in
59     let last_borrow ≝ match borrows with [ VEmpty ⇒ init_borrow | VCons _ bw _ ⇒ bw ] in
60     let bit ≝ xorb (xorb b c) last_borrow in
61     let borrow ≝ borrow_of b c last_borrow in
62       〈bit:::lower_bits, borrow:::borrows〉
63   )
64   〈[[ ]], [[ ]]〉 n x y.
65   
66definition add_n_with_carry:
67      ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. n ≥ 5 →
68      (BitVector n) × (BitVector 3) ≝
69  λn: nat.
70  λb: BitVector n.
71  λc: BitVector n.
72  λcarry: bool.
73  λpf:n ≥ 5.
74 
75    let 〈result, carries〉 ≝ add_with_carries n b c carry in
76    let cy_flag ≝ get_index_v ?? carries 0 ? in
77    let ov_flag ≝ xorb cy_flag (get_index_v ?? carries 1 ?) in
78    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
79      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
80// @(transitive_le  … pf) /2/
81qed.
82
83definition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. n ≥ 5 →
84                                            (BitVector n) × (BitVector 3) ≝
85  λn: nat.
86  λb: BitVector n.
87  λc: BitVector n.
88  λcarry: bool.
89  λpf:n ≥ 5.
90 
91    let 〈result, carries〉 ≝ sub_with_borrows n b c carry in
92    let cy_flag ≝ get_index_v ?? carries 0 ? in
93    let ov_flag ≝ xorb cy_flag (get_index_v ?? carries 1 ?) in
94    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
95      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
96// @(transitive_le  … pf) /2/
97qed.
98
99definition add_8_with_carry ≝
100  λb, c: BitVector 8.
101  λcarry: bool.
102  add_n_with_carry 8 b c carry ?.
103  @le_S @le_S @le_S @le_n (* ugly: fix using tacticals *)
104qed.
105
106definition add_16_with_carry ≝
107  λb, c: BitVector 16.
108  λcarry: bool.
109  add_n_with_carry 16 b c carry ?.
110  @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S
111  @le_S @le_S @le_n (* ugly: fix using tacticals *)
112qed.
113
114(* dpm: needed for assembly proof *)
115definition sub_7_with_carry ≝
116  λb, c: BitVector 7.
117  λcarry: bool.
118  sub_n_with_carry 7 b c carry ?.
119  @le_S @le_S @le_n
120qed.
121
122definition sub_8_with_carry ≝
123  λb, c: BitVector 8.
124  λcarry: bool.
125  sub_n_with_carry 8 b c carry ?.
126  @le_S @le_S @le_S @le_n (* ugly: fix using tacticals *)
127qed.
128
129definition sub_16_with_carry ≝
130  λb, c: BitVector 16.
131  λcarry: bool.
132  sub_n_with_carry 16 b c carry ?.
133  @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S
134  @le_S @le_S @le_n (* ugly: fix using tacticals *)
135qed.
136
137definition increment ≝
138  λn: nat.
139  λb: BitVector n.
140    \fst (add_with_carries n b (zero n) true).
141       
142definition decrement ≝
143  λn: nat.
144  λb: BitVector n.
145    \fst (sub_with_borrows n b (zero n) true).
146
147let rec bitvector_of_nat_aux (n,m:nat) (v:BitVector n) on m : BitVector n ≝
148  match m with
149  [ O ⇒ v
150  | S m' ⇒ bitvector_of_nat_aux n m' (increment n v)
151  ].
152
153definition bitvector_of_nat : ∀n:nat. nat → BitVector n ≝
154  λn,m. bitvector_of_nat_aux n m (zero n).
155
156let rec nat_of_bitvector_aux (n,m:nat) (v:BitVector n) on v : nat ≝
157match v with
158[ VEmpty ⇒ m
159| VCons n' hd tl ⇒ nat_of_bitvector_aux n' (if hd then 2*m +1 else 2*m) tl
160].
161
162definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝
163  λn,v. nat_of_bitvector_aux n O v.
164
165(* TODO: remove when standard library arithmetics/exp.ma is used in place
166   of definition in ASM/Util.ma *)
167theorem lt_O_exp: ∀n,m:nat. O < n → O < n^m.
168#n #m (elim m) normalize // #a #Hind #posn
169@(le_times 1 ? 1) /2 by / qed.
170theorem le_exp: ∀n,m,p:nat. O < p →
171  n ≤m → p^n ≤ p^m.
172  @nat_elim2 #n #m
173  [#ltm #len @lt_O_exp //
174  |#_ #len @False_ind /2 by absurd/
175  |#Hind #p #posp #lenm normalize @le_times // @Hind /2 by monotonic_pred/
176  ]
177qed.
178
179lemma nat_of_bitvector_aux_lt_bound:
180 ∀n.∀v:BitVector n. ∀m,l:nat.
181  m < 2^l → nat_of_bitvector_aux n m v < 2^(n+l).
182 #n #v elim v normalize // -n
183 #n #hd #tl #IH #m #l #B cases hd normalize nodelta
184 @(transitive_le … (IH ? (S l) …))
185 [2,4: change with (?≤2^(S (n+l))) @le_exp /2 by le_n/
186 |1,3: @(transitive_le … (2 * (S m)))
187  [2,4: whd in ⊢ (??%); /2 by le_plus/
188  |3: // | 1: normalize <plus_n_O <plus_n_Sm // ]]
189qed. 
190
191lemma nat_of_bitvector_lt_bound:
192 ∀n: nat. ∀b: BitVector n. nat_of_bitvector n b < 2^n.
193 #n #b lapply (nat_of_bitvector_aux_lt_bound n b 0 0 ?) // <plus_n_O //
194qed.
195
196lemma bitvector_of_nat_ok:
197  ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y.
198 #n elim n -n
199 [ #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
200 | #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *)
201 ]
202qed.
203
204lemma bitvector_of_nat_abs:
205  ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y).
206 #n #x #y #Hx #Hy #Heq @notb_elim
207 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)))
208 cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %);
209 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H / by I/
210 | #H / by I/
211 ]
212qed.
213
214axiom bitvector_of_nat_exp_zero: ∀n.bitvector_of_nat n (2^n) = zero n.
215
216axiom nat_of_bitvector_bitvector_of_nat_inverse:
217  ∀n: nat.
218  ∀b: nat.
219    b < 2^n → nat_of_bitvector n (bitvector_of_nat n b) = b.
220
221axiom bitvector_of_nat_inverse_nat_of_bitvector:
222  ∀n: nat.
223  ∀b: BitVector n.
224    bitvector_of_nat n (nat_of_bitvector n b) = b.
225
226axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n.
227
228axiom eq_bitvector_of_nat_to_eq:
229 ∀n,n1,n2.
230  n1 < 2^n → n2 < 2^n →
231   bitvector_of_nat n n1 = bitvector_of_nat n n2 → n1=n2.
232
233lemma nat_of_bitvector_aux_injective:
234  ∀n: nat.
235  ∀l, r: BitVector n.
236  ∀acc_l, acc_r: nat.
237    nat_of_bitvector_aux n acc_l l = nat_of_bitvector_aux n acc_r r →
238      acc_l = acc_r ∧ l ≃ r.
239  #n #l
240  elim l #r
241  [1:
242    #acc_l #acc_r normalize
243    >(BitVector_O r) normalize /2/
244  |2:
245    #hd #tl #inductive_hypothesis #r #acc_l #acc_r
246    normalize normalize in inductive_hypothesis;
247    cases (BitVector_Sn … r)
248    #r_hd * #r_tl #r_refl destruct normalize
249    cases hd cases r_hd normalize
250    [1:
251      #relevant
252      cases (inductive_hypothesis … relevant)
253      #acc_assm #tl_assm destruct % //
254      lapply (injective_plus_l ? ? ? acc_assm)
255      -acc_assm #acc_assm
256      change with (2 * acc_l = 2 * acc_r) in acc_assm;
257      lapply (injective_times_r ? ? ? ? acc_assm) /2/
258    |4:
259      #relevant
260      cases (inductive_hypothesis … relevant)
261      #acc_assm #tl_assm destruct % //
262      change with (2 * acc_l = 2 * acc_r) in acc_assm;
263      lapply(injective_times_r ? ? ? ? acc_assm) /2/
264    |2:
265      #relevant 
266      change with ((nat_of_bitvector_aux r (2 * acc_l + 1) tl) =
267        (nat_of_bitvector_aux r (2 * acc_r) r_tl)) in relevant;
268      cases (eqb_decidable … (2 * acc_l + 1) (2 * acc_r))
269      [1:
270        #eqb_true_assm
271        lapply (eqb_true_to_refl … eqb_true_assm)
272        #refl_assm
273        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
274      |2:
275        #eqb_false_assm
276        lapply (eqb_false_to_not_refl … eqb_false_assm)
277        #not_refl_assm cases not_refl_assm #absurd_assm
278        cases (inductive_hypothesis … relevant) #absurd
279        cases (absurd_assm absurd)
280      ]
281    |3:
282      #relevant 
283      change with ((nat_of_bitvector_aux r (2 * acc_l) tl) =
284        (nat_of_bitvector_aux r (2 * acc_r + 1) r_tl)) in relevant;
285      cases (eqb_decidable … (2 * acc_l) (2 * acc_r + 1))
286      [1:
287        #eqb_true_assm
288        lapply (eqb_true_to_refl … eqb_true_assm)
289        #refl_assm
290        lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm)
291        -refl_assm #refl_assm
292        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
293      |2:
294        #eqb_false_assm
295        lapply (eqb_false_to_not_refl … eqb_false_assm)
296        #not_refl_assm cases not_refl_assm #absurd_assm
297        cases (inductive_hypothesis … relevant) #absurd
298        cases (absurd_assm absurd)
299      ]
300    ]
301  ]
302qed.
303
304lemma nat_of_bitvector_destruct:
305  ∀n: nat.
306  ∀l_hd, r_hd: bool.
307  ∀l_tl, r_tl: BitVector n.
308    nat_of_bitvector (S n) (l_hd:::l_tl) = nat_of_bitvector (S n) (r_hd:::r_tl) →
309      l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl.
310  #n #l_hd #r_hd #l_tl #r_tl
311  normalize
312  cases l_hd cases r_hd
313  normalize
314  [4:
315    /2/
316  |1:
317    #relevant
318    cases (nat_of_bitvector_aux_injective … relevant)
319    #_ #l_r_tl_refl destruct /2/
320  |2,3:
321    #relevant
322    cases (nat_of_bitvector_aux_injective … relevant)
323    #absurd destruct(absurd)
324  ]
325qed.
326
327lemma BitVector_cons_injective:
328  ∀n: nat.
329  ∀l_hd, r_hd: bool.
330  ∀l_tl, r_tl: BitVector n.
331    l_hd = r_hd → l_tl = r_tl → l_hd:::l_tl = r_hd:::r_tl.
332  #l #l_hd #r_hd #l_tl #r_tl
333  #l_refl #r_refl destruct %
334qed.
335
336lemma refl_nat_of_bitvector_to_refl:
337  ∀n: nat.
338  ∀l, r: BitVector n.
339    nat_of_bitvector n l = nat_of_bitvector n r → l = r.
340  #n
341  elim n
342  [1:
343    #l #r
344    >(BitVector_O l)
345    >(BitVector_O r)
346    #_ %
347  |2:
348    #n' #inductive_hypothesis #l #r
349    lapply (BitVector_Sn ? l) #l_hypothesis
350    lapply (BitVector_Sn ? r) #r_hypothesis
351    cases l_hypothesis #l_hd #l_tail_hypothesis
352    cases r_hypothesis #r_hd #r_tail_hypothesis
353    cases l_tail_hypothesis #l_tl #l_hd_tl_refl
354    cases r_tail_hypothesis #r_tl #r_hd_tl_refl
355    destruct #cons_refl
356    cases (nat_of_bitvector_destruct n' l_hd r_hd l_tl r_tl cons_refl)
357    #hd_refl #tl_refl
358    @BitVector_cons_injective try assumption
359    @inductive_hypothesis assumption
360  ]
361qed.
362
363definition two_complement_negation ≝
364  λn: nat.
365  λb: BitVector n.
366    let new_b ≝ negation_bv n b in
367      increment n new_b.
368   
369definition addition_n ≝
370  λn: nat.
371  λb, c: BitVector n.
372    let 〈res,flags〉 ≝ add_with_carries n b c false in
373      res.
374   
375definition subtraction ≝
376  λn: nat.
377  λb, c: BitVector n.
378    addition_n n b (two_complement_negation n c).
379
380let rec mult_aux (m,n:nat) (b:BitVector m) (c:BitVector (S n)) (acc:BitVector (S n)) on b : BitVector (S n) ≝
381match b with
382[ VEmpty ⇒ acc
383| VCons m' hd tl ⇒
384    let acc' ≝ if hd then addition_n ? c acc else acc in
385    mult_aux m' n tl (shift_right_1 ?? c false) acc'
386].
387
388definition multiplication : ∀n:nat. BitVector n → BitVector n → BitVector (n + n) ≝
389  λn: nat.
390  match n return λn.BitVector n → BitVector n → BitVector (n + n) with
391  [ O ⇒ λ_.λ_.[[ ]]
392  | S m ⇒
393    λb, c : BitVector (S m).
394    let c' ≝ pad (S m) (S m) c in
395      mult_aux ?? b (shift_left ?? m c' false) (zero ?)
396  ].
397
398definition short_multiplication : ∀n:nat. BitVector n → BitVector n → BitVector n ≝
399λn,x,y. (\snd (vsplit ??? (multiplication ? x y))).
400
401(* Division:  001...000 divided by 000...010
402     Shift the divisor as far left as possible,
403                                  100...000
404      then try subtracting it at each
405      bit position, shifting left as we go.
406              001...000 - 100...000 X ⇒ 0
407              001...000 - 010...000 X ⇒ 0
408              001...000 - 001...000 Y ⇒ 1 (use subtracted value as new quotient)
409              ...
410      Then pad out the remaining bits at the front
411         00..001...
412*)
413inductive fbs_diff : nat → Type[0] ≝
414| fbs_diff' : ∀n,m. fbs_diff (S (n+m)).
415
416let rec first_bit_set (n:nat) (b:BitVector n) on b : option (fbs_diff n) ≝
417match b return λn.λ_. option (fbs_diff n) with
418[ VEmpty ⇒ None ?
419| VCons m h t ⇒
420    if h then Some ? (fbs_diff' O m)
421    else match first_bit_set m t with
422         [ None ⇒ None ?
423         | Some o ⇒ match o return λx.λ_. option (fbs_diff (S x)) with [ fbs_diff' x y ⇒ Some ? (fbs_diff' (S x) y) ]
424         ]
425].
426
427let rec divmod_u_aux (n,m:nat) (q:BitVector (S n)) (d:BitVector (S n)) on m : BitVector m × (BitVector (S n)) ≝
428match m with
429[ O ⇒ 〈[[ ]], q〉
430| S m' ⇒
431    let 〈q',flags〉 ≝ add_with_carries ? q (two_complement_negation ? d) false in
432    let bit ≝ head' … flags in
433    let q'' ≝ if bit then q' else q in
434    let 〈tl, md〉 ≝ divmod_u_aux n m' q'' (shift_right_1 ?? d false) in
435    〈bit:::tl, md〉
436].
437
438definition divmod_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n) × (BitVector (S n))) ≝
439  λn: nat.
440  λb, c: BitVector (S n).
441
442    match first_bit_set ? c with
443    [ None ⇒ None ?
444    | Some fbs' ⇒
445        match fbs' return λx.λ_.option (BitVector x × (BitVector (S n))) with [ fbs_diff' fbs m ⇒
446          let 〈d,m〉 ≝ (divmod_u_aux ? (S fbs) b (shift_left ?? fbs c false)) in
447          Some ? 〈switch_bv_plus ??? (pad ?? d), m〉
448        ]
449    ].
450
451definition division_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
452λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\fst p) ].
453     
454definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
455  λn.
456    match n with
457    [ O ⇒ λb, c. None ?
458    | S p ⇒ λb, c: BitVector (S p).
459        let b_sign_bit ≝ get_index_v ? ? b O ? in
460        let c_sign_bit ≝ get_index_v ? ? c O ? in
461        match b_sign_bit with
462        [ true ⇒
463          let neg_b ≝ two_complement_negation ? b in
464          match c_sign_bit with
465          [ true ⇒
466              (* I was worrying slightly about -2^(n-1), whose negation can't
467                 be represented in an n bit signed number.  However, it's
468                 negation comes out as 2^(n-1) as an n bit *unsigned* number,
469                 so it's fine. *)
470              division_u ? neg_b (two_complement_negation ? c)
471          | false ⇒
472              match division_u ? neg_b c with
473              [ None ⇒ None ?
474              | Some r ⇒ Some ? (two_complement_negation ? r)
475              ]
476          ]
477        | false ⇒
478          match c_sign_bit with
479          [ true ⇒
480              match division_u ? b (two_complement_negation ? c) with
481              [ None ⇒ None ?
482              | Some r ⇒ Some ? (two_complement_negation ? r)
483              ]
484          | false ⇒ division_u ? b c
485          ]
486        ]
487   ].
488    //
489qed.
490
491definition modulus_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
492λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\snd p) ].
493           
494definition modulus_s ≝
495  λn.
496  λb, c: BitVector n.
497    match division_s n b c with
498      [ None ⇒ None ?
499      | Some result ⇒
500          let 〈high_bits, low_bits〉 ≝ vsplit bool ? n (multiplication n result c) in
501            Some ? (subtraction n b low_bits)
502      ].
503     
504definition lt_u ≝
505  fold_right2_i ???
506    (λ_.λa,b,r.
507      match a with
508      [ true ⇒ b ∧ r
509      | false ⇒ b ∨ r
510      ])
511    false.
512     
513definition gt_u ≝ λn, b, c. lt_u n c b.
514
515definition lte_u ≝ λn, b, c. ¬(gt_u n b c).
516
517definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
518
519definition lt_s ≝
520  λn.
521  λb, c: BitVector n.
522    let 〈result, borrows〉 ≝ sub_with_borrows n b c false in
523    match borrows with
524    [ VEmpty ⇒ false
525    | VCons _ bwn tl ⇒
526      match tl with
527      [ VEmpty ⇒ false
528      | VCons _ bwpn _ ⇒
529        if xorb bwn bwpn then
530          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
531        else
532          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
533      ]
534    ].
535   
536definition gt_s ≝ λn,b,c. lt_s n c b.
537
538definition lte_s ≝ λn,b,c. ¬(gt_s n b c).
539
540definition gte_s ≝ λn. λb, c. ¬(lt_s n b c).
541     
542alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
543
544(* Some properties of addition_n *)
545lemma commutative_add_with_carries : ∀n,a,b,carry. add_with_carries n a b carry = add_with_carries n b a carry.
546#n elim n
547[ 1: #a #b #carry
548     lapply (BitVector_O … a) lapply (BitVector_O … b) #H1 #H2 destruct @refl
549| 2: #n' #Hind #a #b #carry
550     lapply (BitVector_Sn … a) lapply (BitVector_Sn … b)
551     * #bhd * #btl #Heqb
552     * #ahd * #atl #Heqa destruct
553     lapply (Hind atl btl carry)
554     whd in match (add_with_carries ????) in ⊢ ((??%%) →  (??%%));
555     normalize in match (rewrite_l ??????);
556     normalize nodelta
557     #Heq >Heq
558     generalize in match (fold_right2_i ????????); * #res #carries
559     normalize nodelta
560     cases ahd cases bhd @refl
561] qed.
562
563lemma commutative_addition_n : ∀n,a,b. addition_n n a b = addition_n n b a.
564#n #a #b whd in match (addition_n ???) in ⊢ (??%%); >commutative_add_with_carries
565@refl
566qed.
567
568(* -------------------------------------------------------------------------- *)
569(* Associativity proof for addition_n. The proof relies on the observation
570 * that the two carries (inner and outer) in the associativity equation are not
571 * independent. In fact, the global carry can be encoded in a three-valued bits
572 * (versus 2 full bits, i.e. 4 possibilites, for two carries). I seriously hope
573 * this proof can be simplified, but now it's proved at least. *)
574
575inductive ternary : Type[0] ≝
576| Zero_carry : ternary
577| One_carry : ternary
578| Two_carry : ternary.
579
580definition carry_0 ≝ λcarry.
581    match carry with
582    [ Zero_carry ⇒ 〈false, Zero_carry〉
583    | One_carry ⇒ 〈true, Zero_carry〉
584    | Two_carry ⇒ 〈false, One_carry〉 ].
585   
586definition carry_1 ≝ λcarry.
587    match carry with
588    [ Zero_carry ⇒ 〈true, Zero_carry〉
589    | One_carry ⇒ 〈false, One_carry〉
590    | Two_carry ⇒ 〈true, One_carry〉 ].
591
592definition carry_2 ≝ λcarry.
593    match carry with
594    [ Zero_carry ⇒ 〈false, One_carry〉
595    | One_carry ⇒ 〈true, One_carry〉
596    | Two_carry ⇒ 〈false, Two_carry〉 ].
597
598definition carry_3 ≝ λcarry.
599    match carry with
600    [ Zero_carry ⇒ 〈true, One_carry〉
601    | One_carry ⇒ 〈false, Two_carry〉
602    | Two_carry ⇒ 〈true, Two_carry〉 ].
603
604(* Count the number of true bits in {xa,xb,xc} and compute the new bit along the new carry,
605   according to the last one. *)
606definition ternary_carry_of ≝ λxa,xb,xc,carry.
607if xa then
608  if xb then
609    if xc then
610      carry_3 carry
611    else
612      carry_2 carry
613  else
614    if xc then
615      carry_2 carry
616    else
617      carry_1 carry
618else
619  if xb then
620    if xc then
621      carry_2 carry
622    else
623      carry_1 carry
624  else
625    if xc then
626      carry_1 carry
627    else
628      carry_0 carry.
629
630let rec canonical_add (n : nat) (a,b,c : BitVector n) (init : ternary) on a : (BitVector n × ternary) ≝
631match a in Vector return λsz.λ_. BitVector sz → BitVector sz → (BitVector sz × ternary) with
632[ VEmpty ⇒ λ_,_. 〈VEmpty ?, init〉
633| VCons sz' xa tla ⇒ λb',c'.
634  let xb ≝ head' … b' in
635  let xc ≝ head' … c' in
636  let tlb ≝ tail … b' in
637  let tlc ≝ tail … c' in
638  let 〈bits, last〉 ≝ canonical_add ? tla tlb tlc init in
639  let 〈bit, carry〉 ≝ ternary_carry_of xa xb xc last in
640  〈bit ::: bits, carry〉
641] b c.
642
643(* convert the classical carries (inner and outer) to ternary) *)
644definition carries_to_ternary ≝ λcarry1,carry2.
645  if carry1
646  then if carry2
647       then Two_carry
648       else One_carry
649  else if carry2
650       then One_carry
651       else Zero_carry.
652
653(* Copied back from Clight/casts.ma *)
654lemma add_with_carries_unfold : ∀n,x,y,c.
655  add_with_carries n x y c = fold_right2_i ????? n x y.
656// qed.       
657   
658lemma add_with_carries_Sn : ∀n,a_hd,a_tl,b_hd,b_tl,carry.
659  add_with_carries (S n) (a_hd ::: a_tl) (b_hd ::: b_tl) carry =
660   (let 〈lower_bits,carries〉 ≝ add_with_carries n a_tl b_tl carry in 
661    let last_carry ≝
662    match carries in Vector return λsz:ℕ.(λfoo:Vector bool sz.bool) with 
663    [VEmpty⇒carry
664    |VCons (sz:ℕ) (cy:bool) (tl:(Vector bool sz))⇒cy] 
665    in 
666    if last_carry then 
667      let bit   ≝ xorb (xorb a_hd b_hd) true in 
668      let carry ≝ carry_of a_hd b_hd true in 
669      〈bit:::lower_bits,carry:::carries〉 
670    else 
671      let bit ≝ xorb (xorb a_hd b_hd) false in 
672      let carry ≝ carry_of a_hd b_hd false in 
673      〈bit:::lower_bits,carry:::carries〉).
674#n #a_hd #a_tl #b_hd #b_tl #carry
675whd in match (add_with_carries ????);
676normalize nodelta
677<add_with_carries_unfold
678cases (add_with_carries n a_tl b_tl carry)
679#lower_bits #carries normalize nodelta
680elim n in a_tl b_tl lower_bits carries;
681[ 1: #a_tl #b_tl #lower_bits #carries
682     >(BitVector_O … carries) normalize nodelta
683     cases carry normalize nodelta
684     cases a_hd cases b_hd //
685| 2: #n' #Hind #a_tl #b_tl #lower_bits #carries
686     lapply (BitVector_Sn … carries) * #carries_hd * #carries_tl
687     #Heq >Heq normalize nodelta
688     cases carries_hd cases a_hd cases b_hd normalize nodelta
689     //
690] qed.
691
692(* Correction of [canonical_add], left side. Note the invariant on carries. *)
693lemma canonical_add_left : ∀n,carry1,carry2,a,b,c.
694  let 〈res_ab,flags_ab〉 ≝ add_with_carries n a b carry1 in
695  let 〈res_ab_c,flags_ab_c〉 ≝ add_with_carries n res_ab c carry2 in
696  let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c (carries_to_ternary carry1 carry2) in
697  res_ab_c = res_canonical
698  ∧ (match n return λx. BitVector x → BitVector x → Prop with
699     [ O ⇒ λ_.λ_. True
700     | S _ ⇒ λflags_ab',flags_ab_c'. carries_to_ternary (head' … flags_ab') (head' … flags_ab_c') = last_carry
701     ] flags_ab flags_ab_c).
702#n elim n
703[ 1: #carry1 #carry2 #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try //
704| 2: #n' #Hind #carry1 #carry2 #a #b #c
705     elim (BitVector_Sn … a) #xa * #a' #Heq_a
706     elim (BitVector_Sn … b) #xb * #b' #Heq_b
707     elim (BitVector_Sn … c) #xc * #c' #Heq_c
708     lapply (Hind … carry1 carry2 a' b' c') -Hind
709     destruct >add_with_carries_Sn
710     elim (add_with_carries … a' b' carry1) #Hres_ab #Hflags_ab normalize nodelta
711     lapply Hflags_ab lapply Hres_ab lapply c' lapply b' lapply a'
712     -Hflags_ab -Hres_ab -c' -b' -a'
713     cases n'
714     [ 1: #a' #b' #c' #Hres_ab #Hflags_ab normalize nodelta
715          >(BitVector_O … a') >(BitVector_O … b') >(BitVector_O … c')
716          >(BitVector_O … Hres_ab) >(BitVector_O … Hflags_ab)
717          normalize nodelta #_
718          cases carry1 cases carry2 cases xa cases xb cases xc normalize @conj try //
719     | 2: #n' #a' #b' #c' #Hres_ab #Hflags_ab normalize nodelta
720          elim (BitVector_Sn … Hflags_ab) #hd_flags_ab * #tl_flags_ab #Heq_flags_ab >Heq_flags_ab
721          normalize nodelta
722          elim (BitVector_Sn … Hres_ab) #hd_res_ab * #tl_res_ab #Heq_res_ab >Heq_res_ab
723          cases hd_flags_ab in Heq_flags_ab; #Heq_flags_ab normalize nodelta
724          >add_with_carries_Sn
725          elim (add_with_carries (S n') (hd_res_ab:::tl_res_ab) c' carry2) #res_ab_c #flags_ab_c
726          normalize nodelta
727          elim (BitVector_Sn … flags_ab_c) #hd_flags_ab_c * #tl_flags_ab_c #Heq_flags_ab_c >Heq_flags_ab_c
728          normalize nodelta
729          cases hd_flags_ab_c in Heq_flags_ab_c; #Heq_flags_ab_c
730          normalize nodelta
731          whd in match (canonical_add (S (S ?)) ? ? ? ?);
732          whd in match (tail ???); whd in match (tail ???);
733          elim (canonical_add (S n') a' b' c' (carries_to_ternary carry1 carry2)) #res_canonical #last_carry normalize
734          * #Hres_ab_is_canonical #Hlast_carry <Hlast_carry normalize
735          >Hres_ab_is_canonical
736          cases xa cases xb cases xc try @conj try @refl
737     ]
738] qed.
739
740(* Symmetric. The two sides are most certainly doable in a single induction, but lazyness
741   prevails over style.  *)
742lemma canonical_add_right : ∀n,carry1,carry2,a,b,c.
743  let 〈res_bc,flags_bc〉 ≝ add_with_carries n b c carry1 in
744  let 〈res_a_bc,flags_a_bc〉 ≝ add_with_carries n a res_bc carry2 in
745  let 〈res_canonical, last_carry〉 ≝ canonical_add ? a b c (carries_to_ternary carry1 carry2) in
746  res_a_bc = res_canonical
747  ∧ (match n return λx. BitVector x → BitVector x → Prop with
748     [ O ⇒ λ_.λ_. True
749     | S _ ⇒ λflags_bc',flags_a_bc'. carries_to_ternary (head' … flags_bc') (head' … flags_a_bc') = last_carry
750     ] flags_bc flags_a_bc).
751#n elim n
752[ 1: #carry1 #carry2 #a #b #c >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c) try @conj try //
753| 2: #n' #Hind #carry1 #carry2 #a #b #c
754     elim (BitVector_Sn … a) #xa * #a' #Heq_a
755     elim (BitVector_Sn … b) #xb * #b' #Heq_b
756     elim (BitVector_Sn … c) #xc * #c' #Heq_c
757     lapply (Hind … carry1 carry2 a' b' c') -Hind
758     destruct >add_with_carries_Sn
759     elim (add_with_carries … b' c' carry1) #Hres_bc #Hflags_bc normalize nodelta
760     lapply Hflags_bc lapply Hres_bc lapply c' lapply b' lapply a'
761     -Hflags_bc -Hres_bc -c' -b' -a'
762     cases n'
763     [ 1: #a' #b' #c' #Hres_bc #Hflags_bc normalize nodelta
764          >(BitVector_O … a') >(BitVector_O … b') >(BitVector_O … c')
765          >(BitVector_O … Hres_bc) >(BitVector_O … Hflags_bc)
766          normalize nodelta #_
767          cases carry1 cases carry2 cases xa cases xb cases xc normalize @conj try //
768     | 2: #n' #a' #b' #c' #Hres_bc #Hflags_bc normalize nodelta
769          elim (BitVector_Sn … Hflags_bc) #hd_flags_bc * #tl_flags_bc #Heq_flags_bc >Heq_flags_bc
770          normalize nodelta
771          elim (BitVector_Sn … Hres_bc) #hd_res_bc * #tl_res_bc #Heq_res_bc >Heq_res_bc
772          cases hd_flags_bc in Heq_flags_bc; #Heq_flags_bc normalize nodelta
773          >add_with_carries_Sn
774          elim (add_with_carries (S n') a' (hd_res_bc:::tl_res_bc) carry2) #res_a_bc #flags_a_bc
775          normalize nodelta
776          elim (BitVector_Sn … flags_a_bc) #hd_flags_a_bc * #tl_flags_a_bc #Heq_flags_a_bc >Heq_flags_a_bc
777          normalize nodelta
778          cases (hd_flags_a_bc) in Heq_flags_a_bc; #Heq_flags_a_bc
779          whd in match (canonical_add (S (S ?)) ????);
780          whd in match (tail ???); whd in match (tail ???);
781          elim (canonical_add (S n') a' b' c' (carries_to_ternary carry1 carry2)) #res_canonical #last_carry normalize
782          * #Hres_bc_is_canonical #Hlast_carry <Hlast_carry normalize
783          >Hres_bc_is_canonical
784          cases xa cases xb cases xc try @conj try @refl
785     ]
786] qed.
787
788
789(* Note that we prove a result more general that just associativity: we can vary the carries. *)
790lemma associative_add_with_carries :
791  ∀n,carry1,carry2,a,b,c.
792  (\fst (add_with_carries n a (let 〈res,flags〉 ≝ add_with_carries n b c carry1 in res) carry2))
793   =
794  (\fst (add_with_carries n (let 〈res,flags〉 ≝ add_with_carries n a b carry1 in res) c carry2)).
795#n cases n
796[ 1: #carry1 #carry2 #a #b #c
797      >(BitVector_O … a) >(BitVector_O … b) >(BitVector_O … c)
798      normalize try @refl
799| 2: #n' #carry1 #carry2 #a #b #c
800     lapply (canonical_add_left … carry1 carry2 a b c)
801     lapply (canonical_add_right … carry1 carry2 a b c)
802     normalize nodelta
803     elim (add_with_carries (S n') b c carry1) #res_bc #flags_bc
804     elim (add_with_carries (S n') a b carry1) #res_ab #flags_ab
805     normalize nodelta
806     elim (add_with_carries (S n') a res_bc carry2) #res_a_bc #flags_a_bc
807     normalize nodelta     
808     elim (add_with_carries (S n') res_ab c carry2) #res_ab_c #flags_ab_c
809     normalize nodelta
810     cases (canonical_add ? a b c (carries_to_ternary carry1 carry2)) #canonical_bits #last_carry
811     normalize nodelta
812     * #HA #HB * #HC #HD destruct @refl
813] qed.
814
815(* This closes the proof of associativity for bitvector addition. *)     
816
817lemma associative_addition_n : ∀n,a,b,c. addition_n n a (addition_n n b c) = addition_n n (addition_n n a b) c.
818#n #a #b #c
819whd in match (addition_n ???) in ⊢ (??%%);
820whd in match (addition_n n b c);
821whd in match (addition_n n a b);
822lapply (associative_add_with_carries … false false a b c)
823elim (add_with_carries n b c false) #bc_bits #bc_flags
824elim (add_with_carries n a b false) #ab_bits #ab_flags
825normalize nodelta
826elim (add_with_carries n a bc_bits false) #a_bc_bits #a_bc_flags
827elim (add_with_carries n ab_bits c false) #ab_c_bits #ab_c_flags
828normalize
829#H @H
830qed.
831
832
833
834definition max_u ≝ λn,a,b. if lt_u n a b then b else a.
835definition min_u ≝ λn,a,b. if lt_u n a b then a else b.
836definition max_s ≝ λn,a,b. if lt_s n a b then b else a.
837definition min_s ≝ λn,a,b. if lt_s n a b then a else b.
838
839definition bitvector_of_bool:
840      ∀n: nat. ∀b: bool. BitVector (S n) ≝
841  λn: nat.
842  λb: bool.
843   (pad n 1 [[b]])⌈n + 1 ↦ S n⌉.
844  //
845qed.
846
847definition full_add ≝
848  λn: nat.
849  λb, c: BitVector n.
850  λd: Bit.
851    fold_right2_i ? ? ? (
852      λn.
853       λb1, b2: bool.
854        λd: Bit × (BitVector n).
855        let 〈c1,r〉 ≝ d in
856          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
857           (xorb (xorb b1 b2) c1) ::: r〉)
858     〈d, [[ ]]〉 ? b c.
859   
860definition half_add ≝
861  λn: nat.
862  λb, c: BitVector n.
863    full_add n b c false.
864
865definition add ≝
866  λn: nat.
867  λl, r: BitVector n.
868    \snd (half_add n l r).
869
870lemma half_add_carry_Sn:
871  ∀n: nat.
872  ∀l: BitVector n.
873  ∀hd: bool.
874    \fst (half_add (S n) (hd:::l) (false:::(zero n))) =
875      andb hd (\fst (half_add n l (zero n))).
876  #n #l elim l
877  [1:
878    #hd normalize cases hd %
879  |2:
880    #n' #hd #tl #inductive_hypothesis #hd'
881    whd in match half_add; normalize nodelta
882    whd in match full_add; normalize nodelta
883    normalize in ⊢ (??%%); cases hd' normalize
884    @pair_elim #c1 #r #c1_r_refl cases c1 %
885  ]
886qed.
887
888lemma half_add_zero_carry_false:
889  ∀m: nat.
890  ∀b: BitVector m.
891    \fst (half_add m b (zero m)) = false.
892  #m #b elim b try %
893  #n #hd #tl #inductive_hypothesis
894  change with (false:::(zero ?)) in match (zero ?);
895  >half_add_carry_Sn >inductive_hypothesis cases hd %
896qed.
897
898axiom half_add_true_true_carry_true:
899  ∀n: nat.
900  ∀hd, hd': bool.
901  ∀l, r: BitVector n.
902    \fst (half_add (S n) (true:::l) (true:::r)) = true.
903
904lemma add_Sn_carry_add:
905  ∀n: nat.
906  ∀hd, hd': bool.
907  ∀l, r: BitVector n.
908    add (S n) (hd:::l) (hd':::r) =
909      xorb (xorb hd hd') (\fst (half_add n l r)):::add n l r.
910  #n #hd #hd' #l elim l
911  [1:
912    #r cases hd cases hd'
913    >(BitVector_O … r) normalize %
914  |2:
915    #n' #hd'' #tl #inductive_hypothesis #r
916    cases (BitVector_Sn … r) #hd''' * #tl' #r_refl destruct
917    cases hd cases hd' cases hd'' cases hd'''
918    whd in match (xorb ??);
919    cases daemon
920  ]
921qed.
922 
923lemma add_zero:
924  ∀n: nat.
925  ∀l: BitVector n.
926    l = add n l (zero …).
927  #n #l elim l try %
928  #n' #hd #tl #inductive_hypothesis
929  change with (false:::zero ?) in match (zero ?);
930  >add_Sn_carry_add >half_add_zero_carry_false
931  cases hd <inductive_hypothesis %
932qed.
933
934axiom most_significant_bit_zero:
935  ∀size, m: nat.
936  ∀size_proof: 0 < size.
937    m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false.
938  normalize in size_proof; normalize @le_S_S assumption
939qed.
940   
941axiom zero_add_head:
942  ∀m: nat.
943  ∀tl, hd.
944    (hd:::add m (zero m) tl) = add (S m) (zero (S m)) (hd:::tl).
945
946lemma zero_add:
947  ∀m: nat.
948  ∀b: BitVector m.
949    add m (zero m) b = b.
950  #m #b elim b try %
951  #m' #hd #tl #inductive_hypothesis
952  <inductive_hypothesis in ⊢ (???%);
953  >zero_add_head %
954qed.
955
956axiom bitvector_of_nat_one_Sm:
957  ∀m: nat.
958    ∃b: BitVector m.
959      bitvector_of_nat (S m) 1 ≃ b @@ [[true]].
960
961axiom increment_zero_bitvector_of_nat_1:
962  ∀m: nat.
963  ∀b: BitVector m.
964    increment m b = add m (bitvector_of_nat m 1) b.
965
966axiom add_associative:
967  ∀m: nat.
968  ∀l, c, r: BitVector m.
969    add m l (add m c r) = add m (add m l c) r.
970
971lemma bitvector_of_nat_aux_buffer:
972  ∀m, n: nat.
973  ∀b: BitVector m.
974    bitvector_of_nat_aux m n b = add m (bitvector_of_nat m n) b.
975  #m #n elim n
976  [1:
977    #b change with (? = add ? (zero …) b)
978    >zero_add %
979  |2:
980    #n' #inductive_hypothesis #b
981    whd in match (bitvector_of_nat_aux ???);
982    >inductive_hypothesis whd in match (bitvector_of_nat ??) in ⊢ (???%);
983    >inductive_hypothesis >increment_zero_bitvector_of_nat_1
984    >increment_zero_bitvector_of_nat_1 <(add_zero m (bitvector_of_nat m 1))
985    <add_associative %
986  ]
987qed.
988
989definition sign_extension: Byte → Word ≝
990  λc.
991    let b ≝ get_index_v ? 8 c 1 ? in
992      [[ b; b; b; b; b; b; b; b ]] @@ c.
993  normalize
994  repeat (@le_S_S)
995  @le_O_n
996qed.
997
998lemma bitvector_of_nat_sign_extension_equivalence:
999  ∀m: nat.
1000  ∀size_proof: m < 128.
1001    sign_extension … (bitvector_of_nat 8 m) = bitvector_of_nat 16 m.
1002  #m #size_proof whd in ⊢ (??%?);
1003  >most_significant_bit_zero
1004  [1:
1005    elim m
1006    [1:
1007      %
1008    |2:
1009      #n' #inductive_hypothesis whd in match bitvector_of_nat; normalize nodelta
1010      whd in match (bitvector_of_nat_aux ???);
1011      whd in match (bitvector_of_nat_aux ???) in ⊢ (???%);
1012      >(bitvector_of_nat_aux_buffer 16 n')
1013      cases daemon
1014    ]
1015  |2:
1016    assumption
1017  ]
1018qed.
1019
1020axiom add_commutative:
1021  ∀n: nat.
1022  ∀l, r: BitVector n.
1023    add … l r = add … r l.
1024
1025axiom nat_of_bitvector_add:
1026 ∀n,v1,v2.
1027  nat_of_bitvector n v1 + nat_of_bitvector n v2 < 2^n →
1028   nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2.
1029
1030axiom add_bitvector_of_nat:
1031 ∀n,m1,m2.
1032  bitvector_of_nat n (m1 + m2) =
1033   add n (bitvector_of_nat n m1) (bitvector_of_nat n m2).
1034
1035(* CSC: corollary of add_bitvector_of_nat *)
1036axiom add_overflow:
1037 ∀n,m,r. m + r = 2^n →
1038  add n (bitvector_of_nat n m) (bitvector_of_nat n r) = zero n.
1039
1040example add_SO:
1041  ∀n: nat.
1042  ∀m: nat.
1043    add n (bitvector_of_nat … m) (bitvector_of_nat … 1) = bitvector_of_nat … (S m).
1044 cases daemon.
1045qed.
1046
1047axiom add_bitvector_of_nat_plus:
1048  ∀n,p,q:nat.
1049    add n (bitvector_of_nat ? p) (bitvector_of_nat ? q) = bitvector_of_nat ? (p+q).
1050   
1051lemma add_bitvector_of_nat_Sm:
1052  ∀n, m: nat.
1053    add … (bitvector_of_nat … 1) (bitvector_of_nat … m) =
1054      bitvector_of_nat n (S m).
1055 #n #m @add_bitvector_of_nat_plus
1056qed.
1057
1058axiom le_to_le_nat_of_bitvector_add:
1059  ∀n,v,m1,m2.
1060    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 ≤ m2 →
1061      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) ≤
1062      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
1063
1064lemma lt_to_lt_nat_of_bitvector_add:
1065  ∀n,v,m1,m2.
1066    m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 →
1067      nat_of_bitvector n (add n v (bitvector_of_nat n m1)) <
1068      nat_of_bitvector n (add n v (bitvector_of_nat n m2)).
1069#n #v #m1 #m2 #m2_ok #bounded #H
1070lapply (le_to_le_nat_of_bitvector_add n v (S m1) m2 ??) try assumption
1071#K @(transitive_le … (K H))
1072cases daemon (*CSC: TRUE, complete*)
1073qed.
1074
1075definition sign_bit : ∀n. BitVector n → bool ≝
1076λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
1077
1078definition sign_extend : ∀m,n. BitVector m → BitVector (n+m) ≝
1079λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
1080
1081definition zero_ext : ∀m,n. BitVector m → BitVector n ≝
1082λm,n.
1083  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
1084  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (pad … v)
1085  | nat_eq n' ⇒ λv. v
1086  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
1087  ].
1088
1089definition sign_ext : ∀m,n. BitVector m → BitVector n ≝
1090λm,n.
1091  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
1092  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (sign_extend … v)
1093  | nat_eq n' ⇒ λv. v
1094  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
1095  ].
1096
1097example sub_minus_one_seven_eight:
1098  ∀v: BitVector 7.
1099  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
1100  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
1101 cases daemon.
1102qed.
1103
1104axiom sub16_with_carry_overflow:
1105  ∀left, right, result: BitVector 16.
1106  ∀flags: BitVector 3.
1107  ∀upper: BitVector 9.
1108  ∀lower: BitVector 7.
1109    sub_16_with_carry left right false = 〈result, flags〉 →
1110      vsplit bool 9 7 result = 〈upper, lower〉 →
1111        get_index_v bool 3 flags 2 ? = true →
1112          upper = [[true; true; true; true; true; true; true; true; true]].
1113  //
1114qed.
1115
1116axiom sub_16_to_add_16_8_0:
1117 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
1118  get_index' ? 2 0 flags = false →
1119  sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 →
1120   v1 = add ? v2 (sign_extension (false:::v3)).
1121
1122axiom sub_16_to_add_16_8_1:
1123 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
1124  get_index' ? 2 0 flags = true →
1125  sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 →
1126   v1 = add ? v2 (sign_extension (true:::v3)).
Note: See TracBrowser for help on using the repository browser.