Episode 281 - Exploring Lurk: a New Language for Recursive zk-SNARKs

Transcript

[Music] welcome to zero knowledge I'm your host Anna Rose in this podcast we will be exploring the latest in zero knowledge research and the decentralized web as well as new paradigms that promise to change the way we interact and transact online this week I chat with chimei kunzong and Francois Gario from lurk lab lurk is a turn complete programming language for recursive ZK snarks we discuss how lurk could be understood as a dialect of lisp what lisp is and how developers familiar with that family of languages would be

able to interact with lurk we discuss how this compares to other zkdsls as well as the new innovations that it brings to the table now before we kick off Tanya will share a little bit about this week's sponsor ever feel like developing zero knowledge proofs is a daunting task while the team at risk zero is here to remind you that it doesn't have to be that way they're out of the box tooling allows developers to access the magic of ZK proofs from any chain without needing to learn custom languages or build custom ZK circuits Bonsai risk Zero's most anticipated product is a proving Marketplace that enables any protocol or application to leverage fast CK proofs in languages like rust go and C plus

visit r0.link forward slash ZK podcast to learn more and sign up for the Bonsai wait list you can also find the link in our show notes and now here's our episode [Music] today I'm here with chimei kunzong co-founder of lurk lab and Francois garrio head of engineering at lurk lab and we're going to be talking about lurk welcome to the show to both of you hi and it's a pleasure to be here yeah it's great looking forward to it she made this is the first time we're meeting and I'd like to hear a little bit about the work you were doing maybe before lurk what led you to work on this problem it really came directly out of the work I did on the file coin proofs I led the

team that did the implementation as opposed to the research and protocol development of the filecoin proofs as so we did a lot of uh snark stuff and kind of pushed the limits of garage 16 and discovered a lot of the limits of it in the process and so after file corn launched that opened up a little bit of space in my brain to think about other things and I was able to start answering the question well what if what if we didn't have to use 2016 technology energy after the next fun thing that I work on and look kind of came out of that wait I want to hear a little bit about this work at protocol Labs though so like there's a snark under the hood I don't know that we really ever covered

that what are these snarks for where is it in that protocol as you probably know filecoin is a blockchain that gives you power based on files that you store in order for that to work you need to be able to prove that you're actually storing some particular uh data and so those two different major proofs that are used in that one we call proof of replication this is a big very heavy proof that you've taken some starting data either 32 or 64 gigabytes and transformed it into a new random-ish bit of data which we call proof of replication and this is what stops you

from just making any copies of the same data and pretending that you're storing many copies when actually only of one copy so this replication is the unique copy that's the big proof and then there's something called proof of space time which is on an ongoing basis you keep making a proof that you still have that data so the blockchain challenges you says Hey prove to me that you know one little piece of this file that you have replicated before and that's a smaller cheaper proof when you created this where they kind of created as the same snark but they're running like a smaller portion are they two separate

ones well they're quite different they have some of the same components everything is based around Merkle trees um but the proof of replication there's a complicated process that is you can almost think of it as a kind of intentionally expensive encryption that involves sequential shot 256 hashing and that's just to show that you've correctly replicated the data then at the very end there's a commitment to the result so this creates a Merkle root then later in post uh the the Merkel proof of that same root is used so there's some

overlap but none of the part that has to do with the original data being turned into the replica ever needs to be proved again I think I remember the the file coin trusted setup I believe you did one and I remember it being a really long one is that true well so with growth 16 there's kind of two different setups that has to be done one is the powers of Tau which is general and could be used for many circuits and then there's circuit specific ones at the time I think uh there wasn't a powers of Tau large enough I think others may have made one of the same size or even larger since then but we did sort of the one that's you know 100 plus million

constraints will be uh supported we could have done larger but we didn't want the price parameters to be too huge so in order to make the statements as large as possible we went for the biggest uh powers of Tau we could do at the time and then our large circuits used all of that I see and were you able though with your trusted setup could you run one trusted setup for both of those snarks like the large one and the small one given that the small one I guess would have been included like it would have had enough constraints in there yeah you can just use part of the the powers of Tau that you need but we have to still do the you know the circuit specific trusted setup for each of the each of them different proofs that we

had what were you doing before this or was this the first time you were doing snark stuff or had you done anything like that before no I had absolutely no context for snarks uh I think maybe that's that's part of what enabled me to do it because uh before this I was just doing uh Consulting working for a a Dev shop named carbon5 we got brought in to help with the file coin node okay and so uh you know as a generalist programmer but I read the file coin white paper very carefully and there was sort of these holes in the explanation around how these proofs actually worked and I was fascinated by it so I kept asking all these inconvenient questions and it sort

of came out that nobody was really actively working on that part uh and so I managed to insert myself in there and so I I learned on the Fly got it it was quite an experience so this project was your initiation into the snorkeling yes so after this kind of file coin work was completed you were sort of looking around for something new when did the alert projects start it's sort of gradually came online I would say it spun out of the snark vdf project we had been part of the vdf alliance by weaming protocol Labs here and this is with the ethereum foundation I think we've heard about it exactly and originally there

