Certora Script Update & Minor changes (#470)

Fixes #468 

This PR eliminates the use of a script for the Certora FV and uses the
Certora CLI command directly.

In addition, extra small changes included in this PR:
- Natspec changes in Harness solidity code.
- Inclusion of Recovery Module in the README.
- Using the latest version of checkout (`v4`) for GitHub CI.

.github/workflows/certora_4337.yml

@@ -19,12 +19,12 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        rule: ['verify4337Module.sh', 'verifyTransactionExecutionMethods.sh', 'verifyValidationData.sh', 'verifySignatureLengthCheck.sh']
+        rule: ['Safe4337Module', 'TransactionExecutionMethods', 'ValidationDataLastBitOne', 'SignatureLengthCheck']
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
 
       - name: Install pnpm
-        uses: pnpm/action-setup@v3
+        uses: pnpm/action-setup@v4
         with:
           version: 9
 
@@ -33,7 +33,7 @@ jobs:
         with: { python-version: 3.11 }
 
       - name: Install certora cli
-        run: pip install -Iv certora-cli==7.3.0
+        run: pip install -r modules/4337/certora/requirements.txt
 
       - name: Install solc
         run: |
@@ -47,8 +47,7 @@ jobs:
       - name: Verify rule ${{ matrix.rule }}
         working-directory: ./modules/4337
         run: |
-          echo "key length" ${#CERTORAKEY}
-          chmod +x ./certora/scripts/${{ matrix.rule }}
-          ./certora/scripts/${{ matrix.rule }}
+          echo "Certora key length" ${#CERTORAKEY}
+          certoraRun certora/conf/${{ matrix.rule }}.conf --wait_for_results=all
         env:
           CERTORAKEY: ${{ secrets.CERTORA_KEY }}

README.md

@@ -7,6 +7,7 @@ This repository contains a collection of modules for the [Safe Smart Account](ht
 - [4337 Module](./modules/4337)
 - [Allowance Module](./modules/allowances)
 - [Passkey](./modules/passkey)
+- [Recovery Module](./modules/recovery/)
 
 ## Examples
 

modules/4337/certora/harnesses/Account.sol

@@ -94,8 +94,10 @@ contract Account is Safe {
     }
 }
 
-// @notice This is a harness contract for the rule that verfies the validation data
-//         in case the checkSignature functions reverts.
+/*
+ * @notice This is a harness contract for the rule that verfies the validation data
+ *         in case the checkSignature functions reverts.
+ */
 contract AlwaysRevertingAccount {
     function checkSignatures(bytes32 dataHash, bytes memory data, bytes memory signatures) public view {
         revert();

modules/4337/certora/requirements.txt

@@ -0,0 +1 @@
+certora-cli==7.3.0