From 62187169ad1fd55221eef7a752f7ee81c87d1d34 Mon Sep 17 00:00:00 2001 From: Jan Ferdinand Sauer Date: Sun, 2 Jun 2024 10:54:41 +0200 Subject: [PATCH] perf!: Simplify constraints of instruction `swap` BREAKING CHANGE: Instruction `swap` can now take immediate argument 0. This is almost entirely equivalent to instruction `nop`, with the exception of the resulting program's size: `nop` is an instruction of size 1. --- specification/src/arithmetization-overview.md | 8 +- ...ruction-specific-transition-constraints.md | 103 +----------------- specification/src/instructions.md | 2 +- triton-vm/src/error.rs | 17 --- triton-vm/src/instruction.rs | 27 +---- triton-vm/src/lib.rs | 1 - triton-vm/src/parser.rs | 16 +-- triton-vm/src/table/processor_table.rs | 61 ++++------- triton-vm/src/vm.rs | 19 ++-- 9 files changed, 48 insertions(+), 206 deletions(-) diff --git a/specification/src/arithmetization-overview.md b/specification/src/arithmetization-overview.md index c1f8470bc..9cb971b6a 100644 --- a/specification/src/arithmetization-overview.md +++ b/specification/src/arithmetization-overview.md @@ -15,9 +15,9 @@ | [CascadeTable](cascade-table.md) | 6 | 2 | 12 | | [LookupTable](lookup-table.md) | 4 | 2 | 10 | | [U32Table](u32-table.md) | 10 | 1 | 13 | -| DegreeLowering | 216 | 36 | 324 | +| DegreeLowering | 212 | 36 | 320 | | Randomizers | 0 | 1 | 3 | -| **TOTAL** | **365** | **86** | **623** | +| **TOTAL** | **361** | **86** | **619** | ## Constraints @@ -50,7 +50,7 @@ After automatically lowering degree to 4: | table name | #initial | #consistency | #transition | #terminal | |:-----------------------------------------------|---------:|-------------:|------------:|----------:| | [ProgramTable](program-table.md) | 6 | 4 | 10 | 2 | -| [ProcessorTable](processor-table.md) | 31 | 10 | 231 | 1 | +| [ProcessorTable](processor-table.md) | 31 | 10 | 227 | 1 | | [OpStackTable](operational-stack-table.md) | 3 | 0 | 5 | 0 | | [RamTable](random-access-memory-table.md) | 7 | 0 | 13 | 1 | | [JumpStackTable](jump-stack-table.md) | 6 | 0 | 6 | 0 | @@ -59,5 +59,5 @@ After automatically lowering degree to 4: | [LookupTable](lookup-table.md) | 3 | 1 | 4 | 1 | | [U32Table](u32-table.md) | 1 | 26 | 34 | 2 | | [Grand Cross-Table Argument](table-linking.md) | 0 | 0 | 0 | 14 | -| **TOTAL** | **81** | **94** | **390** | **23** | +| **TOTAL** | **81** | **94** | **386** | **23** | diff --git a/specification/src/instruction-specific-transition-constraints.md b/specification/src/instruction-specific-transition-constraints.md index f9fbb1afe..94d773209 100644 --- a/specification/src/instruction-specific-transition-constraints.md +++ b/specification/src/instruction-specific-transition-constraints.md @@ -70,105 +70,10 @@ In addition to its [instruction groups](instruction-groups.md), this instruction ### Description -1. Argument `i` is not 0 and
- if `i` is 1, then `st0` is moved into `st1` and
- if `i` is 2, then `st0` is moved into `st2` and
- if `i` is 3, then `st0` is moved into `st3` and
- if `i` is 4, then `st0` is moved into `st4` and
- if `i` is 5, then `st0` is moved into `st5` and
- if `i` is 6, then `st0` is moved into `st6` and
- if `i` is 7, then `st0` is moved into `st7` and
- if `i` is 8, then `st0` is moved into `st8` and
- if `i` is 9, then `st0` is moved into `st9` and
- if `i` is 10, then `st0` is moved into `st10` and
- if `i` is 11, then `st0` is moved into `st11` and
- if `i` is 12, then `st0` is moved into `st12` and
- if `i` is 13, then `st0` is moved into `st13` and
- if `i` is 14, then `st0` is moved into `st14` and
- if `i` is 15, then `st0` is moved into `st15`. -1. If `i` is 1, then `st1` is moved into `st0` and
- if `i` is 2, then `st2` is moved into `st0` and
- if `i` is 3, then `st3` is moved into `st0` and
- if `i` is 4, then `st4` is moved into `st0` and
- if `i` is 5, then `st5` is moved into `st0` and
- if `i` is 6, then `st6` is moved into `st0` and
- if `i` is 7, then `st7` is moved into `st0` and
- if `i` is 8, then `st8` is moved into `st0` and
- if `i` is 9, then `st9` is moved into `st0` and
- if `i` is 10, then `st10` is moved into `st0` and
- if `i` is 11, then `st11` is moved into `st0` and
- if `i` is 12, then `st12` is moved into `st0` and
- if `i` is 13, then `st13` is moved into `st0` and
- if `i` is 14, then `st14` is moved into `st0` and
- if `i` is 15, then `st15` is moved into `st0`. -1. If `i` is not 1, then `st1` does not change. -1. If `i` is not 2, then `st2` does not change. -1. If `i` is not 3, then `st3` does not change. -1. If `i` is not 4, then `st4` does not change. -1. If `i` is not 5, then `st5` does not change. -1. If `i` is not 6, then `st6` does not change. -1. If `i` is not 7, then `st7` does not change. -1. If `i` is not 8, then `st8` does not change. -1. If `i` is not 9, then `st9` does not change. -1. If `i` is not 10, then `st10` does not change. -1. If `i` is not 11, then `st11` does not change. -1. If `i` is not 12, then `st12` does not change. -1. If `i` is not 13, then `st13` does not change. -1. If `i` is not 14, then `st14` does not change. -1. If `i` is not 15, then `st15` does not change. -1. The op stack pointer does not change. -1. The running product for the Op Stack Table remains unchanged. - -### Polynomials - -1. `ind_0(hv3, hv2, hv1, hv0)`
- `+ ind_1(hv3, hv2, hv1, hv0)·(st1' - st0)`
- `+ ind_2(hv3, hv2, hv1, hv0)·(st2' - st0)`
- `+ ind_3(hv3, hv2, hv1, hv0)·(st3' - st0)`
- `+ ind_4(hv3, hv2, hv1, hv0)·(st4' - st0)`
- `+ ind_5(hv3, hv2, hv1, hv0)·(st5' - st0)`
- `+ ind_6(hv3, hv2, hv1, hv0)·(st6' - st0)`
- `+ ind_7(hv3, hv2, hv1, hv0)·(st7' - st0)`
- `+ ind_8(hv3, hv2, hv1, hv0)·(st8' - st0)`
- `+ ind_9(hv3, hv2, hv1, hv0)·(st9' - st0)`
- `+ ind_10(hv3, hv2, hv1, hv0)·(st10' - st0)`
- `+ ind_11(hv3, hv2, hv1, hv0)·(st11' - st0)`
- `+ ind_12(hv3, hv2, hv1, hv0)·(st12' - st0)`
- `+ ind_13(hv3, hv2, hv1, hv0)·(st13' - st0)`
- `+ ind_14(hv3, hv2, hv1, hv0)·(st14' - st0)`
- `+ ind_15(hv3, hv2, hv1, hv0)·(st15' - st0)` -1. `ind_1(hv3, hv2, hv1, hv0)·(st0' - st1)`
- `+ ind_2(hv3, hv2, hv1, hv0)·(st0' - st2)`
- `+ ind_3(hv3, hv2, hv1, hv0)·(st0' - st3)`
- `+ ind_4(hv3, hv2, hv1, hv0)·(st0' - st4)`
- `+ ind_5(hv3, hv2, hv1, hv0)·(st0' - st5)`
- `+ ind_6(hv3, hv2, hv1, hv0)·(st0' - st6)`
- `+ ind_7(hv3, hv2, hv1, hv0)·(st0' - st7)`
- `+ ind_8(hv3, hv2, hv1, hv0)·(st0' - st8)`
- `+ ind_9(hv3, hv2, hv1, hv0)·(st0' - st9)`
- `+ ind_10(hv3, hv2, hv1, hv0)·(st0' - st10)`
- `+ ind_11(hv3, hv2, hv1, hv0)·(st0' - st11)`
- `+ ind_12(hv3, hv2, hv1, hv0)·(st0' - st12)`
- `+ ind_13(hv3, hv2, hv1, hv0)·(st0' - st13)`
- `+ ind_14(hv3, hv2, hv1, hv0)·(st0' - st14)`
- `+ ind_15(hv3, hv2, hv1, hv0)·(st0' - st15)` -1. `(1 - ind_1(hv3, hv2, hv1, hv0))·(st1' - st1)` -1. `(1 - ind_2(hv3, hv2, hv1, hv0))·(st2' - st2)` -1. `(1 - ind_3(hv3, hv2, hv1, hv0))·(st3' - st3)` -1. `(1 - ind_4(hv3, hv2, hv1, hv0))·(st4' - st4)` -1. `(1 - ind_5(hv3, hv2, hv1, hv0))·(st5' - st5)` -1. `(1 - ind_6(hv3, hv2, hv1, hv0))·(st6' - st6)` -1. `(1 - ind_7(hv3, hv2, hv1, hv0))·(st7' - st7)` -1. `(1 - ind_8(hv3, hv2, hv1, hv0))·(st8' - st8)` -1. `(1 - ind_9(hv3, hv2, hv1, hv0))·(st9' - st9)` -1. `(1 - ind_10(hv3, hv2, hv1, hv0))·(st10' - st10)` -1. `(1 - ind_11(hv3, hv2, hv1, hv0))·(st11' - st11)` -1. `(1 - ind_12(hv3, hv2, hv1, hv0))·(st12' - st12)` -1. `(1 - ind_13(hv3, hv2, hv1, hv0))·(st13' - st13)` -1. `(1 - ind_14(hv3, hv2, hv1, hv0))·(st14' - st14)` -1. `(1 - ind_15(hv3, hv2, hv1, hv0))·(st15' - st15)` -1. `op_stack_pointer' - op_stack_pointer` -1. `RunningProductOpStackTable' - RunningProductOpStackTable` +For 0 ⩽ `i` < 16: +1. Stack element `i` is moved to the top. +1. The top stack element is moved to position `i` +1. For `j` ≠ `i`: stack element `j` remains unchanged. ## Instruction `nop` diff --git a/specification/src/instructions.md b/specification/src/instructions.md index 566a3b582..a4e799246 100644 --- a/specification/src/instructions.md +++ b/specification/src/instructions.md @@ -26,7 +26,7 @@ The third property allows efficient arithmetization of the running product for t | `push` + `a` | 1 | `_` | `_ a` | Pushes `a` onto the stack. | | `divine` + `n` | 9 | e.g., `_` | e.g., `_ b a` | Pushes `n` non-deterministic elements `a` to the stack. Interface for secret input. 1 ⩽ `n` ⩽ 5 | | `dup` + `i` | 17 | e.g., `_ e d c b a` | e.g., `_ e d c b a d` | Duplicates the element `i` positions away from the top. 0 ⩽ `i` < 16 | -| `swap` + `i` | 25 | e.g., `_ e d c b a` | e.g., `_ e a c b d` | Swaps the `i`th stack element with the top of the stack. 0 < `i` < 16 | +| `swap` + `i` | 25 | e.g., `_ e d c b a` | e.g., `_ e a c b d` | Swaps the `i`th stack element with the top of the stack. 0 ⩽ `i` < 16 | Instruction `divine n` (together with [`merkle_step`](#many-in-one)) make Triton a virtual machine that can execute non-deterministic programs. As programs go, this concept is somewhat unusual and benefits from additional explanation. diff --git a/triton-vm/src/error.rs b/triton-vm/src/error.rs index 815fdcf58..b625b76ad 100644 --- a/triton-vm/src/error.rs +++ b/triton-vm/src/error.rs @@ -66,9 +66,6 @@ pub enum InstructionError { #[error("vector assertion failed: stack[{0}] != stack[{}]", .0 + tip5::DIGEST_LENGTH)] VectorAssertionFailed(usize), - #[error("cannot swap stack element 0 with itself")] - SwapST0, - #[error("0 does not have a multiplicative inverse")] InverseOfZero, @@ -313,11 +310,7 @@ mod tests { use proptest_arbitrary_interop::arb; use test_strategy::proptest; - use crate::instruction::AnInstruction::*; - use crate::instruction::LabelledInstruction; - use crate::op_stack::OpStackElement::ST0; use crate::triton_program; - use crate::Program; use super::*; @@ -368,16 +361,6 @@ mod tests { assert!(1 == index); } - #[test] - fn swap_st0() { - // The parser rejects this program. Therefore, construct it manually. - let swap_0 = LabelledInstruction::Instruction(Swap(ST0)); - let halt = LabelledInstruction::Instruction(Halt); - let program = Program::new(&[swap_0, halt]); - let_assert!(Err(err) = program.run([].into(), [].into())); - let_assert!(InstructionError::SwapST0 = err.source); - } - #[proptest] fn assert_unequal_vec( #[strategy(arb())] test_vector: [BFieldElement; tip5::DIGEST_LENGTH], diff --git a/triton-vm/src/instruction.rs b/triton-vm/src/instruction.rs index 326814093..d6a410419 100644 --- a/triton-vm/src/instruction.rs +++ b/triton-vm/src/instruction.rs @@ -442,10 +442,6 @@ impl AnInstruction { Split | Lt | And | Xor | Log2Floor | Pow | DivMod | PopCount ) } - - pub fn has_illegal_argument(&self) -> bool { - matches!(self, Swap(ST0)) - } } impl Display for AnInstruction { @@ -497,10 +493,6 @@ impl Instruction { _ => return Err(illegal_argument_error), }; - if new_instruction.has_illegal_argument() { - return Err(illegal_argument_error); - } - Ok(new_instruction) } } @@ -665,10 +657,6 @@ impl<'a> Arbitrary<'a> for LabelledInstruction { let legal_label = String::from(u.arbitrary::()?); let instruction = instruction.map_call_address(|_| legal_label.clone()); - if let Swap(ST0) = instruction { - return Ok(Self::Instruction(Swap(ST1))); - } - Ok(Self::Instruction(instruction)) } } @@ -796,18 +784,9 @@ mod tests { } impl Instruction { - #[must_use] - fn replace_default_argument_if_illegal(self) -> Self { - match self { - Swap(ST0) => Swap(ST1), - _ => self, - } - } - fn flag_set(self) -> u32 { - let instruction = self.replace_default_argument_if_illegal(); InstructionBucket::iter() - .map(|bucket| u32::from(bucket.contains(instruction))) + .map(|bucket| u32::from(bucket.contains(self))) .enumerate() .map(|(bucket_index, contains_self)| contains_self << bucket_index) .fold(0, |acc, bit_flag| acc | bit_flag) @@ -922,7 +901,7 @@ mod tests { assert!(Push(bfe!(0)).change_arg(bfe!(7)).is_ok()); assert!(Dup(ST0).change_arg(bfe!(1024)).is_err()); assert!(Swap(ST0).change_arg(bfe!(1337)).is_err()); - assert!(Swap(ST0).change_arg(bfe!(0)).is_err()); + assert!(Swap(ST0).change_arg(bfe!(0)).is_ok()); assert!(Swap(ST0).change_arg(bfe!(1)).is_ok()); assert!(Pop(N4).change_arg(bfe!(0)).is_err()); assert!(Pop(N1).change_arg(bfe!(2)).is_ok()); @@ -962,7 +941,6 @@ mod tests { fn opcodes_are_consistent_with_shrink_stack_indication_bit() { let shrink_stack_indicator_bit_mask = 2; for instruction in Instruction::iter() { - let instruction = instruction.replace_default_argument_if_illegal(); let opcode = instruction.opcode(); println!("Testing instruction {instruction} with opcode {opcode}."); let shrinks_stack = instruction.op_stack_size_influence() < 0; @@ -1007,7 +985,6 @@ mod tests { #[test] fn instructions_act_on_op_stack_as_indicated() { for test_instruction in all_instructions_without_args() { - let test_instruction = test_instruction.replace_default_argument_if_illegal(); let (program, stack_size_before_test_instruction) = construct_test_program_for_instruction(test_instruction); let public_input = PublicInput::from(bfe_array![0]); diff --git a/triton-vm/src/lib.rs b/triton-vm/src/lib.rs index 69b966025..2ff69019e 100644 --- a/triton-vm/src/lib.rs +++ b/triton-vm/src/lib.rs @@ -454,7 +454,6 @@ macro_rules! triton_instr { $crate::instruction::LabelledInstruction::Instruction(instruction) }}; (swap $arg:literal) => {{ - assert_ne!(0_u32, $arg, "`swap 0` is illegal."); let argument = $crate::op_stack::OpStackElement::try_from($arg).unwrap(); let instruction = $crate::instruction::AnInstruction::::Swap(argument); $crate::instruction::LabelledInstruction::Instruction(instruction) diff --git a/triton-vm/src/parser.rs b/triton-vm/src/parser.rs index b92f9c2ae..fb1d6365a 100644 --- a/triton-vm/src/parser.rs +++ b/triton-vm/src/parser.rs @@ -366,15 +366,9 @@ fn dup_instruction() -> impl Fn(&str) -> ParseResult> { fn swap_instruction() -> impl Fn(&str) -> ParseResult> { move |s: &str| { - let (s, _) = token1("swap")(s)?; // require space before argument + let (s, _) = token1("swap")(s)?; let (s, stack_register) = stack_register(s)?; - - let instruction = Swap(stack_register); - if instruction.has_illegal_argument() { - return cut(context("instruction `swap` cannot take argument `0`", fail))(s); - } - - Ok((s, instruction)) + Ok((s, Swap(stack_register))) } } @@ -971,12 +965,6 @@ pub(crate) mod tests { expected_error_count: 1, message: "instruction `pop` cannot take argument `0`", }); - parse_program_neg_prop(NegativeTestCase { - input: "swap 0", - expected_error: "instruction `swap` cannot take argument `0`", - expected_error_count: 1, - message: "instruction `swap` cannot take argument `0`", - }); parse_program_neg_prop(NegativeTestCase { input: "swap 16", diff --git a/triton-vm/src/table/processor_table.rs b/triton-vm/src/table/processor_table.rs index 791e92574..4fdf38878 100644 --- a/triton-vm/src/table/processor_table.rs +++ b/triton-vm/src/table/processor_table.rs @@ -1444,8 +1444,6 @@ impl ExtProcessorTable { fn instruction_swap( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { - let one = || circuit_builder.b_constant(1); - let indicator_poly = |idx| Self::indicator_polynomial(circuit_builder, idx); let curr_row = |col: ProcessorBaseTableColumn| { circuit_builder.input(CurrentBaseRow(col.master_base_table_index())) }; @@ -1453,26 +1451,29 @@ impl ExtProcessorTable { circuit_builder.input(NextBaseRow(col.master_base_table_index())) }; - let st_column = ProcessorTable::op_stack_column_by_index; - let top_moves_to_i = |i| indicator_poly(i) * (next_row(st_column(i)) - curr_row(ST0)); - let i_moves_to_top = |i| indicator_poly(i) * (next_row(ST0) - curr_row(st_column(i))); - - let top_moves_to_indicated_element = (1..OpStackElement::COUNT).map(top_moves_to_i).sum(); - let indicated_element_moves_to_top = (1..OpStackElement::COUNT).map(i_moves_to_top).sum(); - let indicated_element_is_swapped = vec![ - indicator_poly(0) + top_moves_to_indicated_element, - indicated_element_moves_to_top, - ]; - - let i_does_not_change = - |i| (one() - indicator_poly(i)) * (next_row(st_column(i)) - curr_row(st_column(i))); - let other_elements_do_not_change = (1..OpStackElement::COUNT) - .map(i_does_not_change) + let stack = (0..OpStackElement::COUNT) + .map(ProcessorTable::op_stack_column_by_index) .collect_vec(); + let stack_with_swapped_i = |i| { + let mut stack = stack.clone(); + stack.swap(0, i); + stack.into_iter() + }; + + let next_stack = stack.iter().map(|&st| next_row(st)).collect_vec(); + let curr_stack_with_swapped_i = |i| stack_with_swapped_i(i).map(curr_row).collect_vec(); + + let next_stack_is_current_stack_with_swapped_i = |i| { + Self::indicator_polynomial(circuit_builder, i) + * (Self::compress_stack(circuit_builder, next_stack.clone()) + - Self::compress_stack(circuit_builder, curr_stack_with_swapped_i(i))) + }; + let next_stack_is_current_stack_with_correct_element_swapped = (0..OpStackElement::COUNT) + .map(next_stack_is_current_stack_with_swapped_i) + .sum(); [ - indicated_element_is_swapped, - other_elements_do_not_change, + vec![next_stack_is_current_stack_with_correct_element_swapped], Self::instruction_group_decompose_arg(circuit_builder), Self::instruction_group_step_2(circuit_builder), Self::instruction_group_no_ram(circuit_builder), @@ -3863,24 +3864,10 @@ pub(crate) mod tests { #[test] fn transition_constraints_for_instruction_swap() { - let programs = [ - triton_program!(swap 1 halt), - triton_program!(swap 2 halt), - triton_program!(swap 3 halt), - triton_program!(swap 4 halt), - triton_program!(swap 5 halt), - triton_program!(swap 6 halt), - triton_program!(swap 7 halt), - triton_program!(swap 8 halt), - triton_program!(swap 9 halt), - triton_program!(swap 10 halt), - triton_program!(swap 11 halt), - triton_program!(swap 12 halt), - triton_program!(swap 13 halt), - triton_program!(swap 14 halt), - triton_program!(swap 15 halt), - ]; - let test_rows = programs.map(|program| test_row_from_program(program, 0)); + let test_rows = (0..OpStackElement::COUNT) + .map(|i| triton_program!(swap {i} halt)) + .map(|program| test_row_from_program(program, 0)) + .collect_vec(); let debug_info = TestRowsDebugInfo { instruction: Swap(OpStackElement::ST0), debug_cols_curr_row: vec![ST0, ST1, ST2], diff --git a/triton-vm/src/vm.rs b/triton-vm/src/vm.rs index 8774f21a1..a53bbe60c 100644 --- a/triton-vm/src/vm.rs +++ b/triton-vm/src/vm.rs @@ -228,7 +228,7 @@ impl VMState { Push(field_element) => self.push(field_element), Divine(n) => self.divine(n)?, Dup(stack_element) => self.dup(stack_element), - Swap(stack_element) => self.swap(stack_element)?, + Swap(stack_element) => self.swap(stack_element), Halt => self.halt(), Nop => self.nop(), Skiz => self.skiz()?, @@ -345,14 +345,10 @@ impl VMState { vec![] } - fn swap(&mut self, stack_register: OpStackElement) -> Result> { - if stack_register == ST0 { - return Err(SwapST0); - } - (self.op_stack[ST0], self.op_stack[stack_register]) = - (self.op_stack[stack_register], self.op_stack[ST0]); + fn swap(&mut self, st: OpStackElement) -> Vec { + (self.op_stack[ST0], self.op_stack[st]) = (self.op_stack[st], self.op_stack[ST0]); self.instruction_pointer += 2; - Ok(vec![]) + vec![] } fn nop(&mut self) -> Vec { @@ -2403,6 +2399,13 @@ pub(crate) mod tests { assert!(bfe!(2) == standard_out[0]); } + #[test] + fn swap_st0_is_like_no_op() { + let program = triton_program!(push 42 swap 0 write_io 1 halt); + let_assert!(Ok(standard_out) = program.run([].into(), [].into())); + assert!(bfe!(42) == standard_out[0]); + } + #[test] fn read_mem_uninitialized() { let program = triton_program!(read_mem 3 halt);