was a plan to do this RSA based vdf and they had some issues with the trusted setup around that but all all for the last couple years I've been working closely with supernational who really helped to optimize our proofs and many other things and we were talking about this idea of doing a a snark based proof and so I kind of took charge of that from the particle lab side and got that spun up with ethereum Foundation uh and supernational as a partnership and if you followed that work you know some research was done and they came I'm up with this kind of sloth-based vdf and

around that the question of how how are you going to make that work comes up and there were a couple candidates for the back end proof it doesn't necessarily need to be one or the other we looked at Halo 2 we looked at Nova we ended up going with Nova but this got me really inside the mindset of recursive snarks and I'd already been wondering you know what can we do with recursive snarks so as that work progressed uh lurk sort of co-evolved with that got it and just because you mentioned Nova I'm assuming the time frame for this is like summer 2022 or fall 2022 is that roughly when you were looking at that so funnily

enough uh this was in 2021. oh yeah I'll say something about that but I I looked this up for the show and the initial alert commit was actually on July 7th 2021 okay and sort of the the secret information here is that we've been working with Nova before Nova was really exactly a thing ah were you working with srinath then yeah sreenath is the guy yeah basically what happened is at a certain point Justin Drake from the ethereum foundation and I started talking to sunach to see will this actually work and he was very excited I think that people wanted to use his stuff so we said well can you get this licensed in

in the right way through uh your employer Microsoft and that did happen and we started building on it but at that point uh the recursion wasn't fully implemented the paper had been written but the implementation wasn't there but we were still able to understand what it was going to be and start building on top of it so it wasn't for a little while that it actually became fully usable but we knew it would be cool cool Francois I want to hear a little bit about your story and where it starts to intersect here we've known each other from the ZK Community for a little longer I think we might have met like a ZK jobs fair or like one of the ZK hack events online yes yeah very good so my story starts a million years ago when I

had a pass background in formal proof and programming languages research um I gained a PhD in 2011 the domain and then for about three years until 2015 I worked in the Scala community in the community of the skyline language doing some developer tooling for for the programming language and then I kind of gave that up for a while until in 2018 a friend that had not seen for 10 years like bumped me on the shoulder at Facebook beta and I was doing deep learning training so nothing to do with languages and told me hey you know what we have this small chinchy tiny blockchain project and I've heard that you can do things in formal verification I'm sure we're gonna have bugs are you

interested in fixing them and I ended up doing a little bit of formal verification as well as building the blockchain for the gem project and then I worked on layer ones basically for a long while until uh somewhere in 2022 the end of 2021 at the end of Day 2021 I was really tired like tired of what I was doing but also mostly tired period um okay and so I swore to myself that if I was going to do anything else if I was going to start working like crazy again I would basically choose something that had an indiscuitable proposal to novelty and that has an indiscuitably Francois shaped problem to solve

and lyric was a match made in heaven I had been interested in DJ proves basically uh thanks to you since the GK Summit 4. what if you are doing yeah does he gets Summit form was an absolutely crazy event to get into because this is just this was a small co-working space in San Francisco exactly and basically it's that one day workshop they invite you to wipe your head around a Halo Marlin and holography fit proofs so many things got introduced yeah and Zach giving the new Holds Barred all technical explanation of punk which was quite the the shock

and other things like the the transparent snack from dark compilers like absolutely crazy crazy work kudos for organizing something in like November 2018 and which basically I that day I blue screened like I just blue screen from the beginning of the day at the top of the year like at nine to five PM I basically spent the entire day in a constant state of oh my God what is this and so after two three years of catching up uh the I I received an email from somebody at Pro collab telling me the alert team is looking for something and I remember having told to chime before and I thought you know what I'm gonna humor the guy um I had a nice conversation you know

push comes to Charlotte I'm probably not gonna get interested but I'll get a nice conversation out of the stuff and lo and behold I got interested I joined and I've been working on luck happily ever since cool all right so let's actually talk about lurk I feel like we've done some good sort of Storytelling about where the project comes from but what is it is it a language is it a protocol what is lurk lurk is definitely a language as far as I'm concerned uh but the nature of the language sort of embeds it into the proof context in a way that blurs some of those lines because what lurk is is a Content addressed language for data

but look is also a lisp and lisp is a language that really blurs the line between data and programs it might make sense for us to Define this a little bit because you just said lisp is a language but then you refer to a list and I actually don't know anything about this so can you tell us what that is lisp is a large family of languages and that have certain characteristics in common so when I say lyric is a lisp I mean lurk is a dialect of list okay what kind of language is it what like who uses it where does it exist so lisp was um very popular during like the previous

