commit
7a3a3116b7
@ -1,5 +0,0 @@ |
||||
--- |
||||
'openzeppelin-solidity': minor |
||||
--- |
||||
|
||||
`TransparentUpgradeableProxy`: support value passthrough for all ifAdmin function. |
@ -1,56 +1,60 @@ |
||||
# Running the certora verification tool |
||||
|
||||
These instructions detail the process for running CVT on the OpenZeppelin (Wizard/Governor) contracts. |
||||
These instructions detail the process for running Certora Verification Tool on OpenZeppelin Contracts. |
||||
|
||||
Documentation for CVT and the specification language are available |
||||
[here](https://certora.atlassian.net/wiki/spaces/CPD/overview) |
||||
Documentation for CVT and the specification language are available [here](https://certora.atlassian.net/wiki/spaces/CPD/overview). |
||||
|
||||
## Prerequisites |
||||
|
||||
Follow the [Certora installation guide](https://docs.certora.com/en/latest/docs/user-guide/getting-started/install.html) in order to get the Certora Prover Package and the `solc` executable folder in your path. |
||||
|
||||
> **Note** |
||||
> An API Key is required for local testing. Although the prover will run on a Github Actions' CI environment on selected Pull Requests. |
||||
|
||||
## Running the verification |
||||
|
||||
The scripts in the `certora/scripts` directory are used to submit verification |
||||
jobs to the Certora verification service. After the job is complete, the results will be available on |
||||
[the Certora portal](https://vaas-stg.certora.com/). |
||||
The Certora Verification Tool proves specs for contracts, which are defined by the `./specs.json` file along with their pre-configured options. |
||||
|
||||
These scripts should be run from the root directory; for example by running |
||||
The verification script `./run.js` is used to submit verification jobs to the Certora Verification service. |
||||
|
||||
``` |
||||
sh certora/scripts/verifyAll.sh <meaningful comment> |
||||
You can run it from the root of the repository with the following command: |
||||
|
||||
```bash |
||||
node certora/run.js [[CONTRACT_NAME:]SPEC_NAME] [OPTIONS...] |
||||
``` |
||||
|
||||
The most important of these is `verifyAll.sh`, which checks |
||||
all of the harnessed contracts (`certora/harness/Wizard*.sol`) against all of |
||||
the specifications (`certora/spec/*.spec`). |
||||
Where: |
||||
|
||||
The other scripts run a subset of the specifications or the contracts. You can |
||||
verify different contracts or specifications by changing the `--verify` option, |
||||
and you can run a single rule or method with the `--rule` or `--method` option. |
||||
- `CONTRACT_NAME` matches the `contract` key in the `./spec.json` file and may be empty. It will run all matching contracts if not provided. |
||||
- `SPEC_NAME` refers to a `spec` key from the `./specs.json` file. It will run every spec if not provided. |
||||
- `OPTIONS` extend the [Certora Prover CLI options](https://docs.certora.com/en/latest/docs/prover/cli/options.html#certora-prover-cli-options) and will respect the preconfigured options in the `specs.json` file. |
||||
|
||||
For example, to verify the `WizardFirstPriority` contract against the |
||||
`GovernorCountingSimple` specification, you could change the `--verify` line of |
||||
the `WizardControlFirstPriortity.sh` script to: |
||||
> **Note** |
||||
> A single spec may be configured to run for multiple contracts, whereas a single contract may run multiple specs. |
||||
|
||||
``` |
||||
--verify WizardFirstPriority:certora/specs/GovernorCountingSimple.spec \ |
||||
Example usage: |
||||
|
||||
```bash |
||||
node certora/run.js AccessControl # Run the AccessControl spec against every contract implementing it |
||||
``` |
||||
|
||||
## Adapting to changes in the contracts |
||||
|
||||
Some of our rules require the code to be simplified in various ways. Our |
||||
primary tool for performing these simplifications is to run verification on a |
||||
contract that extends the original contracts and overrides some of the methods. |
||||
These "harness" contracts can be found in the `certora/harness` directory. |
||||
|
||||
This pattern does require some modifications to the original code: some methods |
||||
need to be made virtual or public, for example. These changes are handled by |
||||
applying a patch to the code before verification. |
||||
|
||||
When one of the `verify` scripts is executed, it first applies the patch file |
||||
`certora/applyHarness.patch` to the `contracts` directory, placing the output |
||||
in the `certora/munged` directory. We then verify the contracts in the |
||||
`certora/munged` directory. |
||||
|
||||
If the original contracts change, it is possible to create a conflict with the |
||||
patch. In this case, the verify scripts will report an error message and output |
||||
rejected changes in the `munged` directory. After merging the changes, run |
||||
`make record` in the `certora` directory; this will regenerate the patch file, |
||||
which can then be checked into git. |
||||
Some of our rules require the code to be simplified in various ways. Our primary tool for performing these simplifications is to run verification on a contract that extends the original contracts and overrides some of the methods. These "harness" contracts can be found in the `certora/harness` directory. |
||||
|
||||
This pattern does require some modifications to the original code: some methods need to be made virtual or public, for example. These changes are handled by applying a patch |
||||
to the code before verification by running: |
||||
|
||||
```bash |
||||
make -C certora apply |
||||
``` |
||||
|
||||
Before running the `certora/run.js` script, it's required to apply the corresponding patches to the `contracts` directory, placing the output in the `certora/patched` directory. Then, the contracts are verified by running the verification for the `certora/patched` directory. |
||||
|
||||
If the original contracts change, it is possible to create a conflict with the patch. In this case, the verify scripts will report an error message and output rejected changes in the `patched` directory. After merging the changes, run `make record` in the `certora` directory; this will regenerate the patch file, which can then be checked into git. |
||||
|
||||
For more information about the `make` scripts available, run: |
||||
|
||||
```bash |
||||
make -C certora help |
||||
``` |
||||
|
@ -0,0 +1,14 @@ |
||||
--- token/ERC721/ERC721.sol 2023-03-07 10:48:47.736822221 +0100
|
||||
+++ token/ERC721/ERC721.sol 2023-03-09 19:49:39.669338673 +0100
|
||||
@@ -199,6 +199,11 @@
|
||||
return _owners[tokenId];
|
||||
}
|
||||
|
||||
+ // FV
|
||||
+ function _getApproved(uint256 tokenId) internal view returns (address) {
|
||||
+ return _tokenApprovals[tokenId];
|
||||
+ }
|
||||
+
|
||||
/**
|
||||
* @dev Returns whether `tokenId` exists.
|
||||
*
|
@ -0,0 +1,59 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
|
||||
pragma solidity ^0.8.0; |
||||
|
||||
import "../patched/utils/structs/DoubleEndedQueue.sol"; |
||||
|
||||
contract DoubleEndedQueueHarness { |
||||
using DoubleEndedQueue for DoubleEndedQueue.Bytes32Deque; |
||||
|
||||
DoubleEndedQueue.Bytes32Deque private _deque; |
||||
|
||||
function pushFront(bytes32 value) external { |
||||
_deque.pushFront(value); |
||||
} |
||||
|
||||
function pushBack(bytes32 value) external { |
||||
_deque.pushBack(value); |
||||
} |
||||
|
||||
function popFront() external returns (bytes32 value) { |
||||
return _deque.popFront(); |
||||
} |
||||
|
||||
function popBack() external returns (bytes32 value) { |
||||
return _deque.popBack(); |
||||
} |
||||
|
||||
function clear() external { |
||||
_deque.clear(); |
||||
} |
||||
|
||||
function begin() external view returns (int128) { |
||||
return _deque._begin; |
||||
} |
||||
|
||||
function end() external view returns (int128) { |
||||
return _deque._end; |
||||
} |
||||
|
||||
function length() external view returns (uint256) { |
||||
return _deque.length(); |
||||
} |
||||
|
||||
function empty() external view returns (bool) { |
||||
return _deque.empty(); |
||||
} |
||||
|
||||
function front() external view returns (bytes32 value) { |
||||
return _deque.front(); |
||||
} |
||||
|
||||
function back() external view returns (bytes32 value) { |
||||
return _deque.back(); |
||||
} |
||||
|
||||
function at_(uint256 index) external view returns (bytes32 value) { |
||||
return _deque.at(index); |
||||
} |
||||
} |
@ -0,0 +1,37 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
|
||||
pragma solidity ^0.8.0; |
||||
|
||||
import "../patched/token/ERC721/ERC721.sol"; |
||||
|
||||
contract ERC721Harness is ERC721 { |
||||
constructor(string memory name, string memory symbol) ERC721(name, symbol) {} |
||||
|
||||
function mint(address account, uint256 tokenId) external { |
||||
_mint(account, tokenId); |
||||
} |
||||
|
||||
function safeMint(address to, uint256 tokenId) external { |
||||
_safeMint(to, tokenId); |
||||
} |
||||
|
||||
function safeMint(address to, uint256 tokenId, bytes memory data) external { |
||||
_safeMint(to, tokenId, data); |
||||
} |
||||
|
||||
function burn(uint256 tokenId) external { |
||||
_burn(tokenId); |
||||
} |
||||
|
||||
function tokenExists(uint256 tokenId) external view returns (bool) { |
||||
return _exists(tokenId); |
||||
} |
||||
|
||||
function unsafeOwnerOf(uint256 tokenId) external view returns (address) { |
||||
return _ownerOf(tokenId); |
||||
} |
||||
|
||||
function unsafeGetApproved(uint256 tokenId) external view returns (address) { |
||||
return _getApproved(tokenId); |
||||
} |
||||
} |
@ -0,0 +1,11 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
|
||||
pragma solidity ^0.8.0; |
||||
|
||||
import "../patched/interfaces/IERC721Receiver.sol"; |
||||
|
||||
contract ERC721ReceiverHarness is IERC721Receiver { |
||||
function onERC721Received(address, address, uint256, bytes calldata) external pure returns (bytes4) { |
||||
return this.onERC721Received.selector; |
||||
} |
||||
} |
@ -0,0 +1,19 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
|
||||
pragma solidity ^0.8.0; |
||||
|
||||
import "../patched/security/Pausable.sol"; |
||||
|
||||
contract PausableHarness is Pausable { |
||||
function pause() external { |
||||
_pause(); |
||||
} |
||||
|
||||
function unpause() external { |
||||
_unpause(); |
||||
} |
||||
|
||||
function onlyWhenPaused() external whenPaused {} |
||||
|
||||
function onlyWhenNotPaused() external whenNotPaused {} |
||||
} |
@ -0,0 +1,12 @@ |
||||
pragma solidity ^0.8.0; |
||||
|
||||
import "../patched/governance/TimelockController.sol"; |
||||
|
||||
contract TimelockControllerHarness is TimelockController { |
||||
constructor( |
||||
uint256 minDelay, |
||||
address[] memory proposers, |
||||
address[] memory executors, |
||||
address admin |
||||
) TimelockController(minDelay, proposers, executors, admin) {} |
||||
} |
@ -0,0 +1,366 @@ |
||||
import "helpers.spec" |
||||
|
||||
methods { |
||||
pushFront(bytes32) envfree |
||||
pushBack(bytes32) envfree |
||||
popFront() returns (bytes32) envfree |
||||
popBack() returns (bytes32) envfree |
||||
clear() envfree |
||||
|
||||
// exposed for FV |
||||
begin() returns (int128) envfree |
||||
end() returns (int128) envfree |
||||
|
||||
// view |
||||
length() returns (uint256) envfree |
||||
empty() returns (bool) envfree |
||||
front() returns (bytes32) envfree |
||||
back() returns (bytes32) envfree |
||||
at_(uint256) returns (bytes32) envfree // at is a reserved word |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Helpers │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
|
||||
function min_int128() returns mathint { |
||||
return -(1 << 127); |
||||
} |
||||
|
||||
function max_int128() returns mathint { |
||||
return (1 << 127) - 1; |
||||
} |
||||
|
||||
// Could be broken in theory, but not in practice |
||||
function boundedQueue() returns bool { |
||||
return |
||||
max_int128() > to_mathint(end()) && |
||||
min_int128() < to_mathint(begin()); |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Invariant: end is larger or equal than begin │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
invariant boundariesConsistency() |
||||
end() >= begin() |
||||
filtered { f -> !f.isView } |
||||
{ preserved { require boundedQueue(); } } |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Invariant: length is end minus begin │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
invariant lengthConsistency() |
||||
length() == to_mathint(end()) - to_mathint(begin()) |
||||
filtered { f -> !f.isView } |
||||
{ preserved { require boundedQueue(); } } |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Invariant: empty() is length 0 and no element exists │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
invariant emptiness() |
||||
empty() <=> length() == 0 |
||||
filtered { f -> !f.isView } |
||||
{ preserved { require boundedQueue(); } } |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Invariant: front points to the first index and back points to the last one │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
invariant queueEndings() |
||||
at_(length() - 1) == back() && at_(0) == front() |
||||
filtered { f -> !f.isView } |
||||
{ |
||||
preserved { |
||||
requireInvariant boundariesConsistency(); |
||||
require boundedQueue(); |
||||
} |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Function correctness: pushFront adds an element at the beginning of the queue │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule pushFront(bytes32 value) { |
||||
require boundedQueue(); |
||||
|
||||
uint256 lengthBefore = length(); |
||||
|
||||
pushFront@withrevert(value); |
||||
|
||||
// liveness |
||||
assert !lastReverted, "never reverts"; |
||||
|
||||
// effect |
||||
assert front() == value, "front set to value"; |
||||
assert length() == lengthBefore + 1, "queue extended"; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: pushFront preserves the previous values in the queue with a +1 offset │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule pushFrontConsistency(uint256 index) { |
||||
require boundedQueue(); |
||||
|
||||
bytes32 beforeAt = at_(index); |
||||
|
||||
bytes32 value; |
||||
pushFront(value); |
||||
|
||||
// try to read value |
||||
bytes32 afterAt = at_@withrevert(index + 1); |
||||
|
||||
assert !lastReverted, "value still there"; |
||||
assert afterAt == beforeAt, "data is preserved"; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Function correctness: pushBack adds an element at the end of the queue │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule pushBack(bytes32 value) { |
||||
require boundedQueue(); |
||||
|
||||
uint256 lengthBefore = length(); |
||||
|
||||
pushBack@withrevert(value); |
||||
|
||||
// liveness |
||||
assert !lastReverted, "never reverts"; |
||||
|
||||
// effect |
||||
assert back() == value, "back set to value"; |
||||
assert length() == lengthBefore + 1, "queue increased"; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: pushBack preserves the previous values in the queue │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule pushBackConsistency(uint256 index) { |
||||
require boundedQueue(); |
||||
|
||||
bytes32 beforeAt = at_(index); |
||||
|
||||
bytes32 value; |
||||
pushBack(value); |
||||
|
||||
// try to read value |
||||
bytes32 afterAt = at_@withrevert(index); |
||||
|
||||
assert !lastReverted, "value still there"; |
||||
assert afterAt == beforeAt, "data is preserved"; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Function correctness: popFront removes an element from the beginning of the queue │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule popFront { |
||||
requireInvariant boundariesConsistency(); |
||||
require boundedQueue(); |
||||
|
||||
uint256 lengthBefore = length(); |
||||
bytes32 frontBefore = front@withrevert(); |
||||
|
||||
bytes32 popped = popFront@withrevert(); |
||||
bool success = !lastReverted; |
||||
|
||||
// liveness |
||||
assert success <=> lengthBefore != 0, "never reverts if not previously empty"; |
||||
|
||||
// effect |
||||
assert success => frontBefore == popped, "previous front is returned"; |
||||
assert success => length() == lengthBefore - 1, "queue decreased"; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: at(x) is preserved and offset to at(x - 1) after calling popFront | |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule popFrontConsistency(uint256 index) { |
||||
requireInvariant boundariesConsistency(); |
||||
require boundedQueue(); |
||||
|
||||
// Read (any) value that is not the front (this asserts the value exists / the queue is long enough) |
||||
require index > 1; |
||||
bytes32 before = at_(index); |
||||
|
||||
popFront(); |
||||
|
||||
// try to read value |
||||
bytes32 after = at_@withrevert(index - 1); |
||||
|
||||
assert !lastReverted, "value still exists in the queue"; |
||||
assert before == after, "values are offset and not modified"; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Function correctness: popBack removes an element from the end of the queue │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule popBack { |
||||
requireInvariant boundariesConsistency(); |
||||
require boundedQueue(); |
||||
|
||||
uint256 lengthBefore = length(); |
||||
bytes32 backBefore = back@withrevert(); |
||||
|
||||
bytes32 popped = popBack@withrevert(); |
||||
bool success = !lastReverted; |
||||
|
||||
// liveness |
||||
assert success <=> lengthBefore != 0, "never reverts if not previously empty"; |
||||
|
||||
// effect |
||||
assert success => backBefore == popped, "previous back is returned"; |
||||
assert success => length() == lengthBefore - 1, "queue decreased"; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: at(x) is preserved after calling popBack | |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule popBackConsistency(uint256 index) { |
||||
requireInvariant boundariesConsistency(); |
||||
require boundedQueue(); |
||||
|
||||
// Read (any) value that is not the back (this asserts the value exists / the queue is long enough) |
||||
require index < length() - 1; |
||||
bytes32 before = at_(index); |
||||
|
||||
popBack(); |
||||
|
||||
// try to read value |
||||
bytes32 after = at_@withrevert(index); |
||||
|
||||
assert !lastReverted, "value still exists in the queue"; |
||||
assert before == after, "values are offset and not modified"; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Function correctness: clear sets length to 0 │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule clear { |
||||
clear@withrevert(); |
||||
|
||||
// liveness |
||||
assert !lastReverted, "never reverts"; |
||||
|
||||
// effect |
||||
assert length() == 0, "sets length to 0"; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: front/back access reverts only if the queue is empty or querying out of bounds │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule onlyEmptyRevert(env e) { |
||||
require nonpayable(e); |
||||
requireInvariant boundariesConsistency(); |
||||
require boundedQueue(); |
||||
|
||||
method f; |
||||
calldataarg args; |
||||
|
||||
bool emptyBefore = empty(); |
||||
|
||||
f@withrevert(e, args); |
||||
|
||||
assert lastReverted => ( |
||||
(f.selector == front().selector && emptyBefore) || |
||||
(f.selector == back().selector && emptyBefore) || |
||||
(f.selector == popFront().selector && emptyBefore) || |
||||
(f.selector == popBack().selector && emptyBefore) || |
||||
f.selector == at_(uint256).selector // revert conditions are verified in onlyOutOfBoundsRevert |
||||
), "only revert if empty or out of bounds"; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: at(index) only reverts if index is out of bounds | |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule onlyOutOfBoundsRevert(uint256 index) { |
||||
requireInvariant boundariesConsistency(); |
||||
require boundedQueue(); |
||||
|
||||
at_@withrevert(index); |
||||
|
||||
assert lastReverted <=> index >= length(), "only reverts if index is out of bounds"; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: only clear/push/pop operations can change the length of the queue │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule noLengthChange(env e) { |
||||
requireInvariant boundariesConsistency(); |
||||
require boundedQueue(); |
||||
|
||||
method f; |
||||
calldataarg args; |
||||
|
||||
uint256 lengthBefore = length(); |
||||
f(e, args); |
||||
uint256 lengthAfter = length(); |
||||
|
||||
assert lengthAfter != lengthBefore => ( |
||||
(f.selector == pushFront(bytes32).selector && lengthAfter == lengthBefore + 1) || |
||||
(f.selector == pushBack(bytes32).selector && lengthAfter == lengthBefore + 1) || |
||||
(f.selector == popBack().selector && lengthAfter == lengthBefore - 1) || |
||||
(f.selector == popFront().selector && lengthAfter == lengthBefore - 1) || |
||||
(f.selector == clear().selector && lengthAfter == 0) |
||||
), "length is only affected by clear/pop/push operations"; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: only push/pop can change values bounded in the queue (outside values aren't cleared) │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule noDataChange(env e) { |
||||
requireInvariant boundariesConsistency(); |
||||
require boundedQueue(); |
||||
|
||||
method f; |
||||
calldataarg args; |
||||
|
||||
uint256 index; |
||||
bytes32 atBefore = at_(index); |
||||
f(e, args); |
||||
bytes32 atAfter = at_@withrevert(index); |
||||
bool atAfterSuccess = !lastReverted; |
||||
|
||||
assert !atAfterSuccess <=> ( |
||||
f.selector == clear().selector || |
||||
(f.selector == popBack().selector && index == length()) || |
||||
(f.selector == popFront().selector && index == length()) |
||||
), "indexes of the queue are only removed by clear or pop"; |
||||
|
||||
assert atAfterSuccess && atAfter != atBefore => ( |
||||
f.selector == popFront().selector || |
||||
f.selector == pushFront(bytes32).selector |
||||
), "values of the queue are only changed by popFront or pushFront"; |
||||
} |
@ -0,0 +1,589 @@ |
||||
import "helpers.spec" |
||||
import "methods/IERC721.spec" |
||||
|
||||
methods { |
||||
// exposed for FV |
||||
mint(address,uint256) |
||||
safeMint(address,uint256) |
||||
safeMint(address,uint256,bytes) |
||||
burn(uint256) |
||||
|
||||
tokenExists(uint256) returns (bool) envfree |
||||
unsafeOwnerOf(uint256) returns (address) envfree |
||||
unsafeGetApproved(uint256) returns (address) envfree |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Helpers │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
|
||||
// Could be broken in theory, but not in practice |
||||
function balanceLimited(address account) returns bool { |
||||
return balanceOf(account) < max_uint256; |
||||
} |
||||
|
||||
function helperTransferWithRevert(env e, method f, address from, address to, uint256 tokenId) { |
||||
if (f.selector == transferFrom(address,address,uint256).selector) { |
||||
transferFrom@withrevert(e, from, to, tokenId); |
||||
} else if (f.selector == safeTransferFrom(address,address,uint256).selector) { |
||||
safeTransferFrom@withrevert(e, from, to, tokenId); |
||||
} else if (f.selector == safeTransferFrom(address,address,uint256,bytes).selector) { |
||||
bytes params; |
||||
require params.length < 0xffff; |
||||
safeTransferFrom@withrevert(e, from, to, tokenId, params); |
||||
} else { |
||||
calldataarg args; |
||||
f@withrevert(e, args); |
||||
} |
||||
} |
||||
|
||||
function helperMintWithRevert(env e, method f, address to, uint256 tokenId) { |
||||
if (f.selector == mint(address,uint256).selector) { |
||||
mint@withrevert(e, to, tokenId); |
||||
} else if (f.selector == safeMint(address,uint256).selector) { |
||||
safeMint@withrevert(e, to, tokenId); |
||||
} else if (f.selector == safeMint(address,uint256,bytes).selector) { |
||||
bytes params; |
||||
require params.length < 0xffff; |
||||
safeMint@withrevert(e, to, tokenId, params); |
||||
} else { |
||||
require false; |
||||
} |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Ghost & hooks: ownership count │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
ghost ownedTotal() returns uint256 { |
||||
init_state axiom ownedTotal() == 0; |
||||
} |
||||
|
||||
ghost mapping(address => uint256) ownedByUser { |
||||
init_state axiom forall address a. ownedByUser[a] == 0; |
||||
} |
||||
|
||||
hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) STORAGE { |
||||
ownedByUser[newOwner] = ownedByUser[newOwner] + to_uint256(newOwner != 0 ? 1 : 0); |
||||
ownedByUser[oldOwner] = ownedByUser[oldOwner] - to_uint256(oldOwner != 0 ? 1 : 0); |
||||
|
||||
havoc ownedTotal assuming ownedTotal@new() == ownedTotal@old() |
||||
+ to_uint256(newOwner != 0 ? 1 : 0) |
||||
- to_uint256(oldOwner != 0 ? 1 : 0); |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Ghost & hooks: sum of all balances │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
ghost sumOfBalances() returns uint256 { |
||||
init_state axiom sumOfBalances() == 0; |
||||
} |
||||
|
||||
hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { |
||||
havoc sumOfBalances assuming sumOfBalances@new() == sumOfBalances@old() + newValue - oldValue; |
||||
} |
||||
|
||||
ghost mapping(address => uint256) ghostBalanceOf { |
||||
init_state axiom forall address a. ghostBalanceOf[a] == 0; |
||||
} |
||||
|
||||
hook Sload uint256 value _balances[KEY address user] STORAGE { |
||||
require ghostBalanceOf[user] == value; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Invariant: ownedTotal is the sum of all balances │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
invariant ownedTotalIsSumOfBalances() |
||||
ownedTotal() == sumOfBalances() |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Invariant: balanceOf is the number of tokens owned │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
invariant balanceOfConsistency(address user) |
||||
balanceOf(user) == ownedByUser[user] && |
||||
balanceOf(user) == ghostBalanceOf[user] |
||||
{ |
||||
preserved { |
||||
require balanceLimited(user); |
||||
} |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Invariant: owner of a token must have some balance │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
invariant ownerHasBalance(uint256 tokenId) |
||||
balanceOf(ownerOf(tokenId)) > 0 |
||||
{ |
||||
preserved { |
||||
requireInvariant balanceOfConsistency(ownerOf(tokenId)); |
||||
require balanceLimited(ownerOf(tokenId)); |
||||
} |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Invariant: tokens that do not exist are not owned and not approved │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
invariant notMintedUnset(uint256 tokenId) |
||||
(!tokenExists(tokenId) <=> unsafeOwnerOf(tokenId) == 0) && |
||||
(!tokenExists(tokenId) => unsafeGetApproved(tokenId) == 0) |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: ownerOf and getApproved revert if token does not exist │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule notMintedRevert(uint256 tokenId) { |
||||
requireInvariant notMintedUnset(tokenId); |
||||
|
||||
bool e = tokenExists(tokenId); |
||||
|
||||
address owner = ownerOf@withrevert(tokenId); |
||||
assert e <=> !lastReverted; |
||||
assert e => owner == unsafeOwnerOf(tokenId); // notMintedUnset tells us this is non-zero |
||||
|
||||
address approved = getApproved@withrevert(tokenId); |
||||
assert e <=> !lastReverted; |
||||
assert e => approved == unsafeGetApproved(tokenId); |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: unsafeOwnerOf and unsafeGetApproved don't revert │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule unsafeDontRevert(uint256 tokenId) { |
||||
unsafeOwnerOf@withrevert(tokenId); |
||||
assert !lastReverted; |
||||
|
||||
unsafeGetApproved@withrevert(tokenId); |
||||
assert !lastReverted; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: balance of address(0) is 0 │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule zeroAddressBalanceRevert() { |
||||
balanceOf@withrevert(0); |
||||
assert lastReverted; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rules: total supply can only change through mint and burn │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule supplyChange(env e) { |
||||
uint256 supplyBefore = ownedTotal(); |
||||
method f; calldataarg args; f(e, args); |
||||
uint256 supplyAfter = ownedTotal(); |
||||
|
||||
assert supplyAfter > supplyBefore => ( |
||||
supplyAfter == supplyBefore + 1 && |
||||
( |
||||
f.selector == mint(address,uint256).selector || |
||||
f.selector == safeMint(address,uint256).selector || |
||||
f.selector == safeMint(address,uint256,bytes).selector |
||||
) |
||||
); |
||||
assert supplyAfter < supplyBefore => ( |
||||
supplyAfter == supplyBefore - 1 && |
||||
f.selector == burn(uint256).selector |
||||
); |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rules: balanceOf can only change through mint, burn or transfers. balanceOf cannot change by more than 1. │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule balanceChange(env e, address account) { |
||||
requireInvariant balanceOfConsistency(account); |
||||
require balanceLimited(account); |
||||
|
||||
uint256 balanceBefore = balanceOf(account); |
||||
method f; calldataarg args; f(e, args); |
||||
uint256 balanceAfter = balanceOf(account); |
||||
|
||||
// balance can change by at most 1 |
||||
assert balanceBefore != balanceAfter => ( |
||||
balanceAfter == balanceBefore - 1 || |
||||
balanceAfter == balanceBefore + 1 |
||||
); |
||||
|
||||
// only selected function can change balances |
||||
assert balanceBefore != balanceAfter => ( |
||||
f.selector == transferFrom(address,address,uint256).selector || |
||||
f.selector == safeTransferFrom(address,address,uint256).selector || |
||||
f.selector == safeTransferFrom(address,address,uint256,bytes).selector || |
||||
f.selector == mint(address,uint256).selector || |
||||
f.selector == safeMint(address,uint256).selector || |
||||
f.selector == safeMint(address,uint256,bytes).selector || |
||||
f.selector == burn(uint256).selector |
||||
); |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rules: ownership can only change through mint, burn or transfers. │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule ownershipChange(env e, uint256 tokenId) { |
||||
address ownerBefore = unsafeOwnerOf(tokenId); |
||||
method f; calldataarg args; f(e, args); |
||||
address ownerAfter = unsafeOwnerOf(tokenId); |
||||
|
||||
assert ownerBefore == 0 && ownerAfter != 0 => ( |
||||
f.selector == mint(address,uint256).selector || |
||||
f.selector == safeMint(address,uint256).selector || |
||||
f.selector == safeMint(address,uint256,bytes).selector |
||||
); |
||||
|
||||
assert ownerBefore != 0 && ownerAfter == 0 => ( |
||||
f.selector == burn(uint256).selector |
||||
); |
||||
|
||||
assert (ownerBefore != ownerAfter && ownerBefore != 0 && ownerAfter != 0) => ( |
||||
f.selector == transferFrom(address,address,uint256).selector || |
||||
f.selector == safeTransferFrom(address,address,uint256).selector || |
||||
f.selector == safeTransferFrom(address,address,uint256,bytes).selector |
||||
); |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rules: token approval can only change through approve or transfers (implicitly). │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule approvalChange(env e, uint256 tokenId) { |
||||
address approvalBefore = unsafeGetApproved(tokenId); |
||||
method f; calldataarg args; f(e, args); |
||||
address approvalAfter = unsafeGetApproved(tokenId); |
||||
|
||||
// approve can set any value, other functions reset |
||||
assert approvalBefore != approvalAfter => ( |
||||
f.selector == approve(address,uint256).selector || |
||||
( |
||||
( |
||||
f.selector == transferFrom(address,address,uint256).selector || |
||||
f.selector == safeTransferFrom(address,address,uint256).selector || |
||||
f.selector == safeTransferFrom(address,address,uint256,bytes).selector || |
||||
f.selector == burn(uint256).selector |
||||
) && approvalAfter == 0 |
||||
) |
||||
); |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rules: approval for all tokens can only change through isApprovedForAll. │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule approvedForAllChange(env e, address owner, address spender) { |
||||
bool approvedForAllBefore = isApprovedForAll(owner, spender); |
||||
method f; calldataarg args; f(e, args); |
||||
bool approvedForAllAfter = isApprovedForAll(owner, spender); |
||||
|
||||
assert approvedForAllBefore != approvedForAllAfter => f.selector == setApprovalForAll(address,bool).selector; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: transferFrom behavior and side effects │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule transferFrom(env e, address from, address to, uint256 tokenId) { |
||||
require nonpayable(e); |
||||
|
||||
address operator = e.msg.sender; |
||||
uint256 otherTokenId; |
||||
address otherAccount; |
||||
|
||||
requireInvariant ownerHasBalance(tokenId); |
||||
require balanceLimited(to); |
||||
|
||||
uint256 balanceOfFromBefore = balanceOf(from); |
||||
uint256 balanceOfToBefore = balanceOf(to); |
||||
uint256 balanceOfOtherBefore = balanceOf(otherAccount); |
||||
address ownerBefore = unsafeOwnerOf(tokenId); |
||||
address otherOwnerBefore = unsafeOwnerOf(otherTokenId); |
||||
address approvalBefore = unsafeGetApproved(tokenId); |
||||
address otherApprovalBefore = unsafeGetApproved(otherTokenId); |
||||
|
||||
transferFrom@withrevert(e, from, to, tokenId); |
||||
bool success = !lastReverted; |
||||
|
||||
// liveness |
||||
assert success <=> ( |
||||
from == ownerBefore && |
||||
from != 0 && |
||||
to != 0 && |
||||
(operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator)) |
||||
); |
||||
|
||||
// effect |
||||
assert success => ( |
||||
balanceOf(from) == balanceOfFromBefore - to_uint256(from != to ? 1 : 0) && |
||||
balanceOf(to) == balanceOfToBefore + to_uint256(from != to ? 1 : 0) && |
||||
unsafeOwnerOf(tokenId) == to && |
||||
unsafeGetApproved(tokenId) == 0 |
||||
); |
||||
|
||||
// no side effect |
||||
assert balanceOf(otherAccount) != balanceOfOtherBefore => (otherAccount == from || otherAccount == to); |
||||
assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore => otherTokenId == tokenId; |
||||
assert unsafeGetApproved(otherTokenId) != otherApprovalBefore => otherTokenId == tokenId; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: safeTransferFrom behavior and side effects │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId) filtered { f -> |
||||
f.selector == safeTransferFrom(address,address,uint256).selector || |
||||
f.selector == safeTransferFrom(address,address,uint256,bytes).selector |
||||
} { |
||||
require nonpayable(e); |
||||
|
||||
address operator = e.msg.sender; |
||||
uint256 otherTokenId; |
||||
address otherAccount; |
||||
|
||||
requireInvariant ownerHasBalance(tokenId); |
||||
require balanceLimited(to); |
||||
|
||||
uint256 balanceOfFromBefore = balanceOf(from); |
||||
uint256 balanceOfToBefore = balanceOf(to); |
||||
uint256 balanceOfOtherBefore = balanceOf(otherAccount); |
||||
address ownerBefore = unsafeOwnerOf(tokenId); |
||||
address otherOwnerBefore = unsafeOwnerOf(otherTokenId); |
||||
address approvalBefore = unsafeGetApproved(tokenId); |
||||
address otherApprovalBefore = unsafeGetApproved(otherTokenId); |
||||
|
||||
helperTransferWithRevert(e, f, from, to, tokenId); |
||||
bool success = !lastReverted; |
||||
|
||||
assert success <=> ( |
||||
from == ownerBefore && |
||||
from != 0 && |
||||
to != 0 && |
||||
(operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator)) |
||||
); |
||||
|
||||
// effect |
||||
assert success => ( |
||||
balanceOf(from) == balanceOfFromBefore - to_uint256(from != to ? 1: 0) && |
||||
balanceOf(to) == balanceOfToBefore + to_uint256(from != to ? 1: 0) && |
||||
unsafeOwnerOf(tokenId) == to && |
||||
unsafeGetApproved(tokenId) == 0 |
||||
); |
||||
|
||||
// no side effect |
||||
assert balanceOf(otherAccount) != balanceOfOtherBefore => (otherAccount == from || otherAccount == to); |
||||
assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore => otherTokenId == tokenId; |
||||
assert unsafeGetApproved(otherTokenId) != otherApprovalBefore => otherTokenId == tokenId; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: mint behavior and side effects │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule mint(env e, address to, uint256 tokenId) { |
||||
require nonpayable(e); |
||||
requireInvariant notMintedUnset(tokenId); |
||||
|
||||
uint256 otherTokenId; |
||||
address otherAccount; |
||||
|
||||
require balanceLimited(to); |
||||
|
||||
uint256 supplyBefore = ownedTotal(); |
||||
uint256 balanceOfToBefore = balanceOf(to); |
||||
uint256 balanceOfOtherBefore = balanceOf(otherAccount); |
||||
address ownerBefore = unsafeOwnerOf(tokenId); |
||||
address otherOwnerBefore = unsafeOwnerOf(otherTokenId); |
||||
|
||||
mint@withrevert(e, to, tokenId); |
||||
bool success = !lastReverted; |
||||
|
||||
// liveness |
||||
assert success <=> ( |
||||
ownerBefore == 0 && |
||||
to != 0 |
||||
); |
||||
|
||||
// effect |
||||
assert success => ( |
||||
ownedTotal() == supplyBefore + 1 && |
||||
balanceOf(to) == balanceOfToBefore + 1 && |
||||
unsafeOwnerOf(tokenId) == to |
||||
); |
||||
|
||||
// no side effect |
||||
assert balanceOf(otherAccount) != balanceOfOtherBefore => otherAccount == to; |
||||
assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore => otherTokenId == tokenId; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: safeMint behavior and side effects │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f -> |
||||
f.selector == safeMint(address,uint256).selector || |
||||
f.selector == safeMint(address,uint256,bytes).selector |
||||
} { |
||||
require nonpayable(e); |
||||
requireInvariant notMintedUnset(tokenId); |
||||
|
||||
uint256 otherTokenId; |
||||
address otherAccount; |
||||
|
||||
require balanceLimited(to); |
||||
|
||||
uint256 supplyBefore = ownedTotal(); |
||||
uint256 balanceOfToBefore = balanceOf(to); |
||||
uint256 balanceOfOtherBefore = balanceOf(otherAccount); |
||||
address ownerBefore = unsafeOwnerOf(tokenId); |
||||
address otherOwnerBefore = unsafeOwnerOf(otherTokenId); |
||||
|
||||
helperMintWithRevert(e, f, to, tokenId); |
||||
bool success = !lastReverted; |
||||
|
||||
assert success <=> ( |
||||
ownerBefore == 0 && |
||||
to != 0 |
||||
); |
||||
|
||||
// effect |
||||
assert success => ( |
||||
ownedTotal() == supplyBefore + 1 && |
||||
balanceOf(to) == balanceOfToBefore + 1 && |
||||
unsafeOwnerOf(tokenId) == to |
||||
); |
||||
|
||||
// no side effect |
||||
assert balanceOf(otherAccount) != balanceOfOtherBefore => otherAccount == to; |
||||
assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore => otherTokenId == tokenId; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: burn behavior and side effects │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule burn(env e, uint256 tokenId) { |
||||
require nonpayable(e); |
||||
|
||||
address from = unsafeOwnerOf(tokenId); |
||||
uint256 otherTokenId; |
||||
address otherAccount; |
||||
|
||||
requireInvariant ownerHasBalance(tokenId); |
||||
|
||||
uint256 supplyBefore = ownedTotal(); |
||||
uint256 balanceOfFromBefore = balanceOf(from); |
||||
uint256 balanceOfOtherBefore = balanceOf(otherAccount); |
||||
address ownerBefore = unsafeOwnerOf(tokenId); |
||||
address otherOwnerBefore = unsafeOwnerOf(otherTokenId); |
||||
address otherApprovalBefore = unsafeGetApproved(otherTokenId); |
||||
|
||||
burn@withrevert(e, tokenId); |
||||
bool success = !lastReverted; |
||||
|
||||
// liveness |
||||
assert success <=> ( |
||||
ownerBefore != 0 |
||||
); |
||||
|
||||
// effect |
||||
assert success => ( |
||||
ownedTotal() == supplyBefore - 1 && |
||||
balanceOf(from) == balanceOfFromBefore - 1 && |
||||
unsafeOwnerOf(tokenId) == 0 && |
||||
unsafeGetApproved(tokenId) == 0 |
||||
); |
||||
|
||||
// no side effect |
||||
assert balanceOf(otherAccount) != balanceOfOtherBefore => otherAccount == from; |
||||
assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore => otherTokenId == tokenId; |
||||
assert unsafeGetApproved(otherTokenId) != otherApprovalBefore => otherTokenId == tokenId; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: approve behavior and side effects │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule approve(env e, address spender, uint256 tokenId) { |
||||
require nonpayable(e); |
||||
|
||||
address caller = e.msg.sender; |
||||
address owner = unsafeOwnerOf(tokenId); |
||||
uint256 otherTokenId; |
||||
|
||||
address otherApprovalBefore = unsafeGetApproved(otherTokenId); |
||||
|
||||
approve@withrevert(e, spender, tokenId); |
||||
bool success = !lastReverted; |
||||
|
||||
// liveness |
||||
assert success <=> ( |
||||
owner != 0 && |
||||
owner != spender && |
||||
(owner == caller || isApprovedForAll(owner, caller)) |
||||
); |
||||
|
||||
// effect |
||||
assert success => unsafeGetApproved(tokenId) == spender; |
||||
|
||||
// no side effect |
||||
assert unsafeGetApproved(otherTokenId) != otherApprovalBefore => otherTokenId == tokenId; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: setApprovalForAll behavior and side effects │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule setApprovalForAll(env e, address operator, bool approved) { |
||||
require nonpayable(e); |
||||
|
||||
address owner = e.msg.sender; |
||||
address otherOwner; |
||||
address otherOperator; |
||||
|
||||
bool otherIsApprovedForAllBefore = isApprovedForAll(otherOwner, otherOperator); |
||||
|
||||
setApprovalForAll@withrevert(e, operator, approved); |
||||
bool success = !lastReverted; |
||||
|
||||
// liveness |
||||
assert success <=> owner != operator; |
||||
|
||||
// effect |
||||
assert success => isApprovedForAll(owner, operator) == approved; |
||||
|
||||
// no side effect |
||||
assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => ( |
||||
otherOwner == owner && |
||||
otherOperator == operator |
||||
); |
||||
} |
@ -0,0 +1,96 @@ |
||||
import "helpers.spec" |
||||
|
||||
methods { |
||||
paused() returns (bool) envfree |
||||
pause() |
||||
unpause() |
||||
onlyWhenPaused() |
||||
onlyWhenNotPaused() |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Function correctness: _pause pauses the contract │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule pause(env e) { |
||||
require nonpayable(e); |
||||
|
||||
bool pausedBefore = paused(); |
||||
|
||||
pause@withrevert(e); |
||||
bool success = !lastReverted; |
||||
|
||||
bool pausedAfter = paused(); |
||||
|
||||
// liveness |
||||
assert success <=> !pausedBefore, "works if and only if the contract was not paused before"; |
||||
|
||||
// effect |
||||
assert success => pausedAfter, "contract must be paused after a successful call"; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Function correctness: _unpause unpauses the contract │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule unpause(env e) { |
||||
require nonpayable(e); |
||||
|
||||
bool pausedBefore = paused(); |
||||
|
||||
unpause@withrevert(e); |
||||
bool success = !lastReverted; |
||||
|
||||
bool pausedAfter = paused(); |
||||
|
||||
// liveness |
||||
assert success <=> pausedBefore, "works if and only if the contract was paused before"; |
||||
|
||||
// effect |
||||
assert success => !pausedAfter, "contract must be unpaused after a successful call"; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Function correctness: whenPaused modifier can only be called if the contract is paused │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule whenPaused(env e) { |
||||
require nonpayable(e); |
||||
|
||||
onlyWhenPaused@withrevert(e); |
||||
assert !lastReverted <=> paused(), "works if and only if the contract is paused"; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Function correctness: whenNotPaused modifier can only be called if the contract is not paused │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule whenNotPaused(env e) { |
||||
require nonpayable(e); |
||||
|
||||
onlyWhenNotPaused@withrevert(e); |
||||
assert !lastReverted <=> !paused(), "works if and only if the contract is not paused"; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rules: only _pause and _unpause can change paused status │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule noPauseChange(env e) { |
||||
method f; |
||||
calldataarg args; |
||||
|
||||
bool pausedBefore = paused(); |
||||
f(e, args); |
||||
bool pausedAfter = paused(); |
||||
|
||||
assert pausedBefore != pausedAfter => ( |
||||
(!pausedAfter && f.selector == unpause().selector) || |
||||
(pausedAfter && f.selector == pause().selector) |
||||
), "contract's paused status can only be changed by _pause() or _unpause()"; |
||||
} |
@ -0,0 +1,275 @@ |
||||
import "helpers.spec" |
||||
import "methods/IAccessControl.spec" |
||||
|
||||
methods { |
||||
TIMELOCK_ADMIN_ROLE() returns (bytes32) envfree |
||||
PROPOSER_ROLE() returns (bytes32) envfree |
||||
EXECUTOR_ROLE() returns (bytes32) envfree |
||||
CANCELLER_ROLE() returns (bytes32) envfree |
||||
isOperation(bytes32) returns (bool) envfree |
||||
isOperationPending(bytes32) returns (bool) envfree |
||||
isOperationReady(bytes32) returns (bool) |
||||
isOperationDone(bytes32) returns (bool) envfree |
||||
getTimestamp(bytes32) returns (uint256) envfree |
||||
getMinDelay() returns (uint256) envfree |
||||
|
||||
hashOperation(address, uint256, bytes, bytes32, bytes32) returns(bytes32) envfree |
||||
hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) returns(bytes32) envfree |
||||
|
||||
schedule(address, uint256, bytes, bytes32, bytes32, uint256) |
||||
scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) |
||||
execute(address, uint256, bytes, bytes32, bytes32) |
||||
executeBatch(address[], uint256[], bytes[], bytes32, bytes32) |
||||
cancel(bytes32) |
||||
|
||||
updateDelay(uint256) |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Helpers │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
// Uniformly handle scheduling of batched and non-batched operations. |
||||
function helperScheduleWithRevert(env e, method f, bytes32 id, uint256 delay) { |
||||
if (f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector) { |
||||
address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; |
||||
require hashOperation(target, value, data, predecessor, salt) == id; // Correlation |
||||
schedule@withrevert(e, target, value, data, predecessor, salt, delay); |
||||
} else if (f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector) { |
||||
address[] targets; uint256[] values; bytes[] payloads; bytes32 predecessor; bytes32 salt; |
||||
require hashOperationBatch(targets, values, payloads, predecessor, salt) == id; // Correlation |
||||
scheduleBatch@withrevert(e, targets, values, payloads, predecessor, salt, delay); |
||||
} else { |
||||
calldataarg args; |
||||
f@withrevert(e, args); |
||||
} |
||||
} |
||||
|
||||
// Uniformly handle execution of batched and non-batched operations. |
||||
function helperExecuteWithRevert(env e, method f, bytes32 id, bytes32 predecessor) { |
||||
if (f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector) { |
||||
address target; uint256 value; bytes data; bytes32 salt; |
||||
require hashOperation(target, value, data, predecessor, salt) == id; // Correlation |
||||
execute@withrevert(e, target, value, data, predecessor, salt); |
||||
} else if (f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector) { |
||||
address[] targets; uint256[] values; bytes[] payloads; bytes32 salt; |
||||
require hashOperationBatch(targets, values, payloads, predecessor, salt) == id; // Correlation |
||||
executeBatch@withrevert(e, targets, values, payloads, predecessor, salt); |
||||
} else { |
||||
calldataarg args; |
||||
f@withrevert(e, args); |
||||
} |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Definitions │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
definition DONE_TIMESTAMP() returns uint256 = 1; |
||||
definition UNSET() returns uint8 = 0x1; |
||||
definition PENDING() returns uint8 = 0x2; |
||||
definition DONE() returns uint8 = 0x4; |
||||
|
||||
definition isUnset(bytes32 id) returns bool = !isOperation(id); |
||||
definition isPending(bytes32 id) returns bool = isOperationPending(id); |
||||
definition isDone(bytes32 id) returns bool = isOperationDone(id); |
||||
definition state(bytes32 id) returns uint8 = (isUnset(id) ? UNSET() : 0) | (isPending(id) ? PENDING() : 0) | (isDone(id) ? DONE() : 0); |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Invariants: consistency of accessors │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
invariant isOperationCheck(bytes32 id) |
||||
isOperation(id) <=> getTimestamp(id) > 0 |
||||
filtered { f -> !f.isView } |
||||
|
||||
invariant isOperationPendingCheck(bytes32 id) |
||||
isOperationPending(id) <=> getTimestamp(id) > DONE_TIMESTAMP() |
||||
filtered { f -> !f.isView } |
||||
|
||||
invariant isOperationDoneCheck(bytes32 id) |
||||
isOperationDone(id) <=> getTimestamp(id) == DONE_TIMESTAMP() |
||||
filtered { f -> !f.isView } |
||||
|
||||
invariant isOperationReadyCheck(env e, bytes32 id) |
||||
isOperationReady(e, id) <=> (isOperationPending(id) && getTimestamp(id) <= e.block.timestamp) |
||||
filtered { f -> !f.isView } |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Invariant: a proposal id is either unset, pending or done │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
invariant stateConsistency(bytes32 id, env e) |
||||
// Check states are mutually exclusive |
||||
(isUnset(id) <=> (!isPending(id) && !isDone(id) )) && |
||||
(isPending(id) <=> (!isUnset(id) && !isDone(id) )) && |
||||
(isDone(id) <=> (!isUnset(id) && !isPending(id))) && |
||||
// Check that the state helper behaves as expected: |
||||
(isUnset(id) <=> state(id) == UNSET() ) && |
||||
(isPending(id) <=> state(id) == PENDING() ) && |
||||
(isDone(id) <=> state(id) == DONE() ) && |
||||
// Check substate |
||||
isOperationReady(e, id) => isPending(id) |
||||
filtered { f -> !f.isView } |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: state transition rules │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule stateTransition(bytes32 id, env e, method f, calldataarg args) { |
||||
require e.block.timestamp > 1; // Sanity |
||||
|
||||
uint8 stateBefore = state(id); |
||||
f(e, args); |
||||
uint8 stateAfter = state(id); |
||||
|
||||
// Cannot jump from UNSET to DONE |
||||
assert stateBefore == UNSET() => stateAfter != DONE(); |
||||
|
||||
// UNSET → PENDING: schedule or scheduleBatch |
||||
assert stateBefore == UNSET() && stateAfter == PENDING() => ( |
||||
f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector || |
||||
f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector |
||||
); |
||||
|
||||
// PENDING → UNSET: cancel |
||||
assert stateBefore == PENDING() && stateAfter == UNSET() => ( |
||||
f.selector == cancel(bytes32).selector |
||||
); |
||||
|
||||
// PENDING → DONE: execute or executeBatch |
||||
assert stateBefore == PENDING() && stateAfter == DONE() => ( |
||||
f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector || |
||||
f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector |
||||
); |
||||
|
||||
// DONE is final |
||||
assert stateBefore == DONE() => stateAfter == DONE(); |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: minimum delay can only be updated through a timelock execution │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule minDelayOnlyChange(env e) { |
||||
uint256 delayBefore = getMinDelay(); |
||||
|
||||
method f; calldataarg args; |
||||
f(e, args); |
||||
|
||||
assert delayBefore != getMinDelay() => (e.msg.sender == currentContract && f.selector == updateDelay(uint256).selector), "Unauthorized delay update"; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: schedule liveness and effects │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f -> |
||||
f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector || |
||||
f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector |
||||
} { |
||||
require nonpayable(e); |
||||
|
||||
// Basic timestamp assumptions |
||||
require e.block.timestamp > 1; |
||||
require e.block.timestamp + delay < max_uint256; |
||||
require e.block.timestamp + getMinDelay() < max_uint256; |
||||
|
||||
bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId); |
||||
|
||||
uint8 stateBefore = state(id); |
||||
bool isDelaySufficient = delay >= getMinDelay(); |
||||
bool isProposerBefore = hasRole(PROPOSER_ROLE(), e.msg.sender); |
||||
|
||||
helperScheduleWithRevert(e, f, id, delay); |
||||
bool success = !lastReverted; |
||||
|
||||
// liveness |
||||
assert success <=> ( |
||||
stateBefore == UNSET() && |
||||
isDelaySufficient && |
||||
isProposerBefore |
||||
); |
||||
|
||||
// effect |
||||
assert success => state(id) == PENDING(), "State transition violation"; |
||||
assert success => getTimestamp(id) == to_uint256(e.block.timestamp + delay), "Proposal timestamp not correctly set"; |
||||
|
||||
// no side effect |
||||
assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected"; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: execute liveness and effects │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule execute(env e, method f, bytes32 id, bytes32 predecessor) filtered { f -> |
||||
f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector || |
||||
f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector |
||||
} { |
||||
bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId); |
||||
|
||||
uint8 stateBefore = state(id); |
||||
bool isOperationReadyBefore = isOperationReady(e, id); |
||||
bool isExecutorOrOpen = hasRole(EXECUTOR_ROLE(), e.msg.sender) || hasRole(EXECUTOR_ROLE(), 0); |
||||
bool predecessorDependency = predecessor == 0 || isDone(predecessor); |
||||
|
||||
helperExecuteWithRevert(e, f, id, predecessor); |
||||
bool success = !lastReverted; |
||||
|
||||
// The underlying transaction can revert, and that would cause the execution to revert. We can check that all non |
||||
// reverting calls meet the requirements in terms of proposal readiness, access control and predecessor dependency. |
||||
// We can't however guarantee that these requirements being meet ensure liveness of the proposal, because the |
||||
// proposal can revert for reasons beyond our control. |
||||
|
||||
// liveness, should be `<=>` but can only check `=>` (see comment above) |
||||
assert success => ( |
||||
stateBefore == PENDING() && |
||||
isOperationReadyBefore && |
||||
predecessorDependency && |
||||
isExecutorOrOpen |
||||
); |
||||
|
||||
// effect |
||||
assert success => state(id) == DONE(), "State transition violation"; |
||||
|
||||
// no side effect |
||||
assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected"; |
||||
} |
||||
|
||||
/* |
||||
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ |
||||
│ Rule: cancel liveness and effects │ |
||||
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
||||
*/ |
||||
rule cancel(env e, bytes32 id) { |
||||
require nonpayable(e); |
||||
|
||||
bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId); |
||||
|
||||
uint8 stateBefore = state(id); |
||||
bool isCanceller = hasRole(CANCELLER_ROLE(), e.msg.sender); |
||||
|
||||
cancel@withrevert(e, id); |
||||
bool success = !lastReverted; |
||||
|
||||
// liveness |
||||
assert success <=> ( |
||||
stateBefore == PENDING() && |
||||
isCanceller |
||||
); |
||||
|
||||
// effect |
||||
assert success => state(id) == UNSET(), "State transition violation"; |
||||
|
||||
// no side effect |
||||
assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected"; |
||||
} |
@ -0,0 +1,7 @@ |
||||
methods { |
||||
hasRole(bytes32, address) returns(bool) envfree |
||||
getRoleAdmin(bytes32) returns(bytes32) envfree |
||||
grantRole(bytes32, address) |
||||
revokeRole(bytes32, address) |
||||
renounceRole(bytes32, address) |
||||
} |
@ -0,0 +1,20 @@ |
||||
methods { |
||||
// IERC721 |
||||
balanceOf(address) returns (uint256) envfree => DISPATCHER(true) |
||||
ownerOf(uint256) returns (address) envfree => DISPATCHER(true) |
||||
getApproved(uint256) returns (address) envfree => DISPATCHER(true) |
||||
isApprovedForAll(address,address) returns (bool) envfree => DISPATCHER(true) |
||||
safeTransferFrom(address,address,uint256,bytes) => DISPATCHER(true) |
||||
safeTransferFrom(address,address,uint256) => DISPATCHER(true) |
||||
transferFrom(address,address,uint256) => DISPATCHER(true) |
||||
approve(address,uint256) => DISPATCHER(true) |
||||
setApprovalForAll(address,bool) => DISPATCHER(true) |
||||
|
||||
// IERC721Metadata |
||||
name() returns (string) => DISPATCHER(true) |
||||
symbol() returns (string) => DISPATCHER(true) |
||||
tokenURI(uint256) returns (string) => DISPATCHER(true) |
||||
|
||||
// IERC721Receiver |
||||
onERC721Received(address,address,uint256,bytes) returns (bytes4) => DISPATCHER(true) |
||||
} |
@ -0,0 +1,25 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
|
||||
pragma solidity ^0.8.0; |
||||
|
||||
/** |
||||
* @dev ERC-1967: Proxy Storage Slots. This interface contains the events defined in the ERC. |
||||
* |
||||
* _Available since v4.8.3._ |
||||
*/ |
||||
interface IERC1967 { |
||||
/** |
||||
* @dev Emitted when the implementation is upgraded. |
||||
*/ |
||||
event Upgraded(address indexed implementation); |
||||
|
||||
/** |
||||
* @dev Emitted when the admin account has changed. |
||||
*/ |
||||
event AdminChanged(address previousAdmin, address newAdmin); |
||||
|
||||
/** |
||||
* @dev Emitted when the beacon is changed. |
||||
*/ |
||||
event BeaconUpgraded(address indexed beacon); |
||||
} |
@ -0,0 +1,9 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
|
||||
pragma solidity ^0.8.0; |
||||
|
||||
contract ERC20ExcessDecimalsMock { |
||||
function decimals() public pure returns (uint256) { |
||||
return type(uint256).max; |
||||
} |
||||
} |
@ -1,3 +1,3 @@ |
||||
[fuzz] |
||||
runs = 10000 |
||||
max_test_rejects = 100000 |
||||
max_test_rejects = 150000 |
||||
|
@ -1 +1 @@ |
||||
Subproject commit eb980e1d4f0e8173ec27da77297ae411840c8ccb |
||||
Subproject commit c2236853aadb8e2d9909bbecdc490099519b70a4 |
File diff suppressed because it is too large
Load Diff
@ -0,0 +1 @@ |
||||
openzeppelin/=contracts/ |
@ -1 +1 @@ |
||||
certora-cli==3.6.3 |
||||
certora-cli==3.6.4 |
||||
|
@ -0,0 +1,22 @@ |
||||
// OPTIONS
|
||||
const VALUE_SIZES = [224, 160]; |
||||
|
||||
const defaultOpts = size => ({ |
||||
historyTypeName: `Trace${size}`, |
||||
checkpointTypeName: `Checkpoint${size}`, |
||||
checkpointFieldName: '_checkpoints', |
||||
keyTypeName: `uint${256 - size}`, |
||||
keyFieldName: '_key', |
||||
valueTypeName: `uint${size}`, |
||||
valueFieldName: '_value', |
||||
}); |
||||
|
||||
module.exports = { |
||||
OPTS: VALUE_SIZES.map(size => defaultOpts(size)), |
||||
LEGACY_OPTS: { |
||||
...defaultOpts(224), |
||||
historyTypeName: 'History', |
||||
checkpointTypeName: 'Checkpoint', |
||||
keyFieldName: '_blockNumber', |
||||
}, |
||||
}; |
@ -0,0 +1,256 @@ |
||||
const format = require('../format-lines'); |
||||
const { capitalize } = require('../../helpers'); |
||||
const { OPTS, LEGACY_OPTS } = require('./Checkpoints.opts.js'); |
||||
|
||||
// TEMPLATE
|
||||
const header = `\
|
||||
pragma solidity ^0.8.0; |
||||
|
||||
import "forge-std/Test.sol"; |
||||
import "../../contracts/utils/Checkpoints.sol"; |
||||
import "../../contracts/utils/math/SafeCast.sol"; |
||||
`;
|
||||
|
||||
/* eslint-disable max-len */ |
||||
const common = opts => `\
|
||||
using Checkpoints for Checkpoints.${opts.historyTypeName}; |
||||
|
||||
// Maximum gap between keys used during the fuzzing tests: the \`_prepareKeys\` function with make sure that
|
||||
// key#n+1 is in the [key#n, key#n + _KEY_MAX_GAP] range.
|
||||
uint8 internal constant _KEY_MAX_GAP = 64; |
||||
|
||||
Checkpoints.${opts.historyTypeName} internal _ckpts; |
||||
|
||||
// helpers
|
||||
function _bound${capitalize(opts.keyTypeName)}( |
||||
${opts.keyTypeName} x, |
||||
${opts.keyTypeName} min, |
||||
${opts.keyTypeName} max |
||||
) internal view returns (${opts.keyTypeName}) { |
||||
return SafeCast.to${capitalize(opts.keyTypeName)}(bound(uint256(x), uint256(min), uint256(max))); |
||||
} |
||||
|
||||
function _prepareKeys( |
||||
${opts.keyTypeName}[] memory keys, |
||||
${opts.keyTypeName} maxSpread |
||||
) internal view { |
||||
${opts.keyTypeName} lastKey = 0; |
||||
for (uint256 i = 0; i < keys.length; ++i) { |
||||
${opts.keyTypeName} key = _bound${capitalize(opts.keyTypeName)}(keys[i], lastKey, lastKey + maxSpread); |
||||
keys[i] = key; |
||||
lastKey = key; |
||||
} |
||||
} |
||||
|
||||
function _assertLatestCheckpoint( |
||||
bool exist, |
||||
${opts.keyTypeName} key, |
||||
${opts.valueTypeName} value |
||||
) internal { |
||||
(bool _exist, ${opts.keyTypeName} _key, ${opts.valueTypeName} _value) = _ckpts.latestCheckpoint(); |
||||
assertEq(_exist, exist); |
||||
assertEq(_key, key); |
||||
assertEq(_value, value); |
||||
} |
||||
`;
|
||||
|
||||
const testTrace = opts => `\
|
||||
// tests
|
||||
function testPush( |
||||
${opts.keyTypeName}[] memory keys, |
||||
${opts.valueTypeName}[] memory values, |
||||
${opts.keyTypeName} pastKey |
||||
) public { |
||||
vm.assume(values.length > 0 && values.length <= keys.length); |
||||
_prepareKeys(keys, _KEY_MAX_GAP); |
||||
|
||||
// initial state
|
||||
assertEq(_ckpts.length(), 0); |
||||
assertEq(_ckpts.latest(), 0); |
||||
_assertLatestCheckpoint(false, 0, 0); |
||||
|
||||
uint256 duplicates = 0; |
||||
for (uint256 i = 0; i < keys.length; ++i) { |
||||
${opts.keyTypeName} key = keys[i]; |
||||
${opts.valueTypeName} value = values[i % values.length]; |
||||
if (i > 0 && key == keys[i-1]) ++duplicates; |
||||
|
||||
// push
|
||||
_ckpts.push(key, value); |
||||
|
||||
// check length & latest
|
||||
assertEq(_ckpts.length(), i + 1 - duplicates); |
||||
assertEq(_ckpts.latest(), value); |
||||
_assertLatestCheckpoint(true, key, value); |
||||
} |
||||
|
||||
if (keys.length > 0) { |
||||
${opts.keyTypeName} lastKey = keys[keys.length - 1]; |
||||
if (lastKey > 0) { |
||||
pastKey = _bound${capitalize(opts.keyTypeName)}(pastKey, 0, lastKey - 1); |
||||
|
||||
vm.expectRevert(); |
||||
this.push(pastKey, values[keys.length % values.length]); |
||||
} |
||||
} |
||||
} |
||||
|
||||
// used to test reverts
|
||||
function push(${opts.keyTypeName} key, ${opts.valueTypeName} value) external { |
||||
_ckpts.push(key, value); |
||||
} |
||||
|
||||
function testLookup( |
||||
${opts.keyTypeName}[] memory keys, |
||||
${opts.valueTypeName}[] memory values, |
||||
${opts.keyTypeName} lookup |
||||
) public { |
||||
vm.assume(values.length > 0 && values.length <= keys.length); |
||||
_prepareKeys(keys, _KEY_MAX_GAP); |
||||
|
||||
${opts.keyTypeName} lastKey = keys.length == 0 ? 0 : keys[keys.length - 1]; |
||||
lookup = _bound${capitalize(opts.keyTypeName)}(lookup, 0, lastKey + _KEY_MAX_GAP); |
||||
|
||||
${opts.valueTypeName} upper = 0; |
||||
${opts.valueTypeName} lower = 0; |
||||
${opts.keyTypeName} lowerKey = type(${opts.keyTypeName}).max; |
||||
for (uint256 i = 0; i < keys.length; ++i) { |
||||
${opts.keyTypeName} key = keys[i]; |
||||
${opts.valueTypeName} value = values[i % values.length]; |
||||
|
||||
// push
|
||||
_ckpts.push(key, value); |
||||
|
||||
// track expected result of lookups
|
||||
if (key <= lookup) { |
||||
upper = value; |
||||
} |
||||
// find the first key that is not smaller than the lookup key
|
||||
if (key >= lookup && (i == 0 || keys[i-1] < lookup)) { |
||||
lowerKey = key; |
||||
} |
||||
if (key == lowerKey) { |
||||
lower = value; |
||||
} |
||||
} |
||||
|
||||
// check lookup
|
||||
assertEq(_ckpts.lowerLookup(lookup), lower); |
||||
assertEq(_ckpts.upperLookup(lookup), upper); |
||||
assertEq(_ckpts.upperLookupRecent(lookup), upper); |
||||
} |
||||
`;
|
||||
|
||||
const testHistory = opts => `\
|
||||
// tests
|
||||
function testPush( |
||||
${opts.keyTypeName}[] memory keys, |
||||
${opts.valueTypeName}[] memory values, |
||||
${opts.keyTypeName} pastKey |
||||
) public { |
||||
vm.assume(values.length > 0 && values.length <= keys.length); |
||||
_prepareKeys(keys, _KEY_MAX_GAP); |
||||
|
||||
// initial state
|
||||
assertEq(_ckpts.length(), 0); |
||||
assertEq(_ckpts.latest(), 0); |
||||
_assertLatestCheckpoint(false, 0, 0); |
||||
|
||||
uint256 duplicates = 0; |
||||
for (uint256 i = 0; i < keys.length; ++i) { |
||||
${opts.keyTypeName} key = keys[i]; |
||||
${opts.valueTypeName} value = values[i % values.length]; |
||||
if (i > 0 && key == keys[i - 1]) ++duplicates; |
||||
|
||||
// push
|
||||
vm.roll(key); |
||||
_ckpts.push(value); |
||||
|
||||
// check length & latest
|
||||
assertEq(_ckpts.length(), i + 1 - duplicates); |
||||
assertEq(_ckpts.latest(), value); |
||||
_assertLatestCheckpoint(true, key, value); |
||||
} |
||||
|
||||
// Can't push any key in the past
|
||||
if (keys.length > 0) { |
||||
${opts.keyTypeName} lastKey = keys[keys.length - 1]; |
||||
if (lastKey > 0) { |
||||
pastKey = _bound${capitalize(opts.keyTypeName)}(pastKey, 0, lastKey - 1); |
||||
|
||||
vm.roll(pastKey); |
||||
vm.expectRevert(); |
||||
this.push(values[keys.length % values.length]); |
||||
} |
||||
} |
||||
} |
||||
|
||||
// used to test reverts
|
||||
function push(${opts.valueTypeName} value) external { |
||||
_ckpts.push(value); |
||||
} |
||||
|
||||
function testLookup( |
||||
${opts.keyTypeName}[] memory keys, |
||||
${opts.valueTypeName}[] memory values, |
||||
${opts.keyTypeName} lookup |
||||
) public { |
||||
vm.assume(keys.length > 0); |
||||
vm.assume(values.length > 0 && values.length <= keys.length); |
||||
_prepareKeys(keys, _KEY_MAX_GAP); |
||||
|
||||
${opts.keyTypeName} lastKey = keys[keys.length - 1]; |
||||
vm.assume(lastKey > 0); |
||||
lookup = _bound${capitalize(opts.keyTypeName)}(lookup, 0, lastKey - 1); |
||||
|
||||
${opts.valueTypeName} upper = 0; |
||||
for (uint256 i = 0; i < keys.length; ++i) { |
||||
${opts.keyTypeName} key = keys[i]; |
||||
${opts.valueTypeName} value = values[i % values.length]; |
||||
|
||||
// push
|
||||
vm.roll(key); |
||||
_ckpts.push(value); |
||||
|
||||
// track expected result of lookups
|
||||
if (key <= lookup) { |
||||
upper = value; |
||||
} |
||||
} |
||||
|
||||
// check lookup
|
||||
assertEq(_ckpts.getAtBlock(lookup), upper); |
||||
assertEq(_ckpts.getAtProbablyRecentBlock(lookup), upper); |
||||
|
||||
vm.expectRevert(); this.getAtBlock(lastKey); |
||||
vm.expectRevert(); this.getAtBlock(lastKey + 1); |
||||
vm.expectRevert(); this.getAtProbablyRecentBlock(lastKey); |
||||
vm.expectRevert(); this.getAtProbablyRecentBlock(lastKey + 1); |
||||
} |
||||
|
||||
// used to test reverts
|
||||
function getAtBlock(${opts.keyTypeName} key) external view { |
||||
_ckpts.getAtBlock(key); |
||||
} |
||||
|
||||
// used to test reverts
|
||||
function getAtProbablyRecentBlock(${opts.keyTypeName} key) external view { |
||||
_ckpts.getAtProbablyRecentBlock(key); |
||||
} |
||||
`;
|
||||
/* eslint-enable max-len */ |
||||
|
||||
// GENERATE
|
||||
module.exports = format( |
||||
header, |
||||
// HISTORY
|
||||
`contract Checkpoints${LEGACY_OPTS.historyTypeName}Test is Test {`, |
||||
[common(LEGACY_OPTS), testHistory(LEGACY_OPTS)], |
||||
'}', |
||||
// TRACEXXX
|
||||
...OPTS.flatMap(opts => [ |
||||
`contract Checkpoints${opts.historyTypeName}Test is Test {`, |
||||
[common(opts), testTrace(opts)], |
||||
'}', |
||||
]), |
||||
); |
@ -1,18 +1,42 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
pragma solidity ^0.8.0; |
||||
|
||||
import "erc4626-tests/ERC4626.test.sol"; |
||||
import {ERC4626Test} from "erc4626-tests/ERC4626.test.sol"; |
||||
|
||||
import {SafeCast} from "../../../../contracts/utils/math/SafeCast.sol"; |
||||
import {ERC20Mock} from "../../../../contracts/mocks/ERC20Mock.sol"; |
||||
import {ERC4626Mock} from "../../../../contracts/mocks/ERC4626Mock.sol"; |
||||
import {SafeCast} from "openzeppelin/utils/math/SafeCast.sol"; |
||||
import {ERC20} from "openzeppelin/token/ERC20/ERC20.sol"; |
||||
import {ERC4626} from "openzeppelin/token/ERC20/extensions/ERC4626.sol"; |
||||
|
||||
import {ERC20Mock} from "openzeppelin/mocks/ERC20Mock.sol"; |
||||
import {ERC4626Mock} from "openzeppelin/mocks/ERC4626Mock.sol"; |
||||
import {ERC4626OffsetMock} from "openzeppelin/mocks/token/ERC4626OffsetMock.sol"; |
||||
|
||||
contract ERC4626VaultOffsetMock is ERC4626OffsetMock { |
||||
constructor( |
||||
ERC20 underlying_, |
||||
uint8 offset_ |
||||
) ERC20("My Token Vault", "MTKNV") ERC4626(underlying_) ERC4626OffsetMock(offset_) {} |
||||
} |
||||
|
||||
contract ERC4626StdTest is ERC4626Test { |
||||
ERC20 private _underlying = new ERC20Mock(); |
||||
|
||||
function setUp() public override { |
||||
_underlying_ = address(new ERC20Mock()); |
||||
_underlying_ = address(_underlying); |
||||
_vault_ = address(new ERC4626Mock(_underlying_)); |
||||
_delta_ = 0; |
||||
_vaultMayBeEmpty = true; |
||||
_unlimitedAmount = true; |
||||
} |
||||
|
||||
/** |
||||
* @dev Check the case where calculated `decimals` value overflows the `uint8` type. |
||||
*/ |
||||
function testFuzzDecimalsOverflow(uint8 offset) public { |
||||
/// @dev Remember that the `_underlying` exhibits a `decimals` value of 18. |
||||
offset = uint8(bound(uint256(offset), 238, uint256(type(uint8).max))); |
||||
ERC4626VaultOffsetMock erc4626VaultOffsetMock = new ERC4626VaultOffsetMock(_underlying, offset); |
||||
vm.expectRevert(); |
||||
erc4626VaultOffsetMock.decimals(); |
||||
} |
||||
} |
||||
|
@ -0,0 +1,347 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
// This file was procedurally generated from scripts/generate/templates/Checkpoints.t.js. |
||||
|
||||
pragma solidity ^0.8.0; |
||||
|
||||
import "forge-std/Test.sol"; |
||||
import "../../contracts/utils/Checkpoints.sol"; |
||||
import "../../contracts/utils/math/SafeCast.sol"; |
||||
|
||||
contract CheckpointsHistoryTest is Test { |
||||
using Checkpoints for Checkpoints.History; |
||||
|
||||
// Maximum gap between keys used during the fuzzing tests: the `_prepareKeys` function with make sure that |
||||
// key#n+1 is in the [key#n, key#n + _KEY_MAX_GAP] range. |
||||
uint8 internal constant _KEY_MAX_GAP = 64; |
||||
|
||||
Checkpoints.History internal _ckpts; |
||||
|
||||
// helpers |
||||
function _boundUint32(uint32 x, uint32 min, uint32 max) internal view returns (uint32) { |
||||
return SafeCast.toUint32(bound(uint256(x), uint256(min), uint256(max))); |
||||
} |
||||
|
||||
function _prepareKeys(uint32[] memory keys, uint32 maxSpread) internal view { |
||||
uint32 lastKey = 0; |
||||
for (uint256 i = 0; i < keys.length; ++i) { |
||||
uint32 key = _boundUint32(keys[i], lastKey, lastKey + maxSpread); |
||||
keys[i] = key; |
||||
lastKey = key; |
||||
} |
||||
} |
||||
|
||||
function _assertLatestCheckpoint(bool exist, uint32 key, uint224 value) internal { |
||||
(bool _exist, uint32 _key, uint224 _value) = _ckpts.latestCheckpoint(); |
||||
assertEq(_exist, exist); |
||||
assertEq(_key, key); |
||||
assertEq(_value, value); |
||||
} |
||||
|
||||
// tests |
||||
function testPush(uint32[] memory keys, uint224[] memory values, uint32 pastKey) public { |
||||
vm.assume(values.length > 0 && values.length <= keys.length); |
||||
_prepareKeys(keys, _KEY_MAX_GAP); |
||||
|
||||
// initial state |
||||
assertEq(_ckpts.length(), 0); |
||||
assertEq(_ckpts.latest(), 0); |
||||
_assertLatestCheckpoint(false, 0, 0); |
||||
|
||||
uint256 duplicates = 0; |
||||
for (uint256 i = 0; i < keys.length; ++i) { |
||||
uint32 key = keys[i]; |
||||
uint224 value = values[i % values.length]; |
||||
if (i > 0 && key == keys[i - 1]) ++duplicates; |
||||
|
||||
// push |
||||
vm.roll(key); |
||||
_ckpts.push(value); |
||||
|
||||
// check length & latest |
||||
assertEq(_ckpts.length(), i + 1 - duplicates); |
||||
assertEq(_ckpts.latest(), value); |
||||
_assertLatestCheckpoint(true, key, value); |
||||
} |
||||
|
||||
// Can't push any key in the past |
||||
if (keys.length > 0) { |
||||
uint32 lastKey = keys[keys.length - 1]; |
||||
if (lastKey > 0) { |
||||
pastKey = _boundUint32(pastKey, 0, lastKey - 1); |
||||
|
||||
vm.roll(pastKey); |
||||
vm.expectRevert(); |
||||
this.push(values[keys.length % values.length]); |
||||
} |
||||
} |
||||
} |
||||
|
||||
// used to test reverts |
||||
function push(uint224 value) external { |
||||
_ckpts.push(value); |
||||
} |
||||
|
||||
function testLookup(uint32[] memory keys, uint224[] memory values, uint32 lookup) public { |
||||
vm.assume(keys.length > 0); |
||||
vm.assume(values.length > 0 && values.length <= keys.length); |
||||
_prepareKeys(keys, _KEY_MAX_GAP); |
||||
|
||||
uint32 lastKey = keys[keys.length - 1]; |
||||
vm.assume(lastKey > 0); |
||||
lookup = _boundUint32(lookup, 0, lastKey - 1); |
||||
|
||||
uint224 upper = 0; |
||||
for (uint256 i = 0; i < keys.length; ++i) { |
||||
uint32 key = keys[i]; |
||||
uint224 value = values[i % values.length]; |
||||
|
||||
// push |
||||
vm.roll(key); |
||||
_ckpts.push(value); |
||||
|
||||
// track expected result of lookups |
||||
if (key <= lookup) { |
||||
upper = value; |
||||
} |
||||
} |
||||
|
||||
// check lookup |
||||
assertEq(_ckpts.getAtBlock(lookup), upper); |
||||
assertEq(_ckpts.getAtProbablyRecentBlock(lookup), upper); |
||||
|
||||
vm.expectRevert(); |
||||
this.getAtBlock(lastKey); |
||||
vm.expectRevert(); |
||||
this.getAtBlock(lastKey + 1); |
||||
vm.expectRevert(); |
||||
this.getAtProbablyRecentBlock(lastKey); |
||||
vm.expectRevert(); |
||||
this.getAtProbablyRecentBlock(lastKey + 1); |
||||
} |
||||
|
||||
// used to test reverts |
||||
function getAtBlock(uint32 key) external view { |
||||
_ckpts.getAtBlock(key); |
||||
} |
||||
|
||||
// used to test reverts |
||||
function getAtProbablyRecentBlock(uint32 key) external view { |
||||
_ckpts.getAtProbablyRecentBlock(key); |
||||
} |
||||
} |
||||
|
||||
contract CheckpointsTrace224Test is Test { |
||||
using Checkpoints for Checkpoints.Trace224; |
||||
|
||||
// Maximum gap between keys used during the fuzzing tests: the `_prepareKeys` function with make sure that |
||||
// key#n+1 is in the [key#n, key#n + _KEY_MAX_GAP] range. |
||||
uint8 internal constant _KEY_MAX_GAP = 64; |
||||
|
||||
Checkpoints.Trace224 internal _ckpts; |
||||
|
||||
// helpers |
||||
function _boundUint32(uint32 x, uint32 min, uint32 max) internal view returns (uint32) { |
||||
return SafeCast.toUint32(bound(uint256(x), uint256(min), uint256(max))); |
||||
} |
||||
|
||||
function _prepareKeys(uint32[] memory keys, uint32 maxSpread) internal view { |
||||
uint32 lastKey = 0; |
||||
for (uint256 i = 0; i < keys.length; ++i) { |
||||
uint32 key = _boundUint32(keys[i], lastKey, lastKey + maxSpread); |
||||
keys[i] = key; |
||||
lastKey = key; |
||||
} |
||||
} |
||||
|
||||
function _assertLatestCheckpoint(bool exist, uint32 key, uint224 value) internal { |
||||
(bool _exist, uint32 _key, uint224 _value) = _ckpts.latestCheckpoint(); |
||||
assertEq(_exist, exist); |
||||
assertEq(_key, key); |
||||
assertEq(_value, value); |
||||
} |
||||
|
||||
// tests |
||||
function testPush(uint32[] memory keys, uint224[] memory values, uint32 pastKey) public { |
||||
vm.assume(values.length > 0 && values.length <= keys.length); |
||||
_prepareKeys(keys, _KEY_MAX_GAP); |
||||
|
||||
// initial state |
||||
assertEq(_ckpts.length(), 0); |
||||
assertEq(_ckpts.latest(), 0); |
||||
_assertLatestCheckpoint(false, 0, 0); |
||||
|
||||
uint256 duplicates = 0; |
||||
for (uint256 i = 0; i < keys.length; ++i) { |
||||
uint32 key = keys[i]; |
||||
uint224 value = values[i % values.length]; |
||||
if (i > 0 && key == keys[i - 1]) ++duplicates; |
||||
|
||||
// push |
||||
_ckpts.push(key, value); |
||||
|
||||
// check length & latest |
||||
assertEq(_ckpts.length(), i + 1 - duplicates); |
||||
assertEq(_ckpts.latest(), value); |
||||
_assertLatestCheckpoint(true, key, value); |
||||
} |
||||
|
||||
if (keys.length > 0) { |
||||
uint32 lastKey = keys[keys.length - 1]; |
||||
if (lastKey > 0) { |
||||
pastKey = _boundUint32(pastKey, 0, lastKey - 1); |
||||
|
||||
vm.expectRevert(); |
||||
this.push(pastKey, values[keys.length % values.length]); |
||||
} |
||||
} |
||||
} |
||||
|
||||
// used to test reverts |
||||
function push(uint32 key, uint224 value) external { |
||||
_ckpts.push(key, value); |
||||
} |
||||
|
||||
function testLookup(uint32[] memory keys, uint224[] memory values, uint32 lookup) public { |
||||
vm.assume(values.length > 0 && values.length <= keys.length); |
||||
_prepareKeys(keys, _KEY_MAX_GAP); |
||||
|
||||
uint32 lastKey = keys.length == 0 ? 0 : keys[keys.length - 1]; |
||||
lookup = _boundUint32(lookup, 0, lastKey + _KEY_MAX_GAP); |
||||
|
||||
uint224 upper = 0; |
||||
uint224 lower = 0; |
||||
uint32 lowerKey = type(uint32).max; |
||||
for (uint256 i = 0; i < keys.length; ++i) { |
||||
uint32 key = keys[i]; |
||||
uint224 value = values[i % values.length]; |
||||
|
||||
// push |
||||
_ckpts.push(key, value); |
||||
|
||||
// track expected result of lookups |
||||
if (key <= lookup) { |
||||
upper = value; |
||||
} |
||||
// find the first key that is not smaller than the lookup key |
||||
if (key >= lookup && (i == 0 || keys[i - 1] < lookup)) { |
||||
lowerKey = key; |
||||
} |
||||
if (key == lowerKey) { |
||||
lower = value; |
||||
} |
||||
} |
||||
|
||||
// check lookup |
||||
assertEq(_ckpts.lowerLookup(lookup), lower); |
||||
assertEq(_ckpts.upperLookup(lookup), upper); |
||||
assertEq(_ckpts.upperLookupRecent(lookup), upper); |
||||
} |
||||
} |
||||
|
||||
contract CheckpointsTrace160Test is Test { |
||||
using Checkpoints for Checkpoints.Trace160; |
||||
|
||||
// Maximum gap between keys used during the fuzzing tests: the `_prepareKeys` function with make sure that |
||||
// key#n+1 is in the [key#n, key#n + _KEY_MAX_GAP] range. |
||||
uint8 internal constant _KEY_MAX_GAP = 64; |
||||
|
||||
Checkpoints.Trace160 internal _ckpts; |
||||
|
||||
// helpers |
||||
function _boundUint96(uint96 x, uint96 min, uint96 max) internal view returns (uint96) { |
||||
return SafeCast.toUint96(bound(uint256(x), uint256(min), uint256(max))); |
||||
} |
||||
|
||||
function _prepareKeys(uint96[] memory keys, uint96 maxSpread) internal view { |
||||
uint96 lastKey = 0; |
||||
for (uint256 i = 0; i < keys.length; ++i) { |
||||
uint96 key = _boundUint96(keys[i], lastKey, lastKey + maxSpread); |
||||
keys[i] = key; |
||||
lastKey = key; |
||||
} |
||||
} |
||||
|
||||
function _assertLatestCheckpoint(bool exist, uint96 key, uint160 value) internal { |
||||
(bool _exist, uint96 _key, uint160 _value) = _ckpts.latestCheckpoint(); |
||||
assertEq(_exist, exist); |
||||
assertEq(_key, key); |
||||
assertEq(_value, value); |
||||
} |
||||
|
||||
// tests |
||||
function testPush(uint96[] memory keys, uint160[] memory values, uint96 pastKey) public { |
||||
vm.assume(values.length > 0 && values.length <= keys.length); |
||||
_prepareKeys(keys, _KEY_MAX_GAP); |
||||
|
||||
// initial state |
||||
assertEq(_ckpts.length(), 0); |
||||
assertEq(_ckpts.latest(), 0); |
||||
_assertLatestCheckpoint(false, 0, 0); |
||||
|
||||
uint256 duplicates = 0; |
||||
for (uint256 i = 0; i < keys.length; ++i) { |
||||
uint96 key = keys[i]; |
||||
uint160 value = values[i % values.length]; |
||||
if (i > 0 && key == keys[i - 1]) ++duplicates; |
||||
|
||||
// push |
||||
_ckpts.push(key, value); |
||||
|
||||
// check length & latest |
||||
assertEq(_ckpts.length(), i + 1 - duplicates); |
||||
assertEq(_ckpts.latest(), value); |
||||
_assertLatestCheckpoint(true, key, value); |
||||
} |
||||
|
||||
if (keys.length > 0) { |
||||
uint96 lastKey = keys[keys.length - 1]; |
||||
if (lastKey > 0) { |
||||
pastKey = _boundUint96(pastKey, 0, lastKey - 1); |
||||
|
||||
vm.expectRevert(); |
||||
this.push(pastKey, values[keys.length % values.length]); |
||||
} |
||||
} |
||||
} |
||||
|
||||
// used to test reverts |
||||
function push(uint96 key, uint160 value) external { |
||||
_ckpts.push(key, value); |
||||
} |
||||
|
||||
function testLookup(uint96[] memory keys, uint160[] memory values, uint96 lookup) public { |
||||
vm.assume(values.length > 0 && values.length <= keys.length); |
||||
_prepareKeys(keys, _KEY_MAX_GAP); |
||||
|
||||
uint96 lastKey = keys.length == 0 ? 0 : keys[keys.length - 1]; |
||||
lookup = _boundUint96(lookup, 0, lastKey + _KEY_MAX_GAP); |
||||
|
||||
uint160 upper = 0; |
||||
uint160 lower = 0; |
||||
uint96 lowerKey = type(uint96).max; |
||||
for (uint256 i = 0; i < keys.length; ++i) { |
||||
uint96 key = keys[i]; |
||||
uint160 value = values[i % values.length]; |
||||
|
||||
// push |
||||
_ckpts.push(key, value); |
||||
|
||||
// track expected result of lookups |
||||
if (key <= lookup) { |
||||
upper = value; |
||||
} |
||||
// find the first key that is not smaller than the lookup key |
||||
if (key >= lookup && (i == 0 || keys[i - 1] < lookup)) { |
||||
lowerKey = key; |
||||
} |
||||
if (key == lowerKey) { |
||||
lower = value; |
||||
} |
||||
} |
||||
|
||||
// check lookup |
||||
assertEq(_ckpts.lowerLookup(lookup), lower); |
||||
assertEq(_ckpts.upperLookup(lookup), upper); |
||||
assertEq(_ckpts.upperLookupRecent(lookup), upper); |
||||
} |
||||
} |
@ -0,0 +1,55 @@ |
||||
// SPDX-License-Identifier: MIT |
||||
|
||||
pragma solidity ^0.8.0; |
||||
|
||||
import "forge-std/Test.sol"; |
||||
|
||||
import "../../contracts/utils/ShortStrings.sol"; |
||||
|
||||
contract ShortStringsTest is Test { |
||||
string _fallback; |
||||
|
||||
function testRoundtripShort(string memory input) external { |
||||
vm.assume(_isShort(input)); |
||||
ShortString short = ShortStrings.toShortString(input); |
||||
string memory output = ShortStrings.toString(short); |
||||
assertEq(input, output); |
||||
} |
||||
|
||||
function testRoundtripWithFallback(string memory input, string memory fallbackInitial) external { |
||||
_fallback = fallbackInitial; // Make sure that the initial value has no effect |
||||
ShortString short = ShortStrings.toShortStringWithFallback(input, _fallback); |
||||
string memory output = ShortStrings.toStringWithFallback(short, _fallback); |
||||
assertEq(input, output); |
||||
} |
||||
|
||||
function testRevertLong(string memory input) external { |
||||
vm.assume(!_isShort(input)); |
||||
vm.expectRevert(abi.encodeWithSelector(ShortStrings.StringTooLong.selector, input)); |
||||
this.toShortString(input); |
||||
} |
||||
|
||||
function testLengthShort(string memory input) external { |
||||
vm.assume(_isShort(input)); |
||||
uint256 inputLength = bytes(input).length; |
||||
ShortString short = ShortStrings.toShortString(input); |
||||
uint256 shortLength = ShortStrings.byteLength(short); |
||||
assertEq(inputLength, shortLength); |
||||
} |
||||
|
||||
function testLengthWithFallback(string memory input, string memory fallbackInitial) external { |
||||
_fallback = fallbackInitial; |
||||
uint256 inputLength = bytes(input).length; |
||||
ShortString short = ShortStrings.toShortStringWithFallback(input, _fallback); |
||||
uint256 shortLength = ShortStrings.byteLengthWithFallback(short, _fallback); |
||||
assertEq(inputLength, shortLength); |
||||
} |
||||
|
||||
function toShortString(string memory input) external pure returns (ShortString) { |
||||
return ShortStrings.toShortString(input); |
||||
} |
||||
|
||||
function _isShort(string memory input) internal pure returns (bool) { |
||||
return bytes(input).length < 32; |
||||
} |
||||
} |
Loading…
Reference in new issue