Skip to content

Commit

Permalink
feat!: instruction divine_sibling pushes divined digest onto stack
Browse files Browse the repository at this point in the history
  • Loading branch information
@jan-ferdinand
jan-ferdinand committed Nov 2, 2023
1 parent b282415 commit 4602fad
Show file tree
Hide file tree
Showing 4 changed files with 87 additions and 71 deletions.
1 change: 0 additions & 1 deletion triton-vm/src/example_programs.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -157,7 +157,6 @@ fn merkle_tree_authentication_path_verify() -> Program {
// stack after: [* r4 r3 r2 r1 r0 1 d4 d3 d2 d1 d0]
traverse_tree:
dup 5 push 1 eq skiz return // break loop if node index is 1
push 0 push 0 push 0 push 0 push 0 // prepare for instruction `divine_sibling`
divine_sibling hash recurse // move up one level in the Merkle tree

// subroutine: compare digests
Expand Down
2 changes: 1 addition & 1 deletion triton-vm/src/instruction.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -338,7 +338,7 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
ReadMem => 1,
WriteMem => -1,
Hash => -5,
DivineSibling => 0,
DivineSibling => 5,
AssertVector => 0,
SpongeInit => 0,
SpongeAbsorb => 0,
Expand Down
103 changes: 66 additions & 37 deletions triton-vm/src/table/processor_table.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1703,10 +1703,10 @@ impl ExtProcessorTable {
.concat()
}

/// Recall that in a Merkle tree, the indices of left (respectively right)
/// leafs have 0 (respectively 1) as their least significant bit. The first
/// two polynomials achieve that helper variable hv0 holds the result of
/// st10 mod 2. The second polynomial sets the new value of st10 to st10 div 2.
/// Recall that in a Merkle tree, the indices of left (respectively right) leafs have 0
/// (respectively 1) as their least significant bit. The first two polynomials achieve that
/// helper variable hv0 holds the result of st5 mod 2. The second polynomial sets the new value
/// of st10 to st5 div 2.
fn instruction_divine_sibling(
circuit_builder: &ConstraintCircuitBuilder<DualRowIndicator>,
) -> Vec<ConstraintCircuitMonad<DualRowIndicator>> {
Expand All @@ -1719,44 +1719,49 @@ impl ExtProcessorTable {
circuit_builder.input(NextBaseRow(col.master_base_table_index()))
};

// Helper variable hv0 is either 0 or 1.
let hv0_is_0_or_1 = curr_base_row(HV0) * (curr_base_row(HV0) - one());

// The 11th stack register is shifted by 1 bit to the right.
let st10_is_shifted_1_bit_right =
next_base_row(ST10) * constant(2) + curr_base_row(HV0) - curr_base_row(ST10);

// The second pentuplet either stays where it is, or is moved to the top
let maybe_move_st5 = (one() - curr_base_row(HV0))
* (curr_base_row(ST5) - next_base_row(ST0))
+ curr_base_row(HV0) * (curr_base_row(ST5) - next_base_row(ST5));
let maybe_move_st6 = (one() - curr_base_row(HV0))
* (curr_base_row(ST6) - next_base_row(ST1))
+ curr_base_row(HV0) * (curr_base_row(ST6) - next_base_row(ST6));
let maybe_move_st7 = (one() - curr_base_row(HV0))
* (curr_base_row(ST7) - next_base_row(ST2))
+ curr_base_row(HV0) * (curr_base_row(ST7) - next_base_row(ST7));
let maybe_move_st8 = (one() - curr_base_row(HV0))
* (curr_base_row(ST8) - next_base_row(ST3))
+ curr_base_row(HV0) * (curr_base_row(ST8) - next_base_row(ST8));
let maybe_move_st9 = (one() - curr_base_row(HV0))
* (curr_base_row(ST9) - next_base_row(ST4))
+ curr_base_row(HV0) * (curr_base_row(ST9) - next_base_row(ST9));

let specific_constraints = vec![
let new_st10_is_previous_st5_div_2 =
next_base_row(ST10) * constant(2) + curr_base_row(HV0) - curr_base_row(ST5);

let maybe_move_st0 = (one() - curr_base_row(HV0))
* (next_base_row(ST0) - curr_base_row(ST0))
+ curr_base_row(HV0) * (next_base_row(ST5) - curr_base_row(ST0));
let maybe_move_st1 = (one() - curr_base_row(HV0))
* (next_base_row(ST1) - curr_base_row(ST1))
+ curr_base_row(HV0) * (next_base_row(ST6) - curr_base_row(ST1));
let maybe_move_st2 = (one() - curr_base_row(HV0))
* (next_base_row(ST2) - curr_base_row(ST2))
+ curr_base_row(HV0) * (next_base_row(ST7) - curr_base_row(ST2));
let maybe_move_st3 = (one() - curr_base_row(HV0))
* (next_base_row(ST3) - curr_base_row(ST3))
+ curr_base_row(HV0) * (next_base_row(ST8) - curr_base_row(ST3));
let maybe_move_st4 = (one() - curr_base_row(HV0))
* (next_base_row(ST4) - curr_base_row(ST4))
+ curr_base_row(HV0) * (next_base_row(ST9) - curr_base_row(ST4));

let maybe_shift_known_digest_down_the_stack = vec![
hv0_is_0_or_1,
st10_is_shifted_1_bit_right,
maybe_move_st5,
maybe_move_st6,
maybe_move_st7,
maybe_move_st8,
maybe_move_st9,
new_st10_is_previous_st5_div_2,
maybe_move_st0,
maybe_move_st1,
maybe_move_st2,
maybe_move_st3,
maybe_move_st4,
];

let op_stack_grows_by_5_and_top_11_elements_unconstrained = vec![
next_base_row(ST11) - curr_base_row(ST6),
next_base_row(ST12) - curr_base_row(ST7),
next_base_row(ST13) - curr_base_row(ST8),
next_base_row(ST14) - curr_base_row(ST9),
next_base_row(ST15) - curr_base_row(ST10),
next_base_row(OpStackPointer) - curr_base_row(OpStackPointer) - constant(5),
Self::running_product_op_stack_accounts_for_growing_stack_by(circuit_builder, 5),
];
[
specific_constraints,
Self::instruction_group_op_stack_remains_and_top_eleven_elements_unconstrained(
circuit_builder,
),
maybe_shift_known_digest_down_the_stack,
op_stack_grows_by_5_and_top_11_elements_unconstrained,
Self::instruction_group_step_1(circuit_builder),
Self::instruction_group_keep_ram(circuit_builder),
]
Expand Down Expand Up @@ -3238,6 +3243,7 @@ pub(crate) mod tests {
use rand::Rng;
use strum::IntoEnumIterator;
use test_strategy::proptest;
use twenty_first::shared_math::digest::Digest;

use crate::error::InstructionError;
use crate::error::InstructionError::DivisionByZero;
Expand All @@ -3250,6 +3256,7 @@ pub(crate) mod tests {
use crate::table::master_table::*;
use crate::triton_program;
use crate::vm::NUM_HELPER_VARIABLE_REGISTERS;
use crate::NonDeterminism;

use super::*;

Expand Down Expand Up @@ -3573,6 +3580,28 @@ pub(crate) mod tests {
);
}

#[test]
fn transition_constraints_for_instruction_divine_sibling() {
let programs = [
triton_program!(push 2 swap 5 divine_sibling halt),
triton_program!(push 3 swap 5 divine_sibling halt),
];
let dummy_digest = Digest::new([1, 2, 3, 4, 5].map(BFieldElement::new));
let non_determinism = NonDeterminism::new(vec![]).with_digests(vec![dummy_digest]);
let programs_with_input = programs.map(|program| ProgramAndInput {
program,
public_input: vec![],
non_determinism: non_determinism.clone(),
});
let test_rows = programs_with_input.map(|p_w_i| test_row_from_program_with_input(p_w_i, 2));
test_constraints_for_rows_with_debug_info(
DivineSibling,
&test_rows,
&[ST0, ST1, ST2, ST3, ST4, ST5],
&[ST0, ST1, ST2, ST3, ST4, ST5, ST6, ST7, ST8, ST9, ST10],
);
}

#[test]
fn transition_constraints_for_instruction_eq() {
let programs = [
Expand Down
52 changes: 20 additions & 32 deletions triton-vm/src/vm.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -159,7 +159,7 @@ impl<'pgm> VMState<'pgm> {
hvs[1..6].copy_from_slice(&decomposition);
}
DivineSibling => {
let node_index = self.op_stack.peek_at(ST10).value();
let node_index = self.op_stack.peek_at(ST5).value();
hvs[0] = BFieldElement::new(node_index % 2);
}
Split => {
Expand Down Expand Up @@ -486,7 +486,6 @@ impl<'pgm> VMState<'pgm> {
}

fn divine_sibling(&mut self) -> Result<Vec<CoProcessorCall>> {
let _st0_through_st4 = self.op_stack.pop_multiple::<{ DIGEST_LENGTH }>()?;
let (known_digest, _) = self.op_stack.pop_multiple()?;
let (node_index, _) = self.op_stack.pop_u32()?;

Expand All @@ -500,12 +499,15 @@ impl<'pgm> VMState<'pgm> {
for &digest_element in right_digest.iter().rev() {
let _ = self.op_stack.push(digest_element);
}
let mut all_underflow_io = vec![];
for &digest_element in left_digest.iter().rev() {
let _ = self.op_stack.push(digest_element);
let underflow_io = self.op_stack.push(digest_element);
all_underflow_io.push(underflow_io);
}
let op_stack_calls = self.underflow_io_sequence_to_co_processor_calls(all_underflow_io);

self.instruction_pointer += 1;
Ok(vec![])
Ok(op_stack_calls)
}

fn assert_vector(&mut self) -> Result<Vec<CoProcessorCall>> {
Expand Down Expand Up @@ -1155,24 +1157,17 @@ pub(crate) mod tests {
}
}

pub(crate) fn test_program_for_divine_sibling_noswitch() -> ProgramAndInput {
pub(crate) fn test_program_for_divine_sibling_no_switch() -> ProgramAndInput {
let program = triton_program!(
push 3
push 4 push 2 push 2 push 2 push 1
push 17 push 18 push 19 push 20 push 21
push 3
push 4 push 2 push 2 push 2 push 1
divine_sibling

push 0 eq assert
push 1 eq assert
push 2 eq assert
push 3 eq assert
push 4 eq assert
push 4 push 3 push 2 push 1 push 0
assert_vector pop 5 pop 5

push 1 eq assert
push 2 eq assert
push 2 eq assert
push 2 eq assert
push 4 eq assert
push 4 push 2 push 2 push 2 push 1
assert_vector pop 5 pop 5

assert halt
);
Expand All @@ -1189,22 +1184,15 @@ pub(crate) mod tests {

pub(crate) fn test_program_for_divine_sibling_switch() -> ProgramAndInput {
let program = triton_program!(
push 2
push 4 push 2 push 2 push 2 push 1
push 17 push 18 push 19 push 20 push 21
push 2
push 4 push 2 push 2 push 2 push 1
divine_sibling

push 1 eq assert
push 2 eq assert
push 2 eq assert
push 2 eq assert
push 4 eq assert
push 4 push 2 push 2 push 2 push 1
assert_vector pop 5 pop 5

push 0 eq assert
push 1 eq assert
push 2 eq assert
push 3 eq assert
push 4 eq assert
push 4 push 3 push 2 push 1 push 0
assert_vector pop 5 pop 5

assert halt
);
Expand Down Expand Up @@ -1823,7 +1811,7 @@ pub(crate) mod tests {
test_program_for_call_recurse_return(),
test_program_for_write_mem_read_mem(),
test_program_for_hash(),
test_program_for_divine_sibling_noswitch(),
test_program_for_divine_sibling_no_switch(),
test_program_for_divine_sibling_switch(),
test_program_for_assert_vector(),
test_program_for_sponge_instructions(),
Expand Down

0 comments on commit 4602fad

Please sign in to comment.