Zero-Knowledge Location Privacy

Transcript

hello everyone welcome to a new learn and share session and I'm Vian Placencia and today we have Shen and Jens who will be talking about zero knowledge location privacy as usual you can write the questions in the chat and Shang and Jen will answer all of them at the end of the presentation you can also unmute yourself at the end of the presentation to ask questions H welcome Shen Rance and thank you so much for being here and the stage is yours feel free to start when you want okay so let me share the screen so thank you wean for introducing

us and we are um we feel pleasure to be able to present our work on zero knowledge location privacy at PS is learn and share here so um yep so today we are going to um present our work zero knowledge location privacy while accurate floating Point SNS and and this work is done by yanuka and Sebastian from TM and Philip from UCL and me from hku so yeah so let's get started so nowadays location based services are ubiquitous so there are a lot of um G location enabled devices

like um tracking devices for example tile or air tag and mobile phones like mobile devices like smartphones and vehicles so the data collected by these devices are sometimes open source and for example in open street map which Pro um provides open open source mapping data and open cell ID for wireless data New York City also open sourced their taxi data and these data are used for um special data processing and Analysis um in um services like uber Uber Eats and

Airbnb and snowflake Marketplace which is a a platform where you can share your um data or purchase third parties data however and for this services to work you always have to give your exact location which um often leads to mishandling of data for example in the um taxi data open sourced by New York City um there um anonymization technique has a flow that um leads to the um privacy leak for example people may learn your behavior or the place you

visit um the core problem of their um anonymization technique is that they simply um hash their the the taxes um license number and the taxes ID but um without SS so um you researchers can simply Bru Force the um the the search all um PR images of the hash and um infer which um which image the digress corresponds to yeah so um in this work we study the

problem whether we can develop a solution that um provides location of fation while um with with without ever disclosing the actual location so um our idea is to prove location is bounded by a hexagon in zero knowledge without and leaking the exact position of the improver so why hexagons well hexagons provide a lot of um great um geomic property is for example it can um test light a plane without gaps it

has rotational or reflectional Symmetry and the distances between its Center and all its vertices and are equal and um hexagons are um actually used in i i hro gold polyes which um uses hexagons for perfect translation of a sphere with um extra 12 pentagons um yeah to cover the sphere so a real world example is a succer bow is the classical design of a

succer bow which um has um 12 black tiles for pentagons and 20 um white tiles for hexagons and this um I H Goldberg poen is actually used in the industry for example and Uber H3 the the index system proposed by Uber assigns 3D coordinates to each hex um hexagonal cell and and the hexagon actually provides um various solution from um one square meter to 4

million square kilometer yeah and um um to um apply the Uber H3 index system in our zero knowledge proof um there is a problem that we need to tackle that is um how can we return accuracy towards hexagon boundaries and the major challenges are twofold first and the hexagons can be either very small or very large and second um mapping uh coordinate to um the index in over H3 requires um

trigonometric functions so these challenges leads to the solution and that um we use a data type and that supports both uh representing both small and large values as well as allowing for um complex operations like geometric functions so this data type is floating Point numbers so in floating Point numbers there are basically two formats the and base 10 formats called that's Mo formats and the base 2 one code binary formats and um

today we are um going to talk about binary formats and examples of them are single um single Precision um floating Point values and double for double Precision floating Point values Etc and in this binary formats we have always have one bit sign s but the length of the exponent and matisa can vary and for example there are um for for the single Precision floating point value the length of exponent e is sorry is eight while the length um of the exponent for double

is 11 and for matisa and the single Precision floating point value has 23 bits while for double it has um 52 bits and generally a real real number or a normal real number has is expressed by this equation the the sign if the sign is zero then Alpha is positive while if the sign is one then Alpha is negative and the exponent is actually biased means that and we need to

um minus 2 to the power of E minus one + 1 to get the real exponent and in the mantisa there is a an is an explicit leading one that is omitted in the um encoding so the sign the biased exponent and the mantisa with implicit leading one and compromise the the entire real number so why we need to use floating Point number and we know there are there is another format for encoding unreal

numbers in computers which is fix point in fix Point numbers and the for example we consider format with 16 pbit whole number and 16bit and fractional that is the fractional part is always fixed with L 16 bits and the matisa part is also fixed with 16 bits and such a floating uh fixed Point number can have range um from minus 3 to th000 to um um Plus plus 32,000 with Precision

