Refactor path configuration for safe modules to remove redundant dire…

…ctories.

* Remove unnecessary directory references in Safe4337Module.conf
* Update package paths in SignatureLengthCheck.conf, TransactionExecutionMethods.conf and ValidationDataLastBitOne.conf
* Refactor checkSignatures function in Account.sol to be viewless

modules/4337/certora/conf/Safe4337Module.conf

@@ -15,9 +15,10 @@
     ],
     "rule_sanity": "basic",
     "solc": "solc8.23",
+    "solc_allow_path":"../../node_modules",
     "verify": "Safe4337Module:certora/specs/Safe4337Module.spec",
     "packages": [
-        "@account-abstraction=../../node_modules/.pnpm/@[email protected]/node_modules/@account-abstraction",
-        "@safe-global=../../node_modules/.pnpm/@[email protected][email protected][email protected][email protected]_/node_modules/@safe-global"
+        "@account-abstraction=node_modules/@account-abstraction",
+        "@safe-global=node_modules/@safe-global"
     ]
 }

modules/4337/certora/conf/SignatureLengthCheck.conf

@@ -8,9 +8,10 @@
     "msg": "Safe4337Module: Signatures Length Check",
     "rule_sanity": "basic",
     "solc": "solc8.23",
+    "solc_allow_path":"../../node_modules",
     "verify": "Safe4337ModuleHarness:certora/specs/SignatureLengthCheck.spec",
     "packages": [
-        "@account-abstraction=../../node_modules/.pnpm/@[email protected]/node_modules/@account-abstraction",
-        "@safe-global=../../node_modules/.pnpm/@[email protected][email protected][email protected][email protected]_/node_modules/@safe-global"
+        "@account-abstraction=node_modules/@account-abstraction",
+        "@safe-global=node_modules/@safe-global"
     ]
 }

modules/4337/certora/conf/TransactionExecutionMethods.conf

@@ -15,6 +15,7 @@
     ],
     "rule_sanity": "advanced",
     "solc": "solc8.23",
+    "solc_allow_path":"../../node_modules",
     "verify": "Safe4337Module:certora/specs/TransactionExecutionMethods.spec",
     "packages": [
         "@account-abstraction=../../node_modules/.pnpm/@[email protected]/node_modules/@account-abstraction",

modules/4337/certora/conf/ValidationDataLastBitOne.conf

@@ -15,9 +15,10 @@
     ],
     "rule_sanity": "basic",
     "solc": "solc8.23",
+    "solc_allow_path":"../../node_modules",
     "verify": "Safe4337Module:certora/specs/ValidationDataLastBitOne.spec",
     "packages": [
-        "@account-abstraction=../../node_modules/.pnpm/@[email protected]/node_modules/@account-abstraction",
-        "@safe-global=../../node_modules/.pnpm/@[email protected][email protected][email protected][email protected]_/node_modules/@safe-global"
+        "@account-abstraction=node_modules/@account-abstraction",
+        "@safe-global=node_modules/@safe-global"
     ]
 }

modules/4337/certora/harnesses/Account.sol

@@ -99,11 +99,11 @@ contract Account is Safe {
  *         in case the checkSignature functions reverts.
  */
 contract AlwaysRevertingAccount {
-    function checkSignatures(bytes32 dataHash, bytes memory data, bytes memory signatures) public view {
+    function checkSignatures(bytes32 dataHash, bytes memory data, bytes memory signatures) public pure {
         revert();
     }
 
-    function getSignatures(bytes calldata signature) external returns (bytes memory slice) {
+    function getSignatures(bytes calldata signature) external pure returns (bytes memory slice) {
         slice = signature[12:];
     }
 }