source: src/ASM/BitVector.ma @ 1646

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