AI boom when people thought that symbolic AI was going to be the thing I see what era is this is this like 2008 this would have been what like 80s 90s oh 80s 90s okay okay yeah way back got it so lisp is the in many ways the OG functional programming language it is is a programming language that has a loud Footprints in AI as GMA just mentioned but it is also a programming language that has such a loud footprint in the academic world every functional programming language that you have heard of say the the ml families or the old camels and and so on or the the Haskell family always a moral Parenthood to lisp

as this functional programming language that they've tried to improve on change another aspect that you may mentioned is this ability that lisp has to introspect on its own programs which is the foundation of this blurring between data and computation where lisp the create terms that you've evaluate other terms of the same language which ties in deeply into the way it implements recursion but originally instant creation from the 1960s that is now considered a little bit passive mostly for reasons of Trends and culture but also because it has a descendant that people like a little bit

better these days called JavaScript which morally is another functional programming language lisp has had many descendants including of course the quantum dimensional camera Haskell but JavaScript is at the moment the the language that is such a gigantic attraction to uh 17 million programmers um that the attraction for the lease Community has been a little bit dimmed but the bright light of the JavaScript so there is still very much a community of programmers that work in this and like this meta reflective introspective aspects to play with things like macros for example that is as far as regular programming languages are concerned to

my knowledge none of them except maybe gab have such a strong band as lurk which is really a proof language that makes proofs about its own evaluation I see I want to just ask one language you didn't mention in that list is rust is there any connection between rust and lisp because I know there's a connection between Haskell and rust isn't there so when it comes to connections between functional between programming languages you have languages that are if you wish this hodgepodge of a lot of connections and a very generalist influences that are kind of using everything you could possibly we

integrate to make the best programming language and then there are programming languages that have a very strong band towards one more fiber if you will that are a little bit more specialized in their influences um so rust is in that first category it's a little bit The Rice Bowl of programming languages that uses uh so yes it has connections to lisp it's very difficult to not have connections to list it's a little bit like not being in the center of Jesse scan these days um but it has connections with many other Concepts whereas languages like the ones we mentioned have this very strict functional upcoming language bands that essentially relates to how much they deal with statefulness so very

easy to make statual statements and rest a little bit more exotic if you if you do it in Haskell camera or JavaScript the difference means yes there's a problem to it between Russ and list but it's a little bit more faint but let me jump jump in on one thing that you said there because I feel like because people don't follow lists very closely people don't know a lot about commonless but common lisp is really a multi-paradigm language where imperative programming and stateful you know mutable State uh are very easy to deal with lurk is very influenced by commonless just simply through the accident of my programming history but in some ways look backs off

of some of the power of commonness because of the realities of snarks and of content addressing uh so lyric is in some ways funny because you know we we don't get mutable content addressing if you want to you know mutate contenders addressable data you need some abstraction on top of that so lurk is a bit more of a purist than the lisp Community became I want to ask ask you about how lurk because I think this is really interesting to see like sort of the history of its creation but you know we've on the show talked about ZK Focus snark dsls quite a few times I mean I've

done a whole episode with Alex osmere now this is out of date this is like two years old where he mapped out all the dsls at the time and I think there we already had like 12 or something and now there's more so I am curious like is this similar to anything that we've seen is it at all like circom or like Noir or like artworks or like anything like that or or maybe like Leo or snarky JS yeah I'm just curious if there's any competition anything you would put in your category in many ways no okay it's different what the idea is that um a lot of the languages you mentioned are languages that aim at performing what we would call Direct compilation into circuits um so you take a program

um that is specified by the user which and then by the user and at the end you get a circuit there's nothing wrong with that approach inherently it's very direct it's very understandable but it is what it is and what it is is a non-uniform model of computation and non-info model of computation is pedantic programming languages for you don't actually quite meet all the terms of Turing completeness so we aim to classify theoretically programming languages by their ability to be true and complete that is to express everything that you might want to compute meaning my programming language you have an idea of something you want to compute in your head you you get during completeness most languages that are doing direct

compilation stop a little bit short of that because they need to model when it comes to Circuit this model of computation by which big programs lead to Big circuits small programs lead to small circuits it is a little bit uh counter-intuitive to what we are able to do with lurk and with regular programming languages which is we have a compiler that will get you the result of the execution and the evaluation of your program irrespective of its size and our compiler does not need to be proportional to size your circuit that's where you get the general during completeness meaning uh it might take a

while to evaluate your program but we don't need to represent it through a compiled program that is as gigantic as your input in order to evaluate it does this have anything to do with the Nova factoring you sort of mentioned Nova at the beginning the fact that you're using this folding is there something in the snark that it's built on I don't actually know how to describe this but or is that is that something else precise okay before we explain that help me say that better because is lurk built on Nova is it built for Nova is it built with Nova let me try to clarify the relationship though actually let me just throw one

