Skip to content

Commit

Permalink
add script to derive opcodes automatically, change opcodes slightly
Browse files Browse the repository at this point in the history
  • Loading branch information
jan-ferdinand committed Nov 11, 2022
1 parent 9668fbe commit 10064b2
Show file tree
Hide file tree
Showing 3 changed files with 110 additions and 24 deletions.
86 changes: 86 additions & 0 deletions opcodes.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,86 @@
import functools
from enum import IntEnum, IntFlag, auto

class Instruction(IntEnum):
Pop = 0
Push = auto()
Divine = auto()
Dup = auto()
Swap = auto()
Nop = auto()
Skiz = auto()
Call = auto()
Return = auto()
Recurse = auto()
Assert = auto()
Halt = auto()
ReadMem = auto()
WriteMem = auto()
Hash = auto()
DivineSibling = auto()
AssertVector = auto()
Add = auto()
Mul = auto()
Invert = auto()
Split = auto()
Eq = auto()
Lsb = auto()
XxAdd = auto()
XxMul = auto()
XInvert = auto()
XbMul = auto()
ReadIo = auto()
WriteIo = auto()

class InstructionBucket(IntFlag):
HasArg = auto()
ShrinkStack = auto()

# ===

def in_bucket(instruction_bucket, instruction):
if instruction_bucket == InstructionBucket.HasArg:
return instruction in [Instruction.Push, Instruction.Dup, Instruction.Swap, Instruction.Call]
if instruction_bucket == InstructionBucket.ShrinkStack:
return instruction in [Instruction.Pop, Instruction.Skiz, Instruction.Assert, Instruction.WriteIo,
Instruction.Add, Instruction.Mul, Instruction.Eq, Instruction.XbMul]
return False

def flag_set(instruction):
instruction_flags = [bucket for bucket in InstructionBucket if in_bucket(bucket, instruction)]
return functools.reduce(lambda x, y: x | y, instruction_flags, 0)

def opcode(instruction):
if instruction == Instruction.Halt:
return 0
instruction_flag_set = flag_set(instruction)
index_within_flag_set = 1 if instruction_flag_set == flag_set(Instruction.Halt) else 0
for inst in Instruction:
if inst < instruction and instruction_flag_set == flag_set(inst):
index_within_flag_set += 1
return index_within_flag_set * 2**len(InstructionBucket) + instruction_flag_set

def print_all_opcodes():
for instruction in Instruction:
print(f"{opcode(instruction):>02} {str(instruction)}")

def print_max_opcode():
print(f"highest opcode: {max([opcode(instruction) for instruction in Instruction])}")

# ===

def opcodes_are_unique_test():
all_opcodes = [opcode(instruction) for instruction in Instruction]
all_opcodes = sorted(all_opcodes)
assert(list(set(all_opcodes)) == list(all_opcodes))

def tests():
opcodes_are_unique_test()

# ===

tests()

print_all_opcodes()
print()
print_max_opcode()
24 changes: 12 additions & 12 deletions specification/src/instructions.md
Original file line number Diff line number Diff line change
Expand Up @@ -54,16 +54,16 @@ the value `a` was supplied as a secret input.

| Instruction | Opcode | old OpStack | new OpStack | old `ramv` | new `ramv` | Description |
|:------------|-------:|:------------|:------------|:-----------|:-----------|:----------------------------------------------------------------------------------------|
| `read_mem` | 24 | `_ p a` | `_ p v` | `v` | `v` | Reads value `v` from RAM at address `p` and overwrites the top of the OpStack with `v`. |
| `write_mem` | 28 | `_ p v` | `_ p v` | `_` | `v` | Writes OpStack's top-most value `v` to RAM at the address `p`. |
| `read_mem` | 20 | `_ p a` | `_ p v` | `v` | `v` | Reads value `v` from RAM at address `p` and overwrites the top of the OpStack with `v`. |
| `write_mem` | 24 | `_ p v` | `_ p v` | `_` | `v` | Writes OpStack's top-most value `v` to RAM at the address `p`. |

## Hashing

| Instruction | Opcode | old OpStack | new OpStack | Description |
|:-----------------|-------:|:----------------|:------------------------------|:--------------------------------------------------------------------------------------------------------|
| `hash` | 32 | `_jihgfedcba` | `_yxwvu00000` | Overwrites the stack's 10 top-most elements with their hash digest (length 6) and 6 zeros. |
| `divine_sibling` | 36 | `_ i*****edcba` | e.g., `_ (i div 2)edcbazyxwv` | Helps traversing a Merkle tree during authentication path verification. See extended description below. |
| `assert_vector` | 40 | `_` | `_` | Assert equality of `st(i)` to `st(i+5)` for `0 <= i < 4`. Crashes the VM if any pair is unequal. |
| `hash` | 28 | `_jihgfedcba` | `_yxwvu00000` | Overwrites the stack's 10 top-most elements with their hash digest (length 6) and 6 zeros. |
| `divine_sibling` | 32 | `_ i*****edcba` | e.g., `_ (i div 2)edcbazyxwv` | Helps traversing a Merkle tree during authentication path verification. See extended description below. |
| `assert_vector` | 36 | `_` | `_` | Assert equality of `st(i)` to `st(i+5)` for `0 <= i < 4`. Crashes the VM if any pair is unequal. |

