The MemoryBridge is used within AIR evaluation functions to constrain logical memory
operations (read/write). It adds all necessary constraints and interactions.
The auxiliary columns for a memory read operation with block size N.
These columns should be automatically managed by the memory controller.
To fully constrain a memory read, in addition to these columns,
the address space, pointer, and data must be provided.
Constraints and interactions for a logical memory read of (address, data) at time timestamp.
This reads (address, data, timestamp_prev) from the memory bus and writes
(address, data, timestamp) to the memory bus.
Includes constraints for timestamp_prev < timestamp.
Constraints and interactions for a logical memory write of (address, data) at time
timestamp. This reads (address, data_prev, timestamp_prev) from the memory bus and writes
(address, data, timestamp) to the memory bus.
Includes constraints for timestamp_prev < timestamp.