zkStudyClub - Reef: Fast ZK Regex Proofs (Eli Margolin, Jess Woods, Lef Ioannidis: UPenn)

Transcript

hello everyone and welcome back to another edition of ZK Study Club this week we are excited to welcome some of the authors of reef which is a new paper out on fast as synct non- interactive zero knowledge regex proofs not to be confused with regx proofs which are not a thing regex proofs and uh yeah we have left uh Eli and Jess here um three of the five co-authors of this paper uh which also includes sth who's been a presenter on on on ZK Study Club a couple of times and yeah pretty excited about this one because this kind of describes I think a little bit more application oriented use case for ZK and so with that I'll pass it over to you all thank you very much for being here

the floor is yours awesome thank you so much so since Alex introduced us um again I'm Eli and I'm here with my collaborators LEF and Jess and today we're going to talk about Reef so when we talk about zero knowledge regular expression proofs we're talking about matching a public regex against a private document so why is this something we even care about well it turns out there's a lot of applications for something like this across a variety of domains so in something like system and network security you might have Network administrators who want to enforce a DNS blocklist while users of the network might want the privacy of fored to them by oblivious DNS over

https alternatively you might have users using a protocol called ape which allows them to register and authenticate to a server without having to provide their password but if this is in a corporate or institutional setting the server might want some guarantee that the user has a password that's better than 1 two 3 45 alternatively users might want spam keyword filtering while not having to show the entire contents of their email to Google or proton mail or whoever in the realm of justice and journalism you might want to prove things about redacted government documents which are the results of Foya or Freedom of Information Act requests and then finally in the case of biology and

personalized medicine individuals might want to prove certain things about their genetic code like genetic mutations to personalize drug treatments without having to provide all of their DNA to a big Pharma company and this is the last uh this last use case is the one we're going to talk the most about today but we examine all of these in the paper so let's think about a clinical trial setting Vicki is running a clinical trial and she's looking for participants to her trial with a very specific genetic mutation she can actually represent that mutation with a regular expression and let's say that Patty has the correct genetic mutation and would like to participate in the

trial one approach to this is Patty registers online and as long as there space is automatically accepted and enrolled in the trial of course with this approach though Vicki can't confirm that Patty actually meets any specific set of participation criteria and this isn't what happens in the real world in the real world we have Patty send Vicki her DNA in the clear Vicky then confirms that Patty has the correct genetic mutation and can make a decision about whether or not to enroll her in the clinical trial but the problem here is that Vicki has Patty's DNA in plain text even if Patty isn't ultimately accepted

into the clinical trial so we want to prove that Patty qualifies for Vicki's trial meaning her genetic code matches the regular expression of the mutation Vicky is looking for without Vicky learning Patty's DNA before she's been enrolled we're all here today because obviously we can do this with zero knowledge proofs with the zero knowledge proof Patty can register for I's trial and attach a proof that she qualifies meaning a proof that her genetic code matches the regex of the variant that Vicki is looking for Vicki can then verify this proof and decide whether or not she wants to enroll Patty in the trial but because we do this in zero knowledge Vicky only learns if Patty

qualifies for her trial if she decides not to enroll Patty in the trial Vicky learns nothing else about Patty's DNA so we can do this in four easy steps so first Vicki expresses her regx matching statement as a circuit satisfiability instance Vicki publishes her circuit Patty finds a satisfying witness and Patty proves to Vicki that she knows the satisfying witness when we talk about Reef we're mostly focusing on this first step how do we express regex matching statements as circuit satisfiability instances and in particular we focus on how do we express these matching statements as rank one constraints systems so we're going to

talk a lot about R1 Cs and uh R1 CS constraints throughout the rest of the talk so right off the bat you might have an intuition for how we could do this we can take our regex here we have a plus b. star so match strings with more than one a followed by a single B followed by anything any number of times and so you might remember all the way back from your intro to Theory classes that we can represent all regular Expressions as non-determinate itic finite automa these are defined by a set of States Q an alphabet Sigma a transition function Delta which tells us given a state and a character how do we move to the next

state where do we go next we have a set of start States and ex set of accepting States so let's consider what it would take to express this as an arithmetic circuit the biggest part of our automa is that Delta that transition function and naively we could represent this with a series of cascading if statements if you're in state zero and you see an a move to State one if you're in state zero and you see a b stay on state zero etc etc we would then do this for every single character in the document processing a character and a state one at a time we could write this up in your favorite you know zero knowledge proof language circom zres take your pick and generate an arithmetic circuit cool so

why are we here well it turns out there's a couple of problems with this approach the first is that of regex expressiveness while it's true that non-deterministic finite autometa can be used to express any regular expression in you know formal language Theory what it means to be a regular expression has really expanded over the past 20 30 years to include things like this this includes something called a look ahead specifically look ahads are type of structure in regular Expressions there are also look behinds they're collectively referred to as lookarounds and essentially what this regular expression is saying is three conditions need to be met by my string it has to

