zkVM 课程第一周作业

[qijinzing]

第二节课程结束后留下几个问题思考，希望对大家的学习有帮助。（可以任选回答）

• How does Lasso lookup, R1CS, and offline memory checking work together? Why Jolt need R1CS?
• Why Jolt-with-curves is fast in proving elliptic curve operations? How Jolt prove elliptic curve operations?
• How Jolt combined with Binius?
• I tried to verify Schnorr signature using Jolt, it requires 500GB+ memory. why does Jolt consume such a large memory?

[baidang201]

1 Lasso查找、R1CS和离线内存检查的协同工作机制：
Lasso查找通过预计算的方式优化内存随机访问
R1CS系统将计算转换为代数约束
离线内存检查用于验证内存访问的正确性
三者配合可以实现高效的零知识证明:
Lasso处理内存访问
R1CS确保计算正确性
离线检查验证内存完整性

2 Jolt-with-curves的优化机制：
使用预编译的专用电路处理常见椭圆曲线运算
实现了针对曲线运算的特定优化
通过批处理技术减少证明开销
利用定制的约束系统降低复杂度

3 Jolt与Binius的结合：
Binius作为高层框架调用Jolt的底层功能
Jolt提供基础的零知识证明能力
Binius负责更复杂的协议逻辑
两者配合可以构建完整的零知识应用

4 关于Schnorr签名验证的内存消耗问题：
大量内存消耗主要来自R1CS约束系统
Schnorr签名验证涉及复杂的椭圆曲线运算
每个运算都会产生大量约束条件

建议的优化方案：
使用批处理技术
优化约束生成
考虑使用其他签名方案

[HaroldGin931]

不要水答案哈

[wcc19840827]

1. How does Lasso lookup, R1CS, and offline memory checking work together? Why Jolt need R1CS?

Proving

1. Use Lasso lookup to speed up ISA execution and generate traces.
2. Prove that bytecode in the execution traces is part of bytecode in the setup phase with offline memory checking.
3. Transforms R1CS into sumcheck by Spartan.
4. Prove that all instruction lookups in the execution traces are correct with primary sumcheck and offline memory checking.
5. Prove that all read-write memory operations in the execution traces are correct with offline memory checking.
6. Prove that program I/O is valid with sumcheck protocol.
7. Prove that read timestamps in memory operations are correct with check the lookup table of timestamp range .

R1CS

The whole VM process (fetch-decode-execute) is correct by gluing and constraining the steps involved via an R1CS.

• Instruction lookup inputs and outputs are consistent with the value read/written from/to memory

[wcc19840827]

2. Why Jolt-with-curves is fast in proving elliptic curve operations? How Jolt prove elliptic curve operations?

Why

Elliptic curve operations are usually field operations between two 256-bit large integers, and usually eight 4-byte ints are processed in a loop.
But Jolt uses table lookup instead of calculation, directly skipping the large number calculation stage. Then sum check is used instead of R1CS, so elliptic curve operations can be quickly proved.

How

Use Visualize Lasso:

1. Decomposable Tables: subtable
2. Multi-Linear Extension: convert Vector -> Polynomial
3. Commitment: PCS
4. Sum Check: $Init \cup Write = Read \cup Final$
5. GKR Prove: random MLE point in merkel tree

[wcc19840827]

3. How Jolt combined with Binius?

I find the introduction from Binius-JoltBook

Binius is a new commitment scheme that allows Jolt to use smaller fields more efficiently. Here is a brief summary of changes that will occur in Jolt in order to incorporate the Binius commitment scheme:

• Addition and multiplication instructions will be handled via gadgets/constraint-systems instead of lookups. We may want to handle XOR and LT via gadgets too for performance reasons.

• Booleanity constraints in the R1CS can be omitted as that is guaranteed by the binding properties of the Binius commitment scheme.

• In offline memory checking (both Lasso for lookups a.k.a. read-only memory, and Spice for read-write memory), access counts need to be incremented. The Binius paper (Section 4.4) proposes to do this by sticking counts in the exponent of a generator of an appropriate multiplicative subgroup of $GF(2^{128})$, but it seems more efficient to plan to do the count increments via the addition gadget.

  For Spice, the count written during a write operation is set to the maximum of a global counter and the count returned by the preceding read operation, plus 1. If the prover is honest, this written count will always equal the global counter plus 1. This max can be implemented by having the prover commit to the binary representation of $v=global_{count}−returned_{count}$ and using the addition gadget to confirm that $returned_{count}+v=global_{count}$

• Constraints that involve addition by IMM, the immediate value, will need to implement addition via gadget.

