ZK9: Lurk: Lambda the Ultimate Recursive Knowledge - François Garillot (Protocol|Lurk Labs)

Transcript

foreign [Music] we have our next talk coming up here we have a Francois uh did I get that right probably not um but he's gonna be talking about lurk so Francois here in the audience feel free to come on up to the stage and we'll get started oh you're right next to me did I say your name wrong all right it's fine all right okay all right let's all welcome uh Francois everyone [Applause] hi let me see if you can all right

um so it's great to be here uh I won't bore you about too many years I'm Francois I'm an engineer work at work labs you can find me on Twitter for as long as that platform continues to exist I'm gonna talk a little bit about zika proof languages um and I want to motivate why the hell would somebody try to start to even stop thinking about writing yet another Ziggy proof language in 2023 because there's like four examples on these slides but there's actually many many many more that I'm not even in there ask anybody from anuma they have

an entire stable of them at home so um to do that I need to go back to what it means to try to write something about circuits they are Sim okay so this is not the best line to present our CS comparing competition but the idea is you want to write a proof of f of x equals y um It's actually an f of x and W because you probably want hidden Witnesses in there and you're gonna have to run through the traditional transformation into uh r1cs or qap and then pass that on to your cryptographic backend your goal is to write that circuit that corresponds to your computation

and the traditional way of doing this is the direct complete compilation approach you try to think about your Source language your Source language as primitive types some control structures and some operations and you try to write an arithmetic circuit for that okay so that means you write small combinators that represent some of your control structures you place holes in there while you're up your circuits small combinators for your operations very straightforward you basically go through your program not line by line but AST type by AST type and then produce a circuit that matches that one to one right

but there's a couple of problems with that one of the problems is that one of the main problems is that your compilation Target doesn't work with you r1cs is a bit of a pain in the butt in that it's completely flat which was the point of the of the previous the point that was maybe difficult difficult to capture on the previous slide which is that um there is no notion of control flow one of the difficult not impossible but kind of engineeringly difficult ways of representing things in r1cs is representing branching let's assume that you do something that the involves a division but you only do that Division if some condition is true

if the condition is false do you care that the division is by a number that is zero if you have a division by zero in your ones yes that's a motivation for your prover to immediately stop and say hey I encounter the division by zero that stuff isn't defined as a problem here if that was a non-taken branch in your Source program you don't care so now you don't have an error in your own CS in your proverb but that requires you to go back to your ones yes inspect the branch and see which branch you have taken except by the time you have our once yes you no longer have the ability to move like that in the AST because I want CS again it's completely flat

another problem is that you don't have branches you have sorry you don't have loops you need to unroll on the loops now that's not a real problem if all the loops are unrollable if you could go through a loop from 0 to 100 well okay there's gonna be a hundred times the subject for the loop right but let's say you want to represent this so this is lisp yes I'm making new release but come on it's five lines this is a thing that is just looking at it looking at an integer saying if it's even if it's even it returns n over two which is good because it even that's the

thing you can compute otherwise I reach on 3n plus one that's known as the Syracuse recurrence now does that stuff converge it turns out that if you try it at home on small integers you'll find that after a certain number of steps and over two three n plus one three n plus one and over two that kind of thing you will converge to one does it always converge to one we don't know that's the subject of the that's why the name of this function is collapse it's the collapse contexture that this function uh always convert the iterations of the the Syracuse recurrence always converge to one so this function can times you need to need to grow recurrence to convert to one

right now don't get me wrong there's a very nice theorem that just says that I want TS has full capable calculability expressivity you can Implement your turing machine with your r1cs which means that for any instance of this function you can produce an r1cs circuit but you can produce an r1cs for the function you can't represent that function in open form in all the time big otherwise you've solved the Collette's conjecture in which case like why are you in this talk and not collecting your million dollar price okay so we we see the drawbacks and to what that concretely means in terms of

engineering terms is that I need to have the whole trace of my program in memory which is a problem because a I need to generate that Trace in I want Cs and like you when you evaluate a program you don't generate the whole Trace you don't keep everything in memory you just have the current cash that you need to see the current state of your program the second is now you need to actually have that in memory which means if you need to have approver that approves arbitrary size programs you need that program to be pretty big if your smart contract is huge and more importantly if the trace of your smart contract is huge you need all

