Правило для проверки total supply в ERC-20
Проверяемое правило:
Total supply токена > баланс любого пользователя
Правило несложное, выглядит так. Сминтили токены на аккаунт, проверяем
/// @title Total supply after mint is at least the balance of the receiving account
rule totalSupplyAfterMint(address account, uint256 amount) {
env e;
mint(e, account, amount);
uint256 userBalanceAfter = balanceOf(account);
uint256 totalAfter = totalSupply();
// Verify that the total supply of the system is at least the current balance of the account.
assert totalAfter >= userBalanceAfter, "total supply is less than a user's balance";
}
Вот только по отчету certora это правило будет нарушено/violated
Потому что Certora работает так, что проверяет все возможные пути, даже те, которые невероятны/недостижимы. В данном случае один из таких путей это когда totalSuplly() вернет значение меньше, чем balanceOf()
Потому что Certora не запускает код, она проверяет его математически, для нее нет значения в чем суть той или иной функции, она делает over-approximation, т.е. чрезмерные предположения. И эта часть наверное наиболее сложная, потому что требует изменить логику работы с кодом, который требуется написать
Поэтому существуют
Preconditions - условия, которые мы задаем явно
В данном случае после строчки с env e следует добавить:
// Assume that in the current state before calling mint, the total supply of the
// system is at least the user balance.
uint256 userBalanceBefore = balanceOf(account);
uint256 totalBefore = totalSupply();
require totalBefore >= userBalanceBefore;
То есть обозначить, что total supply до операции был больше, чем user balance до операции
Про переменные надо еще сказать следующее:
- неинициализированная переменная может принимать любое значение
- require тем не менее может ограничить ее каким-либо образом
- переменные внутри правила immutable
- а вот ghost переменные могут меняться
Ссылки:
- Туториал, взятый за основу
- Спецификация
https://t.me/web3securityresearch