VampIR: LLVM for polynomial circuits, now with benchmarks!

Transcript

[Music] hello everyone I am Josh Fitzgerald I'm from heliacs I'm going to present to you uh vampire our programming language for arithmetic circuits that is universal and does not um is not tied to any specific back end or proof system implementation so um yeah we're calling it like llvm for polynomial circuits meaning that we have one representation for arithmetic circuits which can serve as a target for front-end languages and

also can be used in any proof system back end as well so if you can compile into vampire you can take advantage of any proof system backend that you would like and you can also choose from a whole slew of front-end languages as long as there's a compiler to vampire so this is a workshop uh it's I'm hoping to make this very Interactive and I'll be live coding up here if you want to live code yourself if you brought a device you can join the workshop code space so there is a QR code here that should take you there

if uh you can't get that on your device you can go to anoma's GitHub find the vampire repo there's a branch called ecc6 click on the code button and it should show you a code space called symmetrical xylophone which you can use to to code along you'll be you'll have the same version of vampire that I have and it even has some syntax highlighting as well okay so I'm going to leave this up a little bit while I give kind of an introduction to vampire just to give people a chance to use it if you want to um

at uh at heliacs we we want to use zero knowledge proofs in our stack and our our main goal with um with our stack is we want things to be not monolithic uh we want to be able to let people spin up all sorts of different blockchains with different security concerns and and different properties including privacy uh if you want privacy then you can use uh zero knowledge proofs snarks Starks Etc um but there are all these different

proof systems to choose from each with their own properties and different implementations of this proof systems which also differ and that presents a problem for us at Helix in building a Noma because we want our our stack to be as open as possible meaning you're not forced to choose a particular proof system if you want to use a proof system that has different characteristics that fit your use case better you should be able to that's uh that's how we think of it so that means we need a way of expressing our validity predicates which is what we

call them on a Noma in in a way that is universal for for all proof systems okay so um I'll give just a little bit more intro then we're going to be doing some live coding um we may or may not finish the live coding portion uh we're going to be looking at the Blake 2s hash and and coding up a circuit in Vampire for blake2s we'll be compiling it we'll be creating proofs and verifying our circuits as we go if there's time left I'll give you a little

progress report about where vampire stands now and where to go if you want to get involved okay so I've covered this a little bit already so I'll try and go fast uh we have this project called the masp it's the multi-asset shielded pool it is a component of our namata chain which is in development right now the masp was written a few years ago in Bellman and it uses the growth 16 proving system uh we were interested in taking our masp and adding something like recursion to it

so we were we were interested in looking at Halo 2 can we use the mask in Halo 2 uh we were also thinking about uh using uh Planck without uh recursion uh maybe to get some better efficiency so we were wondering can we write the masp in Planck or Planck up or Ultra Planck which has lookups so I tried rewriting the masp in these other proof systems and it turns out to be quite difficult to do by hand there's also lots of problems because uh something that's nicely audited like the masp in a certain

circuit format when you apply Transformations by hand to rewrite it in another format you could introduce new bugs that that you don't see and it's actually quite tricky to do well and it's also tricky to do efficiently so what we wanted is to be able to write a circuit like our masp in a universal format like vampire and then we can have that circuit be audited and tested very well and then we can take that and Port it into any back end that we choose that also lets us compare different backends for for Speed

and efficiency and so on and something else we would like to do is have a nice Target for front-end languages as well we have a language called juvex it's a dependently typed functional language similar to Haskell and we can compile from juviks into vampire and then prove circuits with a couple of different backends right now theoretically we can compile to and from other circuit IRS like Acer a Seer is the uh

uh intermediate representation for circuits in Noir used by the Aztec team so uh and we also have aeroscript is another possible Target for compilation to and from Vampire and with Seer and airscript for instance we could write a circuit in juviks and compile it in barrettenberg or Bellman Planck up Halo 2 or Winterfell or or any other thing that we write a compiler for um we could also or someone could write a compiler from say Socrates into vampire and now circuits written in Socrates

