ZK HACK mini - Writing STARK proofs with Winterfell

Transcript

thank you so much anna hello everyone really happy to uh to present this in front of everyone and seems like it turned out is really awesome so um really happy to do this and if any questions come up during the session feel free to post them in the chat i'll try to answer them as soon as i see them um but yeah if anything is unclear do let me know all right so this session is about winterfell winterfell is a stark groover and very fire and we'll get into that but in terms of the overall outline um i want to give a very quick introduction to starks just to describe what they are how they compare to other

systems other proving systems then this is not going to be like a deep dive interest parks just a very high level overview and then we're going to do an overview of winterfell and what the library is and some uh key features and things like that uh and then uh we're gonna build a postmodern vgf uh this is gonna be kind of like uh actual coding exercise where i will in real time uh code up uh quantum media fusing winterfell and then if we have some time um we'll also do another example a similar like walkthrough to demonstrate other features of winterfell using fibonacci but you know fibonacci example but we'll see if we can get there

all right so uh i'm sure a lot of people here are probably familiar with this setting so when we talk about geo knowledge proofs and proofs of computational integrity in general um there is all usually approver and identifier and you know they have some common function and they have you know some input some of which could be private which is called a witness and they have some outputs for this function and then the goal of the approver is to convince the verifier that you know they've executed this function with this inputs and got the desired output but the way they want to do this is first of all they don't want to send the witness to the va fireball they also don't want the verifier to have to run the function in its entirety so they do this by

sending this proof and this is the zero knowledge proof and the properties that we want to have with this is that um we want uh the prover to run in uh kind of quasi-linear time we want the verification to be as efficient as possible you know ideally in constant time but logarithmic time is okay some systems have actual linear time uh we'll talk about this a bit later but ideally it would be at least logarithmic or it must look at me and then we want the proof size to be fairly small and this is all of this is in the size of the computation so the idea is that we can run this computation for maybe days or hours or whatever and then the very fire can make sure that the computation was run correctly in milliseconds checking a fairly small proof um and the exciting

thing for me is at least is that this f function that could be initial complete computations and obviously some computations are more amenable to being efficient within zero-knowledge proofs but in theory at least it could be any uh during the computation and actually in practice it could be any training complete computation you know again with some caveats um zero knowledge proves really exploded over the last few years i'm gonna i mean kind of the beginnings were laid in in in the 80s but really from practical standpoint they've become useful maybe in the last five years or so maybe a bit more so um this is just like a sampling of

different proof systems and when they appeared and you know there is a lot uh here and even more that i'm not listing here um but one of the things that i want to point out is that proving systems all have very different properties and there are a few properties that we well there are all the properties that we care about that the few that i want to highlight here one of these properties in transparency meaning we don't need a trusted setup for the proving system to work the other is the sync verifier so on the previous slide i i said that verification time could some proving systems could be linear and ideally we want to avoid linear systems so if our verification time is logarithmic or constant

uh then we call this system to have succinct verifier and then another property is postpartum security meaning um you know you uh even if elliptical cryptography breaks down we the system should still remain uh secure so this is kind of like highlighting which systems fall where um this winterfell is a start program verifier so i'm going to go a bit more deeply into the start system um but before going there uh just showing the table uh this kind of highlights some other properties and list different proving systems and kind of how they compare to each other there are a lot of

caveats to this table there are a lot of new ones uh uh so uh this is true most of the time but maybe in specific some specific settings this may not be true but i think the overarching point that i want to make by showing a table like this is that there is no ideal proving system there are proven systems that have uh small proofs uh but they require for example trusted setups there are systems that are transparent and fast but they have fairly large proofs and so forth so when i think about cooling systems i try to think about as i think about programming languages that you know there are some proving systems that are suitable for specific use cases but there is no kind of like over our

ideal programming language and there is no ideal proving system at least with the proving systems we haven't come up with one yet um all right um let's talk a bit more about stark starts and advantages um that they have as compared to some other systems so uh first advantage is they're transparent and scalable what this means is that there is no trusted setup and there is no pre-processing so in many other systems especially the ones that have very small proofs um you need to run trusted setup and trusted setups are attained they're fairly difficult sharky street and then you know you need to worry about whether they have been compromised or not we've gotten much better now i think

with running trusted setups so uh there are there there is less risk that something will go wrong but uh obviously no trusty setup is better than they even the best setup in my opinion at least um the other thing is that uh sparks use very limited cryptography and this means they only require you know from cryptographic standpoint the collision resistant hash function and that makes them post quantum secure because uh uh as far as we know at least quantum computers cannot break uh or at least we don't know how to break uh hash functions using quantum computers um one other uh benefit which is actually

very interesting is that they're fairly flexible like start proving system is very flexible and that it can work in many different fields um even something like as small as like let's say 32-bit field is possible and they have you can choose among very different trade-offs and you can do it dynamically so you can dynamically adjust the security level of a of a proof for example without changing you know circuit definitions or anything of that sort you can dynamically uh kind of change if you care about let's say proving as proof size versus improving time you can if you if you want small crews for example you can spend a bit more time generating those proofs and they will be

smaller but if you care about proving time you can uh maybe tell generate larger proofs uh and then your proving time will be smaller all of this kind of works within bounds you can go to extreme on any one of these dimensions but you do have these trade-offs where you can choose i think these trade-offs are fairly complicated result of other improving systems where for example once you've chosen the security level you can't easily reduce or increase it or you know it's not trivial to how you would get a you know smaller proof or reduce approving time by increasing the proof size or anything of that sort um starks that the other advantage of starks is in specific settings and we'll talk about them specifically when you you know computations are uniform

they're extremely performant and the verifier even in other settings is also extreme like very uh very fast for most practical proofs you only need you know single-digit milliseconds to verify those regardless of how long the computation was the prover is very fast as well um i've given some benchmarks for my mdm specifically so for example the single cpu core you can improve around uh uh 7 000 cycles of medium vm execution and the nice thing also is that proof generation is massively paralyzable meaning you can split it across multiple cores and

