diff --git a/triton-vm/src/aet.rs b/triton-vm/src/aet.rs index b94219b5b..3c109a6e0 100644 --- a/triton-vm/src/aet.rs +++ b/triton-vm/src/aet.rs @@ -335,7 +335,7 @@ impl AlgebraicExecutionTrace { fn record_ram_call(&mut self, ram_call: RamTableCall) { self.ram_trace - .append(Axis(0), ram_call.to_table_rows().view()) + .push_row(ram_call.to_table_row().view()) .unwrap(); } } diff --git a/triton-vm/src/example_programs.rs b/triton-vm/src/example_programs.rs index 59837ad26..917bc0d1e 100644 --- a/triton-vm/src/example_programs.rs +++ b/triton-vm/src/example_programs.rs @@ -128,7 +128,7 @@ fn merkle_tree_authentication_path_verify() -> Program { // stack before: [* r4 r3 r2 r1 r0] // stack after: [* r4 r3 r2 r1 r0] check_aps: - push 1 read_mem 1 pop 1 dup 0 // get number of APs left to check + push 0 read_mem 1 pop 1 dup 0 // get number of APs left to check // stack: [* r4 r3 r2 r1 r0 num_left num_left] push 0 eq // see if there are authentication paths left // stack: [* r4 r3 r2 r1 r0 0 num_left num_left==0] @@ -205,21 +205,21 @@ fn verify_sudoku() -> Program { // inconsistency is found. initialize_flag: push 1 // _ 1 - push 9 // _ 1 9 - write_mem 1 // _ 10 + push 0 // _ 1 0 + write_mem 1 // _ 1 pop 1 // _ return invalidate_flag: push 0 // _ 0 - push 9 // _ 0 9 - write_mem 1 // _ 10 + push 0 // _ 0 0 + write_mem 1 // _ 1 pop 1 // _ return assert_flag: - push 10 // _ 10 - read_mem 1 // _ flag 9 + push 0 // _ 0 + read_mem 1 // _ flag -1 pop 1 // _ flag assert // _ halt @@ -230,7 +230,7 @@ fn verify_sudoku() -> Program { push 23 push 19 push 17 push 13 push 11 push 7 push 5 push 3 push 2 - push 0 write_mem 5 write_mem 4 + push 1 write_mem 5 write_mem 4 pop 1 return @@ -276,6 +276,7 @@ fn verify_sudoku() -> Program { return check_columns: + push 82 call check_one_column push 83 call check_one_column push 84 call check_one_column push 85 call check_one_column @@ -284,7 +285,6 @@ fn verify_sudoku() -> Program { push 88 call check_one_column push 89 call check_one_column push 90 call check_one_column - push 91 call check_one_column return check_one_column: @@ -295,15 +295,15 @@ fn verify_sudoku() -> Program { return check_squares: - push 31 call check_one_square - push 34 call check_one_square - push 37 call check_one_square - push 58 call check_one_square - push 61 call check_one_square - push 64 call check_one_square - push 85 call check_one_square - push 88 call check_one_square - push 91 call check_one_square + push 30 call check_one_square + push 33 call check_one_square + push 36 call check_one_square + push 57 call check_one_square + push 60 call check_one_square + push 63 call check_one_square + push 84 call check_one_square + push 87 call check_one_square + push 90 call check_one_square return check_one_square: @@ -470,20 +470,20 @@ pub(crate) fn calculate_new_mmr_peaks_from_append_with_safe_lists() -> Program { // After: _ tasm_list_safe_u32_push_digest: dup 5 // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list - push 2 add // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list+2 - read_mem 2 // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] capacity len *list + push 1 add // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list+1 + read_mem 2 // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] capacity len *list-1 // Verify that length < capacity - swap 2 // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list len capacity - dup 1 // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list len capacity len - lt // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list len capacity>len - assert // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list len + swap 2 // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list-1 len capacity + dup 1 // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list-1 len capacity len + lt // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list-1 len capacity>len + assert // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list-1 len // Adjust ram pointer - push 5 // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list len 5 - mul // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list 5·len - add // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list+5·len - push 2 // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list+5·len 2 + push 5 // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list-1 len 5 + mul // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list-1 5·len + add // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list+5·len-1 + push 3 // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list+5·len 3 add // _ *list elem[4] elem[3] elem[2] elem[1] elem[0] *list+5·len+2 // Write all elements @@ -493,8 +493,8 @@ pub(crate) fn calculate_new_mmr_peaks_from_append_with_safe_lists() -> Program { pop 1 // _ *list // Increase length indicator by one - push 1 add // _ *list+1 - read_mem 1 // _ len *list + read_mem 1 // _ len *list-1 + push 1 add // _ len *list swap 1 // _ *list len push 1 // _ *list len 1 add // _ *list len+1 @@ -590,8 +590,8 @@ pub(crate) fn calculate_new_mmr_peaks_from_append_with_safe_lists() -> Program { // Before: _ *list // After: _ elem{N - 1}, elem{N - 2}, ..., elem{0} tasm_list_safe_u32_pop_digest: - push 1 add // _ *list+1 - read_mem 1 // _ len *list + read_mem 1 // _ len *list-1 + push 1 add // _ len *list // Assert that length is not 0 dup 1 // _ len *list len @@ -607,13 +607,14 @@ pub(crate) fn calculate_new_mmr_peaks_from_append_with_safe_lists() -> Program { add // _ len *list len-1 swap 1 // _ len len-1 *list write_mem 1 // _ len *list+1 + push -1 add // _ len *list // Read elements - swap 1 // _ *list+1 len - push 5 // _ *list+1 len 5 - mul // _ *list+1 5·len - // _ *list+1 offset_for_last_element - add // _ *list+offset_for_last_element+1 + swap 1 // _ *list len + push 5 // _ *list len 5 + mul // _ *list 5·len + // _ *list offset_for_last_element + add // _ *list+offset_for_last_element // _ address_for_last_element read_mem 5 // _ [elements] address_for_last_element-5 pop 1 // _ [elements] @@ -663,18 +664,18 @@ pub(crate) fn calculate_new_mmr_peaks_from_append_with_safe_lists() -> Program { // Before: _ size // After: _ *next_addr tasm_memory_dyn_malloc: - push 1 // _ size *free_pointer+1 - read_mem 1 // _ size *next_addr' *free_pointer - swap 1 // _ size *free_pointer *next_addr' + push 0 // _ size *free_pointer + read_mem 1 // _ size *next_addr' *free_pointer-1 + pop 1 // _ size *next_addr' // add 1 iff `next_addr` was 0, i.e. uninitialized. - dup 0 // _ size *free_pointer *next_addr' *next_addr' - push 0 // _ size *free_pointer *next_addr' *next_addr' 0 - eq // _ size *free_pointer *next_addr' (*next_addr' == 0) - add // _ size *free_pointer *next_addr + dup 0 // _ size *next_addr' *next_addr' + push 0 // _ size *next_addr' *next_addr' 0 + eq // _ size *next_addr' (*next_addr' == 0) + add // _ size *next_addr - dup 0 // _ size *free_pointer *next_addr *next_addr - dup 3 // _ size *free_pointer *next_addr *next_addr size + dup 0 // _ size *next_addr *next_addr + dup 2 // _ size *next_addr *next_addr size // Ensure that `size` does not exceed 2^32 split @@ -693,10 +694,10 @@ pub(crate) fn calculate_new_mmr_peaks_from_append_with_safe_lists() -> Program { eq assert - swap 1 // _ size *free_pointer *(next_addr + size) *next_addr - swap 3 // _ *next_addr *free_pointer *(next_addr + size) size - pop 1 // _ *next_addr *free_pointer *(next_addr + size) - swap 1 // _ *next_addr *(next_addr + size) *free_pointer + swap 1 // _ size *(next_addr + size) *next_addr + swap 2 // _ *next_addr *(next_addr + size) size + pop 1 // _ *next_addr *(next_addr + size) + push 0 // _ *next_addr *(next_addr + size) *free_pointer write_mem 1 // _ *next_addr *free_pointer+1 pop 1 // _ *next_addr return diff --git a/triton-vm/src/lib.rs b/triton-vm/src/lib.rs index ef98442f0..e35da4f9b 100644 --- a/triton-vm/src/lib.rs +++ b/triton-vm/src/lib.rs @@ -97,11 +97,11 @@ //! return //! //! sum_of_squares_ram: -//! push 18 // 18 +//! push 17 // 18 //! read_mem 1 // s₄ 17 //! pop 1 // s₄ //! dup 0 mul // s₄² -//! push 43 // s₄² 43 +//! push 42 // s₄² 43 //! read_mem 1 // s₄² s₅ 42 //! pop 1 // s₄² s₅ //! dup 0 mul // s₄² s₅² @@ -618,8 +618,8 @@ mod tests { #[test] fn lib_use_initial_ram() { let program = triton_program!( - push 52 read_mem 1 pop 1 - push 43 read_mem 1 pop 1 + push 51 read_mem 1 pop 1 + push 42 read_mem 1 pop 1 mul write_io 1 halt ); diff --git a/triton-vm/src/stark.rs b/triton-vm/src/stark.rs index 7dac3c6de..222bcbb39 100644 --- a/triton-vm/src/stark.rs +++ b/triton-vm/src/stark.rs @@ -1221,11 +1221,11 @@ pub(crate) mod tests { let program = triton_program!( push 9 push 8 push 5 write_mem 2 pop 1 // write 8 to address 5, 9 to address 6 push 18 push 15 write_mem 1 pop 1 // write 18 to address 15 - push 6 read_mem 1 pop 2 // read from address 5 - push 16 read_mem 1 pop 2 // read from address 15 + push 5 read_mem 1 pop 2 // read from address 5 + push 15 read_mem 1 pop 2 // read from address 15 push 7 push 5 write_mem 1 pop 1 // write 7 to address 5 - push 16 read_mem 1 // _ 18 15 - push 6 read_mem 1 // _ 18 15 7 5 + push 15 read_mem 1 // _ 18 14 + push 5 read_mem 1 // _ 18 14 7 4 halt ); let (_, _, master_base_table, _, _) = @@ -2126,6 +2126,13 @@ pub(crate) mod tests { ) } + #[test] + fn claim_in_ram_corresponds_to_currently_running_program() { + triton_table_constraints_evaluate_to_zero( + test_program_claim_in_ram_corresponds_to_currently_running_program(), + ); + } + fn triton_table_constraints_evaluate_to_zero(program_and_input: ProgramAndInput) { let (_, _, master_base_table, master_ext_table, challenges) = master_tables_for_low_security_level(program_and_input); diff --git a/triton-vm/src/table/processor_table.rs b/triton-vm/src/table/processor_table.rs index 2b119787f..66d8855be 100644 --- a/triton-vm/src/table/processor_table.rs +++ b/triton-vm/src/table/processor_table.rs @@ -404,23 +404,21 @@ impl ProcessorTable { } let previous_row = maybe_previous_row?; - let previous_instruction = Self::instruction_from_row(previous_row)?; + let instruction = Self::instruction_from_row(previous_row)?; - let instruction_type = match previous_instruction { + let instruction_type = match instruction { ReadMem(_) => ram_table::INSTRUCTION_TYPE_READ, WriteMem(_) => ram_table::INSTRUCTION_TYPE_WRITE, _ => return None, }; // longer stack means relevant information is on top of stack, i.e., in stack registers - let row_with_longer_stack = match previous_instruction { + let row_with_longer_stack = match instruction { ReadMem(_) => current_row.view(), WriteMem(_) => previous_row.view(), _ => unreachable!(), }; - let op_stack_delta = previous_instruction - .op_stack_size_influence() - .unsigned_abs() as usize; + let op_stack_delta = instruction.op_stack_size_influence().unsigned_abs() as usize; let mut factor = XFieldElement::one(); for ram_pointer_offset in 0..op_stack_delta { @@ -428,10 +426,8 @@ impl ProcessorTable { let ram_value_index = ram_pointer_offset + num_ram_pointers; let ram_value_column = Self::op_stack_column_by_index(ram_value_index); let ram_value = row_with_longer_stack[ram_value_column.base_table_index()]; - - let ram_pointer = row_with_longer_stack[ST0.base_table_index()]; - let offset = BFieldElement::new(ram_pointer_offset as u64); - let offset_ram_pointer = ram_pointer + offset; + let offset_ram_pointer = + Self::offset_ram_pointer(instruction, row_with_longer_stack, ram_pointer_offset); let clk = previous_row[CLK.base_table_index()]; let compressed_row = clk * challenges[RamClkWeight] @@ -443,6 +439,23 @@ impl ProcessorTable { Some(factor) } + fn offset_ram_pointer( + instruction: Instruction, + row_with_longer_stack: ArrayView1, + ram_pointer_offset: usize, + ) -> BFieldElement { + let ram_pointer = row_with_longer_stack[ST0.base_table_index()]; + let offset = BFieldElement::new(ram_pointer_offset as u64); + + match instruction { + // adjust for ram_pointer pointing in front of last-read address: + // `push 0 read_mem 1` leaves stack as `_ a -1` where `a` was read from address 0. + ReadMem(_) => ram_pointer + offset + BFIELD_ONE, + WriteMem(_) => ram_pointer + offset, + _ => unreachable!(), + } + } + fn instruction_from_row(row: ArrayView1) -> Option { let opcode = row[CI.base_table_index()]; let instruction: Instruction = opcode.try_into().ok()?; @@ -2965,8 +2978,14 @@ impl ExtProcessorTable { let ram_value_column = ProcessorTable::op_stack_column_by_index(ram_value_index); let ram_value = row_with_longer_stack(ram_value_column); + let additional_offset = match instruction_type { + ram_table::INSTRUCTION_TYPE_READ => 1, + ram_table::INSTRUCTION_TYPE_WRITE => 0, + _ => panic!("Invalid instruction type"), + }; + let ram_pointer = row_with_longer_stack(ST0); - let offset = constant(ram_pointer_offset as u32); + let offset = constant(additional_offset + ram_pointer_offset as u32); let offset_ram_pointer = ram_pointer + offset; let compressed_row = curr_base_row(CLK) * challenge(RamClkWeight) @@ -3839,7 +3858,7 @@ pub(crate) mod tests { triton_program!(push 4 read_mem 4 push 0 eq assert swap 3 push 4 eq assert halt), triton_program!(push 5 read_mem 5 push 0 eq assert swap 4 push 5 eq assert halt), ]; - let initial_ram = (0..5).map(|i| (i, i + 1)).collect(); + let initial_ram = (1..=5).map(|i| (i, i)).collect(); let non_determinism = NonDeterminism::default().with_ram(initial_ram); let programs_with_input = programs.map(|program| ProgramAndInput { program, diff --git a/triton-vm/src/table/ram_table.rs b/triton-vm/src/table/ram_table.rs index da755f635..7a4903dd8 100644 --- a/triton-vm/src/table/ram_table.rs +++ b/triton-vm/src/table/ram_table.rs @@ -5,7 +5,6 @@ use itertools::Itertools; use ndarray::parallel::prelude::*; use ndarray::s; use ndarray::Array1; -use ndarray::Array2; use ndarray::ArrayView1; use ndarray::ArrayView2; use ndarray::ArrayViewMut2; @@ -43,31 +42,23 @@ pub(crate) const PADDING_INDICATOR: BFieldElement = BFieldElement::new(2); pub struct RamTableCall { pub clk: u32, pub ram_pointer: BFieldElement, + pub ram_value: BFieldElement, pub is_write: bool, - pub values: Vec, } impl RamTableCall { - pub fn to_table_rows(self) -> Array2 { + pub fn to_table_row(self) -> Array1 { let instruction_type = match self.is_write { true => INSTRUCTION_TYPE_WRITE, false => INSTRUCTION_TYPE_READ, }; - let num_values = self.values.len(); - let pointers = (0..num_values) - .map(|offset| self.ram_pointer + BFieldElement::from(offset as u32)) - .collect::>(); - let values = Array1::from(self.values); - - let mut rows = Array2::zeros((num_values, BASE_WIDTH)); - rows.column_mut(CLK.base_table_index()) - .fill(self.clk.into()); - rows.column_mut(InstructionType.base_table_index()) - .fill(instruction_type); - rows.column_mut(RamPointer.base_table_index()) - .assign(&pointers); - rows.column_mut(RamValue.base_table_index()).assign(&values); - rows + + let mut row = Array1::zeros(BASE_WIDTH); + row[CLK.base_table_index()] = self.clk.into(); + row[InstructionType.base_table_index()] = instruction_type; + row[RamPointer.base_table_index()] = self.ram_pointer; + row[RamValue.base_table_index()] = self.ram_value; + row } } @@ -533,10 +524,10 @@ pub(crate) mod tests { use super::*; #[proptest] - fn ram_table_call_can_be_converted_to_table_rows( + fn ram_table_call_can_be_converted_to_table_row( #[strategy(arb())] ram_table_call: RamTableCall, ) { - let _ = ram_table_call.to_table_rows(); + let _ = ram_table_call.to_table_row(); } pub fn constraints_evaluate_to_zero( diff --git a/triton-vm/src/vm.rs b/triton-vm/src/vm.rs index c19412327..767b25574 100644 --- a/triton-vm/src/vm.rs +++ b/triton-vm/src/vm.rs @@ -61,6 +61,8 @@ pub struct VMState<'pgm> { /// The read-write **random-access memory** allows Triton VM to store arbitrary data. pub ram: HashMap, + ram_calls: Vec, + /// The **Op-stack memory** stores Triton VM's entire operational stack. pub op_stack: OpStack, @@ -122,6 +124,7 @@ impl<'pgm> VMState<'pgm> { secret_individual_tokens: non_determinism.individual_tokens.into(), secret_digests: non_determinism.digests.into(), ram: non_determinism.ram, + ram_calls: vec![], op_stack: OpStack::new(program_digest), jump_stack: vec![], cycle_count: 0, @@ -267,6 +270,14 @@ impl<'pgm> VMState<'pgm> { .collect() } + fn start_recording_ram_calls(&mut self) { + self.ram_calls.clear(); + } + + fn stop_recording_ram_calls(&mut self) -> Vec { + self.ram_calls.drain(..).map(RamCall).collect() + } + fn pop(&mut self, n: NumberOfWords) -> Result> { for _ in 0..n.num_words() { self.op_stack.pop()?; @@ -368,53 +379,59 @@ impl<'pgm> VMState<'pgm> { } fn read_mem(&mut self, n: NumberOfWords) -> Result> { + self.start_recording_ram_calls(); let mut ram_pointer = self.op_stack.pop()?; - - let mut ram_values = vec![]; for _ in 0..n.num_words() { - ram_pointer.decrement(); - let ram_value = self.ram.get(&ram_pointer).copied().unwrap_or(BFIELD_ZERO); + let ram_value = self.ram_read(ram_pointer)?; self.op_stack.push(ram_value); - ram_values.push(ram_value); + ram_pointer.decrement(); } - ram_values.reverse(); - self.op_stack.push(ram_pointer); - - let ram_table_call = RamTableCall { - clk: self.cycle_count, - ram_pointer, - is_write: false, - values: ram_values, - }; + let ram_calls = self.stop_recording_ram_calls(); self.instruction_pointer += 2; - Ok(vec![RamCall(ram_table_call)]) + Ok(ram_calls) } fn write_mem(&mut self, n: NumberOfWords) -> Result> { + self.start_recording_ram_calls(); let mut ram_pointer = self.op_stack.pop()?; - - let mut ram_values = vec![]; for _ in 0..n.num_words() { let ram_value = self.op_stack.pop()?; - self.ram.insert(ram_pointer, ram_value); - ram_values.push(ram_value); + self.ram_write(ram_pointer, ram_value); ram_pointer.increment(); } - self.op_stack.push(ram_pointer); + let ram_calls = self.stop_recording_ram_calls(); + + self.instruction_pointer += 2; + Ok(ram_calls) + } + + fn ram_read(&mut self, ram_pointer: BFieldElement) -> Result { + let ram_value = self.ram.get(&ram_pointer).copied().unwrap_or(BFIELD_ZERO); - ram_pointer -= n.into(); let ram_table_call = RamTableCall { clk: self.cycle_count, ram_pointer, + ram_value, + is_write: false, + }; + self.ram_calls.push(ram_table_call); + + Ok(ram_value) + } + + fn ram_write(&mut self, ram_pointer: BFieldElement, ram_value: BFieldElement) { + let ram_table_call = RamTableCall { + clk: self.cycle_count, + ram_pointer, + ram_value, is_write: true, - values: ram_values, }; + self.ram_calls.push(ram_table_call); - self.instruction_pointer += 2; - Ok(vec![RamCall(ram_table_call)]) + self.ram.insert(ram_pointer, ram_value); } fn hash(&mut self) -> Result> { @@ -966,6 +983,7 @@ pub(crate) mod tests { use strum::IntoEnumIterator; use test_strategy::proptest; use twenty_first::shared_math::b_field_element::BFIELD_ZERO; + use twenty_first::shared_math::bfield_codec::BFieldCodec; use twenty_first::shared_math::other::random_elements; use twenty_first::shared_math::other::random_elements_array; use twenty_first::shared_math::polynomial::Polynomial; @@ -986,6 +1004,7 @@ pub(crate) mod tests { use crate::table::processor_table::ProcessorTraceRow; use crate::triton_asm; use crate::triton_program; + use crate::Claim; use super::*; @@ -1083,7 +1102,8 @@ pub(crate) mod tests { push 3 push 1 push 2 // _ 3 1 2 push 7 // _ 3 1 2 7 write_mem 3 // _ 10 - read_mem 2 // _ 3 1 8 + push -1 add // _ 9 + read_mem 2 // _ 3 1 7 pop 1 // _ 3 1 assert halt // _ 3 }) @@ -1638,7 +1658,6 @@ pub(crate) mod tests { // - Some addresses are read before written to. // - Other addresses are written to before read. for address in memory_addresses.iter().take(num_memory_accesses / 4) { - let address = address.value() + 1; instructions.extend(triton_asm!(push {address} read_mem 1 pop 1 push 0 eq assert)); } @@ -1654,7 +1673,7 @@ pub(crate) mod tests { reading_permutation.swap(i, j); } for idx in reading_permutation { - let address = memory_addresses[idx].value() + 1; + let address = memory_addresses[idx]; let value = memory_values[idx]; instructions .extend(triton_asm!(push {address} read_mem 1 pop 1 push {value} eq assert)); @@ -1682,7 +1701,7 @@ pub(crate) mod tests { reading_permutation.swap(i, j); } for idx in reading_permutation { - let address = memory_addresses[idx].value() + 1; + let address = memory_addresses[idx]; let value = memory_values[idx]; instructions .extend(triton_asm!(push {address} read_mem 1 pop 1 push {value} eq assert)); @@ -1765,6 +1784,35 @@ pub(crate) mod tests { } } + pub(crate) fn test_program_claim_in_ram_corresponds_to_currently_running_program( + ) -> ProgramAndInput { + let program = triton_program! { + dup 15 dup 15 dup 15 dup 15 dup 15 // _ [own_digest] + push 4 read_mem 5 pop 1 // _ [own_digest] [claim_digest] + assert_vector // _ [own_digest] + halt + }; + let claim = Claim { + program_digest: program.hash::(), + input: vec![], + output: vec![], + }; + + let initial_ram = claim + .encode() + .into_iter() + .enumerate() + .map(|(address, value)| (address as u64, value.value())) + .collect(); + let non_determinism = NonDeterminism::default().with_ram(initial_ram); + + ProgramAndInput { + program, + public_input: vec![], + non_determinism, + } + } + #[proptest] fn xxadd( #[strategy(arb())] left_operand: XFieldElement, @@ -1942,20 +1990,20 @@ pub(crate) mod tests { let program = triton_program!( push 8 push 5 write_mem 1 pop 1 // write 8 to address 5 push 18 push 15 write_mem 1 pop 1 // write 18 to address 15 - push 6 read_mem 1 pop 2 // read from address 5 - push 16 read_mem 1 pop 2 // read from address 15 + push 5 read_mem 1 pop 2 // read from address 5 + push 15 read_mem 1 pop 2 // read from address 15 push 7 push 5 write_mem 1 pop 1 // write 7 to address 5 - push 16 read_mem 1 // _ 18 15 - push 6 read_mem 1 // _ 18 15 7 5 + push 15 read_mem 1 // _ 18 14 + push 5 read_mem 1 // _ 18 14 7 4 halt ); let terminal_state = program .debug_terminal_state([].into(), [].into(), None, None) .unwrap(); - assert_eq!(BFieldElement::new(5), terminal_state.op_stack.peek_at(ST0)); + assert_eq!(BFieldElement::new(4), terminal_state.op_stack.peek_at(ST0)); assert_eq!(BFieldElement::new(7), terminal_state.op_stack.peek_at(ST1)); - assert_eq!(BFieldElement::new(15), terminal_state.op_stack.peek_at(ST2)); + assert_eq!(BFieldElement::new(14), terminal_state.op_stack.peek_at(ST2)); assert_eq!(BFieldElement::new(18), terminal_state.op_stack.peek_at(ST3)); } @@ -1973,20 +2021,21 @@ pub(crate) mod tests { swap 1 // _ 0 5 | 3 1 pop 1 // _ 0 5 | 3 write_mem 1 // _ 0 4 | - read_mem 1 // _ 0 5 | 3 - swap 2 // _ 3 5 | 0 - pop 1 // _ 3 5 | - swap 1 // _ 5 3 | - push 1 // _ 5 3 | 1 - add // _ 5 4 | - read_mem 1 // _ 5 5 | 3 + push -1 add // _ 0 3 | + read_mem 1 // _ 0 5 | 2 + swap 2 // _ 2 5 | 0 + pop 1 // _ 2 5 | + swap 1 // _ 5 2 | + push 1 // _ 5 2 | 1 + add // _ 5 3 | + read_mem 1 // _ 5 5 | 2 halt ); let terminal_state = program .debug_terminal_state([].into(), [].into(), None, None) .unwrap(); - assert_eq!(BFieldElement::new(3), terminal_state.op_stack.peek_at(ST0)); + assert_eq!(BFieldElement::new(2), terminal_state.op_stack.peek_at(ST0)); assert_eq!(BFieldElement::new(5), terminal_state.op_stack.peek_at(ST1)); assert_eq!(BFieldElement::new(5), terminal_state.op_stack.peek_at(ST2)); } @@ -2095,7 +2144,7 @@ pub(crate) mod tests { #[test] fn read_non_deterministically_initialized_ram_at_address_0() { - let program = triton_program!(push 1 read_mem 1 pop 1 write_io 1 halt); + let program = triton_program!(push 0 read_mem 1 pop 1 write_io 1 halt); let mut initial_ram = HashMap::new(); initial_ram.insert(0_u64.into(), 42_u64.into()); @@ -2118,7 +2167,7 @@ pub(crate) mod tests { ) { let program = triton_program!( read_mem 1 swap 1 write_io 1 - push {address.value() + 1} read_mem 1 pop 1 write_io 1 + push {address} read_mem 1 pop 1 write_io 1 halt );