search

morpho-org / morpho-token-upgradeable

Other
7 stars 7 forks source link

[Certora] Check underflow and overflows. #97

Open colin-morpho opened 1 week ago

colin-morpho commented 1 week ago

The ERC20 specification is patched to take support the possible (in practice impossible) overflows. We should prove that these operations are safe.

QGarchery commented 1 week ago

Related comments:

colin-morpho commented 4 days ago

As of today, proving properties w.r.t delegatee's voting power with Certora seem really difficult. Instead, in https://github.com/morpho-org/morpho-token-upgradeable/pull/98/commits/a61550f74f2d08419d12aaf5204aaebb8a085608 we assume them to be true and prove that there are no overflows under these hypothesis. Closing this issue as we see no way to prove the required properties.