diff --git a/specification/src/arithmetization-overview.md b/specification/src/arithmetization-overview.md index ac3f8c01..6a365a3a 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 (-/8/4) | 0/113/226 | 0/14/38 | 0/155/340 | +| DegreeLowering (-/8/4) | 0/118/230 | 0/14/38 | 0/160/344 | | Randomizers | 0 | 1 | 3 | -| **TOTAL** | **149/262/375** | **50/64/88** | **299/454/639** | +| **TOTAL** | **149/267/379** | **50/64/88** | **299/459/643** | ## Constraints @@ -44,14 +44,14 @@ Before automatic degree lowering: | [U32Table](u32-table.md) | 1 | 15 | 22 | 2 | 12 | | [Grand Cross-Table Argument](table-linking.md) | 0 | 0 | 0 | 14 | 1 | | **TOTAL** | **79** | **76** | **150** | **23** | **19** | -| (# nodes) | (534) | (624) | (6176) | (213) | | +| (# nodes) | (534) | (624) | (6679) | (213) | | After lowering degree to 8: | table name | #initial | #consistency | #transition | #terminal | |:-----------------------------------------------|---------:|-------------:|------------:|----------:| | [ProgramTable](program-table.md) | 6 | 4 | 10 | 2 | -| [ProcessorTable](processor-table.md) | 29 | 10 | 160 | 1 | +| [ProcessorTable](processor-table.md) | 29 | 10 | 165 | 1 | | [OpStackTable](operational-stack-table.md) | 3 | 0 | 5 | 0 | | [RamTable](random-access-memory-table.md) | 7 | 0 | 12 | 1 | | [JumpStackTable](jump-stack-table.md) | 6 | 0 | 6 | 0 | @@ -60,15 +60,15 @@ After lowering degree to 8: | [LookupTable](lookup-table.md) | 3 | 1 | 4 | 1 | | [U32Table](u32-table.md) | 1 | 18 | 24 | 2 | | [Grand Cross-Table Argument](table-linking.md) | 0 | 0 | 0 | 14 | -| **TOTAL** | **79** | **80** | **273** | **23** | -| (# nodes) | (534) | (635) | (6438) | (213) | +| **TOTAL** | **79** | **80** | **278** | **23** | +| (# nodes) | (534) | (635) | (6956) | (213) | After lowering degree to 4: | table name | #initial | #consistency | #transition | #terminal | |:-----------------------------------------------|---------:|-------------:|------------:|----------:| | [ProgramTable](program-table.md) | 6 | 4 | 10 | 2 | -| [ProcessorTable](processor-table.md) | 31 | 10 | 234 | 1 | +| [ProcessorTable](processor-table.md) | 31 | 10 | 238 | 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 | 7 | 0 | @@ -77,8 +77,8 @@ After 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** | **394** | **23** | -| (# nodes) | (538) | (676) | (6731) | (213) | +| **TOTAL** | **81** | **94** | **398** | **23** | +| (# nodes) | (538) | (676) | (7246) | (213) | @@ -90,8 +90,8 @@ In order to gauge the runtime cost for this step, the following table provides e | Type | Processor | Op Stack | RAM | |:-------------|----------:|---------:|------:| -| static | 35381 | 65645 | 23226 | -| dynamic | 46805 | 73265 | 27034 | +| static | 37759 | 70227 | 24996 | +| dynamic | 49456 | 78029 | 28895 | ## Opcode Pressure @@ -104,7 +104,7 @@ The table below helps answer this question at a glance. | IsU32 | ShrinksStack | HasArg | Num Opcodes | |-------------:|-------------:|-------------:|-------------:| | n | n | n | 12 | -| n | n | y | 8 | +| n | n | y | 10 | | n | y | n | 11 | | n | y | y | 3 | | y | n | n | 6 | diff --git a/specification/src/instruction-groups.md b/specification/src/instruction-groups.md index f7ae7bde..8a462615 100644 --- a/specification/src/instruction-groups.md +++ b/specification/src/instruction-groups.md @@ -40,6 +40,8 @@ A summary of all instructions and which groups they are part of is given in the | `pop` + `n` | x | x | x | x | | | x | | | | | | | | x | | `push` + `a` | | | x | x | | | x | x | | | | | | | | | `divine` + `n` | x | x | x | x | | | x | | x | | | | | | | +| `pick` + `i` | x | | x | x | | | x | | | x | | | | | | +| `place` + `i` | x | | x | x | | | x | | | x | | | | | | | `dup` + `i` | x | | x | x | | | x | x | | | | | | | | | `swap` + `i` | x | | x | x | | | x | | | x | | | | | | | `nop` | | | x | x | | x | | | | x | 0 | x | | | | diff --git a/specification/src/instruction-specific-transition-constraints.md b/specification/src/instruction-specific-transition-constraints.md index f7716470..d7619e31 100644 --- a/specification/src/instruction-specific-transition-constraints.md +++ b/specification/src/instruction-specific-transition-constraints.md @@ -20,6 +20,30 @@ In addition to its [instruction groups](instruction-groups.md), this instruction This instruction is fully constrained by its [instruction groups](instruction-groups.md) +## Instruction `pick` + `i` + +This instruction makes use of [indicator polynomials](instruction-groups.md#indicator-polynomials-ind_ihv3-hv2-hv1-hv0). +In addition to its [instruction groups](instruction-groups.md), this instruction has the following constraints. + +### Description + +For 0 ⩽ `i` < 16: +1. Stack element `i` is moved to the top. +1. For 0 ⩽ `j` < `i`: stack element `j` is shifted down by 1. +1. For `j` > `i`: stack element `j` remains unchanged. + +## Instruction `place` + `i` + +This instruction makes use of [indicator polynomials](instruction-groups.md#indicator-polynomials-ind_ihv3-hv2-hv1-hv0). +In addition to its [instruction groups](instruction-groups.md), this instruction has the following constraints. + +### Description + +For 0 ⩽ `i` < 16: +1. Stack element 0 is moved to position `i`. +1. For 0 ⩽ `j` < `i`: stack element `j` is shifted up by 1. +1. For `j` > `i`: stack element `j` remains unchanged. + ## Instruction `dup` + `i` This instruction makes use of [indicator polynomials](instruction-groups.md#indicator-polynomials-ind_ihv3-hv2-hv1-hv0). diff --git a/specification/src/instructions.md b/specification/src/instructions.md index 68d2ecb5..83758310 100644 --- a/specification/src/instructions.md +++ b/specification/src/instructions.md @@ -25,8 +25,10 @@ The third property allows efficient arithmetization of the running product for t | `pop` + `n` | 3 | e.g., `_ c b a` | e.g., `_` | Pops the `n` top elements from the stack. 1 ⩽ `n` ⩽ 5 | | `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 | +| `pick` + `i` | 17 | e.g., `_ d x c b a` | e.g., `_ d c b a x` | Moves the element indicated by `i` to the top of the stack. 0 ⩽ `i` < 16 | +| `place` + `i` | 25 | e.g., `_ d c b a x` | e.g., `_ d x c b a` | Moves the top of the stack to the indicated position `i`. 0 ⩽ `i` < 16 | +| `dup` + `i` | 33 | 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` | 41 | 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. @@ -46,7 +48,7 @@ the divined values were supplied as and are read from secret input. | `halt` | 0 | `_` | `_` | `ip` | `ip+1` | `_` | `_` | Solves the halting problem (if the instruction is reached). Indicates graceful shutdown of the VM. | | `nop` | 8 | `_` | `_` | `ip` | `ip+1` | `_` | `_` | Do nothing | | `skiz` | 2 | `_ a` | `_` | `ip` | `ip+s` | `_` | `_` | Skip next instruction if `a` is zero. `s` ∈ {1, 2, 3} depends on `a` and whether the next instruction takes an argument. | -| `call` + `d` | 33 | `_` | `_` | `ip` | `d` | `_` | `_ (ip+2, d)` | Push `(ip+2,d)` to the jump stack, and jump to absolute address `d` | +| `call` + `d` | 49 | `_` | `_` | `ip` | `d` | `_` | `_ (ip+2, d)` | Push `(ip+2,d)` to the jump stack, and jump to absolute address `d` | | `return` | 16 | `_` | `_` | `ip` | `o` | `_ (o, d)` | `_` | Pop one pair off the jump stack and jump to that pair's return address (which is the first element). | | `recurse` | 24 | `_` | `_` | `ip` | `d` | `_ (o, d)` | `_ (o, d)` | Peek at the top pair of the jump stack and jump to that pair's destination address (which is the second element). | | `recurse_or_return` | 32 | `_ b a .....` | `_ b a .....` | `ip` | `d` or `o` | `_ (o, d)` | `_ (o, d)` or `_` | Like `recurse` if `st5 = a != b = st6`, like `return` if `a == b`. See also extended description below. | @@ -64,7 +66,7 @@ The instruction is designed to facilitate loops using pointer equality as termin | Instruction | Opcode | old op stack | new op stack | old RAM | new RAM | Description | |:------------------|-------:|:---------------------|:-----------------------|:--------------------|:--------------------|:---------------------------------------------------------------------------------------------------------------------------------------------| -| `read_mem` + `n` | 41 | e.g., `_ p+2` | e.g., `_ v2 v1 v0 p-1` | [p: v0, p+1, v1, …] | [p: v0, p+1, v1, …] | Reads consecutive values `vi` from RAM at address `p` and puts them onto the op stack. Decrements RAM pointer (`st0`) by `n`. 1 ⩽ `n` ⩽ 5 | +| `read_mem` + `n` | 57 | e.g., `_ p+2` | e.g., `_ v2 v1 v0 p-1` | [p: v0, p+1, v1, …] | [p: v0, p+1, v1, …] | Reads consecutive values `vi` from RAM at address `p` and puts them onto the op stack. Decrements RAM pointer (`st0`) by `n`. 1 ⩽ `n` ⩽ 5 | | `write_mem` + `n` | 11 | e.g., `_ v2 v1 v0 p` | e.g., `_ p+3` | [] | [p: v0, p+1, v1, …] | Writes op stack's `n` top-most values `vi` to RAM at the address `p+i`, popping the `vi`. Increments RAM pointer (`st0`) by `n`. 1 ⩽ `n` ⩽ 5 | For the benefit of clarity, the effect of every possible argument is given below. @@ -112,7 +114,7 @@ Triton VM cannot know the number of elements that will be absorbed. | Instruction | Opcode | old op stack | new op stack | Description | |:-------------|-------:|:-------------|:-------------|:---------------------------------------------------------------------------------------------------------------------------| | `add` | 42 | `_ b a` | `_ c` | Computes the sum (`c`) of the top two elements of the stack (`b` and `a`) over the field. | -| `addi` + `a` | 49 | `_ b` | `_ c` | Computes the sum (`c`) of the top element of the stack (`b`) and the immediate argument (`a`). | +| `addi` + `a` | 65 | `_ b` | `_ c` | Computes the sum (`c`) of the top element of the stack (`b`) and the immediate argument (`a`). | | `mul` | 50 | `_ b a` | `_ c` | Computes the product (`c`) of the top two elements of the stack (`b` and `a`) over the field. | | `invert` | 64 | `_ a` | `_ b` | Computes the multiplicative inverse (over the field) of the top of the stack. Crashes the VM if the top of the stack is 0. | | `eq` | 58 | `_ b a` | `_ (a == b)` | Tests the top two stack elements for equality. | @@ -143,7 +145,7 @@ Triton VM cannot know the number of elements that will be absorbed. | Instruction | Opcode | old op stack | new op stack | Description | |:-----------------|-------:|:----------------|:----------------|:-----------------------------------------------------------------------------------------| -| `read_io` + `n` | 49 | e.g., `_` | e.g., `_ c b a` | Reads `n` B-Field elements from standard input and pushes them to the stack. 1 ⩽ `n` ⩽ 5 | +| `read_io` + `n` | 73 | e.g., `_` | e.g., `_ c b a` | Reads `n` B-Field elements from standard input and pushes them to the stack. 1 ⩽ `n` ⩽ 5 | | `write_io` + `n` | 19 | e.g., `_ c b a` | e.g., `_` | Pops `n` elements from the stack and writes them to standard output. 1 ⩽ `n` ⩽ 5 | ## Many-In-One diff --git a/triton-air/src/table/processor.rs b/triton-air/src/table/processor.rs index 6c4b105e..a0b6c04e 100644 --- a/triton-air/src/table/processor.rs +++ b/triton-air/src/table/processor.rs @@ -880,6 +880,96 @@ fn instruction_divine( .concat() } +fn instruction_pick( + circuit_builder: &ConstraintCircuitBuilder, +) -> Vec> { + let curr_row = |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); + + let stack = (0..OpStackElement::COUNT) + .map(ProcessorTable::op_stack_column_by_index) + .collect_vec(); + let stack_with_picked_i = |i| { + let mut stack = stack.clone(); + let new_top = stack.remove(i); + stack.insert(0, new_top); + stack.into_iter() + }; + + let next_stack = stack.iter().map(|&st| next_row(st)).collect_vec(); + let curr_stack_with_picked_i = |i| stack_with_picked_i(i).map(curr_row).collect_vec(); + + let compress = |stack: Vec<_>| -> ConstraintCircuitMonad<_> { + assert_eq!(OpStackElement::COUNT, stack.len()); + let weight = |i| circuit_builder.challenge(stack_weight_by_index(i)); + let enumerated_stack = stack.into_iter().enumerate(); + enumerated_stack.map(|(i, st)| weight(i) * st).sum() + }; + + let next_stack_is_current_stack_with_picked_i = |i| { + indicator_polynomial(circuit_builder, i) + * (compress(next_stack.clone()) - compress(curr_stack_with_picked_i(i))) + }; + let next_stack_is_current_stack_with_correct_element_picked = (0..OpStackElement::COUNT) + .map(next_stack_is_current_stack_with_picked_i) + .sum(); + + [ + vec![next_stack_is_current_stack_with_correct_element_picked], + instruction_group_decompose_arg(circuit_builder), + instruction_group_step_2(circuit_builder), + instruction_group_no_ram(circuit_builder), + instruction_group_no_io(circuit_builder), + instruction_group_keep_op_stack_height(circuit_builder), + ] + .concat() +} + +fn instruction_place( + circuit_builder: &ConstraintCircuitBuilder, +) -> Vec> { + let curr_row = |col: MainColumn| circuit_builder.input(CurrentMain(col.master_main_index())); + let next_row = |col: MainColumn| circuit_builder.input(NextMain(col.master_main_index())); + + let stack = (0..OpStackElement::COUNT) + .map(ProcessorTable::op_stack_column_by_index) + .collect_vec(); + let stack_with_placed_i = |i| { + let mut stack = stack.clone(); + let old_top = stack.remove(0); + stack.insert(i, old_top); + stack.into_iter() + }; + + let next_stack = stack.iter().map(|&st| next_row(st)).collect_vec(); + let curr_stack_with_placed_i = |i| stack_with_placed_i(i).map(curr_row).collect_vec(); + + let compress = |stack: Vec<_>| -> ConstraintCircuitMonad<_> { + assert_eq!(OpStackElement::COUNT, stack.len()); + let weight = |i| circuit_builder.challenge(stack_weight_by_index(i)); + let enumerated_stack = stack.into_iter().enumerate(); + enumerated_stack.map(|(i, st)| weight(i) * st).sum() + }; + + let next_stack_is_current_stack_with_placed_i = |i| { + indicator_polynomial(circuit_builder, i) + * (compress(next_stack.clone()) - compress(curr_stack_with_placed_i(i))) + }; + let next_stack_is_current_stack_with_correct_element_placed = (0..OpStackElement::COUNT) + .map(next_stack_is_current_stack_with_placed_i) + .sum(); + + [ + vec![next_stack_is_current_stack_with_correct_element_placed], + instruction_group_decompose_arg(circuit_builder), + instruction_group_step_2(circuit_builder), + instruction_group_no_ram(circuit_builder), + instruction_group_no_io(circuit_builder), + instruction_group_keep_op_stack_height(circuit_builder), + ] + .concat() +} + fn instruction_dup( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { @@ -2071,6 +2161,8 @@ pub fn transition_constraints_for_instruction( Instruction::Pop(_) => instruction_pop(circuit_builder), Instruction::Push(_) => instruction_push(circuit_builder), Instruction::Divine(_) => instruction_divine(circuit_builder), + Instruction::Pick(_) => instruction_pick(circuit_builder), + Instruction::Place(_) => instruction_place(circuit_builder), Instruction::Dup(_) => instruction_dup(circuit_builder), Instruction::Swap(_) => instruction_swap(circuit_builder), Instruction::Halt => instruction_halt(circuit_builder), diff --git a/triton-isa/src/instruction.rs b/triton-isa/src/instruction.rs index 1884457e..4313d6c2 100644 --- a/triton-isa/src/instruction.rs +++ b/triton-isa/src/instruction.rs @@ -32,6 +32,8 @@ pub const ALL_INSTRUCTIONS: [Instruction; Instruction::COUNT] = [ Instruction::Pop(NumberOfWords::N1), Instruction::Push(BFieldElement::ZERO), Instruction::Divine(NumberOfWords::N1), + Instruction::Pick(OpStackElement::ST0), + Instruction::Place(OpStackElement::ST0), Instruction::Dup(OpStackElement::ST0), Instruction::Swap(OpStackElement::ST0), Instruction::Halt, @@ -213,6 +215,8 @@ pub enum AnInstruction { Pop(NumberOfWords), Push(BFieldElement), Divine(NumberOfWords), + Pick(OpStackElement), + Place(OpStackElement), Dup(OpStackElement), Swap(OpStackElement), @@ -279,17 +283,19 @@ impl AnInstruction { AnInstruction::Pop(_) => 3, AnInstruction::Push(_) => 1, AnInstruction::Divine(_) => 9, - AnInstruction::Dup(_) => 17, - AnInstruction::Swap(_) => 25, + AnInstruction::Pick(_) => 17, + AnInstruction::Place(_) => 25, + AnInstruction::Dup(_) => 33, + AnInstruction::Swap(_) => 41, AnInstruction::Halt => 0, AnInstruction::Nop => 8, AnInstruction::Skiz => 2, - AnInstruction::Call(_) => 33, + AnInstruction::Call(_) => 49, AnInstruction::Return => 16, AnInstruction::Recurse => 24, AnInstruction::RecurseOrReturn => 32, AnInstruction::Assert => 10, - AnInstruction::ReadMem(_) => 41, + AnInstruction::ReadMem(_) => 57, AnInstruction::WriteMem(_) => 11, AnInstruction::Hash => 18, AnInstruction::AssertVector => 26, @@ -298,7 +304,7 @@ impl AnInstruction { AnInstruction::SpongeAbsorbMem => 48, AnInstruction::SpongeSqueeze => 56, AnInstruction::Add => 42, - AnInstruction::AddI(_) => 49, + AnInstruction::AddI(_) => 65, AnInstruction::Mul => 50, AnInstruction::Invert => 64, AnInstruction::Eq => 58, @@ -314,7 +320,7 @@ impl AnInstruction { AnInstruction::XxMul => 74, AnInstruction::XInvert => 72, AnInstruction::XbMul => 82, - AnInstruction::ReadIo(_) => 57, + AnInstruction::ReadIo(_) => 73, AnInstruction::WriteIo(_) => 19, AnInstruction::MerkleStep => 36, AnInstruction::MerkleStepMem => 44, @@ -328,6 +334,8 @@ impl AnInstruction { AnInstruction::Pop(_) => "pop", AnInstruction::Push(_) => "push", AnInstruction::Divine(_) => "divine", + AnInstruction::Pick(_) => "pick", + AnInstruction::Place(_) => "place", AnInstruction::Dup(_) => "dup", AnInstruction::Swap(_) => "swap", AnInstruction::Halt => "halt", @@ -381,6 +389,7 @@ impl AnInstruction { match self { AnInstruction::Pop(_) | AnInstruction::Push(_) => 2, AnInstruction::Divine(_) => 2, + AnInstruction::Pick(_) | AnInstruction::Place(_) => 2, AnInstruction::Dup(_) | AnInstruction::Swap(_) => 2, AnInstruction::Call(_) => 2, AnInstruction::ReadMem(_) | AnInstruction::WriteMem(_) => 2, @@ -392,10 +401,7 @@ impl AnInstruction { /// Get the i'th instruction bit pub fn ib(&self, arg: InstructionBit) -> BFieldElement { - let opcode = self.opcode(); - let bit_number: usize = arg.into(); - - ((opcode >> bit_number) & 1).into() + bfe!((self.opcode() >> usize::from(arg)) & 1) } pub fn map_call_address(&self, f: F) -> AnInstruction @@ -407,6 +413,8 @@ impl AnInstruction { AnInstruction::Pop(x) => AnInstruction::Pop(*x), AnInstruction::Push(x) => AnInstruction::Push(*x), AnInstruction::Divine(x) => AnInstruction::Divine(*x), + AnInstruction::Pick(x) => AnInstruction::Pick(*x), + AnInstruction::Place(x) => AnInstruction::Place(*x), AnInstruction::Dup(x) => AnInstruction::Dup(*x), AnInstruction::Swap(x) => AnInstruction::Swap(*x), AnInstruction::Halt => AnInstruction::Halt, @@ -456,6 +464,8 @@ impl AnInstruction { AnInstruction::Pop(n) => -(n.num_words() as i32), AnInstruction::Push(_) => 1, AnInstruction::Divine(n) => n.num_words() as i32, + AnInstruction::Pick(_) => 0, + AnInstruction::Place(_) => 0, AnInstruction::Dup(_) => 1, AnInstruction::Swap(_) => 0, AnInstruction::Halt => 0, @@ -523,6 +533,8 @@ impl Display for AnInstruction { write!(f, "{}", self.name())?; match self { AnInstruction::Push(arg) => write!(f, " {arg}"), + AnInstruction::Pick(arg) => write!(f, " {arg}"), + AnInstruction::Place(arg) => write!(f, " {arg}"), AnInstruction::Pop(arg) => write!(f, " {arg}"), AnInstruction::Divine(arg) => write!(f, " {arg}"), AnInstruction::Dup(arg) => write!(f, " {arg}"), @@ -546,6 +558,8 @@ impl Instruction { AnInstruction::Call(arg) => Some(*arg), AnInstruction::Pop(arg) => Some(arg.into()), AnInstruction::Divine(arg) => Some(arg.into()), + AnInstruction::Pick(arg) => Some(arg.into()), + AnInstruction::Place(arg) => Some(arg.into()), AnInstruction::Dup(arg) => Some(arg.into()), AnInstruction::Swap(arg) => Some(arg.into()), AnInstruction::ReadMem(arg) => Some(arg.into()), @@ -568,6 +582,8 @@ impl Instruction { AnInstruction::Pop(_) => AnInstruction::Pop(num_words?), AnInstruction::Push(_) => AnInstruction::Push(new_arg), AnInstruction::Divine(_) => AnInstruction::Divine(num_words?), + AnInstruction::Pick(_) => AnInstruction::Pick(op_stack_element?), + AnInstruction::Place(_) => AnInstruction::Place(op_stack_element?), AnInstruction::Dup(_) => AnInstruction::Dup(op_stack_element?), AnInstruction::Swap(_) => AnInstruction::Swap(op_stack_element?), AnInstruction::Call(_) => AnInstruction::Call(new_arg), @@ -1106,11 +1122,13 @@ pub mod tests { #[test] fn can_change_arg() { - for intsr in ALL_INSTRUCTIONS { - if let Some(arg) = intsr.arg() { - assert_ne!(intsr, intsr.change_arg(arg + bfe!(1)).unwrap()); + for instr in ALL_INSTRUCTIONS { + if let Some(arg) = instr.arg() { + let new_instr = instr.change_arg(arg + bfe!(1)).unwrap(); + assert_eq!(instr.opcode(), new_instr.opcode()); + assert_ne!(instr, new_instr); } else { - assert!(intsr.change_arg(bfe!(0)).is_err()) + assert!(instr.change_arg(bfe!(0)).is_err()) } } } diff --git a/triton-isa/src/lib.rs b/triton-isa/src/lib.rs index dcc84569..e75aadaa 100644 --- a/triton-isa/src/lib.rs +++ b/triton-isa/src/lib.rs @@ -219,6 +219,8 @@ macro_rules! triton_asm { [pop $arg:literal; $num:expr] => { vec![ $crate::triton_instr!(pop $arg); $num ] }; [push $arg:literal; $num:expr] => { vec![ $crate::triton_instr!(push $arg); $num ] }; [divine $arg:literal; $num:expr] => { vec![ $crate::triton_instr!(divine $arg); $num ] }; + [pick $arg:literal; $num:expr] => { vec![ $crate::triton_instr!(pick $arg); $num ] }; + [place $arg:literal; $num:expr] => { vec![ $crate::triton_instr!(place $arg); $num ] }; [dup $arg:literal; $num:expr] => { vec![ $crate::triton_instr!(dup $arg); $num ] }; [swap $arg:literal; $num:expr] => { vec![ $crate::triton_instr!(swap $arg); $num ] }; [call $arg:ident; $num:expr] => { vec![ $crate::triton_instr!(call $arg); $num ] }; @@ -267,6 +269,16 @@ macro_rules! triton_instr { let instruction = $crate::instruction::AnInstruction::::Divine(argument); $crate::instruction::LabelledInstruction::Instruction(instruction) }}; + (pick $arg:literal) => {{ + let argument = $crate::op_stack::OpStackElement::try_from($arg).unwrap(); + let instruction = $crate::instruction::AnInstruction::::Pick(argument); + $crate::instruction::LabelledInstruction::Instruction(instruction) + }}; + (place $arg:literal) => {{ + let argument = $crate::op_stack::OpStackElement::try_from($arg).unwrap(); + let instruction = $crate::instruction::AnInstruction::::Place(argument); + $crate::instruction::LabelledInstruction::Instruction(instruction) + }}; (dup $arg:literal) => {{ let argument = $crate::op_stack::OpStackElement::try_from($arg).unwrap(); let instruction = $crate::instruction::AnInstruction::::Dup(argument); diff --git a/triton-isa/src/op_stack.rs b/triton-isa/src/op_stack.rs index 6c349e44..cbd89951 100644 --- a/triton-isa/src/op_stack.rs +++ b/triton-isa/src/op_stack.rs @@ -83,6 +83,19 @@ impl OpStack { self.stack.pop().ok_or(OpStackError::TooShallow) } + pub fn insert(&mut self, index: OpStackElement, element: BFieldElement) { + let insertion_index = self.len() - usize::from(index); + self.stack.insert(insertion_index, element); + self.record_underflow_io(UnderflowIO::Write); + } + + pub fn remove(&mut self, index: OpStackElement) -> BFieldElement { + self.record_underflow_io(UnderflowIO::Read); + let top_of_stack = self.len() - 1; + let index = top_of_stack - usize::from(index); + self.stack.remove(index) + } + fn record_underflow_io(&mut self, io_type: fn(BFieldElement) -> UnderflowIO) { let underflow_io = io_type(self.first_underflow_element()); self.underflow_io_sequence.push(underflow_io); @@ -982,4 +995,34 @@ mod tests { let_assert!(Ok(some_u32) = op_stack.get_u32(st)); assert!(valid_u32 == some_u32); } + + #[proptest] + fn inserting_an_element_into_the_stack_puts_it_at_the_correct_position( + #[strategy(arb())] insertion_index: OpStackElement, + #[strategy(arb())] insertion_element: BFieldElement, + ) { + let mut op_stack = OpStack::default(); + op_stack.insert(insertion_index, insertion_element); + prop_assert_eq!(insertion_element, op_stack[insertion_index]); + + let expected_len = OpStackElement::COUNT + 1; + prop_assert_eq!(expected_len, op_stack.len()); + } + + #[proptest] + fn removing_an_element_from_the_stack_removes_the_correct_element( + #[strategy(arb())] removal_index: OpStackElement, + ) { + let mut op_stack = OpStack::default(); + for i in (0..OpStackElement::COUNT as u64).rev() { + op_stack.push(bfe!(i)); + } + + let expected_element = BFieldElement::from(removal_index); + let removed_element = op_stack.remove(removal_index); + prop_assert_eq!(expected_element, removed_element); + + let expected_len = 2 * OpStackElement::COUNT - 1; + prop_assert_eq!(expected_len, op_stack.len()); + } } diff --git a/triton-isa/src/parser.rs b/triton-isa/src/parser.rs index df662652..3adfff87 100644 --- a/triton-isa/src/parser.rs +++ b/triton-isa/src/parser.rs @@ -234,10 +234,12 @@ fn an_instruction(s: &str) -> ParseResult> { let pop = pop_instruction(); let push = push_instruction(); let divine = divine_instruction(); + let pick = pick_instruction(); + let place = place_instruction(); let dup = dup_instruction(); let swap = swap_instruction(); - let opstack_manipulation = alt((pop, push, divine, dup, swap)); + let opstack_manipulation = alt((pop, push, divine, pick, place, dup, swap)); // Control flow let halt = instruction("halt", AnInstruction::Halt); @@ -385,6 +387,22 @@ fn divine_instruction() -> impl Fn(&str) -> ParseResult> { } } +fn pick_instruction() -> impl Fn(&str) -> ParseResult> { + move |s: &str| { + let (s, _) = token1("pick")(s)?; + let (s, arg) = stack_register(s)?; + Ok((s, AnInstruction::Pick(arg))) + } +} + +fn place_instruction() -> impl Fn(&str) -> ParseResult> { + move |s: &str| { + let (s, _) = token1("place")(s)?; + let (s, arg) = stack_register(s)?; + Ok((s, AnInstruction::Place(arg))) + } +} + fn dup_instruction() -> impl Fn(&str) -> ParseResult> { move |s: &str| { let (s, _) = token1("dup")(s)?; // require space before argument diff --git a/triton-vm/src/stark.rs b/triton-vm/src/stark.rs index b84dbea3..1de993ba 100644 --- a/triton-vm/src/stark.rs +++ b/triton-vm/src/stark.rs @@ -2369,6 +2369,33 @@ pub(crate) mod tests { ); } + #[test] + fn prove_verify_program_using_pick_and_place() { + let input = bfe_vec![6, 3, 7, 5, 1, 2, 4, 4, 7, 3, 6, 1, 5, 2]; + let program = triton_program! { // i: 13 12 11 10 9 8 7 6 5 4 3 2 1 0 + read_io 5 read_io 5 read_io 4 // _ 6 3 7 5 ›1‹ 2 4 4 7 3 6 ›1‹ 5 2 + pick 2 pick 9 place 13 place 13 // _ 1 1 6 3 7 5 ›2‹ 4 4 7 3 6 5 ›2‹ + pick 0 pick 7 place 13 place 13 // _ 2 2 1 1 6 ›3‹ 7 5 4 4 7 ›3‹ 6 5 + pick 2 pick 8 place 13 place 13 // _ 3 3 2 2 1 1 6 7 5 ›4‹›4‹ 7 6 5 + pick 3 pick 4 place 13 place 13 // _ 4 4 3 3 2 2 1 1 6 7 ›5‹ 7 6 ›5‹ + pick 0 pick 3 place 13 place 13 // _ 5 5 4 4 3 3 2 2 1 1 ›6‹ 7 7 ›6‹ + pick 0 pick 3 place 13 place 13 // _ 6 6 5 5 4 4 3 3 2 2 1 1 ›7‹›7‹ + pick 1 pick 1 place 13 place 13 // _ 7 7 6 6 5 5 4 4 3 3 2 2 1 1 + write_io 5 write_io 5 write_io 4 // _ + halt + }; + + let program_and_input = ProgramAndInput::new(program).with_input(input); + let output = program_and_input.run().unwrap(); + let expected_output = bfe_vec![1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 6, 7, 7]; + assert!(expected_output == output); + + prove_and_verify( + program_and_input, + DEFAULT_LOG2_FRI_EXPANSION_FACTOR_FOR_TESTS, + ); + } + #[test] fn constraints_evaluate_to_zero_on_many_u32_operations() { let many_u32_instructions = ProgramAndInput::new( @@ -2712,6 +2739,16 @@ pub(crate) mod tests { assert // _ addr 0 pop 2 // _ + // stack manipulation + push 1 push 2 push 3 // _ 1 2 3 + place 2 // _ 3 1 2 + pick 1 // _ 3 2 1 + swap 2 // _ 1 2 3 + dup 2 assert // _ 1 2 3 + addi -2 assert // _ 1 2 + addi -1 assert // _ 1 + assert // _ + // dot_step push 0 push 0 push 0 // _ [accumulator; 3] push 500 // _ [accumulator; 3] addr_0 diff --git a/triton-vm/src/table/processor.rs b/triton-vm/src/table/processor.rs index 135254c3..6e37c424 100644 --- a/triton-vm/src/table/processor.rs +++ b/triton-vm/src/table/processor.rs @@ -931,6 +931,40 @@ pub(crate) mod tests { assert_constraints_for_rows_with_debug_info(&test_rows, debug_info); } + #[test] + fn transition_constraints_for_instruction_pick() { + let set_up_stack = (0..OpStackElement::COUNT) + .rev() + .flat_map(|i| triton_asm!(push { i })) + .collect_vec(); + let test_rows = (0..OpStackElement::COUNT) + .map(|i| triton_program!({&set_up_stack} pick {i} push {i} eq assert halt)) + .map(|program| test_row_from_program(program, 16)) + .collect_vec(); + + let debug_info = TestRowsDebugInfo { + instruction: Instruction::Pick(OpStackElement::ST0), + debug_cols_curr_row: vec![MainColumn::ST0, MainColumn::ST1, MainColumn::ST2], + debug_cols_next_row: vec![MainColumn::ST0, MainColumn::ST1, MainColumn::ST2], + }; + assert_constraints_for_rows_with_debug_info(&test_rows, debug_info); + } + + #[test] + fn transition_constraints_for_instruction_place() { + let test_rows = (0..OpStackElement::COUNT) + .map(|i| triton_program!(push 42 place {i} dup {i} push 42 eq assert halt)) + .map(|program| test_row_from_program(program, 1)) + .collect_vec(); + + let debug_info = TestRowsDebugInfo { + instruction: Instruction::Place(OpStackElement::ST0), + debug_cols_curr_row: vec![MainColumn::ST0, MainColumn::ST1, MainColumn::ST2], + debug_cols_next_row: vec![MainColumn::ST0, MainColumn::ST1, MainColumn::ST2], + }; + assert_constraints_for_rows_with_debug_info(&test_rows, debug_info); + } + #[test] fn transition_constraints_for_instruction_dup() { let programs = [ diff --git a/triton-vm/src/vm.rs b/triton-vm/src/vm.rs index eccd41d8..1ffc9720 100644 --- a/triton-vm/src/vm.rs +++ b/triton-vm/src/vm.rs @@ -278,6 +278,8 @@ impl VMState { match current_instruction { Instruction::Pop(_) | Instruction::Divine(_) + | Instruction::Pick(_) + | Instruction::Place(_) | Instruction::Dup(_) | Instruction::Swap(_) | Instruction::ReadMem(_) @@ -378,6 +380,8 @@ impl VMState { Instruction::Pop(n) => self.pop(n)?, Instruction::Push(field_element) => self.push(field_element), Instruction::Divine(n) => self.divine(n)?, + Instruction::Pick(stack_element) => self.pick(stack_element), + Instruction::Place(stack_element) => self.place(stack_element)?, Instruction::Dup(stack_element) => self.dup(stack_element), Instruction::Swap(stack_element) => self.swap(stack_element), Instruction::Halt => self.halt(), @@ -490,6 +494,22 @@ impl VMState { Ok(vec![]) } + fn pick(&mut self, stack_register: OpStackElement) -> Vec { + let element = self.op_stack.remove(stack_register); + self.op_stack.push(element); + + self.instruction_pointer += 2; + vec![] + } + + fn place(&mut self, stack_register: OpStackElement) -> InstructionResult> { + let element = self.op_stack.pop()?; + self.op_stack.insert(stack_register, element); + + self.instruction_pointer += 2; + Ok(vec![]) + } + fn dup(&mut self, stack_register: OpStackElement) -> Vec { let element = self.op_stack[stack_register]; self.op_stack.push(element);