[Certora] OfferTree Soundness - #816

Merged

QGarchery merged 167 commits into

mainfrom

certora/offer-tree

Sep 21, 2026

Commits on Jun 1, 2026

Commits on Jun 2, 2026

removed assumptions from soundness rule
bhargavbh
committed
9d0635b
tuned
bhargavbh
committed
4a3f121
tuned; retained market-level hashLeaf
bhargavbh
committed
5dec124
cleanup ratification spec
bhargavbh
committed
956a11f
varibale renaming in create_certificate.py; tuned checker
bhargavbh
committed
ea94696
Merge origin/main into certora/offer-tree

bhargavbh
and
claude
committed
7d251ea
added high-level verification approach in README
bhargavbh
committed
fa88df5
fmt
bhargavbh
committed
a1b4b8e
acknowledge URD spec in README
bhargavbh
committed
be2a563
asserts replaced with raising exceptions
bhargavbh
committed
6aaa420

Commits on Jun 3, 2026

tuned
bhargavbh
committed
bec4e8f

Commits on Jul 8, 2026

Merge branch 'main' into certora/offer-tree
MathisGD
authored
c5fb0c9

Commits on Aug 7, 2026

Merge branch 'main' into certora/offer-tree
bhargavbh
committed
bf8c505

Commits on Aug 9, 2026

updated to match latest midnight
bhargavbh
committed
6a5f897

Commits on Aug 10, 2026

Merge branch 'main' into certora/offer-tree
MathisGD
authored
758bfba

Commits on Aug 27, 2026

Improved multiplication overflow check

jhoenicke
authored and
bhargavbh
committed
b8c5a24
Remove investigation of all reverting mulDiv

jhoenicke
authored and
bhargavbh
committed
86fd2d1
Rewording of comments

jhoenicke
authored and
bhargavbh
committed
a613bc8
More comment refinement

jhoenicke
authored and
bhargavbh
committed
8da8e32
blue fallback rolling first iteration

MathisGD
authored and
bhargavbh
committed
80eec16
nit

MathisGD
authored and
bhargavbh
committed
2fe1897
lint

MathisGD
authored and
bhargavbh
committed
58cf26e
refactor: roll event

peyha
authored and
bhargavbh
committed
f112dec
refactor: undo

peyha
authored and
bhargavbh
committed
99aefcc
doc

peyha
authored and
bhargavbh
committed
7942e0d
feat: auction

peyha
authored and
bhargavbh
committed
9ba4fdb
feat: auction end

peyha
authored and
bhargavbh
committed
fc42bf1
test: remove wrong test

peyha
authored and
bhargavbh
committed
059e09f
refactor: error name

peyha
authored and
bhargavbh
committed
dff0e87
fix: require end time

peyha
authored and
bhargavbh
committed
9b4a0cb
refactor: inline incentive()

peyha
authored and
bhargavbh
committed
fed6519
test: lltv test

peyha
authored and
bhargavbh
committed
01a91b3
fix: remove increasing incentive requirement

peyha
authored and
bhargavbh
committed
eb46443
doc

peyha
authored and
bhargavbh
committed
bf81ea9
fix: incentive at start max value check

peyha
authored and
bhargavbh
committed
098e1e3
doc

peyha
authored and
bhargavbh
committed
1a1f195
doc

peyha
authored and
bhargavbh
committed
b5aa320
Update src/periphery/blue-fallback-rolling/BlueFallbackRolling.sol

authored and
bhargavbh
committed
ffb0dca
Add files via upload

MathisGD
authored and
bhargavbh
committed
a729282
newest file

MathisGD
authored and
bhargavbh
committed
367e97b
Add files via upload

MathisGD
authored and
bhargavbh
committed
9c8831f
Rename 2026-05-19-midnight-core-stermi-audit.pdf to 2026-05-19-stermi.pdf

MathisGD
authored and
bhargavbh
committed
cea79ab
refactor: interface folder

peyha
authored and
bhargavbh
committed
73755a4
fix: decreasing incentive

peyha
authored and
bhargavbh
committed
79a30b8
test: coverage

peyha
authored and
bhargavbh
committed
f89c785
test: midnight coverage

peyha
authored and
bhargavbh
committed
1e52be2
test: periphery coverage

peyha
authored and
bhargavbh
committed
4b9d2e7
chore: fmt

peyha
authored and
bhargavbh
committed
bac71f7
feat: min rollable debt

peyha
authored and
bhargavbh
committed
c02787f
fix: partial roll when below minrollableassets

peyha
authored and
bhargavbh
committed
df175fe
feat: revert to assets=debt condition

