Skip to content

Commit

Permalink
feat: Add instruction addi
Browse files Browse the repository at this point in the history
  • Loading branch information
@aszepieniec @jan-ferdinand
aszepieniec authored and jan-ferdinand committed Aug 12, 2024
1 parent e55c247 commit 3b5bc12
Show file tree
Hide file tree
Showing 9 changed files with 76 additions and 16 deletions.
12 changes: 6 additions & 6 deletions specification/src/arithmetization-overview.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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** |
<!-- auto-gen info stop table_overview -->

## Constraints
Expand Down Expand Up @@ -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 |
Expand All @@ -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** |
<!-- auto-gen info stop constraints_overview -->


Expand All @@ -71,7 +71,7 @@ In order to gauge the runtime cost for this step, the following table provides e
<!-- auto-gen info start tasm_air_evaluation_cost -->
| Processor | Op Stack | RAM |
|----------:|---------:|------:|
| 34477 | 63981 | 22620 |
| 34609 | 64237 | 22716 |
<!-- auto-gen info stop tasm_air_evaluation_cost -->

## Opcode Pressure
Expand All @@ -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 |
Expand Down
3 changes: 2 additions & 1 deletion specification/src/instruction-groups.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 | | |
Expand Down
13 changes: 7 additions & 6 deletions specification/src/instructions.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
14 changes: 12 additions & 2 deletions triton-vm/src/instruction.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -189,6 +189,7 @@ pub enum AnInstruction<Dest: PartialEq + Default> {

// Base field arithmetic on stack
Add,
AddI(BFieldElement),
Mul,
Invert,
Eq,
Expand Down Expand Up @@ -245,6 +246,7 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
SpongeAbsorbMem => 48,
SpongeSqueeze => 56,
Add => 42,
AddI(_) => 49,
Mul => 50,
Invert => 64,
Eq => 58,
Expand All @@ -260,7 +262,7 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
XxMul => 74,
XInvert => 72,
XbMul => 82,
ReadIo(_) => 49,
ReadIo(_) => 57,
WriteIo(_) => 19,
MerkleStep => 36,
XxDotStep => 80,
Expand Down Expand Up @@ -292,6 +294,7 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
SpongeAbsorbMem => "sponge_absorb_mem",
SpongeSqueeze => "sponge_squeeze",
Add => "add",
AddI(_) => "addi",
Mul => "mul",
Invert => "invert",
Eq => "eq",
Expand Down Expand Up @@ -327,6 +330,7 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
Dup(_) | Swap(_) => 2,
Call(_) => 2,
ReadMem(_) | WriteMem(_) => 2,
AddI(_) => 2,
ReadIo(_) | WriteIo(_) => 2,
_ => 1,
}
Expand Down Expand Up @@ -368,6 +372,7 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
SpongeAbsorbMem => SpongeAbsorbMem,
SpongeSqueeze => SpongeSqueeze,
Add => Add,
AddI(x) => AddI(*x),
Mul => Mul,
Invert => Invert,
Eq => Eq,
Expand Down Expand Up @@ -415,6 +420,7 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
SpongeAbsorbMem => 0,
SpongeSqueeze => 10,
Add => -1,
AddI(_) => 0,
Mul => -1,
Invert => 0,
Eq => -1,
Expand Down Expand Up @@ -456,6 +462,7 @@ impl<Dest: Display + PartialEq + Default> Display for AnInstruction<Dest> {
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(()),
}
Expand All @@ -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,
}
Expand All @@ -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),
Expand Down Expand Up @@ -564,6 +573,7 @@ const fn all_instructions_with_default_args() -> [AnInstruction<BFieldElement>;
SpongeAbsorbMem,
SpongeSqueeze,
Add,
AddI(BFieldElement::ZERO),
Mul,
Invert,
Eq,
Expand Down Expand Up @@ -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}.");
}
}
}
Expand Down
5 changes: 5 additions & 0 deletions triton-vm/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -474,6 +474,11 @@ macro_rules! triton_instr {
let instruction = $crate::instruction::AnInstruction::<String>::WriteMem(argument);
$crate::instruction::LabelledInstruction::Instruction(instruction)
}};
(addi $arg:expr) => {{
let argument = $crate::prelude::BFieldElement::from($arg);
let instruction = $crate::instruction::AnInstruction::<String>::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::<String>::ReadIo(argument);
Expand Down
13 changes: 12 additions & 1 deletion triton-vm/src/parser.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -254,6 +254,7 @@ fn an_instruction(s: &str) -> ParseResult<AnInstruction<String>> {

// 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);
Expand All @@ -270,7 +271,7 @@ fn an_instruction(s: &str) -> ParseResult<AnInstruction<String>> {
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));
Expand Down Expand Up @@ -304,6 +305,8 @@ fn an_instruction(s: &str) -> ParseResult<AnInstruction<String>> {
assert,
sponge_absorb_mem,
sponge_absorb,
addi,
add,
));

alt((
Expand Down Expand Up @@ -348,6 +351,14 @@ fn push_instruction() -> impl Fn(&str) -> ParseResult<AnInstruction<String>> {
}
}

fn addi_instruction() -> impl Fn(&str) -> ParseResult<AnInstruction<String>> {
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<AnInstruction<String>> {
move |s: &str| {
let (s, _) = token1("divine")(s)?;
Expand Down
1 change: 1 addition & 0 deletions triton-vm/src/stark.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
23 changes: 23 additions & 0 deletions triton-vm/src/table/processor_table.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2076,6 +2076,28 @@ impl ExtProcessorTable {
.concat()
}

fn instruction_addi(
circuit_builder: &ConstraintCircuitBuilder<DualRowIndicator>,
) -> Vec<ConstraintCircuitMonad<DualRowIndicator>> {
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<DualRowIndicator>,
) -> Vec<ConstraintCircuitMonad<DualRowIndicator>> {
Expand Down Expand Up @@ -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),
Expand Down
8 changes: 8 additions & 0 deletions triton-vm/src/vm.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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()?,
Expand Down Expand Up @@ -583,6 +584,12 @@ impl VMState {
Ok(vec![])
}

fn addi(&mut self, i: BFieldElement) -> Vec<CoProcessorCall> {
self.op_stack[ST0] += i;
self.instruction_pointer += 2;
vec![]
}

fn mul(&mut self) -> Result<Vec<CoProcessorCall>> {
let lhs = self.op_stack.pop()?;
let rhs = self.op_stack.pop()?;
Expand Down Expand Up @@ -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
))
Expand Down

0 comments on commit 3b5bc12

Please sign in to comment.