openvm_circuit/system/memory/offline_checker/
columns.rs

1//! Defines auxiliary columns for memory operations: `MemoryReadAuxCols`,
2//! `MemoryReadWithImmediateAuxCols`, and `MemoryWriteAuxCols`.
3
4use openvm_circuit_primitives::is_less_than::LessThanAuxCols;
5use openvm_circuit_primitives_derive::AlignedBorrow;
6use openvm_stark_backend::p3_field::PrimeField32;
7
8use crate::system::memory::offline_checker::bridge::AUX_LEN;
9
10// repr(C) is needed to make sure that the compiler does not reorder the fields
11// we assume the order of the fields when using borrow or borrow_mut
12/// Base structure for auxiliary memory columns.
13#[repr(C)]
14#[derive(Clone, Copy, Debug, AlignedBorrow)]
15pub struct MemoryBaseAuxCols<T> {
16    /// The previous timestamps in which the cells were accessed.
17    pub prev_timestamp: T,
18    /// The auxiliary columns to perform the less than check.
19    pub timestamp_lt_aux: LessThanAuxCols<T, AUX_LEN>,
20}
21
22impl<F: PrimeField32> MemoryBaseAuxCols<F> {
23    #[inline(always)]
24    pub fn set_prev(&mut self, prev_timestamp: F) {
25        self.prev_timestamp = prev_timestamp;
26    }
27}
28
29#[repr(C)]
30#[derive(Clone, Copy, Debug, AlignedBorrow)]
31pub struct MemoryWriteAuxCols<T, const N: usize> {
32    pub base: MemoryBaseAuxCols<T>,
33    pub prev_data: [T; N],
34}
35
36impl<const N: usize, T> MemoryWriteAuxCols<T, N> {
37    pub fn from_base(base: MemoryBaseAuxCols<T>, prev_data: [T; N]) -> Self {
38        Self { base, prev_data }
39    }
40
41    #[inline(always)]
42    pub fn get_base(self) -> MemoryBaseAuxCols<T> {
43        self.base
44    }
45
46    #[inline(always)]
47    pub fn prev_data(&self) -> &[T; N] {
48        &self.prev_data
49    }
50
51    /// Sets the previous data **without** updating the less than auxiliary columns.
52    #[inline(always)]
53    pub fn set_prev_data(&mut self, data: [T; N]) {
54        self.prev_data = data;
55    }
56}
57
58/// The auxiliary columns for a memory read operation with block size `N`.
59/// These columns should be automatically managed by the memory controller.
60/// To fully constrain a memory read, in addition to these columns,
61/// the address space, pointer, and data must be provided.
62#[repr(C)]
63#[derive(Clone, Copy, Debug, AlignedBorrow)]
64pub struct MemoryReadAuxCols<T> {
65    pub(in crate::system::memory) base: MemoryBaseAuxCols<T>,
66}
67
68impl<F: PrimeField32> MemoryReadAuxCols<F> {
69    pub fn new(prev_timestamp: u32, timestamp_lt_aux: LessThanAuxCols<F, AUX_LEN>) -> Self {
70        Self {
71            base: MemoryBaseAuxCols {
72                prev_timestamp: F::from_canonical_u32(prev_timestamp),
73                timestamp_lt_aux,
74            },
75        }
76    }
77
78    #[inline(always)]
79    pub fn get_base(self) -> MemoryBaseAuxCols<F> {
80        self.base
81    }
82
83    /// Sets the previous timestamp **without** updating the less than auxiliary columns.
84    #[inline(always)]
85    pub fn set_prev(&mut self, timestamp: F) {
86        self.base.prev_timestamp = timestamp;
87    }
88}
89
90#[repr(C)]
91#[derive(Clone, Debug, AlignedBorrow)]
92pub struct MemoryReadOrImmediateAuxCols<T> {
93    pub base: MemoryBaseAuxCols<T>,
94    pub is_immediate: T,
95    pub is_zero_aux: T,
96}
97
98impl<T, const N: usize> AsRef<MemoryReadAuxCols<T>> for MemoryWriteAuxCols<T, N> {
99    fn as_ref(&self) -> &MemoryReadAuxCols<T> {
100        // Safety:
101        //  - `MemoryReadAuxCols<T>` is repr(C) and its only field is the first field of
102        //    `MemoryWriteAuxCols<T, N>`.
103        //  - Thus, the memory layout of `MemoryWriteAuxCols<T, N>` begins with a valid
104        //    `MemoryReadAuxCols<T>`.
105        unsafe { &*(self as *const MemoryWriteAuxCols<T, N> as *const MemoryReadAuxCols<T>) }
106    }
107}
108
109impl<T, const N: usize> AsMut<MemoryBaseAuxCols<T>> for MemoryWriteAuxCols<T, N> {
110    fn as_mut(&mut self) -> &mut MemoryBaseAuxCols<T> {
111        &mut self.base
112    }
113}
114
115impl<T> AsMut<MemoryBaseAuxCols<T>> for MemoryReadAuxCols<T> {
116    fn as_mut(&mut self) -> &mut MemoryBaseAuxCols<T> {
117        &mut self.base
118    }
119}
120
121impl<T> AsMut<MemoryBaseAuxCols<T>> for MemoryReadOrImmediateAuxCols<T> {
122    fn as_mut(&mut self) -> &mut MemoryBaseAuxCols<T> {
123        &mut self.base
124    }
125}
openvm_circuit/system/memory/offline_checker/columns.rs

openvm_circuit/system/memory/offline_checker/
columns.rs