contain an a it has to contain a b and it has to be between two and six characters long unfortunately nfas are really bad at expressing these and lookarounds in general result in a pretty significant State explosion so that's not great the second problem is with our Delta function and iterating through it once for every single character in the document and a sort of normal zero knowledge proof system this requires unfolding the for Loop right representing Delta in the circuit once for every time we plan on calling it which is pretty expensive but maybe if the Delta function is cheap it's not an

issue but that's not the case if we represent this Delta function as a series of cascading if statements this requires size of alphabet times size of automa if statements which comes out to you know Big O of size of alphabet times size of automa constraints so if you're keeping a track at home this naive solution requires size of document times size of alphabet times size of automatic constraints that's bad for large documents like Patty with her DNA it's bad for large alphabets like asy or unic code and it's bad for large large automa like those that result from reg X's with lookaround so Reef addresses each of

these in turn with three key insights the first Insight is the introduction of something we call skipping alternating finite automa or safas so alternating finite automa already exist in the literature they've existed since the 90s and they allow us to express lookarounds much more succinctly than traditional non deterministic finite autom we then extend afas to create a new class of automa that allow us to skip over irrelevant parts of the document second we replace that series of cascading if statements with start State character end State lookup arguments in the

circuit and then finally we make all of this much more performant by using a recursive proof system through these three key insights re is able to decouple Pro a running time from document size in a way that previous Works haven't been able to so at a very high level brief works as follows Patty commits to her DNA using a commitment scheme that is hiding and binding Vicki publishes a regex of the genetic variant required to participate in her trial Patty proes in zero knowledge that her committed DNA matches the public regular expression because we use a commitment scheme that is hiding and we do this in zero knowledge Vicki learns

nothing except whether or not Patty's DNA matches the regular expression Vicki then verifies Patty's proof so we're going to talk about each of those three key insights and components of reef the sappha the lookup arguments and the use of recursive proof systems we're also going to talk about some additional optimizations we implemented to make reef reef much more performant and then finally we're going to talk about how we evaluated Reef and how it compares to other existing systems and with that I'm going to hand it over to left uh yeah so um the the key observation uh that that that we made is that the regular Expressions we want to

match are sparse um so that means a really big document and really small regular expression um it's possible to much because it has a lot of wild cards that kind of capture the biggest part of the document um in the exist automata in the literature wild cards like the ones you see here at the end of the of the string are kind of matched uh the same way uh as characters um we introduced um so in in in afas for example as you see here on on the left uh there's two two types of States uh there is the existential quantifiers so this corresponds to uh to the NFA uh the existing NFA States right you you get a choice between character A

or B and we add another type of state which is the universal quantifier State and this is a bit different this means that uh every child coming off of of that of that state must match the rest of the string um so uh if if we look at the regx and look at this AFA diagram we can we can sort of see that uh the left hand child corresponds to the left look ahead the middle to the Middle look ahead and the right hand uh child which is a really long kind of chain of wild cards corresponds to the to to the rightmost regx uh the 226 wild card um but uh if if we were to match the the right child

right we would have to do all those transitions uh while we don't really need to check the characters underneath because they are wild cards all we need to know is that uh we can we can skip over that that region and that's kind of the intuition for skipping alternating finite automata we replace uh this long Wild Card regions with uh with a labeled Edge we label the edges with Skip and then we provide sort of a set of intervals which says by how much are we allowed to skip uh the cursor at that point uh we also have a a skip with an asterisk which says that you can pick basically any future cursor to fast forward to and then we of course

maintain the normal edges with characters from nfas and afas so in order to see safas in action we'll go through an example uh so the same regx as the one we had before compiles to the same Safa and uh let's take this the string you see the string is indexed the second row is indices of each letter um and we start at position zero and with cursor with a cursor at position one uh so this is a universal Quantified state so as I said uh all children must match so this is a logical end um so I will take all Transitions and these are skip transitions so that means I can basically come up with a cursor to fast

forward to on the left most child I have a star skip so I can pick any cursor uh in this case it's convenient to pick the same equals one because uh really we know that the a that we're looking for in the next step is at position one um and the second one we pick cursor two because that's where the B is at and the third one we we don't really care we can pick any uh cursor to as long as it's between the 2 to six uh interval the most convenient one is to just fast forward to the end of the string the cursor number six and accept uh so so that's done what about the other two let's see so we start at State one at cursor at position one we

consume the a which is at cursor position one and that puts us in uh that that bumps the cursor by one and that puts us in state number two so state number two is an accepting state with a with a skip self Loop that allows us to basically uh as I said earlier pick any future cursor to to skip to and we will pick cursor number six which is the last cursor and that puts us again in an accepting state with the the last cursor of the string so we accept and then and then we go to state number three uh which points cursor two points at B we will consume the B and then uh we bump the cursor by one we're at cursor position three and again

