Ghost state в Foundry: модель ожидаемого выпуска
В предыдущем уроке чужие попытки сохраняли снимок записи. Однако простой инвариант ненулевого активного хеша всё ещё мог принять неправильный выпуск. Теперь handler будет хранить независимое ожидание по каждому выбранному номеру.
Такое вспомогательное состояние часто называют ghost state. Оно существует в проверяющей программе и не становится частью прикладного контракта. Усилим handler и заменим наблюдаемое свойство точным сравнением digest и активности. Код пока не исполнялся; согласованность модели и реестра является ожидаемым результатом будущей кампании.
Модель развивается из действий
После успешной разрешённой публикации ожидаемый хеш становится равным переданному аргументу, а флаг — true. После разрешённого отключения изменяется только флаг. Чужие попытки не меняют ожидание. Это три правила прикладного договора, которые не требуют чтения записанного результата для построения модели.
Добавим структуру и mapping в CatalogHandler. Публичный getter модели нужен invariant-файлу для сравнения, но не входит в список генерируемых действий. Селекторы по-прежнему ограничивают поверхность четырьмя методами из предыдущего урока.
struct ExpectedEdition {
bytes32 digest;
bool active;
}
mapping(uint256 => ExpectedEdition) public expected;Для ещё не опубликованного номера mapping возвращает (0, false). Это соответствует пустому реестру. При создании нового handler не нужно предварительно заполнять двадцать записей нулями: правила значений по умолчанию дают одинаковое исходное ожидание для всей выбранной области.
Обновляем разрешённую публикацию
Заменим тело publish в handler. Преобразования входов остаются прежними, а после нормально завершённого прикладного вызова записывается ожидаемый выпуск. Если вызов неожиданно отклоняется, последующее присваивание не выполняется обычным путём.
function publish(uint256 rawId, bytes32 rawDigest) external {
uint256 id = bound(rawId, 1, 20);
bytes32 digest = rawDigest == bytes32(0)
? bytes32(uint256(1))
: rawDigest;
vm.prank(publisher);
catalog.publish(id, digest);
expected[id] = ExpectedEdition(digest, true);
}Обратите внимание: мы сохраняем digest, выбранный до вызова, а не значение getter после него. Если реализация записала постоянный хеш или хеш другого номера, модель продолжает ожидать именно аргумент разрешённой публикации. Последующее сравнение должно обнаружить ошибку.
Модель не считает ошибочную запись успешным эталоном только потому, что вызов завершился без revert. Нормальное завершение позволяет перейти к сравнению результата, но не гарантирует его правильность. Это ключевое различие между наблюдением технического успеха вызова и подтверждением прикладного договора.
Выбираем отключение по ожиданию
В предыдущем handler активность читалась из реестра для решения, выполнять ли отключение. Теперь используем собственное ожидаемое состояние. Так неверный флаг исследуемой программы не определяет всю будущую историю и не мешает заметить её отклонение от модели.
function deactivate(uint256 rawId) external {
uint256 id = bound(rawId, 1, 20);
if (!expected[id].active) return;
vm.prank(publisher);
catalog.deactivate(id);
expected[id].active = false;
}Отпечаток в модели сохраняется. Если прикладная реализация удаляет struct целиком, ожидаемое состояние остаётся (previousDigest, false), а реестр возвращает (0, false). Такое отличие не замечалось слабой условной проверкой активности и становится видимым точному сравнению.
Неактивная ожидаемая запись по-прежнему приводит к пропуску разрешённого отключения. Отрицательный сценарий повторного отключения находится в обычном наборе функций. Handler направлен на содержательные разрешённые переходы и чужие попытки; все возможные ошибки состояния он не обязан смешивать в одном маршруте.
Сравниваем все наблюдаемые курсы
В invariant-файле заменим invariantActiveCoursesHaveDigests более сильной функцией. Инвариант неизменного издателя оставим отдельно. Оба getter возвращают одинаковую по форме пару, но значения происходят из разных оснований.
function invariantCoursesMatchExpectedEditions() public view {
for (uint256 id = 1; id <= 20; ++id) {
(bytes32 wantedDigest, bool wantedActive) = handler.expected(id);
(bytes32 actualDigest, bool actualActive) = catalog.courses(id);
assertEq(actualDigest, wantedDigest);
assertEq(actualActive, wantedActive);
}
}Цикл проверяет также соседние номера, не изменённые последним действием. Если публикация 17 неожиданно повреждает 18, сравнение всей малой области предназначено для обнаружения такого нарушения. Для бесконечного по практическому размеру пространства ключей подобного обхода нет; выбранная область остаётся явным ограничением.
Модель не должна обновляться в publishAsReader и deactivateAsReader. Эти методы ожидают запрет и неизменность записи. Их снимки до и после сохраняются как локальная диагностика, а общий инвариант дополнительно сравнивает текущее состояние с независимым выпуском.
Изменённый пример с удалением хеша
Представим историю: издатель публикует first, затем отключает курс. Ошибочная реализация делает delete courses[id]. Обычный инвариант формы не замечает проблемы, потому что запись неактивна. Ghost state оставляет first, следовательно, точное сравнение digest должно нарушиться.
Если автор модели тоже удалит запись, ошибочные программы согласуются друг с другом. Поэтому модель рецензируется по таблице требований, а не копируется построчно из реализации. У нас правило деактивации выражено отдельным присваиванием флага, что делает сохранение отпечатка заметным при чтении.
Для замены выпуска модель хранит только последний допустимый digest. История прошлых хешей не нужна для этого свойства. Если требование расширяется до последовательности событий или сохранённых редакций, оно должно получить собственную модель наблюдения и данные; текущий mapping не обещает этого автоматически.
Согласуем начальное состояние
Наш пример создаёт новый пустой реестр и новый пустой handler вместе. Если вместо этого подключить реестр с уже опубликованными курсами, нулевое ожидание станет неверным. Для такой кампании потребуется отдельный доверенный начальный снимок, его происхождение и ясное решение о том, почему эти данные принимаются как исходный договор.
Чтение всех существующих записей в модель перед началом может быть допустимой подготовкой исследования дальнейших переходов, но не подтверждает правильность прежней истории. Эти два вывода нельзя смешивать. Локальная новая лаборатория избегает такого допущения: оба объекта начинают с состояния, заданного конструктором и правилами mapping.
Если позднее добавятся начальные публикации в setUp, их ожидаемые значения должны одновременно попасть в модель из явно выбранных аргументов. Простое изменение только реестра породит рассогласование до случайной истории. Благодаря такому правилу подготовка становится частью проверяемого договора, а не скрытым источником значений, о которых рецензент узнаёт только после неожиданного сообщения об ошибке.
Не прячем модель за результатом программы
Проверяющий код имеет право читать реестр для фактического сравнения, но не для определения правильного ответа. Разделение легко потерять при удобном рефакторинге: функция «синхронизировать модель» из getter после каждого действия делает инвариант почти бессмысленным.
Также не добавляем catch, который записывает в модель текущий результат при любом отказе. Неожиданный отказ разрешённого действия должен оставаться заметным, а его политика будет задана следующей главой. Согласованная пустота после всех отвергнутых публикаций не является доказательством работающей библиотеки.
Теперь у каждого наблюдаемого номера есть независимый текущий выпуск. В следующем уроке добавим категории действий и политику откатов. Модели handler рассматриваются в руководстве Foundry, mapping — в Solidity 0.8.30. Оглавление курса.