Skip to content

Commit

Permalink
Make reverts rules shorter using double implication
Browse files Browse the repository at this point in the history
  • Loading branch information
@sunbreak1211
sunbreak1211 committed Nov 16, 2023
1 parent ba8209c commit a0bd6b1
Show file tree
Hide file tree
Showing 10 changed files with 73 additions and 242 deletions.
12 changes: 3 additions & 9 deletions certora/AllocatorBuffer.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,9 +53,7 @@ rule rely_revert(address usr) {
bool revert1 = e.msg.value > 0;
bool revert2 = wardsSender != 1;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2, "Revert rules failed";
}

// Verify correct storage changes for non reverting deny
Expand Down Expand Up @@ -87,9 +85,7 @@ rule deny_revert(address usr) {
bool revert1 = e.msg.value > 0;
bool revert2 = wardsSender != 1;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2, "Revert rules failed";
}

// Verify correct storage changes for non reverting approve
Expand Down Expand Up @@ -118,7 +114,5 @@ rule approve_revert(address asset, address spender, uint256 amount) {
bool revert1 = e.msg.value > 0;
bool revert2 = wardsSender != 1;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2, "Revert rules failed";
}
13 changes: 3 additions & 10 deletions certora/AllocatorRegistry.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,9 +54,7 @@ rule rely_revert(address usr) {
bool revert1 = e.msg.value > 0;
bool revert2 = wardsSender != 1;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2, "Revert rules failed";
}

// Verify correct storage changes for non reverting deny
Expand Down Expand Up @@ -88,9 +86,7 @@ rule deny_revert(address usr) {
bool revert1 = e.msg.value > 0;
bool revert2 = wardsSender != 1;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2, "Revert rules failed";
}

// Verify correct storage changes for non reverting file
Expand Down Expand Up @@ -123,8 +119,5 @@ rule file_revert(bytes32 ilk, bytes32 what, address data) {
bool revert2 = wardsSender != 1;
bool revert3 = what != to_bytes32(0x6275666665720000000000000000000000000000000000000000000000000000);

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert revert3 => lastReverted, "revert3 failed";
assert lastReverted => revert1 || revert2 || revert3, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed";
}
20 changes: 5 additions & 15 deletions certora/AllocatorRoles.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -86,9 +86,7 @@ rule rely_revert(address usr) {
bool revert1 = e.msg.value > 0;
bool revert2 = wardsSender != 1;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2, "Revert rules failed";
}

// Verify correct storage changes for non reverting deny
Expand Down Expand Up @@ -120,9 +118,7 @@ rule deny_revert(address usr) {
bool revert1 = e.msg.value > 0;
bool revert2 = wardsSender != 1;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2, "Revert rules failed";
}

// Verify correct storage changes for non reverting setIlkAdmin
Expand Down Expand Up @@ -154,9 +150,7 @@ rule setIlkAdmin_revert(bytes32 ilk, address usr) {
bool revert1 = e.msg.value > 0;
bool revert2 = wardsSender != 1;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2, "Revert rules failed";
}

// Verify correct storage changes for non reverting setUserRole
Expand Down Expand Up @@ -192,9 +186,7 @@ rule setUserRole_revert(bytes32 ilk, address who, uint8 role, bool enabled) {
bool revert1 = e.msg.value > 0;
bool revert2 = ilkAuthIlk != e.msg.sender;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2, "Revert rules failed";
}

// Verify correct storage changes for non reverting setRoleAction
Expand Down Expand Up @@ -231,9 +223,7 @@ rule setRoleAction_revert(bytes32 ilk, uint8 role, address target, bytes4 sign,
bool revert1 = e.msg.value > 0;
bool revert2 = ilkAuthIlk != e.msg.sender;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2, "Revert rules failed";
}

// Verify correct response from canCall
Expand Down
49 changes: 11 additions & 38 deletions certora/AllocatorVault.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,9 +78,7 @@ rule rely_revert(address usr) {
bool revert1 = e.msg.value > 0;
bool revert2 = !canCall && wardsSender != 1;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2, "Revert rules failed";
}

// Verify correct storage changes for non reverting deny
Expand Down Expand Up @@ -113,9 +111,7 @@ rule deny_revert(address usr) {
bool revert1 = e.msg.value > 0;
bool revert2 = !canCall && wardsSender != 1;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2, "Revert rules failed";
}

// Verify correct storage changes for non reverting file
Expand All @@ -142,10 +138,7 @@ rule file_revert(bytes32 what, address data) {
bool revert2 = !canCall && wardsSender != 1;
bool revert3 = what != to_bytes32(0x6a75670000000000000000000000000000000000000000000000000000000000);

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert revert3 => lastReverted, "revert3 failed";
assert lastReverted => revert1 || revert2 || revert3, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed";
}

// Verify correct storage changes for non reverting draw
Expand Down Expand Up @@ -209,20 +202,10 @@ rule draw_revert(uint256 wad) {
bool revert9 = vatDaiNstJoin + wad * RAY() > max_uint256;
bool revert10 = nstTotalSupply + wad > max_uint256;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert revert3 => lastReverted, "revert3 failed";
assert revert4 => lastReverted, "revert4 failed";
assert revert5 => lastReverted, "revert5 failed";
assert revert6 => lastReverted, "revert6 failed";
assert revert7 => lastReverted, "revert7 failed";
assert revert8 => lastReverted, "revert8 failed";
assert revert9 => lastReverted, "revert9 failed";
assert revert10 => lastReverted, "revert10 failed";
assert lastReverted => revert1 || revert2 || revert3 ||
revert4 || revert5 || revert6 ||
revert7 || revert8 || revert9 ||
revert10, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2 || revert3 ||
revert4 || revert5 || revert6 ||
revert7 || revert8 || revert9 ||
revert10, "Revert rules failed";
}

// Verify correct storage changes for non reverting wipe
Expand Down Expand Up @@ -290,18 +273,8 @@ rule wipe_revert(uint256 wad) {
bool revert9 = vatDaiVault + wad * RAY() > max_uint256;
bool revert10 = rate * dart > max_int256();

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert revert3 => lastReverted, "revert3 failed";
assert revert4 => lastReverted, "revert4 failed";
assert revert5 => lastReverted, "revert5 failed";
assert revert6 => lastReverted, "revert6 failed";
assert revert7 => lastReverted, "revert7 failed";
assert revert8 => lastReverted, "revert8 failed";
assert revert9 => lastReverted, "revert9 failed";
assert revert10 => lastReverted, "revert10 failed";
assert lastReverted => revert1 || revert2 || revert3 ||
revert4 || revert5 || revert6 ||
revert7 || revert8 || revert9 ||
revert10, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2 || revert3 ||
revert4 || revert5 || revert6 ||
revert7 || revert8 || revert9 ||
revert10, "Revert rules failed";
}
56 changes: 12 additions & 44 deletions certora/funnels/DepositorUniV3.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,9 +107,7 @@ rule rely_revert(address usr) {
bool revert1 = e.msg.value > 0;
bool revert2 = !canCall && wardsSender != 1;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2, "Revert rules failed";
}

// Verify correct storage changes for non reverting deny
Expand Down Expand Up @@ -142,9 +140,7 @@ rule deny_revert(address usr) {
bool revert1 = e.msg.value > 0;
bool revert2 = !canCall && wardsSender != 1;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2, "Revert rules failed";
}

// Verify correct storage changes for non reverting setLimits
Expand Down Expand Up @@ -193,10 +189,7 @@ rule setLimits_revert(address gem0, address gem1, uint24 fee, uint96 cap0, uint9
bool revert2 = !canCall && wardsSender != 1;
bool revert3 = gem0 >= gem1;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert revert3 => lastReverted, "revert3 failed";
assert lastReverted => revert1 || revert2 || revert3, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed";
}

// Verify correct response from getPosition
Expand Down Expand Up @@ -284,14 +277,8 @@ rule uniswapV3MintCallback_revert(uint256 amt0Owed, uint256 amt1Owed, bytes data
bool revert5 = gem1BalanceOfBuffer < to_mathint(amt1Owed);
bool revert6 = gem1AllowanceBufferDepositor < to_mathint(amt1Owed);

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert revert3 => lastReverted, "revert3 failed";
assert revert4 => lastReverted, "revert4 failed";
assert revert5 => lastReverted, "revert5 failed";
assert revert6 => lastReverted, "revert6 failed";
assert lastReverted => revert1 || revert2 || revert3 ||
revert4 || revert5 || revert6, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2 || revert3 ||
revert4 || revert5 || revert6, "Revert rules failed";
}

