why can't memory just be treated as part of the input / output
One thing that Nova does not exactly do (but Supernova does?) is supporting VM memory. We can think of memory as part of the state of computation and is abstractly just a vector that is "carried" with the computation.
Is this just making a new row/vector in the R1CS?
A natural design [1] for supporting memory that is folding friendly would be the following:
READ
, ADD
, and WRITE
, and make them folding-friendly.READ
First, we describe READ
access. Specifically, this means proving that the
The proof for opening at the
And, to verify the correctness of the proof, we simply check that
Now, we build an R1CS and define its components. Notice that the verification of evaluation at
variable | value |
---|---|
ADD
Suppose we want to change
Hence, to update
WRITE
Suppose we want to change READ
to prove the value of ADD
Note that opening a commitment is expensive, so READ
is more expensive than ADD
.
Supernova is about supporting different types of F, that correspond to e.g. diff opcodes, like ADD, MUL etc, in a VM. This reduces the prover overhead because an additional opcodes doesn't incur additional cost on the circuit. See https://zkresear.ch/t/towards-a-nova-based-zk-vm/105#supernova-vm-10
I don't think there's any else specific to memory in SuperNova.
More for other doc: It might also be useful to make a distinction between stack vs heap memory since they have diff characteristics
Proposal for Handling The Memory of zkVM, https://hackmd.io/vF1jobzsRoubyUASqQG0Zw?both ↩︎