D3M version 2.0

.github/workflows/certora.yml

@@ -0,0 +1,56 @@
+name: Certora
+
+on: [push]
+
+jobs:
+  certora:
+    name: Certora
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+          - name: Hub admin & getters
+            rules: rely rely_revert deny deny_revert file_ilk_uint256 file_ilk_uint256_revert file_ilk_address file_ilk_address_revert ilk_getters
+          - name: Hub exit, cage, cull, uncull and their reverts
+            rules: exit exit_revert cage cage_revert cull cull_revert uncull uncull_revert
+          - name: Hub exec non revert
+            rules: exec_normal exec_ilk_culled exec_vat_caged
+          - name: Hub exec normal revert
+            rules: exec_normal_revert
+          - name: Hub exec ilk culled and vat caged revert
+            rules: exec_ilk_culled_revert exec_vat_caged_revert
+          - name: Hub double exec
+            rules: exec_exec
+
+    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.5.12
+        run: solc-select install 0.5.12
+
+      - name: Solc Select 0.8.14
+        run: solc-select install 0.8.14
+
+      - name: Install Certora
+        run: pip3 install certora-cli-alpha-master==20220824.13.29
+
+      - name: Certora ${{ matrix.name }}
+        run: make certora-hub short=1 rule="${{ matrix.rules }}"
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}

.github/workflows/tests.yaml

@@ -1,25 +1,20 @@
-on: [push, pull_request]
+on: [push]
 
 jobs:
   tests:
     runs-on: ubuntu-latest
     steps:
-    - name: Checkout repository and submodules
-      uses: actions/checkout@v2
-      with:
-        submodules: recursive
+      - uses: actions/checkout@v3
 
-    - name: Install nix 2.3.6
-      uses: cachix/install-nix-action@v13
-      with:
-        install_url: https://releases.nixos.org/nix/nix-2.3.6/install
-        nix_path: nixpkgs=channel:nixos-unstable
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          version: nightly
 
-    - name: Use maker and dapp cachix
-      uses: cachix/cachix-action@v10
-      with:
-        name: maker
-        extraPullNames: dapp
+      - name: Install Dependencies
+        run: forge install
 
-    - name: Run tests
-      run: nix-shell --pure --argstr url ${{ secrets.ETH_RPC_URL }} --run 'dapp test -v --rpc'
+      - name: Run tests
+        run: make test
+        env:
+          ETH_RPC_URL: ${{ secrets.ETH_RPC_URL }}

.gitignore

@@ -1,2 +1,11 @@
 /out
 /cache
+resource_errors.json
+
+# certora
+*autoFinder_*
+.*certora*
+.last_confs/
+*.zip
+.zip-output-url.txt
+certora_debug_log.txt

.gitmodules

@@ -1,6 +1,3 @@
-[submodule "lib/ds-test"]
-	path = lib/ds-test
-	url = https://github.com/dapphub/ds-test
-[submodule "lib/ds-value"]
-	path = lib/ds-value
-	url = https://github.com/dapphub/ds-value
+[submodule "lib/dss-test"]
+	path = lib/dss-test
+	url = https://github.com/makerdao/dss-test

Makefile

@@ -1,6 +1,5 @@
-all    		 :; DAPP_BUILD_OPTIMIZE=1 DAPP_BUILD_OPTIMIZE_RUNS=200 dapp --use solc:0.6.12 build
-clean  		 :; dapp clean
-test   		 :; ./test.sh match=$(match) optimizer=1
-test-dev   	 :; ./test.sh match=$(match) optimizer=0
-test-forge 	 :; ./test-forge.sh match=$(match) block=$(block)
-deploy 		 :; make && dapp create DssDirectDepositAaveDai 0xdA0Ab1e0017DEbCd72Be8599041a2aa3bA7e740F 0x4449524543542d4141564556322d444149000000000000000000000000000000 0x7d2768dE32b0b80b7a3454c06BdAc94A69DDc7A9 0xd784927Ff2f95ba542BfC824c8a8a98F3495f6b5
+all         :; DAPP_BUILD_OPTIMIZE=1 DAPP_BUILD_OPTIMIZE_RUNS=200 dapp --use solc:0.8.14 build
+clean       :; dapp clean
+test        :; ./test.sh solc="0.8.14" match="$(match)" block="$(block)" match-test="$(match-test)" match-contract="$(match-contract)"
+test-forge  :; make test
+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,D3MTestGem=solc-0.8.14 --optimize_map D3MHub=200,Vat=0,DaiJoin=0,Dai=0,End=0,D3MTestPlan=200,D3MTestPool=200,D3MTestGem=200 --rule_sanity basic src/D3MHub.sol certora/dss/Vat.sol certora/dss/DaiJoin.sol certora/dss/Dai.sol certora/dss/End.sol src/tests/stubs/D3MTestPlan.sol src/tests/stubs/D3MTestPool.sol src/tests/stubs/D3MTestGem.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=D3MTestGem --verify D3MHub:certora/D3MHub.spec --settings -mediumTimeout=180 --staging$(if $(short), --short_output,)$(if $(rule), --rule $(rule),)$(if $(multi), --multi_assert_check,)