maybe use uh gpu fpga acceleration and all of that stuff and uh you know it is a tough engineering challenge to scale it beyond kind of like let's say what is available over the shelves but it is kind of not impossible to uh in theory around this in like in in thousands of parallel threads and massively juice proof generation time um as i mentioned there is no ideal proving system so there is uh there are some disadvantages that sparks have uh perhaps the most frequently assigned disadvantage is the proof size uh no matter what you do you're probably gonna end up with dozens of kilobytes were approved so even the simplest proof something like proving a pre-image of

rescue hash function is probably going to be somewhere around 16 kilobytes maybe you can get and get it down to like 12 kilobytes with you know flexing some parameters and on the upper side like executing one million cycles of might and vm you're probably gonna be around uh 80 kilobytes and then you know if you go beyond that you could go you know depending on what the computation is uh probably you know close like for for the largest computations that i've uh ran closer to 200 kilobytes and i think uh beyond that it's probably computations that are not very practical at this point in time so uh if you think about proof size it's probably somewhere between 15 and for most practical amputation 15 and like 120 kilobytes and maybe for some extremely large computations it could go up to 200

kilobytes um another kind of disadvantage is that uh you know so far uh at least there hasn't been recursive starts i think so and we'll talk about this a bit later but recursion is definitely possible with starks but it hasn't been yet demonstrated um and uh recursion is very important so there are i think many people working on building recursive starts right now so uh this will be solved but at least at this point in time there are other recursion systems out there but stocks haven't been made recursive yet and then um the other potentially complicating thing for starts is the energy ization air equitization is more difficult to work

with than other ones yes i'll go into this in the next slide or next couple of slides but basically uh it is not as straightforward to work with and you know especially build like standalone gadgets in air that can be integrated in other areas and so forth so that uh complicates and uh things that makes the learning curve for using starts much higher than in some other uh improving systems um all right i mentioned this arithmetization here so let's talk a little bit about about what it is so arithmetization is a kind of a step in building this proofs of computational integrity that takes a program that is written in some higher

level language and reduces it to a set of polynomial equations basically or other statements about polynomials and this this is true for most other improving systems as well or at least many other cooling systems but for star x this is a uh their recommendation is called air as i mentioned in the other slide for other proving systems a lot of other cruising systems it's called r1cs and this arithmetization step is something that you know not all the people kind of immediately know what it is but it is needed to build proof so let me take you through the a fairly simple example of uh um kind of eight meters uh advertising a

program so let's see let's say our program is something as simple as like this function that takes some input and a number of steps and then what it tries to do is just like with every um for every step it just cubes the previous state of the variable or whatever input it got and then adds four digits to it and then after a while it returns this variable uh r so basically if you think about you just initialize the variable to something and then uh for n steps you uh cube it and then sub constant to it um one of the things that we do in error rectification first is what we call what we call an execution trace an execution trace is basically just uh uh kind of a matrix but in this case it's going to

be just a single column but basically it's a it's something that records the state of a computation at every step of its execution so in this case uh our execution trace is going to be fairly simple we start with you know the initial value so x0 the initial state of our computation initialized to s and then with every step we take the previous value qubit and net 42 to it and then once we get to the end this is kind of our output and we do this for n steps once we have the execution trace and i would say kind of coming up with an execution trace for this computation is fairly straightforward but if you think about more complicated computations uh it becomes much less straightforward especially for something like a

program that is um you know very complicated and has a lot of like let's say branching logic lots of loops and things like that and we'll get to uh kind of like this uniformity of the program uh in a second and the the kind of taking it from execution trace to air is a set of polynomials that kind of like impose constraints over uh this execution trace so uh what it means is that this this equation should hold for all steps of the execution trace or at least the steps that are specified there so for example this relationship is something that is described describes like how you transition from

one row to the next this this equation describes what should be the first state and this equation describes what should be the last state and this basically is an entire kind of description of this simple computation uh so this is what we call air and error by the way i should have said earlier stands for algebraic intermediate representation so once we have air then we can start generating proofs but this is a crucial step and frequently again this is very non-trivial of how you reduce a program to its air representation uh and it's in many ways it is more art than science i would say at this point quiz um all right uh to compare so i mentioned r1c as it was used by many

other proving systems uh just to do a quick comparison uh with air and say why it is maybe a bit more difficult to work with air again so both of them work over finite fields i would say that air is well suited for uniform computations while r1cs is probably better suited for some construction computations although you can do either with you know you can attempt to do both with this with either one of these approaches you just for example trying to describe an unstructured computation with air is going to be very very inefficient um on the other hand uh trying to describe

a very structured computation with r1cs violet is possible to do that and you basically need to unroll loops uh and uh kind of represent within this circuit so it's possible but also probably not as efficient as doing it there so there are different types of computation the uniform computation again i mean something that uh you know you you have some uh kernel of a computation and you repeat it uh many times if you need to repeat it many times then the computation is uh kind of uniform and many times could be thousands of times or millions of times um one of the important things of uh or reasons why air working with air is difficult uh is difficult is because compassibility um is fairly complicated

basically because of this uniform structure by computation if you have two uniform computations it's not always trivial of how do you combine them together so that they still remain uniform with unstructured computation it's fairly easy you can connect the circuits in fairly trivially and you like you have a sub-circuit and another sub-circuit you can connect that fairly easily this is not the case with air uh you need to think a lot and maybe like it breaks the uniformity in some ways where you try to connect to computation so you need to work a lot to try to figure out how to combine them efficiently i think this leads to calculation from higher level languages being fairly difficult for areas compared to r1cs

i know of a few projects that are you know trying to reduce higher level languages to um to r1cs but i don't think there is a project even that is you know i try to do it at some point in time to try to build a dsl for air but it is uh i think much more complicated than uh working with r1cs for example uh one advantage that air has over about cs is that you can describe potentially unbounded computations with air meaning once you have this kernel of a kind of repeated computation you can um um you can kind of like you're not bounded by how many steps you want to apply for i mean there are some kind of theoretical bounds within a given field

