►
From YouTube: A ZoKrates Update by Thibaut Schaeffer | Devcon Bogotá
Description
Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on Swarm, IPFS and more.
https://archive.devcon.org/archive/watch/6/a-zokrates-update/
zkSNARKs are becoming a cornerstone of decentralised technologies. Yet they are often considered impenetrable to newcomers. We will present an update on the ZoKrates toolbox, a set of tools aimed at making developing zkSNARK applications easier using a high-level language instead of handcrafted circuits.
Speaker(s): Thibaut Schaeffer
Skill level: Intermediate
Track: ZKPs: Privacy, Identity, Infrastructure, & More
Keywords: language,zksnark,zokrates
Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/
Devcon is the Ethereum conference for developers, researchers, thinkers, and makers.
Devcon 6 was held in Bogotá, Colombia on Oct 11 - 14, 2022.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/
A
A
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.
A
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
the
kind
of
snarks
that
are
easy
to
verify
today
on
ethereum,
so
you
can
verify
directly
in
your
smart
contracts.
A
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.
A
So
where
does
it
run
so
the
part
of
Socrates
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
in
terms
of
the
schemes,
so
there's
back-end
implementations
that
we
support.
A
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.
A
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.
A
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.
A
A
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.
A
But
if
you
look
at
the
code,
it's
almost
line
for
line
equivalent
to
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.
A
A
Here.
What
we're
doing
is
that
we're
introducing
a
new
variable
res
and
then
constraining
it
with
this
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.
A
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.
A
A
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.
A
A
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.
A
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.
A
Okay,
so
now
I
have
ABC
as
SPL
elements
now
I
have
this
first
constraint,
which
was
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.
A
A
A
A
A
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.
A
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
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.
A
The
next
thing
that
I
want
to
talk
about
which
is
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,
if
you
start
from
your
your
zocoties
program,
and
you
run
the
compilation.
A
And
then,
if
you
want
to
execute
your
program,
you
take
your
input
and
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
using
a
powersoft
Tau
ceremony
and
run
your
verifier
in
the
browser,
etc,
etc.
A
A
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.
A
A
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.
A
Another
use
case
is
vdfs,
because
some
of
the
vdfs
actually
have
the
structure
of
having
some
state,
which
is
then
to
which
you
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,
is
integrating
a
proof
system
called
Nova
which
does
exactly
this
and
the
way
that
I'm
not
going
to
go
too
much
in
detail
here.
A
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.
A
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.
A
A
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
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.
A
A
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.
A
That's
that
was
the
case
and
those
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.