ZK Hack Montréal: Polygon - The eSTARK Proving System & Plonky3

Transcript

[Music] [Music] hello everyone we are ector and Roger ER from from the polygon we are currently working on polygon gkbm I don't know why that we are supposed to be like the Spanish Mafia I don't know why we got this name to be honest yeah and and the idea of this talk is well to explain a little bit the tracks that we are going to be offering during this ZK hack specifically we both are going to be explaining like the eif fire which I will say it's like the cryptographic option of the two on that

we have and then we will have a we have Brian in the in the plony 3 tool stack which is probably much more generic yes thank you uh so well let's start with the basics ER I'm sure that most of the people in this room know what is a gkbm what isk roll up and all this stuff but if just one person doesn't know what it is I think this slide will be worth it okay so as you can see in the slide H I'd like to summary ZK rollup as an application that leaves between two layers Layer Two and layer one I I think I I I like to say that layer two is like

the execution layer and layer one is like the ification layer and the main idea of a rollup well basically users send transactions on the layer two okay then this transaction somehow get roll up into a single subception in L1 so you can imagine this as having a bnch of transactions in L2 that's that gets compiled down to a single transaction in L1 and well that that would be like the optimistic part of the GK rollup but if you want to add GK to a ZK rollup then somehow you have to generate a validity proof of what you're doing is actually correct and valid okay

for example you cannot send a negative number of coins from one to another one and all these uh invalid operations so basically ER when we compute when we let's say when we group these transactions in a batch what we do is we generate a proof of the validity of such instuctions okay and the layer one is called called like the validity layer because this proof is verif verified on a smart contract on layer one okay so user send transactions to Layer Two and the proof gets verified on layer one thank you okay going a little bit more in the details what actually happens when a

user send a transactions to L2 is that as as you might as you might know ER transactions can be expressed as a set of op codes of ebm up codes okay and what we do well the first the first option that we had is we callate a proof of the we could generate directly a proof of the validity of these up codes of the evm op codes but as you might as you might know H the ebm was not designed to be GK friendly okay which means that the set of O codes in the evbm are not that easy to prove okay so the idea was to design our our set of op codes okay this is what we call the ZK op codes okay and in fact when we get

the set of op codes of a transaction we transpile this set of O codes to our own set of O codes okay and then we basically prove or gener proof of this let's say that the equivalent program with with our own set of V codes instead of the original one okay so basically the zbm gets fed as an input the list of tailor made op codes that we have then we have the evbm program okay basically we enforced that the zbm only can let's say follow the evm program and not any other program and then we gener a proof that not only

that the the single GK up covs of every transaction are correct but also that they follow the correct logic okay theoretically speaking ER the the ebm program is hardcoded in the gkbm okay which means that theoretically you could substitute this program with any other program okay and convert the zbm to a zvm okay so you can extract the ethereum from the question okay ER so going even deeper into the details ER the design of the zbm is not a is not like a super complex and and

and a super complex uh processor but we SED to The Divide so we decided to do like the divide and Cur option and we divided the logic into multiple components okay so for example we have the evm has up codes of let's say of very very different flavor for example we have Artic operations there are binary operations there are me memory operations okay and what we did was to design er a specific co-processors for each ER let's say set of common O cods Okay so for example as you can see the in the in the image we have a processor that deals with arithmetic op codes we

have another one H that is with binary or course for example we have a very specific one that H proves the validity of sha 256 ER upcodes in the in the evm for example when you verify the [Music] um transactions okay and then we also have the memory we have the program and we have the idea was to design it in a very in a in a very modular manner in the sense thatting a proof or better say artize the problem of proving the validity of a of a evbm will been like super easy okay so uh yeah these are the two B that we have okay we are as I said

before we are going to be focusing on explaining how we have implemented our verifier okay and the idea ER does not deals with ER the proving to ex that we have but the idea of the bounty is to be able H to reimplement our verifier ER not as we are going to be explaining not how how we have done it which is what we are going to be explaining right now but the idea is to implement a new processor okay so it's like adding a new processor to the previous diagram that specifically computes the verification part verification part of our circuit okay we are very curious about the numbers that we could get by doing it directly as

compared to how we have done it okay that's right yeah yeah H so what is estar H so for those familiars with h St this challenge will be I will say quite a straightforward okay because estar is the name for our proving system so basically what you have to do is to implement the verifier of this proving the proving system and the E that it's extra in the star name it's basically a let's say that we that's let's say that what we have done is adding a new set of arguments to the start proving system okay so basically

if you're able to understand what is a stark so you for will be able to understand what is fry it should be easy or more less easy to implement the verifier within our tool stack so I'm going to jump and I will try to explain first how we verif currently verify the Starks and then what's our proposal that could be another way way to implement it that might be more efficient so uh um basically we use two two languages one's thcom the other one's spill both of us are inhouse languages uh is probably more extended because it's been in the

