ZK11: Binius: a Hardware-Optimized SNARK - Jim Posen

Transcript

[Music] uh hello ZK Summit uh it's a pleasure to be here I'm Jim I'm the CTO of UL batana and co-founder and if you've heard us heard of us before you probably know that we are also building specialized Computing hardware for ZK proving much like the companies Justin mentioned in his uh excellent talk before this um and we completely agree that specialized Computing tasks like ZK proving require dedicated specialized proving Hardware our efforts have been focused on fpgas which are field programmable Gator Rays this lets us use native digital logic uh

while still being able to iterate quickly but W vatana is not just a hardware company we are a cryptographic acceleration company so what do I mean by that well high performance Computing needs fast and efficient Hardware yes but it also needs finely tuned software and optimized algorithms that are all designed to work together this is known as Hardware software codesign and you know this basically means we don't just want to take a algorithm and a software implementation and go build an Asic for it we uh want to look at this from a hardware software codesign perspective and that's what led us to do the research and implementation of Bas which is a new snark based on towers of binary

fields which I'll be talking about today um but quickly I want to give a couple of examples of Hardware software codesign that you might already be familiar with so we can look at the industries of uh storage and machine learning for two examples here so in the world of storage we used to have hard Diss and now it's you know uh ssds solid state drives and nand Flash are extremely prevalent uh and they've led to a huge Improvement in IO performance uh if if you don't believe me just try running an ethereum node on a hard disk and let me know how that goes um but they appeared at first to have a big problem which is that rights to the same memory location with

Nan flash uh wear down the hardware very quickly and so this required a whole uh the industry to build a firmware and software stack above it to work with the hardware to do what's called wear leveling which Mak sure that rights to the same logical location actually go to different physical locations so that the you know the The Flash doesn't wear out we can also look at machine learning where Google uh created this tensor processing unit and their first generation of the TPU uh did not support 32bit floating Point uh arithmetic which is what many ml models were using instead they decided to use 8bit fixo quantization and forced the model

developers to use this as well simply because 8bit fixo computation is far more efficient uh according to their blog post this let them fit about 20 time 25 times more multipliers so the point is this is these are examples where the hardware design feeds into the software design so where do we start with Hardware software code design we need to start by profiling the options that are out there so catak is a really good Benchmark because it's the number one challenge in bottleneck for steam scaling ethereum today uh and it also that means that there are widely available benchmarks uh that are

optimized for it so we can look at scroll and plon e3's implementations scroll uses Halo 2 which is a plon protocol kcg commitment scheme with the BN 254 curve and py 3 uses the fry commitment scheme with a 32-bit field um and what we can see here is that the proof size is about 50 times smaller for scroll but the proving speed is 10 to 15 times worse um py 3 can be run in one of two modes using either katak which is a faster hash function or Poseidon 2 which is more recursion friendly so we're going to focus on Pony 3 uh primarily for the the remainder of this talk um I need to give a little bit of

an overview of where proof systems spend their time you have four key uh steps generating the witness is basically uh storing the the trace of uh register and memory States over time it's not particularly computationally expensive but it's a bit tricky to paralyze committing the witness is basically like fancy hashing in the case of plony 3 and Bas this is applying an error correcting code and and hashing the trace uh there's the vanishing argument which is either a polinomial divisibility check or uh the interactive Su Che protocol um it basically computationally boils down to lots and lots of Pol evaluations or arithmetic circuit evaluations at

different points and then there's the opening proof which is kind of like where the crypto magic happens but actually we're not going to worry about it too much the time to do the opening proof is usually not super significant because it can be uh batched over multiple pols which advertises the cost so when we look at like where Pony 3 is spending its time it just immediately jumps out that commitments are what we needs to tackle first it's you know the pony 3 prover spends almost half its time doing commitments with a fast hash function catch Shack in almost 75% of the time when using Poseidon 2 and so I can't go into all the details on bineas but what I want to convey is

