foreign
[Music]
math this is also developing this is
also tooling for developers so today I'm
going to present Socrates I'm going to
give a quick introduction to what it is
for those of you who don't know it and
then I will present a few things that
we've been working on and that I'm
excited to share so what is Socrates if
you want to program snarks today
there's different tools that you can use
maybe some of you have heard of Socrates
and all those tools have different
trade-offs in terms of power that they
give to developers and how easy they are
to use and how high level or low level
they are Socrates
has a positioning as a very high level
language so when you write Socrates it
looks very similar to if you were
writing rust or python or something like
that it compiles to r1cs so this is uh
the kind of snarks that are easy to
verify today on ethereum so you can
verify directly in your smart contracts
it uses modular backend implementations
which means that rocket is does not
develop a proof system itself but rather
uses
back-end implementations from the
community for different proof systems
and just targets that and uses those
great implementations
in order to have such a high level
language but still have something that's
really efficient at the at the low level
zocoties Max use of optimizations in the
compiler which is something that's also
different from some other tools which
give you a very low level access to
what's going on on the constraint level
but don't really apply a lot of
optimizations
um so where does it run so the part of
Socrates uh which allows you to compile
so the compiler you can run it natively
on your machine we have a remix plugin
as well and we also now have a
playground that you can access at play
dot socrate.es which I encourage you to
to start that's probably the easiest way
to get started with Socrates and just
write some simple programs
um in terms of the schemes so there's
back-end implementations that we support
we currently have support for a graph 16
which is some of you may know the the
snark that is the smallest
and the fastest to verify for gm17 which
is an uh
an evolution of graph 16 let's say for
Moreland which is a universal snark
which I'll touch on a bit later
and for Nova which I also go into which
is a new type of exciting snark that
enables new use cases
for proving so the particular
implementations we rely on Bellman Arc
Bel person and also snark.js
I'll also go into a bit more detail on
on that integration
and in terms of the verifier we have you
can verify in JavaScript or in this in
the CLI and for some of the schemes that
are compatible with devm we generate a
verifier contract so that you can
directly send your proofs to your smart
contracts and verify them and and Link
them to your dab
so to give a bit of a Hello word of
zocoties here's a a program which takes
two private inputs A and B
and one public input C and then asserts
that a times B is equals to C so
technically this is a program where with
which you can prove that you know the
factorization of a number the way you
would run that is you would first
compile that program which would turn it
into this low level representation uh
that's let's say r1cs
then you could execute that program with
an input here three three and nine then
you could generate a proof using a
particular proof system and you could
also
generate a verifier that you can then
Deploy on the evm
and then send you proof to and then
convince basically convince the network
that you actually knew this
factorization for an example if
something that's a little bit more
advanced to make the point that this is
actually a high level language
here's the implementation and Socrates
of the shot 256 function
so just to give you a few things that
are expected in high level language we
have a module import system you can
import constants as well we have for
Loops of course we have function calls
and also one exciting thing that we
added kind of recently and maybe some of
you who use rust are familiar with that
feature is the notion of constant
generics so in this case the shot 25
shot 256 function is a hash function
that can take an arbitrary number of
bytes as input however in circuits all
the inputs are always static so all of
these uh the size of the input will
always have to be known at compile time
but this is something that we do you can
still Define this uh as something that
is generic over K and then have a number
of rounds of this sha round function
but then when you compile your program
and actually use the function the shot
five six
this this variable K is going to have a
concrete value which will then compile
to the exact number of blocks that
you're hashing and if you're trying to
do something that's Dynamic calling this
function on something that's not whose
size does not know that compile time is
just going to fail at compile time so we
can have a very idiomatic implementation
of chapter five six of course there's
more complexity in the show around but
if you look at the code it's
almost line for line equivalent to uh an
implementation that you would see on
Wikipedia for example as pseudocode
implementation
now I'm going to go in a bit more detail
on a a detail of the shot 256
implementation so inside the Sha round
this expression needs to be calculated
a lot of times it basically takes three
unsigned integers a b and c of 32 bits
and calculates a and bigs or ancs or BNC
and this is something that you can just
write like this in Socrates today
compile and it will translate that to a
number of constraints at the low level
however
if you do the math and look at the let's
say the first bit of a the first bit of
B and the first bit of C
you can see that if you considering them
as numbers so as field elements they
actually verify so the result actually
verifies those two equations
so you define or you constrain a new
variable BC to be equals to equal to B
times C and here I just want to clarify
that these constraints are the low level
constraints that we deal with so the
r1cn's constraints they look like this
they have one sign which is linear so in
this case it's only one variable but you
can have a sum of different variables
one side which is quadratic right so
this first one uh just defines BC or
like constrains a new variable BC to be
equal to B times C and then uh
introduces this res variable here which
is our result for the first bit
um and then constrains it in this way
and this is actually more efficient that
what the compiler would generate itself
because here we have uh more knowledge
of what we're actually trying to do
than the compiler does
on the flip side here what we're doing
is that we're introducing a new variable
res and then constraining it with this
uh with this equation however when
you're dealing with such low level
details in strikes it's really easy to
introduce new variables but fail to
constrain them sufficiently so that you
actually introduce vulnerabilities in
your circuits
so this is something that Socrates does
not expose at the moment to the
developer which means that you can only
do this one which is less efficient if
you look at more lower level tools they
let you use these things but then it's
at your own risk
and then it's likely that you're going
to introduce vulnerabilities
so what I want to showcase today is uh
the addition to Socrates a way to
actually encode this thing and have
um the performance from this thing in
the context of the higher level language
yeah so I have a video now if you could
start the video right so this is using
the actually the Socrates playground so
here I defined the default function
which I call the default function where
I just I'll just use the compiler uh to
generate the constraints for this uh
this expression
here I'm going to create an uh an entry
point for this program
uh so taking also a b and c returning a
u32
and I'm just gonna call the default
function and see how many constraints
are created in the process
so I compile and then I get the result
260 constraints here and now what I'm
going to do is to Define another version
of this function which hopefully will
reduce the number of constraints by
leveraging this lower level
implementation so I call it hand
optimized
has the same signature a b and c
also return a u32
as I described earlier I want to operate
on each individual bit of this year 32
so the first thing I'm going to do is
turning those u32 into an array of
booleans
we have sort of a magic tool in our
standard library to do that which is
called the cast function and which
can do this conversion for you and here
I want to point out that this is
actually free because the u32 type is
actually represented as 32 bits under
the hood so we're not paying any
constraints for this
so just cast the three of them
the next thing I'm going to do is
introduce a new array of booleans
for the result
here one relatively new feature we have
is that everything is immutable by
default so here I have to declare this
variable mutable if I want to be able to
modify it after
okay
so now that I have all the bits I can
start a for Loop
so for I from
0 to 32
and here I'm going to consider the if
bit of a b and c
and if we want to have access to those
low level constraints we need to reason
at the level of field elements so we
need to turn those booleans into field
Elements which is a lower level
representation
for this I call this Bluetooth field
function which I'm going to
Define in a second
I do the same for B and C
and here
I'm going to Define this function and
again this is something that's going to
be free that's not going to create any
constraints for the same reason as
earlier because the Boolean
is actually presented as a field element
at the low level
it's just that it can only be value 0
for false and one for two
so I can just return that using a
ternary expression
okay
so now I have ABC as uh SPL elements
now I have this first constraint which
was uh BC
equals B times C and actually this
constraint I can already Define in in
the high level language because I'm
doing both constraining and assigning VC
so I do that so I have that first
constraint is done then I declare this
result all again mutable
and this is where the interesting new
thing happens I have this assembly block
that I can create and here as I I have
access to and two special kinds of
statements
the first one is going to be just an
assignment so I introduce I just assign
the value
BC minus this other expression to Res
but I did not create any constraints
it's purely just an assignment
so this has no influence on the
constraint system
and then I want to be able to use this
this res value later but to use it I
need to make sure that it's really
constrained in the constraint system
so after this is I did this assignment I
add actually constrained which
which makes sure that everything
is uh is set in stone
so here BC minus res equals this
multiplication you can see that again
this can be any expression here when I
assign but this has to be linear equals
quadratic right so here
this is this is working
okay so now I have everything set up
um and I'm convinced that res has a
result that I need
the next thing that I want to do is that
I actually want to have a Boolean I'm
going to go the other way around and
reconstruct my result but I want to have
a Boolean and I want to go from a field
element to a Boolean and here I want to
make it really clear that this is an
unsafe a potentially unsafe operation
because this res value I know that it's
0 or 1 because I I wrote this but in
theory it could be any value so I need
to be really careful when I do this
um but I can force uh the creation of
this Boolean with this value
finally I reconstruct the u32 value from
the Boolean array
using this cost function again
okay and I changed my entry point to use
the hand optimized version
so we were at 260 and now we're at 164.
so we made uh quite quite a bit uh dent
in our constraint count
so what's the idea here
um
we want to keep all the guarantees that
we have from our higher level language
we have types we have things we know
that booleans can be only zero one if
you don't write assembly blocks but at
the same time we want to have access to
this low level thing and here I think
there's actually a parallel with rust in
a way which says okay we we have a
compiler that's like really strict all
these things but we still want to be
able to do all these lower level things
we want to disable a bunch of checks and
we have a similar approach where as a
developer you would write most of your
program in safe zocots let's say but
then for the few parts that need the
extra performance you can write them in
those ASM blocks and try to make those
blocks as small as possible so that when
you need to review the code or make sure
that things are not unconstrained you
know exactly where to look at and these
things are relatively small
um one side effect of this also for us
as a compiler team is that we can use
this ourselves to reduce the complexity
of the compiler this particular
um operation and the shot 256 algorithm
we in the compiler we have a special
case which detects whenever we're doing
this and uses this exact constraints
but now potentially using assembly
blocks what we can do is rewriting
some of
the internals of the compiler to
actually use these things
which then reduce the size of the
compiler code base and makes it easier
to reason about an audit the next thing
that I want to talk about which is uh
unrelated to this is the fact that
Socrates is not compatible with with
snot JS so snog JS is a JavaScript
library for snorix from the identity
team from the circum team which has a
bunch of tools allowing you to work with
snarks in a JavaScript context
what we have now available today is uh
if you start from your your zocoties
program and you run the compilation
currently
um it returns an output which is the low
level zocchi's representation but you
can also optionally return and Dot r1cs
file which is uh the format that is
accepted by it's not Js
and then if you want to execute your
program you take your input and uh and
the program itself and you can create
a witness file which is also compatible
with with snot Js
and from this point on your Instagram JS
lens so you can do whatever snog JS
enables you to do using different proof
systems uh using a powersoft Tau
ceremony
um
uh and run your verifier in the browser
etc etc
so any tooling that's compatible with
these formats can now be used with
circuses as well
another topic that I wanted to touch on
quickly is the
is incrementally incrementally
verifiable computation so this is a
scary word but it's basically the idea
that if you have a computation
which you can split in steps which are
basically the same function
being run over and over again on the
same on on the state and updating the
state
then you can actually use recursive
snarks to prove this computation
incrementally so as opposed to Socrates
currently to others proof systems where
we can think of them as more like an
Asic so your circuit is like this Asic
that's really set in a stone and you can
do only one computation and everything
is bounded and static in this case you
can have a computation where you run one
round of the computation and then
another one later and you can prove the
execute the execution of that
competition at each step
so some use cases for that are
succinctly verifiable blockchain so
maybe some of you have heard of the Mina
blockchain where basically you use this
to have a a blockchain where each time
you get a new block you
you verify the previous block as well as
the transaction of this block and it
creates a snark and then you have this
kind of recursive verification
another use case is vdfs because some of
the vdfs actually have the structure of
having some state which is then to which
you
um apply a function recursively and then
being able to have a snark of this
computation can be really really useful
so what we're working on now now we're
actually pretty close to having this
ready in production uh is integrating a
um proof system called Nova which does
exactly this and the way that I'm not
going to go too much in detail here but
the way that the API would work for
developers today is that you write a
function and the only
restriction here is that the input needs
to be the type the input type needs to
be the output type because you want the
recursive aspect to to work
and then you can compile this function
to a specific curve so you need to use
this balance curve because under the
hood Nova uses cycles of electric curves
so this doesn't work for any curve but
we support the curves that enable that
and then you can basically prove a
number of steps starting from a given a
given State and even after running this
you could run it again starting from the
last state that you had
this hope this opens a lot of use cases
for people who want to to experiment
with
incrementable incremental verifiable
computation so I invite you to to test
that it's it's going to be out very soon
okay
um since I only have two minutes left
I'll just go very quickly through some
things that we that we added recently so
there's the powers of Tau ceremony so if
you look at gross 16 for example it's it
requires a trusted setup and the powers
of tower ceremony enables you to do that
using NPC
so you can do that directly with this
oxtail CLI and also in the in soccer
says JS actually
we also have support for lock statements
uh that you can where you can inspect
certain values of your code at runtime
we have support for the more input
system that I mentioned earlier which is
a universal setup which means that you
can do one setup and then use it for
different circuits we also change a lot
of the syntax following some feedback
from from members of the community and
finally yeah the this this playground
which is now accessible
which I invite you to to check out okay
I think that's that's all I had to share
uh so thanks for listening if there's
any questions yeah I'm happy to take
questions
um can we use the new Nova support to
write
um another but shorter SDK VM
I think in theory yes I'm not sure it
would be the most efficient
but they were already
actually a long time ago
VMS that were built on top of recursive
snarks but they were using recursion
at each cycle of the CPU which was
quite inefficient but maybe there's a
new take that could be
that you can have on on that so that
would be
one cycle for each op code right that
that's that was the case and those uh
project 10 years ago it's a project
called tiny Ram
where that's what they did they
basically took the state of the CPU and
just run each time one one up code and
then have a recursive snarks a recursive
snark each time but maybe there's other
approaches to leverage this proof system
so instead of making users to write very
optimized code have you put effort on
kind of making the compiler kind of
figure out what the user wants and then
optimize the circuit based on that so
are you saying that okay is your
question
that we should instead of having low
level code have the have the compiler
detect when it can do those
optimizations right I'm in both but like
you will only talk about what the case
right
so this is something that as I mentioned
this is something that we do currently
where we identify some of those use
cases I mean some of those cases and
just have them in the compiler
um but it's just really hard to cover
them to cover them all because it's
really use case dependent uh here this
is just for one part of the shot 256
function but there's so many different
things that you could optimize
um so I think it's actually a good idea
to open that to developers but in a way
that that's quite separated from the
rest of the high level code
[Applause]