• In the "collation" sum-check of Lasso that collates results of sub-table lookups into the result of the original big-table lookup, the algebraic implementation of "concatenate the results into one field element" changes. Over a large prime-order field, concatenating two 8-bit values a and b corresponds to $2^8⋅a+b$. Over $GF(2^{128})$ constructed via towering, $2^8$ gets replaced with an appropriate element of the tower basis. The same change affects various R1CS constraints ensuring that certain committed values are a limb decomposition of another committed value.

• Many performance optimizations become available within the various invocations of the sum-check protocol, leveraging that $GF(2^{128})$ has small characteristic and most values being summed are in $GF(2^k)$ for small k.

[Ah-lam]

（1）How does Lasso lookup, R1CS, and offline memory checking work together? Why Jolt need R1CS?

一个VM通常需要完成两件事：

• 针对VM支持的指令集架构ISA，重复执行Fetch-Decode-Execute逻辑；
• 对RAM进行读写操作。

对应到Jolt，Jolt zkVM设计了三个相互协同的组件（Lasso lookup, R1CS, and offline memory checking），以确保VM从指令执行到内存状态转变的整体正确性。

首先，Lasso lookup主要用于解决Fetch-Decode-Execute逻辑中的Execute部分，每一条RISC‑V指令的“执行”过程不是通过传统的大量算术约束来验证，而是通过预先构造的巨大查找表来完成。为此，Jolt将RISC-V指令集预编译为庞大的结构化查找表，每个RICS-V的指令对应表中的某个或某几个Items。
其二，除了指令执行外，虚拟机在执行过程中还涉及大量内存读写操作。offline memory checking用来证明每一次内存读取都确实返回了该地址上最近一次写入的正确值，从而证明内存状态在整个执行过程中的一致性。
其三，虽然Lasso lookup和offline memory checking已经涵盖了大部分执行与状态转移的正确性验证，但仍有一些程序逻辑（例如program counter (PC) update、指令标志位的校验以及各个阶段之间的衔接）无法直接用查找证明来捕捉。为此，Jolt采用了R1CS来粘合各个部分，这也相当于实现了Fetch-Decode-Execute逻辑中的Fetch-Decode部分。

总结一下，为何需要R1CS？
主要包括两点：
1). 动态逻辑补充：Lasso lookup主要解决静态指令执行的验证问题，offline memory checking 主要解决大规模读写一致性；而程序中对控制流、寄存器状态、指令时序等依赖关系，需要 R1CS 以数学形式进行描述和验证。
2). 执行粘合剂：R1CS 把指令执行（lookup）和内存操作（offline checking）的各自证明结果结合成一份完整且可验证的execution trace，确保全局状态一致，不会出现“单点正确、整体出错”的情况。

（2） Why Jolt-with-curves is fast in proving elliptic curve operations? How Jolt prove elliptic curve operations?

Jolt‐with‐curves 能够快速证明椭圆曲线运算，主要归功于其将复杂的椭圆曲线操作转换为table lookup问题。其基本思路是基于Lookup Singularity： Jolt采用Lasso lookup argument，将原本复杂的椭圆曲线运算预先构造为一个巨大但结构化的lookup table，这个lookup table包含了在椭圆曲线的base field上预先计算好的运算结果，Prover只需证明execution trace中的查找结果与lookup table中预期的结果一致。同时，利用查找表的分解性，Jolt将对整个查找表的查询拆分成对若干个小子表的查找，通过查找验证这些小部分，再合成整体结果，就可以高效地证明运算的正确性 --> 通过这一思路，Jolt大幅降低Prover的计算负担。

Jolt如何证明椭圆曲线运算：
基本思路是将lookup argument与Sum-Check协议结合，大致分为下面三步：

• 预先构造一张包含椭圆曲线运算各项预期结果的查找表；
• 将待证明的椭圆曲线操作的输入数据进行分块；
• 利用Lasso lookup argument和Sum-Check协议，证明这些分块数据在查找表中对应位置的值与运算结果一致。

（3） How Jolt combined with Binius?

Jolt最初的方案采用的是基于椭圆曲线的Hyrax多项式承诺方案，这一方案在证明时需要执行大量的椭圆曲线运算，而这些运算虽然在验证侧较为高效，但对证明者来说却开销较大。为了解决这一瓶颈，Jolt正在向Binius承诺方案转型。

