Two-phase SMT abstraction for symbolic division/modulo and multiplication - #1075

Open

gustavo-grieco wants to merge 157 commits into

mainfrom

arith-abstraction

Commits on Feb 17, 2026

proof of concept of of div-encoding

gustavo-grieco
authored and
msooseth
committed
038d31a
axioms

gustavo-grieco
authored and
msooseth
committed
536e063
avoid unsoundness

gustavo-grieco
authored and
msooseth
committed
0513779
fixes and tests

gustavo-grieco
authored and
msooseth
committed
b687ca8
fixes

gustavo-grieco
authored and
msooseth
committed
113a25a
Update src/EVM/SMT/DivEncoding.hs
msooseth
committed
f3e103e
fixes

gustavo-grieco
authored and
msooseth
committed
3d995ed
Remove warning
msooseth
committed
21cd753
Cleanup
msooseth
committed
e73af5a
Cleanup
msooseth
committed
45b71c5
Rename, lineup
msooseth
committed
8716a51
Fix code repetition
msooseth
committed
f4d7fdf
Cleanup
msooseth
committed
e60173a
Waaay cleaner setup
msooseth
committed
df399c6
Update cabal
msooseth
committed
81d2690
Less obvious comments
msooseth
committed
e03cd05
Cleanup
msooseth
committed
1c48980
Cleanup
msooseth
committed
1dad96c
Cleaner
msooseth
committed
c3112cd
Cleanup
msooseth
committed
40bd88c
Cleanup
msooseth
committed
d9c5089
Cleanup
msooseth
committed
d1f5333
Cleanup
msooseth
committed
d24dfdd
Cleanup
msooseth
committed
7554795
Update
msooseth
committed
ce537e1
Cleanup
msooseth
committed
d20beeb
Fixing
msooseth
committed
b07ee28
assertProps is now abst+axioms+refine
msooseth
committed
de82732
Update
msooseth
committed
3ad2715
Proper 2-phase
msooseth
committed
6816fc9
Cleanup
msooseth
committed
1f654ec
OK, now doing assertProps on its own as well
msooseth
committed
b20e92d
Better comments
msooseth
committed
51e93d1
No more exprToSMT
msooseth
committed
e65f984
Fixing testing
msooseth
committed
6a55da8
Cleanup
msooseth
committed
c7e543f
Cleanup
msooseth
committed
a9a86c8
Fixing
msooseth
committed
ae8fb7f
Cleanup
msooseth
committed
0e6403b
Less code
msooseth
committed
38eec42
I think this is better
msooseth
committed
8901ba6
Fixing
msooseth
committed
327fe28
Update
msooseth
committed
560dce3
Cleanup
msooseth
committed
36b9b05
Cleanup
msooseth
committed
fd796b0
Flush output buffer via traceM
msooseth
committed
4ef42ae
Making more progress
msooseth
committed
d6ed757
Rename
msooseth
committed
ce1bd7a
Cleaner code
msooseth
committed
2d72720
OK, let's try this?
msooseth
committed
0e25ff9
Remove nonsense comment
msooseth
committed
de03abf
Moving code lower
msooseth
committed
7a42090
Cleanup
msooseth
committed
96e0980
None of this 1-K stuff, also correct Cex handing on 3rd phase
msooseth
committed
cb15623
Maybe cleaner
msooseth
committed
3cb47e0
Rename
msooseth
committed
a2bf7f1
Better naming
msooseth
committed
52edee6
More cleanup
msooseth
committed
cd5333f
More cleanup
msooseth
committed
d9ac366
Cleanup
msooseth
committed
0b0d161
Better printing
msooseth
committed
e0abb57
Cleaner
msooseth
committed
bf5e111
Cleanup
msooseth
committed
c38dcbf
Cleaning up comments
msooseth
committed
ca534eb
Cleaner
msooseth
committed
ec81d15
Fix spacing
msooseth
committed
bb54f86
Even cleaner
msooseth
committed
4c82008
Update
msooseth
committed
15038e8
Cleanup
msooseth
committed
29acc17
Moving functions, sorry!
msooseth
committed
c68cd6e
Cleanupo
msooseth
committed
5fbf561
Better naming
msooseth
committed
114b4ce
Better naming
msooseth
committed
1f350e5
Adding div/mod bounds
msooseth
committed
e73cfc6
More
msooseth
committed
7b54eb4
Cleanup
msooseth
committed
3b180b9
Better comments
msooseth
committed
73c1d9a
Update
msooseth
committed
7c093e4
Cleanup
msooseth
committed
7c88e62
Cleanup
msooseth
committed
d057c91
Cleanup
msooseth
committed
6072b47
Cleanup
msooseth
committed
85dc0b4
Fixing
msooseth
committed
c1ac1ce
Update
msooseth
committed
7447f0d
Cleanup
msooseth
committed
66f14aa
Now without divmod
msooseth
committed
4d775f3
Even less
msooseth
committed
b40f875
Cleanup
msooseth
committed
94d98a8
Cleanup
msooseth
committed
2d4d344
Cleanup
msooseth
committed
9476412
Update
msooseth
committed
d0ef06b
Better
msooseth
committed
b2b8b4f
Better printing
msooseth
committed
359f5dc
Move
msooseth
committed
4de3a17
Update
msooseth
committed
d5d2659
Update tests
msooseth
committed
05198eb
Cleanup
msooseth
committed
0002c69
Adding tests
msooseth
committed
d7bdb55
Cleanup
msooseth
committed
36221ec
Fix dumping
msooseth
committed
0aebdfb
Fix dumping
msooseth
committed
936280b