thing in really quickly before I forget I think that uh in in the list of comparable Technologies before we didn't mention Cairo oh uh and I think that Cairo is probably the thing that lyric is most comparable to in terms of the the kinds of computations it facilitates got it we could come back to that later if we want to uh so lurk and Nova when I first came up with lurk my default idea was that Halo 2 would probably be the back end and then later when the vdf project pivoted to Nova I became very aware of Nova and had many many long conversations with srinath and Nova became sort of the platonically ideal

back end that we think about but we actually have a gross 16 back end we we could in theory have a completely data compatible and I'll explain what I mean by that Halo 2 back end what I mean by data compatible is because all of our data is content addressed it depends on the hashing that we use and Nova actually uses the pasta curves partially because I said she not like can we use the positive curve so it will be compatible with Halo or Halo 2 because we were thinking in terms of this you know big picture big tent view of what we can do with snacks and if the data is not compatible the thing is you're gonna have to do all this work of converting data between one universe and another so

we really want to focus on the curves and the hashing representations so Nova is what we're targeting and a lot of our plans are based on our knowledge and guesses about where Nova is going to go because I have sort of intera an irrational it's not irrational it's actually a completely rational faith in Sri not's ability to bring out the new hotness uh month after month interesting I want to ask you you just mentioned Nova as a back end I don't really understand what that means for language yeah maybe you can even like help me visualize this a bit well I'll take a cut at it and then I think uh Francois will be able to explain it in better

formal terms but the way to think about it is that lyric as a language as a lisp it's essentially a language for formatting data like Json would be that has a defined interpretation so we say here's a piece of data what happens when I evaluate this so I'll give you some trivial examples so you get the idea what if the datum is the number seven well that just evaluates to itself so you could imagine having a command line you type in seven and then the response is seven but we could also have data that represents some kind of an expression like seven plus six I put in

seven plus six and then it's evaluated and the result is thirteen okay so having some rules of evaluation lets us take a data language and turn it into a programming language and that's basically the lisp idea so lurk deals at that level of abstraction it defines uh some semantics and an evaluation model that lets you take some content addressable data which is like the kind of data that ipfs uses for example and evaluate it and then give you a result it doesn't really care how you prove that so this is where we say you can plug in a back end so we have a graph 16 and snark pack back end just saying if you want to use BLS 12 381 to encode

your data and you like the properties of gross16 plus snark pack then you can use that if you want to use the pasta curves and you like like the properties that Anova proof will give you you can use that if you want to use the same universe of data and you like the properties that Halo 2 gives you and you want to stop and write a Halo 2 backend for lurk which we haven't done yet then you can use that Etc right so the idea here is that in all the the backends that we've recently mentioned uh Halo 2 Nova across 16 and knowing that the header to one isn't implemented yet what we're talking about is backends that are able to do something with a proof as

long as it does the same thing over and over again and this has a deep connection to how you define programming languages on the one hand and the fact that we have a single universal circuit for all load programs on the other hand there are some cryptographic backends namely all the ones that we've cited that let you obtain an interesting and small proof as long as that proof is all about doing the same thing over and over again now natively when you define a programming language you have to Define and not even talk thinking about a proof programming language yet you design your programming language with its syntax yes something that people will have Frameworks or whatever traditionally because it's traditional but you also

need to provide how you're going to evaluate this language and this defines the language itself you can't just throw syntax at the wall and hope that people will understand how to compute with this you have to explain to people how you go from the syntax into evaluating the results that you obtain how do you compute with this language now what you're defining here is an interpreter and the definition of The Interpreter for very large class of programming languages including all the functional programming languages we've talked about Haskell and camel is defined with an abstract State machine you really think about it in terms of a graph in your mind so it tells you okay you're in that state if you're in that state and you

are facing this particular program here is how you make progress with the evaluation of that program to move to another state in your graph okay now you have a graph depending on how complex your your programming language is it may be big or small uh lisp is rather small and if you look at Advance and late later and modern programming languages they get a little bit bigger but the idea is there are nodes in between those nodes that are those States the partial States the the steps the milestones in the evaluation of your program and edges describe how you go from one Milestone to the next and all of those edges are directed and flow towards the final evaluated form of your program and tell

you this is the result which you have a computer list 13. that sort of graph has a stat function that step function is the name given to the union of all the edges how do you maintain your state across the evaluation of your language that step function is precisely what you execute over and over and over again so the definition of your language is in fact equivalent to the definition of the step function of an abstract State machine now this is unusual if you have not formally studied programming languages but if you have this is literally your textbook um there are professors that

will you make you work through that model on a regular basis in nearly every University the list standard traditional abstract State machine is a thing named the CK machine for control environment continuation continuation doesn't start with a c but don't ask and that cek machine which was out of the works of matches Verizon and co-authors a million years ago is what we've implemented to evaluate our lisp or more exactly since we have a dialect of list we have a clever variant of the CK machine that still has a very strong moral Parenthood once you put that in a circuit and you express this in a

