Skip to content

Commit ad9d7d4

Browse files
osmanyasar05osmanyasar05
committed
add proof
1 parent 8eff281 commit ad9d7d4

3 files changed

Lines changed: 136 additions & 8 deletions

File tree

‎DatapathVerification/BitHeap/BVComb.lean‎

Lines changed: 113 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -87,6 +87,108 @@ theorem bitheapOfVar_go (i : Nat) (bv : BitVecEnv w) (k : Nat) (hk : k ≤ w) :
8787
rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil]
8888
sorry
8989

90+
theorem foldl_addBit_evalMod (idx : Nat) (h : BitHeap w) (cs : List Circuit) :
91+
(List.foldl (fun a c => addBit idx c a) h cs).evalMod env
92+
= (h.evalMod env + (cs.map (fun c => 2^idx * (c.eval env).toInt)).sum) % 2^w := by
93+
induction cs generalizing h with
94+
| nil =>
95+
simp [evalMod]
96+
| cons c tl ih =>
97+
simp only [List.foldl_cons, List.map_cons, List.sum_cons, ih, BitHeap.evalMod_heap_addBit, Int.emod_add_emod]
98+
grind
99+
100+
theorem foldl_columns_evalMod (acc : BitHeap w) (ps : List (Column × Nat)) :
101+
(ps.foldl (fun a p => List.foldl (fun a' c => addBit p.2 c a') a p.1.elems.toList)
102+
acc).evalMod env
103+
= (acc.evalMod env
104+
+ (ps.map (fun p =>
105+
(p.1.elems.toList.map (fun c => 2^p.2 * (c.eval env).toInt)).sum)).sum) % 2^w := by
106+
induction ps generalizing acc with
107+
| nil =>
108+
simp [evalMod]
109+
| cons p tl ih =>
110+
simp only [List.foldl_cons, List.map_cons, List.sum_cons]
111+
rw [ih, foldl_addBit_evalMod, Int.emod_add_emod]
112+
grind
113+
114+
theorem hornersMethod_eq_sum_zipIdx (env : Circuit.BitEnv) (l : List Column) (s : Nat) :
115+
(2^s : Int) * (HornersMethod env l : Int)
116+
= ((l.zipIdx s).map (fun p =>
117+
(p.1.elems.toList.map (fun c => 2^p.2 * (c.eval env).toInt)).sum)).sum := by
118+
induction l generalizing s with
119+
| nil =>
120+
simp [HornersMethod]
121+
| cons p ps ih =>
122+
simp [HornersMethod, List.zipIdx_cons, List.map_cons, List.sum_cons]
123+
rw [← ih]
124+
rw [Int.mul_add]
125+
have : 2 ^ s * (2 * ↑(HornersMethod env ps)) = 2 ^ (s + 1) * (HornersMethod env ps) := by
126+
grind
127+
norm_cast
128+
simp [this, Column.eval_eq_sum]
129+
induction p.elems.toList with
130+
| nil =>
131+
simp
132+
| cons c tl ih' =>
133+
simp only [List.map_cons, List.sum_cons]
134+
grind
135+
136+
theorem eval_eq_sum_columns (h : BitHeap w) (env : Circuit.BitEnv) :
137+
((h.eval env : Int))
138+
= (h.columns.toList.zipIdx.map (fun p =>
139+
(p.1.elems.toList.map (fun c => 2^p.2 * (c.eval env).toInt)).sum)).sum := by
140+
simp [eval]
141+
have h0 := hornersMethod_eq_sum_zipIdx env h.columns.toList 0
142+
simp only [pow_zero, one_mul] at h0
143+
exact h0
144+
145+
theorem mergeInto_evalMod(acc h : BitHeap w) :
146+
(mergeInto acc h).evalMod env = (acc.evalMod env + h.evalMod env) % 2^w := by
147+
simp [mergeInto]
148+
rw [Vector.foldl, ←Array.foldl_toList]
149+
rw [foldl_columns_evalMod]
150+
simp only [evalMod, Vector.toArray_zipIdx, Array.toList_zipIdx, Int.emod_add_emod,
151+
Int.add_emod_emod]
152+
rw [eval_eq_sum_columns, eval_eq_sum_columns]
153+
grind
154+
155+
theorem foldl_mergeInto_evalMod (hs : List (BitHeap w)) (acc : BitHeap w) :
156+
(hs.foldl mergeInto acc).evalMod env
157+
= (acc.evalMod env + (hs.map (·.evalMod env)).sum) % 2^w := by
158+
induction hs generalizing acc with
159+
| nil =>
160+
simp only [evalMod, List.foldl_nil, List.map_nil, List.sum_nil, add_zero, dvd_refl,
161+
Int.emod_emod_of_dvd]
162+
| cons h tl ih =>
163+
simp only [List.foldl_cons, List.map_cons, List.sum_cons]
164+
rw [ih]
165+
rw [mergeInto_evalMod]
166+
simp
167+
grind
168+
169+
theorem foldl_add_init {w : ℕ} (acc hd : BitVec w) (tl : List (BitVec w)) :
170+
List.foldl (· + ·) (acc + hd) tl = List.foldl (· + ·) acc tl + hd := by
171+
induction tl generalizing acc with
172+
| nil => rfl
173+
| cons x xs ih =>
174+
simp only [List.foldl_cons]
175+
rw [← ih]
176+
grind
177+
178+
theorem foldl_add_toNat_go (acc : BitVec w) (l : List (BitVec w)) :
179+
((l.foldl (· + ·) acc).toNat : Int)
180+
= ((acc.toNat : Int) + (l.map (fun x => (x.toNat : Int))).sum) % 2^w := by
181+
induction l with
182+
| nil =>
183+
simp only [List.foldl_nil, List.map_nil, List.sum_nil, add_zero]
184+
norm_cast
185+
simp only [BitVec.toNat_mod_cancel]
186+
| cons hd tl ih =>
187+
simp only [List.foldl_cons, List.map_cons, List.sum_cons]
188+
rw [foldl_add_init]
189+
rw [BitVec.toNat_add]
190+
simp [ih]
191+
grind
90192

