source: src/ASM/BitVector.ma @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 7.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
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
228(*
229axiom bitvector_of_string:
230  ∀n: nat.
231  ∀s: String.
232    BitVector n.
233   
234axiom string_of_bitvector:
235  ∀n: nat.
236  ∀b: BitVector n.
237    String.
238*)
239
240lemma bitvector_3_cases:
241  ∀w: BitVector 3.
242   ∃b0,b1,b2: bool.
243    w ≃ [[b0;b1;b2]].
244  #w
245 repeat (cases (BitVector_Sn … w)  #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w)
246 >(BitVector_O … w) %
247qed.
248
249lemma bitvector_11_cases:
250  ∀w: BitVector 11.
251    ∃b0,b1,b2,b3,b4,b5,b6,b7,b8,b9,b10: bool.
252      w ≃ [[b0;b1;b2;b3;b4;b5;b6;b7;b8;b9;b10]].
253 #w
254 repeat (cases (BitVector_Sn … w)  #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w)
255 >(BitVector_O … w) %
256qed.
257
258lemma bitvector_3_elim_prop:
259  ∀P: BitVector 3 → Prop.
260    P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
261    P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
262    P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
263  #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
264  cases (bitvector_3_cases … H9) #l #assm cases assm
265  -assm #c #assm cases assm
266  -assm #r #assm cases assm destruct
267  cases l cases c cases r assumption
268qed.
Note: See TracBrowser for help on using the repository browser.