Vamp-IR: a universal language for arithmetic circuits

Transcript

hello hello hello hi okay hello everyone i am uh josh fitzgerald i'm from anoma uh and i'm going to present to you a vampire it's a language for arithmetic circuits so first thing is why make a language for arithmetic circuits um the answer is it's a big pain to write circuits uh we have dsls which can help with this but

um dsls are often highly tied to a specific proof system or back end and if you want to change the proof system that you're using or change the back end library then you often have to rewrite the circuit essentially from scratch and uh it's it's uh challenging um if you're like me you might find it fun to just mess around with polynomials and try to figure out if they're equal and and things like that but it's not a very efficient use of time uh at enomo we have a multi-asset shielded pool that's the masp here in the in the middle

and uh it was written for group 16 in the bellman library we wanted to extend or convert that to another proving system like plonk so i spent some time trying to do this i read the um the the spec for the masp and uh tried to translate by hand all the polynomials into planck library and once you do that you're left wondering did i do that correctly did i make a mistake did i leave out a con a critical constraint somewhere

the worst thing that could happen if you're writing a circuit is that it's under constrained and there is some satisfying solution to that circuit that shouldn't be there and it's hard to tell when you're working with complex circuits if if you've done it correctly also um have you done it in an optimal way it's just it's really difficult so why don't we have a language for arithmetic circuits that can represent an arithmetic circuit canonically and universally so that that same circuit can just be

ported to whichever library you want to use and then all you need to do is write a compiler from this language to the backend library and that takes care of transforming it into a form that those libraries want so that's the the basic idea behind vampire on the other side you can write dsls that uh compile two vampire um so at noma we have uh some languages that are going to do this we have juvix and alucard juvix is our dependently typed programming language for validity

predicates and it will also create a an arithmetic circuit that represents those predicates a la card is a lisp like tool for for writing circuits it's going to have some some helpful gadgets like smt solvers and things like that to to make writing circuits easier and there's no reason you couldn't write a compiler from say socrates or circom those languages into vampire as well and then on the other side you can change vampire into r1cs or or plonkish

constraints and then if you need to refine it further for a particular library that you're using you can do that as well all these arrows are compilers so what started as a cryptography project has now become a compiler project and we've got a a great team of compiler experts who are working on this now so let me show you how arithmetic circuits can be represented here are

two arithmetic circuits i do them like they're printed circuits it's a really good analogy for what they actually are because you have these different nodes and they're connected by wires and you can apply a signal to these nodes at the top you could also wire two nodes together and that means that those will have the same value so imagine applying a voltage somewhere if you have wire connecting to another node that node has the same voltage i guess um

i'm not an electrician i don't know if that's actually true but so yeah here's our two circuits um an arithmetic circuit is just a representation of the computation of a polynomial so here we have actually the same polynomial twice um this side is the factored version the other side is multiplied out two very different looking circuits they represent the same polynomial but the order of computation the computational steps are different uh over here you add two pairs of things and then multiply on the other side you

multiply like four pairs of things and then add them all up all right oh yeah this is what i was saying earlier you can you can take two circuits and join them together by drawing wires across what this lets you do is treat a circuit like a function all you have to do is specify the inputs and outputs of the circuit and then when you compose two circuits the compiler will know how to handle those inputs and outputs it will make

sure the the inputs of the outer function match the outputs of the inner function you know also this wiring here is what you would actually need to do if you wanted to do a modular uh if you wanted to find the remainder by uh dividing by 16 you would have to do this you the calculating the remainder is easy it can be done here but you need to make sure that the remainder isn't too big so then you have to use a range proof on the other side so this is actually what you would do

an arithmetic circuit defines a system of polynomial equations as well um so there's uh our system of equations on the the right side there along with that range uh four it's a four bit range circuit here okay you can also represent an arithmetic circuit as an expression tree that's because an expression trees just polynomial if you have addition and multiplication so there's another representation here all right

you can also represent an arithmetic circuit as a kind of flat list of gates and wires so we have five inputs it's for z d and they each have an index and then you can list the uh the operations we're multiplying one and one that's a times a multi-two is b times b so we're getting a squared and b squared and so on the box on the far right those are equalities if you are saying

the the gate at index 11 is equal to the gate at zero you're s you're drawing a wire that is basically that's this wire here okay so sometimes you need extra equalities to get all the wires in the right spot that's what those are okay so i want to give an example of what it would look like to write a circuit in vampire now that we know what circuits are i think you can kind of see how this will work together

