Next Generation DSLs and IRs - Panel
Devcon·Mon, Oct 9, 2023, 12:00 AM
Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on IPFS and more. https://archive.devcon.org/archive/watch/6/next-generation-dsls-and-irs/index We discuss the future of higher-level langauges and circuit representations with developers from a number of toolstacks. Speaker(s): Jordi Baylina, Ying Tong, Louis Guthmann, Brandon Kase, Kev Skill level: Beginner Track: ZKPs: Privacy, Identity, Infrastructure, & More Keywords: zk Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum Learn more about devcon: https://www.devcon.org/ Learn more about ethereum: https://ethereum.org/ Devcon is the Ethereum conference for developers, researchers, thinkers, and makers. Devcon 6 was held in Bogotá, Colombia on Oct 11 - 14, 2022. Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/
Transcript
foreign [Music] so our next panel is on dsls and IRS for ZK circuits yeah these are all um implementers and authors of some very popular CK dsls and IRS and so today we're gonna get together and um I've prepared a few high-level questions here I'm going to read them out um so the first one is sort of an exercise to locate each other on the language stack and see how we relate to each other and the second afterwards is to then figure out um to what extent can we share infrastructure or should we even try is it impossible after a certain point um and over here I want to note also a lot of Prior work from the compiler and smt verifier communities so can we also reuse some of their work and then lastly I had a high level question about you know what programming in ZK should look like what's your ideal DSL is it very different from normal programming yeah so just keep these in your head and I think I want to save maybe 25 minutes for audience questions at the end so I think let's start with a round of introductions um I have like I have pre-prepared some visuals for you um in case you need them so the first first one is pill Jordy so can you give us an introduction to what pill is a language mainly it's Bill means polynomial identity language and mainly what it is is when you define a circuit that's based on polynomials for example a Planck is an example of a way of um circuit that's based on polynomials but you can do much more things much more complex uh that's our base in polynomials that still allows you to just write those identities and then out of those identities just build the proof automatically the same way that you do in a normal uh zero knowledge language the same way that you did in circum you can do it in peel here you need to do something else because you need to maybe write the weakness somehow but it's just a kind of abstraction where you can just focus in writing what are the identities uh that you want to fulfill and yeah this is mainly what Spiel and Jordy also is the author of circom um which is a very another popular Library so how does pill relate to circom well bill is for polynomials and circuit is more for uh signals you're just working we are not working with polynomials at all you are just building uh um you have just signals and you just build constraints around those signals not constraints around polynomials so um the idea of circum is uh it's circum is a low level language because you can write everything every every uh every circuit you can write it in circum circum does not have any special library right it's better than you need any plugin special so all the circum is rated in circum so it's on there but at the same time is a high level language because it allows you connections so you can have you have blocks and and then you connect blocks even small blocks you do Big Blocks Big Blocks you do a bigger blocks and so in this sense you can go all the way down and on the way up uh on circum that's why it's so flexible and then it connects very good with snark.js and other proving systems and yeah it has been there for years has been already a full rebrite we now introduce uh introduced uh these new extensions of the language it's mainly um mainly our Anonymous templates and we also already are adapting to Planck circum was born in Darwin CS era okay and now but in Noble works perfectly in Planck so we have also custom Gates and yeah we're extending uh the language and it's a full community that's working on there thanks Jody so yeah to me it's interesting this um distinction between um a language for polynomials versus first signals and I'm gonna skip to Noir because as I understand it nor can Target both Planck and r1cs and air and even more back ends so Kev what's nor about um can you hear me yeah so Noir is a lot more high level uh it compiles it compiles down to something called a Sear and essentially you never tell the proving system how to do something you just tell it what you want to do so for example uh if you want to do a char-256 uh you don't tell it to use custom Gates the proving system just decides uh what's the best way to do it so in this way we're sort of back-end agnostic fully so for example you'll never see like uh custom Gates inside of Noir or any sort of that syntax or lookup tables you might see maps for example yeah so yeah cool um I'll just go around I have questions I'll just go around the intros first um so this is the picture I found for Cairo I really apologize I'm sure that better pictures exist but um this is the best either produced 100 um so um yeah so I guess Cairo deferred to um to some extent I wouldn't be able to actually go into I want to see friends but Carol is just during complete language so you were writing Cairo you were the same way you're writing solidity or in any smart contract language that you can think of so from the perspective of Cairo you write a program this program is completed to a carabite code which is run into the Cairo VM and prove among all the programs that are proven within the same proof so in that sense it's like there is not things much much difference you don't have things in there you don't have lookups you just have like um you know programming and sometime for some operations we do have this notion of built-in but built-in are just something you call as part of the function and the best for last kimchi slash snarky JS um Brandon hello um thank you yes uh so uh this is snarky JS with a Y different from snark.js had a few people confused this week um yeah uh you know name name might evolve I don't know um so uh yeah so kimchi is our is the proof system that snarky JS is built on top of uh right now um the way that it's built we can plug into other proof systems we just haven't yet um kimchi is the proof system that is in uh Mina or well in in the test net of mina that will be hard forked pending Community voting um but the idea is I mean kimchi is a Planck 15 type proof system it has no trusted setup it's Universal uh and uh we support like infinite and efficient recursion which is important for mina this is sync blockchain um but it but the cool thing is you can also use this proof system to build Uh custom zkps which are our smart contracts on Mina um and uh and you can build circuits outside of mina as well so uh I I don't know there's not much in this picture I want to explain I guess the the one really important thing about snarky JS you can see on the top left there um the the code snippet um it is typescript and is extremely high level language um and and there's this sort of uh I guess there's a lot of reasons why we designed it the way we did I'll just point out a couple things one is we get all the tooling and infrastructure and ecosystem that comes with typescript um so you know npm is great vs code is great all the Integrations already work and are good um and uh we think that you know when people are writing zero knowledge proofs or writing any programs like the model that people are used to thinking about computations is you know you have a function it takes some input and you produce some output so one of the things that snarky.js does is it lets you write your computations with your circuits at the same time and the output of those functions gets sort of fed in as a public input automatically for you so in the end your your code actually looks like normal code cool thank you so I'm gonna start with an opinionated question which is um what is what do you think of um intermediate representations so what Cersei is this project um that's inspired very much by llvm and everyone's turning to look at the screen but so the idea behind that is to define a common standard IR um to which many different front ends compile and from which many backend many different back-ends can compile so how well do you think your project would fit into a model like that okay like yeah okay yeah I'll start I mean yeah so so uh snarky JS is like I said like super high level um and right now it's directly connected to kimchi but um we could and probably should connect to some intermediate representation so that uh we can you know share that work of connecting to custom back-ends in the case of circum actually it exports to two different languages [Music] internally it has an intermediate representation already is uh second one so exporting that to other language like rust or like go is in the in the road map and uh okay exporting to maybe some other intermediate representation if it looks like uh good enough uh that's uh that that would be definitely possible here I'm not sure about the specification I have not read it yet but for example there are things that how you paralyze uh witness computation in circum we have a way that you have different components because there are components you can say that this component this company is is can be run in parallel so the windows computation can be run in parallel this is very important especially when you are doing big circuits so uh you know I'm not sure maybe some somebody that's explained that would that would be maybe an answer for for them but they uh sometimes there are details there that are not that that easy so in the context of Cairo um so it won't really even work um I mean because Cairo as of now doesn't have internet representation and directly by basically just a very high level you know like a bit like Seas representation just like compared to assembly and Carol itself Carol the current version at least to just directly generated by code that said Cairo we have carrier one coming in a couple of months uh and camera one has don't have something called Sierra and Sierra is within literally means safe intimate representation and the purpose of Sierra is to enable uh the language to turn deterministic actually so Caro is not deterministic but Sarah will make it deeper Mystic because when you make a language for an L1 or two four four blockchain itself if you want determinism you want determinism for a very specific reason actually which is you want to be able to prove a fair transactions without determinism you screw it for that and so we for now we don't have it and it is those Vector that we control by making by right now whitelisting the contract but tomorrow when we're going to go for permissionlessness and then centralization you can obviously do that so we are working to have this safe internet presentation which will be deterministic and this the intermediate step will be able to actually compile to multiple backend so either Cabo or like an optimize for xc6 for execution layer and potentially from phoenixes but in that case we'll probably lose most of what you're gaining and what you wanted so uh I I don't see I don't know if it's practical to compile for I I don't know about Cersei but I would be it's a great name for Stark by the way uh but uh yeah I don't know uh I don't expect so I don't know if you could do that yeah so we did once have an effort to integrate a Seer with Cersei uh we dropped it just due to priorities uh from what I remember it was fairly easy if we extend Cersei to have uh these black box functions uh just because the Cersei IR just can't optimize uh for these black box functions um so yeah it's possible we just haven't picked back up on it yeah I I think nor is probably the newest shiniest language like it just dropped um and I'm I have lots of questions about Acer acir is noir's intermediate representation so it can compile both to r1cs and Planck um so how does this IR capture both of these um very different arithmetizations um uh essentially you have these arithmetic Gates which are just linear Expressions which aren't bounded so for r1cs that's quite simple to compile down to for plunk because you usually have like width 4 or some uh fixed width we have something in a sear which basically chops the gates into the perfect width for a blank for the Black Box functions it's really just the proving system just takes in the witness indices and just fills in the constraints for them so it's quite simple what it's doing it's not doing anything complicated yeah that makes sense Brandon did you have thoughts um on the IR thing yeah well I I think I spoke in the in the beginning a bit I mean yeah I I guess yeah I don't have anything else to add um cool um so what I'm hearing is like basically compiling to an IR you could stand to lose some um some very specific performance optimizations uh unless the the IR allows you to Black Box things easily cool I don't have a question for Louie as well what do you mean when you say uh Cairo is not deterministic and that your IR is deterministic so so Cairo today so proof our dkps or Language basic you can create hint and in that break vitaminism um but we we Carriage there is not domestic so for men to be more specific we actually have two flavors of Cairo uh what we like what I like to call Pure Caro which is the one you would just directly prove a program within within sharp or sharp being the shareproof infrastructure that we provide or um or um that's your pure Caro and what's dark X is star X is built on and even Stark net itself is built with and you have what we call Stark net Cairo and Stockton Cairo don't have a notion of State Dove has a notion of like Cisco and plenty of things that you get from the OS itself so you have like Cairo for a start net you have Cairo for real pure Cairo so the thing is that the Cairo Force darknet cannot be non-deterministic and that is for a very pure incentive reason because if you don't have determinism that you can make transactions that are not provable meaning I'm the only one we know that this transaction is done in and I only want to know the hint and therefore the rest of the word cannot prove it and so for instance let's give an example that people like to choose you know I want to do a force transaction for man one you know being that optimistic roll-up push I mean talks a lot about um then in this context with determinism I can't this is a dose Vector because I don't know if the transaction is getting pushed to me is provable by me I don't know that and so and another thing that is important to you that fair transactions so fair transaction can be valid you know the price of this pool only swap move and now for my transaction failed and otherwise it can be uh malicious so I'm spamming the network with transaction hoping to get what I want but if I don't I don't think I don't pay anything and that's why I can spam the network for anything and I need to run it and so creating those Vector so Force darknet we have to make Cairo deterministic or I mean the version of Cairo for Stockton will be deterministic for that purpose and to make it deterministic we need to prove that the program was compiled into deterministic version of Cairo which is a safe intermediate representation called Sierra and the Sierra will compile to Cairo itself and so right stuff will be proven within starnet when I'm deploying a contract I will be proving to use darknet that this contract was compiled with using CLM so this is what I mean by Carol become deterministic in that conflict [Music] I guess my next question is uh number three which is yeah when you were writing your languages what features did you prioritize so for example um Noir is very rust-like they even have a version of cargo called nargo um and then uh snarky js's like typescript um Cairo is also a pretty high level yeah it's Miss right now it's a mix of scene but right the new version will be very rust-like which is coming in the I say three months right and for example ganark was just written directly in go Halo 2 is written directly in Rust but but pill and circum are like kind of closer to the metal I think so is Halo the metal the circuit I mean um and so is Halo 2 so yeah what are your thoughts on uh the trade-offs between like higher level representations and lower level representations and um how did you you know decide on the designs that you did can maybe start so the first that's actually an interesting story from from uh from Star War expertise experience so the first version of Star Kick so starcx was and it is the first product in stockward and which is basically a centralized but non-custodial back end for uh dabs who need scalability so you know customers are dydx diversify uh immutable and so rare and so the first version were written you know very low level literally in polynoms uh and this thing does transfer and swaps and so we started to work in Cairo it was 2019 and it became production ready uh in uh in May 2020 um the first case of actually uh where we used it for what's for the ready to bake off in June 2020. um and so um the funny story that the improve the performance of the of the system massively improved when we start using Cairo because it was much higher level and who had a lot more flexibility in the way we could reason about the system in the way we could write about the system Not only was again in philosophy in velocity but also again in actual Pure Performance and so um there is you know in some green of and when you need that performance Improvement we have these things that are built in the same built-in as equivalent to Cairo to those specific shape on your CPU like the one that does 64 bits and so if you really need like optimization at the very low level for a specific operation like say proving um right now we did it first okay check we did it for um um for um uh for a seriesic signatures we in the range proof and sort of things that we write them in those and for the rest we just write in and so there was not really any trade-off in many way except that much simpler and nicer to write nowhere too yeah that's interesting that like a higher level language actually improve your performance but yeah I guess so you're pushing a lot of the manual optimization to the compilers and like stuff that computers are better at and then the commonly used so-called pre-compiles um you do hand write that you started when when I started to write circum the main purpose is as I said before is circum is at the end it's a low level language so it is that if you're writing silicon you should understand what you are doing you should understand what's in the what's behind the the circuit level of course you can do things in um in a high level because you can connect things but the idea is that you have precise and this is some something that's very specific to circum is you it should not be any hidden constraint anywhere so other constraints are there you can check the code maybe you need to go inside the circum leap or someplace in the library but you will find all the constraints there and you can track them and you can see them so you can have full control of what you are doing this of course is dangerous I'm not saying that that's why because you know you need to understand if you're I've seen people that writing circum language that they don't know what they are writing so it's not going to work okay and this is we we understand this is a a thing but this is what circum is uh for circum is for writing would say Circle means for people that understand what's happening underneath that's the that's the thing okay um said that the disease will be linking with what he said is I think that in the future nobody will have to write circuits and because uh Siri is a very specific thing for politics and and then you can write you you will be able to write things in in Cairo for example or things in maybe some high level or even in in solidity there's a kbm at the end is a language that you're writing a language and you you're building a zero knowledge you're building a zero knowledge there so you can uh there is other projects like Risk 5 that are also building on top of that so it's uh the the zkbm what brings behind to the to the to the world is that you can have any any processor any base a risk 5 an ebm or chiro-like or some some specific virtual machine so some processor and then you build on top of that processor but the circuit is the processor the circuit is like the hardware okay so it's like maybe we can talk about Hardware language and software language uh silicon is a hardware language okay and so for language should be normal so for language C solidity python or any other language that builds on top of that I don't see a space for um I don't see but this is a it's opinionated on me but I don't see a space for a specific language as a specific high level language because I think that a very high level language should be enough to to run on top of that can I just add one thing but it's what you said um I tend to agree with the entire statement about however language there is one thing though um I don't I I'm not sure and I don't think necessary that you know things like python or Russ will run enable you to write vkps tomorrow because there is still a very strong Paradigm competing Paradigm Beyond it a very strong differences which might require you still to have like a different accepting that you're working on something different yeah probably this is but this is this is at this point we are running faster so it's uh I think it's just a matter of uh times and yeah and how difficult it is you know right now uh depending is if you are if you want to run a very very complex uh uh language very complex thing it's one thing but if it's complex it's going to be also difficult to write a complexity so I I think the way to go is high level language cool yeah so um I uh I and my team have a very very strong opinion about this so I guess for for background um so Mina the the Mina protocol um we started building it in uh 2017.
um and uh for those that don't know Mina basically is just like an enormous uh like zkp circuit that that powers everything so there's um a recursive uh a like linearly recursive proof for uh compressing the blockchain that follows you know the rules of blockchains um uh there's like consensus logic there's verifiable random functions where like uh fractional numbers are approximated using like crazy uh calculus things basically enormous enormous programs and and uh enormous circuits and and we realized very early on in 2017 that like we could not write the circuits manually um and and I agree it's I I would I would sort of I mean in some ways it's like it's like programming directly with Hardware but I think you can also kind of think of it metaphorically like writing Assembly Language um and and you know you can't like uh these days when you're trying to write a really complex program you don't use Assembly Language you use a higher level language so um so we so we built the first version of snarky which is an embedded ocamel DSL in 2017 um and uh we used it for and we still use it you know whatever five years six years later um and uh it's great and we've learned a lot and and the the specific um you know we've taken those ideas and brought them to snarky JS which is just sort of like bringing that into into typescript instead of ocamel um the uh you know we we thought about like okay if we could build a high level language that compiles into something and then like Implement a bunch of optimizations but the the landscape of proof systems is we thought would evolve quickly it has evolved quickly it continues to evolve quickly um and so uh it makes sense right now um I guess it's similar to what we were just talking about like uh you you you can't today efficiently use like a regular language directly like uh like you can't write a rust program um and have it run efficiently uh in you know for some definition of efficiency um uh but um but you can uh you can build like a little library or framework in in a language that already exists embedded in it so that's what we did with ocamel it's what we did with typescript um and uh and and and you can you can build um you can expose the lowest level so so like the there are people who are like experts at optimizing constraints for the proof system and then you can build abstractions over that uh and with types builds um you know type structures build computations um and and this has worked for building this enormous uh system that we have in Mina and we see it starting to work as well for building really complicated applications with crazy recursion and all this stuff in in snacky.js yeah [Music] um I think I disagree with everybody that's okay that's why you're here um from like uh I I think that using rust at least for our use case um it would be a bit clunky to encode like um semantics for like privacy like private State and public state so I mean it it's possible but um I think for the user just be a bit clunkier which is why uh I think maybe if you're not using it for the Privacy use case then high level languages like rust and go might work um for uh for for using typescript and uh languages like that right now um when we were designing Noir it just seemed like we needed to restrict the user from doing uh very specific things that it seems like in typescript they could just counteract it and uh I guess one example that I always bring up is the if statements like uh if you're using like a high level language you sort of can't just do if something else something because in typescript or high level languages that works different from like a circuit based if so in Cairo we actually do a cattle at the runtime so we don't evaluate if statements we only evaluate the path we take that's why uh yeah uh of course I have a counter opinion to that um yeah I think uh um the the costs uh of of using a custom language in in my opinion in my team's opinion uh severely outweigh the the benefits so I guess just to talk about the if example yes you you can't use the built-in typescript if in the context of uh like within a circuit but if you are if you are Computing a value that you're then using in a circuit you can use if statements and and if you're if you're actually in the circuit there are tools in in the typescript ecosystem that can help us actually Warn and or error to the user like we can use eslint to provide an error if you're using an if statement in in a place that uh you shouldn't be and and that and of course that won't be perfect but um we've found that that actually uh is is working really well so I actually I'm agreeing with both of you so I'm gonna explain what I mean by that um I agree that you should have um basically your specific language at the same time that um that I mean that tends to help you think about the Computing model you are in and at the same time you also want a language that are familiar to the public or people are already using and so one solution that we I mean first of all I'm saying I didn't say about Cairo so Cairo actually been CPU air so roughly Cairo can evaluate any program and it was clear to everyone here but it's and notably what it means that there is two things that you get that you don't get in circuit usually which you you only get you get recursion um very easy recursion you don't have to evaluate your circuit and second thing that you get for free is you only evaluate the if statement the path you're taking so when you have many many ifs then you actually only you don't pay for all the branches you only pay for the the one you're using and so um one consequence of this one thing that we were able to do was I think all the team built is they started to see trans compiler from one for the higher than other language two characters so we have one right now a language compiler called skyro made by your team out of Switzerland which is combining Idris or just being a functional language to Cairo for the story if you are if you want to use it you'll be the first one to ever use it so have fun uh I actually never found anyone who wants to use a functional language so maybe there is one in this room uh but uh just like functional languages so go for it uh Idris um so seriously if you want to do have fun go for it seriously it's crazy but uh but so I'm trying to say that um I don't know if it's the ultimate path but uh um they there is like there is a middle ground can I uh yeah so um yeah so just uh for for in in snarky.js today connected to kimchi I mean this is powered by kimchi of course but uh we we also can handle recursion infinite recursion and in snarky.js we've built an interface that's just it's like essentially the same is writing a recursive function so you just you you know you you put your function in a JavaScript object that's the only difference um and whatever arguments you have if you type them as like proof then uh the system will know that you are trying to do something recursively and it'll do all the complicated for you uh and in your in your code you can just say like you know if if like P is your proof you just say like P dot verify and that sets up all the constraints for your circuit uh and then and then the other bit about the if statement branching thing like today in I think any proof system that I'm aware of including kimchi including the current version of kimchi um yeah you have to pay for both branches and you can kind of approximate branching by like multiplying by zero or one um but we are actually working on an extension to the proof system that will uh will allow you to do these kind of like arbitrary jumps in an efficient way and that though is uh you know I'm not working on oh is it not a CPU like you know like basically running in the arbitrary program then um yeah I always VM basically at that point um you you get essentially the the power of a VM with the performance of direct circuit yeah so it's kind of the Holy Grail and and the I mean the intuition behind it is like uh there's you know there's like look up tables and and custom Gates and all these things in Planck um you can sort of extend that to uh allow um for like arbitrary Ram like random access memory and then you can kind of do another fancy thing to get arbitrary jumps efficiently um and the details of this I'd have to connect you with a cryptographer on my team but um I am told that this is the path that we're going towards I've seen that I've seen that in your repo is the dynamic lookup table right yeah Jordan has been silent for a while you know at the end is this is what are you writing Hardware or software if you're writing Hardware you need a hardware language if you're writing software my my my opinion is just use a standard software language and uh why because the hardware and the problem is that you need the piece of Hardware you need the process or the hardware that that can compile to this software but this is there so this is where to go cool um I want to save some time for the audience to ask questions so we have about 15 minutes so any questions from the audience so we actually touched on Hardware a lot during this conversation it'd be interesting to hear uh from the different panelists like what you actually see the kind of future of ZK Hardware to be in like what direction it's going not that kind of Hardware we were talking about I think we're talking about but yeah we can talk about that too but we should we we can't we can't talk about like real physical Hardware as well yeah we're talking about the polynomial Hardware it's like you know arithmetic Hardware I recognize that I I can no we're making a joke but let's uh on the artwork acceleration so I'm gonna take a hot stake here um star query at this stage do not believe that we need them um as simple as that um the reason is because the software itself is being improving so fast and the structure in the architecture of how you do things has been improving so far that at this stage we we don't know what the future will look like and so what I mean by this is hardware development is you're roughly a year and a half before getting to production and a year and a half from a year and a half ago uh Cairo were barely working started with in premises uh recursion wasn't working um we and and so for instance the thing that we are working on right now so we already do recursive recursive proof on production today of approve ourself but like for instance one architecture we're not doing it at the moment is um basically a three of proofs like basically right now the only thing we do is we have what you call jobs and jobs are like those Stark Nets starkware infrastructure used all of that to Sharp and so all the customers and you start and included of the infrastructure are sharing the same proof so every every one of that is using is basically everyone is paying a marginal cost of the proof cost on that and so um so for instance diversify or immutable like right now is having like 70ps in their environment and they're using a significant amount of a step within this proof so they do one job and we have other proof and also another type of of the job is approved so we um so we don't really we didn't went all the way yet into that uh tree architecture and so full Hardware um there is already a significant like you know the the thing Central fact that we can't really say this is very good that said I have a friend of mine I guess umovich from uh the company called wait uh it's uh which is a very good friend of mine he's also already working on this making uh groundbreaking Improvement on outbreakable explanation Shake pronunciation or even like you know uh MSM which I have no idea what it means but uh I would let him to you he's not here today but yeah I would let him answer that another day um I I yeah so different I guess slightly different opinion um so in in uh in snarky when you use snarky JS for writing applications on Mina or just in general we're encouraging um the the proof computation to happen actually like on the user's machine um in this way you get uh privacy and and uh you know there's there are ways that you can sort of do part of the computation on the machine to get the privacy and do the rest on a server all these things but um when you have a proof system that has a lot of cool features in it uh like kimchi um it's it's slower than a proof system that has a lot less features in it um and uh Hardware acceleration would then kind of you know make it faster I I think it would be uh cool I guess like you know we're encouraging people with snarky Jazz to write uh circuits with recursion with with linear recursion or tree recursion that's been working in Mina and Mina's mainnet for a year and a half sort of internally and and now on our decentralized test net we have uh you know you can do it with custom circuits and and settle on chain and all that stuff and it works um uh and and yeah and it's a little bit slow right now we're working on optimizing it um but I I am imagining a world like I think a cool world would be one in which like The Ledger that we all have um or something like that uh that has our wallet on it also would have like a a snark accelerator uh companionship or something um I I don't think that's coming anytime soon but um something like that could be cool and and even like obviously in the shorter term taking advantage of like gpus fpgas and silicon like at any level I think would be helpful uh because it would it makes these proof systems that are I think like have a lot more features um uh more you know faster so you can do different kinds of applications than you could if if they were slower I would distinguish this is actually a very um very different so talk about zero watch proof we can distinguish between a small small proofs and uh big proofs because the big profile for ckvms and for uh roll ups and for when you want to do aggregation and these high computation stuff and then small proof more questions but they're more related to something like Identity or a game or something that you want to run especially in the client I think the client has a lot of sense uh because it's uh it's where the hardware you know you are building you do a a big investment but then you you you you can uh spread to many mobile phones or too many uh places so this makes a lot of sense and for things like you know these privacy things for for things like uh uh gaming for things like identity uh just proving things about your data I know all this that so uh I think this makes a lot of sense in in in that direction for the hardware um so for the big things and I'm talking more specific to maybe a specific project which is the ckvm but so representativity is that for us we are I tell you why we are interested in Hardware uh maybe here you will you will you will see why the idea is that um uh in a so if you want to have a competition the days that you want to have a competition uh that approving competition you know disaster there is a market for for for uh generating proofs big those big proofs uh here you can have there is a problem is that you have a centralized maybe you have some provider that has a lot of power and these monopolites the the the system in the case of ckvm this is not a big problem because you can only build the proof that's already deterministic so you cannot do crazy things but you can degrade the network so the problem is that somebody that has a huge power that's able to generate a lot of proofs maybe just stops and stops doing that and and and then uh the the network just degrades so in for us the way for us to to to to to avoid that is to have the best the best proverb available even in Hardware when I'm saying Hardware at least in fpgas or whatever even Asics if it's required so but the idea is to have the best approver a valuable open source and a valuable for everybody so that there is no monopolistic uh proverb that can take that that's why for us it's so important that the proverb is open source that the property is available for everybody and not only that that the technology to build the Brewer is available for for the community because this is the guarantee that we have that the network would not be degraded it won't even have to on top of this um in the context of stock net the way we are looking we're going to look at this proving Market is by actually having uh like a kind of POS exam mechanism where we have a leader who would be the proving one and we have like a in Cascade another one and second one would come afterwards uh if there is degradation and so um the the other thing is that I just want to say I forgot to say let's talk about that but um people have been very focusing a lot on on um on acceleration because Stark are very slow and there is no because the operation that he did curve and so on uh and some means I mean I mean but I mean at least uh Jordy and I uh working more on stocks which are much faster and much easier to to use to to work on on regular servers so I think that maybe a difference of nor take relate to that machine I mean uh so I'm gonna answer the question I wanted to hear instead of the one you actually asked uh because I don't really know much about uh Hardware acceleration uh in terms of uh programming for Hardware versus programming for a software I think proving systems are changing too much for at least us to focus on uh sort of being so close to the metal just because the muscle might change next year or the year or the year after uh I will say that for privacy it's sort of a different space uh if you have privacy you need to sort of think about how to accelerate approver like because we usually use wasm whereas if you don't have privacy it's really fpgas and GPS like how do you accelerate uh this this massive beefy machine I I guess just to um there was this discussion about like uh you know markets for decentralized provers um and this is just my I just have to say this because too many people are surprised by this at this conference sorry if it's a little bit off topic but Mina has a decentralized sequencers decentralized provers a Marketplace for producing proofs um that are sort of needed by the system and this has been in production for a while and uh we um encourage more people to look at it when they're thinking about their marketplaces and and everything cool great answers thanks guys actually there's a worker okay um I have a question it's like maybe continuing on the hardware thing but most of the I mean a lot of people kind of um compiling Target now is actually solidity so actually a lot of people are moving on ethereum and kind of this is Defcon so like uh the most artificial kind of constraints that I'm seeing is probably the fact that we have one pre-compiled curve to work with but we can only work with BN 128 so wondering what's your intuition why why don't we have more curves to walk with in your opinion I don't know it seems like it will kind of release a lot of the bottleneck so okay I I can make two comments uh the first one in the pure application Level and why people should care about what you're describing um so I think that one of the biggest original saying that if you're made when they were built in order to see in retrospect right we couldn't know is to have had EOS I think EOS was a mistake but and and um and you're right having new curve like you know uh being able to use the p2056 when it is on your phone or even being able to RSA verification I mean just to throw random ideas right um would be unlocking a lot of use cases I mean just to give you an example um starting running through the company on gaming that is using the construction to verify p2056 the the you're using your securing clip of your phone to sign signatures for gaming that's awesome which is awesome um that's actually not for me the biggest you know lock of the verifying the evm the main difference the one problem is that um either you the Computing Paradigm of the VM is very different from when you have nvk I mean beats Boolean logic is expensive and ZK is cheap on the evm right so this is kind of the starting point um and um while if like you know a lot of team are looking into I mean diving I mean or you would talk more about that than me um about you know putting the vvm uh we didn't make the choice because we were in our opinion we were optimizing for performance of The Proving system and then now that we have that can we back work make it Backward Compatible and so we have in our case warp which is like a tooling that enables you to transpire from uh solidity to Cairo and the practicality of it I can't really judge no one really used it in production but they managed to recently announce they managed to compile to unifa V3 which is a significant bit and um there are an existing effort right now to rewrite the vvm in Cairo so I don't know once again if it's a POC if it's for fun or I don't know maybe maybe it would be practical to prove that I want to see the numbers I won't believe it going to your question um why uh why not others I think maybe you should ask to the EF people maybe better but what's clear is that at least the BLS 381 this is a must and this is will be introduced sooner or later uh in in ethereum among other things because signatures so because all the all the staking stuff it's it's done with this BLS stuff and also bien well at the beginning was that was not safe because there was something discovered but then it's much more safe that we thought that was safe so it's it's there you know it's some there are some doubts of the BN Corp so I think that sooner or later ethereum will have there has been some efforts I know that there has been some uh stops uh at some point uh on these this this adding this and here is for example uh we are implementing the fully VM right now we don't have to compile anything like we just get the code and put it there doing that what has been an effort but what are the difficult things what what what what's the what are the piece that's really difficult to add so we were able to to build the evm but there is one one piece that's complex we'll do it but it's really difficult to do it um this pre-compile contract of the bn1 so complicating the complicating the uh the layer ones uh VMS uh is not a good thing and this is uh there are you know there are some of course there are some mistakes we did with the IBM was created one was created uh wasm was not even an option at that point just for you to just people to realize on that of ZK nobody knows they didn't exist but uh so here and and the wife what I've been hearing what I see is that uh dbm should tend to simplify not to get more not to get more complex and this is I think this is a feeling that uh in ethereum the people that's working scissoring we have uh ebm is probably too complex and we need to tend to simplify the gas models the the sum of codes and and if you see the proposals that are uh coming are more in the not in extending the ABM but in simplifying dbm and said that I think that the BLS is is a must yeah so um I guess similar similar to uh Stark where we we started not with evm compatibility in mind for for mina um and snarky.js and our proof system um but differently from starkware we didn't we didn't start with like performance in mind um because we're we're not trying to build like uh CK ZK roll up scalability solution um we we were like okay there's all these cool things you can do with ZK uh with with privacy and recursion um and and we want to build a proof system uh that enables uh people to take advantage of all those cool things um and uh and and so um in the same vein as what you were talking about like there's all these cool things now that you can do in in our proof system and on Mina and you know we're working on an uh ethereum Bridge so that the mean estate can just be fully verified from within ethereum and and the idea here is like we want to bring all these great features uh to ethereum Developers but uh you know like I guess typescript is you know people are writing front ends into typescript anyway so hopefully it's not too bad um but uh but yeah rather rather than like kind of trying to put all these things inside evm it's like okay let's use you know efficient uh elliptic curves and all these things uh to to do these interesting privacy and recursion all this stuff and then uh wrap it up in a nice present that can be verified quickly on evm I can say my question is because uh you know start the standards are evolving sometimes and this is like a like the the hottest the metal will be in terms of zero knowledge standards so some of the time the constraints on the standards come from things that are not necessarily very efficient and eventually Downstream you you don't understand how you got something that is using a certain aspect so a lot of it down Downstream decisions are being taken because of of that right we have baby jab jar because it fits the prime field and and I mean it could be more efficient to amazing like uh kind of from a philosophical kind of aspect of at some point you need to leave with with there that's the point and and and you you can I mean you know you can wish us we we could wish and we did many times you know uh wish I suppose if we can't but the reality that you you won't get to adapt I mean we may be all convinced here and Decay the future but maybe other people outside or not and so we it's a consensus we want to agree on what's what's good so I tend to agree with Jordy we need actually a much more in favor of simplifying the network than doing it than trying to bring more more things to make our life simpler right now and uh just to give you yeah that's basically yeah I don't know for this is uh look in in the second circuit we are using a different Prime field we are using the goldilock spring field we are building a stark we are building a recursion of a stark we are doing a lot of crazy cryptography in there and just in the last moment we just built the glow 16 or a plonk that's just but this is the last the last piece so it's like the adapter if you want to the network if if so maybe then that so maybe the IBM you you just need one thing hash functions how many hash functions needs uh requires the ABM well we have ketchak we have a a shadow 56 recently a 30 minute Blake uh is it necessary maybe with Shadow 56 would be more more than enough from the beginning you couldn't argue that the pre-compile could have been you know like we could have made things cheaper or in first place or maybe you know made many things that are wide if more so much more efficient of the spring you know there's many things you could discuss in the back but this is why why and why this is possible right now and maybe and this is changed from three four years ago it's because we have this validity proof we can compute things of chain and validate them on chain so we just need to care how we validate these things on chain and bn128 or if you want to BLS it's more than is more than enough so probably if the if the ethereum had to be done now uh it would be less uh cryptographic Primitives and uh more basic thing because we can we can we can accelerate that of chain uh and and validate that uh with uh with the visibility proof on chain and just to conclude on this if you want to have much more impact and make one change changing I mean it's going very ballsy changing kitchen might be more helpful no because you change we pass it on in which which in which prime field yeah yeah but that's that's that's the thing you know it's and I've been thinking you know all of us we haven't have been thinking on that this why Poseidon is not in the or why the so why don't we have a milk C at some point uh it's not in the in the VM and and this is the thing but as we evolve as we evolve we see that this is less important because we have because this computational proof are getting much faster and much better so we require less this so we can sacrifice a little bit of optimization right now we can look in in in the ABN circuit we can we can validate for 500 catch acts in the in the proof we can validate uh I don't know like something like 100 or 200 uh cdsas with the cdsa ethereum Corps in there we can do paintings inside there we can do everything in there silly it's not optimal doable and it's it's getting every time more efficient so at the point that we have this we require less how from the L1 we require less Health from that so so that's why I think that this tendency to simplify is is is is is is a trend oh yeah I I also feel like part of dunk sharding is moving in that direction like they introduced the pre-compile for Point evaluation for kcg and you know then you can understand kcg proofs but beyond that it's all blobs you know it's all um delegated to the Roll-Ups well we are we are over time so there's one last question okay ask it ask it thanks thanks yeah I just wanted to know that I see a lot of sense in like breaking this evm eyes and creating DSL not only for like opening new area of innovation and like clear question to basically Amina I mean does it make sense or you also like for example to collaborate with Cairo and uh maybe like you know since like it's better model for the CK than uh like imperative languages and uh yeah basically work on better tooling for uh yeah I mean operational verification I I think we are we already are right I mean we we have uh someone on on at o1 Labs which is like the the team that incubated Mina um is is looking into getting Cairo to work with with kimchi yeah and there is even one in the room who actually took her work and made it into work with Winterfell so you can look at the guy in a very nice blue shirt over there Max so yeah next has a practical Cairo a very very fire and prover uh in Winterfell today um I mean to be honest it's actually go back to the point question about simplifying stuff um why we have no l2s we have L2 that can do stuff um let's use their their advantage to bridge where we could do the B4 and so like you know an example uh there is a team actually maybe like maybe in the room actually over there uh snapshot X is working right now to do N1 voting using L2 to make them cheap and that's something you couldn't do before so that's this kind of thing that we can do with l2s now that we couldn't do and then one we don't have to change that one for that so simplify please cool thank you all panelists [Applause]
Automatic transcript — names and jargon may be misspelled.