.05 however although these um fixed Point numbers have um better performance in Hardware the they often needs um a lot more um space to store than um floating Point numbers on the other hand um for example we can use only 16bit floating Point numbers to represent values with similar precision and ranges or even larger ranges so such a floating Point number 16bit floating Point number um yeah as we have um talked before um can be split into three parts

the um sign part the exponent part and the matisa part and and such encoding maps to the real number this one so the exponent actually has a bias so um it's actually file in instead of um one 101 which is um 30 16 + 4 which is 20 so it has a bias of minus 15 yeah and the m has a leading um zero so it it's actually one point the the the um encode this value yeah

so this um this binary string actually um includes 546 okay so another problem is why why we need an accurate floating point in snarks so in fact um um arithmetic errors can cause detrimental um effect for example in um so so in the um arum by flat uh flight v88 there is an accident that um when people converts floating Point

numbers to integers there are some um accuracy loss that um prevent that prevents the um rocket from um flying normally and um causing the the um the dis disaster in um the um the rocket yeah so um our goal is to um propose a method that allows for accurate floating Point numbers with is well tested against um present standards like I e754 so um let's see how can we um

achieve this in um snars but before that we um majorly um we briefly introduce how AR floating Point arithmetic is done um in Modern Hardware so generally there are five steps in um a basic floating Point operation first is to um compute the exponent which depends on the actual operation but for example um for addition and subtraction the um result the resulting exponent is the maximum value of both and for um multiplication or division the um resulting exponent is

the um sum or difference of these two and the next step is to compute the mantisa part which um is actually um also depends on the the actual um operation we are interested in um so for addition and subtraction the mantisa is also the mantisa uh the the um addition and subra subtraction of the corresponding mesas and this is also the case for multiplication and division and the third step is to normalize the mantisa that is for a

mantisa who is too small like whose lens is smaller than M we need to left shift M until its length is um Big M while we decrement e um by the corresponding offset and for mantisa which is who large whose lens is um larger than M then we um on the other hand write shift M until the the length um equals M's length equals Big M and we um increment e at the same time so the fourth step is runting that is um

we run the final mantisa According to some rules and um in I e754 the default rounding rule is to round to nearest while ties to um even that is um for 0.1 and Z is the nearest number where for 0.8 one is the is the nearest well for 0.5 and 1.5 we always Maps them to the nearest even number that is 0.5 maps to Z while the rounding result of 1.5 is two instead of one because two is a even

number where one isn't and um the rounding direction is actually determined by three beats the guard beit the wrong beit and the sticky beit so and in I e754 the guard bit and the wrong bit are both both the wrong uh the guard beit G and the wrong bit R are important because um there might might be some accuracy loss and in I mean and the there the resulting mantisa might have um less Precision than the original

which um uh which may cause some accuracy loss in the final result if we only have one of G and R so both of them are important however in our our application we and keep the accurate intermediate mantisa so we don't really need both of these bits we we only need one and the sticky bits yep so the final um direction is computed by um G and P or r or s that is um if G is one and the there are some

nonzero bits in the wrong bit or the sticky bit then we um need to add the Intermediate matisa by one while and if G is one and round is zero and all all bit all following bits are zero then the rounding Direction depends on the parity P if the parity is one if the intermediate Mates is one then we need to add one while if the intermediate Mata is already odd is already even then we don't don't need to add one and on the other hand if the guard bit G is

zero then the the following following bits are smaller than um one one z z z and um so we don't need to um add one into to the final um mantisa yeah and finally we need to handle some edge cases like um division by zero or overflow or underflow Etc and um now let's get into um more details of floating Point numbers so

um first we we consider how uh and how a floating Point number and and encod an encoding of the floating Point number maps to the real number if the exponent is e exponent e is zero then there are two cases where um if the mantisa m is also zero then and it maps to Plus orus Z while and if the Mana m is non zero then it maps to subnormal numbers which is actually um written by

this and um for a nonzero exponent e which is smaller than this 2 to the E minus one then the resulting um real number is called normal numbers and finally there are two where the cases where um e is um equal to two to the um Big E minus one and then um we say the real number is Infinities if the Mata part is all zeros while the um real number is soall not numbers or n if the um mantisa part is non zero

