ZK9: VampIR: LLVM for polynomial circuits, now with benchmarks! - Joshua Fitzgerald (Anoma)

Transcript

foreign [Music] I am Josh from Noma and this is going to be a workshop on vampire um an llvm for polynomial circuits this event is going to be really Interactive um I'm just going to do like five 10 minutes max of intro and then we're just going to start using vampire and try to build something with it I have some ideas of what to do but it's

pretty open for interpretation so um hopefully we have lots of questions and and people can bring some ideas as well but I do have backup in case no one does um before I do my introduction I you if you brought a device you can go ahead and get a head start on getting vampire uh probably the best way to get it is to go to github.com Noma slash vampire Dash in it there's a branch there called ZK Summit

and that branch has a code space that I set up and if you use the code space version you'll get uh semantic highlighting with vampire because it has an extension built in if you don't use that you can also get the binary under releases or you can build it from Source if you wish if you use those options you won't get the syntax highlighting um so I recommend doing the code space um but you know the choice is yours so if you brought a device and you you want to

play along go ahead and you can start getting that and I'll just go through my first few slides just going to be a brief introduction oh this is really important all right we have some exclusive vampire stickers available today available only to participants in this Workshop they're really cool they are a cat logo see if I can uh I'm bringing this up now because I don't want to forget to hand these out

so if this thing ends and I have not handed these out uh somebody somebody say something uh you can go to there should be a button called code green button and go down and launch it you do have to be signed into GitHub I think for that to work okay yep okay so uh I'll just start with the introduction to vampire uh oops

uh the agenda I basically covered this um for the live coding uh I have Blake 2s hash as like an abstract goal we probably wouldn't finish it or maybe we would I don't know um but at least components that would be used there would be useful in many different circuits so it's a decent thing to to start um so why make a language for arithmetic circuits um a while ago I was asked to see if our masp it's a multi-asset shielded pool circuit

would be more efficient using uh Planck with lookups than it was with r1cs and growth 16 which is what it was originally written for the masp is just a version of sapling with a couple of extra things to allow multiple assets um so I I yeah I went and I tried to rewrite this in uh plonk um lookups and uh it was really really annoying um it's kind of a challenge I never actually finished that project um and the most frustrating thing about it

is that the underlying circuit that you are checking is the exact same if you're using r1cs or or Planck there's a there's a relation that you are checking it's the same relation you just have to express it a little differently depending on the back end that you're using um there's differences in the expression based on proof system but then also implementations of proof systems can change the way it needs to be expressed so you have all these different possibilities for how to express one thing which is fundamentally the same thing

uh in in a bunch of different places and uh there really shouldn't you shouldn't have to rewrite the same circuit in two different ways just to test to see if it's better in one proof system than another it's just too much time so what is vampire this is kind of a uh aspiration here um we can have vampires and IR the white circles are like front end languages ZK languages um

you are probably familiar with Socrates and surcom they've been around for a while Noir is from Aztec uh heliacs has a language called juviks which we're going to use as a front end for circuits and so you can start from any of those front-end languages that you see there and there's a path to vampire and then there's a path out of vampire to any of the back ends which are the black circles on the other side um so any front-end language that wants to hook up to this graph

uh they can do so by targeting vampire or they could Target the IRS by Noir uh a Seer I think is how they pronounce it or if you want to use Starks you can Target airscript and if we can compile back and forth between these things then um hitting any one of those targets gets you all the options here without having to rewrite anything that's the the big goal um so I'll just talk very briefly about arithmetic circuits and and what they are an arithmetic circuit is the is a representation of the computation of a

polynomial uh here are two circuits uh they compute the same polynomial or the polynomials are equal but the circuits are different because the steps are done in a different order the circuit on the left is a more efficient way of computing that polynomial uses fewer operations so two different circuits same polynomial um circuit's a really good word for for these objects because they really do uh function a lot like an actual circuit uh if these were printed circuit boards