web space since 2018 or so uh pill is more new uh this is um just a small spoiler we are working on a much uh bet second version of the language but this is not the topic of uh this talk so what we do right now uh um we the idea is that we use recursion in ourm so we can prove in multiple batches uh with a single proof that's then sandon chain and to do that we need to be able to verify Starks so we can then aggregate them together so the way we do it is we originally uh wrote a St verifier in circum which uh then we will show you we

will do a bit of live through through the code and we can show you where you can find it but um that will come later and so and we we implemented in ccum and we what we saw is that it was um a bit expensive so the number of constraints of that verifier was uh too was way too much so we didn't fulfill our our purpose because it was too expensive to then Agate and it it wasn't worth it so what we came up with is we okay so let's let's use custom Gates because then we know that there's some parts of the verifier that uh can that are repetitive of the or that can we can be um split in a separate in a separate uh in a separate part we can verify it

apart um but the problem is that uh circum allows you to write custom Gates but you cannot verify it because uh as you probably know custom gate um we can um we can do the comp with can do the computation but we cannot prove that uh the the correctness of that of the of the of the code you're writing so we needed to find a way okay it's it's fine because with custom gr we can um we can reduce a lot the number of constraints of the verifier itself but then we need to because for example we have a poson custom grade which basically means that we simply have the input of the poson and the output of the of the poson but

then then we will need to verify that that poson was uh properly calculated and then okay it was okay so now we have um we add custom rates the numbers look much much better but now we need to find a way to to um prove it and so what we did is we went through a bit of a long path but uh taking advantage of of of peill that basically our zbm was right in inel we said okay so we if we can transpile that circum to to peel we will be able to generate to

validate the correctness of of verify the correctness of those constraint of of those custom gates in pill so basically what we do is we we have we had the stb fire we add the custom Gates and now that that we have this we can uh transpile that that r1c the R1 CS of the circum circuit um to pill and then in pill we can write the um we can we're going to write the verification of those custom Gates but as you can see we're doing like a quite a long path cuz we're we are going from circum to peel and then we will go back to circum when we verify the next star and what we started thinking is okay so maybe this is not

necessary all maybe we can with pel itself we can write the whole verifier and in the same modular way ector was explaining that in this game we have like SE separate components we can split uh the verification like in in some different models that we will see right I think in the next slide but I'm not sure about that yeah so uh on the right side you can see like zbm we have like the arithmetic the binary the padding uh several different um uh models so we thought okay we we we can probably do the same with the verifier but with uh different ones like for example fry can be a a mole um the fft uh the evaluation

Pon there's like many pieces that you can start breaking the verifier down into these small pieces and and create small processors that then make they can add all together and forier but as you can see like there for example fry is like you could have a a co-processor that ver that verifies fry that's completely independent it it serves for a purpose but all are like small pieces that they will all addap together and you can move on so I think that that's the idea that hopefully it's more or less clear that what and the motivation I hope it's clear like why what the way we're doing it and what

we're proposing that would be a cool alternative because also you would be diving into peel that's our language and I think that the best way to for for us for to get introduced to that we will show you an example and we will do a bit of a walk through through a code yeah if you scan the QR code it will guide you to a gab repo where we place the example and this is what we are going to be explaining right now okay the idea basically show show showcase the our tool stack what what you'll need to build the St verifier uh at least to give you a sense of how we have done it forvm okay so we have divided we typically

divide the the when we have to Define an arithmetization between two repos in the components repo you will have the logic not only for the armatization of each component but also the executor of each component okay basically the executor is the logic that fill ups the exe execution tra for this particular component and then in the source code you will have you will find all all the logic let's say gluing all the components all together generating the entire computational trace and generating the proof ver verifying the proof generating the recursive part and so on and so forth okay so let's start with the

basics okay so er the idea of this example is a very very basic chip okay it's a chip that uh only performs a particular operation okay so we will see like the main logic of the Chip And then we will see how this let's say when the chip has to perform this particular operation it will tell the other component or it will ask the other component to perform and to verify this particular oper operation okay it's like a I will say it's like a enhanced version of a fibon a typical traditional fibak example okay so in the in in in in the

components uh for each folder in the components you will have like the aration logic and executor okay the aromatization is written in in P have to make it bigger so if you're familiar with fibon I mean you can see here like the first part of the of the main you're simply verifying a fibon a Fibonacci Sequence where basically we can go a bit more detail if you want uh but probably you you've seen this if you've played around like it's the basically hello world of uh of zkb of

