Fix unsound require assumptions in Liveness spec (#781) - #784

Merged

QGarchery merged 20 commits into

mainfrom

fix/781-liveness-assert-soundness

Jul 28, 2026

Commits on Jul 23, 2026

Fix unsound require assumptions in Liveness spec (#781)
claude
committed
2a2921a
Add bounds to satisfy rules in Liveness spec
claude
committed
1fa71de
Assume transferred amount is uint128-bounded in transfer summary
claude
committed
fbdec3e
Bound the balance ghost on both sides in the transfer summary
claude
committed
594a374
Assume Morpho is not the caller in remaining liveness rules
claude
committed
82d864d
Address review: bound balance as uint256, sound receive-side overflow require, drop redundant per-rule bounds
claude
committed
6b4653a
Apply suggestion from @MathisGD
MathisGD
authored
e46c62c
Apply suggestion from @MathisGD
MathisGD
authored
222c1ae
Tighten liveness assumptions to the transferred amount (review)
claude
committed
212557a
Merge commit '3085651a79553bbabbfd8be309c262dab45b686e' into fix/781-liveness-assert-soundness
claude
committed
afca181
Tighten liveness assumptions via computed transfer amount (Util helpers)
claude
committed
67f25d2
Assume no interest accrual in by-shares liveness rules so the transfer-amount bound holds
claude
committed
10e1279
Reference the idleAmountLessThanBalance invariant on the liquidate collateral bound
claude
committed
3efd5c5

Commits on Jul 24, 2026

Commits on Jul 26, 2026

Clarify the receive-branch require comment
claude
committed
837740c

Commits on Jul 28, 2026

nitpicks
QGarchery
committed
7e758a6
require idleAmountLessThanBalance in the right way
QGarchery
committed
afa2329
Merge pull request #786 from morpho-org/review-fix-liveness
MathisGD
authored
fdd6209