circuit this machine is universal in that it can take any list program and them to iterated Applications of the state machine moving to the graph evaluate that program and that is how we have a universal circuit and that is how we've implemented the lisp you just said though you would take a lisp program would it mean that someone interacting with this would write in lisp or is it in lurk is it an existing program that it re-uses or so yes it is the lurk program so you would write in lurg which happened to be a dialect of lisp and through speaking a little bit fast I may have mentioned earliest lease program but what I really met is that it would

be a lot of program if you want to call the Dollar compiler yeah the best way to think about it is just to remember that lurk is a lisp where lisp is a broad family of languages going back to you know and McCarthy's 1960 paper it's basically you know just the way to turn the Lambda calculus into a programming language as fast as possible okay this is definitely a more in the Deep language land than I'm than I I'm not a developer so it's it's hard for me to fully follow this what I am getting though is that it's a unique construction and what I want to understand is like how do people actually interact with this we had talked about these other dsls which like

those to me are kind of clear like the they're either trying to create circuits with a language or they're trying to Black Box the zkp and then you can create private applications using these things but in in this case like what do people use this for so you would interact with it in the same way that you do with the zkdsl but with a few key advantages that will put your mind at ease in the the correct intuitions about your execution one thing that programmers or family programming languages have as an intuition is that if you have a program that has 10 different branches meaning you have a

case statement or a large if with many Alternatives then the only thing you should be paying for when you run into that program with a particular set of inputs is one of those branches not all 10 at the same time but in a once yes or in a circuit organization in general you end up paying for all those branches including the ones you don't take it's the same thing when you're looking at a big for Loop that runs through 1 to 500 iterations and has an early stopping case you know a break statement that tells you no no I'm actually finished with with that fault you would assume that the only thing you pay for is maybe the two

iterations until you break out of the for Loop and it actually is the case that inner one CS you end up compiling this to a for Loop that runs to all 500 Integrations the idea is that circuits in general don't have control structures they are literally a wired out drawn out structure that has no ability to jump at different points of the execution this has led to very famous issues such as if you have addition by zero and one of the Alternatives and you happen to not be in that Branch you will still error out on the division by zero but the point is lurk by running modeling the evaluation of your competition rather than the

declarative description of your computation should be which is what the circuit diary compilation circuit dsls are allows you the ability to recover your intuitions your intuitions are that you walk through a program you jump at particular points of that program when it's written out and lyric is perfectly able to do that for you I still don't understand though what kind of program would it be used I think I need something a little even higher level here like what kind of application or thing would live in this ecosystem are you using this to develop like a Roll-Up smart contract are you using this to develop a application or am I totally am I in the wrong category altogether

this is correct on both both counts okay the difficulty in in relaying what is going on here is that the model is so General and we are in a world in an ecosystem where a lot of tooling is specializing things a lot yeah so yes to the roll up yes to to the generic proofs that happens to be here but cryptographic elements and very much yes to a zkml use case that potentially would have absolutely nothing to do with blockchains whatever okay huh the idea here is that we don't want to operate under vendor lock in absentions you can write your proofs and there are difficulties here to adapt to any

particular use case and we have definitely worked on making sure that you had two links for those use cases but you can write a proof about things that talk about medical tree and maybe talk about the correctness of some cryptographic signatures you write that in your list dialect and Tara you've written a zika page or you can write something about the processing of a particular picture and turning that picture into grayscale and then maybe cropping it and that's a very famous use case about the fact that the latest Sony a alpha 7 generation 4 cameras have the ability to sign stuff and this is a work by danbone and one of

his PhD students primarily Trisha data where you can definitely take a picture prove that it was taken and geostumped at a particular locations and then you want to process it before you display it on the BBC's website right therefore the signature that you have on the original picture does not carry over the reduced is cropped or grayscaled image that he ends up on BBC's website and that's what you see and you'd like to verify the authenticity and the provenance of that picture but if you wanted to write this this is what we're building towards we want lurk to give you the ability to build this case that expresses image processing and makes a proof of the results of that image process interesting so what would they use right

now without it would they use a mixture of these dsls that I just mentioned or they have to create a lot of their own stuff so you have several options you have the the direct compilation dsls that have the limitation that if you are writing a relatively long program because you don't have any inherent link to recursion that would allow you to compress the the size of your proof you're limited to a certain size and then there's also the the disadvantages we mentioned what would an example be that we might know there the the traditional description would be Socrates circum if you are not plugging it second is very much a front end so if you're not plugging it with a inherently

recursive backend the classical examples and then you have the the dsls that have some even some of those dsls that are doing direct competition are kind of true honing you into let's say their major or main blockchain of application right taking Leo and using it in a context completely separated from alio is theoretically possible but this is not necessarily what the tool is being designed for at the moment and then you have the VM models the virtual machines that have digital having disability of creating succinct proofs independent when they have

