certora updates (#17)

* certora updates * ignore solidity warnings in servicer * ignore solidity warnings rollover manager * replace newSplitParallel certora config proverarg * get rid of branch versions of certora * replace newSplitParallel certora config proverarg * update access roles test for servicer with new controller function for mint access * remove extra semicolon * remove specialist role from servicer specs certora * link controller to servicer in servicer spec for certora * prevent previous term locker from conflicting with controller treasury address * add envfree declaration of get treasury address to rollover exposure certora spec * no zero address msg sender in exposure opening on new rollover certora * treasuery cannot be borrow address * treasuery cannot be borrow address * treasuery address always 100 * treasuery address always 100 * 100 address for treasury imported from rules for servicer * 100 address for treasury imported from rules for servicer * 100 address for treasury imported from rules for servicer * controller harness for certora * controller harness for certora * fix acccess roles for servicer certora spec * 100 address for treasury imported from rules for servicer * 100 address for treasury imported from rules for servicer * further split tests * undo servicer update * minting changes certora spec * minting changes certora spec * beta cli runs for errors in certora prod * add 2 new reverts for repayments in certora * NONDET summary for access roles controller call for mint open exposure certora * split repay and redemption revert certora specs * add semicolon to end of summary in access roles servicer certora * ignore solidity warnings certora * split repay and redemption revert certora specs * verify mint exposure access methods certora * add env to verifyMintExposureAccess calls * DISPATCHER true verifyMintExposureAccess * trying to get linking to work * trying to get linking to work * trying to get linking to work * trying to get linking to work * redemption reverts branch version removed * redemption reverts branch version removed * redemption reverts branch version removed * get mint integrity to stop timing out
term-finance · Jun 27, 2024 · 262098c · 262098c
1 parent 7da1ba7
commit 262098c
Show file tree

Hide file tree

Showing 35 changed files with 384 additions and 53 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -44,15 +44,12 @@ jobs:
           - "termRepoCollateralManager.conf"
           - "termRepoLocker.conf"
           - "termRepoRolloverManager.conf"
-          - "termRepoServicer.conf"
           - "termRepoServicer-lockFulfill.conf"
-          - "termRepoServicer-lockFulfillReverts.conf"
           - "termRepoServicer-mintCollapse.conf"
+          - "termRepoServicer-mintIntegrity.conf"
           - "termRepoServicer-mintCollapseReverts.conf"
           - "termRepoServicer-repaymentsRedemptions.conf"
-          - "termRepoServicer-repaymentsRedemptionsReverts.conf"
           - "termRepoServicer-stateVariables.conf"
-          - "termRepoServicer.conf"
           - "termRepoToken.conf"
     steps:
       - uses: actions/checkout@master
@@ -83,3 +80,44 @@ jobs:
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
           SOLC_VERSION: 0.8.18
+  formal-verfication-beta:
+    runs-on: ubuntu-latest
+    needs: test
+    strategy:
+      matrix:
+        ruleset:
+          - "termRepoServicer-lockFulfillReverts.conf"
+          - "termRepoServicer-repaymentsReverts.conf"
+          - "termRepoServicer-redemptionsReverts.conf"
+          - "termRepoServicer-rolloverReverts.conf"
+          - "termRepoServicer.conf"
+    steps:
+      - uses: actions/checkout@master
+        with:
+          fetch-depth: 0
+      - uses: actions/setup-node@v4
+        with:
+          node-version: "18.15"
+          cache: yarn
+      - uses: actions/setup-python@v4
+        with:
+          python-version: "3.11"
+      - run: |
+          yarn install --immutable
+          yarn build
+      - run: |
+          pip3 install certora-cli-beta
+      - run: |
+          msg="${2:-"$(hostname) - ${conf_file} - $(date +%s)"}"
+
+          pip3 install solc-select
+          solc-select install ${SOLC_VERSION}
+
+          certoraRun "./certora/confs/${{ matrix.ruleset }}" \
+            --msg "$(hostname) - ${{ matrix.ruleset }} - $(date +%s)" \
+            --wait_for_results all \
+            --rule_sanity basic
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+          SOLC_VERSION: 0.8.18
+
diff --git a/certora/confs/termAuctionBidLocker-locking.conf b/certora/confs/termAuctionBidLocker-locking.conf
@@ -21,6 +21,6 @@
     ],
     "server": "production",
     "rule_sanity": "basic",