have access to all these different back-ends okay uh arithmetic circuits these are the the objects that that vampire describes an arithmetic circuit is a representation of the computation of a polynomial so I have two arithmetic circuits here um both have five variables and if you look at the equations down here at the bottom you should see that they're actually the same polynomial but they're computed differently uh this uh this one on the left

is more simple because it's been factored out right they're actually the same so these are two different arithmetic circuits but they represent the same polynomial so yeah arithmetic circuits represent a computation of a polynomial not a polynomial itself um you should also see how these circuits they're not like functions they don't have inputs and outputs they just kind of have inputs and they either satisfy the circuit or don't okay um

so that makes it a little uh weird uh you know we're very used to using functions in in programming but with arithmetic circuits you kind of have to simulate functions because they don't naturally have them okay arithmetic circuits can be joined by wiring them together and it's like literally what you would expect if you had an electronic circuit and you you wired two contacts together those contacts will have to have the same voltage or or whatever right so here's two circuits one does div mod and the other does range for that's uh

so it's checking to see if something's four bits and if you take the remainder of divmod and connect it to Z over here in the range circuit you're showing that the remainder from div mod is four bits because R and Z have to have the same value okay arithmetic circuits are can also be thought of as a system of polynomial equations or or a way of computing a system of polynomial equations so all these circuits can be represented with polynomials like here on the right and this is the the format that we

choose to represent them with in in Vampire okay so uh that's the end of the intro uh we're going to proceed with live coding demonstration uh we're going to be looking at the Blake 2s hash function you can find the spec to Blake 2s online I've got the URL right here I've got the most important parts for us today up on the screen we're going to be writing a circuit that checks uh correct computation of function G if you look at function G what it does

is it takes a vector of 16 words a b c and d are actually just indices of the four words that we are working with in this round of the function each round you do a different operation on on a different set of the forward of 16 words and X and Y are pieces of the the state that is getting folded into all this okay so uh you can see what we do we're taking the forwards which are V of a v of b v of c and V of d and we're doing a couple of simple operations adding them mod 2

to the 32. W is 32 as you can see over here doing a rotation and xor so we need to write circuits that do addition uh mod 2-32 rotations of different amounts and xor okay if we can get all of those then we have our our function G if you look at the Blake 2s spec function G is like the the core of of everything it's it's done many times

but there's not much else to the hash function Beyond function G it's it's like the most significant part of the of the hash function um we probably won't get through the entire function G but uh we're gonna try okay this is a simple definition in Vampire uh we call them aliases mainly because it let me get a letter a in a convenient spot in an acronym for vampire but the definition is a name followed by the inputs equal sign you have curly brackets in the body of the Alias you have

Expressions that end with semicolons and at the end you have a return value that's the out with no semicolon and finally after the curly braces the closing curly brace you have another semicolon so we do a lot of a lot of what we're going to do today is defining these aliases okay here's an example this is the function that constrains an input to be Boolean so we have death Bull X then there should be an equal sign in

there then we have x squared equals x that's an expression that constrains X to be equal to its Square the only two solutions to that are zero and one and then this also returns X that's mainly for convenience because you may want to combine some lines just do a little inlining there you wouldn't have to return X to constrain X okay but this one returns X which is nice then below that you see Bool a this is a constraint expression that's using this definition so what that will do is allocate a new variable a and add a

squared equals a into the constraint system yes because there is some similar things to work on extension Fields or are we only working over gf2 uh vampire uses big integers which can then be reduced into field Expressions later vampire itself is not aware of of fields um it's uh it's basically uh integers only specific it's it works in integers uh vampire itself does not have any awareness of uh finite Fields so you

have to re-implement it uh starting from here I want to build a so like later in the compiler stack uh the integer representations are converted into like finite fields um but each proof system uses you know different elliptic curves they have different like base fields and scalar fields so vampire itself trying to be agnostic to that stuff does not uh it doesn't use finite fields in the language itself if you wanted to simulate uh finite field arithmetic in Vampire you can do that using uh you know like modulo and that kind of thing

