Add section for random values and allow declaring names for accessing random values

[tohrnii]

For some backends it may be useful to have a random_values section. This section would enable naming/grouping of random values similar to how trace columns section allows for trace columns. The syntax for this section could look as follows:

random_values:
    rand: [15]

The above specifies that there should be 15 random available for use in auxiliary trace constraints, and that these random values will be available under variable $rand.

Similar to trace columns, we could name various values as follows:

random_values:
    rand: [a, b]

The above specifies that a and b names could be used to refer to specific random values, and also that $rand variable could be used to refer to the entire vector.

Originally posted by @bobbinth in #53.

[grjte]

A couple of questions here:

1. Do we still want to have a default $rand, or are we replacing that by this section so that they must always be declared? (if we're replacing it, we'll probably want to add some checks in the IR to make sure all sizes and accesses are declared / legal)
2. Do we still want to use the '$' now that we're naming these? If so, I think we should also access the named array values that way, i.e., by $rand[0] and $a $b.

@bobbinth what did you have in mind when you wrote this comment?

[bobbinth]

I was thinking that this section would be optional - but I can also see an argument for making it mandatory. If we do keep it optional, I think we should assume rand as the default value. In the future, we could allow people to specify their own names (e.g., alphas instead of rand).

Regarding $, I was thinking this could be our general way of addressing variables declared in such sections. So, for example we have $main and $aux. $rand would be treated the same way.

So, in this example:

random_values:
    rand: [a, b]

We could access the first random value simply as a or as $rand[0].

[Fumuran]

I have a couple of questions:

1. Do we want to allow more than one array in the section?
2. Do we want to create array(s) according to the trace segments, or we want to make random values independent from trace segments?

[grjte]

@Overcastan great question. This comes down to how "random values" work. The proof protocol works in rounds. The prover sends a commitment to the verifier, then the verifier sends some randomness, then the prover sends another commitment using that randomness, then the verifier could send more randomness, etc.

1. Prover sends a commitment to the main trace (segment 0)
2. Verifier sends some randomness
3. Prover uses the randomness to commit to the aux trace (segment 1) & sends it to the verifier

In MidenVM and Winterfell, this is where we stop. Therefore at the moment, there's only one set of randomness, and that's the randomness which is used when building the "segment 1" trace.

In theory in the future it would be nice to make this generic so that it would be possible to use AirScript for a system that has more rounds (and therefore more sets of randomness, used for segment 2, 3, etc...).

However, for now we can keep it simple and just have the randomness be associated with the auxiliary trace. We haven't yet adjusted the AirScript language to make more segments possible anyway - only main (0) and aux (1) are supported.

[grjte]

In other words, there's no need to do anything other than what's described in the original issue here and Bobbin's comment above. We'll leave handling of additional trace segments/randomness for the future

[bobbinth]

I was thinking that this section would be optional - but I can also see an argument for making it mandatory.

Coming back to my earlier comment. I've realized that this section must be optional as there use cases when we don't need the second trace segment (i.e., we'd have only main) and thus, there will be no random values.

[Fumuran]

Should we return some type of Error if there are no aux trace columns, but random values section is declared? And if it declared, but empty?

[tohrnii]

@Overcastan sounds good to me. Also we have an open issue #46 that can probably be combined with this. Wdyt?

[Fumuran]

Also we have an open issue #46 that can probably be combined with this. Wdyt?

I agree, I could combine it in the PR next to #128 and add checks for both declaration and usage

[grjte]

@Overcastan sounds good to me. Also we have an open issue #46 that can probably be combined with this. Wdyt?

I don't think we should combine #46 in the first PR, because we should address just the parser first. In the follow-up PR with IR and codegen changes, #46 could be included

[grjte]

Based on #128 and #129, I want to ask a point of clarification. My understanding from the discussion above was that the old method of using random values would still work, but we would now have the optional ability to define named random values.

In other words, we would be able to do all of the following:

def AuxiliaryAir

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

public_inputs:
    stack_inputs: [16]

boundary_constraints:
    # auxiliary boundary constraint with a random value
    enf p1.first = $rand[0]
  
integrity_constraints:
    # integrity constraints against the auxiliary trace with random values
    enf p0' = p0 * (a + $rand[0] + b + $rand[1])
    enf p1 = p1' * (c + $rand[0])

def AuxiliaryAir

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

public_inputs:
    stack_inputs: [16]

random_values:
    rand: [r, s]

boundary_constraints:
    # auxiliary boundary constraint with a random value
    enf p1.first = r
  
integrity_constraints:
    # integrity constraints against the auxiliary trace with random values
    enf p0' = p0 * (a + r + b + s)
    enf p1 = p1' * (c + $rand[0])

def AuxiliaryAir

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

public_inputs:
    stack_inputs: [16]

random_values:
    alphas: [r, s]

boundary_constraints:
    # auxiliary boundary constraint with a random value
    enf p1.first = $alphas[0]
  
integrity_constraints:
    # integrity constraints against the auxiliary trace with random values
    enf p0' = p0 * (a + r + b + s)
    enf p1 = p1' * (c + $alphas[0])

Have I misunderstood your intention @bobbinth ?

[bobbinth]

I think the second and third examples work - but I was thinking of the first one a bit differently. Specifically, we would always have to specify random_values section. So, for the first example, it would look like so:

def AuxiliaryAir

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

random_values:
  rand: [2]

public_inputs:
    stack_inputs: [16]

boundary_constraints:
    # auxiliary boundary constraint with a random value
    enf p1.first = $rand[0]
  
integrity_constraints:
    # integrity constraints against the auxiliary trace with random values
    enf p0' = p0 * (a + $rand[0] + b + $rand[1])
    enf p1 = p1' * (c + $rand[0])

I'm open to other suggestions though.

[grjte]

I think the second and third examples work - but I was thinking of the first one a bit differently. Specifically, we would always have to specify random_values section. So, for the first example, it would look like so:

def AuxiliaryAir

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

random_values:
  rand: [2]

public_inputs:
    stack_inputs: [16]

boundary_constraints:
    # auxiliary boundary constraint with a random value
    enf p1.first = $rand[0]
  
integrity_constraints:
    # integrity constraints against the auxiliary trace with random values
    enf p0' = p0 * (a + $rand[0] + b + $rand[1])
    enf p1 = p1' * (c + $rand[0])

I'm open to other suggestions though.

@bobbinth this is fine with me - it's exactly what I was trying to clarify. The first example was what we had previously, and I was trying to figure out if we were removing that functionality

[bobbinth]

we would always have to specify random_values section

To make my statement more precise: if there are one or more aux segments, we should always have random_values section.

[tohrnii]

Closed by #129 and #134