Nova and Memory

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:

  1. we assume that our memory is a
    k
    -element array
    v=(v0,,vk1)
    .
  2. we commit the entire memory using KZG commitments. This means we commit to
    v
    with
    c=[p(X)]=i=0k1vi[Li(X)]

    using some secret point
    {[si]}i{0,,k1}
    as in KZG.
  3. we define 3 operations on memory, READ, ADD, and WRITE, and make them folding-friendly.

READ

First, we describe READ access. Specifically, this means proving that the

i-th element of array
v
, namely,
vi
, is equal to
y
for some public value
y
. In case of polynomial commitment, it is equivalent to proving that
p(ωi)=yi
.

The proof for opening at the

i-th position is computed as
wi=[p(X)p(ωi)Xωi].

And, to verify the correctness of the proof, we simply check that

e([s][ωi],wi)=e(c[yi],[1]).

Now, we build an R1CS and define its components. Notice that the verification of evaluation at

ωi require the involvement of
[s],c,[ωi],[yi],wi
and
[1]
, with no secret elements, so the witness vector is exactly this information.

variable value
w
([s]c[ωi][yi]wi[1])T.
A
(101000).
B
(000010).
C
(010100).

ADD

Suppose we want to change

xi to
xi+t
. Then we want to commit to a new vector
(x0,,xi1,xi+t,xi+1,,xk1)
, with commitment
c=t[Li(X)]+jxj[Lj(X)]=c+t[Li(X)]

Hence, to update

c to
c
, we simply make the addition for
c
and
t[Li(X)]
.

WRITE

Suppose we want to change

xi to
xi
. We first perform a READ to prove the value of
xi
. Then we set
t=xixi
, and ADD
t
to
xi
.

Note that opening a commitment is expensive, so READ is more expensive than ADD.

From Oskar:

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

References


  1. Proposal for Handling The Memory of zkVM, https://hackmd.io/vF1jobzsRoubyUASqQG0Zw?both ↩︎