証明された暗号解析結果のためのボードであり、実行されるものではありません。
チャレンジは2つの世界と、あなたが証明しなければならない命題を固定します。あなたは敵対者と、それが両者を区別するという証明を書きます。勝利とはその証明です。何も実行されず、サンプリングも再生もされず、それが有効かどうかを判断するために人間が提出物を読むこともありません。
ステータス: 検証器は動作します。 verify: issue は、チャレンジに固定された型に対して CI で展開（elaborate）され、#print axioms で監査されます。判定はコメントとして返されます。記録は依然として手作業で scoring/ledger.json に追加されています。
これはスタンドアロンの Lake プロジェクトです。数学部分をリビジョンに固定された git 依存関係として取り込むため、ボードはそのモードの固定された命題に対して検証を行います:
require RandomSystems from git
"https://github.com/MarcIlunga/random-systems.git" @ "08aec7a7"
ビルド時間はキャッシュであり、問題ではありません。Mathlib の olean は CDN から
lake exe cache get で取得され、約 400 MB の固定リビジョンとチャレンジの olean は
マニフェストと自前のソースをキーとした Actions キャッシュに格納されています。
| パス | 内容 |
|---|---|
challenges/<name>/Challenge.lean | 信頼済み。 提出物が満たすべき正確な型を固定する。アップロードには含まれない。 |
challenges/<name>/Cost.lean | フォームの数値から提出物ごとにプラットフォームが生成する。 |
challenges/<name>/config.json | スコアリング、パー、許可される公理、タイムアウト。チャレンジを追加する際に編集する唯一のファイル。 |
challenges/<name>/Solve.template.lean | 提出者が記入するスケルトン。 |
tools/manifest.py | challenges/ から docs/data/manifest.json を導出する。 |
tools/ledger.py | scoring/ledger.json から docs/data/ledger.json を導出し、レコードをスコアリングしてソートする。 |
tools/record.py | 検証済みの提出物を台帳に追加する。proved でないものは拒否する。 |
tools/verify.py | 1 件の提出物を検証する。チャレンジ id を argv[1] に、本文を stdin に、JSON の判定結果を stdout に。lean-golf と同じインターフェース。 |
tools/lint_challenges.py | すべてのチャレンジ設定がボードと検証器に必要なものを備えているか確認する。 |
tools/check_site.py | 静的サイトが自身の生成データを読み込んでレンダリングできるか確認する。 |
scoring/ledger.json | レコードセット。 |
docs/ | GitHub Pages サイト。静的で、生成された 2 つのファイルのみを読み込む。 |
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
verify.yml は push と pull request で実行されます。--check ゲート、設定の lint、サイトチェック、そして検証器が受け入れるべき／拒否すべき一連の提出物 — sorry、native_decide、未知のチャレンジ、ゼロアドバンテージ、Lean ブロックを含まない本文 — です。workflow_dispatch は issue を開かずにオンデマンドで 1 件の提出物を検証します。
submission.yml は verify: issue を 2 つのジョブで処理します。最初のジョブは信頼できない入力を解析し、書き込みスコープを一切持ちません。2 番目のジョブはその判定をダウンロードしてコメントを投稿します。この分割は lean-golf のものであり、issue 本文がトークンに到達できない理由でもあります。
提出物は、チャレンジが固定する型を inhabit する 1 つの宣言 です:
-- 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 := …
3 つの緩い名前ではなく 1 つの構造にしているのは、緩い名前が衝突するからです。strategy/verdict/attackWins をすでに宣言している Challenge.lean をインポートする Solve.lean は、「すでに宣言されています」 というエラーで失敗します。提出物を信頼された型の値にすることで衝突が解消され、検証者の型チェックは単一の #check にまで削減されます。
成立しなければならないことが 2 つあり、どちらも信頼に基づいてはいません。
数値は命題の一部です。 プラットフォームがそれらを Cost.lean に書き込み、Challenge.lean がそれらから score を構築し、score は Solution.wins の型の中に現れます。数値を変更すれば、証明すべき内容が変わります。
提出物は我々の型に属していなければなりません。 監査ステップは、信頼されたチャレンジを提出物とともにインポートし、以下を展開します
example : Challenge.SpoC128.Solution := Solution.SpoC128.solution
自前の Challenge.SpoC128.Solution を宣言する提出物は我々のものと衝突し、それ以外の型を使う提出物は型チェックを通らない。このステップがなければ、単にチャレンジをインポートしない提出物が同名の自明な構造体を定義し、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、advantage 1 | コンパイル成功 — 正直な主張 |
budget = 1、advantage 1 | 失敗 — Wins 1 1 は異なる、より強い定理である |
budget = 3、advantage 2 | 失敗 — advantage 1 を超えるものは存在し得ない |
そして過少申告のインセンティブも存在しない: score = log₂(budget / advantage^e) であるため、主張する advantage を小さくするか、主張する budget を大きくすると、スコアは上がる。どちらの方向も不利になる。唯一の手は、実際に証明できる最も厳密な主張である。
検証器が何も読まずに下す、さらに 4 つの却下:
| 不正行為 | 判定 |
|---|---|
| 主張を弱める | 固定された Solution に対する型不一致 |
| 都合のよい仮説を追加する | 同上 |
証明を sorry する | sorryAx は permitted_axioms に含まれない |
native_decide / maxHeartbeats の引き上げ | 即座に却下 |
事前に固定されたものは何もない。誰も研究していない方式において、どのコストでどの advantage に到達できるかは研究課題そのものであるため、あらゆる目標値は推測にすぎない——そして高すぎる目標値を設定すると、本物の 2⁻³⁰ 識別器がゼロと採点されてしまう。ボードは代わりに結果を測定する:
score = log₂( budget / advantage^e )
単位あたりのクエリの優位性。その2を底とする対数が、攻撃が反証するセキュリティレベル（ビット単位）である。低いほど良い。優位性を過小に申告するとスコアは上がるため、証明できる以上に低く主張しても得るものは何もない。
e はチャレンジごとに定まり、デフォルト値はない。判定ゲームでは e = 2 であり、優位性 α を増幅するにはおよそ α⁻² 回の繰り返しが必要となる。探索寄りのゲームでは e = 1 である。どちらの慣習も文献に存在し、その不一致は知られている（Micciancio–Walter, On the Bit Security of Cryptographic Primitives）。したがって各チャレンジはどちらを使うかを明示する。
パーは設計者自身の主張であり、仕様書から取られているため、攻撃難度に関する推測がどこにも現れない。パー未満はその主張の破綻である。
レコードはスコアの良い順に並ぶ。それがランキングのすべてである。