91193
theorem toBitHeap_correct (c : ArithCircuit w) (bv : BitVecEnv w) :
92194
c.toBitHeap.evalMod bv.toBitEnv = ((c.denote bv).toNat : Int):= by
@@ -97,9 +199,17 @@ theorem toBitHeap_correct (c : ArithCircuit w) (bv : BitVecEnv w) :
97199
simp [denote]
98200
norm_cast
99201
rw [BitVec.toNat_mod_cancel]
100-
| case2 =>
101-
sorry
102-
| case3 =>
202+
| case2 args ih =>
203+
simp only [denote, BitHeap.addBitHeap]
204+
rw [foldl_mergeInto_evalMod]
205+
rw [foldl_add_toNat_go]
206+
simp only [empty_evalMod, List.map_map, zero_add, BitVec.ofNat_eq_ofNat, BitVec.toNat_ofNat,
207+
Nat.zero_mod, Int.cast_ofNat_Int]
208+
congr 1
209+
congr 1
210+
simp only [List.map_inj_left, Function.comp_apply]
211+
assumption
212+
| case3 l r ih1 ih2=>
103213
sorry
104214

105215
end ArithCircuit

‎DatapathVerification/BitHeap/BitHeap.lean‎

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,10 @@ Evaluate a bit-heap modulo 2^width, to compute the final sum of all the bits in
6868
def evalMod (h : BitHeap w) (env : BitEnv) : Int :=
6969
h.eval env % 2^(w)
7070

71+
@[simp]
72+
theorem empty_evalMod (env : BitEnv) : (empty w).evalMod env = 0 := by
73+
simp [evalMod, empty_eval]
74+
7175
def get (h : BitHeap w) (column : Nat) : Column :=
7276
h.columns.getD column (Column.empty)
7377

@@ -126,11 +130,12 @@ theorem evalMod_truncate (h : BitHeap w) (n : Nat) (hn : n ≤ w) (env : BitEnv)
126130
simp [evalMod, eval, truncate]
127131
sorry
128132

129-
def addBitHeap (bhs : List (BitHeap w)) : BitHeap w:=
130-
let h := BitHeap.empty w
131-
let h := bhs.foldl (fun acc heap => heap.columns.zipIdx.foldl (fun acc' (column, index) =>
132-
column.elems.toList.foldl (fun acc' c => acc'.addBit index c) acc') acc) h
133-
h
133+
def mergeInto (acc h : BitHeap w) : BitHeap w :=
134+
h.columns.zipIdx.foldl (fun acc' (col, idx) =>
135+
col.elems.toList.foldl (fun a c => a.addBit idx c) acc') acc
136+
137+
def addBitHeap (bhs : List (BitHeap w)) : BitHeap w :=
138+
bhs.foldl mergeInto (BitHeap.empty w)
134139

135140
def mulBitHeap (h0 h1 : BitHeap w) : BitHeap (2 * w - 1) :=
136141
let h := BitHeap.empty (2 * w - 1)

‎DatapathVerification/BitHeap/Column.lean‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -67,6 +67,19 @@ theorem foldl_sum (l : List Circuit) (env : BitEnv) (a : Nat) :
6767
| cons p ps ih =>
6868
grind
6969

70+
theorem eval_eq_sum (col : Column) (env : Circuit.BitEnv) :
71+
((col.eval env : Int)) = (col.elems.toList.map (fun c => (c.eval env).toInt)).sum := by
72+
simp [eval]
73+
rw [Std.HashSet.fold_eq_foldl_toList, foldl_sum, Nat.zero_add]
74+
have hpt : ∀ b : Bool, ((b.toNat : Int)) = b.toInt := by
75+
intro b; cases b <;> rfl
76+
induction col.elems.toList with
77+
| nil => simp
78+
| cons p ps ih =>
79+
simp only [List.map_cons, List.sum_cons]
80+
push_cast
81+
rw [ih, hpt]
82+
7083
@[simp]
7184
theorem eval_erase (col : Column) (c : Circuit) (env : BitEnv) (h : c ∈ col) :
7285
(col.erase c).eval env = col.eval env - (c.eval env).toNat := by

0 commit comments

Comments
 (0)