Repository files navigation

This library contains specifications and JavaScript runtime for AirAssembly - a language for encoding Algebraic Intermediate Representation (AIR) of computations. AIR is a representation used inzk-STARKs to construct succinct proofs of computational integrity.

AirAssembly is a low-level language and is intended to be a compilation target for other, higher-level, languages (e.g.AirScript). It uses a simple s-expression-based syntax to specify:

1. Inputs required by the computations.
2. Logic for generating execution traces for the computations.
3. Logic for evaluating transition constraints for the computations.
4. Metadata needed to compose the computations with other computations.

Full specifications for AirAssembly can be foundhere.

This library is not intended for standalone use, but is rather meant to be a component used in STARK provers/verifiers (e.g.genSTARK). Nevertheless, you can install it separately like so:

$ npm install @guildofweavers/air-assembly --save

Once installed, you can use the library to compile AirAssembly source code into AirModules, and then use these modules to generate execution trace tables and constraint evaluation tables for computations.

The code below illustrates how to do this on the example of aMiMC computation. Other examples can be foundhere.

import{compile,instantiate}from'@guildofweavers/air-assembly';constsource=`(module    (field prime 4194304001)    (const $alpha scalar 3)    (function $mimcRound        (result vector 1)        (param $state vector 1) (param $roundKey scalar)        (add            (exp (load.param $state) (load.const $alpha))            (load.param $roundKey)))    (export mimc        (registers 1) (constraints 1) (steps 32)        (static            (cycle (prng sha256 0x4d694d43 32)))        (init            (param $seed vector 1)            (load.param $seed))        (transition            (call $mimcRound (load.trace 0) (get (load.static 0) 0)))        (evaluation            (sub                (load.trace 1)                (call $mimcRound (load.trace 0) (get (load.static 0) 0))))))`;// instantiate AirModule objectconstschema=compile(Buffer.from(source));constair=instantiate(schema,'mimc');// generate trace tableconstcontext=air.initProvingContext([],[3n]);consttrace=context.generateExecutionTrace();// generate constraint evaluation tableconsttracePolys=air.field.interpolateRoots(context.executionDomain,trace);constconstraintEvaluations=context.evaluateTransitionConstraints(tracePolys);

Complete API definitions can be found inair-assembly.d.ts. Here is a quick overview of the provided functionality.

The library exposes a small set of functions that can be used to compile AirAssembly source code, instantiate AirModules, and perform basic analysis of the underlying AIR. These functions are:

• compile(source:Buffer |string, limits?:StarkLimits):AirSchema
  Parses and compiles AirAssembly source code into anAirSchema object. Ifsource parameter is aBuffer, it is expected to contain AirAssembly code. Ifsource is astring, it is expected to be a path to a file containing AirAssembly code. Iflimits parameter is provided, generatedAirSchema will be validated against these limits.

• instantiate(schema:AirSchema, component:string, options?:ModuleOptions):AirModule
  Creates anAirModule object for the specifiedcomponent within the providedschema. TheAirModule can then be used to generate execution trace tables and evaluate transition constraints. The optionaloptions parameter can be used to control instantiation of theAirModule.

• instantiate(schema:AirSchema, options?:ModuleOptions):AirModule
  An overloaded version of theinstantiate() function withcomponent name assumed to equal "default". If the providedschema does not have a default component export, an error will be thrown.

• analyze(schema:AirSchema, component:name):SchemaAnalysisResult
  Performs basic analysis of thecomponent within the providedschema to infer such things as degree of transition constraints, number of additions and multiplications needed to evaluate transition function etc.

When instantiating anAirModule object, anAirModuleOptions object can be provided to specify any of the following parameters for the module:

StarkLimits object defines limits against whichAirSchema andAirModule objects are validated.StarkLimits objects can contain any of the following properties:

To generate an execution trace for a computation defined by AirAssembly source code, the following steps should be executed:

1. Compile AirAssembly source code intoAirSchema using the top-levelcompile() function.
2. Pass the resultingAirSchema to the top-levelinstantiate() function to create anAirModule. You'll also need to specify the name of theAirComponent exported from theAirSchema becauseAirModules are instantiated for a specific component.
3. Create aProvingContext by invokingAirModule.initProvingContext() method. If the computation contains input registers, then input values for these registers must be passed to theinitProvingContext() method. This instantiates theProvingContext for a specific set of inputs.
4. Generate the execution trace by invokingProvingContext.generateExecutionTrace() method.

The code block bellow illustrates these steps:

constschema=compile(Buffer.from(source));constair=instantiate(schema,`mimc`,{extensionFactor:16});constcontext=air.initProvingContext([],[3n]);consttrace=context.generateExecutionTrace();

In the above:

• source is a string variable containing AirAssembly source code similar to the one shown in theusage section.
• TheAirModule is instantiated for the exportedmimc component using default limits but setting extension factor to16.
• An empty inputs array is passed as the first parameter to theinitProvingContext() method since the computation shown in theusage section does not define any input registers.
• A seed array with value3 is passed as the second parameter to theinitProvingContext() method sincecomponent initializer expects a vector parameter to initialize the first row of the execution trace.
• After the code is executed, thetrace variable will be amatrix with 1 row and 32 columns (corresponding to 1 register and 32 steps).

The execution trace for the single register will look like so:

[             3, 1539309651, 3863242857, 3506640509, 1371547896, 215222094,  220283781,  2120321425,    2290167095, 3044083866, 3673976270, 2694057310,  995327947, 2470701222, 798926004,  2416031839,     4124930959,  680273881,  115120944, 2405022753,  963841868, 327198005,  34356700,   1065113318,    2951801258,  791752781, 1878966595, 2503692690, 1792666246, 3884924604, 3800788053, 2681237718]

Transition constraints described in AirAssembly source code can be evaluated either as a prover or as a verifier. Both methods are described below.

When generating a STARK proof, transition constraints need to be evaluated at all points of the evaluation domain. This can be done efficiently by invokingProvingContext.evaluateTransitionConstraints() method. To evaluate the constraints, the following steps should be executed:

1. Create a proving context and generate an execution trace as described in theprevious section.
2. Generate a set of trace polynomials by interpolating execution trace columns over the execution domain.
3. Evaluate the constraints by invokingProvingContext.evaluateTransitionConstraints() method and passing trace polynomials to it.

The code block bellow illustrates steps 2 and 3:

consttracePolys=air.field.interpolateRoots(context.executionDomain,trace);constconstraintEvaluations=context.evaluateTransitionConstraints(tracePolys);

In the above:

• AirModule'sfield object is used to interpolate the execution trace. TheinterpolateRoots() method takes a vector ofx values as the first parameter, and a matrix ofy values as the second parameter (the matrix is expected to have a distinct set ofy values in each row). The output is a matrix where each row contains an interpolated polynomial.
• evaluateTransitionConstraints() method returns amatrix where each row corresponds to a transition constraint evaluated over the composition domain.

For example, evaluating constraints for AirAssembly code from theusage section, will produce a matrix with a single row containing the following values:

[    0, 1888826267,  934997684,  522697873,         0, 3636300716,  301925789,  369141145,    0,  767283131,  270628806, 1668446351,         0, 1739694248, 3247199818, 2569615536,    0,   44729160, 4039819553, 3564072931,         0, 1616917451, 1151293301, 3209868277,    0, 3410907990, 4004509077, 4190379432,         0, 3101507817, 3553581961, 2793433224,    0,  330772896, 4060647779, 2512435701,         0, 3403188821,  235591542, 3772363484,    0, 2256420389, 2357121513,   61957993,         0, 3272390069,  197242509, 2878395132,    0,  155740407,  298885317, 3310802262,         0,   19161130,  691333255, 1102311751,    0, 1751005830, 2349558192, 3473961491,         0, 4006336837,  565227775, 4021023132,    0, 3315940573,  989407555, 2088778801,         0,  898450568, 3610287112, 3576441219,    0,  326707597, 2532917782, 3330991749,         0, 4162556873, 1554019377, 4171366685,    0,  984976271, 2011763604,  728626530,         0, 3611841258, 2245193661, 2605704194,    0, 2583926003, 3992303847, 2748879594,         0, 2379703446,  430289311, 3052280185,    0,  179547660, 1215051408, 2628504587,         0, 2862551083, 2740849758,  925951430,    0, 4000243259,  913649599, 1118200600,         0, 1484209861, 1897468182,  190582872,    0, 4135707956, 1007284323, 2027805646,         0, 1310083809, 2946378676,  350300836,    0, 3019962854, 1468795609, 1874742277, 803208359, 4116321517, 3116095172,   77399359]

Note: The constraints are evaluated over the composition domain (not evaluation domain). The evaluations can be extended to the full evaluation domain by interpolating them over the composition domain, and then evaluating the resulting polynomials over the evaluation domain. But in practice, to improve performance, the evaluations are first merged into a single vector via random linear combination, and then this single vector is extended to the full evaluation domain.

When verifying a STARK proof, transition constraints need to be evaluated at a small subset of points. This can be done by invokingVerificationContext.evaluateConstraintsAt() method which evaluates constraints at a single point of evaluation domain. To evaluate constraints at a single point, the following steps should be executed:

1. Compile AirAssembly source code intoAirSchema using the top-levelcompile() function.
2. Pass the resultingAirSchema together with exported component name to the top-levelinstantiate() function to create anAirModule.
3. Create aVerificationContext by invokingAirModule.initVerificationContext() method. If the computation contains input registers, input shapes for these registers must be passed to theinitVerificationContext() method. If any of the input registers are public, input values for these registers must also be passed to the method.
4. Evaluate constraints by invokingVerificationContext.evaluateConstraintsAt() method and passing to it an x-coordinate of the desired point from the evaluation domain, as well as corresponding values of register traces.

The code block bellow illustrates these steps:

