POD: recursive, logical, client-side proofs - Rob Knight

Transcript

All right. Thank you. Thank you very much. Great to It's great to see everyone who has come out. Some some fantastic talks. I don't know if I can follow those with anything nearly as interesting, but I'm going to tell you a little bit about something I've been working on for the last kind of year or so. It's a project that's been underway for maybe about 18 months. So, if you were at Devcon in 2024, Devcon SEA in Bangkok, you might have heard an original kind of early presentation on the work that we were doing on on what we call Pod 2.

So, I'm going to give an update on that project and tell you a bit about what we've been able to to figure out. And what we built is a system for a composable recursive client-side ZK proofs built on a kind of logic engine. So, using a kind of logic language as the the way of expressing the proofs. So, Pod 2 is a is a project from 0x Park. We're a research organization. And we're building on top of what we learned from Pod 1. Pod 1 was used in ZooPass. So, if you used ZooPass at any previous event, I know it's been used at ETH Prague in the past. Or if you played Frog Crypto, then you will have used pods.

And our aim here is to innovate primarily in develop developer experience interoperability composability, not so much on raw proof speed, proof size, memory usage, and so on and so forth, but the layer on top of that. How do we make a system that is composable across different use cases? And in addition, how do we go beyond thinking of ZK as solely a privacy technology? So, not deemphasizing privacy, but adding other things to it. We have that private foundation, but what else can we get from this technology?

And the major unlock on on the technical level for this has been the availability of of client-side recursive ZK proofs. So, I'm sure most people here familiar with ZK proofs, but recursion basically allows you to take an existing proof and use its outputs as the input was one of the inputs into a new proof. And at first this doesn't sound all that exciting, but if you're a software engineer, you will know that recursion is the thing that allows you to do everything. If you have recursion, you can you can count numbers. You can you can count numbers. You can do, you know, all kinds of other things. So, recursion is an incredibly powerful primitive.

Um and that means that we can break, for example, we can break a large proof down into a a series of chunks. Um but it also means we can model protocols between multiple parties where, you know, I make a proof and I give that to you, and then you take my proof and make a new proof and send it back to me, and this is how we know that throughout our entire interaction we're both following a protocol. Another way of saying this is that we can verify state machines. We can verify data that changes over time or that evolves over time, proving that each state transition was valid.

So, where Pods sit in the sort of ZK ecosystem is as a high-level language for expressing the things that we want to prove. And this is important because writing things in in circuits is hard. Even with LLMs, LLMs definitely do help. It's 2026. LLMs make everything much easier, but circuits are still a kind of arcane, weird math thing that like ordinary engineers don't know how to work with. So, we want to present this kind of higher-level language that is more conceptually uh kind of easy to work with.

Um we also want to add in certain baseline features like, for instance, composability, which you don't naturally get at the lower level. So, the core semantics of pods are built around facts or what we call statements. And a statement is something that is simply true. It's It's self-evidently true. It's logically true. Um assuming that our code has no bugs. Um and statements can be deduced by logical operations. So, for example, I have here some I mean, if you can see this, um some kind of fairly trivial statements at the bottom. Uh we have that the number 42 is equal to the number 42.

Uh that the number 41 is less than the number 42. Um that a dictionary containing uh the key pair uh foo and bar uh contains the key foo and the value bar. Th- These might seem like really kind of stupid statements. Like, why would anybody bother saying something like this? Because it's it's self-evidently true. I I I don't really need to prove it. But, understand that this is a kind of logical building block of a system. So, we extend this a little bit further um by the way that we handle our container types, dictionaries, arrays, and sets. So, we represent all dictionaries, arrays, and sets as having a Merkle tree. So, there is uh we Merkleize that key-value store or that array or that set.

And this allows us to take any dictionary. So, for instance, this this dictionary I have here which is key foo and value 42. We now have a Merkle root for that dictionary, and that's a unique identifier for that dictionary based on its content. This allows us to create what we call an anchored key. And an anchored key takes that root hash, so here 0x1234, um dot foo. That means the key foo in the dictionary with the root hash 0x1234. We can now substitute in that identifier in any place where we're using the value 42 because we can prove that the value at that location is is equal to the value 42. So, we can rewrite our statements

um going away from making these kind of plain self-evident statements to making a statement that now has this abstraction. Because I know the full content of the dictionary 0x1234, but potentially nobody else does. So now I can produce a statement that is beginning to hide some information. We're moving away from these self-evident statements to statements that that hide things. We can then go one level further abstract. We can take that equal 0x1234.foo 42 and make a different statement, which is greater than 0x1234.foo 10. So now the relationship we're proving is that whatever value it is

