Skip to content

Commit 8eff281

Browse files
osmanyasar05osmanyasar05
committed
wip
1 parent d1bc3db commit 8eff281

6 files changed

Lines changed: 87 additions & 16 deletions

File tree

‎DatapathVerification/BitHeap/BVComb.lean‎

Lines changed: 43 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,9 @@ inductive ArithCircuit : Nat → Type
2626

2727
def BitVecEnv (w : Nat) := Nat → BitVec w
2828

29+
def BitVecEnv.toBitEnv (bv : BitVecEnv w) : Circuit.BitEnv :=
30+
fun n => (bv (n / w)).getLsbD (n % w)
31+
2932
/--
3033
Convert a bitheap into a new bitheap that has a single row,
3134
by using the naive compression algorithm.
@@ -35,15 +38,15 @@ def BitHeap.toSingleRow (bh : BitHeap w) : CircuitVector :=
3538
pp1.columns.toArray.map fun col => col.elems.toList.headD (.const false)
3639

3740
namespace ArithCircuit
41+
3842
/--
39-
Given a bitvector (x : BV 3), but a bitheap
43+
Given a bitvector (x : BV 3), build a bitheap
4044
```
4145
* * *
4246
x2 x1 x0
4347
```
4448
-/
4549
def bitheapOfVar (varIndex : Nat) : BitHeap w :=
46-
-- I want to create a bitheap that has one bit-variable per bit in the bitvector variable.
4750
-- | We need to know that this index is unique which is a gigantic pain.
4851
List.range w |>.foldl (fun bh i => bh.addBit i (BitHeap.Circuit.bit (varIndex * w + i))) (BitHeap.empty w)
4952

@@ -61,6 +64,44 @@ def toCircuitVector (c : ArithCircuit w) : CircuitVector :=
6164
let bh := c.toBitHeap
6265
BitHeap.toSingleRow bh
6366

67+
theorem BitVecEnv.toBitEnv_apply (bv : BitVecEnv w) (i k : Nat) (hk : k < w) :
68+
bv.toBitEnv (i * w + k) = (bv i).getLsbD k := by
69+
simp [BitVecEnv.toBitEnv]
70+
have h1 : (i * w + k) / w = i := by
71+
have hw : 0 < w := by grind
72+
rw [Nat.mul_comm, Nat.mul_add_div hw, Nat.add_eq_left, Nat.div_eq_of_lt hk]
73+
have h2 : k % w = k := by
74+
exact Nat.mod_eq_of_lt hk
75+
simp [h1, h2]
76+
77+
theorem bitheapOfVar_go (i : Nat) (bv : BitVecEnv w) (k : Nat) (hk : k ≤ w) :
78+
((List.range k).foldl
79+
(fun bh j => bh.addBit j (.bit (i * w + j)))
80+
(BitHeap.empty w)).eval bv.toBitEnv
81+
= (bv i).toNat % 2 ^ k := by
82+
induction k with
83+
| zero =>
84+
simp only [List.range_zero, List.foldl_nil, empty_eval, pow_zero]
85+
grind
86+
| succ m ih =>
87+
rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil]
88+
sorry
89+
90+
91+
theorem toBitHeap_correct (c : ArithCircuit w) (bv : BitVecEnv w) :
92+
c.toBitHeap.evalMod bv.toBitEnv = ((c.denote bv).toNat : Int):= by
93+
fun_induction toBitHeap with
94+
| case1 varIndex =>
95+
simp only [BitHeap.evalMod, bitheapOfVar]
96+
rw [bitheapOfVar_go varIndex bv w (le_refl w)]
97+
simp [denote]
98+
norm_cast
99+
rw [BitVec.toNat_mod_cancel]
100+
| case2 =>
101+
sorry
102+
| case3 =>
103+
sorry
104+
64105
end ArithCircuit
65106

66107
end Comb

‎DatapathVerification/BitHeap/BitHeap.lean‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,16 @@ Evaluate a bit-heap, to compute the final sum of all the bits in the heap.
5252
def eval (h : BitHeap w) (env : BitEnv) : Nat :=
5353
HornersMethod env h.columns.toList
5454

55+
@[simp]
56+
theorem empty_eval (env : BitEnv) : (empty w).eval env = 0 := by
57+
simp [eval, empty]
58+
induction w with
59+
| zero =>
60+
simp [HornersMethod]
61+
| succ w ih =>
62+
simp [List.replicate_succ, HornersMethod]
63+
grind
64+
5565
/--
5666
Evaluate a bit-heap modulo 2^width, to compute the final sum of all the bits in the heap.
5767
-/

‎DatapathVerification/BitHeap/Circuit.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ def numVars (c : Circuit) : Nat :=
3636
| .const _ => 0
3737

3838
/-- An environment assigns a value to each bit, where bits are given by natural number indexes. -/
39-
def BitEnv := Nat → Bool
39+
abbrev BitEnv := Nat → Bool
4040

4141
/-- Evaluate a circuit under a given environment. -/
4242
def eval (c : Circuit) (env : BitEnv) : Bool :=

