ZK11: Make Lurk Work - Chhi'mèd Künzang

Transcript

[Music] so this is supposed to be a lightning talk uh I will Pace it accordingly I don't know who made these slides uh don't look at them too carefully so uh my name is Chim Kong I'm the creator of the lurk programming language and I work at lurk lab lur is a zero knowledge programming language which means it's possible to create succinct zero knowledge proofs of program evaluation we do this with snarks uh as a review statements to be proved in snarks need to be represented as arithmetic circuits if I want to prove that for example 7 a^2 + 3B plus C = D I need to express this in circuit

like so so unfortunately if I want to create a single circuit that can prove any arbitrary turn complete program evaluation it would need to be a really big circuit in fact it would need to be infinitely large since there's no guarantee of how long a program takes to terminate or even if it ever does uh so the progression I present in this talk is mostly about how we take advantage of a series of cryptographic improvements to progressively refactor our circuit into ever more efficient topologies so remember that the notional starting point is a single monolithic circuit so lur is a lisp IT addresses

one part of the circuit size problem by representing programs as symbolic Expressions we use hash consing with cryptographic hashes to construct source code graphs and the result is small Merkel routs that can be unpacked as needed as a computation progresses this allows us to structure evaluation of any expression as a sequence of short bounded reductions over uniform small IO so the resulting circuit is still concretely large but our design has factored that very large circuit into a Rel relatively small one I called it a mediumsized of about 11,000 constraints this smaller circuit is then repeated many times as needed to fully reduce an

input expression to an output expression so the especially good thing about our factorization of lur reduction is that it gives our proof the shape of IVC incrementally verifiable computation this allows us to use a folding scheme like that provided by Nova to compress the many repeated steps into only a single circuit instance whose satisfiability must be finally proved not only does this make for a small proof the folding process itself is also much more efficient than proving each step in a snark so this provides efficiency in time space and communication unfortunately not every computation can be performed efficiently in raw lur for example if we wanted to

compute uh shot 256 by implement it in lur directly the result would be very inefficient we would require lur iterations for every operation and remember each lur iteration costs 11,000 constraints and that would be big to the big uh so very very many repetitions to lur reduction for even a single Shaw 256 uh fortunately expressing sha 256 efficiently in a circuit is already a solved problem if we could just use an optimized R1 CS implementation that would be fine so L's goal is not to replace accelerated cryptographic implementations but to interoperate with them seamlessly allowing for safe expressive d dnamic highle application development fortunately Supernova a

later development supports non-uniform IVC and we've implemented this in our RSB Fork of Nova what non-uniform means here is that each step can fold one of many distinct circuits with all the same benefits of ordinary folding uh this allows us to support computations that require the lur Universal reduction circuit and arbitrary custom optimized circuits which we call co-processors so think of co-processor is like an ffi that lets you code in Python but call out to C++ for performance unfortunately Nic alone does not solve the whole problem you can think of the larger problem as one of efficient packing taking a step back let's consider the overhead imposed by folding itself since the lurk circuit is

quite small if we fold it naively the cost will be dominated by the recursive overhead folding recursion is actually about twice as expensive as lurk reduction itself so we solve this by repeating the lur reduction many times in one circuit increasing circuit size but improving efficiency by amortizing the recursive overhead ni nivc puts a wrench in the gears though because non-uniform circuit folding still happens in a step-by-step manner so consider what happens if we want to prove shot to 56 three times interspersed with the lurk reductions grouped in a single folding step circuit now every time we want to insert a shot 256 proof our sequential lurk reduction is interrupted and we forced to use three blocks of lur reduction when we

really only needed one this is inefficient lookup arguments come to the rescue in particular we use the log up technique implemented directly in our R1 CS circuits this allows us to quer a sha 256 Oracle non-deterministically so our sequential lurk reduction blocks can proceed uninterrupted and therefore complete efficiently then we prove the results on which we have depended in independent co-processor proving blocks we call this technique memo set conceptually we maintain two sets a one record results One records results we have assumed and represents a to-do list of statements that must still be proved the other record statements we have

