Contracts + Certora specs

.github/workflows/certora.yml

@@ -0,0 +1,43 @@
+name: Certora
+
+on: [push, pull_request]
+
+jobs:
+  certora:
+    name: Certora
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        sky:
+          - sky
+          - mkr-sky
+
+    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.8.21
+        run: solc-select install 0.8.21
+
+      - name: Install Certora
+        run: pip3 install certora-cli
+
+      - name: Verify ${{ matrix.sky }}
+        run: make certora-${{ matrix.sky }}
+        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 }}

.gitmodules

@@ -1,3 +1,3 @@
-[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

Makefile

@@ -1,3 +1,3 @@
-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-sky     :; PATH=${PATH} certoraRun certora/Sky.conf$(if $(rule), --rule $(rule),)
+certora-mkr-sky :; PATH=${PATH} certoraRun certora/MkrSky.conf$(if $(rule), --rule $(rule),)

README.md

@@ -0,0 +1,19 @@
+# SKY Token and contract associated
+
+This repository includes 2 smart contracts:
+
+- SKY token
+- MkrSky Converter
+
+### SKY token
+
+This is a standard erc20 implementation with regular `permit` functionality + EIP-1271 smart contract signature validation.
+In principle `PauseProxy` and `MkrSky` would be the only two contracts set as `wards(address)`.
+
+### MkrSky
+
+It is a converter between `Mkr` and `Sky` (both ways). Using the `mint` and `burn` capabilities of both tokens it is possible to exchange one to the other. The exchange rate is 1:`rate` (value defined as `immutable`).
+
+**Note:** if one of the tokens removes `mint` capabilities to this contract, it means that the path which gives that token to the user won't be available.
+
+**Note 2:** In the MKR -> SKY conversion, if the user passes a `wad` amount not multiple of `rate`, it causes that a dusty value will be lost.

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/MkrMock.sol

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

certora/MkrSky.conf

@@ -0,0 +1,25 @@
+{
+    "files": [
+        "src/MkrSky.sol",
+        "src/Sky.sol",
+        "certora/MkrMock.sol"
+    ],
+    "link": [
+        "MkrSky:sky=Sky",
+        "MkrSky:mkr=MkrMock"
+    ],
+    "rule_sanity": "basic",
+    "solc": "solc-0.8.21",
+    "solc_optimize_map": {
+        "MkrSky": "200",
+        "Sky": "200",
+        "MkrMock": "0"
+    },
+    "verify": "MkrSky:certora/MkrSky.spec",
+    "prover_args": [
+        "-mediumTimeout 180"
+    ],
+    "optimistic_loop": true,
+    "multi_assert_check": true,
+    "wait_for_results": "all"
+}

certora/MkrSky.spec

@@ -0,0 +1,183 @@
+// MkrSky.spec
+
+using Sky as sky;
+using MkrMock as mkr;
+
+methods {
+    function rate() external returns (uint256) envfree;
+    function sky.wards(address) external returns (uint256) envfree;
+    function sky.totalSupply() external returns (uint256) envfree;
+    function sky.balanceOf(address) external returns (uint256) envfree;
+    function sky.allowance(address, address) external returns (uint256) envfree;
+    function mkr.wards(address) external returns (uint256) envfree;
+    function mkr.totalSupply() external returns (uint256) envfree;
+    function mkr.balanceOf(address) external returns (uint256) envfree;
+    function mkr.allowance(address, address) external returns (uint256) envfree;
+}
+
+ghost balanceSumSky() returns mathint {
+    init_state axiom balanceSumSky() == 0;
+}
+
+hook Sstore sky.balanceOf[KEY address a] uint256 balance (uint256 old_balance) {
+    havoc balanceSumSky assuming balanceSumSky@new() == balanceSumSky@old() + balance - old_balance && balanceSumSky@new() >= 0;
+}
+
+invariant balanceSumSky_equals_totalSupply() balanceSumSky() == to_mathint(sky.totalSupply());
+
+ghost balanceSumMkr() returns mathint {
+    init_state axiom balanceSumMkr() == 0;
+}
+
+hook Sstore mkr.balanceOf[KEY address a] uint256 balance (uint256 old_balance) {
+    havoc balanceSumMkr assuming balanceSumMkr@new() == balanceSumMkr@old() + balance - old_balance && balanceSumMkr@new() >= 0;
+}
+
+invariant balanceSumMkr_equals_totalSupply() balanceSumMkr() == to_mathint(mkr.totalSupply());
+
+// Verify correct storage changes for non reverting mkrToSky
+rule mkrToSky(address usr, uint256 wad) {
+    env e;
+
+    require e.msg.sender != currentContract;
+
+    requireInvariant balanceSumSky_equals_totalSupply();
+    requireInvariant balanceSumMkr_equals_totalSupply();
+
+    address other;
+    require other != usr;
+    address other2;
+    require other2 != e.msg.sender;
+
+    mathint rate = rate();
+    mathint skyTotalSupplyBefore = sky.totalSupply();
+    mathint skyBalanceOfUsrBefore = sky.balanceOf(usr);
+    mathint skyBalanceOfOtherBefore = sky.balanceOf(other);
+    mathint mkrTotalSupplyBefore = mkr.totalSupply();
+    mathint mkrBalanceOfSenderBefore = mkr.balanceOf(e.msg.sender);
+    mathint mkrBalanceOfOtherBefore = mkr.balanceOf(other2);
+
+    mkrToSky(e, usr, wad);
+
+    mathint skyTotalSupplyAfter = sky.totalSupply();
+    mathint skyBalanceOfUsrAfter = sky.balanceOf(usr);
+    mathint skyBalanceOfOtherAfter = sky.balanceOf(other);
+    mathint mkrTotalSupplyAfter = mkr.totalSupply();
+    mathint mkrBalanceOfSenderAfter = mkr.balanceOf(e.msg.sender);
+    mathint mkrBalanceOfOtherAfter = mkr.balanceOf(other2);
+
+    assert skyTotalSupplyAfter == skyTotalSupplyBefore + wad * rate, "mkrToSky did not increase sky.totalSupply by wad * rate";
+    assert skyBalanceOfUsrAfter == skyBalanceOfUsrBefore + wad * rate, "mkrToSky did not increase sky.balanceOf[usr] by wad * rate";
+    assert skyBalanceOfOtherAfter == skyBalanceOfOtherBefore, "mkrToSky did not keep unchanged the rest of sky.balanceOf[x]";
+    assert mkrTotalSupplyAfter == mkrTotalSupplyBefore - wad, "mkrToSky did not decrease mkr.totalSupply by wad";
+    assert mkrBalanceOfSenderAfter == mkrBalanceOfSenderBefore - wad, "mkrToSky did not decrease mkr.balanceOf[sender] by wad";
+    assert mkrBalanceOfOtherAfter == mkrBalanceOfOtherBefore, "mkrToSky did not keep unchanged the rest of mkr.balanceOf[x]";
+}
+
+// Verify revert rules on mkrToSky
+rule mkrToSky_revert(address usr, uint256 wad) {
+    env e;
+
+    requireInvariant balanceSumSky_equals_totalSupply();
+    requireInvariant balanceSumMkr_equals_totalSupply();
+
+    require e.msg.sender != currentContract;
+
+    mathint rate = rate();
+    mathint mkrBalanceOfSender = mkr.balanceOf(e.msg.sender);
+    mathint mkrAllowanceSenderMkrSky = mkr.allowance(e.msg.sender, currentContract);
+    mathint skyWardsMkrSky = sky.wards(currentContract);
+    mathint skyTotalSupply = sky.totalSupply();
+
+    mkrToSky@withrevert(e, usr, wad);
+
+    bool revert1 = e.msg.value > 0;
+    bool revert2 = mkrBalanceOfSender < to_mathint(wad);
+    bool revert3 = mkrAllowanceSenderMkrSky < to_mathint(wad);
+    bool revert4 = skyWardsMkrSky != 1;
+    bool revert5 = skyTotalSupply + wad * rate > max_uint256;
+    bool revert6 = usr == 0 || usr == sky;
+
+    assert revert1 => lastReverted, "revert1 failed";
+    assert revert2 => lastReverted, "revert2 failed";
+    assert revert3 => lastReverted, "revert3 failed";
+    assert revert4 => lastReverted, "revert4 failed";
+    assert revert5 => lastReverted, "revert5 failed";
+    assert revert6 => lastReverted, "revert6 failed";
+    assert lastReverted => revert1 || revert2 || revert3 ||
+                           revert4 || revert5 || revert6, "Revert rules are not covering all the cases";
+}
+
+// Verify correct storage changes for non reverting skyToMkr
+rule skyToMkr(address usr, uint256 wad) {
+    env e;
+
+    require e.msg.sender != currentContract;
+
+    requireInvariant balanceSumSky_equals_totalSupply();
+    requireInvariant balanceSumMkr_equals_totalSupply();
+
+    address other;
+    require other != e.msg.sender;
+    address other2;
+    require other2 != usr;
+
+    mathint rate = rate();
+    mathint skyTotalSupplyBefore = sky.totalSupply();
+    mathint skyBalanceOfSenderBefore = sky.balanceOf(e.msg.sender);
+    mathint skyBalanceOfOtherBefore = sky.balanceOf(other);
+    mathint mkrTotalSupplyBefore = mkr.totalSupply();
+    mathint mkrBalanceOfUsrBefore = mkr.balanceOf(usr);
+    mathint mkrBalanceOfOtherBefore = mkr.balanceOf(other2);
+
+    skyToMkr(e, usr, wad);
+
+    mathint skyTotalSupplyAfter = sky.totalSupply();
+    mathint skyBalanceOfSenderAfter = sky.balanceOf(e.msg.sender);
+    mathint skyBalanceOfOtherAfter = sky.balanceOf(other);
+    mathint mkrTotalSupplyAfter = mkr.totalSupply();
+    mathint mkrBalanceOfUsrAfter = mkr.balanceOf(usr);
+    mathint mkrBalanceOfOtherAfter = mkr.balanceOf(other2);
+
+    assert skyTotalSupplyAfter == skyTotalSupplyBefore - wad, "skyToMkr did not decrease sky.totalSupply by wad";
+    assert skyBalanceOfSenderAfter == skyBalanceOfSenderBefore - wad, "skyToMkr did not decrease sky.balanceOf[sender] by wad";
+    assert skyBalanceOfOtherAfter == skyBalanceOfOtherBefore, "skyToMkr did not keep unchanged the rest of sky.balanceOf[x]";
+    assert mkrTotalSupplyAfter == mkrTotalSupplyBefore + wad / rate, "skyToMkr did not increase mkr.totalSupply by wad / rate";
+    assert mkrBalanceOfUsrAfter == mkrBalanceOfUsrBefore + wad / rate, "skyToMkr did not increase mkr.balanceOf[usr] by wad / rate";
+    assert mkrBalanceOfOtherAfter == mkrBalanceOfOtherBefore, "skyToMkr did not keep unchanged the rest of mkr.balanceOf[x]";
+}
+
+// Verify revert rules on skyToMkr
+rule skyToMkr_revert(address usr, uint256 wad) {
+    env e;
+
+    requireInvariant balanceSumSky_equals_totalSupply();
+    requireInvariant balanceSumMkr_equals_totalSupply();
+
+    require e.msg.sender != currentContract;
+
+    mathint rate = rate();
+    require rate > 0;
+    mathint skyBalanceOfSender = sky.balanceOf(e.msg.sender);
+    mathint skyAllowanceSenderMkrSky = sky.allowance(e.msg.sender, currentContract);
+    mathint mkrWardsMkrSky = mkr.wards(currentContract);
+    mathint mkrTotalSupply = mkr.totalSupply();
+
+    skyToMkr@withrevert(e, usr, wad);
+
+    bool revert1 = e.msg.value > 0;
+    bool revert2 = skyBalanceOfSender < to_mathint(wad);
+    bool revert3 = skyAllowanceSenderMkrSky < to_mathint(wad);
+    bool revert4 = mkrWardsMkrSky != 1;
+    bool revert5 = mkrTotalSupply + wad / rate > max_uint256;
+    bool revert6 = usr == 0 || usr == mkr;
+
+    assert revert1 => lastReverted, "revert1 failed";
+    assert revert2 => lastReverted, "revert2 failed";
+    assert revert3 => lastReverted, "revert3 failed";
+    assert revert4 => lastReverted, "revert4 failed";
+    assert revert5 => lastReverted, "revert5 failed";
+    assert revert6 => lastReverted, "revert6 failed";
+    assert lastReverted => revert1 || revert2 || revert3 ||
+                           revert4 || revert5 || revert6, "Revert rules are not covering all the cases";
+}

certora/SignerMock.sol

@@ -0,0 +1,11 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+
+pragma solidity ^0.8.21;
+
+contract SignerMock {
+    bytes32 sig;
+
+    function isValidSignature(bytes32, bytes memory) external view returns (bytes32) {
+        return sig;
+    }
+}