Building Zero knowledge proofs with Keelung

Transcript

go go go Victor Victor he uh hello everyone um initially my talk be English um just wondering is anyone here who don't speak mandering no uh oh that's one okay sure great then I'll be speaking

English yeah I I was going to be this it was going to be English anyway uh can I go full screen how do I go full screen this one what what what what uhhuh oh okay cool okay hello everyone um my name is Victor um this talk it will be super fast because I initially made this slides for 55 minutes and later out I I I just found out I only got like 30 minutes um but yeah it's the last one so I guess we can spend as much as we want right so kilum is a uh language that was designed for fast private and secure little

launch applications um and we are from btq BT Q is a post is a quent technology company focus on building post Quant infrastructures uh in blockchains such as blockchain because I believe we have all solutions now um and we have a lot of uh experts on uh postum cryptography and of course Keyon is one of our project um kilon is open source now so you can go to GitHub and see our open source repo um we have separate two separate repo for kilon one is the compiler which uh can which usually will be built into native binaries and we want is the language itself and of course we have documentation so go there

if you want to learn kilum by yourself uh oh okay so here's uh okay here's some outlines here uh this is the main three parts I'll be doing today uh and later there are some details about kilum infrastructures that I'll probably not go into details because we don't have time for that uh but I still want uh to give a little everything for everyone so first of all I still introduce from Little proof if some of you who don't know little know proof is I'll give a very very very brief examples and later I'll introduce kilong and talk about why we need a language for building little proof applications okay so what are leic proofs as a lot of you might have know

leic proofs uh proofs of knowledge are things that help the pro and to show the verifier that they know something but this is very very uh general idea idea you don't know what it actually means right so for example a password is something uh the prover may want to show that they know something um but telling the verifier of the password itself is very dangerous so you need a hash uh for example uh is which is a common practic they Pro law approver to show verifier that they know something without revealing it so for example this is called the Ali Baba cave example but there two there two people here are called Alice and Bob not Ali and Baba uh so if if you if if there is a cave

it's a circle it's a circle shaped uh Cave and there's a door in the cave and Alice can go and Bob can go into the cave and check that he cannot open the door in in the cave but Alice know how to want to show Bob that she know how to open the door so what she can do she what can she do she can go into the cave and go out on the other side and Bob can watch at the entrance of the cave and see uh Alis has turned a circle around and success successfully pass through the door so now Al has suly proved Bob that she knows how to open the door without revealing how she open the door so what what's more what's a more

concrete uh I think there a more concrete definition about this uh little knowledge proof so it's not just about a verifier not about aover showing they know something it's more about they showing that they know an answer to a problem and without revealing the answer itself but more concretely um in the setting of uh existing Z knowledge proof system uh the the system allows the prover to show very there no solution to accept a variable such that it certifies certain constraints what does it mean uh let's to um before we dive into that let's take Us's take look some uh applications of lkps we have identif identity identity verification uh

privacy preserving cryptocurrency transactions voting systems uh medical and health records all these things require uh you know a lot of privacy requirements uh but uh they want to for example in voting system you want to reveal that you're actually a citizen but you don't want to reveal your actual identity so how are can reconstructed most many protocols now from using the computational circuit model uh by Circuit uh actually means a a set of variables and constraints so this circuits are open formulated with bunch of polinomial equations or as we code with analogy of circuit we code in Gates um some common example of this

interfaces are RCS and air or air uh in short but most we will focus on RCS today and this this is also what kilum mainly produce okay so let's do a quick review here what's a typ CO KP application development workflow so we have per descriptions which are constraints and we put them into the proving assistance and proving assistance give out two programs one is a pro one is for approver one is for verifier and the prover uh takes the public problem description and input their private information and generate this Cod so-called proof and verifier take the proof and the uh open problem description and

verify that this Pro actually satisfy their uh constraints without getting uh the private information that was input by the approver so the RCs is the problem description uh and The Proven system include grow 16 or plun or Aurora which Aurora is the one we use right now because uh we want it is a poent it's a Content safe protocol um but uh for for existing projects on on uan for example uh they use a lot of grow 16 and plunk is uh there are a lot of uh extended version of plunk system we call them plish but I think they are still in

research so what how we why do we need a language because descriptions can be very very complicated um so we separate the problem descriptions and constraints so problem descriptions now can be we should we should Express them in more human readable ways instead of weird constraint like RCS uh we will see how RCS look like later so there are there do there have already been some Works some language that uh do some basically the same thing as kilong but I also talk about why kilong why we need a new DSL for this kind of problem okay so let's see how complicated RCS can be RCS what is RCs

