source: Deliverables/D3.3/id-lookup-branch/ASM/BitVector.ma @ 3341

Last change on this file since 3341 was 990, checked in by sacerdot, 9 years ago

Do no longer use the daemon automatically :-)

File size: 6.1 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 "ASM/FoldStuff.ma".
11include "ASM/Vector.ma".
12include "ASM/String.ma".
13
14(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
15(* Common synonyms.                                                           *)
16(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
17
18definition BitVector ≝ λn: nat. Vector bool n.
19definition Bit ≝ bool.
20definition Nibble ≝ BitVector 4.
21definition Byte7 ≝ BitVector 7.
22definition Byte ≝ BitVector 8.
23definition Word ≝ BitVector 16.
24definition Word11 ≝ BitVector 11.
25
26(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
27(* Inversion                                                                  *)
28(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
29
30lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
31 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
32 #n #hd #tl #abs @⊥ destruct (abs)
33qed.
34
35lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
36 ∃hd.∃tl.v ≃ VCons bool n hd tl.
37 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
38 [ #abs @⊥ destruct (abs)
39 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
40qed.
41
42(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
43(* Lookup.                                                                    *)
44(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
45
46(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
47(* Creating bitvectors from scratch.                                          *)
48(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
49
50definition zero: ∀n:nat. BitVector n ≝
51  λn: nat. replicate bool n false.
52   
53definition maximum: ∀n:nat. BitVector n ≝
54  λn: nat. replicate bool n true.
55 
56definition pad ≝
57  λm, n: nat.
58  λb: BitVector n. pad_vector ? false m n b.
59     
60(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
61(* Other manipulations.                                                       *)
62(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
63
64(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
65(* Logical operations.                                                        *)
66(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
67   
68definition conjunction_bv: ∀n. ∀b, c: BitVector n. BitVector n ≝
69  λn: nat.
70  λb: BitVector n.
71  λc: BitVector n.
72    zip_with ? ? ? n (andb) b c.
73   
74interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c).
75   
76definition inclusive_disjunction_bv ≝
77  λn: nat.
78  λb: BitVector n.
79  λc: BitVector n.
80    zip_with ? ? ? n (orb) b c.
81   
82interpretation "BitVector inclusive disjunction"
83  'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c).
84         
85definition exclusive_disjunction_bv ≝
86  λn: nat.
87  λb: BitVector n.
88  λc: BitVector n.
89    zip_with ? ? ? n (exclusive_disjunction) b c.
90   
91interpretation "BitVector exclusive disjunction"
92  'exclusive_disjunction b c = (exclusive_disjunction ? b c).
93   
94definition negation_bv ≝
95  λn: nat.
96  λb: BitVector n.
97    map bool bool n (notb) b.
98   
99interpretation "BitVector negation" 'negation b c = (negation_bv ? b c).
100
101(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
102(* Rotates and shifts.                                                        *)
103(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
104 
105(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
106(* Conversions to and from lists and natural numbers.                         *)
107(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
108
109definition eq_b ≝
110  λb, c: bool.
111    if b then
112      c
113    else
114      notb c.
115
116lemma eq_b_eq:
117  ∀b, c.
118    eq_b b c = true → b = c.
119  #b #c
120  cases b
121  cases c
122  normalize //
123qed.
124
125definition eq_bv ≝
126  λn: nat.
127  λb, c: BitVector n.
128    eq_v bool n eq_b b c.
129
130lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y.
131  (x = y → P true) →
132  (x ≠ y → P false) →
133  P (eq_bv n x y).
134#P #n #x #y #Ht #Hf whd in ⊢ (?%) @(eq_v_elim … Ht Hf)
135#Q * *; normalize /3/
136qed.
137
138lemma eq_bv_true: ∀n,v. eq_bv n v v = true.
139@eq_v_true * @refl
140qed.
141
142lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false.
143#n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ]
144qed.
145
146lemma eq_bv_refl:
147  ∀n,v. eq_bv n v v = true.
148  #n #v
149  elim v
150  [ //
151  | #n #hd #tl #ih
152    normalize
153    cases hd
154    [ normalize
155      @ ih
156    | normalize
157      @ ih
158    ]
159  ]
160qed.
161
162lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1.
163 #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/]
164qed.
165
166lemma eq_eq_bv:
167  ∀n, v, q.
168    v = q → eq_bv n v q = true.
169  #n #v
170  elim v
171  [ #q #h <h normalize %
172  | #n #hd #tl #ih #q #h >h //
173  ]
174qed.
175
176lemma eq_bv_eq:
177  ∀n, v, q.
178    eq_bv n v q = true → v = q.
179  #n #v #q generalize in match v
180  elim q
181  [ #v #h @BitVector_O
182  | #n #hd #tl #ih #v' #h
183    cases (BitVector_Sn ? v')
184    #hd' * #tl' #jmeq >jmeq in h;
185    #new_h
186    change in new_h with ((andb ? ?) = ?);
187    cases(conjunction_true … new_h)
188    #eq_heads #eq_tails
189    whd in eq_heads:(??(??(%))?);
190    cases(eq_b_eq … eq_heads)
191    whd in eq_tails:(??(?????(%))?);
192    change in eq_tails with (eq_bv ??? = ?);
193    <(ih tl') //
194  ]
195qed.
196
197axiom bitvector_of_string:
198  ∀n: nat.
199  ∀s: String.
200    BitVector n.
201   
202axiom string_of_bitvector:
203  ∀n: nat.
204  ∀b: BitVector n.
205    String.
Note: See TracBrowser for help on using the repository browser.