ZK7: VampIR: universal representation for arithmetic circuits - Joshua Fitzgerald - Anoma

Transcript

[Music] now we will begin with joshua's talk on vampire hello i'm joshua fitzgerald i'm with anoma and i don't know if david and joseph are still here or not but we should definitely talk because your your expression framework is uh hi uh very similar to uh what we're trying to do with vampire um so yeah we should we should get in touch um

vampire is a a universal intermediate representation for circuits we we were at a noma we were looking for a some kind of intermediate representation that we can use to sit between um our programming language we have called juvix juvix is a dependently typed programming language can be used for many things but we would like it to be able to create zero knowledge proofs and so we we wanted something to sit between juvix and a proof system back end

like our zk garage planck implementation but you immediately get a problem if you want to use something like planck because it's so configurable that you you write a circuit for for one configuration of plonk with you know three wires or three variables or four wires or lookups or custom gates or without lookups and without custom gates and you have to change your circuits uh so we really wanted uh something that was uh universal so here's what we have a vampire is a proof system agnostic

language for arithmetic circuits circuits written in vampire can be compiled to any proof system uh using any constraint system or configuration including those with custom gates and lookup tables so out my image didn't show up that's too bad um arithmetic circuits uh just some background they are a representation of polynomial constraints so uh in this beautiful empty box here there is you know just seeing your mind's eye um a

a diagram of an arithmetic circuit where you have inputs at the top and they're joined with wires going into gates like times and plus and they you know they feed together if you've seen that diagram before that's exactly what would be here and on the right side then we have the um the polynomial version they both express the same thing this is for a range gate and this would check to see if the variable y is four bits all right okay

so uh constraint systems uh we have a few of these there's like r1cs and and plonkish and the constraint systems are just another representation of a system of polynomials but you only allow certain kinds of polynomials polynomials of a certain format into the the system uh something that the the proof system back end can can process um with r1cs i you you have this expression that's like a times b minus c but a b and c can be a linear combination of variables right so r1cs allows one product of a linear

combination of variables whereas plonkish constraints have a fixed number of variables i i almost put on here that a plankish constraint has maximum degree two which is like the original uh planck but it's not really true once you start getting into custom gates and things you can you can change that you can expand that so because planck is so configurable really i i couldn't think of anything else that really captures what it is other than it's it's got a fixed number of variables you can change the relationships that those uh variables

must have so these two different constraint systems uh mean you have to write a circuit in two different ways and with plonkish there's actually many more ways that you could that you may need to to write your circuit so yeah there's some annoyances with constraint systems that are limited like this um circuits written in different constraint systems can look very different constraints written in some constraint system may not resemble the source if you're if you're implementing

something it's got a canonical formula uh then but that formula doesn't fit into your constraint system then you have to rewrite and you have to break your your polynomials into pieces and suddenly it doesn't really resemble uh the original source so you can make mistakes that way circuits have to be rewritten in order to use them in another proof system or configuration it's a big pain it's also painful to benchmark a circuit in different proof systems or configurations you might have a circuit that you suspect will perform better with

lookups enabled for instance but lookup gates come with their own cost they're not free so you want to know is this circuit will it work better with uh with lookups or not um you'd want to to use it in in two different ways one with lookups and one without but you have to rewrite the circuit in order to use it in two different ways and then you have to verify that circuits are actually the same what if you made a mistake when you were rewriting the circuit so that's a challenge uh some more annoyances um

no canonical circuit format so it's harder to take someone's circuit that they wrote specifically in a back end um proof system like implementation and then translate that into some other proof system implementation iterating on circuit designs is difficult make a change it might change the the entire thing front-end languages or dsls can become very tied to a particular constraint system or proof system implementation

so you're kind of stuck it might be easy to write circuits using a particular dsl but then what if you what if that dsl only ends up using r1cs but you want to try it out in plonk then you have to use some other dsl so yeah there's a couple of issues here's an example of some circuits that don't resemble each other because they're written in different constraint systems they also don't resemble the source this is the the formula for a twisted edwards addition on twisted edward's elliptic curve

so you've got three points here they have x and y coordinates and those points add together according to that formula up there if um this these two constraints at the bottom are satisfied uh so we've got six variables here the capital a capital d these are just parameters that specify a particular curve i didn't want to write the huge numbers out so i just use those so these two constraints here neither one will fit into r1cs or most uh plunkish configurations as is

so uh here's here's that those same constraints rewritten using r1cs and three-wire planck this is like the original planck with three wires a maximum of one term of degree 2. and you can kind of see how this works the o variables are auxiliary variables that have to be added into the system so that your your constraints um can fit in so i like in this first line here under r1cs we are

