break-golf

Доска для результатов криптоанализа, которые доказаны, а не выполнены.

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

Статус: верификатор работает. Issue с verify: разворачивается в CI против закреплённого типа задачи и проверяется с помощью #print axioms; вердикт возвращается в виде комментария. Записи по-прежнему добавляются в scoring/ledger.json вручную.

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

require RandomSystems from git
  "https://github.com/MarcIlunga/random-systems.git" @ "08aec7a7"

Время сборки — это кэш, а не проблема: oleans Mathlib поступают из его CDN через lake exe cache get, а ~400 МБ oleans закреплённой ревизии и челленджей лежат в кэше Actions с ключом по манифесту и нашим собственным исходникам.

Структура

Путь	Что это
challenges/<name>/Challenge.lean	Доверенный. Фиксирует точные типы, которые должна реализовать отправка. Не входит ни в одну загрузку.
challenges/<name>/Cost.lean	Генерируется платформой для каждой отправки на основе чисел из формы.
challenges/<name>/config.json	Оценка, par, разрешённые аксиомы, таймаут. Единственный файл, который вы редактируете, чтобы добавить челлендж.
challenges/<name>/Solve.template.lean	Скелет, который заполняет отправитель.
tools/manifest.py	Выводит docs/data/manifest.json из challenges/.
tools/ledger.py	Выводит docs/data/ledger.json из scoring/ledger.json, оценивая и сортируя записи.
tools/record.py	Добавляет проверенную отправку в реестр. Отклоняет всё, что не имеет статуса proved.
tools/verify.py	Проверяет одну отправку: id челленджа как argv[1], тело на stdin, JSON-вердикт на stdout. Тот же интерфейс, что у lean-golf.
tools/lint_challenges.py	Каждый конфиг челленджа содержит всё, что нужно таблице и верификатору.
tools/check_site.py	Статический сайт может загружать и отображать свои сгенерированные данные.
scoring/ledger.json	Набор записей.
docs/	Сайт на GitHub Pages. Статический; читает только два сгенерированных файла.
examples/	Тестовые фикстуры: отправка, которая проходит проверку и ничего не выигрывает, и её близнец с завышенными притязаниями.

python3 tools/manifest.py          # rewrite the manifest
python3 tools/manifest.py --check  # fail if stale
python3 tools/ledger.py            # rescore and sort the records
python3 tools/lint_challenges.py   # configs are complete
python3 tools/check_site.py        # the site can render what the tools generate

printf '%s' "$BODY" | python3 tools/verify.py spoc128    # one submission

CI

verify.yml запускается при push и pull request: проверки --check, линт конфигурации, проверка сайта и набор отправок, которые верификатор должен принимать и должен отклонять — sorry, native_decide, неизвестный челлендж, нулевое преимущество, тело без блока Lean. workflow_dispatch проверяет одну отправку по требованию без открытия issue.

submission.yml обрабатывает issue verify: в двух заданиях. Первое разбирает недоверенный ввод и не имеет write-скоупов; второе скачивает его вердикт и публикует комментарий. Это разделение взято из lean-golf, и именно поэтому тело issue не может добраться до токена.

Отправляющий никогда не пишет утверждение

Отправка — это одно объявление, населяющее тип, который фиксирует челлендж:

-- Challenge.lean, trusted. The verifier builds its own copy.
def score : Golf.Score := ⟨budget, advNum, advDen⟩   -- from the submission form

structure Solution where
  strategy : game.Param → PFunDDS.DDE game.Query game.Response
  verdict  : List (game.Query × Option game.Response) → Bool
  wins     : Golf.Attack.Wins (G := game) ⟨strategy, verdict⟩ score.budget score.advantage

-- Solve.lean, the upload.
def solution : Challenge.SpoC128.Solution where
  strategy := …
  verdict  := …
  wins     := …

Одна структура вместо трёх свободных имён, потому что свободные имена конфликтуют: Solve.lean, который импортирует Challenge.lean, уже объявляющий strategy/verdict/attackWins, завершается ошибкой "has already been declared". Превращение отправки в значение доверенного типа устраняет конфликт и сводит проверку типов верификатором к одному #check.

Почему безопасно, что отправитель выбирает оценку

Должны выполняться два условия, и ни одно из них не принимается на веру.

Числа являются частью утверждения. Платформа записывает их в Cost.lean, Challenge.lean строит score из них, и score появляется внутри типа Solution.wins. Изменение числа меняет то, что должно быть доказано.

Отправка должна принадлежать нашему типу. Шаг аудита импортирует доверенный челлендж вместе с отправкой и разворачивает

example : Challenge.SpoC128.Solution := Solution.SpoC128.solution

поэтому заявка, объявляющая собственный Challenge.SpoC128.Solution, конфликтует с нашей, а заявка, использующая любой другой тип, не проходит проверку типов. Без этого шага заявка, которая просто никогда не импортирует challenge, может определить тривиальную структуру с тем же именем и быть «доказанной» при 0 битах — эта дыра была реальной, и обе атаки теперь являются CI-кейсами.

Количество запросов не требует отдельного доказательства. Это не утверждение о готовом противнике; это аргумент конструктора. Attack.distinguisher q — это DDD.ofDDE strategy q verdict, усечённый на q по построению, и Attack.silent_past доказывает, что он не выдаёт ничего сверх этого. Невозможно перерасходовать бюджет, поэтому проверять нечего.

budget, advNum и advDen берутся из формы заявки, и им не доверяют. В этом нет необходимости: платформа подставляет их в Cost.lean, Challenge.lean строит score из них, а score появляется внутри Solution.wins. Таким образом, числа являются частью утверждения, а не заявлением о нём.

Проверено на реальной атаке SpoC-128:

Утверждение	Результат
budget = 3, преимущество 1	компилируется — честное утверждение
budget = 1, преимущество 1	не проходит — Wins 1 1 — это другая, более сильная теорема
budget = 3, преимущество 2	не проходит — ничто не может превысить преимущество 1

И нет стимула занижать: score = log₂(budget / advantage^e), поэтому меньшее заявленное преимущество или больший заявленный бюджет повышают счёт. Оба направления хуже. Единственный ход — максимально точное утверждение, которое вы действительно можете доказать.

Ещё четыре отказа, которые верификатор выносит, ничего не читая:

Чит	Вердикт
ослабить утверждение	несовпадение типов с закреплённым Solution
добавить удобную гипотезу	то же самое
sorry доказательство	sorryAx отсутствует в permitted_axioms
native_decide / повышенный maxHeartbeats	отклоняется сразу

Подсчёт очков

Ничего не фиксируется заранее. Для схемы, которую никто не изучал, какое преимущество достижимо при каких затратах — это исследовательский вопрос, поэтому любая цель — догадка, а цель, установленная слишком высоко, оценивает подлинный различитель 2⁻³⁰ как ноль. Вместо этого таблица измеряет результат:

score = log₂( budget / advantage^e )

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