I think this works perfect thank you
okay so we have about an hour and a half
um and the content here is one workshop
for about 50 minutes and then we'll have
three Li in talks from my co-hosts Arno
ahmmad aush Gupta and Kevin quack um I
hope we're going to be able to figure
this one out because otherwise it's
going to be really awkward you guys will
all have to like sit next to me show you
the screen
so um what we'll talk about today is you
might have seen from Branch presentation
you know the the last talk during the
CLS gup was talking about how um our
mental model has evolved over time as
we've been working on different projects
and one of the big update that happened
about a year ago was um making this
concept of PCD a bit more usable using
pods and GBC so the tickets you have for
con the frogs you have for Devcon
they're all pods you can operate on pods
via these cryptographic machineries
called GPC and this summer we started
kind of like being getting a bit
frustrated with b and GPC because it
felt like they were powerful yet brittle
and not expressive enough so what we've
been working through um over the last
four months is an upgrade to that system
and there's a lot of like interesting
challenges that that we have had to
solve so what I'll go through today is
is kind of talking about how that
happened and then we'll do a bunch of
live coding um that always goes well uh
and then afterwards we'll have our no
and aad talk about the circuits that we
had to write the zero know circuits that
we had to write to make this new PL two
system work then a US CTA will come and
talk about ZK email um which is a way to
import emails which actually are
cryptographically signed in a way we can
make use of them and it fits very
philosophically with with the rest to
the system finally we'll have Kevin quar
come and talk about how we build the
Cyber frog these little chips you might
have used that are framed throughout the
conference where you can get some rare
frogs from so today it's all about pods
pod one pod two things that are
philosophically pods that we don't call
pods yet it's the Pod
Singularity so uh that's the agenda uh
and the workshop I will go through is
has three part the first one is I will
reuse some of the slides from the talk I
gave on Wednesday
um if this is boring because you've seen
it already just boo me and we we'll go
faster also because this is a small
classroom one affordance we have is feel
free to stop me at any time we're not
actually going to do set time Q&A if you
have a question just raise your hand um
one of
the the AV people will bring you a a mic
and we can go through the question um so
I'll go through some of these slides
then I'll pull up uh my trusty PEX PEX
is a Lis repple that we built that you
can use to make pods and modify them Etc
so we'll do some live codings and if we
have enough time I want to show you how
the greater than logical operation in
pod is implemented across the whole code
base to kind of see like what it entails
to to add more to this
logic okay
so to motivate this a little bit our
thesis at Park is that programmable
cryptography enables this thing we call
the universal data adapter almost like a
turing machine moment for data so just
like we've had electronic circuits for a
long time but it took like the correct
mental model to squeeze the most out of
them by think of them as like this like
abstract machine you can program
similarly we've had data for a long time
but it seems like we still haven't found
the right abstraction to make data more
than dead bits that are hard to
interpret outside of the context they
were created in um and what what we
don't claim we have we have reached the
tring machine moment for data this is
what we aspire to and another another
goal here is to get more out of data we
are in a world that where data gets more
and more valuable yet at the same time
data gets locked up more and more into
these data prisons where like people
want to protect the data at the expense
of getting less out of it one one idea
I've been talking about uh with people
at Devcon
is Google at least Google search is
making use of all of Public's data for
multiple people you know like what they
gave you is like bundling a database
with with a bunch of data about the
world that you can query Dropbox is
about private data for yourself right so
if we do draw the 2x two mckeny Matrix
is there all of private data for
everybody and of course that seems a
little bit silly at first but I would
like to have a system that I can ask hey
how many espressos did people drink
yesterday and we for sure know that like
we we have like a pretty good appr
approximation of this across all the
sqlite databases in the world but it's
really hard to be able to ask that
question because data has these like
contradictory push and pull where you're
trying to secure it which like makes it
se you can make like you can you can
extract less value out of it and at the
same time the way to extract more value
out of data is to kind of like
centralize them in one place which
brings a whole share of problem so yeah
we want to take data out of their data
prison we want to enable more
interoperability and usage of data um
and in doing that breakdown
silos um and one more thing I'll say
here is that we want to be able to
enable a pragmatic route towards data
ownership in the world where data keeps
increasing in value and that is very per
ious because if data keeps increasing in
value yet holding your data means your
data does not create any value at all
the incentive to to hold your own data
just keeps decreasing over time you know
so we want to be able to like get out of
that Loop um so that's the system we've
built over the last year pod and GPC
pods are packets of data that are
specially issued so they need to be
issued in specific ways and then GPC are
cryptographic machines that can ingest
pods and make claims about them using
zkps so claims like hey the entry killed
age in this pod is over a certain number
or my frog is more beautiful than your
frog or that kind of stuff these are the
kind of claims you can make with GPC um
and it's great because it's quite
flexible yet performant enough to run on
mobile browsers and it's about
production ready but um oh yeah and all
of you are using it because your tickets
and your frogs are all pods in GPC so
the T how the system works is an
authority comes together ATT test to
some data via an EDS job job signature
they get a pod you put a bunch of PODS
together into a GPC and you get a GPC
claim and you can show that to a
verifier and convince them of something
so the way it looks like is you sign
some data you get some serialized key
value data here we will take the date of
birth as a specific entry will will will
Trace through this whole computation um
then you can construct a GPC config that
says hey I'm looking for a pod called ID
card with an entry called datea of birth
and I want to make a claim that it's in
this range and on top of that there's Al
an entry called card holder which won't
be revealed and I want this to match a
private key I will put inside this GPC
that makes it such that other people
cannot use your pods and then out of
that you get a bunch of stuff that you
can plug back into a function to verify
the claim and you get a booing value out
that's basically how pod one and GPC
work it's great because it enables this
architecture there which I mean is kind
of General it's it's pretty General most
ID systems actually today use that that
that kind of like architecture where
there's an issue that issues some some
data to a client and the client will
make claims to a verifier and verifier
can verify these claims okay so and and
on top of that it's extremely performant
and you don't need new zero n
circuits um and as I said earlier during
the summer of 2024 we got we wanted more
out of our systems um and the reason we
want more out of our system which I
remind you is this is that well first
the first limitation is this system
needs specifically issued data so you
need to go and like get people to issue
data in a specific way which I mean if
you think about it it's not going to
happen second is it's limited to one
round of computation U and a lot of the
time use cases of data needs more than
one round of transformation you know one
round of transformation is useful but it
would be great if we could keep
executing more programs on top of our
data and maintain the cryptographic
integrity and also it's limited to
single prer use cases what I mean by
that
is while the GPC can hide things from
the pods that were put into it um the
person executing the GPC actually has to
know about all the parts that flow into
this GPC so if I don't know me and my
friend are trying to figure out which
frog is the most beautiful I have to
give the Pod to my friend or my friend
has to give me their pod so it it it
starts becoming a little bit tricky when
you have multiple people in high stake
data um the world today has lots of
cryptographic data yet it's very
heterogeneous so every anything from
blockchains to email to TLS to national
ID systems they're all enry like Cog
graphic data yet formatted in very
different ways with different signature
systems
Etc the basic use cases often require
more than two rounds of transformation
and potentially a whole world might open
up if we can have data flow through
different aggregor aggregators and
different Services yet not lose their
integrity like today most of the time
all of the data falls into like a big
Silo and then gets processed and
consumed out of that it's very rare for
like two silos to ping pong data between
each other that's not that that's not
where the things goes usually and um the
sad thing is there's a lot of works on
domain specific systems out there for
processing all that kind of
cryptographic data yet zero
interoperability between them uh and
what ends up usually happening is
companies or open source groups build a
specific import as an example for email
data or for TAS data and build an entire
ecosystem on top for consuming that
piece of data as opposed to having these
these packets be able to flow through
like with each other so one way to think
about the unlock of cryptography is that
zero Lun proofs enable trustless
refactoring and import so you can import
cryptographic data refactor it Etc
without losing its Integrity um and the
unlock of more interactive technology
like FH coar MPCs that you can combine
data confidentially across many people
so where we want to get to is is this
kind of like verifiable and
interoperable computational graph we
import cryptographic data we compute
over it uh AV people can you be a bit
quieter excuse me hey guys
guys quiet it's a
classroom so you can import data compute
over it recursively and then export it
to a verifier
so we think this address the limitations
of the AIT system if we can get there
because as I said earlier there's a lot
of cryptographic data in the world yet
it needs to be transformed to be usable
um most use cases require multiple
people to compute together most of the
time recursively over many steps of
transformation okay so that's it now you
know why you're here
we're trying to solve this problem um so
in order to do that we had to solve a
couple problem the first one is the
program composability problem what I
mean by that is that let's say you have
a group of like a bunch of friends and
all of these friends issue you a piece
of cryptographic data um so it's like an
array of of of packets you put this
array of packet in a function that
counts how many best friend you have
imagine that the friend packet as a as a
value called is best you get 13 out of
that then you want to operate on this
further as an example a different person
or a different company wants to operate
on top of this result that you got and
they have a function called is grade
friend groups which test how many best
friends you have and if you have more
than three or or three you consider to
have a great friend group it's a pretty
basic example of data that flows through
multiple uh multiple programs so
abstractly would look like this you have
a bunch of PODS that come in they go
through a program you get another pod
you go through yet another program and
you get your final pod so the trick the
tricky thing here is is in order to
implement this you need the second
program to understand the first program
right if I were to tell you like
42 42 is the output of my program unless
you know what program I executed this
data type does not mean anything to you
at all like data type out of its context
is basically kind of useless you can add
things like schemas Etc but it becomes
very brittle very quickly it's really
hard to compose programs on top of each
other so let's say these two programs
are built by different people at
different point of in time there's one
solution to this which is like every
time a program consumes data from a
different program you hardcode the fact
that hey I know this out program behaves
this way I'm going to interpret the
output in a in that specific way if you
want to do it just in time or like
dynamically you need to start going into
um systems that are pretty hard to work
without human interventions things like
static analysis formal proofs Etc and we
know from the halting problem theorem
that in the limit uh it's really hard
it's basically uncomputable for a
program to analyze another program or at
least for some kind of properties so the
approach we've taken there is to
essentially throw away the CPU model and
go towards logic so what I mean by this
is instead of as an example executing up
code in in a virtual risk 5 CPU ASM CPU
we execute logical operations logical
deductions um so you would have
something like a logic virtual machine
where you replace memory slots with
logical statements so instead of this
piece of data is at this slot in memory
it's like there is is a statement that
says uh there exist an a such that a
implies whatever um that kind of logical
statements you replace up code with
logical operations or deductions so
here's a deduction as an example if a is
smaller than b you can deduce that a is
not equal b or if a is defined as 10 and
B is defined as 10 you can deduce a
equals B data becomes theorems uh
programs become proofs so mathematical
proofs and your system looks like this
where you have some pieces of data that
exist that they' been attested to you
treat them as axioms and then through
logical proofs you produce theorems that
they themselves produce new theorems Etc
the reason why this works in theory is
that math is built to be interoperable I
can give you a theorem if you believe
that theorem has been proven you can
prove more things using my theorem or my
LMA it's very much different from the
story with programs and computation in
general so now if we take back this
example I gave um the way you would turn
this into is you have the blue theorem
which is Justin has 13 best friends and
you want to get to the green theorem
which is Justin is a great friend group
and so if you write this down in plain
English you would have something like I
have 12 best friends implies I have more
than three best friends um so now you
get to a system with two kinds of proof
formal proofs and zero knowledge proofs
the zero knowledge proofs are used to
both show that the formal proofs were
executed correctly but also as a way to
remove specific inputs to the formal
proof as an example if I Constructor
formal proof that shows that my age is
over 21 I may want to remove the axium
that says what my age is
while you can still audit the audit
trail of this axom in the first place so
this is all a little bit abstract that's
why we'll do coding after this and we'll
see it either break or succeed in front
of our eyes so the great thing with this
is that you can kind of compute theorems
on top of theorems on top of theorems at
least if we build the system correctly
and as an example I will show you a
little bit how a very early version of a
system works so this is the list of
logical statements that can exist in a
piece of data this is the most basic one
which is the value of a key is a scalar
or a vector of scaler this is basically
what you usually have when you have data
which is the value of AG is 26 or the
value of I don't know something else is
this list of numbers but then on top of
that we have other kind of logical
statement so as an example we have an
equal statement that says well this key
equals that key this seems a little bit
silly because if you see the two keys
well you can derve they close to each
other but what if one of the keys not
there anymore right and it's using yet
different statements um here's a turnar
statements which ISS that the sum of
these two Keys equals the third key
right so you you have to think in terms
of logic and not in terms of computation
anymore here's a a list of operation so
operations remember there are deductions
that are applied to statements to
compute new statements so as an example
the equality from entry statement takes
two value of statements and then it
checks the entries within the value of
statements and if the entries are indeed
equal it produces a new logical
statement that says the two values the
two entries are equal easy right um so
from from a cryptography perspective
what we had to do is instead of writing
a z zkm that has circuits proving the
state transition of a CPU architecture
like Risk five or wasm or whatever we
build a virtual machine that a circuits
proving The Logical operation on
statements is done correctly um it's a
cryptographically verified theor
improver if you want so this all seems
again like very abstract why did you
guys go all the way there to show that
your age is over 18 or something like
that well the reason is you can it's
very neat because when you get this to
work you can wrap it up with a
programming language that looks like
what people expect but under the hood
operates on logical operations so you
can make the user experience of using
this pretty decent but at the same time
now you get pretty good composability at
the program level as opposed to having
these programs that output data types
that you didn't have to compute over
without really knowing what the the
previous program did okay um I'll go
through this a bit bit faster because
this is not really the point of this
Workshop but another challenge we wanted
to solve is this challenge of imports so
we want to turn verifiable data into
value of statements and we're we're
happy having some value of statements
have special meaning so as an example uh
if you were to import an email we are
okay having some keys that says
underscore from underscore 2core
timestamp and these are not entries that
can be set by the content of the email
these are entries that come from
metadata about the email the great
things with importing everything as
value of statements is that all of our
Machinery that op operates on entries
can be used to operate on things like
public Keys like who sent the email Etc
um so as example if I want to compute
with one of my frog frogs are pod ones
in some ways they're foreign
cryptographic data from the perspective
of the Pod two system they're on
different curves different signing
algorithms different merization and so
what we have to do is we have to build
what we call an introduction gadget for
this paa one so you you would write a a
circuit that would verify that the
signature of the spot is correct it
would store the signer into a value of
statement with Kore signer and it would
copy each but entry into an equivalent
value of entry and then you can take two
frogs you can import them and then you
can put together a statement that says
Todd is more beautiful than the mustache
frog so if you go through all of this
this is the kind of stuff you can
do so we want to be able to import all
kinds of stuff whether it's um data from
the web data from blockchains data from
Virtual Worlds um even mathematical
proofs themselves and in order to do
that um well we also have to make it not
too hard to use this system uh if we go
back to the place where you need to be a
cryptographer and an expert in logic in
order to use this we've regressed so
it's really important this thing is not
extremely difficult to use so this is
what the Assembly of our system look
like it's a bunch of uh operations don't
ask me why we use strings you can ask
Ahmad you will no I'm joking Ahmad has
been trying to remove the strings from
the system um and so what you have to do
as a user of the system is you basically
have to craft a sequence of logical up
codes to make new pods and also when you
get a pod out you have to read The
Logical statements and make sure they
actually claim what you want to to
verify so this is pretty hard to work
with so what we did is we built this
this little logic programming language
to create pods and verify them it's
currently a list because it's the only
kind of programming language you can
write in two weeks but we'll we we could
have other things in the future and it's
great because it do an interactive
development Loop so it's it's easy to
play with it um so instead of showing
you an example of PEX I'm just going to
like do it live so uh pray for me cool
so um actually I have a note here of you
can do this with me if you want but no
guarantee that this will work on your
computer so if it doesn't don't complain
um if you go on get up.com zxp parkpark
net and you have cargo nightly
specifically this version uh take a
picture of it um you can run cargo build
in a Pex crate and cargo run-- release
the D- release is important otherwise
everything is going to take like 5 hours
um and you can follow along if it breaks
please don't tell me but it doesn't work
because I won't be able to fix it on
your computer instead you just start
watching but for some of you it will
work I know for a fact that on Linux
it's really hard to get it working uh
Ahmad has been trying to put together a
PR because there's a dependency on open
SSL don't ask me why we have a
dependency on open SSL that doesn't work
but on Mac it should work and on Windows
same thing I don't know I mean uh my
friend here Alex got it working on
Windows as well so so we can look later
okay so I will put the mic back
because I need both of my hands to type
super fast all
right um so I will go just like you in
the PEX crate and I will just run the
system in release okay so
oh okay so what this does so you might
notice there is a little statement that
says Ripple synchronize with other peers
the fun thing with this lisp is it's
actually a multiplayer Lis so when you
boot up a reppel you actually connected
to all the people that use the reel as
well so we can do operations on our pods
Etc uh we'll try to get it working here
but it's it's not that important the
second thing that takes a while is we
don't we recreate the parameters of our
circuits and the verification key every
time we boot it up because we don't want
to serialize them on dis yet because we
changed them all the time so um I'm in
the rapple you can see I have a public
key I have a little username my username
is pulser Voyager and so what I can do
with this repple is I can create pods I
can either create pods out of nothing uh
if you remember my slides it's like
importing a pod but because we don't
have any good importing system yet for
existing cryptographic data the way I'm
going to import pods I'm just going to
self sign them but you could imagine
that if you were to import a pod as well
and you gave me your username we would
be able to compute on top of each
other's pod what I can do as well is I
can create pods from previous pods which
is really the key of the system so um
let's make a pod so also this language
and also the logic only support numbers
and list of numbers so there are many
things I would like to show that don't
use numbers and use different kind of
things so you will see some of my
examples are a little bit contrived but
it's it's because we have to work with
what we have so um can can people show
hands if they have read the list syntax
before or something similar so I can see
whether I have to spend a lot of time on
this okay so one thing to know about
lisp is that um it's a very simple kind
of programming language it's really easy
to parse the way it works is every every
time you see brackets you try to find
the closing bracket for this and you
have to imagine in your head that the
computer is going to turn this into the
result of that computation so as an
example if I do plus one two it uses the
infix notation instead of sorry the
prefix notation instead of infix
notation this means the computation I'm
executing is plus and it's over one and
two so this is going to turn
into three see I get scale or three and
if I want to do different things with
different orders I can keep putting
bracket so as an example if I do uh plus
3 4 what's going to happen here is three
and four are going to be summed first
and then it's going to be summed with
one so we're going to get eight out of
that right so if you don't understand
the syntax at any moment tell me and
I'll I'll explain you how it works but
it's not as scary as it seems and the
reason why we wrote a list once again is
because it's really easy to write a list
parser and Lexar and interpreter whereas
it's really hard to write a parser Lexar
and interpreter for imperative languages
um um okay so let's make some pod the
first pod I'm going to make is almost
like an ID card for myself so what's
what's this ID card going to have and
remember we can only use numbers so
first I have some form of like national
ID it's kind of like my user ID in the
system um I might have an age on it I
know that the proper way to do this
would be date of birth but we'll skip
that so I'm 26 and also in my in my ID
card I have the ZIP Code 11 I've never
used zip code this much in my life by
the way zip codes are great because
they're also a number thing about you in
the most other things okay so I press
enter here and I get a pod and you'll
notice that uh we get like useful
debugging window here that tells that
tells us the type of our pod that is the
cryptographic Machinery you have to use
to verify the Pod is schnor 16 so schnor
is a signing algorithm so this is a self
sign pod that I just made about myself
and inside we have a bunch of logical
statements all of these statements have
value of statements so they just make a
claim about an entry in the system in
this specific pod so you'll see that it
claims that my age is 26 my ID is the
number I typed and my zip code is 121
and on top of that we have another value
of statement that has been added
automatically that I did not set and
that in fact I cannot set because it
starts with an under score which is the
public key that signed this pod um it's
the same here so you'll notice that as
an example for this pod the public key
which is an important value in order to
Anchor that piece of information to
reality is something we can can operate
on the same way we can operate on other
kinds of data public keys are not
special in the system they're just
data cool okay so let's make another pod
and this aod is going to be a past tub
uh so this past Tu it's issued by
someone else ideally I would be able to
change my private key in the reple I
can't and also if I exit the reple it
deletes all my pods so we're in this
very annoying system where the past up
is going to be signed by the same
Authority but could be signed by a
different one doesn't have to be signed
by the same Pro key
so I have a salary um let's say 120,000
units um this B stop is linked to an ID
of someone using any kind of ID system
and that's it so now I have another pod
same same deal we have some value of
statements um same there's a signer okay
so now what I want to do if we go back
to this computational graph um let me
bring it up
here I have two pods let's say pod red
and P pod green which are pods they have
been issued by different like people one
is my ID card maybe it was imported from
whatever horrible format the government
uses to make ID ID cards be
cryptographically verified and then the
other one is a past up and imagine
that's been imported using uh the ZK
email system that aush is going to tell
us about later where it parsed my
pasteup email from let's say like Gusto
or your payroll system now I have these
two pods I want to make a new part out
of it and what this new pod is is just
says um I want to do a draw on all of my
data which say like the ID my my ID has
this much annual salary with this ZIP
code right let's try to do that so what
I need to do is I need to take two pods
and need put them into one pod and also
need to create some logical statements
that kind of like makes everything fit
together and it will make more sense as
I read it so we're going to create a new
pod um actually let's do like an an even
more interesting example which is not
only do I want to show that I have a
specific salary I actually don't want to
reveal the amount of salary I just want
to show it's over a certain amount right
so we'll do salary over amount that's
the name of our pod so first here what
we'll do is we're going to query for
pods within this pod and the thing
that's important to know about what I'm
going to do is that the quer is
approvable so the way I express my query
using this query language gets turned
into a bunch of stuff within the logic
VM that shows I've done this query
correctly
which is but also that it Imports a
bunch of statements from previous part
such that a verifier down the line can
be like okay they truly imported a real
ID not something that they're like
little brother signed or something like
that so um on top of that we're going to
use a new piece of syntax which is
defined because as a quer a pod I'm
going to get bindings to values in the
Pod and I want to reuse them so I will
bind them to variables because you you
might have noticed in lists there are no
real variables by default you just
compute so here we'll need some some
variable like stuff otherwise it's going
to get really gnarly so first we're
going to query for things in my ID card
pod so we'll say okay so ID card ID H
zip code these are the names of the
variables I want to bind the outcome of
my PO query to and we'll use this
statement called pot question mark and
so what follows pot question mark is a
it's a query language so what we'll do
here with the query language is we're
going to be very open we're just going
to say hey I want a pod that as an ID
that as an age
that is a zip
code and whose signer is equal to a
specific
value okay so what I'm doing here is
what this query does is it asks for a
pod with these three things and also it
adds a constraint for the signer this
constraint currently it's a PL text
constraint so what this means it's not
actually verified I'll have to do
something with the signer later such
that like this this query cannot
actually be cheated later so we'll we'll
get a binder to this as well ID signer
let's do it this
way
okay um one thing you might notice is I
cannot explicitly pass pods into other
pods I can only query for pods the
reason we've made this decision to only
allowing for pods to be queried is
because if you query for a pod the query
should include everything that's
necessary for this pod to be then like
used as a legitimate entry so if a query
were to return multiple pods they should
be
equivalent because if they're not
equivalent from the perspective of the
verifier that that means your query is
not like tight enough uh this is an
aspirational goal maybe we'll have to
change that uh but for now this is how
it works so we'll do another defined um
where we're going to get binding store
pay stubs so we'll have salary salary
and then past up
ID same deal here
salary ID and then I also need
also if anything doesn't make sense feel
free to interrupt me and ask me
questions because it's only going to get
crazier from here uh cool okay so now I
have all of these little variables right
if the query succeed that is what am I
going to do with these things well the
first thing is um I want things to be
revealed in this part right what I'll
asample what I revealed is I reveal my
ZIP code so I'll say zip code remember
the syntax is key value key value key
value so I say there will be a a key
called zip code and the value will be
zip code which I got from this spot I'm
querying
here um and then that's the only thing
I'm going to reveal in the clear
everything else I'm going to reveal are
specific constraints that are applied
between these B so the first thing I'm
going to constr is I'm going to say ID
card
ID equals BB ID right because otherwise
that means I'm using either someone
else's PB or someone else's ID card um
then I'm going to make a claim that my
salary is over 100,000
units um another thing I'll do is I'm
going to claim that the ID so okay what
I want to do here is I want to reveal I
want to show that the pods I've been
using are using are from a specific
signer not from like my little brother
or something there are two ways for me
to do this one way is I reveal both
signers another way to do this is I
reveal one signer and I show that it's
equal to the other signer which is
equivalent right so we'll we'll do the
second way because it's more fun so we's
say ID signer equal
Bop
signer and on top of that we will reveal
um the signer which is the
signer okay so are we using everything
we got here so we're using ID card ID oh
and H what should we do with
h over 18 okay let's do
that so I'm going to REM remove this
this closing thing otherwise it's going
to just create the
Pod so age is over 18 quum okay so now
we'll press enter and if the demo God is
on my side this will succeed oh it's
working all right so we just made a zero
proof and we created a new pod what's
inside our new pod well we have a bunch
of logical
statements uh let's read this together
because there's a lot going on so the
first thing you'll
notice is that some entries now are
prefixed or or entries used to not be
prefixed entries that are prefixed are
entries that provably come from other
pods um the the the origin doesn't
really matter like what's written be
behind the column doesn't really matter
the only thing that matters is if it's
written in two places you know that this
entry both of these entry came from the
same pod the reason why it's really
important to have traces of where
entries come from is because you cannot
the point of a pod the reason why a pod
is a list of key value and not just a
single key and a single value is because
there exist in the world values that go
together as an example I can't take my
age and combine it with your name and
make a new person out of that these
entries need to remain logically groups
so that's why we have this so let's read
it together um maybe we we'll do the the
the the easy stuff first so first we
introduced a constant constants don't ex
exist in the system so we just said
100,000 equals 100,000 or at least the
entry named 100,000 as a string equals
100,000 uh We've reveal we have this
entry called zip code code 121 and
notice that if you were just to see this
that doesn't mean that my zip code is
that zip code that just mean that
there's an entrical zip code in the
current pod that has a specific value
there's another constant which says 18
is is 18 and finally there's another
entry in the current pod that says serer
equals this public key so if you were to
just see these these four blue values
that wouldn't really prove anything that
just says I just made a pod with a bunch
of entries in them what matters now is
the relationship between these entries
and previous entries through logical
statements so let's read them from the
top so the top says there's a pod whose
origin ends with 973 and in that pod
there was an entry called age and it's
over
18 there are two pods one that end with
973 the other one that ends with 226
where both of their under SC scanners
were the same the Pod that ends with 226
had a salary entry which is over 100,000
and both pods have the same ID finally
the ZIP code entry in the current pod is
the same as the ZIP code entry in the 73
pod and the signer in the current pod is
the same as the underscore c73 pod so
this EXA basically as a
claim kind of like shows logically what
we've been trying to show so far okay so
I'll stop here because we just did a lot
um if there are questions we can go
through this like many times so let me
know if there are questions here so
far yes can uh can one volunteer bring a
mic oh thanks Arturo
thank
you thanks for the introduction if we
assume that this is the technical
capability what would be an application
M um
so the current technical capabilities
which have to do with importing data are
pretty limited because we're just
signing pods ourselves right so what
this means is this is only useful
currently if just like the pod one
systems people that are use issuing
useful data like the swamp that issues
your frogs issues you Frog as these
schnore 16 pods right so if you could do
that then the way to think about the
system is it's a way to operate on data
and then make further and further
refinement of data and combination of
data in such a way that the data
Integrity is maintained so there's a
couple of things you can do one is um
I'll take the national ID kind of lens
even if it's not my favorite one because
it speaks the most to people which is
that if you expect a data issuer to be
able to answer any kind of question that
someone would want to ask about that
data it's really annoying for them
because they have to do a lot of work
ideally what you want them is to want
them to issue some data and be like now
it's your problem to operate on that
data but at least you cannot make like
false data pretending to be me so as an
example um if so I come from Belgium if
the government of Belgium they're
Europeans so they're further thinking um
they start issuing passport or national
ID card using the schnore 16 pod um now
I can do things like go somewhere and
prove that my age is a specific amount
or I can claim a government benefit
anonymously without being able to claim
it multiple time or I can use that to
sign digital documents or I can kind of
like anything that involves my identity
is just logical statements apply to my
identity as example signing a document
is a pod that says the hash of that
document as an entry and then there is
my I don't know ID number or something
else there provably coming from an ID
card sign but the Belgian government and
the required infrastructure would be
that the government and your employer
both have public Keys yes so so they do
the the government has public Keys your
passport is signed your ID card is
signed so what I'm saying is the current
the current system really sucks right
because you you need people to issue
their own pods where we're trying to get
to and I thought we would get to there
for this demo but we did not it's going
to take us one more week is the first
demo of an introduction Gadget where you
can take existing cryptography data that
is in a totally different format and
import it as a pod and then you can
operate on it so what we were trying to
do but we didn't get enough sleep this
week is to import frogs which are not
nor 16 pods they're different kind of
cryptographic data and then do
operations on our frogs right so as an
example the NFC card in your passport is
signed by the public key of your
government but it's using some garbage
signature scheme it's like a totally
different system so there are people
today that build bespoke systems to
operate on passports what I would like
to do is be able to import a passport as
a part and everything else that consumes
part two and does operation part two can
use it so on the verification side you
do need the person or the company or the
program that is verifying this data to
accept the truth of that data so in some
ways you don't need infrastructure at
the attestation side because we'll just
be able to import it but we do need
infrastructure at the verification side
so I think the way we should start with
this system is we should bring it to
companies not governments that need to
like essentially compute stuff on on top
of official data and instead of them
having to pay like $3 per verification
for something like Persona where they
have to like get the video of you and
your passport being watched by someone
they can just accept the part too right
so of course they would have to make
sure that all this stuff is audited
works correctly but I think the way to
bring this to Market sorry we're going
way out of bound of this Workshop now is
to go to to people that need data from
other sources that needs to be processed
in a way where it's cheaper for them to
do
so and last question building on that
the verifier what does what do they need
the verifier yes they just need a lower
program and then what they they get and
they need the public keys they need
anything that's part of the axiomatic
pod to tie them to reality so it might
be public Keys it might be certificate
Authority it's it's it will depend on
each use case and the resulting Port but
not the input ports no they don't need
the input Parts they don't need the
computational graphs yeah thank you
thank you for your questions
there's a question the front
aruro thanks um so this language is kind
of like a relational algebra the way
that it's yes it's like prologue yeah
and so um when we're saying that we have
the programs now are approvable in the
sense that if you listed the queries and
maybe the lines of evaluation you could
use some rules of inference to say that
these are this computation is done by
rules of inference and not by evaluation
and then when we talk about the zero the
zero knowledge proof you're going to
write a verifier of that algebra and
snark the verifier of this algebra yeah
I just wanted to make sure I understand
the two steps of like because there's
two proofs going on one two proofs yeah
it's kind of like this pi squared
project that I heard about earlier this
week a little bit Yeah they used the K
framework yeah but in the similar way
like they have this front l that's
provable in some other sense of the word
that yeah correct and then I have a
question so lisp is cool because it's
also like homo ionic so lisp is data
code is data and we're just giving
examples that's pretty similar to the
normal data that we're used to looking
at is there a way that you can leverage
this fact that code is also data in in
this framework or that's I mean probably
far out future but yeah so this is a
great question and you will need to do
this when you start doing first and
second order logic cuz you know this
this logic that we have right now is a
bastard propositional logic uh it has
numbers usually propositional L doesn't
have numbers it just has statements
about stuff like it is raining or it is
not raining here we have numbers if you
don't have numbers for the ultra nerds
here you would have to do it in a way
where you define the zero number and
then you define successor and so three
is successor of successor of successor
of zero but then you see how narly it
gets very quickly so we added numbers to
propositional logic if you want to do
first order logic you're going to need
to be able to manipulate statements via
other statements like groups of
statements via other statements and so
the the the semantic of lisp will help
here quite a bit like I I could imagine
how this would be useful but we that's
where we stopped yeah so the lisp is I
mean it's you said it's just a
convenience for defining a language but
actually you might keep it because it's
useful yeah it's possible yes the reason
why I say that is because because people
get spooked out by the lisp like oh this
is amazing but I will never use it
because it's a lisp you know if there
was a space elevator that required you
to write some lisp to go on a bunch of
people would not they be like it's just
too hard that's a good way of putting
it thanks cool uh if anyone keeps like
if you oh more questions let's
[Music]
go thanks for the introduction uh more
on the verification side um the premise
of that is you trust this blob of data
in the pot that is issued by someone
right to be authentic
yeah so here you do not trust these guys
you only trust um these original pods
that were created here yes based on the
public keys right or anything else it
could have been imported from an email
and it would be based on who sent the
email it could come like it's it doesn't
matter it's based on some way of
representing Authority so in the
verification side then does it mean that
it it it it needs some sort of a trusted
Source registry that says that you know
this identifier of this signer is
trustworthy correct but it can be built
on top so you see how you have this pod
here right so if you trust the system
what you trust is these statements have
been done in a way that is sound from a
logical perspective now the way you
would actually trust this pod is you
have to check this number right which is
the public key of both of the pods we we
constructed that logical statement so
the way I'm thinking about the system is
I want to layer in Trust on top of the
logic I don't want to Big trust in the
logic because I want to manipulate
things that are like that are linked to
trust just like I'm manipulating
anything else but you're right that for
this to actually be useful we would
layer it and something else on top So
eventually it would need some sort of
something like a CA certificate like
Authority that kind of I think there
could be many different competing ways
even of doing that some people might use
CA some people might use a blockchain as
a way to register schemas but we don't
want to bundle this with a specific kind
of registy because we think it's a
mistake that is being made by a bunch of
projects out there where they're
building this monolith of like the way
we import data example from passport the
way we verify public key using this
specific blockchain the way we operate
using these specific circuits we want to
unbundle everything whether it's where
the data come from how the competition
got done and where which which registry
of truth of trust is being used yeah all
right thank you very much you're
welcome cool so um how much time do I
have 10 minutes dang okay
um what would be more interesting making
more pods looking in the code base to
show how a specific logical operation
Works something else beatboxing um
anyone has an
opinion code base cool let's look at the
code
base I can't do two things at the same
time I am a single threaded processor I
would have to stop everything to
beatbox um Okay so
cool so this is a file that we have that
list all of the operations that
currently exist in the system it's just
an enom in Rust um one specific entry
here is greater from entries so what
this operation does is it takes two
statements you see S and S what the
statements need to be is they need to be
value of statements so statements that
point to the value of an entry and then
if the entry is Behind These two value
of statements if the first one is bigger
than the second one it will add a new
statement which is something like
greater than we we can check later
so um let's see how that actually
happens
so let's command f for this so okay I
will not show you guys the front end I
will not show you how in the Lis this
gets turned into the specific command
but now you have to kind of like believe
me that this command is called at some
point pointing to the right statement
so first
um one thing I'll show you is how to
evaluate this statement in plain text so
not using cryptography so if we see here
when I have the greater from entries I
destructure um two value of statements
and then the actual entries between them
and then I turn these entries into u64
and if the first one is indeed bigger
than the second one I create a new
statement which is greater than the
first key the second
key so till then this should make sense
right like we're just showing how this
happens in plain text okay
so now how does this happens uh in a
circuit so what we'll do here is first
um in a circuit every single one of
these statements need to be turned into
op codes and these op codes are field
element into the field we're using which
is the goldilock field so the greater
from entries gets thrown into this up
codes up code number five um and then
another thing I will do is it will take
the operant of this statement here it's
S1 and S2 and turn them into a vector of
oper that will be injected in the
circuit as well I think there's one last
thing that oh this is just a way to sort
these statements because they need to be
sorted in a specific way okay so in our
circuit here's what we do so let's go to
the top of our circuit um what the the
top of the circuit does it says there's
a current Builder the Builder is just an
object that you have in the proving
system we use to be able to add new
constraint and there is um a bunch of
statements right and and they targets
so this mumbo jumbo here is a way to be
able to select from the list of entries
we have the entry that corresponds to
the statement um we need to do some like
Matrix kind of like indexing thing so
what we'll do here is
uh we have this op is valid AR right so
the code is still not great Ahad will
tell you how we got there but we'll make
it better but what you have to think to
do here is you have to index you can
imagine so the circuit model is not the
computational model you have to execute
everything all the time and then what
you do is you have selectors that turned
on for what you actually need to check
so what we do in this massive array op
is valid is we basically check the
validity of every single operation that
could happen on the statements that are
currently being selected and when you
turn on the selector for the actual
operation that we're doing the other
ones we don't care about them so the way
this works is the selector for this
array is going to be the op code so
remember the op code of Greater from
entries is up code number four so
uh one0 1 two 3 4 yeah it's currently
the fourth one so when greater form
entries is turned on what actually gets
checked is an end statement on whether
statement the the first statement is is
indeed a value of statement in the
second statement is indeed a value of
statement
so if you read this this doesn't
actually do the greater from entries
right what it does is it just checks
that you're doing the greater than on
actual entries not whether the first one
is greater than the second one so for
reasons obscure that it discovered this
morning and we'll have to ask aad why
it's done this way the way the place
where we actually do this checked is
here so we have the greater than up code
Target and we say hey if the current up
code is indeed the greater than from the
greater from entries up code we do an
assertion that says uh it it that that
something is less than and here the
statement two is less than the statement
one so you'll see this is still a messy
code base but at the end of the day
everything you know the operation that
gots executed at the end of just gets
converted into some some circuit
operation and so you also notice that
it's actually pretty easy to add new
operations right like here we just had
to add like eight or nine lines of code
to add to to add an operation um of
course there are difficulties when you
start having complex data types like
arrays Etc but a lot of the difficulty
in system is to write everything else
that happens on top of these logical up
codes so that you can manipulate them
easily because one one thing we did is
we had this massive we have this massive
test that checks this kind of like web
of trust like computation um and when
you write these up codes yourself it
just takes hours and most of the time
you get it wrong so like a lot of the
the a lot of the smart stuff here that
makes this easy to use comes from The
Logical programming language right and
then the layer on top of course you have
to write the circuits correctly um some
of the circuits here is like pretty
tricky like if you want to show that
that an entry is contained in an array
you can you should do this using like a
Merkle proof as an example to make this
more efficient so so there's a lot of
work here both at the programming
language at the Lo logic level at the
circuit level um so I'll stop here for
questions or for future prompts I think
we have five more minutes before I pass
it off and we can also do maybe a light
Q&A cool okay
done
here yeah this is a good question I
think so as I've been working on so my
my role here was to work on the PEX
language um and what I've discovered is
like every time I want to make more
complicated program I have to make the
program language smarter which is not a
good sign so that means we're probably
doing it in a wrong way so um one
inspiration we have which is still a bit
out of touch with what we're trying to
do is interactive theor imprs so like
IRAs Etc but these are heavily
human assisted and also they're like
very complex Beast so I would rather not
have to write an interactive theor
improver in order to make this useful so
um yeah I've been trying to find in the
literature outside people that have been
writing programs in an imperative way or
or in something that's not like a
theorem prover in a way where you can
turn that into logical operations and
there is some cool stuff out there
there's this programming language called
agda that you can use to make make
proofs about its own correctness um and
it's like not that bad to use it so yeah
there's still a lot of work to do there
on like the right way to express this
one challenge that we have that we set
ourselves to be able to achieve with the
language to then decide if it's the
right way to do it or not is to be able
to construct pods that might uh recurse
like an infinite amount of time so
imagine a kind of pod I would like to
construct which is a pod that shows me
how far away I am from someone so what
this would mean is let's say it's from
how far away is from Alex so Alex is
isues a part to all of his friends where
he has a bunch of logical statments that
says he attested to someone's public key
and then these people can attest to
someone else like me because I don't
actually know Alex directly and I would
like the Pod there to have a number that
says I am two degrees away from Alex and
I want to be able to like do it for
someone else and be 3 degrees for Alex
so there's a trivial way to do this
where the size of the pods in terms of
how many logical statements it has
increases linearly with the distance
from Alex we would like to do this in a
way where the number of statements does
not increase linearly by having more
powerful logic where we can count using
probably first order logic or something
else like that and also where the script
the PEC script that we write for this is
the same for every degree of separation
because currently the way you would do
it with the current PEX you would have
to write different scripts for each
degree of separation so if we can do
that in a way where it's constant size
script and constant side logic uh we
would be pretty happy if we cannot do
that then we'll have to revisit our
approach cool cool and I I'll I I'll
close it here um now we're going to have
a talk so everybody wake up uh different
person different style we're gonna have
a talk from Arno and Ahmad about the
circuits and how they were put together
so here I showed you guys the easy part
which was ex putting the operations
together the really hard part of this
was making this system like basically
infinitely recursive where you can
ingest multiple pods some snor pods some
frony pods in a way you can keep
recursing and that was pretty tricky to
do correctly so that will be the the
next speakers you guys want to come on
stage
thank
[Applause]
you and while we prepare if anyone has
more questions I can answer them I'll
just take the
mic hey yesly uh so some uh talk about K
and the matching logic over there so
hard would be to plug the result of the
K execution so the magic logic over
there into pods um yeah I think so we
spent a bunch of time looking at K uh
even writing some like little K
definitions ourselves for like toy
languages um I think the way we're
thinking about this is we really want to
figure out like what's the right tool
for the job you know because we were
thinking about like oh should we just
like write a Z proof for like the
the improver or something like that and
there's been a bunch of work there from
like students of Dan Bonet as an example
but these proofs are incredibly
expensive and really hard to put
together I don't know what are numbers
yet for something like K I don't know if
you guys are writing proofs yourself or
using something like a zkm but it's
probably very expensive um like the pods
we put together here they take like two
seconds on a on a laptop so that's
pretty neat but in some ways what I
would like is it would like I one thing
that would be really cool is to be able
to dynamically size the complexity of
the logic based on the claims you're
trying to make and use less powerful
kinds of logic that are faster to prove
or more powerful kinds of logic that are
more expensive to prove that would be a
really cool system whereas an example
you could tap into K if you want to make
like really complex proves and very
powerful proves but if you just want to
show your age is over 18 you can just
like make that pod yourself in like 30
millisecond on a on a phone or something
like that but I would be interested to
look more into it are you working at pi
squared awesome yes okay cool yeah so
you're the guys that like prove the K
framework execution right yeah yeah we
can chat about this all right thank you
oh
yeah all right welcome to the to our
lightning talk on pod two uh show of
hands who here is not yet sure what a
pod
is who here is too afraid to put their
hand
up okay at least one person um so pods
in a nutshell you basically have a key
Value Store of some sort you
cryptographically um you know sign it in
some manner um I'll I'll say a little
bit about that in a moment um we'll be
talking about the next generation of pod
that was uh already alluded to by Justin
and the summary of pod two is that it
allows for easier composability than pod
one that's essentially it all the
advantages of pod one are there in pod
two it's just a matter of having being
able to compose pods which we cannot do
with pod one in quite the same
way so just a QR code with uh link to
our repo you can find all the code here
uh Justin's already provided this link
but here it is in the form of a QR code
if you like to scan QR codes instead um
so we actually have an ongoing Port of
pod one to rust and that's in the parket
Pod subdirectory and then pod two has
the our current efforts uh in developing
pod 2 so pod one so far as I mentioned
you basically have a key Value Store you
meriz it this isn't an entirely new idea
but it is a solid one there's a nice
blog post by Joe geps and merizing the
key value store for Fun and Profit worth
reading um and we construct things in
such a way that it's easy to make ZK
proofs about these things yeah so we use
the you know appropriate signature
scheme and so on so we can use grth 16
for
proofs um and the ZK workflow for pod
one is essentially you take your pods
you have some kind of configuration
proof configuration that says what you
want to prove and you plug that into
some procedure called GPC prove what you
get out of that is a Gro 16 proof
together with some revealed claims and
this is the rough workflow now let's say
you wanted to take the output of this
and generate a brand new proof so
something like you know taking a bunch
of PODS taking a bunch of proofs
revealed claims putting it in a box and
then spitting out a brand new proof um
but how do we do this um it's not
entirely clear how to do this with our
current setup uh using circom and grth
16 now why would we not proceed with
Groth 16 why is Groth 16 not
suitable for this application R now so
very quickly uh the main idea here is
like we can do recursion over the grth
16 it's just like it's too expensive for
like most of like the real world uh
applications uh the main idea is that
this Brute Force recursion will be like
uh we Define a circuit that verifies uh
like a full proof of the same system so
in in 16 will be like having a A1c
circuit that verifies like the logic of
the ping checks and and so on of a 6
proof which requires some like uh in in
the worst case like some non-native
arithmetic of the elliptic Cur which is
very expensive in circuit and in some
cases where we can use some c c curve
Cycles uh we can get this a bit down but
uh nowadays we have like some like uh
more efficient uh options uh such as
like the Stark Side of Things uh we um
using also some of those like uh small
Prime field uh systems like Goldilocks
in the case of PL 2 or Marine primes in
in PL 3 uh we can we can achieve this
like kind of recursion which like
instead of taking like uh millions of
constraints it takes like hundreds of of
gates and and then it's like uh it
translates like smaller proving times
like few
seconds so um so far as I mentioned a
pod well actually I didn't exactly
mention it but essentially a pod
consists of a claim and a proof here
yeah
would not sync up on this one so one
thing i' say is this is POD one which is
a system that's currently used for frogs
Etc which has limitations and so Ahad
and AR are going to talk both about pod
one and pod two what I showed you guys
is POD two just so it's super clear um
sorry for that Interruption exactly no
worries so essentially we have a claim
and a proof with pod one you essentially
claim I have this key Value Store some
party with this public given public key
um attests to the validity of this
collection of keys and values key value
Pairs and then proof is just a
signature but then when we plug it into
that box to get a ZK proof we get
something of a completely different form
um our claim is that we have a proof
config and it is consistent with some
set of revealed claims like maybe you
reveal your date of birth or something
out from an ID pod and then the proof
would just be some grth 16 proof like
plus or minus some extra bits to say
exactly what circuit we're dealing with
like you know artifacts um and so you
can see see it's sort of heterogeneous
here as far as the form of claim or
proof and our our approach now is to
kind of unify these in such a way that
the claims should be of roughly the same
data type and that's where pod two comes
in and in a nutshell we again have a
claim and a proof the claim is basically
we have a bunch of statements named
statements so we have a map taking some
key you can just assume it's some
identifier it doesn't really matter what
form it is to a statement and our proof
is either going to be a a signature of
some sort kind of like with pod one in
our case we use a schnor type signature
scheme but we're kind of branching out
from that and or it could be a ZK proof
in the form of a planky 2 proof so we've
shifted from grth 16 to planky 2 and now
what is a statement well to get into
what a statement is I need to tell you
exactly how things are laid out um but
let's just start with statements a
statement could either say nothing at
all or as Justin said you could say hey
the state is I have a value this is its
name it comes from this place um and in
this case we have a notion of origin and
anchored key um I won't really say too
much about that but the rough idea is we
we're going to have processes for
constructing new pods and we kind of
want to say how these new pods were
constructed in the process and keep
track of their Origins um and um yeah I
mean we have other such statements like
equality
non-equality inequalities are also in
there but I just omitted them here but
then we have things like sum of which
Justin already talked about and to to
actually construct statements you apply
operations so again we have like no Ops
uh constructing new entries copying
statements and so on and the idea is
we're going to have these boxes where
you can actually take pods and all you
could do you could just copy statements
from these pods um and verify that the
copying was done properly in
ZK now uh as I said earlier we kind of
had like we had pod and GPC they're kind
of like two completely different animals
here we have a pod and we have PODS of
different types now claims will always
be maps from keys to
statements um but proofs could differ in
their formats so we Define a schnor pod
to be a pod whose claims are of the form
value of key is value yeah so all all of
its statements will have that form and
the proof will always be a schnore
signature now we have the notion of an
oracle pod which can take claims of any
form so here we're assuming there's some
trusted party or some trusted machine in
the cloud perhaps we have a fully
homomorphically encrypted setup going on
where we could just pass all this data
to some server and it's going to run
those non ZK programs and you know it's
going to take a bunch of PODS and it's
going to check that you know this entry
in that pod is greater than that entry
in that pod and then it's going to spit
out a brand new pod attesting to all of
that so we call that an oracle pod and
it is pretty much a snor pod with a
god-given an oracle signature basically
and why would we have this well besides
you know being optimistic about fully
homomorphic encryption and perhaps even
multi-party computation um it gives us a
model of what the ZK circuit is going to
do just outside of ZK and that's what a
planky pod is it's basically an oracle
pod but done in the circuit and the
proof is not a signature but a plony 2
proof and I mean as I said you basically
want to take some data and construct a
pod out of it some dat yeah one minute
no two minutes okay great uh we have
gadgets constructing pods you use
gadgets that's our terminology that's
essentially what the slide says so you
can construct a schnor pod using a
schnor gadget which basically means
taking this key Value Store at the
secret key and Bam schnor pod and
similar deal with the planky gadget I'll
sort of rush over to the ZK circuit um
because we don't really have much time
but long story short we have a recur Ive
circuit in plony 2 where we plug in a
bunch of schnor or Oracle pods together
with plony pods we verify signatures or
plony pod uh yeah proofs plony proofs
and then in the circuit we you know
check a bunch of stuff so we also have
to keep track of where these pods um
come from where their values come from
and so on all this stuff has to be
checked in the circuit the operations
have to be applied yada yada yada plony
pod comes out future directions uh this
is the workflow needs to be streamlined
the cryptography is not that strong at
the moment um we kind of want non-native
arithmetic non-native schemes so we want
to use our pod ones so you know BN 254
based crypto in this 64-bit field which
is bit difficult and that is essentially
what leads to the backwards
compatibility that we're kind of hoping
to get out of this yeah U by the way
these slides are on my GitHub I can link
to them if anybody wants to have a look
at them later on so you don't have to
take pictures thank you very much for
your attention
[Applause]
being an MC for a bit we have a little
bit of time for questions for Arnold
andad so oh yeah we have a hands raiser
arur do you have a
mic so um do you think of roughly the
schnor Pod is like a self-attestation
the Oracle pod is anything that you
would use via an introduction Gadget
will come in as an oracle pod whether
it's originally like a proof from a zvm
or something signed or whatever is that
just how things will sort of always be
introduced and then the plugy pod's
always within the system um kind of sort
of actually I would view it slightly
differently the introduction Gadget at
least the way I viewed it was more to go
from our legac Legacy pod ones to schnor
pods actually so schnor pods are pretty
much exactly the same as the pods you
you know the Frog pods the ticket pods
Etc that we've had so far um what that
no they wouldn't be schnor pods but they
could be they could have been schnor
pods it's just that we had a different
cryptographic scheme but if you take
those you would use the introduction
Gadget to get a schnor pod to then use
here well you wouldn't get a schnor pod
cuz it wouldn't be schnor signed it
would be a ZK proof on it yeah well I'm
saying okay so you would essentially get
a snorepod but you do that in ZK so that
you you don't have to actually attest
well I guess we could call them
differently yeah so there there are many
ways to do it I guess I think the
comment you made which you're right
about which is like things inside the
system would be prony pods it's true
that strong pods are going to be self
basically self attestations and then
um foreign cryptographic data being
imported one way we could do it which is
not necessarily the right way I mean the
way I'mma describe it works as well is
we would make a new Gadget type for each
new kinds of data that you would import
basically so you would have like an
email pod you for to import stuff from a
Us's ZK email we would have a passport
pod for like a specific kinds of pass
okay that's what I was sort of wondering
is if you were going to try to import
them under the same pod type or just
introduce a new specific pod type for
each yeah and so the the cost of of
having a new pod type is you need the
verifier for that pod type to be part of
the spine pod right the plunky Pod so
one tricky thing is if ideally you would
get to a stage where you don't need to
embed the verification key for all of
these gadgets into the spine pod and you
would be able to like dynamically load
them by witnessing them and having like
some form like certificate Authority
system or something like that but very
much work in
progress thank you I mean I think we do
kind of need a new type it would
essentially look like a schnor pod but
with a ZK proof instead so we' put some
constraints on the types of statements
you happen
there it seems like we're super out of
time so uh our next speaker is aush
Gupta aush Gupta is gonna talk about ZK
email so um ZK email is a way to
introduce uh cryptographic data from
email systems um and it's uh very much
philosophically fits within what we've
been talking about over the last hour
which is making use of cryptographic
data and Computing on top of it
cool um maybe just so I can get a sense
of where people at um and how much I
should spend on background maybe like
raise your hand if you've heard of ZK
email or seen any of our talks this week
um Okay cool so in that case I'll kind
of skim over the basics and I'll focus
more on the like interesting new stuff
that I didn't cover in all of our other
talks um so we'll quickly go through the
basics and I'll talk about some of the
interesting infrastructure that is
relevant not just for email proofs but
generally for provent proofs um and one
vision of how doing this sort of
programmable cryptography might look
like and then hopefully expanding uh the
sense of what you can do with like weird
applications that you know are kind of
half zkl and half other Primitives um
that might you know lend itself well to
the idea of oh like what if you like
compose these proofs can you get more
interesting
things okay so the first thing I want to
talk about is how I see um adoption of
say cryp graphic technology in the
context of all the other cryptographic
technology if we look at um cryog
graphic infra over the last you know 10
to 20 years we see that there's a
practice of making things more user
inuitive but not a practice of say like
uh private key ownership so for instance
with VPN it was very hard to set them up
at first and then now it's much more
turn key in that adoption curve maybe
took like 10 15 years um end to end
encrypted chat um initially you had to
roll your own pgp now you can use endend
encrypted Messengers um previously you
had to roll your own tour you have to
find your own exit nodes now you can
just use Brave incognito mode
um to have TLS interpret TLS or have TLS
in your website you had to do very
bespoke certificate stuff now it's all
Happening by default um and similarly
you can you can make a similar argument
for say like uh blockchains or web three
data or even cryptography in general and
um one of the main takeaways here is
that like there should be an easy way to
do these kinds of proofs um where you
don't have to punch private data to a
server because in all the cry all the
technology we've seen in the past where
cryptographic technology is like the
purpose of the thing or the end game
like you never want to manage private
data for users it's always on the client
side um and I think you know folks
alluded to this in many of the earlier
talk lots of digital signatures you can
take um you can take pass Keys you can
use this to do transactions very easily
um you can take passports you can do
this to proove citizenship you can take
app a test you can use this to approve
execution of some app on your phone um
and of course emails um and the really
interesting thing here is that uh as
long as you have a digital signature you
can put a ZK proof on top of that and
then verify that offchain data onchain
and so the hope is that
um more seeing more of these and driving
more of this adoption can make this kind
of concept of cryptographic
interoperability more tangible um and so
I guess most folks already know this but
email are sonicor the Deon protocol we
stuff this into a ZK proof and we add
selective privacy on top this means we
can keep whatever data we want in the
email private we can directly verify the
web to mail server and we can verify
them on chain um there's a bunch of
interesting Primitives that we're
thinking about um
the the the nice thing here is that
we've tried to abstract these all the
way so we have libraries for all of
these things in all the different ZK
proving languages and we're constantly
iterating on these but the hope is that
users actually creating these kinds of
proof should not have to think about the
details of which of these Primitives
they're using um and you know one simple
idea of something you could do is very
simple email redaction or whistleblowing
um where you know you you take an email
you highlight what you want to hide and
you reveal everything else um but you
can do much more complicated things one
cool thing that zkp recently built is a
domain Marketplace on top of ethereum
where you can prove you transfer a
domain on name cheap you get a
confirmation email and you use that for
the seller to unlock the escro money
that the buyer locked on chain um and
this is quite interesting because this
means that you can as long as you have a
signature you can build markets on top
of it you can build interoperability on
top of it um but how do we have a
million zkp tops um and so the idea is
you need to be able to make these new
kinds of proofs very very fast and
integrate them very very fast and part
of this is the pods Vision it's you know
very easy to to select which proofs you
want and part of it is actually defining
these kinds of proofs in a very bespoke
way for each proof system and
so one of one of the Visions we have is
that it should be very easy for an app
developer to not have to think about
these details of what is the back end of
the cryptographic infrastructure they're
using they just say I want it to happen
on the client side or on the server side
and it should just happen um and so you
know we we we've investigated all these
invested we've you know created
primitive in many of these languages but
um the point is that we we decided to
abstract this away so that you you you
kind of had the proof system to decided
for you and so the idea is you can say
look I want this specific ZK email proof
maybe the the proof that you got say
rejected from Devcon and then I'm going
to specify whether I'm local or not and
I can put other parameters here if I
want to be more selective like oh I want
this to be you know I want the Pod
version of this I want it to be
composable with rust whatever it is and
create prover will automatically
determine the best prover for your use
case and when you actually want to use
it you can uh just uh call exactly what
you want to do generate proof verify
onchain whatever and it'll just happen
in the background for you um um and the
hope is that again by extracting
extracting this abstracting this away
from actual developers um you don't have
to think about the ZK as deeply anymore
but how do you actually create these
proofs like that Devcon rejection proof
um The Hope is that you can make this
really easy to make so we've done a
bunch of iteration with folks building
different kinds of patterns um and we've
kind of settled on this flow that seems
to be intuitive for most people which is
basically you name your pattern you
upload an example email and then we
autofill a bunch of information from
your example email so we say you know
who is the sender what is a selector
what are all the different lengths and
we will autofill this information for
you and then um one of the things we
Noti is that when you actually want to
parse the email you have to basically
Define this like Rex to do that um this
is a great gor post where he talks about
how Rex is kind of like a very early
vision of neural networks it was like uh
the folks who were inventing this stuff
were like oh like rexes are really
powerful and so that's part of the
reason that we rely on them for a lot of
the pars saying um and in a kind of a
different way we basically like we
notice one of the problems is that
people often like don't Define
deterministic re is very well uh like
many folks like because there's some
constraints like oh you can't use
lookarounds you can't like go back or
else you break some of like things
become a lot more expensive um we like
basically train this AI on all of our
patterns and now the idea that it'll
automatically you say oh I want to
extract the username out of this body
and it'll should automatically generate
something that will extract the username
out of that body um so the hope is the
flow of making these proofs is like much
more intuitive and you get kind of a
pattern that looks like this it's like
maybe 20 25 lines you don't have to read
it obviously but it's basically like
some reject of where you're actually
parsing um the domains and the
parameters of the email itself and this
will just get applied to all the
relevant emails um and then the cool
thing is imagine you want to like reuse
some proof that somebody else is using
you see oh I want to reuse name chep's
domain proof and instead of building a
Marketplace on top of that I want to
unlock another domain the other way or
something you want to build some other
composable thing on top of it then you
want the ability to look at existing
proofs that everybody is using making on
chain verify them reuse them and so we
have this nice little registry where
people can look at all the existing
proofs
um and the really cool thing is there's
sort of this like versel like Vision
where you want to be able to deploy
things very easily so once you've
defined this pattern we automatically
deploy this little front end for you
where we say look we're automatically
going to create this thing where you can
sign in with your Google account we'll
filter which emails should be in fact
parse if you look at the bottom we
filtered their inbox to say these are
the correct emails that will parse for
this kind of proof and the user can
automatically verify them and so and you
know another interesting analogy that I
think we see in like normal development
space we haven't yet see in in ZK space
is like how do you actually do this kind
of version history because these emails
change formats all the time or people
want to maybe like Fork the pattern for
Devcon rejection to ship Devcon
acceptance or something and so you want
like a very like natively integrated
GitHub like capability to say oh I like
this pattern but I want to tweak it a
bit or I want to use an older version
for this older email or whatever um and
so building these kinds of version
Primitives I think is very
powerful um folks have built a lot of
cool stuff um someone built a Dropbox
verification someone built proof of
flight ticket from one uh and you only
reveal F and two um someone built your
part of a slack workspace now you can
start to see how this composability
really matters like I can prove now that
I'm part of the company slck workspace
and I took a flight to Bangkok and now
I'm going to get automatically
reimbursed on chain um and so as you
start composing these together you get
very interesting powerful Primitives um
you can prove you exported your LinkedIn
data and then you sell that to open AI
um you can prove you exported your open
AI data and then sell that to
anthropic um you can prove you completed
some issue on GitHub and automatically
get paid um you can prove you ordered
padti in Thailand um you basically have
a grabber seat that shows your location
is Thailand and Pad Tai was in the order
um and of course that you maybe got
rejected or accepted to
Devcon um and now you can see how this
SDK makes a lot more sense you just
choose the one you want to import and we
can automatically fetch that from the
registry um yeah so this is this is live
folks can try it out um another I think
underrated piece of infrastructure is
like archiving these public keys this is
the case for Deacon but this also going
to be Cas for all the other public keys
on the internet the country public keys
for passports the uh ID public keys for
ID cards there's not really a clear
Archive of these keys anywhere and so
our Hope was that we should make it easy
for folks to see these old public keys
and then access them where they want to
and like why is this relevant um so
here's one example like this is like
Hillary Clinton's email inbox um from
2016 we ran like Deon verification over
all of it and these red ones are the
ones that no longer verify because we no
longer have those deom keys um and this
problem is going to happen more and more
like as we build the signature
verification per is we need a place
where we can settle these public Keys um
and for for deim it's very easy you just
hit this DNS registry um and you can
kind of search on this archive and the
hope is that you know right now this is
one server that's doing this archiving
but you can imagine you can build a
whole consensus layer on top of this you
could have a bunch of own independent
archiving nodes and when you want to
fetch a value you say do a threshold
signature over all those archiving nodes
and you say look yep like 10 out of 10
of the archiving noes said that this was
in fact the public key on that day
sounds good to me and and you can kind
of almost build a content sens Network
that is just archiving Keys um and
there's one cool trick specifically with
RSA where you can recover lost public
keys so we were able to like get public
keys from 10 years ago that no longer
exist and you do this like cool RSA gcg
trick that I don't have time to get into
but you can look at this if you want um
it's pretty nifty um and then users have
to contribute how they actually like
access these keys so for emails you have
to contribute the URL for passports
you'd have to contribute the the country
kind of URL um and so it's always there
has to be some kind of mechanism to
contribute to this kind of AR
Network um cool and then maybe to
inspire a little more I'll just kind of
Rapid Fire some applications um one
thing folks have really wanted is the
ability to use Google signin directly so
we kind of built a school primitive
where you can enter a command and then
sign in with Google and the sign in with
Google will sign that command and then
prove it on chain um you can do uh kind
of credible whistleblowing or domain
proof so for instance you can prove you
work at a company and then uh the
question is how do you do moderation on
Anonymous message boards um so for
instance maybe you want to prove you
worked at Boeing
but you don't want to Ral who you are
but you want to say look I forgot to put
screws on that plane maybe don't fly in
that one um well you know the best way
to do this is you prove your an employee
there and then we do moderation with
tees um with this kind of teleport style
thing which is which is quite cool um
you can have email trigger transactions
um it kind of looks like you'll get an
email like this or you'll do a sign in
and you can approve a transaction on
chain um it's very easy to build this
kind of thing and uh yeah I'm excited to
to jam more and I'll take any questions
[Applause]
it's
fine um any
question okay I have questions yeah uh
so so you you were talking about the
idea of having kind of like a consensus
Network to save public key um from your
perspective like what's the actual like
what what do you think personally is the
like the scalable way to just like
Google search Style just like save the
whole internet like public key from a
public key perspective whether it's like
htps certificates domain name public
Keys Etc just everything that's being
used yeah it would be really nice if you
had signatur so like if these countries
added sxg or RFC 9421 to their web pages
you would have direct signatures that
then you could save and you don't need a
Network anymore you need one person to
save the signature and that's good
enough um unfortunately like many of
these keys are distributed across
various internet infrastructure like
certificate authorities that aren't
really on the Internet or on a website
or on like DNS without DNS sex they
don't have signatures and so the classic
method of like yeah ideally we just use
a Wayback machine toiz archiving but
much of the stuff is not on like a hdps
web page it's on some other public key
infrastructure that's not directly tied
to the internet in some easy way and so
that's why I think we want this like
other Paradigm of archiving um but yeah
I wish way back machine just added the
ability to do this um
yeah yeah it's a good question like we
are like how do we think about the risk
of bootstrapping this on top of the deom
standard which may not have been
engineered to do like all the security
things we want it to do um and maybe one
thing I would say is that this is sort
of like an intermediate transition like
it's kind of if we want to get signed
data everywhere and if we want to get
really like all those private keys to be
in like super security EES or whatever
uh down the line we have to prove to
people hey you can do interesting stuff
today and I think that a lot of that
comes from like look like you can do
these interesting composable proofs oh
you can do account recovery and like
yeah the security is like the same
security as the ability for you to send
from another Gmail account um like you
know if you can do that you can break
the system but the hope is that like
Gmail Outlook Etc have engineered their
systems to be good enough that this
works at a small enough scale and then
hope you can eventually get proof
there's more robust signatures people
add DNS SE because they oh this is a
real thing people want and are using so
I would even say this is like a
transition period of how oh we need to
connect these kind of Worlds of data
before all the data is signed and
verifiable hello um so here I'm I'm
going to talk about uh cyber frogs um if
you've uh played around with the frog
game by registration you might have seen
one of these things uh this is a little
box um a little uh sort of custom
circuit board a uh PCD PCB if you will
um that like it has the ability to
generate um pod v1s uh entirely on uh a
kind of like pod pipeline that's built
using uh to run on this very small cheap
uh like uh risk 5 processor so first and
and I think that there's a couple of
lessons here that I think are going to
be interesting to people interested in
sort of General software uh programmable
cryptography uh
that I think parallels um like like
Hardware I think parallels uh like
programmable cryptography uh in
particular ways so uh going back to some
history stuff uh this is ANC oh it's uh
wait okay this is aniac it's from 1945
one of the first computers it was $7.5
million and it ran at 0.05 megahertz a
few years later there was the Apollo
guidance computer $4.4 million 2 MHz
uh and in 1984 we had the Macintosh
about
$7,000 uh 8 MHz this is mors law roughly
um so this is the cyberfrog it costs
about $5 totally custom like ordered and
designed and fabricated and with
essentially this cost over the course of
about a week it runs at 160 megahertz so
you can see uh and it has a risk five uh
core and that specific core is about
$160 um and that sort of shows the scale
of like how Moors law has essentially
made like computers super cheap super
small um and I think this is kind of
like a a diagram I think that shows some
of the parallels between like in the
past we had these big room siiz
supercomputers uh that sort of do the
equivalent of sort of the very small
amount of compute that you can get for
literal pennies now um and if you sort
of go horizontally and like preserve the
scale the size and cost uh you end up
with essentially the like latest AI
supercomputers on the right is the
latest Nvidia dgx like super cluster
thing which is sort of the equivalent of
a few trillion Hertz uh versus 5,000
Hertz um on the bottom you can sort of
have uh you can see this Arrow it's kind
of meant to represent essentially uh
like conservation of sort of compute
quantity so uh this like one dollar
processor has actually orders of
magnitude more compute capability than
that like original ENC
um uh but you can also end up creating
an even slower computer uh on top of
that like trillion like terascale like
supercomputer and that's sort of the
overhead of a lot of these like uh
programmable cryptography systems if
you've uh played the Frog Zone thing
also um that's sort of an example of the
sort of tremendous overhead that some of
these Frontier techniques uh involve um
so going back to the FR cyber frogs I
think there's another as aspect besides
the sort of computational capability oh
and I I think uh what's sort of
interesting is basically working with
this sort of very cheap like dollar
scale infrastructure uh you're sort of
playing with a restricted Computing
environment the way that like uh you
sort of are when you're working with
sort of programmable cryptography
environments you're like they're both
sort of situations where you're sort of
artificially working with relatively
cheap or relatively slow computers so I
think that's uh the first half of the
first parallel I think of why um sort of
playing with Hardware is interesting uh
the second one is that like they're both
called circuits like when you're working
with ZK snarks uh and also when you're
working with like electronic circuits
they're both naturally circuits uh on
the left I have um uh this is a
screenshot from ZK reppel which is a
little circom like developer environment
that runs in the browser uh that I built
a few years ago um and on the right is a
screenshot from eased a uh which is a
also a web-based uh very easy to get
started with uh like a system for
Designing circuit boards including uh
like the uh uh cyberfrog which this is a
sort of uh screenshot of part of it um
you can see that they're both about like
sort of declaring signals one is a
graphical interface the other one's sort
of more code-like but ultimately it gets
compiled down into uh something that in
the electrical world is called a net
list um it's pretty much equivalent to
the sort of R1 uh CS sort of uh
representation that like uh is sort of
the intermediate uh like part of circom
that eventually uh turns into like sort
of plon or grth 16 or whatever um
so you have this um and then at the end
it gets compiled into a sort of like
physical uh representation uh like uh by
some sort of compiler on the left is
sort of a little application that
generates uh that takes that sort of R1
CS stuff turns it into like a little
plun prover uh and then on the right you
have uh the sort of laid out PCB um for
the Frog this is sort of the tail
section
um and so like I think basically there's
two things that I think are interesting
like one is sort of working in these
constrainted envir environments are kind
of similar uh and and kind of fun uh and
the second is sort of structurally when
you're working with Hardware uh you're
building circuits and a lot of these
circuits are develop a lot of similar
mental models around abstraction and
connecting things together uh that uh
also apply uh and actually it's just
like nowadays with how cheap it is to
manufacture stuff in China like I think
if you have the skills to like build
circuits with uh like software and uh
like ZK snarks you can also pretty much
apply a lot of those same skills to
building sort of physical things that
are shaped like frogs so
yeah um happy to answer any questions
[Applause]