本教程将展示如何在 Circom 中创建一个栈。

请注意——本章内容较长。

然而，当我们要在下一章创建一个简单的 ZK 虚拟机（ZKVM）时，关于如何创建栈的 ZK 证明的策略将是至关重要的。理解 ZKVM 工作原理的大部分基础工作都已经前置到了本章。

栈能够将一个数字压入（push）栈顶，将栈顶元素弹出（pop），或者不进行任何更改。

栈在本质上是可变的，但在 Circom 中，我们只被允许使用不可变数组。因此，必须使用不可变数组对栈进行建模。每次栈发生变化（通过 pop 或 push）时，我们都会创建一个新的数组来表示新的栈状态。

这可能看起来效率低下，但由于 ZK 中的信号是不可变的，因此别无他法（更高级的 ZK 技术有优化此问题的方法，但该讨论超出了本文的范围）。

第一个要求是栈具有固定的“最大高度”——即不可变数组的长度。为了跟踪栈有多少被“使用”了，我们采用了一个称为“栈指针”（stack pointer）的独立变量，它是一个从零开始的索引，告诉我们将下一个元素压入何处。sp 指向数组中未使用的位置，也就是新值应该被压入的地方，它比栈顶的索引高出一位。下图展示了一个包含三个元素（10、16 和 20）的栈：

栈指针 sp 指向索引 3，该位置为空，用 $\circ$ 表示。栈会忽略索引 3（当前的 sp）或更大的任何值。它们可能具有非零值，但电路不会考虑它们。

假设我们将元素 21 压入栈中。这意味着我们增加栈指针并复制之前的所有值。更新后的栈现在具有 sp = 4。

如果我们从栈中弹出元素，sp 递减，并且我们不会将值 21 复制到下一个栈中：

如果栈没有发生变化，我们仍然会经历某种计算步骤，在此步骤中，我们只需将之前的所有值复制到下一个栈中。

由于 sp 每次迭代都会发生变化，我们需要每次都将新值存储在一个新的信号中，因为信号的值一旦分配就无法更新。因此，我们使用一个数组来跟踪每次迭代时 sp 的值：

正如有栈的最大高度一样，我们能更新栈的次数也有一个最大值，因为用于模拟栈的表（在底层是一个 2D Circom 数组）必须是固定大小的。

最大大小取决于我们的应用程序。在区块链环境中，执行 100 万条指令的可能性非常小，但在为计算更密集的应用程序创建电路时，我们可能需要分配更大的电路来容纳潜在的栈大小。

栈的约束

无论我们是进行 push、pop 还是什么都不做，从 0 到 sp - 2（含边界）的元素都需要被复制（并被约束为相等）到下一个栈。在下面的示例中，栈指针在 4 的位置，然后我们执行了 pop 操作，栈指针变为 3。位于栈指针索引 0、1、2（橙色部分）的元素被复制了。

如果指令是 pop，那么我们还要求新的栈指针比上一个栈指针少 1。

push 的约束

在进行 push 时，所有直到 sp - 1 的值都必须复制到新栈中（请注意，栈指针指向一个空白区域，因此无需复制它）。位于 sp - 1 的值必须被约束为所压入的值。

在上面的示例中，栈指针为 3，我们复制了 0、1、2 中的元素。我们还约束栈指针递增 1。我们必须同时约束栈指针比之前的值大 1。

pop 的约束

在进行 pop 时，所有直到 sp - 2 的值都必须复制到新栈中。我们约束栈指针递减 1。

nop（无操作）的约束

所有直到 sp - 1 的值都必须被约束为保持不变。sp 必须被约束为等于上一次迭代的值。

根据一组指令更新栈

在指令的每次迭代中，我们需要知道是要压入一个数字、弹出栈顶，还是什么都不做，我们将用“操作码”或“指令” PUSH、POP 或 NOP 来表示。

例如，假设我们得到了指令 PUSH 10 POP PUSH 16 PUSH 15 PUSH 4 NOP POP。我们可以将这组指令表示为一个数组：

