这篇文章深入探讨了STARKs中的算术化方法以及其与计算完整性之间的关系,主要聚焦于AIR及其变体PAIR。文章详细分析了在STARKs中的算术中介表示、执行轨迹的定义和构建、以及多元多项式的约束形式。作者提供了丰富的数学背景支持,并通过示例和公式说明了算术化过程的具体实施方案,是一篇技术深度和结构清晰的文章。
原文公式有缺失
本系列是对论文 Study of Arithmetization Methods for STARKs 的高级探索。
随着区块链交易量的增加,扩展性和性能优化成为关键关注点。STARKs 提供了一种有前景的解决方案,但其安全性和计算需求也必须考虑到以实现最佳性能。在本系列中,我们将重点讨论 STARKs 的两种算术化方法,AIR 及其变种 PAIR,以及它们对 Reed-Solomon 接近性测试、RPT 的可靠性影响——即,检查函数是否看起来像低度多项式。我们将比较这些方法在 RPT 的度界限方面的表现。
💡
本系列的第一部分探讨了使用 AIR 进行计算完整性声明的算术化。它创建了执行跟踪有效性与精心构造的多项式的特定属性之间的等价关系。让我们开始吧!
算术化是一种使用有限域上的低度多项式将计算问题简化为代数问题的技术。在 STARKs 中,算术化包括三个阶段阿尔戈:代数中间表示(AIR)、代数布局和路由(APR)以及代数链接 IOP(ALI)。AIR 用于将计算完整性声明转化为多项式的关系和属性。APR 将 AIR 转变为 Reed-Solomon 的 成员资格 问题,ALI 则使用 公共随机性 将这些问题组合成一组较小的 Reed-Solomon 接近性 问题。
在我们进一步探讨之前,我们应该澄清我们如何定义执行跟踪。程序的 执行跟踪 记录了程序/机器运行时的不同状态。这些状态由时钟周期分隔,并给定了编码重要参数的值。状态可以通过状态变量的集合来表示,也可以通过一个结合所有这些的单一值来表示。由于计算操作是离散的,因此使用有限域来赋值状态变量,这样也可以避免数值溢出和下溢。
一般来说,跟踪函数将从一个有限域映射到状态变量的多维空间。我们将使用具有列(宽度)的表来表示对的评估。
执行跟踪由对在某个具有特殊属性的域上的评估构成:
执行跟踪可以用如下表格表示:
每一行表示机器在特定时钟周期的状态,并与的连续幂相关联。在这个上下文中,跟踪的所有列都可以通过使用 拉格朗日插值 插值得到度为的多项式。例如 . 因此,跟踪函数从执行跟踪中独特定义。
就本系列的帖子而言,多项式是涉及在域中进行加法和乘法的有限表达式,并且也输出一个值。
在 STARKs 中,代数中间表示是对计算算术约束的高级描述。计算完整性声明通过以多项式形式表达的约束来强制执行。
除了指定,, 要定义 AIR,我们需要一组约束。记 为索引约束集合的一个子集。当,对于,约束是一个集合
这些组件允许我们将计算完整性约束重写为多项式!
为了简化,我们有多变量多项式 。我们希望变量对应于跟踪表的元素,这些元素应受到约束以转化计算完整性声明。这些元素可以通过表的列和行来指定。这是 掩码 的目标,它是一份如下的列表:
掩码的元素是的类型。这里, 和 用于指定跟踪表上的列和行偏移。主要思想是,我们可以用 的每个 替换 的参数。因此我们将得到 AIR 分配:
📝
示例: 考虑求和约束
这应该解读为 ” 对于行 0 和 1,列 2 中的跟踪元素应等于前两行中列 0 和 1 的跟踪元素的和”。我们将定义约束元素为
使得 在 enforce 时强制实现求和约束,即前两行。
在不深入探讨掩码本身如何工作的细节前,我们将这个构造简化为
这意味着如果这些函数在某些指定点评估为零则计算完整性声明是有效的。因此,计算完整性被简化为检查多项式的根!你可以在 论文 的第3节中看到更多详细信息。
在 APR 中,AIR 实例和证明直接映射到一组 Reed-Solomon 接近性问题(函数是否看起来像低度多项式)。要构建这个新框架,我们将定义 为集合 的 消失多项式,得出
注意到它在关联集的所有点上评估为零: 对于所有 。
如果函数 在 每个元素上都有根(诚实证明者情况),则表达式
定义度多项式,
作为所述的保证,上限为上面所述的的紧凑上界,这一方面由验证者和证明者共同承认。这些新的多项式生成有用的 Reed-Solomon 成员资格问题:是或不是低度的。
因此,APR 产生的约束与相应的原始计算完整性约束是等效的。
➡️
在继续之前,证明者必须对跟踪函数的低度扩展作出承诺。这意味着证明者必须在大域上评估此函数(该域在证明者与验证者之间之前已同意),然后将该数据公开提交到不可变的数据库(Merkle 树应该能够满足要求)。
ALI,算术化的最后一步,通过构建组合多项式来减少所需的 Reed-Solomon 接近性测试数量。ALI 背后的基本思想是使用公共随机性将多项式组合成单个低度多项式。此过程涉及验证者与证明者之间的互动(ALI 中的 I),可以使用 Fiat-Shamir 转换使其非互动。
ALI 的一个主要优点是,它限制了证明者影响接近性测试的能力,因为注入了随机性。通过使证明者在计算上难以实现且在概率上不太可能操纵 APR 多项式,ALI 多项式不太可能满足后续接近性测试的期望结果。换句话说,当输入实例不可满足时,ALI 生成与低度多项式显著不同的 RPT 问题实例(请参阅 DEEP-FRI 论文 的第 1.4 节)。
在证明者已经承诺对跟踪的低度扩展后,他们可以通过组合单个,多项式创建组合多项式,其中在诚实证明者情况下具有,与 。在其一般形式中,验证者提供随机多项式 在代数扩展域 (更大的域促进安全性),使组合多项式变为
其中是度调整多项式,确保所有约束在低度分析中被平等对待,并向组合约束的过程注入随机性,促进安全性。特别地,通过选择 使得来调节的度,因此对应约束的度限可调整为
如果 是低于 的多项式,则相应的 APR 多项式,的度最多,为所需。
这应该通过后续的 RPT 进行测试(同样,FRI 非常适合此任务)。
你现在已经了解了 STARKs 的约束算术化的主要步骤!在下一篇文章中,我们将深入探讨细节,并探索协调约束实施的替代方法:PAIR - 预处理 AIR。
- 原文链接: threesigma.xyz/blog/arit...
- 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~
如果觉得我的文章对您有用,请随意打赏。你的支持将鼓励我继续创作!