gkbm yes okay so uh basically what we we what we do here is to define the let's say like like the design of the computational tra we have the col we have the public input of the funaki sequence and we have some set of constraints checking that the public inut are being introduced correctly to the computational trace and then when we have to ER let's say that when we have to perform the particular operation okay which is not a still speaking fibak Edition with the syntax what we are doing here is we are um sending let's say this operation uh to be to be checked for the other component which is what we call the

model component okay so this is a very very simple logic and then in the module component in its arithmetization we have the actual check that the that this particular operation is being done correctly okay so basically what we are doing here is a modular division okay so basically we check that the question and the reminder computed are are done correctly okay so then in the well I'm sorry because we have done it we have done it h we have done it everything in JavaScript okay just for being as fast as possible but here you have the logic filling up the the particular

computational trace for this component okay so for example here we are Computing the equation or the reminder for each of the inputs that are being received by the main component okay and otherwise we fill the TR with do values so that the constraints are being satisfied okay this is for the model component we have the very same logic for the main component and then so basically like just to summar to summarize it so we have like if you see like components folder so we have we have a appeal file and then we have the corresponding

executor which basically uh when we there's the pill file that is the one we've just shown you and then when we write the executors if I can go back one second to that there's the um you can build the constants on one side and and and the committed polinomial on the other side but that's the only thing you need to do to be able to generate a proof so once you write have written the uh p p file and the and its executors everything else there there's a straight uh you can run a set of of command lines we will show you we will show you now uh what what those commments are and you can generate a proove and verify it and so probably

easiest way can I yeah I will I will show it I don't want to to bore you a lot because if I start like coding you will as said before by R you will go to Twitter that's what I usually do so let let me open if not if not that's fine I will cool so then I'm going to open the packages I'm sorry that's in JavaScript because usually for that that's what we you we use for uh to speed up development it's you can do any we have our production code is in C++ and moving to rest but usually we find JavaScript that's easier

because it's less trick language it's probably not as good but it's speed the development process so if I open the package this one and let me close this you can see here there's like a bunch of uh comments but basically the one I'm going to focus is in test main as you can see there's uh a set a set of uh commment you need to run in order that that will generate the proof so if I go briefly through it firstly we generate the We Run The executors so so we generate a Comm file and a con files and once we have that you also you will need to define a St stru I'm assuming

that you all more or less familiar with how star Works basically star conru is a config a very simple conf config file that defines some B that need in order to generate the Stark proof in our case we basically have the number of bits the extens how the how the extension uh and the fry steps and the number of queries for the for verifying fry and basically that's it you just need to write the pills write the executors and then you just run in this case test main but you can see the commands are the same you just simp you simply have to change files if you have if you are pointing to different

directories but you can generate a proof out of the box so I I will run it and I can show you the logs that [Music] and also like in fact all of this as you can see generating approv it's verifying verification succeeded and and a circum was generated in fact that's not even necessary cuz what we if if we check the logs you will see that there's the third uh option the the Third command line let me see if I find it here there's pill verify so basically

we have a we have a a program that uh given a appeal and a commit file and a constant file we can automatically check if if the pill if if the file if theit files U fulfill the the the constraints so if in this case we can see if it Su if this succeeds you can you can also generate the proof but that should not be needed because it would it would be uh generated it should succeed so it's you just need to see that the verification succeeded in order to know that the proof will be valid and in this repo we've also added uh our

current um verifier like you can see here in sources or wait okay there's a circum example and this is what I was explaining before we have um the main main circum let me close this which you can go through it it's a bunch of code but at the end uh there's like separate components like for example all this part is basically generating the transcript where generating the trans the transcript for the Stark uh there's another function that what does is verify verify the

fry and so there's like five or six main components and what I said before that right now and that's why we are encouraging you to like try to rewrite it in pill is that there's like some um custom Gates and that's why we need to generate the P the pill that for example here you will see that in this case we have that's that's a poson is a bit more trick so let me find an easier [Music] one this one for example so basically every time we we the verifier operates in the extend in the extended field we simply say that there's a custom gate

there so we will just um circum will not verify anything we'll just store the input of the the two values that you are you multiplying and the output and then we will send that to we will pass the to peill and you can see here that from line 637 to like 654 basically what we're doing is we are impaled the we are write we are writing how an multiplication in the extended field will look like and we are checking that that that given the two inputs and that we do the operation and we check that this matches with the output that circum said that okay I've not I've not checked it but this should be the

correct one so if if you can check that if if you do it on circum maybe there's like a thousand constraints and here just a simple check that this will that that the constraint fulfills which is much cheaper and at just one row and I think that's pretty much it if we will be around for the whole for the whole day probably feel free to ask any questions if you want to know more if you are if you have questions about about the about pill about about zbm about about the if you maybe interested in recr about what we're doing we're here to try yeah sure what do you think