but you know you can for practical purposes say it can be applied for you know billions and trillions and like 2 to the 64 times whatever all right just to give you another example so let's talk about like uh you know with a fibonacci function how would we represent an execution trace of a fibonacci function and you know in this case let's say when i use a single column again with 64 steps so we're going to compute the 64th term with vanishing function we're going to use a small uh field to do this and as i mentioned before like an execution tree is just is a recording of a compute records a step of a record the state of the computation at any given step so in

this case on the right hand side so i have this r representing the step of the state of the computation so we start with 1 1 here could have started with 0 1 probably but in here we start with one one and then you know our fibonacci sequence proceeds as usual we take the previous two terms add them together and get the next term uh and get the previous two terms uh sum them up and get the next terms and so forth until we get uh to the end uh this is again a very simple computation and execution trace uh uh for a fibonacci sequence is pretty pretty straightforward to build uh if we get to the fibonacci example i would show that that will show uh this

kind of like if we get to coding the fibonacci example toward then i'll show that this is not the only way to write a fibonacci sequence uh using sparks and this is like where some far fun and complexity come into play where there are many different ways to describe a financial sequence or or an execution trace for a fibonacci sequence um all right one of the things that i want to mention um about the kind of constraints that we think about when we impose constraints on the computation uh is types of different constraints and they they would be helpful to understand in the context of this uh zk hub because you know if you try to solve some of the puzzles this understanding of what is the

boundary constraint and what does a transition contain will come into play so the first uh type of constraints is transition constraints they basically describe algebraic relationships between two or more steps of the computation of a computation so imagine that this is our execution trace previously we had a single column and now i'm showing here multiple columns four columns to be precise and these are our steps and again here are only showing four steps but it could be millions of steps for practical purposes so transition constraints and you can think of them as a function that takes uh you know two nearby rows but doesn't have to be limited to nearby rows but it could be like three nearby rows or whatever but basically two nearby rows

uh as inputs and does some algebraic operations with them and then produces some value and we say that the constraint is satisfied if the result is zero and crucially we need to describe our constraints in such a way where for every valid transition the function should output zero and for every invalid transition it should not output non-zero so those are two important conditions for transition constraints work and and again here i'm using just two rows uh it could be multiple rows as long as they're local so they have to be local kind of like you can you cannot just grab rows from any place in the computation trace they have to be let's say offset by some constant from uh one row

or you know it should be impossible to looking at a specific row to just grab the uh nearby rows and and compute this and nearby could be relative it could be you know a thousand steps apart although probably uh for practical reasons you may not want to make uh kind of jumps between rows as big um the other type of constraint and here basically when we evaluate these constraints uh we apply the same function uh to every consecutive pair of rows and this is going to be kind of our constraint evolution step i'll show a little bit of this later on the other type of constraints is boundary constraints and boundary constraints assert that values um

at a given cell are equal to some uh kind of some other some constant value something that approval of a5 wants to assert so uh for example we may want to say that the first cell in the first row is equal to some value x and the third cell in the last row is equal to some value y boundary constraints are usually used to uh impose like input and outputs or like describe input outputs into the computation uh here i'm showing them placed against the first and last row but in reality they could be placed against any row any cell in the trace they do come at a cost so you probably want to impose them uh on the as few rows as possible

um all right so this kind of is a very quick very high level introduction to starks this kind of glosses over a little details of the protocol there is much much more depth to it but i hope at least at the high level it provides a quick overview um i'll pause for a second to see if there any questions um i'm i don't think i'm seeing any um all right so i'll continue actually do you want to just q a part of the um if you like go on the sessions tab in q a there's a bunch of questions there

oh yeah let me go sessions chat and then q a and i know i had a future yep i see it i see and if you want i don't know if you want to read them out loud or just if you need to read them yep um all right so i see the top questions right here can you explain the cost of a boundary constraint so the cost of boundary constraints is is such that you know you basically if you try to impose them in an unstructured way where you just pick like let's say some random rows in a trace and you try to uh

impose boundary constraints against those rows you probably your complexity grows with kind of a linear linearly with the number of impulse rows more or less i mean there are some caveats to that uh so if you just do it this way you basically transform verification to a linear verification if you have a lot of uh rows that you will nester kind of assert values for that's why we usually try to keep it minimal so first and last row it's just two so basically it doesn't increase the complexity of verification that much if there are other ways to do it if you have a repeated value that repeats some cycles that are powers of two it's fairly cheap to assert those but again if you take just a random number of rows

it's fairly inefficient and verification complexity becomes linear in the number of rows that you try to assert boundary constraints for can can you try to explain how these constraints are represented with a stark and what math is used i mean if we think kind of like from a theoretical standpoint they're just algebraic expressions they're you know expressions about polynomials how you code them up uh is a different i mean in winterfell you code them up using rust and in some cases you may have gsl that could explain could be used to describe those constraints

but underneath it all it's still just algebraic expressions of you know uh like this column and this matrix or taking a value from this matrix multiply from this cell in the matrix multiplying it by the next value from the same row a different row for example is equal to zero something like that so they're just the algebraic expressions that need to evaluate to zero for all valid transitions and non-zero to something that is not valid um let me see please uh please any simple example that computation structures you uh might be uh so i guess maybe the question is about

structure versus unfortunate computation so the simplest or uniform computation so uniform computation uh the simplest form you think you you have something very simple inside the loop and you repeat this many many times that's like a very simple uniform computation uh an unstructured computation think about that in a potential program that has very few loops a bunch of branching logic uh um i don't know there's a lot of nested default statements and things like that and there is really no repeated patterns inside the program that's an unstructured computation um i think uh in most in most cases that we kind of come across for a lot of useful use cases the computations tend to be structured i

mean it's very infrequently where you would come up with something that is completely unstructured where uh you don't make use of uh loops or it's all like you know like a giant like monolith program with a bunch of e-file statements there are cases like that i'm sure but i think those are fairly few what is field modulus in this case as i mentioned we follow the proving systems we work in uh some kind of some sort of finite fields and finding field is a mathematical concept uh in in this case uh the finite field is a prime field which means that uh any kind of algebraic mathematical

operations that happens we take values you know elements from the field uh for example you know if it's multiplication we multiply two values and then we apply the modulus of creation by this prime number so uh if you think about computer science terms you will get an overflow if you go above the modulus and you kind of wrap around and come back um it's the next question is having the whole execution trace makes stark so large not really it's not really related to the execution trees um i mean when you generate a proof that uh having to have like the entire execution trace and memory it does impose kind of like uh

