Skip to content

Commit

Permalink
combine the two setup rules into one more concise rules
Browse files Browse the repository at this point in the history
  • Loading branch information
Derek Sorensen authored and Derek Sorensen committed Dec 18, 2024
1 parent a8561df commit c97107a
Showing 1 changed file with 8 additions and 26 deletions.
34 changes: 8 additions & 26 deletions certora/specs/v1.5/Setup.spec
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,10 @@ methods {

// ---- Rules ------------------------------------------------------------------

/// @dev setup can only be called if threshold = 0
/// @status Done: https://prover.certora.com/output/39601/202435585f914643abd02fe37b8d1fc5?anonymousKey=e74abb4876b18456b372d84e44ad78e3a22a0566
/// @dev setup can only be called if threshold = 0 and setup sets threshold > 0
/// @status Done: https://prover.certora.com/output/39601/7849e9a464e042ea89bfe68fc226edbc?anonymousKey=5c1387afecb8bc86f23df3be5eb886a5cd82787f

rule setupThresholdZero(
rule setupThresholdZeroAndSetsPositiveThreshold(
address[] _owners,
uint256 _threshold,
address to,
Expand All @@ -36,28 +36,10 @@ rule setupThresholdZero(
setup(e,_owners,_threshold,to,data,fallbackHandler,
paymentToken,payment,paymentReceiver);

assert (old_threshold == 0);
}

/// @dev setup sets threshold > 0
/// @status Done: https://prover.certora.com/output/39601/202435585f914643abd02fe37b8d1fc5?anonymousKey=e74abb4876b18456b372d84e44ad78e3a22a0566

rule setupSetsPositiveThreshold(
address[] _owners,
uint256 _threshold,
address to,
bytes data,
address fallbackHandler,
address paymentToken,
uint256 payment,
address paymentReceiver) {
env e;

// a successful call to setup
setup(e,_owners,_threshold,to,data,fallbackHandler,
paymentToken,payment,paymentReceiver);

uint256 new_threshold = getThreshold();

assert (new_threshold > 0);
}
assert (
new_threshold > 0 &&
old_threshold == 0
);
}

0 comments on commit c97107a

Please sign in to comment.