source: src/ASM/BitVector.ma @ 868

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

more changes

File size: 4.2 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   
113axiom bitvector_of_string:
114  ∀n: nat.
115  ∀s: String.
116    BitVector n.
117   
118axiom string_of_bitvector:
119  ∀n: nat.
120  ∀b: BitVector n.
121    String.
Note: See TracBrowser for help on using the repository browser.