[#95] Update rule for hooks

5afe · Sep 19, 2023 · e3644ca · e3644ca
1 parent f919192
commit e3644ca
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 4 deletions.
diff --git a/certora/scripts/verifyManager.sh b/certora/scripts/verifyManager.sh
@@ -9,8 +9,9 @@ fi
 certoraRun contracts/SafeProtocolManager.sol contracts/SafeProtocolRegistry.sol contracts/test/TestExecutorCertora.sol \
     --verify SafeProtocolManager:certora/specs/Manager.spec \
     --link "SafeProtocolManager:registry=SafeProtocolRegistry" \
+    --solc solc8.18 \
     --optimistic_loop \
-    --loop_iter 3 \
+    --loop_iter 1 \
     --optimistic_hashing \
     --hashing_length_bound 352 \
     --rule_sanity \

diff --git a/certora/specs/Manager.spec b/certora/specs/Manager.spec
@@ -4,6 +4,9 @@ using TestExecutorCertora as testExecutorCertora;
 methods {
     function setRegistry(address) external;
     function registry() external returns (address) envfree;
+
+    function _.supportsInterface(bytes4) external => DISPATCHER(true);
+
     function testExecutorCertora.called() external returns (bool) envfree;
     function contractRegistry.check(address module) external returns (uint64, uint64) envfree;
     function _.execTransactionFromModule(
@@ -61,14 +64,16 @@ rule onlyEnabledAndListedPluginCanExecuteCall(){
     assert testExecutorCertora.called() => (listedAt > 0 && flagged == 0);
 }
 
-rule hookUpdates(){
+rule hooksUpdates(address safe, SafeProtocolManager.SafeTransaction transactionData){
+
     method f; env e; calldataarg args;
     storage initialStorage = lastStorage;
-    f(e, args);
+    executeTransaction(e, safe, transactionData);
 
     env e2;
     setHooks(e2, 0) at initialStorage;
-    f@withrevert(e, args);
+
+    executeTransaction@withrevert(e, safe, transactionData);
 
     assert !lastReverted;
 }