triton_vm/
memory_layout.rs

1pub use constraint_builder::codegen::MEM_PAGE_SIZE;
2
3use air::challenge_id::ChallengeId;
4use arbitrary::Arbitrary;
5use itertools::Itertools;
6use strum::EnumCount;
7use twenty_first::prelude::*;
8
9use crate::table::master_table::MasterAuxTable;
10use crate::table::master_table::MasterMainTable;
11
12/// Memory layout guarantees for the [Triton assembly AIR constraint
13/// evaluator][tasm_air] with input lists at dynamically known memory locations.
14///
15/// [tasm_air]: crate::constraints::dynamic_air_constraint_evaluation_tasm
16#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash, Arbitrary)]
17pub struct DynamicTasmConstraintEvaluationMemoryLayout {
18    /// Pointer to a region of memory that is reserved for (a) pointers to
19    /// {current, next} {main, aux} rows, and (b) intermediate values in the
20    /// course of constraint evaluation. The size of the region must be at
21    /// least [`MEM_PAGE_SIZE`] [`BFieldElement`]s.
22    pub free_mem_page_ptr: BFieldElement,
23
24    /// Pointer to an array of [`XFieldElement`]s of length
25    /// [`NUM_CHALLENGES`][num_challenges].
26    ///
27    /// [num_challenges]: ChallengeId::COUNT
28    pub challenges_ptr: BFieldElement,
29}
30
31/// Memory layout guarantees for the [Triton assembly AIR constraint
32/// evaluator][tasm_air] with input lists at statically known memory locations.
33///
34/// [tasm_air]: crate::constraints::static_air_constraint_evaluation_tasm
35#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash, Arbitrary)]
36pub struct StaticTasmConstraintEvaluationMemoryLayout {
37    /// Pointer to a region of memory that is reserved for constraint
38    /// evaluation. The size of the region must be at least
39    /// [`MEM_PAGE_SIZE`] [`BFieldElement`]s.
40    pub free_mem_page_ptr: BFieldElement,
41
42    /// Pointer to an array of [`XFieldElement`]s of length
43    /// [`MasterMainTable::NUM_COLUMNS`].
44    pub curr_main_row_ptr: BFieldElement,
45
46    /// Pointer to an array of [`XFieldElement`]s of length
47    /// [`MasterAuxTable::NUM_COLUMNS`].
48    pub curr_aux_row_ptr: BFieldElement,
49
50    /// Pointer to an array of [`XFieldElement`]s of length
51    /// [`MasterMainTable::NUM_COLUMNS`].
52    pub next_main_row_ptr: BFieldElement,
53
54    /// Pointer to an array of [`XFieldElement`]s of length
55    /// [`MasterAuxTable::NUM_COLUMNS`].
56    pub next_aux_row_ptr: BFieldElement,
57
58    /// Pointer to an array of [`XFieldElement`]s of length
59    /// [`NUM_CHALLENGES`][num_challenges].
60    ///
61    /// [num_challenges]: ChallengeId::COUNT
62    pub challenges_ptr: BFieldElement,
63}
64
65pub trait IntegralMemoryLayout {
66    /// Determine if the memory layout's constraints are met, _i.e._, whether
67    /// the various pointers point to large enough regions of memory.
68    fn is_integral(&self) -> bool {
69        let memory_regions = self.memory_regions();
70        if memory_regions.iter().unique().count() != memory_regions.len() {
71            return false;
72        }
73
74        let disjoint_from_all_others = |region| {
75            let mut all_other_regions = memory_regions.iter().filter(|&r| r != region);
76            all_other_regions.all(|r| r.disjoint_from(region))
77        };
78        memory_regions.iter().all(disjoint_from_all_others)
79    }
80
81    fn memory_regions(&self) -> Box<[MemoryRegion]>;
82}
83
84impl IntegralMemoryLayout for StaticTasmConstraintEvaluationMemoryLayout {
85    fn memory_regions(&self) -> Box<[MemoryRegion]> {
86        let all_regions = [
87            MemoryRegion::new(self.free_mem_page_ptr, MEM_PAGE_SIZE),
88            MemoryRegion::new(self.curr_main_row_ptr, MasterMainTable::NUM_COLUMNS),
89            MemoryRegion::new(self.curr_aux_row_ptr, MasterAuxTable::NUM_COLUMNS),
90            MemoryRegion::new(self.next_main_row_ptr, MasterMainTable::NUM_COLUMNS),
91            MemoryRegion::new(self.next_aux_row_ptr, MasterAuxTable::NUM_COLUMNS),
92            MemoryRegion::new(self.challenges_ptr, ChallengeId::COUNT),
93        ];
94        Box::new(all_regions)
95    }
96}
97
98impl IntegralMemoryLayout for DynamicTasmConstraintEvaluationMemoryLayout {
99    fn memory_regions(&self) -> Box<[MemoryRegion]> {
100        let all_regions = [
101            MemoryRegion::new(self.free_mem_page_ptr, MEM_PAGE_SIZE),
102            MemoryRegion::new(self.challenges_ptr, ChallengeId::COUNT),
103        ];
104        Box::new(all_regions)
105    }
106}
107
108#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash)]
109pub struct MemoryRegion {
110    start: BFieldElement,
111    size: u64,
112}
113
114impl MemoryRegion {
115    pub fn new<A: Into<u64>>(address: A, size: usize) -> Self {
116        let start = bfe!(address.into());
117        let size = u64::try_from(size).unwrap();
118        Self { start, size }
119    }
120
121    pub fn disjoint_from(self, other: &Self) -> bool {
122        !self.overlaps(other)
123    }
124
125    pub fn overlaps(self, other: &Self) -> bool {
126        self.contains_address(other.start) || other.contains_address(self.start)
127    }
128
129    pub fn contains_address<A: Into<u64>>(self, addr: A) -> bool {
130        // move all arithmetic to u128 to avoid overflows
131        let addr = u128::from(addr.into());
132        let start = u128::from(self.start.value());
133        let end = start + u128::from(self.size);
134        (start..end).contains(&addr)
135    }
136}
137
138#[cfg(test)]
139#[cfg_attr(coverage_nightly, coverage(off))]
140mod tests {
141    use proptest::prelude::*;
142    use proptest_arbitrary_interop::arb;
143    use test_strategy::proptest;
144    use twenty_first::bfe;
145
146    use super::*;
147
148    impl Default for StaticTasmConstraintEvaluationMemoryLayout {
149        /// For testing purposes only.
150        fn default() -> Self {
151            let mem_page_size = MEM_PAGE_SIZE as u64;
152            let mem_page = |i| bfe!(i * mem_page_size);
153            StaticTasmConstraintEvaluationMemoryLayout {
154                free_mem_page_ptr: mem_page(0),
155                curr_main_row_ptr: mem_page(1),
156                curr_aux_row_ptr: mem_page(2),
157                next_main_row_ptr: mem_page(3),
158                next_aux_row_ptr: mem_page(4),
159                challenges_ptr: mem_page(5),
160            }
161        }
162    }
163
164    impl Default for DynamicTasmConstraintEvaluationMemoryLayout {
165        /// For testing purposes only.
166        fn default() -> Self {
167            let mem_page_size = MEM_PAGE_SIZE as u64;
168            let mem_page = |i| bfe!(i * mem_page_size);
169            DynamicTasmConstraintEvaluationMemoryLayout {
170                free_mem_page_ptr: mem_page(0),
171                challenges_ptr: mem_page(1),
172            }
173        }
174    }
175
176    #[proptest]
177    fn size_0_memory_region_contains_no_addresses(
178        #[strategy(arb())] region_start: BFieldElement,
179        #[strategy(arb())] address: BFieldElement,
180    ) {
181        let region = MemoryRegion::new(region_start, 0);
182        prop_assert!(!region.contains_address(region_start));
183        prop_assert!(!region.contains_address(address));
184    }
185
186    #[proptest]
187    fn size_1_memory_region_contains_only_start_address(
188        #[strategy(arb())] region_start: BFieldElement,
189        #[strategy(arb())]
190        #[filter(#region_start != #address)]
191        address: BFieldElement,
192    ) {
193        let region = MemoryRegion::new(region_start, 1);
194        prop_assert!(region.contains_address(region_start));
195        prop_assert!(!region.contains_address(address));
196    }
197
198    #[test]
199    fn definitely_integral_memory_layout_is_detected_as_integral() {
200        assert!(StaticTasmConstraintEvaluationMemoryLayout::default().is_integral());
201        assert!(DynamicTasmConstraintEvaluationMemoryLayout::default().is_integral());
202    }
203
204    #[test]
205    fn definitely_non_integral_memory_layout_is_detected_as_non_integral() {
206        let layout = StaticTasmConstraintEvaluationMemoryLayout {
207            free_mem_page_ptr: bfe!(0),
208            curr_main_row_ptr: bfe!(1),
209            curr_aux_row_ptr: bfe!(2),
210            next_main_row_ptr: bfe!(3),
211            next_aux_row_ptr: bfe!(4),
212            challenges_ptr: bfe!(5),
213        };
214        assert!(!layout.is_integral());
215
216        let layout = DynamicTasmConstraintEvaluationMemoryLayout {
217            free_mem_page_ptr: bfe!(0),
218            challenges_ptr: bfe!(5),
219        };
220        assert!(!layout.is_integral());
221    }
222
223    #[test]
224    fn memory_layout_integrity_check_does_not_panic_due_to_arithmetic_overflow() {
225        let mem_layout = DynamicTasmConstraintEvaluationMemoryLayout {
226            free_mem_page_ptr: bfe!(BFieldElement::MAX),
227            challenges_ptr: bfe!(1_u64 << 63),
228        };
229        assert!(mem_layout.is_integral());
230    }
231}
triton_vm/memory_layout.rs

triton_vm/
memory_layout.rs
