Skip to content

Commit

Permalink
Changes to asserts
Browse files Browse the repository at this point in the history
  • Loading branch information
lucasmt committed Sep 30, 2024
1 parent 4af2542 commit 8b9ea05
Showing 1 changed file with 23 additions and 13 deletions.
36 changes: 23 additions & 13 deletions src/test/kontrol/RepoTokenListInvariants.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ contract RepoTokenListInvariantsTest is Test, KontrolCheats {
if (mode == Mode.Assume) {
vm.assume(condition);
} else {
assertTrue(condition);
assert(condition);
}
}

Expand Down Expand Up @@ -102,7 +102,7 @@ contract RepoTokenListInvariantsTest is Test, KontrolCheats {
/**
* Assume or assert that there are no duplicate tokens in the list.
*/
function _establishNoDuplicates(Mode mode) internal {
function _establishNoDuplicateTokens(Mode mode) internal {
address current = _repoTokenList.head;

while (current != RepoTokenList.NULL_NODE) {
Expand Down Expand Up @@ -215,9 +215,12 @@ contract RepoTokenListInvariantsTest is Test, KontrolCheats {
kevm.symbolicStorage(address(this));
_initializeRepoTokenList();

// Our initialization procedure guarantees this invariant,
// so we assert instead of assuming
_establishNoDuplicateTokens(Mode.Assert);

// Assume that the invariants are satisfied before the function is called
_establishSortedByMaturity(Mode.Assume);
_establishNoDuplicates(Mode.Assume);
_establishNoMaturedTokens(Mode.Assume);
_establishPositiveBalance(Mode.Assume);

Expand All @@ -236,14 +239,14 @@ contract RepoTokenListInvariantsTest is Test, KontrolCheats {


// Assert that the size of the list increased by 1
assertEq(_countNodesInList(), count + 1);
assert(_countNodesInList() == count + 1);

// Assert that the new RepoToken is in the list
assertTrue(_repoTokenInList(repoToken));
assert(_repoTokenInList(repoToken));

// Assert that the invariants are preserved
_establishSortedByMaturity(Mode.Assert);
_establishNoDuplicates(Mode.Assert);
_establishNoDuplicateTokens(Mode.Assert);
_establishNoMaturedTokens(Mode.Assert);
_establishPositiveBalance(Mode.Assert);
}
Expand All @@ -259,9 +262,12 @@ contract RepoTokenListInvariantsTest is Test, KontrolCheats {
kevm.symbolicStorage(address(this));
_initializeRepoTokenList();

// Our initialization procedure guarantees this invariant,
// so we assert instead of assuming
_establishNoDuplicateTokens(Mode.Assert);

// Assume that the invariants are satisfied before the function is called
_establishSortedByMaturity(Mode.Assume);
_establishNoDuplicates(Mode.Assume);
_establishNoMaturedTokens(Mode.Assume);
_establishPositiveBalance(Mode.Assume);

Expand All @@ -275,14 +281,14 @@ contract RepoTokenListInvariantsTest is Test, KontrolCheats {
_repoTokenList.insertSorted(repoToken);

// Assert that the size of the list didn't change
assertEq(_countNodesInList(), count);
assert(_countNodesInList() == count);

// Assert that the RepoToken is still in the list
assertTrue(_repoTokenInList(repoToken));
assert(_repoTokenInList(repoToken));

// Assert that the invariants are preserved
_establishSortedByMaturity(Mode.Assert);
_establishNoDuplicates(Mode.Assert);
_establishNoDuplicateTokens(Mode.Assert);
_establishNoMaturedTokens(Mode.Assert);
_establishPositiveBalance(Mode.Assert);
}
Expand Down Expand Up @@ -313,9 +319,13 @@ contract RepoTokenListInvariantsTest is Test, KontrolCheats {
// Save the number of tokens in the list before the function is called
uint256 count = _countNodesInList();

// Our initialization procedure guarantees this invariant,
// so we assert instead of assuming
_establishNoDuplicateTokens(Mode.Assert);

// Assume that the invariants are satisfied before the function is called
_establishSortedByMaturity(Mode.Assume);
_establishNoDuplicates(Mode.Assume);
_establishNoDuplicateTokens(Mode.Assume);
_establishPositiveBalanceForNonMaturedTokens(Mode.Assume);

// Assume that the call to redeemTermRepoTokens will not revert
Expand All @@ -325,11 +335,11 @@ contract RepoTokenListInvariantsTest is Test, KontrolCheats {
_repoTokenList.removeAndRedeemMaturedTokens();

// Assert that the size of the list is less than or equal to before
assertLe(_countNodesInList(), count);
assert(_countNodesInList() <= count);

// Assert that the invariants are preserved
_establishSortedByMaturity(Mode.Assert);
_establishNoDuplicates(Mode.Assert);
_establishNoDuplicateTokens(Mode.Assert);

// Now the following invariants should hold as well
_establishNoMaturedTokens(Mode.Assert);
Expand Down

0 comments on commit 8b9ea05

Please sign in to comment.