performance penalties because you have to you know it would consume a lot of memory you will see some benchmarks later on uh but as far as the proof site itself it's not really related to that it's more related to uh how the prover uh like queries this trace and in case of start to use merkle trees and you need to provide the commercial path for every query that you provide and that's actually what uh creates a complex you can make cloud proof smaller if you give up some of the properties for example if you don't want them to be post quantum you can use something else right into the merkle tree as a way to commit or to do the screening stuff but um in that case uh you know you can reduce proof sizes significantly but you

lose post quantum security let's see i think i might have missed something but i think i covered everything if i didn't miss something just post it again and i'll i'll get back to it uh a little bit later all right i'm not sure what happened let me restart this can you guys see my screen yep

i think so awesome awesome all right um i don't know one more time all right uh let's get into winterfell right now uh so winterfell um is a general-purpose spark pruvit verifier and it's written rust and it's open sourced and it's under your mighty license and uh what this means is that uh so for general purpose means that uh you can describe any arbitrary computation using winterfell um it is kind of a fairly low level uh um so it's not may not be as easy but you

can actually you know any during complete computation or you can describe using winterfell um it's written in rust so we get a lot of benefits of using uh rust which one of the which is uh it's very configurable you can swap a swap out and not cover this maybe a bit later um you know hash functions and fields and without sacrificing performance and uh it is fully open sourced and it's so published to create seo so we can start using it and we will be using it actually for the ziki hack mini so winterfell is actually not a single library it's a collection

of different components so there is the uh they fire an approver the kruger is used to generate proofs and verifiers just to verify things but we also try to break it up into kind of smaller components and modular components that could be used potentially to build other pruning systems so there is the fry protocol which is uh used within winterfell you know it's it's one of the core sub-particles within starx that allows you to test whether you know approver committed to something that is a polynomial or not there is the arithmetization crate that allows is basically independent from ref which allows you to describe air for uh computations and then a bit more foundationally there is uh kind of the

uh crates that help us use cryptography or uh you know algebraic operations that i need to support our protocol such as you know math and finance fields or ffts and things like that um and then we also have a fairly expensive crate which is uh just has a bunch of examples of how you can use winterfell to build proofs from something as simple as you know fibonacci sequence to something as complicated as you know verifying you know thousands of lampard signatures for example uh so uh or proving that you verified helmets of lumber signatures so there is a lot of things that uh you can learn just by looking at the

examples there and to highlight just a few key features of winterfell so there is a i would say relatively simple interface so you don't need to understand the full start protocol to use it you do need to understand uh how arithmeticization works uh but this is non-trivial in itself but at least you don't need to learn the rest of it um as i mentioned it's very configurable you can dynamically select which finite field you want to be in so right now we have support for four or three different finite fields within winterfell and it's fairly trivial to add more if needed we have dynamically selectable hash functions right now you can choose between chakri and blake three uh and you know in the

future we'll add something like you know poseidon or rescue uh so that you couldn't he do this uh uh kind of recursive start proofs and then you know you can fairly easily tune security and like do this trade-off between proof size security and improving time uh in in real time using uh kind of like just tweaking a few options and sometimes these are even um these are kind of even runtime parameters they're not even compile-time parameters um and then it's fully multi-threaded so uh you can run it on as many courses that are available uh within some benchmarks uh uh in you know you get about 7x speed up with

eight four machine and thirty five expedite the 64 core machine and uh part of this memory bound so if you have faster memory you might be able um uh you might be able to uh you know even see a bigger speed up um in terms of uh i see a question whether security depends on field size uh it doesn't depend directly on field size so you can go you can use a small field like a 32-bit field potentially you do have to do some extra things which winter will take care of uh um for you if you use a small field for example fry protocol needs to be run in a large field so what you do is you run an extension of a small field for the fry particle part so but those are

basically taken care of by winterfell you can just from a standpoint of the user you can work in a 64-bit field and that's all all you need to care about um just to highlight the kind of like overall process of start food generation again not going very deep into this and the parts that are handled by winterfell so we have this certification step which takes a computation or a program and trans uh transforms it into a set of statements about polynomials uh and then um in the next step in the start protocol and this is the very high level you do something that's called low degree extension where you kind of interpret this

columns in the execution traces polynomials or evaluations of some polynomial and then you kind of like interpolate them and evaluate them over a larger domain and then next step you do this constraint evaluations where you actually evaluate the constraints that we have described as part of our utilization you evaluate them over this extended execution trace and then you do something called constraint composition this is basically combining all constraints together into a single polynomial this is done for kind of efficiency purposes and then you do this low degree testing for which you do fry uh you know we use right for that and then um in terms of like which parts of this uh you as a user of winterfell need to care

about is just the optimization part everything else is done handled by winterfell the user needs to provide uh the description of the computation uh all right uh some benchmarks here i'm not gonna cover this whole table so let's just focus uh on the last row so basically um this is uh as i mentioned verifying um this is for verifying lampwork plus signatures so we have uh a lot of kind of like this signatures that require hashing so lampard for those who don't know is a very simple cash based signature it's a one-time signature uh where you have a key and you can't reuse the key you know if you sign more than once

um but it is very robust for example is post quantum secure and you know people usually don't use lampard signatures because they have fairly large grooves but if you have something like if you need to aggregate a lot of signatures you know let's say you will agree a thousand signatures i don't remember on the top of my head but if you just had let's say raw lampard plus lumber signatures you would get something like megabytes of data um but you can put them together into a single start proof for example and that becomes much more uh manageable so like you can compress signatures in this way for example and aggregate them together we actually have a paper written about this so

in this case if we have it this is running on an eight core machine so it takes about 23 seconds to verify uh 1024 uh uh lampard signatures uh what this basically means is your full practical purpose is just aggregating the signatures together so like once you verify them nobody else needs to verify them again uh you can say you know there is this uh public keys and identified a thousand signatures and you can trust me by looking at this proof uh and as i mentioned like verification time is fairly uh fast it's uh about six milliseconds for verifying this proof the proof is fairly large very large not i wouldn't see but it's