[PUSH, 10, POP, 0, PUSH, 16, PUSH, 15, PUSH, 4, NOP, 0, POP, 0]

不失一般性，我们可以将 PUSH 表示为数字 1，POP 表示为 2，NOP 表示为 0，因此上述指令可以按如下方式编码。

请注意，每条指令后面始终跟随着一个常量。对于 PUSH，这是要压入的值；但对于 POP 和 NOP，其后的常量会被忽略。将指令放在索引 0、2、4…… 等位置，使我们能够以 2 为步长遍历这些指令。换句话说，如果指令可能带有参数或不带参数，那么我们需要根据是否有参数来改变步长。这种条件式的步长会增加我们示例的复杂性，因此我们将操作码置于偶数间隔处，以便始终能保持固定步长为 2。

现在，让我们生成一个 “metaTable”（元数据表），它告诉我们在执行的每一行中将发生哪种操作。如果我们添加 is_push、is_pop 或 is_nop 这些列来指示哪条指令处于激活状态，那么我们会得到以下表格。

最终结果将如下所示，但我们将在下一节中一步步重建此表：

对 sp 的解释是：如果当前指令是 push，则下一个值应写入的位置。如果指令是 pop，那么 sp - 1 就是不应该被复制的元素。

填充表格

要填充从 is_push 到 arg 的表格列，我们可以简单地在循环中复制指令：如果当前指令是 PUSH，则将 is_push 设置为 1，其他指令以此类推。我们将得到如下结果：

栈指针必须始终从零开始，因此我们可以简单地对其进行硬编码：

我们可以通过以下方式填充剩余的栈指针列：如果指令是 PUSH，则递增；对于 POP，则递减；对于 NOP，则保持不变。请注意，我们是基于当前行更新下一个 sp。因此，在第 0 次迭代时，我们如下更新第 1 行：

也就是说，由于当前的 is_push 为 1，且当前的 sp 为 0，我们将 0 + 1 写入下一个单元格。然后我们如下填充 sp 列的剩余部分：

然后，我们简单地使用 sp 和 arg 列，在条件为 is_push 等于 1 时，将 push 的值写入相应的单元格中。请注意，在此步骤中，只有 is_push == 1 的行才会被填充：

注意，以前的值尚未被复制过来——我们将在稍后的部分解决这个问题。

处理第 0 行

第 0 行是特殊的，因为它不会从上一行复制任何值。为了避免必须根据当前是否处于第 0 行来进行逻辑分支，我们让表格的大小比实际需要的增加一行，然后从第 1 行开始构建我们的约束。这样一来，每一行总是复制它上面的一行。

在接下来的代码演示中，我们在第 0 行硬编码约束条件，因为之后若将第 0 行作为是否复制前一行值的边界情况来处理，将会非常不便。

复制前一行

现在，我们需要确保值从一行到下一行被正确复制。一个单元格会复制它上方的值，直到下一行的栈指针减 1 的位置。请记住，sp 指向栈上方的空白空间，因此 sp - 1 指向栈顶。

列和栈的术语

由于我们将栈“侧放”存储在表格中，我们会将栈底称为列（column）0，位于该列顶部的元素（如果存在）称为列 1，以此类推。当我们说“列”时，指的是以底层为零开始的栈的“索引”。

复制的约束

1. 如果 is_push = 1，那么栈中 0..sp - 1（含边界）的所有元素都必须被复制。位于 sp 的单元格将包含新增加的值。这将复制整个栈。
2. 如果 is_nop = 1，那么栈中 0..sp - 1（含边界）的所有元素都必须被复制。不会向 sp 所在的单元格写入任何内容。这将复制整个栈。
3. 如果 is_pop = 1，那么栈中 0..sp - 2（含边界）的所有元素都必须被复制。请记住，sp 指向栈上方的一个空单元格，所以 sp - 1 是将被弹出的值。sp - 2 及以下的所有元素都必须被复制。这将复制除栈顶以外的所有元素。

