enhances rules about module and transaction guards to include the proposition that the correct guard is called

Author: Derek Sorensen

certora/conf/v1.5/guards.conf

@@ -3,7 +3,9 @@
     "files": [
         "certora/harnesses/SafeHarness.sol",
         "certora/mocks/ModuleGuardMock.sol", // a module guard 
+        "certora/mocks/ModuleGuardMockDuplicate.sol",
         "certora/mocks/TxnGuardMock.sol", // a (safe) guard
+        "certora/mocks/TxnGuardMockDuplicate.sol",
     ],
     "link": [
 

certora/mocks/ModuleGuardMockDuplicate.sol

@@ -0,0 +1,71 @@
+// SPDX-License-Identifier: LGPL-3.0-only
+/* solhint-disable one-contract-per-file */
+pragma solidity >=0.7.0 <0.9.0;
+import {IModuleGuard} from "../munged/base/ModuleManager.sol";
+import {IERC165} from "../munged/interfaces/IERC165.sol";
+import "../munged/libraries/Enum.sol";
+
+contract ModuleGuardMockDuplicate is IModuleGuard {
+
+    constructor(){
+        preCheckedTransactions = false ;
+        postCheckedTransactions = false ;
+    }
+
+    // some mock variables 
+    bool public preCheckedTransactions ;
+    bool public postCheckedTransactions ;
+
+    function resetChecks() external {
+        preCheckedTransactions = false ;
+        postCheckedTransactions = false ;
+    }
+
+    /**
+     * @notice Checks the module transaction details.
+     * @dev The function needs to implement module transaction validation logic.
+     * @param to The address to which the transaction is intended.
+     * @param value The value of the transaction in Wei.
+     * @param data The transaction data.
+     * @param operation The type of operation of the module transaction.
+     * @param module The module involved in the transaction.
+     * @return moduleTxHash The hash of the module transaction.
+     */
+    function checkModuleTransaction(
+        address to,
+        uint256 value,
+        bytes memory data,
+        Enum.Operation operation,
+        address module
+    ) external override returns (bytes32 moduleTxHash) {
+        // updates transaction checked
+        preCheckedTransactions = true ;
+        // if it passes, it returns a string of bytes
+        return bytes32(0);
+    }
+
+    /**
+     * @notice Checks after execution of module transaction.
+     * @dev The function needs to implement a check after the execution of the module transaction.
+     * @param txHash The hash of the module transaction.
+     * @param success The status of the module transaction execution.
+     */
+    function checkAfterModuleExecution(bytes32 txHash, bool success) external override {
+        postCheckedTransactions = true;
+    }
+
+    /**
+     * @dev Returns true if this contract implements the interface defined by `interfaceId`.
+     * See the corresponding EIP section
+     * https://eips.ethereum.org/EIPS/eip-165#how-interfaces-are-identified
+     * to learn more about how these ids are created.
+     *
+     * This function call must use less than 30 000 gas.
+     */
+    function supportsInterface(bytes4 interfaceId) external view virtual override returns (bool) {
+        return
+            interfaceId == type(IModuleGuard).interfaceId || // 0x58401ed8
+            interfaceId == type(IERC165).interfaceId; // 0x01ffc9a7
+    }
+
+}

certora/mocks/TxnGuardMockDuplicate.sol

@@ -0,0 +1,78 @@
+// SPDX-License-Identifier: LGPL-3.0-only
+/* solhint-disable one-contract-per-file */
+pragma solidity >=0.7.0 <0.9.0;
+import {ITransactionGuard} from "../munged/base/GuardManager.sol";
+import {IERC165} from "../munged/interfaces/IERC165.sol";
+import "../munged/libraries/Enum.sol";
+
+contract TxnGuardMockDuplicate is ITransactionGuard {
+
+    constructor(){}
+
+    // some mock variables 
+    bool public preCheckedTransactions ;
+    bool public postCheckedTransactions ;
+
+    function resetChecks() external {
+        preCheckedTransactions = false ;
+        postCheckedTransactions = false ;
+    }
+
+    /**
+     * @notice Checks the transaction details.
+     * @dev The function needs to implement transaction validation logic.
+     * @param to The address to which the transaction is intended.
+     * @param value The value of the transaction in Wei.
+     * @param data The transaction data.
+     * @param operation The type of operation of the transaction.
+     * @param safeTxGas Gas used for the transaction.
+     * @param baseGas The base gas for the transaction.
+     * @param gasPrice The price of gas in Wei for the transaction.
+     * @param gasToken The token used to pay for gas.
+     * @param refundReceiver The address which should receive the refund.
+     * @param signatures The signatures of the transaction.
+     * @param msgSender The address of the message sender.
+     */
+    function checkTransaction(
+        address to,
+        uint256 value,
+        bytes memory data,
+        Enum.Operation operation,
+        uint256 safeTxGas,
+        uint256 baseGas,
+        uint256 gasPrice,
+        address gasToken,
+        address payable refundReceiver,
+        bytes memory signatures,
+        address msgSender
+    ) external override {
+        // updates transaction checked
+        preCheckedTransactions = true;
+    }
+
+    /**
+     * @notice Checks after execution of the transaction.
+     * @dev The function needs to implement a check after the execution of the transaction.
+     * @param hash The hash of the transaction.
+     * @param success The status of the transaction execution.
+     */
+    function checkAfterExecution(bytes32 hash, bool success) external override {
+        // updates transaction checked
+        postCheckedTransactions = true ;
+    }
+
+    /**
+     * @dev Returns true if this contract implements the interface defined by `interfaceId`.
+     * See the corresponding EIP section
+     * https://eips.ethereum.org/EIPS/eip-165#how-interfaces-are-identified
+     * to learn more about how these ids are created.
+     *
+     * This function call must use less than 30 000 gas.
+     */
+    function supportsInterface(bytes4 interfaceId) external view virtual override returns (bool) {
+        return
+            interfaceId == type(ITransactionGuard).interfaceId || // 0xe6d7a83a
+            interfaceId == type(IERC165).interfaceId; // 0x01ffc9a7
+    }
+
+}

certora/specs/v1.5/Guards.spec

@@ -1,7 +1,9 @@
 /* A specification of the safe guard and module guard */
 
 using ModuleGuardMock as modGuardMock;
+using ModuleGuardMockDuplicate as modGuardMock2;
 using TxnGuardMock as txnGuardMock;
+using TxnGuardMockDuplicate as txnGuardMock2;
 using SafeHarness as safe;
 
 // ---- Methods block ----------------------------------------------------------
@@ -140,7 +142,7 @@ rule setModuleGuardReentrant(address guard) {
 
 
 /// @dev the transaction guard gets called both pre- and post- any execTransaction
-/// @status Done: https://prover.certora.com/output/39601/a05e24787c68404d877ae4acce693734?anonymousKey=02030d2ca97a19d0d7a70deb5a91dc4b75bca89d
+/// @status Done: https://prover.certora.com/output/39601/a9a8eaeba7994e10bf29dbe8813798b9?anonymousKey=fbddda2f78b44a7df3dff4707715b90b2d08ab63
 rule txnGuardCalled(
     address to,
     uint256 value,
@@ -157,19 +159,24 @@ rule txnGuardCalled(
     // the txn guard is the mock
     require (getSafeGuard() == txnGuardMock);
 
-    // execTxn passes
+    txnGuardMock.resetChecks(e); // reset the check triggers
+    txnGuardMock2.resetChecks(e);
+
     execTransaction(e,to,value,data,operation,safeTxGas,baseGas,
         gasPrice,gasToken,refundReceiver,signatures);
 
     // the pre- and post- module transaction guards were called
     assert (
         txnGuardMock.preCheckedTransactions() && 
-        txnGuardMock.postCheckedTransactions()
+        txnGuardMock.postCheckedTransactions() &&
+        // the right guard was called
+        !txnGuardMock2.preCheckedTransactions(e) && 
+        !txnGuardMock2.postCheckedTransactions(e)
     );
 }
 
 /// @dev the module guard gets called both pre- and post- any execTransactionFromModule
-/// @status Done: https://prover.certora.com/output/39601/a05e24787c68404d877ae4acce693734?anonymousKey=02030d2ca97a19d0d7a70deb5a91dc4b75bca89d
+/// @status Done: https://prover.certora.com/output/39601/7591e8c61e6d407b847e38bbe8238e13?anonymousKey=5d99429f5046e77825a4ed015af0a6a0d088538d
 rule moduleGuardCalled(
         address to,
         uint256 value,
@@ -180,17 +187,22 @@ rule moduleGuardCalled(
     require (getModuleGuardExternal() == modGuardMock);
 
     modGuardMock.resetChecks(e); // reset the check triggers
+    modGuardMock2.resetChecks(e);
+    
     execTransactionFromModule(e,to,value,data,operation);
 
     // the pre- and post- module transaction guards were called
     assert (
         modGuardMock.preCheckedTransactions() && 
-        modGuardMock.postCheckedTransactions()
+        modGuardMock.postCheckedTransactions() &&
+        // the correct guard was called
+        !modGuardMock2.preCheckedTransactions(e) && 
+        !modGuardMock2.postCheckedTransactions(e)
     );
 }
 
 /// @dev the module guard gets called both pre- and post- any execTransactionFromModuleReturnData
-/// @status Done: https://prover.certora.com/output/39601/15cfd3430d794986a26d304c9e2fbc6e?anonymousKey=92f0976aba6cb3fe40cf6c728d34b140a438bbae
+/// @status Done: https://prover.certora.com/output/39601/2de5a471d628464e8aaf4b9022e515de?anonymousKey=c4997fd77ba3808cf9bdc6a432f9b20eea551c95
 rule moduleGuardCalledReturn(
         address to,
         uint256 value,
@@ -201,12 +213,17 @@ rule moduleGuardCalledReturn(
     require (getModuleGuardExternal() == modGuardMock);
 
     modGuardMock.resetChecks(e); // reset the check triggers
+    modGuardMock2.resetChecks(e);
+
     execTransactionFromModuleReturnData(e,to,value,data,operation);
 
     // the pre- and post- module transaction guards were called
     assert (
         modGuardMock.preCheckedTransactions() && 
-        modGuardMock.postCheckedTransactions()
+        modGuardMock.postCheckedTransactions() &&
+        // the correct guard was called
+        !modGuardMock2.preCheckedTransactions(e) && 
+        !modGuardMock2.postCheckedTransactions(e)
     );
 }