Песочница

Квитанции решений и CSK Reference

Проверяемое подмножество Lispex служит исходным языком для CSK Reference. Зафиксируйте вход, получите переносимую квитанцию, проверьте её офлайн, а после изменения правил прогоните корпус заново.

Начиная с v1.3 проверяемое подмножество Lispex служит публичным исходным языком для CSK Reference. Это намеренно узкое утверждение. Программы Lispex по-прежнему выполняет эталонный интерпретатор; проверяемое подмножество — та часть языка, где каждое вычисление оставляет след, который позже можно проверить заново на своей машине.

Как это работает

Напишите небольшое решающее правило и зафиксируйте вход, на котором оно работает. Вычисление оставит квитанцию — один переносимый файл формата csk.differential-receipt/v0, связывающий правило, зафиксированный вход и ответ хешами.

Дальше:

  • lispex verify <receipt> проверяет квитанцию и всё, на что она ссылается, офлайн. Ни сети, ни сервисов — достаточно самого файла.
  • lispex replay <corpus> --against <version-or-receipts-dir> после изменения правила прогоняет закоммиченный корпус решений против закреплённой версии или каталога квитанций и показывает, какие ответы разошлись.

Что входит в проверяемое подмножество

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

  • фиксированный набор форм в традиции R7RS — без макросов и скрытого состояния;
  • закреплённые встроенные процедуры и входные данные, которые явно привязывает хост, а не запрашивает само правило;
  • галерея правил, ожидаемые артефакты которой лежат рядом с самими правилами;
  • JSON-контракты с точностью до байта для квитанций, отчётов, графов, манифестов и релизных бандлов.

О чём квитанция говорит — и о чём молчит

Квитанция показывает, что конкретное правило на конкретном зафиксированном входе дало конкретный ответ и что записанные артефакты согласованы между собой. Она не говорит, что решение было к кому-то применено, когда и кем, и не заменяет ничью проверку. Это дело отдельных слоёв — подписи, меток времени, развёртывания и ревью.

npm-дистрибутив verify и replay — инструмент проверки артефактов публичной спецификации. Он сверяет байты и хеши; он не выполняет исходный код Lispex и не заменяет эталонный интерпретатор.

Где что искать

  • Песочница на этом сайте выполняет правила проверяемого подмножества прямо в браузере.
  • CLI, установленный через npm install -g lispex, запускает файлы командой lispex run, а квитанции и корпусы проверяет командами lispex verify и lispex replay. Примеры есть в разделе «Начало работы».
  • Документы спецификации — определение проверяемого подмножества, формат квитанции, контракты отчётов verify и replay — выходят вместе с корпусом галереи решений отдельной публичной поставкой CSK Reference. Ссылка появится здесь, когда определится её публичный адрес.