so in uh in in order to um handle all all these cases while um operate uh compute the floating Point operations um that are compliant to the standard we first in introduce some General optimizations in circuit and then we discuss our tailored um optimizations for um floating point so first um a common um technique used in um snar circuit to um improve efficiency is the nondeterministic advice or so-called hints which instead

of um execute execute the um original computation inside the circuit we ask the pr to provide some hints to the circuit and the circuit can check the correctness of the this hints in a more um efficient way than um the original computation so for example um if we um compute um Alpha over beta the division between Alpha and beta instead of computing um the division of this mantisa in circuit we ask the pr to f um

the quent Q and the remainder r as hints and then the circuit only need to um inverse the Mattis of alpha equals Q * um beta's M plus r and um as well as The Well formedness of Q and R another example is the computation of square root of a floating Point number l so again instead of computing um the mat of alpha in circuit we also ask the approver to fit in the square root n as a hint and then the circuit only needs

to enforce the square of n is smaller than um Alpha Mana which is also smaller than m m + one the square of n + one yeah this cheack is actually sufficient because there is only um one square uh one number that um satisfies this this track which is the um the actual the correct square root number of um Alpha and another technique that um

in recent years is why look up arguments and so for example if we want to check um if the value V is in the range from zero to to the power of big V where big V is a constant then we um ask the Prov to feed and v0 V1 Etc as hints and the pro uh the circuit enforces that um V is indeed the conation of this this so-call lmbs of v and then and the circuit also enforces that um v0 V1 this

all these limbs are in a PR computed lookup table VI look up argument in fact if v0 V1 and um Etc are all bits then uh this method is in fact the um traditional bit decomposition technique while if the length of v0 V1 is larger than one then um we can um to handle this more efficiently by building a larger lookup table however and this range check becomes more

um um more expensive when um the the bond the the range Bond of the value V is variable um in our case we always consider um the U the upper bound of this value V also has a upper bond which is two to the power of big U so to um do a variable sized range check we um in fact decompose this cheack into two that is we first inforce V is smaller than um 2 to the power of U but um L greater than or equal to zero

and then we also inforce U minus vus one is um greater than or equal to zero while smaller than 2 to the power of U so as we can see the variable siiz range track costs um twice as much as constant size and range tracks now and let's discuss the integer operations so we we are majorly interested in two operations first is the um computation of absolute value of

X and second is the right shift operation on X so to compute the absolute value of x we first need need to define the sign of X because um all these um variables in a circuit are in a finite field but there is no um sign in in this um field elements so we manually divide um the finite field into two parts so um we we say the sign of X is one or X is positive if x is in this range from 1

to um P minus one / 2 and um on the other hand we say x is z uh s s of X is zero or X is negative if um X lies in the range from um p + 1 / 2 to um P minus one so by doing so we are able to um determine whether whether X is positive or negative and to aieve this in an arithmetic circuit we also um Leverage The nondetermined itic um feature the

nondeterministic nature of arithmetic circuits so we ask the pro to provide the sign S as a hint and then compute the absolute value depends on S which is um if s is one then X is positive while um if s is zero then X is negative so we um compute the um oppsite number of this x then the circuit enforces that s is is indeed a bit is um indeed either zero or one and we check if the absolute value

is um in this range between zero and 2 to the power of L so if the pr Pro provides a fake s and incorrect s then the absolute value would be negative and such a Negative value cannot fit in this this range because here L is um reasonably um small than the um the the log two of this field order and finally the circuit um simply returns S as the sign and the the

absolute value and now let's um see how we improve the computation of um right shift so here we also assume that the X has um upper Bound 2 to the power of L and D has upper bound K so let's compare the left hand side with the right hand side so um intuitively we can um ask the pr to provide the quent Q and the um um the the the remainder r as hint for this division operation and we

enforce the um q and R are well formed and we also enforces Q and R and can recover the original X by comparing x with Q * 2 to the D plus r and finally um return q and R however as we have discussed before this um this D is in fact a variable so the upper Bond of R is also a variable and this track is in fact pretty expensive so um in order to get void of this variable sized um Range check we

instead ask the Prov to um provide hint QR for the operation x * 2 the Power of K minus D over 2 the^ of K so in this case the um the divisor to to the power of K is a constant so um when we check the range of R we are comparing it with um zero and 2 to the power of K the divisor so this becomes a constant sized and range cheack which is in fact um twice as effective as this um variable sized range