we can pick cursor number six and then we see here we have three check marks because all three children coming off of state zero at this point have accepted so that means the whole Safa is accepted and the regx matches the string um so next we need to uh encode the Safa as a as a lookup argument and uh Jess will tell you exactly how we do that okay so we need to now represent our safas um in our um R1 CS instance um which is our arithmetic circuit um and so we do that by using lookup arguments and what lookup arguments do um is It's A Primitive it's essentially a way to

prove that some set of values V1 through VM or in a particular table T um so in the case of reef we have two tables uh we have our private document table um where we have all the indices and all the characters that are in the document um and by private table I of course just mean a commitment to this table right um and then we have a public sappha table um that's deterministically derivable from the reg X by both the prover and the verifier um and this table represents all the edges in the sappa so all the entries are you know the the state that an edge starts on the character for that edge and the state that that edge ends on and this replaces our Delta function um and so we

transition through the sappha in our Circuit by proving that each Edge we take is indeed a valid Edge in our table and that the corresponding character for that edge is at the correct cursor position in our document table um and so to understand how we get a little bit of extra efficiency out of um lookup arguments we should first talk a little bit about recursive proof systems um so if you are familiar with the the cryptographic literature in this space um this is also called IVC or incrementally verifiable computation um we're going to use the word recursive because it's a little more intuitive and um because the Nova paper uses that word and we use the Nova System um so recursive proof

systems um are where some prover you know wants to prove some um function Fu multiple times um and so the approver takes the R1 CS instance representing Fu and produces know for a single correct execution of um and so proving a single step uh isn't that useful you can do that without a recursive proof system um but with a recursive proof system you are um able to prove then that um some prior proof Pi Zer in this case um verifies correctly in addition to proving another execution of Fu and so you can do this in a chain uh as many as many times as

you want for as many iterations um and then the verifier only needs to see and verify um the final proof uh in this case Pi J minus one um and this establishes in like a domino fashion that all the prior proofs were correctly verifiable um and so that all the prior um f executions are verifiable um and this helps with our um unfolding the Delta function problem that we saw before um so now we can only do um within each circuit we only have to do one Delta or a small batch of Deltas um and the circuit size and therefore verifier time is parameterized by a single iteration instead of J iterations of something um which is

ideal um I'm checking for questions I'm good um so yeah we're all good keep keep on going thanks this is great um so we use a particular lookup argument called NL lookup um it was designed specifically for recursive proof systems um and uh the way and lookup works is we have some table and we represent our table as a multi-linear polinomial t such that t evaluated at a particular index produces the value in the table at that index um so in this running DNA example um T at zero is character a t at1 is character C so on and so

forth and the way in lookup works is it applies the Su check protocol to reduce some set of M lookups which are just evaluations of t um to a single evaluation of T at a random Point um and if you're familiar with the the ZK space you probably know what Su is um and if you're not that's totally fine you can treat it as a black box um what's important to know is that it takes um M log T time to make this reduction um for M lookups um and then T time to do this final check which is the final evaluation of T at a random um okay so as we talked about we're going to be using a cursive proof systems we're going to be doing batches

of lookups you know we'll do the first proof we'll do you know 10 lookups then the second proof we'll do the next 10 lookups and in re case this will be like you know the first 10 characters in the document and the next 10 characters in the document and so on and so forth um so you'll end up with something that that looks like this where we have these batches um question how is the PO how is the polinomial T multi-linear that is a great question um it's a little bit um in the weeds which is why we didn't include it but basically what you do is um you create a multi-linear so you know you can represent a table as a polinomial um pretty easily where you just say like okay Zer a is

one point one B is the next Point 2 C is the next point so on and so forth um and then you can create a multilinear extension of that polinomial where essentially the index instead of being like a single field element like two uh is now a binary representation of that field element so like you know 0 one0 is index two um and so it's uh parameterized by L variables L being log to size of table um does that make sense do you do you use a binary field and its extensions um you we use a um we use a

regular Prime field uh because then you know all the the binary elements are um representations in the table so you know if you evaluate t on 00 Z you get the thing at index zero but you can also evaluate it on um you know T of a random Point 17 319 um and it gives you a value that's not in the table but consistent with the the polom got it thanks awesome good question Okay so um we have these batches um where you know in round one I do M lookups I reduce them to a single claim um T of R1 equals V Prime 1 in the next

round two I do um M new lookups that are different from the first round reduce them to a new claim T of R2 at V Prime 2 um so on and so this is not the the best runtime we could get um because you'll notice that we're doing you know the reduction work per round and we're doing an evaluation of T every round um and that that t is Big because the table can be very big and so we'd like to get rid of that if possible and you'll notice that each of these claims we have at the end you know T of R1 V Prime 1 um are themselves just evaluations on T um they're evaluations of this polinomial so they're actually like lookups in and of themselves so what we can do is we

