source: src/ASM/BitVector.ma @ 724

Last change on this file since 724 was 724, checked in by campbell, 9 years ago

More tractable version of bitvector_of_nat / nat_of_bitvector.

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.
43    let padding ≝ replicate bool m false in
44      append bool m n padding b.
45     
46(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
47(* Other manipulations.                                                       *)
48(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
49
50(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
51(* Logical operations.                                                        *)
52(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
53   
54definition conjunction_bv: ∀n. ∀b, c: BitVector n. BitVector n ≝
55  λn: nat.
56  λb: BitVector n.
57  λc: BitVector n.
58    zip_with ? ? ? n (andb) b c.
59   
60interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c).
61   
62definition inclusive_disjunction_bv ≝
63  λn: nat.
64  λb: BitVector n.
65  λc: BitVector n.
66    zip_with ? ? ? n (orb) b c.
67   
68interpretation "BitVector inclusive disjunction"
69  'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c).
70         
71definition exclusive_disjunction_bv ≝
72  λn: nat.
73  λb: BitVector n.
74  λc: BitVector n.
75    zip_with ? ? ? n (exclusive_disjunction) b c.
76   
77interpretation "BitVector exclusive disjunction"
78  'exclusive_disjunction b c = (exclusive_disjunction ? b c).
79   
80definition negation_bv ≝
81  λn: nat.
82  λb: BitVector n.
83    map bool bool n (notb) b.
84   
85interpretation "BitVector negation" 'negation b c = (negation_bv ? b c).
86
87(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
88(* Rotates and shifts.                                                        *)
89(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
90 
91(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
92(* Conversions to and from lists and natural numbers.                         *)
93(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
94
95definition eq_bv ≝
96  λn: nat.
97  λb, c: BitVector n.
98    eq_v bool n (λd, e.
99      if (d ∧ e) ∨ ((¬d) ∧ (¬e)) then
100        true
101      else
102        false) b c.
103
104lemma eq_bv_elim: ∀P:bool → Prop. ∀n. ∀x,y.
105  (x = y → P true) →
106  (x ≠ y → P false) →
107  P (eq_bv n x y).
108#P #n #x #y #Ht #Hf whd in ⊢ (?%) @(eq_v_elim … Ht Hf)
109#Q * *; normalize /3/
110qed.
111   
112axiom bitvector_of_string:
113  ∀n: nat.
114  ∀s: String.
115    BitVector n.
116   
117axiom string_of_bitvector:
118  ∀n: nat.
119  ∀b: BitVector n.
120    String.
Note: See TracBrowser for help on using the repository browser.