ZK9: AirScript - a simple and efficient way to write AIR constraints - grjte (Polygon Miden)

Transcript

foreign [Music] and now it's my great pleasure to introduce Christian who will talk about airscript a simple efficient way to write a constraints take it away um so I could perhaps also have titled this an auditable and maintainable way to write error constraints because that is one of the major goals of various script as well to start off with what is airscript it's a domain specific language for writing and auditing error constraints for the Stark proving system so error constraints we'll go through that first it will be a recap for some of you and maybe new for one or two um what we're doing is taking a

computation and changing it into a bunch of polynomials that we can then use for our proving system so this is the process of arithmetization and in our case we want these polynomials to be in this specific algebraic intermediate representation form which is air and we want to use Fry at the end of the start proving process so these need to be some low degree polynomials um so this is what era's clean strains do they describe a computation as a set of bounded degree polynomials and they fit into the Stark proving proof generation process like this we have our execution Trace which we um extend using whatever bullet Factor we choose during our low degree extension then we do constraint

evaluation against that extended execution Trace we then combine all of those together into the composition polynomial and then we run fry and the air constraints fit in right here from the extended execution trays to the constrained evaluations so how do we Define them there are a few different types of air constraints first you've got your boundary constraints which are against specific cells in your execution Trace so at the beginning and the end in particular is where we usually impose our boundary constraints saying that some first the initial value in you know column zero at row zero is X and then at the end of our computation we have a

value y somewhere else in the trace we've got our validity constraints which we impose against a single row so that says when I check this function against r0 against the row it should equal zero and I perform that same check at every row and then finally we've got transition constraints which we'll take in two or more rows so a frame of rows in the execution trays and check that we get zero so if we look at this example with the Fibonacci how we would Express this in air constraints first we have our execution Trace which has two columns A and B and we're looking for the 64th Fibonacci number so you can see that we're just going through Fibonacci here

and the steps of the trace we have 32 steps and we'll start by setting our boundary constraints so a at zero should equal one and B at zero should equal one if we don't start with those we're in trouble um or we're doing something else and then B at row 31 should equal the 64th Fibonacci number so those are the boundary constraints we need to Define Fibonacci and then we need to Define our transition constraints which say the value of the value in column A at the next row should equal the value of column A at the current row plus the value in column B at the current row so one plus one equals two um at the first two rows there and then we need to also enforce the value in column B so we'd say B in the next row

equals being the current row plus a in the next row so here we've got three equals two plus one or three equals one plus two I guess is how it's expressed here and that's all we need to Define Fibonacci in error constraints against our execution Trace so um why do we actually want a DSL for this why airscript well if we want to kind of look at this as a black box of our Stark River and our Stark verifier our approver takes in the execution Trace some public inputs and the error constraints as we just saw and it gives us a proof the Stark verifier takes in these same public inputs it takes in the proof and it takes in the same error constraints and then it says yes or no so we need these error constraints in two places to start with and we'd rather

not Define them twice moreover in Maiden for polygon Maiden we have multiple verification contexts so we've got our Winterfell star verifier which is our sort of regular verification we've got a mide and assembly Stark verifier that we use for doing recursive verification inside might and VM and then we'll have a solidity start verifier for doing verification on ethereum and all of those need to know about the same set of air constraints and of course as we just saw the prover also needs to know them so now we've got our constraints that we need in four places and any good software Engineers look at this and say well I don't want to write these things four times in four different languages because that's going to cause a lot of issues with maintainability and correctness and it's also a really big ask for any auditor to

say hey go um check my constraints in my assembly which you've never seen before check them in solidity check them in Rust um so what we'd like is to enable a single source of Truth for the air that is easily maintainable and auditable and that's why we have developed air script the goals of it starting off we want it to be readable for developers and Auditors ideally um I'd like you to be able to look at airscript without having read our docs and understand what's going on um at most maybe you have to learn one or two new keywords in the language we want it to be powerful because we need to be able to describe constraints complex enough for a zkvm and finally we'd like it to be modular so decouple the IR and the code gen so