README.md

@@ -1,19 +1,52 @@
 # 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 Direct Deposit Module interfaces with third party lending protocols to enable a maximum variable borrow rate for selected assets. Maker Governance is able to pick a target variable borrow rate, and the module will automatically deposit/remove liquidity to ensure that target rate is hit.
+The Dai Direct Deposit Module (D3M) is a tool for directly injecting DAI into third party protocols.
 
-## DssDirectDepositAaveDai
+![D3M](https://ipfs.io/ipfs/QmfAPBsAQbPoAiMB7vypuBwC41X5yrzYKNMUia4nGyoN23)
 
-### Configuration
+As seen in the image above, external protocols are viewed under the simplified ERC-4626-like interface. Pool adapters are used to convert protocol complexity into simplified concepts of Excess Capacity + DAI liquidity + DAI outstanding. How DAI is converted between these states is completely protocol-specific and mostly irrelevant to the D3M.
+
+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.
+
+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.
+
+### D3MPool
+
+A "dumb" adapter which is responsible for depositing or withdrawing DAI from the target protocol based on instructions from the Hub. Also contains functions which provide information such as `maxDeposit()` and `maxWithdraw()`. These inform the hub the maximum room to deposit or withdraw respectively. Abstractly we view this `maxWithdraw()` value as the available DAI liquidity that can be immediately withdrawn. Different protocols have different mechanisms for making DAI liquidity available. For example, some protocols raise interest rates to encourage more 3rd party deposits (or repays from borrowers). In the other cases, there could be a function such as `intendToWithdraw()` which signals to the pool operator that they should begin liquidating some positions to free up DAI.
+
+### D3MPlan
+
+The D3MPlan can be viewed as the targeting logic for D3M instances. The plan is responsible for reading all relevant information from its state (i.e. the target rate) and possibly from the external protocol (i.e. current balance of supply and borrowing in the market) and condensing this down to a debt target. This desired target debt is forwarded to the Hub to take action to reach this target debt level asap.
+
+### General Configuration
 
-Below are the configurable parameters for the Aave DAI D3M:
+The below parameter exists for each D3M implementation:
 
 - `tau` [seconds] - The expiry for when bad debt is sent to the vow debt queue. This must be set during initialization to enforce a deadline for when this module is considered to be in a failure mode where no more liquidity is available in the pool to unwind. Unwinding can still occur after this period elapses.
+
+# Specific Implementations
+
+## Aave D3M
+
+### Configuration
+
+Below is a configurable parameter for the Aave DAI D3M:
+
 - `bar` [ray] - The target borrow rate on Aave for the DAI market. This module will aim to enforce that borrow limit.
 
-### Operation
+Any stkAave that is accured can be permissionlessly collected into the pause proxy by calling `collect()`.
+
+## Compound D3M
+
+### Configuration
+
+Below is a configurable parameter for the Compound DAI D3M:
 
-A permissionless `exec()` function exists which will perform all necessary steps to enforce the maximum borrow rate to within the available liquidity and debt ceiling constraints. `exec()` will need to be called on a somewhat regular basis to keep the system running properly. Upon unwinding interest will automatically be collected, but you can also permissionlessly call `reap()` to pull in all collected interest as well.
+- `barb` [wad] - The target borrow rate per block on Compound for the DAI market. This module will aim to enforce that borrow limit.
 
-Any stkAave that is accured can be permissionlessly collected into the pause proxy by calling `collect(address[], uint256)`.
+Any Comp that is accured can be permissionlessly collected into the pause proxy by calling `collect()`.