about 250 kilobytes and you know you can flex it uh this is for 123 bit security level so you know if you wanted to get a higher security level you would either expend more time or potentially you know have a larger proof and then as i mentioned one of the i think performance related uh kind of downsides of starx is that you need to have fairly a lot of large amount of ram available so in this case it takes about almost eight gigabytes of ram to generate proof uh eight gigabytes is not too bad most computers have it but if you wanted to go beyond that you can see you know the the ram requirements could grow pretty much linearly with the number of uh signatures and in this case

uh you know proving time um also grows fairly almost linearly it's quite linear but the proof size you can see it doesn't change all that much it you know we went uh we increased this manifold but the proof size increased by uh less than 50 um i've listed the r1 cs equivalent here it's not a very fair comparison i would say because this is an extremely structured computation where you have just you know basically a loop that verifies a bunch of signatures so it is more kind of spark friendly for r1cs this would take quite a bit of quite a few constraints to represent but again this is not like the type of computation i think that is very well suitable for one cs all right um

this kind of like covers my overview and then the next thing would be to code well work on the postpartum uh vtf uh i'll do a quick intro and then we'll do uh coding of the vdf uh let me see i might do do i have uh how much time do i have at this point i think i i have about 40 minutes right yep all right so i think we are doing well on time let me see if there are any questions yeah q a has a couple more and actually folks can upvote other

other people's questions if they also feel they want them answered so first question is can you use winterfell to compile a verifier into a smart contract or how would you integrate this into a web 3 application so for winterfell uh specifically um i mean uh you would need to write a dairy fire that can verify winterfell proofs and salinity or something like that uh uh to create a smart contract so natively you can just compile it but you can it's not it shouldn't be too difficult to uh write a like use the logic that we we have in the verifying rust and just write it up in solidity in that case you can verify uh proofs that winterfell generates

you know on blockchains how easy it is to extend winterfell to support computations in the 256-bit prime field uh wouldn't be slow so it's not difficult we just you know uh there is like a set of trades that need to be implemented to support the 56 bit fields uh would it be slow uh i mean it would be slower and it probably so the smaller fields you have the kind of like the larger you feel this your your complexity is growing faster than linear so it's not just like if you let's say go from 64 to 256 bit fields it's going

to be more than four times lower it's probably going to be closer to like 20 or 30 times lower if you go from 64 to 56 bit field so it is going to be slower but it may be acceptable for many use cases um it's it's not gonna be uh preheated prohibitively slow um why is it important to have quantum security uh in the near term um i mean i think it's more kind of like a philosophical question whether you wanted to have it or not i think uh in the near term and midterm we probably don't need to be concerned about quantum security but if we're building systems that we expect to last tens of years or decades or something like

that maybe it's a bit more uh you know you want to you know build something that is going to last for a long time but again i mean it's more kind of like a philosophical question of you know maybe you can admit the system later on as well uh in my ca in many cases um you know you get this postponed to security with starks and because it is using only hash functions you get other nice benefits like the speed for example so one of the things i mentioned you could make a start proof smaller by replacing merkle trees with some other vector commitments but it is likely also make uh loose post quantum security but it also most likely going to make uh proving time slower so

because we need to rely on this very few cryptographic primitives we get other benefits as well so uh post quantum security by itself not a huge factor in my opinion but it's nice to have it if you can get it by getting other things let me see uh another question i'm aware of plonky too is it uh the fast when it comes to proving time uh why does winterfell faster than that um we haven't i mean first of all plonky 2

is extremely fast in the aggressive context uh winterfell doesn't support recursion yet so it's uh it's difficult to compare to be honest uh and as i said it's very computation specific there might be computations that are faster in winterfell uh might be there might be other computations at the faster pokey too i think it's difficult to say which one is faster unless you have like a very good set of benchmarks and even then it's going to be difficult so i can't really say especially on the approver side on the very fire side i think it's fairly easy and i think on the very fire side they're fairly comparable in most cases just like single milliseconds but there will be a workshop on plonky too uh i believe uh in a week from now so uh

might be a good question to ask uh uh the authors uh there as well but again i think performance comparisons across this different proving systems and libraries are very difficult so composibility so another question compassibility will start can you elaborate a little bit on that how scalable is it in that respect i think compatibility with starts is very difficult especially like if you think about building standalone libraries or gadgets for example that you people can reuse i think that is a fairly complicated challenge and i don't know if anybody is actually trying to solve that there is another approach that i think works well for stances in the virtual machines this will be in the next uh

talk that i give about why virtual machines are useful and especially in the start context and this is how you kind of address the compressibility problem i think and another question do you know other two congenital star proofs and can be verified in solidity um i think there are a couple of limitations of improving systems out there um i think start where i mean i know for sure start where it has a uh solidity verifier for the proving systems that they're using um i believe uh xerox at some point had a star crew

improver that i believe had a solidity verifier as well so um i'm not quite sure if uh you know what state those systems are in and at what extent uh you know uh you can openly use them um but uh yeah you can i mean you can write uh a very fine solidity there is no the verifier is actually fairly simple in terms of uh of what needs to be done uh so it it's it shouldn't be too difficult for people who know how to code up uh insulated to to write a verifier the stock verifier all right um i think i covered everyone but if not do

uh re-post your questions okay let's go to the postpartum media so uh first let's talk about verifiable delay functions so verifiable delay function is a function that takes some input and produces some output and we want to have the following properties yeah we want to given some input x we want to compute the output in some time t and it should be very difficult to reduce t by more than some small well-known constant and specifically you shouldn't be able to apply parallelism so it doesn't matter how much hardware you throw that you can't reduce t by that much and maybe you can like uh do some

specialized uh hardware which could be a little bit faster than generic hardware but again it shouldn't be significantly faster so you can basically just throw resources that didn't compute and reduce t by a lot and then if we have y and x it should be very easy or fast to verify that y was actually derived from x using f so this is uh kind of like we want uh the complexity to be at least logarithmic and you know maybe ideal even uh constant but at least like a polygraph we can see um and uh some optional properties that would be nice to have is that we want to have you know trusted set up for example