um modular arithmetic you can use that to to simulate finite Fields although it's a bit expensive okay in Vampire okay um usually you want to avoid doing that if you can okay okay uh Just One More Concept I want to make sure that we look at is this keyword called Fresh uh an arithmetic circuit is not uh it's not really a program it does not uh it does not know what values are inside these variables

and um so it can't like compute values that need to go into these variables in a zero knowledge proof system the prover needs to compute all the values of all the variables that they are are submitting as part of their proof so the prover needs to know how to compute these vampire if it were only polynomials only these constraints wouldn't know how to do this so we have fresh there's a similar Concept in circum I believe um they've got a symbol for this but what fresh does is it allocates a brand new variable fresh variable

and the expression inside the parentheses tells the prover later on how to compute that variable um fresh does not create any constraints so you have to be careful with using fresh just because we have a fresh X Mod 2. does not mean that X will actually be or that b0 I guess will actually be X Mod 2.

it's not constrained um if you just use fresh you're just creating a a new variable the bull that I've put in front of fresh actually applies the constraints does that make sense fresh does not create constraints you have to apply the constraints separately okay all right there's more in this presentation oh yeah we can do some cool stuff like Korean and we have tuples I'm going to kind of fast forward through

this um we have lists uh we can you know find heads and tails of lists we can even iterate over lists we may not be using some of those features in our live coding but we do have them pretty cool okay so uh I'm going to switch to the live coding portion now okay oh good okay

so uh I'm just going to create a file for us to work in see if I find it over here all right um how does this look to you can you can we read that even up there okay good all right so let's start with our first definition um I will be switching back and forth with the Blake 2s spec that I had up here earlier

let me get that prepared uh okay so there that there's that uh we need to do um Edition mod 2 to the 32. so we're going to start by working on that uh when you do mod 2 to the 32 well when you do mod at all the the result of modular division needs to be within a certain range right it's not correct if it's larger than the divisor right

so we need range proofs in order to do modular division so we're going to start with some range proofs the simplest range proof is something we've already seen which is uh constraining X to be zero or one that's it shows X is one bit right it's a range proof so I'll quickly just get this going um should be the exact same as what we saw before So Def Bool x equals uh in curly braces

x squared equals x and then we're going to return X as well that lets us use x in you know we can compose this with with other stuff and use x uh don't forget semicolon at the end and now that we have a definition we can apply this constraint to variables if we want so to do that I'm just going to write y with a semicolon bull y with a semicolon this is this is an expression it is a constraint it will apply this bull definition to Y meaning that Y Must Be A Boolean

so we have a circuit here it has one variable y and what this circuit does is check that Y is either 0 or 1. okay so uh we're going to go ahead and compile this and create a proof and then verify the proof and then we'll come back and put some weird value in for y and show that the verification fails okay so let's see does this have my history in it no no okay so the command we're going to use if you're in the code space you can use

Vamp vampir for Vampire uh I'll just show you we have a helpful CLI that will print out your options and and commands we're going to use Halo 2 today so we'll do Empire Halo 2. our first step is going to be to compile and what are we compiling uh our source code is blake2s.pir and our output let's call it

Blake to blake2s dot uh Halo 2. okay this will take our circuit that's written in vampire and uh compile it into a universal format that is then put into like a binary file called blake2s.hilator 2. and uh if I haven't made any syntax errors that should work okay vampire does have a type system it does some some type checking we need that in order to handle uh certain like compositions of functions and higher

order functions um so this lists the definition Bool as a function from integers to integers okay yes under the hood is that transpiling to rust and then compiling a rust binary um no we use rust the compiler is written in Rust but it under the hood it is [Music] um uh it's uh compiling to a uh basically a tree okay um but it's using the like the rust Halo 2 Library like but at the rust

syntax tree level um well for compilation it doesn't use uh Halo 2 at all um Halo 2 hasn't come into the picture yet uh but yeah we're using we're using like rest libraries and rest data structures uh to represent uh vampire uh because the compiler is written in Rust yep cool thanks [Music] circuits meaning that it is intending for usual operating system yes yes yes [Music] um what is um the set we are working on is it a

