makerdao · hexonaut · Jul 28, 2022 · Jul 28, 2022 · Jul 28, 2022 · Jul 28, 2022
diff --git a/.gitmodules b/.gitmodules
@@ -1,3 +1,3 @@
-[submodule "lib/ds-test"]
-	path = lib/ds-test
-	url = https://github.com/dapphub/ds-test
+[submodule "lib/forge-std"]
+	path = lib/forge-std
+	url = https://github.com/foundry-rs/forge-std
diff --git a/Makefile b/Makefile
@@ -1,9 +1,9 @@
 all             :; FOUNDRY_OPTIMIZER=true FOUNDRY_OPTIMIZER_RUNS=200 forge build --use solc:0.8.15
 clean           :; forge clean
-test            :; ./test.sh $(match) $(runs)
-cov             :; rm -rf coverage && mkdir coverage && forge coverage --report lcov && lcov -r lcov.info 'src/test/*' 'src/utils/*' -o lcov.info && genhtml lcov.info --output-directory coverage
-certora-con-fee :; certoraRun --solc ~/.solc-select/artifacts/solc-0.8.15/solc-0.8.15 --optimize_map TeleportConstantFee=200 --rule_sanity basic src/TeleportConstantFee.sol --verify TeleportConstantFee:certora/TeleportConstantFee.spec $(if $(rule),--rule $(rule),) --multi_assert_check --short_output
-certora-lin-fee :; certoraRun --solc ~/.solc-select/artifacts/solc-0.8.15/solc-0.8.15 --optimize_map TeleportLinearFee=200 --rule_sanity basic src/TeleportLinearFee.sol --verify TeleportLinearFee:certora/TeleportLinearFee.spec $(if $(rule),--rule $(rule),) --multi_assert_check --short_output
-certora-join    :; certoraRun --solc ~/.solc-select/artifacts/solc-0.8.15/solc-0.8.15 --optimize_map TeleportJoin=200,FeesMock=0,Auxiliar=0,VatMock=0,DaiMock=0,DaiJoinMock=0 --rule_sanity basic src/TeleportJoin.sol certora/FeesMock.sol certora/Auxiliar.sol src/test/mocks/VatMock.sol src/test/mocks/DaiMock.sol src/test/mocks/DaiJoinMock.sol --link TeleportJoin:vat=VatMock TeleportJoin:daiJoin=DaiJoinMock DaiJoinMock:vat=VatMock DaiJoinMock:dai=DaiMock --verify TeleportJoin:certora/TeleportJoin.spec $(if $(rule),--rule $(rule),) --multi_assert_check --short_output --settings -optimisticUnboundedHashing=true,-mediumTimeout=30
-certora-router  :; certoraRun --solc ~/.solc-select/artifacts/solc-0.8.15/solc-0.8.15 --optimize_map TeleportRouter=200,TeleportJoinMock=0,DaiMock=0 --rule_sanity basic src/TeleportRouter.sol certora/TeleportJoinMock.sol src/test/mocks/DaiMock.sol --link TeleportRouter:dai=DaiMock --verify TeleportRouter:certora/TeleportRouter.spec $(if $(rule),--rule $(rule),) --multi_assert_check --short_output
-certora-oracle  :; certoraRun --solc ~/.solc-select/artifacts/solc-0.8.15/solc-0.8.15 --optimize_map TeleportOracleAuth=200,TeleportJoinMock=0,Auxiliar=0 --rule_sanity basic src/TeleportOracleAuth.sol certora/TeleportJoinMock.sol certora/Auxiliar.sol --link TeleportOracleAuth:teleportJoin=TeleportJoinMock Auxiliar:oracle=TeleportOracleAuth --verify TeleportOracleAuth:certora/TeleportOracleAuth.spec --loop_iter 10 --optimistic_loop $(if $(rule),--rule $(rule),) --multi_assert_check --short_output
+test            :; ./test.sh $(match)
+cov				:; rm -rf coverage && mkdir coverage && forge coverage --report lcov && lcov -r lcov.info 'src/test/*' 'src/utils/*' -o lcov.info && genhtml lcov.info --output-directory coverage
+certora-con-fee :; PATH=~/.solc-select/artifacts/solc-0.8.15:${PATH} certoraRun --solc_map TeleportConstantFee=solc-0.8.15 --optimize_map TeleportConstantFee=200 --rule_sanity basic src/TeleportConstantFee.sol --verify TeleportConstantFee:certora/TeleportConstantFee.spec $(if $(rule),--rule $(rule),) --multi_assert_check --short_output
+certora-lin-fee :; PATH=~/.solc-select/artifacts/solc-0.8.15:${PATH} certoraRun --solc_map TeleportLinearFee=solc-0.8.15 --optimize_map TeleportLinearFee=200 --rule_sanity basic src/TeleportLinearFee.sol --verify TeleportLinearFee:certora/TeleportLinearFee.spec $(if $(rule),--rule $(rule),) --multi_assert_check --short_output
+certora-join    :; PATH=~/.solc-select/artifacts/solc-0.8.15:${PATH} certoraRun --solc_map TeleportJoin=solc-0.8.15,FeesMock=solc-0.8.15,Auxiliar=solc-0.8.15,VatMock=solc-0.8.15,DaiMock=solc-0.8.15,DaiJoinMock=solc-0.8.15 --optimize_map TeleportJoin=200,FeesMock=0,Auxiliar=0,VatMock=0,DaiMock=0,DaiJoinMock=0 --rule_sanity basic src/TeleportJoin.sol certora/FeesMock.sol certora/Auxiliar.sol src/test/mocks/VatMock.sol src/test/mocks/DaiMock.sol src/test/mocks/DaiJoinMock.sol --link TeleportJoin:vat=VatMock TeleportJoin:daiJoin=DaiJoinMock DaiJoinMock:vat=VatMock DaiJoinMock:dai=DaiMock --verify TeleportJoin:certora/TeleportJoin.spec $(if $(rule),--rule $(rule),) --multi_assert_check --short_output --settings -optimisticUnboundedHashing=true,-mediumTimeout=30
+certora-router  :; PATH=~/.solc-select/artifacts/solc-0.8.15:${PATH} certoraRun --solc_map TeleportRouter=solc-0.8.15,GatewayMock=solc-0.8.15,DaiMock=solc-0.8.15,Auxiliar=solc-0.8.15 --optimize_map TeleportRouter=200,GatewayMock=0,DaiMock=0,Auxiliar=0 --rule_sanity basic src/TeleportRouter.sol certora/GatewayMock.sol src/test/mocks/DaiMock.sol certora/Auxiliar.sol --link TeleportRouter:dai=DaiMock --verify TeleportRouter:certora/TeleportRouter.spec $(if $(rule),--rule $(rule),) --multi_assert_check --short_output
+certora-oracle  :; PATH=~/.solc-select/artifacts/solc-0.8.15:${PATH} certoraRun --solc_map TeleportOracleAuth=solc-0.8.15,TeleportJoinMock=solc-0.8.15,Auxiliar=solc-0.8.15 --optimize_map TeleportOracleAuth=200,TeleportJoinMock=0,Auxiliar=0 --rule_sanity basic src/TeleportOracleAuth.sol certora/TeleportJoinMock.sol certora/Auxiliar.sol --link TeleportOracleAuth:teleportJoin=TeleportJoinMock Auxiliar:oracle=TeleportOracleAuth --verify TeleportOracleAuth:certora/TeleportOracleAuth.spec --loop_iter 10 --optimistic_loop $(if $(rule),--rule $(rule),) --multi_assert_check --short_output
diff --git a/certora/Auxiliar.sol b/certora/Auxiliar.sol
@@ -32,6 +32,10 @@ contract Auxiliar {
         ));
     }
 
