source: Deliverables/D4.1/Matita/BitVector.ma @ 363

Last change on this file since 363 was 362, checked in by sacerdot, 10 years ago

Less ambiguous definitions.

File size: 6.7 KB
RevLine 
[236]1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* BitVector.ma: Fixed length bitvectors, and common operations on them.      *)
[240]3(*               Most functions are specialised versions of those found in    *)
4(*               Vector.ma as a courtesy, or Boolean functions lifted into    *)
5(*               BitVector variants.                                          *)
[236]6(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
7
[246]8include "Vector.ma".
[240]9
[236]10(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
11(* Common synonyms.                                                           *)
12(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
13
[228]14ndefinition BitVector ≝ λn: Nat. Vector Bool n.
[263]15ndefinition Bit ≝ Bool.
[230]16ndefinition Nibble ≝ BitVector (S (S (S (S Z)))).
17ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))).
18ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))).
19ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))).
[271]20ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S Z))))))))))).
[224]21
[236]22(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[240]23(* Lookup.                                                                    *)
24(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
25
[362]26(*
[337]27ndefinition get_index_bv ≝
[240]28  λn: Nat.
29  λb: BitVector n.
30  λm: Nat.
[266]31  λp: m < n.
[362]32    get_index_bv Bool n b m p.
[240]33   
34interpretation "BitVector get_index" 'get_index b n = (get_index ? b n).
35   
[337]36ndefinition set_index_bv ≝
[240]37  λn: Nat.
38  λb: BitVector n.
39  λm: Nat.
[266]40  λp: m < n.
41  λc: Bool.
[314]42    set_index Bool n b m c.
[240]43   
44ndefinition drop ≝
45  λn: Nat.
46  λb: BitVector n.
47  λm: Nat.
48    drop Bool n b m.
[362]49*)
[240]50
51(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[236]52(* Creating bitvectors from scratch.                                          *)
53(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
54
[362]55ndefinition zero: ∀n:Nat. BitVector n ≝
56  λn: Nat. replicate Bool n false.
[228]57   
[362]58ndefinition max: ∀n:Nat. BitVector n ≝
59  λn: Nat. replicate Bool n true.
60
61(*
[237]62ndefinition append ≝
63  λm, n: Nat.
64  λb: BitVector m.
65  λc: BitVector n.
66    append Bool m n b c.
[362]67*)
68 
[237]69ndefinition pad ≝
70  λm, n: Nat.
71  λb: BitVector n.
[260]72    let padding ≝ replicate Bool m false in
[237]73      append Bool m n padding b.
[240]74     
75(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
76(* Other manipulations.                                                       *)
77(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[237]78
[362]79(*
[240]80ndefinition reverse ≝
81  λn: Nat.
82  λb: BitVector n.
83    reverse Bool n b.
84
85ndefinition length ≝
86  λn: Nat.
87  λb: BitVector n.
88    length Bool n b.
[362]89*)
[240]90
[236]91(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
92(* Logical operations.                                                        *)
93(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
94   
[343]95ndefinition conjunction_bv ≝
[228]96  λn: Nat.
97  λb: BitVector n.
98  λc: BitVector n.
[240]99    zip_with Bool Bool Bool n conjunction b c.
100   
101interpretation "BitVector conjunction" 'conjunction b c = (conjunction ? b c).
[237]102   
[343]103ndefinition inclusive_disjunction_bv ≝
[228]104  λn: Nat.
105  λb: BitVector n.
106  λc: BitVector n.
[240]107    zip_with Bool Bool Bool n inclusive_disjunction b c.
108   
109interpretation "BitVector inclusive disjunction"
110  'inclusive_disjunction b c = (inclusive_disjunction ? b c).
[237]111         
[343]112ndefinition exclusive_disjunction_bv ≝
[228]113  λn: Nat.
114  λb: BitVector n.
115  λc: BitVector n.
[240]116    zip_with Bool Bool Bool n exclusive_disjunction b c.
[232]117   
[240]118interpretation "BitVector exclusive disjunction"
119  'exclusive_disjunction b c = (exclusive_disjunction ? b c).
120   
[337]121ndefinition negation_bv ≝
[234]122  λn: Nat.
123  λb: BitVector n.
124    map Bool Bool n (negation) b.
[240]125   
126interpretation "BitVector negation" 'negation b c = (negation ? b c).
[238]127
128(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
129(* Rotates and shifts.                                                        *)
130(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
131
[362]132(*
[337]133ndefinition rotate_left_bv ≝
134  λn, m: Nat.
[238]135  λb: BitVector n.
136    rotate_left Bool n m b.
137
[337]138ndefinition rotate_right_bv ≝
139  λn, m: Nat.
[238]140  λb: BitVector n.
[240]141    rotate_right Bool n m b.
[236]142   
[337]143ndefinition shift_left_bv ≝
144  λn, m: Nat.
[240]145  λb: BitVector n.
146  λc: Bool.
147    shift_left Bool n m b c.
148   
[337]149ndefinition shift_right_bv ≝
150  λn, m: Nat.
[240]151  λb: BitVector n.
152  λc: Bool.
153    shift_right Bool n m b c.
[362]154*)
155 
[236]156(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
157(* Conversions to and from lists and natural numbers.                         *)
158(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
[232]159
[362]160(*
[237]161ndefinition list_of_bitvector ≝
162  λn: Nat.
163  λb: BitVector n.
164    list_of_vector Bool n b.
[236]165   
[237]166ndefinition bitvector_of_list ≝
167  λl: List Bool.
168    vector_of_list Bool l.
[362]169*)
[234]170
[353]171nlet rec bitvector_of_nat_aux (n: Nat) (bound: Nat) on bound ≝
172 match bound with
173  [ Z ⇒ Empty Bool (* IT WILL NOT HAPPEN *)
174  | S bound ⇒
175    let divrem ≝ divide_with_remainder n (S (S Z)) in
176    let div ≝ first Nat Nat divrem in
177    let rem ≝ second Nat Nat divrem in
178      match div with
179        [ Z ⇒
180          match rem with
181            [ Z ⇒ Empty Bool
182            | S r ⇒ true :: (bitvector_of_nat_aux Z bound)
183            ]
184        | S d ⇒
185          match rem with
186            [ Z ⇒ false :: (bitvector_of_nat_aux (S d) bound)
187            | S r ⇒ true :: (bitvector_of_nat_aux (S d) bound)
188            ]
189        ]].
[236]190
[315]191ndefinition eq_bv ≝
192  λn: Nat.
193  λb, c: BitVector n.
194    eq_v Bool n (λd, e.
195      if inclusive_disjunction (conjunction d e) (conjunction (negation d)
196                                                              (negation e)) then
197        true
198      else
199        false) b c.
200
[273]201nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝
[353]202  let biglist ≝ reverse ? (bitvector_of_nat_aux m m) in
[273]203  let size ≝ length ? biglist in
[362]204  let bitvector ≝ vector_of_list ? biglist in
[273]205  let difference ≝ n - size in
[351]206   less_than_or_equal_b_elim …
207    (λH:size ≤ n. ((pad difference size bitvector)⌈BitVector n ↦ BitVector (difference+size)⌉))
208    (λH:¬(size ≤ n). max n).
209 nnormalize; nrewrite > (plus_minus_inverse_right n ?); //; nassumption.
[273]210nqed.
211
[237]212nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b ≝
213  match b with
214    [ Empty ⇒ Z
215    | Cons o hd tl ⇒
[260]216      let hdval ≝ match hd with [ true ⇒ S Z | false ⇒ Z ] in
[248]217        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
[349]218    ].
Note: See TracBrowser for help on using the repository browser.