that we can support all these multiple targets that I was just talking about and the benefits of modularity what we should have here is our airscript source which goes to the airscript IR and then to these three backends so Winterfell which takes care of our approver and our sort of default verifier our mine assembly back end for the constraint evaluation in our mind assembly verifier and our solidity back end for the same thing in our solidity verifier and so at the top level it should be readable and auditable here in the airscript IR we'll do some common optimizations and then we can do back-end specific optimizations for the specific backgrounds another benefit here is that actually we could add a few more back ends so we could add a backhand for polygon zero we could add a back end for triton VM for risk zero

and then you get to the point where you can actually be verifying approved from um someone else you can be verifying approved from someone else's VM in your own VM by just generating um the evaluation of the constraints in the format that their VM understands so an overview of the aeroscript language we start off with several sections which sort of follow the shape of what we need to know for our execution trays and for our error constraints so we have Trace declarations defining the shape of the execution Trace we have our set of public inputs which defines the shape of the public inputs then we specify the boundary constraints and then we specify the Integrity constraints so this is exactly what we saw with the Fibonacci

example but we structure it into groups within our airscript file so these are what the trace the trace decorations look like we have our Trace columns and we say first we've got our um main set of columns so we can have multiple execution Trace segments the idea with these segments the first one is the one that's built before the prover makes their first commitment the approver then sends that to the verifier and then gets a bunch of random values and then can commit to another Trace segment using those random values and that would be this auxiliary Trace segment So currently we're limited to two but in the future we plan to support more Trace segments as well we can bind a name to the columns so in our main Trace we've got uh what's the math on that we've got seven columns and we

decided to call the first one a the second one B and C is actually a group of four columns that all do something together maybe they do range checking or whatever so we can group them and refer back to them later we've got periodic columns which Define polynomials that can be efficiently evaluated by the verifier so some people will use constant polynomials we choose to use periodic columns that sort of repeat however eating pattern and then we Define our constraints against against these periodic columns so when k0 is zero we use it to select for a specific set of constraints and when it's one we apply a different set of constraints and then finally we've got random values and we can bind a name to those as well so that we can access those when we're setting the constraints for the

auxiliary Trace public inputs as I said we need to find the shape of public inputs sorry a question the way you defined k0 K1 the periodic columns could you explain that again maybe we can we okay yeah it's not the constraint definitions work out so the yeah so the public inputs we're going to say we have a set of initial values that we expect our Trace to start out looking like and then we have some terminal value which is actually what we're Computing with our computation and

that's sort of the point of it we can declare an unlimited number of these named public inputs and each of them is a fixed size array of one or more values in the future in order to support mine VM in fact we need to have variable length public inputs and so we'll be supporting variable length input tables the boundary constraints um it's defined so that we can set constraints against the first or the last boundary in the trace um MF is our keyword that means in force so that's the one new keyword that you need to learn for airscript I think sort of maybe there's one more but um enforce that a at the first row equals zero be at the first row equals one and then enforce that b at the last row equals this terminal value that was our result that we expect

and so these boundary constraints can be based either on constants or on public input values and finally we have our integrity constraints and these Define um these describe the validity constraints that are applied at every row or transition constraints that are applied over a frame of two or more rows and we've got our new um we support common arithmetic arithmetic Expressions as you would expect because you have to be able to use those um we can access all of the trace columns that we defined and all of the random values that we defined we can Define some intermediate variables with the let keyword and we also support list comprehension syntax the one other thing to note here is we have this m a prime equals X plus one

I'm not sure if I fully explained earlier that we use this Prime to signify the next row so a is the current row of column A and A Prime is the next row of column A so here we're saying we expect a in the next row to equal a plus b plus one so those are all of the basic um things that we use in aeroscript and here's an example with the Fibonacci constraints of what it looks like we're going to Define our FIB error and then we set our Trace columns so we'll have these two columns A and B and then we'll set our public inputs the result we expect it to be one and then we'll start with our boundary constraints so a in the first row should be zero B in the first row should be one and at the end B in the last row should

should be this result then we have our integrity constraints and these are you know of course the same thing that we looked at before it's a in the next row equals a plus B and B in the next row equals B plus a in the next row and that's it that's what Fibonacci looks like in aeroscript now that's quite simple and we did say that we want it to be powerful enough to describe the constraints for a ZK virtual machine among other things um so let's add constants constants are useful here we're defining our MDS and inverse MDS matrices um I didn't write them out because I would take up more than the screen adding to constants let's have some functions so these are pure functions no side effects we'll pass in a vector of

