This commit is contained in:
Hadrien Croubois
2023-03-10 15:08:42 +01:00
parent f35c824435
commit 9f39697a44

View File

@ -2,66 +2,50 @@ const product = (...arrays) => arrays.reduce((a, b) => a.flatMap(ai => b.map(bi
module.exports = [ module.exports = [
{ {
"spec": "AccessControl", spec: 'AccessControl',
"contract": "AccessControlHarness", contract: 'AccessControlHarness',
"files": ["certora/harnesses/AccessControlHarness.sol"] files: ['certora/harnesses/AccessControlHarness.sol'],
}, },
{ {
"spec": "Ownable", spec: 'Ownable',
"contract": "OwnableHarness", contract: 'OwnableHarness',
"files": ["certora/harnesses/OwnableHarness.sol"] files: ['certora/harnesses/OwnableHarness.sol'],
}, },
{ {
"spec": "Ownable2Step", spec: 'Ownable2Step',
"contract": "Ownable2StepHarness", contract: 'Ownable2StepHarness',
"files": ["certora/harnesses/Ownable2StepHarness.sol"] files: ['certora/harnesses/Ownable2StepHarness.sol'],
}, },
{ {
"spec": "ERC20", spec: 'ERC20',
"contract": "ERC20PermitHarness", contract: 'ERC20PermitHarness',
"files": ["certora/harnesses/ERC20PermitHarness.sol"], files: ['certora/harnesses/ERC20PermitHarness.sol'],
"options": ["--optimistic_loop"] options: ['--optimistic_loop'],
}, },
{ {
"spec": "ERC20FlashMint", spec: 'ERC20FlashMint',
"contract": "ERC20FlashMintHarness", contract: 'ERC20FlashMintHarness',
"files": [ files: ['certora/harnesses/ERC20FlashMintHarness.sol', 'certora/harnesses/ERC3156FlashBorrowerHarness.sol'],
"certora/harnesses/ERC20FlashMintHarness.sol", options: ['--optimistic_loop'],
"certora/harnesses/ERC3156FlashBorrowerHarness.sol"
],
"options": ["--optimistic_loop"]
}, },
{ {
"spec": "ERC20Wrapper", spec: 'ERC20Wrapper',
"contract": "ERC20WrapperHarness", contract: 'ERC20WrapperHarness',
"files": [ files: ['certora/harnesses/ERC20PermitHarness.sol', 'certora/harnesses/ERC20WrapperHarness.sol'],
"certora/harnesses/ERC20PermitHarness.sol", options: ['--link ERC20WrapperHarness:_underlying=ERC20PermitHarness', '--optimistic_loop'],
"certora/harnesses/ERC20WrapperHarness.sol"
],
"options": [
"--link ERC20WrapperHarness:_underlying=ERC20PermitHarness",
"--optimistic_loop"
]
}, },
{ {
"spec": "Initializable", spec: 'Initializable',
"contract": "InitializableHarness", contract: 'InitializableHarness',
"files": ["certora/harnesses/InitializableHarness.sol"] files: ['certora/harnesses/InitializableHarness.sol'],
}, },
...product( ...product(
[ "GovernorBase", "GovernorInvariants", "GovernorStates", "GovernorFunctions" ], ['GovernorBase', 'GovernorInvariants', 'GovernorStates', 'GovernorFunctions'],
[ "ERC20VotesBlocknumberHarness", "ERC20VotesTimestampHarness" ], ['ERC20VotesBlocknumberHarness', 'ERC20VotesTimestampHarness'],
).map(([ spec, token ]) => ({ ).map(([spec, token]) => ({
spec, spec,
"contract": "GovernorHarness", contract: 'GovernorHarness',
"files": [ files: ['certora/harnesses/GovernorHarness.sol', `certora/harnesses/${token}.sol`],
"certora/harnesses/GovernorHarness.sol", options: [`--link GovernorHarness:token=${token}`, '--optimistic_loop', '--optimistic_hashing'],
`certora/harnesses/${token}.sol` })),
],
"options": [
`--link GovernorHarness:token=${token}`,
"--optimistic_loop",
"--optimistic_hashing"
]
}))
]; ];