then uh you could I don't know hook a volt meter up to one of the nodes and read the the value at that node so each of these nodes has some kind of value that will be applied the witnesses and either the the circuit runs correctly or a gets fried or something if you don't satisfy it another thing is that you can join arithmetic circuits together by basically just wiring them up here I have two representations of circuits this one is div mod so I take X and Y and uh

you get the quotient and remainder out of x divided by y and then over here we have a range function that tests if something is uh four bits fits in four bits so by wiring together R and Z you're forcing those values to be the same value and so you can compose arithmetic circuits like you would functions the only thing is you have to designate what the inputs and outputs are unlike functions which like have this feature

built in circuits basically only have inputs but you can you can designate certain ones to be considered inputs and outputs and wire them together and and still get some composition and this is the last slide I think on this um arithmetic circuits are also just systems of polynomial equations and nothing about them is more difficult than the stuff you did in great school this is the system for a range proof of four bits here

maximum degree is two and we have one polynomial with five variables that's that's it it's not that uh challenging it's just polynomials underneath uh I think uh yeah okay so uh now we're going to move on to the live coding portion um with our goal being blake2s we'll see if we get there uh we may not so um a little bit about Blake 2s this is the more important stuff that we need to

do blake2s actually what's on the screen will only get us uh the um the the function that you repeat over and over again for many rounds this function G to do the full blake2s hash there's a couple of steps at the beginning and a couple of steps at the end that I didn't put on the screen but if we uh if we get there then we'll we'll include those as well uh if you want to see the full spec for blake2s um I have the link up here or you can you can just Google blake2s spec or RFC or something it'll come up okay

so uh before I switch over to the code I just want to show what's going on here uh this G function uh you have a vector of 16 words each word is 32 bits and on each iteration of this function you select four of those 16 and you're only working with those four so most of these inputs here are not actually used a b c and d are the indices of the four

that you are using in that round and then they're you know elsewhere in this there's a schedule of which ones you use on each round um so V of a and b b those are two of the the words that we're using so we'll probably start this just with four inputs and not really worry about the whole 16 um then X and Y I believe is some extra data that comes in from somewhere else so we have basically six

32 bit words and with those we will add three of them together here do uh mod to the 32 just to keep the result as 32 bits then we have xor and we have a rotation uh and then all the other steps are just the same so we need to do mod 2 to the 32 we need to do rotations and xor and addition if we can do all of those then we have

the building blocks for this G function [Music] um these rotations are they're all rotations right and uh down here at the bottom of this table I have the actual amount that's supposed to rotate uh so you rotate 16 bits 12 bits eight and then seven okay so we may need to come back to this a couple of times just to see what we're doing but uh what are the wrongs it says like rounds and word problems no no um f is another function

and F basically has the beginning steps then 10 Rounds in this case of G that you do over and over and then there's some final bits to F so F calls G in the middle and you yeah uh yeah any other questions over this before we clear from the screen we can always come back to it okay uh all right uh these are some slides that I'm probably not going to use very much um showing how vampire works but we can just do that uh in the code space oh and of course uh while I was

having you guys uh get code space and everything opened up I could have been doing that myself let's see hopefully it doesn't take too long oh perfect okay okay so uh yes that's exactly what okay uh

yeah well okay uh bigger or okay for now slightly bigger uh I don't know I didn't try it uh that works okay we'll see how it works okay

uh all right so first uh we'll just write our first maybe a vampire statement uh well we're at our first vampire statement here uh vampire has basically two kind of atomic statements uh one is a binding and one is a constraint and even though those words are synonyms uh they're treated differently in in Vampire uh we use the keyword def uh as for binding and a constraint has an equal sign in it somewhere okay so uh

let's start uh we're trying to do um mod 2 to the 32. I in order to do modular arithmetic you need a range check um you have to check that the remainder is less than the divisor right otherwise it's not the correct version so uh eventually we'll be doing a full range check of 32 bits to get there we're going to start with a range check for a single bit so how do you uh tell that a variable is one bit

