From da5ae45367c60e9f365fddc7eea2a2a1b5506120 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 18 Mar 2024 10:26:44 +0100 Subject: [PATCH 1/7] chore: update CI to CVL version 7 --- .github/workflows/certora.yml | 8 ++++---- Makefile | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 780ce205..570ca44b 100644 --- a/.github/workflows/certora.yml +++ b/.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 }}" diff --git a/Makefile b/Makefile index 532060d4..8952b68a 100644 --- 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 --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 --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 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 --struct_link D3MHub:pool=D3MTestPool D3MHub:plan=D3MTestPlan --verify D3MHub:certora/D3MHub.spec --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 From d8a85f85f1ae506e07166ce9c0b996ea2bc6ee6f Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 18 Mar 2024 10:47:27 +0100 Subject: [PATCH 2/7] fix: separate multiple prover args --- Makefile | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 8952b68a..65ee5d92 100644 --- a/Makefile +++ b/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 --solc_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 --struct_link D3MHub:pool=D3MTestPool D3MHub:plan=D3MTestPlan --verify D3MHub:certora/D3MHub.spec --prover_args '-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 From efa9fd335d5007136c08789d97ba247fd9dd30fa Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 18 Mar 2024 13:30:03 +0100 Subject: [PATCH 3/7] docs: small changes to the README --- README.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index c480ccd1..41a73800 100644 --- a/README.md +++ b/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: From 7f9752ac808a88989ec79e9574905baa513035cb Mon Sep 17 00:00:00 2001 From: Sam MacPherson Date: Mon, 18 Mar 2024 12:46:33 -0400 Subject: [PATCH 4/7] revert certora changes --- .github/workflows/certora.yml | 2 +- Makefile | 12 +----------- 2 files changed, 2 insertions(+), 12 deletions(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 570ca44b..1496d196 100644 --- 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 index 65ee5d92..532060d4 100644 --- a/Makefile +++ b/Makefile @@ -1,15 +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 \ - 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,) +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 From 574965d210e45762334c9c56bc1fa2793d548f81 Mon Sep 17 00:00:00 2001 From: Sam MacPherson Date: Tue, 19 Mar 2024 09:12:40 -0400 Subject: [PATCH 5/7] remove increase in error threshold --- src/tests/integration/MetaMorpho.t.sol | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/tests/integration/MetaMorpho.t.sol b/src/tests/integration/MetaMorpho.t.sol index 0f231c20..34ab4896 100644 --- a/src/tests/integration/MetaMorpho.t.sol +++ b/src/tests/integration/MetaMorpho.t.sol @@ -71,9 +71,6 @@ contract MetaMorphoTest is IntegrationBaseTest { vm.createSelectFork(vm.envString("ETH_RPC_URL"), 19456934); - // Need to increase to 3 - roundingTolerance = 3; - // Deploy. d3m.oracle = D3MDeploy.deployOracle(address(this), admin, ilk, address(dss.vat)); d3m.pool = D3MDeploy.deploy4626TypePool(address(this), admin, ilk, address(hub), address(dai), address(spDai)); From 6b827d0cd725847c3137d22b41c6055b269865b6 Mon Sep 17 00:00:00 2001 From: Sam MacPherson Date: Tue, 19 Mar 2024 09:32:07 -0400 Subject: [PATCH 6/7] enable the asserts again with the rounding taken into account --- src/tests/integration/IntegrationBase.t.sol | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/tests/integration/IntegrationBase.t.sol b/src/tests/integration/IntegrationBase.t.sol index 115100f5..f4da6d40 100644 --- a/src/tests/integration/IntegrationBase.t.sol +++ b/src/tests/integration/IntegrationBase.t.sol @@ -388,7 +388,8 @@ abstract contract IntegrationBaseTest is DssTest { vow.heal(_min(vat.sin(address(vow)), vat.dai(address(vow)))); assertRoundingEq(vat.gem(ilk, address(end)), 0); assertEq(vat.sin(address(vow)), 0); - //assertGe(vat.dai(address(vow)), prevDai); // As also probably accrues interest + // Adding 1e27 for rounding error earlier on + assertGe(vat.dai(address(vow)) + 1e27, prevDai); // As also probably accrues interest } function test_unwind_mcd_caged_skimmed() public { @@ -458,7 +459,8 @@ abstract contract IntegrationBaseTest is DssTest { vow.heal(_min(vat.sin(address(vow)), vat.dai(address(vow)))); assertRoundingEq(vat.gem(ilk, address(end)), 0); assertEq(vat.sin(address(vow)), 0); - //assertGe(vat.dai(address(vow)), prevDai); // As also probably accrues interest + // Adding 1e27 for rounding error earlier on + assertGe(vat.dai(address(vow)) + 1e27, prevDai); // As also probably accrues interest } function test_unwind_mcd_caged_wait_done() public { From bcd532c462b100d036e20e6695dbdaec787a5086 Mon Sep 17 00:00:00 2001 From: Sam MacPherson Date: Tue, 19 Mar 2024 09:52:47 -0400 Subject: [PATCH 7/7] use approx eq instead and remove comments --- src/tests/integration/IntegrationBase.t.sol | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/tests/integration/IntegrationBase.t.sol b/src/tests/integration/IntegrationBase.t.sol index f4da6d40..eddeb423 100644 --- a/src/tests/integration/IntegrationBase.t.sol +++ b/src/tests/integration/IntegrationBase.t.sol @@ -388,8 +388,7 @@ abstract contract IntegrationBaseTest is DssTest { vow.heal(_min(vat.sin(address(vow)), vat.dai(address(vow)))); assertRoundingEq(vat.gem(ilk, address(end)), 0); assertEq(vat.sin(address(vow)), 0); - // Adding 1e27 for rounding error earlier on - assertGe(vat.dai(address(vow)) + 1e27, prevDai); // As also probably accrues interest + assertApproxEqAbs(vat.dai(address(vow)), prevDai, 1e27); } function test_unwind_mcd_caged_skimmed() public { @@ -459,8 +458,7 @@ abstract contract IntegrationBaseTest is DssTest { vow.heal(_min(vat.sin(address(vow)), vat.dai(address(vow)))); assertRoundingEq(vat.gem(ilk, address(end)), 0); assertEq(vat.sin(address(vow)), 0); - // Adding 1e27 for rounding error earlier on - assertGe(vat.dai(address(vow)) + 1e27, prevDai); // As also probably accrues interest + assertApproxEqAbs(vat.dai(address(vow)), prevDai, 1e27); } function test_unwind_mcd_caged_wait_done() public {