ZK HACK - Aleo Workshop Part 2 - Leo the circuit compiler: the why and the what

Transcript

so i think we can move on with part two compilers the why and the what [Music] one of the consequences of our design of using a proof on chain is that we need developers to make proofs which means they need to make circuits you know their programs have to make proofs and there's two real ways to approach this the first is to just teach them how to do it and this really sucks because it's like a lot of work it takes a few months to learn the cryptography and start building the circuits and learning how to debug them

and that's just a big barrier to entry and slows down production times and all this kind of stuff it's really not ideal so the other solution solution two is to like make code make circuits by itself you know if you can write code in a language that's similar to one you know and you don't have to deal with the circuit directly we can automate away some of this process and make it a lot easier we can reduce the knowledge requirements in terms of cryptography and also bring down development times which are both really important and this is why we made leo and it's why circum2 exists and noir and cairo and all the others it's

to make the life of the developer easier and help us achieve value more quickly we talk about compiling to circuits and this just means you're writing your code and turning it into a circuit i just want to go over the whole kind of process here you have your high level idea in this example it's a voting system you know voters do this to vote and vote time occurs by this other thing we're going to want to add some more detail where we're going to say votes occur points on a bls curve maybe encryption is through this thing and decryption is through this other thing then we have to make our circuit

and what i have for you here on the right is these are constraints in a rank one constraint system which is a type of snark so these are the things you're actually using in your program and we're gonna have to discuss a little bit how you turn a voting system into things like this and then you do your computation and you get out the proof i'm going to be discussing these uh sorry these constraints with you to some extent and i may be throwing you in in the deep end a little bit but part of my point is going to be that you don't want to work with these constraints directly like i mean i want to because i like it and i find it fun

but most people it's not relevant if you're trying to build a product which you think is going to help people derive value in the real world you want this to be as automated as possible so you can focus on the parts that you know and understand but i'm going to explore the constraints just to show you a little bit of what's going on so on cs values in in these constraints this x1 this x2 this e this v uh they are like are they uh are they characters or what what are they they're all specific things they're all just numbers specifically numbers between zero and p minus 1.

now the size of this p is determined by the elliptic curve you work with but they're all field elements they're all just numbers between here so you don't have a u weights you don't have a character you don't have a string and we're going to have to learn how to use these field elements along with constraints to have all the functionality that we want so this is you know very abstract in a computer you have all these nand gates and if you put them in the right ways together you can do logic and you can run a cpu and you can do graphics processing and all this other stuff but in a proof system this is the starting point and for reference

this size of p it's massive like this is blf 12 377. there's a curve we use a leo and this number has like i think around 10 to the 80 digits after it and that's a phenomenally large number it's like the number of particles in the universe and i mean we're only our solar system is only a tiny part of those number of particles and i feel like there's a lot of stuff happening here so you can do a lot with the numbers in between this space yeah and it also gives us some of the security properties as for the constraints the top so these bullet points these are

just examples of what it can look like you know x2 equals x1 multiplied by x1 uh second example a third example but they all have to satisfy this bottom equation and i know this can look a little scary but you don't need to worry about the details it's more useful to understand a few of the examples and see some of the properties for example i don't have any squares anywhere in the first constraint i have x1 multiplied by x1 which is x1 squared but we don't want to use anything any higher power in the constraint system so we just call it x2 you know in reality it is x1 squared but we won't do that we'll just call it x2

yeah okay so binary operations if you we have one of these x values let's have an x what if we want it to be a binary operation what if we want to ensure x is boolean that it's zero or one now i have a question for you here i can give you one or two minutes and i want you to see if you can figure out what the constraint should be what i mean by that is can you come up with an equation like the first line um well where it will only be satisfiable if the x in the equation is zero or one so i'll give you one or two minutes to

see if you can work that out and play around with the math at the heart of this so as a hint what property do only zero and one have in common i'm on whole numbers i'll just give you a minute here to see if you can write something down and then i'll go through what we would expect okay so

hopefully some of you may have worked out that we would expect something like this first line we have x multiplied by x minus one equals zero so well the right hand side is zero so that means the left-hand side must be zero and if we are multiplying two things together then to get zero one of them has to be zero itself so either x is zero looks good that's what we want or x minus one is zero and if x minus one is zero then x must be one so the only x that satisfies this is x equals zero or one which is exactly what we wanted