-    "contract_compiler_skip_severe_warning_as_error": true,
+    "ignore_solidity_warnings": true,
     "verify": "TermAuctionBidLockerHarness:certora/specs/termAuctionBidLocker/rulesLocking.spec"
 }
diff --git a/certora/confs/termAuctionBidLocker-lockingReverts.conf b/certora/confs/termAuctionBidLocker-lockingReverts.conf
@@ -21,6 +21,6 @@
     ],
     "server": "production",
     "rule_sanity": "basic",
-    "contract_compiler_skip_severe_warning_as_error": true,
+    "ignore_solidity_warnings": true,
     "verify": "TermAuctionBidLockerHarness:certora/specs/termAuctionBidLocker/rulesLockingReverts.spec"
 }
diff --git a/certora/confs/termAuctionBidLocker-stateVariables.conf b/certora/confs/termAuctionBidLocker-stateVariables.conf
@@ -21,6 +21,6 @@
     ],
     "server": "production",
     "rule_sanity": "basic",
-    "contract_compiler_skip_severe_warning_as_error": true,
+    "ignore_solidity_warnings": true,
     "verify": "TermAuctionBidLockerHarness:certora/specs/termAuctionBidLocker/rulesStateVariables.spec"
 }
diff --git a/certora/confs/termAuctionBidLocker.conf b/certora/confs/termAuctionBidLocker.conf
@@ -21,6 +21,6 @@
     ],
     "server": "production",
     "rule_sanity": "basic",
-    "contract_compiler_skip_severe_warning_as_error": true,
+    "ignore_solidity_warnings": true,
     "verify": "TermAuctionBidLockerHarness:certora/specs/termAuctionBidLocker/rules.spec"
 }
diff --git a/certora/confs/termRepoCollateralManager-batchDefault.conf b/certora/confs/termRepoCollateralManager-batchDefault.conf
@@ -21,7 +21,7 @@
     "solc_optimize": "50",
     "loop_iter": "2",
     "optimistic_loop": true,