uh does anyone know what uh what constraint you need I'd say like the x is one bit zero or one yeah yeah yeah okay so um okay uh that would be a constraint that uh shows that X is a bit this constraint is added to nope not quite not quite equals zero uh

the vampire compiler will add this constraint to a list of constraints and the the X there will be solicited from the prover when in the proving phase and a value would be put in there then it generates a plug or Halo 2 or whatever constraint on the back side when you occupy the circuit so that's that's all that we'll do there but we don't just we don't want to keep writing this over and over again with a new variable name each time that's annoying so we would like to use a definition to bind this to uh it's something so that we can just reuse it right

so this is a constraint but we will change this into a definition say we do Def uh let's call it Bool X equals girly braces um need a semicolon at the end outside of the braces and then inside here this is basically just a closure that has its own constraints that are generated inside and then those are appended to the full thing inside here you can put other definitions if you

want constraints whatever so what we will do is uh oh The X we have deaf Bool X so we are defining a function called Bool on an input X and we can use x inside and the compiler will know where to find X because it's the it's the input here but you can also just conjure up whatever variables you want inside of this as well um and all that's happening there is uh instead of temporary variables being generated by the compiler it generates

the same temporary variables but gives some of them names if you choose to give them names here um so I could use you know I could say uh y equals t or something inside here I wouldn't but I could the compiler would add y equals T into the constraint system be pointless here but you can do it you don't have to declare every variable uh yeah I mean the the variables here are just placeholders that will eventually hold values right so um yeah they're just they're just added to like a big hash map of variables and

at the end in the proving phase um the approver will supply values for those and they'll take on some value so when you when you use a variable even without declaring it it just gets added to the map yeah if it was right why you could see here and then use Google to generate a lot of things y equal C would just have no effect in the end right because effectively you have two variables that are only constrained by being equal to each other so you can assign anything uh they would almost not have an effect but the prover would still need to provide values for Y and T that are actually equal yeah yes right so so

exactly uh let's go ahead and put in our Boolean constraint here so x times x minus 1 equals zero uh in the last version of this I put a semicolon at the end uh here I'm not going to because the last line of every uh definition uh does not have a semicolon and it's the return value when the return is an equation uh it's essentially I mean if you know functions it's like it's returning a unit um it doesn't do anything functionally there's nothing that happens after that

instead that constraint is just like as a side effect added to the constraint system but you can also put a semicolon here and put X after it and now as a side effect the constraint x times x minus 1 is added to the constraint system but then if you call this Bool X um you actually get a return value that you can use inside of other constraints and definitions an equation doesn't really return

anything at all it's like a uh yeah and and losing the losing the words for it like yeah it's just a function with no return it just has a side effect of adding things to the constraint system this one has the same side effect but it also enables Bool X or Bool whatever if you call it to have a value that you can use yeah a very practical person can I use comments in this vampire uh yeah uh two slashes uh also you can do slash asterisk uh for for block comments if you want uh okay so here's our Boolean constraint

and uh now I can call Bool uh let's say Bool a okay so this will uh call this but with a in place of X I mean you guys get this I'm sure I will add a times a minus 1 equals zero to the constraint system and it has a value of a which is not being used that's fine but it could be used let's just go ahead and compile and prove and verify this why not

uh so to compile the command is if you're in the code space you can just use vampire it's got the binary loaded into it if you did this some other way of course you you'll have to do this a little bit differently but uh we'll just use vampire then we uh choose the back end that we want uh we have two back ends available now we have Halo 2 and Planck from ZK garage if you use Planck you have to do a setup so let's use Halo 2 instead so we can

skip that that process we'll do a plonk one later but for right now when we're kind of messing around we don't want to have to do that every time okay so uh we'll do vampire Halo 2 compile then dash s for our source and uh sources blake2s dot uh vampire or if you if you created your own file change it appropriately

