Constraint description language

[bobbinth]

As we write more and more constraints, it becomes clear that some tools to help with this task are needed. Our current approach is to write constraints directly in Rust. This creates a few challenges:

1. The readability suffers greatly. Meaning, it takes a lot of time to read Rust code and understand what is actually going on. For people who are not familiar with Rust, reading constraints this way is probably prohibitively expensive.
2. Modifying constraints which are in place becomes challenging because multiple places usually need to be updated and tracking all of them down takes effort.
3. A lot of optimizations are left on the table. This is primarily driven by the desire to retain some readability and maintainability.

It would be really nice if we had a tool which could be used to write constraints in human-readable form (or as close to this as possible), and then this tool would perform algebraic optimizations (e.g., to minimize number of multiplications) and output very performant Rust code.

Some of my current thoughts on potential properties of this tool:

1. Describing constraints should be as close to writing actual formulas as possible.
2. We don't need to support full power of AIR (at least for now). For example, we can limit transition constraints to two consecutive rows. In terms of AIR "features", here is what I think we need at the minimum:
   a. Transition constraints (over two consecutive rows).
   b. Boundary constraints (at least on the first and the last rows).
   c. Multiset checks (using just one additional trace segment).
   d. Periodic columns.
3. The tool should have the following high-level features:
   a. We should be able to write constraints in a modular way. For example, one module for memory constraints, another module for decoder constraints etc.
   b. The tool should be able to infer degrees of transition constraints automatically.
   c. It would be really nice if the tool could output code for prover and verifier separately - so that it would be possible to take advantage of optimizations only possible in the base field. Though, maybe this could be a feature which gets added later on.
4. We could implement the tool using Rust macros or as a stand-alone parser/emitter, but I think the important thing to have is that constraint descriptions should be accessible to people who don't know Rust.

Below are some sketches of how describing constraints could look like.

state: [ctx, addr, clk, u0, u[4], v[4], d0, d1, t]

