diff --git a/.gitignore b/.gitignore
index e2e7327..04ef355 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,5 @@
/out
+# certora
+.*certora*
+.last_confs/
+*.zip
diff --git a/certora/Dai.sol b/certora/Dai.sol
new file mode 100644
index 0000000..dd50d1b
--- /dev/null
+++ b/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 .
+
+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);
+ }
+}
diff --git a/certora/DaiJoin.sol b/certora/DaiJoin.sol
new file mode 100644
index 0000000..dd1ba75
--- /dev/null
+++ b/certora/DaiJoin.sol
@@ -0,0 +1,135 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+
+/// join.sol -- Basic token adapters
+
+// Copyright (C) 2018 Rain
+//
+// 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 .
+
+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);
+ }
+}
diff --git a/certora/Vat.sol b/certora/Vat.sol
new file mode 100644
index 0000000..6518009
--- /dev/null
+++ b/certora/Vat.sol
@@ -0,0 +1,246 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+
+/// vat.sol -- Dai CDP database
+
+// Copyright (C) 2018 Rain
+//
+// 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 .
+
+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 Vat {
+ // --- Auth ---
+ mapping (address => uint) public wards;
+ function rely(address usr) external auth { require(live == 1, "Vat/not-live"); wards[usr] = 1; }
+ function deny(address usr) external auth { require(live == 1, "Vat/not-live"); wards[usr] = 0; }
+ modifier auth {
+ require(wards[msg.sender] == 1, "Vat/not-authorized");
+ _;
+ }
+
+ mapping(address => mapping (address => uint)) public can;
+ function hope(address usr) external { can[msg.sender][usr] = 1; }
+ function nope(address usr) external { can[msg.sender][usr] = 0; }
+ function wish(address bit, address usr) internal view returns (bool) {
+ return either(bit == usr, can[bit][usr] == 1);
+ }
+
+ // --- Data ---
+ struct Ilk {
+ uint256 Art; // Total Normalised Debt [wad]
+ uint256 rate; // Accumulated Rates [ray]
+ uint256 spot; // Price with Safety Margin [ray]
+ uint256 line; // Debt Ceiling [rad]
+ uint256 dust; // Urn Debt Floor [rad]
+ }
+ struct Urn {
+ uint256 ink; // Locked Collateral [wad]
+ uint256 art; // Normalised Debt [wad]
+ }
+
+ mapping (bytes32 => Ilk) public ilks;
+ mapping (bytes32 => mapping (address => Urn )) public urns;
+ mapping (bytes32 => mapping (address => uint)) public gem; // [wad]
+ mapping (address => uint256) public dai; // [rad]
+ mapping (address => uint256) public sin; // [rad]
+
+ uint256 public debt; // Total Dai Issued [rad]
+ uint256 public vice; // Total Unbacked Dai [rad]
+ uint256 public Line; // Total Debt Ceiling [rad]
+ uint256 public live; // Active Flag
+
+ // --- Init ---
+ constructor() public {
+ wards[msg.sender] = 1;
+ live = 1;
+ }
+
+ // --- Math ---
+ function add(uint x, int y) internal pure returns (uint z) {
+ z = x + uint(y);
+ require(y >= 0 || z <= x);
+ require(y <= 0 || z >= x);
+ }
+ function sub(uint x, int y) internal pure returns (uint z) {
+ z = x - uint(y);
+ require(y <= 0 || z <= x);
+ require(y >= 0 || z >= x);
+ }
+ function mul(uint x, int y) internal pure returns (int z) {
+ z = int(x) * y;
+ require(int(x) >= 0);
+ require(y == 0 || z / y == int(x));
+ }
+ 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);
+ }
+ function mul(uint x, uint y) internal pure returns (uint z) {
+ require(y == 0 || (z = x * y) / y == x);
+ }
+
+ // --- Administration ---
+ function init(bytes32 ilk) external auth {
+ require(ilks[ilk].rate == 0, "Vat/ilk-already-init");
+ ilks[ilk].rate = 10 ** 27;
+ }
+ function file(bytes32 what, uint data) external auth {
+ require(live == 1, "Vat/not-live");
+ if (what == "Line") Line = data;
+ else revert("Vat/file-unrecognized-param");
+ }
+ function file(bytes32 ilk, bytes32 what, uint data) external auth {
+ require(live == 1, "Vat/not-live");
+ if (what == "spot") ilks[ilk].spot = data;
+ else if (what == "line") ilks[ilk].line = data;
+ else if (what == "dust") ilks[ilk].dust = data;
+ else revert("Vat/file-unrecognized-param");
+ }
+ function cage() external auth {
+ live = 0;
+ }
+
+ // --- Fungibility ---
+ function slip(bytes32 ilk, address usr, int256 wad) external auth {
+ gem[ilk][usr] = add(gem[ilk][usr], wad);
+ }
+ function flux(bytes32 ilk, address src, address dst, uint256 wad) external {
+ require(wish(src, msg.sender), "Vat/not-allowed");
+ gem[ilk][src] = sub(gem[ilk][src], wad);
+ gem[ilk][dst] = add(gem[ilk][dst], wad);
+ }
+ function move(address src, address dst, uint256 rad) external {
+ require(wish(src, msg.sender), "Vat/not-allowed");
+ dai[src] = sub(dai[src], rad);
+ dai[dst] = add(dai[dst], rad);
+ }
+
+ function either(bool x, bool y) internal pure returns (bool z) {
+ assembly{ z := or(x, y)}
+ }
+ function both(bool x, bool y) internal pure returns (bool z) {
+ assembly{ z := and(x, y)}
+ }
+
+ // --- CDP Manipulation ---
+ function frob(bytes32 i, address u, address v, address w, int dink, int dart) external {
+ // system is live
+ require(live == 1, "Vat/not-live");
+
+ Urn memory urn = urns[i][u];
+ Ilk memory ilk = ilks[i];
+ // ilk has been initialised
+ require(ilk.rate != 0, "Vat/ilk-not-init");
+
+ urn.ink = add(urn.ink, dink);
+ urn.art = add(urn.art, dart);
+ ilk.Art = add(ilk.Art, dart);
+
+ int dtab = mul(ilk.rate, dart);
+ uint tab = mul(ilk.rate, urn.art);
+ debt = add(debt, dtab);
+
+ // either debt has decreased, or debt ceilings are not exceeded
+ require(either(dart <= 0, both(mul(ilk.Art, ilk.rate) <= ilk.line, debt <= Line)), "Vat/ceiling-exceeded");
+ // urn is either less risky than before, or it is safe
+ require(either(both(dart <= 0, dink >= 0), tab <= mul(urn.ink, ilk.spot)), "Vat/not-safe");
+
+ // urn is either more safe, or the owner consents
+ require(either(both(dart <= 0, dink >= 0), wish(u, msg.sender)), "Vat/not-allowed-u");
+ // collateral src consents
+ require(either(dink <= 0, wish(v, msg.sender)), "Vat/not-allowed-v");
+ // debt dst consents
+ require(either(dart >= 0, wish(w, msg.sender)), "Vat/not-allowed-w");
+
+ // urn has no debt, or a non-dusty amount
+ require(either(urn.art == 0, tab >= ilk.dust), "Vat/dust");
+
+ gem[i][v] = sub(gem[i][v], dink);
+ dai[w] = add(dai[w], dtab);
+
+ urns[i][u] = urn;
+ ilks[i] = ilk;
+ }
+ // --- CDP Fungibility ---
+ function fork(bytes32 ilk, address src, address dst, int dink, int dart) external {
+ Urn storage u = urns[ilk][src];
+ Urn storage v = urns[ilk][dst];
+ Ilk storage i = ilks[ilk];
+
+ u.ink = sub(u.ink, dink);
+ u.art = sub(u.art, dart);
+ v.ink = add(v.ink, dink);
+ v.art = add(v.art, dart);
+
+ uint utab = mul(u.art, i.rate);
+ uint vtab = mul(v.art, i.rate);
+
+ // both sides consent
+ require(both(wish(src, msg.sender), wish(dst, msg.sender)), "Vat/not-allowed");
+
+ // both sides safe
+ require(utab <= mul(u.ink, i.spot), "Vat/not-safe-src");
+ require(vtab <= mul(v.ink, i.spot), "Vat/not-safe-dst");
+
+ // both sides non-dusty
+ require(either(utab >= i.dust, u.art == 0), "Vat/dust-src");
+ require(either(vtab >= i.dust, v.art == 0), "Vat/dust-dst");
+ }
+ // --- CDP Confiscation ---
+ function grab(bytes32 i, address u, address v, address w, int dink, int dart) external auth {
+ Urn storage urn = urns[i][u];
+ Ilk storage ilk = ilks[i];
+
+ urn.ink = add(urn.ink, dink);
+ urn.art = add(urn.art, dart);
+ ilk.Art = add(ilk.Art, dart);
+
+ int dtab = mul(ilk.rate, dart);
+
+ gem[i][v] = sub(gem[i][v], dink);
+ sin[w] = sub(sin[w], dtab);
+ vice = sub(vice, dtab);
+ }
+
+ // --- Settlement ---
+ function heal(uint rad) external {
+ address u = msg.sender;
+ sin[u] = sub(sin[u], rad);
+ dai[u] = sub(dai[u], rad);
+ vice = sub(vice, rad);
+ debt = sub(debt, rad);
+ }
+ function suck(address u, address v, uint rad) external auth {
+ sin[u] = add(sin[u], rad);
+ dai[v] = add(dai[v], rad);
+ vice = add(vice, rad);
+ debt = add(debt, rad);
+ }
+
+ // --- Rates ---
+ function fold(bytes32 i, address u, int rate) external auth {
+ require(live == 1, "Vat/not-live");
+ Ilk storage ilk = ilks[i];
+ ilk.rate = add(ilk.rate, rate);
+ int rad = mul(ilk.Art, rate);
+ dai[u] = add(dai[u], rad);
+ debt = add(debt, rad);
+ }
+}
diff --git a/certora/flash.spec b/certora/flash.spec
new file mode 100644
index 0000000..a265a14
--- /dev/null
+++ b/certora/flash.spec
@@ -0,0 +1,164 @@
+// flash.spec
+
+// certoraRun src/flash.sol:DssFlash certora/Vat.sol certora/DaiJoin.sol certora/Dai.sol --link DssFlash:vat=Vat DssFlash:dai=Dai DssFlash:daiJoin=DaiJoin DaiJoin:vat=Vat DaiJoin:dai=Dai --verify DssFlash:certora/flash.spec --rule_sanity --solc_args "['--optimize','--optimize-runs','200']"
+
+using Dai as daiToken
+using DaiJoin as daiJoin
+using Vat as vat
+
+methods {
+ wards(address) returns (uint256) envfree
+ vat() returns (address) envfree
+ daiJoin() returns (address) envfree
+ dai() returns (address) envfree
+ max() returns (uint256) envfree
+ CALLBACK_SUCCESS() returns (bytes32) envfree
+ CALLBACK_SUCCESS_VAT_DAI() returns (bytes32) envfree
+ maxFlashLoan(address) returns (uint256) envfree
+ flashFee(address, uint256) returns (uint256) envfree
+ daiJoin.live() returns (uint256) envfree
+ daiJoin.vat() returns (address) envfree
+ daiJoin.dai() returns (address) envfree
+ vat.wards(address) returns (uint256) envfree
+ vat.can(address, address) returns (uint256) envfree
+ vat.dai(address) returns (uint256) envfree
+ vat.sin(address) returns (uint256) envfree
+ vat.vice() returns (uint256) envfree
+ vat.debt() returns (uint256) envfree
+
+ onFlashLoan(address, address, uint256, bytes) => HAVOC_ECF
+}
+
+ghost lockedGhost() returns uint256;
+
+hook Sstore locked uint256 n_locked STORAGE {
+ havoc lockedGhost assuming lockedGhost@new() == n_locked;
+}
+
+hook Sload uint256 value locked STORAGE {
+ require lockedGhost() == value;
+}
+
+// Verify that wards behaves correctly on rely
+rule rely(address usr) {
+ env e;
+
+ rely(e, usr);
+
+ assert(wards(usr) == 1, "Rely did not set the wards as expected");
+}
+
+// Verify revert rules on rely
+rule rely_revert(address usr) {
+ env e;
+
+ uint256 ward = wards(e.msg.sender);
+
+ rely@withrevert(e, usr);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = ward != 1;
+
+ assert(revert1 => lastReverted, "Sending ETH did not revert");
+ assert(revert2 => lastReverted, "Lack of auth did not revert");
+ assert(lastReverted => revert1 || revert2, "Revert rules are not covering all the cases");
+}
+
+// Verify that wards behaves correctly on deny
+rule deny(address usr) {
+ env e;
+
+ deny(e, usr);
+
+ assert(wards(usr) == 0, "Deny did not set the wards as expected");
+}
+
+// Verify revert rules on deny
+rule deny_revert(address usr) {
+ env e;
+
+ uint256 ward = wards(e.msg.sender);
+
+ deny@withrevert(e, usr);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = ward != 1;
+
+ assert(revert1 => lastReverted, "Sending ETH did not revert");
+ assert(revert2 => lastReverted, "Lack of auth did not revert");
+ assert(lastReverted => revert1 || revert2, "Revert rules are not covering all the cases");
+}
+
+// Verify that max behave correctly on file
+rule file(bytes32 what, uint256 data) {
+ env e;
+
+ file(e, what, data);
+
+ assert(max() == data, "File did not set max as expected");
+}
+
+// Verify revert rules on file
+rule file_revert(bytes32 what, uint256 data) {
+ env e;
+
+ uint256 ward = wards(e.msg.sender);
+
+ file@withrevert(e, what, data);
+
+ bool revert1 = e.msg.value > 0;
+ bool revert2 = ward != 1;
+ bool revert3 = what != 0x6d61780000000000000000000000000000000000000000000000000000000000; // what != "max"
+ bool revert4 = data > 10 ^ 45;
+
+ assert(revert1 => lastReverted, "Sending ETH did not revert");
+ assert(revert2 => lastReverted, "Lack of auth did not revert");
+ assert(revert3 => lastReverted, "File unrecognized param did not revert");
+ assert(revert4 => lastReverted, "Max too large did not revert");
+
+ assert(lastReverted => revert1 || revert2 || revert3 || revert4, "Revert rules are not covering all the cases");
+}
+
+// Verify that only unlocked dai has a max flash loan
+rule maxFlashLoan(address token) {
+ uint256 locked = lockedGhost();
+
+ uint256 expectedMax = locked == 0 && token == dai() ? max() : 0;
+
+ uint256 actualMax = maxFlashLoan(token);
+
+ assert(actualMax == expectedMax, "Max flash loan is invalid");
+}
+
+// Verify flash fee always returns 0
+rule flashFee(address token, uint256 amount) {
+ uint256 fee = flashFee(token, amount);
+
+ assert(fee == 0, "Fee should always be 0");
+}
+
+// Verify revert rules on flashFee
+rule flashFee_revert(address token, uint256 amount) {
+ address _dai = dai();
+
+ flashFee@withrevert(token, amount);
+
+ bool revert1 = token != _dai;
+
+ assert(revert1 => lastReverted, "Non-dai token did not revert");
+
+ assert(lastReverted => revert1, "Revert rules are not covering all the cases");
+}
+
+// Verify flash loan works as expected
+rule flashLoan() {
+ env e;
+ calldataarg args;
+
+ uint256 sin = vat.sin(currentContract);
+
+ bool result = flashLoan(e, args);
+
+ assert(vat.sin(currentContract) == sin, "sin should be unchanged");
+ assert(result, "result should be true");
+}
diff --git a/src/flash.sol b/src/flash.sol
index 7eb82f1..3ac5304 100644
--- a/src/flash.sol
+++ b/src/flash.sol
@@ -56,10 +56,8 @@ contract DssFlash is IERC3156FlashLender, IVatDaiFlashLender {
VatLike public immutable vat;
DaiJoinLike public immutable daiJoin;
DaiLike public immutable dai;
- address public immutable vow; // vow intentionally set immutable to save gas
uint256 public max; // Maximum borrowable Dai [wad]
- uint256 public toll; // Fee [wad = 100%]
uint256 private locked; // Reentrancy guard
bytes32 public constant CALLBACK_SUCCESS = keccak256("ERC3156FlashBorrower.onFlashLoan");
@@ -80,26 +78,21 @@ contract DssFlash is IERC3156FlashLender, IVatDaiFlashLender {
}
// --- Init ---
- constructor(address daiJoin_, address vow_) public {
+ constructor(address daiJoin_) public {
wards[msg.sender] = 1;
emit Rely(msg.sender);
VatLike vat_ = vat = VatLike(DaiJoinLike(daiJoin_).vat());
daiJoin = DaiJoinLike(daiJoin_);
DaiLike dai_ = dai = DaiLike(DaiJoinLike(daiJoin_).dai());
- vow = vow_;
vat_.hope(daiJoin_);
dai_.approve(daiJoin_, type(uint256).max);
}
// --- Math ---
- uint256 constant WAD = 10 ** 18;
uint256 constant RAY = 10 ** 27;
uint256 constant RAD = 10 ** 45;
- function _add(uint256 x, uint256 y) internal pure returns (uint256 z) {
- require((z = x + y) >= x);
- }
function _mul(uint256 x, uint256 y) internal pure returns (uint256 z) {
require(y == 0 || (z = x * y) / y == x);
}
@@ -109,7 +102,7 @@ contract DssFlash is IERC3156FlashLender, IVatDaiFlashLender {
if (what == "max") {
// Add an upper limit of 10^27 DAI to avoid breaking technical assumptions of DAI << 2^256 - 1
require((max = data) <= RAD, "DssFlash/ceiling-too-high");
- } else if (what == "toll") toll = data;
+ }
else revert("DssFlash/file-unrecognized-param");
emit File(what, data);
}
@@ -130,7 +123,7 @@ contract DssFlash is IERC3156FlashLender, IVatDaiFlashLender {
) external override view returns (uint256) {
require(token == address(dai), "DssFlash/token-unsupported");
- return _mul(amount, toll) / WAD;
+ return 0;
}
function flashLoan(
IERC3156FlashBorrower receiver,
@@ -142,21 +135,19 @@ contract DssFlash is IERC3156FlashLender, IVatDaiFlashLender {
require(amount <= max, "DssFlash/ceiling-exceeded");
uint256 amt = _mul(amount, RAY);
- uint256 fee = _mul(amount, toll) / WAD;
- uint256 total = _add(amount, fee);
vat.suck(address(this), address(this), amt);
daiJoin.exit(address(receiver), amount);
- emit FlashLoan(address(receiver), token, amount, fee);
+ emit FlashLoan(address(receiver), token, amount, 0);
require(
- receiver.onFlashLoan(msg.sender, token, amount, fee, data) == CALLBACK_SUCCESS,
+ receiver.onFlashLoan(msg.sender, token, amount, 0, data) == CALLBACK_SUCCESS,
"DssFlash/callback-failed"
);
- dai.transferFrom(address(receiver), address(this), total); // The fee is also enforced here
- daiJoin.join(address(this), total);
+ dai.transferFrom(address(receiver), address(this), amount);
+ daiJoin.join(address(this), amount);
vat.heal(amt);
return true;
@@ -170,29 +161,17 @@ contract DssFlash is IERC3156FlashLender, IVatDaiFlashLender {
) external override lock returns (bool) {
require(amount <= _mul(max, RAY), "DssFlash/ceiling-exceeded");
- uint256 prev = vat.dai(address(this));
- uint256 fee = _mul(amount, toll) / WAD;
-
vat.suck(address(this), address(receiver), amount);
- emit VatDaiFlashLoan(address(receiver), amount, fee);
+ emit VatDaiFlashLoan(address(receiver), amount, 0);
require(
- receiver.onVatDaiFlashLoan(msg.sender, amount, fee, data) == CALLBACK_SUCCESS_VAT_DAI,
+ receiver.onVatDaiFlashLoan(msg.sender, amount, 0, data) == CALLBACK_SUCCESS_VAT_DAI,
"DssFlash/callback-failed"
);
vat.heal(amount);
- require(vat.dai(address(this)) >= _add(prev, fee), "DssFlash/insufficient-fee");
return true;
}
-
- function convert() external lock {
- daiJoin.join(address(this), dai.balanceOf(address(this)));
- }
-
- function accrue() external lock {
- vat.move(address(this), vow, vat.dai(address(this)));
- }
}
diff --git a/src/flash.t.sol b/src/flash.t.sol
index b1be1cc..c93a3df 100644
--- a/src/flash.t.sol
+++ b/src/flash.t.sol
@@ -333,8 +333,6 @@ contract DssFlashTest is DSTest {
bytes32 constant ilk = "gold";
- uint256 constant RATE_ONE_PCT = 10 ** 16;
-
function ray(uint256 wad) internal pure returns (uint256) {
return wad * 10 ** 9;
}
@@ -371,7 +369,7 @@ contract DssFlashTest is DSTest {
vat.rely(address(daiJoin));
dai.rely(address(daiJoin));
- flash = new DssFlash(address(daiJoin), address(vow));
+ flash = new DssFlash(address(daiJoin));
pip = new DSValue();
pip.poke(bytes32(uint256(5 ether))); // Spot = $2.5
@@ -407,7 +405,7 @@ contract DssFlashTest is DSTest {
dai.rely(address(dexTradeReceiver));
}
- function test_mint_no_fee_payback () public {
+ function test_mint_payback () public {
flash.vatDaiFlashLoan(immediatePaybackReceiver, rad(10 ether), "");
flash.flashLoan(immediatePaybackReceiver, address(dai), 10 ether, "");
@@ -455,123 +453,6 @@ contract DssFlashTest is DSTest {
flash.flashLoan(immediatePaybackReceiver, address(dai), 10 ether, "");
}
- // test happy path onFlashLoan() returns vat.dai() == add(_amount, fee)
- // Make sure we test core system accounting balances before and after.
- function test_mint_with_fee () public {
- flash.file("toll", RATE_ONE_PCT);
- mintAndPaybackReceiver.setMint(10 ether);
-
- flash.vatDaiFlashLoan(mintAndPaybackReceiver, rad(100 ether), "");
- flash.accrue();
-
- assertEq(vow.Joy(), rad(1 ether));
- assertEq(vat.dai(address(mintAndPaybackReceiver)), rad(9 ether));
-
- flash.flashLoan(mintAndPaybackReceiver, address(dai), 100 ether, "");
- flash.accrue();
-
- assertEq(vow.Joy(), rad(2 ether));
- assertEq(vat.dai(address(mintAndPaybackReceiver)), rad(9 ether));
- assertEq(dai.balanceOf(address(mintAndPaybackReceiver)), 9 ether);
- }
-
- // Test mint doesn't fail when contract already has a Dai balance
- function test_preexisting_dai_in_flash () public {
- flash.file("toll", RATE_ONE_PCT);
-
- // Move some collateral to the flash so it preexists the loan
- vat.move(address(this), address(flash), rad(1 ether));
-
- mintAndPaybackReceiver.setMint(10 ether);
-
- flash.vatDaiFlashLoan(mintAndPaybackReceiver, rad(100 ether), "");
- flash.accrue();
-
- assertEq(vow.Joy(), rad(2 ether));
- assertEq(vat.dai(address(mintAndPaybackReceiver)), rad(9 ether));
- // Ensure pre-existing amount remains in flash
- assertEq(vat.dai(address(flash)), 0);
-
- // Test for erc20 dai
- dai.mint(address(flash), 1 ether);
-
- flash.flashLoan(mintAndPaybackReceiver, address(dai), 100 ether, "");
- flash.accrue();
-
- assertEq(vow.Joy(), rad(3 ether));
- assertEq(vat.dai(address(mintAndPaybackReceiver)), rad(9 ether));
- assertEq(dai.balanceOf(address(mintAndPaybackReceiver)), 9 ether);
- // Ensure pre-existing amount remains in flash
- assertEq(vat.dai(address(flash)), 0);
- assertEq(dai.balanceOf(address(flash)), 1 ether);
- flash.convert();
- assertEq(vat.dai(address(flash)), rad(1 ether));
- assertEq(dai.balanceOf(address(flash)), 0);
- flash.accrue();
- assertEq(vow.Joy(), rad(4 ether));
- assertEq(vat.dai(address(flash)), 0);
- assertEq(dai.balanceOf(address(flash)), 0);
- }
-
- // test onFlashLoan that return vat.dai() < add(_amount, fee) fails
- function testFail_mint_insufficient_dai1 () public {
- flash.file("toll", 5 * RATE_ONE_PCT);
- mintAndPaybackAllReceiver.setMint(4 ether);
-
- flash.vatDaiFlashLoan(mintAndPaybackAllReceiver, rad(100 ether), "");
- }
- function testFail_mint_insufficient_dai2 () public {
- flash.file("toll", 5 * RATE_ONE_PCT);
- mintAndPaybackAllReceiver.setMint(4 ether);
-
- flash.flashLoan(mintAndPaybackAllReceiver, address(dai), 100 ether, "");
- }
-
- // test onFlashLoan that return vat.dai() > add(_amount, fee)
- // ERC 3156 says to use approve instead of transfer so you never take more than you require
- // This is an intentional difference between ERC20 Flash Mint and Vat Dai Flash Mint
- function test_mint_too_much_dai2 () public {
- flash.file("toll", 5 * RATE_ONE_PCT);
- mintAndPaybackAllReceiver.setMint(10 ether);
-
- // First mint overpays
- flash.flashLoan(mintAndPaybackAllReceiver, address(dai), 100 ether, "");
- flash.accrue();
-
- assertEq(vow.Joy(), rad(5 ether));
- assertEq(dai.balanceOf(address(flash)), 0 ether);
- }
- // The vat dai version will allow overpays
- function test_mint_too_much_dai1 () public {
- flash.file("toll", 5 * RATE_ONE_PCT);
- mintAndPaybackAllReceiver.setMint(10 ether);
-
- // First mint overpays
- flash.vatDaiFlashLoan(mintAndPaybackAllReceiver, rad(100 ether), "");
- flash.accrue();
-
- assertEq(vow.Joy(), rad(10 ether));
- assertEq(vat.dai(address(flash)), 0);
- }
-
- // test that data sends properly
- function test_mint_data () public {
- flash.file("toll", 5 * RATE_ONE_PCT);
- uint256 mintAmount = 8 ether;
-
- flash.vatDaiFlashLoan(mintAndPaybackDataReceiver, rad(100 ether), abi.encodePacked(mintAmount));
- flash.accrue();
-
- assertEq(vow.Joy(), rad(5 ether));
- assertEq(vat.dai(address(mintAndPaybackDataReceiver)), rad(3 ether));
-
- flash.flashLoan(mintAndPaybackDataReceiver, address(dai), 100 ether, abi.encodePacked(mintAmount));
- flash.accrue();
-
- assertEq(vow.Joy(), rad(10 ether));
- assertEq(dai.balanceOf(address(mintAndPaybackDataReceiver)), 3 ether);
- }
-
// test reentrancy disallowed
function testFail_mint_reentrancy1 () public {
flash.vatDaiFlashLoan(reentrancyReceiver, rad(100 ether), "");
@@ -599,12 +480,10 @@ contract DssFlashTest is DSTest {
}
function test_flash_fee () public {
- flash.file("toll", 5 * RATE_ONE_PCT);
- assertEq(flash.flashFee(address(dai), 100 ether), 5 ether);
+ assertEq(flash.flashFee(address(dai), 100 ether), 0);
}
function testFail_flash_fee () public {
- flash.file("toll", 5 * RATE_ONE_PCT);
flash.flashFee(address(daiJoin), 100 ether); // Any other address should fail
}