TritonVM / triton-vm

Triton is a virtual machine that comes with Algebraic Execution Tables (AET) and Arithmetic Intermediate Representations (AIR) for use in combination with a STARK proof system.
https://triton-vm.org
Apache License 2.0
247 stars 37 forks source link

Identify optimal opcodes and instruction grouping. #4

Closed jan-ferdinand closed 2 years ago

jan-ferdinand commented 2 years ago

In order to keep the degree of the AIR polynomials low, we group instructions exhibiting the same behavior in certain aspects, allowing to (de)select for those aspects. This is achieved by decomposing register “current instruction” ci using helper registers “instruction bucket” ib0 through ib5 (or some other, more suitable number of them).

For optimal AIRity, we need to identify

Current groups are described in arithmetization.md, section AIR. They might be improved upon and should definitely be subject of discussions.

Identifying the opcodes should (probably) happen programmatically. Part of this issue is therefor to write a script that computes an instruction's opcode based on its group membership.

(Originally issue number 8 in the internal issue tracker.)

jan-ferdinand commented 2 years ago

(Originally posted by @sshine.)

Identifying the opcodes should (probably) happen programmatically.

I assume you mean identifying the opcode groups numbers. (Their bit masks determine the groups, so same thing.)

This issue reminds me of genetic algorithms for SSA optimization phase ordering, where a meta-heuristic is used to decide the optimal order in which to apply compiler optimizations for a highly optimizing compiler (MLton). Going with such a programmatic approach, I think our problem is simpler, because our input is a proposed grouping of instructions, the evaluation function is the time it takes to evaluate number of multiplications it takes to disambiguate the instructions (the average cost of nullifiers) for a representative set of AIR constraints (e.g. something related to Merkle trees, or a recursive STARK proof), and the mutation is moving some instructions to other groups.

I'm not sure if it's difficult to make a good guess, though.

Either way, being able to compare two groupings would be valuable either if we experiment manually or we decide to automate some of the guessing.

jan-ferdinand commented 2 years ago

Their bit masks determine the groups, so same thing.

Good thing you say this: not necessarily.

The decomposition does not have to be a binary one. The base does not even need to be fixed. Each register ib can have a different maximum value.

jan-ferdinand commented 2 years ago

The decomposition does not have to be a binary one

In a similar vein: the opcodes do not necessarily form a single, continuous range. All we need is an injective mapping from instruction to the B-Field. For example, we are free to chose push = $\frac{1}{2}$ and pop = $\frac{1}{3}$ if it best serves our needs.

jan-ferdinand commented 2 years ago

(Originally posted by @sshine.)

Right now every instruction that takes an argument has an odd opcode, which helps skiz determine whether nia is a one-word or a two-word instruction for its hv0. This isn't documented anywhere, and it is subject to change in the context of this issue.

Either document this choice if we choose to settle on it, or make sure to change how hv0 is constructed for skiz if a better instruction grouping is found that uses a different convention, and document that.

jan-ferdinand commented 2 years ago

Some parts of this issue are now obsolete, others are completed.