source: src/ASM/Arithmetic.ma @ 2993

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