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 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
8 include "arithmetics/nat.ma".
10 include "ASM/FoldStuff.ma".
11 include "ASM/Vector.ma".
12 include "ASM/String.ma".
14 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
15 (* Common synonyms. *)
16 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
18 definition BitVector ≝ λn: nat. Vector bool n.
19 definition Bit ≝ bool.
20 definition Nibble ≝ BitVector 4.
21 definition Byte7 ≝ BitVector 7.
22 definition Byte ≝ BitVector 8.
23 definition Word ≝ BitVector 16.
24 definition Word11 ≝ BitVector 11.
26 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
28 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
30 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
31 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
32 #n #hd #tl #abs @⊥ destruct (abs)
35 lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
36 ∃hd.∃tl.v ≃ VCons bool n hd tl.
37 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
38 [ #abs @⊥ destruct (abs)
39 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
42 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
44 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
46 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
47 (* Creating bitvectors from scratch. *)
48 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
50 definition zero: ∀n:nat. BitVector n ≝
51 λn: nat. replicate bool n false.
53 definition maximum: ∀n:nat. BitVector n ≝
54 λn: nat. replicate bool n true.
58 λb: BitVector n. pad_vector ? false m n b.
60 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
61 (* Other manipulations. *)
62 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
64 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
65 (* Logical operations. *)
66 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
68 definition conjunction_bv: ∀n. ∀b, c: BitVector n. BitVector n ≝
72 zip_with ? ? ? n (andb) b c.
74 interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c).
76 definition inclusive_disjunction_bv ≝
80 zip_with ? ? ? n (orb) b c.
82 interpretation "BitVector inclusive disjunction"
83 'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c).
85 definition exclusive_disjunction_bv ≝
89 zip_with ? ? ? n (exclusive_disjunction) b c.
91 interpretation "BitVector exclusive disjunction"
92 'exclusive_disjunction b c = (exclusive_disjunction ? b c).
94 definition negation_bv ≝
97 map bool bool n (notb) b.
99 interpretation "BitVector negation" 'negation b c = (negation_bv ? b c).
101 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
102 (* Rotates and shifts. *)
103 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
105 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
106 (* Conversions to and from lists and natural numbers. *)
107 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
118 eq_b b c = true → b = c.
128 eq_v bool n eq_b b c.
130 lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y.
134 #P #n #x #y #Ht #Hf whd in ⊢ (?%) @(eq_v_elim … Ht Hf)
135 #Q * *; normalize /3/
138 lemma eq_bv_true: ∀n,v. eq_bv n v v = true.
142 lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false.
143 #n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct | @NE ]
147 ∀n,v. eq_bv n v v = true.
162 lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1.
163 #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/]
168 v = q → eq_bv n v q = true.
171 [ #q #h
\ 5h normalize="" %="" |="" #n="" #hd="" #tl="" #ih="" #q="" #h=""
\ 6h //
177 eq_bv n v q = true → v = q.
178 #n #v #q generalize in match v
181 | #n #hd #tl #ih #v' #h
182 cases (BitVector_Sn ? v')
183 #hd' * #tl' #jmeq >jmeq in h;
185 change in new_h with ((andb ? ?) = ?);
186 cases(conjunction_true … new_h)
188 whd in eq_heads:(??(??(%))?);
189 cases(eq_b_eq … eq_heads)
190 whd in eq_tails:(??(?????(%))?);
191 change in eq_tails with (eq_bv ??? = ?);
196 axiom bitvector_of_string:
201 axiom string_of_bitvector: