From 10064b25a3f5f09e1b4386fa4b6813a1d836c0e4 Mon Sep 17 00:00:00 2001 From: Jan Ferdinand Sauer Date: Fri, 11 Nov 2022 19:45:42 +0100 Subject: [PATCH] add script to derive opcodes automatically, change opcodes slightly --- opcodes.py | 86 +++++++++++++++++++++++++++++++ specification/src/instructions.md | 24 ++++----- triton-vm/src/instruction.rs | 24 ++++----- 3 files changed, 110 insertions(+), 24 deletions(-) create mode 100644 opcodes.py diff --git a/opcodes.py b/opcodes.py new file mode 100644 index 000000000..0912f125b --- /dev/null +++ b/opcodes.py @@ -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() diff --git a/specification/src/instructions.md b/specification/src/instructions.md index 285322ec0..8d7016c31 100644 --- a/specification/src/instructions.md +++ b/specification/src/instructions.md @@ -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`. @@ -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. | diff --git a/triton-vm/src/instruction.rs b/triton-vm/src/instruction.rs index c89410d78..10fbc240f 100644 --- a/triton-vm/src/instruction.rs +++ b/triton-vm/src/instruction.rs @@ -194,22 +194,22 @@ impl AnInstruction { 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, } }