fix: updated certora rules

bgd-labs · Jul 25, 2024 · f413948 · f413948
1 parent dcc5b30
commit f413948
Show file tree

Hide file tree

Showing 9 changed files with 9 additions and 27 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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": [