peyha
authored and
bhargavbh
committed
9c1031a
doc: readme

peyha
authored and
bhargavbh
committed
642713a
Remove lltv check

claude
authored and
bhargavbh
committed
7670ea8
Reword lltv warning comment

claude
authored and
bhargavbh
committed
88344c5
Move lltv warning to contract natspec

claude
authored and
bhargavbh
committed
82ff177
chore: lint

peyha
authored and
bhargavbh
committed
38fa6f8
doc: readme

peyha
authored and
bhargavbh
committed
77188c9
[rolling fallback] append LTV note to rounding comment

claude
authored and
bhargavbh
committed
b8508cd
test: cover authorized fallback config setters

authored and
bhargavbh
committed
aa0d660
feat: allow authorized fallback config setters

authored and
bhargavbh
committed
d4e32d3
test: require fallback config authorization first

authored and
bhargavbh
committed
8297909
fix: check fallback config authorization first

authored and
bhargavbh
committed
6a129c4
feat: equality case for end start comp

peyha
authored and
bhargavbh
committed
35143e5
Revert "feat: equality case for end start comp"

peyha
authored and
bhargavbh
committed
f65b91e
doc: periphery readme

peyha
authored and
bhargavbh
committed
7d727f8
Update src/periphery/blue-fallback-rolling/BlueFallbackRolling.sol

authored and
bhargavbh
committed
631c286
refactor: inline interface

peyha
authored and
bhargavbh
committed
c614e85
refactor: rolled assets too low

peyha
authored and
bhargavbh
committed
db3f600
Add Certora spec: realizable bad debt cannot increase without price update

claude
authored and
bhargavbh
committed
b5d2d62
Apply suggestion from @MathisGD

MathisGD
authored and
bhargavbh
committed
9a50fa9
Fix RealizableBadDebt rules: health bridge for take/withdrawCollateral, leave-zero for liquidate

claude
authored and
bhargavbh
committed
e003af3
Tighten mulDiv ghosts in liquidateRealizesBadDebt to close seize-path counterexample

claude
authored and
bhargavbh
committed
9446625
Prove mulDivUp >= mulDivDown in MulDiv.spec

claude
authored and
bhargavbh
committed
d0051d2
Merge take/withdrawCollateral into parametric rule; assert liquidate leaves zero bad debt

claude
authored and
bhargavbh
committed
bfe5d11
Help prover on liquidateRealizesBadDebt: import LIF seize bound + split asserts

claude
authored and
bhargavbh
committed
eed485c
Isolate hard liquidate realizable-bad-debt rule with getter-form seize bound

claude
authored and
bhargavbh
committed
7f77776
Split RealizableBadDebtLiquidate by liquidate input branch; lighten solver portfolio

claude
authored and
bhargavbh
committed
024a893
Bound realizable bad debt after liquidation by 2 (mulDivUp rounding dust)

claude
authored and
bhargavbh
committed
bcdccd1
Bound realizable bad debt after liquidation by 3; enable case-splitting for repaid-input branch

claude
authored and
bhargavbh
committed
aad45e1
Pin collateral invariant for full bitmap loop in RealizableBadDebtLiquidate (drop spurious >3 CEX); revert splitParallel

claude
authored and
bhargavbh
committed
c3f8d3a
Use deterministic mulDiv ghost in RealizableBadDebtLiquidate to kill spurious ghost-slack CEX

claude
authored and
bhargavbh
committed
a1f624f
Prove double-mulDivUp subadditivity lemma; apply in RealizableBadDebtLiquidate to bound bad-debt dust

claude
authored and
bhargavbh
committed
8e0a58f
Materialize seize-bound term in RealizableBadDebtLiquidate repaid branch to close chaining timeout

claude
authored and
bhargavbh
committed
94b10cc
Restrict RealizableBadDebtLiquidate repaid branch to single collateral for tractability

claude
authored and
bhargavbh
committed
28406dd
Try -depth 0 (match passing peers) + restore 2 collaterals on RealizableBadDebtLiquidate repaid branch

claude
authored and
bhargavbh
committed
9c246c1
Try cvc5-heavy portfolio + collateralIndex/single-collateral pins on RealizableBadDebtLiquidate repaid branch; 30-min timeout

