From 450831a613d30249d2ae6ebdfa1d66e6fc846dfd Mon Sep 17 00:00:00 2001
From: r4bbit <445106+0x-r4bbit@users.noreply.github.com>
Date: Fri, 1 Mar 2024 10:42:11 +0100
Subject: [PATCH] fix(Certora specs): ensure prover runs rules on
 `currentContract`

Since we're implementing rules for `StakeManager` migrations, we need
multiple instances inside the certora specs.

This results in the prover trying to run rules on the other
`StakeManager` instance as well, which isn't always desired,
as it causes some rules to fail, even though they'd pass if they'd be
executed only on the `currentContract`.

This commit makes the filter condition for relevant rules stronger, such
that the prover will not run them on the `newStakeManager` contract
instance.
---
 certora/specs/StakeManagerStartMigration.spec | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/certora/specs/StakeManagerStartMigration.spec b/certora/specs/StakeManagerStartMigration.spec
index 8cbfdc3..f4496a9 100644
--- a/certora/specs/StakeManagerStartMigration.spec
+++ b/certora/specs/StakeManagerStartMigration.spec
@@ -41,7 +41,7 @@ definition blockedWhenNotMigrating(method f) returns bool = (
       );
 
 rule rejectWhenMigrating(method f) filtered {
-  f -> blockedWhenMigrating(f)
+  f -> blockedWhenMigrating(f) && f.contract == currentContract
 } {
   calldataarg args;
   env e;
@@ -68,7 +68,7 @@ rule allowWhenMigrating(method f) filtered {
 
 
 rule rejectWhenNotMigrating(method f) filtered {
-  f -> blockedWhenNotMigrating(f)
+  f -> blockedWhenNotMigrating(f) && f.contract == currentContract
 } {
   calldataarg args;
   env e;
@@ -103,8 +103,9 @@ rule startMigrationCorrect {
   assert newStakeManager.totalSupplyBalance() == currentContract.totalSupplyBalance();
 }
 
-rule migrationLockedIn {
-  method f;
+rule migrationLockedIn(method f) filtered {
+  f -> !blockedWhenMigrating(f) && f.contract == currentContract
+} {
   env e;
   calldataarg args;