source: src/ASM/BitVector.ma @ 1928

Last change on this file since 1928 was 1928, checked in by mulligan, 8 years ago

Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should rightfully be in another file. Added a new file, ASM/UtilBranch.ma for code that should rightfully be in ASM/Util.ma but is incomplete (i.e. daemons).

File size: 6.7 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 lapply (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 lapply (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(* jpb: we already have bitvector_of_nat and friends in the library, maybe
61 * we should unify this in some way *) 
62let rec nat_to_bv (n : nat) (k : nat) on n : BitVector n ≝
63  match n with
64  [ O ⇒ VEmpty ?
65  | S n' ⇒
66    eqb (k mod 2) 1 ::: nat_to_bv n' (k ÷ 2)
67  ].
68 
69let rec bv_to_nat (n : nat) (b : BitVector n) on b : nat ≝
70  match b with
71  [ VEmpty ⇒ 0
72  | VCons n' x b' ⇒ (if x then 1 else 0) + bv_to_nat n' b' * 2].
73
74(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
75(* Other manipulations.                                                       *)
76(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
77
78(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
79(* Logical operations.                                                        *)
80(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
81   
82definition conjunction_bv: ∀n. ∀b, c: BitVector n. BitVector n ≝
83  λn: nat.
84  λb: BitVector n.
85  λc: BitVector n.
86    zip_with ? ? ? n (andb) b c.
87   
88interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c).
89   
90definition inclusive_disjunction_bv ≝
91  λn: nat.
92  λb: BitVector n.
93  λc: BitVector n.
94    zip_with ? ? ? n (orb) b c.
95   
96interpretation "BitVector inclusive disjunction"
97  'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c).
98         
99definition exclusive_disjunction_bv ≝
100  λn: nat.
101  λb: BitVector n.
102  λc: BitVector n.
103    zip_with ? ? ? n xorb b c.
104   
105interpretation "BitVector exclusive disjunction"
106  'exclusive_disjunction b c = (xorb b c).
107   
108definition negation_bv ≝
109  λn: nat.
110  λb: BitVector n.
111    map bool bool n (notb) b.
112   
113interpretation "BitVector negation" 'negation b c = (negation_bv ? b c).
114
115(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
116(* Rotates and shifts.                                                        *)
117(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
118 
119(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
120(* Conversions to and from lists and natural numbers.                         *)
121(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
122
123definition eq_b ≝
124  λb, c: bool.
125    if b then
126      c
127    else
128      notb c.
129
130lemma eq_b_eq:
131  ∀b, c.
132    eq_b b c = true → b = c.
133  #b #c
134  cases b
135  cases c
136  normalize //
137qed.
138
139definition eq_bv ≝
140  λn: nat.
141  λb, c: BitVector n.
142    eq_v bool n eq_b b c.
143
144lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y.
145  (x = y → P true) →
146  (x ≠ y → P false) →
147  P (eq_bv n x y).
148#P #n #x #y #Ht #Hf whd in ⊢ (?%); @(eq_v_elim … Ht Hf)
149#Q * *; normalize /3/
150qed.
151
152lemma eq_bv_true: ∀n,v. eq_bv n v v = true.
153@eq_v_true * @refl
154qed.
155
156lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false.
157#n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ]
158qed.
159
160lemma eq_bv_refl:
161  ∀n,v. eq_bv n v v = true.
162  #n #v
163  elim v
164  [ //
165  | #n #hd #tl #ih
166    normalize
167    cases hd
168    [ normalize
169      @ ih
170    | normalize
171      @ ih
172    ]
173  ]
174qed.
175
176lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1.
177 #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/]
178qed.
179
180lemma eq_eq_bv:
181  ∀n, v, q.
182    v = q → eq_bv n v q = true.
183  #n #v
184  elim v
185  [ #q #h <h normalize %
186  | #n #hd #tl #ih #q #h >h //
187  ]
188qed.
189
190lemma eq_bv_eq:
191  ∀n, v, q.
192    eq_bv n v q = true → v = q.
193  #n #v #q generalize in match v;
194  elim q
195  [ #v #h @BitVector_O
196  | #n #hd #tl #ih #v' #h
197    cases (BitVector_Sn ? v')
198    #hd' * #tl' #jmeq >jmeq in h;
199    #new_h
200    change with ((andb ? ?) = ?) in new_h;
201    cases(conjunction_true … new_h)
202    #eq_heads #eq_tails
203    whd in eq_heads:(??(??(%))?);
204    cases(eq_b_eq … eq_heads)
205    whd in eq_tails:(??(?????(%))?);
206    change with (eq_bv ??? = ?) in eq_tails;
207    <(ih tl') //
208  ]
209qed.
210
211corollary refl_iff_eq_bv_true:
212  ∀n: nat.
213  ∀x: BitVector n.
214  ∀y: BitVector n.
215    eq_bv n x y = true ↔ x = y.
216  #n #x #y whd in match iff; normalize nodelta
217  @conj /2/
218qed.
219
220axiom bitvector_of_string:
221  ∀n: nat.
222  ∀s: String.
223    BitVector n.
224   
225axiom string_of_bitvector:
226  ∀n: nat.
227  ∀b: BitVector n.
228    String.
Note: See TracBrowser for help on using the repository browser.