From f4139480e22da6ff4fda40a8a43364717b136b64 Mon Sep 17 00:00:00 2001 From: sendra Date: Thu, 25 Jul 2024 16:03:34 +0200 Subject: [PATCH] fix: updated certora rules --- .../confs/verifyCrossChainControllerWithEmergency.conf | 4 +--- .../verifyCrossChainForwarder-encode-decode-correct.conf | 4 +--- .../certora/confs/verifyCrossChainForwarder-envelopRetry.conf | 4 +--- .../certora/confs/verifyCrossChainForwarder-invariants.conf | 4 +--- .../certora/confs/verifyCrossChainForwarder-newEnvelope.conf | 4 +--- security/certora/confs/verifyCrossChainForwarder-sanity.conf | 4 +--- security/certora/confs/verifyCrossChainForwarder-shuffle.conf | 4 +--- .../certora/confs/verifyCrossChainForwarder-simpleRules.conf | 4 +--- security/certora/confs/verifyCrossChainReceiver.conf | 4 +--- 9 files changed, 9 insertions(+), 27 deletions(-) diff --git a/security/certora/confs/verifyCrossChainControllerWithEmergency.conf b/security/certora/confs/verifyCrossChainControllerWithEmergency.conf index 1e23f4ac..6f14e437 100644 --- a/security/certora/confs/verifyCrossChainControllerWithEmergency.conf +++ b/security/certora/confs/verifyCrossChainControllerWithEmergency.conf @@ -8,11 +8,9 @@ "optimistic_hashing": true, "optimistic_loop": true, "packages": [ - "solidity-utils/=lib/aave-helpers/lib/solidity-utils/src", + "solidity-utils/=lib/solidity-utils/src", "forge-std/=lib/aave-helpers/lib/forge-std/src", "openzeppelin-contracts/=lib/openzeppelin-contracts", - "aave-helpers/=lib/aave-helpers/src", - "aave-address-book/=lib/aave-helpers/lib/aave-address-book/src", ], "process": "emv", "prover_args": [ diff --git a/security/certora/confs/verifyCrossChainForwarder-encode-decode-correct.conf b/security/certora/confs/verifyCrossChainForwarder-encode-decode-correct.conf index 732947d8..8d80db6f 100644 --- a/security/certora/confs/verifyCrossChainForwarder-encode-decode-correct.conf +++ b/security/certora/confs/verifyCrossChainForwarder-encode-decode-correct.conf @@ -5,11 +5,9 @@ ], "link": [], "packages": [ - "solidity-utils/=lib/aave-helpers/lib/solidity-utils/src", + "solidity-utils/=lib/solidity-utils/src", "forge-std/=lib/aave-helpers/lib/forge-std/src", "openzeppelin-contracts/=lib/openzeppelin-contracts", - "aave-helpers/=lib/aave-helpers/src", - "aave-address-book/=lib/aave-helpers/lib/aave-address-book/src", ], "verify": "CrossChainForwarderHarnessED:security/certora/specs/CrossChainForwarder-encode-decode-correct.spec", "solc": "solc8.19", diff --git a/security/certora/confs/verifyCrossChainForwarder-envelopRetry.conf b/security/certora/confs/verifyCrossChainForwarder-envelopRetry.conf index 634a09d6..03d75474 100644 --- a/security/certora/confs/verifyCrossChainForwarder-envelopRetry.conf +++ b/security/certora/confs/verifyCrossChainForwarder-envelopRetry.conf @@ -5,11 +5,9 @@ ], "link": [], "packages": [ - "solidity-utils/=lib/aave-helpers/lib/solidity-utils/src", + "solidity-utils/=lib/solidity-utils/src", "forge-std/=lib/aave-helpers/lib/forge-std/src", "openzeppelin-contracts/=lib/openzeppelin-contracts", - "aave-helpers/=lib/aave-helpers/src", - "aave-address-book/=lib/aave-helpers/lib/aave-address-book/src", ], "verify": "CrossChainForwarderHarness:security/certora/specs/CrossChainForwarder-envelopRetry.spec", "solc": "solc8.19", diff --git a/security/certora/confs/verifyCrossChainForwarder-invariants.conf b/security/certora/confs/verifyCrossChainForwarder-invariants.conf index 3b8960f1..3507fc6c 100644 --- a/security/certora/confs/verifyCrossChainForwarder-invariants.conf +++ b/security/certora/confs/verifyCrossChainForwarder-invariants.conf @@ -5,11 +5,9 @@ ], "link": [], "packages": [ - "solidity-utils/=lib/aave-helpers/lib/solidity-utils/src", + "solidity-utils/=lib/solidity-utils/src", "forge-std/=lib/aave-helpers/lib/forge-std/src", "openzeppelin-contracts/=lib/openzeppelin-contracts", - "aave-helpers/=lib/aave-helpers/src", - "aave-address-book/=lib/aave-helpers/lib/aave-address-book/src", ], "verify": "CrossChainForwarderHarness:security/certora/specs/invariants.spec", "solc": "solc8.19", diff --git a/security/certora/confs/verifyCrossChainForwarder-newEnvelope.conf b/security/certora/confs/verifyCrossChainForwarder-newEnvelope.conf index ab0b4295..810a41b9 100644 --- a/security/certora/confs/verifyCrossChainForwarder-newEnvelope.conf +++ b/security/certora/confs/verifyCrossChainForwarder-newEnvelope.conf @@ -5,11 +5,9 @@ ], "link": [], "packages": [ - "solidity-utils/=lib/aave-helpers/lib/solidity-utils/src", + "solidity-utils/=lib/solidity-utils/src", "forge-std/=lib/aave-helpers/lib/forge-std/src", "openzeppelin-contracts/=lib/openzeppelin-contracts", - "aave-helpers/=lib/aave-helpers/src", - "aave-address-book/=lib/aave-helpers/lib/aave-address-book/src", ], "verify": "CrossChainForwarderHarness:security/certora/specs/CrossChainForwarder-newEnvelope.spec", "solc": "solc8.19", diff --git a/security/certora/confs/verifyCrossChainForwarder-sanity.conf b/security/certora/confs/verifyCrossChainForwarder-sanity.conf index aa232247..64dc1167 100644 --- a/security/certora/confs/verifyCrossChainForwarder-sanity.conf +++ b/security/certora/confs/verifyCrossChainForwarder-sanity.conf @@ -5,11 +5,9 @@ ], "link": [], "packages": [ - "solidity-utils/=lib/aave-helpers/lib/solidity-utils/src", + "solidity-utils/=lib/solidity-utils/src", "forge-std/=lib/aave-helpers/lib/forge-std/src", "openzeppelin-contracts/=lib/openzeppelin-contracts", - "aave-helpers/=lib/aave-helpers/src", - "aave-address-book/=lib/aave-helpers/lib/aave-address-book/src", ], "verify": "CrossChainForwarderHarness:security/certora/specs/CrossChainForwarder-sanity.spec", "solc": "solc8.19", diff --git a/security/certora/confs/verifyCrossChainForwarder-shuffle.conf b/security/certora/confs/verifyCrossChainForwarder-shuffle.conf index d339929e..fffea3c7 100644 --- a/security/certora/confs/verifyCrossChainForwarder-shuffle.conf +++ b/security/certora/confs/verifyCrossChainForwarder-shuffle.conf @@ -5,11 +5,9 @@ ], "link": [], "packages": [ - "solidity-utils/=lib/aave-helpers/lib/solidity-utils/src", + "solidity-utils/=lib/solidity-utils/src", "forge-std/=lib/aave-helpers/lib/forge-std/src", "openzeppelin-contracts/=lib/openzeppelin-contracts", - "aave-helpers/=lib/aave-helpers/src", - "aave-address-book/=lib/aave-helpers/lib/aave-address-book/src", ], "verify": "CrossChainForwarderHarness:security/certora/specs/CrossChainForwarder-shuffle.spec", "solc": "solc8.19", diff --git a/security/certora/confs/verifyCrossChainForwarder-simpleRules.conf b/security/certora/confs/verifyCrossChainForwarder-simpleRules.conf index 3ebe53d2..d4c994fd 100644 --- a/security/certora/confs/verifyCrossChainForwarder-simpleRules.conf +++ b/security/certora/confs/verifyCrossChainForwarder-simpleRules.conf @@ -5,11 +5,9 @@ ], "link": [], "packages": [ - "solidity-utils/=lib/aave-helpers/lib/solidity-utils/src", + "solidity-utils/=lib/solidity-utils/src", "forge-std/=lib/aave-helpers/lib/forge-std/src", "openzeppelin-contracts/=lib/openzeppelin-contracts", - "aave-helpers/=lib/aave-helpers/src", - "aave-address-book/=lib/aave-helpers/lib/aave-address-book/src", ], "verify": "CrossChainForwarderHarness:security/certora/specs/CrossChainForwarder-simpleRules.spec", "solc": "solc8.19", diff --git a/security/certora/confs/verifyCrossChainReceiver.conf b/security/certora/confs/verifyCrossChainReceiver.conf index 95a66182..948ccd45 100644 --- a/security/certora/confs/verifyCrossChainReceiver.conf +++ b/security/certora/confs/verifyCrossChainReceiver.conf @@ -11,11 +11,9 @@ "optimistic_hashing": true, "optimistic_loop": true, "packages": [ - "solidity-utils/=lib/aave-helpers/lib/solidity-utils/src", + "solidity-utils/=lib/solidity-utils/src", "forge-std/=lib/aave-helpers/lib/forge-std/src", "openzeppelin-contracts/=lib/openzeppelin-contracts", - "aave-helpers/=lib/aave-helpers/src", - "aave-address-book/=lib/aave-helpers/lib/aave-address-book/src", ], "process": "emv", "prover_args": [