Refactor: make DssVestSuckable.join a constructor parameter

.github/workflows/certora.yml

@@ -32,6 +32,9 @@ jobs:
       - name: Install solc-select
         run: pip3 install solc-select
 
+      - name: Solc Select 0.5.12
+        run: solc-select install 0.5.12
+
       - name: Solc Select 0.6.12
         run: solc-select install 0.6.12
 

Makefile

@@ -1,13 +1,14 @@
+PATH := ~/.solc-select/artifacts/solc-0.6.12:~/.solc-select/artifacts/solc-0.5.12:~/.solc-select/artifacts:$(PATH)
 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                  :; ./test.sh match="$(match)" block="$(block)" match-test="$(match-test)" match-contract="$(match-contract)"
-solc-select           :; pip3 install solc-select && solc-select install 0.6.12
+solc-select           :; pip3 install solc-select && solc-select install 0.5.12 && 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-mintable      :; $(if $(CERTORAKEY),, @echo "set certora key"; exit 1;) certoraRun --solc ~/.solc-select/artifacts/solc-0.6.12/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      :; $(if $(CERTORAKEY),, @echo "set certora key"; exit 1;) certoraRun --solc ~/.solc-select/artifacts/solc-0.6.12/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 :; $(if $(CERTORAKEY),, @echo "set certora key"; exit 1;) certoraRun --solc ~/.solc-select/artifacts/solc-0.6.12/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
+certora-mintable      :; PATH=${PATH} certoraRun certora/DssVestMintable.conf $(if $(rule), --rule $(rule),)
+certora-suckable      :; PATH=${PATH} certoraRun certora/DssVestSuckable.conf $(if $(rule), --rule $(rule),)
+certora-transferrable :; PATH=${PATH} certoraRun certora/DssVestTransferrable.conf $(if $(rule), --rule $(rule),)
 deploy-mintable       :; make && dapp create DssVestMintable $(gem)
 deploy-suckable       :; make && dapp create DssVestSuckable 0xdA0Ab1e0017DEbCd72Be8599041a2aa3bA7e740F
 deploy-transferrable  :; make && dapp create DssVestTransferrable $(owner) $(gem)

README.md

@@ -32,7 +32,9 @@ After deployment, governance must set the `cap` value using the `file` function.
 
 #### DssVestSuckable
 
-Pass the MCD [chainlog](https://github.com/makerdao/dss-chain-log) address to the constructor to set up the contract for scheduled Dai `suck`s. Note: this contract must be given authority to `suck()` Dai from the `vat`'s surplus buffer.
+Pass the MCD [chainlog](https://github.com/makerdao/dss-chain-log) address to the constructor to set up the contract for scheduled Dai or USDS `suck`s. Note: this contract must be given authority to `suck()` Dai from the `vat`'s surplus buffer.
+
+To choose between Dai and USDS, supply the relevant join (`MCD_JOIN_DAI` or `USDS_JOIN`) as the `address _join` constructor parameter.
 
 A `vat.live` check is introduced to disable `vest()` in the event of Emergency Shutdown (aka Global Settlement).
 

certora/DssVestMintable.conf

@@ -0,0 +1,25 @@
+{
+  "verify": "DssVestMintable:certora/DssVestMintable.spec",
+  "parametric_contracts": [
+    "DssVestMintable"
+  ],
+  "files": [
+    "src/DssVest.sol:DssVestMintable",
+    "certora/harness/DSToken.sol",
+    "certora/harness/MockAuthority.sol"
+  ],
+  "solc": "solc-0.6.12",
+  "solc_optimize_map": {
+    "DssVestMintable": "200",
+    "DSToken": "0",
+    "MockAuthority": "0"
+  },
+  "link": [
+    "DssVestMintable:gem=DSToken",
+    "DSToken:authority=MockAuthority"
+  ],
+  "build_cache": true,
+  "rule_sanity": "basic",
+  "multi_assert_check": true,
+  "wait_for_results": "all"
+}