kind of saving x1 times y2 in a new variable called 01 which then we can use later if if you remember high school math you might have to take system of equations and eliminate variables use substitution that kind of thing we're kind of doing the reverse here we're adding in variables so that we can actually use more constraints of lower degree or that that fit the format similar things happening on the right side with three wire plonk but because three-wire planck doesn't allow

an arbitrary number of variables in in the system there we have to include more constraints all right and compare those to the originals if you showed me either of these circuits at the top here i wouldn't know unless i sat down and did the the math that they actually correspond to what's at the bottom right would you they don't look anything like it and it's some work to recover those original equations so the cure for all these problems is

we need a circuit language that allows for arbitrary polynomial constraints uh then we can write arithmetic circuits in a like a canonical way that's universal so we just get rid of the references to any constraint system format whatever and we just write polynomials after all arithmetic circuits are just an expression of a system of polynomials so if we really want to write arithmetic circuits in like their their native language we should just use polynomials that are not constrained in any way all right so that's that's easy enough you can then

take these polynomials and convert them into r1cs or plonkish constraints you can do some things like taking any multiplication of variables and saving them in a new one just like on on previous slide but we we still have a problem if you're if you're just using polynomials what do you do about proof system back ends with custom gates and lookup gates i had hoped and my my hopes were quickly dashed but

i had hoped that we would be able to search through a list of constraints for constraints that match certain pattern and then replace those with a lookup gate or a custom gate um so that we didn't need any anything but polynomials i i just really wanted this pure polynomial language it's not quite doable searching through thousands tens of thousands of constraints for particular patterns um not the most efficient and there's a pretty simple thing we can do to to avoid having to do that

um yeah i basically just said this the arbitrary polynomial constraints aren't enough we need some extra information we need to indicate if uh certain uh sub-circuits or sets of polynomials could be replaced with a a common custom gate or lookup gate so uh this all these problems gave rise to vampire uh vampire stands for uh well the v stands for vampire um

vampire aliased multi-variable polynomial intermediate representation so the design principles for for vampire are we should have a representation of a circuit that expresses the intention of the circuit and hopefully we can do that without including a bunch of details from the particular proof system that you want to use or constraint system or the the implementation of that proof system uh it should just express the circuit itself the circuit is a is one one thing and it should be kind of

encapsulated there so we can separate our concerns a representation of a circuit should be flexible enough to allow for custom gates and lookup tables all right so how does vampire work vampire accepts multi-variable polynomial constraints of any format so this this achieves our our first principle which is polynomials in any format i don't have any reference to a our particular proof system or constraint system

so if we were rewriting those uh twisted edwards edition formulas in vampire we would just use the original formulas at the bottom um these are okay these are slightly modified from the formulas in the in the book because they usually write the write them as a fraction so but all you have to do is multiply both sides and you can recover this these polynomials in this format with no no division at all but it basically looks exactly like the formula you would read out of a book so it's much easier to check

all right for uh for indicating look up tables and and custom gates we just attach a little bit of extra information which also is very natural to do uh which is you can take a a sub circuit which is just a list of constraints and kind of group them together and give them a name that you can reuse later on uh you definitely want this just for for ergonomic reasons you would want this right so the vampire language allows collections of polynomials or sub-circuits to be given a reusable name called an alias uh the aliases

uh maybe maybe macros and a more a more appropriate name for these but then you don't get the nice uh acronym right so uh yeah we can call these an alias here is a definition of two aliases and we have check on sw curve this takes two coordinates and checks that those coordinates are the coordinates of a point on a particular short wire stress curve and you can see like if you know formulas for elliptic curves the the polynomial that's there it just is that is the formula

so nothing nothing complicated there and uh then we also have a range 4x this is um checking that x is uh four bits um and you saw those equations earlier okay aliases can have a signature kind of like a function signature which indicates which variables you should consider to be outputs one of the awkward things about programming in circuits is that arithmetic circuits

don't really have outputs it's not a computation where you put something in and get something out but a lot of the computations you want to check are are function like with outputs um and so what we do is we have these signatures along with aliases which indicate which variable should be considered outputs which which then lets us compose uh aliases as if they were functions with actual outputs so that's what the x1 y1 x2 y2 arrow

x3y 3 indicates so the the x3 and y3 would be outputs of this alias outputs and quotes okay so yeah once you have outputs uh then you can compose these as well so here's twisted edwards add done twice so we're adding three points together and getting a fourth as a result so in the parentheses we have our first one twisted edwards add x1 y1 x2 y2 because of the definition