如果栈指针分别为 0 或 1，条件 2 和 3 将面临边界情况，因为会发生下溢（underflow）。因此，我们需要特殊列来指示 sp 是否小于 2 或 1，并且我们需要以不同方式处理复制。具体而言：

• 如果 sp = 0，则不复制任何内容
• 如果 sp = 1，仅当指令是 NOP 或 PUSH 时，我们才会复制列 0 的单元格

我们创建额外的列（copy0、copy1、copy2、copy3）作为标志，以指示（column0、column1、column2、column3）对应的值是否将被复制到下一行。

处理初始条件

在为第 0 行创建约束时，我们还有另一个边界情况——如果我们尝试复制上一行的值，将会造成数组下溢。因此，我们需要对这一行进行不同处理——我们以一种更“硬编码”的方式填充第一行的值，然后从第 1 行开始迭代式地创建约束。

确定 copy 应该是零还是一

回顾前面的约束条件：

1. 如果 is_push = 1，那么所有 0..sp - 1（含边界）的值都必须被复制。位于 sp 的单元格将包含新值。
2. 如果 is_nop = 1，那么所有 0..sp - 1（含边界）的值都必须被复制。不会向 sp 所在的单元格写入任何内容。
3. 如果 is_pop = 1，那么所有 0..sp - 2（含边界）的值都必须被复制。请记住，sp 指向栈上方的一个空单元格，所以 sp - 1 是将被弹出的值。sp - 2 及以下的所有元素都必须被复制。

我们可以将这些总结为条件 A 和 B：

A. 如果 sp 为 1 或更大，且我们当前的列在 sp 的索引下方 1 位以内，并且当前指令是 PUSH 或 NOP，我们应该复制
B. 如果 sp 为 2 或更大，且我们当前的列在 sp 的索引下方 2 位以内，并且当前指令是 POP，我们应该复制

如果当前所在的列不符合上述任何条件，则不进行复制。这包括：

• 当前列在栈指针处或之上
• 当前列在栈指针下方 1 位，并且当前指令是 pop
• 栈指针 = 0

使用上面的规则，让我们来填充表格。在第 0 行，sp = 0，所以所有的 copy 列都将是 0：

在索引为 1 的行，sp 等于或大于 1，指令是 POP，但对于任何一列均不满足条件 A 或 B，因此我们不复制：

在第 2 行，sp 为 0，所以什么都不会被复制：

在第 3 行，sp 为 1 且指令是 PUSH，所以 column0 满足条件 A：

“如果 sp 为 1 或更大，且我们当前的列在 sp 的索引下方 1 位以内，并且当前指令是 PUSH 或 NOP，我们应该复制”

并将 copy0 设置为 1：

在第 4 行，sp 为 2 且指令是 PUSH，所以列 0 和列 1 满足条件 A：

在第 5 行，sp 为 3 且指令是 NOP，所以列 0、1 和 2 满足条件 A，即“如果 sp 为 1 或更大，且我们当前的列在 sp 的索引下方 1 位以内，并且当前指令是 PUSH 或 NOP，我们应该复制”：

在第 6 行，sp 为 1 且指令是 POP，所以我们使用条件 B：

“如果 sp 为 2 或更大，且我们当前的列在 sp 的索引下方 2 位以内，并且当前指令是 POP，我们应该复制”

这意味着列 0 和 1 将被复制：

复制条件的 Circom 实现

我们可以在 Circom 中创建一个专用组件（component），来确定是否应该从上方复制值。

• A. 如果 sp 为 1 或更大，且我们当前的列在 sp 的索引下方 1 位以内，并且当前指令是 PUSH 或 NOP，我们应该复制
• B. 如果 sp 为 2 或更大，且我们当前的列在 sp 的索引下方 2 位以内，并且当前指令是 POP，我们应该复制

该组件将用于循环中，以确定特定列 j 是否应该被复制。如果特定列应该被复制，它将把 out 设置为 1。此组件应用于每一行的每一列。