can roll each lookup into the next round so you know after round one we have this claim about t of R1 equals V Prime 1 and we roll that into the next round of lookups during round two then we roll round two's lookup into the next round of lookups at R3 um and so now we only have to to the the only T we actually have to evaluate is the final check so in this like three round little example it would just be T of R3 the last thing we have to to evaluate we only have to do it once um and so a this allows us to reduce all lookups over our whole recursive proof system to a single polinomial evaluation which is very cool means that the the number of lookups increases the the cost per lookup decreases um and B it it

allows us to move this this final T evaluation outside the proof system right so now our circuit can just be parameterized by this m log T reduction and the verifier checks that once and then this T is moved outside the proof system um so in the case of like sappa tables uh since the sappa table is public this can be done totally in the clear without any sort of cryptographic Machinery uh which is really nice um in the case of the document table we we have to do it against a document commitment so you have to commit to the document uh with a commitment that allows polinomial evaluation like inner product argument um but that saves us a lot of time okay now we're going to talk about

optimizations um that we do on top of end lookup um up until now we've been talking about the complexity of our R1 CS instance or circuit um and therefore the the verifiers work to verify the proof and the verif fire's work to do this final check um but it's also important to talk about the PR's work to produce the witnesses uh for the end lookup instances in our circuit um and so since because because the the prover uses um because we use some check within and lookup um the prover has to compute over the whole table to compute the sum check Witnesses every round um so this means that the approver does t work for each iteration excuse me which is not ideal especially in cases like DNA where the

table might be much much bigger than the actual um lookups we do but we might only do lookups because our salv has allow us to only do lookups over you know the stuff that's related to the regx we might have this full chromosome and this a very small Gene and so then we're the prover is doing work over the whole chromosome each time which gets out of hand very quickly um so in this example that I have over here on the right um you'll notice these lookups only come from the bottom half of the table we have this t110 which is of course T at five because all these are in binary the T at five is a we have T at 7 um is G and so these only come from the bottom half of the table so it's a waste of

time to do computation over the whole table um so what we do is we allow the prover to pretend that only this bottom half of the table exists and just do his computations over this bottom half of the table and we call this process projecting onto a particular subtable um and so now our lookups look like this where as far as the approver is concerned this a lookup is at index zero instead of index five uh because the first half of the table doesn't exist um and so now the Pro's time is parameterized by this new table T1 um which is half the size of the original table um it's important to note here that the um the verifier time improves a little bit not that much the verifier still has to do this this final check over the

original table um a so that it can make sure the prover isn't doing anything um and B it's so that we don't have to change our commitment because there might be situations in which we want to commit to you know a genome and then prove multiple things about it with different reg xes which maybe have different projections um so the verifier makes this final check against the original table um so we don't have to change the command so you might be wondering does this method generalize to multiple projections um and it does so you could have you might imagine a situation like this where we have um you know oh we have these lookups from this first fourth of the table and then we

have some other setup lookups from the third fourth of the table um and so the most you know straightforward naive solution would be you could um have two and lookup instances in your rank one in your in your R1 CS instance um and you could have two sets of lookups and theover computes lookups over table one or table two um and this is more efficient then do the pro doing lookups over the whole original table um but you have to have extra circuitry to distinguish your lookups and it is is a mess um so what we we do is we allow the prover to actually combine these two tables um he pretends this is just one table um and gives it a new structure um where he says you know okay this first chunk is going to be chunk

zero the second chunk is going to be trunk one and so this is what the pr sees um and so now our lookups have to a little different you know G is at index 0 0 a is at index 01 um and this is fine this is great it allows us to do one and look of instance have one running claim it allows the prover to pretend that this small table is all that exists he doesn't have to understand that there's multiple tables happening um again we have to um structure our final check to correspond to the um original table structure which is this this green column here the verifier has to s sort of understand where these chunks came from so he can understand how to check them against the

original commitment um so in this in this final check the prover says like okay my final Claim about my hybrid table that I have is uh about this point r0 R1 and so r0o sort of tells the the the verifier to select like okay which original chunk did this come from um then R1 indexes in the actual table um then theover has to provide this this original structure information this t00 and T10 that tell us how the the chunks relate to the original document um and so this generalizes to any number of disjoint chunks in the table um in fact you can even have chunks from different tables um and in

that case the verifier would say like Okay so this first chunk comes from table T at t0 and this second chunk comes from a different table table F at F10 and that's totally fine that works out um in fact you can even have one of these tables be public like our Safa table and one of them be private like the document table um and as long as the verifier does some some bookkeeping and he knows where these things are coming from he can perform this final check half against the commitment and half in the clear um which is really nice because it means we can combine our um public sappa table and our private document table into just one table so there's just one and lookup in the circuit um so to summarize um we talk about document projections um which um

