diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml new file mode 100644 index 0000000..da850d6 --- /dev/null +++ b/.github/workflows/certora.yml @@ -0,0 +1,46 @@ +name: Certora + +on: [push, pull_request] + +jobs: + certora: + name: Certora + runs-on: ubuntu-latest + strategy: + fail-fast: false + matrix: + alm-controller: + - rate-limits + - mainnet-controller + - foreign-controller + + steps: + - name: Checkout + uses: actions/checkout@v3 + with: + submodules: recursive + + - 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-beta + + - name: Verify ${{ matrix.alm-controller }} + run: make certora-${{ matrix.alm-controller }} results=1 + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..d35537f --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "spark-alm-controller"] + path = spark-alm-controller + url = https://github.com/marsfoundation/spark-alm-controller.git diff --git a/ForeignController.conf b/ForeignController.conf new file mode 100644 index 0000000..46727b6 --- /dev/null +++ b/ForeignController.conf @@ -0,0 +1,38 @@ +{ + "files": [ + "spark-alm-controller/src/ForeignController.sol", + "spark-alm-controller/src/ALMProxy.sol", + "harness/CctpMock.sol", + "harness/Psm3Mock.sol", + "spark-alm-controller/src/RateLimits.sol", + "harness/UsdcMock.sol", + "harness/UsdsMock.sol", + "harness/SUsdsMock.sol", + "harness/Auxiliar.sol" + ], + "solc": "solc-0.8.21", + "solc_optimize": "200", + "packages": [ + "forge-std/interfaces/=spark-alm-controller/lib/forge-std/src/interfaces", + "openzeppelin-contracts/=spark-alm-controller/lib/openzeppelin-contracts", + "lib/openzeppelin-contracts/=spark-alm-controller/lib/openzeppelin-contracts", + "spark-psm/src/interfaces/=spark-alm-controller/lib/spark-psm/src/interfaces", + "erc20-helpers/interfaces/=spark-alm-controller/lib/spark-psm/lib/erc20-helpers/src/interfaces", + "src=spark-alm-controller/src" + ], + "link": [ + "ForeignController:proxy=ALMProxy", + "ForeignController:cctp=CctpMock", + "ForeignController:psm=Psm3Mock", + "ForeignController:rateLimits=RateLimits", + "ForeignController:usdc=UsdcMock" + ], + "verify": "ForeignController:ForeignController.spec", + "rule_sanity": "basic", + "multi_assert_check": true, + "optimistic_loop": true, + "parametric_contracts": ["ForeignController"], + "smt_timeout": "7000", + "build_cache": true, + "msg": "ForeignController" +} diff --git a/ForeignController.spec b/ForeignController.spec new file mode 100644 index 0000000..44a1d5c --- /dev/null +++ b/ForeignController.spec @@ -0,0 +1,406 @@ +// ForeignController.spec + +using ALMProxy as proxy; +using CctpMock as cctp; +using Psm3Mock as psm; +using RateLimits as rateLimits; +using UsdcMock as usdc; +using UsdsMock as usds; +using SUsdsMock as sUsds; +using Auxiliar as aux; + +methods { + // storage variables + function active() external returns (bool) envfree; + function mintRecipients(uint32) external returns (bytes32) envfree; + // constants + function DEFAULT_ADMIN_ROLE() external returns (bytes32) envfree; + function FREEZER() external returns (bytes32) envfree; + function RELAYER() external returns (bytes32) envfree; + function LIMIT_PSM_DEPOSIT() external returns (bytes32) envfree; + function LIMIT_PSM_WITHDRAW() external returns (bytes32) envfree; + function LIMIT_USDC_TO_CCTP() external returns (bytes32) envfree; + function LIMIT_USDC_TO_DOMAIN() external returns (bytes32) envfree; + // getters + function hasRole(bytes32,address) external returns (bool) envfree; + function getRoleAdmin(bytes32) external returns (bytes32) envfree; + // + function proxy.CONTROLLER() external returns (bytes32) envfree; + function proxy.hasRole(bytes32,address) external returns (bool) envfree; + function rateLimits.CONTROLLER() external returns (bytes32) envfree; + function rateLimits.hasRole(bytes32,address) external returns (bool) envfree; + function rateLimits.getRateLimitData(bytes32) external returns (IRateLimits.RateLimitData) envfree; + function cctp.lastSender() external returns (address) envfree; + function cctp.lastSig() external returns (bytes4) envfree; + function cctp.times() external returns (uint256) envfree; + function psm.lastSender() external returns (address) envfree; + function psm.lastSig() external returns (bytes4) envfree; + function psm.retValue() external returns (uint256) envfree; + function usdc.lastSender() external returns (address) envfree; + function usdc.lastSig() external returns (bytes4) envfree; + function aux.makeAssetKey(bytes32,address) external returns (bytes32) envfree; + function aux.makeDomainKey(bytes32,uint32) external returns (bytes32) envfree; + // + function _._ => DISPATCH [ + _.approve(address,uint256), + _.deposit(address,address,uint256), + _.withdraw(address,address,uint256), + _.depositForBurn(uint256,uint32,bytes32,address) + ] default HAVOC_ALL; +} + +persistent ghost bool callProxySuccess; +hook CALL(uint256 g, address addr, uint256 value, uint256 argsOffset, uint256 argsLength, uint256 retOffset, uint256 retLength) uint256 rc { + if (addr == proxy) { + callProxySuccess = rc != 0; + } +} + +ghost uint256 cctpBurnLimit; +function burnLimitsPerMessageSummary() returns uint256 { + return cctpBurnLimit; +} + +// Verify no more entry points exist +rule entryPoints(method f) filtered { f -> !f.isView } { + env e; + + calldataarg args; + f(e, args); + + assert f.selector == sig:grantRole(bytes32,address).selector || + f.selector == sig:revokeRole(bytes32,address).selector || + f.selector == sig:renounceRole(bytes32,address).selector || + f.selector == sig:setMintRecipient(uint32,bytes32).selector || + f.selector == sig:freeze().selector || + f.selector == sig:reactivate().selector || + f.selector == sig:depositPSM(address,uint256).selector || + f.selector == sig:withdrawPSM(address,uint256).selector || + f.selector == sig:transferUSDCToCCTP(uint256,uint32).selector; +} + +// Verify that each storage layout is only modified in the corresponding functions +rule storageAffected(method f) { + env e; + + bytes32 anyBytes32; + address anyAddr; + uint32 anyUint32; + + bool hasRoleBefore = hasRole(anyBytes32, anyAddr); + bytes32 roleAdminBefore = getRoleAdmin(anyBytes32); + bool activeBefore = active(); + bytes32 mintRecipientsBefore = mintRecipients(anyUint32); + + calldataarg args; + f(e, args); + + bool hasRoleAfter = hasRole(anyBytes32, anyAddr); + bytes32 roleAdminAfter = getRoleAdmin(anyBytes32); + bool activeAfter = active(); + bytes32 mintRecipientsAfter = mintRecipients(anyUint32); + + assert hasRoleAfter != hasRoleBefore => + f.selector == sig:grantRole(bytes32,address).selector || + f.selector == sig:revokeRole(bytes32,address).selector || + f.selector == sig:renounceRole(bytes32,address).selector, "Assert 1"; + assert roleAdminAfter == roleAdminBefore, "Assert 2"; + assert activeAfter != activeBefore => + f.selector == sig:freeze().selector || + f.selector == sig:reactivate().selector, "Assert 3"; + assert mintRecipientsAfter != mintRecipientsBefore => + f.selector == sig:setMintRecipient(uint32,bytes32).selector, "Assert 4"; +} + +// Verify correct storage changes for non reverting grantRole +rule grantRole(bytes32 role, address account) { + env e; + + bytes32 otherRole; + address otherAccount; + require otherRole != role || otherAccount != account; + + bool hasOtherBefore = hasRole(otherRole, otherAccount); + + grantRole(e, role, account); + + bool hasRoleAfter = hasRole(role, account); + bool hasOtherAfter = hasRole(otherRole, otherAccount); + + assert hasRoleAfter, "Assert 1"; + assert hasOtherAfter == hasOtherBefore, "Assert 2"; +} + +// Verify revert rules on grantRole +rule grantRole_revert(bytes32 role, address account) { + env e; + + bool hasRoleAdminSender = hasRole(getRoleAdmin(role), e.msg.sender); + + grantRole@withrevert(e, role, account); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleAdminSender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting revokeRole +rule revokeRole(bytes32 role, address account) { + env e; + + bytes32 otherRole; + address otherAccount; + require otherRole != role || otherAccount != account; + + bool hasOtherBefore = hasRole(otherRole, otherAccount); + + revokeRole(e, role, account); + + bool hasRoleAfter = hasRole(role, account); + bool hasOtherAfter = hasRole(otherRole, otherAccount); + + assert !hasRoleAfter, "Assert 1"; + assert hasOtherAfter == hasOtherBefore, "Assert 2"; +} + +// Verify revert rules on revokeRole +rule revokeRole_revert(bytes32 role, address account) { + env e; + + bool hasRoleAdminSender = hasRole(getRoleAdmin(role), e.msg.sender); + + revokeRole@withrevert(e, role, account); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleAdminSender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting renounceRole +rule renounceRole(bytes32 role, address account) { + env e; + + bytes32 otherRole; + address otherAccount; + require otherRole != role || otherAccount != account; + + bool hasOtherBefore = hasRole(otherRole, otherAccount); + + renounceRole(e, role, account); + + bool hasRoleAfter = hasRole(role, account); + bool hasOtherAfter = hasRole(otherRole, otherAccount); + + assert !hasRoleAfter, "Assert 1"; + assert hasOtherAfter == hasOtherBefore, "Assert 2"; +} + +// Verify revert rules on renounceRole +rule renounceRole_revert(bytes32 role, address account) { + env e; + + renounceRole@withrevert(e, role, account); + + bool revert1 = e.msg.value > 0; + bool revert2 = account != e.msg.sender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting setMintRecipient +rule setMintRecipient(uint32 destinationDomain, bytes32 mintRecipient) { + env e; + + uint32 otherUint32; + require otherUint32 != destinationDomain; + + bytes32 mintRecipientsOtherBefore = mintRecipients(otherUint32); + + setMintRecipient(e, destinationDomain, mintRecipient); + + bytes32 mintRecipientsDestinationDomainAfter = mintRecipients(destinationDomain); + bytes32 mintRecipientsOtherAfter = mintRecipients(otherUint32); + + assert mintRecipientsDestinationDomainAfter == mintRecipient, "Assert 1"; + assert mintRecipientsOtherAfter == mintRecipientsOtherBefore, "Assert 1"; +} + +// Verify revert rules on setMintRecipient +rule setMintRecipient_revert(uint32 destinationDomain, bytes32 mintRecipient) { + env e; + + bool hasRoleAdminSender = hasRole(DEFAULT_ADMIN_ROLE(), e.msg.sender); + + setMintRecipient@withrevert(e, destinationDomain, mintRecipient); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleAdminSender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting freeze +rule freeze() { + env e; + + freeze(e); + + bool activeAfter = active(); + + assert !activeAfter, "Assert 1"; +} + +// Verify revert rules on freeze +rule freeze_revert() { + env e; + + bool hasRoleFreezerSender = hasRole(FREEZER(), e.msg.sender); + + freeze@withrevert(e); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleFreezerSender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting reactivate +rule reactivate() { + env e; + + reactivate(e); + + bool activeAfter = active(); + + assert activeAfter, "Assert 1"; +} + +// Verify revert rules on reactivate +rule reactivate_revert() { + env e; + + bool hasRoleAdminSender = hasRole(DEFAULT_ADMIN_ROLE(), e.msg.sender); + + reactivate@withrevert(e); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleAdminSender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting depositPSM +rule depositPSM(address asset, uint256 amount) { + env e; + + require asset == usdc || asset == usds || asset == sUsds; + + bytes32 key = aux.makeAssetKey(LIMIT_PSM_DEPOSIT(), asset); + IRateLimits.RateLimitData rateLimitsPsmDepositData = rateLimits.getRateLimitData(key); + mathint currentRateLimitBefore = rateLimits.getCurrentRateLimit(e, key); + + depositPSM(e, asset, amount); + + mathint currentRateLimitAfter = rateLimits.getCurrentRateLimit(e, key); + address assetLastSenderAfter = asset.lastSender(e); + bytes4 assetLastSigAfter = asset.lastSig(e); + address psmLastSenderAfter = psm.lastSender(); + bytes4 psmLastSigAfter = psm.lastSig(); + + assert currentRateLimitBefore == max_uint256 => currentRateLimitAfter == max_uint256, "Assert "; + assert currentRateLimitBefore < max_uint256 => currentRateLimitAfter == currentRateLimitBefore - amount, "Assert "; + assert assetLastSenderAfter == proxy, "Assert "; + assert assetLastSigAfter == to_bytes4(0x095ea7b3), "Assert "; + assert psmLastSenderAfter == proxy, "Assert "; + assert psmLastSigAfter == to_bytes4(0x8340f549), "Assert "; +} + +// Verify revert rules on depositPSM +rule depositPSM_revert(address asset, uint256 amount) { + env e; + + require asset == usdc || asset == usds || asset == sUsds; + + bool hasRoleRelayerSender = hasRole(RELAYER(), e.msg.sender); + bool active = active(); + + bytes32 key = aux.makeAssetKey(LIMIT_PSM_DEPOSIT(), asset); + IRateLimits.RateLimitData rateLimitsPsmDepositData = rateLimits.getRateLimitData(key); + mathint currentRateLimit = rateLimits.getCurrentRateLimit(e, key); + + // Setup assumptions + require proxy.hasRole(proxy.CONTROLLER(), currentContract); + require rateLimits.hasRole(rateLimits.CONTROLLER(), currentContract); + // Practical assumptions + require e.block.timestamp >= rateLimitsPsmDepositData.lastUpdated; + require rateLimitsPsmDepositData.slope * (e.block.timestamp - rateLimitsPsmDepositData.lastUpdated) + rateLimitsPsmDepositData.lastAmount <= max_uint256; + + depositPSM@withrevert(e, asset, amount); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleRelayerSender; + bool revert3 = !active; + bool revert4 = rateLimitsPsmDepositData.maxAmount == 0; + bool revert5 = amount > currentRateLimit; + bool revert6 = !callProxySuccess; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5 || revert6, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting withdrawPSM +rule withdrawPSM(address asset, uint256 amount) { + env e; + + bytes32 key = aux.makeAssetKey(LIMIT_PSM_WITHDRAW(), asset); + IRateLimits.RateLimitData rateLimitsPsmWithdrawData = rateLimits.getRateLimitData(key); + mathint currentRateLimitBefore = rateLimits.getCurrentRateLimit(e, key); + + mathint amountWithdrawn = psm.retValue(); + + withdrawPSM(e, asset, amount); + + mathint currentRateLimitAfter = rateLimits.getCurrentRateLimit(e, key); + address psmLastSenderAfter = psm.lastSender(); + bytes4 psmLastSigAfter = psm.lastSig(); + + assert currentRateLimitBefore + amountWithdrawn <= rateLimitsPsmWithdrawData.maxAmount => currentRateLimitAfter == currentRateLimitBefore + amountWithdrawn, "Assert "; + assert currentRateLimitBefore + amountWithdrawn > rateLimitsPsmWithdrawData.maxAmount => currentRateLimitAfter == rateLimitsPsmWithdrawData.maxAmount, "Assert "; + assert psmLastSenderAfter == proxy, "Assert "; + assert psmLastSigAfter == to_bytes4(0xd9caed12), "Assert "; +} + +// Verify revert rules on withdrawPSM +rule withdrawPSM_revert(address asset, uint256 amount) { + env e; + + bool hasRoleRelayerSender = hasRole(RELAYER(), e.msg.sender); + bool active = active(); + + bytes32 key = aux.makeAssetKey(LIMIT_PSM_WITHDRAW(), asset); + IRateLimits.RateLimitData rateLimitsPsmWithdrawData = rateLimits.getRateLimitData(key); + mathint currentRateLimit = rateLimits.getCurrentRateLimit(e, key); + + // Setup assumptions + require proxy.hasRole(proxy.CONTROLLER(), currentContract); + require rateLimits.hasRole(rateLimits.CONTROLLER(), currentContract); + // Practical assumptions + require e.block.timestamp >= rateLimitsPsmWithdrawData.lastUpdated; + require rateLimitsPsmWithdrawData.slope * (e.block.timestamp - rateLimitsPsmWithdrawData.lastUpdated) + rateLimitsPsmWithdrawData.lastAmount <= max_uint256; + + mathint amountWithdrawn = psm.retValue(); + + withdrawPSM@withrevert(e, asset, amount); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleRelayerSender; + bool revert3 = !active; + bool revert4 = rateLimitsPsmWithdrawData.maxAmount == 0; + bool revert5 = rateLimitsPsmWithdrawData.maxAmount < max_uint256 && currentRateLimit + amountWithdrawn > max_uint256; + bool revert6 = !callProxySuccess; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5 || revert6, "Revert rules failed"; +} diff --git a/MainnetController.conf b/MainnetController.conf new file mode 100644 index 0000000..a1ea20b --- /dev/null +++ b/MainnetController.conf @@ -0,0 +1,44 @@ +{ + "files": [ + "spark-alm-controller/src/MainnetController.sol", + "spark-alm-controller/src/ALMProxy.sol", + "spark-alm-controller/src/RateLimits.sol", + "harness/CctpMock.sol", + "harness/DaiUsdsMock.sol", + "harness/PsmMock.sol", + "harness/AllocatorVaultMock.sol", + "harness/DaiMock.sol", + "harness/UsdsMock.sol", + "harness/UsdcMock.sol", + "harness/SUsdsMock.sol", + "harness/Auxiliar.sol" + ], + "solc": "solc-0.8.21", + "solc_optimize": "200", + "packages": [ + "forge-std/interfaces/=spark-alm-controller/lib/forge-std/src/interfaces", + "openzeppelin-contracts/=spark-alm-controller/lib/openzeppelin-contracts", + "lib/openzeppelin-contracts/=spark-alm-controller/lib/openzeppelin-contracts", + "src=spark-alm-controller/src" + ], + "link": [ + "MainnetController:proxy=ALMProxy", + "MainnetController:rateLimits=RateLimits", + "MainnetController:cctp=CctpMock", + "MainnetController:daiUsds=DaiUsdsMock", + "MainnetController:psm=PsmMock", + "MainnetController:vault=AllocatorVaultMock", + "MainnetController:dai=DaiMock", + "MainnetController:usds=UsdsMock", + "MainnetController:usdc=UsdcMock", + "MainnetController:susds=SUsdsMock" + ], + "verify": "MainnetController:MainnetController.spec", + "rule_sanity": "basic", + "multi_assert_check": true, + "optimistic_loop": true, + "parametric_contracts": ["MainnetController"], + "smt_timeout": "7000", + "build_cache": true, + "msg": "MainnetController" +} diff --git a/MainnetController.spec b/MainnetController.spec new file mode 100644 index 0000000..8fa5ac6 --- /dev/null +++ b/MainnetController.spec @@ -0,0 +1,740 @@ +// MainnetController.spec + +using ALMProxy as proxy; +using RateLimits as rateLimits; +using CctpMock as cctp; +using DaiUsdsMock as daiUsds; +using PsmMock as psm; +using AllocatorVaultMock as vault; +using DaiMock as dai; +using UsdsMock as usds; +using UsdcMock as usdc; +using SUsdsMock as sUsds; +using Auxiliar as aux; + +methods { + // storage variables + function active() external returns (bool) envfree; + function mintRecipients(uint32) external returns (bytes32) envfree; + // immutables + function buffer() external returns (address) envfree; + function psmTo18ConversionFactor() external returns (uint256) envfree; + // constants + function DEFAULT_ADMIN_ROLE() external returns (bytes32) envfree; + function FREEZER() external returns (bytes32) envfree; + function RELAYER() external returns (bytes32) envfree; + function LIMIT_USDC_TO_CCTP() external returns (bytes32) envfree; + function LIMIT_USDC_TO_DOMAIN() external returns (bytes32) envfree; + function LIMIT_USDS_MINT() external returns (bytes32) envfree; + function LIMIT_USDS_TO_USDC() external returns (bytes32) envfree; + // getters + function hasRole(bytes32,address) external returns (bool) envfree; + function getRoleAdmin(bytes32) external returns (bytes32) envfree; + // + function proxy.CONTROLLER() external returns (bytes32) envfree; + function proxy.hasRole(bytes32,address) external returns (bool) envfree; + function rateLimits.CONTROLLER() external returns (bytes32) envfree; + function rateLimits.hasRole(bytes32,address) external returns (bool) envfree; + function rateLimits.getRateLimitData(bytes32) external returns (IRateLimits.RateLimitData) envfree; + function cctp.lastSender() external returns (address) envfree; + function cctp.lastSig() external returns (bytes4) envfree; + function cctp.times() external returns (uint256) envfree; + function daiUsds.lastSender() external returns (address) envfree; + function daiUsds.lastSig() external returns (bytes4) envfree; + function psm.lastSender() external returns (address) envfree; + function psm.lastSig() external returns (bytes4) envfree; + function vault.lastAmount() external returns (uint256) envfree; + function vault.lastSender() external returns (address) envfree; + function vault.lastSig() external returns (bytes4) envfree; + function dai.lastSender() external returns (address) envfree; + function dai.lastSig() external returns (bytes4) envfree; + function usds.lastFrom() external returns (address) envfree; + function usds.lastTo() external returns (address) envfree; + function usds.lastAmount() external returns (uint256) envfree; + function usds.lastSender() external returns (address) envfree; + function usds.lastSig() external returns (bytes4) envfree; + function usdc.lastSender() external returns (address) envfree; + function usdc.lastSig() external returns (bytes4) envfree; + function sUsds.lastSender() external returns (address) envfree; + function sUsds.lastSig() external returns (bytes4) envfree; + function aux.makeDomainKey(bytes32,uint32) external returns (bytes32) envfree; + // + function _._ => DISPATCH [ + _.approve(address,uint256), + _.transfer(address,uint256), + _.transferFrom(address,address,uint256), + _.depositForBurn(uint256,uint32,bytes32,address), + _.usdsToDai(address,uint256), + _.daiToUsds(address,uint256), + _.usdsToDai(address,uint256), + _.buyGemNoFee(address,uint256), + _.sellGemNoFee(address,uint256), + _.draw(uint256), + _.wipe(uint256), + _.deposit(uint256,address), + _.withdraw(uint256,address,address), + _.redeem(uint256,address,address) + ] default HAVOC_ALL; + function _.burnLimitsPerMessage(address token) external => burnLimitsPerMessageSummary() expect uint256; +} + +persistent ghost bool callProxySuccess; +hook CALL(uint256 g, address addr, uint256 value, uint256 argsOffset, uint256 argsLength, uint256 retOffset, uint256 retLength) uint256 rc { + if (addr == proxy) { + callProxySuccess = rc != 0; + } +} + +ghost uint256 cctpBurnLimit; +function burnLimitsPerMessageSummary() returns uint256 { + return cctpBurnLimit; +} + +definition defDivUp(mathint a, mathint b) returns mathint = a == 0 ? 0 : (a - 1) / b + 1; +definition defMin(mathint a, mathint b) returns mathint = a < b ? a : b; + +// Verify no more entry points exist +rule entryPoints(method f) filtered { f -> !f.isView } { + env e; + + calldataarg args; + f(e, args); + + assert f.selector == sig:grantRole(bytes32,address).selector || + f.selector == sig:revokeRole(bytes32,address).selector || + f.selector == sig:renounceRole(bytes32,address).selector || + f.selector == sig:setMintRecipient(uint32,bytes32).selector || + f.selector == sig:freeze().selector || + f.selector == sig:reactivate().selector || + f.selector == sig:mintUSDS(uint256).selector || + f.selector == sig:burnUSDS(uint256).selector || + f.selector == sig:depositToSUSDS(uint256).selector || + f.selector == sig:withdrawFromSUSDS(uint256).selector || + f.selector == sig:redeemFromSUSDS(uint256).selector || + f.selector == sig:swapUSDSToUSDC(uint256).selector || + f.selector == sig:swapUSDCToUSDS(uint256).selector || + f.selector == sig:transferUSDCToCCTP(uint256,uint32).selector || + f.selector == sig:swapUSDSToUSDC(uint256).selector; +} + +// Verify that each storage layout is only modified in the corresponding functions +rule storageAffected(method f) { + env e; + + bytes32 anyBytes32; + address anyAddr; + uint32 anyUint32; + + bool hasRoleBefore = hasRole(anyBytes32, anyAddr); + bytes32 roleAdminBefore = getRoleAdmin(anyBytes32); + bool activeBefore = active(); + bytes32 mintRecipientsBefore = mintRecipients(anyUint32); + + calldataarg args; + f(e, args); + + bool hasRoleAfter = hasRole(anyBytes32, anyAddr); + bytes32 roleAdminAfter = getRoleAdmin(anyBytes32); + bool activeAfter = active(); + bytes32 mintRecipientsAfter = mintRecipients(anyUint32); + + assert hasRoleAfter != hasRoleBefore => + f.selector == sig:grantRole(bytes32,address).selector || + f.selector == sig:revokeRole(bytes32,address).selector || + f.selector == sig:renounceRole(bytes32,address).selector, "Assert 1"; + assert roleAdminAfter == roleAdminBefore, "Assert 2"; + assert activeAfter != activeBefore => + f.selector == sig:freeze().selector || + f.selector == sig:reactivate().selector, "Assert 3"; + assert mintRecipientsAfter != mintRecipientsBefore => + f.selector == sig:setMintRecipient(uint32,bytes32).selector, "Assert 4"; +} + +// Verify correct storage changes for non reverting grantRole +rule grantRole(bytes32 role, address account) { + env e; + + bytes32 otherRole; + address otherAccount; + require otherRole != role || otherAccount != account; + + bool hasOtherBefore = hasRole(otherRole, otherAccount); + + grantRole(e, role, account); + + bool hasRoleAfter = hasRole(role, account); + bool hasOtherAfter = hasRole(otherRole, otherAccount); + + assert hasRoleAfter, "Assert 1"; + assert hasOtherAfter == hasOtherBefore, "Assert 2"; +} + +// Verify revert rules on grantRole +rule grantRole_revert(bytes32 role, address account) { + env e; + + bool hasRoleAdminSender = hasRole(getRoleAdmin(role), e.msg.sender); + + grantRole@withrevert(e, role, account); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleAdminSender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting revokeRole +rule revokeRole(bytes32 role, address account) { + env e; + + bytes32 otherRole; + address otherAccount; + require otherRole != role || otherAccount != account; + + bool hasOtherBefore = hasRole(otherRole, otherAccount); + + revokeRole(e, role, account); + + bool hasRoleAfter = hasRole(role, account); + bool hasOtherAfter = hasRole(otherRole, otherAccount); + + assert !hasRoleAfter, "Assert 1"; + assert hasOtherAfter == hasOtherBefore, "Assert 2"; +} + +// Verify revert rules on revokeRole +rule revokeRole_revert(bytes32 role, address account) { + env e; + + bool hasRoleAdminSender = hasRole(getRoleAdmin(role), e.msg.sender); + + revokeRole@withrevert(e, role, account); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleAdminSender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting renounceRole +rule renounceRole(bytes32 role, address account) { + env e; + + bytes32 otherRole; + address otherAccount; + require otherRole != role || otherAccount != account; + + bool hasOtherBefore = hasRole(otherRole, otherAccount); + + renounceRole(e, role, account); + + bool hasRoleAfter = hasRole(role, account); + bool hasOtherAfter = hasRole(otherRole, otherAccount); + + assert !hasRoleAfter, "Assert 1"; + assert hasOtherAfter == hasOtherBefore, "Assert 2"; +} + +// Verify revert rules on renounceRole +rule renounceRole_revert(bytes32 role, address account) { + env e; + + renounceRole@withrevert(e, role, account); + + bool revert1 = e.msg.value > 0; + bool revert2 = account != e.msg.sender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting setMintRecipient +rule setMintRecipient(uint32 destinationDomain, bytes32 mintRecipient) { + env e; + + uint32 otherUint32; + require otherUint32 != destinationDomain; + + bytes32 mintRecipientsOtherBefore = mintRecipients(otherUint32); + + setMintRecipient(e, destinationDomain, mintRecipient); + + bytes32 mintRecipientsDestinationDomainAfter = mintRecipients(destinationDomain); + bytes32 mintRecipientsOtherAfter = mintRecipients(otherUint32); + + assert mintRecipientsDestinationDomainAfter == mintRecipient, "Assert 1"; + assert mintRecipientsOtherAfter == mintRecipientsOtherBefore, "Assert 1"; +} + +// Verify revert rules on setMintRecipient +rule setMintRecipient_revert(uint32 destinationDomain, bytes32 mintRecipient) { + env e; + + bool hasRoleAdminSender = hasRole(DEFAULT_ADMIN_ROLE(), e.msg.sender); + + setMintRecipient@withrevert(e, destinationDomain, mintRecipient); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleAdminSender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting freeze +rule freeze() { + env e; + + freeze(e); + + bool activeAfter = active(); + + assert !activeAfter, "Assert 1"; +} + +// Verify revert rules on freeze +rule freeze_revert() { + env e; + + bool hasRoleFreezerSender = hasRole(FREEZER(), e.msg.sender); + + freeze@withrevert(e); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleFreezerSender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting reactivate +rule reactivate() { + env e; + + reactivate(e); + + bool activeAfter = active(); + + assert activeAfter, "Assert 1"; +} + +// Verify revert rules on reactivate +rule reactivate_revert() { + env e; + + bool hasRoleAdminSender = hasRole(DEFAULT_ADMIN_ROLE(), e.msg.sender); + + reactivate@withrevert(e); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleAdminSender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting mintUSDS +rule mintUSDS(uint256 usdsAmount) { + env e; + + mintUSDS(e, usdsAmount); + + uint256 vaultLastAmountAfter = vault.lastAmount(); + address vaultLastSenderAfter = vault.lastSender(); + bytes4 vaultLastSigAfter = vault.lastSig(); + address usdsLastFromAfter = usds.lastFrom(); + address usdsLastToAfter = usds.lastTo(); + uint256 usdsLastAmountAfter = usds.lastAmount(); + address usdsLastSenderAfter = usds.lastSender(); + bytes4 usdsLastSigAfter = usds.lastSig(); + + // assert vaultLastAmountAfter == usdsAmount, "Assert 1"; + assert vaultLastSenderAfter == proxy, "Assert 2"; + assert vaultLastSigAfter == to_bytes4(0x3b304147), "Assert 3"; + // assert usdsLastFromAfter == buffer(), "Assert 4"; + // assert usdsLastToAfter == proxy, "Assert 5"; + // assert usdsLastAmountAfter == usdsAmount, "Assert 6"; + assert usdsLastSenderAfter == proxy, "Assert 7"; + assert usdsLastSigAfter == to_bytes4(0x23b872dd), "Assert 8"; +} + +// Verify revert rules on mintUSDS +rule mintUSDS_revert(uint256 usdsAmount) { + env e; + + bool hasRoleRelayerSender = hasRole(RELAYER(), e.msg.sender); + bool active = active(); + + bytes32 LIMIT_USDS_MINT = LIMIT_USDS_MINT(); + IRateLimits.RateLimitData rateLimitsUsdsMintData = rateLimits.getRateLimitData(LIMIT_USDS_MINT); + mathint currentRateLimit = rateLimits.getCurrentRateLimit(e, LIMIT_USDS_MINT); + + // Setup assumptions + require proxy.hasRole(proxy.CONTROLLER(), currentContract); + require rateLimits.hasRole(rateLimits.CONTROLLER(), currentContract); + // Practical assumptions + require e.block.timestamp >= rateLimitsUsdsMintData.lastUpdated; + require rateLimitsUsdsMintData.slope * (e.block.timestamp - rateLimitsUsdsMintData.lastUpdated) + rateLimitsUsdsMintData.lastAmount <= max_uint256; + + mintUSDS@withrevert(e, usdsAmount); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleRelayerSender; + bool revert3 = !active; + bool revert4 = rateLimitsUsdsMintData.maxAmount == 0; + bool revert5 = usdsAmount > currentRateLimit; + bool revert6 = !callProxySuccess; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5 || revert6, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting burnUSDS +rule burnUSDS(uint256 usdsAmount) { + env e; + + burnUSDS(e, usdsAmount); + + uint256 vaultLastAmountAfter = vault.lastAmount(); + address vaultLastSenderAfter = vault.lastSender(); + bytes4 vaultLastSigAfter = vault.lastSig(); + address usdsLastFromAfter = usds.lastFrom(); + address usdsLastToAfter = usds.lastTo(); + uint256 usdsLastAmountAfter = usds.lastAmount(); + address usdsLastSenderAfter = usds.lastSender(); + bytes4 usdsLastSigAfter = usds.lastSig(); + + // assert vaultLastAmountAfter == usdsAmount, "Assert 1"; + assert vaultLastSenderAfter == proxy, "Assert 2"; + assert vaultLastSigAfter == to_bytes4(0xb38a1620), "Assert 3"; + // assert usdsLastFromAfter == proxy, "Assert 4"; + // assert usdsLastToAfter == proxy, "Assert 5"; + // assert usdsLastAmountAfter == usdsAmount, "Assert 6"; + assert usdsLastSenderAfter == proxy, "Assert 7"; + assert usdsLastSigAfter == to_bytes4(0xa9059cbb), "Assert 8"; +} + +// Verify revert rules on burnUSDS +rule burnUSDS_revert(uint256 usdsAmount) { + env e; + + bool hasRoleRelayerSender = hasRole(RELAYER(), e.msg.sender); + bool active = active(); + + bytes32 LIMIT_USDS_MINT = LIMIT_USDS_MINT(); + IRateLimits.RateLimitData rateLimitsUsdsMintData = rateLimits.getRateLimitData(LIMIT_USDS_MINT); + mathint currentRateLimit = rateLimits.getCurrentRateLimit(e, LIMIT_USDS_MINT); + + // Setup assumptions + require proxy.hasRole(proxy.CONTROLLER(), currentContract); + require rateLimits.hasRole(rateLimits.CONTROLLER(), currentContract); + // Practical assumptions + require e.block.timestamp >= rateLimitsUsdsMintData.lastUpdated; + require rateLimitsUsdsMintData.slope * (e.block.timestamp - rateLimitsUsdsMintData.lastUpdated) + rateLimitsUsdsMintData.lastAmount <= max_uint256; + + burnUSDS@withrevert(e, usdsAmount); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleRelayerSender; + bool revert3 = !active; + bool revert4 = rateLimitsUsdsMintData.maxAmount == 0; + bool revert5 = rateLimitsUsdsMintData.maxAmount < max_uint256 && currentRateLimit + usdsAmount > max_uint256; + bool revert6 = !callProxySuccess; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5 || revert6, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting depositToSUSDS +rule depositToSUSDS(uint256 usdsAmount) { + env e; + + depositToSUSDS(e, usdsAmount); + + address usdsLastSenderAfter = usds.lastSender(); + bytes4 usdsLastSigAfter = usds.lastSig(); + address sUsdsLastSenderAfter = sUsds.lastSender(); + bytes4 sUsdsLastSigAfter = sUsds.lastSig(); + + assert usdsLastSenderAfter == proxy, "Assert "; + assert usdsLastSigAfter == to_bytes4(0x095ea7b3), "Assert "; + assert sUsdsLastSenderAfter == proxy, "Assert "; + assert sUsdsLastSigAfter == to_bytes4(0x6e553f65), "Assert "; +} + +// Verify revert rules on depositToSUSDS +rule depositToSUSDS_revert(uint256 usdsAmount) { + env e; + + bool hasRoleRelayerSender = hasRole(RELAYER(), e.msg.sender); + bool active = active(); + + // Setup assumptions + require proxy.hasRole(proxy.CONTROLLER(), currentContract); + require rateLimits.hasRole(rateLimits.CONTROLLER(), currentContract); + + depositToSUSDS@withrevert(e, usdsAmount); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleRelayerSender; + bool revert3 = !active; + bool revert4 = !callProxySuccess; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting withdrawFromSUSDS +rule withdrawFromSUSDS(uint256 usdsAmount) { + env e; + + withdrawFromSUSDS(e, usdsAmount); + + address sUsdsLastSenderAfter = sUsds.lastSender(); + bytes4 sUsdsLastSigAfter = sUsds.lastSig(); + + assert sUsdsLastSenderAfter == proxy, "Assert "; + assert sUsdsLastSigAfter == to_bytes4(0xb460af94), "Assert "; +} + +// Verify revert rules on withdrawFromSUSDS +rule withdrawFromSUSDS_revert(uint256 usdsAmount) { + env e; + + bool hasRoleRelayerSender = hasRole(RELAYER(), e.msg.sender); + bool active = active(); + + // Setup assumptions + require proxy.hasRole(proxy.CONTROLLER(), currentContract); + require rateLimits.hasRole(rateLimits.CONTROLLER(), currentContract); + + withdrawFromSUSDS@withrevert(e, usdsAmount); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleRelayerSender; + bool revert3 = !active; + bool revert4 = !callProxySuccess; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting redeemFromSUSDS +rule redeemFromSUSDS(uint256 sUsdsSharesAmount) { + env e; + + redeemFromSUSDS(e, sUsdsSharesAmount); + + address sUsdsLastSenderAfter = sUsds.lastSender(); + bytes4 sUsdsLastSigAfter = sUsds.lastSig(); + + assert sUsdsLastSenderAfter == proxy, "Assert "; + assert sUsdsLastSigAfter == to_bytes4(0xba087652), "Assert "; +} + +// Verify revert rules on redeemFromSUSDS +rule redeemFromSUSDS_revert(uint256 sUsdsSharesAmount) { + env e; + + bool hasRoleRelayerSender = hasRole(RELAYER(), e.msg.sender); + bool active = active(); + + // Setup assumptions + require proxy.hasRole(proxy.CONTROLLER(), currentContract); + require rateLimits.hasRole(rateLimits.CONTROLLER(), currentContract); + + redeemFromSUSDS@withrevert(e, sUsdsSharesAmount); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleRelayerSender; + bool revert3 = !active; + bool revert4 = !callProxySuccess; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting swapUSDSToUSDC +rule swapUSDSToUSDC(uint256 usdcAmount) { + env e; + + swapUSDSToUSDC(e, usdcAmount); + + address usdsLastSenderAfter = usds.lastSender(); + bytes4 usdsLastSigAfter = usds.lastSig(); + address daiUsdsLastSenderAfter = daiUsds.lastSender(); + bytes4 daiUsdsLastSigAfter = daiUsds.lastSig(); + address daiLastSenderAfter = dai.lastSender(); + bytes4 daiLastSigAfter = dai.lastSig(); + address psmLastSenderAfter = psm.lastSender(); + bytes4 psmLastSigAfter = psm.lastSig(); + + assert usdsLastSenderAfter == proxy, "Assert "; + assert usdsLastSigAfter == to_bytes4(0x095ea7b3), "Assert "; + assert daiUsdsLastSenderAfter == proxy, "Assert "; + assert daiUsdsLastSigAfter == to_bytes4(0x68f30150), "Assert "; + assert daiLastSenderAfter == proxy, "Assert "; + assert daiLastSigAfter == to_bytes4(0x095ea7b3), "Assert "; + assert psmLastSenderAfter == proxy, "Assert "; + assert psmLastSigAfter == to_bytes4(0x067d9274), "Assert "; +} + +// Verify revert rules on swapUSDSToUSDC +rule swapUSDSToUSDC_revert(uint256 usdcAmount) { + env e; + + bool hasRoleRelayerSender = hasRole(RELAYER(), e.msg.sender); + bool active = active(); + + bytes32 LIMIT_USDS_TO_USDC = LIMIT_USDS_TO_USDC(); + IRateLimits.RateLimitData rateLimitsUsdsToUsdcData = rateLimits.getRateLimitData(LIMIT_USDS_TO_USDC); + mathint currentRateLimit = rateLimits.getCurrentRateLimit(e, LIMIT_USDS_TO_USDC); + + mathint psmTo18ConversionFactor = psmTo18ConversionFactor(); + + // Setup assumptions + require proxy.hasRole(proxy.CONTROLLER(), currentContract); + require rateLimits.hasRole(rateLimits.CONTROLLER(), currentContract); + // Practical assumptions + require e.block.timestamp >= rateLimitsUsdsToUsdcData.lastUpdated; + require rateLimitsUsdsToUsdcData.slope * (e.block.timestamp - rateLimitsUsdsToUsdcData.lastUpdated) + rateLimitsUsdsToUsdcData.lastAmount <= max_uint256; + + swapUSDSToUSDC@withrevert(e, usdcAmount); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleRelayerSender; + bool revert3 = !active; + bool revert4 = rateLimitsUsdsToUsdcData.maxAmount == 0; + bool revert5 = usdcAmount > currentRateLimit; + bool revert6 = !callProxySuccess; + bool revert7 = usdcAmount * psmTo18ConversionFactor > max_uint256; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5 || revert6 || + revert7, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting swapUSDCToUSDS +rule swapUSDCToUSDS(uint256 usdcAmount) { + env e; + + swapUSDCToUSDS(e, usdcAmount); + + address usdcLastSenderAfter = usdc.lastSender(); + bytes4 usdcLastSigAfter = usdc.lastSig(); + address psmLastSenderAfter = psm.lastSender(); + bytes4 psmLastSigAfter = psm.lastSig(); + address daiLastSenderAfter = dai.lastSender(); + bytes4 daiLastSigAfter = dai.lastSig(); + address daiUsdsLastSenderAfter = daiUsds.lastSender(); + bytes4 daiUsdsLastSigAfter = daiUsds.lastSig(); + + assert usdcLastSenderAfter == proxy, "Assert "; + assert usdcLastSigAfter == to_bytes4(0x095ea7b3), "Assert "; + assert psmLastSenderAfter == proxy, "Assert "; + assert psmLastSigAfter == to_bytes4(0x86c34f42), "Assert "; + assert daiLastSenderAfter == proxy, "Assert "; + assert daiLastSigAfter == to_bytes4(0x095ea7b3), "Assert "; + assert daiUsdsLastSenderAfter == proxy, "Assert "; + assert daiUsdsLastSigAfter == to_bytes4(0xf2c07aae), "Assert "; +} + +// Verify revert rules on swapUSDCToUSDS +rule swapUSDCToUSDS_revert(uint256 usdcAmount) { + env e; + + bool hasRoleRelayerSender = hasRole(RELAYER(), e.msg.sender); + bool active = active(); + + bytes32 LIMIT_USDS_TO_USDC = LIMIT_USDS_TO_USDC(); + IRateLimits.RateLimitData rateLimitsUsdsToUsdcData = rateLimits.getRateLimitData(LIMIT_USDS_TO_USDC); + mathint currentRateLimit = rateLimits.getCurrentRateLimit(e, LIMIT_USDS_TO_USDC); + + mathint psmTo18ConversionFactor = psmTo18ConversionFactor(); + + // Setup assumptions + require proxy.hasRole(proxy.CONTROLLER(), currentContract); + require rateLimits.hasRole(rateLimits.CONTROLLER(), currentContract); + // Practical assumptions + require e.block.timestamp >= rateLimitsUsdsToUsdcData.lastUpdated; + require rateLimitsUsdsToUsdcData.slope * (e.block.timestamp - rateLimitsUsdsToUsdcData.lastUpdated) + rateLimitsUsdsToUsdcData.lastAmount <= max_uint256; + + swapUSDCToUSDS@withrevert(e, usdcAmount); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleRelayerSender; + bool revert3 = !active; + bool revert4 = rateLimitsUsdsToUsdcData.maxAmount == 0; + bool revert5 = rateLimitsUsdsToUsdcData.maxAmount < max_uint256 && currentRateLimit + usdcAmount > max_uint256; + bool revert6 = !callProxySuccess; + bool revert7 = psmTo18ConversionFactor == 0; + bool revert8 = usdcAmount * psmTo18ConversionFactor > max_uint256; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5 || revert6 || + revert7 || revert8, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting transferUSDCToCCTP +rule transferUSDCToCCTP(uint256 usdcAmount, uint32 destinationDomain) { + env e; + + require cctp.times() == 0; + + mathint burnLimit = cctpBurnLimit; + + mathint calcTimes = burnLimit > 0 ? defDivUp(usdcAmount, burnLimit) : 0; + + transferUSDCToCCTP(e, usdcAmount, destinationDomain); + + address usdcLastSenderAfter = usdc.lastSender(); + bytes4 usdcLastSigAfter = usdc.lastSig(); + address cctpLastSenderAfter = cctp.lastSender(); + bytes4 cctpLastSigAfter = cctp.lastSig(); + mathint cctpTimesAfter = cctp.times(); + + assert usdcLastSenderAfter == proxy, "Assert "; + assert usdcLastSigAfter == to_bytes4(0x095ea7b3), "Assert "; + assert calcTimes > 0 => cctpLastSenderAfter == proxy, "Assert "; + assert calcTimes > 0 => cctpLastSigAfter == to_bytes4(0x6fd3504e), "Assert "; + assert cctpTimesAfter == calcTimes, "Assert "; +} + +// Verify revert rules on transferUSDCToCCTP +rule transferUSDCToCCTP_revert(uint256 usdcAmount, uint32 destinationDomain) { + env e; + + bool hasRoleRelayerSender = hasRole(RELAYER(), e.msg.sender); + bool active = active(); + + bytes32 LIMIT_USDC_TO_CCTP = LIMIT_USDC_TO_CCTP(); + IRateLimits.RateLimitData rateLimitsUsdcToCctpData = rateLimits.getRateLimitData(LIMIT_USDC_TO_CCTP); + mathint currentRateLimitUsdcToCctp = rateLimits.getCurrentRateLimit(e, LIMIT_USDC_TO_CCTP); + + bytes32 keyDomain = aux.makeDomainKey(LIMIT_USDC_TO_DOMAIN(), destinationDomain); + IRateLimits.RateLimitData rateLimitsUsdcToDomainData = rateLimits.getRateLimitData(keyDomain); + mathint currentRateLimitUsdcToDomain = rateLimits.getCurrentRateLimit(e, keyDomain); + + bytes32 mintRecipient = mintRecipients(destinationDomain); + + // Setup assumptions + require proxy.hasRole(proxy.CONTROLLER(), currentContract); + require rateLimits.hasRole(rateLimits.CONTROLLER(), currentContract); + // Practical assumptions + require e.block.timestamp >= rateLimitsUsdcToCctpData.lastUpdated; + require rateLimitsUsdcToCctpData.slope * (e.block.timestamp - rateLimitsUsdcToCctpData.lastUpdated) + rateLimitsUsdcToCctpData.lastAmount <= max_uint256; + require e.block.timestamp >= rateLimitsUsdcToDomainData.lastUpdated; + require rateLimitsUsdcToDomainData.slope * (e.block.timestamp - rateLimitsUsdcToDomainData.lastUpdated) + rateLimitsUsdcToDomainData.lastAmount <= max_uint256; + + transferUSDCToCCTP@withrevert(e, usdcAmount, destinationDomain); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleRelayerSender; + bool revert3 = !active; + bool revert4 = rateLimitsUsdcToCctpData.maxAmount == 0; + bool revert5 = usdcAmount > currentRateLimitUsdcToCctp; + bool revert6 = rateLimitsUsdcToDomainData.maxAmount == 0; + bool revert7 = usdcAmount > currentRateLimitUsdcToDomain; + bool revert8 = mintRecipient == to_bytes32(0x0); + bool revert9 = !callProxySuccess; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4 || revert5 || revert6 || + revert7 || revert8 || revert9, "Revert rules failed"; +} diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..6f14d6e --- /dev/null +++ b/Makefile @@ -0,0 +1,4 @@ +PATH := ~/.solc-select/artifacts/:~/.solc-select/artifacts/solc-0.8.21:$(PATH) +certora-rate-limits :; PATH=${PATH} certoraRun RateLimits.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) +certora-mainnet-controller :; PATH=${PATH} certoraRun MainnetController.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) +certora-foreign-controller :; PATH=${PATH} certoraRun ForeignController.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) diff --git a/RateLimits.conf b/RateLimits.conf new file mode 100644 index 0000000..d1ea9c3 --- /dev/null +++ b/RateLimits.conf @@ -0,0 +1,19 @@ +{ + "files": [ + "spark-alm-controller/src/RateLimits.sol" + ], + "solc": "solc-0.8.21", + "solc_optimize": "200", + "packages": [ + "openzeppelin-contracts/=spark-alm-controller/lib/openzeppelin-contracts", + "lib/openzeppelin-contracts/=spark-alm-controller/lib/openzeppelin-contracts", + "src=spark-alm-controller/src" + ], + "verify": "RateLimits:RateLimits.spec", + "rule_sanity": "basic", + "multi_assert_check": true, + "parametric_contracts": ["RateLimits"], + "smt_timeout": "7000", + "build_cache": true, + "msg": "RateLimits" +} diff --git a/RateLimits.spec b/RateLimits.spec new file mode 100644 index 0000000..af2362d --- /dev/null +++ b/RateLimits.spec @@ -0,0 +1,304 @@ +// RateLimits.spec + +methods { + // constants + function DEFAULT_ADMIN_ROLE() external returns (bytes32) envfree; + function CONTROLLER() external returns (bytes32) envfree; + // getters + function hasRole(bytes32,address) external returns (bool) envfree; + function getRoleAdmin(bytes32) external returns (bytes32) envfree; + function getRateLimitData(bytes32) external returns (IRateLimits.RateLimitData) envfree; + // +} + +definition defMin(mathint a, mathint b) returns mathint = a < b ? a : b; +definition defGetCurrentRateLimit(env e, bytes32 key) returns mathint = + currentContract._data[key].maxAmount == max_uint256 + ? max_uint256 + : defMin( + currentContract._data[key].slope * (e.block.timestamp - currentContract._data[key].lastUpdated) + currentContract._data[key].lastAmount, + currentContract._data[key].maxAmount + ); + +// Verify no more entry points exist +rule entryPoints(method f) filtered { f -> !f.isView } { + env e; + + calldataarg args; + f(e, args); + + assert f.selector == sig:grantRole(bytes32,address).selector || + f.selector == sig:revokeRole(bytes32,address).selector || + f.selector == sig:renounceRole(bytes32,address).selector || + f.selector == sig:setRateLimitData(bytes32,uint256,uint256,uint256,uint256).selector || + f.selector == sig:setRateLimitData(bytes32,uint256,uint256).selector || + f.selector == sig:setUnlimitedRateLimitData(bytes32).selector || + f.selector == sig:triggerRateLimitDecrease(bytes32,uint256).selector || + f.selector == sig:triggerRateLimitIncrease(bytes32,uint256).selector; +} + +// Verify that each storage layout is only modified in the corresponding functions +rule storageAffected(method f) { + env e; + + bytes32 anyBytes32; + address anyAddr; + + bool hasRoleBefore = hasRole(anyBytes32, anyAddr); + bytes32 roleAdminBefore = getRoleAdmin(anyBytes32); + IRateLimits.RateLimitData dataBefore = getRateLimitData(anyBytes32); + + calldataarg args; + f(e, args); + + bool hasRoleAfter = hasRole(anyBytes32, anyAddr); + bytes32 roleAdminAfter = getRoleAdmin(anyBytes32); + IRateLimits.RateLimitData dataAfter = getRateLimitData(anyBytes32); + + assert hasRoleAfter != hasRoleBefore => + f.selector == sig:grantRole(bytes32,address).selector || + f.selector == sig:revokeRole(bytes32,address).selector || + f.selector == sig:renounceRole(bytes32,address).selector, "Assert 1"; + assert roleAdminAfter == roleAdminBefore, "Assert 2"; + assert dataAfter.maxAmount != dataBefore.maxAmount => + f.selector == sig:setRateLimitData(bytes32,uint256,uint256,uint256,uint256).selector || + f.selector == sig:setRateLimitData(bytes32,uint256,uint256).selector || + f.selector == sig:setUnlimitedRateLimitData(bytes32).selector, "Assert 3"; + assert dataAfter.slope != dataBefore.slope => + f.selector == sig:setRateLimitData(bytes32,uint256,uint256,uint256,uint256).selector || + f.selector == sig:setRateLimitData(bytes32,uint256,uint256).selector || + f.selector == sig:setUnlimitedRateLimitData(bytes32).selector, "Assert 4"; + assert dataAfter.lastAmount != dataBefore.lastAmount => + f.selector == sig:setRateLimitData(bytes32,uint256,uint256,uint256,uint256).selector || + f.selector == sig:setRateLimitData(bytes32,uint256,uint256).selector || + f.selector == sig:setUnlimitedRateLimitData(bytes32).selector || + f.selector == sig:triggerRateLimitDecrease(bytes32,uint256).selector || + f.selector == sig:triggerRateLimitIncrease(bytes32,uint256).selector, "Assert 5"; + assert dataAfter.lastUpdated != dataBefore.lastUpdated => + f.selector == sig:setRateLimitData(bytes32,uint256,uint256,uint256,uint256).selector || + f.selector == sig:setRateLimitData(bytes32,uint256,uint256).selector || + f.selector == sig:setUnlimitedRateLimitData(bytes32).selector || + f.selector == sig:triggerRateLimitDecrease(bytes32,uint256).selector || + f.selector == sig:triggerRateLimitIncrease(bytes32,uint256).selector, "Assert 6"; +} + +// Verify correct storage changes for non reverting grantRole +rule grantRole(bytes32 role, address account) { + env e; + + bytes32 otherRole; + address otherAccount; + require otherRole != role || otherAccount != account; + + bool hasOtherBefore = hasRole(otherRole, otherAccount); + + grantRole(e, role, account); + + bool hasRoleAfter = hasRole(role, account); + bool hasOtherAfter = hasRole(otherRole, otherAccount); + + assert hasRoleAfter, "Assert 1"; + assert hasOtherAfter == hasOtherBefore, "Assert 2"; +} + +// Verify revert rules on grantRole +rule grantRole_revert(bytes32 role, address account) { + env e; + + bool hasRoleAdminSender = hasRole(getRoleAdmin(role), e.msg.sender); + + grantRole@withrevert(e, role, account); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleAdminSender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting revokeRole +rule revokeRole(bytes32 role, address account) { + env e; + + bytes32 otherRole; + address otherAccount; + require otherRole != role || otherAccount != account; + + bool hasOtherBefore = hasRole(otherRole, otherAccount); + + revokeRole(e, role, account); + + bool hasRoleAfter = hasRole(role, account); + bool hasOtherAfter = hasRole(otherRole, otherAccount); + + assert !hasRoleAfter, "Assert 1"; + assert hasOtherAfter == hasOtherBefore, "Assert 2"; +} + +// Verify revert rules on revokeRole +rule revokeRole_revert(bytes32 role, address account) { + env e; + + bool hasRoleAdminSender = hasRole(getRoleAdmin(role), e.msg.sender); + + revokeRole@withrevert(e, role, account); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleAdminSender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting renounceRole +rule renounceRole(bytes32 role, address account) { + env e; + + bytes32 otherRole; + address otherAccount; + require otherRole != role || otherAccount != account; + + bool hasOtherBefore = hasRole(otherRole, otherAccount); + + renounceRole(e, role, account); + + bool hasRoleAfter = hasRole(role, account); + bool hasOtherAfter = hasRole(otherRole, otherAccount); + + assert !hasRoleAfter, "Assert 1"; + assert hasOtherAfter == hasOtherBefore, "Assert 2"; +} + +// Verify revert rules on renounceRole +rule renounceRole_revert(bytes32 role, address account) { + env e; + + renounceRole@withrevert(e, role, account); + + bool revert1 = e.msg.value > 0; + bool revert2 = account != e.msg.sender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting setRateLimitData +rule setRateLimitData(bytes32 key, uint256 maxAmount, uint256 slope, uint256 lastAmount, uint256 lastUpdated) { + env e; + + setRateLimitData(e, key, maxAmount, slope, lastAmount, lastUpdated); + + IRateLimits.RateLimitData dataAfter = getRateLimitData(key); + + assert dataAfter.maxAmount == maxAmount, "Assert 1"; + assert dataAfter.slope == slope, "Assert 2"; + assert dataAfter.lastAmount == lastAmount, "Assert 3"; + assert dataAfter.lastUpdated == lastUpdated, "Assert 4"; +} + +// Verify revert rules on setRateLimitData +rule setRateLimitData_revert(bytes32 key, uint256 maxAmount, uint256 slope, uint256 lastAmount, uint256 lastUpdated) { + env e; + + bool hasRoleAdminSender = hasRole(DEFAULT_ADMIN_ROLE(), e.msg.sender); + + setRateLimitData@withrevert(e, key, maxAmount, slope, lastAmount, lastUpdated); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleAdminSender; + bool revert3 = lastAmount > maxAmount; + bool revert4 = lastUpdated > e.block.timestamp; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting setRateLimitData +rule setRateLimitData2(bytes32 key, uint256 maxAmount, uint256 slope) { + env e; + + setRateLimitData(e, key, maxAmount, slope); + + IRateLimits.RateLimitData dataAfter = getRateLimitData(key); + + assert dataAfter.maxAmount == maxAmount, "Assert 1"; + assert dataAfter.slope == slope, "Assert 2"; + assert dataAfter.lastAmount == maxAmount, "Assert 3"; + assert dataAfter.lastUpdated == e.block.timestamp, "Assert 4"; +} + +// Verify revert rules on setRateLimitData +rule setRateLimitData2_revert(bytes32 key, uint256 maxAmount, uint256 slope) { + env e; + + bool hasRoleAdminSender = hasRole(DEFAULT_ADMIN_ROLE(), e.msg.sender); + + setRateLimitData@withrevert(e, key, maxAmount, slope); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleAdminSender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting setUnlimitedRateLimitData +rule setUnlimitedRateLimitData(bytes32 key) { + env e; + + setUnlimitedRateLimitData(e, key); + + IRateLimits.RateLimitData dataAfter = getRateLimitData(key); + + assert dataAfter.maxAmount == max_uint256, "Assert 1"; + assert dataAfter.slope == 0, "Assert 2"; + assert dataAfter.lastAmount == max_uint256, "Assert 3"; + assert dataAfter.lastUpdated == e.block.timestamp, "Assert 4"; +} + +// Verify revert rules on setUnlimitedRateLimitData +rule setUnlimitedRateLimitData_revert(bytes32 key) { + env e; + + bool hasRoleAdminSender = hasRole(DEFAULT_ADMIN_ROLE(), e.msg.sender); + + setUnlimitedRateLimitData@withrevert(e, key); + + bool revert1 = e.msg.value > 0; + bool revert2 = !hasRoleAdminSender; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct behaviour for getRateLimitData getter +rule getRateLimitData(bytes32 key) { + env e; + + IRateLimits.RateLimitData data = getRateLimitData(key); + + assert data.maxAmount == currentContract._data[key].maxAmount, "Assert 1"; + assert data.slope == currentContract._data[key].slope, "Assert 2"; + assert data.lastAmount == currentContract._data[key].lastAmount, "Assert 3"; + assert data.lastUpdated == currentContract._data[key].lastUpdated, "Assert 4"; +} + +// Verify correct behaviour for getCurrentRateLimit getter +rule getCurrentRateLimit(bytes32 key) { + env e; + + mathint limit = defGetCurrentRateLimit(e, key); + + mathint limitRet = getCurrentRateLimit(e, key); + + assert limitRet == limit, "Assert 1"; +} + +// // Verify correct storage changes for non reverting triggerRateLimitDecrease +// rule triggerRateLimitDecrease(bytes32 key, uint256 amountToDecrease) { +// env e; + +// triggerRateLimitDecrease(e, key, amountToDecrease); + +// IRateLimits.RateLimitData dataAfter = getRateLimitData(key); + +// assert dataAfter.maxAmount == max_uint256, "Assert 1"; +// assert dataAfter.slope == 0, "Assert 2"; +// assert dataAfter.lastAmount == max_uint256, "Assert 3"; +// assert dataAfter.lastUpdated == e.block.timestamp, "Assert 4"; +// } diff --git a/harness/AllocatorVaultMock.sol b/harness/AllocatorVaultMock.sol new file mode 100644 index 0000000..57ea8db --- /dev/null +++ b/harness/AllocatorVaultMock.sol @@ -0,0 +1,21 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +pragma solidity ^0.8.21; + +contract AllocatorVaultMock { + uint256 public lastAmount; + address public lastSender; + bytes4 public lastSig; + + function draw(uint256 amount) external { + lastAmount = amount; + lastSender = msg.sender; + lastSig = msg.sig; + } + + function wipe(uint256 amount) external { + lastAmount = amount; + lastSender = msg.sender; + lastSig = msg.sig; + } +} diff --git a/harness/Auxiliar.sol b/harness/Auxiliar.sol new file mode 100644 index 0000000..db4da14 --- /dev/null +++ b/harness/Auxiliar.sol @@ -0,0 +1,14 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +pragma solidity ^0.8.21; + +contract Auxiliar { + + function makeAssetKey(bytes32 key, address asset) external pure returns (bytes32) { + return keccak256(abi.encode(key, asset)); + } + + function makeDomainKey(bytes32 key, uint32 domain) external pure returns (bytes32) { + return keccak256(abi.encode(key, domain)); + } +} diff --git a/harness/CctpMock.sol b/harness/CctpMock.sol new file mode 100644 index 0000000..ff4a5f0 --- /dev/null +++ b/harness/CctpMock.sol @@ -0,0 +1,26 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +pragma solidity ^0.8.21; + +contract CctpMock { + address public localMinter; + uint256 public lastAmount; + uint32 public lastDestinationDomain; + bytes32 public lastMintRecipient; + address public lastToken; + address public lastSender; + bytes4 public lastSig; + uint256 public times; + uint64 public retValue; + + function depositForBurn(uint256 amount, uint32 destinationDomain, bytes32 mintRecipient, address token) external returns (uint64) { + lastAmount = amount; + lastDestinationDomain = destinationDomain; + lastMintRecipient = mintRecipient; + lastToken = token; + lastSender = msg.sender; + lastSig = msg.sig; + times++; + return retValue; + } +} diff --git a/harness/DaiMock.sol b/harness/DaiMock.sol new file mode 100644 index 0000000..97ac691 --- /dev/null +++ b/harness/DaiMock.sol @@ -0,0 +1,22 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +pragma solidity ^0.8.21; + +contract DaiMock { + address public lastTo; + uint256 public lastAmount; + address public lastSender; + bytes4 public lastSig; + uint256 public retValue; + + function balanceOf(address) external view returns (uint256) { + return retValue; + } + + function approve(address to, uint256 amount) external { + lastTo = to; + lastAmount = amount; + lastSender = msg.sender; + lastSig = msg.sig; + } +} diff --git a/harness/DaiUsdsMock.sol b/harness/DaiUsdsMock.sol new file mode 100644 index 0000000..286b716 --- /dev/null +++ b/harness/DaiUsdsMock.sol @@ -0,0 +1,24 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +pragma solidity ^0.8.21; + +contract DaiUsdsMock { + address public lastUsr; + uint256 public lastWad; + address public lastSender; + bytes4 public lastSig; + + function daiToUsds(address usr, uint256 wad) external { + lastUsr = usr; + lastWad = wad; + lastSender = msg.sender; + lastSig = msg.sig; + } + + function usdsToDai(address usr, uint256 wad) external { + lastUsr = usr; + lastWad = wad; + lastSender = msg.sender; + lastSig = msg.sig; + } +} diff --git a/harness/Psm3Mock.sol b/harness/Psm3Mock.sol new file mode 100644 index 0000000..08fab61 --- /dev/null +++ b/harness/Psm3Mock.sol @@ -0,0 +1,30 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +pragma solidity ^0.8.21; + +contract Psm3Mock { + address public lastAsset; + address public lastReceiver; + uint256 public lastAmount; + address public lastSender; + bytes4 public lastSig; + uint256 public retValue; + + function deposit(address asset, address receiver, uint256 amount) external returns (uint256) { + lastAsset = asset; + lastReceiver = receiver; + lastAmount = amount; + lastSender = msg.sender; + lastSig = msg.sig; + return retValue; + } + + function withdraw(address asset, address receiver, uint256 amount) external returns (uint256) { + lastAsset = asset; + lastReceiver = receiver; + lastAmount = amount; + lastSender = msg.sender; + lastSig = msg.sig; + return retValue; + } +} diff --git a/harness/PsmMock.sol b/harness/PsmMock.sol new file mode 100644 index 0000000..6e5eae8 --- /dev/null +++ b/harness/PsmMock.sol @@ -0,0 +1,29 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +pragma solidity ^0.8.21; + +contract PsmMock { + address public lastUsr; + uint256 public lastGemAmount; + address public lastSender; + bytes4 public lastSig; + uint256 public retValue; + + function sellGemNoFee(address usr, uint256 gemAmt) external { + lastUsr = usr; + lastGemAmount = gemAmt; + lastSender = msg.sender; + lastSig = msg.sig; + } + + function buyGemNoFee(address usr, uint256 gemAmt) external { + lastUsr = usr; + lastGemAmount = gemAmt; + lastSender = msg.sender; + lastSig = msg.sig; + } + + function fill() external returns (uint256) { + return retValue; + } +} diff --git a/harness/SUsdsMock.sol b/harness/SUsdsMock.sol new file mode 100644 index 0000000..58377c2 --- /dev/null +++ b/harness/SUsdsMock.sol @@ -0,0 +1,49 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +pragma solidity ^0.8.21; + +contract SUsdsMock { + address public lastTo; + uint256 public lastAmount; + uint256 public lastAssets; + uint256 public lastShares; + address public lastReceiver; + address public lastOwner; + address public lastSender; + bytes4 public lastSig; + uint256 public retValue; + + function approve(address to, uint256 amount) external returns (bool) { + lastTo = to; + lastAmount = amount; + lastSender = msg.sender; + lastSig = msg.sig; + return true; + } + + function deposit(uint256 assets, address receiver) external returns (uint256) { + lastAssets = assets; + lastReceiver = receiver; + lastSender = msg.sender; + lastSig = msg.sig; + return retValue; + } + + function withdraw(uint256 assets, address receiver, address owner) external returns (uint256) { + lastAssets = assets; + lastReceiver = receiver; + lastOwner = owner; + lastSender = msg.sender; + lastSig = msg.sig; + return retValue; + } + + function redeem(uint256 shares, address receiver, address owner) external returns (uint256) { + lastShares = shares; + lastReceiver = receiver; + lastOwner = owner; + lastSender = msg.sender; + lastSig = msg.sig; + return retValue; + } +} diff --git a/harness/UsdcMock.sol b/harness/UsdcMock.sol new file mode 100644 index 0000000..084cc09 --- /dev/null +++ b/harness/UsdcMock.sol @@ -0,0 +1,18 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +pragma solidity ^0.8.21; + +contract UsdcMock { + address public lastTo; + uint256 public lastAmount; + address public lastSender; + bytes4 public lastSig; + + function approve(address to, uint256 amount) external returns (bool) { + lastTo = to; + lastAmount = amount; + lastSender = msg.sender; + lastSig = msg.sig; + return true; + } +} diff --git a/harness/UsdsMock.sol b/harness/UsdsMock.sol new file mode 100644 index 0000000..1d0eeb4 --- /dev/null +++ b/harness/UsdsMock.sol @@ -0,0 +1,37 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +pragma solidity ^0.8.21; + +contract UsdsMock { + address public lastFrom; + address public lastTo; + uint256 public lastAmount; + address public lastSender; + bytes4 public lastSig; + + function approve(address to, uint256 amount) external returns (bool) { + lastTo = to; + lastAmount = amount; + lastSender = msg.sender; + lastSig = msg.sig; + return true; + } + + function transferFrom(address from, address to, uint256 amount) external returns (bool) { + lastFrom = from; + lastTo = to; + lastAmount = amount; + lastSender = msg.sender; + lastSig = msg.sig; + return true; + } + + function transfer(address to, uint256 amount) external returns (bool) { + lastFrom = msg.sender; + lastTo = to; + lastAmount = amount; + lastSender = msg.sender; + lastSig = msg.sig; + return true; + } +} diff --git a/spark-alm-controller b/spark-alm-controller new file mode 160000 index 0000000..25447fa --- /dev/null +++ b/spark-alm-controller @@ -0,0 +1 @@ +Subproject commit 25447fa679521dc2ec4e37de8f820bee7c01cd4f