AIR密码学家专家

专家级知识用于设计、实现和审计零知识证明系统中的代数中间表示（AIR）。

核心思维

声音第一思维：每次约束审查都从“骗子如何溜走？”开始。以对抗性思维。手工构建反例轨迹。利用多项式身份漏洞。

代数精度：约束定义有限域上的解空间。缺少约束不仅仅是一个错误——它是恶意证明者额外的自由度。

有限域基础

基本直觉：

特征和逆元：每个非零元素都有乘法逆元。没有零因子。
单位根：2^k阶的乘法子群使FFT友好的评估域成为可能。
扩展域：当你需要更多的代数结构时（例如，M31 → QM31用于Stwo）。
Frobenius内射：x → x^p映射是域线性的；对于扩展域算术至关重要。

多项式力学

插值：给定n个点，唯一通过它们的多项式度数< n。拉格朗日基使之明确。

消失多项式：Z_H(x) = ∏(x - h) 对于h ∈ H在域H上消失。这是约束执行的基础。

度数行为：

乘法：deg(f·g) = deg(f) + deg(g)
组合：deg(f∘g) = deg(f) · deg(g)
低度数测试验证函数是“接近”低度数多项式

评估域：乘法余子群用于分离。膨胀因子确定安全边际在轨迹度数和域大小之间。

轨迹设计原则

列分类

类型	定义	示例
真实来源	规范见证数据	PC，寄存器，内存值
派生	从源列计算	标志，分解
辅助	添加以降低度数	中间产品

关键规则：每一列都必须受到约束。未受约束的列是证明者的自由变量。

行语义

精确定义每一行代表什么：

CPU周期/指令
内存操作
填充（必须可区分！）

行类型需要选择器。选择器必须是：

布尔：s(s-1) = 0
互斥：Σ s_i = 1（或覆盖证明）
实际上受到约束（不仅仅是文档化的）

最小与冗余列

从最小开始。只有在以下情况下添加辅助列：

需要降低度数
声音需要显式的中间值
验证成本占主导

约束类别

转换约束（局部）

表达行i和行i+1之间的正确步骤关系：

next_pc = pc + instruction_size  (当不分支时)
next_register[k] = f(current_state, opcode)

危险：写关系而不是函数。多个有效的下一个状态=不安全。

边界约束

将特定行固定在特定值：

初始：第0行状态与预期开始匹配
最终：最后一行满足终止条件
I/O：公共输入/输出绑定在已知位置

危险：“最后一行”必须唯一定义。可变长度轨迹需要显式的停止处理。

布尔性和范围约束

对于布尔b：b(b-1) = 0

对于k位值x，位b0…b{k-1}：

x = Σ b_i · 2^i
b_i(b_i - 1) = 0  for all i

危险：忘记分解位的布尔性约束。

选择器纪律

选择器控制哪些约束适用于哪些行。

清单：

[ ] 每个选择器都是布尔的
[ ] 每行恰好有一个选择器活跃（或显式覆盖）
[ ] 没有“幽灵模式”其中所有选择器=0
[ ] 选择器本身受到约束（不是自由的）

经典错误：所有选择器为零使得所有门控约束真值。

全局一致性论证

排列/多集等式

通过大乘积证明两个多集相等：

∏(α - a_i) = ∏(α - b_i)

清单：

初始乘积=1（边界约束）
最终乘积相等（边界约束）
挑战α绑定到承诺后
正确处理重复项

危险：乘积击中零，错过边界约束，挑战重用。

查找论证

证明列A中的所有值都出现在表T中。

清单：

表已承诺/固定
压缩是抗碰撞的（足够的随机性）
重复查找声音计数

危险：弱压缩允许表外值。

内存一致性

内存操作形成日志：（地址，时间戳，值，is_write）

模式：

按地址排序，然后按时间戳排序
同一地址的连续操作：读取看到最后的写入
排列链接内存日志到CPU轨迹

危险：

跨不同轨迹部分的地址别名
时间戳未证明单调
未强制执行读之前写

商和组合

约束多项式C(x)应在轨迹域H上消失。

商：Q(x) = C(x) / Z_H(x)

如果C在H上不消失，Q有极点 → 不是低度数 → FRI拒绝。

行集控制

约束适用于不同的行集：

所有行：除以Z_H(x)
除了最后一行：除以Z_H(x) / (x - ω^ {n-1})
仅第一行：乘以Lagrange选择器用于行0
仅最后一行：乘以Lagrange选择器用于行n-1

危险：旨在“所有行”的约束由于错误的消失因子而意外仅在子集上执行。

度数核算

跟踪每个约束的度数：

基础约束度数：d
选择器乘法后：d + deg(selector)
边界多项式后：d + deg(boundary)

组合多项式的度数必须保持在域大小以下，并有足够的余地（膨胀因子）。

Fiat-Shamir卫生

成绩单必须绑定：

所有承诺（轨迹，查找表等）
公共输入
轨迹长度/域参数
任何证明者消息

挑战分离：不同的论证需要独立的挑战。重用挑战创建代数漏洞。

危险：挑战在承诺之前派生 → 证明者可以适应见证。

对抗性见证练习

在声明AIR声音之前，尝试破坏它：

所有选择器=0：约束仍然强制执行吗？
腐败一列：它可以在未检测到的情况下漂移吗？
攻击最后一行：将不一致性倾倒入包装？
重复/省略内存事件：全局检查是否捕获它？
强制乘积为零：利用大乘积边界？
利用门控：通过留下标志未受约束使“如果标志那么X”空值？

如果你找到一个反例轨迹，你发现了一个错误。

常见漏洞模式

模式	症状	修复
未受约束的列	证明者任意设置	添加约束
缺少布尔性	非二进制“布尔”	添加b(b-1)=0
选择器泄漏	约束绕过	强制排他性
最后一行逃逸	不一致性隐藏	适当的终端约束
乘积零	排列论证失败	边界检查，域分离
挑战重用	代数取消	每个论证单独挑战
弱压缩	查找碰撞	增加随机性

性能意识设计

在不成为工程师的情况下了解权衡：

选择	证明者成本	验证者成本	声音
更多列	更高内存	未改变	中性
更高学位	更多FRI轮次	更多查询	观察膨胀
更多行	线性扩展	日志扩展	中性
辅助列	内存+约束	未改变	可以改善

经验法则：

降低度数的辅助列通常值得
本地约束比全局论证更便宜
预计算表与动态检查：取决于表大小

审查交付物

审查AIR时，产出：

列清单：名称，含义，范围，在哪里受约束
约束图：每个语义声明→哪个约束执行它
度数表：每个约束的度数贡献
对抗性测试：尝试的反例
风险排名：关键/高/中等发现
建议修复：具体的约束添加/修改

见references/review-checklist.md了解完整的系统审查表。