starkoracles / air-script

A domain-specific language for writing AIR constraints for STARKs
MIT License
0 stars 0 forks source link

Handle Aux constraints #7

Open skaller opened 1 year ago

skaller commented 1 year ago

So how do these work?

skaller commented 1 year ago

Added example xauxchk.air which is the same as example.air but with aux trace and constraints added. BUG: the transpile works, cairo is generated for the aux trace. However, I didn't make a VM and inputs. The test harness doesn't generate an error message, it just does no tests.

I need an error, to enforce extreme programming methodology, i.e. to force me to fix the error by adding the VM and inputs. Currently, even if there is a VM, if there are no inputs, again there is no error, just no tests are done.

The VM will have to accept in aux input (first line of trace), however it cannot generate a trace without also getting the random values.

skaller commented 1 year ago

So here's what i will implement. I comment first it seems to me there is no use for an aux trace. The evaluation and merge are identical to the main trace. The only difference is the aux trace uses random inputs, and can't use public values, and whilst the aux trace can refer to the main trace, the main trace cannot refer to the aux trace.

This has no impact on the evaluation, so we might as well just widen the main trace.

  1. Add an input random.all with some numbers in the first and only line
  2. All the VM will use the same random numbers for the moment.
  3. If there aren't enough numbers, the VM will just wrap around.
  4. The aux trace will be produced as part of the main trace in the same file
  5. The inputs will have to provide initial data for both the main and auxilliary traces
  6. The outputs will have to be for both as well, otherwise the boundary constraints for the aux trace can't be checked
  7. An additional file will be produced called <testname>.trace_widths which contains a list of the widths of the trace segments. This allows the trace to be split (vertically) by the fixed Winterfell main.rs code.
  8. The cairo code handles main and aux traces (any number) separately based on the air file, so
  9. The trace_widths file has to agree with the air.

In the future, we might derive the trace_widths from the air but in some sense this is backwards: the air is actually based on what the vm actually does

Consequently the only change to the general VM spec at the moment is that it has to write the trace_widths file but this is an invariant property of the VM.

It is NOT clear to me at this time exactly how Winterfell handles this. It appears to generate the random values from a public coin. But in this case, the aux trace cannot be produced by the VM. Instead, it has to be produced by the prover. However the airscript file format only provides constraints on the aux trace and does not determine how to generate it.

skaller commented 1 year ago

OK, so this is the WRONG idea. The aux trace is built by the prover AFTER the main trace has been committed to a Merkel tree, the random numbers are generated by seeding a public coin with the root hash.

This means we need aux trace builder code. For Winterfell, that will have to be Rust. Exactly how that gets used to select an evaluation frame to pass to the verifier I don't know, nor how to get the generator to actually get the aux trace into Winterfell .. nor how to get out the data needed to check our cairo. [The routines are already there].

There's an unrelated by similar problem with public inputs and outputs, which for a real VM like Miden, are not the same as the first and last row of the main trace.