that to be pretty big so let's look at one of the ways of thinking about updating staging memory and then we're going to connect that to how you write your language in 2023 so IVC is incrementally verifiable computation it is ID that okay if what you really want to prove is a thing that is an iteration of the same function over and over again well you don't need to have the whole trace of the same function over and over again in memory you can verify the correctness step by step and typically the way you would do this in a way too strong of a paradigm

than what I'm going to to use today is you would recursively verify the correctness of a proof that is given to you at the prior step produce a new proof and then pass that on to the next step now the fun part is that um we have a very good iuc candidate that works a Heckle of a lot more easily called Nova so Nova says hey you know what that whole idea of having each step generator proofs and then you eat the proof of the prior step you verify it entirely that means verifying a snug within your circuit so you write the r1cs or verify in your snack that's great but it's a

bit costly and I don't like things that are costly or more exactly not that doesn't um so that's the the idea of this iteration of the same function here we're iterating F receiving proofs at each step and in step by one I verify the proof of Pi zero and then produce a new proof that will be great but you can actually go faster you can just fold the proof you generate an r1cs instant that is equivalent to both the folding of the prior proof and the new increments that you're trying to produce at the current step and all of this folding arguments is

really cheap we're talking about 20 000 constraints so that Paradigm IVC in general and Nova in particular Lee gets you in a place where you don't have to have the whole trace of everything in memory but at a cost which is you have to have a natively iterative form to what you want to prove what you want to prove has to be the same function repeated over and over again turns out languages are a little bit like that let's dig into this so when you define a language one of the usual ways of doing it is to give it an interpreter you basically yes Define the syntax in your AST but that's not enough

you have to explain okay how do you reduce the DST and how do you compute what that language is supposed to Output right it turns out that the definition of interpreters in people that are in PL and compilers have standard correspondences with how to write some VMS and in particle that have by code and Abstract machines at least more generally in order to get to that result more specifically what I'm trying to get at is that we Define yeah we Define languages using abstract machines so if you think of an abstract machine you've probably encountered thousands in but the idea is that stuff

has is represented with a gray with a graph which nodes are states of JavaScript machine and it has Arrow edges that relate different nodes that allow you to relate with those States looks like and it turns out that in the top of this diagram you're going to see most of the semantics we generally use to define languages and you'll see that those translate in completely standard ways to abstract machines so what does that tell us it tells us anytime anybody is sitting down to define a language whether they know it or not whether it is the formalism of what they're doing in most cases what

they're doing is writing a freaking abstract machine already natively for a very large class of languages that's cool because abstract machines are nice abstract machines have a natural formulation in terms of something like this and if you are not in programming languages this is scary if you are in programming languages this is your textbook the fun part is that abstract machines have this natural expression of what their step function is that is okay I've just received on the left here some term of the source language along with some

elements that represent the state of my abstract machine here we're looking at the cek machine and the cek Machine is the standard abstract machine behind a standard implementation of lisp and it has rules that allow you to rewrite whatever you you wherever you are in your analysis of the source into something that is more elaborate on the right it's called cek because you have a control term which is the term of your language which is in the in the syntax you see on the top and it maintains an environment and then a continuation for whatever you're going to do once you have locally you're locally finished

reducing that portion of your language what is cool about abstract machines is they have a step function that is all of those ideas that you can take to move from one state to another of the abstract machine that itself is a small program it tells you okay if you receive a term in your soul your source and if you are that particular moment if you have the of of the evaluation of your language you can progress to The Next Step using one of the rewrite distribution rules that you see on this slide so what I'm going to claim is that lurk has respect that fundamentally is as easy as that more exactly it's as long as that

it fits in one freaking slide and this is a micro VM because we can directly plug it into Nova so the architecture of lurk is that simple it is a micro zkvm that just has the stepper of a CK machine inside its unique circuit executing alert proof is stepping to a CK machine stepping to a CK machine is evaluating the list program so what do you do now if you want to do this but you you'll tell me well I have various programs and I want to compile