and no fancy cryptography uh to build the ctf so we're going to build this pdf and we need the no fancy cryptography part for post quantumness of this um so in our case the the delay function we can choose could be something like you know taking a value raising it to some power and then adding a constant to it and again this is kind of like a toy example so maybe if you're building a real media this may not be a good approach to it but i think this is more kind of to illustrate the point um sorry i'm not sure why this keeps happening all right so if you want to describe

this function this is you'll notice that this is the same almost example that i used uh when i described error you take some seed and number of steps and you repeatedly apply this power um when we work in finite fields we can actually uh run this function in reverse direction which is a bit more uh computationally intensive so uh you know there is like in the inverse of alpha which can be computed in the opposite direction and uh depending on which field you you use this could be kind of you can compute uh in the reverse direction maybe at time t and then in the forward direction the same thing can be computed maybe in like 100 of that time or something like that but it

depends on which field you use uh you know it's the difference is smaller for smaller fields and larger for larger fields but basically um we have these two options we're going to use the reverse direction uh to compute uh our vdf so if we think about this so we apply this video function for me so uh the the reverse direction we have item in a number of steps and on my computer and actually it should hold roughly true for uh most general purpose hardware out there and this would take about 1.5 1.7 seconds to compute this this function for about a million iterations um

and then you know we could do the naive computation back as i mentioned in this case it's probably going to take you know maybe about 100 milliseconds maybe a bit less actually to just compute it in the in the forward direction identify this but we want to do something even you know more sophisticated than that because the difference between verifying and uh and actually computing is is you wouldn't want it to be a constant factor we want it to be kind of like exponentially faster to verify than it is to compute and uh we could use a start proof so instead of like spending 100 milliseconds and verifying uh that uh the function was committed correctly

with the start proof we can do it in two or three milliseconds um so this is where the stack pool comes in so we will run the function in this direction and then we'll verify that it was executed correctly using a start proof all right some parameters for our computation so this is the function this is kind of what we call a transition function for a computation uh we'll use this uh 128 bit field that we have available in winterfell um this is more kind of you know for initiative purposes this is not a super performance field so for predictable purposes maybe you would want to use a different field and obviously as i said this is a true example anyway so don't use this in production um

our transition constraints are going to be described like this so we take the um we take kind of the next term and subtract the previous term from it and i'm not sure yeah we can actually describe it in a different way i think i actually screwed up this definition here but uh we'll uh we'll see the real one once i start coding uh and then we want uh the boundary constraints uh we want to start let's say this value five and then if we run it for about a million steps we should get with this large value at the end so this is kind of the setting of our vdf and what we want to do so let's

put it up let me stop sharing and bring up um me zoom in a little bit can everyone see uh writing no financially zooming more not so good i think it should be zoomed in more and i also know that i think for the video it's good for when you're doing code stuff to just close like turn your video off because then the the capture will just be of the screen i see okay

um but i think could you zoom a little bit closer i don't know if other people in the audience have opinions but to me it's still pretty small how about that guys i think this is looking good you can also make it a full screen if you need and you can hide to anyone who's curious you can actually hide the chat if you need to there's a little arrow near where the number of people here are okay i'll jump off go for it sounds good all right so here i have like a basic um uh projects that happen in uh digital tv code uh just to show what we have here we just have a single dependency which is winterfell and we're

using a concurrent feature to generate cools concurrently um so fairly bare-bones stuff here so let me see so the first thing that we want to do is um let's start with um defining our function so um i have all of this coded up before so i'm just going to paste some stuff here to save on time so here's our video function and in this case let me actually bring in all the imports that i need for this um felt in this context is just a field

element so field element in uh we're using a 128 big field available in winterfell um and then let me bring in some constants that we described in our uh in the slides out there so we have our alpha which is three we have um this is kind of the inverse alpha and we have the our value of 42 which we will be adding so our function is fairly simple um if you remember we compute the next state by taking the uh the current state subtracting the 42 from it and raising it to inverse alpha this is kind of our transition function for a given step and then we apply it for you know n whatever number of n is in our case and it's

going to be like a million steps basically um the next thing that we need to define is um a set of public in like what how do we think about public inputs into this computation if you remember uh to the very beginning of the presentation and you know i said we have a function um this but this is our function and then uh the proven verifier needs to kind of know the public inputs that go into this boot there is there was also this witness thing that there's a secret input we don't need it for this specific uh computation uh so we only care about public inputs and in our case public inputs would be um also fairly straightforward so the public inputs is the value from

which we start uh the single sealed element and then what we get at the end and even though this is the result we still kind of aggregate this into something that we call public inputs and then we need to implement uh kind of we need to tell the proving system how we can serialize that so this is kind of like a almost boilerplate plate of some sort but uh this is just needed to serialize this into a set of bytes all right so the next step is more complicated so we need to actually define air for the computation so we have the function now we need to translate it into air and within winterfell we do this

by creating a struct and then implementing error trait on that track so um in our case um let's say let's call it vdf air and we'll go into the kind of what goes into it what we'll actually put into this track but for now let's just implement air for uh the dtf air to implement the trade we need to specify a few things first we need to specify which is the base field we use for the computation and this is in our case just the field element that we have defined

the other thing that we need is define what shape our public inputs have for the for the communication in this case it will be our vgf inputs the next thing that uh we need to implement is um we need to tell um you know the trade requires like a way to instantiate itself well it destructs instantiates itself so we need a new function um in our case the new function has a specific signature so uh the trade imposes this you know traders by the way for those who don't know raster or not similar trade it's kind of like an interface

so we need to have this function which uh takes uh something called the trace info public inputs uh and options and these options are really describing the parameter set for the start protocol so like they say which hash function should be used which you know actually you know how many queries and uh you know this is kind of the details of the start protocol but they basically explain uh or define um which parameters we need to use and those parameters affect like security level of a start they affect the you know proving time and things like that so uh we'll get into some of these parameters a bit later uh all right so there is uh uh we'll implement this function in a