the hardest part of this is yeah yeah look to you yeah Look to You H for sure we are not asking you to let's say artize all the all the part in this uh in this part with the custom Gates but instead what we are asking to you is to translate some of the parts in the logic of this U main verifier from ccum to pill okay and I would say that the hardest part is the fly logic part okay assuming I mean assuming that you do not know how fry works you will need to do an extra work trying to understand the

protocol but if you do actually know the fry protocol it must be quite forward and we're not expecting like to have a full verifier that but we want you we want you to play with peel and maybe start with a small bar fry I think it's a nice one like it's quite as itself it's quite complete but you can just it would be perfectly fine if you just have time to do like a some sub component just for you to encourage you to play with peel play around see our tool set and I mean if if you have the full verifier that would be awesome but probably 36 hours you have you'll have to sleep so that's it answer your question more

or less yeah cool any other questions uh you you aut to generate the you autogen C com script from from P or not yes okay that's I can so we have also put it here but uh I can show it to you more more in in detail if you want if you want to see exactly how all the pieces that we are using to generate that we can go through it but in here you will you will see that there's a second there's basically the first part is the test main B we give an appeal we generate uh approve

and verify it and then you can see that there's two comments here that that generate the circum and it compiles the circum this was the first step I was mentioning before we are generating a start verifier with custom Gades and get the R1 Cs and then there's this uh second part Test Pro verifier pill which it calls verifier setup and verifier exit which which if you uh take a look at it it will go through pillar which is the other Ripple that we have not uh PL here but is where there all the logic that's undergo that's uh happening is and you you will if you

follow the script you will find where exactly the the pill is is compiled and everything but I can help you through that so uh R1 CS basically is grass 16 basically right plank oh plank okay cuz we we needed to convert uh back to peill and it was um I mean I can we do with yeah yeah we do a transpilation from the a13 description of the three circuit to the let's say to a PL description which is quite a St forward because the pl description is like a subset of the A1 cs1 I can but so you have a stark verifier you turn it into a plank circuit and then you run a

verifier and it in Ser in what is the motivation and then you said pill itself can verify as so are you if you're familiar with plun yeah so here you can see that uh this uh Lin 59 we are basically uh proving uh PL constraint and so the is we have this direct direct conversion from circum to to pill but the motivation comes from that with circom we added custom Gates which then we are not checking the constraints inside the custom Gates we just doing the computation so as I was

explaining before for the extended multiplication or for a posidon for example we circum would just be saying so here's uh the input that I'm sending to Poseidon and here's the output so then we need to verify that those inputs are well connected with the posidon and that's that this is where pill comes into play because what we did is we converted the we trans transpiled uh the plun um r1c plun constraints which is straightforward and okay so now we have to prove that all the custom GES that you've added are correct and here for example that's what I was showing you before here you can see there's posidon gate which basically as I I was saying

it proves that a Poseidon is um properly executed or the extended multiplication but this was um this is the extend the extended multiplication so this was way cheaper rather than uh letting um that that writing straightforward in in circum so you are doing some kind of a recursive a snark basically or Stark you go a stark to snark and then you come back to peel no it's it's not it's not an a star because we are not we are not in fact generating a proof of the ccom it's more about expressiveness so we we we we encountered that it was at the

beginning it was much easier to space everything with ccom with R1 CS because the logic of the ver verifier is not U let's say is not as as a structure of the as the proving part okay so we have the circum description but we do not generate a proof of the circum description we we transpile the set of constraints to appeal description and then what we do is we generate a stark of the appeal description okay which is a if it's well done for sure it's theoretically equivalent to the1 cs1 okay so we never do like this transformation between a sar or a star we use compute Starks IOD thank you and then this goes to recur to the recursion and if you're interested

we can we can show you how this connects with our recursive systems and how we aggregate different proofs together but that's the main component thank you any other questions okay so then uh Brian will talk about blun the blun 3 track uh my name is Brian uh I'm the senior D engineer at polygon sorry my voice sounds a little bit you know it's because I got a really bad flu uh so I'm trying to protect Everyone by wearing a mask so but don't be afraid come talk to me if you have questions I'm super

welcoming I'm just hiding my smile under the mask all right uh so I'll just quickly go uh let's take a look at this page where this bounty is uh so we have three links uh first is the planky 3 repo itself so if you wanted to go through planky 3 repo uh you can do so and then the second link is what we're going to be going through during this 30 minute session it's a simple Fibonacci implementation in planky 3 framework uh or toolkit and the third one is more advanced version of of an example using plony 3 so it's basically a Kat implementation in uh

using planky 3 so being able to generate a proof that you executed this Kat hash correctly or not so sha three all right so this will be the repo that we we're going through today so if you don't have the link you can scan this QR code right now I'll just put it up here for a moment oops uh all right so in this sort of 30 minute session what we're going to be covering is what is plony 3 and how does it work in a brief session I'm not going

