Certora CI (#49)

makerdao · Mar 25, 2022 · 50b7140 · 50b7140
1 parent 90188d2
commit 50b7140
Show file tree

Hide file tree

Showing 7 changed files with 96 additions and 15 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -0,0 +1,44 @@
+name: Certora
+
+on: [push, pull_request]
+
+jobs:
+  certora:
+    name: Certora
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        vest:
+          - mintable
+          - suckable
+          - transferrable
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+
+      - uses: actions/setup-java@v2
+        with:
+          distribution: 'zulu'
+          java-version: '11'
+          java-package: jre
+
+      - name: Set up Python 3.8
+        uses: actions/setup-python@v3
+        with:
+          python-version: 3.8
+
+      - name: Install solc-select
+        run: pip3 install solc-select
+
+      - name: Solc Select 0.6.12
+        run: solc-select install 0.6.12
+
+      - name: Install Certora
+        run: pip3 install certora-cli
+
+      - name: Verify ${{ matrix.vest }}
+        run: make certora-${{ matrix.vest }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
diff --git a/.gitignore b/.gitignore
@@ -7,4 +7,4 @@ corpus/
 # certora
 .*certora*
 .last_confs/
-*.zip
+resource_errors.json
diff --git a/Makefile b/Makefile
@@ -1,13 +1,13 @@
 all    :; DAPP_BUILD_OPTIMIZE=1 DAPP_BUILD_OPTIMIZE_RUNS=200 dapp --use solc:0.6.12 build
 clean  :; dapp clean && rm -rf crytic-export corpus
 test   :; make && ./test.sh $(match)
+solc-select           :; pip3 install solc-select && solc-select install 0.6.12
 echidna-mintable      :; ./echidna/echidna.sh mintable
 echidna-suckable      :; ./echidna/echidna.sh suckable
 echidna-transferrable :; ./echidna/echidna.sh transferrable
-certora-solc          :; pip3 install solc-select && solc-select install 0.6.12
-certora-mintable      :; certoraRun --solc ~/.solc-select/artifacts/solc-0.6.12 src/DssVest.sol:DssVestMintable certora/DSToken.sol certora/MockAuthority.sol --link DssVestMintable:gem=DSToken DSToken:authority=MockAuthority --verify DssVestMintable:certora/DssVestMintable.spec --rule_sanity --solc_args "['--optimize','--optimize-runs','200']"
-certora-suckable      :; certoraRun --solc ~/.solc-select/artifacts/solc-0.6.12 src/DssVest.sol:DssVestSuckable certora/ChainLog.sol certora/Vat.sol certora/DaiJoin.sol certora/Dai.sol --link DssVestSuckable:chainlog=ChainLog DssVestSuckable:vat=Vat DssVestSuckable:daiJoin=DaiJoin DaiJoin:vat=Vat DaiJoin:dai=Dai --verify DssVestSuckable:certora/DssVestSuckable.spec --rule_sanity --solc_args "['--optimize','--optimize-runs','200']"
-certora-transferrable :; certoraRun --solc ~/.solc-select/artifacts/solc-0.6.12 src/DssVest.sol:DssVestTransferrable certora/Dai.sol --link DssVestTransferrable:gem=Dai --verify DssVestTransferrable:certora/DssVestTransferrable.spec --rule_sanity --solc_args "['--optimize','--optimize-runs','200']"
+certora-mintable      :; certoraRun --solc ~/.solc-select/artifacts/solc-0.6.12 src/DssVest.sol:DssVestMintable certora/DSToken.sol certora/MockAuthority.sol --link DssVestMintable:gem=DSToken DSToken:authority=MockAuthority --verify DssVestMintable:certora/DssVestMintable.spec --solc_args "['--optimize','--optimize-runs','200']" --rule_sanity $(if $(rule),--rule $(rule),) --multi_assert_check --short_output
+certora-suckable      :; certoraRun --solc ~/.solc-select/artifacts/solc-0.6.12 src/DssVest.sol:DssVestSuckable certora/ChainLog.sol certora/Vat.sol certora/DaiJoin.sol certora/Dai.sol --link DssVestSuckable:chainlog=ChainLog DssVestSuckable:vat=Vat DssVestSuckable:daiJoin=DaiJoin DaiJoin:vat=Vat DaiJoin:dai=Dai --verify DssVestSuckable:certora/DssVestSuckable.spec --solc_args "['--optimize','--optimize-runs','200']" --rule_sanity  $(if $(rule),--rule $(rule),) --multi_assert_check --short_output
+certora-transferrable :; certoraRun --solc ~/.solc-select/artifacts/solc-0.6.12 src/DssVest.sol:DssVestTransferrable certora/Dai.sol --link DssVestTransferrable:gem=Dai --verify DssVestTransferrable:certora/DssVestTransferrable.spec --solc_args "['--optimize','--optimize-runs','200']" --rule_sanity  $(if $(rule),--rule $(rule),) --multi_assert_check --short_output
 deploy-mintable       :; make && dapp create DssVestMintable $(gem)
 deploy-suckable       :; make && dapp create DssVestSuckable 0xdA0Ab1e0017DEbCd72Be8599041a2aa3bA7e740F
 deploy-transferrable  :; make && dapp create DssVestTransferrable $(owner) $(gem)
diff --git a/README.md b/README.md
@@ -1,5 +1,6 @@
 [![Tests](https://github.com/makerdao/dss-vest/actions/workflows/tests.yml/badge.svg)](https://github.com/makerdao/dss-vest/actions/workflows/tests.yml)
 [![Echidna](https://github.com/makerdao/dss-vest/actions/workflows/echidna.yml/badge.svg)](https://github.com/makerdao/dss-vest/actions/workflows/echidna.yml)
+[![Certora](https://github.com/makerdao/dss-vest/actions/workflows/certora.yml/badge.svg)](https://github.com/makerdao/dss-vest/actions/workflows/certora.yml)
 
 # dss-vest
 
@@ -160,7 +161,7 @@ Allows governance to schedule a point in the future to end the vest. Used for pl
 
 - Install solc-select and install solc 0.6.12 artifacts:
   ```
-  make certora-solc
+  make solc-select
   ```
 
 ### Run Certora Specs

diff --git a/certora/DssVestMintable.spec b/certora/DssVestMintable.spec
@@ -41,12 +41,13 @@ hook Sload uint256 value locked STORAGE {
 }
 
 invariant everythingNotSetIfUsrNotSet(uint256 _id) usr(_id) == 0 => bgn(_id) == 0 && clf(_id) == 0 && fin(_id) == 0 && mgr(_id) == 0 && res(_id) == 0 && tot(_id) == 0 && rxd(_id) == 0
-
+filtered { f -> !f.isFallback }
 invariant usrCantBeZeroIfCreate(uint256 _id) _id > 0 && _id <= ids() => usr(_id) != 0
-
+filtered { f -> !f.isFallback }
 invariant clfGreaterOrEqualBgn(uint256 _id) clf(_id) >= bgn(_id)
-
+filtered { f -> !f.isFallback }
 invariant finGreaterOrEqualClf(uint256 _id) fin(_id) >= clf(_id)
+filtered { f -> !f.isFallback }
 
 // The following invariant is replaced with a rule as it was kind of difficult to be finished this way.
 // Leaving this commented for possible future option to be finished.
@@ -79,6 +80,17 @@ rule rxdLessOrEqualTot(method f) filtered { f -> !f.isFallback } {
     assert(rxd(_id) <= tot(_id));
 }
 
+// Verify fallback always reverts
+// Important as we are filtering it out from invariants and some rules
+rule fallback_revert(method f) filtered { f -> f.isFallback } {
+    env e;
+
+    calldataarg arg;
+    f@withrevert(e, arg);
+
+    assert(lastReverted, "Fallback did not revert");
+}
+
 // Verify that returned value is what expected in TWENTY_YEARS
 rule TWENTY_YEARS() {
     uint256 twenty = TWENTY_YEARS();

diff --git a/certora/DssVestSuckable.spec b/certora/DssVestSuckable.spec
@@ -51,12 +51,13 @@ hook Sload uint256 value locked STORAGE {
 }
 
 invariant everythingNotSetIfUsrNotSet(uint256 _id) usr(_id) == 0 => bgn(_id) == 0 && clf(_id) == 0 && fin(_id) == 0 && mgr(_id) == 0 && res(_id) == 0 && tot(_id) == 0 && rxd(_id) == 0
-
+filtered { f -> !f.isFallback }
 invariant usrCantBeZeroIfCreate(uint256 _id) _id > 0 && _id <= ids() => usr(_id) != 0
-
+filtered { f -> !f.isFallback }
 invariant clfGreaterOrEqualBgn(uint256 _id) clf(_id) >= bgn(_id)
-
+filtered { f -> !f.isFallback }
 invariant finGreaterOrEqualClf(uint256 _id) fin(_id) >= clf(_id)
+filtered { f -> !f.isFallback }
 
 // The following invariant is replaced with a rule as it was kind of difficult to be finished this way.
 // Leaving this commented for possible future option to be finished.
@@ -89,6 +90,17 @@ rule rxdLessOrEqualTot(method f) filtered { f -> !f.isFallback } {
     assert(rxd(_id) <= tot(_id));
 }
 
+// Verify fallback always reverts
+// Important as we are filtering it out from invariants and some rules
+rule fallback_revert(method f) filtered { f -> f.isFallback } {
+    env e;
+
+    calldataarg arg;
+    f@withrevert(e, arg);
+
+    assert(lastReverted, "Fallback did not revert");
+}
+
 // Verify that returned value is what expected in TWENTY_YEARS
 rule TWENTY_YEARS() {
     uint256 twenty = TWENTY_YEARS();

diff --git a/certora/DssVestTransferrable.spec b/certora/DssVestTransferrable.spec
@@ -39,12 +39,13 @@ hook Sload uint256 value locked STORAGE {
 }
 
 invariant everythingNotSetIfUsrNotSet(uint256 _id) usr(_id) == 0 => bgn(_id) == 0 && clf(_id) == 0 && fin(_id) == 0 && mgr(_id) == 0 && res(_id) == 0 && tot(_id) == 0 && rxd(_id) == 0
-
+filtered { f -> !f.isFallback }
 invariant usrCantBeZeroIfCreate(uint256 _id) _id > 0 && _id <= ids() => usr(_id) != 0
-
+filtered { f -> !f.isFallback }
 invariant clfGreaterOrEqualBgn(uint256 _id) clf(_id) >= bgn(_id)
-
+filtered { f -> !f.isFallback }
 invariant finGreaterOrEqualClf(uint256 _id) fin(_id) >= clf(_id)
+filtered { f -> !f.isFallback }
 
 // The following invariant is replaced with a rule as it was kind of difficult to be finished this way.
 // Leaving this commented for possible future option to be finished.
@@ -77,6 +78,17 @@ rule rxdLessOrEqualTot(method f) filtered { f -> !f.isFallback } {
     assert(rxd(_id) <= tot(_id));
 }
 
+// Verify fallback always reverts
+// Important as we are filtering it out from invariants and some rules
+rule fallback_revert(method f) filtered { f -> f.isFallback } {
+    env e;
+
+    calldataarg arg;
+    f@withrevert(e, arg);
+
+    assert(lastReverted, "Fallback did not revert");
+}
+
 // Verify that returned value is what expected in TWENTY_YEARS
 rule TWENTY_YEARS() {
     uint256 twenty = TWENTY_YEARS();