tasm_lib/
memory.rs

1//! Memory convention used in this crate:
2//!
3//! - A memory page is contiguous memory of size 2^32 words, aligned to 2^32 word boundaries.
4//!   There is one exception: due to the [base field's prime][prime] being 2^64 - 2^32 + 1,
5//!   the last page, starting at address 2^64 - 2^32, is of size 1.
6//! - The dynamic allocator lives at address [`DYN_MALLOC_ADDRESS`][dyn_malloc_addr], _i.e._, -1.
7//!   It is a single word, containing a counter of allocated pages.
8//!   It occupies the only page that is not of size 2^32 words.
9//! - Page 0 is reserved for non-deterministically initialized memory.
10//! - The last full page, number (2^32)-2, starting at address 2^64 - 2ยท(2^32),
11//!   is reserved for [static allocations][static_malloc_addr].
12//! - The two preceding pages, number 2^32-4 and 2^32-3 are used by the
13//!   [STARK verifier][stark_verifier] (when standard memory layouts are used).
14//! - Pages 1 through 2^31-1 are dynamically allocated by the
15//!   [dynamic allocator][dynamic_allocator] snippet.
16//! - Pages 2^31 through 2^32-5 are not in use by this crate.
17//!
18//! [prime]: BFieldElement::P
19//! [dyn_malloc_addr]: dyn_malloc::DYN_MALLOC_ADDRESS
20//! [static_malloc_addr]: crate::library::STATIC_MEMORY_FIRST_ADDRESS
21//! [stark_verifier]: crate::verifier::stark_verify::StarkVerify
22//! [dynamic_allocator]: dyn_malloc::DynMalloc
23
24use std::collections::HashMap;
25
26use num::One;
27use triton_vm::memory_layout::MemoryRegion;
28use triton_vm::prelude::*;
29
30pub mod dyn_malloc;
31pub mod memcpy;
32
33/// Non-deterministically initialized memory lives in the range $[0: 2^{32})$
34///
35/// See the [memory convention][self] for details.
36pub const FIRST_NON_DETERMINISTICALLY_INITIALIZED_MEMORY_ADDRESS: BFieldElement =
37    BFieldElement::new(0);
38
39pub const LAST_ADDRESS_AVAILABLE_FOR_NON_DETERMINISTICALLY_ALLOCATED_MEMORY: BFieldElement =
40    BFieldElement::new(u32::MAX as u64);
41
42/// Returns the address of the last populated word belonging to the memory region
43/// designated for non-determinism.
44pub fn last_populated_nd_memory_address(
45    memory: &HashMap<BFieldElement, BFieldElement>,
46) -> Option<BFieldElement> {
47    memory
48        .keys()
49        .map(|b| b.value())
50        .filter(|u| *u <= LAST_ADDRESS_AVAILABLE_FOR_NON_DETERMINISTICALLY_ALLOCATED_MEMORY.value())
51        .max()
52        .map(|address| bfe!(address))
53}
54
55/// Returns the address of the first unpopulated word belonging to the memory
56/// region designated for non-determinism.
57pub fn first_free_nd_address(
58    memory: &HashMap<BFieldElement, BFieldElement>,
59) -> Option<BFieldElement> {
60    let last_populated = last_populated_nd_memory_address(memory);
61    match last_populated {
62        None => Some(FIRST_NON_DETERMINISTICALLY_INITIALIZED_MEMORY_ADDRESS),
63        Some(last_populated) => match last_populated {
64            LAST_ADDRESS_AVAILABLE_FOR_NON_DETERMINISTICALLY_ALLOCATED_MEMORY => None,
65            addr => Some(addr + BFieldElement::one()),
66        },
67    }
68}
69
70pub fn nd_memory_region() -> MemoryRegion {
71    let size = LAST_ADDRESS_AVAILABLE_FOR_NON_DETERMINISTICALLY_ALLOCATED_MEMORY.value()
72        - FIRST_NON_DETERMINISTICALLY_INITIALIZED_MEMORY_ADDRESS.value();
73
74    MemoryRegion::new(
75        FIRST_NON_DETERMINISTICALLY_INITIALIZED_MEMORY_ADDRESS,
76        size.try_into().unwrap(),
77    )
78}
79
80/// Stores the encoding of the given object into memory at the given address, and returns
81/// the address of the first untouched memory cell after.
82pub fn encode_to_memory<T: BFieldCodec>(
83    memory: &mut HashMap<BFieldElement, BFieldElement>,
84    address: BFieldElement,
85    object: &T,
86) -> BFieldElement {
87    let encoding = object.encode();
88    for (i, e) in encoding.iter().enumerate() {
89        memory.insert(address + bfe!(i), *e);
90    }
91    address + bfe!(encoding.len())
92}
93
94/// Return the code to read `n` words from memory. Top of stack must point
95/// to last word of words to read. Leaves mutated pointer on top of stack.
96///
97/// ```text
98/// BEFORE: _ *last_word
99/// AFTER:  _ [loaded_words; n] (*first_word - 1)
100/// ```
101pub fn load_words_from_memory_leave_pointer(n: usize) -> Vec<LabelledInstruction> {
102    let num_full_chunk_reads = n / 5;
103    let num_remaining_words = n % 5;
104    let mut instructions = triton_asm![read_mem 5; num_full_chunk_reads];
105    if num_remaining_words > 0 {
106        instructions.extend(triton_asm!(read_mem {
107            num_remaining_words
108        }));
109    }
110    instructions
111}
112
113/// Return the code to read `n` words from memory. Top of stack must point
114/// to last word of words to read. Pops the memory pointer from the stack.
115///
116/// ```text
117/// BEFORE: _ *last_word
118/// AFTER:  _ [loaded_words; n]
119/// ```
120pub fn load_words_from_memory_pop_pointer(n: usize) -> Vec<LabelledInstruction> {
121    let instructions = load_words_from_memory_leave_pointer(n);
122
123    triton_asm!(
124        {&instructions}
125        pop 1
126    )
127}
128
129/// Return the code to write `n` words to memory. Leaves a modified pointer
130/// on the stack.
131///
132/// ```text
133/// BEFORE: _ [words_to_write; n] *first_word
134/// AFTER:  _ (*last_word + 1)
135/// ```
136pub fn write_words_to_memory_leave_pointer(n: usize) -> Vec<LabelledInstruction> {
137    let num_full_chunk_reads = n / 5;
138    let num_remaining_words = n % 5;
139    let mut instructions = vec![triton_instr!(write_mem 5); num_full_chunk_reads];
140    if num_remaining_words > 0 {
141        instructions.extend(triton_asm!(write_mem {
142            num_remaining_words
143        }));
144    }
145
146    instructions
147}
148
149/// Return the code to write `n` words to memory. Pops the memory pointer.
150///
151/// ```text
152/// BEFORE: _ [words_to_write; n] *first_word
153/// AFTER:  _
154/// ```
155pub fn write_words_to_memory_pop_pointer(n: usize) -> Vec<LabelledInstruction> {
156    let instructions = write_words_to_memory_leave_pointer(n);
157
158    triton_asm!(
159        {&instructions}
160        pop 1
161    )
162}
163
164#[cfg(test)]
165mod tests {
166    use std::collections::HashMap;
167
168    use num::Zero;
169    use proptest::prop_assert;
170    use proptest_arbitrary_interop::arb;
171    use test_strategy::proptest;
172    use triton_vm::prelude::BFieldElement;
173
174    use super::*;
175
176    #[test]
177    fn last_populated_nd_memory_address_looks_sane() {
178        let empty_memory = HashMap::default();
179        assert!(last_populated_nd_memory_address(&empty_memory).is_none());
180        assert_eq!(
181            Some(BFieldElement::zero()),
182            first_free_nd_address(&empty_memory)
183        );
184
185        let empty_nd_region: HashMap<_, _> = [(bfe!(1u64 << 32), BFieldElement::new(42))]
186            .into_iter()
187            .collect();
188        assert!(last_populated_nd_memory_address(&empty_nd_region).is_none());
189        assert_eq!(
190            Some(BFieldElement::zero()),
191            first_free_nd_address(&empty_nd_region)
192        );
193
194        for address in [0, 1, 100, u32::MAX - 3, u32::MAX - 1, u32::MAX] {
195            let one_populated_word: HashMap<_, _> = [(bfe!(address), BFieldElement::new(42))]
196                .into_iter()
197                .collect();
198            assert_eq!(
199                Some(bfe!(address)),
200                last_populated_nd_memory_address(&one_populated_word)
201            );
202        }
203
204        for address in [1, 100, u32::MAX - 3, u32::MAX - 1, u32::MAX] {
205            let two_populated_words: HashMap<_, _> = [
206                (bfe!(address), BFieldElement::new(42)),
207                (bfe!(address - 1), BFieldElement::new(42)),
208            ]
209            .into_iter()
210            .collect();
211            assert_eq!(
212                Some(bfe!(address)),
213                last_populated_nd_memory_address(&two_populated_words)
214            );
215        }
216
217        let much_poulated_zero_is_empty: HashMap<_, _> =
218            (1..4000).map(|address| (bfe!(address), bfe!(42))).collect();
219        assert_eq!(
220            Some(bfe!(3999)),
221            last_populated_nd_memory_address(&much_poulated_zero_is_empty)
222        );
223        assert_eq!(
224            Some(bfe!(4000)),
225            first_free_nd_address(&much_poulated_zero_is_empty)
226        );
227
228        let much_poulated_zero_populated: HashMap<_, _> =
229            (0..4021).map(|address| (bfe!(address), bfe!(42))).collect();
230        assert_eq!(
231            Some(bfe!(4020)),
232            last_populated_nd_memory_address(&much_poulated_zero_populated)
233        );
234        assert_eq!(
235            Some(bfe!(4021)),
236            first_free_nd_address(&much_poulated_zero_populated)
237        );
238
239        let scattered_population: HashMap<_, _> = [(bfe!(30), bfe!(42)), (bfe!(2000), bfe!(42))]
240            .into_iter()
241            .collect();
242        assert_eq!(
243            Some(bfe!(2000)),
244            last_populated_nd_memory_address(&scattered_population)
245        );
246        assert_eq!(
247            Some(bfe!(2001)),
248            first_free_nd_address(&scattered_population)
249        );
250    }
251
252    #[test]
253    fn first_free_nd_address_looks_sane() {
254        for address in [0, 1, 100, u32::MAX - 3, u32::MAX - 3] {
255            let one_populated_word: HashMap<_, _> = [(bfe!(address), BFieldElement::new(42))]
256                .into_iter()
257                .collect();
258            assert_eq!(
259                Some(bfe!(address + 1)),
260                first_free_nd_address(&one_populated_word)
261            );
262
263            let two_populated_words: HashMap<_, _> = [
264                (bfe!(address), BFieldElement::new(42)),
265                (bfe!(address + 1), BFieldElement::new(42)),
266            ]
267            .into_iter()
268            .collect();
269            assert_eq!(
270                Some(bfe!(address + 2)),
271                first_free_nd_address(&two_populated_words)
272            );
273        }
274
275        let last_word_populated: HashMap<_, _> = [(
276            LAST_ADDRESS_AVAILABLE_FOR_NON_DETERMINISTICALLY_ALLOCATED_MEMORY,
277            bfe!(42),
278        )]
279        .into_iter()
280        .collect();
281        assert!(first_free_nd_address(&last_word_populated).is_none());
282    }
283
284    #[proptest]
285    fn all_addresses_between_0_and_u32max_belong_to_nd_memory(nd_address: u32) {
286        prop_assert!(nd_memory_region().contains_address(bfe!(nd_address)));
287    }
288
289    #[proptest]
290    fn addresses_outside_u32_range_do_not_belong_to_nd_memory(
291        #[strategy(arb())]
292        #[filter(#address.value() > u32::MAX as u64)]
293        address: BFieldElement,
294    ) {
295        prop_assert!(!nd_memory_region().contains_address(address));
296    }
297}