to dive too deep and I don't even thing I can't explain it too well if we dive too deep so just on the surface level understand what this is for why did we even build this and what kind of solving that we're a problem we're solving uh and then we're going to go through a step-by-step process of how to write your own air scripts and from there how do you build out the pipeline of a zkp system fast using plony 3 and at last we'll run it and then see if it works or not all right so what is plony 3 and how does it work first let's understand plony 3 plony 3 is basically a toolkit that helps you create ZK system with these um it's

basically a really performant uh piop uh system but it's also very different from some of the others where they have a very fixed design as in if you use their Tool St if you use their toolkit you're basically stuck with one field or one particular hash function but in planky 3 it's composable as in uh we provide the option for you to choose the kind uh the kind of field that you want it's out of five which we have a list at the at the very bottom of this page or and then also you can also choose your own I guess like hash functions that fits your program's needs and depending on the configuration your program and your program Logic the

performance might vary and it's super super easy to test out as in uh once you finish writing your air scripts all you need to do to test out different fields or test out different hash functions is just changing one or two lines of code so we abstract away a lot of the complexity when it comes to developing your own zkp systems all right so if we map it into a some the product that we we are all familiar with let's say pytorch or tensor flow it has been out there for the longest time and we were able to build a lot of amazing models on top of it so that's sort of where py 3 is plony 3 is sort of that you know

tensor flow or pie torch that of a position uh but for zkp system and you can use plony 3 to abstract away the you know prover or verifier I guess like implementation process it's just one or two lines of code to implement uh all you need to do is just focus on your app application and focus on your creativity and of course on top of that you can make all kinds of combinations to build a complex ZK system such as ZK VMS like the one from suake lab sp1 or you know valita is also a really good example uh whereas simple or you can also build a very simple one circuit uh

sort of a a zkp application like this one and I'm showing a Fibonacci sequence so now that we kind of understand where the position is for plony 3 is basically what you use to build your own zkp system fast and how does it work right and what is the input that requires from users perspective or developers perspective uh so first thing uh this is up to us as design uh developer who are using planky 3 to develop you need to be able to know what your program is the your application or whatever Pro uh computation logic is and you need to implement that in air air scripts so air

is sort of a constraint system or I guess like a like a framework or logic that is that is UN parallel to R1 CS um you might be familiar with R1 CS uh air is a little bit less structured um more freedom um uh which we're going to go through in a bit and to work with a air you need to be able to generate a execution trace of your program and then on top of that you define your air uh sort of constraints or relations of different elements in your uh execution tra and I'll say from developers perspective these two are these two steps are one of the main

steps that you will have to focus spend most time in and remaining is all configuration we're we'll still go true um but you don't have to 100% understand if you're not from the really cryptography background so first you need to decide on the finite field that you're going to work with it could be uh it could be baby bear it could be Goldilocks uh it could be menai uh meren 3 31 and more and on top of that uh you need to decide on some of your your data structure basically um you can just understand it that way um and also decide on your uh based on the field

there are different uh polinomial commitment scheme that works best with the field uh we have templates for it which you don't have to memorize you can just kind of reference it and copy paste it over to your projects um and also you know defining your fast for your transformation I guess matrixes um those also comes with the template and configure your fry configs um those are I think I think ha kind of cover a little bit up sorry I I think Roger kind of covered a little bit it's just if you don't know fry maybe you can just go with a template uh it's just some some of the uh some of the elements that you need to to configure uh as in like how

many numbers of queries uh stuff like that uh and also we need to create this Challenger sequence because uh we have a Challen we have a pro proof generator and then we also have a verifier both will need a sequence of challenges so we'll be using will create a same sequence of challenges uh to implement this FIA Shamir and then of course with all of these pres setups that we have done we have we use another one line to Define okay this is our star and then we will use it to generate proof uh we also have a verifier uh that will you know take the inputs uh take the proof and the

input State and the final State and also the challenge sequence to verify whether if it's correct or not all right we're we'll go through all all of these in the code example so don't panic uh but this is just a general run through of how plony 3 works so this modular design really allows you know easy customizations and optimizations for different components whereas you can you know in a lot of these examples you can just swap this three this is just one line of definition you can just swap it with another type of field and then it will still work the whole system and it it makes developer really easy to test out okay what kind of field what kind of hashes works best for my air script that

I just defined all right um yeah this is my advice uh seems complicated but don't panic you don't have to understand all of it right let's un let's go through the Fibonacci AA example now now that we kind of understood what planky is plunky 3 is and how it works in a brief level so from developers perspective there are six steps that is required to build out your plony 3 uh sort of a pro ZK system first uh on the left side there are three major steps which they all mean uh they're all contributing to build your air scripts and then on the right side is where the plony three part

