From 3b5bc128c086489301803e0f5b8881d00f681e97 Mon Sep 17 00:00:00 2001 From: Alan Szepieniec Date: Wed, 7 Aug 2024 17:10:43 +0200 Subject: [PATCH] feat: Add instruction `addi` --- specification/src/arithmetization-overview.md | 12 +++++----- specification/src/instruction-groups.md | 3 ++- specification/src/instructions.md | 13 ++++++----- triton-vm/src/instruction.rs | 14 +++++++++-- triton-vm/src/lib.rs | 5 ++++ triton-vm/src/parser.rs | 13 ++++++++++- triton-vm/src/stark.rs | 1 + triton-vm/src/table/processor_table.rs | 23 +++++++++++++++++++ triton-vm/src/vm.rs | 8 +++++++ 9 files changed, 76 insertions(+), 16 deletions(-) diff --git a/specification/src/arithmetization-overview.md b/specification/src/arithmetization-overview.md index 4d62474d0..18fa8537b 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 | 201 | 36 | 309 | +| DegreeLowering | 203 | 36 | 311 | | Randomizers | 0 | 1 | 3 | -| **TOTAL** | **350** | **86** | **608** | +| **TOTAL** | **352** | **86** | **610** | ## 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 | 207 | 1 | +| [ProcessorTable](processor-table.md) | 31 | 10 | 209 | 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 | @@ -59,7 +59,7 @@ 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** | **367** | **23** | +| **TOTAL** | **81** | **94** | **369** | **23** | @@ -71,7 +71,7 @@ In order to gauge the runtime cost for this step, the following table provides e | Processor | Op Stack | RAM | |----------:|---------:|------:| -| 34477 | 63981 | 22620 | +| 34609 | 64237 | 22716 | ## Opcode Pressure @@ -84,7 +84,7 @@ The table below helps answer this question at a glance. | IsU32 | ShrinksStack | HasArg | Num Opcodes | |-------------:|-------------:|-------------:|-------------:| | n | n | n | 12 | -| n | n | y | 7 | +| n | n | y | 8 | | n | y | n | 11 | | n | y | y | 3 | | y | n | n | 5 | diff --git a/specification/src/instruction-groups.md b/specification/src/instruction-groups.md index 564242672..da76489ca 100644 --- a/specification/src/instruction-groups.md +++ b/specification/src/instruction-groups.md @@ -58,7 +58,8 @@ A summary of all instructions and which groups they are part of is given in the | `sponge_absorb` | | | x | x | | x | | | | | | | | | | | `sponge_absorb_mem` | | | x | | | x | | | | | 5 | | | | | | `sponge_squeeze` | | | x | x | | x | | | | | | | | | | -| `add` | | | x | x | | x | | | | | | | x | | | +| `add` | | | x | x | | | | | | | | | x | | | +| `addi` + `a` | | | x | x | | | x | | | x | 1 | | | | | | `mul` | | | x | x | | x | | | | | | | x | | | | `invert` | | | x | x | | x | | | | x | 1 | | | | | | `eq` | | | x | x | | x | | | | | | | x | | | diff --git a/specification/src/instructions.md b/specification/src/instructions.md index 6913c522c..3493bf4cb 100644 --- a/specification/src/instructions.md +++ b/specification/src/instructions.md @@ -109,12 +109,13 @@ Triton VM cannot know the number of elements that will be absorbed. ## Base Field Arithmetic on Stack -| 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. | -| `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. | +| 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`). | +| `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. | ## Bitwise Arithmetic on Stack diff --git a/triton-vm/src/instruction.rs b/triton-vm/src/instruction.rs index 4217f20f1..a9ed24e14 100644 --- a/triton-vm/src/instruction.rs +++ b/triton-vm/src/instruction.rs @@ -189,6 +189,7 @@ pub enum AnInstruction { // Base field arithmetic on stack Add, + AddI(BFieldElement), Mul, Invert, Eq, @@ -245,6 +246,7 @@ impl AnInstruction { SpongeAbsorbMem => 48, SpongeSqueeze => 56, Add => 42, + AddI(_) => 49, Mul => 50, Invert => 64, Eq => 58, @@ -260,7 +262,7 @@ impl AnInstruction { XxMul => 74, XInvert => 72, XbMul => 82, - ReadIo(_) => 49, + ReadIo(_) => 57, WriteIo(_) => 19, MerkleStep => 36, XxDotStep => 80, @@ -292,6 +294,7 @@ impl AnInstruction { SpongeAbsorbMem => "sponge_absorb_mem", SpongeSqueeze => "sponge_squeeze", Add => "add", + AddI(_) => "addi", Mul => "mul", Invert => "invert", Eq => "eq", @@ -327,6 +330,7 @@ impl AnInstruction { Dup(_) | Swap(_) => 2, Call(_) => 2, ReadMem(_) | WriteMem(_) => 2, + AddI(_) => 2, ReadIo(_) | WriteIo(_) => 2, _ => 1, } @@ -368,6 +372,7 @@ impl AnInstruction { SpongeAbsorbMem => SpongeAbsorbMem, SpongeSqueeze => SpongeSqueeze, Add => Add, + AddI(x) => AddI(*x), Mul => Mul, Invert => Invert, Eq => Eq, @@ -415,6 +420,7 @@ impl AnInstruction { SpongeAbsorbMem => 0, SpongeSqueeze => 10, Add => -1, + AddI(_) => 0, Mul => -1, Invert => 0, Eq => -1, @@ -456,6 +462,7 @@ impl Display for AnInstruction { Dup(arg) | Swap(arg) => write!(f, " {arg}"), Call(arg) => write!(f, " {arg}"), ReadMem(arg) | WriteMem(arg) => write!(f, " {arg}"), + AddI(arg) => write!(f, " {arg}"), ReadIo(arg) | WriteIo(arg) => write!(f, " {arg}"), _ => Ok(()), } @@ -470,6 +477,7 @@ impl Instruction { Pop(arg) | Divine(arg) => Some(arg.into()), Dup(arg) | Swap(arg) => Some(arg.into()), ReadMem(arg) | WriteMem(arg) => Some(arg.into()), + AddI(arg) => Some(*arg), ReadIo(arg) | WriteIo(arg) => Some(arg.into()), _ => None, } @@ -491,6 +499,7 @@ impl Instruction { Call(_) => Call(new_arg), ReadMem(_) => ReadMem(num_words?), WriteMem(_) => WriteMem(num_words?), + AddI(_) => AddI(new_arg), ReadIo(_) => ReadIo(num_words?), WriteIo(_) => WriteIo(num_words?), _ => return Err(illegal_argument_error), @@ -564,6 +573,7 @@ const fn all_instructions_with_default_args() -> [AnInstruction; SpongeAbsorbMem, SpongeSqueeze, Add, + AddI(BFieldElement::ZERO), Mul, Invert, Eq, @@ -841,7 +851,7 @@ pub mod tests { let opcode = instruction.opcode(); let maybe_entry = opcodes_to_instruction_map.insert(opcode, instruction); if let Some(other_instruction) = maybe_entry { - panic!("{other_instruction} and {instruction} both have opcode {opcode}.",); + panic!("{other_instruction} and {instruction} both have opcode {opcode}."); } } } diff --git a/triton-vm/src/lib.rs b/triton-vm/src/lib.rs index b0c931d3b..3e1ffa55b 100644 --- a/triton-vm/src/lib.rs +++ b/triton-vm/src/lib.rs @@ -474,6 +474,11 @@ macro_rules! triton_instr { let instruction = $crate::instruction::AnInstruction::::WriteMem(argument); $crate::instruction::LabelledInstruction::Instruction(instruction) }}; + (addi $arg:expr) => {{ + let argument = $crate::prelude::BFieldElement::from($arg); + let instruction = $crate::instruction::AnInstruction::::AddI(argument); + $crate::instruction::LabelledInstruction::Instruction(instruction) + }}; (read_io $arg:literal) => {{ let argument = $crate::op_stack::NumberOfWords::try_from($arg).unwrap(); let instruction = $crate::instruction::AnInstruction::::ReadIo(argument); diff --git a/triton-vm/src/parser.rs b/triton-vm/src/parser.rs index 89e875c90..8e4c89278 100644 --- a/triton-vm/src/parser.rs +++ b/triton-vm/src/parser.rs @@ -254,6 +254,7 @@ fn an_instruction(s: &str) -> ParseResult> { // Arithmetic on stack instructions let add = instruction("add", Add); + let addi = addi_instruction(); let mul = instruction("mul", Mul); let invert = instruction("invert", Invert); let eq = instruction("eq", Eq); @@ -270,7 +271,7 @@ fn an_instruction(s: &str) -> ParseResult> { let x_invert = instruction("x_invert", XInvert); let xb_mul = instruction("xb_mul", XbMul); - let base_field_arithmetic_on_stack = alt((add, mul, invert, eq)); + let base_field_arithmetic_on_stack = alt((mul, invert, eq)); let bitwise_arithmetic_on_stack = alt((split, lt, and, xor, log_2_floor, pow, div_mod, pop_count)); let extension_field_arithmetic_on_stack = alt((xx_add, xx_mul, x_invert, xb_mul)); @@ -304,6 +305,8 @@ fn an_instruction(s: &str) -> ParseResult> { assert, sponge_absorb_mem, sponge_absorb, + addi, + add, )); alt(( @@ -348,6 +351,14 @@ fn push_instruction() -> impl Fn(&str) -> ParseResult> { } } +fn addi_instruction() -> impl Fn(&str) -> ParseResult> { + move |s: &str| { + let (s, _) = token1("addi")(s)?; + let (s, elem) = field_element(s)?; + Ok((s, AddI(elem))) + } +} + fn divine_instruction() -> impl Fn(&str) -> ParseResult> { move |s: &str| { let (s, _) = token1("divine")(s)?; diff --git a/triton-vm/src/stark.rs b/triton-vm/src/stark.rs index 709ac76d9..f75a98c33 100644 --- a/triton-vm/src/stark.rs +++ b/triton-vm/src/stark.rs @@ -2831,6 +2831,7 @@ pub(crate) mod tests { // base field arithmetic add mul // _ bfe_0 bfe_1 bfe_2 bfe_3 + addi 0 // _ bfe_0 bfe_1 bfe_2 bfe_3 invert // _ bfe_0 bfe_1 bfe_2 bfe_3 mul add // _ bfe_0 bfe_1 eq // _ bfe_0 diff --git a/triton-vm/src/table/processor_table.rs b/triton-vm/src/table/processor_table.rs index 02404020f..cc6dcf346 100644 --- a/triton-vm/src/table/processor_table.rs +++ b/triton-vm/src/table/processor_table.rs @@ -2076,6 +2076,28 @@ impl ExtProcessorTable { .concat() } + fn instruction_addi( + circuit_builder: &ConstraintCircuitBuilder, + ) -> Vec> { + let curr_base_row = |col: ProcessorBaseTableColumn| { + circuit_builder.input(CurrentBaseRow(col.master_base_table_index())) + }; + let next_base_row = |col: ProcessorBaseTableColumn| { + circuit_builder.input(NextBaseRow(col.master_base_table_index())) + }; + + let specific_constraints = + vec![next_base_row(ST0) - curr_base_row(ST0) - curr_base_row(NIA)]; + [ + specific_constraints, + Self::instruction_group_step_2(circuit_builder), + Self::instruction_group_op_stack_remains_except_top_n(circuit_builder, 1), + Self::instruction_group_no_ram(circuit_builder), + Self::instruction_group_no_io(circuit_builder), + ] + .concat() + } + fn instruction_mul( circuit_builder: &ConstraintCircuitBuilder, ) -> Vec> { @@ -2680,6 +2702,7 @@ impl ExtProcessorTable { SpongeAbsorbMem => ExtProcessorTable::instruction_sponge_absorb_mem(circuit_builder), SpongeSqueeze => ExtProcessorTable::instruction_sponge_squeeze(circuit_builder), Add => ExtProcessorTable::instruction_add(circuit_builder), + AddI(_) => ExtProcessorTable::instruction_addi(circuit_builder), Mul => ExtProcessorTable::instruction_mul(circuit_builder), Invert => ExtProcessorTable::instruction_invert(circuit_builder), Eq => ExtProcessorTable::instruction_eq(circuit_builder), diff --git a/triton-vm/src/vm.rs b/triton-vm/src/vm.rs index f86cac9c5..bca6406a2 100644 --- a/triton-vm/src/vm.rs +++ b/triton-vm/src/vm.rs @@ -246,6 +246,7 @@ impl VMState { SpongeSqueeze => self.sponge_squeeze()?, AssertVector => self.assert_vector()?, Add => self.add()?, + AddI(field_element) => self.addi(field_element), Mul => self.mul()?, Invert => self.invert()?, Eq => self.eq()?, @@ -583,6 +584,12 @@ impl VMState { Ok(vec![]) } + fn addi(&mut self, i: BFieldElement) -> Vec { + self.op_stack[ST0] += i; + self.instruction_pointer += 2; + vec![] + } + fn mul(&mut self) -> Result> { let lhs = self.op_stack.pop()?; let rhs = self.op_stack.pop()?; @@ -1543,6 +1550,7 @@ pub(crate) mod tests { ProgramAndInput::new(triton_program!( push 2 push -1 add assert push -1 push -1 mul assert + push 5 addi -4 assert push 3 dup 0 invert mul assert halt ))