cheack then we um simply compute um x * 2 to the^ of K minus D um and compare it with Q * 2 power of K plus r and um returns Q as the result and R as the remainder okay so then let me introduce how we um we introduced and optimizations um tailored for our floating Point operations so first um we convert the um

I e754 um representation to a circuit efficient form first we treat um subnormal numbers as normal numbers to avoid handling these values separately so this is done by Shifting the mantisa to the left by D minus one bits so that um the all zeros are shifted out in a subnormal numbers while the one becomes the implicit leading bit at the same time we also decrement the exponent by one minus uh by D minus

one so um the original exponent is zero for subnormal numbers and the resulting one in our circuit becomes 1 minus D and we also Mark this this one as implicit because this is the case in um normal numbers however um we can um although these um subnormal numbers um behave similarly in normal um operations one Pitfall is that um in ring we need to take care of this this um subnormal numbers because they have um lower Precision than normal

ones and and we we will introduce this um later yeah so for um the ex and for a normal number we also expand the expand its um exponent and Mana to simplify computation that is for a normal number and with E and M as its exponent and mantisa we compute the unbiased form of exponent and um we also compute the mantisa with its um explicit

leading one finally we also um um we we also unify all Nan values by using a canonical Nan however um this doesn't allow some techniques like n boxing but um over all people um don't really do this um complicated technique we only treat n as a um as a abnormal value so it's um it makes sense to um do this unification yeah so because um n and

zeros behave similarly in multiplication we simply set um the mantisa of this um n values to zero so um they can share some um computation in um multiplication with zeros and um in turn can save some constraints in our circuits and um let's talk about um bit operations for rounding so um as we discussed before um subnormal numbers is treated as normal number

however it actually has lower Precision so in rounding we need to preserve um less number of bits than um normal numbers for um for subnormal values yeah so this leads to um our design of configurable mtis Silence that is and we keep M +1 bits for normal but M +1 minus Delta e be for subnormal where and this Delta e is a parameter that and controls how many bits to keep for um subnormal numbers and the second Technique we

apply is um to um split the intermediate mantisa to um compute the um rounding Direction more efficiently so here um we um instead of um handling this guard bit and round bit and sticky bit um separately we first and only need one of this guard bit and round bit so we only need round bit and then um to compute this scky bit we don't really

need to compute the logical or of all all of these following following bits we um can simply um keep all these values uh these following bits and compare s with zero um because um Computing logical or in circuit um um is uh cost one constraints for each operations so there are a lot of bits here and and the overall cost is pretty high while comparing a value with um another value only takes um two

constraints yeah and um so instead of um Computing G and logical and p r r r s we know and compute R and P or S equals z yeah and um back to our um technique for splitting the intermediate MAA into um four parts the M Prime part the parity part the round bit part and the S part for all bits in this um sticky

sticky bit computation so we first and need to avoid a variable sized range check on this s because um the the the the the resulting M may be smaller than this m m+ one but can be in instead MN + one minus Delta e where Delta e is variable so we need to um we need to um compute the the resulting s with a variable sized range cheack but um as we have mentioned

before the variable size the range check is is expensive so um we need to um apply some techniques that um um that we mentioned before which is to um left shift the mantisa and the the entire mantisa before splitting and then we simply um make this s the length of this s constant to um save some constraints and finally we um determine the rounding Direction by um removing the guard bit and removing the logical

or in this in the computation of this sticky bit and so yeah as I just talked about we remove the guard bit and simply um assume the intermediate M has sufficient Precision while um we get a void of the get rid of this logical or in sticky be by simply and comparing s with zero and finally we talk about two examples for um floating Point circuits which is and the multiplication and the computation of square root so to

multiply um two floating Point values Alpha and beta we first um add their exponent as um um as I talked about as I talked earlier and then um we multiply the Manas to get the intermediate mantisa which is m equals um the product of um Alpha M and beta's M and M is either zero or Li in the range from 2 to the power of 2 m to to the to the power of 2 m + 2 two because um the the M of Alpha and beta are um

either zero or in 2 to the power of M and 2 to the power of m + one so the resulting m is in this range and by observing that the M um the range of M we can in fact simplify the normalization process that is um we only need to receive a single bit from the approver as a hint which is the um MSB that is the 2 m + 1 B of M and um this is because um M now