really shines is configure your ZK system using planky 3 uh and run it see if it works so first Define your program in our case will be Fibonacci right so we need to understand what is this computation and we need to find out what are some of the requirements of this computation uh so first we have we have three uh I can think of three requirements and if you have more feel free to create a PR and then I'll add on top of this uh so first every Fibonacci Program start with zero and one right so that's like a initial State uh sort of a sort of constraint or or requirements

that we need and then the second constraint is you know on each iteration um the current Uh current two inputs um when they transition into next state as in like next iteration the second element of the current two inputs will go to the first element of the second iteration and then the sum of the current iterations uh will become the second element of the next iteration it's a little bit if I describe it in words it's a little bit whining I should have drawn a graph uh but but it's basically you know a b c d where B is equal to C right and then a

plus b is equal to D and that sort of a sort of a logic and then the third requirement it's also now we're going to iterate end times of this FCI sequence then we should expect a very definite result that should match should be the exact result of you know after running end times a Fibonacci Sequence uh for instance if it's three times then our result should be should be two right so now that we understood our programs and some of the requirements how do we translate that into air constraints uh so there are a couple of tips to be

mindful of uh when describing air scripts we uh there are four things to be taken note of first is Define a valid State transitions from current state to the next state and AKA uh what are the constraints when transitioning from current role to the second role um this is how we are defining it of course there are different ways of defining the structure for for for air for for for air scripts like you don't even have to make it into a matrix you could just make it into a complete one onedimensional vector and then access every Elements by bits um this will

complicate a lot of the topics and for now what we're working with is every step every iteration means a rle and how many roles it has in this Matrix means how many computation or how many iteration it has done in this Matrix so just picture that Matrix in your head right now and this valid State transition means from one role to another role what is the relations of each element uh from the previous role to the second role so that's first second thing to be mindful of is inside this current role this this current role I don't care about all the adjacent role just my role uh is there

any relationships or is there any constraints I should be mindful of for instance um in this one in this role uh let's say in this current Matrix uh program uh there's only one element that I need to be mindful of and I just need to check whether this element is zero or one then I can do something like you know uh putting up the constraint l x * x - one equals z to to make sure that X is only equal to zero or one like a bullying result uh but of course we have in our library we have to assert bull to check it uh so just be mindful of those in our Fibonacci program we don't have this

requirement but and then the third will be you know check your initial State when the program begins do it has a very specific initial inputs or state that it should start with and at the end do you expect a very definite result uh that you need to to double check with so these are the four things to be mindful of when you're writing your air scripts um regardless I think this is getting a little bit more a little bit too abstract now so let's just dive straight into the code uh if you want to read more details I have written these so yeah please take your time and read it and then if you have any questions I'll be at the booth uh waiting for you

to ask me questions right so in actual code how do you write your air circuits and what is it that we're trying to achieve right uh so first um how this air circuit or air constraint it exists in plony 3 this sort of a library in a format of a struct a rust stru and in this case what we need to Define is first uh Struck it could be empty if you don't have any inputs uh but in our case we need to have inputs what are the inputs first we need to Define how many steps are we going to iterate as in like for this Fibonacci Sequence do I need to

run it three times four times eight times to get the result I want and after eight times what is that result I also need to check uh if the program if the if this air circuit has calculated correctly so I also need to give them my expected final value result to check it at last so these are the two inputs that I have to find to feed into this plunky uh uh this air scripts and then I'll Implement some traits right first uh first trait is uh since we're working with the Matrix and in this very specific example I've have decided to make my Matrix uh two element

uh per roll sort of a matrix because per iteration I only need to check the the the the inputs the two inputs right whether at the beginning it say does it start with zero and one and then in the next state is it like one one where it has a a valid transition from the first iteration to the second iteration so stuff like those and I I only need two elements in this case per iteration so I set the The Matrix width as two and depending on your program this Matrix width can be much wider it can just be one um it's all it's pretty flexible and now that I have defined

width of the Matrix uh let's define our constraints right so the way we do this is sort of adding this sort of uh this eval function uh for for our for for our air uh air struct it's sort of like in AI where you have this learning rate sort of a uh like after after you train the model or calculate it you you do this sort of a critical uh I maybe I'm nervous I kind of forgot that term uh but it's like at at last you you kind of double check it right sort of evaluate it um it's sort of similar it's what it does is a from one state to transition

to another state or from one one iteration transition into another iteration is going to call this EV Val function and it's going to check inside uh check the conditions inside this and first let's take a look at what what I what I designed for this so uh this main is sort of uh the the variable that you use to access the current Matrix uh iteration uh as in and then by using this roll slice um zero index you can get the current iteration rle and by adding one index you can get the next one um so how does it know that the width is uh I'm I'm getting exactly