Copy
include "circomlib/comparators.circom";
include "circomlib/gates.circom";

// RETURNS 1 IF ALL THE INPUTS ARE 1
template AND3() {
  signal input in[3];
  signal output out;
  
  signal temp;
  temp <== in[0] * in[1];
  out <== temp * in[2];
}

// j is the column number
// bits is how many bits we need
// for the LessEqThan component
template ShouldCopy(j, bits) {
  signal input sp;
  signal input is_pop;
  signal input is_push;
  signal input is_nop;
  
  // out = 1 if should copy
  signal output out;
  
  // sanity checks
  is_pop + is_push + is_nop === 1;
  is_nop * (1 - is_nop) === 0;
  is_push * (1 - is_push) === 0;
  is_pop * (1 - is_pop) === 0;
  
  // it's cheaper to compute ≠ 0 than > 0 to avoid
  // converting the number to binary
  signal spEqZero;
  signal spGteOne;
  spEqZero <== IsZero()(sp);
  spGteOne <== 1 - spEqZero;
  
  // it's cheaper to compute ≠ 0 and ≠ 1 than ≥ 2
  signal spEqOne;
  signal spGteTwo;
  spEqOne <== IsEqual()([sp, 1]);
  spGteTwo <== (1 - spEqOne) * (1 - spEqZero);
  
  // the current column is 1 or more 
  // below the stack pointer
  signal oneBelowSp <== LessEqThan(bits)([j, sp - 1]);
  
  // the current column is 2 or more
  // below the stack pointer
  signal twoBelowSP <== LessEqThan(bits)([j, sp - 2]);
  
  // condition A
  component a3A = AND3();
  a3A.in[0] <== spGteOne;
  a3A.in[1] <== oneBelowSp;
  a3A.in[2] <== is_push + is_nop;
  
  // condition B
  component a3B = AND3();
  a3B.in[0] <== spGteTwo;
  a3B.in[1] <== twoBelowSP;
  a3B.in[2] <== is_pop;
  
  component or = OR();
  or.a <== a3A.out;
  or.b <== a3B.out;  
  out <== or.out;
}

我们可以在循环中使用上述组件来确定上一个栈的哪些部分应该被复制到新栈中。以下模板返回一个包含 0 或 1 的数组，以确定应该复制哪些列。例如，如果有 4 列并且应该复制前 2 列，那么它将返回 [1, 1, 0, 0]：

Copy
template CopyStack(m) {
  var nBits = 4;
    signal output out[m];
    signal input sp;
    signal input is_pop;
    signal input is_push;
    signal input is_nop;

    component ShouldCopys[m];
    
    // loop over the columns
    for (var j = 0; j < m; j++) {
        ShouldCopys[j] = ShouldCopy(j, nBits);
        ShouldCopys[j].sp <== sp;
        ShouldCopys[j].is_pop <== is_pop;
        ShouldCopys[j].is_push <== is_push;
        ShouldCopys[j].is_nop <== is_nop;
        out[j] <== ShouldCopys[j].out;
    }
}

最终版的栈

以下代码是栈的最终实现版本，它将所有组件组合在一起。既然我们已经展示了 ShouldCopy 和 CopyStack 的组件，读者可以直接跳转到最后的组件 StackBuilder。之前的组件均来自前面的章节。我们将它放在一个文件中，以便读者可以方便地将其复制并粘贴到 zkrepl 中进行测试：

Copy
include "circomlib/comparators.circom";
include "circomlib/gates.circom";

template AND3() {
  signal input in[3];
  signal output out;
  
  signal temp;
  temp <== in[0] * in[1];
  out <== temp * in[2];
}

