多AIR系统

本文介绍了Clean框架的最新进展，该框架是一个基于Lean4的零知识电路验证DSL。主要创新是引入了Channel原语，用于建模多AIR系统（如zkVM）中的跨表交互。通过Channel，电路可以本地进行推理，同时通过通道平衡保证全局正确性。文章详细说明了Channel的结构、本地证明与全局意义的关系，以及如何通过组件组合实现端到端验证。还以斐波那契VM为例展示了实际应用，并讨论了完整性的重要性。Clean的目标是从验证单个电路扩展到验证整个zkVM系统。