Certora Specs

.gitignore

@@ -1 +1,5 @@
 /out
+# certora
+.*certora*
+.last_confs/
+*.zip

certora/Dai.sol

@@ -0,0 +1,145 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+
+// Copyright (C) 2017, 2018, 2019 dbrock, rain, mrchico
+
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU Affero General Public License as published by
+// the Free Software Foundation, either version 3 of the License, or
+// (at your option) any later version.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU Affero General Public License for more details.
+//
+// You should have received a copy of the GNU Affero General Public License
+// along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+pragma solidity >=0.5.12;
+
+// FIXME: This contract was altered compared to the production version.
+// It doesn't use LibNote anymore.
+// New deployments of this contract will need to include custom events (TO DO).
+
+contract Dai {
+    // --- Auth ---
+    mapping (address => uint) public wards;
+    function rely(address guy) external auth { wards[guy] = 1; }
+    function deny(address guy) external auth { wards[guy] = 0; }
+    modifier auth {
+        require(wards[msg.sender] == 1, "Dai/not-authorized");
+        _;
+    }
+
+    // --- ERC20 Data ---
+    string  public constant name     = "Dai Stablecoin";
+    string  public constant symbol   = "DAI";
+    string  public constant version  = "1";
+    uint8   public constant decimals = 18;
+    uint256 public totalSupply;
+
+    mapping (address => uint)                      public balanceOf;
+    mapping (address => mapping (address => uint)) public allowance;
+    mapping (address => uint)                      public nonces;
+
+    event Approval(address indexed src, address indexed guy, uint wad);
+    event Transfer(address indexed src, address indexed dst, uint wad);
+
+    // --- Math ---
+    function add(uint x, uint y) internal pure returns (uint z) {
+        require((z = x + y) >= x);
+    }
+    function sub(uint x, uint y) internal pure returns (uint z) {
+        require((z = x - y) <= x);
+    }
+
+    // --- EIP712 niceties ---
+    bytes32 public DOMAIN_SEPARATOR;
+    // bytes32 public constant PERMIT_TYPEHASH = keccak256("Permit(address holder,address spender,uint256 nonce,uint256 expiry,bool allowed)");
+    bytes32 public constant PERMIT_TYPEHASH = 0xea2aa0a1be11a07ed86d755c93467f4f82362b452371d1ba94d1715123511acb;
+
+    constructor(uint256 chainId_) public {
+        wards[msg.sender] = 1;
+        DOMAIN_SEPARATOR = keccak256(abi.encode(
+            keccak256("EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)"),
+            keccak256(bytes(name)),
+            keccak256(bytes(version)),
+            chainId_,
+            address(this)
+        ));
+    }
+
+    // --- Token ---
+    function transfer(address dst, uint wad) external returns (bool) {
+        return transferFrom(msg.sender, dst, wad);
+    }
+    function transferFrom(address src, address dst, uint wad)
+        public returns (bool)
+    {
+        require(balanceOf[src] >= wad, "Dai/insufficient-balance");
+        if (src != msg.sender && allowance[src][msg.sender] != uint(-1)) {
+            require(allowance[src][msg.sender] >= wad, "Dai/insufficient-allowance");
+            allowance[src][msg.sender] = sub(allowance[src][msg.sender], wad);
+        }
+        balanceOf[src] = sub(balanceOf[src], wad);
+        balanceOf[dst] = add(balanceOf[dst], wad);
+        emit Transfer(src, dst, wad);
+        return true;
+    }
+    function mint(address usr, uint wad) external auth {
+        balanceOf[usr] = add(balanceOf[usr], wad);
+        totalSupply    = add(totalSupply, wad);
+        emit Transfer(address(0), usr, wad);
+    }
+    function burn(address usr, uint wad) external {
+        require(balanceOf[usr] >= wad, "Dai/insufficient-balance");
+        if (usr != msg.sender && allowance[usr][msg.sender] != uint(-1)) {
+            require(allowance[usr][msg.sender] >= wad, "Dai/insufficient-allowance");
+            allowance[usr][msg.sender] = sub(allowance[usr][msg.sender], wad);
+        }
+        balanceOf[usr] = sub(balanceOf[usr], wad);
+        totalSupply    = sub(totalSupply, wad);
+        emit Transfer(usr, address(0), wad);
+    }
+    function approve(address usr, uint wad) external returns (bool) {
+        allowance[msg.sender][usr] = wad;
+        emit Approval(msg.sender, usr, wad);
+        return true;
+    }
+
+    // --- Alias ---
+    function push(address usr, uint wad) external {
+        transferFrom(msg.sender, usr, wad);
+    }
+    function pull(address usr, uint wad) external {
+        transferFrom(usr, msg.sender, wad);
+    }
+    function move(address src, address dst, uint wad) external {
+        transferFrom(src, dst, wad);
+    }
+
+    // --- Approve by signature ---
+    function permit(address holder, address spender, uint256 nonce, uint256 expiry,
+                    bool allowed, uint8 v, bytes32 r, bytes32 s) external
+    {
+        bytes32 digest =
+            keccak256(abi.encodePacked(
+                "\x19\x01",
+                DOMAIN_SEPARATOR,
+                keccak256(abi.encode(PERMIT_TYPEHASH,
+                                     holder,
+                                     spender,
+                                     nonce,
+                                     expiry,
+                                     allowed))
+        ));
+
+        require(holder != address(0), "Dai/invalid-address-0");
+        require(holder == ecrecover(digest, v, r, s), "Dai/invalid-permit");
+        require(expiry == 0 || now <= expiry, "Dai/permit-expired");
+        require(nonce == nonces[holder]++, "Dai/invalid-nonce");
+        uint wad = allowed ? uint(-1) : 0;
+        allowance[holder][spender] = wad;
+        emit Approval(holder, spender, wad);
+    }
+}

