Formal Verification, часть 3.2

Что содержит .spec файл

👨‍💻 Sorts: Uninterpreted Sorts по сути своей являются абстрактными типами данных, которые можно сравнивать друг с другом. А неинтерпретируемыми они называются, потому что существуют интерпретируемые: в текущем контексте это все Solidity типы
Пример

sort Foo;

ghost bar(Foo, Foo) returns Foo;

rule myRule {
   Foo x;
   Foo y;
   Foo z = bar(x, y);
   assert x == y && y == z;
}

Создаем тип данных Foo, привязываем его к призрачной переменной bar и используем в правиле. Пока не использовал на практике, но пишут что в некоторых ситуациях проще делать так, ладно


👨‍💻 Ghosts: Призрачные/гост/ghost переменные это почти как обычные переменные, но они могут передавать информацию между rules/правилами и hooks/хуками, и использоваться в саммари методов. Во втором случае это уже ghost function
Пример

ghost uint x;
ghost mapping(address => mathint) balances;

но гост переменные не могут быть кортежами, зато могут содержать в себе условия относительно их самих, которые нельзя нарушать


👨‍💻 Hooks: Хуки позволяют привязаться кодом к низкоуровневым операциям, например к чтению/записи в STORAGE. Их определенное количество и каждый имеет свой шаблон применения, работают в связке с ghost переменными
Пример

ghost mathint sum_of_balances {
    init_state axiom sum_of_balances == 0;
}

hook Sstore _balances[KEY address a] uint new_value (uint old_value) STORAGE {
    // when balance changes, update ghost
    sum_of_balances = sum_of_balances + new_value - old_value;
}

Такая вот верхушка айсберга. Сложность формальной верификации отчасти в том, что она использует свой язык (но другого пути нет), который содержит огромное количество ньюансов. У меня на данный момент исписано около 20 страниц формата а4 с разбором тех ошибок, которые мне выдавал prover и это я можно сказать только начал

Вторая сложность в том, что сама логика проверки свойств кода не похожа на обычное тестирование. Например, очень сложно привыкнуть к предположению, что любая функция тебе вернет что угодно. Даже если у нее на входе require с ограничением, даже если она должна возвращать только положительные значения

https://t.me/web3securityresearch