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

Last change on this file since 410 was 410, checked in by mulligan, 9 years ago

Using bitvectortries for a dictionary doesn't work even if we hypothesise conversion functions from bitvectors to string, and back again. Many changes, including most of the assembly function implemented.

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