those programs for once yes no no no you don't need to compile your programs to or once yes past those programs are as inputs to the standard evaluator of your language um that's not an evaluator runs through its steps and then once it has enough steps you just send that to Nova to fold and suddenly you don't need to have the entire trace of your program in memory suddenly you can natively represent branches because your program will not go into branches that it doesn't need to go in your evaluator won't go there so those proof steps simply disappear in

the path of the logic of to your interpreter suddenly you only need one circuit I do mean one circuit that circuit is universal it can take any risk program any inputs for that list program and evaluate it that stepper is Tiny it is in fact so tiny that the natural ID that we had initially was hey you know what we write a stepper circuit and if it's small enough well it's only going to be slightly bigger than the Nova recursion overhead which means we're going to run one step or one step of the separate stepper one step of the abstract machine

for one step of Nova and then we can fold this and then only we need to fit in memory is really what it takes to evaluate one step of the circuit turns out we're under the Nova regression threshold our circuit is well under 20K I don't want to make commitments because we're going to add stuff to the Circuit to accelerate some cryptography but we're gonna add stuff that has nothing to do with the freaking lisp right we can also commit to functions so we we have a central notion of commitment supported natively in the language

um the the commitments of course did not have this size it wouldn't be cryptographically secure we're using standard post Aid and commitments it's just that distance commitments are tedious to read on slides so I'm going a little bit smaller here but um we have this ability to we have a rebel that will give you the the commitments for your particular programs and that means programs can be standard you remember it was a bit difficult to represent the in open form the function that represents the the collapse recurrence we're gonna come back to it you can open commitments along your proof um and you can open that to non-uh deterministically provide

openings for for particular commitment to programs and so what that means is that we're in fact hashkinsing all the things is just giving a unique hash that allows you to compute structural equality between two terms of your program without having to go through the full term right um we hash all values rigorously and maintain a store throughout um the the the the deployment of the proof um and so that gives us a quality semantics between programs or between inputs at a very cheap cost so

we can Define functions we have no problem um defining functions in open form and then reusing them whenever it is needed we also have functional commitments so you can commit to a particular particular function and then want to approve that Express itself in the terms of the function that has this particular commitment would pass those inputs gets you that output and then we can even do things Express things easily that look like functional commitments like higher order functional commitments you can have a particular data interface

that says that hey if you I can take my particular data I'm committed to the data and then I can take any function and then apply that function to the data and get you a proof of what the output looks like so that's kind of cool um it lets you prove that you've run the function that a client gave you um onto your own data okay now one of the interesting parts of this is that this is just a bit beginning lurk is doing a release called when zero Alpha we have a blog post a preprint we

have more we have a spec we've already audited we have a tutorial and you should definitely look up the slides to get access to all of this but the summary if you remember nothing else out of this presentation is that a lot of languages are natively defined as abstract machines we have new paradigms for IVC for record recursion like Nova that allow us to make that sort of recursion um extremely cheap as long as as we understand how to natively express our computation as iterated computation whether or not you like

um list like languages and I hope you do it is certainly a heck of a lot nicer that than on our NCS language but the general argument for what we're building carries to so much more it carries to essentially any functional like language um that you can define an abstract stepper for an abstract machine stepper four um and that would include JavaScript for example um you can then have a micro VM that has none of the limitations of r1cs and that at the cost of taking a little bit of care for what hashing looks like in your language definition can be content

addressable you can publish interesting modules online and then reuse them in a vast library of stuff um we are also on Twitter in zulip and are happy to discuss all of those topics at any level of nerdiness that you're interested in um and feel free to reach out [Applause] awesome Francois thank you we have time to take questions and thanks for the great talk this seems to be very powerful technique do you

have some maybe some some numbers to give us a sense what are the costs like either comparing to Native executions or to other ZK languages um we are working on those benchmarks um we so comparing to Native execution is not um a we're hoping for a smaller slow slow down than most of the other systems it's going to be difficult to beat stocks at their own their own game therefore for the proving time at least um but the the general idea is that