+    function addressToBytes32(address addr) external pure returns (bytes32) {
+        return bytes32(uint256(uint160(addr)));
+    }
+
     function bytes32ToAddress(bytes32 addr) external pure returns (address) {
         return address(uint160(uint256(addr)));
     }

diff --git a/certora/GatewayMock.sol b/certora/GatewayMock.sol
@@ -0,0 +1,23 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+pragma solidity 0.8.15;
+
+import "../src/TeleportGUID.sol";
+
+contract GatewayMock {
+    TeleportGUID public teleportGUID;
+    bytes32 public sourceDomain;
+    bytes32 public targetDomain;
+    uint256 public amount;
+
+    function registerMint(
+        TeleportGUID memory teleportGUID_
+    ) external {
+        teleportGUID = teleportGUID_;
+    }
+
+    function settle(bytes32 sourceDomain_, bytes32 targetDomain_, uint256 amount_) external {
+        sourceDomain = sourceDomain_;
+        targetDomain = targetDomain_;
+        amount = amount_;
+    }
+}
diff --git a/certora/TeleportJoin.spec b/certora/TeleportJoin.spec
@@ -265,6 +265,62 @@ definition operatorFeeAmt(bool canGenerate, uint256 operatorFee)
                         :
                             0;
 
+// Verify that registerMint behaves correctly
+rule registerMint(
+        join.TeleportGUID guid
+    ) {
+    env e;
+
+    bytes32 hashGUID = aux.getGUIDHash(guid);
+
+    bool    blessedBefore;
+    uint248 pendingBefore;
+    blessedBefore, pendingBefore = teleports(hashGUID);
+
+    registerMint(e, guid);
+
+    bool    blessedAfter;
+    uint248 pendingAfter;
+    blessedAfter, pendingAfter = teleports(hashGUID);
+
+    assert(blessedBefore == false, "blessed before call should be false");
+    assert(blessedAfter == true, "blessed after call should be true");
+    assert(pendingAfter == guid.amount, "pending has not acted as expected");
+}
+
+// Verify revert rules on registerMint
+rule registerMint_revert(
+        join.TeleportGUID guid
+    ) {
+    env e;
+
+    uint256 ward = wards(e.msg.sender);
+
+    bytes32 hashGUID = aux.getGUIDHash(guid);
+
+    bytes32 domain = domain();
+
+    bool vatLive = vat.live() == 1;
+    uint256 line = vatLive ? line(guid.sourceDomain): 0;
+    int256 debt = debt(guid.sourceDomain);
+
+    bool    blessed;
+    uint248 pending;
+    blessed, pending = teleports(hashGUID);
+
+    registerMint@withrevert(e, guid);
+
+    bool revert1  = e.msg.value > 0;
+    bool revert2  = ward != 1;
+    bool revert3  = blessed;
+
+    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 that requestMint behaves correctly
 rule requestMint(
         join.TeleportGUID guid,
@@ -665,7 +721,7 @@ rule mintPending_revert(
                            revert22 || revert23 || revert24, "Revert rules are not covering all the cases");
 }
 
-rule settle(bytes32 sourceDomain, uint256 batchedDaiToFlush) {
+rule settle(bytes32 sourceDomain, bytes32 targetDomain, uint256 amount) {
     env e;
 
     bool vatLive = vat.live() == 1;
@@ -679,9 +735,9 @@ rule settle(bytes32 sourceDomain, uint256 batchedDaiToFlush) {
 
     uint256 vatDaiJoinBefore = vat.dai(currentContract);
 
-    uint256 amtToPayBack = batchedDaiToFlush <= artBefore ? batchedDaiToFlush : artBefore;
+    uint256 amtToPayBack = amount <= artBefore ? amount : artBefore;
 
-    settle(e, sourceDomain, batchedDaiToFlush);
+    settle(e, sourceDomain, targetDomain, amount);
 
     int256 debtAfter = debt(sourceDomain);
 
@@ -693,24 +749,26 @@ rule settle(bytes32 sourceDomain, uint256 batchedDaiToFlush) {
 
     uint256 vatDaiJoinAfter = vat.dai(currentContract);
 
-    assert(to_mathint(debtAfter) == to_mathint(debtBefore) - to_mathint(batchedDaiToFlush), "debt has not decreased as expected");
+    assert(to_mathint(debtAfter) == to_mathint(debtBefore) - to_mathint(amount), "debt has not decreased as expected");
     assert(vatLive => inkAfter == inkBefore - amtToPayBack, "ink has not decreased as expected");
     assert(vatLive => artAfter == artBefore - amtToPayBack, "art has not decreased as expected");
     assert(!vatLive => inkAfter == inkBefore, "ink has not stayed the same as expected");
     assert(!vatLive => artAfter == artBefore, "art has not stayed the same as expected");
     assert(vatLive => cureAfter == (artBefore - amtToPayBack) * RAY(), "cure has not been updated as expected");
     assert(!vatLive => cureAfter == cureBefore, "cure has not stayed the same as expected");
-    assert(vatLive => vatDaiJoinAfter == vatDaiJoinBefore + (batchedDaiToFlush - amtToPayBack) * RAY(), "join vat dai has not increased as expected 1");
-    assert(!vatLive => vatDaiJoinAfter == vatDaiJoinBefore + batchedDaiToFlush * RAY(), "join vat dai has not increased as expected 2");
+    assert(vatLive => vatDaiJoinAfter == vatDaiJoinBefore + (amount - amtToPayBack) * RAY(), "join vat dai has not increased as expected 1");
+    assert(!vatLive => vatDaiJoinAfter == vatDaiJoinBefore + amount * RAY(), "join vat dai has not increased as expected 2");
 }
 
-rule settle_revert(bytes32 sourceDomain, uint256 batchedDaiToFlush) {
+rule settle_revert(bytes32 sourceDomain, bytes32 targetDomain, uint256 amount) {
     env e;
 
     require(vat() == vat);
     require(daiJoin.vat() == vat);
     require(daiJoin.dai() == dai);
 
+    bytes32 domain = domain();
+
     bool vatLive = vat.live() == 1;
 
     int256 debt = debt(sourceDomain);
@@ -727,21 +785,22 @@ rule settle_revert(bytes32 sourceDomain, uint256 batchedDaiToFlush) {
     uint256 daiBalJoin = dai.balanceOf(currentContract);
     uint256 daiAllJoinDaiJoin = dai.allowance(currentContract, daiJoin);
 
-    uint256 amtToPayBack = batchedDaiToFlush <= art ? batchedDaiToFlush : art;
+    uint256 amtToPayBack = amount <= art ? amount : art;
 
-    settle@withrevert(e, sourceDomain, batchedDaiToFlush);
+    settle@withrevert(e, sourceDomain, targetDomain, amount);
 
     bool revert1  = e.msg.value > 0;
-    bool revert2  = batchedDaiToFlush > max_int256();
-    bool revert3  = batchedDaiToFlush * RAY() > max_uint256;
-    bool revert4  = batchedDaiToFlush * RAY() > vatDaiDaiJoin;
-    bool revert5  = vatDaiJoin + batchedDaiToFlush * RAY() > max_uint256;
-    bool revert6  = daiBalJoin < batchedDaiToFlush;
-    bool revert7  = daiAllJoinDaiJoin < batchedDaiToFlush;
-    bool revert8  = vatLive && amtToPayBack > 0 && -1 * to_mathint(amtToPayBack) * RAY() < min_int256();
-    bool revert9  = vatLive && amtToPayBack > ink;
-    bool revert10 = vatLive && vatGemJoin + amtToPayBack > max_uint256;
-    bool revert11 = to_mathint(debt) - to_mathint(batchedDaiToFlush) < min_int256();
+    bool revert2  = targetDomain != domain;
+    bool revert3  = amount > max_int256();
+    bool revert4  = amount * RAY() > max_uint256;
+    bool revert5  = amount * RAY() > vatDaiDaiJoin;
+    bool revert6  = vatDaiJoin + amount * RAY() > max_uint256;
+    bool revert7  = daiBalJoin < amount;
+    bool revert8  = daiAllJoinDaiJoin < amount;
+    bool revert9  = vatLive && amtToPayBack > 0 && -1 * to_mathint(amtToPayBack) * RAY() < min_int256();
+    bool revert10 = vatLive && amtToPayBack > ink;
+    bool revert11 = vatLive && vatGemJoin + amtToPayBack > max_uint256;
+    bool revert12 = to_mathint(debt) - to_mathint(amount) < min_int256();
 
     assert(revert1  => lastReverted, "revert1 failed");
     assert(revert2  => lastReverted, "revert2 failed");
@@ -754,9 +813,10 @@ rule settle_revert(bytes32 sourceDomain, uint256 batchedDaiToFlush) {
     assert(revert9  => lastReverted, "revert9 failed");
     assert(revert10 => lastReverted, "revert10 failed");
     assert(revert11 => lastReverted, "revert11 failed");
+    assert(revert12 => lastReverted, "revert12 failed");
 
     assert(lastReverted => revert1  || revert2  || revert3  ||
                            revert4  || revert5  || revert6  ||
                            revert7  || revert8  || revert9  ||
-                           revert10 || revert11, "Revert rules are not covering all the cases");
+                           revert10 || revert11 || revert12, "Revert rules are not covering all the cases");
 }
diff --git a/certora/TeleportJoinMock.sol b/certora/TeleportJoinMock.sol
@@ -9,8 +9,6 @@ contract TeleportJoinMock {
     uint256 public operatorFee;
     uint256 public postFeeAmount;
     uint256 public totalFee;
-    bytes32 public sourceDomain;
-    uint256 public batchedDaiToFlush;
 
     function requestMint(
         TeleportGUID memory teleportGUID_,
@@ -23,9 +21,4 @@ contract TeleportJoinMock {
         postFeeAmount_ = postFeeAmount;
         totalFee_ = totalFee;
     }
-
-    function settle(bytes32 sourceDomain_, uint256 batchedDaiToFlush_) external {
-        sourceDomain = sourceDomain_;
-        batchedDaiToFlush = batchedDaiToFlush_;
-    }
 }