-    "contract_compiler_skip_severe_warning_as_error": true,
+    "ignore_solidity_warnings": true,
     "prover_args": [
         "-smt_initialSplitDepth 3",
         "-depth 10"

diff --git a/certora/confs/termRepoCollateralManager-batchLiquidation.conf b/certora/confs/termRepoCollateralManager-batchLiquidation.conf
@@ -21,7 +21,7 @@
     "solc_optimize": "50",
     "loop_iter": "2",
     "optimistic_loop": true,
-    "contract_compiler_skip_severe_warning_as_error": true,
+    "ignore_solidity_warnings": true,
     "prover_args": [
         "-smt_initialSplitDepth 3",
         "-depth 10"

diff --git a/certora/confs/termRepoCollateralManager-batchLiquidationWithRepoToken.conf b/certora/confs/termRepoCollateralManager-batchLiquidationWithRepoToken.conf
@@ -21,7 +21,7 @@
     "solc_optimize": "50",
     "loop_iter": "2",
     "optimistic_loop": true,
-    "contract_compiler_skip_severe_warning_as_error": true,
+    "ignore_solidity_warnings": true,
 	"prover_args": [
 		"-smt_initialSplitDepth 4",
 		"-depth 20",

diff --git a/certora/confs/termRepoCollateralManager-stateVariables.conf b/certora/confs/termRepoCollateralManager-stateVariables.conf
@@ -21,7 +21,7 @@
     "solc_optimize": "50",
     "loop_iter": "3",
     "optimistic_loop": true,
-    "contract_compiler_skip_severe_warning_as_error": true,
+    "ignore_solidity_warnings": true,
     "prover_args": [
         "-depth 15",
         "-splitParallel true"

diff --git a/certora/confs/termRepoCollateralManager.conf b/certora/confs/termRepoCollateralManager.conf
@@ -21,7 +21,7 @@
     "solc_optimize": "50",
     "loop_iter": "3",
     "optimistic_loop": true,
-    "contract_compiler_skip_severe_warning_as_error": true,
+    "ignore_solidity_warnings": true,
     "prover_args": [
         "-depth 15",
         "-splitParallel true"

diff --git a/certora/confs/termRepoRolloverManager.conf b/certora/confs/termRepoRolloverManager.conf
@@ -15,7 +15,7 @@
     "solc_optimize": "50",
     "loop_iter": "3",
     "optimistic_loop": true,
-    "contract_compiler_skip_severe_warning_as_error": true,
+    "ignore_solidity_warnings": true,
     "parametric_contracts": [
         "TermRepoRolloverManagerHarness"
     ],

diff --git a/certora/confs/termRepoServicer-lockFulfill.conf b/certora/confs/termRepoServicer-lockFulfill.conf
@@ -20,14 +20,14 @@
 		"-smt_initialSplitDepth 5",
 		"-depth 15",
 		"-mediumTimeout 20",
-		"-newSplitParallel true",
+		"-splitParallel true",
 		"-splitParallelTimelimit 7200",
 		"-splitParallelInitialDepth 10"
 	],
     "solc_optimize": "50",
     "loop_iter": "2",
     "optimistic_loop": true,
-    "contract_compiler_skip_severe_warning_as_error": true,
+    "ignore_solidity_warnings": true,
 
     "smt_timeout": "7200",
     "parametric_contracts": [

diff --git a/certora/confs/termRepoServicer-lockFulfillReverts.conf b/certora/confs/termRepoServicer-lockFulfillReverts.conf
@@ -27,7 +27,7 @@
     "solc_optimize": "50",
     "loop_iter": "2",
     "optimistic_loop": true,
-    "contract_compiler_skip_severe_warning_as_error": true,
+    "ignore_solidity_warnings": true,
 
     "smt_timeout": "7200",
     "parametric_contracts": [

diff --git a/certora/confs/termRepoServicer-mintCollapse.conf b/certora/confs/termRepoServicer-mintCollapse.conf
@@ -20,14 +20,14 @@
 		"-smt_initialSplitDepth 5",
 		"-depth 15",
 		"-mediumTimeout 2",
-		"-newSplitParallel true",
+		"-splitParallel true",
 		"-splitParallelTimelimit 7200",
 		"-splitParallelInitialDepth 5"
 	],
     "solc_optimize": "50",
     "loop_iter": "2",
     "optimistic_loop": true,
-    "contract_compiler_skip_severe_warning_as_error": true,
+    "ignore_solidity_warnings": true,
     "smt_timeout": "7200",
     "parametric_contracts": [
         "TermRepoServicerHarness"

diff --git a/certora/confs/termRepoServicer-mintCollapseReverts.conf b/certora/confs/termRepoServicer-mintCollapseReverts.conf
@@ -23,7 +23,7 @@
     "solc_optimize": "50",
     "loop_iter": "2",
     "optimistic_loop": true,
-    "contract_compiler_skip_severe_warning_as_error": true,
+    "ignore_solidity_warnings": true,
     "smt_timeout": "7200",
     "parametric_contracts": [
         "TermRepoServicerHarness"

diff --git a/certora/confs/termRepoServicer-mintIntegrity.conf b/certora/confs/termRepoServicer-mintIntegrity.conf
@@ -0,0 +1,37 @@
+{
+    "files": [
+        "certora/harness/TermRepoServicerHarness.sol",
+        "contracts/TermAuctionBidLocker.sol",
+        "contracts/TermController.sol",
+        "contracts/TermRepoLocker.sol",
+        "contracts/TermRepoToken.sol",
+        "contracts/TermRepoRolloverManager.sol",
+        "certora/harness/TermRepoCollateralManagerHarness.sol",
+        "certora/helpers/DummyERC20A.sol"
+    ],
+    "link": [
+        "TermRepoServicerHarness:termRepoToken=TermRepoToken",
+        "TermRepoServicerHarness:termRepoLocker=TermRepoLocker",
+        "TermRepoServicerHarness:termRepoCollateralManager=TermRepoCollateralManagerHarness",
+        "TermRepoServicerHarness:termRepoRolloverManager=TermRepoRolloverManager",
+        "TermRepoCollateralManagerHarness:termRepoLocker=TermRepoLocker"
+    ],
+    "prover_args": [
+		"-depth 15",
+        "-splitParallel true"
+	],
+    "solc_optimize": "50",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "ignore_solidity_warnings": true,
+    "smt_timeout": "7200",
+    "parametric_contracts": [
+        "TermRepoServicerHarness"
+    ],
+    "rule_sanity": "basic",
+    "packages": [
+        "@chainlink=node_modules/@chainlink",
+        "@openzeppelin=node_modules/@openzeppelin"
+    ],
+    "verify": "TermRepoServicerHarness:certora/specs/termRepoServicer/rulesMintIntegrity.spec"
+}
diff --git a/certora/confs/termRepoServicer-redemptionsReverts.conf b/certora/confs/termRepoServicer-redemptionsReverts.conf
@@ -0,0 +1,37 @@
+{
+    "files": [
+        "certora/harness/TermRepoServicerHarness.sol",
+        "contracts/TermAuctionBidLocker.sol",
+        "contracts/TermController.sol",
+        "contracts/TermRepoLocker.sol",
+        "contracts/TermRepoToken.sol",
+        "contracts/TermRepoRolloverManager.sol",
+        "certora/harness/TermRepoCollateralManagerHarness.sol",
+        "certora/helpers/DummyERC20A.sol"
+    ],
+    "link": [
+        "TermRepoServicerHarness:termRepoToken=TermRepoToken",
+        "TermRepoServicerHarness:termRepoLocker=TermRepoLocker",
+        "TermRepoServicerHarness:termRepoCollateralManager=TermRepoCollateralManagerHarness",
+        "TermRepoServicerHarness:termRepoRolloverManager=TermRepoRolloverManager",
+        "TermRepoCollateralManagerHarness:termRepoLocker=TermRepoLocker"
+    ],
+    "prover_args": [
+		"-depth 15",
+        "-splitParallel true"
+	],
+    "solc_optimize": "50",
+    "ignore_solidity_warnings": true,
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "smt_timeout": "7200",
+    "parametric_contracts": [
+        "TermRepoServicerHarness"
+    ],
+    "rule_sanity": "basic",
+    "packages": [
+        "@chainlink=node_modules/@chainlink",
+        "@openzeppelin=node_modules/@openzeppelin"
+    ],
+    "verify": "TermRepoServicerHarness:certora/specs/termRepoServicer/rulesRedemptionsReverts.spec"
+}
diff --git a/certora/confs/termRepoServicer-repaymentsRedemptions.conf b/certora/confs/termRepoServicer-repaymentsRedemptions.conf
@@ -20,12 +20,12 @@
 		"-smt_initialSplitDepth 5",
 		"-depth 15",
 		"-mediumTimeout 20",
-		"-newSplitParallel true",
+		"-splitParallel true",
 		"-splitParallelTimelimit 7200",
 		"-splitParallelInitialDepth 5"
 	],
     "solc_optimize": "50",
-    "contract_compiler_skip_severe_warning_as_error": true,
+    "ignore_solidity_warnings": true,
     "loop_iter": "2",
     "optimistic_loop": true,
     "smt_timeout": "7200",
@@ -37,6 +37,5 @@
         "@chainlink=node_modules/@chainlink",
         "@openzeppelin=node_modules/@openzeppelin"
     ],
-    "prover_version": "jtoman/finder-fixes-will-it-ever-end",
     "verify": "TermRepoServicerHarness:certora/specs/termRepoServicer/rulesRepaymentsRedemptions.spec"
 }
diff --git a/...ervicer-repaymentsRedemptionsReverts.conf → ...s/termRepoServicer-repaymentsReverts.conf b/...ervicer-repaymentsRedemptionsReverts.conf → ...s/termRepoServicer-repaymentsReverts.conf
@@ -25,7 +25,7 @@
 		"-splitParallelInitialDepth 5"
 	],
     "solc_optimize": "50",
-    "contract_compiler_skip_severe_warning_as_error": true,
+    "ignore_solidity_warnings": true,
     "loop_iter": "2",
     "optimistic_loop": true,
     "smt_timeout": "7200",
@@ -37,6 +37,5 @@
         "@chainlink=node_modules/@chainlink",
         "@openzeppelin=node_modules/@openzeppelin"
     ],
-    "prover_version": "jtoman/finder-fixes-will-it-ever-end",
-    "verify": "TermRepoServicerHarness:certora/specs/termRepoServicer/rulesRepaymentsRedemptionsReverts.spec"
+    "verify": "TermRepoServicerHarness:certora/specs/termRepoServicer/rulesRepaymentsReverts.spec"
 }
diff --git a/certora/confs/termRepoServicer-rolloverReverts.conf b/certora/confs/termRepoServicer-rolloverReverts.conf
@@ -0,0 +1,42 @@
+{
+    "files": [
+        "certora/harness/TermRepoServicerHarness.sol",
+        "contracts/TermAuctionBidLocker.sol",
+        "contracts/TermController.sol",
+        "contracts/TermRepoLocker.sol",
+        "contracts/TermRepoToken.sol",
+        "contracts/TermRepoRolloverManager.sol",
+        "certora/harness/TermRepoCollateralManagerHarness.sol",
+        "certora/helpers/DummyERC20A.sol"
+    ],
+    "link": [
+        "TermRepoServicerHarness:termRepoToken=TermRepoToken",
+        "TermRepoServicerHarness:termRepoLocker=TermRepoLocker",
+        "TermRepoServicerHarness:termRepoCollateralManager=TermRepoCollateralManagerHarness",
+        "TermRepoServicerHarness:termController=TermController",
+        "TermRepoServicerHarness:termRepoRolloverManager=TermRepoRolloverManager",
+        "TermRepoCollateralManagerHarness:termRepoLocker=TermRepoLocker"
+    ],
+    "prover_args": [
+		"-smt_initialSplitDepth 10",
+		"-depth 20",
+		"-mediumTimeout 2",
+		"-splitParallel true",
+		"-splitParallelTimelimit 7200",
+		"-splitParallelInitialDepth 10"
+	],
+    "solc_optimize": "50",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "ignore_solidity_warnings": true,
+    "smt_timeout": "7200",
+    "parametric_contracts": [
+        "TermRepoServicerHarness"
+    ],
+    "rule_sanity": "basic",
+    "packages": [
+        "@chainlink=node_modules/@chainlink",
+        "@openzeppelin=node_modules/@openzeppelin"
+    ],
+    "verify": "TermRepoServicerHarness:certora/specs/termRepoServicer/rulesRolloverReverts.spec"
+}
diff --git a/certora/confs/termRepoServicer-stateVariables.conf b/certora/confs/termRepoServicer-stateVariables.conf
@@ -20,12 +20,12 @@
 		"-smt_initialSplitDepth 10",
 		"-depth 20",
 		"-mediumTimeout 2",
-		"-newSplitParallel true",
+		"-splitParallel true",
 		"-splitParallelTimelimit 7200",
 		"-splitParallelInitialDepth 10"
 	],
     "solc_optimize": "50",
-    "contract_compiler_skip_severe_warning_as_error": true,
+    "ignore_solidity_warnings": true,
     "loop_iter": "2",
     "optimistic_loop": true,
     "smt_timeout": "7200",