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