一个用于展示已证明（而非运行得出）的密码分析结果的榜单。
一道挑战固定两个世界以及你必须证明的命题。你编写一个敌手，以及一个证明该敌手能区分这两个世界的证明。胜利在于证明本身：不执行任何东西、不采样、不重放，也没有人来阅读提交内容以判定它是否算数。
状态：验证器可运行。 一个 verify: issue 会在 CI 中针对挑战所固定的类型进行精化，并用 #print axioms 进行审计；判定结果以评论形式返回。记录仍由人工添加到 scoring/ledger.json。
这是一个独立的 Lake 项目。它把数学部分作为固定到某个修订版本的 git 依赖引入，因此榜单是针对该模式的固定命题进行验证的：
require RandomSystems from git
"https://github.com/MarcIlunga/random-systems.git" @ "08aec7a7"
构建时间是缓存，不是问题：Mathlib 的 oleans 通过
lake exe cache get 从其 CDN 获取，而约 400 MB 的固定修订版和挑战 oleans 位于
Actions 缓存中，以 manifest 和我们自己的源代码为键。
| 路径 | 说明 |
|---|---|
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 | 验证一次提交：挑战 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
verify.yml 在推送和拉取请求时运行：--check 门禁、配置 lint、站点检查，以及验证器必须接受和必须拒绝的一组提交——一个 sorry、一个 native_decide、一个未知挑战、一个零优势、一个没有 Lean 块的正文。workflow_dispatch 按需验证单个提交，而无需开启 issue。
submission.yml 分两个作业处理 verify: issue。第一个作业解析不可信输入，并且不持有任何写入权限；第二个作业下载其判定结果并发布评论。这种拆分是 lean-golf 的做法，也正是 issue 正文无法触及 token 的原因。
一个提交是一个声明，其类型由挑战固定：
-- 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 导入一个已经声明了
strategy/verdict/attackWins 的 Challenge.lean 会失败，并报错 "has already been declared"。
将提交内容设为受信任类型的值可消除冲突，并将验证器的类型检查缩减为单个 #check。
必须满足两件事，且两者都不被信任。
数字是命题的一部分。 平台将它们写入
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，优势 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 )
每单位优势的查询次数；其以二为底的对数就是该攻击所反驳的安全级别（以比特计）。越低越好。低估你的优势会提高分数，因此声称低于你所能证明的并无任何好处。
e 是每个挑战各自的参数，没有默认值。对于判定类博弈，e = 2——优势 α 大约需要 α⁻² 次重复才能放大——而对于搜索类博弈，e = 1。这两种约定都见于文献中，且这种不一致是已知的（Micciancio–Walter，On the Bit Security of Cryptographic Primitives），因此每个挑战都会声明其采用哪一种。
标准值（par）是设计者自己的主张，取自规范，因此任何地方都不会出现对攻击难度的猜测。低于标准值即意味着该主张被攻破。
记录按分数从优到劣排列。这就是全部排名。