recursion they have the disability of creating small rules but they are in many ways relatively heavy weight and bring in a modalization for the ones that are ZK EVMS of the data model of ethereum that you may or may not care about yeah regular model of it ethereum is great don't get me wrong for a certain class of proofs but if do you care about Patricia trees if you're doing image manipulation maybe not and an example of that I guess would be something like Risk zero right ah so risk zero is one of the very few generic virtual machines oh so what you mean then is more like the ZK VMS something like maiden so this is EVMS specifically Maiden actually has a

claim to generality okay but um but my internet and Reserve uh indeed generic VM so they might serve your use case you might do image processing with them that might work but they have a different Traders and the most fundamental one is the idea that there are those low level VMS and so you're a little bit further from your proof instant you don't directly program in Risk 5 assembly you don't directly program in my donation which is very much part of their value proposition the idea of selecting the risk 5 instruction set is to say to everyone that wants to hear that you're going to compile jewelry Theory but at the same time that comes with

consequences so the most obvious one is that the proof that you obtain as a cryptographic artifact at the outcome of this is a proof that has been made on the input language of those virtual machines so if you're making a proof with resero you get a proof on the risk 5 in construction set so it's the proof is about the risk 5 assembly that may be something that you're willing to audit and that may be something that includes no errors but it also may not that is if there is a bug in your compiler from your Source language whatever it happens to be and compiling into risk 5 assembly then that barge me let's say remove some

statements from your original program and there may be something missing in your proof of course I'm speculating um I am not saying that this is the case for a particular cases but I want to highlight a more interesting thing which is that if you're going to write directly in this in learn you have the advantage of having a noticeable program in which you literally write down your proof intent this is what I want to write a proof about and you get a diary proof on that and nothing else yeah I want to jump in there because I think this is an important point when you think about what the future of zero knowledge proofs and the data they operate might look

like because we're still really early in this but if you think about the dream of content address data like we have file coin and a universe of data that people want to make proofs on and manipulate there's going to be more and more uh zero knowledge proofs at the application Level and it's really important that there be a lightweight way of doing this that people can understand like with filecoin we had kind of the luxury of taking a really long time to write these proofs and they're very heavy and they had to be audited Etc but what we really want is just I as a regular old programmer get up in the morning and I

need to do something and I write a little program and I have the data available to operate on I give you the proof and then that's sort of good forever and the really interesting thing about lurk is that lurk is just sort of a Content address data language that's very expressive and it's directly interpreted by the lurk proof circuit so for example if I want to prove to you hey I know of some data such that if you perform this mathematical function on it you'll get some other results I can just write that I just write that down in the simplest possible way as an expression

tree and that's really all lisp is it's just a way of describing an expression true and I can say this is the case and here's a proof of it and the nice thing about that that artifact is really durable I can put that on ipfs I can put that in file coin I can put that on ethereum and anybody who can who can hash that expression and check it can say oh this is a proof that that's true so there there's no Assembly Language involved nobody is decompiling this and saying you know is there a bug in you know this Assembly Language or something interesting you're telling me that you will know of a number such that number times 7 is 56 and I'm saying yes I did

and you say I can't imagine what that number would be but I trust you because you have a proof you just sort of mentioned the interaction with some of these other blockchains and stuff but like would someone create a VM with lurk that then lives on a blockchain what you just described about like how you can you know you can look into the blockchain maybe prove something from it but like how does it connect to an actual blockchain and which one are you focused on you mentioned filecoin and stuff like that but like yeah so there's two aspects of that and and there's the simple verifier and then the contact addressing and I'll let you may talk to the the content addressing but the simple aspect is there's no need for a VM and this is really important you just

need a simple verifier contract we produce proofs that can the reasonable Assumption of choosing a back end are simply verifiable on chain for a modded cost the aspect that is interesting is that we are therefore not assuming that you need a VM and yet because we are micro VM we give you the those inputant advantages of recovering a computation model that is intuitive to you um stands on a number that is not prime you should just pay the price of a few iterations not the entire sequence of operations it's important if you look at Decay

bridges for example and we are converging towards basically relapse Centric architectures on every other blockchain today every other blockchain is at the moment focused on how do we build a roller SDK run up sdks fantastic they let everybody develop their own new rollup but every new Rob every n plus one scroll up that is successful immediately creates a need for at least n Bridges right because now everybody wants to bridge to and from their local blockchain or their local work into that neural and what are we going to use for that ticket Bridge either we use the multi-6 bridges that are what they are and have led to

the amount of hacks that were well aware and that have a security problem or use actual DK Bridges cool we can either Define those using the direct competition model we've had so far which means find six stop cryptographers and and close them into a cabin in the woods until they come back with the second definition of your light line protocol good luck with that or we adopt something recursive a VM model but if that VM model is something that is that low levels only we're getting into computation modalization of the data model of the uh of the chain and that gets a bit complicated whereas if you have a quick skirting language that goes a lot faster so you can prove off chain