Jolt combined with Binius主要体现在以下几个方面：
1). 使用small field和稀疏性优势:
Binius承诺方案设计时考虑到在许多zkVM应用中，证明者的witness（在VM中，主要指CPU execution trace中的各个状态）往往是小且稀疏的。与Hyrax不同，Binius工作在二进制域中，这使得对这些小数值的承诺和后续evaluation更高效。换句话说，证明者不必进行昂贵的MSMs，而是利用小数值的特性降低计算成本。
2). 与Sum‑Check协议的天然契合:
Binius承诺方案本质上与基于Sum‑Check协议的多变量交互式证明PIOP非常兼容。在Jolt的设计中，Lasso lookup argument利用了Sum‑Check协议来验证lookuptable中预先计算的值，而Binius正好能够高效地承诺这些通过多变量多项式表示的小值。这样一来，整个证明流程中，无论是在查找环节还是在后续的承诺和evaluation中，都能保持低开销，从而使得Prover的性能获得提升（根据 a16z crypto的公开文档，预期可以提高5倍左右）。
3). 降低Prover的计算成本并提高递归友好性:
传统的Hyrax在Verifier端需要进行$O(\sqrt{N})$级别的操作，且对递归证明不够友好，而Binius通过在更小域上的承诺，不仅减少了Prover的计算工作，使得递归验证时所需的电路规模降低。

（4） I tried to verify Schnorr signature using Jolt, it requires 500GB+ memory. why does Jolt consume such a large memory?

在Jolt的论文《Jolt: SNARKs for Virtual Machines via Lookups》的摘要中提到：“Although size-$2^{128}$ tables are vastly too large to materialize in full, the tables arising in Jolt are structured, avoiding costs that grow linearly with the table size.”

Jolt的设计核心在于利用Lasso lookup argument来验证虚拟机的执行，而lookup argument本质上需要定义一个非常巨大的查找表，其理论规模远超实际可存储的大小。
Jolt是如何解决这个问题的呢？其主要方法是使用Lasso的decomposition技术，将超大查找表拆解成多个小表，再利用多线性扩展来间接验证lookup的结果，从而避免直接materialize整个大表。

基于上述原理，当我们需要验证Schnorr signature时，使用的内存超过500GB，有可能是实现中没有充分利用查找表的decomposition技术，结果就是，系统尝试materialize过多的lookup table内容，从而导致内存需求暴涨。

[aulnes]

1. How does Lasso lookup, R1CS, and offline memory checking work together? Why Jolt need R1CS?

首先从high-level给出一个基于jolt范式ZKVM的证明过程直觉，即三个部件分别执行不同的证明任务：
1 lasso lookup 执行所有的指令内检查，即根据指令的opcode，“调用”不同的lookup table对指令中的立即数、地址和操作进行检查，确保指令执行的结果符合预期。这一部分被称为Performing instruction logic，具体指令设计见jolt paper section 4、5和6。
2 offline memory checking证明所有设计“存储”的操作的consistency。具体来说，有program code，registers和random access memory三部分。所有设计存储和读取的操作会形成一张memory表（？），然后使用成熟的内存检查技术进行证明，常见的作法是加入时间戳和操作类型和计数器再整体进行检查。
3 R1CS对所有执行trace进行约束，并假设上述两个部件执行正确。例如，约束下一指令的PC等于上一指令的PC+4，或者跳转到某个寄存器内的新地址。

R1CS补充了那些不适合或者无需用lookup证明的约束关系，同时将各个部件“整合”在了一起（比如存储和指令内的一致性等等）。

2. Why Jolt-with-curves is fast in proving elliptic curve operations? How Jolt prove elliptic curve operations?

因为jolt-with-curve采用的是基于椭圆曲线的PCS，使得证明的任何elliptic curve operations都是native field arithmetization，不需要对其进行范围约束。jolt证明椭圆曲线操作的算术与普通的算术操作类似，例如计算一个scalar multiplication，s*G，即构造一个大查找表包含所有scalar和group element及相应结果（？）。

3. How Jolt combined with Binius?

本身Jolt仍然采用PIOP+PCS的设计范式，同时其PIOP的核心为sum-check protocol，其为一multilinear多项式。而基于Binius的多项式承诺方式，工作在二进制域及其扩域上，正好与multilinear多项式不谋而合。同时，Binius改造了Ligero/Brakedown式的PCS，其二进制域的特性使得其能很好适配用于构建Merkle tree的哈希函数（如keccak），因为主流的哈希函数都涉及位运算。

4. I tried to verify Schnorr signature using Jolt, it requires 500GB+ memory. why does Jolt consume such a large memory?

正如之前提到的，Schnorr signature设计大量椭圆曲线上的运算，例如scalar multiplication和field operation。因此，对于这种field specific
的操作，无法像课上提到的AND运算一样，将大整数截断为数个比特段进行分别lookup操作。所以，其lookup table会非常庞大，具体取决于椭圆曲线的base field，一般都在256bit以上。这会带来沉重的内存开销。

PS.个人理解，欢迎讨论。