proved for a final proof to be valid we need to demonstrate that everything we depended on has actually been proved log up lets us Pro this efficiently so this provides a significant upgrade to our co-processor solving the packing problem because now we never have to waste Space by discarding reduction circuits we can now conceptually call into co-processor circuits from anywhere in fact this technique makes it possible for co-processors to call one another from within their bodies we call this upgrade co-routines by their nature co-routines support arbitrary Mutual recursion and are memorized any co- routine quer is proved at most once so now we can efficiently Implement arbitrary dynamic

programming problem s however this incredible power comes with a potential soundness problem because co- routines are so expressive we can use them to express and seemingly solve impossible problems for example a function Fu that calculates its value by calling itself with the same input will never terminate in a real computer if we're not careful the co- routine query production method would allow us to First choose a solution then rely on that solution in its own proof resulting in a circular proof of what should instead be a non-terminating program and this is not good uh so the solution is to forbid cyclic computation in other words the

co-routine dependency graph must be a dag a directed acyclic graph it's okay for a co- co- routine to call like a different instance of itself but it can't call the exact same instance in a cycle so if Cycles are permitted the provs afford a non-deterministic choice not only is this computationally incorrect it also subverts our goal that it should be possible for arbitrary lyric programs to have deterministic results we solved this problem with what we call Providence whenever we prove a statement in the memo set we must also include its Providence Providence is a list of dependent Oracle queries and their Providence because we use hash consing to represent the Providence it is impossible for us to produce a cyclic

graph therefore any provably constructed Provence is guaranteed to be a dag and absurdity is forbidden remember that I said the lurk circuit is mediumsized one of the big problems is hashing as mentioned before hashing solves real problems for us I didn't go into the independent benefits of content addressing but it's extremely valuable that lurk iio allows for arbitrarily structured potentially private fully committed data however our uniform treatment of this hash conon data obligates us to perform a lot of hashing internal to reduction itself this makes us sad because even cheap posidon hashing is somewhat expensive good news now that we have co-

routines we can eliminate internal structural hashing without loss of expressiveness when a structural hash would not escape the computation as the case for the majority of the hashing the lur circuit performs we can instead perform a memorized allocation apart from the low co- routine overhead this only costs one constraint to increment the allocator address pointer note that this has not come with a security cost in fact these memorized Constructor allocations Implement a form of right once memory because addresses can never be removed uh or never be duplicated this is even more Collision resistant than the best hash for similar reasons this means we can replace the Providence hashing with allocated conses while still enjoying the constructive

guarantee the Providence be a dag look ma no hashing um now the lurk circuit can be small so we still use hashing for Content addressing but lurks content address data language is strictly a feature the important point is that now we pay as we go hashing on demand and only exactly as lazily needed either for external input or output so what's left to do we can apply a similar co- routin technique to further atomize the lurk circuit itself this can be thought of as the final step in a long process of breaking Universal

computation into ever smaller steps that can therefore be optimally packed into proofs this long process has expose the dialectic tension between the efficiencies provided by uniformity which allows for folding and the benefits of heterogeneity which allows for optimization due to specialization and minimization co- routines are lurks resolution to this tension they effectively allow instantiation of virtual circuits whose size and shape are non non-deterministically chosen by the prover as a solution to the optimization problem presented by each Dynamic computation expressing the lurk reduction itself through co- routines will finally let us reach our goal from medium to small to

Tiny so we know what we have to do and all there remains is to prove it I finished on time oh oh by the way uh Cod teams also free us from circuit topology assumptions and open the path to new and promising backends so we're also actively investigating plunky 3 as the engine to power the next generation of the lurk VM thanks [Applause] BR that was very efficient uh we have actually got a couple of minutes if you want to take some questions not really anybody oh no

um are there any we you can also obviously catch CH mode afterwards as well any questions okay we'll uh stay on time then thank you chid great