and then we need uh to store the output somewhere so Dash o little o uh let's call this uh blake2s dot um Halo 2. okay so uh this is compilation uh what's going on in complex compilation is the the list of constraints is being generated uh definitions are being expanded and things are being unrolled and added to a constraint system which is just a it's just a list of binary relations

you have a you know like Z equals x times y or Z equals X Plus y and everything is broken down into constraints like that we do have a type checker um you can see I know it's small down here in the terminal but uh says Bool 10 is into int so it's a function taking an integer and returning an integer uh then if everything type checks we synthesize the arithmetic circuit synthesis is our word for basically calling the back end

and loading the constraints that we generated into the back end um and then then it's done so we just got a a binary of the representation of the circuit that was put into payload 2. and then we can do a proof so let's do that next the command is vampire Halo 2.

prove to do a proof you uh include a circuit so it's Dash C our circuit was the output of the previous one so Blake to s dot Halo 2. and then this will also output a proof inhaler two so we need to do Dash o okay uh big 2s dot proof I guess so we'll run that command

um if you uh don't include other options there's some other options for this if you just run the the one that I did uh it will solicit the values for the variables from you in the terminal you can also input the values into like a Json file and it will just read them out but since this is short and easy terminals fine so um it's asking us for the value of a so okay uh a is one proof is generated here

this is this is the point where we're really just calling uh Halo 2. with their API you could you could also just do this inhaler to itself at this point okay so uh We've generated a proof the proof has not been checked at all at this point so you could put in whatever you wanted for a you would still generate a proof and it would say proof generation success doesn't mean that the proof is going to be valid just means that you successfully generated a proof okay but next we will verify so you can probably

guess what this is uh vampire Halo 2 uh verify we need uh the circuit so Dash C Blake 2s Dot Taylor two we need the proof as an input so Dash p for proof um Blake 2s Dot uh proof I'm going to misspelled everything okay we don't need to Output anything uh it will just tell us the proof is valid or not

Okay so here we go and uh proof is valid um so we're good I put in one so the proof is valid uh I can easily go back and uh put in something else see if we can get an invalid proof we already did the compilation we don't need to do that again because the Witnesses are not involved in the compilation step so we'll just do prove again and this time I'm gonna punch some numbers in um proof generation success but when I go to verify I get a constraint system

failure which indicates that the proof is invalid some of our error messages are a bit esoteric still but that yeah that's proof invalid okay yeah yeah sure what we have proved is uh whatever number the prover put in uh is either zero or one um but we don't know which one okay so uh that's that's the basics

um we're gonna build up from this and see how far we can get with blake2 uh we have some uh really cool new features in Vampire um including uh mapping folding uh iterating we have tuples and lists we can Curry functions we have higher order functions and that's all enabled by the type checking system yeah uh table lookups are not supported directly in Vampire but it doesn't really matter because uh what you can do there is I put a definition in like this

and a back-end compiler that translates this into say Halo 2 or Planck or whatever can see that definition and if it has a lookup available it can ignore the constraint system stuff in the inside that we told it about and just do the same thing with the lookup so yeah the back end can make that decision uh if it has it available it can swap anything out that it wants as long as these functions are like specified um then yeah I can make that change and use lookups and from The Vampire side of things it's the same uh well

here we I mean we wrote the the back end compiler that translates to Halo 2. and right now we don't use any of Halo 2's lookups but we recently found out that at least the way that we're we're using Halo 2 maybe we can change it but it's automatically generating a big lookup table for something um we didn't even know that but it does that apparently automatically and so we could then use lookups in our compiler to Halo 2 if we want um yeah a silly question but like like if you would have chips or something that you

would already want to use that yeah uh yeah uh in the back end compiler you um if you you can choose to map any of these uh definitions to a chip a custom gate whatever Gadget whatever it's called in the back end okay yeah yeah so yeah the vampire language itself is intended to be very minimal so that it doesn't need to know uh anything at all about front or back end the less it knows the better because it's more easy to Target it for multiple front and backhands

