Winter AIR

此crate包含用于以STARK特定格式描述任意计算所需的组件。

算术化

在我们能够生成证明来证明某些计算已正确执行之前，我们需要将这些计算简化为涉及一组有界次数多项式的代数陈述。这一步骤通常称为算术化。有关AIR算术化的基础知识，请参阅StarkWare的优秀帖子

• 算术化 I
• 算术化 II
• StarkDEX深度解析：STARK核心引擎

为计算提出有效的算术化是非平凡的，描述算术化可能是繁琐且易出错的。《code>Air trait旨在帮助后者，希望这也会使前者变得更简单。

为了为给定的计算定义AIR，您需要实现Air trait，它包括以下内容

1. 通过BaseField关联类型定义您的计算的基本字段（有关可用的字段选项，请参阅math crate）。
2. 通过PublicInputs关联类型定义所需用于您的计算的一组公共输入。
3. 实现Air::new()函数。在此函数的一部分中，您应该创建一个AirContext结构，它将所有过渡约束的次数作为构造参数之一。
4. 实现context()方法，该方法应返回对在Air::new()函数中创建的AirContext结构的引用。
5. 实现evaluate_transition()方法，该方法应在给定的评估框架上评估过渡约束。
6. 实现返回给定计算实例断言向量的 get_assertions() 方法。
7. 如果您的计算需要 周期值，您还可以重写默认的 get_periodic_column_values() 方法。

有关更多信息，请参阅 Air trait 的定义，并查看 examples crate，它说明了如何为多个不同的计算实现该特质。

转换约束

转换约束定义了计算的两个连续步骤之间的代数关系。在 Winterfell 中，转换约束在 evaluate_transition() 函数内部进行评估，该函数接受以下参数

• frame：&EvaluationFrame<FieldElement>，其中包含计算的当前和下一个状态的向量。
• periodic_values：&[FieldElement]，当为计算定义了周期列时，这将包含计算当前步骤的周期列的值。否则，这将是一个空切片。
• result：&mut [FieldElement]，这是约束评估结果应该写入的切片。

如果且仅当函数返回后，result 切片包含所有零时，约束才被认为是满足的。通常，过渡约束评估函数需要按照以下方式工作

• 对于所有有效的连续计算步骤之间的转换，转换约束应该评估为零。
• 对于任何无效的转换，至少必须有一个约束评估为非零值。

请注意，由于转换约束定义了代数关系，因此应仅使用代数运算（加法、减法和乘法）来描述它们（除法可以使用乘法的逆来模拟）。

约束度

影响证明生成时间和证明大小的关键因素之一是转换约束的最大度。这个度越高，我们需要的膨胀因子就越大。通常，我们希望保持这个度尽可能低——例如，在 4 或 8 以下。为了准确地描述您的转换约束的度，请记住以下内容

• 所有跟踪列的度都是 1。
• 当将跟踪列相乘时，度会增加 1。例如，如果我们的约束涉及两个列的乘法，则该约束的度将是 2。我们可以使用 TransitionConstraintDegree 结构来描述此约束：TransitionConstraintDegree::new(2)。
• 周期列的度取决于它们的周期长度，但在大多数情况下，这些度非常接近 1。
• 为了描述涉及迹列和周期列乘积的约束程度，使用with_cycles()构造函数的TransitionConstraintDegree结构体。例如，如果我们的约束涉及一个迹列和一个周期为32步的周期列的乘积，则程度可以描述为：TransitionConstraintDegree::with_cycles(1, vec![32])。

一般来说，应谨慎使用乘法 - 尽管有一些方法可以稍微放宽这一限制（查看mulfib8示例）。

迹断言

断言用于指定计算的合法执行迹必须包含某些单元格中的某些值。它们通常用于将公共输入与特定的执行迹相关联，但也可以用于以其他方式约束计算。在Winterfell内部，断言被转换为边界约束。

为了为您的计算定义断言，您需要实现get_assertions()函数的Air特质。每个计算都必须至少有一个断言。断言可以是以下类型：

