**Home Edition**

# Discussion notes #4.2: AirAssembly: a low-level language for encoding AIR of computations
Presenter: Bobbin Threadbare

Authors:
- Bobbin Threadbare

To be presented on 2020-04-30.

Resources:
* [Latest PDF version](https://docs.zkproof.org/pages/standards/accepted-workshop3/proposal-airAssembly.pdf)
* [Miro Whiteboard](https://zkproof.org/workshop3-board)
* [Working Group](https://community.zkproof.org/g/WG_AIRASSEMBLY)
* [Additional related links](https://hackmd.io/@HtwXZr-PTFCniCs7fWFSmQ/B1AwbdI_8)

----

## Real-time notes
_Note takers:_ Anaïs Querol, Daira Hopwood

> Others are welcome to augment/annotate using notes. Add your name. ---Eran Tromer

Problem statement: Presenting [AirAssembly](https://github.com/GuildOfWeavers/AirAssembly
)

AIR arithmetization
AirAssembly language and examples

We can think of computations in two different ways: circuit computations and machine computations.


AIR main concepts:
* computation state (like values of registers at a given time)
* execution trace (sequence of computation states)
* transition function (relates consecutive states)
* transition constraints (that hold between consecutive states)
* boundary constraints (control states at the start and end of the trace)
* computation state is split into dynamic and static registers
* examples: cyclic and "holey" (repeating at given period) registers

Representation: arith circ vs trans funct
Arithm: R1CS vs AIR
Benefits: easi reduction from gpc and composition vs fast proof generation and verif times
Languages: Snarky Circom ZoKrates vs AirScript, AirAssembly
Used in: most snarks vs starks

**Algebraic Intermediate Representation (AIR)**

Main concepts:
- Computation state: registers
- Execution trace (2dim matrix row captures state of register through time)
- transition function: repeats until the end
- transition constraints: takes consecutive steps and holds if output all zeros
- boundary constraints: specify register at certain time has a value (check steps). essentially the same, but helpful to think of them separately

Execution trace: can have dynamic registers (r0...) and static registers (k0...). Examples: cyclic registers, holey registers

important: trace length must be power of two, static registers can be public or secret

transition function: take current state of static registers and dynamic and produces next step of the dynamic
can apply arithmetic switching as a selector of transition functions

all arith ops allowed, degree grows when registers raised to power, or multiplied, long range transition function work with more than 2 consec states

def transition constraint

d_i = g(s_i, s_i+1, k_i)
frequently just d_i = s_i+1 - f(s_i,k_i)
but can be more complex also
d_i= g1(s_i+1,k_i)-g_2(s_i,k_i)

division not allowed but can be emulated, degree may or not be the same as deg trans fun, long range const work for more than 2 consec states (same as before)

**AirAssembly language**

aims to describe: logic for generating exec trace, for gen const evals, logic for interpreting inputs

AirScript -> AirAssembly -> genSTARK
(source, module, prover/verifier)

not only genstark but can be written in wasm or rust... (genstark is written in javascript)

also airscript could be something different (fooscript, barscript...)

AirAssembly syntax (not for humans). modeled after webassembly.


data types: scalar, vector, matrix
arith ops: add, sub, mul, div, exp, prod, inv,neg
...

vector operations

module
field
constants
functions
components
static registers
trace initializer
transition function
constraiant evaluator

AirAssembly execution

Inputs - build static register traces - execution trace table - apply transition function - execution trace table - evaluate transition constraints -constraint evaluation table

explains how to instantiate registers at initialization time

AirAssembly examples

MiMC arithmetization

$r_{i+1,0} = r_{i,0}^3 + k_{i,0}$

Params: input value 3, static register cycle 1 2 3 4 computation steps 64, field mod 2ˆ32 - e*2ˆ25 + 1 (note 64 is a divisor of field - 1)

shows airassembly code

Trace length must be power of 2.

Transition function: dynamic x static -> dynamic

Can have "long-range" transition functions that work with more than 2 consecutive states.

Degree of the transition constraints is limited.

AirAssembly: capture this arithmetization as an intermediate representation.
{AirScript, ...} -> AirAssembly -> multiple STARK prover/verifiers

genSTARK translates AirAssembly into a combination of WebAssembly and input to STARK prover.

Questions:
* on expressiveness of AIR relative to arithmetic circuits
- equally expressive via use of arithmetic switching, not necessarily equally efficient

Both prover and verifier read the same AirAssembly. Verifier computes on many fewer points.


Discussion:
* First standardization proposal for a front-end. What aspects of front-ends are worth standardizing?
- Markulf: Very specific to a proving system. Can we generalize? Other proof systems exploit batching.

* Ale: Composition is much more complicated for AIR than it is for (say) R1CS. What is the minimal composition infrastructure for AIR? We have to be very "stingy" in the overhead of this infrastructure because we pay a lot for each gate/step.
- Bobbin: the separation between AirScript and AirAssembly makes composition easier.

----
Charter Ideas

Goals:

-

Milestones:

-

----

## Discussion topics

_Suggestions welcome! Please append at the end, and the moderators will incorporate into the schedule._

~15 minutes each, by default.

## Minor questions on talk

* in slide 3: the row called "Languages" should be better renamed to "Frontends"
* in slide 4: rename r_{2,3} to r_{3,2} (typically the index of a row comes before the index of a column)
* in slide 5: any better name than "holey" registers?
*

Markulf: reminds him of arithmetic circuit and in each level you apply the same function iteratively
Bobbin: converting this to an arith circuit wouldnt be very efficient

Justin Thaler: output of airassembly? outputs exec proof matrix?
Bobbin: genstark library understands airassembly and parses and translates source code with javascript and webassembly and then obtains executable code and then generates the stark proof
starks work like inputs exec trace and constr eval compose into polynomial and then lowdeg proof... all this part is done in genstark and does not depend on the input to the genstark (output of airassembly). idea airassembly prepares the input for the genstark.
justin: benefit of stark, avoid preprocessing but restricted to very repeated computations. is there any way to avoid this processing?
bobbin: no preprocessing in starks in fact, both p and v read description (code in airassembly shown before) and then prover generates execution trace, constraint evaluations and all that, but verif only evaluates some queries on some points, 80 points, instead of thousands that the prover does.
justin: tinyram program? there are frontends that do similar things starting tinyram instead of airassembly. pros and cons?
bobbin: airass define constraints of how tiny ram works. (description of that machine in airassemb) and then write programs in whatever language tinyram understands

daira: prover time taken to generate exec trace vs crypto optns?
bobbin: depends on program, but in general time eec trace negl vs ffts have to run. maybe 2 sec in total 80% ffts composing and all but exec trace negl time fraction
daira: similar to witness computation

## Minor questions on document

* The following sentence appears throughout the document: "A handle must start with $ character followed by a letter, and can contain any combination of letters, numbers, and underscores." Maybe define the notion of a handle once, and then you don't have to repeat it every time?
* Why are load and store operations defined in the section "Arithmetic expressions"? Maybe one should move them to a separate section titled "Memory operations".
* Figure 1 and Figure 2 have somewhat confusing notation when compared to the text. Does k_i represent a static register or all static registers at time i? (Likely the latter, but if so then k_0,k_1,k_2,k_3 in the same figure should have names k_{i,0},k_{i,1},k_{i,2},k_{i,3}.)
* Similarly, in text the notation s_i (r_{i,0},r_{i,1},r_{i,2},...) should be defined, for consistency with Fig 2. (And Fig 1 should be modified to add s_i and s_{i+1}.)
* page 09: inconsitency between "initializer" and "trace initializer"

more discussions:

justin: first std proposal of frontend. talk about front ends what is worth standardizing....

markulf: this one is very specific to one proof system, but wonder if exists more abstract and general. feeling something happening here that makes it easier repetition of function, but maybe some systems exploit this fact as well?
bobin: not sure if others would benefit from that. no answer if same could be applicable outside of air but interesting
justin: over and over again avoiding preprocessing or whatever reason, recurring theme in research literature and interesting question if can be standardize instead of being only an idea
daira: plonk, not so similar, but maybe similar to ... plonk configuration selector, polynomial constraints... similar to what is being done here
alessandro chiesa: specific vs generic: historically circuits / r1cs. cryptographers built proof systems for arith or bool circuits 20 years ago. now more proof systems more convenient to go to generalization: r1cs. general in many settings (transp snarks, preprocessing...) empirical dessign decision somehow. here something will happen for machine like computation (for pairing, hash based snarks...). what is the ultimate air formulation that will work for future proof systems? more of an empirical statement.

bobbin: makes sense to do it?: module there to create tree table.

daira: automatization in prover side.

bobbin: doesnt even read transition function. exec trace tradeoff. want to have table as part of the definition?

daira: maybe api to construct relation

bobbin: interesting question. air assembly not composable. working on it. airscript compiles into airassembly. if it could accept many airassembly to merge them into one, but many tradeoffs.

daira: add new registers to check when one module is in?

bobbin: yes, as a selector for these use this transition functions, for others use this other one

daira: registers number maximum number needed for each module

bobbin: everytime you add selector function you add degree because 1 multiplication more and higher degree longer prover to run so biggest issue with composition.

alessandro: analogy with r1cs. two pieces of circuit want to have together all need to do is identify what variables are shared between gadgets. but had no restrictions.
daira: semantically very clean as well
alessandro: starks want comput with lots of structure because want to exploit this structure, so issue, if have heterogenity in computation because trying to put together two types. am i sharing registers? how often are they repeating? annoying. in normal computation we also have assembly code but have o.s. managing processes for us. maybe write minimal operating system and then express computations there. but now overheads. balancing these two things: minimal infrastracture to put together programs with small overhead.

bobbin: airscript tried to do composition but was very limiting. so difficult question, agree

justin: what led you to create this low level high level library, other than c program with less usability?
bobbin: first implemented in ... overhead associated to language. decided to go to minimum amount of needed... that was airassembly. and airscript has many more things you can do such as loops and all. programming easier but if you dont have this airassembly tool then it makes it complicated.

justin: airscript outputs airassembly?
bobbin: yes, airscirpt compiles to airassembly

jamie lokier: airassembly to me reminds me of ... maybe some things done in hardware could optimize?
justin: good research direction

alesandro: bigger matrix but also complexity of transition constraints and important parameter doesnt show up so much is the degree, so pay multiplicatively in that degree. often you allocate more registers to decrease degree. efficient airs wont go over 5-6 degree.

alessandro: document bobbin prepared. opinion of draft describing air assembly, what direction should it go?

daniel benarroch: previous description were more abstract. maybe here more explicit examples and primitives given in airassembly format. focus maybe on commitments...
bobbin: would be glad to give them. language should be powerful enough to not compromise performance.

anais: using examples of primitives or problems such as mimc, pedersens, fibonacci, are really helpful both for understanding how to use airscript but also the functioning of starks themselves

daira: some gadgets efficiently described in starks plonk and other proof systems and optimized for some particular systems. how can we show this in a standard? standards can be huge, huge effort to organize it to make it accessible

bobbin: maybe different could use different standards.

alessandro: such document involve non trivial discussions for a programmer that is richer and more useful than writing r1cs, maybe include types like bobbin asked. it is not trivial, there is a lot to think about

daira: summarize interface rather than

alessandro: many people understand r1cs. one could do the effort to come up with a dsl dsr? that pople could use. similar complexity, there is no dsl for single language

alessandro: if zkp has anything to do with airassembly, then whats the role

eran tromer: difficult task to have unification. instead focused has been to offer interoperability. zkinterface approach. different frontends to collaborate, and populate variable assignments. while maintaining agnosticism what level of abstraction or language was used beneath. challenging part is r1cs very shallow, not have much structure but for air it is much more difficult to come with an abstraction for interoperability.

sky_hard: r1cs combinatorial circuit in design. air clock design. both needed because computers have both. why do we want to choose only one, as a user you dont care which one is working. interested in opinion of others as well.

justin: one reason r1cs unstructured verifiers going to read the whole so could save that step for the efficiency. but could also consider r1cs with more structure.

daira: plonk already is not an unstructured bag of constraints, you can have gates that access previous and next rows

alessandro: theory paper succinct r1cs. imagine r1cs staircase matrix as transition function, think of proof system that use many matrices some are structured some are noto, arbitrary matrices. exploit them if have structure. no structure, then you have to read. smooth connexion between machines and how circuits work

daira: waiting for the right abstraction vs standardize what we have already?

daniel: if std what we already have, will it be flexible enough to reuse and have people not reimplement everything from scratch

jamie lokier: sequentially thinking vs r1cs, tends to lead to produce different types of circuits. suspect both could be translated backwards and forwards, but difficult to automate.

daira: you do have to think differently based on what layout you are following.

jamie lokier: subroutines that call each other?

daira: what we are building here is constraint systems.

jamie lokier: dont mean functions per se but like a macro in the constraint system scenario