fix certora

coinbase · Apr 8, 2024 · 4f107ab · 4f107ab
1 parent ce8015b
commit 4f107ab
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 3 deletions.
diff --git 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
@@ -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();