source: src/ASM/BitVector.ma @ 981

Last change on this file since 981 was 961, checked in by campbell, 10 years ago

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File size: 4.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/Util.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(* Lookup.                                                                    *)
28(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
29
30(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
31(* Creating bitvectors from scratch.                                          *)
32(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
33
34definition zero: ∀n:nat. BitVector n ≝
35  λn: nat. replicate bool n false.
36   
37definition maximum: ∀n:nat. BitVector n ≝
38  λn: nat. replicate bool n true.
39 
40definition pad ≝
41  λm, n: nat.
42  λb: BitVector n. pad_vector ? false m n b.
43     
44(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
45(* Other manipulations.                                                       *)
46(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
47
48(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
49(* Logical operations.                                                        *)
50(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
51   
52definition conjunction_bv: ∀n. ∀b, c: BitVector n. BitVector n ≝
53  λn: nat.
54  λb: BitVector n.
55  λc: BitVector n.
56    zip_with ? ? ? n (andb) b c.
57   
58interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c).
59   
60definition inclusive_disjunction_bv ≝
61  λn: nat.
62  λb: BitVector n.
63  λc: BitVector n.
64    zip_with ? ? ? n (orb) b c.
65   
66interpretation "BitVector inclusive disjunction"
67  'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c).
68         
69definition exclusive_disjunction_bv ≝
70  λn: nat.
71  λb: BitVector n.
72  λc: BitVector n.
73    zip_with ? ? ? n (exclusive_disjunction) b c.
74   
75interpretation "BitVector exclusive disjunction"
76  'exclusive_disjunction b c = (exclusive_disjunction ? b c).
77   
78definition negation_bv ≝
79  λn: nat.
80  λb: BitVector n.
81    map bool bool n (notb) b.
82   
83interpretation "BitVector negation" 'negation b c = (negation_bv ? b c).
84
85(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
86(* Rotates and shifts.                                                        *)
87(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
88 
89(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
90(* Conversions to and from lists and natural numbers.                         *)
91(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
92
93definition eq_b ≝
94  λb, c: bool.
95    if b then
96      c
97    else
98      notb c.
99
100definition eq_bv ≝
101  λn: nat.
102  λb, c: BitVector n.
103    eq_v bool n eq_b b c.
104
105lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y.
106  (x = y → P true) →
107  (x ≠ y → P false) →
108  P (eq_bv n x y).
109#P #n #x #y #Ht #Hf whd in ⊢ (?%) @(eq_v_elim … Ht Hf)
110#Q * *; normalize /3/
111qed.
112
113lemma eq_bv_true: ∀n,v. eq_bv n v v = true.
114@eq_v_true * @refl
115qed.
116
117lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false.
118#n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ]
119qed.
120   
121axiom bitvector_of_string:
122  ∀n: nat.
123  ∀s: String.
124    BitVector n.
125   
126axiom string_of_bitvector:
127  ∀n: nat.
128  ∀b: BitVector n.
129    String.
Note: See TracBrowser for help on using the repository browser.