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

triton_vm/
memory_layout.rs