yeah so it doesn't know about lookups it doesn't know about custom Gates back-end compiler that does know about those features in its own back end can make decisions there okay um so let's uh add some more uh functions here um the goal is to get a first goal should be to get a range proof of 32 bits so here's a range proof of one bit we're going to kind of iterate on this and get a range proof of 32 bits so uh one way to do that

is uh we will next make a range circuit for two bits and with that we can jump up to four bits and then eight bits and just go up like that so let's try it that way okay so uh this bull function that we already have we could also say that this is like range one of x just to remind ourselves it's a range of

one bit so let's go ahead and try and make a function that does a range of two bits okay all right so uh the strategy here is we're going to take the input X we're going to split it into uh two bits we're going to check that each of those bits is a bit also that X actually is the result of packing those two bits together so uh what we'll do is

inside here we're going to do a new definition we'll call this b0 for the low bit um and what we need to do here this is where it gets a little bit funky um in the constraint system what we would need after this is well we don't need anything after this uh b0 is just a variable that the prover will supply the value for um however unlike

this expression up here x times x minus 1. um our evaluator will not know how to put how to how to take this input X and compute the correct value for b0 um our evaluator is something that's called automatically in the proving phase um it's it's not necessary to use our evaluator any prover once they know the circuit if they know how to generate the witness values all the values of all the like intermediate variables

they can just do that themselves really the necessary part of vampires already done by that point but if you use the the vampire prover it has an evaluator and it may not know uh how to generate some of the values of uh intermediate variables so we have a a command to give advice to the evaluator on constructing these values that command is called Fresh um

fresh needs parentheses after it and then inside fresh you can write an expression that computes the witness value from the input here so we want this to be the lowest bit of X so we just want to take mod 2. so we'll do X we use percent for mod okay so fresh means we are adding a a fresh like unconstrained

absolutely free variable into our variable map and then X mod 2 is saved for later during the proving phase that way the prover only needs to give X and then this is called to help compute b0 another way to do it is approver just gives values for x and all the intermediate values in between there'd be a pain so we we have this extra thing yes we have a restricted Library here of

operations you can do inside fresh um you can do addition multiplication uh you can do field division integer division mod of course and we also have another operation which is basically division or zero if the denominator is zero uh it don't it won't fail the division it will just put a zero instead for that value which is actually useful in conditionals like if you want to do an if statement you need that to access these fresh variable in our

Circuit by X X we're going to be 0 . I mean now we can refer to it as sb0 right yeah yeah um this is extremely important and also a reason why we're thinking about um removing fresh or rethinking this system um this is a definition this line has not added any constraints to our system there is nothing requiring b0 to actually be the first bit of x we're just saying that when the prover

gets to that phase that's what they should put in in order to satisfy the circuit um but no constraints are added at this point so let's go ahead and add a constraint um we can do that just by saying uh Bool b0 and then Christmas calls bull adds a constraint constraining b0 to be a bit and and now now it's good um so yeah this is a this is a tricky spot where uh if you if you forget to add the

constraint then you'll have an under constrained circuit which is really bad um and uh so we're we're thinking about removing fresh and having witness generation handled outside of this document so that if you're if you're in in here um all you see is constraints and you won't accidentally think that okay well X mod 2 is be zero so it's constrained because it's um okay uh then we're going to repeat this again with uh B1 the high bit of X yeah fresh

uh I haven't used circum enough to confirm that but uh witness generation uh has to happen for both there's got to be some way of specifying that so it sounds like that's that's doing but don't quote me too much on that okay so we'll repeat this again uh def B1 equals fresh uh this time we need to get the second bit of X so we'll do X uh uh integer division is backslash

so uh x divided by two uh percent two and then Bool B1 okay so uh okay so we're dividing by two so that gets rid of the lower bit and then we do mod 2 to get the the single bit that's of what's left okay all this does is make the prover Supply two bits called b0 and B1