that if we want really really fast verifiable and zero knowledge Computing I'm going to argue that binary fields are the right fundamental primitive to be building this on uh and that's for two reasons basically they give us very efficient arithmetic and we can get very efficient arithmetization so starting with finite field arithmetic we have two common classes of finite Fields there are prime fields and binary Fields Prime fields are probably more familiar these are numbers the integers modulo some prime number uh binary Fields might be less familiar the most fundamental binary field is F2 it's the field with zero and one of bits um and then for any K bits we can define a

binary field that fits in exactly K bits and uh you know this is this is different from Prime Fields so Prime Fields don't have a canonical representation in in K bits meaning when we're talking about a 32-bit Prime field uh this means it fits within 32 bits but not that every 32bit string Maps uniquely to a uh a field element which is actually really convenient property that binary Fields do have integer uh Prime field add addition is just integer addition with a conditional subtraction whereas with binary Fields this is a bitwise operation it's exor oops how do I go

back um multiplication of prime Fields is basically integer multiplication with a reduction method there's a lot of options here but basically unless you have a special form of your prime your reduction is going to incur M uh more integer multiplications whereas in binary Fields the multiplication operator is uh polinomial multiplication again not going to go into the details but what I do want to make clear here is that multiplication in binary Fields is carless so like remember back to grade school when you were learning how to like add and multiply numbers by hand you have to you have to keep track of the carries and then the last digit that

you have depends on all of the previous digits uh and the same exact thing happens in digital circuits you can see how the last output bit of an ital multiplier depends on basically all of the previous computations so the total dependency path is uh is really long and in circuits this creates propagation delay of the signal which limits the to maximum clock speed that you can run uh these multipliers at whereas binary Fields basically all the output bits are sort of computed independently based on a small number of input bits and they're combined using exor Gates whereas the integer multiplier needs these much more expensive full adder and half adder

boxes which is what uh hafa mean there another fun fact uh squaring in binary Fields is just really cheap it's just a crazy math fact that in binary Fields x + y^2 = x^2 + y squared and so when you're multiplying or when you're squaring field elements the number of cross terms in terms of bits or limbs that you would need to compute uh is is much lower it's just this diagonal as we can see in this representation so the thing is like binary fields are not a secret new technique in cryptography at all they're they're very commonly used in cryptography um if

you've seen one of those the QR codes well guess what there using binary Fields uh they're using read Sol and error correcting codes over binary Fields they're used in the AES encryption standard they're used in the GMAC which is used in as GCM mode binary field elliptic curves is a very well studied field for Hardware efficiency um the original fry and ZK Stark protocols were defined for for binary fields and one primitive that you might not be aware of is is gral which is a hash function that appeared in the sh three competition as a finalist along with katak and Blake 2 it's based on the design of AES um and it's particularly interesting for us with use with bineas

because it's fairly recursion friendly uh uh while still being you know a fairly classically defined hash function natively based on F28 so I'm not going to formally Define what tower fields are um but they are a type of binary field that is not used in any of those previous constructions that we identify as being really really good for snarks and having lots of interesting benefits and so I'm not going to Define them formally but I'll kind of show you how they behave so we can take a string of 128 bits um and as I said this we can interpret this as a unique element of the

128bit uh binary field or we can interpret these 128 bits as a vector of say two 64bit Tower field elements or 4 32bit Tower field elements or 16 8bit Tower field elements all the way down to 128 1bit F2 elements um and this is all doesn't require any computation this is a basically a typ cast on a string of bits which is a really interesting and useful property and we make use of the fact that we can pack small field elements into larger ones with no computation over and over throughout the design of the Bas protocol in terms of computational

efficiency uh here are some of the kind of astics of implementation we can see that uh fan and Par identified this particular construction of a tower as having really interesting computational properties we can do multiplication of field elements with the same ASM totic complexity as katuba integer integer multiplication which is sub quadratic uh inversion crazily is the same astics and our fpga prototype show that it's only one and a half times more expensive than multiplication in digital logic um and something that's really important for us is because the fields contain these subfields if you want to multiply a