is is a is the const assistance for expressing computation that can be used for generating Z knowledge proofs so grow 16 and plun and Aurora this three proof all use R1 CS as their interface so it itself does not contain any information for theologic proof but it's just a description of variables and their uh constraints and rncs comprise a set of constraints of a set of variables each constraint consists three linear combination of variables arranged as follow uh so there you can see here are three pooms um so for for a set of variabl that's from x0 to xn you can construct a constraint like this uh where a a z to a

m b 0 to BN c0 to CM are all constants so this is a linear combination um and in most since uh they are most be elements of the same finite field this is very important because this is required by the cryptography system and this is where all the problem comes from so for example um if we want a if we want a uh we have a problem here and like this uh this is is a polinomial uh this this is polinomial how to say that constraint okay so uh the power the power of X Plus x equal to

26 uh if you look at first s you probably don't know what actual answer is and the problem can get very complex so complicated that uh the computer cannot solve it but only someone can uh only someone with an answer can answer it like you know um like R say you know like uh yeah things like that but like factorization um if the prover have the answer to this question they might want to prove that they know the answer without revealing it but before that you had to it has to be translated to this rncs constraint system so you can see here are three constraint we introduce two ex additional intermediary variables

Y and Z and if you look very closely you can see well uh X is actually the X right there uh but we use three constraint to express the sensing as the example we provide so all R1 CS has to be written in this way so you can see each of three of this uh constraint satisfy our definition of rncs okay so yeah you can you can multiply two thing together each of them are only just additions okay let's so this just a very quick example it's not yet we also tell we also have to tell the ZK proving system which variables

are private so the proof can be generated without revealing this informations and some of the inputs can be B public so what's more complicated is for example bullying uh we have I have said that I've mentioned that we have only uh finite field elements so finite field elements uh kind of can kind of be compared to on sign integer with a certain size how do you how do you express buling in in a system that only allow uh uh un integer or only allow finite field elements so uh bulling expression can be can be expressed but you have to be mimic in a way such as this um if two finite field elements

multiply by itself is itself then it's either one or zero um in this way we add a constraint to that variable to make it appear as a bullet so um this is a very simple example you can do operation on that like negation and or xor but yes you can see if you don't want just bullying you want a lot of other constructs like equalities like conditionals U things can be very complicated very quickly um so nobody want to write this weird constraint manually if all this can be expressed in languages in human readable ways they'll be uh much more

better so it's almost impossible to construct we need a program language and compiler okay so what uh I think a lot of you might know what dsls are so I will introduce further so we need a higher level intuitive way to describe the KP citations and we want this language to be so uh to be more intuitive such that uh people without cryptography knowledge can use it and Abstract the details on the lineing protal such as R1 CS or a so not only can do a lot of this language try to uh mimic the style of C or you know rust but um a lot of features in those language cannot cannot be used there or so we we just don't

allow this in our language such that is more intuitive uh yeah most most General prop property language are just not desined for this okay here are some existing uh dsls so we're just adding one more DSL but all of them have stand along ecosystem so what we do is that we embed Keyon this language in hasco is a general purpose functional programing language that fits a really it's a uh that plays a really great role um uh Define other languages so we have compiler that's also written in hasco and it's based on Saro it's a it's an academic work by Golden stal uh

it's open sourced so let's take really quick look about about kilon uh we have inter inherited all language features of hasco uh such as it functions and module system and when we maintain a simple small C language um and we do have uh interface between kilong and hcode such that we can use existing hcod libraries uh and functions uh we have three perty data types which are field elements bullings and on integers so as you can see uh the buing we Define uh you can just use buing directly in your language and without um knowing the underlying weird constraints translations and and

we also have uh a m uh we have keep tracks of the constraints on variables and we Al have simulated a mle array uh this is uh a Monet so we use a Monet but if you I can't talk about what monad is so if you want to know what mon is we need like maybe maybe three more hours uh so just yeah just think of it as a environment things like that so what does a what does a kilon program look like um here it's a a kilon program is always a valid has program um and here at one is a valid higho program and this is the type signature of a high scho program we say oh add1 is a has uh

object um we don't use object here uh has Type has scene code comp of type comp field um comp is a Monet and field is the uh kilong is the type of the return uh is a return type of the kilon program so you can see this program take input prob input and return it is uh and add it by one and return it okay okay so back to our example if we want to assert something is to assert uh we want to take write a describe a problem that is uh we have a input of X and uh we want to ass that uh it we have

as a constraint that uh the power of 4 X Plus X is 260 we can write it this way uh which uh this program rains nothing but it takes a private input okay so we can generate constraints from the the program we just provided uh here is a jci that's the the um interactive interface of hasco so we use all the we use compile which is provided by our uh K library and you can see the constraints are generated uh there are three constraints and you can see they are they are the same as as we have provided okay why another DSL because it's more flexible it's tensible compared to existing languages because

