Reducing Safe Contract Code Size

certora/harnesses/SafeHarness.sol

@@ -16,18 +16,18 @@ contract SafeHarness is Safe {
     }
 
     // harnessed functions
-    function signatureSplitPublic(bytes memory signatures, uint256 pos) public pure returns (uint8 v, bytes32 r, bytes32 s) {
+    function signatureSplitPublic(bytes memory signatures, uint256 pos) public pure returns (uint256 v, bytes32 r, bytes32 s) {
         require(signatures.length >= 65 * (pos + 1));
         return signatureSplit(signatures, pos);
     }
 
-    function getCurrentOwner(bytes32 dataHash, uint8 v, bytes32 r, bytes32 s) public pure returns (address currentOwner) {
+    function getCurrentOwner(bytes32 dataHash, uint256 v, bytes32 r, bytes32 s) public pure returns (address currentOwner) {
         if (v == 0 || v == 1) {
             currentOwner = address(uint160(uint256(r)));
         } else if (v > 30) {
-            currentOwner = ecrecover(keccak256(abi.encodePacked("\x19Ethereum Signed Message:\n32", dataHash)), v - 4, r, s);
+            currentOwner = ecrecover(keccak256(abi.encodePacked("\x19Ethereum Signed Message:\n32", dataHash)), uint8(v - 4), r, s);
         } else {
-            currentOwner = ecrecover(dataHash, v, r, s);
+            currentOwner = ecrecover(dataHash, uint8(v), r, s);
         }
     }
 

certora/specs/Signatures.spec

@@ -4,13 +4,13 @@ methods {
     function isOwner(address) external returns (bool) envfree;
 
     // harnessed
-    function signatureSplitPublic(bytes,uint256) external returns (uint8,bytes32,bytes32) envfree;
-    function getCurrentOwner(bytes32, uint8, bytes32, bytes32) external returns (address) envfree;
+    function signatureSplitPublic(bytes,uint256) external returns (uint256,bytes32,bytes32) envfree;
+    function getCurrentOwner(bytes32, uint256, bytes32, bytes32) external returns (address) envfree;
     function getTransactionHashPublic(address, uint256, bytes, Enum.Operation, uint256, uint256, uint256, address, address, uint256) external returns (bytes32) envfree;
     // needed for the getTransactionHash ghost for the execTransaction <> signatures rule
 
     // summaries
-    function SignatureDecoder.signatureSplit(bytes memory signatures, uint256 pos) internal returns (uint8,bytes32,bytes32) => signatureSplitGhost(signatures,pos);
+    function SignatureDecoder.signatureSplit(bytes memory signatures, uint256 pos) internal returns (uint256,bytes32,bytes32) => signatureSplitGhost(signatures,pos);
     function Safe.checkContractSignature(address, bytes32, bytes memory, uint256) internal => NONDET;
     // needed for the execTransaction <> signatures rule
     function Safe.getTransactionHash(
@@ -33,7 +33,7 @@ methods {
 
 definition MAX_UINT256() returns uint256 = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff;
 
-ghost mapping(bytes => mapping(uint256 => uint8)) mySigSplitV;
+ghost mapping(bytes => mapping(uint256 => uint256)) mySigSplitV;
 ghost mapping(bytes => mapping(uint256 => bytes32)) mySigSplitR;
 ghost mapping(bytes => mapping(uint256 => bytes32)) mySigSplitS;
 
@@ -50,7 +50,7 @@ ghost transactionHashGhost(
         address /*refundReceiver*/,
         uint256 /*_nonce*/ ) returns bytes32 ;
 
-function signatureSplitGhost(bytes signatures, uint256 pos) returns (uint8,bytes32,bytes32) {
+function signatureSplitGhost(bytes signatures, uint256 pos) returns (uint256,bytes32,bytes32) {
     return (mySigSplitV[signatures][pos], mySigSplitR[signatures][pos], mySigSplitS[signatures][pos]);
 }
 
@@ -63,10 +63,10 @@ rule checkSignatures() {
     bytes signaturesAB;
     bytes signaturesA;
     bytes signaturesB;
-    uint8 vA; bytes32 rA; bytes32 sA;
-    uint8 vB; bytes32 rB; bytes32 sB;
-    uint8 vAB1; bytes32 rAB1; bytes32 sAB1;
-    uint8 vAB2; bytes32 rAB2; bytes32 sAB2;
+    uint256 vA; bytes32 rA; bytes32 sA;
+    uint256 vB; bytes32 rB; bytes32 sB;
+    uint256 vAB1; bytes32 rAB1; bytes32 sAB1;
+    uint256 vAB2; bytes32 rAB2; bytes32 sAB2;
     vA, rA, sA = signatureSplitPublic(signaturesA, 0);
     vB, rB, sB = signatureSplitPublic(signaturesB, 0);
     vAB1, rAB1, sAB1 = signatureSplitPublic(signaturesAB, 0);

contracts/Safe.sol

@@ -192,7 +192,7 @@ contract Safe is
 
         // We require some gas to emit the events (at least 2500) after the execution and some to perform code until the execution (500)
         // We also include the 1/64 in the check that is not send along with a call to counteract potential shortings because of EIP-150
-        require(gasleft() >= ((safeTxGas * 64) / 63).max(safeTxGas + 2500) + 500, "GS010");
+        if (gasleft() < ((safeTxGas * 64) / 63).max(safeTxGas + 2500) + 500) revertWithError("GS010");
         // Use scope here to limit variable lifetime and prevent `stack too deep` errors
         {
             uint256 gasUsed = gasleft();
@@ -202,7 +202,7 @@ contract Safe is
             gasUsed = gasUsed.sub(gasleft());
             // If no safeTxGas and no gasPrice was set (e.g. both are 0), then the internal tx is required to be successful
             // This makes it possible to use `estimateGas` without issues, as it searches for the minimum gas where the tx doesn't revert
-            require(success || safeTxGas != 0 || gasPrice != 0, "GS013");
+            if (!success && safeTxGas == 0 && gasPrice == 0) revertWithError("GS013");
             // We transfer the calculated tx costs to the tx.origin to avoid sending it to intermediate contracts that have made calls
             uint256 payment = 0;
             if (gasPrice > 0) {
@@ -239,10 +239,10 @@ contract Safe is
             // For native tokens, we will only adjust the gas price to not be higher than the actually used gas price
             payment = gasUsed.add(baseGas).mul(gasPrice < tx.gasprice ? gasPrice : tx.gasprice);
             (bool refundSuccess, ) = receiver.call{value: payment}("");
-            require(refundSuccess, "GS011");
+            if (!refundSuccess) revertWithError("GS011");
         } else {
             payment = gasUsed.add(baseGas).mul(gasPrice);
-            require(transferToken(gasToken, receiver, payment), "GS012");
+            if (!transferToken(gasToken, receiver, payment)) revertWithError("GS012");
         }
     }
 
@@ -257,7 +257,7 @@ contract Safe is
      */
     function checkContractSignature(address owner, bytes32 dataHash, bytes memory signatures, uint256 offset) internal view {
         // Check that signature data pointer (s) is in bounds (points to the length of data -> 32 bytes)
-        require(offset.add(32) <= signatures.length, "GS022");
+        if (offset.add(32) > signatures.length) revertWithError("GS022");
 
         // Check if the contract signature is in bounds: start of data is s + 32 and end is start + signature length
         uint256 contractSignatureLen;
@@ -267,7 +267,7 @@ contract Safe is
             contractSignatureLen := mload(add(add(signatures, offset), 0x20))
         }
         /* solhint-enable no-inline-assembly */
-        require(offset.add(32).add(contractSignatureLen) <= signatures.length, "GS023");
+        if (offset.add(32).add(contractSignatureLen) > signatures.length) revertWithError("GS023");
 
         // Check signature
         bytes memory contractSignature;
@@ -279,7 +279,7 @@ contract Safe is
         }
         /* solhint-enable no-inline-assembly */
 
-        require(ISignatureValidator(owner).isValidSignature(dataHash, contractSignature) == EIP1271_MAGIC_VALUE, "GS024");
+        if (ISignatureValidator(owner).isValidSignature(dataHash, contractSignature) != EIP1271_MAGIC_VALUE) revertWithError("GS024");
     }
 
     /**
@@ -292,7 +292,7 @@ contract Safe is
         // Load threshold to avoid multiple storage loads
         uint256 _threshold = threshold;
         // Check that a threshold is set
-        require(_threshold > 0, "GS001");
+        if (_threshold == 0) revertWithError("GS001");
         checkNSignatures(msg.sender, dataHash, signatures, _threshold);
     }
 
@@ -309,11 +309,11 @@ contract Safe is
      */
     function checkNSignatures(address executor, bytes32 dataHash, bytes memory signatures, uint256 requiredSignatures) public view {
         // Check that the provided signature data is not too short
-        require(signatures.length >= requiredSignatures.mul(65), "GS020");
+        if (signatures.length < requiredSignatures.mul(65)) revertWithError("GS020");
         // There cannot be an owner with address 0.
         address lastOwner = address(0);
         address currentOwner;
-        uint8 v;
+        uint256 v;
         bytes32 r;
         bytes32 s;
         uint256 i;
@@ -327,7 +327,7 @@ contract Safe is
                 // Check that signature data pointer (s) is not pointing inside the static part of the signatures bytes
                 // This check is not completely accurate, since it is possible that more signatures than the threshold are send.
                 // Here we only check that the pointer is not pointing inside the part that is being processed
-                require(uint256(s) >= requiredSignatures.mul(65), "GS021");
+                if (uint256(s) < requiredSignatures.mul(65)) revertWithError("GS021");
 
                 // The contract signature check is extracted to a separate function for better compatibility with formal verification
                 // A quote from the Certora team:
@@ -339,17 +339,18 @@ contract Safe is
                 // When handling approved hashes the address of the approver is encoded into r
                 currentOwner = address(uint160(uint256(r)));
                 // Hashes are automatically approved by the sender of the message or when they have been pre-approved via a separate transaction
-                require(executor == currentOwner || approvedHashes[currentOwner][dataHash] != 0, "GS025");
+                if (executor != currentOwner && approvedHashes[currentOwner][dataHash] == 0) revertWithError("GS025");
             } else if (v > 30) {
                 // If v > 30 then default va (27,28) has been adjusted for eth_sign flow
                 // To support eth_sign and similar we adjust v and hash the messageHash with the Ethereum message prefix before applying ecrecover
-                currentOwner = ecrecover(keccak256(abi.encodePacked("\x19Ethereum Signed Message:\n32", dataHash)), v - 4, r, s);
+                currentOwner = ecrecover(keccak256(abi.encodePacked("\x19Ethereum Signed Message:\n32", dataHash)), uint8(v - 4), r, s);
             } else {
                 // Default is the ecrecover flow with the provided data hash
                 // Use ecrecover with the messageHash for EOA signatures
-                currentOwner = ecrecover(dataHash, v, r, s);
+                currentOwner = ecrecover(dataHash, uint8(v), r, s);
             }
-            require(currentOwner > lastOwner && owners[currentOwner] != address(0) && currentOwner != SENTINEL_OWNERS, "GS026");
+            if (currentOwner <= lastOwner || owners[currentOwner] == address(0) || currentOwner == SENTINEL_OWNERS)
+                revertWithError("GS026");
             lastOwner = currentOwner;
         }
     }
@@ -361,7 +362,7 @@ contract Safe is
      * @param hashToApprove The hash to mark as approved for signatures that are verified by this contract.
      */
     function approveHash(bytes32 hashToApprove) external {
-        require(owners[msg.sender] != address(0), "GS030");
+        if (owners[msg.sender] == address(0)) revertWithError("GS030");
         approvedHashes[msg.sender][hashToApprove] = 1;
         emit ApproveHash(hashToApprove, msg.sender);
     }

contracts/base/FallbackManager.sol

@@ -31,13 +31,12 @@ abstract contract FallbackManager is SelfAuthorized {
             where the first 3 bytes of the previous calldata + the first byte of the address make up a valid function signature. The subsequent call would result in unsanctioned access to Safe's internal protected methods.
             For some reason, solidity matches the first 4 bytes of the calldata to a function signature, regardless if more data follow these 4 bytes.
         */
-        require(handler != address(this), "GS400");
+        if (handler == address(this)) revertWithError("GS400");
 
-        bytes32 slot = FALLBACK_HANDLER_STORAGE_SLOT;
         /* solhint-disable no-inline-assembly */
         /// @solidity memory-safe-assembly
         assembly {
-            sstore(slot, handler)
+            sstore(FALLBACK_HANDLER_STORAGE_SLOT, handler)
         }
         /* solhint-enable no-inline-assembly */
     }
@@ -61,7 +60,6 @@ abstract contract FallbackManager is SelfAuthorized {
     //      and having the original caller address may enable additional verification scenarios.
     // solhint-disable-next-line payable-fallback,no-complex-fallback
     fallback() external {
-        bytes32 slot = FALLBACK_HANDLER_STORAGE_SLOT;
         /* solhint-disable no-inline-assembly */
         /// @solidity memory-safe-assembly
         assembly {
@@ -74,7 +72,7 @@ abstract contract FallbackManager is SelfAuthorized {
                 mstore(0x40, add(pos, length))
             }
 
-            let handler := sload(slot)
+            let handler := sload(FALLBACK_HANDLER_STORAGE_SLOT)
             if iszero(handler) {
                 return(0, 0)
             }

contracts/base/GuardManager.sol

@@ -86,14 +86,11 @@ abstract contract GuardManager is SelfAuthorized {
      * @param guard The address of the guard to be used or the 0 address to disable the guard
      */
     function setGuard(address guard) external authorized {
-        if (guard != address(0)) {
-            require(Guard(guard).supportsInterface(type(Guard).interfaceId), "GS300");
-        }
-        bytes32 slot = GUARD_STORAGE_SLOT;
+        if (guard != address(0) && !Guard(guard).supportsInterface(type(Guard).interfaceId)) revertWithError("GS300");
         /* solhint-disable no-inline-assembly */
         /// @solidity memory-safe-assembly
         assembly {
-            sstore(slot, guard)
+            sstore(GUARD_STORAGE_SLOT, guard)
         }
         /* solhint-enable no-inline-assembly */
         emit ChangedGuard(guard);
@@ -107,11 +104,10 @@ abstract contract GuardManager is SelfAuthorized {
      * @return guard The address of the guard
      */
     function getGuard() internal view returns (address guard) {
-        bytes32 slot = GUARD_STORAGE_SLOT;
         /* solhint-disable no-inline-assembly */
         /// @solidity memory-safe-assembly
         assembly {
-            guard := sload(slot)
+            guard := sload(GUARD_STORAGE_SLOT)
         }
         /* solhint-enable no-inline-assembly */
     }

contracts/base/ModuleManager.sol

@@ -31,12 +31,12 @@ abstract contract ModuleManager is SelfAuthorized, Executor, GuardManager {
      * @param data Optional data of call to execute.
      */
     function setupModules(address to, bytes memory data) internal {
-        require(modules[SENTINEL_MODULES] == address(0), "GS100");
+        if (modules[SENTINEL_MODULES] != address(0)) revertWithError("GS100");
         modules[SENTINEL_MODULES] = SENTINEL_MODULES;
         if (to != address(0)) {
-            require(isContract(to), "GS002");
+            if (!isContract(to)) revertWithError("GS002");
             // Setup has to complete successfully or transaction fails.
-            require(execute(to, 0, data, Enum.Operation.DelegateCall, type(uint256).max), "GS000");
+            if (!execute(to, 0, data, Enum.Operation.DelegateCall, type(uint256).max)) revertWithError("GS000");
         }
     }
 
@@ -47,9 +47,9 @@ abstract contract ModuleManager is SelfAuthorized, Executor, GuardManager {
      */
     function enableModule(address module) public authorized {
         // Module address cannot be null or sentinel.
-        require(module != address(0) && module != SENTINEL_MODULES, "GS101");
+        if (module == address(0) || module == SENTINEL_MODULES) revertWithError("GS101");
         // Module cannot be added twice.
-        require(modules[module] == address(0), "GS102");
+        if (modules[module] != address(0)) revertWithError("GS102");
         modules[module] = modules[SENTINEL_MODULES];
         modules[SENTINEL_MODULES] = module;
         emit EnabledModule(module);
@@ -63,8 +63,8 @@ abstract contract ModuleManager is SelfAuthorized, Executor, GuardManager {
      */
     function disableModule(address prevModule, address module) public authorized {
         // Validate module address and check that it corresponds to module index.
-        require(module != address(0) && module != SENTINEL_MODULES, "GS101");
-        require(modules[prevModule] == module, "GS103");
+        if (module == address(0) || module == SENTINEL_MODULES) revertWithError("GS101");
+        if (modules[prevModule] != module) revertWithError("GS103");
         modules[prevModule] = modules[module];
         modules[module] = address(0);
         emit DisabledModule(module);
@@ -86,7 +86,7 @@ abstract contract ModuleManager is SelfAuthorized, Executor, GuardManager {
         Enum.Operation operation
     ) public virtual returns (bool success) {
         // Only whitelisted modules are allowed.
-        require(msg.sender != SENTINEL_MODULES && modules[msg.sender] != address(0), "GS104");
+        if (msg.sender == SENTINEL_MODULES || modules[msg.sender] == address(0)) revertWithError("GS104");
         // Execute transaction without further confirmations.
         address guard = getGuard();
 
@@ -155,8 +155,8 @@ abstract contract ModuleManager is SelfAuthorized, Executor, GuardManager {
      * @return next Start of the next page.
      */
     function getModulesPaginated(address start, uint256 pageSize) external view returns (address[] memory array, address next) {
-        require(start == SENTINEL_MODULES || isModuleEnabled(start), "GS105");
-        require(pageSize > 0, "GS106");
+        if (start != SENTINEL_MODULES && !isModuleEnabled(start)) revertWithError("GS105");
+        if (pageSize == 0) revertWithError("GS106");
         // Init array with max page size
         array = new address[](pageSize);