Formally verified `mulExpRay` - #599

Open

duncancmt wants to merge 122 commits into

Commits on Apr 15, 2026

Fix unsafe bool handling at Solidity/Yul assembly boundaries

duncancmt
and
claude
committed
8790bef
Fix bool cleanliness at Yul boundaries
duncancmt
committed
edb5e6b
Optimize bool truthiness at Yul boundaries
duncancmt
committed
6ae0786
Fix additional bool cleanup sites missed in first pass

duncancmt
and
claude
committed
632ee47
Simplify strict bool decoder assembly
duncancmt
committed
a27a056
Improve FastLogic and fix CrossChainReceiverFactory bool cleanup

duncancmt
and
claude
committed
2f4e4a0
Add comments to FastLogic explaining dirty-bool handling

duncancmt
and
claude
committed
fd8946f
Merge branches claude/bool and codex/bool
duncancmt
committed
5e1a2bd
Cleaning up slop
duncancmt
committed
ba92d74
Stack-too-deep
duncancmt
committed
cdf522f
Stack-too-deep
duncancmt
committed
936ebc5
Cleaning up slop
duncancmt
committed
008ca48
Cleaning up slop
duncancmt
committed
cfc6a2e
Cleaning up slop
duncancmt
committed
6551562
Cleaning up slop
duncancmt
committed
7eb275d
Reduce stack pressure
duncancmt
committed
058e62c

Commits on Apr 16, 2026

Fix CI
duncancmt
committed
6f22edc
`forge fmt`
duncancmt
committed
41e5a5b

Commits on May 18, 2026

Bug! `calls[i].target` may alias `calls[j].data`, resulting in malleability. Make 2 passes over `calls[]` to fix this.
duncancmt
committed
600c2e8

Commits on May 19, 2026

WIP: RobinHood chain
duncancmt
committed
b2ad52c
WIP: RobinHood chain
duncancmt
committed
1a4609c
WIP: RobinHood chain -- add WETH address
duncancmt
committed
34b4cd6

Commits on May 21, 2026

WIP: RobinHood chain -- add to SafeConfig.sol
duncancmt
committed
f43837c
WIP: RobinHood chain -- test for hardfork support
duncancmt
committed
d3c0322

Commits on May 26, 2026

WIP: RobinHood chain -- deploy MultiCall and CrossChainReceiverFactory
duncancmt
committed
b1f8687

Commits on May 27, 2026

WIP: RobinHood chain -- deploy AllowanceHolder
duncancmt
committed
3cac7fb
WIP: RobinHood chain -- compilation errors
duncancmt
committed
b0de7d2
Finished: deploy Settler to RobinHood chain
duncancmt
committed
84349ec

Commits on Jun 5, 2026

Add STS URL for RobinHood Chain
duncancmt
committed
7377478
Put chainid back in initcode for RobinHood Chain
duncancmt
committed
492c9c7

Commits on Jun 8, 2026

Add UniswapV3 and UniswapV4 support on RobinHood chain
duncancmt
committed
8da090e
Merge branch 'master' into dcmt/robinhood-chain
duncancmt
committed
6e7b0ae
`CHANGELOG.md`
duncancmt
committed
db2420d

Commits on Jun 12, 2026

Merge branch 'master' into dcmt/bool
duncancmt
committed
5362a61
Resolve Uniswap V3 unit test conflict

duncancmt
and
codex
committed
d08627c
Use iszero masks for ternary swaps

duncancmt
and
codex
committed
fd8aab3
Clean up slop
duncancmt
committed
b153a5a

Commits on Jun 19, 2026

Clean up useless/failing tests
duncancmt
committed
ec99760
Use `_mockExpectCall` instead of an explicit mock contract
duncancmt
committed
fbb0526
Fix too-lax test
duncancmt
committed
55ff3b8
Rename `fastUniswapV2Pool` => `FastUniswapV2Pool`
duncancmt
committed
306bc60
Remove unused `_HAS_WNATIVE`
duncancmt
committed
aa85e50
Relax `isForwarded` masking in `UniswapV3Fork` to canonicalization
duncancmt
committed
3e4a7a1
Merge branch 'master' into dcmt/bool
duncancmt
committed
600794a
Address bool boundary review feedback

duncancmt
and
codex
committed
2ab0f81
Test dirty UniswapV3 swap direction encoding

duncancmt
and
codex
committed
528e5ed
Fix mock DAI permit domain separator

duncancmt
and
codex
committed
b156ec5
Add directions for agents around commenting and code archaeology
duncancmt
committed
c138946
Require that AI agents add a `Co-Authored-By:` to each commit message
duncancmt
committed
803fe15
More AGENTS.md instructions for coauthorship
duncancmt
committed
0fe01eb
Fix UniV3 forwarded flag decoding

duncancmt
and
codex
committed
66585e3
Regenerate integration gas snapshots

duncancmt
and
codex
committed
b260967

Commits on Jun 26, 2026

Add EkuboV3 actions on RobinHood chain
duncancmt
committed
6265835
Formatting
duncancmt
committed
3c22d9c

Commits on Jun 30, 2026

Commits on Jul 8, 2026

Commits on Jul 9, 2026

Add scaled exp ray multiplication

duncancmt
and
codex
committed
469bccf
Repair exp proof seam for shared kernel

duncancmt
and
codex
committed
f9a160f
Add mulExpRay proof pipeline