12 State elements and then we'll get out another Vector of 12 State elements and we've done some manipulation here with our list comprehension syntax um now one thing that would be very handy is if we could have sort of a default implementation of our of our function that will get compiled and be used for all of our verifiers but maybe we could have a way to do um an extra fast optimized one that we use for the proverb so maybe actually for the apply MDS function and approver I want to write it in assembly code um so what we have is this way to define an external subroutine for the prover and we say okay if you're the prover use this mds.rs file this rust file that knows how to do apply MDS and so we can

swap it out in that one case we have finally evaluator functions so this is the other new keyword is this EV and the idea with evaluator functions is that they do have a side effect and the side effect is that they enforce constraints so you'll see this emph keyword again in the last row which is actually enforcing the constraint here so our evaluator function rescue Prime takes in um instead of just taking in a vector of um in the way that our Pure function did it actually takes in a set of columns so inside of these brackets you can see we're passing in the state and those 12 State columns are actually columns from our execution trace and that's why we can then enforce against them and so what we have here are the rescue

Prime constraints in airscript and that's the hash function that we actually now use rescue Prime optimized but that's the hash function that's used inside might and VM so these are the constraints for hashing um it would be great to throw those into a module so that we don't have to have everything in one big file so we'll call this mod rescue and everything else stays the same and now let's import and apply an evaluator function so we'll Define a new module this is for our chiplets which is where we have sort of our specialized computations like hashing bitwise operations Etc memory so we'll Define our triplets module and we'll import rescue Prime from our rescue module and now we'll have our hash chiplet constraints where

we we get the shape of our hash chiplet which has three selector columns it has a row column it has these 12 State columns for the hash function and it has an index column and we're only going to pass in the state to our rescue Prime evaluator function because that's actually all that it needs to verify so we'll just pass the state and enforce all the rescue Prime constraints against the state in our hash shiplet and then we'll do whatever else we need to do with the selectors and with the other things inside the hash chiplet and then from the rest of our triplet constraints we can just again we get actually a larger set of columns being passed into here because we've got many more triplet columns we've got it's got its own selector it's got some columns from the auxiliary Trace segment but again we'll

only pass the chiplet columns through to the hash chiplet to then enforce everything that needs to be enforced there and so now we get to the mine and virtual machine constraints and first off this is what the maiden VM execution Trace looks like um two system columns 23 decoder columns 19 stack columns Etc and here on the end are the this is the section that does the chiplets that I mentioned so we've got our hasher bitwise memory and padding and there's 18 columns there and that's what we just kind of looked at but chiplets module and now we'll look at the mine and VM constraints in one slide in our script from the top here is the maiden VM error

we are going to import the evaluator functions to apply to each of these sections of the trace our system decoder stack range Checker and chiplet then we'll Define the shape of our Trace so we've got our system columns decoder columns stack columns range columns and chiplet columns and then we do have an auxiliary segment and this is where we have uh the columns that we use for multi-set checks so in mine and VM we think of it as a a table helps maintain the Integrity of that set of columns so the decode or tables there are three of them help keep the decoder columns correct and a bus is for communicating between this set of columns and some other set of columns in the trace so for example here we've got the range bus is for sending requests for range checks

so that's our Trace public inputs we need a program hash we need our initial stack inputs and we need the stack outputs that we get after execution and then the boundary constraints I'm emitting for brevity because I can't actually fit all the constraints for a ZK VM in one slide but close now the Integrity constraints we're going to enforce using this evaluator function the system constraints on the system columns we're going to do the same thing for the decoder constraints and we'll pass in the second Trace segment for the decoder tables then we'll do the stat constraints range Checker constraints and enforce the chiplet constraints and these are the ones that we looked at earlier um in a little bit more depth and that is all of it that's the mind and VM

constraints in airscript hopefully um if you've coded in a language before this is fairly readable for you and we've achieved our goal of readability auditability and being able to maintain our constraints in in one place so yeah any questions all right that's left thanks for the talk uh I always wondered when I was uh when I was thinking about air in the periodic constraints it's so cheap to generalize to non-periodic constraints using it the pre-computed selector polynomials a la Planck are