large field element by a subfield element it's basically linear in the size of your your large field element assuming uh you know the small one is is constant so astics we know a good guideline but we also get really good concrete performance so CPU benchmarks we have show uh that our our our implementation of binary Tower Fields um with simd optimizations is actually outperforms BN 254 scal scalar field Ops uh and the quartic extension of baby bear um all I should say that all of these benchmarks are for uh cryptographically large Fields 128bit uh extension Fields

because that becomes the bottleneck in the sum Che protocol um now the quadratic extension of Goldilocks is also really fast that's uh 200 Mega multiplications per second but actually there's a binary field called the poly valve field which is itself not a tower field but it is isomorphic to one and we're able to leverage this in our sum check prover so we can operate conceptually over the 128bit tower field but use the explicit isomorphism into polyal to get really really fast uh High throughput binary uh multiplication in the 128bit uh security parameter um so this is pretty good but

really the fpga numbers show the real benefits here so our team uh is working on fpga implementations of this and here are some some numbers so starting with meren 31 as a baseline which is about the most efficient uh Prime field operation you know you could do or that we see in snark land we can't just compare throughput the way we did with with CPU so the way to interpret this is we want to look at the number of logic gates required and then the maximum clock frequency that this could run at and this lets us derive this this area times delay um efficiency metric that we have to compare them so we see that a 32-bit

binary field multiplier is about five times more efficient than the meren 31-bit prime field multiplier um when you go down to the 16-bit tower field which we're able to use for readed Solon encoding in many cases it's another 5x more efficient and even the 128bit tower field which is four times bigger than meren 31 is only like 2 and a half or less than 2 and 1/2 times uh less efficient even though on its face you would think that it should be you know 16 or or n with katuba times times less efficient um our numbers for the BN 254 estimate did not make it onto the slide but one thing I should say is

all of these uh these multipliers complete in one clock cycle whereas our BN 254 implementation uh requires 49 clock Cycles pipelines to complete and our resource utilization estimate is that it's 200 100 times more gates to do a bon 254 uh multiplication than the 128bit binary Tower field so when you go to especially big integer multiplications where you need to propagate these carries um the you know the benefits of this really shine um here's like a cool thing we're working on a bit of a preview of some upcoming work um that brings together a

lot of the efficiency of binary arithmetics so the vision hash function is an arithmetization optimized hash function this was not designed by us this is from a paper from 2019 the design of symmetric key Primitives for advanced cryptographic protocols but it uses squaring inversion um and and Matrix multiplications and we have been collaborating with 3mi labs and toer and Myon over there uh to create an optimized instance based on on Tower Fields where we get additional computational properties so our sbox can be optimized with fast Inversion from the recursive Tower Field construction uh we can use the squaring

uh in our arithmetization which as I said is very fast and the MDS matrix multiplication uses the fast subfield operations that I mentioned and not only that but we can use additive NT techniques to make this multiplic this matrix multiplication extremely fast so we don't have benchmarks yet um this is a bit of a preview of some upcoming work but uh we're very excited about this construction that will let us have really recursion friendly hashing um so moving on to efficient arithmetization how do you arithmetick so Pony 3 uses air arithmetization and here's just a bit

about how that works under the hood each Kack F permutation occupies 24 rows of their trace and each row has uh more than 2,000 columns it has 2,300 columns with 1 bit values and 400 columns with 16bit values and the total number of nonlinear constraints that you need per row is is about a th to evaluate in your in your uh Vanishing argument and when I say one or 16bit columns uh Starks need to occupy full field elements so you need to pad these one bit columns up to 32bits so on its face this is nearly a 32x loss of efficiency right out the gate and this

is what we're basically trying to capture with with packing and so this is that phenomenon is what we call embedding overhead so kind of the question is do we have the ability to commit small values faster than large values and actually with elliptic curve commitments the answer is is yes with some caveat the uh MSM algorithm basically scales linearly in the size of the scaler it starts to break down when you get below like 10 bits depending how much um work you want to do on your MSM optimization uh but and and then with fry the answer is basically yes down to 32 bits and this

