[Music]
PA
please um uh so hello everybody uh so
today I'm going to present to you uh the
tech we developed to uh develop the
proof system of linear linear actually
use many many different proof systems
for many different use cases it's it is
a complex system what I'm going to
present to you is uh the one the main
one that we use for proving the
execution so concretely proving evm
execution so uh I should present myself
I'm alexand uh I've been working in this
space for seven years now uh and been
focused on cryptography for five years
now uh I've been working on Linea since
the beginning even and doing research
and roll up even before that
uh so yeah just to talk a little bit
about
myself okay so uh uh I'd like to involve
the audience a little bit who knows uh
What uh zvk evm
is right so that's a good half a good
third um so a zvm layer is uh a layer
two
solution uh which is whose purpose is to
help ethereum scalability the idea is
instead of sending transactions on the
ethereum main net you send them to a
certain party linear linear runs uh an
ethereum virtual machine will process
the transaction it will be processed
separately from the main net so the
contracts that are deployed on Main net
are not the same necessarily the same as
the on that are deployed on linear the
state are
separated uh but we can bridge between
the two I'm not going to describe much
more how we bridge between ethereum and
iner uh but what is uh important to uh
remember here is that we basically
bundle the execution of many transaction
and submit one proof at the end we give
you one number uh every finalization
finalizes on average 65,000 transaction
at once uh and since uh we are using
snack proof systems meaning they have a
very short very time which is mostly
independent from how many transactions
are executed that's how we get
scalability verifying the final proof
which is a PL proof TX uh a few
milliseconds but it's for 65,000
transaction so that's why it's much
cheaper and that's how uh the kvms can
achieve a much lower gas
price all right uh so maybe a few word
uh on um on zkp and snar zkps uh I mean
usually we say zkp but most of the time
what we use in production are ZK
argument of knowledge uh and in order to
for a protocol to be uh Z key argument
of knowledge it needs three property you
need zero knowledge zero knowledge means
that the proof does not reveal more than
what it should reveal you need to have
completeness meaning that if you want to
prove something that is true you should
always be capable of generating proof
meaning for instance if you want to know
that you prove the square root of some
number it should work for every number
and not just your favor just one number
and the most important one is uh
argument is knowledge sness or
essentially computational knowledge
sness it is how you say that you know
that you prove that you know uh what
you're proving you
know um and so as I mentioned earlier uh
we are building a ZK VM but really the
ZK is not it's not about zero knowledge
or hiding things it's really about
proving that we know valid execution
traces we explain more on that later uh
but especially we need more properties
we want the verification to be suent to
be small and we want uh also the
verification the protocol to be non
interactive it should be a single proof
a single message and from that we should
be capable of verifying uh
approve okay so let's apply all that to
uh the evm uh the etherum virtual
machine is a state
machine uh you on which we can execute
code uh and a transaction in zvm is like
an instruction from the user uh of that
virtual machine uh it has a lot it is
specialized for running smart contract
it has a lot and a lot of features and
that interact in a complex way between
each other and uh and not every
computation that are easy to do on the
evm are necessarily easy to prove so for
instance I'm thinking about the Kash
function that very smart contract uses
all the time like it's free it's really
not free to
prove um and and so if we want to solve
that problem uh so of course we need to
deal with the inent complexity of the
evm but we so need a proof system that
is flexible enough to solve all the
problem that we need to solve to execute
the
evm
concretely um in order to prove the evm
we have traces of execution that are
instantiated by polinomial we call them
colon in our
framework uh and it could be summed up
as a collection of airs that communicate
with each other by sub argument and
there are many different sub argument
that are possible to use we can have
lookups we can have projection queries
uh we also support variance of lookups
that we call conditional lookup or
fractional
lookups um and so in order to make this
work we need a proof system that is
really flexible and can deal with all
the polymorphism that is inherent to
proving uh linear arithmetization
okay so in order to do that we designed
uh the with framework which is is uh the
main uh um the main gateway between
describing the constraints to represent
evm and actually proving
things uh it has a very neat
particularity is that in the wiard
framework you work you um write
protocols in an ideal model and you
don't have to worry about how you're
going to commit to things or how which
argument you're going to you just say
what you want and then you have a list
of technique like a menu uh which you
apply to that uh protocol statement and
it will create for you uh a proof system
as complicated as you need it to be and
so that's perfect for us it turns out
that this is how in Academia they
describe uh complex protocol like if you
take for example uh the grow 16 uh proof
system uh if you had a look at the paper
before you would see that they say okay
so this is the constraint system at the
beginning then we do something that is
called qap and then we do something that
is called NP and then uh in continuous
and at the end you have a conrete proof
system which is a gross 16 proof system
but that does not translate into the
implementation people just take the
final protocol at the end that you apply
after every step of compilation of grow
16 and and there is a grow 16
implementation so what we do is that we
actually Implement every possible step
so that this step can be reused for
other proof systems and we don't have to
really mentally work out with the work
the whole
protocol in the case of Lina it would
just be
impossible and on top of that we made it
in such a way that if anybody wants to
add their own compilers or do their own
tweak or are their own type of
constraints uh the framework will allow
that without changing the core of
it all right so as I mentioned earlier
the proof system uh the protocol that
you are going to construct you have to
describe it in an ideal model and this
ideal model involves what we call the
wizard Oracle the wizard Oracle is from
the point of view of the protocol
designer a trusted third party it knows
everything it remembers everything it
does computation for free it is always
honest it's like something you really uh
if we if it existed in reality we would
not need cryptography
uh so that does not mean that uh what we
build will not be secure it just means
that the Oracle will concretely be
instantiated by something else in the
future as we compile the protocol so the
protocol can also be described in a
multiun fashion I mentioned at the
beginning that we need non interactivity
but the protocols s this out using the
fat Shamir uh the fet Shamir
trick uh it put some limitation it means
that the verifier can only send random
challenges to the prover but that's a
common limitation that every protocol
have nowaday it's very uncommon to be in
a contrary situation and so essentially
the prover can use the Oracle by sending
big large message to it and the Oracle
will just remember and notify the
verifier that hey uh the pr did is part
of the work you can ask question and so
the verifier can ask questions and the
Oracle respond to the question without
needing to do any computation it's like
a god-like
entity uh and it is always
honest so you don't have to worry about
him
lying so uh as I mentioned the prover
the verifier and the orle can send
messages to each other uh and here comes
the first primitive of the framework
which is what we call uh colons so
colons can be of any sort we have what
we call commitment committed colon
committed colon means means it is sent
to the
Oracle uh and basically being sent to
the Oracle means uh that the prover
cannot change its mind about what was
sent to the orle you can only send
something once to the orle otherwise
you're
cheating uh and the protocol will always
ensure
that uh but on top of that we have what
we call pre-computed colon so
precomputed colons are they can be of
two types they can be sent to the
verifier or sent to the
and uh they are known beforehand so
that's something that is part of the
protocol description actually they
always have the same values you can
think of for instance the plun uh
circuit description which is
instantiated by several polinomial we're
going to see how we can Implement plun
in 10 minute uh so I'm just uh pting
myself forward a little bit uh you need
uh those colons to uh as part of the
proving keys and they describe the plum
circuits and on top of that you can send
proofs and proofs means a message that
is sent directly to the verifier and
there are other types actually we have
eight types of different variant of
colon type so col also have a predefined
size can be one it has b a power of two
it's due to a limitation uh aurent
limitation in the
framework uh and they have a r
assignment and the r uh number is
essentially describing at which round of
interaction the colon is sated by the
prover so that's for the main part um
and then as I said uh so for some colon
that are sent to the Oracle or for some
groups of colons that are sent to the
Oracle the verifier can ask questions
about these colons to the Oracle so
that's what we call queries it's the
common term used in Academia uh if you
know about fries they do uh random
position opening query so that's what
they mean when they mean query in
polinomial IOP protocol that would be
univariate openings in our framework we
query stands for at the same time
constraints so that would be questions
that have a yes or no answer like is
this value the square of this other
value the answer can always be yes or no
most of the time it is sough as a
constraint uh and here we describe it as
a
query and and so we and we also have
open questions that are like polinomial
opening position opening uh and so these
have uh expect a response for from the
orle that is other than yes or no um so
we support many many different types of
query it can be lcaps it can be uh it
can be univarate evaluation it can be uh
inner product between several colons so
essentially uh most of the folklore is
there and because and we implemented it
because we needed it for the concrete
implementation of Vortex and linear
arithmetization
all right uh so as I said once you have
a protocol
description uh the only thing you need
to do is to describe how you want to go
from this description in an Ideal World
with ideal Oracle into concrete protocol
that is secure in the standard model uh
so here is the base uh description that
allow us to go from uh without IOP to
polinomial IOP at the end uh but in
practice this would not be sufficient we
would also need a polinomial commitment
to turn this into a concrete protocol uh
so in this part of the code does not
describe how we do the pomal commitment
but how we go to this
point um okay okay so now let's get onto
a practical example uh so here is uh the
plun uh constraints um description so we
have a set of colums Q's are describing
a PL circuit x a XB XC are describing
the witness uh and also usually we add
another colon on the right that is for
the public inputs and that we are going
to use on top of that plun has some copy
constraints uh which are can be
instantiated by um a permutation
argument which I'm going to show you how
to do okay so let's Implement
plun uh so as I mentioned we need to
Define our protocol then we can compile
it and after we can run run it so
running the prover and verifying it we
can also recurse automatically recurse
it but we're not going to cover that
today all
right okay so first of all defining the
protocol this is done by specifying a
function so the whole framework is in go
uh most of the prover stack of linear is
using KN and the linear prover is also
implemented Ino as it is also relying on
GAR
implementation so uh the defined
function uh has this simple uh signature
and the Builder is an object that is
going to store everything we said to
declare an entity in the protocol so
either queries colums or so on and we
can also specify checks to be done by
the verifier so let's go into
there okay so here are the colon uh
description uh so you can recognize uh
the plun uh colon that we saw at the
beginning uh so the cu's colon are for
the circuit description they should be
the same no matter what we try to prove
so they go into
precomputed uh the XX bxc are a
commitment have to be sent to the Oracle
and Pi the public input is inserted as a
proof object because it has to be
revealed to the prover so it's a bit
cont inuitive that we call that proof
but proof means a message sent to the pr
it is part of the proof even if it's a
nonsense from an Academia perspective
and also a number of public inputs uh
because the pi is po colon is larger
than the actual number of public input
is because every colon should have the
same size
so and that's the value of the CU should
be known beforehand of course because of
the circuit
description okay so now we can declare
the queries uh so on your right you have
the a global constraint which is an
arithmetic expression that has to vanish
uh on the all the rows of every colon
that is touching we can recognize the
equation of the pl gate constraint at
the beginning and we have a fixed permut
which is instantiated by some forc
permutation that has the concatenation
of XA
xbxc uh invariant and that's how PL
proves uh the copy
constraints uh then finally uh we need
to add a verifier check this is to
ensure that the pi that is sent to the
verifier is well formed and that it
should be paded on the right with zeros
okay uh so now once we have that we can
compile that into an actual protocol so
here I added the part that convert uh
the piop into uh a concrete protocol
because I added the vortex. compile
Vortex being the prial commitment that
we use and now uh we just have to run
it uh so the only thing we need to
specify is how concretely uh we are
going to assign uh our colons because
this is the only thing that is unknown
at this stage after reading the protocol
description uh so yeah we just provide
it and we assign it it's for lines of
code uh and so yeah now so we have some
things that allow us to write PL
constraints manually uh but write I
don't know if you have tried writing a
PL Circuit by hand but it is really
difficult uh and it turns out that garx
offers a very nice front end to WR
circuit so let's just write a wrapper of
what we just root uh using Gar so that
we can use a gar circuit
description so I I did the
implementation it was a bit longer than
100 lines but it was essentially a few
automated
stuff okay so let's do a circuit so
let's use uh Fibonacci as a use case uh
so my circuit you have two values U U1
as input and you want to have the 50th
number number of the Fibonacci sequence
generated by U and U1 U and U1 being
public
parameters uh so on your right you have
uh the circuit writing in KN you can see
that it's fairly easy and much simpler
than writing a circuit by hand and then
we just have to run it and that's it you
just create your proof function that is
explaining how to assign the colon you
run with. proof and is going to generate
a proof for you
using vertex of the polinomial
commitment and you can verify that in
one
line all right I have six seconds for
the uh future Improvement so we want to
add more queries and we think we can
also remove the necessity for runs in to
specify runs in the protocol as it
should be inferred
automatically right that's it you can
check out the code
here
yeah amazing alexand thanks so much for
for the great introduction of wizard so
uh reminder that if you scan the QR code
you will attend the session and you can
ask questions and you can also claim an
nft so and you can also vote so if you
have a question that you really want it
to be answered uh vote for them so let's
start with the top one uh does wizard
support local tables and can it be used
to implement uh local tables based on
ckvm uh absolutely so uh the way you
would do it is for instance say um so
what you can do first of all if you want
to do range checks so that's a big use
case for lookup table you already have a
range query so you just take one colon
and you say I have this query that just
enforce the whole colon to be within
Bond and that's all you do uh a second
way if you want to do more complicated R
checks likeor for instance then you
would have to specify three colons for
your exor one colon for the left side
the hand the right side and one for the
result and in this colon you put all the
possible uh all the possib ities uh so
maybe say for 8 Bits to 8 Bits you would
have a Col you would have two to the 16
possibility so you write down all of
that in your table and then you create a
lookup constraints between this table
and a tri plate of color for which you
want to enforce exor uh uh constraint
and you can also add a conditional
lookups you can have a force colon that
say that contains zeros or one and that
activate the the exort constraints or
not great thanks for the answer the next
question is can you create different
custom Gates and at which instance do
you decide which roow corresponds to
each kind of
gate um so when you generate a global
constraint this is essentially what is
your custom gate uh then it's going to
apply over everything um but the wiard
framework is more abstract than this uh
essentially there is a general technique
to do it uh which which is to say that
you add a selectors colon that says
which constraint is going to apply uh
for each and you have a some product of
your constraint custom Gates expression
multiplied by uh an indicative that ask
whether this constraint is active here
or not and you would merge everything
into a single Global constraint in the
end so yes you could Implement custom
gaug actually that's uh what they do all
the time uh when they specify the evm
great the next question is about
recursion so is recursion something that
would be implemented in Wizard or would
it be separately like a commitment uh so
there is separate where you can do a
recursion uh so we do it inside of the
wiard at at the same time and
outside uh so the first way we have a
compilation steps that is called self
recur that usually goes just after
Vortex that text a Vortex proof and rear
matize it and we can do proofs of that
again and we repeat and we can shrink
the proof that's because vertex uh as a
single polinomial commitment has a
square root verifier time but applying
log login application of self retion you
get constant size proof great and the
last question that we have in the queue
at least for now is uh that it's great
that you can define an ideal protocol
programmatically and it seems that that
does make it easy would would does that
make it easy or possible to support
automated formal verif ification or you
see proofs of
security um
so I'm not too sure what it would entail
exactly to formally verify so we could
formally verify uh like the standard set
of compilers that we have I think this
is at least a necessity but then there
is a protocol description it should be
formally verified this I don't know how
how to do it I don't know and I can't
tell you how to make it easy but that
would be a great use case I agree
yeah it will be great maybe after have
the conversation