Define a list program and then put the verifier on chain on any chain where does the prover actually live in this if it's not you sort of mentioned it could be off chain so where does it actually live right so the the nice thing is it sort of doesn't matter so this is a practical question what we would like to see is cheap and efficient proving services that can make these proofs for you and which one you want to use it likely depends on what what kind of contract you need with them how much privacy you need now we want this to be efficient enough that if your answer is you know the only person I trust to make this proof is myself then you say okay you know buy yourself a nice computer

and make the proof at home but once you have the proof that artifact itself can be verified anywhere but we'd certainly like to see you know a centralized or maybe decentralized network of provers that really get down to the basic cost of making these proofs which is is not going to be that expensive because gpus are cheap uh if we have enough success Asics will make the proofs even cheaper the nice thing is that given the way that Nova works and everything else we will be able to in a future version of look separate out the parts of your proof that are truly private that I want

to take advantage of the zero knowledge properties versus the parts where you know I don't care anybody could make this proof for me and I'll get it at a very low commodity cost and uh the next thing with that is that we also aim to use all the efforts that we as a species have all involved into writing very clever circuits the fact that lurk has a design that is moving away from circuits is actually not a bad statement about circuits circuits are useful for some things in particular I mentioned that lurk has a universal circuit um and when I said it has a universal circuit I'm not lying it's a secret right we've wrote One

um so we would be ill-placed to poo poo circuits circuits are very useful when you don't care so much about the developer experience but you really want to squeeze out that every last bit of performance you want to describe your operations in a very minimal fashion and we have integrated that in the language that means I told you lure has a universal circuit it is a dialect of lisp that is evaluated entirely to one single tiny Circuit by the way our circuit is 12 000 constraints approximately we're talking about half the size of the circuit of a shot 256.

it's really really tiny but if you want the list dialect that we offer you to have very efficient operations for a few interesting functions that are key to your use case well you can write a second for it making it a bit more performance squeezing every last piece of performance you can use a 1ts today we have this notion of co-processor that you can program the lyric circuit for in order that those functions can be interpreted in the language using your secretary your plugin of course it requires a little bit of setup in your

proof but basically if you've done a lot of work using at the moment Bell person definitions of the of your gadgets and very shortly second you have the ability to reuse all that work for a very cleverly designed circuits and have it available as a native primitive of the language so you have lurk the universal lisp dialects and then log Prime log seconds Lurch new favorite customized variant of lurk that also happens to do let's say image transformation or hash functions really really fast there's a model that people are probably familiar with for thinking about this which is um the way

that most python programs work that need to do something non-trivial uh you have python which is a language people like it's a high level scripting language and then you need some performant piece and you have a library and that's written in usually C plus plus and from the python programmers perspective they've never left python they're just still writing a simple clean easy to understand program and it can be audited in that way too and then if you've also audited or for some other reason trust the backing Library you get the performance of it for free so we're early in support for this mostly because we don't see it as a

very hard problem like everybody already knows how to make these performance circuits we know that it's very time consuming and difficult it needs to be audited very carefully but it works really well for the problems it works for look just lets you plug those in you can just we basically think of it as an ffi of a Python program with the c plus Library we say just pretend you're writing in Python here but we'll give you the performance of the C plus so if we wanted you know the circuit for shot 256 we just take one plug it in and write a little wrapper for it and that's really our model but the thing that's

most interesting about this because of lurk being a language is that in the future we're going to be able to compile custom circuits from the lurk surface language into efficient circuits and this is going to be the thing that actually cuts down on that development time and gives you both sides of the picture but that's that's a little ways off that comes from my experience with deep learning Frameworks where I've made the number of C plus programmers that had this Joy and contributing to deep learning Frameworks telling me my specialty is really this difficult back-end language but when I integrate that into one of the numerical backends

of a deep learning framework it makes my work more relevant to a much larger class of programmers we don't want xenology proofs to be owned by cryptographers forever but we do want to give them the joy of making their work in writing a specialized circuit relevant to a much larger class of food programmers neat I want to ask about the lurk ecosystem or the stack you know we've talked primarily about a language but you did sort of talk about it potentially having these other dimensions so what is maybe not what it is it is today but what is your plan for what this looks like do you sort of follow

some of the other DSL models of getting I don't know lots of tooling built around it or yeah how are you how are you approaching this project and and yeah what's the sort of roadmap Vision the very nice thing about lyric is that it has this very small footprint between the proof intent your program and the actual cryptographic proof there are very few things that you need Assurance on to make sure that the entire thing is completely secure so what we're actually working on is formal verification of the entire lurk stack I was about to ask that actually crazy okay so basically that means that we have already run through an audit of our lyric circuit which is religiously small and that

we're very confident in and the nofacial base is a very high quality uh quit base led by srinath but it would be even nicer if we had a tooling based formal verification of the entire stack and its small size makes it amenable to that in the on a reasonable timeline when it comes to tooling one of the nice things that we can import the existing tooling that exists for lisp um this is very nice when you want to work with an Editor to just have everything set up already but of course we can take things a little bit further lisp is really the core abstract moral language of what we're developing but we

