Skip to content

Commit

Permalink
test: fix PendingValues verif
Browse files Browse the repository at this point in the history
  • Loading branch information
MathisGD committed Aug 12, 2024
1 parent 5e71fa8 commit a740591
Showing 1 changed file with 7 additions and 1 deletion.
8 changes: 7 additions & 1 deletion certora/specs/PendingValues.spec
Original file line number Diff line number Diff line change
Expand Up @@ -15,16 +15,20 @@ invariant noBadPendingTimelock()
requireInvariant timelockInRange();
// Safe require as it corresponds to some time very far into the future.
require e.block.timestamp < 2^63;
// Safe require as it corresponds to some time very far into the past.
require e.block.timestamp > 0;
}
}

// Check that the pending timelock value is always strictly smaller than the current timelock value.
invariant smallerPendingTimelock()
assert_uint256(pendingTimelock_().value) < timelock()
{
preserved {
preserved with (env e) {
requireInvariant pendingTimelockInRange();
requireInvariant timelockInRange();
// Safe require as it corresponds to some time very far into the past.
require e.block.timestamp > 0;
}
}

Expand Down Expand Up @@ -73,6 +77,8 @@ invariant noBadPendingGuardian()
requireInvariant timelockInRange();
// Safe require as it corresponds to some time very far into the future.
require e.block.timestamp < 2^63;
// Safe require as it corresponds to some time very far into the past.
require e.block.timestamp > 0;
}
}

Expand Down

0 comments on commit a740591

Please sign in to comment.