machine world yeah when we is it a one is this the 32 bits because the Constructor equal x so it's true on any field of characteristic too so okay I don't know if maybe I'm currently seeing my questions uh what is um where are defined the values when there is no nothing else specified I mean where um where are we defining values what is X is it defined over um uh of our Over N over 2 to the power 32 what is it uh yeah okay okay I think I can answer

that um at this stage it is uh it is just a variable it's just a an empty hole that will get filled with some value later when that is filled in we have we already know like what proof system backend we're going to use this is like later in the proving process and uh basically it'll be filled in with a element of a finite field that that proof system needs but right now it's just it's just an empty slot okay you can use constants constants are just big integers and those will be

mapped into a finite field as well eventually but right now um You just have you can have you have variables and and constants which are beginner juice yeah okay okay yeah at this point uh yeah the result of compilation is in is in a binary file um it's uh called uh dot Halo 2 because we anticipate that we may need to have some metadata uh there that's specific to Halo 2 but uh actually I think that the representations of these binaries

um at this point don't actually reference the proof system at all okay uh so let's go on to prove so when we do prove we are now calling the Halo 2 library to do the uh the proving for us what vampire is doing is Computing the witness values now if you remember in this we only have like one variable right and that is why uh but in the constraints system things

get expanded out so that this constraint x squared equals x it's going to have uh multiple well it's going to have a value for x and it's going to have a value for x squared right um so the uh so vampire is taking the inputs that the prover gives and evaluating these constraints to get the other like intermediate variables this were a little bit longer constraint that would maybe make more sense but each each arithmetic operation that we do like squaring here is actually a new variable and the value for that variable

needs to be computed all right so vampire's handling that and then with all of those inputs computed we send that to Halo 2 and it produces proof okay so uh we're going to prove we need a circuit so Dash C our circuit is blake2s dot Halo 2. uh and we we're going to put the output into um Blake 2s uh dot proof okay I didn't send vampire any uh inputs

so it doesn't know what uh what the prover is trying to uh prove with so it's asking the approver for values it's asking for y That's our only variable you can also put your inputs in like a Json format and uh and use vampire that way as well this is like the interactive version which is I don't know maybe nice for a demonstration so let's put one in for y that should satisfy the circuit okay it's generating proven key and improving knowledge of witnesses Etc it says proof generation success um

proof generation success does not mean that the circuit is satisfied because you can generate false proofs all right so Halo 2 took the values that we gave it and it generated proof using the proving algorithm and now we have that proof if we gave a value there that did not satisfy the the circuit we would still have a proof it would still say proof generation success so this this proof has not been verified um okay so now we have a proof Let's uh verify it so uh vampire Halo to verify uh we need the circuit again

and we need a proof Dash p tells you the proof uh and I remember we we put one in for y so we would expect this to pass verification okay yeah so uh you can see here last line zero knowledge proof is valid let's go and redo this and we'll put something else in for y 'all um we'll go back to the prove process and uh put something else in okay we still got a proof out of that but it should be a false proof if I go back to verify okay

um verifiers sent us an error constraint system failure which is what the verifier sends when the the proof fails okay so didn't work okay so that's uh that's the basics of how to use vampire and write a a definition um let's keep on going uh we're going to expand our list of definitions you can do range proofs over a certain number of bits pretty easily if you have a smaller range proof

you can do two of those to get a larger range proof of doubled size right so Bool X is basically a range proof of a single bit so if I want a range proof that is two bits I can use Bool twice and then I have a range proof for two bits so we're going to call this range two we'll have a single input X equals curly braces and this is where we will use fresh we've seen range two before I had that as an example earlier so what I want to do is

um take the first bit or Bit Zero this is actually a definition we're going to define the first bit as bull of fresh of X mod 2. okay fresh xmod 2. that will uh uh the fresh part is just an instruction to the proving algorithm later on that b0 should be computed

