Unnecessary check removed

modules/4337/certora/harnesses/Account.sol

@@ -90,12 +90,12 @@ contract Account is Safe {
 
     All three will have the same canonical hash: 0xe304234a47e4f89d0a95d9fafb42e9c3143e23e951d38add9f781c34f962deb7
     */
-    function canonicalSignatureHash(bytes calldata signatures, uint256 threshold) public pure returns (bytes32 canonical) {
-        uint256 dynamicOffset = threshold * 0x41;
+    function canonicalSignatureHash(bytes calldata signatures, uint256 safeThreshold) public pure returns (bytes32 canonical) {
+        uint256 dynamicOffset = safeThreshold * 0x41;
         bytes memory staticPart = signatures[:dynamicOffset];
         bytes memory dynamicPart = "";
 
-        for (uint256 i = 0; i < threshold; i++) {
+        for (uint256 i = 0; i < safeThreshold; i++) {
             uint256 ptr = i * 0x41;
             uint8 v = uint8(signatures[ptr + 0x40]);
 
@@ -131,17 +131,6 @@ contract Account is Safe {
         }
         canonical = keccak256(abi.encodePacked(staticPart, dynamicPart));
     }
-
-    function containsContractSignature(bytes calldata signatures, uint256 threshold) public pure returns (bool) {
-        for (uint256 i = 0; i < threshold; i++) {
-            uint256 ptr = i * 0x41;
-            uint8 v = uint8(signatures[ptr + 0x40]);
-            if (v == 0) {
-                return true;
-            }
-        }
-        return false;
-    }
 }
 
 // @notice This is a harness contract for the rule that verfies the validation data

modules/4337/certora/specs/SignatureLengthCheck.spec

@@ -5,23 +5,21 @@ methods {
     function combineBytes(bytes, bytes) external returns(bytes) envfree;
 
     // Safe Contract functions
-    function safeContract.containsContractSignature(bytes, uint256) external returns(bool) envfree;
     function safeContract.canonicalSignatureHash(bytes, uint256) external returns(bytes32) envfree;
 }
 
 // This rule verifies that if excess data is added to the dynamic part of the signature, then the signature check will fail.
 rule signatureLengthCheckDirectly(bytes signatures, bytes gasGriefingData, uint256 threshold) {
     require signatures.length > 0;
     require gasGriefingData.length > 0;
-    assert checkSignaturesLength(signatures, threshold) => !checkSignaturesLength(combineBytes(signatures,gasGriefingData), threshold);
+    assert checkSignaturesLength(signatures, threshold) => !checkSignaturesLength(combineBytes(signatures, gasGriefingData), threshold);
 }
 
 // This rule verifies that if excess data is added to the dynamic part of the signature, though it could pass in the safe contract's
 // `checkSignatures(...)`, it will be caught within the `_checkSignaturesLength(...)` call, as the dynamic length is checked.
 rule canonicalHashBasedLengthCheck(bytes signatures, bytes griefedSignatures, uint256 threshold) {
     require safeContract.canonicalSignatureHash(signatures, threshold) == safeContract.canonicalSignatureHash(griefedSignatures, threshold);
     require signatures.length < griefedSignatures.length;
-    require safeContract.containsContractSignature(signatures, threshold);
 
     assert checkSignaturesLength(signatures, threshold) => !checkSignaturesLength(griefedSignatures, threshold);
 }