// j is the column number
// bits is how many bits we need
// for the LessEqThan component
template ShouldCopy(j, bits) {
  signal input sp;
  signal input is_pop;
  signal input is_push;
  signal input is_nop;
  
  // out = 1 if should copy
  signal output out;
  
  // sanity checks
  is_pop + is_push + is_nop === 1;
  is_nop * (1 - is_nop) === 0;
  is_push * (1 - is_push) === 0;
  is_pop * (1 - is_pop) === 0;
  
  // it's cheaper to compute ≠ 0 than > 0 to avoid
  // converting the number to binary
  signal spEqZero;
  signal spGteOne;
  spEqZero <== IsZero()(sp);
  spGteOne <== 1 - spEqZero;
  
  // it's cheaper to compute ≠ 0 and ≠ 1 than ≥ 2
  signal spEqOne;
  signal spGteTwo;
  spEqOne <== IsEqual()([sp, 1]);
  spGteTwo <== (1 - spEqOne) * (1 - spEqZero);
  
  // the current column is 1 or more 
  // below the stack pointer
  signal oneBelowSp <== LessEqThan(bits)([j, sp - 1]);
  
  // the current column is 2 or more
  // below the stack pointer
  signal twoBelowSP <== LessEqThan(bits)([j, sp - 2]);
  
  // condition A
  component a3A = AND3();
  a3A.in[0] <== spGteOne;
  a3A.in[1] <== oneBelowSp;
  a3A.in[2] <== is_push + is_nop;
  
  // condition B
  component a3B = AND3();
  a3B.in[0] <== spGteTwo;
  a3B.in[1] <== twoBelowSP;
  a3B.in[2] <== is_pop;
  
  component or = OR();
  or.a <== a3A.out;
  or.b <== a3B.out;  
  out <== or.out;
}

template CopyStack(m) {
  var nBits = 4;
    signal output out[m];
    signal input sp;
    signal input is_pop;
    signal input is_push;
    signal input is_nop;

    component ShouldCopys[m];
    signal copy[m];
    
    // loop over the columns
  for (var j = 0; j < m; j++) {
    ShouldCopys[j] = ShouldCopy(j, nBits);
    ShouldCopys[j].sp <== sp;
    ShouldCopys[j].is_pop <== is_pop;
    ShouldCopys[j].is_push <== is_push;
    ShouldCopys[j].is_nop <== is_nop;
    out[j] <== ShouldCopys[j].out;
  }
}