it doesn't have any connection with X yet so we need to do that for sure to do that we just say x is equal to b0 Plus 2 times B1 and we will put a semicolon and a return statement can be X that way we can use this and get a value out of it okay can you uh yes

um so we will uh yeah we'll get to that yeah you can you can do uh iterations so um you can supply a an integer value to a function and it will iterate that many times so this is uh you know kind of like uh vampire's version of a loop but instead of like for Loop just give a integer uh yeah we'll do that okay so uh here's our range two um

if we want to if we want to turn this into something that we can iterate on um we'll need to rewrite this a little bit uh let's see um Let's uh uh actually you know what for right now um just because my my instructions for iterator is on the other screen

um let's do a copy and paste and uh we'll go up to four I'm Gonna Change b0 to low and uh B1 to high uh these bulls will change to the range that we just did and change b0 B1 to

low and high so our goal here is to split X into two uh two bit values and then call the range two on those right um so for fresh here we'll need the low half is a two bit thing so we'll do mod four and then the high is we'll do X divided by four mod four um and then we'll change this should be uh range yes yes thank you thank you these should be eights not fours

because they are they are half of two to the fourth that's where they come from uh not the exponents themselves okay um all right and uh then we change this um instead of a two here we need uh eight of the yes uh this should definitely be four all right well let's figure this out um Range two

is two bits so uh zero to three um we put in uh X that is in uh Range four bits so that's uh 16. right and um yeah so we we just need we need two values from zero to three right for the for the low and the high so yeah so this is four yes

and um if you want to hide should what thank you okay all right uh hopefully that's good because we're just gonna copy and paste again and do it again yeah so all of the variable signatures here uh here inside of fresh um inside of fresh uh

I think it wouldn't matter in this case um uh yeah um okay so this is where it gets a bit funky because uh in Vampire um all these values are just integers just big ants you can use really large integers uh but in the back end everything is converted to a field element so if you

um if you take two integers and you do like regular integer division there's a remainder but if you're in a field and you do the division on the field rep field elements represented by those integers then you don't have a remainder because you can always do division and you get a different result so that is why we have Division and integer division even though everything here is an integer when it gets to the evaluation phase we're working with field elements at that point so it's important to specify integer Division versus field division and the the integer division will um

do you know the regular integer division before converting into a field and then the results are the field representations of the quotient remainder okay so um if if you want uh integer division yeah you've got to make sure they're using the the integer division symbol because the the other slash will will give you something different okay so uh let's copy and paste this again and this time we'll go eight

this uh well this this is the easy part these should be fours the range two should be fours and let's just think carefully about what these integers should be um we're giving X as an 8-bit value so we're trying to break it into um two four bit values so we want to do a mod uh 16. yeah and we'll also do the division there

okay um 16 at the bottom right uh do we agree with this great perfect okay uh so we have 16s everywhere we have range fours here uh looks good we'll keep going we only have two more uh I don't think we have to talk about these as much uh copy and paste 8 to 16 change the forest Eights uh and then here this will be 256 right

okay um so yeah I'm on the on the last one Range 32 change these to 16. okay now what goes here um yeah uh well let's just do uh 2 to the 16 and and say oh save ourselves some mental energy okay

I use parentheses all right okay uh yeah we better stop here and just double check that everything works um so let's go down here and call uh range 32 and a and uh since we've changed the uh the code we need to recompile of course uh oh

oh yeah okay all right yeah this uh this happened recently with uh exponents um we need to fix there's an issue on it uh what what's two The Sixteen six five five three six okay I will use this in the meantime okay

okay now compile's fine we see all of our functions there taking integer to integer that's good all right um then we can just go back up to prove it's the same command and it's asking us for a uh let's choose something that should work um you can you can put things in HEX if you want work um so 32 bits is how many in in HEX

