ITADN

Improve MorphoHarness and create a Util file

#699ClosedQGarchery 创建于 2024-10-25
verif
Q
QGarcherycommented
The current verification setup and harness could be improved in 2 ways: - make `MorphoHarness` expose getters that return the struct. For information this is done for metamorpho, for example [here](https://github.com/morpho-org/metamorpho/blob/764d284221f96a0fdb86d6b024187fcd73267c11/certora/helpers/MetaMorphoHarness.sol#L18-L20). This allows to then call the fields of the returned struct (for example [here](https://github.com/morpho-org/metamorpho/blob/764d284221f96a0fdb86d6b024187fcd73267c11/certora/specs/PendingValues.spec#L23)), instead of having a tuple - extract out, in a `Util.sol` file, the functions that do not depend on the state of the contract. For example `wad`, or `maxFee`, or simply add them in the spec when it makes sense. This is because then it makes importing files awkward, and naming weird (we don't want to write `MorphoHarness.WAD()`)
关闭于 2024-10-28 0 条评论