certora/DaiJoin.sol

@@ -0,0 +1,135 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+
+/// join.sol -- Basic token adapters
+
+// Copyright (C) 2018 Rain <rainbreak@riseup.net>
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU Affero General Public License as published by
+// the Free Software Foundation, either version 3 of the License, or
+// (at your option) any later version.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU Affero General Public License for more details.
+//
+// You should have received a copy of the GNU Affero General Public License
+// along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+pragma solidity >=0.5.12;
+
+// FIXME: This contract was altered compared to the production version.
+// It doesn't use LibNote anymore.
+// New deployments of this contract will need to include custom events (TO DO).
+
+interface GemLike {
+    function decimals() external view returns (uint);
+    function transfer(address,uint) external returns (bool);
+    function transferFrom(address,address,uint) external returns (bool);
+}
+
+interface DSTokenLike {
+    function mint(address,uint) external;
+    function burn(address,uint) external;
+}
+
+interface VatLike {
+    function slip(bytes32,address,int) external;
+    function move(address,address,uint) external;
+}
+
+/*
+    Here we provide *adapters* to connect the Vat to arbitrary external
+    token implementations, creating a bounded context for the Vat. The
+    adapters here are provided as working examples:
+      - `GemJoin`: For well behaved ERC20 tokens, with simple transfer
+                   semantics.
+      - `ETHJoin`: For native Ether.
+      - `DaiJoin`: For connecting internal Dai balances to an external
+                   `DSToken` implementation.
+    In practice, adapter implementations will be varied and specific to
+    individual collateral types, accounting for different transfer
+    semantics and token standards.
+    Adapters need to implement two basic methods:
+      - `join`: enter collateral into the system
+      - `exit`: remove collateral from the system
+*/
+
+contract GemJoin {
+    // --- Auth ---
+    mapping (address => uint) public wards;
+    function rely(address usr) external auth { wards[usr] = 1; }
+    function deny(address usr) external auth { wards[usr] = 0; }
+    modifier auth {
+        require(wards[msg.sender] == 1, "GemJoin/not-authorized");
+        _;
+    }
+
+    VatLike public vat;   // CDP Engine
+    bytes32 public ilk;   // Collateral Type
+    GemLike public gem;
+    uint    public dec;
+    uint    public live;  // Active Flag
+
+    constructor(address vat_, bytes32 ilk_, address gem_) public {
+        wards[msg.sender] = 1;
+        live = 1;
+        vat = VatLike(vat_);
+        ilk = ilk_;
+        gem = GemLike(gem_);
+        dec = gem.decimals();
+    }
+    function cage() external auth {
+        live = 0;
+    }
+    function join(address usr, uint wad) external {
+        require(live == 1, "GemJoin/not-live");
+        require(int(wad) >= 0, "GemJoin/overflow");
+        vat.slip(ilk, usr, int(wad));
+        require(gem.transferFrom(msg.sender, address(this), wad), "GemJoin/failed-transfer");
+    }
+    function exit(address usr, uint wad) external {
+        require(wad <= 2 ** 255, "GemJoin/overflow");
+        vat.slip(ilk, msg.sender, -int(wad));
+        require(gem.transfer(usr, wad), "GemJoin/failed-transfer");
+    }
+}
+
+contract DaiJoin {
+    // --- Auth ---
+    mapping (address => uint) public wards;
+    function rely(address usr) external auth { wards[usr] = 1; }
+    function deny(address usr) external auth { wards[usr] = 0; }
+    modifier auth {
+        require(wards[msg.sender] == 1, "DaiJoin/not-authorized");
+        _;
+    }
+
+    VatLike public vat;      // CDP Engine
+    DSTokenLike public dai;  // Stablecoin Token
+    uint    public live;     // Active Flag
+
+    constructor(address vat_, address dai_) public {
+        wards[msg.sender] = 1;
+        live = 1;
+        vat = VatLike(vat_);
+        dai = DSTokenLike(dai_);
+    }
+    function cage() external auth {
+        live = 0;
+    }
+    uint constant ONE = 10 ** 27;
+    function mul(uint x, uint y) internal pure returns (uint z) {
+        require(y == 0 || (z = x * y) / y == x);
+    }
+    function join(address usr, uint wad) external {
+        vat.move(address(this), usr, mul(ONE, wad));
+        dai.burn(msg.sender, wad);
+    }
+    function exit(address usr, uint wad) external {
+        require(live == 1, "DaiJoin/not-live");
+        vat.move(msg.sender, address(this), mul(ONE, wad));
+        dai.mint(usr, wad);
+    }
+}