-
Notifications
You must be signed in to change notification settings - Fork 25
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #41 from usmfum/feat/invariants
Feat/invariants
- Loading branch information
Showing
14 changed files
with
316 additions
and
20 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -124,3 +124,6 @@ typings/ | |
|
||
# ignore types | ||
types/ | ||
|
||
# crytic and echidna | ||
crytic-export/ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,88 @@ | ||
// SPDX-License-Identifier: GPL-3.0-or-later | ||
pragma solidity ^0.6.7; | ||
import "../IUSM.sol"; | ||
import "../USM.sol"; | ||
import "../FUM.sol"; | ||
import "../oracles/TestOracle.sol"; | ||
import "../mocks/MockWETH9.sol"; | ||
import "../WadMath.sol"; | ||
import "@nomiclabs/buidler/console.sol"; | ||
|
||
|
||
/** | ||
* This fuzzing contract tests that USM.sol moves Eth between itself and the clients accordingly to the parameters and return values of mint, burn, fund and defund. | ||
*/ | ||
contract USMFuzzingEthMgmt { | ||
using WadMath for uint; | ||
|
||
USM internal usm; | ||
FUM internal fum; | ||
MockWETH9 internal weth; | ||
TestOracle internal oracle; | ||
|
||
constructor() public { | ||
weth = new MockWETH9(); | ||
oracle = new TestOracle(25000000000, 8); | ||
usm = new USM(address(oracle), address(weth)); | ||
fum = FUM(usm.fum()); | ||
|
||
weth.approve(address(usm), uint(-1)); | ||
usm.approve(address(usm), uint(-1)); | ||
fum.approve(address(usm), uint(-1)); | ||
} | ||
|
||
/// @dev Test that USM.sol takes eth when minting. | ||
/// Any function that is public will be run as a test, with random values assigned to each parameter | ||
function testMintEthValue(uint ethIn) public { // To exclude a function from testing, make it internal | ||
// A failing require aborts this test instance without failing the fuzzing | ||
require(ethIn >= 10**14); // I'm restricting tests to a range of inputs with this | ||
|
||
weth.mint(ethIn); | ||
|
||
uint valueBefore = weth.balanceOf(address(usm)); | ||
usm.mint(address(this), address(this), ethIn); | ||
uint valueAfter = weth.balanceOf(address(usm)); | ||
|
||
// The asserts are what we are testing. A failing assert will be reported. | ||
assert(valueBefore + ethIn == valueAfter); // The value in eth of the USM supply increased by as much as the eth that went in | ||
} | ||
|
||
/// @dev Test that USM.sol returns eth when burning. | ||
/// Any function that is public will be run as a test, with random values assigned to each parameter | ||
function testBurnEthValue(uint usmOut) public { // To exclude a function from testing, make it internal | ||
// A failing require aborts this test instance without failing the fuzzing | ||
require(usmOut >= 10**14); // I'm restricting tests to a range of inputs with this | ||
|
||
uint valueBefore = weth.balanceOf(address(usm)); | ||
uint ethOut = usm.burn(address(this), address(this), usmOut); | ||
uint valueAfter = weth.balanceOf(address(usm)); | ||
|
||
assert(valueBefore - ethOut == valueAfter); // The value in eth of the USM supply decreased by as much as the value in eth of the USM that was burnt | ||
} | ||
|
||
/// @dev Test that USM.sol takes eth when funding. | ||
/// Any function that is public will be run as a test, with random values assigned to each parameter | ||
function testFundEthValue(uint ethIn) public { // To exclude a function from testing, make it internal | ||
require(ethIn >= 10**14); // 10**14 + 1 fails the last assertion | ||
|
||
weth.mint(ethIn); | ||
|
||
uint valueBefore = weth.balanceOf(address(usm)); | ||
usm.fund(address(this), address(this), ethIn); | ||
uint valueAfter = weth.balanceOf(address(usm)); | ||
|
||
assert(valueBefore + ethIn <= valueAfter); // The value in eth of the FUM supply increased by as much as the eth that went in | ||
} | ||
|
||
/// @dev Test that USM.sol returns eth when defunding. | ||
/// Any function that is public will be run as a test, with random values assigned to each parameter | ||
function testDefundEthValue(uint fumOut) public { // To exclude a function from testing, make it internal | ||
require(fumOut >= 10**14); // 10**14 + 1 fails the last assertion | ||
|
||
uint valueBefore = weth.balanceOf(address(usm)); | ||
uint ethOut = usm.defund(address(this), address(this), fumOut); | ||
uint valueAfter = weth.balanceOf(address(usm)); | ||
|
||
assert(valueBefore - ethOut == valueAfter); // The value in eth of the FUM supply decreased by as much as the value in eth of the FUM that was burnt | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,56 @@ | ||
// SPDX-License-Identifier: GPL-3.0-or-later | ||
pragma solidity ^0.6.7; | ||
import "../IUSM.sol"; | ||
import "../USM.sol"; | ||
import "../FUM.sol"; | ||
import "../oracles/TestOracle.sol"; | ||
import "../mocks/MockWETH9.sol"; | ||
import "../WadMath.sol"; | ||
import "@nomiclabs/buidler/console.sol"; | ||
|
||
contract USMFuzzingRoundtrip { | ||
using WadMath for uint; | ||
|
||
USM internal usm; | ||
FUM internal fum; | ||
MockWETH9 internal weth; | ||
TestOracle internal oracle; | ||
|
||
constructor() public { | ||
weth = new MockWETH9(); | ||
oracle = new TestOracle(25000000000, 8); | ||
usm = new USM(address(oracle), address(weth)); | ||
fum = FUM(usm.fum()); | ||
|
||
weth.approve(address(usm), uint(-1)); | ||
usm.approve(address(usm), uint(-1)); | ||
fum.approve(address(usm), uint(-1)); | ||
} | ||
|
||
/// @dev Test minting USM increases the value of the system by the same amount as Eth provided, and that burning does the inverse. | ||
/// Any function that is public will be run as a test, with random values assigned to each parameter | ||
function testMintAndBurnEthValue(uint ethIn) public { // To exclude a function from testing, make it internal | ||
weth.mint(ethIn); | ||
|
||
uint usmOut = usm.mint(address(this), address(this), ethIn); | ||
uint ethOut = usm.burn(address(this), address(this), usmOut); | ||
|
||
assert(ethIn >= ethOut); | ||
} | ||
|
||
/// @dev Test minting USM increases the value of the system by the same amount as Eth provided, and that burning does the inverse. | ||
/// Any function that is public will be run as a test, with random values assigned to each parameter | ||
function testFundAndDefundEthValue(uint ethIn) public { // To exclude a function from testing, make it internal | ||
weth.mint(ethIn); | ||
|
||
uint fumOut = usm.fund(address(this), address(this), ethIn); | ||
uint ethOut = usm.defund(address(this), address(this), fumOut); | ||
|
||
require(fum.totalSupply() > 0); // Edge case - Removing all FUM leaves ETH in USM that will be claimed by the next `fund()` | ||
|
||
assert(ethIn >= ethOut); | ||
} | ||
|
||
// Test that ethBuffer grows up with the fund/defund/mint/burn fee, plus minus eth for fund eth from defund | ||
// Test that with two consecutive ops, the second one gets a worse price | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,21 @@ | ||
// SPDX-License-Identifier: GPL-3.0-or-later | ||
pragma solidity ^0.6.7; | ||
import "../mocks/MockWETH9.sol"; | ||
import "@nomiclabs/buidler/console.sol"; | ||
|
||
contract WETH9Fuzzing { | ||
|
||
MockWETH9 internal weth; | ||
|
||
constructor () public { | ||
weth = new MockWETH9(); | ||
} | ||
|
||
function fuzzMint(uint ethAmount) public { | ||
uint supply = weth.totalSupply(); | ||
uint balance = weth.balanceOf(address(this)); | ||
weth.mint(ethAmount); | ||
assert(weth.totalSupply() == supply); // Since `mint` is a hack, t doesn't change the supply | ||
assert(weth.balanceOf(address(this)) == balance + ethAmount); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
seqLen: 50 | ||
testLimit: 20000 | ||
prefix: "crytic_" | ||
deployer: "0x41414141" | ||
sender: ["0x42424242", "0x43434343"] | ||
cryticArgs: ["--compile-force-framework", "Buidler"] | ||
coverage: true | ||
checkAsserts: true |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
// SPDX-License-Identifier: GPL-3.0-or-later | ||
pragma solidity ^0.6.7; | ||
|
||
import "../external/WETH9.sol"; | ||
|
||
|
||
contract MockWETH9 is WETH9 { | ||
|
||
function mint(uint amount) public { | ||
balanceOf[msg.sender] += amount; | ||
emit Deposit(msg.sender, amount); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.