{ "files": [ "contracts/Vault.sol", // "certora/harness/MarketplaceHarness.sol", // "contracts/Marketplace.sol", // "contracts/Vault.sol", // "contracts/Groth16Verifier.sol", "certora/helpers/ERC20A.sol", ], "parametric_contracts": ["Vault"], "link" : [ "Vault:_token=ERC20A", // "MarketplaceHarness:_vault=Vault", // "MarketplaceHarness:_verifier=Groth16Verifier" ], "packages": [ "@openzeppelin/=node_modules/@openzeppelin/", ], "msg": "Verifying Vault", "rule_sanity": "basic", "verify": "Vault:certora/specs/Vault.spec", // "optimistic_loop": true, "loop_iter": "3", // "optimistic_hashing": true, // "hashing_length_bound": "512", "solc": "solc8.28", }