there any intentions to support that too is has support for periodic columns and they're quite like they're not that expensive either and we don't use very many of them so if if we were doing something like sorry to interrupt it it's not about being expansive but uh I don't have to take so much experience with air so uh but it seems to be to have so much more freedom if you're not restricted to have periodic columns ah I think I think that freedom because the things that we're doing are very periodic so for example our hash function takes eight Trace rows to do a single hash and

so having a periodic column that's defined as being just eight elements lets us use that as selectors for what row of Hashem that period must be a divisor factor of the entire domain size no yeah so there you have some restriction yes but if we're doing it this way I mean yes I think this is a I think this is a bigger conversation maybe yeah thanks so also it's common to talk about those selector columns using the pair Paradigm right what's the advantage of using selector instead of just defining the enforcement domains of air without selectors because it increases

the degree bounds that you're going to work with in Fry yeah um so we use we use a lot of selectors Beyond just um Beyond just the periodic columns that we're talking about we use selectors to determine what operation we're doing for the sac and we have a lot of I mean we have 88 operations that we support so if we weren't using selectors to specify these things or using selectors to specify for example uh to go back too far um to specify which section of the trace we're in then all of that complexity gets pushed somewhere else I think it's pretty equivalent to determine the evaluation of the selector like choosing which operation you're

performing using the selector and just defining the evaluation domains of the air so you could it just is a immediate translation like the selector function it could be defined precisely by the enforcement domains as well yeah okay so I think I think one of the issues here is that are not issues but one of the reasons that we haven't done that is that we use Winterfell as a prover and Winterfell is sort of set up in this specific way where we it it takes in these inputs it takes in the air constraints and then it does the um denominators itself depending on whether their boundary or transition constraints we don't do that within the VM itself um so maybe if these things weren't decoupled then we would have more flexibility flexibility in doing okay so you're saying that Winterfell doesn't uh

you cannot using Winterfell you cannot um manipulate the denominators you always always have to work with selectors such that the denominator is always the entire domain yeah with Winterfell it is baked in that the denominators are either set for transition constraints or for boundary constraints okay okay we have we are working to make the error script syntax so that you could within airscript not be caught by that same restriction for might and VM we follow that because we use uh Winterfell but aeroscript doesn't necessarily need to adhere to that thank you for talk um maybe I've missed it in the beginning but what's the state

of air script have you had any audits um are you comfortable um working or advising people to use it in production and yeah what's what's what's the state yeah it's still in development um uh we have I have a slide here so um the functions and evaluators are like partially implemented at this point the things on the left are the things that are currently implemented I didn't really talk about constraint selectors that we're adding um or having larger evaluation frames Beyond two rows because we only currently use two rows um but this is essentially where we're at right now we aren't quite using it in production yet but also we aren't our our roll-up isn't live yet we don't have

all those those verifier needs yet um so I would not advise somebody to use it in production yet but if it is something that would be useful and interesting please talk to us and be part of the development and Engineering Process as we finish up the rest of it and say we're within two months we plan to be using it for all of our um for generating the evaluation for all of our River and verifier code hi thanks for the talk um from the point of view of the end user you know uh I mean I mean the language is cool but I could write programs in this language only if I'm familiar a lot with there and it's fine maybe you can say okay this is a new programming

Paradigm and you can learn it but maybe for some I don't know if it's possible maybe for some more internal stuff like I don't know the selector columns other periodic columns to to to hide it from the from the user so if I'm understanding your question correctly you're kind of talking about people who want to like write ZK applications right so I would say this is not like a general purpose DK language this is a specific DSL for writing error constraints so the people who would be using this are people who are like have built a stark prover are using start proving system and are looking for a more maintainable way to manage the internals of their system the people who are looking to write CK

applications are probably going to use something like for us it would be my assembly that actually targets like the virtual machine itself or or something like Noir that compiles two circuits thank you how do you debug this stuff as in are there any tools or techniques that allow you to debug some of the to debug air or to debug our kind of implementation your implementation um I mean it's written in Rust and we I guess use the normal tools for debugging rust for error itself no we don't have debugging tools but and I don't think we plan to because you would need something that understands not only the constraints

that you want to have but also understands constraints deeply I think it's one of these things that you just have to do it manually and read through and check that the constraints make sense and that's why we've aimed to have something that's very readable and modular foreign constraints that we can see uh no okay here yeah I don't have another secret slide with those sorry anyone else I can tell you what they are all right then I would say let's thank

the speaker again thank you