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

@@ -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** |
 <!-- auto-gen info stop -->
 
 ## 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** |
 <!-- auto-gen info stop -->

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 <br />
-    if `i` is 1, then `st0` is moved into `st1` and <br />
-    if `i` is 2, then `st0` is moved into `st2` and <br />
-    if `i` is 3, then `st0` is moved into `st3` and <br />
-    if `i` is 4, then `st0` is moved into `st4` and <br />
-    if `i` is 5, then `st0` is moved into `st5` and <br />
-    if `i` is 6, then `st0` is moved into `st6` and <br />
-    if `i` is 7, then `st0` is moved into `st7` and <br />
-    if `i` is 8, then `st0` is moved into `st8` and <br />
-    if `i` is 9, then `st0` is moved into `st9` and <br />
-    if `i` is 10, then `st0` is moved into `st10` and <br />
-    if `i` is 11, then `st0` is moved into `st11` and <br />
-    if `i` is 12, then `st0` is moved into `st12` and <br />
-    if `i` is 13, then `st0` is moved into `st13` and <br />
-    if `i` is 14, then `st0` is moved into `st14` and <br />
-    if `i` is 15, then `st0` is moved into `st15`.
-1. If `i` is 1, then `st1` is moved into `st0` and <br />
-    if `i` is 2, then `st2` is moved into `st0` and <br />
-    if `i` is 3, then `st3` is moved into `st0` and <br />
-    if `i` is 4, then `st4` is moved into `st0` and <br />
-    if `i` is 5, then `st5` is moved into `st0` and <br />
-    if `i` is 6, then `st6` is moved into `st0` and <br />
-    if `i` is 7, then `st7` is moved into `st0` and <br />
-    if `i` is 8, then `st8` is moved into `st0` and <br />
-    if `i` is 9, then `st9` is moved into `st0` and <br />
-    if `i` is 10, then `st10` is moved into `st0` and <br />
-    if `i` is 11, then `st11` is moved into `st0` and <br />
-    if `i` is 12, then `st12` is moved into `st0` and <br />
-    if `i` is 13, then `st13` is moved into `st0` and <br />
-    if `i` is 14, then `st14` is moved into `st0` and <br />
-    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)`<br />
-    `+ ind_1(hv3, hv2, hv1, hv0)·(st1' - st0)`<br />
-    `+ ind_2(hv3, hv2, hv1, hv0)·(st2' - st0)`<br />
-    `+ ind_3(hv3, hv2, hv1, hv0)·(st3' - st0)`<br />
-    `+ ind_4(hv3, hv2, hv1, hv0)·(st4' - st0)`<br />
-    `+ ind_5(hv3, hv2, hv1, hv0)·(st5' - st0)`<br />
-    `+ ind_6(hv3, hv2, hv1, hv0)·(st6' - st0)`<br />
-    `+ ind_7(hv3, hv2, hv1, hv0)·(st7' - st0)`<br />
-    `+ ind_8(hv3, hv2, hv1, hv0)·(st8' - st0)`<br />
-    `+ ind_9(hv3, hv2, hv1, hv0)·(st9' - st0)`<br />
-    `+ ind_10(hv3, hv2, hv1, hv0)·(st10' - st0)`<br />
-    `+ ind_11(hv3, hv2, hv1, hv0)·(st11' - st0)`<br />
-    `+ ind_12(hv3, hv2, hv1, hv0)·(st12' - st0)`<br />
-    `+ ind_13(hv3, hv2, hv1, hv0)·(st13' - st0)`<br />
-    `+ ind_14(hv3, hv2, hv1, hv0)·(st14' - st0)`<br />
-    `+ ind_15(hv3, hv2, hv1, hv0)·(st15' - st0)`
-1. `ind_1(hv3, hv2, hv1, hv0)·(st0' - st1)`<br />
-    `+ ind_2(hv3, hv2, hv1, hv0)·(st0' - st2)`<br />
-    `+ ind_3(hv3, hv2, hv1, hv0)·(st0' - st3)`<br />
-    `+ ind_4(hv3, hv2, hv1, hv0)·(st0' - st4)`<br />
-    `+ ind_5(hv3, hv2, hv1, hv0)·(st0' - st5)`<br />
-    `+ ind_6(hv3, hv2, hv1, hv0)·(st0' - st6)`<br />
-    `+ ind_7(hv3, hv2, hv1, hv0)·(st0' - st7)`<br />
-    `+ ind_8(hv3, hv2, hv1, hv0)·(st0' - st8)`<br />
-    `+ ind_9(hv3, hv2, hv1, hv0)·(st0' - st9)`<br />
-    `+ ind_10(hv3, hv2, hv1, hv0)·(st0' - st10)`<br />
-    `+ ind_11(hv3, hv2, hv1, hv0)·(st0' - st11)`<br />
-    `+ ind_12(hv3, hv2, hv1, hv0)·(st0' - st12)`<br />
-    `+ ind_13(hv3, hv2, hv1, hv0)·(st0' - st13)`<br />
-    `+ ind_14(hv3, hv2, hv1, hv0)·(st0' - st14)`<br />
-    `+ 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`
 

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.

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],

triton-vm/src/instruction.rs

@@ -442,10 +442,6 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
             Split | Lt | And | Xor | Log2Floor | Pow | DivMod | PopCount
         )
     }
-
-    pub fn has_illegal_argument(&self) -> bool {
-        matches!(self, Swap(ST0))
-    }
 }
 
 impl<Dest: Display + PartialEq + Default> Display for AnInstruction<Dest> {
@@ -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::<InstructionLabel>()?);
         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]);

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::<String>::Swap(argument);
         $crate::instruction::LabelledInstruction::Instruction(instruction)

triton-vm/src/parser.rs

@@ -366,15 +366,9 @@ fn dup_instruction() -> impl Fn(&str) -> ParseResult<AnInstruction<String>> {
 
 fn swap_instruction() -> impl Fn(&str) -> ParseResult<AnInstruction<String>> {
     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",

triton-vm/src/table/processor_table.rs

@@ -1444,35 +1444,36 @@ impl ExtProcessorTable {
     fn instruction_swap(
         circuit_builder: &ConstraintCircuitBuilder<DualRowIndicator>,
     ) -> Vec<ConstraintCircuitMonad<DualRowIndicator>> {
-        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()))
         };
         let next_row = |col: ProcessorBaseTableColumn| {
             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],