that is held at 0x1234.foo, which I know but you don't, what it's a number and it's greater than 10. And I can disclose to you the proof that it's a number greater than 10, but you don't learn anything else. So we begin with this very kind of silly kind of stupid like self-evident statement, and then we move into these more abstract statements that are more interesting. And you do this with a kind of graph where different statements are then inputs into other statements. So we start out at the top level again with these very plain self-evident statements, and we move into more abstract statements that are hiding some of the internal structure or hiding how we know that these things are true.

So we can logically deduce these things from our private statements, and the public statements that we that we actually want to reveal are hiding kind of the logical deduction that was done to produce that. We we know that it was true, but we we don't necessarily have to share how we deduced it. And then you can add your own code. If you have one of these statements, you can use that as an input to any statement you want to make. So we can begin to make, you know, more interesting statements on top of the the existing ones. We can extend this further with what we call Podlang, which is a logic language.

So, if you've ever seen anything like Prolog or Datalog, it will look kind of something like that. Um and this allows you to create your own logical rules, your own kind of deduction rules. Um so, you can make new types of statements. Um and these custom predicates can be recursive as well, so you can do lots of quite interesting things with them. I think you might be able to just about see this code at the bottom of the the the the screen here. Um this is a custom predicate, which is the the classic ZK example proving that somebody is over 18. Um and this is the composition of four native statements, these are primitive statements.

Um we're proving so, we we take in a passport, uh the current time, and a set of government public keys, government signers. And we compute um the date 18 years ago from the current time. Um we prove that the date of birth on the passport is less than that, it's earlier than that than that date, it's earlier than 18 years ago. Uh we um prove that the passport has a signer, and we prove that the signer is in that set of government signers that we that we passed in.

So, that then becomes a standalone statement, is over 18 uh becomes a standalone statement that you make on its own. That statement itself can also be an input into other statements, so you can compose um more complex networks of statements. This is a slightly more complex example. Again, I'm I'm not sure if you can read the code perfectly well, but it it it doesn't matter, you don't you don't need to kind of study it. Um this is an implementation of something called Ethos. So, Ethos was originally an experiment done by Zero-Knowledge Proofs several years ago on um on zero-knowledge proofs, which allows you to prove well, um do people know the the mathematician Paul Erdős?

Yes, some people do. Okay. Um so, you get a low Erdős number. Um so, the um Paul Erdős was a prolific mathematician. He wrote lots and lots of papers, and he co-authored lots and lots of papers with other people. And after a while, people realized that that this would this kind of gives you like your Erdős number. If you've If you are Paul Erdős, your Erdős number is zero. Uh if you've co-authored a paper with Paul Erdős, your Erdős number is one. If you've co-authored a paper with someone else who has co-authored with Paul Erdős, but haven't done so yourself, then your number is two, and so on and so forth. So, this this is a measure of your degree of separation away from Paul Erdős.

Um and this implements basically the same algorithm, but in in Padlang. So, um we have at the bottom this this uh is dos uh custom predicate, and either you hit the base case, you are Paul Erdős uh your number is is going to be zero, or we hit the inductive case, you're not Paul Erdős, but you need to be able to prove that you have a chain uh connecting yourself to him. So, we go up to the base case, um the source and destination are the same. You are the You are the person that that um it the distance is being proved proven from.

Um and so, the the the distance is zero. If that is not the case, then we fall through to uh a different path, where you have to prove that you have friend, which is the is friend uh predicate at the top, uh who's signed an attestation of your public key. Um and that person must have a proof of their distance from the from the source. So, we have recursion here in built into the language, and is a natural way of expressing this uh this social graph. The other feature that we have, um that enables interoperability, is what we call introduction pods. And this allows us to introduce data from

external cryptographic sources. And you do this by writing a custom Plonky2 circuit. So So Pod 2 is implemented in in Plonky2. Uh or on top of Plonky2. Um and if you write a custom Plonky2 circuit and some glue code which produces an output in in the format that Pod 2 expects, you can introduce cryptographic facts from other sources. So, for example, an RSA signed by statement allows you to take some message and an RSA public key and prove that that message was signed by that key pair, that RSA key pair. So, even though Pod 2 natively has no concept of RSA signatures, we can extend that and now in our network of

