Skip to content

Commit

Permalink
fix: make spec not contract specific
Browse files Browse the repository at this point in the history
  • Loading branch information
colin-morpho committed Dec 26, 2024
1 parent af46488 commit 64a03dc
Showing 1 changed file with 7 additions and 2 deletions.
9 changes: 7 additions & 2 deletions certora/specs/Protected.spec
Original file line number Diff line number Diff line change
@@ -1,5 +1,10 @@
// SPDX-License-Identifier: GPL-2.0-or-later

methods {
function initiator() external returns address envfree;
function MORPHO() external returns address envfree;
}

// Check that all methods except those noted below comply with the `protected` modifier when an initiator has been set.
rule protectedWithSetInitiator(method f, env e, calldataarg data) filtered {
// Do not check view functions.
Expand All @@ -11,9 +16,9 @@ rule protectedWithSetInitiator(method f, env e, calldataarg data) filtered {
}
{
// Safe require because `protected` functions should be callable by the initiator.
require e.msg.sender != currentContract._initiator;
require e.msg.sender != initiator();
// Safe require because `protected` functions should be callable by Morpho.
require e.msg.sender != currentContract.MORPHO;
require e.msg.sender != MORPHO();
f@withrevert(e,data);
assert lastReverted;
}

0 comments on commit 64a03dc

Please sign in to comment.