[linqining]

How does Lasso lookup, R1CS, and offline memory checking work together? Why Jolt need R1CS?
首先，zkvm的核心理念是通过对vm的执行流程做证明来实现zk证明的，vm的执行流程就是读取指令，解码指令，执行指令的过程，根据vm的执行流程，要证明对其vm执行流程证明，就要实现对这个执行流程的约束和验证，如课件所示
https://doutv.notion.site/Jolt-Lasso-for-Newbies-1591aee049b480b7a44ad7d00e3e9265，
lassoloopup,r1cs,offline memory checking 分别对应
fetch: 读取指令，r1cs约束读取的指令
decode: offline memory checking 约束读取数据的是合法的
execute: lasso 对指令的所有可能结果生成表，通过表查找，约束执行结果的合法性
其中执行指令期间可能涉及内存操作，和decode类似，通过offline memory checking 保证读取数据合法
见https://jolt.a16zcrypto.com/how/architecture.html

Why Jolt-with-curves is fast in proving elliptic curve operations? How Jolt prove elliptic curve operations?
证明有两种路线，一种使用哈希算法生成默克尔根，一种是使用基于椭圆曲线的验证，基于椭圆曲线的的验证计算量更少，运行速度更快。
使用基于椭圆曲线生成的证明，算法中通常需要对一个很大的值取模，这对于小数的计算是非常低效的，针对小数的计算，改用对小素数的取模可以加快运算。

How Jolt combined with Binius?
jolt系统中对于使用sumcheck的证明使用binus,如果io类型的证明使用了binius证明。

I tried to verify Schnorr signature using Jolt, it requires 500GB+ memory. why does Jolt consume such a large memory?
Jolt对所有RISC-V的指令都生成表，占用内存是恒定的，在运行时内存巨大不太可能是由于指令集巨大导致的，注意到Jlot每一步计算都需要生成trace,而Schnorr signature 是计算密集型的操作，和trace是成正比的，Jolt消耗大量内存应该是执行密集型计算生成trace较大导致的

[ennea8]

Why Jolt-with-curves is fast in proving elliptic curve operations? How Jolt prove elliptic curve operations?

椭圆曲线运算涉及大量大数运算，而Jolt

1. 使用查表代替运算跳过大数运算阶段。
2. 同时通过分解来优化查找表的验证过程提高效率。

Jolt如何证明椭圆曲线运算：

1. 预先构造包含椭圆曲线预期结果的查找表
2. 对椭圆曲线数据进行分块
3. 结合 Lasso lookup argument 和 Sum-Check 协议，通过查找对分块数据进行验证

[soga061]

1. Lasso lookup、R1CS 和 offline memory checking 是如何协同工作的？Jolt 为什么需要 R1CS？

• Lasso lookup 用于执行指令。传统 zkVM 会用约束来模拟每条指令的逻辑，而 Jolt 用查表的方式代替复杂的计算，每条指令的结果通过一次查表得到，大幅减少了电路规模。
• Offline memory checking** 用于验证内存读取/写入是否一致。Jolt 使用了一种优化的技术（基于 Spice 系统），确保每次读操作对应的是上一次写入的值。
• R1CS 负责处理不能通过 lookup 或 memory checking 解决的简单逻辑，比如验证操作数的选择、确认查表输入格式正确等。

2. Jolt-with-curves 为什么能高效证明 elliptic curve 运算？Jolt 是如何证明这些运算的？

• Jolt 高效的原因在于它使用了 可分解（decomposable）的大查找表。例如对 64 位输入的 elliptic curve 操作，虽然完整查表需要 $2^{128}$ 大小，但可通过拆分为更小子表来处理。
• 利用 Lasso lookup，将大查表拆解成多个小查表，每个小查表都可以用 multilinear extension 方式高效求值。
• 所以 elliptic curve 运算（如加法、乘法）被转换为多个查表和简单约束的组合，避免了传统电路中的复杂逻辑。

4. 为什么我用 Jolt 验证 Schnorr signature 时需要超过 500GB 的内存？

• Schnorr signature 涉及大量 elliptic curve 运算，这些操作在 Jolt 中通过 Lasso lookup实现，而这需要在巨大查表空间（例如 $2^{128}$）中处理。
• 虽然 Jolt 避免了完整存储查表，但 每步查表、内存访问、操作数分块等信息的中间值仍然需要大量内存来缓存和提交。
• 此外，Jolt 使用的 MSM-based polynomial commitment 方案在面对大规模输入时，会造成非常高的内存开销。

简单说，Jolt 用内存换计算，Schnorr 这类操作查表维度大、中间变量多，最终导致了 500GB+ 的内存需求。