From 1ac50750aab81e74c1760ad4b5c988621c1a15b6 Mon Sep 17 00:00:00 2001 From: Akshay Date: Thu, 4 Jul 2024 15:06:36 +0200 Subject: [PATCH] [#754] FV --- modules/4337/certora/specs/Safe4337Module.spec | 2 ++ modules/4337/certora/specs/ValidationDataLastBitOne.spec | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/modules/4337/certora/specs/Safe4337Module.spec b/modules/4337/certora/specs/Safe4337Module.spec index 112d21637..ade56b0e4 100644 --- a/modules/4337/certora/specs/Safe4337Module.spec +++ b/modules/4337/certora/specs/Safe4337Module.spec @@ -25,6 +25,8 @@ methods { function getOperationHash( Safe4337Module.PackedUserOperation userOp ) external returns(bytes32) envfree => PER_CALLEE_CONSTANT; + function _checkSignatureLength(bytes calldata, uint256) internal returns(bool) => ALWAYS(true); + } persistent ghost ERC2771MessageSender() returns address; diff --git a/modules/4337/certora/specs/ValidationDataLastBitOne.spec b/modules/4337/certora/specs/ValidationDataLastBitOne.spec index 9f48e24bb..c2b1a8970 100644 --- a/modules/4337/certora/specs/ValidationDataLastBitOne.spec +++ b/modules/4337/certora/specs/ValidationDataLastBitOne.spec @@ -12,7 +12,7 @@ methods { Safe4337Module.PackedUserOperation userOp ) external returns(bytes32) envfree => PER_CALLEE_CONSTANT; - function _._checkSignatureLength(bytes calldata, uint256) internal => ALWAYS(true); + function _checkSignatureLength(bytes calldata, uint256) internal returns(bool)=> ALWAYS(true); } rule validationDataLastBitOneIfCheckSignaturesFails(address sender,