is because a fundamental property of read Salon codes that read Solomon codes require a field that's larger uh than your Trace size and so for practical reasons we we basically this caps out at 32 bits with Bas basically we get uh you know great scaling of committing small values down to one bit values we can commit F2 Elements which are single bits um nearly as efficiently um per you know basically paying by the bit um as opposed to larger field elements and the way I like to think about this is that the Bas polinomial commitment scheme basically maximizes the information

density of your committed data which is really important because we saw that commitments were so slow so now to actually talk about what Bas is this is a system we've been developing um in software and we wrote a paper that came out in November called succinct arguments over towers of binary fields that includes the kind of key research contributions uh we talk about an arith amiz uh for snarks over towers of binary Fields this uses a multi-linear polinomial IOP uh based on hyperplan um we generalized the breakdown polinomial commitment scheme and in a follow-up work that we published just last week also

generalized the fry commitment scheme to work over binary fields in a way that eliminates the embedding overhead so uh lets us commit very small elements uh with high efficiency and we also have a few other contributions from that paper we uh add some new gadgets for General multi-linear arguments including a very efficient shift argument and an adaptation of the lasso lookup argument that's able to capture some of the unique NE uniquely good properties of the lasso lookup argument in the uh kind of world of of linear codes and hash functions so to say a bit about how we're able to avoid this embedding

overhead I can't go into to full details uh in this amount of time but very roughly the ideaas we we're leveraging the packing property of tower fields that I talked about earlier so let's let's imagine that we wanted to apply breakdown to the field F2 which is single bits and how you would apply the you know standard breakdown argument to this well you need to do a read Solon encoding which let's say you need a 16bit field size to do that so typically you would pad that one bit up to 16 bits theover would then send a linear combination of the uh the pre-encoding messages to the

verifier and then during the consistency testing phase the verifier needs to open uh random code word locations to test consistency of the uh Prov sent linear combination with the originally committed message we generalize this so instead of padding we take chunks of 16 F2 coefficients at a time and pack them instead into 16bit field elements and then we apply the read Solomon encoding to that so that's you know already 16 times more efficient and then during the consistency testing phase instead of opening single columns at a time the verifier needs to open chunks of 16 columns at a time and test

it with chunks of 16 adjacent symbols in theover sent message um and this is you know able to go through uh and and doesn't have a substantial performance penalty uh over uh you know something like using a regular binary code or um using the same techniques as I said we've also been able to generalize fry to work with uh you know low no embedding overhead in the commitment phase which is I think very cool and you know conceptually uh the way to think about where this is coming from we're not strictly speaking doing a read Solomon code that requires

uh that's a linear code over a field instead we're doing a linear code applied to vectors of these Tower algebra Elements which are defined in our paper um they're basically vectors of field elements and yeah so to say a little bit about how arithmetization now looks in BAS we're able to arithmetick in a in a fairly different way with many fewer committed columns and many fewer nonlinear constraints instead of each uh permutation occupying 24 rows it occupies 1500 rows over F2 but we can also virtually view this as 24 rows over

F2 the 64 K should be 64 there uh each row has only 60 committed columns and then we have 80 virtual columns which are basically non-committed multi-linear pols that we can still evaluate efficiently via the sum protocol which is you know very efficient for the verifier Andover and pictorially this is kind of what it looks like so here is our Trace we have the input state which is a vector of 25 uh 64 bit field elements or uh 64 rows uh the output State we also commit these C and D sort of uh auxiliary States and then we have C Prime and B Prime which

are not committed they are virtually defined columns that are defined as cyclic chunk wise bitwise shifts of you know some of the other columns which is basically exactly the operation that ketak needs in its definition and then we can just constrain that the output state of one round is equal to the input state of the next round um so where does that leave us with respect to Performance well our proof sizes are between two and three times bigger currently than plony 3 but our proving performance is already about half um and uh and we expect that to get better over