only uh the M now has 2 m or 2 m + one bits so um there are only two cases for an nonzero M so um we only need to left shift um the intermediate M by one if it's MSB is zero but um if a nonzero the uh MSB of a non zero m is one then no shift happens so this these are um the only two cases yeah so providing a single bit m is sufficient for our

normalization and um the circuit then enforces this B is a ping value and enfor is that um B minus m b * 2 to the^ of m + one that is m without the leading bit m leading bit B is in the range of 0 to to the 2 to the^ of 2 n + 1 and finally we compute the nor Mana as um M left shift by 1 minus B and the um resulting exponent which is um e plus b next we um wrun the the intermediate

Mana by um adding this um value as um described before and finally we handle some Ed cases like um the multiplication between a normal value and Infinities or um the multiplication of zeros and Infinities which um produces n and um yeah that's all for multiplication and um for the square root of alpha we um first help um have the exponent by left shift the um uh the

exponent of alpha by one and we obtain the um tentative um exponent e and the bit one uh the the B which um is the shifted out bit Yeah and then we compute the square root of the matisa of alpha so again um we um ask the prover to provide a hint for the square root operation and we we enforce the range of uh the the range of this original m is between um the square of N and the

square of n + one so um and however in our um in our case and we need to shift the original matisa before Computing the square root as um um the the original matisa only has um Big M bits of precision and after taking the square root and the Precision becomes m / 2 which is too small for um uh too small for a desired um Precision value so we need to first shift it to the left by n+ 4 bits to

make sure that the resulting n is accurate enough and we also add um the bit B to double the um original matisa when this original exponent is odd before um the shifting operation and we can even and avoid this normalization process by observing that the um MSB of non zero um and the square root is always one so we don't really

need to um left shift or right shift the um intermediate mat however um in rounding we need to be careful because um the square root may require infinite bits of storage however our n only has a about M Big M bits so we um introduce some auxiliary information to help determine the sticky bit that is um if the shifted um is a perfect square then n is followed by all

zeros so the sticky bit should be um zero and and otherwise and the following bit should contain some ones so the sticky bit should be one and this logic converts to um the blue part um which um additionally um comput The Logical end between s equal zero and the equality between um n² and and the shifted Mata finally we compute the and we we

handle the Ed cases um for example um the um square root of a negative number is um there is no square root of negative number so we simply return n however for negative 0 the specification defines that its square root is negative Z so we need to return negative Z in this case yeah so so that's all of my part and then let's and invite yans to talk about the um the um

our zlp circuit um with um our tent optimizations oh great uh share this there you go okay great uh thank you Chang um yeah great uh so now that you've seen basically how we represent floating Point values uh in circuits and in kind of like an adapted optimized way um and how we do multiplication and and and compute a square roots um we can basically use this in applications right so um uh in addition to square root and multiplication uh we also have circuits

for uh addition um subtraction and division um you can find the details uh in the paper I guess and I'll just describe the application that we basically uh use the floating Point circuits for right um so changra already introduced um basically the Uber H3 algorithm just to recall um uh how that essentially worked um so you can see on the top right you have the iosa hedron right which is the top leftmost picture and then you basically map that onto the sphere of the earth and then project basically hexagons into each of the EOS sedron right um in kind of like the uh Goldberg

polyhedron formation um and on the left you see basically the uh latitude and longitude mapping to an index of each hexagon that employed in the Uber H3 algorithm okay um so the input basically to this algorithm is the latitude and the longitude and the resolution resolution is from 1 to 15 so if you have a resolution of one each hexagon covers like an area of like a th square kilometers um whereas uh if you have a resolution of 15 the area that an hexagon covers is uh 1 square meter roughly so what you do is essentially in this algorithm you convert the latitude and longitudes to

to radius uh then you convert it to spherical coordinates the the spherical coordinates to to cartisian coordinates XYZ um then for each of the Triangular basically Equis sedron faces um you calculate the closest distance and choose basically the Eon with the minimal ukan distance to the actual latitude and longitude um or XYZ coordinates in this case right um then you calculate the radial distance um based on the resolution as well um uh and uh then you convert that basically in the end to 2D cartisian coordinates and map that to a three-dimensional coordinate system that

