# source:src/ASM/Arithmetic.ma@2113

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

Cleanup: lemmas/theorems/axioms moved to the right places.

File size: 21.7 KB
Line
1include "ASM/BitVector.ma".
2include "ASM/Util.ma".
3
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
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
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
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
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 bitvector_of_nat_ok:
165  ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y.
166 #n elim n -n
167 [ #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
168 | #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *)
169 ]
170qed.
171
172lemma bitvector_of_nat_abs:
173  ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y).
174 #n #x #y #Hx #Hy #Heq @notb_elim
175 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)))
176 cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %);
177 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H / by I/
178 | #H / by I/
179 ]
180qed.
181
182axiom nat_of_bitvector_bitvector_of_nat_inverse:
183  ∀n: nat.
184  ∀b: nat.
185    b < 2^n → nat_of_bitvector n (bitvector_of_nat n b) = b.
186
187axiom bitvector_of_nat_inverse_nat_of_bitvector:
188  ∀n: nat.
189  ∀b: BitVector n.
190    bitvector_of_nat n (nat_of_bitvector n b) = b.
191
192axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n.
193
194lemma nat_of_bitvector_aux_injective:
195  ∀n: nat.
196  ∀l, r: BitVector n.
197  ∀acc_l, acc_r: nat.
198    nat_of_bitvector_aux n acc_l l = nat_of_bitvector_aux n acc_r r →
199      acc_l = acc_r ∧ l ≃ r.
200  #n #l
201  elim l #r
202  [1:
203    #acc_l #acc_r normalize
204    >(BitVector_O r) normalize /2/
205  |2:
206    #hd #tl #inductive_hypothesis #r #acc_l #acc_r
207    normalize normalize in inductive_hypothesis;
208    cases (BitVector_Sn … r)
209    #r_hd * #r_tl #r_refl destruct normalize
210    cases hd cases r_hd normalize
211    [1:
212      #relevant
213      cases (inductive_hypothesis … relevant)
214      #acc_assm #tl_assm destruct % //
215      lapply (injective_plus_l ? ? ? acc_assm)
216      -acc_assm #acc_assm
217      change with (2 * acc_l = 2 * acc_r) in acc_assm;
218      lapply (injective_times_r ? ? ? ? acc_assm) /2/
219    |4:
220      #relevant
221      cases (inductive_hypothesis … relevant)
222      #acc_assm #tl_assm destruct % //
223      change with (2 * acc_l = 2 * acc_r) in acc_assm;
224      lapply(injective_times_r ? ? ? ? acc_assm) /2/
225    |2:
226      #relevant
227      change with ((nat_of_bitvector_aux r (2 * acc_l + 1) tl) =
228        (nat_of_bitvector_aux r (2 * acc_r) r_tl)) in relevant;
229      cases (eqb_decidable … (2 * acc_l + 1) (2 * acc_r))
230      [1:
231        #eqb_true_assm
232        lapply (eqb_true_to_refl … eqb_true_assm)
233        #refl_assm
234        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
235      |2:
236        #eqb_false_assm
237        lapply (eqb_false_to_not_refl … eqb_false_assm)
238        #not_refl_assm cases not_refl_assm #absurd_assm
239        cases (inductive_hypothesis … relevant) #absurd
240        cases (absurd_assm absurd)
241      ]
242    |3:
243      #relevant
244      change with ((nat_of_bitvector_aux r (2 * acc_l) tl) =
245        (nat_of_bitvector_aux r (2 * acc_r + 1) r_tl)) in relevant;
246      cases (eqb_decidable … (2 * acc_l) (2 * acc_r + 1))
247      [1:
248        #eqb_true_assm
249        lapply (eqb_true_to_refl … eqb_true_assm)
250        #refl_assm
251        lapply (sym_eq ? (2 * acc_l) (2 * acc_r + 1) refl_assm)
252        -refl_assm #refl_assm
253        cases (two_times_n_plus_one_refl_two_times_n_to_False … refl_assm)
254      |2:
255        #eqb_false_assm
256        lapply (eqb_false_to_not_refl … eqb_false_assm)
257        #not_refl_assm cases not_refl_assm #absurd_assm
258        cases (inductive_hypothesis … relevant) #absurd
259        cases (absurd_assm absurd)
260      ]
261    ]
262  ]
263qed.
264
265lemma nat_of_bitvector_destruct:
266  ∀n: nat.
267  ∀l_hd, r_hd: bool.
268  ∀l_tl, r_tl: BitVector n.
269    nat_of_bitvector (S n) (l_hd:::l_tl) = nat_of_bitvector (S n) (r_hd:::r_tl) →
270      l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl.
271  #n #l_hd #r_hd #l_tl #r_tl
272  normalize
273  cases l_hd cases r_hd
274  normalize
275  [4:
276    /2/
277  |1:
278    #relevant
279    cases (nat_of_bitvector_aux_injective … relevant)
280    #_ #l_r_tl_refl destruct /2/
281  |2,3:
282    #relevant
283    cases (nat_of_bitvector_aux_injective … relevant)
284    #absurd destruct(absurd)
285  ]
286qed.
287
288lemma BitVector_cons_injective:
289  ∀n: nat.
290  ∀l_hd, r_hd: bool.
291  ∀l_tl, r_tl: BitVector n.
292    l_hd = r_hd → l_tl = r_tl → l_hd:::l_tl = r_hd:::r_tl.
293  #l #l_hd #r_hd #l_tl #r_tl
294  #l_refl #r_refl destruct %
295qed.
296
297lemma refl_nat_of_bitvector_to_refl:
298  ∀n: nat.
299  ∀l, r: BitVector n.
300    nat_of_bitvector n l = nat_of_bitvector n r → l = r.
301  #n
302  elim n
303  [1:
304    #l #r
305    >(BitVector_O l)
306    >(BitVector_O r)
307    #_ %
308  |2:
309    #n' #inductive_hypothesis #l #r
310    lapply (BitVector_Sn ? l) #l_hypothesis
311    lapply (BitVector_Sn ? r) #r_hypothesis
312    cases l_hypothesis #l_hd #l_tail_hypothesis
313    cases r_hypothesis #r_hd #r_tail_hypothesis
314    cases l_tail_hypothesis #l_tl #l_hd_tl_refl
315    cases r_tail_hypothesis #r_tl #r_hd_tl_refl
316    destruct #cons_refl
317    cases (nat_of_bitvector_destruct n' l_hd r_hd l_tl r_tl cons_refl)
318    #hd_refl #tl_refl
319    @BitVector_cons_injective try assumption
320    @inductive_hypothesis assumption
321  ]
322qed.
323
324definition two_complement_negation ≝
325  λn: nat.
326  λb: BitVector n.
327    let new_b ≝ negation_bv n b in
328      increment n new_b.
329
331  λn: nat.
332  λb, c: BitVector n.
333    let 〈res,flags〉 ≝ add_with_carries n b c false in
334      res.
335
336definition subtraction ≝
337  λn: nat.
338  λb, c: BitVector n.
339    addition_n n b (two_complement_negation n c).
340
341let rec mult_aux (m,n:nat) (b:BitVector m) (c:BitVector (S n)) (acc:BitVector (S n)) on b : BitVector (S n) ≝
342match b with
343[ VEmpty ⇒ acc
344| VCons m' hd tl ⇒
345    let acc' ≝ if hd then addition_n ? c acc else acc in
346    mult_aux m' n tl (shift_right_1 ?? c false) acc'
347].
348
349definition multiplication : ∀n:nat. BitVector n → BitVector n → BitVector (n + n) ≝
350  λn: nat.
351  match n return λn.BitVector n → BitVector n → BitVector (n + n) with
352  [ O ⇒ λ_.λ_.[[ ]]
353  | S m ⇒
354    λb, c : BitVector (S m).
355    let c' ≝ pad (S m) (S m) c in
356      mult_aux ?? b (shift_left ?? m c' false) (zero ?)
357  ].
358
359(* Division:  001...000 divided by 000...010
360     Shift the divisor as far left as possible,
361                                  100...000
362      then try subtracting it at each
363      bit position, shifting left as we go.
364              001...000 - 100...000 X ⇒ 0
365              001...000 - 010...000 X ⇒ 0
366              001...000 - 001...000 Y ⇒ 1 (use subtracted value as new quotient)
367              ...
368      Then pad out the remaining bits at the front
369         00..001...
370*)
371inductive fbs_diff : nat → Type[0] ≝
372| fbs_diff' : ∀n,m. fbs_diff (S (n+m)).
373
374let rec first_bit_set (n:nat) (b:BitVector n) on b : option (fbs_diff n) ≝
375match b return λn.λ_. option (fbs_diff n) with
376[ VEmpty ⇒ None ?
377| VCons m h t ⇒
378    if h then Some ? (fbs_diff' O m)
379    else match first_bit_set m t with
380         [ None ⇒ None ?
381         | Some o ⇒ match o return λx.λ_. option (fbs_diff (S x)) with [ fbs_diff' x y ⇒ Some ? (fbs_diff' (S x) y) ]
382         ]
383].
384
385let rec divmod_u_aux (n,m:nat) (q:BitVector (S n)) (d:BitVector (S n)) on m : BitVector m × (BitVector (S n)) ≝
386match m with
387[ O ⇒ 〈[[ ]], q〉
388| S m' ⇒
389    let 〈q',flags〉 ≝ add_with_carries ? q (two_complement_negation ? d) false in
390    let bit ≝ head' … flags in
391    let q'' ≝ if bit then q' else q in
392    let 〈tl, md〉 ≝ divmod_u_aux n m' q'' (shift_right_1 ?? d false) in
393    〈bit:::tl, md〉
394].
395
396definition divmod_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n) × (BitVector (S n))) ≝
397  λn: nat.
398  λb, c: BitVector (S n).
399
400    match first_bit_set ? c with
401    [ None ⇒ None ?
402    | Some fbs' ⇒
403        match fbs' return λx.λ_.option (BitVector x × (BitVector (S n))) with [ fbs_diff' fbs m ⇒
404          let 〈d,m〉 ≝ (divmod_u_aux ? (S fbs) b (shift_left ?? fbs c false)) in
405          Some ? 〈switch_bv_plus ??? (pad ?? d), m〉
406        ]
407    ].
408
409definition division_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
410λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\fst p) ].
411
412definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
413  λn.
414    match n with
415    [ O ⇒ λb, c. None ?
416    | S p ⇒ λb, c: BitVector (S p).
417        let b_sign_bit ≝ get_index_v ? ? b O ? in
418        let c_sign_bit ≝ get_index_v ? ? c O ? in
419        match b_sign_bit with
420        [ true ⇒
421          let neg_b ≝ two_complement_negation ? b in
422          match c_sign_bit with
423          [ true ⇒
424              (* I was worrying slightly about -2^(n-1), whose negation can't
425                 be represented in an n bit signed number.  However, it's
426                 negation comes out as 2^(n-1) as an n bit *unsigned* number,
427                 so it's fine. *)
428              division_u ? neg_b (two_complement_negation ? c)
429          | false ⇒
430              match division_u ? neg_b c with
431              [ None ⇒ None ?
432              | Some r ⇒ Some ? (two_complement_negation ? r)
433              ]
434          ]
435        | false ⇒
436          match c_sign_bit with
437          [ true ⇒
438              match division_u ? b (two_complement_negation ? c) with
439              [ None ⇒ None ?
440              | Some r ⇒ Some ? (two_complement_negation ? r)
441              ]
442          | false ⇒ division_u ? b c
443          ]
444        ]
445   ].
446    //
447qed.
448
449definition modulus_u : ∀n:nat. BitVector (S n) → BitVector (S n) → option (BitVector (S n)) ≝
450λn,q,d. match divmod_u n q d with [ None ⇒ None ? | Some p ⇒ Some ? (\snd p) ].
451
452definition modulus_s ≝
453  λn.
454  λb, c: BitVector n.
455    match division_s n b c with
456      [ None ⇒ None ?
457      | Some result ⇒
458          let 〈high_bits, low_bits〉 ≝ vsplit bool ? n (multiplication n result c) in
459            Some ? (subtraction n b low_bits)
460      ].
461
462definition lt_u ≝
463  fold_right2_i ???
464    (λ_.λa,b,r.
465      match a with
466      [ true ⇒ b ∧ r
467      | false ⇒ b ∨ r
468      ])
469    false.
470
471definition gt_u ≝ λn, b, c. lt_u n c b.
472
473definition lte_u ≝ λn, b, c. ¬(gt_u n b c).
474
475definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
476
477definition lt_s ≝
478  λn.
479  λb, c: BitVector n.
480    let 〈result, borrows〉 ≝ sub_with_borrows n b c false in
481    match borrows with
482    [ VEmpty ⇒ false
483    | VCons _ bwn tl ⇒
484      match tl with
485      [ VEmpty ⇒ false
486      | VCons _ bwpn _ ⇒
487        if xorb bwn bwpn then
488          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
489        else
490          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
491      ]
492    ].
493
494definition gt_s ≝ λn,b,c. lt_s n c b.
495
496definition lte_s ≝ λn,b,c. ¬(gt_s n b c).
497
498definition gte_s ≝ λn. λb, c. ¬(lt_s n b c).
499
500alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
501
502definition max_u ≝ λn,a,b. if lt_u n a b then b else a.
503definition min_u ≝ λn,a,b. if lt_u n a b then a else b.
504definition max_s ≝ λn,a,b. if lt_s n a b then b else a.
505definition min_s ≝ λn,a,b. if lt_s n a b then a else b.
506
507definition bitvector_of_bool:
508      ∀n: nat. ∀b: bool. BitVector (S n) ≝
509  λn: nat.
510  λb: bool.
511   (pad n 1 [[b]])⌈n + 1 ↦ S n⌉.
512  //
513qed.
514
516  λn: nat.
517  λb, c: BitVector n.
518  λd: Bit.
519    fold_right2_i ? ? ? (
520      λn.
521       λb1, b2: bool.
522        λd: Bit × (BitVector n).
523        let 〈c1,r〉 ≝ d in
524          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
525           (xorb (xorb b1 b2) c1) ::: r〉)
526     〈d, [[ ]]〉 ? b c.
527
529  λn: nat.
530  λb, c: BitVector n.
531    full_add n b c false.
532
534  λn: nat.
535  λl, r: BitVector n.
536    \snd (half_add n l r).
537
539  ∀n: nat.
540  ∀l: BitVector n.
541  ∀hd: bool.
542    \fst (half_add (S n) (hd:::l) (false:::(zero n))) =
543      andb hd (\fst (half_add n l (zero n))).
544  #n #l elim l
545  [1:
546    #hd normalize cases hd %
547  |2:
548    #n' #hd #tl #inductive_hypothesis #hd'
549    whd in match half_add; normalize nodelta
550    whd in match full_add; normalize nodelta
551    normalize in ⊢ (??%%); cases hd' normalize
552    @pair_elim #c1 #r #c1_r_refl cases c1 %
553  ]
554qed.
555
557  ∀m: nat.
558  ∀b: BitVector m.
559    \fst (half_add m b (zero m)) = false.
560  #m #b elim b try %
561  #n #hd #tl #inductive_hypothesis
562  change with (false:::(zero ?)) in match (zero ?);
563  >half_add_carry_Sn >inductive_hypothesis cases hd %
564qed.
565
567  ∀n: nat.
568  ∀hd, hd': bool.
569  ∀l, r: BitVector n.
570    \fst (half_add (S n) (true:::l) (true:::r)) = true.
571
573  ∀n: nat.
574  ∀hd, hd': bool.
575  ∀l, r: BitVector n.
576    add (S n) (hd:::l) (hd':::r) =
577      xorb (xorb hd hd') (\fst (half_add n l r)):::add n l r.
578  #n #hd #hd' #l elim l
579  [1:
580    #r cases hd cases hd'
581    >(BitVector_O … r) normalize %
582  |2:
583    #n' #hd'' #tl #inductive_hypothesis #r
584    cases (BitVector_Sn … r) #hd''' * #tl' #r_refl destruct
585    cases hd cases hd' cases hd'' cases hd'''
586    whd in match (xorb ??);
587    cases daemon
588  ]
589qed.
590
592  ∀n: nat.
593  ∀l: BitVector n.
594    l = add n l (zero …).
595  #n #l elim l try %
596  #n' #hd #tl #inductive_hypothesis
597  change with (false:::zero ?) in match (zero ?);
599  cases hd <inductive_hypothesis %
600qed.
601
602axiom most_significant_bit_zero:
603  ∀size, m: nat.
604  ∀size_proof: 0 < size.
605    m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false.
606  normalize in size_proof; normalize @le_S_S assumption
607qed.
608
610  ∀m: nat.
611  ∀tl, hd.
612    (hd:::add m (zero m) tl) = add (S m) (zero (S m)) (hd:::tl).
613
615  ∀m: nat.
616  ∀b: BitVector m.
617    add m (zero m) b = b.
618  #m #b elim b try %
619  #m' #hd #tl #inductive_hypothesis
620  <inductive_hypothesis in ⊢ (???%);
622qed.
623
624axiom bitvector_of_nat_one_Sm:
625  ∀m: nat.
626    ∃b: BitVector m.
627      bitvector_of_nat (S m) 1 ≃ b @@ [[true]].
628
629axiom increment_zero_bitvector_of_nat_1:
630  ∀m: nat.
631  ∀b: BitVector m.
632    increment m b = add m (bitvector_of_nat m 1) b.
633
635  ∀m: nat.
636  ∀l, c, r: BitVector m.
638
639lemma bitvector_of_nat_aux_buffer:
640  ∀m, n: nat.
641  ∀b: BitVector m.
642    bitvector_of_nat_aux m n b = add m (bitvector_of_nat m n) b.
643  #m #n elim n
644  [1:
645    #b change with (? = add ? (zero …) b)
647  |2:
648    #n' #inductive_hypothesis #b
649    whd in match (bitvector_of_nat_aux ???);
650    >inductive_hypothesis whd in match (bitvector_of_nat ??) in ⊢ (???%);
651    >inductive_hypothesis >increment_zero_bitvector_of_nat_1
652    >increment_zero_bitvector_of_nat_1 <(add_zero m (bitvector_of_nat m 1))
654  ]
655qed.
656
657definition sign_extension: Byte → Word ≝
658  λc.
659    let b ≝ get_index_v ? 8 c 1 ? in
660      [[ b; b; b; b; b; b; b; b ]] @@ c.
661  normalize
662  repeat (@le_S_S)
663  @le_O_n
664qed.
665
666lemma bitvector_of_nat_sign_extension_equivalence:
667  ∀m: nat.
668  ∀size_proof: m < 128.
669    sign_extension … (bitvector_of_nat 8 m) = bitvector_of_nat 16 m.
670  #m #size_proof whd in ⊢ (??%?);
671  >most_significant_bit_zero
672  [1:
673    elim m
674    [1:
675      %
676    |2:
677      #n' #inductive_hypothesis whd in match bitvector_of_nat; normalize nodelta
678      whd in match (bitvector_of_nat_aux ???);
679      whd in match (bitvector_of_nat_aux ???) in ⊢ (???%);
680      >(bitvector_of_nat_aux_buffer 16 n')
681      cases daemon
682    ]
683  |2:
684    assumption
685  ]
686qed.
687
689  ∀n: nat.
690  ∀l, r: BitVector n.
692
694 ∀n,v1,v2.
695  nat_of_bitvector n v1 + nat_of_bitvector n v2 < 2^n →
696   nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2.
697
699  ∀n: nat.
700  ∀m: nat.
701    add n (bitvector_of_nat … m) (bitvector_of_nat … 1) = bitvector_of_nat … (S m).
702 cases daemon.
703qed.
704
706  ∀n,p,q:nat.
707    add n (bitvector_of_nat ? p) (bitvector_of_nat ? q) = bitvector_of_nat ? (p+q).
708
709definition sign_bit : ∀n. BitVector n → bool ≝
710λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
711
712definition sign_extend : ∀m,n. BitVector m → BitVector (n+m) ≝
713λm,n,v. pad_vector ? (sign_bit ? v) ?? v.
714
715definition zero_ext : ∀m,n. BitVector m → BitVector n ≝
716λm,n.
717  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
718  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (pad … v)
719  | nat_eq n' ⇒ λv. v
720  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
721  ].
722
723definition sign_ext : ∀m,n. BitVector m → BitVector n ≝
724λm,n.
725  match nat_compare m n return λm,n.λ_. BitVector m → BitVector n with
726  [ nat_lt m' n' ⇒ λv. switch_bv_plus … (sign_extend … v)
727  | nat_eq n' ⇒ λv. v
728  | nat_gt m' n' ⇒ λv. \snd (vsplit … (switch_bv_plus … v))
729  ].
730
Note: See TracBrowser for help on using the repository browser.