From 4f107ab9adedad9feb4e14e021bd71d3cf84d389 Mon Sep 17 00:00:00 2001
From: Wilson Cusack <wilson.cusack@coinbase.com>
Date: Mon, 8 Apr 2024 11:03:57 -0400
Subject: [PATCH] fix certora

---
 .github/workflows/certora.yml     | 8 ++++++--
 certora/specs/ERC4337Account.spec | 2 +-
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index 48846a7..92be155 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -29,9 +29,13 @@ jobs:
           chmod +x solc-static-linux
           sudo mv solc-static-linux /usr/local/bin/solc8.23
 
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+        with:
+          version: nightly    
+
       - name: Install git submodules
-        run: |
-         git submodule update --init --recursive
+        run: forge build
 
       - name: Verify rule ${{ matrix.params.name }}
         run: >
diff --git a/certora/specs/ERC4337Account.spec b/certora/specs/ERC4337Account.spec
index e945fd9..eef1b74 100644
--- a/certora/specs/ERC4337Account.spec
+++ b/certora/specs/ERC4337Account.spec
@@ -156,7 +156,7 @@ rule OnlyOwnerSelfOrEntryPoint(env e, method f) filtered {
 rule OnlyEntryPoint(env e, method f) filtered {    
     // There is no difference between filtering functions and using them as a lhs of implication
     f -> f.selector == sig:validateUserOp(EntryPointMock.UserOperation, bytes32, uint256).selector 
-        || f.selector == sig:executeWithoutChainIdValidation(bytes).selector
+        || f.selector == sig:executeWithoutChainIdValidation(bytes[]).selector
 } {
     bool ownerBefore = e.msg.sender == entryPoint();