that will expand out into these polynomial constraints and it will you know save the results so to speak in x3y3 uh and then those will become the the two first coordinates down here and uh you know there's a namespace thing going on here to prevent the x3 and y3 from from colliding there so this gives you a really convenient way of expressing circuits it's fairly ergonomic fairly readable and also

this solves our our problem with lookup gates and and custom gates if you're using like standardized uh aliases and that the like a back-end proof system knows about then it can decide uh to replace certain aliases or sub-circuits with a look-up gate or a custom gate because the original polynomial formulas are there a proof system that does not have lookups or custom gates can still use the exact same circuit format

but the the whatever is compiling this this circuit into format that the like the back-end proof system implementation needs can make those decisions uh for itself all right so a compiler targeting improved system that has lookups can replace this four-bit range gate with a lookup table a lookup gate okay um so a benefit of this i wonder if i'm missing another image here but dsls or front-end languages

can have a consistent target to compile to and then also on the back end side proofs various proof system implementations can can use vampire as a consistent source for for circuits and they also may be able to make certain decisions about how to interpret that circuit in a way that makes sense for its particular features a complicated circuit can become fairly readable this is an example from

the zcash protocol spec document this is the sapling output circuit a fairly complicated circuit uh not not as complicated as the spend but the output circuit is here uh we've got basically four lines and um yeah yeah i'm missing more images that's a shame uh if you if you look up the sapling spec there is a part where they they say exactly what needs to be checked in the circuit for for the output

it looks very similar to the lines that we have here so you can you can write these and then and just visually see that it matches what what you expect it to look like so you can you can check circuits against a spec pretty easily also a circuit written in vampire can serve as a speck if it's uh it's universal and and canonical and expresses the intention of a circuit you could be able to use it as a spec itself okay i think that's it yeah there's the zcash protocol specification that i used in part of this so i think we've got just a little time

left um are there any questions oh here's one hold on yeah first of all fantastic great talk and uh really cool work uh i have questions so do you perform sort of sub expression elimination and like you know extracting the common variables out all of those kinds of optimizations at this level or is it like a something at a lower level than that uh yeah um i think at this level uh i mean these these expressions can compile to like a it's like an ast type of thing and and we can do some manipulations

there um and uh yeah you can also write circuits in uh multiple ways since uh vampire does allow general ones you can you can write a circuit in r1cs let's say and then the the general one and uh and eliminate the variables and just check that they are the same um it's easy enough to do by hand if your circuits are small but you can also do it on that automatically that way of a follow-up question also yeah yeah uh and also how do you handle non-determinism in this uh yeah where do witnesses come from um how do we handle non-determinism and

where do witnesses come from all right uh yes so um the the the witnesses will come from like certain initial inputs um that are that are you know independent of everything else and the proof system back end uh implementation will receive a list of those initial inputs and then it should be able to figure out how to calculate any intermediate values and assemble the the witnesses that way because these aliases at least most of them are

definitely going to be like common things that are that are in a standard library it should it should be able to know how to how to compute witnesses for those that has the initials okay cool two questions first is just a very minor point uh i noticed uh on the uh range check the there's a word bool x is bool in this case just another alias that would represent the constraint of binaryness yes yes i had i had more examples in there and i deleted some of them to save some space bool was one of them sure uh yeah so uh bool uh bool x would is an alias that uh that just takes x

times x minus x equals zero and then the other question was just uh in terms of implementation uh how far along is this is this something that people could use right now um what's the sort of status in that regard it's very preliminary uh we have some some prototypes and they don't do all the things we uh want vampire to do yet so yeah we're just starting um so not usable yet but we are working hard on it any other questions would help or why don't you take uh so

would you have for example that uh the uh languages like the asl languages or or other languages export part of the structure so that you don't have to write like another polynomial so another system uh and would it help would it help that the languages the corindia cell languages export information so it says did you export these constraints and these constraints are for this template or are for this specific function so this could help also to optimize and to get the information on that site yes yes uh uh front ends um yeah we're not we're not sure

exactly how much a front-end language might need to know about the proof system back-end on the other side of our intermediate representation uh but but we're thinking that some some amount of that information the configuration or something like that might be very helpful in the in the um like a dsl to to to know about they may be able to export that information into like a separate file that sits alongside a vampire vampire expresses the circuit and any any other information could be you know separate that way you can you can have a circuit

which is portable under different configurations but yeah front end might want to include some some helpful information very cool i think we're actually at time thank you so much for the talk [Music]