break-golf

一个用于展示密码分析结果的看板，这些结果是经过证明的，而非运行出来的。

Challenge 固定两个世界以及你必须证明的命题。你编写一个敌手和一个证明，证明它能区分这两个世界。胜利就是证明本身：不会执行、采样或重放任何东西，也没有人类阅读提交内容来决定其是否有效。

状态：概念验证。 站点是静态的，提交会打开一个 GitHub issue，由人工判断。目前还没有 Lean 验证器作为后端。

布局

python3 tools/manifest.py          # rewrite the manifest
python3 tools/manifest.py --check  # fail if stale
python3 tools/ledger.py            # rewrite the ledger with scores and frontier
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 门禁、配置 lint、站点检查，以及一组验证器必须接受和必须拒绝的提交——一个 sorry、一个 native_decide、一个未知的挑战、一个零优势、一个没有 Lean 代码块的正文。workflow_dispatch 可按需验证一次提交，而无需打开 issue。

submission.yml 分两个 job 处理 verify: issue。第一个解析不受信任的输入，并且不持有任何写入权限；第二个下载其判定并发布评论。这种拆分来自 lean-golf，也正是 issue 正文无法触达令牌的原因。

提交者永远不会编写命题本身

这就是整个机制，与 trailofbits/lean-golf 用于 proof golf 的机制相同。验证器构建它自己的 Challenge.lean 副本。一次提交只提供：

def strategy : game.Param → PFunDDS.DDE game.Query game.Response
def verdict  : List (game.Query × Option game.Response) → Bool
theorem attackWins : attack.Wins score.budget score.advantage

外加表单上的 budget 和 advantage。attack 和 score 是在 Challenge.lean 中由这些数字组装而成的，因此一次提交不能花费比其评分所用更大的预算，也不能证明比其声称的更弱的上界——不是因为我们检查，而是因为它在这两个对象上从来都不执笔。

验证器无需阅读任何内容即可做出的四种拒绝：

native_decide、maxHeartbeats 和 maxRecDepth 同样会被拒绝：一个只有通过提高限制才能完成的证明，是验证器负担不起的证明。

评分

没有什么是预先固定的。对于一个没人研究过的方案，在什么代价下能达到什么优势本身就是研究问题，因此任何目标都只是猜测——而目标设得过高会把真正的 2⁻³⁰ 区分器评为零分。看板改为衡量结果本身：

score = log₂( budget / advantage^e )

每单位优势所需的查询次数；其以 2 为底的对数就是该攻击所驳斥的安全级别（以比特计）。越低越好。低估你的优势会提高分数，因此声称比你所能证明的更少不会带来任何好处。

e 按挑战设置，没有默认值。决策型游戏取 e = 2——优势 α 大约需要 α⁻² 次重复来放大——而搜索型游戏取 e = 1。这两种约定都出现在文献中，且这种不一致是已知的（Micciancio–Walter, On the Bit Security of Cryptographic Primitives），因此每个挑战都会说明自己采用哪一种。

Par 是设计者自己的声称，取自规范，因此任何地方都不包含对攻击难度的猜测。低于 par 即是对该声称的破解。

前沿（frontier） 是主要记录：当没有任何其他结果同时在查询次数和优势两方面都超过它时，该结果就加入前沿。比特分数是它旁边的排名列，Lean 层中的两个已验证引理（Score.workFactor_lt_of_dominates、Score.onFrontier_of_workFactor_min）保证排名永远不会埋没一个在两个轴上都胜出的结果。

挑战

spoc128 — 提交给 NIST LWC 第 2 轮的 SpoC-128。已被破解：3 次查询，优势为 1，1.58 比特。load key n 将 nonce 放入 rate，tagInput 将 tagControl XOR 进同一个 rate，因此 tagInput (load key n) = load key (n ^^^ tagControl)。一个置换输入可以通过两次查询到达，由于置换是公开且可逆的，它的一半在 tag 中泄露，另一半在密文分组中泄露；拼接、求逆、取出 capacity，那就是密钥。

spoc128-ds — 相同的模式，但 nonce 中保留了四个控制位，因此 n ^^^ tagControl 不是合法的 nonce。开放：目前未知任何攻击。 该限制存在于查询的类型中，因此已发表的攻击在这里不仅仅是失败——它根本不能被表示为敌手（SpoC128DS.attack_second_query_illegal）。

这刻意不是该模式的第二个副本。加固 DDC.lean 意味着要维护一个并行的模型；限制查询域只是一个谓词，所有关于该模式的现有定理仍然适用。

这里没有任何内容声称该变体是安全的。堵住一条已发表的通往某个模式的路径，并不能证明不存在其他路径——这正是把它挂出来的意义所在。

添加挑战

在 Lean 层提供一个 Golf.Game——一个公开的参数类型、查询和响应类型，以及两个世界——然后在这里放一个 config.json。通用层位于 RandomSystems/Golf/Game.lean；RandomSystems/Golf/Instances/SpoC128/ 是完整示例，同时也充当对抽象是否忠实的检查：其充分性凭证为 rfl，其参考提交由现有的 attack_distinguishing_advantage 消解，无需重述。

不评分的内容

• 离线工作，这是有意为之。敌手是一个符号对象，看板对查询复杂度进行评分，这是不可区分性（indifferentiability）和 PRP/PRF 切换引理已经所处的信息论框架。需要计算可行性的挑战必须明确说明，并固定一种承担成本的形式。
• 优势放大 被假定为可用：q/α^e 是将一次攻击重复到达到置信度的成本。
• 并列并不等于等价。 相同的比特水平可以容纳截然不同的结果，这就是为什么前沿与排名并列存在，而不是被排名取代。