Invariant testing в Foundry: последовательности действий
В предыдущем уроке мы связали сценарии с требованиями. Теперь расширим порядок действий. Публикация и отключение могут происходить многократно, а заранее записанная цепочка из трёх вызовов рассматривает только один вариант истории.
Stateful-проверка генерирует последовательности обращений и наблюдает свойства накопленного состояния. Начнём с двух простых инвариантов и отдельного файла test/CourseCatalogInvariant.t.sol. В этой главе нет выполненной кампании: код пока не запускался, а ограниченность начального генератора объясняется явно.
Свойство состояния отличается от перехода
Переход отвечает на вопрос: что изменяется после выбранного действия? Например, разрешённая публикация должна заменить отпечаток и установить active. Инвариант спрашивает, какая связь остаётся верной после рассматриваемых действий: активная запись не должна иметь нулевой хеш, а адрес издателя остаётся заданным.
Эти вопросы дополняют друг друга. Свойство «если запись активна, хеш ненулевой» не требует, чтобы разрешённая публикация вообще была возможна. Программа, всегда отклоняющая изменения и сохраняющая пустой mapping, может удовлетворять ему. Поэтому положительные unit- и fuzz-сценарии сохраняются и после появления инвариантов.
Последовательность может случайно чередовать публикацию, повторную публикацию и отключение. Состояние внутри одной истории сохраняется между действиями. Это отличается от функции с параметрами из одиннадцатого урока, где одна заранее определённая история исследуется для разных входных величин.
Создаём отдельную проверяющую программу
Второй файл использует ту же прикладную реализацию и профиль forge-std. Наследование от Test выбранной библиотеки даёт доступ к средствам утверждений и настройки invariant-целей. Отдельный файл помогает не смешать подготовку обычных сценариев с подготовкой генератора последовательностей.
// SPDX-License-Identifier: MIT
pragma solidity 0.8.30;
import {Test} from "forge-std/Test.sol";
import {CourseCatalog} from "../src/CourseCatalog.sol";
contract CourseCatalogInvariantTest is Test {
CourseCatalog internal catalog;
address internal publisher = address(0xA11CE);
function setUp() public {
catalog = new CourseCatalog(publisher);
targetContract(address(catalog));
}
function invariantPublisherIsFixed() public view {
assertEq(catalog.publisher(), publisher);
}
function invariantActiveCourseHasDigest() public view {
(bytes32 digest, bool active) = catalog.courses(17);
if (active) assertTrue(digest != bytes32(0));
}
}Функции инвариантов имеют узнаваемый префикс invariant. Они читают состояние, а изменяющие действия выполняет генератор через выбранную цель. Не помещаем публикацию внутрь самой функции свойства: иначе она стала бы менять наблюдаемый объект вместо простого сравнения.
На текущем шаге второй инвариант относится только к курсу 17. Mapping не умеет сам перечислять все ключи, поэтому фразу «каждая активная запись имеет хеш» наш короткий код пока не проверяет. Ограничение наблюдения должно оставаться видимым рядом с формулировкой свойства.
Начальная цель имеет важное ограничение
Мы указали сам реестр через targetContract. Но случайный отправитель обычно не совпадает с единственным издателем. Большинство изменяющих вызовов может отклоняться с Unauthorized, оставляя состояние пустым. Кроме того, случайный огромный номер редко совпадёт с наблюдаемым 17.
Если будущая кампания в таком виде завершится без нарушения, это ещё не будет полезным исследованием жизненного цикла. Проблема не обязательно в свойстве: генератор может почти не достигать интересующих состояний. Далее настроим цель и добавим handler, который строит содержательные прикладные действия.
Этот промежуточный вариант сохранён для понимания архитектуры. Его нельзя выдавать за окончательную лабораторию реестра. В завершённом комплекте выбранный handler, ограниченные номера и независимое ожидание исправят эти ограничения, не отменяя запрет чужих отправителей.
Разбираем свойство на состояниях
Начальное состояние (0, false) удовлетворяет условной связи: запись неактивна, поэтому условие об активном хеше к ней не применяется. После публикации (digest, true) требуется ненулевой digest. После отключения (digest, false) свойство также сохраняется, поскольку хеш не обязан исчезать.
Ошибочная запись (0, true) должна нарушить инвариант. Однако запись (wrongDigest, true) с неправильным ненулевым хешем его не нарушит. Поэтому нужна более сильная независимая модель из пятнадцатого урока, способная сравнить конкретный ожидаемый выпуск, а не только ненулевую форму.
| Состояние курса 17 | Условный инвариант | Дополнительное требование |
|---|---|---|
| Пустая запись | Выполняется | Публикация должна быть возможна |
| Активный ненулевой хеш | Выполняется | Хеш должен совпасть с последним выпуском |
| Неактивный старый хеш | Выполняется | Отключение обязано сохранить его |
| Активный нулевой хеш | Нарушается | Нулевая публикация должна отклоняться |
Отдельные свойства могут иметь отдельные истории
При чтении отчёта важно понимать, как выбранная версия инструмента организует кампании для разных функций инвариантов. Не следует считать, что два свойства автоматически наблюдали одну идентичную случайную историю и совместно доказали одно отношение. Если нужна согласованная проверка нескольких полей, их удобно сравнить в одной функции на одном состоянии.
В нашем будущем сильном инварианте digest и активность каждого выбранного номера будут сопоставляться с моделью вместе. Простое свойство неизменного издателя можно сохранить отдельно: оно имеет собственный понятный смысл и не требует знать все выпуски.
Проверка состояния после действий также не заменяет наблюдение событий внутри каждого действия. Если журнал относится к договору конкретной публикации, его сравнивают в соответствующем переходе или отдельном сценарии. Инвариант конечного mapping не восстанавливает автоматически все сообщения промежуточной истории.
Не делаем вывод о бесконечном времени
Отдельно рассмотрим историю, которая отключает курс и публикует его снова. Простое условие ненулевого активного хеша не заметит, если вторая публикация оставит старый ненулевой выпуск. Модель последнего разрешённого действия должна ожидать новый аргумент. Это пример ошибки, которую нельзя обнаружить добавлением количества повторений к слабому свойству: сначала необходимо усилить само сравнение результата.
После усиления старое условие можно оставить как удобную диагностику формы записи. Оно объясняет одно отношение быстро, тогда как модель показывает точный выпуск. Небольшие свойства полезны, если их границы понятны и они не выдаются за замену более полного прикладного договора.
У будущей кампании будут число историй и максимальная глубина. Это конечный бюджет, а не рассмотрение всех возможных последовательностей любой длины. Успешный результат означает отсутствие найденного нарушения при заданной модели и параметрах; для более широкого доказательства нужны иные методы.
При подготовке сохраняем также начальное состояние, целевые методы и область отправителей. Даже одинаковая глубина не делает две кампании сопоставимыми, если одна выполняет публикации, а другая только получает ошибки доступа. Полезность исследования определяется достигнутыми прикладными переходами.
В следующем уроке ограничим целевые методы явно. Устройство последовательностей описано в руководстве Foundry по инвариантам, вспомогательный API — в StdInvariant 1.9.7. Оглавление курса.