A ZoKrates Update by Thibaut Schaeffer | Devcon Bogotá

foreign [Music] math this is also developing this is also tooling for developers so today I'm going to present Socrates I'm going to give a quick introduction to what it is for those of you who don't know it and then I will present a few things that we've been working on and that I'm excited to share so what is Socrates if you want to program snarks today there's different tools that you can use maybe some of you have heard of Socrates and all those tools have different trade-offs in terms of power that they give to developers and how easy they are to use and how high level or low level they are Socrates has a positioning as a very high level language so when you write Socrates it looks very similar to if you were writing rust or python or something like that it compiles to r1cs so this is uh the kind of snarks that are easy to verify today on ethereum so you can verify directly in your smart contracts it uses modular backend implementations which means that rocket is does not develop a proof system itself but rather uses back-end implementations from the community for different proof systems and just targets that and uses those great implementations in order to have such a high level language but still have something that's really efficient at the at the low level zocoties Max use of optimizations in the compiler which is something that's also different from some other tools which give you a very low level access to what's going on on the constraint level but don't really apply a lot of optimizations um so where does it run so the part of Socrates uh which allows you to compile so the compiler you can run it natively on your machine we have a remix plugin as well and we also now have a playground that you can access at play dot socrate.es which I encourage you to to start that's probably the easiest way to get started with Socrates and just write some simple programs um in terms of the schemes so there's back-end implementations that we support we currently have support for a graph 16 which is some of you may know the the snark that is the smallest and the fastest to verify for gm17 which is an uh an evolution of graph 16 let's say for Moreland which is a universal snark which I'll touch on a bit later and for Nova which I also go into which is a new type of exciting snark that enables new use cases for proving so the particular implementations we rely on Bellman Arc Bel person and also snark.js I'll also go into a bit more detail on on that integration and in terms of the verifier we have you can verify in JavaScript or in this in the CLI and for some of the schemes that are compatible with devm we generate a verifier contract so that you can directly send your proofs to your smart contracts and verify them and and Link them to your dab so to give a bit of a Hello word of zocoties here's a a program which takes two private inputs A and B and one public input C and then asserts that a times B is equals to C so technically this is a program where with which you can prove that you know the factorization of a number the way you would run that is you would first compile that program which would turn it into this low level representation uh that's let's say r1cs then you could execute that program with an input here three three and nine then you could generate a proof using a particular proof system and you could also generate a verifier that you can then Deploy on the evm and then send you proof to and then convince basically convince the network that you actually knew this factorization for an example if something that's a little bit more advanced to make the point that this is actually a high level language here's the implementation and Socrates of the shot 256 function so just to give you a few things that are expected in high level language we have a module import system you can import constants as well we have for Loops of course we have function calls and also one exciting thing that we added kind of recently and maybe some of you who use rust are familiar with that feature is the notion of constant generics so in this case the shot 25 shot 256 function is a hash function that can take an arbitrary number of bytes as input however in circuits all the inputs are always static so all of these uh the size of the input will always have to be known at compile time but this is something that we do you can still Define this uh as something that is generic over K and then have a number of rounds of this sha round function but then when you compile your program and actually use the function the shot five six this this variable K is going to have a concrete value which will then compile to the exact number of blocks that you're hashing and if you're trying to do something that's Dynamic calling this function on something that's not whose size does not know that compile time is just going to fail at compile time so we can have a very idiomatic implementation of chapter five six of course there's more complexity in the show around but if you look at the code it's almost line for line equivalent to uh an implementation that you would see on Wikipedia for example as pseudocode implementation now I'm going to go in a bit more detail on a a detail of the shot 256 implementation so inside the Sha round this expression needs to be calculated a lot of times it basically takes three unsigned integers a b and c of 32 bits and calculates a and bigs or ancs or BNC and this is something that you can just write like this in Socrates today compile and it will translate that to a number of constraints at the low level however if you do the math and look at the let's say the first bit of a the first bit of B and the first bit of C you can see that if you considering them as numbers so as field elements they actually verify so the result actually verifies those two equations so you define or you constrain a new variable BC to be equals to equal to B times C and here I just want to clarify that these constraints are the low level constraints that we deal with so the r1cn's constraints they look like this they have one sign which is linear so in this case it's only one variable but you can have a sum of different variables one side which is quadratic right so this first one uh just defines BC or like constrains a new variable BC to be equal to B times C and then uh introduces this res variable here which is our result for the first bit um and then constrains it in this way and this is actually more efficient that what the compiler would generate itself because here we have uh more knowledge of what we're actually trying to do than the compiler does on the flip side here what we're doing is that we're introducing a new variable res and then constraining it with this uh with this equation however when you're dealing with such low level details in strikes it's really easy to introduce new variables but fail to constrain them sufficiently so that you actually introduce vulnerabilities in your circuits so this is something that Socrates does not expose at the moment to the developer which means that you can only do this one which is less efficient if you look at more lower level tools they let you use these things but then it's at your own risk and then it's likely that you're going to introduce vulnerabilities so what I want to showcase today is uh the addition to Socrates a way to actually encode this thing and have um the performance from this thing in the context of the higher level language yeah so I have a video now if you could start the video right so this is using the actually the Socrates playground so here I defined the default function which I call the default function where I just I'll just use the compiler uh to generate the constraints for this uh this expression here I'm going to create an uh an entry point for this program uh so taking also a b and c returning a u32 and I'm just gonna call the default function and see how many constraints are created in the process so I compile and then I get the result 260 constraints here and now what I'm going to do is to Define another version of this function which hopefully will reduce the number of constraints by leveraging this lower level implementation so I call it hand optimized has the same signature a b and c also return a u32 as I described earlier I want to operate on each individual bit of this year 32 so the first thing I'm going to do is turning those u32 into an array of booleans we have sort of a magic tool in our standard library to do that which is called the cast function and which can do this conversion for you and here I want to point out that this is actually free because the u32 type is actually represented as 32 bits under the hood so we're not paying any constraints for this so just cast the three of them the next thing I'm going to do is introduce a new array of booleans for the result here one relatively new feature we have is that everything is immutable by default so here I have to declare this variable mutable if I want to be able to modify it after okay so now that I have all the bits I can start a for Loop so for I from 0 to 32 and here I'm going to consider the if bit of a b and c and if we want to have access to those low level constraints we need to reason at the level of field elements so we need to turn those booleans into field Elements which is a lower level representation for this I call this Bluetooth field function which I'm going to Define in a second I do the same for B and C and here I'm going to Define this function and again this is something that's going to be free that's not going to create any constraints for the same reason as earlier because the Boolean is actually presented as a field element at the low level it's just that it can only be value 0 for false and one for two so I can just return that using a ternary expression okay so now I have ABC as uh SPL elements now I have this first constraint which was uh BC equals B times C and actually this constraint I can already Define in in the high level language because I'm doing both constraining and assigning VC so I do that so I have that first constraint is done then I declare this result all again mutable and this is where the interesting new thing happens I have this assembly block that I can create and here as I I have access to and two special kinds of statements the first one is going to be just an assignment so I introduce I just assign the value BC minus this other expression to Res but I did not create any constraints it's purely just an assignment so this has no influence on the constraint system and then I want to be able to use this this res value later but to use it I need to make sure that it's really constrained in the constraint system so after this is I did this assignment I add actually constrained which which makes sure that everything is uh is set in stone so here BC minus res equals this multiplication you can see that again this can be any expression here when I assign but this has to be linear equals quadratic right so here this is this is working okay so now I have everything set up um and I'm convinced that res has a result that I need the next thing that I want to do is that I actually want to have a Boolean I'm going to go the other way around and reconstruct my result but I want to have a Boolean and I want to go from a field element to a Boolean and here I want to make it really clear that this is an unsafe a potentially unsafe operation because this res value I know that it's 0 or 1 because I I wrote this but in theory it could be any value so I need to be really careful when I do this um but I can force uh the creation of this Boolean with this value finally I reconstruct the u32 value from the Boolean array using this cost function again okay and I changed my entry point to use the hand optimized version so we were at 260 and now we're at 164. so we made uh quite quite a bit uh dent in our constraint count so what's the idea here um we want to keep all the guarantees that we have from our higher level language we have types we have things we know that booleans can be only zero one if you don't write assembly blocks but at the same time we want to have access to this low level thing and here I think there's actually a parallel with rust in a way which says okay we we have a compiler that's like really strict all these things but we still want to be able to do all these lower level things we want to disable a bunch of checks and we have a similar approach where as a developer you would write most of your program in safe zocots let's say but then for the few parts that need the extra performance you can write them in those ASM blocks and try to make those blocks as small as possible so that when you need to review the code or make sure that things are not unconstrained you know exactly where to look at and these things are relatively small um one side effect of this also for us as a compiler team is that we can use this ourselves to reduce the complexity of the compiler this particular um operation and the shot 256 algorithm we in the compiler we have a special case which detects whenever we're doing this and uses this exact constraints but now potentially using assembly blocks what we can do is rewriting some of the internals of the compiler to actually use these things which then reduce the size of the compiler code base and makes it easier to reason about an audit the next thing that I want to talk about which is uh unrelated to this is the fact that Socrates is not compatible with with snot JS so snog JS is a JavaScript library for snorix from the identity team from the circum team which has a bunch of tools allowing you to work with snarks in a JavaScript context what we have now available today is uh if you start from your your zocoties program and you run the compilation currently um it returns an output which is the low level zocchi's representation but you can also optionally return and Dot r1cs file which is uh the format that is accepted by it's not Js and then if you want to execute your program you take your input and uh and the program itself and you can create a witness file which is also compatible with with snot Js and from this point on your Instagram JS lens so you can do whatever snog JS enables you to do using different proof systems uh using a powersoft Tau ceremony um uh and run your verifier in the browser etc etc so any tooling that's compatible with these formats can now be used with circuses as well another topic that I wanted to touch on quickly is the is incrementally incrementally verifiable computation so this is a scary word but it's basically the idea that if you have a computation which you can split in steps which are basically the same function being run over and over again on the same on on the state and updating the state then you can actually use recursive snarks to prove this computation incrementally so as opposed to Socrates currently to others proof systems where we can think of them as more like an Asic so your circuit is like this Asic that's really set in a stone and you can do only one computation and everything is bounded and static in this case you can have a computation where you run one round of the computation and then another one later and you can prove the execute the execution of that competition at each step so some use cases for that are succinctly verifiable blockchain so maybe some of you have heard of the Mina blockchain where basically you use this to have a a blockchain where each time you get a new block you you verify the previous block as well as the transaction of this block and it creates a snark and then you have this kind of recursive verification another use case is vdfs because some of the vdfs actually have the structure of having some state which is then to which you um apply a function recursively and then being able to have a snark of this computation can be really really useful so what we're working on now now we're actually pretty close to having this ready in production uh is integrating a um proof system called Nova which does exactly this and the way that I'm not going to go too much in detail here but the way that the API would work for developers today is that you write a function and the only restriction here is that the input needs to be the type the input type needs to be the output type because you want the recursive aspect to to work and then you can compile this function to a specific curve so you need to use this balance curve because under the hood Nova uses cycles of electric curves so this doesn't work for any curve but we support the curves that enable that and then you can basically prove a number of steps starting from a given a given State and even after running this you could run it again starting from the last state that you had this hope this opens a lot of use cases for people who want to to experiment with incrementable incremental verifiable computation so I invite you to to test that it's it's going to be out very soon okay um since I only have two minutes left I'll just go very quickly through some things that we that we added recently so there's the powers of Tau ceremony so if you look at gross 16 for example it's it requires a trusted setup and the powers of tower ceremony enables you to do that using NPC so you can do that directly with this oxtail CLI and also in the in soccer says JS actually we also have support for lock statements uh that you can where you can inspect certain values of your code at runtime we have support for the more input system that I mentioned earlier which is a universal setup which means that you can do one setup and then use it for different circuits we also change a lot of the syntax following some feedback from from members of the community and finally yeah the this this playground which is now accessible which I invite you to to check out okay I think that's that's all I had to share uh so thanks for listening if there's any questions yeah I'm happy to take questions um can we use the new Nova support to write um another but shorter SDK VM I think in theory yes I'm not sure it would be the most efficient but they were already actually a long time ago VMS that were built on top of recursive snarks but they were using recursion at each cycle of the CPU which was quite inefficient but maybe there's a new take that could be that you can have on on that so that would be one cycle for each op code right that that's that was the case and those uh project 10 years ago it's a project called tiny Ram where that's what they did they basically took the state of the CPU and just run each time one one up code and then have a recursive snarks a recursive snark each time but maybe there's other approaches to leverage this proof system so instead of making users to write very optimized code have you put effort on kind of making the compiler kind of figure out what the user wants and then optimize the circuit based on that so are you saying that okay is your question that we should instead of having low level code have the have the compiler detect when it can do those optimizations right I'm in both but like you will only talk about what the case right so this is something that as I mentioned this is something that we do currently where we identify some of those use cases I mean some of those cases and just have them in the compiler um but it's just really hard to cover them to cover them all because it's really use case dependent uh here this is just for one part of the shot 256 function but there's so many different things that you could optimize um so I think it's actually a good idea to open that to developers but in a way that that's quite separated from the rest of the high level code [Applause]