|
| 1 | +{ |
| 2 | + "assert_autofinder_success": true, |
| 3 | + "contract_extensions": { |
| 4 | + "GenericVaultBridgeToken": [ { |
| 5 | + "extension": "VaultBridgeTokenPart2", |
| 6 | + "exclude": [ "rebalanceReserve", |
| 7 | + "allowance", "approve", "asset", "backingDifference", |
| 8 | + "balanceOf", "claimAndRedeem", "convertToAssets", |
| 9 | + "convertToShares", "decimals", "DEFAULT_ADMIN_ROLE", "deposit", |
| 10 | + "depositAndBridge", "depositWithPermit", |
| 11 | + "depositWithPermitAndBridge", "DOMAIN_SEPARATOR", |
| 12 | + "eip712Domain", "getRoleAdmin", "grantRole", "hasRole", |
| 13 | + "lxlyBridge", "lxlyId", "maxDeposit", "maxMint", "maxRedeem", |
| 14 | + "maxWithdraw", "migrationFeesFund", "migrationManager", |
| 15 | + "minimumReservePercentage", "minimumYieldVaultDeposit", "mint", |
| 16 | + "name", "nonces", "paused", "PAUSER_ROLE", |
| 17 | + "performReversibleYieldVaultDeposit", "permit", |
| 18 | + "previewDeposit", "previewMint", "previewRedeem", |
| 19 | + "previewWithdraw", "REBALANCER_ROLE", "redeem", "renounceRole", |
| 20 | + "reservedAssets", "reservePercentage", "revokeRole", |
| 21 | + "stakedAssets", "supportsInterface", "symbol", "totalAssets", |
| 22 | + "totalSupply", "transfer", "transferFrom", "underlyingToken", |
| 23 | + "version", "withdraw", "yield", "YIELD_COLLECTOR_ROLE", |
| 24 | + "yieldRecipient", "yieldVault", |
| 25 | + "yieldVaultMaximumSlippagePercentage", |
| 26 | + ] }, |
| 27 | + ], |
| 28 | + "VaultBridgeTokenInitializer": [ { |
| 29 | + "extension": "VaultBridgeTokenPart2", |
| 30 | + "exclude": [ "rebalanceReserve", |
| 31 | + "allowance", "approve", "asset", "backingDifference", |
| 32 | + "balanceOf", "claimAndRedeem", "convertToAssets", |
| 33 | + "convertToShares", "decimals", "DEFAULT_ADMIN_ROLE", "deposit", |
| 34 | + "depositAndBridge", "depositWithPermit", |
| 35 | + "depositWithPermitAndBridge", "DOMAIN_SEPARATOR", |
| 36 | + "eip712Domain", "getRoleAdmin", "grantRole", "hasRole", |
| 37 | + "lxlyBridge", "lxlyId", "maxDeposit", "maxMint", "maxRedeem", |
| 38 | + "maxWithdraw", "migrationFeesFund", "migrationManager", |
| 39 | + "minimumReservePercentage", "minimumYieldVaultDeposit", "mint", |
| 40 | + "name", "nonces", "paused", "PAUSER_ROLE", |
| 41 | + "performReversibleYieldVaultDeposit", "permit", |
| 42 | + "previewDeposit", "previewMint", "previewRedeem", |
| 43 | + "previewWithdraw", "REBALANCER_ROLE", "redeem", "renounceRole", |
| 44 | + "reservedAssets", "reservePercentage", "revokeRole", |
| 45 | + "stakedAssets", "supportsInterface", "symbol", "totalAssets", |
| 46 | + "totalSupply", "transfer", "transferFrom", "underlyingToken", |
| 47 | + "version", "withdraw", "yield", "YIELD_COLLECTOR_ROLE", |
| 48 | + "yieldRecipient", "yieldVault", |
| 49 | + "yieldVaultMaximumSlippagePercentage", |
| 50 | + ] }, |
| 51 | + ], |
| 52 | + }, |
| 53 | + "contract_recursion_limit": "1", |
| 54 | + "disable_auto_cache_key_gen": true, |
| 55 | + "files": [ |
| 56 | + "certora/harnesses/StorageExtension.sol", |
| 57 | + "certora/harnesses/GenericVaultBridgeToken.sol", |
| 58 | + "certora/mocks/ILxLyBridgeMock.sol", |
| 59 | + "certora/mocks/TokenMock.sol", |
| 60 | + "certora/mocks/VaultMock.sol", |
| 61 | + "src/VaultBridgeTokenInitializer.sol", |
| 62 | + "src/VaultBridgeTokenPart2.sol", |
| 63 | + ], |
| 64 | + "server": "production", |
| 65 | + "global_timeout": "7200", |
| 66 | + "smt_timeout": "7200", |
| 67 | + "loop_iter": "2", |
| 68 | + "link": [ |
| 69 | + "VaultMock:asset=TokenMock", |
| 70 | + ], |
| 71 | + "msg": "GenericVaultBridgeToken", |
| 72 | + "mutations": { |
| 73 | + "gambit": [ |
| 74 | + { |
| 75 | + "filename": "src/vault-bridge-tokens/GenericVaultBridgeToken.sol", |
| 76 | + "num_mutants": 5 |
| 77 | + } |
| 78 | + ] |
| 79 | + }, |
| 80 | + "optimistic_contract_recursion": true, |
| 81 | + "optimistic_hashing": true, |
| 82 | + "optimistic_loop": true, |
| 83 | + "optimistic_summary_recursion": true, |
| 84 | + "packages": [ |
| 85 | + "@types/bun=node_modules/@types/bun", |
| 86 | + "@0xpolygonhermez/zkevm-commonjs=node_modules/@0xpolygonhermez/zkevm-commonjs", |
| 87 | + "@openzeppelin-contracts-upgradeable=dependencies/@openzeppelin-contracts-upgradeable-5.1.0", |
| 88 | + "@openzeppelin-contracts=dependencies/@openzeppelin-contracts-5.1.0", |
| 89 | + "@openzeppelin/contracts=dependencies/@openzeppelin-contracts-5.1.0", |
| 90 | + "forge-std=dependencies/forge-std-1.9.4/src", |
| 91 | + // for zkmevm-contracts |
| 92 | + "@openzeppelin/contracts-upgradeable4=zkevm-contracts/node_modules/@openzeppelin/contracts-upgradeable4", |
| 93 | + "@openzeppelin/contracts-upgradeable5=zkevm-contracts/node_modules/@openzeppelin/contracts-upgradeable5", |
| 94 | + "@zkmcontractsv2=zkevm-contracts/contracts/v2", |
| 95 | + ], |
| 96 | + "process": "emv", |
| 97 | + "prover_args": [ |
| 98 | + "-maxDecompiledCommandCount 5000000", |
| 99 | + "-maxBlockCount 500000", |
| 100 | + ], |
| 101 | + "rule_sanity": "basic", |
| 102 | + "prover_version": "master", |
| 103 | + "parametric_contracts": ["GenericVaultBridgeToken", "VaultBridgeTokenPart2"], |
| 104 | + "solc_map": { |
| 105 | + "StorageExtension": "solc8.29", |
| 106 | + "GenericVaultBridgeToken": "solc8.29", |
| 107 | + "MigrationManager": "solc8.29", |
| 108 | + "VaultBridgeTokenInitializer": "solc8.29", |
| 109 | + "VaultBridgeTokenPart2": "solc8.29", |
| 110 | + "ILxLyBridgeMock": "solc8.29", |
| 111 | + "VaultMock": "solc8.29", |
| 112 | + "TokenMock": "solc8.28", |
| 113 | + }, |
| 114 | + "solc_optimize": "200", |
| 115 | + //"build_cache": true, |
| 116 | + "solc_via_ir": true, |
| 117 | + "storage_extension_harnesses": [ |
| 118 | + "GenericVaultBridgeToken=StorageExtension", |
| 119 | + "VaultBridgeTokenInitializer=StorageExtension", |
| 120 | + ], |
| 121 | + "struct_link": [ |
| 122 | + "GenericVaultBridgeToken:lxlyBridge=ILxLyBridgeMock", |
| 123 | + "GenericVaultBridgeToken:underlyingToken=TokenMock", |
| 124 | + "GenericVaultBridgeToken:yieldVault=VaultMock", |
| 125 | + "GenericVaultBridgeToken:_vaultBridgeTokenPart2=VaultBridgeTokenPart2", |
| 126 | + "VaultBridgeTokenInitializer:underlyingToken=TokenMock", |
| 127 | + "VaultBridgeTokenInitializer:yieldVault=VaultMock", |
| 128 | + ], |
| 129 | + "summary_recursion_limit": "2", |
| 130 | + "verify": "GenericVaultBridgeToken:certora/specs/GenericVaultBridgeToken_ERC4626.spec" |
| 131 | +} |
0 commit comments