let n0 = (ctx' - ctx) * t
let n1 = (addr' - addr) * t

enf n0^2 - n0 = 0
enf (1 - n0) * (ctx' - ctx) = 0
enf (1 - n0) * (n1^2 - n1) = 0
enf (1 - n0) * (1 - n1) * (addr' - addr) = 0

for i in 0..4
    enf (n0 + (1 - n0) * n1) * u'[i] = 0
    enf (1 - n0) * (1 - n1) * (u'[i] - u[i]) = 0

The above describes a subset of memory co-processor constraints. Most of the things should be self-explanatory, but to give a few clarifications:

• let keyword defines a variable, enf keyword enforces a constraint
• $x'$ notation is used to refer to the value in the next row. For example, ctx is value in the current row of column ctx, but ctx' is the value in the next row.

Here is another example to show how modular approach could work:

use: hasher, bitwise, memory

state: [s0, s1, s2, ..15]

enf s0^2 - s0 = 0
enf s0 * (s1^2 - s1) = 0
enf s0 * s1 * (s2^2 - s2) = 0

with 
    s0 enf hasher [1..18]
    (1 - s0) * s1 enf bitwise [2..18]
    (1 - s0) * (1 - s1) * s2 enf memory [3..18]

In the above, hasher, bitwise, and memory are separate modules.

[jan-ferdinand]

Both the description and the examples remind me of vamp-ir. Perhaps the similarities are enough to join forces?

[spartucus]

A similar project is openzl.

[bobbinth]

A few more thoughts on the potential structure of the constraint description file.

Such a file could consist of several sections. A couple come to mind:

• Declaration section: in this section we would define the shape of the expected trace, name and/or define relevant columns.
• Constraint section: in this section we'd define all transition and boundary constraints using column names specified in the declaration section.

Declaration section

In the declaration section we need to define the set of columns we would be working with in both transition and boundary constraint sections. There are 3 sources of columns:

• Main trace columns.
• Auxiliary trace columns.
• Periodic columns.

We could use a variation of destructuring syntax in many languages to name columns from various sources. To give a few examples:

declare:
    main: [a, b]

The above says that the main execution trace should consist of 2 columns, and these columns could be referred to as a and b.

In some cases, we may not need to name all columns. For example:

declare:
    main: [a, b, ..2]

The above says that main trace should consist of 4 columns, but only the first two columns are named.

In many situations it may be useful to group some columns together. We could use the following syntax for that:

declare:
    main: [a, b, c[4], ..2]

The above says that the main trace should consist of 8 columns: individual columns a and b, a group of 4 columns under the name c, and 2 unnamed columns.

Of course, we could declare a single variable to refer to the entire state like so:

declare:
    main: [m[8]]

We could name columns from the auxiliary trace in the same manner as columns of the main trace:

declare:
    main: [a, b, ..2]
    aux: [c, d]

In the above, the main should consist of 4 columns while the auxiliary trace should consist of 2 columns named c and d.

To add periodic columns, we could use const keyword and provide the cycles of values used to define these columns. For example:

declare:
    main: [a, b, ..2]
    aux: [c, d]
    const k1: [0, 1, 2, 3]
    const k2: [0, 0, 0, 0, 0, 0, 0, 1]

In the above, we define 2 periodic columns: the first one with a cycle length of 4 values, and the second one with the cycle length of 8 values.

Another approach could be to break periodic column declaration into a separate section. For example:

trace_columns:
    main: [a, b, ..2]
    aux: [c, d]

periodic_columns:
    k1: [0, 1, 2, 3]
    k2: [0, 0, 0, 0, 0, 0, 0, 1]

It might also be useful to allow declaration of periodic columns in groups like so:

trace_columns:
    main: [a, b, ..2]
    aux: [c, d]

periodic_columns:
    k1: [
        [0, 1, 2, 3],
        [4, 5, 6, 7],
    ]
    k2: [0, 0, 0, 0, 0, 0, 0, 1]

Periodic columns declared in the same group must have the same length.

Constraints section

In the constraints section, we would define the actual constraints using column names defined in the declaration section. A few thoughts about potential notation:

• To refer to the next value in a given column we could use "prime" notation. For example, a' is the next value in column a. This notation would be applicable only to columns of the main and auxiliary trace.
• To specify a constraint, we could use an enf keyword followed by the constraint itself.
• To define an intermediate variable, we could use a let keyword.

A few examples:

// declaration section
// --------------------------------------------------------------------------------

trace_columns:
    main: [a, b, c[4]]

periodic_columns:
    k1: [0, 1, 2, 3]
    k2: [0, 0, 0, 0, 0, 0, 0, 1]

// constraints section
// --------------------------------------------------------------------------------

// values in column a must be binary
enf a^2 - a = 0

// next value of b must be a sum of the values in the first two c columns
enf b' = c[0] + c[1]

// next value in the first c column must be a product of values in the last two c columns
enf c[0]' = c[2] * c[3]

// define x as the product of the current value in periodic column k1 and the next value in the second c column
let x = k1 * c[1]'

// use x in the constraint definition; not that for x, trying to refer to x' would not be valid
enf c[3]' = b * x

We could use the above approach to work with auxiliary columns too. However, for auxiliary columns we also work with random values (provided by the verifier after the prover commits to the main trace), and the question arises as to how to refer to them. One option is to use some symbol - e.g., $ or &. Another option is to use some reserved variable - e.g., rand or alphas.

If we go with the symbol approach, constraint declaration could look as follows:

trace_columns:
    main: [a, b]
    aux: [c]

// &0, &1, &2 are the random values provided by the verifier
let v = &0 + &1 * a + &2 * b
enf c' = c * v

To enforce boundary constraints, we could use an assert keyword. Also, to simplify things for now, we could say that boundary constraints can be imposed only against the first and the last value of a column. For example:

trace_columns:
    main: [a, b]
    aux: [c]

let v = &0 + &1 * a + &2 * b
enf c' = c * v

assert c.first = 1
assert c.last = 1

I think the above probably covers 60% - 70% of what we need. But a few open questions remain:

• What's the best way to iterate over grouped columns?
• How to provide dynamic values for boundary constraints?
• How to simplify application of selectors to sets of constraints?
• How to define constraints in a modular way (e.g., importing constraint from one module into another module)?
• How to provide specialized external routines for some computations (e.g. MDS matrix multiplication)?
• What's the best way to support constants - both scalar and otherwise?

[bobbinth]

Regarding modularity, I think what I sketched out in my original post could work.

Specifically, we use the use keywords to specify external modules and then can invoke this modules using the enf keywords.

For example, let's say we have a module bar defined as follows:

trace_columns:
  main: [a, b, c]
  aux: [d]

enf a' = b + c
enf d' = d * (&0 + a)

Let's also say we have a module foo from which we'd like to invoke `bar. We could do this as follows:

use: bar

trace_columns:
  main: [a, b, c, d]
  aux: [e, f]

enf bar(main[0..2], aux[0..1])

Since the expected number of main and auxiliary columns for foo and bar are different, we need to specify which columns from foo are to be passed to bar. We do this using range notation (i.e., main[0..2]).

If the number of columns were the same, we could have done something like:

enf bar(main, aux)

Or if bar didn't require any auxiliary columns, we could do something like:

enf bar(main[0..3])

[grjte]

If we're using this type of range notation, then I think it should be inclusive of the beginning but exclusive of the end, since that's pretty standard. I think this is the intention, but I just want to clarify because it's not consistent above, where I believe we would want to pass main[0..3] to bar.

[bobbinth]

Yep - that was the intention but I was sloppy in many places.

[bobbinth]

One more thought about constants and variables: I think it would make sense to allow constants and variables of 3 different types:

• scalars
• vectors
• matrixes.

Declaring constants could be done like so:

constants:
  a: 123 // a scalar constant
  b: [1, 2, 3] // a vector constant
  c: [
    [1, 2, 3],
    [4, 5, 6],
  ] // a matrix constant

Referring to these constants inside expressions could be done with index notation:

let x = b[1]
let y = c[0][2]

Something like this could also be possible:

let x = c[1][1..3] // this sets x to [5, 6]

We could build variables from column references as well:

trace_columns:
  main: [a, b]

let x = [a, b]   // x is a vector with current values from a and b
let y = [a', b'] // y is a vector with next values from a and b

[Al-Kindi-0]

Should this be "let x = c[1][1..3] // this sets x to [5, 6]" instead?

[bobbinth]

Yes! Fixed!

[bobbinth]

It may be desirable to have support for simple functions. This could be beneficial for two reasons:

1. Provides a good way to encapsulate some commonly repeated logic.
2. Provides a good way to support external routines.

A good example for this could be MDS matrix multiplication for Rescue Prime constraints. This function needs to be called twice, and in the context of the prover, we could use a much more efficient routine to perform the multiplication (because we know we are in the base field).

To make this feature as simple as possible, we could impose the following limitations:

• Functions are always pure - i.e., there are no side effects.
• Function parameters can be only variables (scalars, vectors, matrixes) - i.e., passing columns to functions is not allowed.

A function declaration could look as follows:

fn apply_mds(state: vector[12]) -> vector[12]:
  // function body goes here

This function takes a vector of 12 elements as a parameter, and returns a vector of 12 elements. To invoke this function, we could do something like this:

trace_columns:
  main: [state[12]]

let x = apply_mds(state)

To support external subroutines, we could use something similar to Rust's attributes. For example:

#[prover("mds.rs")]
fn apply_mds(state: vector[12]) -> vector[12]:
  // function body goes here

The above would mean that when compiling the constraints in the context of the prover, instead of using the body of the function, an apply_mds function from the mds.rs file should be used. The signature of that function would have to be:

fn apply_mds(state: [Felt; 12]) -> [Felt; 12];

However, when the constraints are compiled in the context of the verifier, the body of the function would be used as is.

Summary

Summarizing the last several comments: the above probably covers 80% - 85% of what we need. Obviously, these are just sketches, and I'm sure things can be improved (and I probably have some inconsistencies here and there). However, the outstanding big questions in my mind now are:

• What's the best way to iterate over grouped columns?
• How to provide dynamic values for boundary constraints?
• How to simplify application of selectors to sets of constraints?

[bobbinth]

Regarding iteration: since we are always dealing with lists of known length, I'm inclined to restrict iteration to something similar to Python style list comprehension. For example, if we want to iterate over a list of columns and raise each element to some power, we could do it like this:

trace_columns:
  main: [a, b, c[4]]

// raise value in the current row to power 7
let x = [col^7 for col in c]

// raise value in the next row to power 7
let y = [col'^7 for col in c]

In both cases, the result would be a vector of 4 elements.

We could also iterate over two lists simultaneously like so:

trace_columns:
  main: [a, b, c[4], d[4]]

let diff = [x - y for (x, y) in (c, d)]

If the lists have different number of items, we could use range notation to make sure the number of items to iterate over is the same:

trace_columns:
  main: [a, b, c[4], d[5]]

let diff = [x - y for (x, y) in (c, d[1..5])]

If we wanted to iterate over items and enumerate them, we could do it like so:

trace_columns:
  main: [a, b, c[4]]

let x = [2^i * c for (i, c) in (0..3, c)]

We could also support list folding. For example:

trace_columns:
  main: [a, b, c[4], d[4]]

// compute sum of products of values in c and d
let x += c * d for (c, d) in (c, d)

// compute product of sums of values in c and d
let y *= c + d for (c, d) in (c, d)

Or, an alternative syntax could be:

trace_columns:
  main: [a, b, c[4], d[4]]

// compute sum of products of values in c and d
let x = sum([c * d for (c, d) in (c, d)])

// compute product of sums of values in c and d
let y = prod([c + d for (c, d) in (c, d)])

With this, we have enough tools to write constraints for something like Rescue Prime hash function. Such constraints would look like so:

trace_columns:
  main: [state[12]]

periodic_columns:
  ark1: [
    /* 12 periodic column definitions */
  ]
  ark2: [
    /* 12 periodic column definitions */
  ]

constants:
  mds: [
    /* 12x12 matrix */
  ],
  inv_mds: [
    /* 12x12 matrix */
  ]

#[prover("mds.rs")]
fn apply_mds(state: vector[12]) -> vector[12]:
  [
    sum([m * s for (m, s) in (mds_row, state)])
    for mds_row in mds
  ]

fn apply_inv_mds(state: vector[12]) -> vector[12]:
  [
    sum([m * s for (m, s) in (inv_mds_row, state)])
    for inv_mds_row in inv_mds
  ]

let s1 = [x^7 for x in state]
let s1 = apply_mds(s1)
let s1 = [x + k for (x, k) in (s1, ark1)]

let s2 = [x' + k for (x, k) in (state, ark2)]
let s2 = apply_inv_mds(s2)
let s2 = [x^7 for x in s2]

enf x = y for (x, y) in (s1, s2)

[Al-Kindi-0]

"sum(" missing a parenthesis I believe.

[bobbinth]

Thanks! Fixed!

[bobbinth]

One alternative to the structure described previously is to introduce "evaluator" functions which would take the description of main and auxiliary traces as parameters. So, instead of doing something like this:

trace_columns:
    main: [a, b, ..2]
    aux: [c, d]

enf a' = a + b

We could do something like this:

ev foo(main: [a, b, ..2], aux: [c, d]):
  enf a' = a + b

One advantage of this approach is that we can name evaluator functions and then invoke them from other places. For example:

ev foo(main: [a, b, ..2], aux: [c, d]):
  enf bar(main[0..2])
  // some other constraints

ev bar(main: [a, b]):
  enf a' = a + b

Rescue Prime constraints in this format could look something like this:

rescue.air
--------------------
cycl ark1 = [
  /* 12 periodic column definitions */
]
cycl ark2 = [
  /* 12 periodic column definitions */
]

const mds = [
  /* 12x12 matrix */
]
const inv_mds = [
  /* 12x12 matrix */
]

#[prover("mds.rs")]
fn apply_mds(state: vector[12]) -> vector[12]:
  [
    sum([m * s for (m, s) in (mds_row, state)])
    for mds_row in mds
  ]

fn apply_inv_mds(state: vector[12]) -> vector[12]:
  [
    sum([m * s for (m, s) in (inv_mds_row, state)])
    for inv_mds_row in inv_mds
  ]

ev rescue_prime(main: [state[12]]):
  let s1 = [x^7 for x in state]
  let s1 = apply_mds(s1)
  let s1 = [x + k for (x, k) in (s1, ark1)]

  let s2 = [x' + k for (x, k) in (state, ark2)]
  let s2 = apply_inv_mds(s2)
  let s2 = [x^7 for x in s2]

  enf x = y for (x, y) in (s1, s2)

And then we could invoke them from another constraint file like so:

hasher.air
--------------------
use rescue::rescue_prime

ev hasher(main: [s[3], r, h[12], idx]):
  enf rescue_prime(h)

[grjte]

Here are some preliminary thoughts not addressing the bigger outstanding questions yet. It doesn't really include thoughts on the latest comment yet either

Describing constraints should be as close to writing actual formulas as possible.

In a similar vein, I'd like things being as easy to read as possible, especially since we're thinking of this for purposes of auditing as well as for simplifying the writing process. Ideally, people should be able to read it without referencing a spec (especially if they're generally familiar with constraints).

On that note, I propose:

• use enforce instead of enf. I don't think the length makes much difference, but it's much more readable imo
• I prefer having a separate section for periodic_columns or using a specific keyword like periodic rather than const
• I think we should use a keyword rather than a symbol for the alphas, but if we do use a symbol I don’t think we should use & since it looks like a reference. I would probably prefer to use rand and we could perhaps index it, which would feel consistent with the other syntax. For example rand[0], rand[1], etc.
• I prefer the "alternate syntax" for list folding with the explicit sum() and prod()
• Regarding the latest comment, I would prefer a more explicit keyword than ev (similar to enf vs enforce)

A few other thoughts without real suggestions:
It sort of feels like trace column names should be different from constant names. I think being able to distinguish between them at a glance in the constraint descriptions could be useful. Maybe even something as simple as using capitals (although I know that has another meaning for us in the VM).

I think that the enumeration version of the list comprehension is a bit less readable than the others. (Not saying it’s hard - it just feels a bit less natural, maybe because we’re mixing Rust and Python syntax). Since we’re using python syntax maybe something like range() would make sense. We could even make it fully explicit with start and end e.g. let x = [2^i * c for (i, c) in (range(0,3), c)]. (This is just off the top of my head though.)

Also, with the current enumeration, does this mean we only take as many items as are included in the range? Or would we fail when there’s a mismatched number like in the example let x = [2^i * c for (i, c) in (0..3, c)]

[bobbinth]

Thank you! Some thoughts below:

use enforce instead of enf. I don't think the length makes much difference, but it's much more readable imo

I think this is fine, but then we need to be consistent - e.g., use function instead of fn etc.

I prefer having a separate section for periodic_columns or using a specific keyword like periodic rather than const

If we go with my latest version and use full names, I think periodic is the best option. So, it would look like:

periodic foo = [1, 0, 0, 0];

I think we should use a keyword rather than a symbol for the alphas,

Agreed. I think we should go with rand. One question is whether we want to prefix this reserved variables with something - e.g., $rand, $main, $aux vs. just rand, main, aux.

I prefer the "alternate syntax" for list folding with the explicit sum() and prod()

Agreed. It is easier to use in nested context.

It sort of feels like trace column names should be different from constant names.

I was thinking about it too. Using capital letters is fine - though, if we use more than just a few letters, words with capital letters will look a bit strange. Another option is to prefix columns with some special symbol - e.g. $ or # or & etc.

with the current enumeration, does this mean we only take as many items as are included in the range? Or would we fail when there’s a mismatched number

I was thinking we'd fail to avoid accidental errors.

[Al-Kindi-0]

Agreed. I think we should go with rand. One question is whether we want to prefix this reserved variables with something - e.g., $rand, $main, $aux vs. just rand, main, aux.

I am in favor of using $ for the random challenges as this is a very suggestive notation that is also widely used in cryptography papers.
More generally, I think that the idea of "decorating" alphabets with special symbols might be a fruitful one in order to communicate the functionality/role that a given letter plays in a certain context. I am not totally sure but I believe that the notation for next row element given by ' as in a' follows this pattern. The only problem I see here is how to make this pattern uniform (almost) everywhere.

[bobbinth]

A few thoughts on using selectors. Frequently, we want to apply some set of constraints only if some condition is true. For example, for Rescue Prime constraints used above, we usually want to apply them only on the first 7 steps of an 8 step cycle. This, of course, could be baked into the constraints themselves, but that would make them much less readable and modular.

So, I think some syntax which will help with applying selectors could be very helpful. Here are preliminary sketches on how this could work.

Single selector

First, if we have just a single selector, we could do something like this:

// define a cyclic column consisting of 7 ones and 1 zero.
cycl k0 = [1, 1, 1, 1, 1, 1, 1, 0]

ev foo(main: [a, b, c]):
  enf bar([a, b]) when k0

ev bar(main: [a, b]):
  enf a' = a + b

The above specifies that to all constraints returned from bar evaluator would be multiplied by k0. Specifically, the final constraint would be:

$$ k_0 \cdot (a' - a - b) = 0 $$

We could also have the compiler check whether $k_0$ is binary and output either an error or a warning if it isn't.

Multi selector

While we should be able to describe everything using single selectors, frequently it could be much more convenient to specify that one out of several constraints should apply in a given situation. For this, we could use something like that:

ev foo(main: [a, b, c]):
  // make sure values in a are either ones or zeros
  enf a^2 = a

  match enf:
    bar_add([b, c]) when a
    bar_mul([b, c]) when 1 - a

ev bar_add(main: [a, b]):
  enf a' = a + b

ev bar_mul(main: [a, b]):
  enf a' = a * b

The above would translate into the following constraint:

$$ a \cdot (b' - b - c) + (1 - a) \cdot (b' - b \cdot c) = 0 $$

We could also have the compiler check whether all when conditions are mutually exclusive and output an error or a warning if they are not.

The above methodology would also work if evaluators return different number of constraints. For example:

ev foo(main: [a, b, c]):
  // make sure values in a are either ones or zeros
  enf a^2 = a

  match enf:
    bar_add([b, c]) when a
    bar_mul([b, c]) when 1 - a

ev bar_add(main: [a, b]):
  enf a' = a + b

ev bar_mul(main: [a, b]):
  enf a' = a * b
  enf b' = a

The above would translate to two constraints:

$$ a \cdot (b' - b - c) + (1 - a) \cdot (b' - b \cdot c) = 0 $$

$$ (1 - a) \cdot (c' - b) = 0 $$

And if some constraints are redundant, the compiler can simplify those constraints very easily. For example:

ev foo(main: [a, b, c]):
  // make sure values in a are either ones or zeros
  enf a^2 = a

  match enf:
    bar_add([b, c]) when a
    bar_mul([b, c]) when 1 - a

ev bar_add(main: [a, b]):
  enf a' = a + b
  enf b' = a

ev bar_mul(main: [a, b]):
  enf a' = a * b
  enf b' = a

Would translate to something like:

$$ a \cdot (b' - b - c) + (1 - a) \cdot (b' - b \cdot c) = 0 $$

$$ (c' - b) = 0 $$

Instead of the second constraint being something like: $a \cdot (c' - b) + (1 - a) \cdot (c' - b) = 0$.

Summary

With the last several posts, I think we have general solutions for most items. There are still a bunch of details to figure out, but in terms of big questions, I think there are two left:

• What's the best way to handle boundary constraints, especially for dynamic values? I think my original suggest for boundary constraints may not work as well after switching to "evaluator functions".
• What's the best way to pass computed parameters to evaluator functions? Right now, evaluators take only columns for main and auxiliary traces, but can't accept other parameters - which, I think would be useful to have.

[bobbinth]

One way to handle boundary constraints and in general to define the main file for an AIR for a given computation could be as follows:

def MidenVmAir
use decoder::decoder, stack::stack

trace_columns:
  main: [clk, fmp, dc[23], st[19], rc[4], ch[19]]
  aux: [aux_dec[3], st_over, rc_8bit, rc_bus, hash_sib, ch_bus]

pub_inputs:
  program_hash: [4]
  stack_inputs: [16]
  stack_outputs: [16]
  
transition_constraints:
  enf clk' = clk + 1
  
  enf decoder([dc, clk], [aux_dec, ch_bus])
  enf stack([st, clk, fmp, dc[10..16]], [st_over, rc_bus, ch_bus])
  
boundary_constraints:
  clk.first = 0
  
  col.first = val for (col, val) in (st[0..16], stack_inputs)
  col.last = val for (col, val) in (st[0..16], stack_outputs)

There are a few issues with the above - so, maybe something else would work better, or we can find a way to improve this:

• We may not know the size of public inputs ahead of time. This would mean we'd need to add support for vectors of unknown size.
• If we need a public input which is just a single value, what's the best way to denote its type? Or should we assume that everything is a vector and something like foo: [1] is fine?
• When making a call to stack constraints, we need to pass a set of helper columns which are actually a part of the decoder. Above this is done as dc[10..15] - but this is not ideal as if the structure of the decoder changes, this would need to be updated. Is there a better way to handle things like that?
• It is assumed that all boundary constraints are will be defined under boundary_constraints section. This compromises modularity - probably something better is needed.
• The imports look awkward - I wonder if we should just define a default import per module so that we don't need to specify what is actually getting imported from a given file.

[tohrnii]

Based on discussions with @grjte, we can start the implementation by building different components of the constraint description language for one of the simpler constraints that we have defined in rust for now. Here are the constraints for bitwise chiplet defined in the constraint description language based on the syntax proposed by @bobbinth and others above.

[bobbinth]

I wonder if we should start with something that is even simpler than this. Maybe just constraints agains the clock cycle column. There are two constraints:

• One boundary constraint that clk at the first step is 1.
• One transition constraint which says that clk' = clk + 1.

I think this will lets us implement a minimal subset of the language which can be run through the entire process (from parsing to Rust code generation).

[grjte]

I wonder if we should start with something that is even simpler than this.

I agree with that for the initial parsing step.

My thinking in defining these constraints in this language was not that we would try to tackle all of this first, but so that we would see what most of the "core functionality" would look like with some of our real constraints. It makes it easier to do the following:

1. I think it helps outline a reasonable scope of a first big milestone to work towards (v0.1), since once we can parse this file + handle imports, we can use this system for most our constraints. (More complicated things like evaluators would wait)
2. We can identify & clarify outstanding questions for the simpler version of this DSL now.
3. We can use this file to guide the stages of work.

For me, it helps to see the destination clearly at the beginning, so having something concrete in the language is useful.

We can address all 3 of these points in the new repo (https://github.com/polygon-miden/air-dsl). I'll open issues for each of these points over the next couple days.

[bobbinth]

I agree that seeing how real constraints look is very useful - but I'd still limit the scope for v0.1 much more. For example, I'd leave iteration, ranges, intermediate variables etc. out of scope for now. My preference would be for something as simple as this:

def TestAir

trace_columns:
  main: [clk, fmp, ctx]
  
transition_constraints:
  enf clk' = clk + 1
  
boundary_constraints:
  enf clk.first = 0

Although, maybe it would also be nice to add handling of public inputs, periodic columns, auxiliary columns, and random values.

So, to summarize, in my mind the goal of the initial version would be to:

1. Set up infrastructure for parsing inputs and define basic parsing rules.
2. Define data structures for internal representation of constraints.
3. Set up infrastructure for outputting Rust code in Winterfell format (basically, implementation of Air trait).

Once this is working, we can start adding more and more features. My hope that by v0.3 or v0.4 we'll get to the point where we can describe all VM constraints in a modular way.