um no we don't have those benchmarks the only cost you're paying so Nova noval really does and we're folding a relatively small circuits the number of times that we want at this stage our circuit is small enough to run several steps of the of the reduction inside one one step of Nova um so we're hoping to be uh minimal overhead compared to Nova uh to the best Nova benchmarks and the best benchmarks get a get out of one million constraints which would translate for us into close to a hundreds type of our our reduction uh

into um 1.1 seconds so dude but the difficulty in those benchmarks is to have programs on which we agree on right because the reduction is program dependent um everybody is testing that with chat 256. um we have a problem which is that if we Define Shadow 56 in language without acceleration of course the performance is going to be terrible because we are going to represent bits fundamentally with field element um so give us a little bit of time we're going to come with those benchmarks and show where the real science of this are after we've defined a couple of

cryptographic accelerators okay thank you and but maybe do you have some sort of showcase application you envision that will be possible with like the sailing of those techniques like what kind of applic what kind of function I could compile with that and then run in like yeah so the the the functional commitments is the one that we we put forward because it's absolutely trivial so the ideal functional commitment is to commit to a function the traditional example is a credit score function we chose that okay here's your result of your credit score I'm not giving you all the inputs but it has been committed to

with this transparent function when you can be sure that what I'm giving you is the result of your the standard algorithm for the credit score so your credit score has been completed fairly now the interesting part about this is that the original work on functional commitment by Dan Bonnet and others uh is um only could assume the definition of the function in now once yes and in a 1cs you're really looking at relational calculus so you have plenty of problems with the idea that okay you're defining the relation that defines the function and they're reusing IDs from holographic proofsalamalin to to that Define indexation relation in there to commit to this relationship they had to add

some very clever proving to add that this was defining an actual function that is that the the religion only has one output on the right and that's really difficult and creates a lot of constraints that do not need to be there when you're simply evaluating your Source programming language when you're defining you're evaluating your Source programming language your freaking parser is implementing that this is a function although definite the semantics of your language um so for us this is absolutely trivial you can go from zero to um I've now made a proof about my credit score function um in an afternoon um

the previous generation feels fast on our machines um you're gonna want to know more than that I understand you we're building this give us a little bit of time awesome I think we have time for one more question here um so how easy is it to extend let's say I wanted to use um you know some exotic cryptography in my program maybe a different type of elliptic curve you know middle of this message uh the middle of this encrypted message is a certain character proofs and things like that so

um how do you how do you extend it yes so that's a very good question thanks a lot um so remember when I told you that the idea of Nova is that you're repeating the same function over and over again that's completely true of Nova but that is not true of supernova also excellent work from Serena seji that allows you to customize which circuit you run on each step of your folding so you can have a handful of circuits some of which are your list pay valuator standard and some of which evaluate r1cs functions that are quite a bit faster

and so the nice thing is that there are there are several answers to your question that are all positive one is if you want fancy cryptography you can have cryptographic accelerators built into The Language by representing them classically as circuit and we have had one example with the Spartan the cdsa talk a little bit earlier in the in the breakout room like an Argo um so you can define those accelerators in r1cs join them to be supported natively by the language and then have those proofs been be represented folded

in Nova there's no cost to this the you can use your green blue and red f in there except you have to pay for the um on each folding you have to pay for the the cost of the largest of the boxes that you use um so that's when we're building those cryptographic calculators they will be there soon uh send us money Engineers or whatever um and and we will we're definitely building this the um if you want to talk later about sending us manure Engineers I'm fully available um the second answer is uh the only thing that Nova requires at a basic

cryptographic step is a pair of curves so it needs a curved cycle that curve cycle does not need to be pairing friendly so um palaces Vesta will work but if you are interested in doing that on ethereum for example um doing this with grumpy grumpkin as the curve cycle will grow work as well um we don't have gramkin implemented in code base right now but again our code base is fully generic in the the fields that we use so that would be relatively easy to imply to to in um again Engineers open source contributors we oh yeah all of this is open source and

available today in in repos writing a small programming list generating a proof um and and measuring how much it feel how fast it feels on your laptop is a thing you can do today so uh thank you very much let's give Francois another hand thank you very much