-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore(certora): add
sumOfBalancesIsTotalStaked
invariant
Closes #24
- Loading branch information
Showing
4 changed files
with
34 additions
and
5 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
// SPDX-License-Identifier: MIT | ||
|
||
pragma solidity ^0.8.26; | ||
|
||
import { ERC20 } from "@openzeppelin/contracts/token/ERC20/ERC20.sol"; | ||
|
||
contract ERC20A is ERC20 { | ||
constructor(string memory name_, string memory symbol_) ERC20(name_, symbol_) {} | ||
} | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,3 +1,16 @@ | ||
rule test { | ||
assert true; | ||
using ERC20A as staked; | ||
|
||
methods { | ||
function totalStaked() external returns (uint256) envfree; | ||
} | ||
|
||
ghost mathint sumOfBalances { | ||
init_state axiom sumOfBalances == 0; | ||
} | ||
|
||
hook Sstore users[KEY address account].stakedBalance uint256 newValue (uint256 oldValue) { | ||
sumOfBalances = sumOfBalances - oldValue + newValue; | ||
} | ||
|
||
invariant sumOfBalancesIsTotalStaked() | ||
sumOfBalances == to_mathint(totalStaked()); |