vampire uses something called an alias it's just a definition that takes some expressions these expressions define a circuit and it also gives a signature to that circuit just like a function signature that allows that circuit to be composed with other circuits circuits don't have like a natural composition but if you can specify inputs and outputs then you can do it okay so here are some definitions um this

top one here def bool x uh this does not have an output it just has a single input x and it checks that x is zero or one it does that by multiplying x by itself and making sure that those are equal zero one of the only uh solutions to that polynomial equation so it constrains x to zero or one this 4-bit range function here this is for showing that x is less than 16.

you can use a uh another alias inside of a definition just like this um so this is a squared equals a b squared equals b and so on and then at the end you uh pack those bits together and uh constrain them to be equal to x okay uh on the other side i have three different aliases but the circuit is the same so it's like the same circuit board just with different nodes uh selected or designated as inputs and outputs

so if you want to do mod xy then you want to return r if you want like integer division then you return q if you want div mod like like they have in python or whatever it can return the pair qr same circuit just different signatures okay so this is a tiny circuit which could be used for like an educational game uh in this game a player submits a triple of numbers and they're supposed to receive a score of one like a point

if though that triple is pythagorean um so in a like a zero knowledge uh context what the player would have to do is submit their uh their triple and the score that they claim they should get and then a verifier could check this in zero knowledge that the score is correct given uh the triple okay so a verifier needs to check that if a squared plus b squared equals c squared then the score should be one and if a squared plus b squared is not equal to c squared the score should be

zero okay so i have two aliases defined to do this the top one is pythagorean this checks that x y and z satisfy the pythagorean theorem the middle one there it might be a bit hard to parse exactly what's going on but what that is going to do is uh check if uh x is zero uh then the bit should be one um and if x is non-zero the bit will be zero

you can think about the cases there just do like a case analysis and you can see that it works out and finally at the bottom we have the actual circuit we just say s the score equals is pythagorean abc so if the pythagorean circuit is satisfied then the value in the parenthesis there will be zero and then the the is circuit should output a bit that is one which is the score if the pythagorean circuit is not satisfied then the value there in the parenthesis is non-zero then the is will spit out

zero for the bit the score will be zero okay all right i i'm running out of time so i will breeze through these compilation steps these are this is an example compilation steps here we have like i said we have a team of compiler people who are taking over this portion of vampire i think they're going to change and improve this but this can kind of show you how to get from a vampire circuit that's actually

written in vampire to say a plonk circuit so the input is parsed and put into an abstract structure tree like this got the definitions on the left the actual circuit on the right you can put this into an anf form where you have inputs at the top of the list then you have your functions your aliases and so on all right uh you can expand this um

pythagorean and is they have they have polynomial equations defined inside of them that you can replace those with so you can expand like so you can make some little optimizations like the the equals at the bottom 10 14 that's unnecessary because 14 is an input 10 is also an input so there's no reason to ask the prover to input two numbers that are the same you can just use the one you know why not uh you can do things like change subtractions to additions uh using uh

constant multiples um things like that and then you can plonkify it so i'm calling this three plonkification because it's using like three wire planck um and uh you can kind of see that there's almost a parody here but uh we end up with one less item in our list of plant constraints because uh two operations i think it's uh 11 and 12 can be combined if you're using a plant gate with three wires okay so we have some interesting promising

directions that we're going to [Music] do some research on and incorporate into vampire if if if possible one is tools from algebraic geometry ideals varieties uh grebner bases there are there are some things there that can be useful uh for showing that two circuits are the same for instance smt solvers uh which can also help show that circuits have certain solutions stark circuits

starks use circuits as well as snarks they're a little bit different but we can use vampire to represent those circuits as well and category theory uh cartesian closed categories compile two polynomials apparently we just started talking about this recently uh so we may be able to compile from juvix to vampire in a in a different way using this fact very interesting stuff very new and preliminary

but very cool here's our vampire team i'm really excited that we have these people working on it i think they're going to do a great job so thank you [Applause] is uh yeah it's open source uh you can find

it at uh inoma or github uh look for vampire uh it is not usable yet um we are are working hard on our uh our tree our abstract our ast and that compilation steps uh so you can take a look and see how it's going uh not usable yet but i i hope to have something at least compiling to uh plonk um very soon uh so i think it will be will become usable uh soon yeah more questions so yes that's all thank you

[Applause]