diff --git a/.github/workflows/checks.yml b/.github/workflows/checks.yml index 9a5779d51..61cb96594 100644 --- a/.github/workflows/checks.yml +++ b/.github/workflows/checks.yml @@ -98,6 +98,17 @@ jobs: with: token: ${{ secrets.CODECOV_TOKEN }} + harnesses: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Set up environment + uses: ./.github/actions/setup + - name: Compile harnesses + run: | + make -C certora apply + npm run compile:harnesses + slither: runs-on: ubuntu-latest steps: diff --git a/certora/harnesses/EnumerableMapHarness.sol b/certora/harnesses/EnumerableMapHarness.sol index 5c2f3229b..6155193e9 100644 --- a/certora/harnesses/EnumerableMapHarness.sol +++ b/certora/harnesses/EnumerableMapHarness.sol @@ -49,7 +49,7 @@ contract EnumerableMapHarness { return _map.get(key); } - function _indexOf(bytes32 key) public view returns (uint256) { - return _map._keys._inner._indexes[key]; + function _positionOf(bytes32 key) public view returns (uint256) { + return _map._keys._inner._positions[key]; } } diff --git a/certora/harnesses/EnumerableSetHarness.sol b/certora/harnesses/EnumerableSetHarness.sol index 3d18b183b..09246de6b 100644 --- a/certora/harnesses/EnumerableSetHarness.sol +++ b/certora/harnesses/EnumerableSetHarness.sol @@ -29,7 +29,7 @@ contract EnumerableSetHarness { return _set.at(index); } - function _indexOf(bytes32 value) public view returns (uint256) { - return _set._inner._indexes[value]; + function _positionOf(bytes32 value) public view returns (uint256) { + return _set._inner._positions[value]; } } diff --git a/certora/specs/EnumerableMap.spec b/certora/specs/EnumerableMap.spec index 7b503031f..1801d99f7 100644 --- a/certora/specs/EnumerableMap.spec +++ b/certora/specs/EnumerableMap.spec @@ -13,7 +13,7 @@ methods { function get(bytes32) external returns (bytes32) envfree; // FV - function _indexOf(bytes32) external returns (uint256) envfree; + function _positionOf(bytes32) external returns (uint256) envfree; } /* @@ -69,13 +69,13 @@ invariant atUniqueness(uint256 index1, uint256 index2) ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Invariant: index <> value relationship is consistent │ │ │ -│ Note that the two consistencyXxx invariants, put together, prove that at_ and _indexOf are inverse of one another. │ -│ This proves that we have a bijection between indices (the enumerability part) and keys (the entries that are set │ -│ and removed from the EnumerableMap). │ +│ Note that the two consistencyXxx invariants, put together, prove that at_ and _positionOf are inverse of one │ +│ another. This proves that we have a bijection between indices (the enumerability part) and keys (the entries that │ +│ are set and removed from the EnumerableMap). │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant consistencyIndex(uint256 index) - index < length() => to_mathint(_indexOf(key_at(index))) == index + 1 + index < length() => to_mathint(_positionOf(key_at(index))) == index + 1 { preserved remove(bytes32 key) { requireInvariant consistencyIndex(require_uint256(length() - 1)); @@ -84,16 +84,16 @@ invariant consistencyIndex(uint256 index) invariant consistencyKey(bytes32 key) contains(key) => ( - _indexOf(key) > 0 && - _indexOf(key) <= length() && - key_at(require_uint256(_indexOf(key) - 1)) == key + _positionOf(key) > 0 && + _positionOf(key) <= length() && + key_at(require_uint256(_positionOf(key) - 1)) == key ) { preserved remove(bytes32 otherKey) { requireInvariant consistencyKey(otherKey); requireInvariant atUniqueness( - require_uint256(_indexOf(key) - 1), - require_uint256(_indexOf(otherKey) - 1) + require_uint256(_positionOf(key) - 1), + require_uint256(_positionOf(otherKey) - 1) ); } } diff --git a/certora/specs/EnumerableSet.spec b/certora/specs/EnumerableSet.spec index 3db515838..94d0a918c 100644 --- a/certora/specs/EnumerableSet.spec +++ b/certora/specs/EnumerableSet.spec @@ -9,7 +9,7 @@ methods { function at_(uint256) external returns (bytes32) envfree; // FV - function _indexOf(bytes32) external returns (uint256) envfree; + function _positionOf(bytes32) external returns (uint256) envfree; } /* @@ -52,13 +52,13 @@ invariant atUniqueness(uint256 index1, uint256 index2) ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Invariant: index <> key relationship is consistent │ │ │ -│ Note that the two consistencyXxx invariants, put together, prove that at_ and _indexOf are inverse of one another. │ -│ This proves that we have a bijection between indices (the enumerability part) and keys (the entries that are added │ -│ and removed from the EnumerableSet). │ +│ Note that the two consistencyXxx invariants, put together, prove that at_ and _positionOf are inverse of one │ +│ another. This proves that we have a bijection between indices (the enumerability part) and keys (the entries that │ +│ are added and removed from the EnumerableSet). │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant consistencyIndex(uint256 index) - index < length() => _indexOf(at_(index)) == require_uint256(index + 1) + index < length() => _positionOf(at_(index)) == require_uint256(index + 1) { preserved remove(bytes32 key) { requireInvariant consistencyIndex(require_uint256(length() - 1)); @@ -67,16 +67,16 @@ invariant consistencyIndex(uint256 index) invariant consistencyKey(bytes32 key) contains(key) => ( - _indexOf(key) > 0 && - _indexOf(key) <= length() && - at_(require_uint256(_indexOf(key) - 1)) == key + _positionOf(key) > 0 && + _positionOf(key) <= length() && + at_(require_uint256(_positionOf(key) - 1)) == key ) { preserved remove(bytes32 otherKey) { requireInvariant consistencyKey(otherKey); requireInvariant atUniqueness( - require_uint256(_indexOf(key) - 1), - require_uint256(_indexOf(otherKey) - 1) + require_uint256(_positionOf(key) - 1), + require_uint256(_positionOf(otherKey) - 1) ); } } diff --git a/hardhat.config.js b/hardhat.config.js index 5a7d043ef..230cca5e2 100644 --- a/hardhat.config.js +++ b/hardhat.config.js @@ -1,26 +1,29 @@ /// ENVVAR -// - CI: output gas report to file instead of stdout +// - COMPILE_VERSION: compiler version (default: 0.8.20) +// - SRC: contracts folder to compile (default: contracts) +// - COMPILE_MODE: production modes enables optimizations (default: development) +// - IR: enable IR compilation (default: false) // - COVERAGE: enable coverage report // - ENABLE_GAS_REPORT: enable gas report -// - COMPILE_MODE: production modes enables optimizations (default: development) -// - COMPILE_VERSION: compiler version (default: 0.8.20) // - COINMARKETCAP: coinmarkercat api key for USD value in gas report +// - CI: output gas report to file instead of stdout const fs = require('fs'); const path = require('path'); -const proc = require('child_process'); -const argv = require('yargs/yargs')() +const { argv } = require('yargs/yargs')() .env('') .options({ - coverage: { - type: 'boolean', - default: false, + // Compilation settings + compiler: { + alias: 'compileVersion', + type: 'string', + default: '0.8.20', }, - gas: { - alias: 'enableGasReport', - type: 'boolean', - default: false, + src: { + alias: 'source', + type: 'string', + default: 'contracts', }, mode: { alias: 'compileMode', @@ -33,21 +36,21 @@ const argv = require('yargs/yargs')() type: 'boolean', default: false, }, - foundry: { - alias: 'hasFoundry', + // Extra modules + coverage: { type: 'boolean', - default: hasFoundry(), + default: false, }, - compiler: { - alias: 'compileVersion', - type: 'string', - default: '0.8.20', + gas: { + alias: 'enableGasReport', + type: 'boolean', + default: false, }, coinmarketcap: { alias: 'coinmarketcapApiKey', type: 'string', }, - }).argv; + }); require('@nomicfoundation/hardhat-chai-matchers'); require('@nomicfoundation/hardhat-ethers'); @@ -56,17 +59,13 @@ require('hardhat-gas-reporter'); require('hardhat-ignore-warnings'); require('solidity-coverage'); require('solidity-docgen'); -argv.foundry && require('@nomicfoundation/hardhat-foundry'); - -if (argv.foundry && argv.coverage) { - throw Error('Coverage analysis is incompatible with Foundry. Disable with `FOUNDRY=false` in the environment'); -} for (const f of fs.readdirSync(path.join(__dirname, 'hardhat'))) { require(path.join(__dirname, 'hardhat', f)); } const withOptimizations = argv.gas || argv.coverage || argv.compileMode === 'production'; +const allowUnlimitedContractSize = argv.gas || argv.coverage || argv.compileMode === 'development'; /** * @type import('hardhat/config').HardhatUserConfig @@ -96,7 +95,7 @@ module.exports = { }, networks: { hardhat: { - allowUnlimitedContractSize: !withOptimizations, + allowUnlimitedContractSize, initialBaseFeePerGas: argv.coverage ? 0 : undefined, }, }, @@ -111,9 +110,8 @@ module.exports = { currency: 'USD', coinmarketcap: argv.coinmarketcap, }, + paths: { + sources: argv.src, + }, docgen: require('./docs/config'), }; - -function hasFoundry() { - return proc.spawnSync('forge', ['-V'], { stdio: 'ignore' }).error === undefined; -} diff --git a/hardhat/remappings.js b/hardhat/remappings.js new file mode 100644 index 000000000..cd9984d44 --- /dev/null +++ b/hardhat/remappings.js @@ -0,0 +1,18 @@ +const fs = require('fs'); +const { task } = require('hardhat/config'); +const { TASK_COMPILE_GET_REMAPPINGS } = require('hardhat/builtin-tasks/task-names'); + +task(TASK_COMPILE_GET_REMAPPINGS).setAction((taskArgs, env, runSuper) => + runSuper().then(remappings => + Object.assign( + remappings, + Object.fromEntries( + fs + .readFileSync('remappings.txt', 'utf-8') + .split('\n') + .filter(Boolean) + .map(line => line.trim().split('=')), + ), + ), + ), +); diff --git a/package-lock.json b/package-lock.json index 80f4e2b07..be38fefdd 100644 --- a/package-lock.json +++ b/package-lock.json @@ -15,7 +15,6 @@ "@changesets/read": "^0.6.0", "@nomicfoundation/hardhat-chai-matchers": "^2.0.3", "@nomicfoundation/hardhat-ethers": "^3.0.4", - "@nomicfoundation/hardhat-foundry": "^1.1.1", "@nomicfoundation/hardhat-network-helpers": "^1.0.3", "@openzeppelin/docs-utils": "^0.1.5", "@openzeppelin/merkle-tree": "^1.0.5", @@ -2112,18 +2111,6 @@ "hardhat": "^2.0.0" } }, - "node_modules/@nomicfoundation/hardhat-foundry": { - "version": "1.1.1", - "resolved": "https://registry.npmjs.org/@nomicfoundation/hardhat-foundry/-/hardhat-foundry-1.1.1.tgz", - "integrity": "sha512-cXGCBHAiXas9Pg9MhMOpBVQCkWRYoRFG7GJJAph+sdQsfd22iRs5U5Vs9XmpGEQd1yEvYISQZMeE68Nxj65iUQ==", - "dev": true, - "dependencies": { - "chalk": "^2.4.2" - }, - "peerDependencies": { - "hardhat": "^2.17.2" - } - }, "node_modules/@nomicfoundation/hardhat-network-helpers": { "version": "1.0.9", "resolved": "https://registry.npmjs.org/@nomicfoundation/hardhat-network-helpers/-/hardhat-network-helpers-1.0.9.tgz", diff --git a/package.json b/package.json index 7f2187d85..888767017 100644 --- a/package.json +++ b/package.json @@ -9,7 +9,8 @@ ], "scripts": { "compile": "hardhat compile", - "coverage": "env COVERAGE=true FOUNDRY=false hardhat coverage", + "compile:harnesses": "env SRC=./certora/harnesses hardhat compile", + "coverage": "env COVERAGE=true hardhat coverage", "docs": "npm run prepare-docs && oz-docs", "docs:watch": "oz-docs watch contracts docs/templates docs/config.js", "prepare-docs": "scripts/prepare-docs.sh", @@ -54,7 +55,6 @@ "@changesets/read": "^0.6.0", "@nomicfoundation/hardhat-chai-matchers": "^2.0.3", "@nomicfoundation/hardhat-ethers": "^3.0.4", - "@nomicfoundation/hardhat-foundry": "^1.1.1", "@nomicfoundation/hardhat-network-helpers": "^1.0.3", "@openzeppelin/docs-utils": "^0.1.5", "@openzeppelin/merkle-tree": "^1.0.5",