statements that we can make, we can include statements about RSA. Um similarly, we we've extended that. We have a some sample code to extend that with passport data. So, if you can make a proof of passport, you can then begin to make Pod statements about that passport. Um another thing we have is is verifiable delay functions. So, this is basically a kind of low parallelization or unparallelizable proof of work, uh which is useful in cases where you want to prove that a certain amount of time has elapsed. So, you basically set a challenge, a cryptographic challenge, that is going to take a certain amount to complete.

Um and you make that a requirement of your statement. So, the statement can only be proven true if the work has been completed. This is a kind of useful for certain certain dynamics. We've been using this to to prototype certain game dynamics, for instance. So, all of this is is um kind of the building blocks of the system. We have uh custom predicates, we have sort of native predicates which give you these basic um you know, ability to prove sort of arithmetic relationships. These numbers are the this this number is the sum of these other two numbers. This number is the product of these other two numbers. Uh this element is contained in this set.

Uh this value is the hash of these other two values and so forth. Uh we have custom predicates which let you write your own rules on top of that. We have introduction pods which let you bring in external cryptographic facts that aren't natively supported. Um and you can compose all of these together. So, any proof that is produced by this system can be an input to any other proof provided that it results in the right kinds of statements. So, anybody can write their own Podling code um on top of this to extend the existing set of proofs that uh that exist or the existing existing sets of statements that exist.

So, any custom predicate can kind of interface with can import uh any other custom predicate can rely on a statement verified defined by that by that custom predicate. Um we can join together statements from different sources. So, as in the social graph uh example, um we can kind of join statements as I like to think of joining things across space. Um I have a statement, you have a statement, or I have some private data, you have some private data. We would like to prove the relationship between the data that we uh that we have. So, I make a a proof and give that to you. You then prove some relationship that that

has to data that you have, and you give that back to me. This is for instance the the Ethos example works in that way. Um and this could be between people. It could be between people and institutions. It could be between institutions and institutions. Um and it could indeed be a a um a um sort of multi-uh uh participant network. Uh we can also uh compose uh proofs across time. So, describing the evolution of the same piece of data or the the sort of the same uh if you think of a database, a database contains certain data at a certain moment. And over time, that data gets updated. We insert, we update, we delete uh records

from the database. What we want to prove is that at each step of that process, the updates that we made to that database were valid, that it that they were correct. Again, this is the sort of the state machine uh model. We're proving the correctness of a series of state transitions. So, what a concept that we have for this sort of peer-to-peer or or across uh across space um kind of proof is the request. And so, a request is where I send you basically a kind of under-constrained set of statements. So, I I send you a set of statements with some free containing some free variables.

Um This looks a little bit like a SQL query, and it's it's not kind of accidental that it looks a little bit like a SQL query um because SQL is also kind of comes from that logic programming uh kind of heritage. Um And so, here I'm making a request. And again, I'm not sure if you can see the code perfectly, but um it's a request for a proof of three statements. Um the first um is So, we have EthHub's uh public key. Uh the first argument is a public key, which is in this example is Vitalik's public key.

Um then there's a free variable destination and a and a free variable distance. So, it's a request to prove some that you know some key that has some distance from Vitalik's public key. But then on the second line, we constrain that further. We said the distance must be less than four. And on the third line, uh we say that there must be this random nonce that is provided uh must be signed by whatever public key you you specify as the destination. So, what that really means is this must be your public key. Like you must have the ability to sign this message. So, when we compose these things together, this is a request for you to prove that you have an Ethos distance of less than four from Vitalik.

And if you have the available data locally, uh you know, on on your device uh to satisfy that request, if you had can produce the necessary input statements, then you can produce a proof and send that proof back to me. What's kind of cool about this is that if you can't do that, you will also know why you can't do that. You will be able to like look at the tree of logical um um premises that are required to make these statements and work out, "Aha, I can't prove that my distance is less than four. What do I need if I was going to prove that my distance was less than four? Well, I I I need a friend who's at who's attested to me, and I need a proof that their distance is less than three.

So, now you can ask your friends for the statement, you know, Ethos public key Vitalik um um their public key and a number which is three or or less, and also a an Eth friend attestation. So, the fact that we have a representation of like what it what exactly are the logical premises here and now allows us to kind of reason about and to build, you know, automated reasoning tools, solvers, all all these good things um that will um surface like the missing statements, and then potentially, you know, have gossip networks or have other means of of going out and like searching for people who can provide us with the missing kind of facts that we currently don't have access to.