run over subsets of our larger document table um in its most straightforward setting we talked about um public prescribed offsets which means the prover and the verifier agree like all right we're projecting over this chunk of the table um which works when um the regx has a prescribed offset and we know okay how many how much of the document can we ignore um it doesn't work when you have something like like cley Star like this right X because then saying oh well I'm projecting over this part of the table leaks something about the document um there is a way to to hide uh the projections and there is a way to hide the document length with similar optimizations and we we talk about that

in the paper um and then we talked about hybrid tables uh where you take projections from um different tables which can include you know the full table maybe um and you combine them into a single table which makes the prover and the verifier work um better because the prover only has to do you can pretend everything is one table and the verifier um only has to have one and lookup instance in the circuit um as long as the um document or the part of the document you're projecting over and the sapot table are close in size CL being three orders of magnitude this will give us savings I have a question real quick can you describe again just the document projections concept so and if I'm

thinking about this in terms of a regex you know pattern that I want to run against a document the projection can be thought of as just the portion of the of the sappa table that I that I care about I guess with regard to the r like explain just explain one more time the concept of projections I'm so I think I'm a little confused yeah no no no you're good um think of projections mostly most of the time all right in terms of the sappa table most of the time we're going to want the full sappa table the Full Table Right CU that's your ual that's your actual pattern right the sappa table is your pattern that you're searching yeah that's the actual like sa that's the actual like you know graph with the so this optimization would not apply there no

unless unless you can because because if you were if I was to say to you like I only care about this half of the sappa then why do I have this other what yeah you you wrote too much of the yeah you wrote up to a pattern that was too long right yeah if you exactly um so most of the projections just applyed to the table um and so it's basically saying like all right I know that you know maybe only this half of the document I'm going to look up like maybe the first part of the document is all wild cards so I'm never going to make those lookups so why do I need to include that in my computation I see okay so if you have some knowledge about the structure of the document beforehand you could potentially apply an optimization like this right is it's really because I

guess the the question that comes over my head is like if you let's just say naively say I'm always searching the second half of the document like what if the regx pattern would actually match if you had looked at the character immediately before the second half right you know what I mean so I guess like like you just basically have to know that you're foregoing searching effectively the first half of the document is that or are you just assuming it will always match like in the case of this like clean star thing you're like okay whatever this is all going to match anyway I know the A's start in the second half sorry does this question make sense I think that's it yes yes this question makes sense uh it's a good question um you you don't have to know anything about the structure of the

document what you have to know is you have to understand the structure of the regex like in this first example here this um 10 Wild Card ABC yeah and this is if I guess like just reading this regex I think for for those who might not be familiar with notation I believe this is one or no this is 10 right this is 10 collectively right and then ABC anything so anything plus 10 ABC anything right and it's like anything in the first reg X is is one instance of anything right the dot right any character yes great sry I just wanted to for those who are not reg X fluent I just wanted to say that out loud go ahead no I I appreciate that uh yeah we've been looking at these for for years so it's doesn't always occur to me

to say that um yeah so in this case um I know no matter what the document is I know we will never care about those first 10 characters so I can project past those 10 characters in this ah I see yeah in this second example because there's a DOT star I can't use projections because I actually don't know where the a is going to start without leaking something about the document so it wouldn't work in this this second example I see okay so sorry and let me restate for the purposes of the recording because I said something wrong earlier about the reading of this regex the first the first one is any character 10 times right and I think it has to be so it's it's any it's 10 of any character right so you're always

going to match the first 10 characters no matter what they are right and but you but the but the length of that is bounded by 10 right it's 10 you're saying it's 10 whereas and and you're saying it wouldn't work in the first case because and or sorry in the second case is because that character the clean star is matching any number of times right zero or more so that in that case you know it could be one it could be 10 it could be a 100 instances and so therefore you don't actually know where to offset is fundamentally the idea here is that is that right ah okay great thank you good any other questions cool all right great so now

I'm going to talk a little bit about how we evaluated reef and how it compares to existing systems and protocols so to evaluate Reef we looked at a wide variety of questions these aren't even all of them um and I don't have time to cover everything so I'm going to focus on this subset is can Reef support report a variety of regex's and document sizes is it efficient for theover how does it compare to existing and Alternate Solutions and what impact do the additional optimizations so the projections and the hybrid tables what impact do they have on performance so Reef supports more robust regexes uh with fewer constraints than uh existing systems so at the time that

we publish there were essentially four other systems looking to do something similar zombie which is zero knowledge middle boxes uh ZK regex and ZK email all three of these do you know full regex matching minus you know lookarounds and then there's ZK regg which does uh fixed string matching for regular languages so you'll see here Reef supports everything all of these systems do as well as look around um and not only does it support everything these systems do but it does so with fewer constraints so you'll notice that zombie ZK X and ZK email are all kind of of the form you know size of document times at least size of automa which is right not

