Foundry: независимая модель ожидаемого результата

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

Подготовим независимую ожидаемую запись и сравнение с контрактом. Модель не читает результат courses, чтобы решить, что должно получиться. Её состояние вычисляется из выбранных входов и договора разрешённых переходов. Исходники пока не исполнялись; это разработанная схема проверки, а не подтверждённое поведение приложения.

Почему чтение результата не создаёт ожидание

Представим такую проверку: сначала получить digest из getter, затем снова вызвать getter и сравнить два чтения. Если контракт хранит неправильный хеш постоянно, оба результата совпадут. Мы проверим стабильность чтения, но не соответствие опубликованному выпуску.

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

Независимость не означает создание второго большого контракта с теми же ветвями и возможными ошибками. Небольшая модель может быть гораздо проще реализации: хранить два ожидаемых поля и обновлять их только в явно разрешённых действиях сценария. Чем меньше лишних деталей, тем легче рецензировать её договор.

Описываем ожидаемую запись

Добавим в CourseCatalogTest отдельную структуру и mapping. Это состояние проверяющей программы, а не новая часть CourseCatalog. Значения по умолчанию соответствуют пустому курсу: нулевой отпечаток и неактивный флаг.

struct ExpectedEdition {
    bytes32 digest;
    bool active;
}

mapping(uint256 => ExpectedEdition) internal expected;

function assertMatchesModel(uint256 id) internal view {
    ExpectedEdition memory model = expected[id];
    assertCourse(id, model.digest, model.active);
}

Функция читает ожидаемое состояние из собственного mapping и затем использует ранее написанный getter-сценарий. Здесь важно направление данных: модель передаёт ожидание проверке, а исследуемый реестр предоставляет наблюдаемое значение. Мы не присваиваем expected[id].digest результату catalog.courses(id).

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

Развиваем модель после действия

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

function testFuzzLifecycleMatchesModel(
    uint256 id,
    bytes32 first,
    bytes32 second
) public {
    vm.assume(id != 0);
    vm.assume(first != bytes32(0));
    vm.assume(second != bytes32(0));

    vm.prank(publisher);
    catalog.publish(id, first);
    expected[id] = ExpectedEdition(first, true);
    assertMatchesModel(id);

    vm.prank(publisher);
    catalog.publish(id, second);
    expected[id] = ExpectedEdition(second, true);
    assertMatchesModel(id);

    vm.prank(publisher);
    catalog.deactivate(id);
    expected[id].active = false;
    assertMatchesModel(id);
}

При неожиданном отказе разрешённой публикации исполнение не должно продолжать обычный путь обновления модели. В этой функции нет перехвата ошибки: такой отказ нарушает сценарий. Поэтому присваивание после вызова означает переход, который действительно завершился нормально в рамках будущего исполнения.

Для деактивации изменяется только active. Поле digest сохраняется в модели без обращения к текущему getter. Если реализация ошибочно обнулит отпечаток, сравнение должно обнаружить отличие. Это та же прикладная граница, которую мы вручную рассматривали в девятом уроке, но теперь она выражена отдельным состоянием.

Добавляем запрещённую попытку

После первой публикации можно вставить вызов читателя с second, ожидающий Unauthorized. Модель в этот момент не обновляется. После отказа assertMatchesModel(id) должна по-прежнему сравнивать (first, true) с наблюдаемой записью.

Такое правило отличает намерение от результата. Сам факт передачи second в запрещённый вызов не делает его текущим выпуском. Модель обновляется по договору успешно разрешённого действия, а не по любому пользовательскому желанию. Этот принцип важен и для внешнего приложения, где отправленная транзакция ещё может отклониться.

Если handler позднее будет перехватывать ошибки, потребуется решить, какие отказы ожидаемы и какие должны останавливать проверку. Нельзя молча считать любой отказ приемлемым и синхронизировать модель с ним. Иначе повреждённая реализация, отвергающая все публикации, может выглядеть согласованной с пустым ожиданием.

Разбираем возможную ошибку модели

Предположим, автор после deactivate запишет expected[id] = ExpectedEdition(0, false). Тогда модель повторит ошибочное понимание договора удаления. Если реализация тоже удаляет запись, сравнение пройдёт, хотя требование сохранения хеша нарушено. Независимая структура не освобождает от чтения требований.

Поэтому сохраняем таблицу переходов из второго и девятого уроков как основание для модели. Для каждого обновления можно назвать строку договора: публикация заменяет оба поля, отключение меняет только активность. Рецензент должен понимать это без чтения внутренней реализации контракта.

Действие	Изменение ожидания	Основание
Успешная публикация	Новый хеш, true	Текущий выпуск заменён
Успешное отключение	Только false	Хеш последнего выпуска сохраняется
Запрещённая попытка	Нет изменений	Откат сохраняет прежнее состояние

Пустая согласованность ещё не полезная работа

Если не выполнить ни одного изменяющего действия, пустой реестр и пустая модель совпадут. Такое сравнение правильно описывает начальное состояние, но ничего не рассказывает о переходах. Поэтому в нашей функции публикации находятся непосредственно перед обновлением ожидания и сравнением; их нельзя заменить условием, которое чаще всего пропускает работу.

Позднее при длинной генерации понадобится наблюдать количество содержательных операций. Согласованность модели после сотни бесполезных чтений не равна исследованию сотни замен выпуска. Здесь действия заданы явно и каждый шаг имеет прикладной результат. Для handler мы сохраним этот принцип, но добавим счётчики попыток и реально выполненных переходов, чтобы будущее чтение отчёта не сводилось к одному слову «успешно».

Ограничиваем наблюдаемую область

Наш mapping модели не перечисляет все возможные ключи автоматически. Для проверки нескольких курсов надо сохранить выбранные номера и сравнить каждый из них. Проверка только последнего изменённого ключа может пропустить повреждение соседней записи, поэтому будущий stateful-handler будет работать с ограниченным набором наблюдаемых курсов.

Здесь история заранее задана: публикация, замена, отключение. Она не охватывает произвольное число повторений и переключений ролей. Это следующий уровень развития лаборатории, а не недостающий параметр текущей функции. Сначала мы сделали ожидание независимым, затем расширим порядок действий.

При подготовке отчёта различаем три результата: модель сформулирована, исходник записан, кампания выполнена. Сейчас выполнены первые два пункта. В следующем уроке разберём, что покрытие кода может сказать о таком наборе сценариев. Общий подход к stateful-моделям описан в руководстве Foundry по инвариантам. Оглавление курса.

Оглавление серии