also have empathy for the 17 million JavaScript programmers that are at the moment working with JavaScript and it turns out JavaScript has these such a strong Parenthood to list that it is one very small transpilation task away from Bliss meaning you take place you remove all the parentheses replace them with scoping rules out of three brushes Tada you have JavaScript what that concretely means is that once we have this transpiration Dom and ideally verified suddenly we have this high level language that is entirely verified and that you can have exceptionally strong assurances on that can power all of web 3. we built web 2 with JavaScript not

assembly languages and the idea here is let's try to be build web 3 with like JavaScript rather than assembly languages that might absolve us from levels of complexity we don't necessarily need this is small and beautiful and ideally in the very short future formerly verified let me try to describe what I think is the most important thing about lyric the most important thing about lyric is that it just happens to create a whole bunch of Rhymes that are inherent in how lisp works and how content addressing works and in the needs of zero knowledge proofs and the really important thing is

this identity between programs and data because in web 3 we need to have everything exist as immutable data so we can content address it and lisp takes that as a given and so lurk lets you take data that's in the format that it needs to be in in order to work in this world that we have and do nothing else to it and have a well-defined program and the nice thing about lurk's actual technical design is that you don't have to follow these content addressable links or pointers any more than it is needed to evaluate your proof this is

for the prover and for the verifier uh whoever is having something prove to them they don't need to follow them either so the the prover can hide Secrets inside their proof they can say I know of some data that has these properties and you can absolutely believe that and we think that the proofs have some really good properties computationally but what's more important really is that what we need if we're going to build up a huge Universe of content addressable data that proofs can be made over is that data needs to be durable it needs to last for a long time because producing it is expensive

and you want the proofs that were made in the past to remain valid we want a corpus of you know data that grows forever and that we know things about uh and so really lurk is a data language first and the fact that you can make proofs over it kind of completes the idea but even even if it were to turn out that lurk proofs were not the best way to make proofs you would still need a data language like this so really for us the tooling and the ecosystem is about trying to get that language expressive enough that we can build the future on it and if eventually it turns out that uh there's some better

way to compile alert programs you could say fine then the alert proving part isn't as mature as it will be but we want to get that language right uh and that's why Francois was talking about JavaScript and you know we realize uh the world has kind of figured out a way that it likes to express these kinds of things we have JavaScript and then we have Json right like it works for people and moreover lots of the world's data is already like that so we're kind of leaning into that so we see the tooling building up around that how do we make uh it possible for regular people to express their data and write programs over that data in a form that's actually useful and if they can get proofs out of

that great yeah so that's kind of the road map how can people already interact with lurk and what are you on the lookout for as well from potential contributors or maybe other works that are coming up so when it comes to uh lurk we are at the moment uh making sure that alert is the right language and that means we've talked about JavaScript we've talked about co-processors that allow us to reuse circuits we are extremely welcoming feedback from users that at very specific spots they care about particular features to be available in the language but at the same time we are in the core business of

making sure that lurg is the best programming language to stand up over a recursive procession which means that we consider the recursive proof system to be Community good it's not necessarily ours we want it to be state-of-the-art for everybody out there which means we contribute to the srinas Nova project and we will for sure keep contributing and extending that project but that we also would like to Federate and help a bunch of people that are working on the absolute Deluge of work in that area from Supernova and CCS this new

arithmetization from srinath and and Riyad rabi and Christine Taylor hypernova which is this new work that is addressing how to do Nova based on high degree Gates but we've also helped Nicholas montblad working on sangria for adapting it to plunk until hypernova made that work obsolete we've noticed the Fantastic work from espresso system on protostar yeah and the experimentations of the Privacy scaling equations group in making Novara proving parallelized paranova I think is what they call that indeed and this is super exciting so so here we're just looking to be ourselves nice collaborators that

help make sure that all of this work basically evolves to some sort of engineering for choose folding and game by which we have the absolute best software shooting that allows us to make efficient and very generic proofs if you like lisp as well we have a standard library for lurk that could take a few contributions we are really thankful for the contributors that have already worked on alert the glow and you can team that has worked on compiling a smart contract GSL into lurk already we've had a help from Nita Amin programming languages

researcher at Harvard that has helped us figure out the intricacies of Reflections and macro systems in lisp with ourselves from lurk Lab at our profusion with yatima which was initially team focused on the lean theorem prover and that is of course extremely valuable for uh formal identification effort but it also means that we have empathy and care for the improving community that list is bound to get bigger over time and that is extremely exciting for us cool well thank you to both of you

for coming on the show and sharing with us the story of lurk explaining a little bit about lisp for explaining to me a little bit about the lisp history and um yeah thank you so much to both of you thank you it was a lot of fun thanks for having us on we appreciate it that was really really fun cool I want to say thank you to the podcast team Rachel Henrik and Tanya and tour listeners thanks for listening thank you