source: src/ASM/Arithmetic.ma @ 2782

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