great we had talked about this earlier on Reef however not only do we make that additive so size of document plus size of autometa but we push all of it inside a log right so it's a pretty significant reduction additionally you'll notice Reef has this Alpha at the beginning this is the number of lookup that we have to perform and this is defined entirely by the regex itself this is not defined by the document it's a document independent so we're able to kind of have a number of constraints that's really pretty independent of the document the other uh the fourth system ZK regg um does have sort of an additive number of constraints right so size of document plus size of autometa but they

use something called an aho coric DFA which tends to be you know multiple orders of magnitude larger than safas so this is all Theory theory is great but what about practice so uh sorry Eli can I just interrupt you quickly can you go back I guess just for folks who are watching this video who are may not be all uh familiar with these acronyms like NFA is non-deterministic finite automata and DFA is deterministic right yeah so so tnfa is something called A Thompson non-deterministic finite automa it's what a lot of sort of regular expression matching engines use under the hood uh an acfa stands for an AO cortic deterministic finite on thank you sorry about

that um so we evaluate Reef against four applications uh proving things about large and small redacted documents for Freedom of Information Act requests um oblivious DNS over https block listing proving strong password matching and non-matching and then proving matching and non-matching for specific genetic mutations so this covers a wide range of document sizes going from six characters to 43 million and a wide range of sappa sizes as well so we have some very small safas meaning you know those with 16 States and less than 2,000 transitions to some very very large ones which are

you know almost a thousand States and over a 100,000 transitions so we try to cover a pretty wide range in what we test so in order to test Reef we look at three baselines and we do this because at the time that we were doing Reef there wasn't publicly available source code that we could easily compare against for the existing works so instead we consider three baselines the first is um just kind of the classic DFA or deterministic finite autometa that we talked about at the beginning so representing a Delta function with a bunch of if statements and then just itera rating through it with a for Loop um and you'll notice there's a lot of x's in this column and that's because

even with a machine with 712 gigs of RAM we couldn't compile the circuit the circuit was too big to compile in all of the cases with x's um in the two cases that we could compile it you'll notice it's you know well over a million constraints and sorry like sorry quick question again for me when you said documented redaction large means the document is large or the redaction is large the document is large okay got it thanks yeah no worries um and so next we looked at replacing that four Loop Loop that sort of traditional for loop with a recursive proof system so again we're going to have a Delta function that's a bunch of if statements but now we only have to instantiate it once in the circuit and we can use a recursive proof

system to iterate through the document and you'll notice that there are still some xes here but you know we're doing better we can represent um you know the first three examples with orders of magnitude fewer constraints so it's progress next We compare to kind of the core of reef which is going to be the use of lookup arguments and safas we can now represent everything efficiently um and again we get a pretty big reduction in the number of constraints anywhere from you know 2,000 to almost 100,000 and then the final thing we look at is Reef so this is going to be the safas plus the lookups and the optimizations that Jess described so the use of hybrid public

private tables and the use of projections and you'll see here again the number of constraints goes down but it doesn't go down that much so you might say okay well what is the benefit then of these optimizations well the benefits really come into practice when we look at total PR time so here we have the document redactions example both the small and large one and the DNA matching and non-matching so let's start with the document redactions here we have the sappha plus lookup for the small case and the sappha plus lookup and reef for the large document redactions case you'll notice right away that reef and the sappa plus lookup application are multiple orders of magnitude faster than

the alternative one obvious question that you might have is that okay but the circuit size in the DFA plus recursion case wasn't that much bigger why is it so slow that's because even in the DFA plus recursion case you still have to go through every single character in the document whereas by using safas we can eliminate a lot of that work we have to do significantly fewer number of iterations so here Stafa plus lookup and reef perform about the same so the optimization though really shine in cases like the DNA matching and non-matching case where here we have Reef versus the sappha plus lookup

you'll notice that wreath is um again pretty fast it's much faster also than the sapph plusus look and that's because right in this case the DNA chromosome that we're looking at is 43 million characters long by using projections we avoid having to do operations over the entirety of that table we save a lot of work so in the matching case it's about an order of magnitude faster and in I'm sorry in the non-matching case it's about an order of magnitude faster and in the non-matching case it's about three orders of magnitude faster sorry let me see I see a question in the chat uh sorry if I missed this earlier sappha allows skipping all characters that can be wild cards not relevant to the match yes that

is the key Insight of safas is that for wild cards we don't actually care what the value is it just has to exist so the takeaway here is that even without Reef's additional optimizations the key insights of of reef of the saffas and the use of lookup arguments results in order of magnitude faster Pro time than alternate Solutions so in summary we want succinct zero knowledge proofs for a variety of reg X's that scale well for large documents we can use safas to get better expressivity and Skip irrelevant parts of the document and we can use lookup table for document commitment and sappa

