codex-contracts-eth/certora/confs/Marketplace.conf

{
    "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",
}
Set up certora and implement first rules (#122) Co-authored-by: 0xb337r007 <0xe4e5@proton.me> Co-authored-by: Adam Uhlíř <adam@uhlir.dev> 2024-07-24 18:50:18 +02:00			`{`
			`"files": [`
chore: formally verify request state changes This commit adds CVL rule that formally verifies the state changes of any given request in relation to the functions of the contract that can cause them. Closes #128 2024-08-05 16:27:20 +02:00			`"certora/harness/MarketplaceHarness.sol",`
Set up certora and implement first rules (#122) Co-authored-by: 0xb337r007 <0xe4e5@proton.me> Co-authored-by: Adam Uhlíř <adam@uhlir.dev> 2024-07-24 18:50:18 +02:00			`"contracts/Marketplace.sol",`
			`"contracts/Groth16Verifier.sol",`
			`"certora/helpers/ERC20A.sol",`
			`],`
chore(certora): set MarketplaceHarness as parametric_contract config value 2024-08-16 11:59:59 +02:00			`"parametric_contracts": ["MarketplaceHarness"],`
Set up certora and implement first rules (#122) Co-authored-by: 0xb337r007 <0xe4e5@proton.me> Co-authored-by: Adam Uhlíř <adam@uhlir.dev> 2024-07-24 18:50:18 +02:00			`"link" : [`
chore(certora): set MarketplaceHarness as parametric_contract config value 2024-08-16 11:59:59 +02:00			`"MarketplaceHarness:_token=ERC20A",`
			`"MarketplaceHarness:_verifier=Groth16Verifier"`
Set up certora and implement first rules (#122) Co-authored-by: 0xb337r007 <0xe4e5@proton.me> Co-authored-by: Adam Uhlíř <adam@uhlir.dev> 2024-07-24 18:50:18 +02:00			`],`
chore(certora): set MarketplaceHarness as parametric_contract config value 2024-08-16 11:59:59 +02:00			`"msg": "Verifying MarketplaceHarness",`
Set up certora and implement first rules (#122) Co-authored-by: 0xb337r007 <0xe4e5@proton.me> Co-authored-by: Adam Uhlíř <adam@uhlir.dev> 2024-07-24 18:50:18 +02:00			`"rule_sanity": "basic",`
chore: formally verify request state changes This commit adds CVL rule that formally verifies the state changes of any given request in relation to the functions of the contract that can cause them. Closes #128 2024-08-05 16:27:20 +02:00			`"verify": "MarketplaceHarness:certora/specs/Marketplace.spec",`
Set up certora and implement first rules (#122) Co-authored-by: 0xb337r007 <0xe4e5@proton.me> Co-authored-by: Adam Uhlíř <adam@uhlir.dev> 2024-07-24 18:50:18 +02:00			`"optimistic_loop": true,`
			`"loop_iter": "3",`
			`"optimistic_hashing": true,`
			`"hashing_length_bound": "512",`
			`}`