uh also below i have the same representation you know if you expand the bracket you get x squared minus x equals zero but this is something that you kind of want to avoid because we have this square here and i mentioned that something we shouldn't really be seeing in a constraint system even if it is happening implicitly i want to give you one more of these these problems to see if you can solve this one's a bit more involved and harder we have an if statement so if x equals 1 then y equals z else if x equals zero then y equals r uh so okay this is more of a selector where you have zero and one uh but i

couldn't get the maths to render so i just turned it into an if else if and i'm wondering if you can figure out what this constraint should be and i'll give you a couple minutes here again so again this should be an equation something like this probably involving well we have an x we have a y a z and an r and it looks like we're saying well y should equal this or y should equal that so maybe the constraint would be y equals something and i'll just give you a minute here to see if you can work it out and again one of my points about doing this is that for a lot of people they don't really

want to work with these constraints or this maths or have to understand what's going on ideally we want it to be done for us so that we can focus on the other parts that we care about more okay hopefully that was enough time to play around and see how these things work you may have ended up to something like

this just quickly the lower line this is the constraint that we had before because if we see x has to be one or zero it just makes sense to do a binary check and then we have y equals r plus x multiplied by z minus r and let's check if this does what we want so if x equals zero then y should equal r well if x is zero we have y equals r plus zero multiplied by something well that's going to be zero so we just have y equals r and okay that's exactly what we wanted first part good what about if x equals one then we have y equals r plus one multiplied by z minus r so r plus z

minus r r minus r is zero just left with z y equals z oh okay this is what we wanted cool we got it in so we have libraries that will make these constraints for you you would just put in a selector and it would do this part for you but you still have to kind of understand with the library that you're using what this gate is doing and some of the quirks there but our compiler is going to be automating a lot more for us okay so that was previously we did you know booleans and but what about a u8 now how do you represent a u8 in r1cs it turns out that for design reasons it

usually makes sense to to separate not not just have one thing that represents the u8 but have a binary decomposition so you'll have eight variables and each of those eight variables requires a binary constraint that's already eight constraints then if you want to use the u8 you'll have to sum them together in the correct way it's another constraint you know you add up a lot of these constraints and it gets a bit confusing um but this is to work with some structure that we're used to at u8 and compilers are trying to be trying to do as much of this as possible for us now how about if you use the library to

build a circuit you try to turn your your program you know hangman into code into a circuit what if the proof fails like what do you do if you look through the code and you say well this does what i wanted it to do then the problem isn't like your code it's it's your you need cryptography to debug it there's some quirk about a proof system that you currently don't understand that's preventing you from making your circuit work so if you want to be able to debug that you're going to need some cryptography and to be said this is a very high barrier to entry uh even i spend a few months learning

the cryptography and playing around with things and trying to get them to work and yeah you know we're just going to have fewer developers if that's the case and slow down production times now i just wanted to touch on one thing that tesla has apparently done very well they don't just try to make good cars they're also trying to make factories very quickly they've made you know broke ground and had a functioning factory making cars in shanghai within a year looks like similar time for berlin in germany it looks like a similar time in texas if you're another car company and it takes you four or five years to make a factory to output the cars and your

competitor can do it in one year you're not going to be in as good a position as them are you also it's just going to take you longer to derive value from the thing you're trying to make and if it turns out there was something wrong with the thing you're trying to make then you've wasted a ton of time building it to learn that so we want to make this process as quick as possible so we have leo and we try to add in as many properties that's going to be useful for this endeavor as possible it's similar to javascript and rust many people in the blockchain space use

rust so hopefully it should be quite easy to learn moreover there are 12 million javascript developers this is a huge huge fall it makes sense that we should try and get some of them to join our space to build things as well particularly because uh you know our applications need a variety of builders and i think in general blockchain has a big ux problem your user experience how you do things i mean i'm still terrified every time i send crypto to do anything and anything else i do on a blockchain i do it more because i think i should do it as opposed to the process being easy and nice