second uh then there is another function that we want to implement this is describing how our transition constraints are going to work and the function is called basically a value transition so this function takes something that is called an evaluation frame and evaluation frame is uh basically just a set of two rows like there is a current row in the next row um right now this is kind of a limitation of winterfell where i i describe you know in theory you could have constraints that span many rows but within winterfell we transition the trains uh for at least for now can only work with two consecutive rows over

trace um so this function takes this evaluation frame and then it produces the uh writes values into this result so once it evaluates the constraints it uh it writes the result of constraint evaluations into this uh slice slice and rust context is kind of like an array you can think about it a reference into an array all right so the other thing that we need to the other function that we need to provide is the function this defines our boundary constraints and the boundary constraints in winterfell are defined by something called assertions and we'll implement those in a second

but basically this says uh you know specifies what what values do we want to assign to a computation uh in a given cell for example and then there is some boilerplate and that we need is uh you know a function that returns uh context of this computation uh and this context will i'll see i'll show you guys how we can do so we have kind of stopped out most of this yeah so let's go back to our vgf uh air struct so we need to return context here and this is just boilerplate uh so for this purposes we need to just uh define context here we also want to keep track of uh you

know our public inputs within the struct so we'll just say we have like a seed and result within the vdf air struct so now when we construct let me actually not do this first let's go here uh let's talk about assertions first so um now we have kind of our strike stabbed out uh we have the context implemented and uh um now we need to actually do the neat part of this communication so like the assertions we have two assertions we want to assert that the uh initial value of the the sequence is uh equal to c then the last value of the sequence is equal to

is equal to uh whatever the result that we're claiming we have gotten after executing the function for a million steps or whatever uh so we do this by um basically first we want to figure out what the last step is so we have trace length and we just you know do minus one to see which one is the last step and then we return a vector and a vector will contain the two assertions that we want to impose so the first assertion is that um you know it's a assertion against the single cell in the trace and the cell in the trace is basically this is the index uh we only have a single column so this is going to be zero this means the first step we're going to

assert that at the first row in the in the first column in the first row of the execution trace uh the value of the cell is equal to c and then similarly the second assertion is that in the first column now case again the only column at the last step of the adjection trace the value is equal to result so this is um this is the kind of boundary constraints so winterfell translates this assertions internally into boundary constraints for um for our transition constraints again our transition constraints are fairly simple we'll just you know get the current and the next state from the evaluation frame

and then we have a single boundary constraint uh a single transition constraint sorry and this transition constraint uh will basically take the current state uh we take the next state apply this alpha power to it and then add 42. so this is if you remember like basically this is computing function in the forward direction but then you know if we subtract from the current state it's kind of like uh you know proving that we could we're proving it backwards uh and i should have covered that in the in the presentation but we're basically uh computing the constraint backwards for uh because we can use this property that we're raising to alpha we actually get a fairly small degree so this is our traditional constraint and then the only thing left for the air

thing is you know create the actual uh struct um one of the things that we need to do is create air context so let me let me do this so air context and i'll just copy and paste for to save time uh requires the following uh parameters so we need to provide this trace info that we got here we need to provide this set of options for the start protocol and we also need to provide something called like a description of transition uh constrained degrees um

the concept of degree is fairly important like when we impose uh when we come basically come up with this polynomial to describe our constraints um these polynomials have certain degree in you know if a constraint for example uh use multiplication you know the degree could be you know if just one multiplication two if that if you were using three multiplications the degree could be three so we want usually to keep the degree fairly low because it impacts efficiency and of generating proof and also would impact proof size in our case if you notice about description of constraints we are raising next time to power alpha alpha in our case is three so our constrained degree

is going to be uh three um so we need to create this uh degrees vector that will pass into the context and this would be uh you know we basically create a transition constrained and degree of degree three okay now that we have context everything else is fairly straightforward um we just you know create the struct let me just clean this up a little so we pass the context we grab the seed from the public inputs and then we go grab the result from the public inputs as well so now we have and describe the air for this computation and i know it's probably uh

if you've never seen this before it's probably not super easy to follow let me actually see if there are questions yeah so why did i choose to reverse the operation i think that's a good question and something that i should have explained uh the main reason is that as i mentioned we want to keep the degree of transition constraints as low as possible uh in our um let me see if i have it here let me just bring this here um

we want to raise it to this huge power um here so like this alpha inverse is a huge power so our constraint degree is going to be huge uh and we can't uh you know it wouldn't uh be a practical system where we have such a large constraint but we can do it because of these properties where alpha and alpha inverse we can kind of compute uh the sql both backwards and forwards we can compute it uh kind of like if we're computing in a backwards direction to compute the forward direction we only need to use alpha three and this is the property that we're using here um where we set alpha to three and we can compute the transition constraints backwards and reduce the power of our transition constraints that's the

primary reason for doing it this way another question do we have to manually provide a calculate and provide degree with the constraints yes you need to do that manually the library is not smart enough to kind of like analyze rust code and figure out uh you know how many multiplications you had for a given constraint um there is one uh way to help you though if you use a library in debug mode like if you run the improvement debug mode when it generates the proof it will actually check if the constraint that you specified matches the constrained uh degree that you uh that you claim it should have so in debug mode it will actually tell you

there is something wrong uh if you define that you know that there's a mismatch between the actual degree and the degree that you said it would have uh the reason we do it in debug mode only is because this check is fairly expensive and we do not want to do this check in the in the release mode so while you're developing your proof for example you run it in debug mode and it helps you somewhat to make sure that degrees of constraints are aligned but in really small you we kind of remove this check so that it runs as quickly as possible uh one thing to notice and i should have mentioned it as well so as you notice there is like a single constraint here and we uh and we kind of assume that there is going to be at least one constraint that we can

write into the the size of this uh slice is determined by how many degrees you pass in uh in here so here we pass the single constrained degree and this means here we're going to be able to write a single constraint if we had two constrained degrees here for example we would have access to two constraints we would be able to write into two uh into two kind of cells of this result so all right so this now defines um the the air so the next thing that we need to do is uh uh build approver so let's start with the proverb