we have made use of existing hasco ecosystems so uh hasco is very expressive and yes very Advanced type system a lot of we weirdos have embed a lot of Weir languages in has scho like you can write HTML in Haso you can write C has scho they are all uh totally embed in has scho without you can write them as the program in mind but they are actual High programs so yeah it has yes uh as a the Purity feature is very nice because we don't want side effects in Kong and the ecosystem can be reused uh we use Tasco building system uh haskill testing and package managers and of

course the documentary libraries and of course we have um we hope this could reach more developers than uh the existing uh dsls because all of them are standard on DSL if to learn from scratch so here's a compound overview um it's it's uh I won't go to detail here but in in general uh we separate the syntax Tre and constraints and the compiler just compile the syntax uh into the constraints so when writing hode you don't writing the kilon program you don't have to com uh you don't have to worry about constraint oh the comp will handle it for you okay so we have meta we have a lot of features going on but we'll just

we'll just do a very brief view quick very quickly we have meta programming kilong meta programing kilong is essentially Pro programming in has but you write has they generate kilon programs so it's meta programming kilon and yeah we can reuse function anywhere reuse kilon function as well as reuse meta programs of kilo uh we have loops uh which for example in this sample we add string together and we have conditionals uh uh which are uh which can be translated to our NCS constraint as well okay so uh like for example let's do a quick test uh we I won't provide answers here and if you want to

do them you can think about it yourself uh factorization is a example that um a lot of people want uh this one factorization it I take a this program takes a public input and they take two private inputs so the prover want to provide two private inputs uh private uh PR they know and the verifier want to verify that okay so there is a public input that is um that is how to say that divisor divisor not divisor MTI Factor okay X and Y are both factors of Q yeah um there are lot of

constraints here so if think of it think of it uh X and Y and Q as how do you translate onsign integers to fields to fix because this program can be compiled with any given field we support like for example we have field that has only 64 bit WID how do you how do you support this small field uh how do you use this small field to represent a large uh on Integer that is uh with the width of 128 okay um yeah but we can do that you can write this in in in kilon but if you want to do this in the constraint yourself you're going to be very

problematic um okay we use the sequence buing to represent represent outside integers that's one thing okay but this this the problem was still not solved yet um this for example this kind of representation we use eight B integers just like the comps do it represents a two2 55 so yeah we have on integers uh we have dependent types in kilum which can uh uh assign the width of un compare time and and do a lot of things we have assertions like I showed uh of course we also have okay let let just we also have other features such as multiple arrays

uh of course and on integers of arbitrary long bitwidth we can just use arbitrary long with bitwidth and we have operators on this on integers uh not just operators on Prime um but they look kind of the same and we also have custom data type you can you can write hasco data types and use any kilong as long as this data types can be encoded into kilong into kilong fields or kilon Bings or kilon integers um the translate process is is up to you but I have we have been Auto we have automated this translate process so you can use any data types you want and our compiler will determine if it can be translated to uh kilon programs and then

RCS so yeah we have we want to use as much existing HQ code in K as possible and yeah this can be uh skipped okay so to Lings uh we yeah this also can be skip we have also a gab Cod space playground uh do we have time for the live demo yeah oh no my computer is because the computer issue we can do a left in right now with some future M map like more more libraries crypto creatives more function signatures ciphers the ID standards yeah and new bends we are supporting plun H2 we have integration with snjs which is not complete but will be complete yet so thank you very much for the talk if um thanks for coming and we still have like

5 minutes for q&as so if there's any problem please raise your hand now hey please okay okay okay um so the result of the compilation process would be the prover and the verifier programs correctly do you mean the compilation process yes yes I I I write my Kong program which is hcal pretty much I have the compiler yeah yeah so the compiler actually only only compile the programs into constraints and after

that we feed them to the proving system which I haven't mentioned here I I didn't mention any proving system at all uh but for example SN have integrated some proving system and we have other ring system uh they have they have provided other libraries other executables that generate Pro a verifier okay so the constraint that falls out of the compiler um in order to use that I don't need hasc to use what I in order to use that I don't need hascal it's just for the generation of the Contra yeah yeah yeah if to to prove and verify things you don't need has at all yeah okay thanks so so after developing the ZK applications uh you put the compile constraints online or anywhere and the proof and verifier can just download the

pro proving and verifying binaries with L using H all yeah so any more questions okay just know if um I just have one more thing to add that is I am going to be holding a BF bir of Feer today uh I finding people who like cocktails so if you have good taste and you drink a lot please contact me we'll drink till we are all down and we only drink good kak bars so thank you very much