[Music]
hi um yes so I'm Pier working at PSC and
this is a presentation done GLE with ar
now who's working at zerx Park so we are
going to walk you through uh the library
that uh we have been working on with
winda as well and Carlos over the past
year so let's let me first introduce you
a bit to the concept of IVC which means
incrementally verifiable
computation so um the main entry point
to understanding what is incrementally
verifiable computations is that um those
are kind of computations that are
repetitive so um for instance you see
this little math formula states that you
can obtain the result SN when you apply
a function n times on initial state zero
so to give you some more concrete
example you can think of it as a machine
learning model which always does the
same inferences uh on uh some different
data points or maybe some virtual
machine with a fixed set of op codes
which which does some repetitive
computations uh or a rollup which always
batch verify signatures again and again
and again and even the blockchain
consensus U where the same same
consensus algorithm is apply
um again and
again so what are the benefits of IVC
schemes that use uh folding so uh this
is where the folding schemes thing comes
in uh so folding SCS are used to
basically realize incrementally
verifiable computation and you can see
on this diagram that the idea is that at
every step of the function you will get
a public input so the Z little Z and
sorry and um uh witness so w the little
W thing and at every time the
computation is uh being uh done uh you
will have a new public States Z1 and
maybe if you want to redo another step
of the computation you will have a new
witness W1 so what you can see and
that's interesting is that the F
function is a lied independently every
time you do not have like a big circuit
where you do some kind of loop and you
say from uh IAL 0 to IAL n apply the F
function no that's not how it works here
the F function is really applied
independently every time so you get a
prover that uh whose memory is basically
dependent on the size of the function
that you are applying not on the number
of time that you are applying that the
function so that makes things very
interesting so uh you can use folding
schemes for recursion this is some form
of recursion that we have seen because
um we are just inputting the previous
state into the next St and uh folding
schemes um a folding scheme is a coin
that has been is a term that has been
coined in the Nova paper so it's
something different from what you can
see in some um in some stack protocols
it's here what we mean by folding is
really just basically taking random
linear combinations of uh Witnesses um
and the main intuition is that you can
have a folding scheme uh when um you are
uh taking this kind of combination
between Witnesses because you can show
that if you know two satisfying
Witnesses then if you take the linear
combination of those then you can obtain
another satisfying uh Witness
um also um the main workflow when you
are using um folding schemes to do IVC
is that you will do your uh IVC
computation maybe for end steps you will
get an IVC proof and this proof is not
suent so you will want to um um you will
want to compress it basically using
something that is called a decider and
it's basically a znar proof so we just
snarfy the IVC proof and obtain a more
sucin proof that you can then verify
wherever you want such as
onchain all right so let's just take a
step back and try to think a bit about
what folding schemes how folding schemes
look like so there is now what I call
the folding schemes Zoo so there are a
lot of different kind of folding schemes
because you you have a lot of different
kinds of aromatizations you have a lot
of different kinds of use cases some use
case use lookups other DS some have a
uniform computation some have nonuniform
computations so you we end up with
really a bunch of different folding
schemes some are used for plish circuits
other use some specific kind of
arithmetization
um uh thing that are adapted to folding
some do many to one folding so not two
to one but many to one folding meaning
uh instead of folding two witnesses
together you can fold n of them together
so it's a very efficient form of folding
you have also ltis bit folding more
recently so that's interesting for the
postquantum uh security properties of
those kind of things and so we really
end up with some kind of zoo um with
many different folding
schemes and even in terms of research
it's a very active area of research so
for instance just in April 2023 there
was like four different kind of folding
schemes proposal and way to do VMS with
folding schemes so it's a really active
um area of research um recently there
was some uh zero knowledge layer that
was proposed for IVC proofs so you can
generate your IVC proof on a client and
then make it ZK it's very efficient and
then for instance send that to a server
to have the server compress the proof
and send the proof on chain so those
have some really interesting um zero
knowledge properties um you we also have
latis fold which is postquantum ready
and is a pretty efficient form of um of
folding and um yeah so there is really a
bunch of stuff to to to talk about today
uh about what's going on in in the this
area of
research but let's talk a bit also about
applications because I I think that some
of you are interested to know what's
what's happening there um so for
instance um we did one experiment where
we were um uh building a Bitcoin light
client so the idea was just to prove uh
that the current blockage that we have
is um has been obtained after end blocks
and so we for instance run an uh Nova
which is a folding scheme uh on the
proof of work um uh Bitcoin um algorithm
for 100k blocks and in total that costs
us uh $30 to verify an optimism uh for
running such a huge absolutely huge
computation that we wouldn't do using
a traditional ways of um of znar proving
libraries that we have
today we also have Z kvms today that use
folding so there is the Nexus team I
think that is that is led by Yan gr and
Daniel Marin uh they use I think
hypernova for that there is also the
jolt team um uh they I they published an
update actually today uh stating that
they were interesting interested into
folding and I think they are interested
for it regarding their memory checking
algorithm for their for their ZK VM
there is also ZK machine learning uh
someone Beed into Nova um a billion
parameter I think or yes something a
billion parameter at least there was it
was a
512 CNN um Network
um that they bed into Nova and for which
they generated a proof and I think it
amounted to something like a billion
parameters model uh so you have also ZK
machine learning um yes so there is
really a bunch of projects that have
been um building on folding schemes
lately so yeah for that we have built
Sono and this is what Arno is going to
talk
about hi so yeah so on you thanks uh on
you are interested into like uh being
able to use folding schemes for your
like uh recursive circuits um so we have
this uh Library it's a like a very
experimental um thing um intended for
research but we are starting to like now
polish things uh so the idea was to have
this model Library where we are able to
add and Test new folding schemes uh
compare schemes like aples to aples and
also that allow researchers to easily
add their own schemes as happened with
the MOBA paper by nether uh they publish
the paper where they use sonov to test
their their like new design uh which
they implemented in on top of sonov uh
and now this is this was a request in
son so now this is mered so now like
part of it is in in in the library Al
but also the idea is to make it easy for
for deps to use folding like the idea is
that uh they should have a minimal code
to to be able to then fold the circuits
this idea of plaque and fold and but
also allow since we are building this on
top of the artworks set of Library um
the IDE is that that um it's easy to
switch thanks to artworks between
different curves but then uh in son also
switching between different uh folding
schemes uh and also we have some
experimental like ZK circuit language
kind of like um uh interfaces where you
can use like uh other uh than artworks
um um
languages to to define the circuit that
you want to fold and also like the third
kind of like pillar of son was to be
able to verify on chain um the the the
folding proof because this was something
that uh we we were not able to find in
any any of the other folding
implementations because of the the
characteristics so so yeah uh as I
remarked this is like a very
experimental and research library and
for the moment it's
unoptimized
so yeah so that's the developer
experience of sonov this is like what
you already saw um this is like the the
the idea of of the folding schemes and
this is like how this maps to son uh
they it's very simple like the the the
dev just needs to define the circuit
that wants to be fold uh select which
folding scheme to be used for example
Nova plus cycle fold but then you can
swap uh and with just changing one line
of code into using hypernova or Proto
Galaxy then also setting the final
decider uh that generates this um
compressed snar proof um and and then uh
in the case that you are using the
onchain uh decider uh you can then also
generate the solidity uh code like the
template that you can then deploy and
you can use this to verify the the
proofs on
chain status of the library um so so far
what we have like uh fully implemented
is like Nova hyper nova and Proto Galaxy
folding schemes the three of them using
cycle fold uh techniques uh so um and
then also for for Nova we have like the
full solidity verifier there for
hypernova Proto Galaxy like we we have
the the code in that generates the the
proofs and so on but uh it's just a
matter of like putting time to doing the
solity also then also we we started to
introduce this MOA an NOA these are just
like variant to the Nova scheme uh so
it's like with some tweaking and some
abstractions we can reuse most of the
already existing Nova code that we have
there um so it should be easy to fit
them in also and then for the front end
like how you can Define the circuit that
you want to fold um this is done through
some interface by default is artworks
but uh as experimental thing which is a
bit slower uh you can also use uh circum
Noah and no name but yeah so just to
give you a bit of like a sense Nova is
using this random linear combination for
the folding part which this is then need
this needs to be um checked inside a
circuit so then uh H hypernova instead
of doing this randomly combination uses
it linearizes the the instances and then
runs the S check uh to to prove the the
relation uh and then Proto Galaxy is
instead of random linear combination is
doing linear combinations with the
lrange bases uh in one of the settings
and in the other setting is also using
the S check but just to give you a bit
of sense of that different schemes use
different techniques so one of the goals
also here is like to be able to see in
in different use cases which one fits
better and and so on so having this
modularity then okay so this is how it
looks like the F circuit interface this
is like the the circuit that you want to
actually fold uh you just need to
implement this like the the first three
methods are just like very simple things
and then step native and generative step
constraints those are like the the the
logic that you want to do at each fault
step native is what you do in Ras like
outside the circuit and generate step
constraints is where you define the
logic of the circuit that you want to
fold so this is like the constraint that
you are folding actually just by
defining this interface like if you
implement it then you can plug this into
sonov and then uh sonov takes care of
like wrapping this inside the augmented
function cirquit um and and doing the
IBC folding and and and the rest of of
checks and so on so the idea is to have
this very simple interface that uh also
this is used so when you want to include
a new uh Zig language into being able to
use sonov just by implementing this for
for the language that you want to use uh
you you you already have it then this is
like the the the usual code that you
need uh using sonov to fold the circuit
so the main idea is that here you define
which folding schemes you want to use
and also like as you see this PS and G1
PS and G2 so the G1 G2 those are like
the cures that you use we need a cycle
of Curves but you can pick uh most of
the curves that are available in
artworks and then the pson G1 Pon G2
this is like the commitment scheme that
we use in the first curve and the
secondary curve of the curve cycle and
and then the rest is like more or less
will be the same like here we are doing
100 steps of this uh proof step which is
like the the actual folding of the IBC
and at the end you can just verify the
last one one and so here you are proving
like that after 100 repetitions of this
computation you obtain this final step
coming from the first initial St State
um so so yeah so that that's the main
idea as you can see I mean it's quite uh
like simplified and and easy to I mean
easy to reason is it easy to to have
this uh working and so on and then when
you want to change which folding scheme
you are using it's as simple as just
taking this line and then you can say
okay I want to use still Nova but now I
want to have uh in the in the first
curve I will use kg commitments so that
then I can use the final uh decider uh
the unchain decider that I can then uh
send proofs to ethereum and be verified
or you can say oh you know what I'm
going to change to hypernova so you
don't need to throw away your code you
can just replace this line and now you
are using hypernova or I'm I'm going to
use Proto Galaxy so you can then um
doing this like easy line one line
change uh you should be able to to have
this um
then when it comes to to the decider so
we we we've been folding we have this
last IBC state with the last IBC proof
so now what we can do is is like we can
compress it with the deider so we have
the offchain decider and the onchain
decider so it's also like a similar
interface and then here is how do you
use it
um and the the one of the key things was
this unchain verification um so was one
of the goals because and and we've not
seen many other folding schemes
libraries having this onchain uh
verification so the idea is that in the
original Nova this decider this
compressing of the IBC proof is done
through two Spartan proofs one on each
of the cures um in our case since we are
interested to verify inside the evm uh
the evm has some kind of restrictions uh
like we are limited to a single cure the
V 2504 and also constrained by the gas C
costs so we had to do a bit of
gymnastics to fit this so this is like a
very high level idea so we are using
cycle fold we end up having um some
instances and what we do is we combine
some uh growth 16 circuit that also
contains some non-native arithmetic
stuff uh combined with the KGC
commitments proof so at the end in
ethereum we just verify one growth 16
and two kg commitments for the case of
Nova for example um so this is very
suene and cheap in terms of gas costs um
and also yes so you can generate the
solidity Cote also from from the library
um so uh to to wrap up some preliminary
numbers uh just as a remark um until now
we've been focusing on implementing the
various folding schemes not on
optimizing so that's why now so now we
have the Nova hypernova and Proto Galaxy
all of them using cycle fold um we've
not been focusing on optimization and
efficiency um but looks like the the
current numbers that we have when we
Rand some preliminary benchmarks they
look promising um and and the next steps
will be to start profiling optimizing
and adding benchmarks and like stopping
adding new papers that are appearing and
focus for few months to like optimizing
things and making them a bit more fast
and paralyzing and and so on and then
getting to a f release because until now
is just like commit after commit and the
interface might break so some
unoptimized preliminary numbers so each
folding step this is the recursive
iteration uh for a minimal circuit it
takes like 300 milliseconds um
this is there is this overhead of the
the fixed cost of the five 50,000 uh uh
sorry 50,000 a1cs constraints um then
when but so it Tak this like about uh
300 milliseconds on a like uh today's
laptop then when you want to um prove
offchain the decider and Kur takes less
than one minute it should be much less
uh but it's just that we are using pting
based snarks on both both sides of the C
cycle the idea is that this should be
using Spartan at some point and the
modified version of Spartan that uses
the relaxer 1cs so then it should be
also quite efficient um and then for the
offchain decider which is one of the
main contributions from sonov um we have
this big circuit at the end that does
this gymnastics and non-native
arithmetic stuff to fit into the
ethereum uh curve um that it takes less
than 3 minutes in in a like in a in my
ThinkPad uh and the gas costs are 800k
of gas mostly from GR 16 proofs and kg
proof um well one growth 16 and two kg
proof in case of Nova uh the idea is
that this should be reduced to less than
500 with some tricks of the hashing and
of the bound inputs and and of the um um
combinations of pings um yeah so just as
a wrap up uh main takeaways that you can
get from from this t uh first of all
folding schemes are not a tool that fits
in all the use cases but when when it
fits into some use case that you have a
something that is like the same
structure of the circuit very repetitive
and and done uh a lot of times uh again
and again and again then folding
presents a big uh speed up compared to
full recursion of other approaches and
then uh well some of is experimental uh
the schemes that we have and we have the
onchain verification and preliminary V
marks look promising and the next steps
uh in the short term is to optimize and
and Benchmark well and um do me memory
profiling and and so on and that's it
[Applause]
cool cool
gra um yeah so I personally actually use
son and I can tell that it is quite
generic and also easy to use so if we
take some questions so the most upvoted
one is the first one so folding schemes
initially gained a lot of attention but
we haven't seen many advantages in
Practical implementation against stocks
can you compare them with stocks and
what are the advantages quite opiniated
question right yeah so who one of the
perspectives that we have on on folding
schemes in general is that is not this
tool that fits into all use cases like
the same Hammer that you can use on
everything uh it's very kind of specific
and like uh spe specifically in son we
have this IBC uh model so this you you
need to model your your use case to to
that so it will not fit all the use
cases but for the ones that it fits then
it's it's like it's sub substantially
faster than doing full recursion with
Starks uh but it's not as as like
flexible as as you would have with when
you are doing full recursion like uh
like for example taking a plony to
Circuit where inside you verify a
previous plit to proof this is like full
recursion and so part of your circuit is
doing the full verification of the
previous Stark proof uh this is more
expensive this is a bit slower but it's
much more flexible and and easy to to
manage and from the engineering point of
view also with folding is more specific
so not for all the use cases but when
you have a use case that it fits well
it's it's like in 300 milliseconds you
you can like do each one of the
recursive recursive steps makes sense
maybe you can also do folding with
stocks which takes us to the second
question what's the status of folding of
of
stocks so our team didn't really work on
that uh so maybe you want to you have
something to so there was there was um
some paper where they were showing how
to do folding of starks uh bonded to a
certain number of repetitions um and I
think The Arc paper came last month or
something like this I think the one was
like MOA does stocks fold in or it
something else MOA is with is like a
variant of Nova
okay there are being improvements and
and so but so far uh this library has
been focusing on IBC uh with like Air1
CS or CCS surrounding things not with
with Starks the same for ltis fault I
see next question regarding to ltis ltis
also requires a different like uh so you
work over the uh of polinomial and not
on the like finite fields that we use in
in the traditional snarks um so also it
will require like having F like some
layer of of all this like uh instead of
the field arithmetic the the ring stuff
uh that that it's not at least in in
artworks uh so so yeah and the folding
Starks it looks promising because Starks
are already fast uh if we can get to a
state where we can use the folding
techniques uh so the main idea is that
with folding uh without Starks we use
this uh amorphic commitment schemes so
that you can uh combine commitments to
some vectors or polinomial and then uh
this result of the this linear
combination of them uh still holds some
relations with Starks since the
commitments are not um additively
homomorphic um uh we are not there yet
but uh it looks like uh the people in
the Academia or in behind the papers
will bring some uh improvements yeah I
think Dan Bon is waiting for you to
implement that his
fault uh um so next question uh folding
papers work with different
arithmetization A1 CS blage CCS now that
you did the implementation is it
efficient for anything other than Air1
CS another op answered
question um is it efficient for anything
other than one
CS
uh well uh so there is basically let
lettis fold that is not using the R1 CS
optimization where you can use the idea
that are from the previous folding
papers uh for a different kind of
arithmetization
so uh there is also the question above
what's the status of folding for Stacks
you can reuse the ideas that were in
folding papers for another kind of AR I
guess the arithmetization
um so for a different kind of for an
arithmetization that is different from
R1 CS
um and uh so yeah I guess that that
answer the question if I understand so
yeah if we can just scroll down to see
the questions or maybe I can check them
on my phone
yeah so how does sonobi compareed to
Nexus so um first of all Nexus is like a
full uh Company veed by VCS and their
team is amazing like it's a bunch of
people from Stanford and and so very
good team so no it's like a small team
like we are like three four people uh
and and we've been doing this but like
uh uh in a more experimental uh like not
production uh focused but so far the
benchmarks that we run uh when you run
the Benchmark in the same machine for
the now implementation it's almost like
the same like it's like from 300
milliseconds in Nexus Nova to 310
milliseconds in sonov so it's almost the
same hypernova in son is much slower but
because it's it's far from being
optimized and then uh we also have the
Proto Galaxy uh but in Nexus is not
there but so the thing is that both
libraries are based on artworks so like
the the the max speed should be similar
um and both are using cycle fault which
like the Microsoft Nova is not using
cycle fault it has a different R so we
have time for the Q&A so why if we thank
again our speakers and give them a round
of applause thank you