The instruction `hash` works as follows.
The stack's 10 top-most elements (`jihgfedcba`) are reversed and concatenated with six zeros, resulting in `abcdefghij000000`.
Expand All @@ -88,18 +88,18 @@ In conjunction with instruction `hash` and `assert_vector`, the instruction `div
|:------------|-------:|:----------------|:---------------------|:--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| `add` | 14 | `_ b a` | `_ c` | Computes the sum (`c`) of the top two elements of the stack (`b` and `a`) over the field. |
| `mul` | 18 | `_ b a` | `_ c` | Computes the product (`c`) of the top two elements of the stack (`b` and `a`) over the field. |
| `invert` | 44 | `_ 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. |
| `split` | 48 | `_ a` | `_ lo hi` | Decomposes the top of the stack into the lower 32 bits and the upper 32 bits. Use with care, preferably through [pseudo instructions](pseudo-instructions.md). |
| `invert` | 40 | `_ 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. |
| `split` | 44 | `_ a` | `_ lo hi` | Decomposes the top of the stack into the lower 32 bits and the upper 32 bits. Use with care, preferably through [pseudo instructions](pseudo-instructions.md). |
| `eq` | 22 | `_ b a` | `_ (a == b)` | Tests the top two stack elements for equality. |
| `lsb` | 52 | `_ a` | `_ (a >> 1) (a % 2)` | Bit-shifts `a` to the right by 1 bit and pushes the least significant bit of `a` to the stack. Use with care, preferably through [pseudo instructions](pseudo-instructions.md). |
| `xxadd` | 56 | `_ z y x b c a` | `_ z y x w v u` | Adds the two extension field elements encoded by field elements `z y x` and `b c a`, overwriting the top-most extension field element with the result. |
| `xxmul` | 60 | `_ z y x b c a` | `_ z y x w v u` | Multiplies the two extension field elements encoded by field elements `z y x` and `b c a`, overwriting the top-most extension field element with the result. |
| `xinvert` | 64 | `_ z y x` | `_ w v u` | Inverts the extension field element encoded by field elements `z y x` in-place. Crashes the VM if the extension field element is 0. |
| `lsb` | 48 | `_ a` | `_ (a >> 1) (a % 2)` | Bit-shifts `a` to the right by 1 bit and pushes the least significant bit of `a` to the stack. Use with care, preferably through [pseudo instructions](pseudo-instructions.md). |
| `xxadd` | 52 | `_ z y x b c a` | `_ z y x w v u` | Adds the two extension field elements encoded by field elements `z y x` and `b c a`, overwriting the top-most extension field element with the result. |
| `xxmul` | 56 | `_ z y x b c a` | `_ z y x w v u` | Multiplies the two extension field elements encoded by field elements `z y x` and `b c a`, overwriting the top-most extension field element with the result. |
| `xinvert` | 60 | `_ z y x` | `_ w v u` | Inverts the extension field element encoded by field elements `z y x` in-place. Crashes the VM if the extension field element is 0. |
| `xbmul` | 26 | `_ z y x a` | `_ w v u` | Scalar multiplication of the extension field element encoded by field elements `z y x` with field element `a`. Overwrites `z y x` with the result. |

## Input/Output

| Instruction | Opcode | old OpStack | new OpStack | Description |
|:------------|-------:|:------------|:------------|:------------------------------------------------------------------------|
| `read_io` | 68 | `_` | `_ a` | Reads a B-Field element from standard input and pushes it to the stack. |
| `read_io` | 64 | `_` | `_ a` | Reads a B-Field element from standard input and pushes it to the stack. |
| `write_io` | 30 | `_ a` | `_` | Pops `a` from the stack and writes it to standard output. |
24 changes: 12 additions & 12 deletions triton-vm/src/instruction.rs
Original file line number Diff line number Diff line change
Expand Up @@ -194,22 +194,22 @@ impl<Dest: PartialEq + Default> AnInstruction<Dest> {
Recurse => 16,
Assert => 10,
Halt => 0,
ReadMem => 24,
WriteMem => 28,
Hash => 32,
DivineSibling => 36,
AssertVector => 40,
ReadMem => 20,
WriteMem => 24,
Hash => 28,
DivineSibling => 32,
AssertVector => 36,
Add => 14,
Mul => 18,
Invert => 44,
Split => 48,
Invert => 40,
Split => 44,
Eq => 22,
Lsb => 52,
XxAdd => 56,
XxMul => 60,
XInvert => 64,
Lsb => 48,
XxAdd => 52,
XxMul => 56,
XInvert => 60,
XbMul => 26,
ReadIo => 68,
ReadIo => 64,
WriteIo => 30,
}
}
Expand Down

0 comments on commit 10064b2

Please sign in to comment.