ZK12: Circom buses: the power to structure ZK circuits - Albert Rubio

Transcript

[Music] so I'm here welcome everybody so I'm here to present this new uh feature of uh of circum and uh well I will I'm expecting that all of you know a little bit of circum otherwise it won't be easy to to to follow but in any case just to show that we are adding uh uh an important feature from the point of view of C programming language okay so um just a bit of context of of of uh what is ccom int intended to help

us in a in a knowledge uh protocol it's just this part that is in in in in Black which is we have to build a a circuit and be able to run this circuit okay so this is where circum uh help us okay and uh so circum is a DSL that has this special way of working which is to explicitly provide the constraints of the circuit okay so all is explicit and and then you some you can also provide an efficient way to compute the the

witness if you need and in many cases this goes together so you express the constraints on the computation at the same time but in some cases it it can be split in in in two parts okay so the another nice thing with uh with circum is that we have a library a huge library with many circuits that we can use to build our new circuits on top of it and this is encouraged because we can trust on these circuits and then we build on top of this and and and in in many cases we can get really safe circuits just because we build on top of things that we know are safe okay so uh we have this nice

ecosystem of tools and and so on but when writing circuits programs with uh with circum we we have a a little bit we are lacking types like in other languages okay so because in currently until now until yesterday the the only types you you you had in in circum were signals and AR race of signals okay so of course you can do everything with that but well it's not the best way to to to work okay so what I'm going to present here is that we will now be able to Define new types make collections of signals and so on so

then what's the compiler doing the compiler produce both things the circuit with me which is a constraint system in R1 Cs and an executable in web assembly curring web assembly or C++ that can be used to run efficiently the circuit okay so this is what the compiler produce out of the of the circum code okay so now let's motivate the problem so this is just a a piece of code of the of from the library from the baby jobjob uh circuit and this is the other for this elliptic curve and uh and here you

see that what we want to express is an addition so two points added give a new Point okay but since we have no types uh what we can do so we produce we we have four inputs and and two outputs that are just signals okay because of the names maybe you can figure out what is the meaning so the first two are the one point the second or the other point and and so on okay but nothing is is really making this as a as a each of each pair as a as a whole okay as something that you know it goes together okay so this what you can do but and and then

what happens that you really want points but you have signals just signals okay and even worse in fact there are signals in this case in the Twisted aor form okay so but they're just signals okay so we are not seeing this anywhere and it's not going to be checked in any place by the compiler okay so we need after this clear we need better types okay to to structure the information and then also to increase security because if we had new types then the compiler can check these types okay and then we know that we are what we are passing is of the appropriate type so this is what what uh we pretend to do this and and here is

what we get with buses okay so buses are like strs in other languages but we are programming circuits so then we have buses because bus is the name in a in a circuit so from now on we will use buses and and buses the nice thing is that all all all can be mixed up from now on so you can you can use uh uh you can Define buses using signals arrays of signals all and other buses combine it with arrays of buses whatever you like so everything can be used in an orthogonal way okay so the only thing that we don't have currently but it will

come I hope in in in in a in few time is is a recursion in the definition of buses because we have to well we have to decide how to handle the the the null or something like this okay so then buses Define new types okay and then type checking prevents from from mixing different types okay so the the the security is is is obtained like in other programming languages from now on okay since you types so the the compiler will type check everything and and you will avoid maybe using signals that have not real

meaning you expect okay so this is the the point and uh and and then very soon we will uh release a new version of the circum uh Library which is circum lip with using all these buses uh and and and change compl we'll talk about this a bit later so what we believe is that a complex circum program in production and we have seen many projects that use circum in the in the in the intro in the in the introduction so must use these buses to to increase readability because if you want to audit your your circuit buses will help a lot

and also to increase security okay so let's do a little bit of practice with this so the bra the example okay so suppose that you want to compare dat or whatever and we have the problem as before okay and then you have you can use names of the signals to help a little bit but uh there is not much uh later you can say well no let let's put it all together because then it will be clear but I'm not sure this is clearer than than before because now what's the day the zero or the one position okay you you don't know and it's not it's impossible to to know okay so it makes not much sense to to do it

like this okay so what can we do so of course use a bus use a struck okay then you define it like this and from now on you can now Define templates you see using this like before we had signals okay so it's simply as as simple as this okay uh uh note one little difference so there is just a tiny difference before it was the input and the output keywords were in the middle and that is quite ugly with buses so we decided to to change a little bit the syntax and from now on the recommended syntax is to put the input word uh keyword and output keywords first then

the type and then the name okay but the old style will be still valid it will compile and and no problem okay but just take this into account it's nicer if it is written like this okay let's go a little bit further what can we do with with with buses not only this simple thing we can now have parameterize uh buses like we have parameterized templates okay so this parameter is something that will be known at compile time and same exactly the same you have for templates you will have it for buses and then here what we do is just we Define this array of of uh dates using this uh this uh this parameter and and

