Custom evaluation frames

[maxgillett]

Some AIR constraints cannot be expressed as functions involving just two consecutive rows of trace registers. An example of such a constraint is found in the Cairo whitepaper, where a multi-set permutation check is used to ensure that memory is continuous and read-only. This constraint checks address-value pairs for four different pointer types (pc, dst, op0, op1). When these pointers are located in the same trace row, it is not possible to implement the required cumulative product step constraint for nontrivial programs, as memory accesses for more than one pointer type can occur in a single execution step and are not broken down into individual rows. Thus when we specify additional auxiliary columns for all of the various address-value pairs (regardless of pointer type, and sorted by address) there will be a mismatch in trace length. While sorted address-value columns could be constructed for each pointer type, and continuity constraints could be modified to ensure that memory accesses restricted to a specific pointer type are read-only, it does not appear possible to ensure that the same memory accesses across different pointer types also remain read-only. To solve this issue, the Cairo whitepaper introduces "virtual columns" and "subcolumns" (page 49) to allow for larger evaluation frames that effectively provide non-overlapping windows of the execution trace.

With the above in mind, a simple modification of the current frame implementation could allow for larger window sizes, and otherwise seek to keep the interface the same. We could split the current EvaluationFrame struct into an EvaluationFrame trait and ConsecutiveEvaluationFrame struct implementing this trait (similar to how ExecutionTrace was split in a previous pull request). The ConsecutiveEvaluationFrame (there is probably a better name) will have the same functionality as the current struct (it has a window size of 1), and remain in use for both the two OOD point evaluations and for AIR transition evaluations that only need the current and next row. Users that need a larger window for their transition function (e.g. the current 4 rows and next 4 rows) can create a custom struct satisfying the trait. It might also make sense to allow for the current and next functions to have differing windows sizes. I think at a minimum we will need to modify the evaluate_fragment function in ConstraintEvaluator and the read_main_trace_frame_into function in TraceLde.

[4l0n50]

Just to complement, what you're saying is done here in the Cairo solidity verifier, which checks that OOD evaluations satisfy for example that (T_i(x) - T_i(g^33158*z))/(x - g^33158*z) is low degree. To what you said I would just add that you also need to modify the compose_registers method of DeepComposer struct. However, I don't think it is a good idea to just define larger windows because not all values will be used. In the example above it will require a window of size at least 33158! I think one might instead just define which other (arbitrary?) cells might be needed when evaluating the constraints.

[4l0n50]

However, I don't think it is a good idea to just define larger windows because not all values will be used.

Now that I think, it doesn't really matter even if EvaluationFrame depends on the whole trace. As long as your constraints doesn't depend on too many variables, everything should be ok

[maxgillett]

Yes, the frame will just provide a view of the trace, which shouldn't impact performance. Good point about the DeepComposer modifications. It would be wasteful to construct an OOD frame for all of the row offsets up to the window size (which could be quite large, as you demonstrate). One could either define in EvaluationFrame which row offsets are used in the constraints, or as in the StarkEx contract use OOD evaluations that are both column and row specific. The latter could be achieved by dynamically tracking relative trace indices during constraint evaluation, and storing these in a sparse matrix data structure. I think these are implementation details that can be abstracted away in the definition of EvaluationFrame.