Programmable Cryptography from a Software Engineering Lens | Devcon SEA

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]