constschema=compile(Buffer.from(source));constair=instantiate(schema,'mimc',{extensionFactor:16});constcontext=air.initVerificationContext();constx=air.field.exp(context.rootOfUnity,16n);constrValues=[1539309651n],nValues=[3863242857n];constevaluations=context.evaluateConstraintsAt(x,rValues,nValues,[]);

In the above:

• source is a string variable containing AirAssembly source code similar to the one shown in theusage section.
• TheAirModule formimc component is instantiated using default limits but setting extension factor to16.
• No input shapes or inputs are passed to theinitVerificationContext() method since the computation shown in theusage section does not define any input registers.
• x is set to the 17th value in of the execution domain, whilerValues andnValues contain register traces for 2nd and 3rd steps of the computation. This is because when the extension factor is16, the 2nd value of the execution trace aligns with the 17th value of the evaluation domain.
• After the code is executed, theevaluations variable will be an array with a single value0. This is because applying transition function to value1539309651 (current state of the execution trace) results in3863242857, which is the next state of the execution trace.

AnAirSchema object contains a semantic representation of AirAssembly source code. This representation makes it easy to analyze the source code, and serves as the basis for generatingAirModules. AnAirSchema object can be created by compiling AirAssembly code with the top-levelcompile() function.

AirSchema has the following properties:

Note: definitions forConstant andAirFunction objects mentioned above can be found inair-assembly.d.ts file.

AnAirComponent object is a semantic representation of a specific computation contained withinAirSchema. That is, a singleAirSchema object can contain manyAirComponents each describing a distinct computation. This allows packaging AIR of many computations into a single physical file.

AirComponent has the following properties:

Note: definitions forStaticRegister,AirProcedure, andConstraintDescriptor objects mentioned above can be found inair-assembly.d.ts file.

AnAirModule object contains JavaScript code needed to createProvingContext andVerificationContext objects. These objects can then be used to generate execution trace and evaluate transition constraints for a computation. AnAirModule can be instantiated for a specific component of anAirSchema by using the top-levelinstantiate() function.

AirModule has the following properties:

AirModule exposes the following methods:

• initProvingContext(inputs?:any[], seed?:bigint[]):ProvingContext
  Instantiates aProvingContext object for a specific instance of the computation. This context can then be used to generate execution trace table and constraint evaluation table for the computation.

  • inputs parameter must be provided only if the computation containsinput registers. In such a case, the shape of input objects must be in line with the shapes specified by the computation's input descriptors.
  • seed parameter must be provided only if thetrace initializer for the computation expects a vector parameter.

• initVerificationContext(inputShapes?:InputShape[], publicInputs?:any[]):VerificationContext
  Instantiates aVerificationContext object for a specific instance of the computation. This context can then be used to evaluate transition constraints at a given point of the evaluation domain of the computation. If the computation containsinput registers,inputShapes parameter must be provided to specify the shapes of consumed inputs. If any of the input registers are public,publicInputs parameter must also be provided to specify the actual values of all public inputs consumed by the computation.

AProvingContext object contains properties and methods needed to help generate a proof for a specific instance of a computation. Specifically, aProvingContext can be used to generate an execution trace for a specific set of inputs, and to evaluate transition constraints derived form this trace. To create aProvingContext, useinitProvingContext() method ofAirModule object.

ProvingContext has the following properties:

ProvingContext exposes the following methods:

• generateExecutionTrace():Matrix
  Generates an execution trace for a computation. The return value is amatrix where each row corresponds to a dynamic register, and every column corresponds to a step in a computation (i.e. the number of columns will be equal to the length of the execution trace).

• evaluateTransitionConstraints(tracePolys:Matrix):Matrix
  Evaluates transition constraints for a computation. ThetracePolys parameter is amatrix where each row represents a polynomial interpolated from a corresponding register of the execution trace. The return value is amatrix where each row represents a transition constraint evaluated over the composition domain.

AVerificationContext object contains properties and methods needed to help verify a proof of an instance of a computation (i.e. instance of a computation for a specific set of inputs). Specifically, aVerificationContext can be used to evaluate transition constraints at a specific point of an evaluation domain. To create aVerificationContext, useinitVerificationContext() method ofAirModule object.

VerificationContext has the following properties:

VerificationContext exposes the following methods:

• evaluateConstraintsAt(x:bigint, rValues:bigint[], nValues:bigint[], sValues:bigint[]):bigint[]
  Returns an array of values resulting from evaluating transition constraints at pointx. For example, if the computation is defined by a single transition constraint, an array with one value will be returned. The meaning of the parameters is as follows:
  • x is the point of the evaluation domain corresponding to the current step of the computation.
  • rValues is an array of dynamic register values at the current step of the computation.
  • nValues is an array of dynamic register values at the next step of the computation.
  • sValues is an array of secret register values at the current step of the computation.

AnInputDescriptor object contains information about aninput register defined for the computation.

InputDescriptor has the following properties:

MIT © 2019 Guild of Weavers