as the the lowest bit of whatever the approver puts in for x okay so that's an instruction to the prover and then Bool on the outside that uh can actually constrains that to being zero or one in the constraint system uh we you know we had these kind of like bifurcated systems there's the constraint system part and then there's witness generation uh fresh handles witness Generation Um and these Expressions handle uh the constraints okay so that should work there then let's get the high bit

def B1 equals Bool uh fresh of x uh backslash two backslash two is integer division okay um something to keep in mind because these variables are eventually elements of finite fields there is also finite field division which is going to work differently than integer division uh okay so we have we have multiple division symbols okay most program languages have different ones right uh

backslash is integer division um okay so now what we have are the two bits we've taken X the input and we've unpacked it into two bits and um the thing is that if x were not two bits then um uh let's see if if x were not two bits we would still get values for B1 and b0 because we can still take X and mod it

by two and divide by two uh if we want to check that b0 and B1 actually are that the bits of x not some other bits then we need to do this constraint here x equals to 2 times B1 Plus v0 and then we're going to return X okay uh yeah I think I said this backwards earlier um b0 and B1 are definitely constrained to be bits um but in the uh in the proving process

technically the prover can choose whatever values they want we're instructing the prover to compute it in a certain way but a proof does not have to be created by vampire vampire can create proofs but proofs can come from anybody and they can choose whatever values they want so you have to be careful to include all the constraints that you really mean if we want to show that um b0 and B1 are bits we have this Bool constraint if we want to show that those are the bits of X we have to have this kind of linear constraint down here at the bottom

okay yeah and specifically that would be that uh the witness that has passed has a correct value for x or and a value for x but the sort of virtual variables that are not represented here for fresh xmod 2 and fresh integer division two those values that are supplied are fake right or incorrect uh right right right so um the all variables are the values of all variables are computed by the prover and they they can choose whatever they want um

and uh you know we're using fresh here to instruct the vampire prover to do what we think it should do but uh we always have to keep in mind that proofs can be generated elsewhere and they still need to be correct um so uh yeah like in in an actual um proof system you would be deciding on the values for b0 B1 and an X you'd have to list those out explicitly um and you can choose whatever the prover can choose whatever so we have to make sure they're they're

constrained okay oh I need a semicolon at the end okay uh let's um that looks right to me let's just go ahead and do the next one range for x okay we're going to do this in a similar way we're going to have the high part and the low part okay uh we want the High bits oh it used

to be the low bits for doing mod let's start with low if we want the low bits we're taking something that is supposed to be four bits we want the lower two bits uh two bits is uh two to the two is four right okay so we'll we'll do this and just copy and paste and do the high and this is all good except I'm going to change that to integer division and then we have x equals 4 times the High bits plus the low bits and we'll return X

okay essentially the same as the earlier one I will just copy and paste this whole thing and and do it again to get eight bits and okay so now this is going to be to the fourth which is 16 right okay after range 16 we want uh oh wait wait wait wait wait guys almost let me make this mistake

okay range 8 is a use two range fours in range eight you would use two range Eights to do a range 16. and now we're up to two to the eighth so 256. okay two range 16s give you Range 32 which is what we need to do uh modular arithmetic so we're we're getting somewhere here Range 32 would have two range sixteenths and now we're at 2 to the 16th so okay

six five five three six [Music] oh yeah you know uh we have X you know exponents in Vampire we can just do uh 16. and that should work okay

and let's see if that compiles hopefully we did it all right ah good okay so it compiles uh you can see the type Checker checked uh these definitions they're all functions from integer standards so that makes sense um let's test this out a little bit uh we'll do Range 32 y I need to recompile that I've added that okay so let's do uh prove

okay we have one variable here and it's applying Range 32 so let's uh let's do we can do we can do Hex here so uh 32 bits is uh eight hex characters yeah so um that should be the highest value that is accepted right yeah okay proof is generated successfully now let's uh verify it okay it's valid

um let's do the proof again this time uh what just happened oh I I hit some key okay so this time we want let's just do one more than than that so that would be one followed by eight zeros is that eight foreign okay proof generation success verify okay um now obviously if you were trying to write one of these circuits you'd want to do a lot more testing than

