视频字幕
Cairo 是一种专门设计的编程语言，用于编写可证明计算完整性的程序。它的核心原理是将普通的计算转化为适合 STARK 证明系统验证的代数形式。Cairo 程序首先被编译成 AIR，也就是代数中间表示，然后通过 STARK 证明系统生成可验证的证明。
AIR，也就是代数中间表示，是 Cairo 的核心组件。它将程序的逻辑转换为一组多项式约束，每个约束都定义在有限域上。这些约束包括状态转换约束、内存访问约束、算术运算约束和边界条件约束。通过这种方式，程序的正确执行可以被表示为满足所有多项式约束的问题。
当 Cairo 程序执行时，会生成一个执行轨迹，记录程序运行的每一步状态，包含寄存器值、内存状态等信息。STARK 证明系统接收这个执行轨迹，验证它是否满足 AIR 定义的多项式约束。STARK 具有可扩展性、透明性、后量子安全等特点，能够生成简洁的证明供快速验证。
Cairo 的所有计算都在有限域上进行，这确保了运算的确定性和安全性。有限域 F_p 包含从 0 到 p-1 的所有整数，其中 p 是一个大质数。多项式理论是 STARK 证明的数学基础，通过多项式承诺方案和 FRI 协议，可以高效地证明和验证多项式的性质。
总结一下 Cairo 的底层原理：首先，Cairo 将程序编译为 AIR 代数中间表示，通过多项式约束描述计算逻辑。然后生成执行轨迹记录程序状态，STARK 证明系统验证轨迹的正确性。整个过程基于有限域和多项式理论，实现了高效的可验证计算。这种设计使得 Cairo 成为区块链和零知识证明领域的重要工具。