Rename invariants to avoid name clashes

This commit is contained in:
Mark Spanbroek 2022-02-16 14:15:43 +01:00 committed by markspanbroek
parent e1ef2a2216
commit f9cc73d62f
2 changed files with 36 additions and 31 deletions

View File

@ -6,10 +6,11 @@ import "./AccountLocks.sol";
contract Collateral is AccountLocks { contract Collateral is AccountLocks {
IERC20 public immutable token; IERC20 public immutable token;
Totals private totals; CollateralFunds private funds;
mapping(address => uint256) private balances; mapping(address => uint256) private balances;
constructor(IERC20 _token) invariant { constructor(IERC20 _token) collateralInvariant {
token = _token; token = _token;
} }
@ -19,51 +20,52 @@ contract Collateral is AccountLocks {
function add(address account, uint256 amount) private { function add(address account, uint256 amount) private {
balances[account] += amount; balances[account] += amount;
totals.balance += amount; funds.balance += amount;
} }
function subtract(address account, uint256 amount) private { function subtract(address account, uint256 amount) private {
balances[account] -= amount; balances[account] -= amount;
totals.balance -= amount; funds.balance -= amount;
} }
function transferFrom(address sender, uint256 amount) private { function transferFrom(address sender, uint256 amount) internal {
address receiver = address(this); address receiver = address(this);
require(token.transferFrom(sender, receiver, amount), "Transfer failed"); require(token.transferFrom(sender, receiver, amount), "Transfer failed");
} }
function deposit(uint256 amount) public invariant { function deposit(uint256 amount) public collateralInvariant {
transferFrom(msg.sender, amount); transferFrom(msg.sender, amount);
totals.deposited += amount; funds.deposited += amount;
add(msg.sender, amount); add(msg.sender, amount);
} }
function withdraw() public invariant { function withdraw() public collateralInvariant {
_unlockAccount(); _unlockAccount();
uint256 amount = balanceOf(msg.sender); uint256 amount = balanceOf(msg.sender);
totals.withdrawn += amount; funds.withdrawn += amount;
subtract(msg.sender, amount); subtract(msg.sender, amount);
assert(token.transfer(msg.sender, amount)); assert(token.transfer(msg.sender, amount));
} }
function _slash(address account, uint256 percentage) internal invariant { function _slash(address account, uint256 percentage)
internal
collateralInvariant
{
uint256 amount = (balanceOf(account) * percentage) / 100; uint256 amount = (balanceOf(account) * percentage) / 100;
totals.slashed += amount; funds.slashed += amount;
subtract(account, amount); subtract(account, amount);
} }
modifier invariant() { modifier collateralInvariant() {
Totals memory oldTotals = totals; CollateralFunds memory oldFunds = funds;
_; _;
assert(totals.deposited >= oldTotals.deposited); assert(funds.deposited >= oldFunds.deposited);
assert(totals.withdrawn >= oldTotals.withdrawn); assert(funds.withdrawn >= oldFunds.withdrawn);
assert(totals.slashed >= oldTotals.slashed); assert(funds.slashed >= oldFunds.slashed);
assert( assert(funds.deposited == funds.balance + funds.withdrawn + funds.slashed);
totals.deposited == totals.balance + totals.withdrawn + totals.slashed
);
} }
struct Totals { struct CollateralFunds {
uint256 balance; uint256 balance;
uint256 deposited; uint256 deposited;
uint256 withdrawn; uint256 withdrawn;

View File

@ -5,10 +5,10 @@ import "@openzeppelin/contracts/token/ERC20/IERC20.sol";
contract Marketplace { contract Marketplace {
IERC20 public immutable token; IERC20 public immutable token;
Totals private totals; MarketplaceFunds private funds;
mapping(bytes32 => Request) private requests; mapping(bytes32 => Request) private requests;
constructor(IERC20 _token) invariant { constructor(IERC20 _token) marketplaceInvariant {
token = _token; token = _token;
} }
@ -17,14 +17,17 @@ contract Marketplace {
require(token.transferFrom(sender, receiver, amount), "Transfer failed"); require(token.transferFrom(sender, receiver, amount), "Transfer failed");
} }
function requestStorage(Request calldata request) public invariant { function requestStorage(Request calldata request)
public
marketplaceInvariant
{
bytes32 id = keccak256(abi.encode(request)); bytes32 id = keccak256(abi.encode(request));
require(request.size > 0, "Invalid size"); require(request.size > 0, "Invalid size");
require(requests[id].size == 0, "Request already exists"); require(requests[id].size == 0, "Request already exists");
requests[id] = request; requests[id] = request;
transferFrom(msg.sender, request.maxPrice); transferFrom(msg.sender, request.maxPrice);
totals.received += request.maxPrice; funds.received += request.maxPrice;
totals.balance += request.maxPrice; funds.balance += request.maxPrice;
emit StorageRequested(id, request); emit StorageRequested(id, request);
} }
@ -40,15 +43,15 @@ contract Marketplace {
event StorageRequested(bytes32 id, Request request); event StorageRequested(bytes32 id, Request request);
modifier invariant() { modifier marketplaceInvariant() {
Totals memory oldTotals = totals; MarketplaceFunds memory oldFunds = funds;
_; _;
assert(totals.received >= oldTotals.received); assert(funds.received >= oldFunds.received);
assert(totals.sent >= oldTotals.sent); assert(funds.sent >= oldFunds.sent);
assert(totals.received == totals.balance + totals.sent); assert(funds.received == funds.balance + funds.sent);
} }
struct Totals { struct MarketplaceFunds {
uint256 balance; uint256 balance;
uint256 received; uint256 received;
uint256 sent; uint256 sent;