[PoC] Abstract symbolic multiplication (abst_evm_bvmul) for vault-style verification - #1073

Closed

gustavo-grieco wants to merge 14 commits into

poc-div-encodingfrom

poc-mul-abstraction

Commits on Jun 17, 2026

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