• 单个断言 - 此断言指定执行迹中的一个单元格必须等于特定值。例如：第0列的第0步的值必须等于1。
• 周期性断言 - 此断言指定给定列在指定间隔内的值应等于某些值。例如：第0列的第0步、第8步、第16步、第24步等值必须等于2。
• 序列断言 - 此断言指定给定列在特定间隔内的值必须等于提供的值序列。例如：第0列的第0步的值必须等于1，第8步的值必须等于2，第16步的值必须等于3等。

有关如何定义断言的更多信息，请参阅断言模块，并查看示例crate中的示例。

周期值

有时，可能需要定义一个在执行迹中包含重复值的列。例如，假设我们有一个在第4步包含值1，在其他情况下为0的列。这样的列可以用简单的周期序列[1, 0, 0, 0]来描述。

为了为您计算定义此类列，您可以覆盖get_periodic_column_values()方法，该方法是Air特质的。计算给定步骤的周期列的值将通过periodic_values参数提供给evaluate_transition()方法。

随机化AIR

随机化的 AIR 是 AIR 的一种强大扩展，它使多项式和排列检查成为可能，类似于 PLONKish 系统中可用的检查。这些检查反过来允许高效地描述“非局部”约束，这些约束可以用来构建高效的范围检查、随机访问内存等组件。

使用随机化 AIR，执行轨迹的构建分为多个阶段。在第一阶段，按照与常规 AIR 构建轨迹类似的方式构建 主轨迹段。在随后的阶段，构建 辅助轨迹段。在构建辅助轨迹段时，证明者可以访问验证者发送的额外随机性（在协议的非交互版本中，这种随机性来自之前的轨迹段承诺）。

要描述随机化 AIR，在实现 Air 特性时需要执行以下操作

• 从 Air::context() 方法返回的 AirContext 结构必须使用 AirContext::new_multi_segment() 构造函数进行实例化。以这种方式构建 AIR 上下文时，需要提供一个 TraceLayout，该布局描述了多段执行轨迹的形状。
• 重写 Air::evaluate_aux_transition() 方法。该方法类似于 Air::evaluate_transition() 方法，但它还接受两个额外的参数：aux_evaluation_frame 和 aux_rand_elements。这些参数用于评估辅助轨迹段上的转换约束。
• 重写 Air::get_aux_assertions() 方法。该方法类似于 Air::get_assertions() 方法，但它应该返回针对辅助轨迹段列的断言。

协议参数

ProofOptions 结构定义了一组选项，这些选项在 STARK 证明生成和验证期间使用。这些选项对生成证明的安全性以及证明生成时间有直接影响。具体来说，STARK 证明的安全性取决于

1. 哈希函数 - 证明安全性受协议中使用的哈希函数的碰撞抵抗性限制。例如，如果使用具有 128 位碰撞抵抗性的哈希函数，则 STARK 证明的安全性不能超过 128 位。
2. 有限域 - 证明安全性受协议中使用的有限域限制。这意味着，对于小型域（例如小于 ~128 位），必须使用域扩展来实现适当的安全性。即使是 ~128 位域，为了实现超过 100 位的安全性，可能还需要使用域扩展。
3. 查询次数 - 较高的值会增加证明安全性，但也会增加证明大小。
4. 膨胀因子 - 较高的值会增加证明安全性，但也会增加证明生成时间和证明大小。然而，较高的膨胀因子需要较少的查询才能达到相同的安全级别。因此，通常可以增加膨胀因子，同时减少查询次数，从而使证明变得更小。
5. 磨光因子 - 较高的值会增加证明安全性，但可能会增加证明生成时间。

请参阅options.rs获取有关当前可用选项及其含义的更多信息。此外，可以使用Proof::security_level()函数来估计证明的安全性级别。

包功能

此包可以编译以下功能

• std - 默认启用并依赖于Rust标准库。
• no_std - 不依赖于Rust标准库，并允许编译到WebAssembly。

要使用no_std编译，通过--no-default-features标志禁用默认功能。

许可证

此项目受MIT许可证保护。