Um we can also do a kind of a machine um over time. So, when we have a state machine like a membership list, we can prove that the membership list began. It has a new sort of we have these two possible state transitions. In a real-world example, there would be more than two, but um one is is new membership list. This is the the initial state of the of the list. And then the second transition is we can we can add add members to the list.

Um so, new membership list um inserts a creator, inserts that creator as the initial member, and it inserts the creator as the initial admin of the of the group. Um once you have that set up, you can then add new members to the list. So, add member requires that there's an action type, which is called add member. That action has to be signed by a public key. That public key must be in the list of admins. And if those three things are true, then we're going to compute a new members list, which is the old members list, but with the new member inserted.

And then we're going to compute a new list object, which is the old list object, but the members list key has been updated with the the new list. What this allows you to do then is to prove that this membership list was managed correctly. At no point did a non-admin add somebody. No point did somebody, you know, hack the DB and insert themselves into the membership list. It's not possible. You wouldn't be able to have a cryptographic proof that this was the case. So, this is the beginning of being able to manage kind of governance of of groups, governance of institutions.

Um and this I I feel to me this feels very different from the kinds of things that we were talking about doing with ZK proofs, client-side ZK proofs a few years ago, when we were mostly thinking about this as kind of colloquially, like the little guy and the big guy, and the little guy is me, and you know, I'm really afraid that the big guy wants to snoop on me, and so I'm going to have my data locally, and I'm going to make these like tiny little proofs to the big guy that that that sort of prove that I'm, you know, over 18, or prove prove I have a ticket, or whatever it is. Um but the big guy never makes any proof to me. He just sort of accepts my my proof, and and and, you know, I'm just happy that I get some

privacy. Well, what this points to is a world where actually, if you're interacting with an institution, you could be asking that institution to prove things to you um that they are managing themselves, you know, that they're managing their internal affairs correctly, they're managing their membership list correctly, um and so forth. So it becomes something that is Again, this is the recursion property. It becomes a property of both sides or all sides of the relationship. You begin to put the entire system into a recursive network of zero-knowledge proofs. So it's not just this little thing at the edge, like the entire system is zero is provably correct at at all times.

So you can think of this as as as being a question of, you know, who proves what to whom, um to to slightly paraphrase Lenin. Um and this is As I say, this is moving beyond uh thinking of it purely in terms of privacy. Uh privacy is still there. Privacy is important. Privacy is guaranteed. You can have privacy, really good privacy with this system. Um but you can also think about these other properties. You can think about composability. How do we take these different private statements that people are able to make and plug them together to make new statements? Uh you can think about integrity. How do we use this system to prove a chain of custody for some data or a a sequence of state transitions? How can we prove that those

things were done uh in the right way? Um And so we can prove that in a vote all of the votes were counted. Um in a membership list, we can prove that all members were properly approved. Um And again, this really just boils down to, you know, for the for the for the engineers, uh prove that all state transitions were valid. Um This I I again, for me is is a sort of not uh an abstract question. These were real uh problems that we had with ZooPass. So, we had, you know, ZooPoll, a private voting system that kept your identity private when you were voting, but it didn't actually prove that the result reflected all of the votes that were cast. So, we had privacy at one

level, but we didn't have integrity. Um when we did ZooPass for ticketing, um we then used we extended that so that people could like sign in to uh Gitcoin, for example, and vote in a in Gitcoin funding rounds based on their attendance at an event. But actually, um like that was based on an old kind of, you know, web two-style database of who the attendees were, and then it signs a bunch of tickets um to those people, and all you were proving was that you had a signed ticket. There was no way of constraining like how many signatures were made. So, with this system, you can you can prove that there were, you know, n mem- uh attendees of

an event, and no more than n tickets have been issued. And so, when people then turn up uh to vote in Gitcoin, you know, we can prove that we are not there's no kind of shenanigans going on where we're issuing, you know, extra tickets to people so that they can vote um in that poll. Um I think that just about summarizes everything, and I think we're at time. So, uh if you'd like to talk to me more about this, you'd like to know more about what we're doing, uh this is my signal. I'm trying to uh kind of, you know, socially pressure everybody to get off Telegram. Uh use Signal, it's good, um and it's private. Um so, if you want to talk to me, you have to use Signal. I will ignore your Telegram messages. That will that will not work. Um, yeah. So,

thank you very much.