foreign
[Music]
I'm Nolan I'm ingtong and today we're
going to talk about recursive ZK snarks
the kinds of applications they unlock
and how we can Implement them so first
we should talk about what recursive
proofs even are so in the context of
snork recursion is usually the ability
to verify a smart proof inside of
another snug proof so this is the
ability to say something like I know is
not proof that when I run the smart
verification algorithm on it returns
true inside of another is not proof and
the sort of key part here is that
verification of regressive ZK snarks is
usually not significantly slower than
ordinary regular CK smart verification
so now that we have this primitive in
mind we should think about the sort of
natural question is why would you want
to make recursive smart proofs so
typically regular ZK snarks you know we
think of them as having two uh sort of
properties such signals and their
knowledge so recursion in fact unlocks
powerful versions of both of these
properties
in the form of compression which is a
stronger version of the cygnus and
multi-party composibility from zero
knowledge
so first let's talk about compression we
think of compression as supercharging
succinctness and in particular usually
the applications of compression tend to
share a sort of common pattern
um and this common pattern looks like
you know let's say we have a prover who
wants to show a verifier
um some n pieces of knowledge how do
they do this
they make a proof showing two sort of
things first they show one piece of
knowledge and then they also show you
know Additionally the N minus one other
pieces of knowledge but for these n
minus one pieces instead of showing each
piece individually they will show that
they know a another smart proof of these
n minus one pieces
so the next question is how do you make
the smart pool for the N minus one
pieces of knowledge
um and in fact we use the same kind of
strategy again the N minus one pieces of
knowledge we show one piece of knowledge
and additionally we show that we know
another proof of n minus two pieces of
knowledge
and so then you know you just Cascade
down this sort of strategy and you end
up with the situation where you're
verifying uh one uh snark proof and in
that it's automatically verifying these
n items of knowledge another instance of
compression that's particularly helpful
to point out is the setting where you
want to compose between different proof
systems or arithmetizations and at the
time also pick the good features of each
of them so for instance you can have
some setting where you have two
different proving schemes one where you
have a fast prover but unfortunately the
verifier is slow and another where the
approver is lower but you get the
trade-offs that the verifier is fast so
using recursion you can compose between
the proving system from The Wider
setting to the narrower setting and get
a tiny proof output as well as
fast-provers getting sort of the best of
the Both Worlds
um a concrete sort of instantiation of
this interoperability is the setting
which starts and grot16 in particular
grads grad 16 is very cheap to verify
whereas Starks are very easy to prove so
if you verify a stark roof inside of a
graphics scene snark you end up with a
proof of the original statement with the
fast-prover as well as a fast verifier
so generally compression has this sort
of property that is very mechanical and
usually you're rolling up some giant
list of computation or items of
knowledge increment into a single proof
so just to give a flavor for sort of
what applications this unlocks let's
look at things that are interesting to
roll up so first is signatures over the
summer we built applications using sort
of this primitive of recursive
compression of signatures called
isocratia where we end up with a low
trust low cost sort of roll-up of
off-chain modes and end up securing
governance and then more related to sort
of blockchain land you can do the same
kind of trick with light climb boots and
in fact plumo which is solos light
client is based on this sort of idea and
there's also another group named Axiom
which is exploring sort of more cooler
use cases for this with aggregating and
providing historical data through the
use of recursive snarks and then finally
the sort of Hot Topic in blockchain land
these days is making roll ups of
transactions two particular ones that
are sort of interesting to point out are
Mina who sort of use this recursion
primitive as a consensus player
primitive and polygon Hermes who use the
exact strategy of like using Starks for
fast-prover settings and grad 16 or
snarks for fast verification settings
next let's talk about composability my
personal favorite property unlocked by
recursive Snooks so to give some context
for this let's take a step back let's
think about what a normal ZK proof uh
you know what's the context of a normal
ziki proof we usually think of you know
DK proofs in this context where approver
is showing knowledge to a verifier
without revealing the underlying fact of
the knowledge with recursion in fact you
can unlock something more powerful
approver can show knowledge to a
verifier without fully knowing the
underlying facts themselves
so this is a bit hard to model so I'll
just lead with an example over the
summer we build this application called
eat dos which is a dash number is on
social graphs so these social graphs are
sort of graphs of relationships of
people saying I am your friend kinds of
things and for instance here we have
this graph and vitalik sent someone who
sends someone who sends someone and
finally I ended up with a four degree
path to vitalik now I can prove that I
have a four degree path of italic
without reviewing any or without knowing
any of the intermediate parties in this
path so how do I do this I say I am a
friend of adhian and adyan has a ZK
proof that he is three degrees from
italic so in this process I do not know
the three degrees that precede adyan and
I have still convinced any external as
well as myself that there is a valid
path of four degree between me and
vidalic so of course this is not the
only application you can build um in
general we think composability is
particularly cool to think of in sort of
incomplete information game kinds of
settings and of course the sort of very
typical example the the phrase starting
point we thought of was games like
telephone or Chinese Whispers where you
know you pass a word around or something
and you want to make edits to it uh
incrementally and then you can make more
complex applications like party games
like Mafia those kinds of things and
then more relevant to blockchain land
you can build private State channels and
roll ups of that sort
so now that we have some intuition for
the high level properties of recursive
proofs and now that we've seen some
classes of applications that are enabled
by them you might be feeling that
recursive proofs are kind of
unreasonable we get unlimited
compression and compostability
so I guess the natural question now is
how do we Implement and construct these
systems
so right now there's broadly three
classes of recursive proofs in
production and as we descend the
hierarchy we are relaxing the
requirements on the proof systems which
are eligible for recursive schemes
so at the very top of the hierarchy we
have really the most stringent
requirements so we we need proof systems
with verifiers that are sub-linear that
are succinct in the size of the
statement being proven and this enables
us to do full recursion at every
recursive step
so this has been implemented for the
growth 16 and Fry priv systems
so if we relax our requirements a little
bit and we say even if we don't have a
succinct verifier
maybe we're happy enough just with a
succinct accumulator so intuitively what
this means is that we want a verifier
with this shape that they have a
succinct check a cheap check and then
separately they have an expensive check
and so here we can instantiate an atomic
accumulator and at each recursive step
we only perform the succinct checks
and we accumulate the expensive check
and delay checking it until the end of a
long batch of proofs and doing this
gives us amortization of the expensive
check and finally if we relax even more
um we don't even require a succinct
accumulator well now we're just happy
with a succinct public accumulator and
the idea behind this split accumulation
is simply that you split your
accumulator into a public and private
part and the public part is short and
this is what we accumulate at each
recursive step
um where whereas we delay the
verification of the private part of the
accumulator until the very end so let's
go through these constructions at a high
level one by one just so you can see the
shape of it so probably the cleanest
shape is the the cleanest shape would be
full recursion so
over here we start with our application
circuit and it's f
um
F of w-i-z-i gives you z i plus one
right it's a normal relation
now we bundle that together with a
recursive verifier
and
um basically this recursive verifier
takes in a proof instance that was
produced by the previous instance of the
recursive circuit and so if if we look
forward we we need to generate a proof
of the whole recursive circuit in order
to input to the next recursive instance
so in this way we're chaining recursive
circuits and at each step we are fully
verifying the previous instance and when
we get to the final verifier we no
longer need to bundle it with the
applications are getting here we can
just perform a final verification of the
proof outside the circuit so this is
full recursion is is the cleanest API
um
now we're gonna get slightly more messy
and we're gonna relax our requirements
um to get an atomic accumulation scheme
so now if you recall here an atomic
accumulation scheme our verifier is not
sublinear so in fact the verifier inside
the recursive circuit is just the
accumulation verifier and it only
concerns itself with the succinct checks
of the verifier
um and the expensive check is
accumulated and deferred um at each step
so here we are chaining basically
instances of proofs and accumulators
um and at each step we're just
procrastinating on performing the
expensive check well until we're finally
satisfied at the end of a long chain of
proofs
we perform the final decider
sub-particle that finally bites the
bullet and does the linear time check
but at this point we can do it outside
the circuit and at this point the cost
of the linear time check is amortized
across a big batch of proofs now from
here to Atomic accumulation is just a
small step so it's just splitting up
your accumulator and your proof instance
into a public and private part and now
the verifier the recursive verifier gets
even smaller and it concerns itself only
with accumulating the instances the
public parts and it does not perform it
does not have access to the private
parts of the accumulator and rather it
relies on the Pervert to provide some
commitments to the private parts
which it then performs accumulator
checks on
so a lot of these constructions I've
described are really cutting edge and
they come from a feature of our modern
proof systems that are very modular in
design and as we get a better
understanding of the building blocks and
the components of our proof systems this
lets us customize our proving Stacks
with a lot finer granularity and
recursion as we saw also allows us to
compose proof systems and to get the
best of both worlds in many cases so
here's an example of a modular
conception of a proof system so I work
on the proof system Halo 2. and I think
of Halo 2 in terms of these four
components so at the very front end is
where you're interfacing with your
business logic so you take a relation
and you arithmetize it into
um
so in in Halo 2's case we encode our
values in the LaGrange basis and we
encode constraints on these values as
polynomial identities
we then input these polynomials into
this information theoretic polynomial
IOP
that basically checks the correctness
and the consistency of the polynomials
encoding our circuit and then we realize
this polynomial IOP using a
cryptographic compiler so in this case
it's the inner product argument that and
the Fiat Shamir transform that allows
the proverb to Define their interaction
with the verifier and at the very end of
it Halo 2 is a recursive group system
and we can in fact instantiate an atomic
accumulator over the inner product
argument so these are the four
sort of modular pieces of modern proof
systems that I think of now we can do
pretty funny things
um composing these pieces so I've set up
three cases
um
so the first one is information
theoretic compilers
and an example of this is MPC in the
head
um what this does is it converts one
information theoretic protocol to
another one and in this case
it's the proverb sort of pretending to
run a multi-party computation
in in her head
um so she's really simulating the
multiple views in an NPC and committing
to those views and now the verifier is
only checking the outer protocol being
the NPC instead of checking the inner
protocol which is the ZK proof so this
is one very interesting way to compose
proof systems another way that we've
seen before in this presentation is more
or less just implementing verifier X and
prover Y and you would do this also for
efficiency gains and um
sort of the last Clause of composition
that I came up with was
really just thinking up better
cryptographic compilers so
there's this recent paper by a group at
consensus
um and they they took this protocol gkr
that's highly optimized for repetitive
computations like hash functions
now but the problem of gkr is that it
has a slow verifier and
um
so and it also uses the Fiat Shamir hash
as a cryptographic compiler and this
makes it very inefficient in the context
of recursion
so what the team at consensus did was
they came up with their own
cryptographic compiler that was custom
made for their target proof system and
the target proof system here is like a
growth 16
r1cs
per system
and so really like that's going in the
middle and making changes like
customizing proof systems at a very low
level
um for efficiency and yeah I think this
this leads me to ask
um whether or not we can systematize
this process and
um whether or not we can
I don't know
um explore this optimization space in a
well-defined way
so
you can think of this as kind of a call
to action
so I think there's certain
nice to have certain to Do's that all
proof system implementers would really
like the first being good benchmarks
Fair benchmarks of heavily used
Primitives like hash functions like big
and arithmetic so benchmarks of these
Primitives across different proving
stacks and the second would be it's a
kind of a meta requirement is to think
of like what metrics we're interested in
for example efficiency for example proof
size
and basically how to optimize towards
these Magics so on what basis are we
comparing different compositions and
configurations and the last sort of call
to action would be to think carefully
about how security properties also
compose like excuse me like is it the
least secure approved system the the
fewest bits of secure 30 or like some
weird composition
when we mix and match proof systems so
all these are questions that it would be
great to have everyone's input on
like even this taxonomy that I came up
with I'm not sure that it captures
um all features of proof systems in the
best way so
Nolan and I actually help out at a group
called Xerox Park oh we didn't put the
name on the slide it's 0x Park
um and there we're setting up this task
force to look into this area of
recursion aggregation and composition
um yeah and I think like I might as well
take this opportunity to shout out Xerox
Park and they supported a lot of our
work a lot of those fun apps and a lot
of these Community efforts
yeah I think that is all I have so thank
you awesome well thank you so much we
have time for one or two questions if
you have any questions please raise your
hand we've got a question here on this
side hi I didn't think this would work
for years and years and years
um and I also I'm not I'm not even sure
that does work it does seem way too good
to be true so can you prove and how do
you prove that that it's secure to do
recursive like proofs like this like
where where is the security proof
you know I don't know how to convince
myself that this works actually
yeah I mean that is a good question it
seems very unreasonable that you can
prove like an arbitrarily long history
of computation with a constant size
proof
um it does seem unreasonable so
I will say that security proves exist
there in papers
um but now and do you have like some
intuition as to why the security should
hold uh yeah for sure I I think one sort
of physics-based view that we've seen
before is like it's like oh you're 3D
space and you're collapsing into like a
2d surface
um I forget the exact name of this but
the holographic principle
uh so I I think there is like some sort
of meta justification you can come up
with to convince yourself if that's like
this sort of thing but there is fruits
of all kind that are actually
substantial it's a good question
any last minute questions
we have one at the back all the way over
there
so recursive proofs are real fun but if
you do it at scale then you're you know
it's like you you you have skill and
corruptus snapping at your heels uh
because of the proof carrying data right
if you want to build on recursive proofs
and it doesn't happen at the same time
so let's say you do a proof and you do
recursive proof and then you have to
wait for a state change for something
else it might happen much later you need
to keep the proof carrying data around
and as you know if as you know but most
here that is typically a very large
amount of data
um so it's like if you're doing it at
scale you're really running into the
issues of data provisioning and all the
fun part can get really expensive really
really quickly not even talking about
like the the
um you know the the computational
overhead that you have
yeah yeah for sure I think I don't think
recursive proofs are a silver bullet and
I think they're better suited for some
shapes of applications so recursive
proofs are very commonly used to reduce
proverb space complexity so breaking up
a large circuit into many smaller
parallelizable circuits so yeah but I I
agree like in context of applications
with more complicated and like timely
data flows it's it's we have to put some
care into how and where we are inserting
this proof carrying data yeah
right and also just to add uh I think
there's also some interesting like sort
of clean separation here of like rules
versus data availability sort of
problems um and if you just look at you
know data availability as a sort of
Black Box problem you know you have lots
of blockchain kinds of solutions for it
and for instance isocratia explorers
um one sort of solution that um
maybe you can check out The Blog on
yeah also to add on to that like I I
really like knowledge thing about
composability the fact that um
you know you you can play incomplete
information games so I think sort of fun
applications like that that are unique
to PCD are also very interesting to
explore
amazing that's all the time we have for
today please give Ian and Elaine a big
round of applause
[Applause]