diff --git a/Makefile b/Makefile deleted file mode 100644 index d65554780..000000000 --- a/Makefile +++ /dev/null @@ -1,139 +0,0 @@ - -# Run a single cvl e.g.: -# make -B spec/certora/CErc20/borrowAndRepayFresh.cvl - -# TODO: -# - mintAndRedeemFresh.cvl in progress and is failing due to issues with tool proving how the exchange rate can change -# hoping for better division modelling - currently fails to prove (a + 1) / b >= a / b -# - CErc20Delegator/*.cvl cannot yet be run with the tool -# - cDAI proofs are WIP, require using the delegate and the new revert message assertions - -.PHONY: certora-clean - -CERTORA_BIN = $(abspath script/certora) -CERTORA_RUN = $(CERTORA_BIN)/run.py -CERTORA_CLI = $(CERTORA_BIN)/cli.jar -CERTORA_EMV = $(CERTORA_BIN)/emv.jar - -export CERTORA = $(CERTORA_BIN) -export CERTORA_DISABLE_POPUP = 1 - -spec/certora/Math/%.cvl: - $(CERTORA_RUN) \ - spec/certora/contracts/MathCertora.sol \ - --verify \ - MathCertora:$@ - -spec/certora/Comp/search.cvl: - $(CERTORA_RUN) \ - spec/certora/contracts/CompCertora.sol \ - --settings -b=4,-graphDrawLimit=0,-assumeUnwindCond,-depth=100 \ - --solc_args "'--evm-version istanbul'" \ - --verify \ - CompCertora:$@ - -spec/certora/Comp/transfer.cvl: - $(CERTORA_RUN) \ - spec/certora/contracts/CompCertora.sol \ - --settings -graphDrawLimit=0,-assumeUnwindCond,-depth=100 \ - --solc_args "'--evm-version istanbul'" \ - --verify \ - CompCertora:$@ - -spec/certora/Governor/%.cvl: - $(CERTORA_RUN) \ - spec/certora/contracts/GovernorAlphaCertora.sol \ - spec/certora/contracts/TimelockCertora.sol \ - spec/certora/contracts/CompCertora.sol \ - --settings -assumeUnwindCond,-enableWildcardInlining=false \ - --solc_args "'--evm-version istanbul'" \ - --link \ - GovernorAlphaCertora:timelock=TimelockCertora \ - GovernorAlphaCertora:comp=CompCertora \ - --verify \ - GovernorAlphaCertora:$@ - -spec/certora/Comptroller/%.cvl: - $(CERTORA_RUN) \ - spec/certora/contracts/ComptrollerCertora.sol \ - spec/certora/contracts/PriceOracleModel.sol \ - --link \ - ComptrollerCertora:oracle=PriceOracleModel \ - --verify \ - ComptrollerCertora:$@ - -spec/certora/cDAI/%.cvl: - $(CERTORA_RUN) \ - spec/certora/contracts/CDaiDelegateCertora.sol \ - spec/certora/contracts/UnderlyingModelNonStandard.sol \ - spec/certora/contracts/mcd/dai.sol:Dai \ - spec/certora/contracts/mcd/pot.sol:Pot \ - spec/certora/contracts/mcd/vat.sol:Vat \ - spec/certora/contracts/mcd/join.sol:DaiJoin \ - tests/Contracts/BoolComptroller.sol \ - --link \ - CDaiDelegateCertora:comptroller=BoolComptroller \ - CDaiDelegateCertora:underlying=Dai \ - CDaiDelegateCertora:potAddress=Pot \ - CDaiDelegateCertora:vatAddress=Vat \ - CDaiDelegateCertora:daiJoinAddress=DaiJoin \ - --verify \ - CDaiDelegateCertora:$@ \ - --settings -cache=certora-run-cdai - -spec/certora/CErc20/%.cvl: - $(CERTORA_RUN) \ - spec/certora/contracts/CErc20ImmutableCertora.sol \ - spec/certora/contracts/CTokenCollateral.sol \ - spec/certora/contracts/ComptrollerCertora.sol \ - spec/certora/contracts/InterestRateModelModel.sol \ - spec/certora/contracts/UnderlyingModelNonStandard.sol \ - --link \ - CErc20ImmutableCertora:otherToken=CTokenCollateral \ - CErc20ImmutableCertora:comptroller=ComptrollerCertora \ - CErc20ImmutableCertora:underlying=UnderlyingModelNonStandard \ - CErc20ImmutableCertora:interestRateModel=InterestRateModelModel \ - CTokenCollateral:comptroller=ComptrollerCertora \ - CTokenCollateral:underlying=UnderlyingModelNonStandard \ - --verify \ - CErc20ImmutableCertora:$@ \ - --settings -cache=certora-run-cerc20-immutable - -spec/certora/CErc20Delegator/%.cvl: - $(CERTORA_RUN) \ - spec/certora/contracts/CErc20DelegatorCertora.sol \ - spec/certora/contracts/CErc20DelegateCertora.sol \ - spec/certora/contracts/CTokenCollateral.sol \ - spec/certora/contracts/ComptrollerCertora.sol \ - spec/certora/contracts/InterestRateModelModel.sol \ - spec/certora/contracts/UnderlyingModelNonStandard.sol \ - --link \ - CErc20DelegatorCertora:implementation=CErc20DelegateCertora \ - CErc20DelegatorCertora:otherToken=CTokenCollateral \ - CErc20DelegatorCertora:comptroller=ComptrollerCertora \ - CErc20DelegatorCertora:underlying=UnderlyingModelNonStandard \ - CErc20DelegatorCertora:interestRateModel=InterestRateModelModel \ - CTokenCollateral:comptroller=ComptrollerCertora \ - CTokenCollateral:underlying=UnderlyingModelNonStandard \ - --verify \ - CErc20DelegatorCertora:$@ \ - --settings -assumeUnwindCond \ - --settings -cache=certora-run-cerc20-delegator - -spec/certora/Maximillion/%.cvl: - $(CERTORA_RUN) \ - spec/certora/contracts/MaximillionCertora.sol \ - spec/certora/contracts/CEtherCertora.sol \ - --link \ - MaximillionCertora:cEther=CEtherCertora \ - --verify \ - MaximillionCertora:$@ - -spec/certora/Timelock/%.cvl: - $(CERTORA_RUN) \ - spec/certora/contracts/TimelockCertora.sol \ - --verify \ - TimelockCertora:$@ - -certora-clean: - rm -rf .certora_build.json .certora_config certora_verify.json emv-* diff --git a/gasCosts.json b/gasCosts.json deleted file mode 100644 index 6c1dc43ca..000000000 --- a/gasCosts.json +++ /dev/null @@ -1,204 +0,0 @@ -{ - "first mint": { - "fee": 124570, - "opcodes": {} - }, - "second mint": { - "fee": 84516, - "opcodes": { - "PUSH1 @ 3": 287, - "MSTORE @ 3": 126, - "PUSH1 @ 12": 1, - "CALLDATASIZE @ 3": 18, - "LT @ 2": 9, - "PUSH2 @ 3": 302, - "JUMPI @ 3": 137, - "PUSH1 @ 10": 12, - "CALLDATALOAD @ 3": 22, - "SHR @ 3": 9, - "DUP1 @ 3": 107, - "PUSH4 @ 3": 48, - "GT @ 3": 40, - "DUP1 @ 10": 12, - "JUMPDEST @ 10": 110, - "DUP1 @ 1": 23, - "EQ @ 3": 24, - "CALLVALUE @ 1": 1, - "DUP1 @ 2": 16, - "ISZERO @ 3": 88, - "POP @ 1": 66, - "PUSH2 @ 2": 7, - "PUSH1 @ 2": 58, - "JUMP @ 3": 145, - "JUMPDEST @ 8": 203, - "PUSH1 @ 1": 128, - "DUP3 @ 3": 105, - "DUP5 @ 3": 53, - "SUB @ 3": 67, - "SLT @ 3": 16, - "CALLDATALOAD @ 2": 2, - "SWAP2 @ 3": 86, - "SWAP1 @ 3": 195, - "POP @ 3": 106, - "JUMP @ 2": 57, - "PUSH2 @ 1": 25, - "DUP4 @ 3": 30, - "MLOAD @ 3": 82, - "ADD @ 3": 102, - "DUP2 @ 3": 118, - "PUSH1 @ 15": 1, - "NOT @ 3": 24, - "SHL @ 3": 40, - "AND @ 3": 53, - "OR @ 3": 2, - "SLOAD @ 3": 27, - "PUSH1 @ 800": 22, - "DUP8 @ 3": 10, - "JUMPDEST @ 3": 4, - "DUP4 @ 1": 5, - "LT @ 3": 9, - "DUP2 @ 10": 2, - "PUSH1 @ 6": 17, - "POP @ 2": 133, - "SWAP2 @ 1": 14, - "SWAP3 @ 3": 26, - "DUP6 @ 3": 33, - "GAS @ 3": 1, - "DELEGATECALL @ 2": 1, - "PUSH1 @ 312831": 1, - "CALLVALUE @ 12": 8, - "SSTORE @ 3": 11, - "PUSH2 @ 5000": 1, - "SWAP1 @ 800": 2, - "ADDRESS @ 9": 1, - "DUP7 @ 3": 17, - "EXTCODESIZE @ 3": 7, - "ISZERO @ 700": 7, - "GAS @ 2": 7, - "STATICCALL @ 2": 5, - "PUSH1 @ 307782": 1, - "SWAP4 @ 1": 17, - "SHA3 @ 3": 15, - "SLOAD @ 42": 9, - "DUP2 @ 800": 5, - "PUSH1 @ 9": 6, - "RETURN @ 3": 9, - "ISZERO @ -307082": 1, - "RETURNDATASIZE @ 3": 10, - "DUP2 @ 2": 7, - "MLOAD @ 2": 7, - "SWAP1 @ 2": 7, - "SWAP5 @ 6": 1, - "SWAP6 @ 3": 3, - "SWAP3 @ 2": 7, - "SWAP4 @ 3": 13, - "PUSH1 @ 307684": 1, - "POP @ 10": 1, - "SWAP1 @ 1": 25, - "PUSH8 @ 800": 1, - "DUP4 @ 800": 2, - "DIV @ 3": 7, - "DUP4 @ 5": 7, - "MUL @ 2": 7, - "SWAP1 @ 5": 13, - "DIV @ 2": 6, - "ADD @ 2": 8, - "JUMPDEST @ 2": 2, - "ISZERO @ -306984": 1, - "PUSH6 @ 2": 1, - "DUP10 @ 3": 3, - "SUB @ 2": 5, - "DUP4 @ 2": 2, - "DUP9 @ 3": 5, - "SWAP4 @ 6": 4, - "PUSH8 @ 3": 5, - "SWAP3 @ 1": 6, - "SWAP5 @ 1": 3, - "POP @ 6": 1, - "DUP5 @ 2": 2, - "DUP11 @ 3": 2, - "DUP5 @ 1": 2, - "SWAP6 @ 1": 4, - "SWAP5 @ 3": 6, - "DUP15 @ 3": 1, - "PUSH1 @ 5000": 2, - "DUP14 @ 3": 1, - "SWAP1 @ 6": 2, - "PUSH32 @ 2": 1, - "LOG1 @ 3": 2, - "PUSH1 @ 1774": 1, - "SWAP14 @ 3": 1, - "CALLER @ 3": 1, - "ADDRESS @ 3": 5, - "CALL @ 2": 2, - "PUSH1 @ 307417": 1, - "JUMPDEST @ 800": 1, - "ISZERO @ -306717": 1, - "EQ @ 800": 1, - "PUSH1 @ 307290": 1, - "ISZERO @ -306590": 1, - "ADDRESS @ 6": 1, - "PUSH1 @ 307200": 1, - "ISZERO @ -306500": 1, - "SWAP2 @ 7": 1, - "PUSH1 @ 307152": 1, - "PUSH22 @ 9": 1, - "CALLER @ 42": 2, - "DUP3 @ 2": 2, - "PUSH2 @ 800": 5, - "SWAP5 @ 42": 1, - "DUP4 @ 5000": 1, - "PUSH20 @ 6": 1, - "SWAP3 @ 6": 1, - "SWAP6 @ 42": 1, - "DUP5 @ 5000": 1, - "PUSH16 @ 6": 1, - "SWAP5 @ 2": 1, - "SWAP4 @ 42": 1, - "SWAP2 @ 5000": 1, - "PUSH32 @ 3": 2, - "LOG3 @ 3": 2, - "POP @ 1756": 2, - "ISZERO @ -306452": 1, - "RETURNDATACOPY @ 3": 2, - "PUSH1 @ 306770": 1, - "ISZERO @ -306070": 1, - "SWAP8 @ 1": 1, - "SWAP7 @ 3": 1, - "SWAP2 @ 42": 1, - "MLOAD @ 5000": 1, - "PUSH1 @ 1518": 1, - "CODECOPY @ 3": 1, - "DUP2 @ 6": 1, - "JUMP @ 800": 1, - "SWAP2 @ -312131": 1, - "RETURNDATASIZE @ 2": 1, - "PUSH2 @ 6": 1, - "SWAP2 @ 2": 2 - } - }, - "second mint, no interest accrued": { - "fee": 61306, - "opcodes": {} - }, - "redeem": { - "fee": 95058, - "opcodes": {} - }, - "unitroller-g6 second mint with comp accrued": { - "fee": 138680, - "opcodes": {} - }, - "unitroller-g6 claim comp": { - "fee": 142459, - "opcodes": {} - }, - "unitroller second mint with comp accrued": { - "fee": 116271, - "opcodes": {} - }, - "unitroller claim comp": { - "fee": 155422, - "opcodes": {} - } -} diff --git a/jest.config.js b/jest.config.js deleted file mode 100644 index 2863ba90d..000000000 --- a/jest.config.js +++ /dev/null @@ -1,185 +0,0 @@ -// For a detailed explanation regarding each configuration property, visit: -// https://jestjs.io/docs/en/configuration.html - -module.exports = { - // All imported modules in your tests should be mocked automatically - // automock: false, - - // Stop running tests after `n` failures - // bail: 0, - - // Respect "browser" field in package.json when resolving modules - // browser: false, - - // The directory where Jest should store its cached dependency information - // cacheDirectory: "/private/var/folders/jz/z56b1n2902584b4zplqztm3m0000gn/T/jest_dx", - - // Automatically clear mock calls and instances between every test - // clearMocks: false, - - // Indicates whether the coverage information should be collected while executing the test - // collectCoverage: false, - - // An array of glob patterns indicating a set of files for which coverage information should be collected - // collectCoverageFrom: null, - - // The directory where Jest should output its coverage files - // coverageDirectory: null, - - // An array of regexp pattern strings used to skip coverage collection - // coveragePathIgnorePatterns: [ - // "/node_modules/" - // ], - - // A list of reporter names that Jest uses when writing coverage reports - // coverageReporters: [ - // "json", - // "text", - // "lcov", - // "clover" - // ], - - // An object that configures minimum threshold enforcement for coverage results - // coverageThreshold: null, - - // A path to a custom dependency extractor - // dependencyExtractor: null, - - // Make calling deprecated APIs throw helpful error messages - // errorOnDeprecated: false, - - // Force coverage collection from ignored files using an array of glob patterns - // forceCoverageMatch: [], - - // A path to a module which exports an async function that is triggered once before all test suites - // globalSetup: null, - - // A path to a module which exports an async function that is triggered once after all test suites - // globalTeardown: null, - - // A set of global variables that need to be available in all test environments - // globals: {}, - - // An array of directory names to be searched recursively up from the requiring module's location - // moduleDirectories: [ - // "node_modules" - // ], - - // An array of file extensions your modules use - // moduleFileExtensions: [ - // "js", - // "json", - // "jsx", - // "ts", - // "tsx", - // "node" - // ], - - // A map from regular expressions to module names that allow to stub out resources with a single module - // moduleNameMapper: {}, - - // An array of regexp pattern strings, matched against all module paths before considered 'visible' to the module loader - // modulePathIgnorePatterns: [], - - // Activates notifications for test results - // notify: false, - - // An enum that specifies notification mode. Requires { notify: true } - // notifyMode: "failure-change", - - // A preset that is used as a base for Jest's configuration - // preset: null, - - // Run tests from one or more projects - // projects: null, - - // Use this configuration option to add custom reporters to Jest - reporters: ["default", "jest-junit"], - - // Automatically reset mock state between every test - // resetMocks: false, - - // Reset the module registry before running each individual test - // resetModules: false, - - // A path to a custom resolver - // resolver: null, - - // Automatically restore mock state between every test - // restoreMocks: false, - - // The root directory that Jest should scan for tests and modules within - // rootDir: null, - - // A list of paths to directories that Jest should use to search for files in - // roots: [ - // "" - // ], - - // Allows you to use a custom runner instead of Jest's default test runner - // runner: "jest-runner", - - // The paths to modules that run some code to configure or set up the testing environment before each test - // setupFiles: [], - - // A list of paths to modules that run some code to configure or set up the testing framework before each test - setupFilesAfterEnv: ["/tests/Matchers.js", "/tests/Jest.js"], - - // A list of paths to snapshot serializer modules Jest should use for snapshot testing - // snapshotSerializers: [], - - // The test environment that will be used for testing - testEnvironment: "node", - - // Options that will be passed to the testEnvironment - // testEnvironmentOptions: {}, - - // Adds a location field to test results - // testLocationInResults: false, - - // The glob patterns Jest uses to detect test files - // testMatch: [ - // "**/__tests__/**/*.[jt]s?(x)", - // "**/?(*.)+(spec|test).[tj]s?(x)" - // ], - - // An array of regexp pattern strings that are matched against all test paths, matched tests are skipped - // testPathIgnorePatterns: [ - // "/node_modules/" - // ], - - // The regexp pattern or array of patterns that Jest uses to detect test files - // testRegex: [], - - // This option allows the use of a custom results processor - // testResultsProcessor: null, - - // This option allows use of a custom test runner - // testRunner: "jasmine2", - - // This option sets the URL for the jsdom environment. It is reflected in properties such as location.href - // testURL: "http://localhost", - - // Setting this value to "fake" allows the use of fake timers for functions such as "setTimeout" - // timers: "real", - - // A map from regular expressions to paths to transformers - // transform: null, - - // An array of regexp pattern strings that are matched against all source file paths, matched files will skip transformation - // transformIgnorePatterns: [ - // "/node_modules/" - // ], - - // An array of regexp pattern strings that are matched against all modules before the module loader will automatically return a mock for them - // unmockedModulePathPatterns: undefined, - - // Indicates whether each individual test should be reported during the run - // verbose: null, - - // An array of regexp patterns that are matched against all source file paths before re-running tests in watch mode - // watchPathIgnorePatterns: [], - - // Whether to use watchman for file crawling - // watchman: true, -}; diff --git a/reporterConfig.json b/reporterConfig.json deleted file mode 100644 index 8facae3fe..000000000 --- a/reporterConfig.json +++ /dev/null @@ -1,3 +0,0 @@ -{ - "reporterEnabled": "spec, mocha-junit-reporter" -} diff --git a/script/README.md b/script/README.md deleted file mode 100644 index 01c920da1..000000000 --- a/script/README.md +++ /dev/null @@ -1 +0,0 @@ -Scripts to make common developer tasks easy to type. diff --git a/script/comptroller-abi b/script/comptroller-abi deleted file mode 100755 index 436bf7b99..000000000 --- a/script/comptroller-abi +++ /dev/null @@ -1,33 +0,0 @@ -#!/usr/bin/env node - -const fs = require('fs') - -function mergeInterface(into, from) { - const key = (item) => item.inputs ? `${item.name}/${item.inputs.length}` : item.name; - const existing = into.reduce((acc, item) => { - acc[key(item)] = true; - return acc; - }, {}); - const extended = from.reduce((acc, item) => { - if (!(key(item) in existing)) - acc.push(item) - return acc; - }, into.slice()); - return into.concat(from) -} - -function mergeComptroller(abi) { - abi.Comptroller = mergeInterface(abi.Unitroller, abi[`Comptroller`]) - return abi; -} - -function format(abi) { - return JSON.stringify(abi, null, 4).replace(/^( {4}".*?)$/mg, '\n$1') -} - -function main(path) { - const abi = JSON.parse(fs.readFileSync(path)) - fs.writeFileSync(path, format(mergeComptroller(abi))) -} - -main('networks/mainnet-abi.json')