transitions which gives us Reef which has support for a variety of applications with fast prover and verifier times and fewer constraints than Alternatives so I want to now kind of I know people been asking questions in the chat but I want to open it up to kind of questions more broadly from anyone um super cool I have a couple more questions um if no one else wants to jump in um okay can you go back to the to the comparison slide yes sorry I don't know what I just did all good uh Let's do let's hopefully let all right let's see what's happening um yeah perfect all all right can you guys still see the slides yes hopefully

yep great yep okay and um yeah for these comparisons these concrete kind of you know comparisons I was just curious what is the size of pattern and what is the size of document I know you mentioned in the DNA case it's 43 million characters but yeah maybe you already had this year but okay got document size is and then what's the size of the pattern I guess right because that would affect the lookup table right yeah so we represent the size of the pattern in terms of number of uh states in the autom yeah oh I see so that's so sappha States is effectively the size of the pattern or is is correlated with the size of the pattern um I would say that I would say it's more accurate to say that the

sappha transitions is correlated with the size of the lookup table because the lookup table is made up of the the transitions got it okay so roughly speaking you can think of like the size of P like if I'm if a larger pattern is more transitions smaller pattern is fewer transitions yeah and then I think I can let me double check really quickly um we have in the paper the equivalent um number of states in transitions for um the DFA representation or or NFA representation as well um and in some cases it's smaller or in some cases it's about the same I'm sorry it's never smaller in some cases it's about the same uh like in the redactions case uh whereas in the DNA case it's about four orders of

magnitude larger yeah cool uh go ahead PR yeah thanks for the great talk you guys uh I've been asking some questions in the chat but I thought i' just say hi and also ask a few more questions that I have so the first one is uh so if you could go to the concrete security no not the concrete security the asmic security not security efficiency slides uh this one yeah so I see this Alpha value so is it possible that like if the document is really small I don't know exactly what the alpha value is that some other Solutions might still be better for a small enough

document so the alpha value here is is defined primarily by the regx not by the document so like what you can get is if the document and the reg X are the exact same right if I have the document ABCD and my regx is literally ABCD then you know Alpha is the size of the document right but and so in the worst case I think ASM totically in the absolute worst case you could construct an adversarial regex where Alpha is on the order of the size of the document but otherwise it's going to always be smaller than the size of the document it's why is it adversarial though it doesn't it's just a check right like it's not

necessarily sure I guess if you wanted I guess by I say adversarial I mean like kind of like worst if you want want to construct a worst case Okay the the the worst case and we this this is if you if you read the paper this is the we we have a calculation for Alpha in the paper that's the worst case and in the worst case you have a a reg X that's all look ahads and every look ahead is an exact document match and so Alpha is document size times number of look ahads yeah and I guess like if that's the case you should probably use like an exact matching scheme like those are like you know like cryptographic matching algorithm instead of like doing all of this cool the second question I have is have you tried comparing this uh so for like the TLs attestation

protocols like I don't know if you guys have seen those this problem occurs quite a bit right you have TLS adastation protocols uh there's a notary that says that this is a valid TS tyer text they saw it online and they open like uh some of the plain text inside it or say like you know this this string occur at this position I guess similar to ZK email so I couldn't really map from the comparisons you had uh how it would compare to these other approaches like ZK email like if you were to do the ZK email thing like how much more efficient would it be yeah so I think when you're talking about the like tlsa testation you're talking about like The Deco protocol um yeah yeah yeah okayo and other similar ones yeah yeah yeah so in terms of um

like ZK email so ZK email actually is more more or less what we implemented when we talk about that like DFA Baseline that we compared against that's essentially pretty much exactly the same thing that ZK email does um got it and so right performance- wise reef is a is is much more efficient for that um for Deco and some of these like tlss testation protocols they do something um a little bit different um it's not clear exactly whether or not Reef would be better or worse um in this case I see Let Let me let me make it more particular then right so like one

example of like an implementation that does this sort of RX for TLS attestations is they take this whole string that's the entire TLS session they take all the parts that are not relevant or like you don't want to prove things about and you replace those with stars so then it's like a bunch of stars and then the things that you want to show show are in like the same position so for that case like what would be the order of magnitude Improvement yeah so that's pretty much exactly what we do in the document redaction case so right that is exactly what we do in the document redaction case because redacted government documents are the same thing as you have a document and the parts that you need to redact you. star so you would expect that you know Reef would be much faster because we can skip those

dot stars um makes sense a thing that comes up with TLS TLS attestation and this might be a different issue is that um you kind of are trusting that a lot of times that these Json are properly formatted uh which is a different set of problems entirely confirming that they're properly formatted is a whole other nightmare yeah yeah fair enough and I guess one final question is looks like you guys have a lot of improvement over many protocols so what is left for future work right like what is the juice so to speak left to squeeze if any yeah so so there's a couple um so one of them is like like we kind of just

