source: src/ASM/Arithmetic.ma @ 2676

Last change on this file since 2676 was 2673, checked in by tranquil, 7 years ago

corrected some compilation errors (that might depend on some matita update)

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