Merge pull request #118 from QGarchery/certora/update-certora-ci

Update CI to CVL version 7

.github/workflows/certora.yml

@@ -26,11 +26,11 @@ jobs:
     steps:
       - name: Checkout
         uses: actions/checkout@v3
-      
+
       - uses: actions/setup-java@v3
         with:
-          distribution: 'zulu'
-          java-version: '11'
+          distribution: "zulu"
+          java-version: "11"
           java-package: jre
 
       - name: Set up Python 3.8
@@ -48,7 +48,7 @@ jobs:
         run: solc-select install 0.8.14
 
       - name: Install Certora
-        run: pip3 install certora-cli-beta
+        run: pip3 install certora-cli
 
       - name: Certora ${{ matrix.name }}
         run: make certora-hub short=1 rule="${{ matrix.rules }}"

Makefile

@@ -1,5 +1,15 @@
 all         :; FOUNDRY_OPTIMIZER=true FOUNDRY_OPTIMIZER_RUNS=200 forge build --use solc:0.8.14
 clean       :; forge clean
-certora-hub :; PATH=~/.solc-select/artifacts/solc-0.8.14:~/.solc-select/artifacts/solc-0.5.12:~/.solc-select/artifacts:${PATH} certoraRun --solc_map D3MHub=solc-0.8.14,Vat=solc-0.5.12,DaiJoin=solc-0.5.12,Dai=solc-0.5.12,End=solc-0.5.12,D3MTestPlan=solc-0.8.14,D3MTestPool=solc-0.8.14,TokenMock=solc-0.8.14 --optimize_map D3MHub=200,Vat=0,DaiJoin=0,Dai=0,End=0,D3MTestPlan=200,D3MTestPool=200,TokenMock=200 --rule_sanity basic src/D3MHub.sol certora/dss/Vat.sol certora/dss/DaiJoin.sol certora/dss/Dai.sol certora/dss/End.sol certora/d3m/D3MTestPlan.sol certora/d3m/D3MTestPool.sol src/tests/mocks/TokenMock.sol --link D3MHub:vat=Vat D3MHub:daiJoin=DaiJoin D3MHub:end=End DaiJoin:vat=Vat DaiJoin:dai=Dai End:vat=Vat D3MTestPlan:dai=Dai D3MTestPool:hub=D3MHub D3MTestPool:vat=Vat D3MTestPool:dai=Dai D3MTestPool:share=TokenMock --structLink D3MHub:pool=D3MTestPool D3MHub:plan=D3MTestPlan --verify D3MHub:certora/D3MHub.spec --settings -mediumTimeout=1200,-solver=z3,-adaptiveSolverConfig=false,-smt_nonLinearArithmetic=true$(if $(short), --short_output,)$(if $(rule), --rule $(rule),)$(if $(multi), --multi_assert_check,)
+certora-hub :; PATH=~/.solc-select/artifacts/solc-0.8.14:~/.solc-select/artifacts/solc-0.5.12:~/.solc-select/artifacts:${PATH} \
+	certoraRun \
+	src/D3MHub.sol certora/dss/Vat.sol certora/dss/DaiJoin.sol certora/dss/Dai.sol certora/dss/End.sol certora/d3m/D3MTestPlan.sol certora/d3m/D3MTestPool.sol src/tests/mocks/TokenMock.sol \
+	--verify D3MHub:certora/D3MHub.spec \
+	--solc_map D3MHub=solc-0.8.14,Vat=solc-0.5.12,DaiJoin=solc-0.5.12,Dai=solc-0.5.12,End=solc-0.5.12,D3MTestPlan=solc-0.8.14,D3MTestPool=solc-0.8.14,TokenMock=solc-0.8.14 \
+	--solc_optimize_map D3MHub=200,Vat=0,DaiJoin=0,Dai=0,End=0,D3MTestPlan=200,D3MTestPool=200,TokenMock=200 \
+	--rule_sanity basic \
+	--link D3MHub:vat=Vat D3MHub:daiJoin=DaiJoin D3MHub:end=End DaiJoin:vat=Vat DaiJoin:dai=Dai End:vat=Vat D3MTestPlan:dai=Dai D3MTestPool:hub=D3MHub D3MTestPool:vat=Vat D3MTestPool:dai=Dai D3MTestPool:share=TokenMock \
+	--struct_link D3MHub:pool=D3MTestPool D3MHub:plan=D3MTestPlan \
+	--prover_args '-mediumTimeout 1200' '-solver z3' '-adaptiveSolverConfig false' '-smt_nonLinearArithmetic true' \
+	$(if $(short), --short_output,)$(if $(rule), --rule $(rule),)$(if $(multi), --multi_assert_check,)
 deploy      :; ./deploy.sh config="$(config)"
 deploy-core :; ./deploy-core.sh

README.md

@@ -1,4 +1,5 @@
 # Direct Deposit Module for Maker
+
 ![Build Status](https://github.com/makerdao/dss-direct-deposit/actions/workflows/.github/workflows/tests.yaml/badge.svg?branch=master)
 
 The Dai Direct Deposit Module (D3M) is a tool for directly injecting DAI into third party protocols.
@@ -11,7 +12,7 @@ The D3M is made of 3 components on the Maker side:
 
 ### D3MHub
 
-The primary manager contract responsible for collecting all information and determining which action to take (if any). Each D3M instance is regsitered on the Hub using relevant `file(ilk, ...)` admin functions.
+The primary manager contract responsible for collecting all information and determining which action to take (if any). Each D3M instance is registered on the Hub using relevant `file(ilk, ...)` admin functions.
 
 A permissionless `exec(ilk)` function exists which will perform all necessary steps to update the provided liquidity within the debt ceiling and external protocol constraints. `exec(ilk)` will need to be called on a somewhat regular basis to keep the system running properly. During each call to this function, interest will automatically be collected.
 
@@ -51,7 +52,7 @@ Below is a configurable parameter for the Compound DAI D3M:
 
 Any Comp that is accured can be permissionlessly collected into the pause proxy by calling `collect()`.
 
-### Setup and Testing
+# Setup and Testing
 
 To set up the environment and run tests, run the following commands: