Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion fv/specs/AccessControlDefaultAdminRules.spec
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ invariant defaultAdminRoleAdminConsistency()
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
// Writing this as an invariant would be flagged by Certora as trivial. Writing it as a rule is just as valid: we
// verify the is true for any state of the storage
// verify this is true for any state of the storage
rule ownerConsistency() {
assert defaultAdmin() == owner();
}
Expand Down
2 changes: 1 addition & 1 deletion fv/specs/ERC20Wrapper.spec
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ invariant totalSupplyIsSmallerThanUnderlyingBalance()
require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(from, to);
}
preserved ERC20PermitHarness.burn(address from, uint256 amount) with (env e) {
// If someone can burn from the wrapper, than the invariant obviously doesn't hold.
// If someone can burn from the wrapper, then the invariant obviously doesn't hold.
require from != currentContract;
require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(from, currentContract);
}
Expand Down