Skip to content

Commit 37b15a6

Browse files
feggefegge
committed
Cleaned up correctness proofs for U128 divmod, div, and mod
1 parent 3352477 commit 37b15a6

File tree

5 files changed

+2785
-213
lines changed

5 files changed

+2785
-213
lines changed

‎MidenLean.lean‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ import MidenLean.Proofs.Tactics
1313
import MidenLean.Proofs.U32.Common
1414
import MidenLean.Proofs.U64.Common
1515
import MidenLean.Proofs.U64.Eq
16-
import MidenLean.Proofs.U64.Sub
16+
import MidenLean.Proofs.U64.WrappingSub
1717
import MidenLean.Proofs.U64.OverflowingSub
1818
import MidenLean.Proofs.U64.Lt
1919
import MidenLean.Proofs.U64.Gt
@@ -46,6 +46,8 @@ import MidenLean.Proofs.U128.Clo
4646
import MidenLean.Proofs.U128.Clz
4747
import MidenLean.Proofs.U128.Cto
4848
import MidenLean.Proofs.U128.Ctz
49+
import MidenLean.Proofs.U128.Div
50+
import MidenLean.Proofs.U128.Divmod
4951
import MidenLean.Proofs.U128.Eq
5052
import MidenLean.Proofs.U128.Eqz
5153
import MidenLean.Proofs.U128.Gt
@@ -54,6 +56,7 @@ import MidenLean.Proofs.U128.Lt
5456
import MidenLean.Proofs.U128.Lte
5557
import MidenLean.Proofs.U128.Max
5658
import MidenLean.Proofs.U128.Min
59+
import MidenLean.Proofs.U128.Mod
5760
import MidenLean.Proofs.U128.Not
5861
import MidenLean.Proofs.U128.Neq
5962
import MidenLean.Proofs.U128.Or