claude
authored and
bhargavbh
committed
1e21778
Drop forall quantifiers from RealizableBadDebtLiquidate repaid branch; keep concrete instances (NIA blowup fix per #1083)

claude
authored and
bhargavbh
committed
aca534c
Spec improvements

jochencertora
authored and
bhargavbh
committed
b105ad9
Fix formatting

jochencertora
authored and
bhargavbh
committed
58f86a2
Apply suggestions from code review

authored and
bhargavbh
committed
085246a
Some more review issues:

jochencertora
authored and
bhargavbh
committed
bb98ee9
Fix summary

jochencertora
authored and
bhargavbh
committed
5c05e7f
remove comment

authored and
bhargavbh
committed
c2d82fd
nit

MathisGD
authored and
bhargavbh
committed
b3c76af
nit

MathisGD
authored and
bhargavbh
committed
5754a84
Remove some require

jochencertora
authored and
bhargavbh
committed
1940aeb
Remove the rules no longer needed

jochencertora
authored and
bhargavbh
committed
7360f87
Apply suggestions from code review

authored and
bhargavbh
committed
dc3a82a
Apply suggestions from code review

authored and
bhargavbh
committed
6eba1a5
Inline axioms into rules and reference their MulDiv lemmas

claude
authored and
bhargavbh
committed
88ec1d4
Prove liquidate does not increase another position's realizable bad debt

claude
authored and
bhargavbh
committed
4a86303
Fix inlined axiomAddUpUp antecedent to match original

claude
authored and
bhargavbh
committed
c60091c
Update certora/confs/RealizableBadDebt.conf

authored and
bhargavbh
committed
f10a7bd
Update certora/confs/RealizableBadDebtLiquidate.conf

authored and
bhargavbh
committed
8300f7c
Use general forall form for inlined axiom requires

claude
authored and
bhargavbh
committed
aeac0d0
Pin AddUpUp/InverseUpDown/UpZero axioms to call args (forall form times out)

claude
authored and
bhargavbh
committed
18f8179
Test: make ERC20NoReturn.approve genuinely return nothing

claude
authored and
bhargavbh
committed
8ea0155
Apply suggestion from @MathisGD

MathisGD
authored and
bhargavbh
committed
7997fc5
[tests] BlueFallbackRolling: safe approve on loan token

claude
authored and
bhargavbh
committed
314b913
Port NONDET summaries for tickToPrice and mulDiv to ReentrancyView spec

claude
authored and
bhargavbh
committed
86551f6
Separate MulDiv axiom spec file

jochencertora
authored and
bhargavbh
committed
aef0c2a
fix assertion

jochencertora
authored and
bhargavbh
committed
42ad512
Make ghost persistent (they never change)

jochencertora
authored and
bhargavbh
committed
29b71a3
[blue fallback rolling] require non-decreasing incentive

claude
authored and
bhargavbh
committed
e113fc0
[blue fallback rolling] remove redundant incentive check

claude
authored and
bhargavbh
committed
5277f60
[blue fallback rolling] add configId to Roll event

claude
authored and
bhargavbh
committed
56f27bf
Apply suggestion from @peyha

peyha
authored and
bhargavbh
committed
7f9a1e1
ci: pin foundry-toolchain to v1.9.1

prd-carapulse[bot]
authored and
bhargavbh
committed
34b1ce0
Merge branch 'main' into certora/offer-tree
bhargavbh
committed
cbdbe1d

Commits on Aug 31, 2026

reduced scope to soundness and reference implementation generating roo
bhargavbh
committed
008b787
trimmed comments
bhargavbh
committed
a52e7ac
removed leafHashDisjointFromNodeHash and nodeHashInjective
bhargavbh
committed
a258ed6
fmt
bhargavbh
committed
f6cbe2f
tuned
bhargavbh
committed
c0e2d92
removed hashLeafReproducesHashOffer
bhargavbh
committed
a539e66

Commits on Sep 1, 2026

factored out generate root; restored empty leaf condition
bhargavbh
committed
b5870a9

Commits on Sep 18, 2026

Merge branch 'main' into certora/offer-tree
bhargavbh
committed
5ce2a55
remove smt_timeout from configs
bhargavbh
committed
588da4a
model simplified: node ID is the hash
bhargavbh
committed
98c9332
make offerTree creation idempotent
bhargavbh
committed
0ec785d
GenerateRoot now does not inherit from OfferTree
bhargavbh
committed
a325670
duplicate lead test added
bhargavbh
committed
cd9458a
Disable caching for OfferTree verification
bhargavbh
committed
bee5afa

Commits

Commits on May 7, 2026

Commits on May 19, 2026

Commits on May 20, 2026

Commits on May 21, 2026

Commits on May 25, 2026

Commits on May 26, 2026

Commits on May 29, 2026

Commits on Jun 1, 2026

Commits on Jun 2, 2026

Commits on Jun 3, 2026

Commits on Jul 8, 2026

Commits on Aug 7, 2026

Commits on Aug 9, 2026

Commits on Aug 10, 2026

Commits on Aug 27, 2026