duncancmt
and
codex
committed
9bc035c
Document mulExpRay monotonicity specs

duncancmt
and
codex
committed
79b0eda
Extend mulExpRay proof pipeline

duncancmt
and
codex
committed
2ea4a57
Expose mulExpRay guard tree

duncancmt
and
codex
committed
09680ec
Inline single-use mulExpRay helpers

duncancmt
and
codex
committed
012afb4
Repair exp proof after mulExpRay inlining

duncancmt
and
codex
committed
badf6a0
Add mulExpRay seam word rewrites

duncancmt
and
codex
committed
9807053
Tighten the mulExpRay guard and fold the zero multiplier

duncancmt
and
claude
committed
a346ffa
Rebuild the mulExpRay proof seam on the shared guard

committed
a2944fa
Document why mulExpRay is monotone in the multiplier

duncancmt
and
claude
committed
8c217ce
Prove the mulExpRay runtime surface on its exact domains

committed
3b893a1

Commits on Jul 10, 2026

Widen the exp reduction anchors to the mulExpRay region

duncancmt
and
claude
committed
1493ac2
Carry the exp per-point brackets on the wide region

duncancmt
and
claude
committed
49721f2
Generalize the exp per-point brackets to a symbolic scale

duncancmt
and
claude
committed
9760880
Prove the mulExpRay bracket on the whole value domain

duncancmt
and
claude
committed
7c38e40
Prove mulExpRay monotone in the exponent on the value domain

duncancmt
and
claude
committed
c69c85e
Prove mulExpRay monotone in the multiplier on the value domain

duncancmt
and
claude
committed
5c9c95c
Prove mulExpRay joint monotonicity and complete the natspec signpost

duncancmt
and
claude
committed
04a8331
Document the tactic discipline over the runtime trees

duncancmt
and
claude
committed
eeef5a5
Raise the mulExpRay scale cap to the certified ceiling and pare the guard

duncancmt
and
claude
committed
ee55235
Strengthen agent decision discipline

duncancmt
and
codex
committed
ea11fdd
Add extensible polynomial certificate backends

duncancmt
and
codex
committed
2b35f9a
Add Exp polynomial certificate portfolio

duncancmt
and
codex
committed
20bae78
Use shared polynomial certificates in Ln proofs

duncancmt
and
codex
committed
87e063f
Gate shared certificate soundness axioms

duncancmt
and
codex
committed
ca3562f

Commits on Jul 12, 2026

Certify mulExpRay through 127-bit magnitudes

duncancmt
and
codex
committed
731f34d
Generate contiguous Ln certificate lanes

duncancmt
and
codex
committed
fcd8c94
Unify selective formal proof CI

duncancmt
and
codex
committed
040ae80
Narrow mulExpRay multiplier to int128

duncancmt
and
codex
committed
2b89728

Commits on Jul 13, 2026

Narrow Exp return values to int128

duncancmt
and
codex
committed
7c82ba6
Support int128 minimum in mulExpRay

duncancmt
and
codex
committed
c274118
Inline single-use Exp constants

duncancmt
and
codex
committed
2b2bcae
WIP: clean up AI comments
duncancmt
committed
7a3b33c
WIP: clean up AI comments
duncancmt
committed
be882e8
WIP: clean up AI comments
duncancmt
committed
0c65c4a
WIP: clean up AI comments
duncancmt
committed
ab97735
Tighten Ln downward margin

duncancmt
and
codex
committed
e9bd7aa

Commits on Jul 14, 2026

Add Up UniV3 fork to RobinHood (fork ID 40)
claude
committed
42858c2
WIP: clean up AI comments
duncancmt
committed
b9d8986
WIP: clean up AI comments
duncancmt
committed
9807c96
Finished: clean up AI comments
duncancmt
committed
c3eca02
Merge branch 'dcmt/bool'
duncancmt
committed
c09109b
Fix Exp proof and formal dependency caching

duncancmt
and
codex
committed
df10d57
Merge branch 'dcmt/up-fork'
duncancmt
committed
86b80ca
Add Sheriff (Algebra-like) UniV3 fork to RobinHood with fork ID 41
claude
committed
f698f59
Merge branch 'dcmt/sheriff-fork'
duncancmt
committed
cf1fe3e
fix: changelog support for Across on Monad entry
e1Ru1o
committed
d35d155
Merge branch 'e1Ru1o/changelog-typo'
duncancmt
committed
60e2140
Simplify
duncancmt
committed
cbd2c53
Typo
duncancmt
committed
0b8267c
Merge branch 'master' into dcmt/mul-exp
duncancmt
committed
4db6186

Commits on Jul 15, 2026

Certify tighter Ln approximation margin

duncancmt
and
codex
committed
116b3da
DRY
duncancmt
committed
e856969
Merge mulExp and formal proof updates

duncancmt
and
codex
committed
e3ab9f3
Comment
duncancmt
committed
3099e34
Clean up CI runtime warnings

duncancmt
and
codex
committed
987951a

Commits on Jul 17, 2026

Reword mulExpRay revert docs around a single acceptance rule

duncancmt
and
claude
committed
54341cd

Commits on Jul 23, 2026

Size golf
duncancmt
committed
4d6060d
Track the xor-based headroom bias in the exp proof

duncancmt
and
claude
committed
ea7f972