[Applause]
a bankrupt 4G I think very much for the
introduction who of you knows what
Socrates is roughly so just that we kind
of just okay and then we can do a quick
intro I guess and spend a bit more time
on on the later slides of the
presentation
in order
so something started as my research
project basically at to you Berlin but
by now we're happy to develop it as part
of the serum foundation team as three
people at the moment we're looking into
growth so in the end you're free to to
get in touch
let's start with introduction vision
before we dive into more so the plan of
today's talk is basically three things
first we provide a bit of an
introduction back from those that are
not that familiar with the tool but we
keep it short and we'll give you a bit
of an update on what's been happening in
the last year so basically a dev update
those new features we have where we were
going and then we look at some use cases
so we report back from actual
applications
that's that include improved on their
privacy properties by leveraging
Socrates bases in case marks and as a
last step we'll give you a bit of an
outlook what we think where we should be
going in the next year so Socrates is
basically two things it's a high level
of language for programming CK starts in
and it's a bunch of fooling around all
of that so with Socrates in the language
you can program in an imprinted style as
most programmers are used to some
program and then it provides you tooling
so you can compile that program into an
abstraction that is provable through CK
snarks and then you can use this art
which is cooling to have you program
execute the program
generate to seek a stock truth that
shows you that this execution happened
correctly and it also generates use
among objects solidity contracts that
you can deploy to watching so you can
easily verify statistics Augie theorem
without having to bother with writing
solidity verify as for the specific
secrets are effective
so what are the main goals backs our
face it's basically two things that the
first is enhancing privacy with the
serum we have this platform that's very
general we can do general-purpose
computations it's quite powerful but for
real applications to take off we require
a bit more privacy I think because there
is awareness that all the data put on
the blockchain can remind the news band
in one and that's a showstopper for some
applications and we've seen that later
when we look at the use cases for
Bitcoin we've seen kind of an
improvement through the see cash that
managed to do fully anonymous payment
schemes on top of CK starts and of
course you can't simply do a scheme for
a theorem because the theorems too
generic for that so our approach is to
provide easy to use and convenient
tooling that you can for your specific
application in these theorem contexts
whatever interesting case arts community
to improve your privacy properties and
the second thing is scalability so we're
in the word on the Left right now where
we redundantly process all the
transactions that are submitted to the
blockchain on every node and we would
like in the future and we already do it
in some cases booth to the world and
right where we do not execute complex
things on the blockchain but rather
execute complex things off the block
chains while maintaining privacy because
we do not need to expose all the
information we use in this massive
processing then send the result of that
computation plus prove that tests of
correctness back to blockchain and only
check that as long as the verification
step on chain is cheaper than the native
execution on chain
we'll be able to scale better because of
one plot we can fit more computational
complexity that way so that's the two
main drivers behind why this is
meaningful and why you should heaven
the language itself that we use this or
built as an input to the main specific
language which means that this tailor
mate sufficiently compiled into
abstraction CK starts music sure you can
use a generic programming language like
C or us there's also compilers for that
those many of the data types and the
syntactic constructs they offer yeah
not efficiently translatable into
distinct a snark improvement
abstractions so that's why we kind of
have this DSL to be sure that what to
write is kind of efficient at least it's
Iceland inspired syntax but we borrow
like the best pieces from whatever
language kind of but it's mostly similar
to Python and the thing that makes CK
start programming hard or one of the
things that makes it hard one of the
scary parts our program is this non
determinism which means a call to an
outside component you get some results
and anything that was part of your song
and as you maybe feel this is quite
context is something people do not want
to take care of so Socrates hides away
all this smart specific programming
complexity and hides non determinism
without any loss of extra symmetry or
power and what you can do with it
if you want to check it out thanks to
the guys in the back and good work by
Tebow there is now remix integration off
the tooling so its life on remakes not a
very dangerous version but you can go
play around with it to get a feeling and
you can go through all the steps writing
the program compiling executing
absolutely and also there's going to be
a workshop tomorrow from release and
then go into more details about that and
I will hand over to Tebow from bit of a
deaf update what happened s here right
so the first thing that we focused on or
last month is adding more explicit e to
the syste types well for those of you
who actually use sort is before we have
very basic times that were basically
chill elements which you can think as
integers and we have boolean's but
within we have complex it made it quite
very lowest to my programs so what we
added is a race of multiple dimensions
when it comes to create them with a
given value as well as the spread
operators actually might know from
Jasper to all the languages as well as
slice things against the part of the
right so what I'm gonna see
in the same sort of spirit we added
structures which enable you to create
composite types to represent for example
at point of an entity curve like you're
useful in the context of stars if you
trying to verify a signature inside the
Sun and while the things here we also
have for structures and mutation and
access as you would expect as you have
make other divisions so that's right now
under this series very recently this
these new types and more complex types
bring us even closer to a higher-level
language and that's what this is and it
enables you developers to have code
that's clearer and cleaner
however we don't want to sacrifice
performance in terms of the size of the
circuit that gets generated so in
interviews who can write clear school
code that's okay with this world by a
number of simple yet powerful
maximization steps to program in order
to reduce the size of the program as
much as possible so these optimizations
are the ones you would find in many
programming languages along that
constant propagation which basically
computes as much as possible in your
program at compile time if you have
constants in your program for example
all of this is going to be already
removing old linear constraints those
thoughts are based on quadratic
constraints to all the linear
constraints are substituted so that you
only have to cut right histories and few
other optimizations that we network for
and we even have quite good results in
them on a different and compiler
pipeline we changed from a hand-written
pasta that we were using and the first
version of the practice to a pasta
generator so this is quite internal but
basically the idea is that we used to
have a positive be written by that book
by hands to parse from source code to
the ast and now we have the formal
formal specification of our grammar that
generates a pasta automatically which
actually gave us better performance in
some cases which would signal that our
handwritten pasta was actually that
efficient and also interestingly made it
much more simpler for us to implement
new types that I just described
structures and even rice so we would
totally encourage anyone working on
pregnant which is in the early steps of
the process to use fossil devices
especially using a friend a femoral
contest it was within creativity then
over the course of the past year when we
were
have a simple examples people started
those parts to having more complex
applications we realize that there's a
lot of building blocks that people end
up needing over and over again and that
includes suppose the hash functions the
first thing that people want to do is
Holloway common computer fashion study
is done as well as amended curves so
that we can have elliptic curve
cryptography inside of this table which
is very powerful especially for
scalability schemes so what we did first
was to use sustaining existing other
libraries to import those building
blocks but we we changed our approach
and ended up rewriting all of those
building blocks interpreted itself to
see what it would perform and also to
use our own project so the result of
that is that now as Otis ships with a
standard library which you can import
directly from your source code and use
directly that has those utilities so
some cryptography some utilities to be
packing and unpacking if you wanna go
from bits to etc and we also worked on a
library called my crypto and basically
intuition that is that in the same
library for example I mentioned that we
have a curve cryptography so with the
ticker photography you want to be able
to work for signatures later on however
inside of the stock you're always only
going to verify the signature you're not
going to generate the signatures because
generates a signature look at that
before hitting the stock itself so this
high crypto is our current approach to
this missing component everything that
you can basically do before you install
in this case there is the example of
Hollywood sign message with the ETS a
and then based on on this piece of I
think code you can take output of that
and then feed that into the stock the
stock would verify that the signature
you created is actually valid to finally
we worked on integrating with all
backends so we used to integrate with
only this not which is super specific
limitation of pre-processing stocks we
added support for gamma which is a rust
based Hoover test we use by cash as well
as we've been designing and also
developing integration with something
called Zika interface so maybe some of
you have heard of it it comes from the
seek a proof initiative which is
basically a standard for backends of
reverse proof systems and basically what
this means is that using Socrates it
will soon be possible to integrate with
all the new schemes that came up with
Sibley's
some of you saw long and SuperSonics and
all this is Kingston papa
and we think it would be really really
valuable as you could just write your
program authorities and then would
completely would interoperate with any
of those backends because they always
have the same assumption so now I'm
going to go through much the obligations
that people have been building is of
these I had to actually change the name
okay now we heard a bit more on the
background and in turn changes now we
want to look at what's actually hasn't
been done or is currently being done
with the tooling we provide so first
project is ey nightfall and uni Falls
project for Christian young worldwide
and it's basically a privacy-preserving
implementation of piercing 20 new fc7 21
to open standards on this theorem so
that you can have these tokens in and
use them with complete privacy on e
theorem so we will today not go into
much detail about that because on main
stage tomorrow there's going to be a
talk about the project by the UI for
stem cells and what's interesting to
note though is that was not like us
going to them and telling them please
use it and we'll help you but they
picked it up independently and actually
built it and we didn't really know that
they did it unless they're Indies right
so that was for us cool to see as kind
of a validation that cooling is actually
useful for people and projects are a
little bit something else is a joint
project we did with centrifuge so
centrifuge is a service for financial
documents and it basically means we have
an apartment that two people or a bunch
of people agree on off change its
marching protocol but these documents
financial documents for example invoices
they get anchored on the blockchain and
then it provides a single reference
point everybody can point to right so
that stood of centrifuge model but
having claims that means if there's non
poet unpaid invoice and I have to write
to retrieve that payment that's actually
valid it would be nice to unlock that on
the blockchain right bring that to
theorem as kind of a token to talk
so forget centrifuge wants to be an FTEs
that kind of tokenized acclaim to
retrieve the payment I party in the
future and of course what's important is
credit rating of that counterparty
because it kind of gives you an estimate
of your expected value that you will be
able to retrieve after you can purchase
that program okay so they built this but
the problem is to minted entities in the
correct way to make sure that you need
to expose the value of the invoice which
can be initiatives sometimes and you
also need to expose the buyers
identities or the counterparties
identity so you will know whether yes
with credit rating or not and otherwise
you're not going to buy the circuit
right so nice idea but it's not really
gonna wear it out because this
information is quite sensitive so with
the Socrates based approach we were able
to replace these checks by using C kiss
arms and now the only information that's
exposed fermenting Emma teases the token
amount and it's guaranteed to be smaller
than an invoice amount that allows you
to also set up an invoice into several
NF T's and the counterparties credit
rating so you can only learn the key
fact that you're kind of talking that
you're buying a claim for basically is
credit worthy but you do not learn who
exactly it is and that's that's key in
the protocol how it works is that we
basically replace a traditional NFT
registry that does these checks on the
blockchain through a Socrates program
and then Socrates program does all these
checks as part of the C case mark and
after it did that hit generate you
generate two CK's not proof submitted to
a non chained token registry and that
munching token registry density checks
is proof correct or is proved not
correct and if successful the token is
mentioned and only is that information I
mentioned before and some
just to make sure the right data was
news are exposed in the process so
that's quite nice the implementation the
core part of the code I mean there's
some utility functions and stuff is 80
lines of Socrates core DSL code and you
can find it here on get up and
verification cost was 900 K gas for the
prototypical implementation that was
done which was not highly optimized I
mean there could have been for example
we could have used Peters and
commitments instead of sha and slight
details that will bring down the cost of
proving for example and the verification
cost will probably be around about 300 K
which is not too bad
after Kista moon half for improving time
in that an optimized version was two and
a half minutes so totally practical and
auto consumer that father's very happy
really initially right okay I'm also
gonna quickly go through another project
that I personally worked on as part of
the project at to Berlin in this is
Socrates as well and the problem is that
currently the energy system and East
Germany and most other countries kind of
works like this households are in the
network and there's a electric utility
right and some households they produce
more energy than it consumes because
they have solar solar panels on their
roofs for examples and others consume
more these
and the other households they consume
more Dana prefers buts problem is
everything goes through that electric
utility and I'm forced to make a profit
from the right they make a market they
give me a small to give you little money
for the energy they buy and they resell
it at a higher price and then there's
tax effects and other tax white could be
beneficial to not do it that way
so what we propose how you would do it
we try to do as much in turn me in the
network but we do not do it
one market base where you fit it and ask
which is super expensive and has many
problems but we are on the same we look
back in time after everybody produce or
consume the energy and then we basically
make the matching and match the produced
energy by households with consumed
energy by household and kind of
minimized the amount of energy that ever
goes through that electric utility and
that takes away their their profit and
makes it more profitable for households
to have solar panels installed because a
big issue that in many cases is
unprofitable it's kind of bad for moving
on to radial directions run on it but
meaning okay so that's the idea and the
core problem is we do not trust the
utility with doing this allocation
algorithm this matching right so we want
this to be in a blockchain because then
is untrusted but that means hustles
publish their energy consumption data
and the blockchain that computes to
magic but publishing that beta is really
bad right because then everybody can see
how much energy is could compute used by
everybody or produced by anybody this is
highly sensitive data so we cannot do
that that's why would introduced a
Socrates base TK snark
then does that matching algorithm and
the blockchain only verifies that match
in line with some specific requirements
it's fair and correct the same amount
like yeah the amounts work out it puts
up with or equal all that kind of stuff
okay
sneak peek in the future in one minute
so we've been moving very fast we've
been breaking things we've been changing
specs implementation has been
progressing rapidly and now I think we
need to slow that down a little bit
we need to come to version that staples
and users can actually rely on
subversion start building with it
without us breaking it again and again
through disruptive changes and it would
also allow us to do further
optimizations to code base and crucially
for people that want to use in
production get some audit get
potentially some form of verification on
the optimization steps we do and stuff
like that so that's our plan for the
next year to slow down with it with the
breaking changes and to move to a more
stable release hopefully if you're
interested in the rest another than
programming language and state of
geography we're looking to throw the
team so please get in touch and thank
you very much for your attention
[Applause]