Skip to content

Commit

Permalink
chore: read_mem starts reading at current address
Browse files Browse the repository at this point in the history 
Instead of `push a read_mem 1` reading from address `a-1`, it reads
from address `a`.
  • Loading branch information
@jan-ferdinand
jan-ferdinand committed Nov 15, 2023
2 parents 0cc7dfa + cf79d10 commit 7faad18
Show file tree
Hide file tree
Showing 7 changed files with 202 additions and 135 deletions.
2 changes: 1 addition & 1 deletion triton-vm/src/aet.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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();
}
}
Expand Down
101 changes: 51 additions & 50 deletions triton-vm/src/example_programs.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down Expand Up @@ -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
Expand All @@ -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

Expand Down Expand Up @@ -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
Expand All @@ -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:
Expand All @@ -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:
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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]
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down
8 changes: 4 additions & 4 deletions triton-vm/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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₅²
Expand Down Expand Up @@ -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
);
Expand Down
15 changes: 11 additions & 4 deletions triton-vm/src/stark.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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, _, _) =
Expand Down Expand Up @@ -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);
Expand Down
43 changes: 31 additions & 12 deletions triton-vm/src/table/processor_table.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -404,34 +404,30 @@ 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 {
let num_ram_pointers = 1;
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]
Expand All @@ -443,6 +439,23 @@ impl ProcessorTable {
Some(factor)
}

fn offset_ram_pointer(
instruction: Instruction,
row_with_longer_stack: ArrayView1<BFieldElement>,
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<BFieldElement>) -> Option<Instruction> {
let opcode = row[CI.base_table_index()];
let instruction: Instruction = opcode.try_into().ok()?;
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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,
Expand Down
Loading

0 comments on commit 7faad18

Please sign in to comment.