source: src/ASM/BitVector.ma @ 2122

Last change on this file since 2122 was 2122, checked in by sacerdot, 7 years ago

More stuff moved around in proper places
File size: 7.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 "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
53alias id "bv_zero" = "cic:/matita/cerco/ASM/BitVector/zero.def(2)".
54
55definition maximum: ∀n:nat. BitVector n ≝
56  λn: nat. replicate bool n true.
57 
58definition pad ≝
59  λm, n: nat.
60  λb: BitVector n. pad_vector ? false m n b.
61
62(* jpb: we already have bitvector_of_nat and friends in the library, maybe
63 * we should unify this in some way *) 
64let rec nat_to_bv (n : nat) (k : nat) on n : BitVector n ≝
65  match n with
66  [ O ⇒ VEmpty ?
67  | S n' ⇒
68    eqb (k mod 2) 1 ::: nat_to_bv n' (k ÷ 2)
69  ].
70 
71let rec bv_to_nat (n : nat) (b : BitVector n) on b : nat ≝
72  match b with
73  [ VEmpty ⇒ 0
74  | VCons n' x b' ⇒ (if x then 1 else 0) + bv_to_nat n' b' * 2].
75
76(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
77(* Other manipulations.                                                       *)
78(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
79
80(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
81(* Logical operations.                                                        *)
82(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
83   
84definition conjunction_bv: ∀n. ∀b, c: BitVector n. BitVector n ≝
85  λn: nat.
86  λb: BitVector n.
87  λc: BitVector n.
88    zip_with ? ? ? n (andb) b c.
89   
90interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c).
91   
92definition inclusive_disjunction_bv ≝
93  λn: nat.
94  λb: BitVector n.
95  λc: BitVector n.
96    zip_with ? ? ? n (orb) b c.
97   
98interpretation "BitVector inclusive disjunction"
99  'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c).
100         
101definition exclusive_disjunction_bv ≝
102  λn: nat.
103  λb: BitVector n.
104  λc: BitVector n.
105    zip_with ? ? ? n xorb b c.
106   
107interpretation "BitVector exclusive disjunction"
108  'exclusive_disjunction b c = (xorb b c).
109   
110definition negation_bv ≝
111  λn: nat.
112  λb: BitVector n.
113    map bool bool n (notb) b.
114   
115interpretation "BitVector negation" 'negation b c = (negation_bv ? b c).
116
117(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
118(* Rotates and shifts.                                                        *)
119(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
120 
121(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
122(* Conversions to and from lists and natural numbers.                         *)
123(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
124
125definition eq_b ≝
126  λb, c: bool.
127    if b then
128      c
129    else
130      notb c.
131
132lemma eq_b_refl:
133  ∀b.
134    eq_b b b = true.
135  #b cases b //
136qed.
137
138lemma eq_b_eq:
139  ∀b, c.
140    eq_b b c = true → b = c.
141  #b #c
142  cases b
143  cases c
144  normalize //
145qed.
146
147definition eq_bv ≝
148  λn: nat.
149  λb, c: BitVector n.
150    eq_v bool n eq_b b c.
151
152lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y.
153  (x = y → P true) →
154  (x ≠ y → P false) →
155  P (eq_bv n x y).
156#P #n #x #y #Ht #Hf whd in ⊢ (?%); @(eq_v_elim … Ht Hf)
157#Q * *; normalize /3/
158qed.
159
160lemma eq_bv_true: ∀n,v. eq_bv n v v = true.
161@eq_v_true * @refl
162qed.
163
164lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false.
165#n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ]
166qed.
167
168lemma eq_bv_refl:
169  ∀n,v. eq_bv n v v = true.
170  #n #v
171  elim v
172  [ //
173  | #n #hd #tl #ih
174    normalize
175    cases hd
176    [ normalize
177      @ ih
178    | normalize
179      @ ih
180    ]
181  ]
182qed.
183
184lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1.
185 #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/]
186qed.
187
188lemma eq_eq_bv:
189  ∀n, v, q.
190    v = q → eq_bv n v q = true.
191  #n #v
192  elim v
193  [ #q #h <h normalize %
194  | #n #hd #tl #ih #q #h >h //
195  ]
196qed.
197
198lemma eq_bv_eq:
199  ∀n, v, q.
200    eq_bv n v q = true → v = q.
201  #n #v #q generalize in match v;
202  elim q
203  [ #v #h @BitVector_O
204  | #n #hd #tl #ih #v' #h
205    cases (BitVector_Sn ? v')
206    #hd' * #tl' #jmeq >jmeq in h;
207    #new_h
208    change with ((andb ? ?) = ?) in new_h;
209    cases(conjunction_true … new_h)
210    #eq_heads #eq_tails
211    whd in eq_heads:(??(??(%))?);
212    cases(eq_b_eq … eq_heads)
213    whd in eq_tails:(??(?????(%))?);
214    change with (eq_bv ??? = ?) in eq_tails;
215    <(ih tl') //
216  ]
217qed.
218
219corollary refl_iff_eq_bv_true:
220  ∀n: nat.
221  ∀x: BitVector n.
222  ∀y: BitVector n.
223    eq_bv n x y = true ↔ x = y.
224  #n #x #y whd in match iff; normalize nodelta
225  @conj /2/
226qed.
227
228axiom bitvector_of_string:
229  ∀n: nat.
230  ∀s: String.
231    BitVector n.
232   
233axiom string_of_bitvector:
234  ∀n: nat.
235  ∀b: BitVector n.
236    String.
237
238example sub_minus_one_seven_eight:
239  ∀v: BitVector 7.
240  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
241  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
242 cases daemon.
243qed.
244
245axiom sub16_with_carry_overflow:
246  ∀left, right, result: BitVector 16.
247  ∀flags: BitVector 3.
248  ∀upper: BitVector 9.
249  ∀lower: BitVector 7.
250    sub_16_with_carry left right false = 〈result, flags〉 →
251      vsplit bool 9 7 result = 〈upper, lower〉 →
252        get_index_v bool 3 flags 2 ? = true →
253          upper = [[true; true; true; true; true; true; true; true; true]].
254  //
255qed.
256
257axiom sub_16_to_add_16_8_0:
258 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
259  get_index' ? 2 0 flags = false →
260  sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 →
261   v1 = add ? v2 (sign_extension (false:::v3)).
262
263axiom sub_16_to_add_16_8_1:
264 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
265  get_index' ? 2 0 flags = true →
266  sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 →
267   v1 = add ? v2 (sign_extension (true:::v3)).
Note: See TracBrowser for help on using the repository browser.