Contracts + Certora specs

.github/workflows/certora.yml

@@ -0,0 +1,46 @@
+name: Certora
+
+on: [push, pull_request]
+
+jobs:
+  certora:
+    name: Certora
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        usds:
+          - usds
+          - usds-join
+          - dai-usds
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - 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.8.21
+        run: solc-select install 0.8.21
+
+      - name: Install Certora
+        run: pip3 install certora-cli-beta
+
+      - name: Verify ${{ matrix.usds }}
+        run: make certora-${{ matrix.usds }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}

.github/workflows/tests.yaml

@@ -0,0 +1,20 @@
+on: [push, pull_request]
+
+jobs:
+  tests:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository and submodules
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          version: nightly
+
+      - name: Run tests
+        run: forge test
+        env:
+          ETH_RPC_URL: ${{ secrets.ETH_RPC_URL }}

.gitignore

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

.gitmodules

@@ -1,3 +1,9 @@
-[submodule "lib/dss-test"]
-	path = lib/dss-test
-	url = https://github.com/makerdao/dss-test.git
+[submodule "lib/token-tests"]
+	path = lib/token-tests
+	url = https://github.com/makerdao/token-tests
+[submodule "lib/openzeppelin-contracts-upgradeable"]
+	path = lib/openzeppelin-contracts-upgradeable
+	url = https://github.com/OpenZeppelin/openzeppelin-contracts-upgradeable
+[submodule "lib/openzeppelin-foundry-upgrades"]
+	path = lib/openzeppelin-foundry-upgrades
+	url = https://github.com/OpenZeppelin/openzeppelin-foundry-upgrades

Makefile

@@ -1,3 +1,4 @@
-all         :; forge build --use solc:0.8.16
-clean       :; forge clean
-test        :; forge test -vvv --use solc:0.8.16
+PATH := ~/.solc-select/artifacts/solc-0.8.21:~/.solc-select/artifacts:$(PATH)
+certora-usds      :; PATH=${PATH} certoraRun certora/Usds.conf$(if $(rule), --rule $(rule),)
+certora-usds-join :; PATH=${PATH} certoraRun certora/UsdsJoin.conf$(if $(rule), --rule $(rule),)
+certora-dai-usds  :; PATH=${PATH} certoraRun certora/DaiUsds.conf$(if $(rule), --rule $(rule),)

README.md

@@ -0,0 +1,30 @@
+# USDS Token and contracts associated
+
+This repository includes 3 smart contracts:
+
+- USDS token
+- UsdsJoin
+- DaiUsds Converter
+
+### USDS token
+
+This is a standard erc20 implementation with regular `permit` functionality + EIP-1271 smart contract signature validation.
+
+The token uses the ERC-1822 UUPS pattern for upgradeability and the ERC-1967 proxy storage slots standard.
+It is important that the `UsdsDeploy` library sequence be used for deploying the token.
+
+#### OZ upgradeability validations
+
+The OZ validations can be run alongside the existing tests:  
+`VALIDATE=true forge test --ffi --build-info --extra-output storageLayout`
+
+### UsdsJoin
+
+This is the contract in charge of `mint`ing the erc20 IOUs in exchange of native `vat.dai` balance. It also manages the reverse operation, `burn`ing tokens and releasing `vat.dai`.
+A noticeable code difference against `DaiJoin` is this contract doesn't have any permissions system at all.
+However, in practice, `UsdsJoin` acts the exact same way as the production `DaiJoin` implementation. This is because there isn't any `wards(address)` set there.
+
+### DaiUsds
+
+It is a permissionless converter between `Dai` and `Usds` (both ways). Using the `public` functions of `UsdsJoin` and `DaiJoin` moves from one token to the other. The exchange rate is 1:1.
+It is just a "convenience" contract, users could still get the same outcome executing the separate methods in the `join`s or use any other converter implementation.

certora/Auxiliar.sol

@@ -0,0 +1,61 @@
+pragma solidity 0.8.21;
+
+interface IERC1271 {
+    function isValidSignature(
+        bytes32,
+        bytes memory
+    ) external view returns (bytes4);
+}
+
+contract Auxiliar {    
+    function computeDigestForToken(
+        bytes32 domain_separator,
+        bytes32 permit_typehash,
+        address owner,
+        address spender,
+        uint256 value,
+        uint256 nonce,
+        uint256 deadline
+    ) public pure returns (bytes32 digest){
+        digest =
+        keccak256(abi.encodePacked(
+            "\x19\x01",
+            domain_separator,
+            keccak256(abi.encode(
+                permit_typehash,
+                owner,
+                spender,
+                value,
+                nonce,
+                deadline
+            ))
+        ));
+    }
+
+    function call_ecrecover(
+        bytes32 digest,
+        uint8 v,
+        bytes32 r,
+        bytes32 s
+    ) public pure returns (address signer) {
+        signer = ecrecover(digest, v, r, s);
+    }
+
+    function signatureToVRS(bytes memory signature) public returns (uint8 v, bytes32 r, bytes32 s) {
+        if (signature.length == 65) {
+            assembly {
+                r := mload(add(signature, 0x20))
+                s := mload(add(signature, 0x40))
+                v := byte(0, mload(add(signature, 0x60)))
+            }
+        }
+    }
+
+    function VRSToSignature(uint8 v, bytes32 r, bytes32 s) public returns (bytes memory signature) {
+        signature = abi.encodePacked(r, s, v);
+    }
+
+    function size(bytes memory data) public returns (uint256 size_) {
+        size_ = data.length;
+    }
+}

certora/DaiJoinMock.sol

@@ -0,0 +1,7 @@
+pragma solidity ^0.8.21;
+
+import "../src/UsdsJoin.sol";
+
+contract DaiJoinMock is UsdsJoin {
+    constructor(address vat_, address dai_) UsdsJoin(vat_, dai_) {}
+}

certora/DaiMock.sol

@@ -0,0 +1,7 @@
+pragma solidity ^0.8.21;
+
+import "../src/Usds.sol";
+
+contract DaiMock is Usds {
+
+}

certora/DaiUsds.conf

@@ -0,0 +1,37 @@
+{
+    "files": [
+        "src/DaiUsds.sol",
+        "src/UsdsJoin.sol",
+        "src/Usds.sol",
+        "certora/DaiJoinMock.sol",
+        "certora/DaiMock.sol",
+        "certora/VatMock.sol",
+    ],
+    "link": [
+        "DaiUsds:usdsJoin=UsdsJoin",
+        "DaiUsds:usds=Usds",
+        "DaiUsds:daiJoin=DaiJoinMock",
+        "DaiUsds:dai=DaiMock",
+        "UsdsJoin:usds=Usds",
+        "UsdsJoin:vat=VatMock",
+        "DaiJoinMock:usds=DaiMock",
+        "DaiJoinMock:vat=VatMock"
+    ],
+    "rule_sanity": "basic",
+    "solc": "solc-0.8.21",
+    "solc_optimize_map": {
+        "DaiUsds": "200",
+        "UsdsJoin": "200",
+        "Usds": "200",
+        "DaiJoinMock": "0",
+        "DaiMock": "0",
+        "VatMock": "0"
+    },
+    "verify": "DaiUsds:certora/DaiUsds.spec",
+    "prover_args": [
+        "-mediumTimeout 180"
+    ],
+    "optimistic_loop": true,
+    "multi_assert_check": true,
+    "wait_for_results": "all"
+}