// n is how many instructions we can handle
// since all the instructions might be push,
// our stack needs capacity of up to n
template StackBuilder(n) {
  var NOP = 0;
  var PUSH = 1;
  var POP = 2;

  signal input instr[2 * n];
  
  // we add one extra row for sp because
  // our algorithm always writes to the
  // next row and we don't want to conditionally
  // check for an array-out-of-bounds
  signal output sp[n + 1];

  signal output stack[n][n];

  var IS_NOP = 0;
  var IS_PUSH = 1;
  var IS_POP = 2;
  var ARG = 3;
  
  // metaTable is the columns IS_NOP, IS_PUSH, IS_POP, ARG
  signal metaTable[n][4];

  // first instruction must be PUSH or NOP
  (instr[0] - PUSH) * (instr[0] - NOP) === 0;

  signal first_op_is_push;
  first_op_is_push <== IsEqual()([instr[0], PUSH]);

  // if the first op is NOP, we are forcing the first
  // value to be zero, but this is where the stack
  // pointer is, so it doesn't matter
  stack[0][0] <== first_op_is_push * instr[1];

  // initialize the rest of the first stack to be zero
  for (var i = 1; i < n; i++) {
      stack[0][i] <== 0;
  }

  // we fill out the 0th elements to avoid
  // uninitialzed signals. For a particular
  // execution, we only want one possible witness
  // to correspond to a particular execution
  sp[0] <== 0;
  sp[1] <== first_op_is_push;
  metaTable[0][IS_PUSH] <== first_op_is_push;
  metaTable[0][IS_POP] <== 0;
  metaTable[0][IS_NOP] <== 1 - first_op_is_push;
  metaTable[0][ARG] <== instr[1];

  // spBranch is what we add to the previous
  // stack pointer based on the opcode.
  // Could be 1, 0, or -1 depending on the
  // opcode. Since the first opcode
  // cannot be POP, -1 is not an option here.
  var SAME = 0;
  var INC = 1;
  var DEC = 2;
  signal spBranch[n][3];
  spBranch[0][INC] <== first_op_is_push * 1;
  spBranch[0][SAME] <== (1 - first_op_is_push) * 0;
  spBranch[0][DEC] <== 0;

  // populate the first row of the metaTable
  // and the stack pointer
  component EqPush[n];
  component EqNop[n];
  component EqPop[n];

  component eqSP[n][n];
  signal eqSPAndIsPush[n][n];
  for (var i = 0; i < n; i++) {
      eqSPAndIsPush[0][i] <== 0;
  }

  // signals and components for copying
  component CopyStack[n];
  signal previousCellIfShouldCopy[n][n];
  for (var i = 0; i < n; i++) {
    previousCellIfShouldCopy[0][i] <== 0;
  }
  for (var i = 1; i < n; i++) {
    // check which opcode we are executing
    EqPush[i] = IsEqual();
    EqPush[i].in[0] <== instr[2 * i];
    EqPush[i].in[1] <== PUSH;
    metaTable[i][IS_PUSH] <== EqPush[i].out;

    EqNop[i] = IsEqual();
    EqNop[i].in[0] <== instr[2 * i];
    EqNop[i].in[1] <== NOP;
    metaTable[i][IS_NOP] <== EqNop[i].out;

    EqPop[i] = IsEqual();
    EqPop[i].in[0] <== instr[2 * i];
    EqPop[i].in[1] <== POP;
    metaTable[i][IS_POP] <== EqPop[i].out;

    // get the instruction argument
    metaTable[i][ARG] <== instr[2 * i + 1];

    // if it is a push, write to the stack
    // if it is a copy, write to the stack
    CopyStack[i] = CopyStack(n);
    CopyStack[i].sp <== sp[i];
    CopyStack[i].is_push <== metaTable[i][IS_PUSH];
    CopyStack[i].is_nop <== metaTable[i][IS_NOP];
    CopyStack[i].is_pop <== metaTable[i][IS_POP];
    for (var j = 0; j < n; j++) {
      previousCellIfShouldCopy[i][j] <== CopyStack[i].out[j] * stack[i - 1][j];

      eqSP[i][j] = IsEqual();
      eqSP[i][j].in[0] <== j;
      eqSP[i][j].in[1] <== sp[i];
      eqSPAndIsPush[i][j] <== eqSP[i][j].out * metaTable[i][IS_PUSH];

      // we will either PUSH or COPY or implicilty assign 0
      stack[i][j] <== eqSPAndIsPush[i][j] * metaTable[i][ARG] + previousCellIfShouldCopy[i][j];
    }

    // write to the next row's stack pointer
    spBranch[i][INC] <== metaTable[i][IS_PUSH] * (sp[i] + 1);
    spBranch[i][SAME] <== metaTable[i][IS_NOP] * (sp[i]);
    spBranch[i][DEC] <== metaTable[i][IS_POP] * (sp[i] - 1);
    sp[i + 1] <== spBranch[i][INC] + spBranch[i][SAME] + spBranch[i][DEC];
  }
}

component main = StackBuilder(3);

/* INPUT = {
  "instr": [1, 16, 1, 20, 1, 22]
} */

总结

为了模拟随时间变化的数据结构，我们为所有可能的状态转换编写约束，然后根据标志（flags）激活这些状态转换。标志被约束为与该特定状态转换的指令相匹配。

尽管理解栈数据结构的算术化（arithmetization）可能会让人感到畏惧，但现在我们几乎已经掌握了了解如何构建基于栈的 ZKVM 所需的一切知识，这正是我们在下一章中要介绍的内容。要创建一个基于栈的 ZKVM，我们只需修改本章中介绍的指令及其各自的约束，使其与 ZKVM 的操作码匹配即可。

一般来说，大多数有意义的计算都可以建模为一个初始状态，然后进行增量更新，直至得出最终结果。我们在本章中展示的栈只是其中的一个特例。