time and this is all measured on a on a gcp uh instance with with 11 physical Cor um but really I think the interesting thing is looking at where our prover is spending its time we've basically completely eliminated the commitment bottleneck and created a new bottleneck or or we we're left with a new bottleneck in the sum check uh EV protocol and so the sum Che protocol as I said is just a matter of pushing lots and lots of polinomial evaluations and field multiplications um which uh we intend to you know believe we can extremely efficiently with dedicated hardware and so that is what you should

expect to see from us which is extremely fast proving using Hardware software Cod design with the sum Che protocol accelerated in fpgas and uh and very you know low memory usage Pro proving so that's uh all I have for you and I hopefully have some time for questions uh you can us here and uh yeah all righty yeah we have a few minutes for Q&A and just so you know we have a break on right now um we're running a little bit behind but yeah we can take a few

questions any questions oh there you go oh man in the back yeah sure he raised his hand I was trying to get it go ahead there's a microphone on your seat see you take this you can take this uh okay uh uh and what is performance related to non9 Fields like uh uh scalar fields or B binary ring like native CPU types uh integers I'm I'm sorry where am I uh where you sit oh yeah sorry could you repeat that please

uh the question is what is performance related to uh what is performance sorry uh what is this is oh uh what is performance uh with non-native Fields like integers yes that's a great question um like essentially how do you arithmetization like integer addition and integer multiplication is the question yes yes so our strategy is to uh we can do integer multi uh integer

addition by just basically bitwise decomposition so we do need to pay for that in the sum check protocol but with uh small field sum check optimizations we expect that to be pretty good um we took down the benchmarks for that just cuz they were a little hard to maintain and we uh prioritized the catch act but essentially you can do integer addition with only one auxiliary committed column which is uh the carries um and then integer multiplication we uh are intending to do with the lass up lasso lookup argument so we would use lookups for 8 bit multiplication of Limbs uh and then essentially add them together so we don't have benchmarks for this yet

there's a description of how these gadgets work in the paper oh okay thank you yep testing here thank you thanks for a very interesting presentation so two questions you showed that ketak is arithmetization than posidon for example right oh well certainly it would be more efficient for us to ariti katak than Poseidon just because Poseidon's defin for for Prime fields and um but you know what I tried to show with the vision hash is that there are similar to posid in arithmetization optimized hash

functions for for binary fields and we've been investigating one called called Vision right do do you expect that the V your vision arithmetization will turn out to be more efficient than than ketak uh um it's a really interesting question in terms of Prov speed I'm not I think they're actually both going to be very fast the main benefit to vision is that the proof sizes will be smaller so one thing about embedding overhead we talk about eliminating embedding overhead in the commitment phase but still doing polinomial commitments and opening proofs for small coefficients results in higher proof size so the nice thing about vision is that it's natively defined over a 32-bit field and so we

would expect the proof sizes resulting from that to uh be smaller than catak so that's the main benefit that I see right and also second question so there is there is a huge research now in arithmetic hashes like posidon but also mimy and um um Griffin and other has functions so do your approach suggest that maybe it's the wrong direction to go maybe we should focus on on binary Fields like versions of hash functions over binary Fields rather than Prime Fields yes I think that everything should move to Binary Fields um no I mean I think that especi especially for symmetric cryptography this was one of the things that led us to pursue this that we

realized how expensive arithmetization optimized hash functions were for Prime Fields our results in fpj acceleration of of the Stark protocols highlighted this and uh all indications were that arithmetization optimized hash functions for binary Fields um of which gral could could sort of be interpreted as one are are just more efficient um for for arithmetic reasons right yeah thank you thank you uh do you have an estimate of how much faster like vision is in the fpga versus like a fpga implementation of something I PID in uh you should talk to Danilo we don't have that publicly available yet but uh you know you should

come find us I think we have time for one more question if anyone has one no okay so we're on break now and we'll be back in this room Round of Applause