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

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

Moved over to standard library.

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