[Music]
hi so my name is Jakob Eva Hut and I
work at the information systems
engineering group at T Berlin in Germany
and I'm here today to talk about
Socrates which is a toolbox for CK
snarks on a theorem so let's first look
at how transaction processing works and
traditional blockchain networks as you
can see on the left the transaction is
sent to the network it that then gets
validated at the first node understand
broadcast to the other nodes and at some
point it gets included into some block
after someone solved the proof-of-work
problem now imagine if we had a system
like on the right side where a
transaction is sent to the nodes in a
network but instead of directly being
validated on chain they get forwarded to
a third party the yellow box here and
that's where the transaction processing
happens after the processing off chain
is done the result is written back to
the blockchain
and on chain it is verified to be
correct
only that verification will then happen
redundantly and not the transaction
processing itself so what would be
gained through that one thing will be
scalability if the verification is
cheaper than redoing or executing the
transaction in the first place if you
only have to do the verification on
chain then you can increase throughput
also there is no such thing as a block
cast limit that comes into play here
because there's no need to circumvent
the halting problem a second aspect is
the private information that gets used
on that external node can if we use the
right tools be kept private and
do not have to be published to the
Blackshear network which is also what we
not have at the moment so what our
approach is for that we've heard an
excellent talk by Jason earlier about
Ruben and true--but is one such approach
where you gain scalability by off
training computations and then there's
that verification game played on chain
and with that you gain scalability
another approach is a non-interactive
thorough knowledge crews in that case
you additionally have certain knowledge
that means the private information you
use during your processing on that
external node they are not revealed to
the network okay so what could those
non-interactive sir knowledge proofs b1y
a proven mechanism is ckase narcs I
think many of you are aware of that
technology and it's 10 for zero
knowledge succeed on interactive
arguments of knowledge and here are
several key properties of seek a snark
so the proofs are short and non
interactive that essentially means you
can simply take approve generated by
approvers send it over the network to
verifier and without further
communication it can then be verified
also we have a certain knowledge
property that means some information
that goes into the processing is not
revealed to the network later on
verification cost and that's a big one
is independent of the computational
complexity of the initial computation so
no matter how complex your computation
is the cost of verifying a proof is
always the same ok so that's a key
aspect now a little inconvenience is
that to specify computations in a way
that you can do certain all that proves
on you have to think in an abstraction
that's not very convenient to most
developers so for example you can
specify computations as arithmetic
circuits or rank one constraint systems
of course you can do it but it's just
not convenient to do and
that's what impact usability negatively
let's take a brief look at the process
of using CK's knowledge before we move
on to the tool itself because it's
necessary background so here on the Left
we have a circuit or rank one constraint
system that encodes a computation in
that case we just multiply two numbers
and demand that that equals another
number and for example RSA encryption
uses a different similar construction
from that circuit or rank one constraint
system the first step is a so-called
setup phase which is needed to arrive at
the proving key and a verification key
that are then later on needed in the
proving process so this setup has to be
performed once for a circuit or rank one
constraint system and then it can be
reused over and over again on the right
side here you see the verification
process based on the proving key
approver could for example first find
the solution for the problem at hand and
then generate a proof that it correctly
executed that computation and found a
solution and the cool thing is it could
optionally supply all the information
that went into the processing but it
could also keep some of the information
to itself in that example here the
prover only supplies set which is the
result of the multiplication and not the
factors themselves that went into it and
the verifier can then check the
correctness of the computation without
redoing it and that is much cheaper that
verification process then the proving
process and with that the execution of
the computation itself in the first
place so Curtis so with byzantium
theorem added three new pre composite
enable seek a snark verification on
chain so we have elliptic curve addition
scalar multiplication and so called
parity check but the big question is how
do we use that and that's where it's
okay
comes in so the vision of this toolbox
is to provide a usable abstraction and
tooling to support CKD snarks Ani
theorem to actually make them usable the
goal is to support the complete process
from program code specification to on
chain verification of the execution of
that program code it's supposed to
seamlessly integrate with the theorem
and how it does that we'll see in a
minute
so cretons comprises several things one
is a domain-specific high-level language
that allows you to specify your
computation in a more abstract way than
arithmetic circuits or Anquan constraint
systems which are inconvenient then we
have a compiler which transforms these
programs into provable constraint
systems and then there's support for the
different phases we need to go through
with our CKD Snorks so the setup phase
finding a solution to our constraint
system which is the witness computation
the proof generation itself and then we
can also using the tool export the
solidity smart contract that can then be
used to verify the computation on chain
let's briefly look at the language so
the language at this point is pretty
close to the constraint system but
provides some more convenient
abstractions to specify circuits so the
data type we have is prime field element
you can just think of these as positive
numbers smaller than a huge prime number
so essentially think of it as positive
numbers then we have imparative
statements which is the abstraction most
of you should be used to when
programming we have assertions we have
loops we have conditionals and we have
functions which allow you to structure
your code and keep it a bit less
redundant so let's look at an example
here for answers K or a binomial
coefficient the upper function here
computes the factorial will not look at
that in detail because it's just not
important what's more interesting here
is too low
is the main function as you can see the
main function here takes two arguments N
and K and then there's a return
statement now in Socrates the arguments
of the main function and the value of
the return statement are public that
means when you prove that computation
you use that code to prove the correct
execution execution of that code and K
and the return value become public if
you do not want that to happen if you
want to keep that private that
information you can simply not list it
as arguments but still use the variables
in the processing as we do here and then
when you supply the proof and the inputs
and on K do not appear in there and all
the person verifying the thing would
know is that you computed the binomial
coefficient and what the result was but
NK will not be known let's look at the
user perspective and command-line
interface or purchase provides you so
you start with high level code you write
that high level code and it gets
compiled to a set of conditions were
also called flatten code based on that
you can then find a very valid variable
assignment for that code which is
basically a solution to your program and
that's called a witness so you can use
the tool to find solutions for your
programs and it also supports you with a
setup phase so you can use a tool to
compute a verification key and approving
key which you will need later on
based on the verification key you can
derive a solidity smart contract
deployed to the network and then verify
proves that were generated with the
proving key that came out of the same
set of face and to generate a proof
there's that generate proof ya command
which takes a given witness that you
computed previously and to proving key
and together you generate a proof that
can then be verified by the smartphone
correct you created beforehand the
internal architecture of tool looks like
this so we start with code in that
domain-specific language and that goes
into part powder is then flattened and
then we have an interpreter which
computes solution to the program here
you can decide which part of the
solution will become publicly available
and which part will remain private so
here you have the control and then after
that we do just some format conversions
to yeah to interface with the lip snark
library which we use for the CK snark
operations themselves then there's the
contract Explorer which can be used to
export solidity smart contracts to
verify proofs okay
the on Jam proof verification looks like
this so on the left side here we have
what the circuit is to generated is a
proof it consists of eight elliptic
curve points and inputs on the other
side we have a verification contract
which we also generated and that
contains a verification key seven
elliptic curve point is what that is
made up of and then there's a verify
function which uses the new precompile
that came with Byzantium - yeah check
the validity of the proof and also make
sure that the inputs were correct at the
moment a verification like that costs
around about 1.6 million gasps so
actually a lot that means on a robson
test net we can do four in one block on
the may net it's currently six in one
block the gas cost varies a bit with the
amount of input parameters we
we give with proof but the main cost is
constant and n rather I a couple of
challenges an outlook of how we want to
proceed with circulars what would be
cool in the future so I think for the
language to be more usable more
convenient we would want additional
types so for example boolean types
everything you can do with boolean types
can be done now that's just not as
convenient to do it on prime field
elements and then some integers that
have a binary representation internally
what's very important and that's
basically implementation work ahead of
us is domain-specific library with
important functions so next thing we
need in my opinion is a hash function so
we can do commitments in circuits and
then signature encryption that would be
nice to have also we want to look at
integration of other front ends that can
also be used to arrive at rank one
constraint systems for example Buffett a
generic CK snark challenge that is not
specific to Socrates but rather yeah
always comes up when speaking about the
case Norquist trusted set up phase so if
you supply verification smart contract
and you want to verify something someone
else proves to you and you only want to
be convinced you don't have any problem
you run the setup and you know that you
did it correctly and thus you can trust
approves and you know that the person
proving to you cannot take Bruce because
you were in control of the setup but if
you want to use these proofs to also
convinced third parties other parties
observing these proofs on on the
blockchain then they would have to trust
you with the setup phase so what would
be great if we could eliminate some of
that trust by integrating a distributed
set of phase
it just would have to become a bit more
efficient than it was in C cash
multi-party computation protocol for
example which they employed to do their
trusted set up so I think we'll hear
more about that on Friday in the CK
snark breakout session hopefully okay so
the code is open source it's available
on github you're all welcome to try it
out I'm happy to receive your feedback
keep in mind it's proof of concept and a
research prototype at this place we're
actively developing it and we're always
happy for people who want to contribute
to the further development you can also
contact me by email and I want to give
credits to Christian right Wiesner who
always provided very valuable feedback
and input in discussions and also to
Dennis cüneyt who contributed a lot to
the existing implementation thank you
very much
[Music]