Skip to content

Commit f44ea0f

Browse files
osmanyasar05osmanyasar05
authored
first commit (#27)
1 parent 819c9ee commit f44ea0f

2 files changed

Lines changed: 71 additions & 29 deletions

File tree

‎DatapathVerification/BitHeap/BVComb.lean‎

Lines changed: 15 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ inductive ArithBinopKind
1313
| mul
1414

1515
inductive ArithCircuit : Nat → Type
16-
| var (varIndex : Nat) : ArithCircuit w
16+
| var (varIndex : Nat) (bits : Nat) : ArithCircuit w -- A w-bit operand with lowest `bits` as live bits. Operand is zero-extended from `bits` to `w`.
1717
| add (args : List (ArithCircuit w)) : ArithCircuit w
1818
| mul (l r : ArithCircuit w) : ArithCircuit w
1919
-- | arithunop (kind : ArithUnopKind) (width : Nat) (arg : ArithCircuit)
@@ -40,18 +40,21 @@ Given a bitvector (x : BV 3), build a bitheap
4040
* * *
4141
x2 x1 x0
4242
```
43+
44+
Only the lowest `bits` are added as variables. Remaning bits are 0's.
4345
-/
44-
def bitheapOfVar (varIndex : Nat) : BitHeap w :=
46+
def bitheapOfVar (varIndex : Nat) (bits : Nat) : BitHeap w :=
4547
-- | We need to know that this index is unique which is a gigantic pain.
46-
List.range w |>.foldl (fun bh i => bh.addBit i (BitHeap.Circuit.bit (varIndex * w + i))) (BitHeap.empty w)
48+
List.range (min bits w)
49+
|>.foldl (fun bh i => bh.addBit i (BitHeap.Circuit.bit (varIndex * w + i))) (BitHeap.empty w)
4750

4851
def toBitHeap : ArithCircuit w → BitHeap w
49-
| .var varIndex => bitheapOfVar varIndex
52+
| .var varIndex bits => bitheapOfVar varIndex bits
5053
| .add args => BitHeap.addBitHeap (args.map toBitHeap)
5154
| .mul l r => BitHeap.truncate ((toBitHeap l).mulBitHeap (toBitHeap r)) w (by omega)
5255

5356
def denote (ρ : BitVecEnv w) : ArithCircuit w → BitVec w
54-
| .var i => ρ i
57+
| .var i bits => ((ρ i).setWidth (min bits w)).setWidth w
5558
| .add args => (args.map (denote ρ)).foldl (· + ·) 0
5659
| .mul l r => denote ρ l * denote ρ r
5760

@@ -265,10 +268,13 @@ theorem mulBitHeap_evalMod (h0 h1 : BitHeap w) (env : Circuit.BitEnv) :
265268
theorem toBitHeap_correct (c : ArithCircuit w) (bv : BitVecEnv w) :
266269
c.toBitHeap.evalMod bv.toBitEnv = ((c.denote bv).toNat : Int) := by
267270
fun_induction toBitHeap with
268-
| case1 varIndex =>
269-
simp only [bitheapOfVar, bitheapOfVar_go varIndex bv w (le_refl w), denote]
270-
norm_cast
271-
rw [BitVec.toNat_mod_cancel]
271+
| case1 varIndex bits =>
272+
simp only [bitheapOfVar, denote,
273+
bitheapOfVar_go varIndex bv (min bits w) (Nat.min_le_right bits w)]
274+
have hlt : (bv varIndex).toNat % 2 ^ (min bits w) < 2 ^ w :=
275+
Nat.lt_of_lt_of_le (Nat.mod_lt _ (Nat.two_pow_pos _))
276+
(Nat.pow_le_pow_right (by omega) (Nat.min_le_right bits w))
277+
simp [BitVec.toNat_setWidth, Nat.mod_eq_of_lt hlt]
272278
| case2 args ih =>
273279
simp only [addBitHeap, foldl_mergeInto_evalMod, empty_evalMod, List.map_map, zero_add, denote,
274280
BitVec.ofNat_eq_ofNat, foldl_add_toNat_go, BitVec.toNat_ofNat, Nat.zero_mod, Nat.cast_zero]

‎DatapathVerification/BitHeap/Examples/BVCombExamples.lean‎

Lines changed: 56 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -15,67 +15,67 @@ def testEnv : BitVecEnv 4 := fun i =>
1515

1616
/-- info: 6 -/
1717
#guard_msgs in
18-
#eval (ArithCircuit.var 0 : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
18+
#eval (ArithCircuit.var 0 4 : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
1919

2020
-- add, no overflow: (6+3) % 16 = 9
2121
/-- info: 9 -/
2222
#guard_msgs in
23-
#eval (ArithCircuit.add [.var 0, .var 1] : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
23+
#eval (ArithCircuit.add [.var 0 4, .var 1 4] : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
2424

2525
-- add, WITH overflow: (6+3+5+15) % 16 = 29 % 16 = 13
2626
/-- info: 13 -/
2727
#guard_msgs in
28-
#eval (ArithCircuit.add [.var 0, .var 1, .var 2, .var 3] : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
28+
#eval (ArithCircuit.add [.var 0 4, .var 1 4, .var 2 4, .var 3 4] : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
2929

3030
-- mul, no overflow: (3*5) % 16 = 15 % 16 = 15
3131
/-- info: 15 -/
3232
#guard_msgs in
33-
#eval (ArithCircuit.mul (.var 1) (.var 2) : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
33+
#eval (ArithCircuit.mul (.var 1 4) (.var 2 4) : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
3434

3535
-- mul, WITH overflow: (5*15) % 16 = 75 % 16 = 11
3636
/-- info: 11 -/
3737
#guard_msgs in
38-
#eval (ArithCircuit.mul (.var 2) (.var 3) : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
38+
#eval (ArithCircuit.mul (.var 2 4) (.var 3 4) : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
3939

4040
-- (5*5) % 16 = 25 % 16 = 9
4141
/-- info: 9 -/
4242
#guard_msgs in
43-
#eval (ArithCircuit.mul (.var 2) (.var 2) : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
43+
#eval (ArithCircuit.mul (.var 2 4) (.var 2 4) : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
4444

4545
-- nesting: (6+3)*5 % 16 = 45 % 16 = 13
4646
/-- info: 13 -/
4747
#guard_msgs in
48-
#eval (ArithCircuit.mul (.add [.var 0, .var 1]) (.var 2) : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
48+
#eval (ArithCircuit.mul (.add [.var 0 4, .var 1 4]) (.var 2 4) : ArithCircuit 4).toBitHeap.evalMod (BitVecEnv.toBitEnv testEnv)
4949

5050
----------
5151

5252
/-- info: 13 -/
5353
#guard_msgs in
54-
#eval ((ArithCircuit.add [.var 0, .var 1, .var 2, .var 3] : ArithCircuit 4).toCircuitVector).eval (BitVecEnv.toBitEnv testEnv)
54+
#eval ((ArithCircuit.add [.var 0 4, .var 1 4, .var 2 4, .var 3 4] : ArithCircuit 4).toCircuitVector).eval (BitVecEnv.toBitEnv testEnv)
5555

5656
/-- info: 11 -/
5757
#guard_msgs in
58-
#eval ((ArithCircuit.mul (.var 2) (.var 3) : ArithCircuit 4).toCircuitVector).eval (BitVecEnv.toBitEnv testEnv)
58+
#eval ((ArithCircuit.mul (.var 2 4) (.var 3 4) : ArithCircuit 4).toCircuitVector).eval (BitVecEnv.toBitEnv testEnv)
5959

6060
/-- info: 9 -/
6161
#guard_msgs in
62-
#eval ((ArithCircuit.mul (.var 2) (.var 2) : ArithCircuit 4).toCircuitVector).eval (BitVecEnv.toBitEnv testEnv)
62+
#eval ((ArithCircuit.mul (.var 2 4) (.var 2 4) : ArithCircuit 4).toCircuitVector).eval (BitVecEnv.toBitEnv testEnv)
6363

6464
/-- info: 225 -/
6565
#guard_msgs in
66-
#eval ((ArithCircuit.var 3 : ArithCircuit 4).toBitHeap.mulBitHeap
67-
(ArithCircuit.var 3 : ArithCircuit 4).toBitHeap).eval (BitVecEnv.toBitEnv testEnv)
66+
#eval ((ArithCircuit.var 3 4 : ArithCircuit 4).toBitHeap.mulBitHeap
67+
(ArithCircuit.var 3 4 : ArithCircuit 4).toBitHeap).eval (BitVecEnv.toBitEnv testEnv)
6868

69-
#eval toString ((ArithCircuit.var 3 : ArithCircuit 4).toBitHeap.mulBitHeap
70-
(ArithCircuit.var 3 : ArithCircuit 4).toBitHeap)
69+
#eval toString ((ArithCircuit.var 3 4 : ArithCircuit 4).toBitHeap.mulBitHeap
70+
(ArithCircuit.var 3 4 : ArithCircuit 4).toBitHeap)
7171

7272
------
7373

7474
def compressed (c : ArithCircuit w) : BitHeap w := (DaddaTree.DaddaTree c.toBitHeap).1
7575

76-
def addThree : ArithCircuit 4 := .add [.var 0, .var 1, .var 2]
76+
def addThree : ArithCircuit 4 := .add [.var 0 4, .var 1 4, .var 2 4]
7777

78-
def mulTwo : ArithCircuit 4 := .mul (.var 0) (.var 1)
78+
def mulTwo : ArithCircuit 4 := .mul (.var 0 4) (.var 1 4)
7979

8080
/-- info: "{0 ↦ [b4, b8, b0], 1 ↦ [b1, b5, b9], 2 ↦ [b2, b10, b6], 3 ↦ [b3, b11, b7]}" -/
8181
#guard_msgs in
@@ -84,7 +84,7 @@ def mulTwo : ArithCircuit 4 := .mul (.var 0) (.var 1)
8484
/-- info: "{0 ↦ [(b4 ⊕ b8), b0], 1 ↦ [(b4 ∧ b8), ((b1 ⊕ b5) ⊕ b9)], 2 ↦ [(((b1 ∧ b5) ∨ (b1 ∧ b9)) ∨ (b5 ∧ b9)), ((b2 ⊕ b10) ⊕ b6)], 3 ↦ [(((b2 ∧ b10) ∨ (b2 ∧ b6)) ∨ (b10 ∧ b6)), ((b3 ⊕ b11) ⊕ b7)]}" -/
8585
#guard_msgs in
8686
#eval toString (compressed addThree)
87-
/-- info: "{0 ↦ [(b0 ∧ b4)], 1 ↦ [(b0 ∧ b5), (b1 ∧ b4)], 2 ↦ [((b1 ∧ b5) ⊕ (b2 ∧ b4)), (b0 ∧ b6)], 3 ↦ [((((b3 ∧ b4) ⊕ (b0 ∧ b7)) ⊕ (b2 ∧ b5)) ⊕ (b1 ∧ b6)), ((b1 ∧ b5) ∧ (b2 ∧ b4))]}"-/
87+
/-- info: "{0 ↦ [(b0 ∧ b4)], 1 ↦ [(b0 ∧ b5), (b1 ∧ b4)], 2 ↦ [((b1 ∧ b5) ⊕ (b2 ∧ b4)), (b0 ∧ b6)], 3 ↦ [((((b3 ∧ b4) ⊕ (b0 ∧ b7)) ⊕ (b2 ∧ b5)) ⊕ (b1 ∧ b6)), ((b1 ∧ b5) ∧ (b2 ∧ b4))]}" -/
8888
#guard_msgs in
8989
#eval toString (compressed mulTwo)
9090

@@ -96,13 +96,49 @@ def mulTwo : ArithCircuit 4 := .mul (.var 0) (.var 1)
9696
#guard_msgs in
9797
#eval toString (DaddaTree.DaddaTree mulTwo.toBitHeap).2
9898

99-
def fma : ArithCircuit 4 := .add [mulTwo, .var 2]
99+
def fma : ArithCircuit 4 := .add [mulTwo, .var 2 4]
100100

101101

102102
/-- info: 13 -/
103103
#guard_msgs in
104-
#eval (compressed (.add [.var 0, .var 1, .var 2, .var 3] : ArithCircuit 4)).eval (BitVecEnv.toBitEnv testEnv)
104+
#eval (compressed (.add [.var 0 4, .var 1 4, .var 2 4, .var 3 4] : ArithCircuit 4)).eval (BitVecEnv.toBitEnv testEnv)
105105

106106
/-- info: 11 -/
107107
#guard_msgs in
108-
#eval (compressed (.mul (.var 2) (.var 3) : ArithCircuit 4)).eval (BitVecEnv.toBitEnv testEnv)
108+
#eval (compressed (.mul (.var 2 4) (.var 3 4) : ArithCircuit 4)).eval (BitVecEnv.toBitEnv testEnv)
109+
110+
--- Zero-extension Tests
111+
112+
-- i3 -> i6 zero extension
113+
def mulZext : ArithCircuit 6 := .mul (.var 0 3) (.var 1 3)
114+
115+
/-- info: "{0 ↦ [(b0 ∧ b6)], 1 ↦ [(b0 ∧ b7), (b1 ∧ b6)], 2 ↦ [(b2 ∧ b6), (b1 ∧ b7), (b0 ∧ b8)], 3 ↦ [(b1 ∧ b8), (b2 ∧ b7)], 4 ↦ [(b2 ∧ b8)], 5 ↦ []}" -/
116+
#guard_msgs in
117+
#eval toString mulZext.toBitHeap
118+
119+
/-- info: "[HA(2: (b2 ∧ b6), (b1 ∧ b7)), HA(3: (b1 ∧ b8), (b2 ∧ b7))]" -/
120+
#guard_msgs in
121+
#eval toString (DaddaTree.DaddaTree mulZext.toBitHeap).2
122+
123+
def testEnv6 : BitVecEnv 6 := fun i =>
124+
match i with
125+
| 0 => 5#6
126+
| 1 => 7#6
127+
| _ => 0#6
128+
129+
/-- info: 35 -/
130+
#guard_msgs in
131+
#eval (compressed mulZext).eval (BitVecEnv.toBitEnv testEnv6)
132+
133+
def testEnv3 : BitVecEnv 3 := fun i =>
134+
match i with
135+
| 0 => 5#3
136+
| 1 => 7#3
137+
| _ => 0#3
138+
139+
def mulNoZext : ArithCircuit 3 := .mul (.var 0 3) (.var 1 3)
140+
141+
-- without extension we get the truncated result 3
142+
/-- info: 3 -/
143+
#guard_msgs in
144+
#eval (compressed mulNoZext).eval (BitVecEnv.toBitEnv testEnv3)

0 commit comments

Comments
 (0)