miden-vm icon indicating copy to clipboard operation
miden-vm copied to clipboard

"Backfill" memory range check requests to op exec row instead of AuxTable memory trace row

Open grjte opened this issue 2 years ago • 3 comments

With the current implementation of range check lookups for stack and memory in the p1 column (implemented in #286), it's possible for requests from the stack and requests from memory to occur in the same row of the execution trace, since the memory requests occur during each row of the memory segment of the Auxiliary Table trace, whereas the stack requests occur when the operation is executed. In order to keep the AIR constraint degrees of the p1 column below 9, this requires an additional aux trace column q of intermediate values which holds the stack lookups.

A better approach would be to include the range check requests from memory at the time the mload and mstore operations are executed on the stack. This would guarantee that there would never be more than one set of range check lookups requested by any operation at any given cycle. We could then remove the extra q column.

The complication here is that memory information isn't available until the execution trace is being finalized and all memory accesses are known. Thus, we can't include memory range checks at the time that mload or mstore operations are executed. Instead, when the trace is being finalized, we need to "backfill" the memory lookup information into the decoder columns at the cycle where the operations were executed, and then update the range checker's AuxTraceBuilder so that range check requests by memory are performed at the row where the memory operation was executed rather than at the row where it's included in the memory trace. (This means we need to track those cycles, which is currently not done.)

This requires a refactor of the current approach to the range checker's p1 column in the range checker's AuxTraceBuilder. This will allow us to:

  1. remove the q column, since all required AIR constraints for p1 will be 9 degrees (or fewer)
  2. remove the cycle_range_checks BTree and CycleRangeChecks struct and use vectors of "hints" and "rows" instead, similar to the AuxTraceBuilder pattern in the stack or hasher.

grjte avatar Jul 10 '22 15:07 grjte

One other thing to mention here: because range-checking of delta values will now happen in the stack, we need to make sure that the same delta values are used in memory trace. To do this, we need to include delta values into row values of the memory trace table.

bobbinth avatar Jul 10 '22 18:07 bobbinth

This could also be a good time to revisit the approach to providing delta values and generating the trace (i.e. when to do each thing). Currently, we loop through the trace once in append_range_checks and again in fill_trace. At some point, it would be good to benchmark whether it would faster to generate the trace at the same time that we handle range checks and then copy it (like the bitwise trace is copied in Bitwise::fill_trace). At the very least, both methods should be considered during this refactor.

grjte avatar Jul 14 '22 13:07 grjte

This might be a bit more complicated than I originally thought - primarily because it would affect opcode design. The issue is that, if we put memory range check into the stack, constraint degree for memory operations would increase to 3 (because we need to consume 2 range checks). But the groups where we place memory operations limit their constraint degrees to 2.

For mloadw, mstore, and mstorew, we could use a common prefix (01011). This would also imply that 2 range checks get consumed when we do fmpupdate because it currently shares the same prefix - but I think that's OK (and we can move fmpupdate to another spot after we get rid of u32or).

For mload, we can'd do much except for moving it to a group with higher degree constraints (i.e., degree 6). There are only two empty slots there right now - so, we might want to hold off until we figure out whether they should be taken up by something else.

bobbinth avatar Aug 08 '22 05:08 bobbinth

Closed by #1027 via #982.

bobbinth avatar Aug 07 '23 14:08 bobbinth