mentioned that like with TLS attestation checking that things are properly formatted is a similar but whole other nightmare so seeing whether we can adopt some of the techniques there um we're also looking at using Reef for um a number of other applications that are a little bit more complicated than just straight regx mat matching I don't know Jess if you want to talk about your compiler work at all um yeah like essentially like you know the the insights from Reef that like you only need to to look at the things you need to look at a and um lookup tables are faster than computation which is you know not a new

idea in this space but a good Insight can be applied to um a lot of a lot of other things um yeah I'm working on um proving stuff about compilation passes in zero knowledge um where you have some like a and you prove Transformations on it um yeah cool cool yeah I I think I I just want to understand the Json formatting issue clearly again so like a Json file is a very specific structure right so is the question that it is formatted as a valid Json file or is it something else yeah yeah so to get depending on how in the weeds people

care to get about this um so right regular Expressions describe in like academic Theory land something called regular languages right which for something like Json you can use something called a context free grammar which describes a context free language which is kind of a super set of regular expressions and so when you're checking that a Json is properly formatted or that a string has balanced parentheses or that X ml is validly done that's called that's context free grammar checking which is like greex checking and has very a very similar flavor but is unfortunately significantly more

complicated so is one the subset of the other yeah regex is a subset of contact free sounds good okay awesome thanks a lot and thanks Alex for organizing these I enjoy them a lot yeah no no problem yeah thank and yeah big thanks to the authors and I had a couple more uh questions too um but thank you for your questions for two so one question I had is in your guys' scheme I know there's uh some differentiation between different regx engines on how to handle lazy and greedy quantifiers right like depending on the on the engine like you might be satisfied that you found a match let's say like the you know the number one where it's like do you stop at one if it's one you know if it's curly brace one comma two curly brace do you stop when you find one or do you

keep looking until you find to see if there's matches that also have two right so this concept of like a lazy versus greedy quantifier I guess how do you guys handle those here um is that yeah like yeah if you could just make you know comment on that it would be great so I think I think the answer is um uh non-determinism is sort of a superet of those two and uh we use non-deterministic Witnesses in fact I think in the example that we showed of Safa matching a string um there were multiple Solutions and we no deterministically picked one of them uh so I guess maybe the answer to your question is we don't make a choice we allow it we leave it to the prover got it so as long as it's valid the prover can pick any of as long as

it's valid the prover will yeah exactly got it got it so I guess though it's this maybe is like a hair splitting point but it's kind of interesting right because I guess effectively it depends like for a document redaction case this could possibly come up right there's two instances of the same string and you're basically quantifying you found all of them you could get away with just saying you found one of them but there's still one more right as aover was this like would this be a a real world consideration yeah so I think it is I guess you have to you'd have to quantify basically what you want let's just say you wanted to redact my name from a document right you'd basically have to figure out a way to make the greediest quantifier you'd have to quantify it as

greedy as possible right and I guess figure out how to do that that's probably a matter of writing the pattern yeah what we did is we essentially replaced um we took like a like a leaked documents uh database and essentially did that and every time we saw like kind of like pii we replaced it with a DOT star so you still have a kind of enough text surrounding the dot stars that you kind of have to go through the entire thing like you you can't really cheat with that but that is like a big thing is if you're R redacting you know the entire document and the only thing unredacted is like the wordthe you could maybe run into some messiness there yeah I guess I'm just thinking in the case you guys described you were the prover but if you had an adversarial prover

right you basically you're like hey redact everything for me prove that you did and I said I did and but did I you know I guess it's just kind of this is where this question would come up right like did you actually find all the instances and then redact them or did you only show me four of the five and say you did right and I guess with the would the statement still with the verifier still accept that yeah I think I think um I think what Alex is talking about is kind of the opposite of mat is kind of I want to prove that my name does not exist it's kind of the negation right and in the negation in case we we we like like you said we have to go through and check every part of the document there is no way around this

yeah I think when we were doing the document redaction case we were kind of thinking more along the lines of not proving that you correctly redacted a document but proving that you know let's say I'm a journalist I right proving that you know having the government prove to you that there is some real underlying document that relates to this this redacted document that's been published got okay cool well that's super helpful and very clarifying thank you um yeah I think that was maybe my last question does anyone else on the call here have questions PR U patina anyone else I'm all good thanks um cool uh oh I did actually have

one more question I lied can you provide a reference for the end lookup protocol I don't I'm actually not familiar with that and I I've not seen it before so if you guys could yes just share a reference either in the chat or yeah send it to me and I'll put it in the show notes or in the description I will I will send it to you you can put in the description I also mention that this this end lookup protocol is described by Sho in the um hypernova paper got it okay cool uh all right awesome well thank you guys very much I really appreciate you coming on today last call for questions any have questions uh for uh for the authors here today all right thank you guys so much for

being here really appreciate it this was a great session and uh for those folks who are you know tuning in uh we'll have another session coming up in a couple weeks we'll be announcing more about that in our in our Channel and you should be expected to see this video up on YouTube here very shortly thank you guys very much thanks so much