diff --git a/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_indices.json b/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_indices.json index 65b6c2c0..434dfae1 100644 --- a/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_indices.json +++ b/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_indices.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 2347, "hash_table_height": 318, - "u32_table_height": 2621, + "u32_table_height": 2618, "op_stack_table_height": 1683, "ram_table_height": 208 }, @@ -15,7 +15,7 @@ "benchmark_result": { "clock_cycle_count": 4643, "hash_table_height": 342, - "u32_table_height": 5220, + "u32_table_height": 5217, "op_stack_table_height": 3331, "ram_table_height": 412 }, diff --git a/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_scalars.json b/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_scalars.json index a008df5d..45e9d362 100644 --- a/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_scalars.json +++ b/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_scalars.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 103, "hash_table_height": 96, - "u32_table_height": 44, + "u32_table_height": 41, "op_stack_table_height": 130, "ram_table_height": 34 }, @@ -15,7 +15,7 @@ "benchmark_result": { "clock_cycle_count": 454, "hash_table_height": 258, - "u32_table_height": 47, + "u32_table_height": 44, "op_stack_table_height": 886, "ram_table_height": 304 }, diff --git a/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_scalars_static_length_dyn_malloc_10.json b/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_scalars_static_length_dyn_malloc_10.json index 4d9c7c6f..40a25796 100644 --- a/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_scalars_static_length_dyn_malloc_10.json +++ b/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_scalars_static_length_dyn_malloc_10.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 50, "hash_table_height": 72, - "u32_table_height": 32, + "u32_table_height": 29, "op_stack_table_height": 89, "ram_table_height": 32 }, @@ -15,7 +15,7 @@ "benchmark_result": { "clock_cycle_count": 50, "hash_table_height": 72, - "u32_table_height": 32, + "u32_table_height": 29, "op_stack_table_height": 89, "ram_table_height": 32 }, diff --git a/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_scalars_static_length_dyn_malloc_100.json b/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_scalars_static_length_dyn_malloc_100.json index 39f179aa..d59787ed 100644 --- a/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_scalars_static_length_dyn_malloc_100.json +++ b/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_scalars_static_length_dyn_malloc_100.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 212, "hash_table_height": 414, - "u32_table_height": 32, + "u32_table_height": 29, "op_stack_table_height": 683, "ram_table_height": 302 }, @@ -15,7 +15,7 @@ "benchmark_result": { "clock_cycle_count": 212, "hash_table_height": 414, - "u32_table_height": 32, + "u32_table_height": 29, "op_stack_table_height": 683, "ram_table_height": 302 }, diff --git a/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_scalars_static_length_dyn_malloc_63.json b/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_scalars_static_length_dyn_malloc_63.json index 27164403..9982a769 100644 --- a/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_scalars_static_length_dyn_malloc_63.json +++ b/tasm-lib/benchmarks/tasmlib_hashing_algebraic_hasher_sample_scalars_static_length_dyn_malloc_63.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 146, "hash_table_height": 276, - "u32_table_height": 32, + "u32_table_height": 29, "op_stack_table_height": 441, "ram_table_height": 192 }, @@ -15,7 +15,7 @@ "benchmark_result": { "clock_cycle_count": 146, "hash_table_height": 276, - "u32_table_height": 32, + "u32_table_height": 29, "op_stack_table_height": 441, "ram_table_height": 192 }, diff --git a/tasm-lib/benchmarks/tasmlib_hashing_merkle_root.json b/tasm-lib/benchmarks/tasmlib_hashing_merkle_root.json index 51be3bb9..64d335ae 100644 --- a/tasm-lib/benchmarks/tasmlib_hashing_merkle_root.json +++ b/tasm-lib/benchmarks/tasmlib_hashing_merkle_root.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 6965, "hash_table_height": 3162, - "u32_table_height": 125, + "u32_table_height": 122, "op_stack_table_height": 13566, "ram_table_height": 7673 }, @@ -15,7 +15,7 @@ "benchmark_result": { "clock_cycle_count": 13651, "hash_table_height": 6234, - "u32_table_height": 142, + "u32_table_height": 139, "op_stack_table_height": 26904, "ram_table_height": 15353 }, diff --git a/tasm-lib/benchmarks/tasmlib_hashing_merkle_root_from_xfes_generic.json b/tasm-lib/benchmarks/tasmlib_hashing_merkle_root_from_xfes_generic.json index e235e6da..a1f71d15 100644 --- a/tasm-lib/benchmarks/tasmlib_hashing_merkle_root_from_xfes_generic.json +++ b/tasm-lib/benchmarks/tasmlib_hashing_merkle_root_from_xfes_generic.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 8285, "hash_table_height": 3234, - "u32_table_height": 166, + "u32_table_height": 160, "op_stack_table_height": 13600, "ram_table_height": 6653 }, @@ -15,7 +15,7 @@ "benchmark_result": { "clock_cycle_count": 16251, "hash_table_height": 6306, - "u32_table_height": 184, + "u32_table_height": 178, "op_stack_table_height": 26938, "ram_table_height": 13309 }, diff --git a/tasm-lib/benchmarks/tasmlib_hashing_sponge_hasher_squeeze.json b/tasm-lib/benchmarks/tasmlib_hashing_sponge_hasher_squeeze.json index 01c8e810..f18afd25 100644 --- a/tasm-lib/benchmarks/tasmlib_hashing_sponge_hasher_squeeze.json +++ b/tasm-lib/benchmarks/tasmlib_hashing_sponge_hasher_squeeze.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 29, "hash_table_height": 42, - "u32_table_height": 32, + "u32_table_height": 29, "op_stack_table_height": 41, "ram_table_height": 12 }, @@ -15,7 +15,7 @@ "benchmark_result": { "clock_cycle_count": 29, "hash_table_height": 42, - "u32_table_height": 32, + "u32_table_height": 29, "op_stack_table_height": 41, "ram_table_height": 12 }, diff --git a/tasm-lib/benchmarks/tasmlib_list_contiguous_list_get_pointer_list.json b/tasm-lib/benchmarks/tasmlib_list_contiguous_list_get_pointer_list.json index 910bb3d0..d976ccaf 100644 --- a/tasm-lib/benchmarks/tasmlib_list_contiguous_list_get_pointer_list.json +++ b/tasm-lib/benchmarks/tasmlib_list_contiguous_list_get_pointer_list.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 111, "hash_table_height": 84, - "u32_table_height": 32, + "u32_table_height": 29, "op_stack_table_height": 82, "ram_table_height": 9 }, @@ -15,7 +15,7 @@ "benchmark_result": { "clock_cycle_count": 186, "hash_table_height": 84, - "u32_table_height": 32, + "u32_table_height": 29, "op_stack_table_height": 142, "ram_table_height": 15 }, diff --git a/tasm-lib/benchmarks/tasmlib_list_higher_order_u32_filter_test_hash_xfield_element_lsb.json b/tasm-lib/benchmarks/tasmlib_list_higher_order_u32_filter_test_hash_xfield_element_lsb.json index 93bc2952..1fbaeed4 100644 --- a/tasm-lib/benchmarks/tasmlib_list_higher_order_u32_filter_test_hash_xfield_element_lsb.json +++ b/tasm-lib/benchmarks/tasmlib_list_higher_order_u32_filter_test_hash_xfield_element_lsb.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 870, "hash_table_height": 338, - "u32_table_height": 629, + "u32_table_height": 626, "op_stack_table_height": 836, "ram_table_height": 54 }, @@ -15,7 +15,7 @@ "benchmark_result": { "clock_cycle_count": 529, "hash_table_height": 286, - "u32_table_height": 349, + "u32_table_height": 346, "op_stack_table_height": 494, "ram_table_height": 36 }, diff --git a/tasm-lib/benchmarks/tasmlib_list_higher_order_u32_map_test_hash_xfield_element.json b/tasm-lib/benchmarks/tasmlib_list_higher_order_u32_map_test_hash_xfield_element.json index 41ed1fe7..1b8da027 100644 --- a/tasm-lib/benchmarks/tasmlib_list_higher_order_u32_map_test_hash_xfield_element.json +++ b/tasm-lib/benchmarks/tasmlib_list_higher_order_u32_map_test_hash_xfield_element.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 2870, "hash_table_height": 822, - "u32_table_height": 33, + "u32_table_height": 30, "op_stack_table_height": 3290, "ram_table_height": 437 }, @@ -15,7 +15,7 @@ "benchmark_result": { "clock_cycle_count": 3182, "hash_table_height": 900, - "u32_table_height": 33, + "u32_table_height": 30, "op_stack_table_height": 3650, "ram_table_height": 485 }, diff --git a/tasm-lib/benchmarks/tasmlib_list_higher_order_u32_zip_xfe_with_digest.json b/tasm-lib/benchmarks/tasmlib_list_higher_order_u32_zip_xfe_with_digest.json index b5341dce..4eb7cf52 100644 --- a/tasm-lib/benchmarks/tasmlib_list_higher_order_u32_zip_xfe_with_digest.json +++ b/tasm-lib/benchmarks/tasmlib_list_higher_order_u32_zip_xfe_with_digest.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 394, "hash_table_height": 96, - "u32_table_height": 32, + "u32_table_height": 29, "op_stack_table_height": 507, "ram_table_height": 262 }, @@ -15,7 +15,7 @@ "benchmark_result": { "clock_cycle_count": 294, "hash_table_height": 96, - "u32_table_height": 32, + "u32_table_height": 29, "op_stack_table_height": 367, "ram_table_height": 182 }, diff --git a/tasm-lib/benchmarks/tasmlib_list_new___digest.json b/tasm-lib/benchmarks/tasmlib_list_new___digest.json index af6164eb..dbfc55cd 100644 --- a/tasm-lib/benchmarks/tasmlib_list_new___digest.json +++ b/tasm-lib/benchmarks/tasmlib_list_new___digest.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 33, "hash_table_height": 36, - "u32_table_height": 32, + "u32_table_height": 29, "op_stack_table_height": 25, "ram_table_height": 3 }, @@ -15,7 +15,7 @@ "benchmark_result": { "clock_cycle_count": 33, "hash_table_height": 36, - "u32_table_height": 32, + "u32_table_height": 29, "op_stack_table_height": 25, "ram_table_height": 3 }, diff --git a/tasm-lib/benchmarks/tasmlib_list_range.json b/tasm-lib/benchmarks/tasmlib_list_range.json index 49927bf1..e5dc5c70 100644 --- a/tasm-lib/benchmarks/tasmlib_list_range.json +++ b/tasm-lib/benchmarks/tasmlib_list_range.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 916, "hash_table_height": 78, - "u32_table_height": 39, + "u32_table_height": 36, "op_stack_table_height": 767, "ram_table_height": 49 }, @@ -15,7 +15,7 @@ "benchmark_result": { "clock_cycle_count": 4811, "hash_table_height": 78, - "u32_table_height": 41, + "u32_table_height": 38, "op_stack_table_height": 4047, "ram_table_height": 254 }, diff --git a/tasm-lib/benchmarks/tasmlib_list_split_off_xfe.json b/tasm-lib/benchmarks/tasmlib_list_split_off_xfe.json index 32fb030a..25ebac92 100644 --- a/tasm-lib/benchmarks/tasmlib_list_split_off_xfe.json +++ b/tasm-lib/benchmarks/tasmlib_list_split_off_xfe.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 512, "hash_table_height": 144, - "u32_table_height": 299, + "u32_table_height": 296, "op_stack_table_height": 559, "ram_table_height": 305 }, @@ -15,7 +15,7 @@ "benchmark_result": { "clock_cycle_count": 8492, "hash_table_height": 144, - "u32_table_height": 7066, + "u32_table_height": 7063, "op_stack_table_height": 9679, "ram_table_height": 6005 }, diff --git a/tasm-lib/benchmarks/tasmlib_memory_dyn_malloc.json b/tasm-lib/benchmarks/tasmlib_memory_dyn_malloc.json index 7886cbda..f5bb813c 100644 --- a/tasm-lib/benchmarks/tasmlib_memory_dyn_malloc.json +++ b/tasm-lib/benchmarks/tasmlib_memory_dyn_malloc.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 22, "hash_table_height": 30, - "u32_table_height": 32, + "u32_table_height": 29, "op_stack_table_height": 19, "ram_table_height": 2 }, @@ -15,7 +15,7 @@ "benchmark_result": { "clock_cycle_count": 22, "hash_table_height": 30, - "u32_table_height": 32, + "u32_table_height": 29, "op_stack_table_height": 19, "ram_table_height": 2 }, diff --git a/tasm-lib/benchmarks/tasmlib_mmr_calculate_new_peaks_from_append.json b/tasm-lib/benchmarks/tasmlib_mmr_calculate_new_peaks_from_append.json index b6d64861..2e058e8a 100644 --- a/tasm-lib/benchmarks/tasmlib_mmr_calculate_new_peaks_from_append.json +++ b/tasm-lib/benchmarks/tasmlib_mmr_calculate_new_peaks_from_append.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 3570, "hash_table_height": 396, - "u32_table_height": 164, + "u32_table_height": 161, "op_stack_table_height": 3442, "ram_table_height": 942 }, @@ -15,7 +15,7 @@ "benchmark_result": { "clock_cycle_count": 7037, "hash_table_height": 582, - "u32_table_height": 164, + "u32_table_height": 161, "op_stack_table_height": 6814, "ram_table_height": 1872 }, diff --git a/tasm-lib/benchmarks/tasmlib_neptune_mutator_get_swbf_indices_1048576_45.json b/tasm-lib/benchmarks/tasmlib_neptune_mutator_get_swbf_indices_1048576_45.json index 5f37a7f4..5d0b5be0 100644 --- a/tasm-lib/benchmarks/tasmlib_neptune_mutator_get_swbf_indices_1048576_45.json +++ b/tasm-lib/benchmarks/tasmlib_neptune_mutator_get_swbf_indices_1048576_45.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 4618, "hash_table_height": 481, - "u32_table_height": 4633, + "u32_table_height": 4627, "op_stack_table_height": 3464, "ram_table_height": 469 }, @@ -15,7 +15,7 @@ "benchmark_result": { "clock_cycle_count": 4618, "hash_table_height": 481, - "u32_table_height": 4507, + "u32_table_height": 4501, "op_stack_table_height": 3464, "ram_table_height": 469 }, diff --git a/tasm-lib/benchmarks/tasmlib_verifier_fri_verify.json b/tasm-lib/benchmarks/tasmlib_verifier_fri_verify.json index 6c3bc686..19b004b1 100644 --- a/tasm-lib/benchmarks/tasmlib_verifier_fri_verify.json +++ b/tasm-lib/benchmarks/tasmlib_verifier_fri_verify.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 47806, "hash_table_height": 14670, - "u32_table_height": 17930, + "u32_table_height": 17894, "op_stack_table_height": 47915, "ram_table_height": 17532 }, @@ -15,7 +15,7 @@ "benchmark_result": { "clock_cycle_count": 47806, "hash_table_height": 14670, - "u32_table_height": 17326, + "u32_table_height": 17290, "op_stack_table_height": 47915, "ram_table_height": 17532 }, diff --git a/tasm-lib/benchmarks/tasmlib_verifier_stark_verify_dynamic_inner_padded_height_256_fri_exp_4.json b/tasm-lib/benchmarks/tasmlib_verifier_stark_verify_dynamic_inner_padded_height_256_fri_exp_4.json index f12dbd35..c8c8c89e 100644 --- a/tasm-lib/benchmarks/tasmlib_verifier_stark_verify_dynamic_inner_padded_height_256_fri_exp_4.json +++ b/tasm-lib/benchmarks/tasmlib_verifier_stark_verify_dynamic_inner_padded_height_256_fri_exp_4.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 195675, "hash_table_height": 139885, - "u32_table_height": 25831, + "u32_table_height": 25451, "op_stack_table_height": 178100, "ram_table_height": 285557 }, diff --git a/tasm-lib/benchmarks/tasmlib_verifier_stark_verify_dynamic_inner_padded_height_512_fri_exp_4.json b/tasm-lib/benchmarks/tasmlib_verifier_stark_verify_dynamic_inner_padded_height_512_fri_exp_4.json index 46d92f9a..025833a7 100644 --- a/tasm-lib/benchmarks/tasmlib_verifier_stark_verify_dynamic_inner_padded_height_512_fri_exp_4.json +++ b/tasm-lib/benchmarks/tasmlib_verifier_stark_verify_dynamic_inner_padded_height_512_fri_exp_4.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 204428, "hash_table_height": 147577, - "u32_table_height": 33586, + "u32_table_height": 34195, "op_stack_table_height": 184228, "ram_table_height": 286735 }, diff --git a/tasm-lib/benchmarks/tasmlib_verifier_stark_verify_static_inner_padded_height_256_fri_exp_4.json b/tasm-lib/benchmarks/tasmlib_verifier_stark_verify_static_inner_padded_height_256_fri_exp_4.json index a7b8022a..728a544a 100644 --- a/tasm-lib/benchmarks/tasmlib_verifier_stark_verify_static_inner_padded_height_256_fri_exp_4.json +++ b/tasm-lib/benchmarks/tasmlib_verifier_stark_verify_static_inner_padded_height_256_fri_exp_4.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 184245, "hash_table_height": 126169, - "u32_table_height": 25442, + "u32_table_height": 25582, "op_stack_table_height": 170476, "ram_table_height": 281749 }, diff --git a/tasm-lib/benchmarks/tasmlib_verifier_stark_verify_static_inner_padded_height_512_fri_exp_4.json b/tasm-lib/benchmarks/tasmlib_verifier_stark_verify_static_inner_padded_height_512_fri_exp_4.json index 32174e63..3168d91d 100644 --- a/tasm-lib/benchmarks/tasmlib_verifier_stark_verify_static_inner_padded_height_512_fri_exp_4.json +++ b/tasm-lib/benchmarks/tasmlib_verifier_stark_verify_static_inner_padded_height_512_fri_exp_4.json @@ -4,7 +4,7 @@ "benchmark_result": { "clock_cycle_count": 192998, "hash_table_height": 133861, - "u32_table_height": 34039, + "u32_table_height": 33485, "op_stack_table_height": 176604, "ram_table_height": 282927 }, diff --git a/tasm-lib/src/hashing/sponge_hasher/squeeze.rs b/tasm-lib/src/hashing/sponge_hasher/squeeze.rs index 847dc7ad..b310e480 100644 --- a/tasm-lib/src/hashing/sponge_hasher/squeeze.rs +++ b/tasm-lib/src/hashing/sponge_hasher/squeeze.rs @@ -72,7 +72,6 @@ mod test { use rand::prelude::*; use triton_vm::twenty_first::prelude::Sponge; - use crate::empty_stack; use crate::memory::dyn_malloc; use crate::memory::dyn_malloc::DYN_MALLOC_ADDRESS; use crate::rust_shadowing_helper_functions; @@ -124,7 +123,7 @@ mod test { let mut unstructured = Unstructured::new(&bytes); ProcedureInitialState { - stack: empty_stack(), + stack: self.init_stack_for_isolated_run(), nondeterminism: NonDeterminism::default().with_ram(init_memory), public_input: Vec::default(), sponge: Some(Tip5::arbitrary(&mut unstructured).unwrap()), diff --git a/tasm-lib/src/memory.rs b/tasm-lib/src/memory.rs index 2aa1f4af..e6447438 100644 --- a/tasm-lib/src/memory.rs +++ b/tasm-lib/src/memory.rs @@ -39,6 +39,9 @@ pub const FIRST_NON_DETERMINISTICALLY_INITIALIZED_MEMORY_ADDRESS: BFieldElement pub const LAST_ADDRESS_AVAILABLE_FOR_NON_DETERMINISTICALLY_ALLOCATED_MEMORY: BFieldElement = BFieldElement::new(u32::MAX as u64); +/// The number of pages that can be dynamically allocated. +pub const NUM_PAGES_FOR_DYN_MALLOC: u64 = (1 << 31) - 1; + /// Returns the address of the last populated word belonging to the memory region /// designated for non-determinism. pub fn last_populated_nd_memory_address( diff --git a/tasm-lib/src/memory/dyn_malloc.rs b/tasm-lib/src/memory/dyn_malloc.rs index d0fe405a..579b2f03 100644 --- a/tasm-lib/src/memory/dyn_malloc.rs +++ b/tasm-lib/src/memory/dyn_malloc.rs @@ -14,22 +14,38 @@ use crate::snippet_bencher::BenchmarkCase; use crate::traits::function::Function; use crate::traits::function::FunctionInitialState; +use super::NUM_PAGES_FOR_DYN_MALLOC; + /// The location of the dynamic allocator state in memory. /// /// See the [memory convention][super] for details. pub const DYN_MALLOC_ADDRESS: BFieldElement = BFieldElement::new(BFieldElement::MAX); -/// The address of the first page that can be dynamically allocated. -pub const DYN_MALLOC_FIRST_PAGE: u64 = 1; +/// Initial counter-value if the dynamic allocator state is not initialized. +pub const DYN_MALLOC_INIT_COUNTER: u64 = 1; + +/// Constant that adds extra space between each allocated memory page. Since no +/// program needs all available [NUM_PAGES_FOR_DYN_MALLOC], only every N pages +/// need to be available for the dynamic allocator. If this constant is set to +/// 1, then all pages available for dynamic allocation can be returned. +pub const INTERSPERCE_PARAMETER: u64 = 1 << 3; -/// The number of pages that can be dynamically allocated. -pub const NUM_ALLOCATABLE_PAGES: u64 = (1 << 31) - 1; +/// The number of different pages this snippet can allocate. If the state of +/// the dynamic allocator is initialized to zero, this is also the number of +/// times this memory allocator can be called before crashing due to running +/// out of memory. +pub const NUM_ALLOCATABLE_PAGES: u64 = NUM_PAGES_FOR_DYN_MALLOC / INTERSPERCE_PARAMETER; /// The size of one dynamically allocated page. pub const DYN_MALLOC_PAGE_SIZE: u64 = 1 << 32; +/// The number of words seperating each subsequent page allocated by this +/// snippet. +pub const NUM_WORDS_BETWEEN_ALLOCATED_PAGES: u64 = INTERSPERCE_PARAMETER * DYN_MALLOC_PAGE_SIZE; + +/// The address of the first page that can be dynamically allocated. pub const DYN_MALLOC_FIRST_ADDRESS: BFieldElement = - BFieldElement::new(DYN_MALLOC_FIRST_PAGE * DYN_MALLOC_PAGE_SIZE); + BFieldElement::new(DYN_MALLOC_INIT_COUNTER * NUM_WORDS_BETWEEN_ALLOCATED_PAGES); /// Return a pointer to the next free page of memory. Updates the dyn malloc state /// accordingly @@ -40,7 +56,7 @@ impl DynMalloc { pub fn memory_region() -> MemoryRegion { MemoryRegion::new( DYN_MALLOC_FIRST_ADDRESS, - (NUM_ALLOCATABLE_PAGES * DYN_MALLOC_PAGE_SIZE) + (NUM_PAGES_FOR_DYN_MALLOC * DYN_MALLOC_PAGE_SIZE) .try_into() .unwrap(), ) @@ -88,15 +104,17 @@ impl BasicSnippet for DynMalloc { write_mem 1 pop 1 // _ page_idx // translate page number to address - push {DYN_MALLOC_PAGE_SIZE} // _ page_idx page_size - mul // _ *free_page + push {NUM_WORDS_BETWEEN_ALLOCATED_PAGES} + mul + // _ *free_page + return // BEFORE: _ 0 // AFTER: _ DYN_MALLOC_FIRST_PAGE {dyn_malloc_init}: pop 1 - push {DYN_MALLOC_FIRST_PAGE} + push {DYN_MALLOC_INIT_COUNTER} return } } @@ -110,7 +128,7 @@ impl Function for DynMalloc { ) { let mut page_idx = memory.get(&DYN_MALLOC_ADDRESS).copied().unwrap_or_default(); if page_idx.is_zero() { - page_idx = DYN_MALLOC_FIRST_PAGE.into(); + page_idx = DYN_MALLOC_INIT_COUNTER.into(); } let page_idx = page_idx; @@ -123,7 +141,7 @@ impl Function for DynMalloc { memory.insert(DYN_MALLOC_ADDRESS, next_page_idx); - let page_address = page_idx * BFieldElement::new(DYN_MALLOC_PAGE_SIZE); + let page_address = page_idx * bfe!(NUM_WORDS_BETWEEN_ALLOCATED_PAGES); stack.push(page_address); } @@ -137,7 +155,7 @@ impl Function for DynMalloc { let stack = empty_stack(); let mut memory = HashMap::new(); - let page_number = rng.gen_range(0..(1u64 << 31)); + let page_number = rng.gen_range(0..NUM_ALLOCATABLE_PAGES); memory.insert(DYN_MALLOC_ADDRESS, page_number.into()); FunctionInitialState { stack, memory } @@ -231,6 +249,9 @@ mod tests { negative_prop_disallow_allocation_outside_of_region(bfe!(NUM_ALLOCATABLE_PAGES)); negative_prop_disallow_allocation_outside_of_region(bfe!(NUM_ALLOCATABLE_PAGES + 1)); negative_prop_disallow_allocation_outside_of_region(bfe!(NUM_ALLOCATABLE_PAGES + 2)); + negative_prop_disallow_allocation_outside_of_region(bfe!(NUM_ALLOCATABLE_PAGES * 2)); + negative_prop_disallow_allocation_outside_of_region(bfe!(u32::MAX / 2 - 1)); + negative_prop_disallow_allocation_outside_of_region(bfe!(u32::MAX / 2)); negative_prop_disallow_allocation_outside_of_region(bfe!(u32::MAX - 1)); negative_prop_disallow_allocation_outside_of_region(bfe!(u32::MAX)); }