包含动态循环语句的程序 如何获得其 polynomial constraints？

[keroro520]

我对下图的理解是，在做 consistency check 时，Verifier 会校验 computation trace 跟 compose polynomial 的一致性。其中，compose polynomial 涉及到 "encode the program $A$" -> "polynomial constraints" -> "bundle constraints"。

我的疑惑是， "encode the program $A$" -> "polynomial constraints" 是静态编译的过程吗？如果 program $A$ 包含动态循环控制语句，那要怎么处理？

例如 program $A$ 为下方代码，其中 x 是 private input 或 public input:

function sum(x) {
  acc = 0
  for(i = 1; i <= x; i++) {
    acc = acc + x
  }
  return acc
}

由于程序包含动态循环语句，所以 execution trace 的长度会随着 x 的不同而不同。x = 1 时 trace 为 ADD R0 R0 1，x = 2 时 trace 就变成了 ADD R0 R0 1; ADD R0 R0 2。

那么 PLONK 和 STARK 在 "encode the program $A$" -> "polynomial constraints" 这个过程怎么处理的，怎么得到一个含有动态循环的程序的 polynomial constraints？

[readygo67]

在groth16/plonk 中不同的循环次数会得到不同的电路，所以得不到一个动态的电路。
我的理解，stark中对应不同的循环次数得到的trace的数目不一致 => proof size大小不一样 => 不同的电路。

[keroro520]

感谢你的解答🙏🏻

我接着问一下哈。像zkrollup这种支持任意计算的智能合约的应用，输入不同的 input transaction会得到不同的 polynomial constraints，那verifier在不知道 input transaction 的情况下，似乎就做不了 consistency check 了，因为verifier无法在不知道input的前提下编译出所对应的电路，是这样吗？所以zkrollup verifier不做consistency check？

[readygo67]

如果是plonk verifier，
假设 是一个A -> B 的ERC20转账的场景，不考虑gas，verifier 只关心，

1. A 转出的金额 <= A 转出前的余额，
2. A转出后的余额 = A 转出前的余额 - 转出的金额
3. B 增加后的余额 = B 增加前的余额 + 转出金额
4. B 增加后的余额 > B 增加前的余额(防止上溢)
   如果转出前用户的余额是100， 转出金额可以是[1,100]的 任意值， 这样的交易对verifier 可以用同一个电路验证。
   不清楚 “输入不同的 input transaction会得到不同的 polynomial constraints”想表达是什么意思？

[keroro520]

因为zkrollup支持各种各样的智能合约，比如tx1是 erc20转账，tx2是amm swap，tx3是defi loan等等。不同的 tx 就会对应不同的电路，这是我想表达的“输入不同的input transaction得到不同的电路，所以对应不同的polynomial constraints”。可是zkrollup 又只有一个统一的 verifier。

[keroro520]

更复杂一点的场景是，合约A在执行时，有时会去调用合约B，有时却不调B而会去调用合约C。

[readygo67]

这个可用zkevm 来做，只要验证执行的evm trace 符合要求就可以。简单的说，比如执行一个ADD 指令，只要证明 各个寄存器的更新都符合ADD 的要求即可。你可以查一下zKEVM 的原理。
这个时候就不必拘泥于业务做什么了。

[keroro520]

嗯嗯，谢谢哈，我再看看。
现在是因为在看zkvm，所以萌生了这个问题。我再看看实际的实现，看是我哪儿有误解。

[readygo67]

你可以看看https://www.youtube.com/watch?v=SEp5SFaYQHY 这个视频，里面有讲到一些zkevm思路。

[keroro520]

对于某些固定电路的场景，Verifier 要确保 "Program" 和 "Constraints" 的严格对应关系。比如要求第一条指令必须是 OP_ADD，第二条指令必须是 OP_MUL，那么所对应的 "Constraints" 必须是 [ OP_ADD constraint, OP_MUL constraints, ...]。我认为这类要求「某个位置需要是既定的 instructions」是要硬编码到 Verifier 的代码实现里的。

对于非固定电路的场景，比如 zkRollup，Verifier 不需要确保 "Program"->"Constraints" 的对应关系。我想这应该是 @readygo67 上面指的 “这个时候就不必拘泥于业务做什么了”。

[keroro520]

"consistency check" 正确的理解是指 consistency between "Trace Column Polynomials"<-> "CP"，
但是我在原始提问的时候误解为 "Program" <-> "Constraints"，
所以造成歧义了 😂 cc @readygo67