Certora CVL2 port (#111)

* CVL2 port * fixing specs for port * remove art v assets compare * revert assetsAfter spec * change tranfer to exit * re-add require that was previously deleted * remove unused line * Fix requires and missing asserts (#113) * Remove not necessary constraints (#114) * re-add struct link --------- Co-authored-by: Shelly Grossman <shelly@certora.com> Co-authored-by: sunbreak1211 <129470872+sunbreak1211@users.noreply.github.com>
makerdao · May 12, 2023 · ebcd47d · ebcd47d
1 parent de840a1
commit ebcd47d
Show file tree

Hide file tree

Showing 3 changed files with 629 additions and 716 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -48,7 +48,7 @@ jobs:
         run: solc-select install 0.8.14
 
       - name: Install Certora
-        run: pip3 install certora-cli
+        run: pip3 install certora-cli-beta
 
       - name: Certora ${{ matrix.name }}
         run: make certora-hub short=1 rule="${{ matrix.rules }}"

diff --git a/Makefile b/Makefile
@@ -1,5 +1,5 @@
 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 --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 --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,)
 deploy      :; ./deploy.sh config="$(config)"
 deploy-core :; ./deploy-core.sh