Commits on Feb 18, 2026

Better
msooseth
committed
8bef599
Update
msooseth
committed
706952e
Better
msooseth
committed
a0baa04
Update
msooseth
committed
ba22aac
Update naming
msooseth
committed
81c766a
Cleanup
msooseth
committed
48bc777
Cleanup
msooseth
committed
2426e88
Fixing warning
msooseth
committed
bf156b3
Rename
msooseth
committed
2763078
Fix name of file
msooseth
committed
49296dd
Fixing cabal
msooseth
committed
503d110
No need for this
msooseth
committed
251aef0
Fixing up cli test
msooseth
committed
c95d5f8
No need for these printings
msooseth
committed
0fb590c
Fixing this test
msooseth
committed
a4ef47e
Rename
msooseth
committed
92df580
Fixing val
msooseth
committed
13ad8de
Named correctly
msooseth
committed
898fca9
Fixing naming
msooseth
committed
1d63c63
Renaming
msooseth
committed
4e06446
Update name
msooseth
committed
f3213dd
Update
msooseth
committed
f087d98
Adding test, ifxing import, fixing printing
msooseth
committed
0ab6fb4
Adding the tests
msooseth
committed
1304d32
Cleaner
msooseth
committed
fcb8645
Cleanup
msooseth
committed
1838ea7

Commits on Apr 6, 2026

import fix
gustavo-grieco
committed
cf21972
Merge remote-tracking branch 'origin/main' into poc-div-encoding
gustavo-grieco
committed
5d5cfe0
more fixes
gustavo-grieco
committed
7aaefd0
ignore math-mint-fail test
gustavo-grieco
committed
4b18b03

Commits on Apr 30, 2026

Merge branch 'main' into poc-div-encoding
gustavo-grieco
authored
7f991f6

Commits on Jun 17, 2026

Merge remote-tracking branch 'origin/main' into poc-div-encoding
gustavo-grieco
committed
63b6538
solvers: empty solver returns clean 'Result unknown by SMT solver'

gustavo-grieco
and
claude
committed
b162bfa
Abstract unsigned div/mod (bvudiv/bvurem) in two-phase SMT

gustavo-grieco
and
claude
committed
60ccd59
Merge remote-tracking branch 'origin/main' into poc-div-encoding
gustavo-grieco
committed
1eac9d3
PoC: abstract symbolic multiplication (abst_evm_bvmul) with sound lemmas

gustavo-grieco
and
claude
committed
fd944a4
Add two sound lemmas: divisor-monotonicity and mulDiv bound

gustavo-grieco
and
claude
committed
09ff923
Fix operand-order sensitivity in mul-monotonicity lemma

gustavo-grieco
and
claude
committed
d01b269
Make no-overflow guard cheap and add const-mul monotonicity

gustavo-grieco
and
claude
committed
720a00e
Synthesize cancellation divisions to prove cross-divisor round-trips

gustavo-grieco
and
claude
committed
9ae3456
Use z3 for the two harder Mul-Abstraction proofs

gustavo-grieco
and
claude
committed
4c702b9

Commits on Jun 18, 2026

Use bitwuzla for the round-trip/const-mul tests; add checked-real-code round-trip

gustavo-grieco
and
claude
committed
e9d6496
Keep the PoC abstract: drop domain-specific references and a redundant test

gustavo-grieco
and
claude
committed
2ed340e
Add const-cancellation lemma: (c*x)/c == x for literal c

gustavo-grieco
and
claude
committed
e46f281
Generalize const-cancel and add nested-division collapse

gustavo-grieco
and
claude
committed
368d771
Add fraction-reduce lemma: (c1*x)/c2 == x/(c2/c1) for c1 | c2

gustavo-grieco
and
claude
committed
41969b4
Add ceilDiv-cancel lemma: ceilDiv(c1*x, c2) == (c1/c2)*x for c2 | c1

gustavo-grieco
and
claude
committed
46bcd0d

Commits on Jun 19, 2026

Add scaled-product telescoping lemma; collapse nested divides into the div set

gustavo-grieco
and
claude
committed
64c9640

Commits on Jun 22, 2026

Refactor div/mod abstraction into a dedicated lemma catalogue

gustavo-grieco
and
claude
committed
50cd32f
Add uint256 abstract mul regression
gustavo-grieco
committed
81a6588

Commits on Jun 24, 2026

reduced code
gustavo-grieco
committed
d5ae200
reduced code
gustavo-grieco
committed
6349a3a

Commits on Jul 20, 2026

smt: dedupe builder helpers into SMT.SMTLIB, trim abstraction comments

gustavo-grieco
and
claude
committed
cec6e38
Merge origin/main into arith-abstraction

gustavo-grieco
and
claude
committed
b3db09a

Commits on Jul 21, 2026

Merge remote-tracking branch 'origin/main' into arith-abstraction
gustavo-grieco
committed
52c9f66

Commits on Aug 11, 2026

Merge branch 'main' into arith-abstraction
gustavo-grieco
authored
06b5bf4