uniquely identifies uh each hexagon that is mapped onto the sphere right um R three afterwards also maps that to basically um uh an index in HEX format um we don't do that because igk coordinates already sufficient to identify um a unique hexagon on the sphere basically right um so what's the actual problem with this turns out that this uh transformation um this spherical transformation from lude longitude to index involves a lot of Trigon trigonometric operations right so first one being um uh X Y and Z so the

three-dimensional caran coordinates are calculated from um through uh applying s and cosine basically um to the input latitude and longitudes right which is kind of like the first problem and then afterwards you apply a lot more trigonometric uh uh trigonometric Transformations um such that you finally basically end up with the with the igk coordinates right um I guess on High level it's the only thing you need to know so what we do is we um we essentially apply two optimiz ations right first one is we elim eliminate the first trigonometric function um in the beginning right by uh replacing

basically the X Y and Z coordinates that are usually computed directly by S and cosine um uh with a computation through hints right so we compute the trigonometric functions out of circuit um and then uh use the relation between the trigonometric functions right the trigonometric identities to check in circuits that the provided values are actually what we want them to be right um so then we basically get rid of like the first uh the first uh trigonometric um uh function that we need to compute in circuit um and afterwards as you saw here right like everything besides the first black

box uh is basically uh the rest that you need to do in circuit and turns out if you think about it long enough uh you can figure out how to use uh trigonom trigonometric identities to end up with an optimized version that only uses space basically a square roots um instead of uh trigonometric functions themselves right so what you can see in uh the on the right side is the the the optimized function so you see R for example um is not um uh is not computed from from from uh any trigonometric function just uses square root and exponent ation right um and X and Y similarly where you can see that

the cosos of theta f i that is a constant for example so all of the values the co cosinus s um Co cosine sign and whatever you see on the on the right side in X and Y are all constants right so right those are basically the optimizations that we have on this side um then we basically implemented uh we we implemented everything right we use um to test the floating Point implementation the Berkeley test flow three um a repository which provides a test set of test cases that ensures compliance with the I standard um then we apply basically all of the floating

Point operations in a way that enables us to prove uh the latitude longitudes to index transformation um and double check that our implementation is equivalent with the one of uber by using the Uber code to essentially directly spit out uh the Transformations uh for for different sets um of latitudes longitudes and hexagonal indices um and we do the testing in a way um as you remember in the beginning we said we need floating Point operations to basically uh uh determine uh to retain accuracy towards hexagonal boundaries right um so what you can see on the bottom here is we

test the this against an unoptimized fix Point um implementation that uses uh fairly naive implementations for cosine and S um and as you can see for example for a six uh for fix Point implementation uh with six digits after the comma um the uh basically our tests already fail for the middle of resolution 11 so so for example for resolution 11 uh we have like 10 test cases and each test case is logarithmically closer to the boundary so we kind of like logarithmically approach the boundary of a hexagon for for each of the resolutions as you can

see for for six digits after the coma it already fails for resolution 11 and for fp32 it only uh fails for for uh the end of resolution 15 and for fp64 it basically passes everywhere right um now to the evaluation so how performant are our circuits actually for the floating Point implementation what you can see on the top right is basically the R1 CS constraints um that you need for a table size of the lookup table of two to the^ of 8 um those are divided in basically native constraints which is everything besides kind of like the lookup argument

um uh in this case uh that is uh 31 plus like the 33 which are basically the number of lookup constraints per multiplication that is uh scaling linear with the number of multiplications uh and the 291 in this case would be fixed right for fp32 so the interesting thing here for for the lookup argument what you get is amortization right so in the lookup argument what you have is you have a set of quries and then you have a set of uh table entries which is basically Vector that describes the table um and you can see um the equation that is used to check that the lookup lookup argument is actually correct uh which is derived

from the log of work of o r k um uh this equation is actually checked in circuit um and you can see that basically the right side um that um uh that computes so the the the the constraints that compute the right hand side of the equation are constant as well as checking the quality is constant right so uh those end to like an amortization in the overall number um of constraints that you need if you have like u a certain number of multiplications uh that is larger right so for example for you can see in the bottom right um uh you have two to the power 15 um two to two to the^ 15 uh