two elements per row slice uh because we defined it here in the width so I have defined it as two so per row slice I'm going to get two elements and I'm checking three conditions basically first is it's going to to check hey is this the very first role that we're going through so this function will only be uh we only be access uh when it's when it's reading the very first rle of this Matrix and it's going to check the very first element is it equal to zero so if it's not obviously it's going to fail um and also the second element for of the first row is going to check

if the value is equal to one and you might be questioning like why is it so complicated like AB expression zero why not just zero because we're playing with Fields here they're not like numbers number they're actually you have to access the field version of the zero number so that's why you have to use this sort of a format to access it and same with the one and so that means this will only be accessed one time at the very at the beginning of the The Matrix access uh and this will probably access every single iteration is when transitioning when transitioning from from this row to the next row all right

I'm going to check uh whether the the first uh first element of the next rle is it the same with the current R's second number because we're passing it right uh and the sum of the current R uh is it equal to the second element of the next row this is basic Fibonacci logic and at last um we're going to check uh this final value self. final value is the input that I passed in uh when I when I create this uh airor constraints so it's not calculated by the air circuits but I calculate externally but I pass in as for verification

purpose and then this final value will also be converted into a field expression in this line and then I'll compare if the final final result is the same as what we expect if it passes it will pass all right so now we have sort of completed two steps we have completed the we understood our program and then we have defined our air constraints now it's time to figure out the execution traits that our airor constraint will be applied to so execution traits is if you don't know this term uh but I think majority of you might know already

uh but it's basically uh the the footprint of your program's calculation uh for instance like if you define some sort of a I guess like a like a recursion algorithm when you write in code it would just be like one function right and then it doesn't matter how many times you call it it just like one the code only appears one in your code because you're calling it uh in the runtime uh for x amount of time uh but in the execution Trace if you call that recursion function five times then that part of the code will will appear five times so stuff like that is is literally the footprints of every single clock

counts or program counts um and it keeps tracks of the program States the the the necessary state that is needed um for uh for for I guess your application and in our case for phib Nici number it basically what we're keep tracking of is the two input numbers in every single iteration and we just need to define the program that that keep tracks of it so what it does so first um I need to create a a onedimensional vector uh that keep tracks of all the states and it the size is basically numbers of steps

because that's that's predefined and times two because every step has two elements um and then we just do a for Loop you know uh we Define the initial State AB which is 0o and one and then we do a for Loop uh and then keep on pushing the the current state of the Fibonacci uh calculation into this vector and at last once we fit feed in all of these because our because our air constraints work with the 2v ve 2D Vector uh uh sorry 2D Matrix we'll use this Ro major M Matrix this is this comes with uh the plunky 3 Library there's like sparse Matrix

there's other types of Matrix that you can look into depending on your program's needs uh but we'll just convert it into a 2d uh R Matrix where we can access the program by roll in the the air constraints all right so the these are the complicated part that is sort of done um the build your air circuit uh scripts I explained it a lot but honestly if you're implementing it you'll find it's quite easy maybe there are a lot of edge cases that you need to spend some time to figure out but once you figure it out you just have to implement it that's it um excuse me and now let's configure your zik system and just run it right um

I'm not going to go too deep deep because there are tons of examples that you can just look into but the major part is here step four choose your field and hash functions we currently support multiple fields and multiple hash functions uh and how you define it it's basically you know just this is a template you can do how whatever kind of format you want uh but this should help you debug a lot a lot smoother um so we first need to Define the the the value type the the values field and then on top of that we also need to extend the value because you know this value is you know men uh meren is 31 bit and if we want to create

a challenge on top of it uh we'll have to extend this a bit because 31 bit you know it's it it might be Pro forceable right so we'll extend it uh to a to the level where you know it's a little bit uh more challenging to to to to brute source and it's safer basically um uh and also we'll we'll choose our hash functions and in this case we're choosing uh Kat 256 hash um uh and then and then for the hash functions because it it it is just a hash functions we also need to to to to create a serializer that take reads the field elements to uh to feed into the

hash functions so we also need a fuel hash and and we'll just Define instance of those um so this is just a process of it and if you want to take a look at what are some of the other fields and hash functions that we support I also kind of list it at the very bottom so more complicated example there are also various configurations you can explore in plony 3 currently we support Goldilocks uh baby bear koala bear I don't know what's up with all the bear but and meren 31 and then BN 254 and hashes we support Poseidon Poseidon 2 rescue monolith Kat uh Blake 3 uh shotu uh and I think there are more