so we've got some way to go there leo also creates the l1cs for you just kind of been over this there's a testing framework so you can do unit tests and ensure your application runs as you want it to we've got a package registry so that you can quite easily import other code that people have made and reuse their things to save yourself time and you know borrow kind of the expertise of other teams we've got an import resolver and this will be formally verified by atl2 fear improver and that is that the compilation was done correctly and again these are all the things that we're putting into leo that's not to say that it's quite yet done but we're almost there

one thing i want to focus on a little bit is implementation bugs there's been a lot of losses because things have not been implemented correctly you know in the cryptography or other parts now if you need to build something and very simplistically let's just say you have to do 10 things then there's kind of 10 possible places you can make mistakes but what if lots of people have to do some of these things and we say well these six things everybody has to do so why don't we get some smart people together to build some stuff that automates and does those six things for us

then you have four things you need to do four places you can make mistakes and the other six things are done by some automation software that some very smart technical ex professionals created to try and reduce the possibility of something going wrong so compilers are trying to help a little bit as well to prevent some of these attack vectors what can you do in in leo we have all the data types you're probably used to u8 u128 i8 to ir128 also fields elements characters we've got emojis it's quite fun we've got structs with implementations if you know rust you can define a struct with some things in it

and then you can define some implementations on it and this is what we have we've got if conditioned we've got four loops and we have bounded recursion this is one of the quirks of proof systems you can't have unbounded recursion if you're creating a circuit you need to know how many recursive steps you have and if the number of recursive steps depends on your input you have a problem but what we can do is bounded recursion we can just say hey let's just do 20 recursive steps if you only need 10 of them

then you'll do your 10 recursive steps and you'll just do 10 dummy recursive steps and you'll be able to make a proof of this but you won't be able to do more than 20 recursive steps in this design and this is one of the quirks that you'll have to just understand that it exists not necessarily why it exists what are the knowledge requirements for using leo well again one of the main points is that we want it to be minimal we want it to be as easy to use leo as possible so the crap cryptography happens under the hood it's all done for you the proof uh circuit and proof will be made for you and you won't have to touch any of it

it's kind of just like a translator now if i was to ask you how wi-fi worked what would you say in response to this your phone sends signals to the the router but like what wavelength is it sending what part of your phone is sending it what are the protocols for processing the data and sending it off what's happening in in the router you know i i don't know any of those answers but i can still use wi-fi i can still build things of value that use wi-fi i didn't need to know any of those things so my point to you is that you don't need to know how a snark works you don't need to know how a compiler works you

just need to know what they do to have a functional understanding you know the compiler is going to make a proof for you proofs are smaller which means your blockchain can do things more quickly more cheaply and maintain some privacy for you and now you can code in leo write some program and use it you don't need to know the details it doesn't make sense if everybody had to learn the details it would take us a very long time to start building things that we want to see uh okay so the things you do need to know you're gonna need to know our transaction model which i'm going to touch on just a sec and then you want to

know like program and functional capabilities i touched on the the bound of recursion earlier which is one quirk and there's a couple other quirks going on there but mostly generally speaking should be quite similar to languages that you're used to as for the transaction model we're currently kind of upgrading it we're trying to find the global maximum in how good it can be and there's things here called transitions and transactions so a transition is up to two records in up to two records out and this is the base thing that actually goes on chain but possibly you have an application

where you need more than two records in or two records out in this case you can string transition together to make a big transaction and here is a like a directed acyclic graph to represent that so for example number one here this is a transition takes in records a and b and outputs record d and similar thing going on all the way here uh and all all records d to j and all transitions are going to be sent to the chain you know just because d e f and g come into existence and vanish essentially immediately it doesn't mean they don't go on chain they still do go there

uh you may be wondering why we have two records in two records out why not just more of them and this again is kind of a quirk of proof systems if you if if we said that a transition could take in up to 10 records and output up to 10 records well the transition is actually a graph 16 proof of verification so your transition always has to take in ten records if you only needed two of them you still have eight more records they're just dummy records but your proof is not as small as it could be and this is why we want to make it small but provide the option of stringing them

together to add more functionality but again we're still in search for the global maximum in terms of how efficient this can be we also built alias studio this is an ide you can download it out at studio and again it's just to make things as simple for you as possible you can also use it in vs code and syntax highlighting will be available soon and makes developing a lot lot easier cool i hope you enjoyed part two and understanding and provide some context as to what compilers are for and what they're doing and you know give you some

reference as to when you should be using them