使用 zkMips，客户可以将使用 MIPS 指令集编写的程序外包，让它执行，除了获得结果外，还可以获得易于验证的证据，证明该结果是正确的。创建此证明的软件组件称为 zkVM。
zkVM 的输入是 执行追踪 程序执行情况。由于 zkMips 计算是分步进行的，因此其总体状态可以通过有限变量列表的值来定义。有效计算是一系列状态，从明确定义的初始状态到某种最终状态，其中每个状态转换都代表一个有效的计算步骤。该序列可以表示为一个表，其列代表变量列表，其行代表计算的每个步骤。下图显示了一个玩具示例。
为了证明一个程序的结果是正确的，必须证明从每个状态（行）到下一个状态的所有转换都是有效的，即它与该程序步骤的特定指令的操作码一致。因此，对于每条不同的指令，这种一致性证明都是不同的，这给zkVM软件开发人员带来了艰巨的任务。
但是，有个好消息。上周，贾斯汀·泰勒和斯里纳斯·塞蒂以及阿拉苏·阿伦和里亚德·瓦比一起发表了一篇文章 执行这些一致性检查的新的、更有效的方法。他们发表了两篇论文，介绍了两个互补的系统： Jolt 和 套索。要了解他们的方法，最简单的方法是从 Jolt 开始。
首先，我们知道一个 布尔函数 可以用真值表表示：
我们可以使用字节来获取一个表，而不是比特
请注意，我们为和有 2可能的输入，因此表的总大小为 2¹ = 65536 行。
如果我们使用 32 位字而不是字节，则表的总大小将为 (23/²) ² = 2行；如果是 64 位字，该表将有 2¹ ²行。
这个数字 2¹ ²是巨大的。实际上， AES 加密算法 使用 128 位密钥，因为详尽地搜索所有可能性被认为是不可行的。同样，在现实中实现行数为 2¹ ²的表格是完全不可能的。第二篇论文解决了这个问题，其中介绍了 Lasso。但是现在不用担心；只要假设这样的千兆数据存在即可。
在这个假设下，我们可以通过使用千兆表来实现 “和” 之间的（按位）与，每个 64 位；我们将得到：= [,]。
请注意，zk 证明略有不同。我们不是在计算 = 和 (,) 因为 Prover 已经将、和作为输入（之前可能使用 AND 指令计算）。相反，Prover 需要证明这些值是正确的。换句话说，他必须证明这一点 和（,)，其中我们使用特殊的等号作为重点。
Jolt+Lasso 背后的基本思想是使用表格查找来验证执行跟踪。它们也是使用多项式实现的，但比使用的多项式更简单 Plonk 或 HALO2，这会使 Prover 加速 10 倍或更多。不幸的是，这是以验证器延迟两倍为代价的。
现在我们在这个例子中使用的操作码是 AND。但是很明显，我们可以在表中表示任何其他操作码：按位或、按位 XOR、ADD、SUB 等。当然，每个操作码都有不同的对应表。
Jolt 论文不仅仅讨论操作码。它提出了一个抽象但等效的 CPU 模型，并证明其指令集架构 (ISA) 的每条指令都可以使用表查找来实现，前提是存在千兆表。
Jolt 的细节有时有点乏味，但并不是非常抽象或数学的。它具有 CPU 设计风格，但使用的是 Lasso 模型提供的特定构件，而不是电气工程师的工具。
为了了解 Jolt 讨论的主题，以下是一些示例：
Jolt论文讨论了CPU的ISA中包含的所有指令，详细描述了如何将每条指令简化为表查询，其中一些指令很简单，另一些则使用千兆表。
这种方法真正困难的部分是实现这些千兆字节。这些表中的大多数值永远不会被访问，它们只存在于概念上。
配套的拉索论文描述了这为何可能。这将是我们下一篇文章的主题，即将发布！
本文的作者杰罗恩·范德格拉夫是ZKM的高级研究顾问。
你读过 ZKM 白皮书了吗？在以下地址查看 https://ethresear.ch/t/zkmips-a-zero-knowledge-zk-vm-based-on-mips-architecture/16156
想和我们的核心 ZKM 团队讨论这个话题和其他与 ZK 相关的话题吗？加入我们的 Discord 频道： Discord.gg/bck7HDGCNS
这篇文章最初发表于 http://github.com。
使用 zkMips，客户可以将使用 MIPS 指令集编写的程序外包，让它执行，除了获得结果外，还可以获得易于验证的证据，证明该结果是正确的。创建此证明的软件组件称为 zkVM。
zkVM 的输入是 执行追踪 程序执行情况。由于 zkMips 计算是分步进行的，因此其总体状态可以通过有限变量列表的值来定义。有效计算是一系列状态，从明确定义的初始状态到某种最终状态，其中每个状态转换都代表一个有效的计算步骤。该序列可以表示为一个表，其列代表变量列表，其行代表计算的每个步骤。下图显示了一个玩具示例。
为了证明一个程序的结果是正确的，必须证明从每个状态（行）到下一个状态的所有转换都是有效的，即它与该程序步骤的特定指令的操作码一致。因此，对于每条不同的指令，这种一致性证明都是不同的，这给zkVM软件开发人员带来了艰巨的任务。
但是，有个好消息。上周，贾斯汀·泰勒和斯里纳斯·塞蒂以及阿拉苏·阿伦和里亚德·瓦比一起发表了一篇文章 执行这些一致性检查的新的、更有效的方法。他们发表了两篇论文，介绍了两个互补的系统： Jolt 和 套索。要了解他们的方法，最简单的方法是从 Jolt 开始。
首先，我们知道一个 布尔函数 可以用真值表表示：
我们可以使用字节来获取一个表，而不是比特
请注意，我们为和有 2可能的输入，因此表的总大小为 2¹ = 65536 行。
如果我们使用 32 位字而不是字节，则表的总大小将为 (23/²) ² = 2行；如果是 64 位字，该表将有 2¹ ²行。
这个数字 2¹ ²是巨大的。实际上， AES 加密算法 使用 128 位密钥，因为详尽地搜索所有可能性被认为是不可行的。同样，在现实中实现行数为 2¹ ²的表格是完全不可能的。第二篇论文解决了这个问题，其中介绍了 Lasso。但是现在不用担心；只要假设这样的千兆数据存在即可。
在这个假设下，我们可以通过使用千兆表来实现 “和” 之间的（按位）与，每个 64 位；我们将得到：= [,]。
请注意，zk 证明略有不同。我们不是在计算 = 和 (,) 因为 Prover 已经将、和作为输入（之前可能使用 AND 指令计算）。相反，Prover 需要证明这些值是正确的。换句话说，他必须证明这一点 和（,)，其中我们使用特殊的等号作为重点。
Jolt+Lasso 背后的基本思想是使用表格查找来验证执行跟踪。它们也是使用多项式实现的，但比使用的多项式更简单 Plonk 或 HALO2，这会使 Prover 加速 10 倍或更多。不幸的是，这是以验证器延迟两倍为代价的。
现在我们在这个例子中使用的操作码是 AND。但是很明显，我们可以在表中表示任何其他操作码：按位或、按位 XOR、ADD、SUB 等。当然，每个操作码都有不同的对应表。
Jolt 论文不仅仅讨论操作码。它提出了一个抽象但等效的 CPU 模型，并证明其指令集架构 (ISA) 的每条指令都可以使用表查找来实现，前提是存在千兆表。
Jolt 的细节有时有点乏味，但并不是非常抽象或数学的。它具有 CPU 设计风格，但使用的是 Lasso 模型提供的特定构件，而不是电气工程师的工具。
为了了解 Jolt 讨论的主题，以下是一些示例：
Jolt论文讨论了CPU的ISA中包含的所有指令，详细描述了如何将每条指令简化为表查询，其中一些指令很简单，另一些则使用千兆表。
这种方法真正困难的部分是实现这些千兆字节。这些表中的大多数值永远不会被访问，它们只存在于概念上。
配套的拉索论文描述了这为何可能。这将是我们下一篇文章的主题，即将发布！
本文的作者杰罗恩·范德格拉夫是ZKM的高级研究顾问。
你读过 ZKM 白皮书了吗？在以下地址查看 https://ethresear.ch/t/zkmips-a-zero-knowledge-zk-vm-based-on-mips-architecture/16156
想和我们的核心 ZKM 团队讨论这个话题和其他与 ZK 相关的话题吗？加入我们的 Discord 频道： Discord.gg/bck7HDGCNS
这篇文章最初发表于 http://github.com。
