Module memory

Memory convention used in this crate:

• A memory page is contiguous memory of size 2^32 words, aligned to 2^32 word boundaries. There is one exception: due to the base field’s prime being 2^64 - 2^32 + 1, the last page, starting at address 2^64 - 2^32, is of size 1.
• The dynamic allocator lives at address DYN_MALLOC_ADDRESS, i.e., -1. It is a single word, containing a counter of allocated pages. It occupies the only page that is not of size 2^32 words.
• Page 0 is reserved for non-deterministically initialized memory.
• The last full page, number (2^32)-2, starting at address 2^64 - 2·(2^32), is reserved for static allocations.
• The two preceding pages, number 2^32-4 and 2^32-3 are used by the STARK verifier (when standard memory layouts are used).
• Pages 1 through 2^31-1 are dynamically allocated by the dynamic allocator snippet.
• Pages 2^31 through 2^32-5 are not in use by this crate.

Modules

dyn_malloc

memcpy

Constants

FIRST_NON_DETERMINISTICALLY_INITIALIZED_MEMORY_ADDRESS

Non-deterministically initialized memory lives in the range $[0: 2^{32})$

LAST_ADDRESS_AVAILABLE_FOR_NON_DETERMINISTICALLY_ALLOCATED_MEMORY

Functions

encode_to_memory

Stores the encoding of the given object into memory at the given address, and returns the address of the first untouched memory cell after.

first_free_nd_address

Returns the address of the first unpopulated word belonging to the memory region designated for non-determinism.

last_populated_nd_memory_address

Returns the address of the last populated word belonging to the memory region designated for non-determinism.

load_words_from_memory_leave_pointer

Return the code to read n words from memory. Top of stack must point to last word of words to read. Leaves mutated pointer on top of stack.

load_words_from_memory_pop_pointer

Return the code to read n words from memory. Top of stack must point to last word of words to read. Pops the memory pointer from the stack.

nd_memory_region

write_words_to_memory_leave_pointer

Return the code to write n words to memory. Leaves a modified pointer on the stack.

write_words_to_memory_pop_pointer

Return the code to write n words to memory. Pops the memory pointer.