migration to CVL2. AToken.spec get timedout

Certora · Sep 12, 2023 · 38fd449 · 38fd449
1 parent 27a6d5c
commit 38fd449
Show file tree

Hide file tree

Showing 13 changed files with 500 additions and 419 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -46,7 +46,7 @@ jobs:
           make munged
           cd ..
           echo "key length" ${#CERTORAKEY}
-          sh certora/scripts/${{ matrix.rule }}
+          certoraRun certora/conf/${{ matrix.rule }}
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
 
@@ -55,9 +55,9 @@ jobs:
       max-parallel: 16
       matrix:
         rule:
-          - verifyAToken.sh
-          - verifyPool.sh getReserveNormalizedVariableDebtCheck
-          - verifyReserveConfiguration.sh
-          - verifyStableTokenCLI.sh
-          - verifyUserConfigCLI.sh
-          - verifyVariableTokenCLI.sh
+          - AToken.conf
+          - Pool.conf
+          - ReserveConfiguration.conf
+          - StableTokenCLI.conf
+          - UserConfigCLI.conf
+          - VariableTokenCLI.conf
diff --git a/certora/conf/AToken.conf b/certora/conf/AToken.conf
@@ -0,0 +1,15 @@
+{
+    "cloud": "",
+    "files": [
+        "certora/harness/ATokenHarness.sol",
+        "certora/harness/SimpleERC20.sol"
+    ],
+    "link": [
+        "ATokenHarness:_underlyingAsset=SimpleERC20"
+    ],
+    "optimistic_loop": true,
+    "process": "emv",
+    "solc": "solc8.10",
+    "verify": "ATokenHarness:certora/specs/AToken.spec",
+    "msg": "aToken spec"
+ }
diff --git a/certora/conf/Pool.conf b/certora/conf/Pool.conf
@@ -0,0 +1,23 @@
+{
+    "files": [
+        "certora/harness/ATokenHarness.sol",
+        "certora/harness/PoolHarness.sol",
+        "certora/harness/StableDebtTokenHarness.sol",
+        "certora/munged/protocol/tokenization/VariableDebtToken.sol"
+    ],
+    "link": [
+        "ATokenHarness:POOL=PoolHarness"
+    ],
+    "rule": [
+        "getReserveNormalizedVariableDebtCheck"
+    ],
+    "optimistic_loop": true,
+    "process": "emv",
+    "cloud": "",
+    "prover_args": ["-depth 40","-mediumTimeout 700"],
+    "smt_timeout": "600",
+    "solc": "solc8.10",
+    "verify": "PoolHarness:certora/specs/pool.spec",
+    "msg": "Pool"
+}
+
diff --git a/certora/conf/ReserveConfiguration.conf b/certora/conf/ReserveConfiguration.conf
@@ -0,0 +1,14 @@
+{
+    "cloud": "",
+    "files": [
+        "certora/harness/ReserveConfigurationHarness.sol"
+    ],
+    "msg": "ReserveConfiguration",
+    "optimistic_loop": true,
+    "process": "emv",
+    "prover_args": [
+        "-useBitVectorTheory"
+    ],
+    "solc": "solc8.10",
+    "verify": "ReserveConfigurationHarness:certora/specs/ReserveConfiguration.spec"
+}
diff --git a/certora/conf/StableTokenCLI.conf b/certora/conf/StableTokenCLI.conf
@@ -0,0 +1,13 @@
+{
+    "cache": "StableToken",
+    "cloud": "",
+    "files": [
+        "certora/harness/StableDebtTokenHarness.sol:StableDebtTokenHarness"
+    ],
+    "loop_iter": "4",
+    "msg": "stableTokenCLI",
+    "optimistic_loop": true,
+    "process": "emv",
+    "solc": "solc8.10",
+    "verify": "StableDebtTokenHarness:certora/specs/StableDebtToken.spec"
+}
diff --git a/certora/conf/UserConfigCLI.conf b/certora/conf/UserConfigCLI.conf
@@ -0,0 +1,14 @@
+{
+    "cloud": "",
+    "files": [
+        "certora/harness/UserConfigurationHarness.sol"
+    ],
+    "msg": "UserConfiguration All spec",
+    "optimistic_loop": true,
+    "process": "emv",
+    "prover_args": [
+        "-useBitVectorTheory"
+    ],
+    "solc": "solc8.10",
+    "verify": "UserConfigurationHarness:certora/specs/UserConfiguration.spec"
+}
diff --git a/certora/conf/VariableTokenCLI.conf b/certora/conf/VariableTokenCLI.conf
@@ -0,0 +1,11 @@
+{
+    "cloud": "",
+    "files": [
+        "certora/harness/VariableDebtTokenHarness.sol"
+    ],
+    "msg": "variable debt token",
+    "optimistic_loop": true,
+    "process": "emv",
+    "solc": "solc8.10",
+    "verify": "VariableDebtTokenHarness:certora/specs/VariableDebtToken.spec"
+}