// Verify correct storage changes for non reverting deposit
Expand Down Expand Up @@ -406,20 +393,10 @@ rule deposit_revert(DepositorUniV3.LiquidityParams p) {
bool revert9 = amt0 < to_mathint(p.amt0Min) || amt1 < to_mathint(p.amt1Min);
bool revert10 = amt0 > due0Updated || amt1 > due1Updated;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert revert3 => lastReverted, "revert3 failed";
assert revert4 => lastReverted, "revert4 failed";
assert revert5 => lastReverted, "revert5 failed";
assert revert6 => lastReverted, "revert6 failed";
assert revert7 => lastReverted, "revert7 failed";
assert revert8 => lastReverted, "revert8 failed";
assert revert9 => lastReverted, "revert9 failed";
assert revert10 => lastReverted, "revert10 failed";
assert lastReverted => revert1 || revert2 || revert3 ||
revert4 || revert5 || revert6 ||
revert7 || revert8 || revert9 ||
revert10, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2 || revert3 ||
revert4 || revert5 || revert6 ||
revert7 || revert8 || revert9 ||
revert10, "Revert rules failed";
}

// Verify correct storage changes for non reverting withdraw
Expand Down Expand Up @@ -542,14 +519,8 @@ rule withdraw_revert(DepositorUniV3.LiquidityParams p, bool takeFees) {
bool revert5 = amt0 < to_mathint(p.amt0Min) || amt1 < to_mathint(p.amt1Min);
bool revert6 = amt0 > due0Updated || amt1 > due1Updated;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert revert3 => lastReverted, "revert3 failed";
assert revert4 => lastReverted, "revert4 failed";
assert revert5 => lastReverted, "revert5 failed";
assert revert6 => lastReverted, "revert6 failed";
assert lastReverted => revert1 || revert2 || revert3 ||
revert4 || revert5 || revert6, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2 || revert3 ||
revert4 || revert5 || revert6, "Revert rules failed";
}

// Verify correct storage changes for non reverting collect
Expand Down Expand Up @@ -631,8 +602,5 @@ rule collect_revert(DepositorUniV3.CollectParams p) {
bool revert2 = !canCall && wardsSender != 1;
bool revert3 = p.gem0 >= p.gem1;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert revert3 => lastReverted, "revert3 failed";
assert lastReverted => revert1 || revert2 || revert3, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed";
}
25 changes: 6 additions & 19 deletions certora/funnels/Swapper.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,9 +73,7 @@ rule rely_revert(address usr) {
bool revert1 = e.msg.value > 0;
bool revert2 = !canCall && wardsSender != 1;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2, "Revert rules failed";
}

// Verify correct storage changes for non reverting deny
Expand Down Expand Up @@ -108,9 +106,7 @@ rule deny_revert(address usr) {
bool revert1 = e.msg.value > 0;
bool revert2 = !canCall && wardsSender != 1;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2, "Revert rules failed";
}

// Verify correct storage changes for non reverting setLimits
Expand Down Expand Up @@ -153,9 +149,7 @@ rule setLimits_revert(address src, address dst, uint96 cap, uint32 era) {
bool revert1 = e.msg.value > 0;
bool revert2 = !canCall && wardsSender != 1;

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2, "Revert rules failed";
}

// Verify correct storage changes for non reverting swap
Expand Down Expand Up @@ -243,14 +237,7 @@ rule swap_revert(address src, address dst, uint256 amt, uint256 minOut, address
bool revert6 = srcAllowanceBufferSwapper < to_mathint(amt);
bool revert7 = dstBalanceOfSwapper + dstBalanceOfCallee < to_mathint(minOut);

assert revert1 => lastReverted, "revert1 failed";
assert revert2 => lastReverted, "revert2 failed";
assert revert3 => lastReverted, "revert3 failed";
assert revert4 => lastReverted, "revert4 failed";
assert revert5 => lastReverted, "revert5 failed";
assert revert6 => lastReverted, "revert6 failed";
assert revert7 => lastReverted, "revert7 failed";
assert lastReverted => revert1 || revert2 || revert3 ||
revert4 || revert5 || revert6 ||
revert7, "Revert rules are not covering all the cases";
assert lastReverted <=> revert1 || revert2 || revert3 ||
revert4 || revert5 || revert6 ||
revert7, "Revert rules failed";
}
Loading

0 comments on commit a0bd6b1

Please sign in to comment.