that actually will generate the execution trace so the primary thing for the crewers to generate execution price uh execution trace uh we'll call this uh bgf prover i'm just going to copy and paste to save time and again it would just take the proof options to describe the parameter and one of the things that we need to implement for the for the prover is there is a proof prover trait so here we're going to implement the prover trade for vdf prover and prover trade specifies a few things i'm again just going to copy and paste so the first thing it also needs to specify the field that we're going to

use the base field it needs to specify which air we're working with so the air for this prover so this is going to be the air that we just defined and we need to you know specify whatever we're going to use to describe the execution trace in this case winterfell provides the stress tables track that you can use as a default trace for probably all the most of the needs you have but in case that struck doesn't work for a reason you can always override or implement your own execution trace in whichever way like you you need for your specific use case um as before we have this boilerplate that just returns options um with the computation

and then one other thing that we do need to implement here is how do you take a trace and convert it into public input so in our case it's fairly simple in our case the public inputs are this vdf input and what we get so get pub inputs basically takes a trace and produces the pdf input and we just take the first row or first column first row uh as a seed and the result should be in the same column but the last step of the computation um okay so this kind of like implements a proven trait we need a way to instantiate the proven to build the actual trace so we'll do another just implement the specific

uh not not a trait but just the specific uh functions for this struct and we want to have a new function that creates the prover and then there is going to be this uh the the function where the real work happens this is the building of the trace uh and again in our case this is relatively uh simple our trace uh consists of just a single column uh so we'll just use this uh vector um to contain the values of this column and

then at the end once we've done building it we'll just initialize our um trace table with this column so it will pass it as a in theory like if you had multiple columns you would be able to pass multiple columns here but in our case we just have one column and then um the way we we're going to do this is that we're going to initialize the state of our computation so here's the state is just going to be a single field element um and we'll start by pushing this uh field element into our trace so this is going to initialize the trace with the first step state of the computation and then we're just going to repeat this for you know you know 10 minus one number of steps in this

case and if you notice here we're running the the function in the reverse direction here so we're raising to inverse power alpha while uh when we do the transition that trains we verify it using the just uh alpha itself so in if you remember in inverse alpha is a huge degree but alpha is just three and then once we update the state we again record the state in the trace and then by the end of this loop we have our full execution trace built all right so the last thing that remains here is let's build the main function so we want to run this for like a million

steps and we want to start with value five so this is our initial inputs just for kind of sanity checking making sure that we did everything correctly we're going to run this computation separately using rvdf functions so in theory this is not required if we you know do everything correctly because we'll get the result by building an execution trace but here uh just to see how long it takes to compute the etf we can without building a trace uh we can just uh run it separately and get the result and see if you know we actually quoted things up correctly um the next thing we need to do is we need to define the parameters for our start

proof so this is the option object that i've like been passing everywhere so in here there are a few things that we need to specify i don't think i'll have the time to go all into all of them but there is documentation here that describes uh you know all the parameters and their meanings and so forth but basically we're going to have like you know this is number of queries that determine the security level this is law factor that also determines security level as well as how long approver will run grinding factor that kind of allows you to increase security at the expense of the again improver time hash functions and extension fields that we're going to use and then some fry related parameters as well so once we have this

we are ready to instantiate our approver and this is just very simple to do using the new function that we defined before again we pass our start parameters to say you know for the prover to be aware of the parameters for the protocol uh and the next thing that we want to do is build an execution trace using this prover so yeah this is what we do here actually um we build the trace using the build trace function that we implemented and here we just record uh how long it took and also make sure that this result

you know is the same as the result we got here again this check is only for our sanity to make sure that we didn't screw anything up um let's see so the next step that we need to do is uh generate the proof so once we have the approver and we have our execution trace we need to generate the proof and we do this simply by saying kruger.proof and we pass in our trace and this generates the proof of our computation this it is as simple as that at this point i mean there's been a lot of work to actually write up the air and stuff like that but now that we have the air defined generating a proof for this computation is just as simple as passing

the trace and saying crew we want to just for informational purposes figure out you know how big the proof is and you know print it out so we just serialize it here and see what security level we get and then um let's see we want to again deserialize the proof to make sure that uh serialization deceleration works fine uh and here we would see that you know if we serialized and this realized proof should be the same and the last thing that we want to do in here is just make sure that the proof actually can be verified so here is the simple

set of statements let me explain this but basically we're just saying winterfell verify we specify which error we're using to verify a proof and then we just pass in well one thing i forgot we also need to build public inputs so in this case you know over here uh want to build public inputs in our case the public inputs is just see the result so given the hidden result we can say whether this proof so for these public inputs the verifier should only accept the proofs that are valid meaning we ran the computation specified by this dtf air we started with seed and we ended up with result and this is the proof of

testing for that so this is the whole thing and let's see how it works so it's gonna compile all right so what do we get from this first it ran about the actually running the computation took about 1.7 milliseconds uh 127 seconds which is what i was aiming at executing this function for a million steps takes about 1.7 seconds building execution trace is basically

the same as computing the function there is really no overhead detection of whatever reason came out a bit faster uh probably for some idiosyncratic reasons it should be basically the same changing the proof here took about the same time as running the vdf itself but this is has been spread across uh i have 10 cores on this machine so across 10 cores um if we did on the single core this would take probably close to 20 seconds i want to say maybe a bit more and if we had 16 cores obviously it would be roughly half that maybe a bit less than half um so you can actually verify generate a proof

faster than it takes you to run the vdf um and if you have more cores available it could be you know 10 times faster or maybe 20 times faster to generate the proof that as compared to running the vdf itself uh proof size in this case is 114 kilobytes our target security level is 100 bits and verification crucially this is what we were trying to do this is why we bothered with the stark in the first place is just 1.7 milliseconds so we run the function for 1.7 seconds we spent about 1.7 seconds engineering the proof but then verifying it uh cost us just 1.7 milliseconds so a thousand times faster um

all right uh this kind of like concludes the coding portion of this let me see if you guys have any questions all right i don't see any questions uh so uh either i confused everyone or everybody understood everything thank you so much poppin for this great workshop yeah yeah happy to do it and if there are any other questions or follow-ups always feel free to post them we'll be happy to answer them cool so yeah our