coming along so stay tuned on that regardless um so that's about it for choosing the the field and your hashes and once those are done now we just need to write your ZK system setup it's very I would say it's I would say like if I go through all of these um we can definitely do it but it's not that necessary because it's just the configuration you need for create the start prover and in the process you need a compressor that compresses the hash results to to keep the I guess the result more clean more structure in a fixed size um and then you also need a

Merkel tree uh that is requireed for for I guess like uh the the the challenges uh in in the fry protocol uh and also you need uh you need to you need to you need an extended version of the Merkel tree as well um and also you need uh the the Challenger and all of these will be feed into this fry config uh with some of these configurations that you can play around with normally I would just recommend go go along with the configuration um and then for a polinomial commitment scheme um the one that we're showing in this example we're using Circle PCS there are other uh PCS that we also

support uh depending on the field uh I guess like you can choose whatever fits the best for uh meren 31 uh Circle PCS works really fast so that's why this example is showing this and yeah basically all of the above steps are used to to configure this piece Cs and they will be fed into start config to to finally finish this configuration of uh of the Stark and you can now start using it um there are more examples of this I'll show in a bit uh but let's just quickly go to the Run Part where now that we have the start proof uh start Pro sort of configured is

ready to go what do we do right we have the air Scripts uh we have the execution Trace generator uh we also have the whatam call uh the the the start prover and we just have to use them right so first um let's define our inputs uh we are going to in this case we're going to run eight times for the Fibonacci sequence and the final value that we see is 21 uh if you try to Google it the the the end result of you know eight iterations of Fibonacci is 21 and then this is we're instantiating the air scripts in this case by giving the giving uh these two inputs that we just

defined in this struct uh and we'll get our air scripts and also we need our execution Trace which will just plug the number of steps in and it will be able to generate this trace for us and these two are sufficient enough for for us to generate our proof and of course we're we're doing fiir right because we want we don't want to have ping and pong sequence all the time uh we just want to create the same sequence for both prover and verifier um at once uh so we're doing exactly that here's the Challenger and here's the exact same Challenger that we're defined and one of them will be passed over to

the proof function one of them will be passed over to the verifier function and for the proof function um this config is the start config we're passing this in and this is the air script that we just wrote and Challenger is basically the challenge sequence and Trace is the execution trace and here we're throwing it this empty I kind of forgot what this was uh yeah I'll take a look um but yeah we need this empty Vector I I think it was something similar to the C challenge can't remember exactly uh but then yeah all of these will be used to generate a proof it's just one line of code you have your proof system

um runnable and then you just generated your proof and same thing for the verification process same same confli same err same challenges same uh but the proof that you generated in previous step uh and you throw in it's going to check whether if the verification works or not and the final result should work some something like this you just hit if you get clone this website uh sorry get clone this repo and then do cargo run this is sort of the the the result that you're going to get um maybe I can quickly show right cargo run it's Ultra fast or maybe it's

because it's Fibonacci um but it's fast enough definitely so now we're closing to the end of oh we're getting to the end of this Workshop uh I'll just quickly show another I'll just show right here oh this is another sort of an example of how to access your execution Trace so the execution Trace example that I gave you guys is more of a I guess like picturable uh using a matrix format where each row represents um a current uh each duration right but there's also another way where if you look at this

format it's basically access accessing the states by bits uh so all the uh in in this example all the all the execution traits is in one one entire One D vector and then you're just sort of accessing uh via VIA uh subscripts um but there are a lot of other ways that you you can do it's pretty creative uh it's it's it's just this this is the the logic behind air is it doesn't have a very strict rule on these but it only has just sort of design thinking so you you just need to apply that to your program itself and last but not

least if you take a look at this uh if you go to plony 3 and then plony 3 plony 3 organization plunky 3 repo and then go to KitKat hyphen air folder this is the air implementation of KitKat so basically we have implemented a katat hash function in air scripts uh if you don't know how kitat works you should take a look at it before you start reading uh this repo because it's it will get really complicated and once you're in uh there's two folders there's example folders and Source folder Source folder

is where we have Define uh the air scripts of this C cat um you know this is the main function the the air. RS and then it it calls all the other functions from from these other re uh other other F uh other files so and then with that air fun air scripts defined we have showcased all kinds of examples of the different combinations of different fields and different hash to to calculate the air uh the the Kat hash function uh Kat air scripts and if you look into each files they look quite similar to one another because like I just said you know to

test out different fields or test out different hashes it's just changes of one or two lines and it's that simple so yeah I'll say that's about it um honestly this is actually my very first time presenting plony 3 in front of everyone hopefully it was clear um but if you have any questions you know I'll be at the sponsor Booth wearing my mask so it should be recognizable uh my name is Brian so yeah just come to me anytime but if I have time I can still pick up some questions now or no I think I think we're going to wrap up all right cool all right thank you so much thanks Brian thank you very much