floating Point multiplications in a circuit you'll see that it ends up approaching basically 64 um uh 64 um constraints per multiplication right which is equivalent to what table one says for an fp32 um uh yeah multiplication operation right um so how does that impact our uh zero knowledge location privacy circuit um uh the zero knowledge location privacy circuits um it's fairly performant so for fp32 it only has around 20,000 constraints um just to set that into comparison the Baseline that we use to examp to to to evaluate um fixed Point operations with

like a naive implementation for S cosine and whatever um that uses uh 310,000 constraints right so this implements basically the exact Uber H3 algorithm without optimizations and with naive fixed Point implementation which should have theoretically less constraints because it's not as complex as FL the um computation right and we also apply this to basically another application that is P2P proximity testing so once you have like a proof that proves that you're inside some kind of like hexagon you can out of circuit just determine the distance to the closest point on the boundary of the hexagonal index um and that plus the verification of proof

allows any Pier uh to evaluate basically proximity to creater than 400 Piers per second um right if you noticed um then there might be uh one problem that still arises that is that of authentic locations there is a couple of approaches that you can use here ideally you have signed GPS signals um but that also like um is kind of like suboptimal because then you can still forward the sign GPS signal to some um there is other approaches uh that use kind of like a Byzantine uh Network to basically triangulates the location of specific

um uh specific devices here the problem is that you that you end up uh with like very high in accuracy um so uh I think the lowest that you can get to I mean that depends on the kind of like number of Challengers um that you have in the network but I think uh approximately if you have like I think there was a paper recently that describes this if you have like 100 you get down to like 100 kilom of accuracy um which doesn't allow you to go down to resolutions of like I don't know a square meter right um so uh and yeah for that you also need very accurate timing information because uh if you basically do triangulation based on like round time trip round round trip round time round trip time uh RT then uh

uh yeah you basically uh end up with a very high very large dispence based on the speed of light um right so ideally use like a secure Enclave that just tests to whatever location you are in um problem here is if you look at an iPhone for example secure Enclave doesn't uh provide attestation to location information so you would have to kind find some kind of like workaround um I guess maybe through like uh trust execution environment uh with kind of like Universal programmability um yeah right and if that is given you can do very fun things uh as we already built with this hexagonal index um uh you can apply it arbitrary algorithms um

for example like uber is using this uh to calculate basically optimal routing strategies and pricing strategies right so you could do something like apply IVC and like kind of like um so incrementally verifiable computation and go through kind of like uh yeah a couple of hexagon and get like verifiable pricing for uh basically Uber rights um or Logistics I guess yeah and similarly because we interested in also blockchain applications right um if you have the authentic location you can do something like privacy preserving validator GE location um uh with high authenticity um whilst keeping kind of like the privacy

of the validator um uh without disclosing its location right which would be very cool to do and probably also has some impacts uh uh on the Meb landscape I guess right um there's also some remaining challenges and applications for floating Point snares um our circuits are very Universal uh you don't have to apply this to the zkp or location privacy use case um you can also basically uh try to figure out how to do I e75 for compliance uh Z KVM operations right um so for example everyone's right now building zkm for the risk five instructions at architecture so you there's like um the F extension in the risk five instruction

set architecture so you could think about basically how to apply the optimizations that we provide that are very generic um uh in kind of like optimizing um yeah floating Point computation for zkm um you can build zkl models um by adapting our implementation to half Precision so 16 bit instead of 32bit or 64-bit um or you can do also basically audio authentication because Digital Signal processing always involves uh floating point computations right cool um that marks the end of our talk um uh with our implementation I guess you can now use floting Point arithmetic in your circuits um our implementation

isn't go uh specifically in gar um uh yeah um and it worked pretty well with our application so yeah happy to ask uh and answer any questions uh that you might have thank you and sorry for being a bit over time yeah no worries thank you so much for the great presentation and yeah for the audience feel free to ask questions in the chat and also unmute yourself to speak yeah we can wait a couple of minutes maybe two minutes if there any questions but thank you so much Shang and and J for for the

presentation yeah thank you so much for having us thank you there's one question uh yeah you can just send me I guess or Chang Ru an email um if you'd like to discuss if you've done any similar work um to this one uh let me just drop my email here um the chat you can reach out there you go yeah and mine is if this you can also find me where my UCL email address but and it will I guess it will expire in

September yeah okay then is there any more questions thank you very much for the presentation and thank you everyone for attending and have a nice day everyone thank you so much hope it was helpful have a nice day bye bye bye thank you bye thank you bye