that all we've tested is that there's some kind of boundary at the point where we think it is but it does not prevent uh you know other um you know like higher numbers from um satisfying the circuit if there was some bug in there that would that we missed okay but it seems Seems right okay cool so now we can do uh modular arithmetic so this would be a mod 2 to the 32 just one input okay

uh so if you think about what happens when you do modular with arithmetic uh it's actually very similar to our earlier uh range stuff uh we're going to take X we're going to use integer Division and uh then we're going to do a range proof on those results right okay so we'll do def uh let's call it R for remainder def r is equal to X uh

fresh X mod 2 to the 32. okay this doesn't constrain anything so we need to do a range 32 on top of that okay all right uh then the actual constraint that we need that shows that X and R have the relationship that we expect

them to is going to be that X equals 2 to the 32 Plus uh r no wait that's not quite right we need uh we need a variable here the quotient so let's get our quotient so he's backslash to get the the quotient then here's what we really need okay actually

very similar to what we saw earlier and the the main differences almost messed that up the main difference is we're returning R the remainder rather than x right okay so uh I guess let's do this Z equals mod 2 to 32 y semicolon and let's check this out okay

compiled um now when we run the prover B I've written this last line a little differently than I have before now we have two variables that the the proof generation system is going to request from us both z and y and to test this out we want to choose something for y That's let's say bigger than 2 to the 32 by some amount and then check that Z is the is the Overflow okay so let's do uh [Applause] let's do one followed by eight zeros again

for y okay that looks right and then Z should be what should Z be wait wait a second Z should be zero right because that actually is 2 to the 32. yeah okay so Z should be zero uh let's see if that verifies okay um pretty sure that works okay so we are

we're approaching the end of our time I believe uh so let's let's stop there and uh and if anybody has any questions let's let's go through it yeah um so if you were to write this in Halo 2 raw you'd probably want to do lookups for all their inch checks yes um is there a way to expose that from uh vampire uh there's uh yes the answer is yes but uh it wouldn't be in the vampire language itself um because we want to keep the vampire language as uh agnostic about proof systems as possible but then the answer is you write a compiler that does it

and starting from the vampire Universal representation and uh finding uh the the right Gadgets in the Halo 2 library that you need to use um currently the way that vampire is being used here the universal representation is like uh it's completely flattened out and because of that you lose a lot of structural information that makes it convenient to do the kind of thing that you're you're asking for but there we can also compile in a way that just doesn't doesn't flatten everything out

immediately and then you can have like lookups or or other built-in gadgets if there's one that exists for these like range proofs in the backend Library you can preserve those instead of flattening them all out and then map them straight into the gadget that you want to use cool um one other quick question uh the maybe the three or five year vision for the project is it that you have sort of transpilers or compilers from all front ends so take circum Socrates Etc and then you have transpilers or compilers to all back ends and that sort of community maintained yeah and it becomes standard that people cross compile these things all the time and hopefully

optimize them and put in special lookup things and stuff like that yeah yeah the vision would be that there's a a spec for for Vampire and uh at heliacs we will write the compilers that we need and hopefully other people will write compilers if they need something to go to a certain back end you know I was just talking to a couple of projects uh in the other building today that and and everyone has their own custom like back-end uh like proof systems now like Risk zero has one and uh the the nil Foundation has one um and what they would need to do is is write the compiler for their back end

and if someone has a front-end language that they think makes things really nice they can write a compiler from that language into vampire and then get all the benefits of that ecosystem cool thanks not just uh in the intro you display the link to the our two to address Winterfell is it a possibility or is it working right now yeah this pass from a vampire Earth script to interfere uh no is it already no it's a future yeah yeah so it's the first look okay uh yeah uh speculative so right now we can compile for prom cap allo2 and Belmont that's it uh you can compile with Planck

up inhaler 2 right now plan yeah yeah we're working on a nice back-end trait that will make it easier for for people to add back-ends a lot okay is that all right thank you [Applause] [Music]