This repository has been archived by the owner on Oct 14, 2023. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 216
/
bitvec.lean
222 lines (171 loc) · 6.45 KB
/
bitvec.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
/-
Copyright (c) 2015 Joe Hendrix. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joe Hendrix, Sebastian Ullrich
Basic operations on bitvectors.
This is a work-in-progress, and contains additions to other theories.
-/
import data.vector
@[reducible] def bitvec (n : ℕ) := vector bool n
namespace bitvec
open nat
open vector
local infix `++ₜ`:65 := vector.append
-- Create a zero bitvector
@[reducible] protected def zero (n : ℕ) : bitvec n := repeat ff n
-- Create a bitvector with the constant one.
@[reducible] protected def one : Π (n : ℕ), bitvec n
| 0 := []
| (succ n) := repeat ff n ++ₜ [tt]
protected def cong {a b : ℕ} (h : a = b) : bitvec a → bitvec b
| ⟨x, p⟩ := ⟨x, h ▸ p⟩
-- bitvec specific version of vector.append
def append {m n} : bitvec m → bitvec n → bitvec (m + n) := vector.append
section shift
variable {n : ℕ}
def shl (x : bitvec n) (i : ℕ) : bitvec n :=
bitvec.cong (by simp) $
dropn i x ++ₜ repeat ff (min n i)
def fill_shr (x : bitvec n) (i : ℕ) (fill : bool) : bitvec n :=
bitvec.cong
begin
by_cases (i ≤ n),
{ have h₁ := sub_le n i,
rw [min_eq_right h], rw [min_eq_left h₁, -nat.add_sub_assoc h, add_comm, nat.add_sub_cancel] },
{ have h₁ := le_of_not_ge h,
rw [min_eq_left h₁, sub_eq_zero_of_le h₁, min_zero_left, add_zero] }
end $
repeat fill (min n i) ++ₜ taken (n-i) x
-- unsigned shift right
def ushr (x : bitvec n) (i : ℕ) : bitvec n :=
fill_shr x i ff
-- signed shift right
def sshr : Π {m : ℕ}, bitvec m → ℕ → bitvec m
| 0 _ _ := []
| (succ m) x i := head x :: fill_shr (tail x) i (head x)
end shift
section bitwise
variable {n : ℕ}
def not : bitvec n → bitvec n := map bnot
def and : bitvec n → bitvec n → bitvec n := map₂ band
def or : bitvec n → bitvec n → bitvec n := map₂ bor
def xor : bitvec n → bitvec n → bitvec n := map₂ bxor
end bitwise
section arith
variable {n : ℕ}
protected def xor3 (x y c : bool) := bxor (bxor x y) c
protected def carry (x y c : bool) :=
x && y || x && c || y && c
protected def neg (x : bitvec n) : bitvec n :=
let f := λ y c, (y || c, bxor y c) in
prod.snd (map_accumr f x ff)
-- Add with carry (no overflow)
def adc (x y : bitvec n) (c : bool) : bitvec (n+1) :=
let f := λ x y c, (bitvec.carry x y c, bitvec.xor3 x y c) in
let ⟨c, z⟩ := vector.map_accumr₂ f x y c in
c :: z
protected def add (x y : bitvec n) : bitvec n := tail (adc x y ff)
-- Subtract with borrow
def sbb (x y : bitvec n) (b : bool) : bool × bitvec n :=
let f := λ x y c, (bitvec.carry (bnot x) y c, bitvec.xor3 x y c) in
vector.map_accumr₂ f x y b
protected def sub (x y : bitvec n) : bitvec n := prod.snd (sbb x y ff)
instance : has_zero (bitvec n) := ⟨bitvec.zero n⟩
instance : has_one (bitvec n) := ⟨bitvec.one n⟩
instance : has_add (bitvec n) := ⟨bitvec.add⟩
instance : has_sub (bitvec n) := ⟨bitvec.sub⟩
instance : has_neg (bitvec n) := ⟨bitvec.neg⟩
protected def mul (x y : bitvec n) : bitvec n :=
let f := λ r b, cond b (r + r + y) (r + r) in
(to_list x).foldl f 0
instance : has_mul (bitvec n) := ⟨bitvec.mul⟩
end arith
section comparison
variable {n : ℕ}
def uborrow (x y : bitvec n) : bool := prod.fst (sbb x y ff)
def ult (x y : bitvec n) : Prop := uborrow x y
def ugt (x y : bitvec n) : Prop := ult y x
def ule (x y : bitvec n) : Prop := ¬ (ult y x)
def uge (x y : bitvec n) : Prop := ule y x
def sborrow : Π {n : ℕ}, bitvec n → bitvec n → bool
| 0 _ _ := ff
| (succ n) x y :=
match (head x, head y) with
| (tt, ff) := tt
| (ff, tt) := ff
| _ := uborrow (tail x) (tail y)
end
def slt (x y : bitvec n) : Prop := sborrow x y
def sgt (x y : bitvec n) : Prop := slt y x
def sle (x y : bitvec n) : Prop := ¬ (slt y x)
def sge (x y : bitvec n) : Prop := sle y x
end comparison
section conversion
variable {α : Type}
protected def of_nat : Π (n : ℕ), nat → bitvec n
| 0 x := nil
| (succ n) x := of_nat n (x / 2) ++ₜ [to_bool (x % 2 = 1)]
protected def of_int : Π (n : ℕ), int → bitvec (succ n)
| n (int.of_nat m) := ff :: bitvec.of_nat n m
| n (int.neg_succ_of_nat m) := tt :: not (bitvec.of_nat n m)
def add_lsb (r : ℕ) (b : bool) := r + r + cond b 1 0
def bits_to_nat (v : list bool) : nat :=
v.foldl add_lsb 0
protected def to_nat {n : nat} (v : bitvec n) : nat :=
bits_to_nat (to_list v)
lemma bits_to_nat_to_list {n : ℕ} (x : bitvec n)
: bitvec.to_nat x = bits_to_nat (vector.to_list x) := rfl
theorem to_nat_append {m : ℕ} (xs : bitvec m) (b : bool)
: bitvec.to_nat (xs ++ₜ[b]) = bitvec.to_nat xs * 2 + bitvec.to_nat [b] :=
begin
cases xs with xs P,
simp [bits_to_nat_to_list], clear P,
unfold bits_to_nat list.foldl,
-- the next 4 lines generalize the accumulator of foldl
let x := 0,
change _ = add_lsb x b + _,
generalize 0 y,
revert x, simp,
induction xs with x xs ; intro y,
{ simp, unfold list.foldl add_lsb, simp [nat.mul_succ] },
{ simp, apply ih_1 }
end
theorem bits_to_nat_to_bool (n : ℕ)
: bitvec.to_nat [to_bool (n % 2 = 1)] = n % 2 :=
begin
simp [bits_to_nat_to_list],
unfold bits_to_nat add_lsb list.foldl cond,
simp [cond_to_bool_mod_two],
end
lemma of_nat_succ {k n : ℕ}
: bitvec.of_nat (succ k) n = bitvec.of_nat k (n / 2) ++ₜ[to_bool (n % 2 = 1)] :=
rfl
theorem to_nat_of_nat {k n : ℕ}
: bitvec.to_nat (bitvec.of_nat k n) = n % 2^k :=
begin
revert n,
induction k with k ; intro n,
{ unfold pow, simp [nat.mod_one], refl },
{ have h : 0 < 2, { apply le_succ },
rw [ of_nat_succ
, to_nat_append
, ih_1
, bits_to_nat_to_bool
, mod_pow_succ h],
ac_refl, }
end
protected def to_int : Π {n : nat}, bitvec n → int
| 0 _ := 0
| (succ n) v :=
cond (head v)
(int.neg_succ_of_nat $ bitvec.to_nat $ not $ tail v)
(int.of_nat $ bitvec.to_nat $ tail v)
end conversion
private def repr {n : nat} : bitvec n → string
| ⟨bs, p⟩ :=
"0b" ++ (bs.map (λ b : bool, if b then '1' else '0')).as_string
instance (n : nat) : has_repr (bitvec n) :=
⟨repr⟩
end bitvec
instance {n} {x y : bitvec n} : decidable (bitvec.ult x y) := bool.decidable_eq _ _
instance {n} {x y : bitvec n} : decidable (bitvec.ugt x y) := bool.decidable_eq _ _