[Music]
hi everyone so we are going to talk
about a project that we were working on
and and at at PSC that I mean when we
apply the when we apply for this uh
speaking about this the we were working
on this but now we have stopped working
on this so we are going to go through
what we were doing and the reasons why
we sto working on this so a little bit
of of the retrospective of a of a
project let's say uh so uh in I started
working in 2022 on the ckvm that at that
moment um PSC was working on uh that was
based on Hall to kind of a plish
arithmetization
and because it's it was very complicated
to to build something like that on top
of Hell 2 it's inevitable that you need
to abstract things so as a engineer I
found there like a a treasure drob of of
of really of really interesting
abstractions to be able to build the
ckvm on top of Hal 2 a lot of layers on
top of the Hal 2 to be able to to reason
about it and to kind of like yeah
abstract on it and and and build uh the
what we required and there like the
things like the stay machines no it it
seems like was like the right level of
abstraction to think about proving
computation on top of a plony
arithmetization
and the the cell manager that was used
to kind of place things in a more
efficient way on the blish table and
also how to combine like composability
with something that was called the super
Circuit and Circ and this all this was
built when I started working here but I
started kind of learning uh learning
about it uh and I found like this idea
that these abstractions actually if they
are make in an accessible way uh could
make much more easy for the average
developer to to develop CK apps and that
something like this could help multiply
CK apps development and with that we
started
chikito first as a DSL in Rust then we
added a python frontend to make it even
simpler with the idea that theel ERS
didn't need to even learn Ras they could
do it on Python and then after bringing
it to several hacker houses and working
with with Builders at a experimental
level with with more information about
how it should be built we started kind
of creating our own front our own parel
for a language that kind of has a
similar syntax to circum but has a state
machines and and more
things so in the end what we implemented
the steam machines there are the as the
kind of the definition like the
constraints of the transitions of State
machines are kind of the circuit and the
witness is the trace of a of a instance
of execution of these State machines and
that's kind of like the main abstraction
at chikito and then with the cell
managers we abstract how that is
converted to the plish table and how the
the the witness is is arranged in
efficient way and can be is is
independence of configuring different
ways to try different things then
another thing that we built is like
arbitrary Boolean Expressions
compilation to polinomial identities no
so the the constraints are expressed as
polinomial identities and and we build a
system that any Boolean expression as
complicated as necessary it will be
automatically compiled to to to this and
we kind of develop a a a mini theory
about how
how to build this uh that can be used in
other languages like how to compile any
any Boolean expression into polinomial
identities then we also like compilers
has to optimize and through optimization
can get to better performance that wow
I'm going super slow so yes we did more
things and this is how it looks the code
and uh yeah you can like for example
here you can see like arbitrary buen
Expressions that are compiled
automatically to
constraints and we saw like it was super
easy and and users really quickly could
develop like complicated things like
Blake to Hash that in the ckvn we
couldn't Implement on top of Hell 2
normally with it and we we check that
they has the same performance are
manually doing with h 2 and we found
some things that can be better and and
then the reasons to sunet it is
basically ckvm the race of ckvm make us
re that that now we are in a kind of
ckvm era that the applications we want
to build now are probably better built
by on CK VMS and thank you for all the
people participating in different stages
on on Chito H PSC Engineers researchers
and and grantees and yeah thank you very
much thanks Leo Question
Time have I had to accelerate a
lot any question oh there I'll go
closer I wanted to throw it you want to
throw you can do next okay okay hey
Lance yo what's up Leo um so question on
custom constraint systems I saw that
there was one of the um libraries that
you all Ed when it comes to ccs and ZK
VMS can you like are there any ZK VMS
that are implementing for that to go
from like plunk to
air but that wouldn't be like a to go
plong to air that would be kind of a
easy translation I think like a not a VM
but uh from PL to a be kind of easy
translation no because the difference
kind of the rotations work in the
arithmetization so we we actually yeah
we we implemented the backend as powder
that is kind of air so powder powder
yeah one of the yes the the ah I can
show this yeah I'm famili yeah yeah so
we impl back for powder that is kind of
air yeah so yeah that's e plony and and
and and and even CCS we implemented the
in CCS
sonov um so compile to we we didn't have
time to check the the performance on zob
uh but but it it was it was something
that was compilable to many different uh
proving systems do really
cool I think there's a question here
yeah you want to start
it who who this one
oh hi thank you Nikolai from terminal 3
a few questions actually first um can I
um verify your proof on chain like in B
254 uh that's basically only on now yeah
and then you said you made python but
can I do a rust code and compile it and
because most of cryptography is in Rust
so rust is very useful here and Let's do
let's do these two and then if you want
okay okay so you don't forget so the
first question on chain yes so we for
for the CVM we implemented a verifier in
solidity for the h to proof so as long
like it depends on the proving system
that you use in the in the back end if
it can be verified on on because it's
kind of independent on the proving
system can compile to different proving
systems and uh they generate different
proofs so in the it depends on that and
the second question R is built on Ras
chikito was built on R and then we put
like a parel front but yes you could
interact and connect it with other h h
two circuits built on R and kind of
actually integrated together and another
question okay we have one more question
okay there yeah better you throw it you
want to try again okay
okay last opportunity
H Too Short
soad uh so I actually not sure I
understand the difference between a ZK
VM and a ZK compiler like a ZK VM takes
your rust code transer like let's say
risk five instructions and proves that
okay yes so so so so the C so a ckvm is
one
circuit that it witness is the trace of
the execution of a instruction set so
the CVM is not a compiler it's a circuit
that takes us witness the the trace of
the execution and proves that you have
executed the the correctly the TR the
the program so so in that case you
compile Ras to this instruction
architecture and then uh yeah you you
execute it and you get the trace and
that verify that compiler takes some
kind
of description of what you Circle that
and actually kind of outputs a circuit
itself so you could build a ckvm on a
DSL in a
language I don't hear you
yeah so what what actually executes the
code like where what does the proof
proof if it doesn't prove correct
execution right with the compiler yeah
with a compiler
you generate a circuit that proes
something about a witness so so a ckvm
is a type of circuit no it's a it's a is
a it's a type of circuit that that
proves the execution of the trace of a
specific instruction
set but a circuit can prove any witness
like this follow certain properties
certain constraints in the case of the
ckvm the constraints are the correct
execution of the instruction set
happy I knew that question I knew the
answer if they ask something
different I don't think we have time for
one more question but please feel free
to talk to Leo after he's talk