uh each each byte is two characters so like eight right so if I do f f f f f f f should work verify okay it's valid um let's prove again and then we're going to do um 0x ffff uh proof generation success

uh okay failure okay so yeah it appears that our range proof is working um you'd want to test this a little bit more but seems like it's okay all right so now we can constrain things to arrange and honestly this gets us most of the way to what we need for our blake2s most of it is is ranges weirdly enough so uh let's go back to my slide here okay so now we can do a mod to to the

32. so we can do our first line of this function here okay so uh that is called uh G in the RFC so we'll keep that as well um we're just going to start with four inputs uh actually there's six right there's four from the the words that are in like the state vector and then there's two other ones so um we'll just do uh a b

c d x y um yeah because of our type Checker and the way it works you can just put spaces in between all these and the type Checker will know that g is the function that we're calling because we have we have currying so this is and it just automatically handled and it treats everything essentially the same okay so uh the first line is we take it a plus b plus X and then we do mod 2

to 32. so we'll do oh and uh we're putting that back into a okay uh if you if I say uh I say a equals here um sorry if I say def a equals this will make a new variable also called a with a different ID than the a that's up here if you use Def it's going to create something new

um so what we what we will do is uh oh so that means we can just leave this uh we're not we're not overriding a it's just a new variable also called a with a with an ID that's different um so uh we're going to save the results of this into a new variable um okay yeah um uh let's see

that's a good question uh really honestly we should just use a different variable name uh yeah so let's just do um [Music] a next uh all right so this will be um a plus b plus X and we want to uh do the range 32.

we need the parentheses there because of the addition that we're doing otherwise if these were like separate inputs we could just use spaces operations module 32. or um they're only modulo 232 if we put the Range 32 in front you mean we haven't overflow overflowed uh no no but I I the black formula had this mod 2 to the 32 is that place specific or is

that yeah yeah that's uh yeah that's part of the Blake spec they just use 32-bit values to to represent the message and everything else so um the integers that we have available here are much larger um so there's nothing naturally constraining them uh like when you when you allocate a variable and says you know human 32 or whatever um there's nothing like that we have to put the constraints in that that do that okay uh great so that's the first line um what's the time okay like like yeah yeah sure uh I think this

is supposed to be an hour am I wrong about that or did I just make that assumption I mean obviously you can feel free to leave if you need to go somewhere else but I think it was originally planned to be an hour [Music] oh yeah we are we are wow okay all right uh well well thanks for sticking with me I apologize all right we're gonna like go faster uh well no I'll just uh briefly explain uh the rest of this

um there's a bunch of things that we can already do we can do this step this step in this step right now for exor you can you can return a tuple from a function so you can take a input and split it up into all its bits and then actually get the bits back and then you can do zip and xor all the bits together um for rotations you could also get the bits unpackable and then just to find equalities

if we like the new bit stream but there's actually a better way to do it which is you just use mod again so if you're rotating 16. uh you it's almost the same as a range gate you split it into the 32-bit thing and two 16-bit things pack it together in reverse order and now you've done the rotation do that for 12 and seven as long as you have the ability to do mod um

and that that pretty much does it for one round of this G function exactly two um Okay so I mean that I'm committing to the repository yeah sure um yeah let's go to this we'll wrap it up here uh if you are interested in using vampire want to learn more uh we have a Discord and a person we have as well um we are we're chatting on Discord about uh design changes we want to make um you know we're writing vampire we're

trying to include a couple of uh popular back ends but we really want other people to be able to add their own back-ends if they want to use and make that easy so um we're we're thinking about the design of the interface for that uh so yeah if you if you have questions or suggestions um for what you need to see in Vampire uh definitely I mean talk to me or visit the Discord if you want the uh uh it's uh it's a separate Discord from from your models so I don't know if that's readable here but uh that's the invite link I made it a couple of days ago and it's

last for seven days so if you want to join and do the next couple um I have stickers that's it thanks everybody [Applause]