Vacuity
Одна из ошибок, с которой я столкнулся (и многие до и после меня), гласит rule is vacuous
Что можно перевести как правило бездумное/бессодержательное
Такая ошибка возникает, когда не существует таких путей исполнения программы, при которых выполнялись бы заявленные требования
Например, наше бездумное требование выглядит так:
rule simpleVacuousRule(uint256 x, uint256 y) {
// Contradictory requirement
require (x > y) && (y > x);
assert false; // Should always fail
}У Prover есть свойство rule_sanity, которое может быть задано в .conf файле. Если будет указано, что rule_sanity basic, то прувер пометит это правило как неисполнимое, потому что оно не прошло проверку на корректность. Но если задать rule_sanity none, то правило будет помечено как верифицированное, потому что контрпримера не существует в том плане, что assert недостижим и значит не завершается ошибкой
Происходит это потому, что прувер по умолчанию игнорирует пути, которые завершаются revert'ом симулируемой транзакции
Для включения таких путей в анализ используется оператор @withrevert, который добавляется после названия функции, например someFunction@withrevert(args)
При этом, если someFunction будет ревертнута, то она вернет какое-то случайное значение, а остальные переменные откатятся к своим значениям до транзакции
CVL так же имеет встроенную bool lastReverted, которая изменяется в зависимости от того, была ли последняя вызываемая функция reverted
Зачем это вообще нужно? Чтобы проверять, что некоторые пути действительно всегда недостижимы
Если наша @withRevert функция была ревертнута, то lastReverted становится true и возможно проверить что assert lastReverted. Потому что он теперь во-первых достижим, во-вторых true
Ссылки:
- Туториал, взятый за основу
- Спецификация
- Конфигурация
https://t.me/web3securityresearch