the nice point is that then everything fits well with the templates because for instance here I can define a template with a parameter n that uses an input with uses the same parameter and then everything will work well with the sizes of things and so on okay and then of course then you can call another template with the same end but then I pass field of the of the array of dates and everything matches the types and and everything compiles okay in general I would say that clearly this looks nicer in the and it's far more readable okay otherwise there will be all this amount of signals around all mixed you have to choose whether you

have a raise of arrays or many arrays so it's just uh much cleaner and easy to to read okay now we we we go step further and we mixed buses and tax tax something we introduced kind of two years ago and uh they we were having a bit of subtyping with tax and now we will have types and subtypes this is what I want to present here with this mix of buses and tax so the point is is is this that tax provide a simple form of subtyping okay we don't have inheritance and things like this but we get a little bit of subtyping uh with with tax but now it's really far more powerful combined with

uh with buses because now we have types and then we can just uh get a little bit of of subtyping with with uh with tax and then what happens that we create new types with buses and we Define subtypes Rel sub type relations using tax okay so you you see here that then when you define a bus or use a bus so Tex can be inside and outside and with different meanings if you have it inside they somehow are restricting every instance of this bus I'm seeing that this field has this property okay so I'm restricting what should be in the in the bus and if I had it outside when

using the bus then I'm resting the particular instance of the bus okay so I can do it both I can Define find something that I always want to have this property in the in in the field I add the tack inside the bus but if it's something that maybe sometimes I need it and sometimes I don't then I add it outside when using it okay so the the point is somehow that before we were all with t with signals we were only able to express TS properties of a single signal now since we can put a tack on a whole bus we can Express properties of a combination of signals okay so it's much nicer in this sense later on if you add verification techniques and so on it will go much better because we can check

the semantics of of a whole bunch of of signals that go together okay so let's see it in in the in this in the example of days and going a bit farther than this so This what I mean by tax inside okay so I I hear say for instance don't don't be much worried about the semantics of of these tags and and why I'm using Max bit for day and it just to show that you can use different TXS and and as many as you like non one two different things for different signals okay what whatever you like okay so this is just meaning that there is some bound restriction on the on the signals you can get there okay so there

is one thing but then suppose I create this boss which is profile for an ID and then for a a bunch of of dates meaning whatever and then what I want to add for date is that there a valid date okay so then I add this this TX saying this is a valid date and what's that so I can have a template that creates a valid date from and what's the meaning of creating a valid date it means adding constraints that ensure that the date is valid okay we are creating circuits that ensure things okay so we we can do that and and look if I do the template with without any assumption on the in on the

input signals then I add here constraints and so on checking all the properties the properties of of the of the day the month and then also the global properties of if the month is this one is January then it should be between 1 and 31 if it's blah blah blah okay but the difference between the input and output and the fact that whether I already know some property or not suppose that I because this is used in some context I already know all these stxs from outside then if I know that it should be like this then I have it in my circuit and I don't need to recheck it again you know if you have built circuits many times

you since you're not sure whether you know or you know something or not you keep adding the same constraints again and again and again so using types and subtypes by means of tax we avoid a lot of rechecking of things and which end up with a with a better and more efficient uh circuit okay so now what's the impact of all that in in the in the circum lip so well huge okay but uh but I will just show a little bit so the what what we are doing in this one while writing is adding buses on tax everywhere or in many places and also making it compatible

with different Primes remember that initially we only have this uh this BN uh Prime and and uh and then circum lip was intended to be used with this Prime but now we have kind of I don't remember maybe six uh more primes or even more and then what happens with the ccum lip is not adapted to this so we are just ensuring all the all the all the circuits that we can being compatible with every Prime okay so of course you will use which prime are you exactly using and so on but you can you can make it and and uh and this will be a nice uh a nice Improvement so the the nice thing

is that we have added this these buses and and uh and tax and still we' have been able to prove and formally prove that in most cases the number of constraints is Remains the Same well when using minus o1 okay ah by the way which is now the default Until Now the default was uh uh O2 but the from this release on the default is 01 because many people is using circum for plung and then o O2 is not the the the the way to go okay so from on this is the default okay so keep it in mind because it's important um and

uh and uh and of course looking at the at the new circum Li will help to understand and and and get ideas about how to use and where to use this so let's show a simple example of of the one single example of this use don't know okay so let's come back to this baby jabjab electric curve so you have the the the the the others and so on for for the twisted uh eward form okay look there point it's just like this you you have six six in uh four inputs and two

outputs no meaning apart from X Y used in the name and then you have the the version the Montgomery the the the others for for the Montgomery form and all of a sudden now it's no longer two signals but an array of Dimension two okay so as the Creator uh I was not there so uh and and and you have this okay so for instance this this difference but even more if then you look at the conversion conversion from OS to to to Montgomery and back so here you see you have even this kind of well it's not the type inconsistent but you you inconsistency

but you have there two express the point with two signals and here array of of uh of Dimension to okay but it's all the same because are two signals okay but it's not it's not helping to to to read and also it's clearly error prone because you can mix things that you don't want to mix okay so let's do it with buses Which is far more natural then I have a type for either spon at Point okay so uh two fields and that's it and then oh what a nice thing okay you see this P1 point at Point P2 at point oh now I go to the to the

