[Certora] update position missing rules#970
Conversation
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 6103979082
ℹ️ About Codex in GitHub
Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".
| ghost ghostMulDivDown(uint256, uint256, uint256) returns uint256 { | ||
| // Axioms proven in MulDiv.spec. | ||
| axiom forall uint256 y. forall uint256 z. ghostMulDivDown(0, y, z) == 0; | ||
| axiom forall uint256 x. forall uint256 z. ghostMulDivDown(x, 0, z) == 0; |
There was a problem hiding this comment.
Axiom 2 is not actually proven in Muldiv.spec no ? we should extend mulDivZero to prove that assert mulDivDown(a, 0, d) == 0; and assert mulDivUp(a, 0, d) == 0; i think.
Axiom 3 is ok as it is derivable
There was a problem hiding this comment.
I thought it was added already, but actually it will be the case only after #542
|
|
||
| /// An unauthorized caller cannot change a user's updated credit except via liquidate. | ||
| /// Assumes no reentrancy: callbacks and token transfers are not modeled as re-entering Midnight, so re-entrant collateral changes are not covered. | ||
| rule onlyAuthorizedCanChangeUpdatedCreditExceptLiquidate(env e, method f, calldataarg args, Midnight.Market market, address user) filtered { f -> f.selector != sig:liquidate(Midnight.Market, uint256, uint256, uint256, address, bool, address, address, bytes).selector } { |
There was a problem hiding this comment.
we can also prove onlyAuthorizedCanChangeUpdatedPendingFeeExceptLiquidate as face vzalue of a lender is actually credit - pendingFee maybe it's interesting and a natural companion to this rule , wdyt ?
2 participants
Proves the following items in the wish list: