source: src/ASM/Arithmetic.ma @ 2672

Last change on this file since 2672 was 2672, checked in by sacerdot, 8 years ago

One less axiom on bitvectors.

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