montomery form another bus okay so Montgomery point then nice again you look it's clearly different okay and we you will never mix both because you cannot pass one type to the other because the the compiler would say no we say type error okay and now look it matches perfectly you get a conversor that takes an adward point and produce a momary point okay and same reverse okay so now it's readable and thanks to the type check you have type safety okay so it's clearly more reliable of course it's far more

readable and more reliable you can you understand a bit more what you're doing but now let's do this with tax then the point is this subtyping so because we've seen that they're all points so should we have these two points well a proposal is no use only points and then use Stacks to distinguish them so here you see you have points and then you add the attack Edwards and in the other way we don't add a new boss but we use the same but we had attack Mongomery okay now you cannot mix them again because you will check whether you have the T on you or or not and of course except if you for some

reason decide to to add yourself two TXS which you I mean still is possible to make mistakes like in other languages but on purpose you have to define a type for something that you really don't know if if it it is fulfilling the properties or not okay so there is the kind of things that will be prevented thanks to types in in this context okay so then what we have is this the the and this and then when you have the conversions everything matches again because here I will get this Ed point then I get an output point with the Montgomery attack that will be that I will be able to use there in the other

because it has attack okay everything matches types and and it works nicely okay of course all this is checked by the by the by the compiler in the type check and it has no impact at all in the amount of constraints and so okay if you need to add some extra constraints because you need to be sure that that the conditions that you have Associated to the type are met then you add constraints okay but this is the what you should do it cannot be that you assume that something fulfills a property but you don't have constraints because then of course uh maybe what you produce with the windows will fulfill it but someone can send you a proof that is not uh fulfilling this and you will just

say okay good so then with taxs and and and and buses we get readability type safety but also we are far more re reusable with the code because maybe we have operations for points that always always the same and we can reduce it in both cases okay so it's just the the the standard situation with uh with subtyping okay it simply helps in re re reusability so finally um what we have in this uh as I said in this new circum we have the we have added this B stacks

and make it compatible and the nice thing is that what we pretend is that if we if someone builds circuits on top of the of the circuits from the circum Lip lip can be in the safe site in the sense that we can even certify that if you only use the the templates of circum Li to create new buses or to add tags and so on then you are sure that the properties are fulfilled and you're using properly the the baby jabjab uh elliptic curve and so on okay so it's these kind of things you're not making mistakes in this sense you're using things properly and you can trust all this okay so you

you are safe just by default because you're building on something safe so will later in in the future we will really give a precise definition of this but this is what we intend to do to to to have circuits that are safe by construction okay and well we are still improving and extending it so it will be ready very soon but it's not uh it's not yet so conclusions so circum is it's really one of the most widely used languages for G knowledge protocols I I as I said many of the of the projects that were shown in the intro are built using uh circum and uh

but until now we we were missing this this uh this these extra types or or this type system a proper type system in the language and this what we are providing with uh in in in this new release okay these buses that provide us the the way to structure circuits it provides a far more convenient type system and then we can ensure this type safety and also we believe that it will help auditing uh ZK ZK projects and uh and the new will take advantage of all this thank [Applause] you thank you very much Albert do we have any questions

oh great yeah so uh at what at one point you said uh that ciron Li 2 was using some kind of formal verification ER what did you exactly did you use and how did you do it well I said what what what I said is that what we we have formally verified I mean you know these are circuits made of many uh sometimes thousands of constraints uh for even for the circum lip for just a a a simple part just using one of these uh um circuits in the circle lip okay so then but is imagine

that you want to check that introducing all this you are not having an overhead in the number of constraints okay so you want to check and and also you want to check that you are seeing the same because the circum Li was already audited okay so imagine if we just don't know if they are the same after changing we need to audit again so what we have verified for most of them and and the ones that they are they they don't fulfill the property of being exactly the same as before is because we already know that we have added some extra constraints okay because we know it in purpose or we have removed some

constraints because of the tax we know that this was already checked so then we don't need to add them but apart from these situations we have proved that the circuits before and now are the same but simply are the defined and described in a much better way okay more readable and also uh nicer in the sense that you can use them in a safe way okay so this is the the the key point so this is what we have verified I think we we have time for one more question uh could you perhaps compare and contrast what sorts of things can go in buses and what kinds of things can go

in templates for example sorry in buses is in is it possible to put something like a constraint or a witness generation procedure inside of a bus such that all instances of the bus have that or not no we that so that would okay nice question so the thank you so there is the point where we have code inside the the bus and and and and this producing uh constraints so we are not allowing any code inside the bus by now but probably we we we will but only to Def finally so for instance if you want to have this

recursion it would be good to to to have using the parameter deciding whether some field is there or not and then you can have a nice form of because the the the the the notion of of of null of null in in in in a circuit is not easy okay so it's it's a weird it has a weird semantics but if you cannot code you can have a a a conditional saying well if n is zero then you don't have this field okay for instance and and then you can probably add some code this way I don't think we will like to add code in the sense that if you have some some bus it will just directly

introduce a set of we we are not planning to have this great thank you very much let's thank our speaker once again [Applause]