‎MidenLean/Proofs/U128/Div.lean‎

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,107 @@
1+
import MidenLean.Proofs.U128.Common
2+
import MidenLean.Proofs.U128.Divmod
3+
import MidenLean.Proofs.Tactics
4+
import MidenLean.Generated.U128
5+
6+
namespace MidenLean.Proofs
7+
8+
open MidenLean
9+
open MidenLean.StepLemmas
10+
open MidenLean.Tactics
11+
12+
set_option maxHeartbeats 12000000 in
13+
set_option maxRecDepth 65536 in
14+
private theorem divmod_execWithEnv_eq_exec (fuel : Nat) (s : MidenState)
15+
(hf : 0 < fuel) :
16+
execWithEnv u128ProcEnv fuel s Miden.Core.U128.divmod =
17+
exec 163 s Miden.Core.U128.divmod := by
18+
cases fuel with
19+
| zero => cases hf
20+
| succ fuel' =>
21+
simp (maxSteps := 5000000) [exec, execWithEnv, u128ProcEnv, Miden.Core.U128.divmod]
22+
23+
set_option maxHeartbeats 12000000 in
24+
/-- `u128::div` verifies an advice-supplied quotient and remainder for u128 division,
25+
then drops the remainder word and returns the quotient limbs.
26+
Execution succeeds iff the advice-supplied q and r satisfy q * b + r = a and r < b.
27+
Input stack: [b.a0, b.a1, b.a2, b.a3, a.a0, a.a1, a.a2, a.a3] ++ rest
28+
Advice stack: [r.a0, r.a1, r.a2, r.a3, q.a0, q.a1, q.a2, q.a3] ++ adv_rest
29+
Output stack: [q.a0, q.a1, q.a2, q.a3] ++ rest -/
30+
theorem u128_div_correct
31+
(a b q r : U128) (rest adv_rest : List Felt) (s : MidenState)
32+
(hs : s.stack = b.a0.val :: b.a1.val :: b.a2.val :: b.a3.val ::
33+
a.a0.val :: a.a1.val :: a.a2.val :: a.a3.val :: rest)
34+
(hadv : s.advice = r.a0.val :: r.a1.val :: r.a2.val :: r.a3.val ::
35+
q.a0.val :: q.a1.val :: q.a2.val :: q.a3.val :: adv_rest) :
36+
execWithEnv u128ProcEnv 31 s Miden.Core.U128.div =
37+
some { stack := q.a0.val :: q.a1.val :: q.a2.val :: q.a3.val :: rest,
38+
memory := s.memory,
39+
locals := s.locals,
40+
advice := adv_rest }
41+
↔ (q.toNat * b.toNat + r.toNat = a.toNat ∧ r.toNat < b.toNat) := by
42+
obtain ⟨stk, mem, locs, adv⟩ := s
43+
simp only [] at hs hadv
44+
subst hs
45+
subst hadv
46+
constructor
47+
· intro hexec
48+
unfold Miden.Core.U128.div execWithEnv at hexec
49+
simp only [List.foldlM, u128ProcEnv] at hexec
50+
revert hexec
51+
cases h_dm : execWithEnv u128ProcEnv 30
52+
{ stack := b.a0.val :: b.a1.val :: b.a2.val :: b.a3.val ::
53+
a.a0.val :: a.a1.val :: a.a2.val :: a.a3.val :: rest,
54+
memory := mem,
55+
locals := locs,
56+
advice := r.a0.val :: r.a1.val :: r.a2.val :: r.a3.val ::
57+
q.a0.val :: q.a1.val :: q.a2.val :: q.a3.val :: adv_rest }
58+
Miden.Core.U128.divmod with
59+
| none =>
60+
simp [bind, Bind.bind, Option.bind]
61+
| some val =>
62+
intro _
63+
have h_dm_exec :
64+
exec 163
65+
{ stack := b.a0.val :: b.a1.val :: b.a2.val :: b.a3.val ::
66+
a.a0.val :: a.a1.val :: a.a2.val :: a.a3.val :: rest,
67+
memory := mem,
68+
locals := locs,
69+
advice := r.a0.val :: r.a1.val :: r.a2.val :: r.a3.val ::
70+
q.a0.val :: q.a1.val :: q.a2.val :: q.a3.val :: adv_rest }
71+
Miden.Core.U128.divmod = some val := by
72+
rw [← divmod_execWithEnv_eq_exec 30 _ (by decide)]
73+
exact h_dm
74+
exact u128_divmod_conditions_of_exec a b q r rest adv_rest _ rfl rfl h_dm_exec
75+
· intro ⟨hdiv, hlt⟩
76+
have h_divmod :
77+
exec 163
78+
{ stack := b.a0.val :: b.a1.val :: b.a2.val :: b.a3.val ::
79+
a.a0.val :: a.a1.val :: a.a2.val :: a.a3.val :: rest,
80+
memory := mem,
81+
locals := locs,
82+
advice := r.a0.val :: r.a1.val :: r.a2.val :: r.a3.val ::
83+
q.a0.val :: q.a1.val :: q.a2.val :: q.a3.val :: adv_rest }
84+
Miden.Core.U128.divmod =
85+
some { stack := r.a0.val :: r.a1.val :: r.a2.val :: r.a3.val ::
86+
q.a0.val :: q.a1.val :: q.a2.val :: q.a3.val :: rest,
87+
memory := mem,
88+
locals := locs,
89+
advice := adv_rest } :=
90+
(u128_divmod_correct a b q r rest adv_rest
91+
{ stack := b.a0.val :: b.a1.val :: b.a2.val :: b.a3.val ::
92+
a.a0.val :: a.a1.val :: a.a2.val :: a.a3.val :: rest,
93+
memory := mem,
94+
locals := locs,
95+
advice := r.a0.val :: r.a1.val :: r.a2.val :: r.a3.val ::
96+
q.a0.val :: q.a1.val :: q.a2.val :: q.a3.val :: adv_rest }
97+
rfl rfl).mpr ⟨hdiv, hlt⟩
98+
unfold Miden.Core.U128.div execWithEnv
99+
simp only [List.foldlM, u128ProcEnv]
100+
dsimp only [bind, Bind.bind, Option.bind]
101+
rw [divmod_execWithEnv_eq_exec 30 _ (by decide)]
102+
rw [h_divmod]
103+
miden_bind
104+
rw [stepDropw]
105+
rfl
106+
107+
end MidenLean.Proofs

0 commit comments

Comments
 (0)