‎DatapathVerification/BitHeap/Compressors/NaiveCompression.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,10 +13,10 @@ Another difference with the Wallace tree is that this naive approach consumes ca
1313
-- if height >= 4, apply FA. if height = 3, apply HA.
1414
def reduceColumnStep (col : Nat) (h : BitHeap w) : Option (BitHeap w × Adder) :=
1515
match (h.get col).toList with
16-
| a :: b :: c :: _ :: _ =>
16+
| a :: b :: c :: _ =>
1717
let FA := Adder.fullAdder col a b c
1818
some (Chain.applyAdder FA h, FA)
19-
| a :: b :: _ :: [] =>
19+
| a :: b :: [] =>
2020
let HA := Adder.halfAdder col a b
2121
some (Chain.applyAdder HA h, HA)
2222
| _ => none

‎DatapathVerification/BitHeap/Examples/BVCombExamples.lean‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
import DatapathVerification.BitHeap.BVComb
2+
3+
open BitHeap
4+
open Comb
5+
6+
def testEnv : BitVecEnv 4 := fun i => if i = 0 then 6#4 else 3#4
7+
8+
-- 6x3 = 18
9+
/--
10+
info: 18
11+
-/
12+
#guard_msgs in
13+
#eval (ArithCircuit.mul (.var 0) (.var 1) : ArithCircuit 4).toBitHeap.eval (BitVecEnv.toBitEnv testEnv)
14+
15+
-- 6 + 3 + 3 = 12
16+
/--
17+
info: 12
18+
-/
19+
#guard_msgs in
20+
#eval ((ArithCircuit.add [(.var 0), (.var 1), (.var 2)] : ArithCircuit 4).toCircuitVector).eval (BitVecEnv.toBitEnv testEnv)

‎DatapathVerification/BitHeap/Examples/NaiveCompressionExamples.lean‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -44,10 +44,10 @@ def env2 : BitEnv := fun n => n = 0 || n = 2 || n = 5 || n = 6
4444
-------------
4545

4646
/--
47-
info: 4
47+
info: 0
4848
-/
4949
#guard_msgs in
50-
#eval threeBitsInCol1.eval (show BitEnv from env1)
50+
#eval threeBitsInCol1.evalMod (show BitEnv from env1)
5151

5252
-- Chain length 1 (single FA)
5353
/--
@@ -58,18 +58,18 @@ info: 1
5858

5959
-- Reduced heap evaluates the same
6060
/--
61-
info: 4
61+
info: 0
6262
-/
6363
#guard_msgs in
64-
#eval (NaiveCompression.reduceColumn 1 threeBitsInCol1).1.eval (show BitEnv from env1)
64+
#eval (NaiveCompression.reduceColumn 1 threeBitsInCol1).1.evalMod (show BitEnv from env1)
6565

6666
-------------
6767

6868
/--
6969
info: 6
7070
-/
7171
#guard_msgs in
72-
#eval fiveBitsInCol1.eval (show BitEnv from env1)
72+
#eval fiveBitsInCol1.evalMod (show BitEnv from env1)
7373

7474
-- Chain length 2 (FA + FA)
7575
/--
@@ -87,32 +87,32 @@ info: 6
8787

8888
-------------
8989
/--
90-
info: 9
90+
info: 1
9191
-/
9292
#guard_msgs in
93-
#eval multiColSmall.eval (show BitEnv from env2)
93+
#eval multiColSmall.evalMod (show BitEnv from env2)
9494

9595
/--
96-
info: 2
96+
info: 5
9797
-/
9898
#guard_msgs in
9999
#eval (NaiveCompression.naiveCompression multiColSmall).2.length
100100

101101
-- Value preserved
102102
/--
103-
info: 9
103+
info: 1
104104
-/
105105
#guard_msgs in
106106
#eval (NaiveCompression.naiveCompression multiColSmall).1.eval (show BitEnv from env2)
107107

108108
/--
109-
info: 2
109+
info: 1
110110
-/
111111
#guard_msgs in
112112
#eval (NaiveCompression.naiveCompression multiColSmall).1.maxHeight
113113

114114
/--
115-
info: [FA(1: b2, b4, b3), HA(2: (((b2 ∧ b4) ∨ (b2 ∧ b3)) ∨ (b4 ∧ b3)), b7)]
115+
info: [HA(0: b1, b0), FA(1: b2, b4, b3), FA(1: ((b2 ⊕ b4) ⊕ b3), b5, (b1 ∧ b0)), FA(2: (((b2 ∧ b4) ∨ (b2 ∧ b3)) ∨ (b4 ∧ b3)), b6, b7), HA(2: (((((b2 ⊕ b4) ⊕ b3) ∧ b5) ∨ (((b2 ⊕ b4) ⊕ b3) ∧ (b1 ∧ b0))) ∨ (b5 ∧ (b1 ∧ b0))), (((((b2 ∧ b4) ∨ (b2 ∧ b3)) ∨ (b4 ∧ b3)) ⊕ b6) ⊕ b7))]
116116
-/
117117
#guard_msgs in
118118
#eval (NaiveCompression.naiveCompression multiColSmall).2

0 commit comments

Comments
 (0)