diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml new file mode 100644 index 0000000..f003e8a --- /dev/null +++ b/.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 }} diff --git a/.github/workflows/tests.yaml b/.github/workflows/tests.yaml new file mode 100644 index 0000000..45744fe --- /dev/null +++ b/.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 }} diff --git a/.gitmodules b/.gitmodules index b3244d5..2fe14b5 100644 --- a/.gitmodules +++ b/.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 diff --git a/Makefile b/Makefile index 6e87dce..54f6b4d 100644 --- a/Makefile +++ b/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),) diff --git a/README.md b/README.md index e69de29..642bb70 100644 --- a/README.md +++ b/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. diff --git a/audit/20240904-ChainSecurity_MakerDAO_Sky_audit.pdf b/audit/20240904-ChainSecurity_MakerDAO_Sky_audit.pdf new file mode 100644 index 0000000..a582ad3 Binary files /dev/null and b/audit/20240904-ChainSecurity_MakerDAO_Sky_audit.pdf differ diff --git a/audit/20240904-ChainSecurity_MakerDAO_Sky_deployment_scripts_audit.pdf b/audit/20240904-ChainSecurity_MakerDAO_Sky_deployment_scripts_audit.pdf new file mode 100644 index 0000000..b836f98 Binary files /dev/null and b/audit/20240904-ChainSecurity_MakerDAO_Sky_deployment_scripts_audit.pdf differ diff --git a/audit/20240917-Sherlock_MakerDAO_Endgame_Audit_Report.pdf b/audit/20240917-Sherlock_MakerDAO_Endgame_Audit_Report.pdf new file mode 100644 index 0000000..a1c7bf9 Binary files /dev/null and b/audit/20240917-Sherlock_MakerDAO_Endgame_Audit_Report.pdf differ diff --git a/audit/cantina-report-review-makerdao-ngt.pdf b/audit/cantina-report-review-makerdao-ngt.pdf new file mode 100644 index 0000000..12d7359 Binary files /dev/null and b/audit/cantina-report-review-makerdao-ngt.pdf differ diff --git a/certora/Auxiliar.sol b/certora/Auxiliar.sol new file mode 100644 index 0000000..edb8a34 --- /dev/null +++ b/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; + } +} diff --git a/certora/MkrMock.sol b/certora/MkrMock.sol new file mode 100644 index 0000000..d94612d --- /dev/null +++ b/certora/MkrMock.sol @@ -0,0 +1,7 @@ +pragma solidity ^0.8.21; + +import "../src/Sky.sol"; + +contract MkrMock is Sky { + +} diff --git a/certora/MkrSky.conf b/certora/MkrSky.conf new file mode 100644 index 0000000..a4a1688 --- /dev/null +++ b/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" +} diff --git a/certora/MkrSky.spec b/certora/MkrSky.spec new file mode 100644 index 0000000..0e9ec0a --- /dev/null +++ b/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"; +} diff --git a/certora/SignerMock.sol b/certora/SignerMock.sol new file mode 100644 index 0000000..05ac0b6 --- /dev/null +++ b/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; + } +} diff --git a/certora/Sky.conf b/certora/Sky.conf new file mode 100644 index 0000000..9e10106 --- /dev/null +++ b/certora/Sky.conf @@ -0,0 +1,21 @@ +{ + "files": [ + "src/Sky.sol", + "certora/Auxiliar.sol", + "certora/SignerMock.sol" + ], + "rule_sanity": "basic", + "solc": "solc-0.8.21", + "solc_optimize_map": { + "Sky": "200", + "Auxiliar": "0", + "SignerMock": "0" + }, + "verify": "Sky:certora/Sky.spec", + "prover_args": [ + "-mediumTimeout 180" + ], + "optimistic_loop": true, + "multi_assert_check": true, + "wait_for_results": "all" +} diff --git a/certora/Sky.spec b/certora/Sky.spec new file mode 100644 index 0000000..ebc5e03 --- /dev/null +++ b/certora/Sky.spec @@ -0,0 +1,553 @@ +// Sky.spec + +using Auxiliar as aux; +using SignerMock as signer; + +methods { + function wards(address) external returns (uint256) envfree; + function name() external returns (string) envfree; + function symbol() external returns (string) envfree; + function version() external returns (string) envfree; + function decimals() external returns (uint8) envfree; + function totalSupply() external returns (uint256) envfree; + function balanceOf(address) external returns (uint256) envfree; + function allowance(address, address) external returns (uint256) envfree; + function nonces(address) external returns (uint256) envfree; + function deploymentChainId() external returns (uint256) envfree; + function DOMAIN_SEPARATOR() external returns (bytes32) envfree; + function PERMIT_TYPEHASH() external returns (bytes32) envfree; + function aux.call_ecrecover(bytes32, uint8, bytes32, bytes32) external returns (address) envfree; + function aux.computeDigestForToken(bytes32, bytes32, address, address, uint256, uint256, uint256) external returns (bytes32) envfree; + function aux.signatureToVRS(bytes) external returns (uint8, bytes32, bytes32) envfree; + function aux.VRSToSignature(uint8, bytes32, bytes32) external returns (bytes) envfree; + function aux.size(bytes) external returns (uint256) envfree; + function _.isValidSignature(bytes32, bytes) external => DISPATCHER(true); +} + +ghost balanceSum() returns mathint { + init_state axiom balanceSum() == 0; +} + +hook Sstore balanceOf[KEY address a] uint256 balance (uint256 old_balance) { + havoc balanceSum assuming balanceSum@new() == balanceSum@old() + balance - old_balance && balanceSum@new() >= 0; +} + +invariant balanceSum_equals_totalSupply() balanceSum() == to_mathint(totalSupply()); + +// Verify correct storage changes for non reverting rely +rule rely(address usr) { + env e; + + address other; + require other != usr; + address anyUsr; address anyUsr2; + + mathint wardsOtherBefore = wards(other); + mathint totalSupplyBefore = totalSupply(); + mathint balanceOfBefore = balanceOf(anyUsr); + mathint allowanceBefore = allowance(anyUsr, anyUsr2); + mathint noncesBefore = nonces(anyUsr); + + rely(e, usr); + + mathint wardsUsrAfter = wards(usr); + mathint wardsOtherAfter = wards(other); + mathint totalSupplyAfter = totalSupply(); + mathint balanceOfAfter = balanceOf(anyUsr); + mathint allowanceAfter = allowance(anyUsr, anyUsr2); + mathint noncesAfter = nonces(anyUsr); + + assert wardsUsrAfter == 1, "rely did not set the wards"; + assert wardsOtherAfter == wardsOtherBefore, "rely did not keep unchanged the rest of wards[x]"; + assert totalSupplyAfter == totalSupplyBefore, "rely did not keep unchanged totalSupply"; + assert balanceOfAfter == balanceOfBefore, "rely did not keep unchanged every balanceOf[x]"; + assert allowanceAfter == allowanceBefore, "rely did not keep unchanged every allowance[x][y]"; + assert noncesAfter == noncesBefore, "rely did not keep unchanged every nonces[x]"; +} + +// Verify revert rules on rely +rule rely_revert(address usr) { + env e; + + mathint wardsSender = wards(e.msg.sender); + + rely@withrevert(e, usr); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + + assert revert1 => lastReverted, "revert1 failed"; + assert revert2 => lastReverted, "revert2 failed"; + assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases"; +} + +// Verify correct storage changes for non reverting deny +rule deny(address usr) { + env e; + + address other; + require other != usr; + address anyUsr; address anyUsr2; + + mathint wardsOtherBefore = wards(other); + mathint totalSupplyBefore = totalSupply(); + mathint balanceOfBefore = balanceOf(anyUsr); + mathint allowanceBefore = allowance(anyUsr, anyUsr2); + mathint noncesBefore = nonces(anyUsr); + + deny(e, usr); + + mathint wardsUsrAfter = wards(usr); + mathint wardsOtherAfter = wards(other); + mathint totalSupplyAfter = totalSupply(); + mathint balanceOfAfter = balanceOf(anyUsr); + mathint allowanceAfter = allowance(anyUsr, anyUsr2); + mathint noncesAfter = nonces(anyUsr); + + assert wardsUsrAfter == 0, "deny did not set the wards"; + assert wardsOtherAfter == wardsOtherBefore, "deny did not keep unchanged the rest of wards[x]"; + assert totalSupplyAfter == totalSupplyBefore, "deny did not keep unchanged totalSupply"; + assert balanceOfAfter == balanceOfBefore, "deny did not keep unchanged every balanceOf[x]"; + assert allowanceAfter == allowanceBefore, "deny did not keep unchanged every allowance[x][y]"; + assert noncesAfter == noncesBefore, "deny did not keep unchanged every nonces[x]"; +} + +// Verify revert rules on deny +rule deny_revert(address usr) { + env e; + + mathint wardsSender = wards(e.msg.sender); + + deny@withrevert(e, usr); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + + assert revert1 => lastReverted, "revert1 failed"; + assert revert2 => lastReverted, "revert2 failed"; + assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases"; +} + +// Verify correct storage changes for non reverting transfer +rule transfer(address to, uint256 value) { + env e; + + requireInvariant balanceSum_equals_totalSupply(); + + address other; + require other != e.msg.sender && other != to; + address anyUsr; address anyUsr2; + + mathint wardsBefore = wards(anyUsr); + mathint totalSupplyBefore = totalSupply(); + mathint balanceOfSenderBefore = balanceOf(e.msg.sender); + mathint balanceOfToBefore = balanceOf(to); + mathint balanceOfOtherBefore = balanceOf(other); + mathint allowanceBefore = allowance(anyUsr, anyUsr2); + mathint noncesBefore = nonces(anyUsr); + + transfer(e, to, value); + + mathint wardsAfter = wards(anyUsr); + mathint totalSupplyAfter = totalSupply(); + mathint balanceOfSenderAfter = balanceOf(e.msg.sender); + mathint balanceOfToAfter = balanceOf(to); + mathint balanceOfOtherAfter = balanceOf(other); + mathint allowanceAfter = allowance(anyUsr, anyUsr2); + mathint noncesAfter = nonces(anyUsr); + + assert wardsAfter == wardsBefore, "transfer did not keep unchanged wards"; + assert totalSupplyAfter == totalSupplyBefore, "transfer did not keep unchanged totalSupply"; + assert e.msg.sender != to => balanceOfSenderAfter == balanceOfSenderBefore - value, "transfer did not decrease balanceOf[sender] by value"; + assert e.msg.sender != to => balanceOfToAfter == balanceOfToBefore + value, "transfer did not increase balanceOf[to] by value"; + assert e.msg.sender == to => balanceOfSenderAfter == balanceOfSenderBefore, "transfer did not keep unchanged balanceOf[sender == to]"; + assert balanceOfOtherAfter == balanceOfOtherBefore, "transfer did not keep unchanged the rest of balanceOf[x]"; + assert allowanceAfter == allowanceBefore, "transfer did not keep unchanged every allowance[x][y]"; + assert noncesAfter == noncesBefore, "transfer did not keep unchanged every nonces[x]"; +} + +// Verify revert rules on transfer +rule transfer_revert(address to, uint256 value) { + env e; + + mathint balanceOfSender = balanceOf(e.msg.sender); + + transfer@withrevert(e, to, value); + + bool revert1 = e.msg.value > 0; + bool revert2 = to == 0 || to == currentContract; + bool revert3 = balanceOfSender < to_mathint(value); + + assert revert1 => lastReverted, "revert1 failed"; + assert revert2 => lastReverted, "revert2 failed"; + assert revert3 => lastReverted, "revert3 failed"; + assert lastReverted => revert1 || revert2 || revert3, "Revert rules are not covering all the cases"; +} + +// Verify correct storage changes for non reverting transferFrom +rule transferFrom(address from, address to, uint256 value) { + env e; + + requireInvariant balanceSum_equals_totalSupply(); + + address other; + require other != from && other != to; + address other2; address other3; + require other2 != from || other3 != e.msg.sender; + address anyUsr; address anyUsr2; + + mathint wardsBefore = wards(anyUsr); + mathint totalSupplyBefore = totalSupply(); + mathint balanceOfFromBefore = balanceOf(from); + mathint balanceOfToBefore = balanceOf(to); + mathint balanceOfOtherBefore = balanceOf(other); + mathint allowanceFromSenderBefore = allowance(from, e.msg.sender); + mathint allowanceOtherBefore = allowance(other2, other3); + mathint noncesBefore = nonces(anyUsr); + + transferFrom(e, from, to, value); + + mathint wardsAfter = wards(anyUsr); + mathint totalSupplyAfter = totalSupply(); + mathint balanceOfFromAfter = balanceOf(from); + mathint balanceOfToAfter = balanceOf(to); + mathint balanceOfOtherAfter = balanceOf(other); + mathint allowanceFromSenderAfter = allowance(from, e.msg.sender); + mathint allowanceOtherAfter = allowance(other2, other3); + mathint noncesAfter = nonces(anyUsr); + + assert wardsAfter == wardsBefore, "transferFrom did not keep unchanged wards"; + assert totalSupplyAfter == totalSupplyBefore, "transferFrom did not keep unchanged totalSupply"; + assert from != to => balanceOfFromAfter == balanceOfFromBefore - value, "transferFrom did not decrease balanceOf[from] by value"; + assert from != to => balanceOfToAfter == balanceOfToBefore + value, "transferFrom did not increase balanceOf[to] by value"; + assert from == to => balanceOfFromAfter == balanceOfFromBefore, "transferFrom did not keep unchanged balanceOf[from == to]"; + assert balanceOfOtherAfter == balanceOfOtherBefore, "transferFrom did not keep unchanged the rest of balanceOf[x]"; + assert e.msg.sender != from && allowanceFromSenderBefore != max_uint256 => allowanceFromSenderAfter == allowanceFromSenderBefore - value, "transferFrom did not decrease allowance[from][sender] by value"; + assert e.msg.sender == from => allowanceFromSenderAfter == allowanceFromSenderBefore, "transferFrom did not keep unchanged allowance[from][sender] when from == sender"; + assert allowanceFromSenderBefore == max_uint256 => allowanceFromSenderAfter == allowanceFromSenderBefore, "transferFrom did not keep unchanged allowance[from][sender] when is max_uint256"; + assert allowanceOtherAfter == allowanceOtherBefore, "transferFrom did not keep unchanged the rest of allowance[x][y]"; + assert noncesAfter == noncesBefore, "transferFrom did not keep unchanged every nonces[x]"; +} + +// Verify revert rules on transferFrom +rule transferFrom_revert(address from, address to, uint256 value) { + env e; + + mathint balanceOfFrom = balanceOf(from); + mathint allowanceFromSender = allowance(from, e.msg.sender); + + transferFrom@withrevert(e, from, to, value); + + bool revert1 = e.msg.value > 0; + bool revert2 = to == 0 || to == currentContract; + bool revert3 = balanceOfFrom < to_mathint(value); + bool revert4 = allowanceFromSender < to_mathint(value) && e.msg.sender != from; + + assert revert1 => lastReverted, "revert1 failed"; + assert revert2 => lastReverted, "revert2 failed"; + assert revert3 => lastReverted, "revert3 failed"; + assert revert4 => lastReverted, "revert4 failed"; + assert lastReverted => revert1 || revert2 || revert3 || revert4, "Revert rules are not covering all the cases"; +} + +// Verify correct storage changes for non reverting approve +rule approve(address spender, uint256 value) { + env e; + + address anyUsr; + address anyUsr2; address anyUsr3; + require anyUsr2 != e.msg.sender || anyUsr3 != spender; + + mathint wardsBefore = wards(anyUsr); + mathint totalSupplyBefore = totalSupply(); + mathint balanceOfBefore = balanceOf(anyUsr); + mathint allowanceOtherBefore = allowance(anyUsr2, anyUsr3); + mathint noncesBefore = nonces(anyUsr); + + approve(e, spender, value); + + mathint wardsAfter = wards(anyUsr); + mathint totalSupplyAfter = totalSupply(); + mathint balanceOfAfter = balanceOf(anyUsr); + mathint allowanceSenderSpenderAfter = allowance(e.msg.sender, spender); + mathint allowanceOtherAfter = allowance(anyUsr2, anyUsr3); + mathint noncesAfter = nonces(anyUsr); + + assert wardsAfter == wardsBefore, "approve did not keep unchanged wards"; + assert totalSupplyAfter == totalSupplyBefore, "approve did not keep unchanged totalSupply"; + assert balanceOfAfter == balanceOfBefore, "approve did not keep unchanged every balanceOf[x]"; + assert allowanceSenderSpenderAfter == to_mathint(value), "approve did not set allowance[sender][spender] to value"; + assert allowanceOtherAfter == allowanceOtherBefore, "approve did not keep unchanged the rest of allowance[x][y]"; + assert noncesAfter == noncesBefore, "approve did not keep unchanged every nonces[x]"; +} + +// Verify revert rules on approve +rule approve_revert(address spender, uint256 value) { + env e; + + approve@withrevert(e, spender, value); + + bool revert1 = e.msg.value > 0; + + assert revert1 => lastReverted, "revert1 failed"; + assert lastReverted => revert1, "Revert rules are not covering all the cases"; +} + +// Verify correct storage changes for non reverting mint +rule mint(address to, uint256 value) { + env e; + + requireInvariant balanceSum_equals_totalSupply(); + + address other; + require other != to; + address anyUsr; address anyUsr2; + + bool senderSameAsTo = e.msg.sender == to; + + mathint wardsBefore = wards(anyUsr); + mathint totalSupplyBefore = totalSupply(); + mathint balanceOfToBefore = balanceOf(to); + mathint balanceOfOtherBefore = balanceOf(other); + mathint allowanceBefore = allowance(anyUsr, anyUsr2); + mathint noncesBefore = nonces(anyUsr); + + mint(e, to, value); + + mathint wardsAfter = wards(anyUsr); + mathint totalSupplyAfter = totalSupply(); + mathint balanceOfToAfter = balanceOf(to); + mathint balanceOfOtherAfter = balanceOf(other); + mathint allowanceAfter = allowance(anyUsr, anyUsr2); + mathint noncesAfter = nonces(anyUsr); + + assert wardsAfter == wardsBefore, "mint did not keep unchanged wards"; + assert totalSupplyAfter == totalSupplyBefore + value, "mint did not increase totalSupply by value"; + assert balanceOfToAfter == balanceOfToBefore + value, "mint did not increase balanceOf[to] by value"; + assert balanceOfOtherAfter == balanceOfOtherBefore, "mint did not keep unchanged the rest of balanceOf[x]"; + assert allowanceAfter == allowanceBefore, "mint did not keep unchanged every allowance[x][y]"; + assert noncesAfter == noncesBefore, "mint did not keep unchanged every nonces[x]"; +} + +// Verify revert rules on mint +rule mint_revert(address to, uint256 value) { + env e; + + // Save the totalSupply and sender balance before minting + mathint totalSupply = totalSupply(); + mathint wardsSender = wards(e.msg.sender); + + mint@withrevert(e, to, value); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + bool revert3 = totalSupply + value > max_uint256; + bool revert4 = to == 0 || to == currentContract; + + assert revert1 => lastReverted, "revert1 failed"; + assert revert2 => lastReverted, "revert2 failed"; + assert revert3 => lastReverted, "revert3 failed"; + assert revert4 => lastReverted, "revert4 failed"; + assert lastReverted => revert1 || revert2 || revert3 || revert4, "Revert rules are not covering all the cases"; +} + +// Verify correct storage changes for non reverting burn +rule burn(address from, uint256 value) { + env e; + + requireInvariant balanceSum_equals_totalSupply(); + + address other; + require other != from; + address anyUsr; address anyUsr2; + require anyUsr != from || anyUsr2 != e.msg.sender; + + mathint wardsBefore = wards(anyUsr); + mathint totalSupplyBefore = totalSupply(); + mathint balanceOfFromBefore = balanceOf(from); + mathint balanceOfOtherBefore = balanceOf(other); + mathint allowanceFromSenderBefore = allowance(from, e.msg.sender); + mathint allowanceOtherBefore = allowance(anyUsr, anyUsr2); + mathint noncesBefore = nonces(anyUsr); + + burn(e, from, value); + + mathint wardsAfter = wards(anyUsr); + mathint totalSupplyAfter = totalSupply(); + mathint balanceOfSenderAfter = balanceOf(e.msg.sender); + mathint balanceOfFromAfter = balanceOf(from); + mathint balanceOfOtherAfter = balanceOf(other); + mathint allowanceFromSenderAfter = allowance(from, e.msg.sender); + mathint allowanceOtherAfter = allowance(anyUsr, anyUsr2); + mathint noncesAfter = nonces(anyUsr); + + assert wardsAfter == wardsBefore, "burn did not keep unchanged wards"; + assert totalSupplyAfter == totalSupplyBefore - value, "burn did not decrease totalSupply by value"; + assert balanceOfFromAfter == balanceOfFromBefore - value, "burn did not decrease balanceOf[from] by value"; + assert balanceOfOtherAfter == balanceOfOtherBefore, "burn did not keep unchanged the rest of balanceOf[x]"; + assert e.msg.sender != from && allowanceFromSenderBefore != max_uint256 => allowanceFromSenderAfter == allowanceFromSenderBefore - value, "burn did not decrease allowance[from][sender] by value"; + assert e.msg.sender == from => allowanceFromSenderAfter == allowanceFromSenderBefore, "burn did not keep unchanged allowance[from][sender] when from == sender"; + assert allowanceFromSenderBefore == max_uint256 => allowanceFromSenderAfter == allowanceFromSenderBefore, "burn did not keep unchanged allowance[from][sender] when is max_uint256"; + assert allowanceOtherAfter == allowanceOtherBefore, "burn did not keep unchanged the rest of allowance[x][y]"; + assert noncesAfter == noncesBefore, "burn did not keep unchanged every nonces[x]"; +} + +// Verify revert rules on burn +rule burn_revert(address from, uint256 value) { + env e; + + mathint balanceOfFrom = balanceOf(from); + mathint allowanceFromSender = allowance(from, e.msg.sender); + + burn@withrevert(e, from, value); + + bool revert1 = e.msg.value > 0; + bool revert2 = balanceOfFrom < to_mathint(value); + bool revert3 = from != e.msg.sender && allowanceFromSender < to_mathint(value); + + assert revert1 => lastReverted, "revert1 failed"; + assert revert2 => lastReverted, "revert2 failed"; + assert revert3 => lastReverted, "revert3 failed"; + assert lastReverted => revert1 || revert2 || revert3, "Revert rules are not covering all the cases"; +} + +// Verify correct storage changes for non reverting permit +rule permitVRS(address owner, address spender, uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s) { + env e; + + address anyUsr; + address anyUsr2; address anyUsr3; + require anyUsr2 != owner || anyUsr3 != spender; + address other; + require other != owner; + + mathint wardsBefore = wards(anyUsr); + mathint totalSupplyBefore = totalSupply(); + mathint balanceOfBefore = balanceOf(anyUsr); + mathint allowanceOtherBefore = allowance(anyUsr2, anyUsr3); + mathint noncesOwnerBefore = nonces(owner); + mathint noncesOtherBefore = nonces(other); + + permit(e, owner, spender, value, deadline, v, r, s); + + mathint wardsAfter = wards(anyUsr); + mathint totalSupplyAfter = totalSupply(); + mathint balanceOfAfter = balanceOf(anyUsr); + mathint allowanceOwnerSpenderAfter = allowance(owner, spender); + mathint allowanceOtherAfter = allowance(anyUsr2, anyUsr3); + mathint noncesOwnerAfter = nonces(owner); + mathint noncesOtherAfter = nonces(other); + + assert wardsAfter == wardsBefore, "permit did not keep unchanged wards"; + assert totalSupplyAfter == totalSupplyBefore, "permit did not keep unchanged totalSupply"; + assert balanceOfAfter == balanceOfBefore, "permit did not keep unchanged every balanceOf[x]"; + assert allowanceOwnerSpenderAfter == to_mathint(value), "permit did not set allowance[owner][spender] to value"; + assert allowanceOtherAfter == allowanceOtherBefore, "permit did not keep unchanged the rest of allowance[x][y]"; + assert noncesOwnerBefore < max_uint256 => noncesOwnerAfter == noncesOwnerBefore + 1, "permit did not increase nonces[owner] by 1"; + assert noncesOwnerBefore == max_uint256 => noncesOwnerAfter == 0, "permit did not set nonces[owner] back to 0"; + assert noncesOtherAfter == noncesOtherBefore, "permit did not keep unchanged the rest of nonces[x]"; +} + +// Verify revert rules on permit +rule permitVRS_revert(address owner, address spender, uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s) { + env e; + + bytes32 digest = aux.computeDigestForToken( + DOMAIN_SEPARATOR(), + PERMIT_TYPEHASH(), + owner, + spender, + value, + nonces(owner), + deadline + ); + address ownerRecover = aux.call_ecrecover(digest, v, r, s); + bytes32 returnedSig = owner == signer ? signer.isValidSignature(e, digest, aux.VRSToSignature(v, r, s)) : to_bytes32(0); + + permit@withrevert(e, owner, spender, value, deadline, v, r, s); + + bool revert1 = e.msg.value > 0; + bool revert2 = e.block.timestamp > deadline; + bool revert3 = owner == 0; + bool revert4 = owner != ownerRecover && returnedSig != to_bytes32(0x1626ba7e00000000000000000000000000000000000000000000000000000000); + + assert revert1 => lastReverted, "revert1 failed"; + assert revert2 => lastReverted, "revert2 failed"; + assert revert3 => lastReverted, "revert3 failed"; + assert revert4 => lastReverted, "revert4 failed"; + + assert lastReverted => revert1 || revert2 || revert3 || + revert4, "Revert rules are not covering all the cases"; +} + +// Verify correct storage changes for non reverting permit +rule permitSignature(address owner, address spender, uint256 value, uint256 deadline, bytes signature) { + env e; + + address anyUsr; + address anyUsr2; address anyUsr3; + require anyUsr2 != owner || anyUsr3 != spender; + address other; + require other != owner; + + mathint wardsBefore = wards(anyUsr); + mathint totalSupplyBefore = totalSupply(); + mathint balanceOfBefore = balanceOf(anyUsr); + mathint allowanceOtherBefore = allowance(anyUsr2, anyUsr3); + mathint noncesOwnerBefore = nonces(owner); + mathint noncesOtherBefore = nonces(other); + + permit(e, owner, spender, value, deadline, signature); + + mathint wardsAfter = wards(anyUsr); + mathint totalSupplyAfter = totalSupply(); + mathint balanceOfAfter = balanceOf(anyUsr); + mathint allowanceOwnerSpenderAfter = allowance(owner, spender); + mathint allowanceOtherAfter = allowance(anyUsr2, anyUsr3); + mathint noncesOwnerAfter = nonces(owner); + mathint noncesOtherAfter = nonces(other); + + assert wardsAfter == wardsBefore, "permit did not keep unchanged wards"; + assert totalSupplyAfter == totalSupplyBefore, "permit did not keep unchanged totalSupply"; + assert balanceOfAfter == balanceOfBefore, "permit did not keep unchanged every balanceOf[x]"; + assert allowanceOwnerSpenderAfter == to_mathint(value), "permit did not set allowance[owner][spender] to value"; + assert allowanceOtherAfter == allowanceOtherBefore, "permit did not keep unchanged the rest of allowance[x][y]"; + assert noncesOwnerBefore < max_uint256 => noncesOwnerAfter == noncesOwnerBefore + 1, "permit did not increase nonces[owner] by 1"; + assert noncesOwnerBefore == max_uint256 => noncesOwnerAfter == 0, "permit did not set nonces[owner] back to 0"; + assert noncesOtherAfter == noncesOtherBefore, "permit did not keep unchanged the rest of nonces[x]"; +} + +// Verify revert rules on permit +rule permitSignature_revert(address owner, address spender, uint256 value, uint256 deadline, bytes signature) { + env e; + + bytes32 digest = aux.computeDigestForToken( + DOMAIN_SEPARATOR(), + PERMIT_TYPEHASH(), + owner, + spender, + value, + nonces(owner), + deadline + ); + uint8 v; bytes32 r; bytes32 s; + v, r, s = aux.signatureToVRS(signature); + address null_address = 0; + address ownerRecover = aux.size(signature) == 65 ? aux.call_ecrecover(digest, v, r, s) : null_address; + bytes32 returnedSig = owner == signer ? signer.isValidSignature(e, digest, signature) : to_bytes32(0); + + permit@withrevert(e, owner, spender, value, deadline, signature); + + bool revert1 = e.msg.value > 0; + bool revert2 = e.block.timestamp > deadline; + bool revert3 = owner == 0; + bool revert4 = owner != ownerRecover && returnedSig != to_bytes32(0x1626ba7e00000000000000000000000000000000000000000000000000000000); + + assert revert1 => lastReverted, "revert1 failed"; + assert revert2 => lastReverted, "revert2 failed"; + assert revert3 => lastReverted, "revert3 failed"; + assert revert4 => lastReverted, "revert4 failed"; + + assert lastReverted => revert1 || revert2 || revert3 || + revert4, "Revert rules are not covering all the cases"; +} diff --git a/deploy/SkyDeploy.sol b/deploy/SkyDeploy.sol new file mode 100644 index 0000000..c66506e --- /dev/null +++ b/deploy/SkyDeploy.sol @@ -0,0 +1,41 @@ +// SPDX-FileCopyrightText: © 2023 Dai Foundation +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// 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.8.21; + +import { ScriptTools } from "dss-test/ScriptTools.sol"; + +import { Sky } from "src/Sky.sol"; +import { MkrSky } from "src/MkrSky.sol"; + +import { SkyInstance } from "./SkyInstance.sol"; + +library SkyDeploy { + function deploy( + address deployer, + address owner, + address mkr, + uint256 rate + ) internal returns (SkyInstance memory instance) { + address _sky = address(new Sky()); + ScriptTools.switchOwner(_sky, deployer, owner); + + address _mkrSky = address(new MkrSky(mkr, _sky, rate)); + + instance.sky = _sky; + instance.mkrSky = _mkrSky; + } +} diff --git a/deploy/SkyInit.sol b/deploy/SkyInit.sol new file mode 100644 index 0000000..90dae83 --- /dev/null +++ b/deploy/SkyInit.sol @@ -0,0 +1,57 @@ +// SPDX-FileCopyrightText: © 2023 Dai Foundation +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// 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.8.0; + +import { DssInstance } from "dss-test/MCD.sol"; +import { SkyInstance } from "./SkyInstance.sol"; + +interface SkyLike { + function rely(address) external; +} + +interface MkrSkyLike { + function mkr() external view returns (address); + function sky() external view returns (address); + function rate() external view returns (uint256); +} + +interface MkrLike { + function authority() external view returns (address); +} + +interface MkrAuthorityLike { + function rely(address) external; +} + +library SkyInit { + function init( + DssInstance memory dss, + SkyInstance memory instance, + uint256 rate + ) internal { + address mkr = dss.chainlog.getAddress("MCD_GOV"); + require(MkrSkyLike(instance.mkrSky).mkr() == mkr, "SkyInit/mkr-does-not-match"); + require(MkrSkyLike(instance.mkrSky).sky() == instance.sky, "SkyInit/sky-does-not-match"); + require(MkrSkyLike(instance.mkrSky).rate() == rate, "SkyInit/rate-does-not-match"); + + SkyLike(instance.sky).rely(instance.mkrSky); + MkrAuthorityLike(MkrLike(mkr).authority()).rely(instance.mkrSky); + + dss.chainlog.setAddress("SKY", instance.sky); + dss.chainlog.setAddress("MKR_SKY", instance.mkrSky); + } +} diff --git a/deploy/SkyInstance.sol b/deploy/SkyInstance.sol new file mode 100644 index 0000000..b724cde --- /dev/null +++ b/deploy/SkyInstance.sol @@ -0,0 +1,22 @@ +// SPDX-FileCopyrightText: © 2023 Dai Foundation +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// 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.8.0; + +struct SkyInstance { + address sky; + address mkrSky; +} diff --git a/foundry.toml b/foundry.toml new file mode 100644 index 0000000..a88dbe9 --- /dev/null +++ b/foundry.toml @@ -0,0 +1,10 @@ +[profile.default] +src = "src" +out = "out" +libs = ["lib"] +solc = "0.8.21" +optimizer = true +optimizer_runs = 200 +verbosity = 3 + +# See more config options https://github.com/foundry-rs/foundry/tree/master/config diff --git a/lib/dss-test b/lib/dss-test deleted file mode 160000 index 7529fa1..0000000 --- a/lib/dss-test +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 7529fa1e043b9195f41549852d9c5bb0714eaa27 diff --git a/lib/token-tests b/lib/token-tests new file mode 160000 index 0000000..6bdd5a3 --- /dev/null +++ b/lib/token-tests @@ -0,0 +1 @@ +Subproject commit 6bdd5a38586970acf27166c3205093fd3450d530 diff --git a/src/MkrSky.sol b/src/MkrSky.sol new file mode 100644 index 0000000..3cb27d8 --- /dev/null +++ b/src/MkrSky.sol @@ -0,0 +1,54 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +/// MkrSky.sol -- Mkr/Sky Exchanger + +// Copyright (C) 2023 Dai Foundation +// +// 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.8.21; + +interface GemLike { + function burn(address, uint256) external; + function mint(address, uint256) external; +} + +contract MkrSky { + GemLike public immutable mkr; + GemLike public immutable sky; + uint256 public immutable rate; + + event MkrToSky(address indexed caller, address indexed usr, uint256 mkrAmt, uint256 skyAmt); + event SkyToMkr(address indexed caller, address indexed usr, uint256 skyAmt, uint256 mkrAmt); + + constructor(address mkr_, address sky_, uint256 rate_) { + mkr = GemLike(mkr_); + sky = GemLike(sky_); + rate = rate_; + } + + function mkrToSky(address usr, uint256 mkrAmt) external { + mkr.burn(msg.sender, mkrAmt); + uint256 skyAmt = mkrAmt * rate; + sky.mint(usr, skyAmt); + emit MkrToSky(msg.sender, usr, mkrAmt, skyAmt); + } + + function skyToMkr(address usr, uint256 skyAmt) external { + sky.burn(msg.sender, skyAmt); + uint256 mkrAmt = skyAmt / rate; // Rounding down, dust will be lost if it is not multiple of rate + mkr.mint(usr, mkrAmt); + emit SkyToMkr(msg.sender, usr, skyAmt, mkrAmt); + } +} diff --git a/src/Sky.sol b/src/Sky.sol new file mode 100644 index 0000000..4f405e4 --- /dev/null +++ b/src/Sky.sol @@ -0,0 +1,253 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +/// Sky.sol -- Sky token + +// Copyright (C) 2017, 2018, 2019 dbrock, rain, mrchico +// Copyright (C) 2023 Dai Foundation +// +// 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.8.21; + +interface IERC1271 { + function isValidSignature( + bytes32, + bytes memory + ) external view returns (bytes4); +} + +contract Sky { + mapping (address => uint256) public wards; + + // --- ERC20 Data --- + string public constant name = "SKY Governance Token"; + string public constant symbol = "SKY"; + string public constant version = "1"; + uint8 public constant decimals = 18; + uint256 public totalSupply; + + mapping (address => uint256) public balanceOf; + mapping (address => mapping (address => uint256)) public allowance; + mapping (address => uint256) public nonces; + + // --- Events --- + event Rely(address indexed usr); + event Deny(address indexed usr); + event Approval(address indexed owner, address indexed spender, uint256 value); + event Transfer(address indexed from, address indexed to, uint256 value); + + // --- EIP712 niceties --- + uint256 public immutable deploymentChainId; + bytes32 private immutable _DOMAIN_SEPARATOR; + bytes32 public constant PERMIT_TYPEHASH = keccak256("Permit(address owner,address spender,uint256 value,uint256 nonce,uint256 deadline)"); + + modifier auth { + require(wards[msg.sender] == 1, "Sky/not-authorized"); + _; + } + + constructor() { + wards[msg.sender] = 1; + emit Rely(msg.sender); + + deploymentChainId = block.chainid; + _DOMAIN_SEPARATOR = _calculateDomainSeparator(block.chainid); + } + + function _calculateDomainSeparator(uint256 chainId) private view returns (bytes32) { + return keccak256( + abi.encode( + keccak256("EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)"), + keccak256(bytes(name)), + keccak256(bytes(version)), + chainId, + address(this) + ) + ); + } + + function DOMAIN_SEPARATOR() external view returns (bytes32) { + return block.chainid == deploymentChainId ? _DOMAIN_SEPARATOR : _calculateDomainSeparator(block.chainid); + } + + // --- Administration --- + function rely(address usr) external auth { + wards[usr] = 1; + emit Rely(usr); + } + + function deny(address usr) external auth { + wards[usr] = 0; + emit Deny(usr); + } + + // --- ERC20 Mutations --- + function transfer(address to, uint256 value) external returns (bool) { + require(to != address(0) && to != address(this), "Sky/invalid-address"); + uint256 balance = balanceOf[msg.sender]; + require(balance >= value, "Sky/insufficient-balance"); + + unchecked { + balanceOf[msg.sender] = balance - value; + balanceOf[to] += value; // note: we don't need an overflow check here b/c sum of all balances == totalSupply + } + + emit Transfer(msg.sender, to, value); + + return true; + } + + function transferFrom(address from, address to, uint256 value) external returns (bool) { + require(to != address(0) && to != address(this), "Sky/invalid-address"); + uint256 balance = balanceOf[from]; + require(balance >= value, "Sky/insufficient-balance"); + + if (from != msg.sender) { + uint256 allowed = allowance[from][msg.sender]; + if (allowed != type(uint256).max) { + require(allowed >= value, "Sky/insufficient-allowance"); + + unchecked { + allowance[from][msg.sender] = allowed - value; + } + } + } + + unchecked { + balanceOf[from] = balance - value; + balanceOf[to] += value; // note: we don't need an overflow check here b/c sum of all balances == totalSupply + } + + emit Transfer(from, to, value); + + return true; + } + + function approve(address spender, uint256 value) external returns (bool) { + allowance[msg.sender][spender] = value; + + emit Approval(msg.sender, spender, value); + + return true; + } + + // --- Mint/Burn --- + function mint(address to, uint256 value) external auth { + require(to != address(0) && to != address(this), "Sky/invalid-address"); + unchecked { + balanceOf[to] = balanceOf[to] + value; // note: we don't need an overflow check here b/c balanceOf[to] <= totalSupply and there is an overflow check below + } + totalSupply = totalSupply + value; + + emit Transfer(address(0), to, value); + } + + function burn(address from, uint256 value) external { + uint256 balance = balanceOf[from]; + require(balance >= value, "Sky/insufficient-balance"); + + if (from != msg.sender) { + uint256 allowed = allowance[from][msg.sender]; + if (allowed != type(uint256).max) { + require(allowed >= value, "Sky/insufficient-allowance"); + + unchecked { + allowance[from][msg.sender] = allowed - value; + } + } + } + + unchecked { + balanceOf[from] = balance - value; // note: we don't need overflow checks b/c require(balance >= value) and balance <= totalSupply + totalSupply = totalSupply - value; + } + + emit Transfer(from, address(0), value); + } + + // --- Approve by signature --- + function _isValidSignature( + address signer, + bytes32 digest, + bytes memory signature + ) internal view returns (bool valid) { + if (signature.length == 65) { + bytes32 r; + bytes32 s; + uint8 v; + assembly { + r := mload(add(signature, 0x20)) + s := mload(add(signature, 0x40)) + v := byte(0, mload(add(signature, 0x60))) + } + if (signer == ecrecover(digest, v, r, s)) { + return true; + } + } + + if (signer.code.length > 0) { + (bool success, bytes memory result) = signer.staticcall( + abi.encodeCall(IERC1271.isValidSignature, (digest, signature)) + ); + valid = (success && + result.length == 32 && + abi.decode(result, (bytes4)) == IERC1271.isValidSignature.selector); + } + } + + function permit( + address owner, + address spender, + uint256 value, + uint256 deadline, + bytes memory signature + ) public { + require(block.timestamp <= deadline, "Sky/permit-expired"); + require(owner != address(0), "Sky/invalid-owner"); + + uint256 nonce; + unchecked { nonce = nonces[owner]++; } + + bytes32 digest = + keccak256(abi.encodePacked( + "\x19\x01", + block.chainid == deploymentChainId ? _DOMAIN_SEPARATOR : _calculateDomainSeparator(block.chainid), + keccak256(abi.encode( + PERMIT_TYPEHASH, + owner, + spender, + value, + nonce, + deadline + )) + )); + + require(_isValidSignature(owner, digest, signature), "Sky/invalid-permit"); + + allowance[owner][spender] = value; + emit Approval(owner, spender, value); + } + + function permit( + address owner, + address spender, + uint256 value, + uint256 deadline, + uint8 v, + bytes32 r, + bytes32 s + ) external { + permit(owner, spender, value, deadline, abi.encodePacked(r, s, v)); + } +} diff --git a/test/MkrSky.t.sol b/test/MkrSky.t.sol new file mode 100644 index 0000000..878b67b --- /dev/null +++ b/test/MkrSky.t.sol @@ -0,0 +1,92 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +pragma solidity ^0.8.21; + +import "dss-test/DssTest.sol"; + +import { Sky } from "src/Sky.sol"; +import { MkrSky } from "src/MkrSky.sol"; + +contract Mkr is Sky {} + +contract MkrSkyTest is DssTest { + Mkr mkr; + Sky sky; + MkrSky mkrSky; + + event MkrToSky(address indexed caller, address indexed usr, uint256 mkrAmt, uint256 skyAmt); + event SkyToMkr(address indexed caller, address indexed usr, uint256 skyAmt, uint256 mkrAmt); + + function setUp() public { + mkr = new Mkr(); + sky = new Sky(); + mkrSky = new MkrSky(address(mkr), address(sky), 1200); + mkr.mint(address(this), 1_000_000 * WAD); + mkr.rely(address(mkrSky)); + mkr.deny(address(this)); + sky.rely(address(mkrSky)); + sky.deny(address(this)); + } + + function testExchange() public { + assertEq(mkr.balanceOf(address(this)), 1_000_000 * WAD); + assertEq(mkr.totalSupply(), 1_000_000 * WAD); + assertEq(sky.balanceOf(address(this)), 0); + assertEq(sky.totalSupply(), 0); + + mkr.approve(address(mkrSky), 400_000 * WAD); + vm.expectEmit(true, true, true, true); + emit MkrToSky(address(this), address(this), 400_000 * WAD, 400_000 * WAD * 1200); + mkrSky.mkrToSky(address(this), 400_000 * WAD); + assertEq(mkr.balanceOf(address(this)), 600_000 * WAD); + assertEq(mkr.totalSupply(), 600_000 * WAD); + assertEq(sky.balanceOf(address(this)), 400_000 * WAD * 1200); + assertEq(sky.totalSupply(), 400_000 * WAD * 1200); + + sky.approve(address(mkrSky), 200_000 * WAD * 1200); + vm.expectEmit(true, true, true, true); + emit SkyToMkr(address(this), address(this), 200_000 * WAD * 1200, 200_000 * WAD); + mkrSky.skyToMkr(address(this), 200_000 * WAD * 1200); + assertEq(mkr.balanceOf(address(this)), 800_000 * WAD); + assertEq(mkr.totalSupply(), 800_000 * WAD); + assertEq(sky.balanceOf(address(this)), 200_000 * WAD * 1200); + assertEq(sky.totalSupply(), 200_000 * WAD * 1200); + + address receiver = address(123); + assertEq(mkr.balanceOf(receiver), 0); + assertEq(sky.balanceOf(receiver), 0); + + mkr.approve(address(mkrSky), 150_000 * WAD); + vm.expectEmit(true, true, true, true); + emit MkrToSky(address(this), receiver, 150_000 * WAD, 150_000 * WAD * 1200); + mkrSky.mkrToSky(receiver, 150_000 * WAD); + assertEq(mkr.balanceOf(address(this)), 650_000 * WAD); + assertEq(mkr.balanceOf(receiver), 0); + assertEq(mkr.totalSupply(), 650_000 * WAD); + assertEq(sky.balanceOf(address(this)), 200_000 * WAD * 1200); + assertEq(sky.balanceOf(receiver), 150_000 * WAD * 1200); + assertEq(sky.totalSupply(), 350_000 * WAD * 1200); + + sky.approve(address(mkrSky), 50_000 * WAD * 1200); + vm.expectEmit(true, true, true, true); + emit SkyToMkr(address(this), receiver, 50_000 * WAD * 1200, 50_000 * WAD); + mkrSky.skyToMkr(receiver, 50_000 * WAD * 1200); + assertEq(mkr.balanceOf(address(this)), 650_000 * WAD); + assertEq(mkr.balanceOf(receiver), 50_000 * WAD); + assertEq(mkr.totalSupply(), 700_000 * WAD); + assertEq(sky.balanceOf(address(this)), 150_000 * WAD * 1200); + assertEq(sky.balanceOf(receiver), 150_000 * WAD * 1200); + assertEq(sky.totalSupply(), 300_000 * WAD * 1200); + + sky.approve(address(mkrSky), 50_000 * WAD * 1200 + 1199); + vm.expectEmit(true, true, true, true); + emit SkyToMkr(address(this), address(this), 50_000 * WAD * 1200 + 1199, 50_000 * WAD); + mkrSky.skyToMkr(address(this), 50_000 * WAD * 1200 + 1199); + assertEq(mkr.balanceOf(address(this)), 700_000 * WAD); + assertEq(mkr.balanceOf(receiver), 50_000 * WAD); + assertEq(mkr.totalSupply(), 750_000 * WAD); + assertEq(sky.balanceOf(address(this)), 100_000 * WAD * 1200 - 1199); + assertEq(sky.balanceOf(receiver), 150_000 * WAD * 1200); + assertEq(sky.totalSupply(), 250_000 * WAD * 1200 - 1199); + } +} diff --git a/test/Sky.t.sol b/test/Sky.t.sol new file mode 100644 index 0000000..edb734b --- /dev/null +++ b/test/Sky.t.sol @@ -0,0 +1,29 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +pragma solidity ^0.8.21; + +import "token-tests/TokenFuzzTests.sol"; + +import { Sky } from "src/Sky.sol"; + +contract SkyTest is TokenFuzzTests { + Sky sky; + + function setUp() public { + vm.expectEmit(true, true, true, true); + emit Rely(address(this)); + sky = new Sky(); + + _token_ = address(sky); + _contractName_ = "Sky"; + _tokenName_ = "SKY Governance Token"; + _symbol_ = "SKY"; + } + + function invariantMetadata() public view { + assertEq(sky.name(), "SKY Governance Token"); + assertEq(sky.symbol(), "SKY"); + assertEq(sky.version(), "1"); + assertEq(sky.decimals(), 18); + } +} diff --git a/test/integration/Deployment.t.sol b/test/integration/Deployment.t.sol new file mode 100644 index 0000000..a141def --- /dev/null +++ b/test/integration/Deployment.t.sol @@ -0,0 +1,91 @@ +// SPDX-FileCopyrightText: © 2023 Dai Foundation +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// 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.8.21; + +import "dss-test/DssTest.sol"; + +import { SkyInstance } from "deploy/SkyInstance.sol"; +import { SkyDeploy } from "deploy/SkyDeploy.sol"; +import { SkyInit, MkrLike } from "deploy/SkyInit.sol"; + +import { Sky } from "src/Sky.sol"; +import { MkrSky } from "src/MkrSky.sol"; + +interface ChainlogLike { + function getAddress(bytes32) external view returns (address); +} + +interface MkrAuthorityLike { + function wards(address) external view returns (uint256); +} + +interface GemLike { + function balanceOf(address) external view returns (uint256); + function approve(address, uint256) external; +} + +contract DeploymentTest is DssTest { + address constant LOG = 0xdA0Ab1e0017DEbCd72Be8599041a2aa3bA7e740F; + + address PAUSE_PROXY; + address MKR; + + SkyInstance inst; + + function setUp() public { + vm.createSelectFork(vm.envString("ETH_RPC_URL")); + + PAUSE_PROXY = ChainlogLike(LOG).getAddress("MCD_PAUSE_PROXY"); + MKR = ChainlogLike(LOG).getAddress("MCD_GOV"); + + inst = SkyDeploy.deploy(address(this), PAUSE_PROXY, MKR, 1200); + } + + function testSetUp() public { + DssInstance memory dss = MCD.loadFromChainlog(LOG); + + assertEq(Sky(inst.sky).wards(inst.mkrSky), 0); + assertEq(MkrAuthorityLike(MkrLike(MKR).authority()).wards(inst.mkrSky), 0); + + vm.startPrank(PAUSE_PROXY); + SkyInit.init(dss, inst, 1200); + vm.stopPrank(); + + assertEq(Sky(inst.sky).wards(inst.mkrSky), 1); + assertEq(MkrAuthorityLike(MkrLike(MKR).authority()).wards(inst.mkrSky), 1); + + deal(MKR, address(this), 1000); + + assertEq(GemLike(MKR).balanceOf(address(this)), 1000); + assertEq(GemLike(inst.sky).balanceOf(address(this)), 0); + + GemLike(MKR).approve(inst.mkrSky, 600); + MkrSky(inst.mkrSky).mkrToSky(address(this), 600); + + assertEq(GemLike(MKR).balanceOf(address(this)), 400); + assertEq(GemLike(inst.sky).balanceOf(address(this)), 600 * 1200); + + GemLike(inst.sky).approve(inst.mkrSky, 400 * 1200); + MkrSky(inst.mkrSky).skyToMkr(address(this), 400 * 1200); + + assertEq(GemLike(MKR).balanceOf(address(this)), 800); + assertEq(GemLike(inst.sky).balanceOf(address(this)), 200 * 1200); + + assertEq(ChainlogLike(LOG).getAddress("SKY"), inst.sky); + assertEq(ChainlogLike(LOG).getAddress("MKR_SKY"), inst.mkrSky); + } +}