Instruction Set Architecture

Triton VM is a stack machine with RAM. It is a Harvard architecture with read-only memory for the program. The arithmetization of the VM is defined over the B-field ${\mathbb{F}}_p$ where $p$ is the Oxfoi prime, i.e., $2^{64}-2^{32}+1$.¹ This means the registers and memory elements take values from ${\mathbb{F}}_p$, and the transition function gives rise to low-degree transition verification polynomials from the ring of multivariate polynomials over ${\mathbb{F}}_p$.

At certain points in the course of arithmetization we need an extension field over ${\mathbb{F}}_p$ to ensure sufficient soundness. To this end we use ${\mathbb{F}}_{p^3}=\frac{{\mathbb{F}}_p[X]}{⟨X^3-X+1⟩}$, i.e., the quotient ring of remainders of polynomials after division by the Shah polynomial, $X^3-X+1$. We refer to this field as the X-field for short, and its elements as X-field elements.

Instructions have variable width: they either consist of one word, i.e., one B-field element, or of two words, i.e., two B-field elements. An example for a single-word instruction is add, adding the two elements on top of the stack, leaving the result as the new top of the stack. An example for a double-word instruction is push + arg, pushing arg to the stack.

Triton VM has two interfaces for data input, one for public and one for secret data, and one interface for data output, whose data is always public. The public interfaces differ from the private one, especially regarding their arithmetization.

Data Structures

Memory

The term memory refers to a data structure that gives read access (and possibly write access, too) to elements indicated by an address. Regardless of the data structure, the address lives in the B-field. There are four separate notions of memory:

1. Program Memory, from which the VM reads instructions.
2. Op Stack Memory, which stores the operational stack.
3. RAM, to which the VM can read and write field elements.
4. Jump Stack Memory, which stores the entire jump stack.

Program Memory

Program memory holds the instructions of the program currently executed by Triton VM. It is immutable.

Operational Stack

The stack is a last-in;first-out data structure that allows the program to store intermediate variables, pass arguments, and keep pointers to objects held in RAM. In this document, the operational stack is either referred to as just “stack” or, if more clarity is desired, “op stack.”

From the Virtual Machine's point of view, the stack is a single, continuous object. The first 16 elements of the stack can be accessed very conveniently. Elements deeper in the stack require removing some of the higher elements, possibly after storing them in RAM.

For reasons of arithmetization, the stack is actually split into two distinct parts:

1. the operational stack registers st0 through st15, and
2. the Op Stack Underflow Memory.

The motivation and the interplay between the two parts is described and exemplified in arithmetization of the Op Stack table.

Random Access Memory

Triton VM has dedicated Random Access Memory. It can hold up to $p$ many base field elements, where $p$ is the Oxfoi prime¹. Programs can read from and write to RAM using instructions read_mem and write_mem.

The initial RAM is determined by the entity running Triton VM. Populating RAM this way can be beneficial for a program's execution and proving time, especially if substantial amounts of data from the input streams needs to be persisted in RAM. This initialization is one form of secret input, and one of two mechanisms that make Triton VM a non-deterministic virtual machine. The other mechanism is dedicated instructions.

Jump Stack

Another last-in;first-out data structure, similar to the op stack. The jump stack keeps track of return and destination addresses. It changes only when control follows a call or return instruction, and might change through the recurse_or_return instruction. Furthermore, executing instructions return, recurse, and recurse_or_return require a non-empty jump stack.

Registers

This section covers all columns in the Processor Table. Only a subset of these registers relate to the instruction set; the remaining registers exist only to enable an efficient arithmetization and are marked with an asterisk (*).

Instruction

Register ip, the instruction pointer, contains the address of the current instruction in Program Memory. The instruction is contained in the register current instruction, or ci. Register next instruction (or argument), or nia, either contains the next instruction or the argument for the current instruction in ci. For reasons of arithmetization, ci is decomposed, giving rise to the instruction bit registers, labeled ib0 through ib6.

Stack

The stack is represented by 16 registers called stack registers (st0 – st15) plus the op stack underflow memory. The top 16 elements of the op stack are directly accessible, the remainder of the op stack, i.e, the part held in op stack underflow memory, is not. In order to access elements of the op stack held in op stack underflow memory, the stack has to shrink by discarding elements from the top – potentially after writing them to RAM – thus moving lower elements into the stack registers.

The stack grows upwards, in line with the metaphor that justifies the name "stack".

For reasons of arithmetization, the stack always contains a minimum of 16 elements. Trying to run an instruction which would result in a stack of smaller total length than 16 crashes the VM.

Stack elements st0 through st10 are initially 0. Stack elements st11 through st15, i.e., the very bottom of the stack, are initialized with the hash digest of the program that is being executed. See the mechanics of program attestation for further explanations on stack initialization.

The register op_stack_pointer is not directly accessible by the program running in TritonVM. It exists only to allow efficient arithmetization.

Helper Variables

Some instructions require helper variables in order to generate an efficient arithmetization. To this end, there are 6 helper variable registers, labeled hv0 through hv5. These registers are part of the arithmetization of the architecture, but not needed to define the instruction set.

Because they are only needed for some instructions, the helper variables are not generally defined. For instruction group decompose_arg and instructions skiz, split, eq, merkle_step, merkle_step_mem, xx_dot_step, and xb_dot_step, the behavior is defined in the respective sections.

Instructions

Most instructions are contained within a single, parameterless machine word.

Some instructions take a machine word as argument and are so considered double-word instructions. They are recognized by the form “instr + arg”.

Regarding Opcodes

An instruction's operation code, or opcode, is the machine word uniquely identifying the instruction. For reasons of efficient arithmetization, certain properties of the instruction are encoded in the opcode. Concretely, interpreting the field element in standard representation:

• for all double-word instructions, the least significant bit is 1.
• for all instructions shrinking the operational stack, the second-to-least significant bit is 1.
• for all u32 instructions , the third-to-least significant bit is 1.

The first property is used by instruction skiz. The second property helps with proving consistency of the Op Stack. The third property allows efficient arithmetization of the running product for the Permutation Argument between Processor Table and U32 Table.

Op Stack Manipulation

Instruction divine n (together with merkle_step) make Triton a virtual machine that can execute non-deterministic programs. As programs go, this concept is somewhat unusual and benefits from additional explanation. The name of the instruction is the verb (not the adjective) meaning “to discover by intuition or insight.”

From the perspective of the program, the instruction divine n makes some n elements magically appear on the stack. It is not at all specified what those elements are, but generally speaking, they have to be exactly correct, else execution fails. Hence, from the perspective of the program, it just non-deterministically guesses the correct values in a moment of divine clarity.

Looking at the entire system, consisting of the VM, the program, and all inputs – both public and secret – execution is deterministic: the divined values were supplied as and are read from secret input.

Control Flow

The instructions return, recurse, and recurse_or_return require a non-empty jump stack. Should the jump stack be empty, executing any of these instruction causes Triton VM to crash.

Instruction recurse_or_return behaves – surprise! – either like instruction recurse or like instruction return. The (deterministic) decision which behavior to exhibit is made at runtime and depends on stack elements st5 and st6. If st5 != st6, then recurse_or_return acts like instruction recurse, else like return. The instruction is designed to facilitate loops using pointer equality as termination condition and to play nicely with instructions merkle_step and merkle_step_mem.

Memory Access

For the benefit of clarity, the effect of every possible argument is given below.

Hashing

The instruction hash works as follows. The stack's 10 top-most elements (jihgfedcba) are popped from the stack, reversed, and concatenated with six zeros, resulting in abcdefghij000000. The Tip5 permutation is applied to abcdefghij000000, resulting in αβγδεζηθικuvwxyz. The first five elements of this result, i.e., αβγδε, are reversed and pushed to the stack. For example, the old stack was _ jihgfedcba and the new stack is _ εδγβα.

The instructions sponge_init, sponge_absorb, sponge_absorb_mem, and sponge_squeeze are the interface for using the Tip5 permutation in a Sponge construction. The capacity is never accessible to the program that's being executed by Triton VM. At any given time, at most one Sponge state exists. Only instruction sponge_init resets the state of the Sponge, and only the three Sponge instructions influence the Sponge's state. Notably, executing instruction hash does not modify the Sponge's state. When using the Sponge instructions, it is the programmer's responsibility to take care of proper input padding: Triton VM cannot know the number of elements that will be absorbed.

Base Field Arithmetic on Stack

Bitwise Arithmetic on Stack

Extension Field Arithmetic on Stack

Input/Output

Many-In-One

The instruction merkle_step works as follows. The 6th element of the stack i is taken as the node index for a Merkle tree that is claimed to include data whose digest is the content of stack registers st4 through st0, i.e., edcba. The sibling digest of edcba is εδγβα and is read from the input interface of secret data. The least-significant bit of i indicates whether edcba is the digest of a left leaf or a right leaf of the Merkle tree's current level. Depending on this least significant bit of i, merkle_step either

1. (i = 0 mod 2) interprets edcba as the left digest, εδγβα as the right digest, or
2. (i = 1 mod 2) interprets εδγβα as the left digest, edcba as the right digest.

In either case,

1. the left and right digests are hashed, and the resulting digest zyxwv replaces the top of the stack, and
2. 6th register i is shifted by 1 bit to the right, i.e., the least-significant bit is dropped.

Instruction merkle_step_mem works very similarly to instruction merkle_step. The main difference, as the name suggests, is the source of the sibling digest: Instead of reading it from the input interface of secret data, it is supplied via RAM. Stack element st7 is taken as the RAM pointer, holding the memory address at which the next sibling digest is located in RAM. Executing instruction merkle_step_mem increments the memory pointer by the length of one digest, anticipating an authentication path that is laid out continuously. Stack element st6 does not change when executing instruction merkle_step_mem in order to facilitate instruction recurse_or_return.

In conjunction with instructions recurse_or_return and assert_vector, the instructions merkle_step and merkle_step_mem allow efficient verification of a Merkle authentication path. Furthermore, instruction merkle_step_mem allows verifiable re-use of an authentication path. This is necessary, for example, when verifiably updating a Merkle tree: first, the authentication path is used to confirm inclusion of some old leaf, and then to compute the tree's new root from the new leaf.

Arithmetization

An arithmetization defines two things:

1. algebraic execution tables (AETs), and
2. arithmetic intermediate representation (AIR) constraints.

For Triton VM, the execution trace is spread over multiple tables. These tables are linked by various cryptographic arguments. This division allows for a separation of concerns. For example, the main processor's trace is recorded in the Processor Table. The main processor can delegate the execution of somewhat-difficult-to-arithmetize instructions like hash or xor to a co-processor. The arithmetization of the co-processor is largely independent from the main processor and recorded in its separate trace. For example, instructions relating to hashing are executed by the hash co-processor. Its trace is recorded in the Hash Table. Similarly, bitwise instructions are executed by the u32 co-processor, and the corresponding trace recorded in the U32 Table. Another example for the separation of concerns is memory consistency, the bulk of which is delegated to the Operational Stack Table, RAM Table, and Jump Stack Table.

Algebraic Execution Tables

There are 9 Arithmetic Execution Tables in TritonVM. Their relation is described by below figure. A a blue arrow indicates a Permutation Argument, a red arrow indicates an Evaluation Argument, a purple arrow indicates a Lookup Argument, and the green arrow is the Contiguity Argument.

The grayed-out elements “program digest”, “input”, and “output” are not AETs but publicly available information. Together, they constitute the claim for which Triton VM produces a proof. See “Arguments Using Public Information” and “Program Attestation” for the Evaluation Arguments with which they are linked into the rest of the proof system.

Main Tables

The values of all registers, and consequently the elements on the stack, in memory, and so on, are elements of the B-field, i.e., ${\mathbb{F}}_p$ where $p$ is the Oxfoi prime, $2^{64}-2^{32}+1$. All values of columns corresponding to one such register are elements of the B-Field as well. Together, these columns are referred to as table's main columns, and make up the main table.

Auxiliary Tables

The entries of a table's columns corresponding to Permutation, Evaluation, and Lookup Arguments are elements from the X-field ${\mathbb{F}}_{p^3}$. These columns are referred to as a table's auxiliary columns, both because the entries are elements of the X-field and because the entries can only be computed using the main tables, through an auxiliary process. Together, these columns are referred to as a table's auxiliary columns, and make up the auxiliary table.

Padding

For reasons of computational efficiency, it is beneficial that an Algebraic Execution Table's height equals a power of 2. To this end, tables are padded. The height $h$ of the longest AET determines the padded height for all tables, which is $2^{\lceil {\log }_{2}h\rceil }$.

Arithmetic Intermediate Representation

For each table, up to four lists containing constraints of different type are given:

1. Initial Constraints, defining values in a table's first row,
2. Consistency Constraints, establishing consistency within any given row,
3. Transition Constraints, establishing the consistency of two consecutive rows in relation to each other, and
4. Terminal Constraints, defining values in a table's last row.

Together, all these constraints constitute the AIR constraints.

Arguments Using Public Information

Triton VM uses a number of public arguments. That is, one side of the link can be computed by the verifier using publicly available information; the other side of the link is verified through one or more AIR constraints.

The two most prominent instances of this are public input and output: both are given to the verifier explicitly. The verifier can compute the terminal of an Evaluation Argument using public input (respectively, output). In the Processor Table, AIR constraints guarantee that the used input (respectively, output) symbols are accumulated similarly. Comparing the two terminal values establishes that use of public input (respectively, production of public output) was integral.

The third public argument establishes correctness of the Lookup Table, and is explained there. The fourth public argument relates to program attestation, and is also explained on its corresponding page.

Arithmetization Overview

Tables

Constraints

The following table captures the state of affairs in terms of constraints before automatic degree lowering. In particular, automatic degree lowering introduces new columns, modifies the constraint set (in a way that is equivalent to what was there before), and lowers the constraints' maximal degree.

Before automatic degree lowering:

After lowering degree to 8:

After lowering degree to 4:

Triton Assembly Constraint Evaluation

Triton VM's recursive verifier needs to evaluate Triton VM's AIR constraints. In order to gauge the runtime cost for this step, the following table provides estimates for that step's contribution to various tables.

Opcode Pressure

When changing existing or introducing new instructions, one consideration is: how many other instructions compete for opcodes in the same instruction category? The table below helps answer this question at a glance.

Maximum number of opcodes per row is 16.

Program Table

The Program Table contains the entire program as a read-only list of instruction opcodes and their arguments. The processor looks up instructions and arguments using its instruction pointer ip.

For program attestation, the program is padded and sent to the Hash Table in chunks of size 10, which is the $\text{rate}$ of the Tip5 hash function. Program padding is one 1 followed by the minimal number of 0’s necessary to make the padded input length a multiple of the $\text{rate}$¹.

Main Columns

The Program Table consists of 7 main columns. Those columns marked with an asterisk (*) are only used for program attestation.

Auxiliary Columns

A Lookup Argument with the Processor Table establishes that the processor has loaded the correct instruction (and its argument) from program memory. To establish the program memory's side of the Lookup Argument, the Program Table has auxiliary column InstructionLookupServerLogDerivative.

For sending the padded program to the Hash Table, a combination of two Evaluation Arguments is used. The first, PrepareChunkRunningEvaluation, absorbs one chunk of $\text{rate}$ (i.e. 10) instructions at a time, after which it is reset and starts absorbing again. The second, SendChunkRunningEvaluation, absorbs one such prepared chunk every 10 instructions.

Padding

A padding row is a copy of the Program Table's last row with the following modifications:

1. column Address is increased by 1,
2. column Instruction is set to 0,
3. column LookupMultiplicity is set to 0,
4. column IndexInChunk is set to Address mod $\text{rate}$,
5. column MaxMinusIndexInChunkInv is set to the inverse-or-zero of $\text{rate}-1-\text{IndexInChunk}$,
6. column IsHashInputPadding is set to 1, and
7. column IsTablePadding is set to 1.

Above procedure is iterated until the necessary number of rows have been added.

A Note on the Instruction Lookup Argument

For almost all table-linking arguments, the initial row contains the argument's initial value after having applied the first update. For example, the initial row for a Lookup Argument usually contains $\frac{x}{\alpha -y}$ for some $x$ and $y$. As an exception, the Program Table's instruction Lookup Argument always records 0 in the initial row.

Recall that the Lookup Argument is not just about the instruction, but also about the instruction's argument if it has one, or the next instruction if it has none. In the Program Table, this argument (or the next instruction) is recorded in the next row from the instruction in question. Therefore, verifying correct application of the logarithmic derivative's update rule requires access to both the current and the next row.

Out of all constraint types, only Transition Constraints have access to more than one row at a time. This implies that the correct application of the first update of the instruction Lookup Argument cannot be verified by an initial constraint. Therefore, the recorded initial value must be independent of the second row.

Consequently, the final value for the Lookup Argument is recorded in the first row just after the program description ends. This row is guaranteed to exist because of the mechanics for program attestation: the program has to be padded with at least one 1 before it is hashed.

Arithmetic Intermediate Representation

Let all household items (🪥, 🛁, etc.) be challenges, concretely evaluation points, supplied by the verifier. Let all fruit & vegetables (🥝, 🥥, etc.) be challenges, concretely weights to compress rows, supplied by the verifier. Both types of challenges are X-field elements, i.e., elements of ${\mathbb{F}}_{p^3}$.

Initial Constraints

1. The Address is 0.
2. The IndexInChunk is 0.
3. The indicator IsHashInputPadding is 0.
4. The InstructionLookupServerLogDerivative is 0.
5. PrepareChunkRunningEvaluation has absorbed Instruction with respect to challenge 🪑.
6. SendChunkRunningEvaluation is 1.

Initial Constraints as Polynomials

1. Address
2. IndexInChunk
3. IsHashInputPadding
4. InstructionLookupServerLogDerivative
5. PrepareChunkRunningEvaluation - 🪑 - Instruction
6. SendChunkRunningEvaluation - 1

Consistency Constraints

1. The MaxMinusIndexInChunkInv is zero or the inverse of $\text{rate}-1-$ IndexInChunk.
2. The IndexInChunk is $\text{rate}-1$ or the MaxMinusIndexInChunkInv is the inverse of $\text{rate}-1-$ IndexInChunk.
3. Indicator IsHashInputPadding is either 0 or 1.
4. Indicator IsTablePadding is either 0 or 1.

Consistency Constraints as Polynomials

1. (1 - MaxMinusIndexInChunkInv · (rate - 1 - IndexInChunk)) · MaxMinusIndexInChunkInv
2. (1 - MaxMinusIndexInChunkInv · (rate - 1 - IndexInChunk)) · (rate - 1 - IndexInChunk)
3. IsHashInputPadding · (IsHashInputPadding - 1)
4. IsTablePadding · (IsTablePadding - 1)

Transition Constraints

1. The Address increases by 1.
2. If the IndexInChunk is not $\text{rate}-1$, it increases by 1. Else, the IndexInChunk in the next row is 0.
3. The indicator IsHashInputPadding is 0 or remains unchanged.
4. The padding indicator IsTablePadding is 0 or remains unchanged.
5. If IsHashInputPadding is 0 in the current row and 1 in the next row, then Instruction in the next row is 1.
6. If IsHashInputPadding is 1 in the current row then Instruction in the next row is 0.
7. If IsHashInputPadding is 1 in the current row and IndexInChunk is $\text{rate}-1$ in the current row then IsTablePadding is 1 in the next row.
8. If the current row is not a padding row, the logarithmic derivative accumulates the current row's address, the current row's instruction, and the next row's instruction with respect to challenges 🥝, 🥥, and 🫐 and indeterminate 🪥 respectively. Otherwise, it remains unchanged.
9. If the IndexInChunk in the current row is not $\text{rate}-1$, then PrepareChunkRunningEvaluation absorbs the Instruction in the next row with respect to challenge 🪑. Otherwise, PrepareChunkRunningEvaluation resets and absorbs the Instruction in the next row with respect to challenge 🪑.
10. If the next row is not a padding row and the IndexInChunk in the next row is $\text{rate}-1$, then SendChunkRunningEvaluation absorbs PrepareChunkRunningEvaluation in the next row with respect to variable 🪣. Otherwise, it remains unchanged.

Transition Constraints as Polynomials

1. Address' - Address - 1
2. MaxMinusIndexInChunkInv · (IndexInChunk' - IndexInChunk - 1)
+ (1 - MaxMinusIndexInChunkInv · (rate - 1 - IndexInChunk)) · IndexInChunk'
3. IsHashInputPadding · (IsHashInputPadding' - IsHashInputPadding)
4. IsTablePadding · (IsTablePadding' - IsTablePadding)
5. (IsHashInputPadding - 1) · IsHashInputPadding' · (Instruction' - 1)
6. IsHashInputPadding · Instruction'
7. IsHashInputPadding · (1 - MaxMinusIndexInChunkInv · (rate - 1 - IndexInChunk)) · IsTablePadding'
8. (1 - IsHashInputPadding) · ((InstructionLookupServerLogDerivative' - InstructionLookupServerLogDerivative) · (🪥 - 🥝·Address - 🥥·Instruction - 🫐·Instruction') - LookupMultiplicity)
+ IsHashInputPadding · (InstructionLookupServerLogDerivative' - InstructionLookupServerLogDerivative)
9. (rate - 1 - IndexInChunk) · (PrepareChunkRunningEvaluation' - 🪑·PrepareChunkRunningEvaluation - Instruction')
+ (1 - MaxMinusIndexInChunkInv · (rate - 1 - IndexInChunk)) · (PrepareChunkRunningEvaluation' - 🪑 - Instruction')
10. (IsTablePadding' - 1) · (1 - MaxMinusIndexInChunkInv' · (rate - 1 - IndexInChunk')) · (SendChunkRunningEvaluation' - 🪣·SendChunkRunningEvaluation - PrepareChunkRunningEvaluation')
+ (SendChunkRunningEvaluation' - SendChunkRunningEvaluation) · IsTablePadding'
+ (SendChunkRunningEvaluation' - SendChunkRunningEvaluation) · (rate - 1 - IndexInChunk')
    

Terminal Constraints

1. The indicator IsHashInputPadding is 1.
2. The IndexInChunk is $\text{rate}-1$ or the indicator IsTablePadding is 1.

Terminal Constraints as Polynomials

1. IsHashInputPadding - 1
2. (rate - 1 - IndexInChunk) · (IsTablePadding - 1)

Processor Table

The Processor Table records all of Triton VM states during execution of a particular program. The states are recorded in chronological order. The first row is the initial state, the last (non-padding) row is the terminal state, i.e., the state after having executed instruction halt. It is impossible to generate a valid proof if the instruction executed last is anything but halt.

It is worth highlighting the initialization of the operational stack. Stack elements st0 through st10 are initially 0. However, stack elements st11 through st15, i.e., the very bottom of the stack, are initialized with the hash digest of the program that is being executed. This is primarily useful for recursive verifiers: they can compare their own program digest to the program digest of the proof they are verifying. This way, a recursive verifier can easily determine if they are actually recursing, or whether the proof they are checking was generated using an entirely different program. A more detailed explanation of the mechanics can be found on the page about program attestation.

Main Columns

The processor consists of all registers defined in the Instruction Set Architecture. Each register is assigned a column in the processor table.

Auxiliary Columns

The Processor Table has the following auxiliary columns, corresponding to Evaluation Arguments, Permutation Arguments, and Lookup Arguments:

1. RunningEvaluationStandardInput for the Evaluation Argument with the input symbols.
2. RunningEvaluationStandardOutput for the Evaluation Argument with the output symbols.
3. InstructionLookupClientLogDerivative for the Lookup Argument with the Program Table
4. RunningProductOpStackTable for the Permutation Argument with the Op Stack Table.
5. RunningProductRamTable for the Permutation Argument with the RAM Table. Note that virtual column instruction_type holds value 1 for reads and 0 for writes.
6. RunningProductJumpStackTable for the Permutation Argument with the Jump Stack Table.
7. RunningEvaluationHashInput for the Evaluation Argument with the Hash Table for copying the input to the hash function from the processor to the hash coprocessor.
8. RunningEvaluationHashDigest for the Evaluation Argument with the Hash Table for copying the hash digest from the hash coprocessor to the processor.
9. RunningEvaluationSponge for the Evaluation Argument with the Hash Table for copying the 10 next to-be-absorbed elements from the processor to the hash coprocessor or the 10 next squeezed elements from the hash coprocessor to the processor, depending on the instruction.
10. U32LookupClientLogDerivative for the Lookup Argument with the U32 Table.
11. ClockJumpDifferenceLookupServerLogDerivative for the Lookup Argument of clock jump differences with the Op Stack Table, the RAM Table, and the Jump Stack Table.

Permutation Argument with the Op Stack Table

The subset Permutation Argument with the Op Stack Table RunningProductOpStackTable establishes consistency of the op stack underflow memory. The number of factors incorporated into the running product at any given cycle depends on the executed instruction in this cycle: for every element pushed to or popped from the stack, there is one factor. Namely, if the op stack grows, every element spilling from st15 into op stack underflow memory will be incorporated as one factor; and if the op stack shrinks, every element from op stack underflow memory being transferred into st15 will be one factor.

Notably, if an instruction shrinks the op stack by more than one element in a single clock cycle, each spilled element is incorporated as one factor. The same holds true for instructions growing the op stack by more than one element in a single clock cycle.

One key insight for this Permutation Argument is that the processor will always have access to the elements that are to be read from or written to underflow memory: if the instruction grows the op stack, then the elements in question currently reside in the directly accessible, top part of the stack; if the instruction shrinks the op stack, then the elements in question will be in the top part of the stack in the next cycle. In either case, the Transition Constraint for the Permutation Argument can incorporate the explicitly listed elements as well as the corresponding trivial-to-compute op_stack_pointer.

Padding

A padding row is a copy of the Processor Table's last row with the following modifications:

1. column clk is increased by 1,
2. column IsPadding is set to 1,
3. column cjd_mul is set to 0,

A notable exception: if the row with clk equal to 1 is a padding row, then the value of cjd_mul is not constrained in that row. The reason for this exception is the lack of “awareness” of padding rows in the Jump Stack Table: it keeps looking up clock jump differences in its padding section. All these clock jumps are guaranteed to have magnitude 1.

Arithmetic Intermediate Representation

Let all household items (🪥, 🛁, etc.) be challenges, concretely evaluation points, supplied by the verifier. Let all fruit & vegetables (🥝, 🥥, etc.) be challenges, concretely weights to compress rows, supplied by the verifier. Both types of challenges are X-field elements, i.e., elements of ${\mathbb{F}}_{p^3}$.

Note, that the transition constraint's use of some_column vs some_column_next might be a little unintuitive. For example, take the following part of some execution trace.

In order to verify the correctness of RunningEvaluationHashInput, the corresponding transition constraint needs to conditionally “activate” on row-tuple ($i-1$, $i$), where it is conditional on ci_next (not ci), and verifies absorption of the next row, i.e., row $i$. However, in order to verify the correctness of RunningEvaluationHashDigest, the corresponding transition constraint needs to conditionally “activate” on row-tuple ($i$, $i+1$), where it is conditional on ci (not ci_next), and verifies absorption of the next row, i.e., row $i+1$.

Initial Constraints

1. The cycle counter clk is 0.
2. The instruction pointer ip is 0.
3. The jump address stack pointer jsp is 0.
4. The jump address origin jso is 0.
5. The jump address destination jsd is 0.
6. The operational stack element st0 is 0.
7. The operational stack element st1 is 0.
8. The operational stack element st2 is 0.
9. The operational stack element st3 is 0.
10. The operational stack element st4 is 0.
11. The operational stack element st5 is 0.
12. The operational stack element st6 is 0.
13. The operational stack element st7 is 0.
14. The operational stack element st8 is 0.
15. The operational stack element st9 is 0.
16. The operational stack element st10 is 0.
17. The Evaluation Argument of operational stack elements st11 through st15 with respect to indeterminate 🥬 equals the public part of program digest challenge, 🫑. See program attestation for more details.
18. The op_stack_pointer is 16.
19. RunningEvaluationStandardInput is 1.
20. RunningEvaluationStandardOutput is 1.
21. InstructionLookupClientLogDerivative has absorbed the first row with respect to challenges 🥝, 🥥, and 🫐 and indeterminate 🪥.
22. RunningProductOpStackTable is 1.
23. RunningProductRamTable has absorbed the first row with respect to challenges 🍍, 🍈, 🍎, and 🌽 and indeterminate 🛋.
24. RunningProductJumpStackTable has absorbed the first row with respect to challenges 🍇, 🍅, 🍌, 🍏, and 🍐 and indeterminate 🧴.
25. RunningEvaluationHashInput has absorbed the first row with respect to challenges 🧄₀ through 🧄₉ and indeterminate 🚪 if the current instruction is hash. Otherwise, it is 1.
26. RunningEvaluationHashDigest is 1.
27. RunningEvaluationSponge is 1.
28. U32LookupClientLogDerivative is 0.
29. ClockJumpDifferenceLookupServerLogDerivative starts having accumulated the first contribution.

Consistency Constraints

1. The composition of instruction bits ib0 through ib6 corresponds to the current instruction ci.
2. The instruction bit ib0 is a bit.
3. The instruction bit ib1 is a bit.
4. The instruction bit ib2 is a bit.
5. The instruction bit ib3 is a bit.
6. The instruction bit ib4 is a bit.
7. The instruction bit ib5 is a bit.
8. The instruction bit ib6 is a bit.
9. The padding indicator IsPadding is either 0 or 1.
10. If the current padding row is a padding row and clk is not 1, then the clock jump difference lookup multiplicity is 0.

Transition Constraints

Due to their complexity, instruction-specific constraints are defined in their own section. The following additional constraints also apply to every pair of rows.

1. The cycle counter clk increases by 1.
2. The padding indicator IsPadding is 0 or remains unchanged.
3. If the next row is not a padding row, the logarithmic derivative for the Program Table absorbs the next row with respect to challenges 🥝, 🥥, and 🫐 and indeterminate 🪥. Otherwise, it remains unchanged.
4. The running sum for the logarithmic derivative of the clock jump difference lookup argument accumulates the next row's clk with the appropriate multiplicity cjd_mul with respect to indeterminate 🪞.
5. The running product for the Jump Stack Table absorbs the next row with respect to challenges 🍇, 🍅, 🍌, 🍏, and 🍐 and indeterminate 🧴.
6. 1. If the current instruction in the next row is hash, the running evaluation “Hash Input” absorbs the next row with respect to challenges 🧄₀ through 🧄₉ and indeterminate 🚪.
   2. If the current instruction in the next row is merkle_step or merkle_step_mem and helper variable hv5…
      1. …is 0, the running evaluation “Hash Input” absorbs next row's st0 through st4 and hv0 through hv4…
      2. …is 1, the running evaluation “Hash Input” absorbs next row's hv0 through hv4 and st0 through st4…
         …with respect to challenges 🧄₀ through 🧄₉ and indeterminate 🚪.
   3. Otherwise, it remains unchanged.
7. If the current instruction is hash, merkle_step, or merkle_step_mem, the running evaluation “Hash Digest” absorbs the next row with respect to challenges 🧄₀ through 🧄₄ and indeterminate 🪟. Otherwise, it remains unchanged.
8. If the current instruction is sponge_init, then the running evaluation “Sponge” absorbs the current instruction and the Sponge's default initial state with respect to challenges 🧅 and 🧄₀ through 🧄₉ and indeterminate 🧽. Else if the current instruction is sponge_absorb, then the running evaluation “Sponge” absorbs the current instruction and the current row with respect to challenges 🧅 and 🧄₀ through 🧄₉ and indeterminate 🧽. Else if the current instruction is sponge_squeeze, then the running evaluation “Sponge” absorbs the current instruction and the next row with respect to challenges 🧅 and 🧄₀ through 🧄₉ and indeterminate 🧽. Else if the current instruction is sponge_absorb_mem, then the running evaluation “Sponge” absorbs the opcode of instruction sponge_absorb and stack elements st1 through st4 and all 6 helper variables with respect to challenges 🧅 and 🧄₀ through 🧄₉ and indeterminate 🧽. Otherwise, the running evaluation remains unchanged.
9. 1. If the current instruction is split, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates st0 and st1 in the next row and ci in the current row with respect to challenges 🥜, 🌰, and 🥑, and indeterminate 🧷.
   2. If the current instruction is lt, and, xor, or pow, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates st0, st1, and ci in the current row and st0 in the next row with respect to challenges 🥜, 🌰, 🥑, and 🥕, and indeterminate 🧷.
   3. If the current instruction is log_2_floor, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates st0 and ci in the current row and st0 in the next row with respect to challenges 🥜, 🥑, and 🥕, and indeterminate 🧷.
   4. If the current instruction is div_mod, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates both
      1. st0 in the next row and st1 in the current row as well as the constants opcode(lt) and 1 with respect to challenges 🥜, 🌰, 🥑, and 🥕, and indeterminate 🧷.
      2. st0 in the current row and st1 in the next row as well as opcode(split) with respect to challenges 🥜, 🌰, and 🥑, and indeterminate 🧷.
   5. If the current instruction is merkle_step or merkle_step_mem, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates st5 from the current and next rows as well as opcode(split) with respect to challenges 🥜, 🌰, and 🥑, and indeterminate 🧷.
   6. If the current instruction is pop_count, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates st0 and ci in the current row and st0 in the next row with respect to challenges 🥜, 🥑, and 🥕, and indeterminate 🧷.
   7. Else, i.e., if the current instruction is not a u32 instruction, the logarithmic derivative for the Lookup Argument with the U32 Table remains unchanged.

Terminal Constraints

1. In the last row, register “current instruction” ci is 0, corresponding to instruction halt.

Instruction Groups

Some transition constraints are shared across some, or even many instructions. For example, most instructions must not change the jump stack. Likewise, most instructions must not change RAM. To simplify presentation of the instruction-specific transition constraints, these common constraints are grouped together and aliased. Continuing above example, instruction group keep_jump_stack contains all transition constraints to ensure that the jump stack remains unchanged.

The next section treats each instruction group in detail. The following table lists and briefly explains all instruction groups.

The following instruction groups conceptually fit the category of 'instruction groups' but are not used or enforced through AIR constraints.

A summary of all instructions and which groups they are part of is given in the following table.

Indicator Polynomials ind_i(hv3, hv2, hv1, hv0)

In this and the following sections, a register marked with a ' refers to the next state of that register. For example, st0' = st0 + 2 means that stack register st0 is incremented by 2. An alternative view for the same concept is that registers marked with ' are those of the next row in the table.

For instructions like dup i, swap i, pop n, et cetera, it is beneficial to have polynomials that evaluate to 1 if the instruction's argument is a specific value, and to 0 otherwise. This allows indicating which registers are constraint, and in which way they are, depending on the argument. This is the purpose of the indicator polynomials ind_i. Evaluated on the binary decomposition of i, they show the behavior described above.

For example, take i = 13. The corresponding binary decomposition is (hv3, hv2, hv1, hv0) = (1, 1, 0, 1). Indicator polynomial ind_13(hv3, hv2, hv1, hv0) is defined as hv3·hv2·(1 - hv1)·hv0. It evaluates to 1 on (1, 1, 0, 1), i.e., ind_13(1, 1, 0, 1) = 1. Any other indicator polynomial, like ind_7, evaluates to 0 on (1, 1, 0, 1). Likewise, the indicator polynomial for 13 evaluates to 0 for any other argument.

The list of all 16 indicator polynomials is:

0. ind_0(hv3, hv2, hv1, hv0) = (1 - hv3)·(1 - hv2)·(1 - hv1)·(1 - hv0)
1. ind_1(hv3, hv2, hv1, hv0) = (1 - hv3)·(1 - hv2)·(1 - hv1)·hv0
2. ind_2(hv3, hv2, hv1, hv0) = (1 - hv3)·(1 - hv2)·hv1·(1 - hv0)
3. ind_3(hv3, hv2, hv1, hv0) = (1 - hv3)·(1 - hv2)·hv1·hv0
4. ind_4(hv3, hv2, hv1, hv0) = (1 - hv3)·hv2·(1 - hv1)·(1 - hv0)
5. ind_5(hv3, hv2, hv1, hv0) = (1 - hv3)·hv2·(1 - hv1)·hv0
6. ind_6(hv3, hv2, hv1, hv0) = (1 - hv3)·hv2·hv1·(1 - hv0)
7. ind_7(hv3, hv2, hv1, hv0) = (1 - hv3)·hv2·hv1·hv0
8. ind_8(hv3, hv2, hv1, hv0) = hv3·(1 - hv2)·(1 - hv1)·(1 - hv0)
9. ind_9(hv3, hv2, hv1, hv0) = hv3·(1 - hv2)·(1 - hv1)·hv0
10. ind_10(hv3, hv2, hv1, hv0) = hv3·(1 - hv2)·hv1·(1 - hv0)
11. ind_11(hv3, hv2, hv1, hv0) = hv3·(1 - hv2)·hv1·hv0
12. ind_12(hv3, hv2, hv1, hv0) = hv3·hv2·(1 - hv1)·(1 - hv0)
13. ind_13(hv3, hv2, hv1, hv0) = hv3·hv2·(1 - hv1)·hv0
14. ind_14(hv3, hv2, hv1, hv0) = hv3·hv2·hv1·(1 - hv0)
15. ind_15(hv3, hv2, hv1, hv0) = hv3·hv2·hv1·hv0

Group decompose_arg

Description

1. The helper variables hv0 through hv3 are the binary decomposition of the instruction's argument, which is held in register nia.
2. The helper variable hv0 is either 0 or 1.
3. The helper variable hv1 is either 0 or 1.
4. The helper variable hv2 is either 0 or 1.
5. The helper variable hv3 is either 0 or 1.

Polynomials

1. nia - (8·hv3 + 4·hv2 + 2·hv1 + hv0)
2. hv0·(hv0 - 1)
3. hv1·(hv1 - 1)
4. hv2·(hv2 - 1)
5. hv3·(hv3 - 1)

Group prohibit_illegal_num_words

Is only ever used in combination with instruction group decompose_arg. Therefore, the instruction argument's correct binary decomposition is known to be in helper variables hv0 through hv3.

Description

1. The argument is not 0.
2. The argument is not 6.
3. The argument is not 7.
4. The argument is not 8.
5. The argument is not 9.
6. The argument is not 10.
7. The argument is not 11.
8. The argument is not 12.
9. The argument is not 13.
10. The argument is not 14.
11. The argument is not 15.

Polynomials

1. ind_0(hv3, hv2, hv1, hv0)
2. ind_6(hv3, hv2, hv1, hv0)
3. ind_7(hv3, hv2, hv1, hv0)
4. ind_8(hv3, hv2, hv1, hv0)
5. ind_9(hv3, hv2, hv1, hv0)
6. ind_10(hv3, hv2, hv1, hv0)
7. ind_11(hv3, hv2, hv1, hv0)
8. ind_12(hv3, hv2, hv1, hv0)
9. ind_13(hv3, hv2, hv1, hv0)
10. ind_14(hv3, hv2, hv1, hv0)
11. ind_15(hv3, hv2, hv1, hv0)

Group no_io

Description

1. The running evaluation for standard input remains unchanged.
2. The running evaluation for standard output remains unchanged.

Polynomials

1. RunningEvaluationStandardInput' - RunningEvaluationStandardInput
2. RunningEvaluationStandardOutput' - RunningEvaluationStandardOutput

Group no_ram

Description

1. The running product for the Permutation Argument with the RAM table does not change.

Polynomials

1. RunningProductRamTable' - RunningProductRamTable

Group keep_jump_stack

Description

1. The jump stack pointer jsp does not change.
2. The jump stack origin jso does not change.
3. The jump stack destination jsd does not change.

Polynomials

1. jsp' - jsp
2. jso' - jso
3. jsd' - jsd

Group step_1

Contains all constraints from instruction group keep_jump_stack, and additionally:

Description

1. The instruction pointer increments by 1.

Polynomials

1. ip' - (ip + 1)

Group step_2

Contains all constraints from instruction group keep_jump_stack, and additionally:

Description

1. The instruction pointer increments by 2.

Polynomials

1. ip' - (ip + 2)

Group grow_op_stack

Description

1. The stack element in st0 is moved into st1.
2. The stack element in st1 is moved into st2.
3. The stack element in st2 is moved into st3.
4. The stack element in st3 is moved into st4.
5. The stack element in st4 is moved into st5.
6. The stack element in st5 is moved into st6.
7. The stack element in st6 is moved into st7.
8. The stack element in st7 is moved into st8.
9. The stack element in st8 is moved into st9.
10. The stack element in st9 is moved into st10.
11. The stack element in st10 is moved into st11.
12. The stack element in st11 is moved into st12.
13. The stack element in st12 is moved into st13.
14. The stack element in st13 is moved into st14.
15. The stack element in st14 is moved into st15.
16. The op stack pointer is incremented by 1.
17. The running product for the Op Stack Table absorbs the current row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤.

Polynomials

1. st1' - st0
2. st2' - st1
3. st3' - st2
4. st4' - st3
5. st5' - st4
6. st6' - st5
7. st7' - st6
8. st8' - st7
9. st9' - st8
10. st10' - st9
11. st11' - st10
12. st12' - st11
13. st13' - st12
14. st14' - st13
15. st15' - st14
16. op_stack_pointer' - (op_stack_pointer + 1)
17. RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊·ib1 - 🍉·op_stack_pointer - 🫒·st15)

Group grow_op_stack_by_any_of

Is only ever used in combination with instruction group decompose_arg. Therefore, the instruction's argument n correct binary decomposition is known to be in helper variables hv0 through hv3.

Description

1. If n is 1, then st0 is moved into st1
   else if n is 2, then st0 is moved into st2
   else if n is 3, then st0 is moved into st3
   else if n is 4, then st0 is moved into st4
   else if n is 5, then st0 is moved into st5.
2. If n is 1, then st1 is moved into st2
   else if n is 2, then st1 is moved into st3
   else if n is 3, then st1 is moved into st4
   else if n is 4, then st1 is moved into st5
   else if n is 5, then st1 is moved into st6.
3. If n is 1, then st2 is moved into st3
   else if n is 2, then st2 is moved into st4
   else if n is 3, then st2 is moved into st5
   else if n is 4, then st2 is moved into st6
   else if n is 5, then st2 is moved into st7.
4. If n is 1, then st3 is moved into st4
   else if n is 2, then st3 is moved into st5
   else if n is 3, then st3 is moved into st6
   else if n is 4, then st3 is moved into st7
   else if n is 5, then st3 is moved into st8.
5. If n is 1, then st4 is moved into st5
   else if n is 2, then st4 is moved into st6
   else if n is 3, then st4 is moved into st7
   else if n is 4, then st4 is moved into st8
   else if n is 5, then st4 is moved into st9.
6. If n is 1, then st5 is moved into st6
   else if n is 2, then st5 is moved into st7
   else if n is 3, then st5 is moved into st8
   else if n is 4, then st5 is moved into st9
   else if n is 5, then st5 is moved into st10.
7. If n is 1, then st6 is moved into st7
   else if n is 2, then st6 is moved into st8
   else if n is 3, then st6 is moved into st9
   else if n is 4, then st6 is moved into st10
   else if n is 5, then st6 is moved into st11.
8. If n is 1, then st7 is moved into st8
   else if n is 2, then st7 is moved into st9
   else if n is 3, then st7 is moved into st10
   else if n is 4, then st7 is moved into st11
   else if n is 5, then st7 is moved into st12.
9. If n is 1, then st8 is moved into st9
   else if n is 2, then st8 is moved into st10
   else if n is 3, then st8 is moved into st11
   else if n is 4, then st8 is moved into st12
   else if n is 5, then st8 is moved into st13.
10. If n is 1, then st9 is moved into st10
    else if n is 2, then st9 is moved into st11
    else if n is 3, then st9 is moved into st12
    else if n is 4, then st9 is moved into st13
    else if n is 5, then st9 is moved into st14.
11. If n is 1, then st10 is moved into st11
    else if n is 2, then st10 is moved into st12
    else if n is 3, then st10 is moved into st13
    else if n is 4, then st10 is moved into st14
    else if n is 5, then st10 is moved into st15.
12. If n is 1, then st11 is moved into st12
    else if n is 2, then st11 is moved into st13
    else if n is 3, then st11 is moved into st14
    else if n is 4, then st11 is moved into st15
    else if n is 5, then the op stack pointer grows by 5.
13. If n is 1, then st12 is moved into st13
    else if n is 2, then st12 is moved into st14
    else if n is 3, then st12 is moved into st15
    else if n is 4, then the op stack pointer grows by 4
    else if n is 5, then the running product with the Op Stack Table accumulates st11 through st15.
14. If n is 1, then st13 is moved into st14
    else if n is 2, then st13 is moved into st15
    else if n is 3, then the op stack pointer grows by 3
    else if n is 4, then the running product with the Op Stack Table accumulates st12 through st15.
15. If n is 1, then st14 is moved into st15
    else if n is 2, then the op stack pointer grows by 2
    else if n is 3, then the running product with the Op Stack Table accumulates st13 through st15.
16. If n is 1, then the op stack pointer grows by 1
    else if n is 2, then the running product with the Op Stack Table accumulates st14 and st15.
17. If n is 1, then the running product with the Op Stack Table accumulates st15.

Group keep_op_stack_height

The op stack pointer and the running product for the Permutation Argument with the Op Stack Table remain the same. In other words, there is no access (neither read nor write) from/to the Op Stack Table.

Description

1. The op stack pointer does not change.
2. The running product for the Op Stack Table remains unchanged.

Polynomials

1. op_stack_pointer' - op_stack_pointer
2. RunningProductOpStackTable' - RunningProductOpStackTable

Group op_stack_remains_except_top_n_elements_unconstrained

Contains all constraints from group keep_op_stack_height, and additionally ensures that all but the top n op stack elements remain the same. (The top n elements are unconstrained.)

Description

1. For i in {n, ..., NUM_OP_STACK_REGISTERS-1} The stack element in sti does not change.

Polynomials

1. stn' - stn
2. ...
3. stN' - stN

Group keep_op_stack

Short-hand for op_stack_remains_except_top_n_elements_unconstrained with n=0.

Group binary_operation

Description

1. The stack element in st2 is moved into st1.
2. The stack element in st3 is moved into st2.
3. The stack element in st4 is moved into st3.
4. The stack element in st5 is moved into st4.
5. The stack element in st6 is moved into st5.
6. The stack element in st7 is moved into st6.
7. The stack element in st8 is moved into st7.
8. The stack element in st9 is moved into st8.
9. The stack element in st10 is moved into st9.
10. The stack element in st11 is moved into st10.
11. The stack element in st12 is moved into st11.
12. The stack element in st13 is moved into st12.
13. The stack element in st14 is moved into st13.
14. The stack element in st15 is moved into st14.
15. The op stack pointer is decremented by 1.
16. The running product for the Op Stack Table absorbs clock cycle and instruction bit 1 from the current row as well as op stack pointer and stack element 15 from the next row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤.

Polynomials

1. st1' - st2
2. st2' - st3
3. st3' - st4
4. st4' - st5
5. st5' - st6
6. st6' - st7
7. st7' - st8
8. st8' - st9
9. st9' - st10
10. st10' - st11
11. st11' - st12
12. st12' - st13
13. st13' - st14
14. st14' - st15
15. op_stack_pointer' - (op_stack_pointer - 1)
16. RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊·ib1 - 🍉·op_stack_pointer' - 🫒·st15')

Group shrink_op_stack

Contains all constraints from instruction group binary_operation, and additionally:

Description

1. The stack element in st1 is moved into st0.

Polynomials

1. st0' - st1

Group shrink_op_stack_by_any_of

Is only ever used in combination with instruction group decompose_arg. Therefore, the instruction's argument n correct binary decomposition is known to be in helper variables hv0 through hv3.

Description

1. If n is 1, then st1 is moved into st0
   else if n is 2, then st2 is moved into st0
   else if n is 3, then st3 is moved into st0
   else if n is 4, then st4 is moved into st0
   else if n is 5, then st5 is moved into st0.
2. If n is 1, then st2 is moved into st1
   else if n is 2, then st3 is moved into st1
   else if n is 3, then st4 is moved into st1
   else if n is 4, then st5 is moved into st1
   else if n is 5, then st6 is moved into st1.
3. If n is 1, then st3 is moved into st2
   else if n is 2, then st4 is moved into st2
   else if n is 3, then st5 is moved into st2
   else if n is 4, then st6 is moved into st2
   else if n is 5, then st7 is moved into st2.
4. If n is 1, then st4 is moved into st3
   else if n is 2, then st5 is moved into st3
   else if n is 3, then st6 is moved into st3
   else if n is 4, then st7 is moved into st3
   else if n is 5, then st8 is moved into st3.
5. If n is 1, then st5 is moved into st4
   else if n is 2, then st6 is moved into st4
   else if n is 3, then st7 is moved into st4
   else if n is 4, then st8 is moved into st4
   else if n is 5, then st9 is moved into st4.
6. If n is 1, then st6 is moved into st5
   else if n is 2, then st7 is moved into st5
   else if n is 3, then st8 is moved into st5
   else if n is 4, then st9 is moved into st5
   else if n is 5, then st10 is moved into st5.
7. If n is 1, then st7 is moved into st6
   else if n is 2, then st8 is moved into st6
   else if n is 3, then st9 is moved into st6
   else if n is 4, then st10 is moved into st6
   else if n is 5, then st11 is moved into st6.
8. If n is 1, then st8 is moved into st7
   else if n is 2, then st9 is moved into st7
   else if n is 3, then st10 is moved into st7
   else if n is 4, then st11 is moved into st7
   else if n is 5, then st12 is moved into st7.
9. If n is 1, then st9 is moved into st8
   else if n is 2, then st10 is moved into st8
   else if n is 3, then st11 is moved into st8
   else if n is 4, then st12 is moved into st8
   else if n is 5, then st13 is moved into st8.
10. If n is 1, then st10 is moved into st9
    else if n is 2, then st11 is moved into st9
    else if n is 3, then st12 is moved into st9
    else if n is 4, then st13 is moved into st9
    else if n is 5, then st14 is moved into st9.
11. If n is 1, then st11 is moved into st10
    else if n is 2, then st12 is moved into st10
    else if n is 3, then st13 is moved into st10
    else if n is 4, then st14 is moved into st10
    else if n is 5, then st15 is moved into st10.
12. If n is 1, then st12 is moved into st11
    else if n is 2, then st13 is moved into st11
    else if n is 3, then st14 is moved into st11
    else if n is 4, then st15 is moved into st11
    else if n is 5, then the op stack pointer shrinks by 5.
13. If n is 1, then st13 is moved into st12
    else if n is 2, then st14 is moved into st12
    else if n is 3, then st15 is moved into st12
    else if n is 4, then the op stack pointer shrinks by 4
    else if n is 5, then the running product with the Op Stack Table accumulates next row's st11 through st15.
14. If n is 1, then st14 is moved into st13
    else if n is 2, then st15 is moved into st13
    else if n is 3, then the op stack pointer shrinks by 3
    else if n is 4, then the running product with the Op Stack Table accumulates next row's st12 through st15.
15. If n is 1, then st15 is moved into st14
    else if n is 2, then the op stack pointer shrinks by 2
    else if n is 3, then the running product with the Op Stack Table accumulates next row's st13 through st15.
16. If n is 1, then the op stack pointer shrinks by 1
    else if n is 2, then the running product with the Op Stack Table accumulates next row's st14 and st15.
17. If n is 1, then the running product with the Op Stack Table accumulates next row's st15.

Instruction-Specific Transition Constraints

Instruction pop + n

This instruction is fully constrained by its instruction groups

Instruction push + a

In addition to its instruction groups, this instruction has the following constraints.

Description

1. The instruction's argument a is moved onto the stack.

Polynomials

1. st0' - nia

Instruction divine + n

This instruction is fully constrained by its instruction groups

Instruction pick + i

This instruction makes use of indicator polynomials. In addition to its instruction groups, this instruction has the following constraints.

Description

For 0 ⩽ i < 16:

1. Stack element i is moved to the top.
2. For 0 ⩽ j < i: stack element j is shifted down by 1.
3. For j > i: stack element j remains unchanged.

Instruction place + i

This instruction makes use of indicator polynomials. In addition to its instruction groups, this instruction has the following constraints.

Description

For 0 ⩽ i < 16:

1. Stack element 0 is moved to position i.
2. For 0 ⩽ j < i: stack element j is shifted up by 1.
3. For j > i: stack element j remains unchanged.

Instruction dup + i

This instruction makes use of indicator polynomials. In addition to its instruction groups, this instruction has the following constraints.

Description

1. If i is 0, then st0 is put on top of the stack and
   if i is 1, then st1 is put on top of the stack and
   if i is 2, then st2 is put on top of the stack and
   if i is 3, then st3 is put on top of the stack and
   if i is 4, then st4 is put on top of the stack and
   if i is 5, then st5 is put on top of the stack and
   if i is 6, then st6 is put on top of the stack and
   if i is 7, then st7 is put on top of the stack and
   if i is 8, then st8 is put on top of the stack and
   if i is 9, then st9 is put on top of the stack and
   if i is 10, then st10 is put on top of the stack and
   if i is 11, then st11 is put on top of the stack and
   if i is 12, then st12 is put on top of the stack and
   if i is 13, then st13 is put on top of the stack and
   if i is 14, then st14 is put on top of the stack and
   if i is 15, then st15 is put on top of the stack.

Polynomials

1. ind_0(hv3, hv2, hv1, hv0)·(st0' - st0)
+ ind_1(hv3, hv2, hv1, hv0)·(st0' - st1)
+ ind_2(hv3, hv2, hv1, hv0)·(st0' - st2)
+ ind_3(hv3, hv2, hv1, hv0)·(st0' - st3)
+ ind_4(hv3, hv2, hv1, hv0)·(st0' - st4)
+ ind_5(hv3, hv2, hv1, hv0)·(st0' - st5)
+ ind_6(hv3, hv2, hv1, hv0)·(st0' - st6)
+ ind_7(hv3, hv2, hv1, hv0)·(st0' - st7)
+ ind_8(hv3, hv2, hv1, hv0)·(st0' - st8)
+ ind_9(hv3, hv2, hv1, hv0)·(st0' - st9)
+ ind_10(hv3, hv2, hv1, hv0)·(st0' - st10)
+ ind_11(hv3, hv2, hv1, hv0)·(st0' - st11)
+ ind_12(hv3, hv2, hv1, hv0)·(st0' - st12)
+ ind_13(hv3, hv2, hv1, hv0)·(st0' - st13)
+ ind_14(hv3, hv2, hv1, hv0)·(st0' - st14)
+ ind_15(hv3, hv2, hv1, hv0)·(st0' - st15)

Instruction swap + i

This instruction makes use of indicator polynomials. In addition to its instruction groups, this instruction has the following constraints.

Description

For 0 ⩽ i < 16:

1. Stack element i is moved to the top.
2. The top stack element is moved to position i
3. For j ≠ i: stack element j remains unchanged.

Instruction nop

This instruction is fully constrained by its instruction groups

Instruction skiz

For the correct behavior of instruction skiz, the instruction pointer ip needs to increment by either 1, or 2, or 3. The concrete value depends on the top of the stack st0 and the next instruction, held in nia.

Helper variable hv0 helps with identifying whether st0 is 0. To this end, it holds the inverse-or-zero of st0, i.e., is 0 if and only if st0 is 0, and is the inverse of st0 otherwise.

Efficient arithmetization of instruction skiz makes use of one of the properties of opcodes. Concretely, the least significant bit of an opcode is 1 if and only if the instruction takes an argument. The arithmetization of skiz can incorporate this simple flag by decomposing nia into helper variable registers hv, similarly to how ci is (always) deconstructed into instruction bit registers ib. Correct decomposition is guaranteed by employing a range check.

In addition to its instruction groups, this instruction has the following constraints.

Description

1. Helper variable hv1 is the inverse of st0 or 0.
2. Helper variable hv1 is the inverse of st0 or st0 is 0.
3. The next instruction nia is decomposed into helper variables hv1 through hv5.
4. The indicator helper variable hv1 is either 0 or 1. Here, hv1 == 1 means that nia takes an argument.
5. The helper variable hv2 is either 0 or 1 or 2 or 3.
6. The helper variable hv3 is either 0 or 1 or 2 or 3.
7. The helper variable hv4 is either 0 or 1 or 2 or 3.
8. The helper variable hv5 is either 0 or 1 or 2 or 3.
9. If st0 is non-zero, register ip is incremented by 1. If st0 is 0 and nia takes no argument, register ip is incremented by 2. If st0 is 0 and nia takes an argument, register ip is incremented by 3.

Written as Disjunctive Normal Form, the last constraint can be expressed as:

10. (Register st0 is 0 or ip is incremented by 1), and (st0 has a multiplicative inverse or hv1 is 1 or ip is incremented by 2), and (st0 has a multiplicative inverse or hv1 is 0 or ip is incremented by 3).

Since the three cases are mutually exclusive, the three respective polynomials can be summed up into one.

Polynomials

1. (st0·hv0 - 1)·hv0
2. (st0·hv0 - 1)·st0
3. nia - hv1 - 2·hv2 - 8·hv3 - 32·hv4 - 128·hv5
4. hv1·(hv1 - 1)
5. hv2·(hv2 - 1)·(hv2 - 2)·(hv2 - 3)
6. hv3·(hv3 - 1)·(hv3 - 2)·(hv3 - 3)
7. hv4·(hv4 - 1)·(hv4 - 2)·(hv4 - 3)
8. hv5·(hv5 - 1)·(hv5 - 2)·(hv5 - 3)
9. (ip' - (ip + 1)·st0)
+ ((ip' - (ip + 2))·(st0·hv0 - 1)·(hv1 - 1))
+ ((ip' - (ip + 3))·(st0·hv0 - 1)·hv1)

Helper variable definitions for skiz

1. hv0 = inverse(st0) (if st0 ≠ 0)
2. hv1 = nia mod 2
3. hv2 = (nia >> 1) mod 4
4. hv3 = (nia >> 3) mod 4
5. hv4 = (nia >> 5) mod 4
6. hv5 = nia >> 7

Instruction call + d

In addition to its instruction groups, this instruction has the following constraints.

Description

1. The jump stack pointer jsp is incremented by 1.
2. The jump's origin jso is set to the current instruction pointer ip plus 2.
3. The jump's destination jsd is set to the instruction's argument d.
4. The instruction pointer ip is set to the instruction's argument d.

Polynomials

1. jsp' - (jsp + 1)
2. jso' - (ip + 2)
3. jsd' - nia
4. ip' - nia

Instruction return

In addition to its instruction groups, this instruction has the following constraints.

Description

1. The jump stack pointer jsp is decremented by 1.
2. The instruction pointer ip is set to the last call's origin jso.

Polynomials

1. jsp' - (jsp - 1)
2. ip' - jso

Instruction recurse

In addition to its instruction groups, this instruction has the following constraints.

Description

1. The jump stack pointer jsp does not change.
2. The last jump's origin jso does not change.
3. The last jump's destination jsd does not change.
4. The instruction pointer ip is set to the last jump's destination jsd.

Polynomials

1. jsp' - jsp
2. jso' - jso
3. jsd' - jsd
4. ip' - jsd

Instruction recurse_or_return

In addition to its instruction groups, this instruction has the following constraints.

Description

1. If ST5 equals ST6, then ip in the next row equals jso in the current row.
2. If ST5 equals ST6, then jsp decrements by one.
3. If ST5 equals ST6, then hv0 in the current row is 0.
4. If ST5 is unequal to ST6, then hv0 in the current row is the inverse of (ST6 - ST5).
5. If ST5 is unequal to ST6, then ip in the next row is equal to jsd in the current row.
6. If ST5 is unequal to ST6, then jsp remains unchanged.
7. If ST5 is unequal to ST6, then jso remains unchanged.
8. If ST5 is unequal to ST6, then jsd remains unchanged.

Helper variable definitions for recurse_or_return

To help arithmetizing the equality check between ST5 and ST6, helper variable hv0 is the inverse-or-zero of (ST6 - ST5).

Instruction assert

In addition to its instruction groups, this instruction has the following constraints.

Description

1. The current top of the stack st0 is 1.

Polynomials

1. st0 - 1

Instruction halt

In addition to its instruction groups, this instruction has the following constraints.

Description

1. The instruction executed in the following step is instruction halt.

Polynomials

1. ci' - ci

Instruction read_mem + n

In addition to its instruction groups, this instruction has the following constraints.

Description

1. The RAM pointer st0 is decremented by n.
2. If n is 1, then st1 is moved into st2
   else if n is 2, then st1 is moved into st3
   else if n is 3, then st1 is moved into st4
   else if n is 4, then st1 is moved into st5
   else if n is 5, then st1 is moved into st6.
3. If n is 1, then st2 is moved into st3
   else if n is 2, then st2 is moved into st4
   else if n is 3, then st2 is moved into st5
   else if n is 4, then st2 is moved into st6
   else if n is 5, then st2 is moved into st7.
4. If n is 1, then st3 is moved into st4
   else if n is 2, then st3 is moved into st5
   else if n is 3, then st3 is moved into st6
   else if n is 4, then st3 is moved into st7
   else if n is 5, then st3 is moved into st8.
5. If n is 1, then st4 is moved into st5
   else if n is 2, then st4 is moved into st6
   else if n is 3, then st4 is moved into st7
   else if n is 4, then st4 is moved into st8
   else if n is 5, then st4 is moved into st9.
6. If n is 1, then st5 is moved into st6
   else if n is 2, then st5 is moved into st7
   else if n is 3, then st5 is moved into st8
   else if n is 4, then st5 is moved into st9
   else if n is 5, then st5 is moved into st10.
7. If n is 1, then st6 is moved into st7
   else if n is 2, then st6 is moved into st8
   else if n is 3, then st6 is moved into st9
   else if n is 4, then st6 is moved into st10
   else if n is 5, then st6 is moved into st11.
8. If n is 1, then st7 is moved into st8
   else if n is 2, then st7 is moved into st9
   else if n is 3, then st7 is moved into st10
   else if n is 4, then st7 is moved into st11
   else if n is 5, then st7 is moved into st12.
9. If n is 1, then st8 is moved into st9
   else if n is 2, then st8 is moved into st10
   else if n is 3, then st8 is moved into st11
   else if n is 4, then st8 is moved into st12
   else if n is 5, then st8 is moved into st13.
10. If n is 1, then st9 is moved into st10
    else if n is 2, then st9 is moved into st11
    else if n is 3, then st9 is moved into st12
    else if n is 4, then st9 is moved into st13
    else if n is 5, then st9 is moved into st14.
11. If n is 1, then st10 is moved into st11
    else if n is 2, then st10 is moved into st12
    else if n is 3, then st10 is moved into st13
    else if n is 4, then st10 is moved into st14
    else if n is 5, then st10 is moved into st15.
12. If n is 1, then st11 is moved into st12
    else if n is 2, then st11 is moved into st13
    else if n is 3, then st11 is moved into st14
    else if n is 4, then st11 is moved into st15
    else if n is 5, then the op stack pointer grows by 5.
13. If n is 1, then st12 is moved into st13
    else if n is 2, then st12 is moved into st14
    else if n is 3, then st12 is moved into st15
    else if n is 4, then the op stack pointer grows by 4
    else if n is 5, then with the Op Stack Table accumulates st11 through st15.
14. If n is 1, then st13 is moved into st14
    else if n is 2, then st13 is moved into st15
    else if n is 3, then the op stack pointer grows by 3
    else if n is 4, then the running product with the Op Stack Table accumulates st12 through st15
    else if n is 5, then the running product with the RAM Table accumulates next row's st1 through st5.
15. If n is 1, then st14 is moved into st15
    else if n is 2, then the op stack pointer grows by 2
    else if n is 3, then the running product with the Op Stack Table accumulates st13 through st15
    else if n is 4, then the running product with the RAM Table accumulates next row's st1 through st4
    
16. If n is 1, then the op stack pointer grows by 1
    else if n is 2, then the running product with the Op Stack Table accumulates st14 and st15
    else if n is 3, then the running product with the RAM Table accumulates next row's st1 through st3.
17. If n is 1, then the running product with the Op Stack Table accumulates st15
    else if n is 2, then the running product with the RAM Table accumulates next row's st1 and st2.
18. If n is 1, then the running product with the RAM Table accumulates next row's st1.

Instruction write_mem + n

In addition to its instruction groups, this instruction has the following constraints.

Description

1. The RAM pointer st0 is incremented by n.
2. If n is 1, then st2 is moved into st1
   else if n is 2, then st3 is moved into st1
   else if n is 3, then st4 is moved into st1
   else if n is 4, then st5 is moved into st1
   else if n is 5, then st6 is moved into st1.
3. If n is 1, then st3 is moved into st2
   else if n is 2, then st4 is moved into st2
   else if n is 3, then st5 is moved into st2
   else if n is 4, then st6 is moved into st2
   else if n is 5, then st7 is moved into st2.
4. If n is 1, then st4 is moved into st3
   else if n is 2, then st5 is moved into st3
   else if n is 3, then st6 is moved into st3
   else if n is 4, then st7 is moved into st3
   else if n is 5, then st8 is moved into st3.
5. If n is 1, then st5 is moved into st4
   else if n is 2, then st6 is moved into st4
   else if n is 3, then st7 is moved into st4
   else if n is 4, then st8 is moved into st4
   else if n is 5, then st9 is moved into st4.
6. If n is 1, then st6 is moved into st5
   else if n is 2, then st7 is moved into st5
   else if n is 3, then st8 is moved into st5
   else if n is 4, then st9 is moved into st5
   else if n is 5, then st10 is moved into st5.
7. If n is 1, then st7 is moved into st6
   else if n is 2, then st8 is moved into st6
   else if n is 3, then st9 is moved into st6
   else if n is 4, then st10 is moved into st6
   else if n is 5, then st11 is moved into st6.
8. If n is 1, then st8 is moved into st7
   else if n is 2, then st9 is moved into st7
   else if n is 3, then st10 is moved into st7
   else if n is 4, then st11 is moved into st7
   else if n is 5, then st12 is moved into st7.
9. If n is 1, then st9 is moved into st8
   else if n is 2, then st10 is moved into st8
   else if n is 3, then st11 is moved into st8
   else if n is 4, then st12 is moved into st8
   else if n is 5, then st13 is moved into st8.
10. If n is 1, then st10 is moved into st9
    else if n is 2, then st11 is moved into st9
    else if n is 3, then st12 is moved into st9
    else if n is 4, then st13 is moved into st9
    else if n is 5, then st14 is moved into st9.
11. If n is 1, then st11 is moved into st10
    else if n is 2, then st12 is moved into st10
    else if n is 3, then st13 is moved into st10
    else if n is 4, then st14 is moved into st10
    else if n is 5, then st15 is moved into st10.
12. If n is 1, then st12 is moved into st11
    else if n is 2, then st13 is moved into st11
    else if n is 3, then st14 is moved into st11
    else if n is 4, then st15 is moved into st11
    else if n is 5, then the op stack pointer shrinks by 5.
13. If n is 1, then st13 is moved into st12
    else if n is 2, then st14 is moved into st12
    else if n is 3, then st15 is moved into st12
    else if n is 4, then the op stack pointer shrinks by 4
    else if n is 5, then the running product with the Op Stack Table accumulates next row's st11 through st15.
14. If n is 1, then st14 is moved into st13
    else if n is 2, then st15 is moved into st13
    else if n is 3, then the op stack pointer shrinks by 3
    else if n is 4, then the running product with the Op Stack Table accumulates next row's st12 through st15
    else if n is 5, then the running product with the RAM Table accumulates st1 through st5.
15. If n is 1, then st15 is moved into st14
    else if n is 2, then the op stack pointer shrinks by 2
    else if n is 3, then the running product with the Op Stack Table accumulates next row's st13 through st15
    else if n is 4, then the running product with the RAM Table accumulates st1 through st4.
16. If n is 1, then the op stack pointer shrinks by 1
    else if n is 2, then the running product with the Op Stack Table accumulates next row's st14 and st15
    else if n is 3, then the running product with the RAM Table accumulates st1 through st2.
17. If n is 1, then the running product with the Op Stack Table accumulates next row's st15
    else if n is 2, then the running product with the RAM Table accumulates st1 and st1.
18. If n is 1, then the running product with the RAM Table accumulates st1.

Instruction hash

In addition to its instruction groups, this instruction has the following constraints.

Description

1. st10 is moved into st5.
2. st11 is moved into st6.
3. st12 is moved into st7.
4. st13 is moved into st8.
5. st14 is moved into st9.
6. st15 is moved into st10.
7. The op stack pointer shrinks by 5.
8. The running product with the Op Stack Table accumulates next row's st11 through st15.

Polynomials

1. st5' - st10
2. st6' - st11
3. st7' - st12
4. st8' - st13
5. st9' - st14
6. st10' - st15
7. op_stack_pointer' - op_stack_pointer + 5
8. RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊 - 🍉·op_stack_pointer' - 🫒·st15')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 1) - 🫒·st14')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 2) - 🫒·st13')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 3) - 🫒·st12')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 4) - 🫒·st11')

Instruction assert_vector

In addition to its instruction groups, this instruction has the following constraints.

Description

1. st0 is equal to st5.
2. st1 is equal to st6.
3. st2 is equal to st7.
4. st3 is equal to st8.
5. st4 is equal to st9.
6. st10 is moved into st5.
7. st11 is moved into st6.
8. st12 is moved into st7.
9. st13 is moved into st8.
10. st14 is moved into st9.
11. st15 is moved into st10.
12. The op stack pointer shrinks by 5.
13. The running product with the Op Stack Table accumulates next row's st11 through st15.

Polynomials

1. st5 - st0
2. st6 - st1
3. st7 - st2
4. st8 - st3
5. st9 - st4
6. st5' - st10
7. st6' - st11
8. st7' - st12
9. st8' - st13
10. st9' - st14
11. st10' - st15
12. op_stack_pointer' - op_stack_pointer + 5
13. RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊 - 🍉·op_stack_pointer' - 🫒·st15')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 1) - 🫒·st14')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 2) - 🫒·st13')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 3) - 🫒·st12')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 4) - 🫒·st11')

Instruction sponge_init

This instruction is fully constrained by its instruction groups Beyond that, correct transition is guaranteed by the Hash Table.

Instruction sponge_absorb

In addition to its instruction groups, this instruction has the following constraints. Beyond that, correct transition is guaranteed by the Hash Table.

Description

1. st10 is moved into st0.
2. st11 is moved into st1.
3. st12 is moved into st2.
4. st13 is moved into st3.
5. st14 is moved into st4.
6. st15 is moved into st5.
7. The op stack pointer shrinks by 10.
8. The running product with the Op Stack Table accumulates next row's st6 through st15.

Polynomials

1. st0' - st10
2. st1' - st11
3. st2' - st12
4. st3' - st13
5. st4' - st14
6. st5' - st15
7. op_stack_pointer' - op_stack_pointer + 10
8. RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊 - 🍉·op_stack_pointer' - 🫒·st15')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 1) - 🫒·st14')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 2) - 🫒·st13')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 3) - 🫒·st12')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 4) - 🫒·st11')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 5) - 🫒·st10')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 6) - 🫒·st9')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 7) - 🫒·st8')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 8) - 🫒·st7')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 9) - 🫒·st6')

Instruction sponge_absorb_mem

In addition to its instruction groups, this instruction has the following constraints. Beyond that, correct transition is guaranteed by the Hash Table and the RAM Table.

Description

1. st0 is incremented by 10.

Instruction sponge_squeeze

In addition to its instruction groups, this instruction has the following constraints. Beyond that, correct transition is guaranteed by the Hash Table.

Description

1. st0 is moved into st10.
2. st1 is moved into st11.
3. st2 is moved into st12.
4. st3 is moved into st13.
5. st4 is moved into st14.
6. st5 is moved into st15.
7. The op stack pointer grows by 10.
8. The running product with the Op Stack Table accumulates st6 through st15.

Polynomials

1. st10' - st0
2. st11' - st1
3. st12' - st2
4. st13' - st3
5. st14' - st4
6. st15' - st5
7. op_stack_pointer' - op_stack_pointer - 10
8. RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍉·op_stack_pointer - 🫒·st15)
·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 1) - 🫒·st14)
·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 2) - 🫒·st13)
·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 3) - 🫒·st12)
·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 4) - 🫒·st11)
·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 5) - 🫒·st10)
·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 6) - 🫒·st9)
·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 7) - 🫒·st8)
·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 8) - 🫒·st7)
·(🪤 - 🍋·clk - 🍉·(op_stack_pointer + 9) - 🫒·st6)

Instruction add

In addition to its instruction groups, this instruction has the following constraints.

Description

1. The sum of the top two stack elements is moved into the top of the stack.

Polynomials

1. st0' - (st0 + st1)

Instruction mul

In addition to its instruction groups, this instruction has the following constraints.

Description

1. The product of the top two stack elements is moved into the top of the stack.

Polynomials

1. st0' - st0·st1

Instruction invert

In addition to its instruction groups, this instruction has the following constraints.

Description

1. The top of the stack's inverse is moved into the top of the stack.

Polynomials

1. st0'·st0 - 1

Instruction eq

In addition to its instruction groups, this instruction has the following constraints.

Description

1. Helper variable hv0 is the inverse of the difference of the stack's two top-most elements or 0.
2. Helper variable hv0 is the inverse of the difference of the stack's two top-most elements or the difference is 0.
3. The new top of the stack is 1 if the difference between the stack's two top-most elements is not invertible, 0 otherwise.

Polynomials

1. hv0·(hv0·(st1 - st0) - 1)
2. (st1 - st0)·(hv0·(st1 - st0) - 1)
3. st0' - (1 - hv0·(st1 - st0))

Helper variable definitions for eq

1. hv0 = inverse(rhs - lhs) if rhs ≠ lhs.
2. hv0 = 0 if rhs = lhs.

Instruction split

In addition to its instruction groups, this instruction has the following constraints. Part of the correct transition, namely the range check on the instruction's result, is guaranteed by the U32 Table.

Description

1. The top of the stack is decomposed as 32-bit chunks into the stack's top-most two elements.
2. Helper variable hv0 holds the inverse of $2^{32}-1$ subtracted from the high 32 bits or the low 32 bits are 0.

Polynomials

1. st0 - (2^32·st1' + st0')
2. st0'·(hv0·(st1' - (2^32 - 1)) - 1)

Helper variable definitions for split

Given the high 32 bits of st0 as hi = st0 >> 32 and the low 32 bits of st0 as lo = st0 & 0xffff_ffff,

1. hv0 = (hi - (2^32 - 1)) if lo ≠ 0.
2. hv0 = 0 if lo = 0.

Instruction lt

This instruction is fully constrained by its instruction groups Beyond that, correct transition is guaranteed by the U32 Table.

Instruction and

This instruction is fully constrained by its instruction groups Beyond that, correct transition is guaranteed by the U32 Table.

Instruction xor

This instruction is fully constrained by its instruction groups Beyond that, correct transition is guaranteed by the U32 Table.

Instruction log2floor

This instruction is fully constrained by its instruction groups Beyond that, correct transition is guaranteed by the U32 Table.

Instruction pow

This instruction is fully constrained by its instruction groups Beyond that, correct transition is guaranteed by the U32 Table.

Instruction div_mod

Recall that instruction div_mod takes stack _ d n and computes _ q r where n is the numerator, d is the denominator, r is the remainder, and q is the quotient. The following two properties are guaranteed by the U32 Table:

1. The remainder r is smaller than the denominator d, and
2. all four of n, d, q, and r are u32s.

In addition to its instruction groups, this instruction has the following constraints.

Description

1. Numerator is quotient times denominator plus remainder: n == q·d + r.

Polynomials

1. st0 - st1·st1' - st0'
2. st2' - st2

Instruction pop_count

This instruction is fully constrained by its instruction groups Beyond that, correct transition is guaranteed by the U32 Table.

Instruction xx_add

In addition to its instruction groups, this instruction has the following constraints.

Description

1. The result of adding st0 to st3 is moved into st0.
2. The result of adding st1 to st4 is moved into st1.
3. The result of adding st2 to st5 is moved into st2.
4. st6 is moved into st3.
5. st7 is moved into st4.
6. st8 is moved into st5.
7. st9 is moved into st6.
8. st10 is moved into st7.
9. st11 is moved into st8.
10. st12 is moved into st9.
11. st13 is moved into st10.
12. st14 is moved into st11.
13. st15 is moved into st12.
14. The op stack pointer shrinks by 3.
15. The running product with the Op Stack Table accumulates next row's st13 through st15.

Polynomials

1. st0' - (st0 + st3)
2. st1' - (st1 + st4)
3. st2' - (st2 + st5)
4. st3' - st6
5. st4' - st7
6. st5' - st8
7. st6' - st9
8. st7' - st10
9. st8' - st11
10. st9' - st12
11. st10' - st13
12. st11' - st14
13. st12' - st15
14. op_stack_pointer' - op_stack_pointer + 3
15. RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊 - 🍉·op_stack_pointer' - 🫒·st15')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 1) - 🫒·st14')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 2) - 🫒·st13')

Instruction xx_mul

In addition to its instruction groups, this instruction has the following constraints.

Description

1. The coefficient of x^0 of multiplying the two X-Field elements on the stack is moved into st0.
2. The coefficient of x^1 of multiplying the two X-Field elements on the stack is moved into st1.
3. The coefficient of x^2 of multiplying the two X-Field elements on the stack is moved into st2.
4. st6 is moved into st3.
5. st7 is moved into st4.
6. st8 is moved into st5.
7. st9 is moved into st6.
8. st10 is moved into st7.
9. st11 is moved into st8.
10. st12 is moved into st9.
11. st13 is moved into st10.
12. st14 is moved into st11.
13. st15 is moved into st12.
14. The op stack pointer shrinks by 3.
15. The running product with the Op Stack Table accumulates next row's st13 through st15.

Polynomials

1. st0' - (st0·st3 - st2·st4 - st1·st5)
2. st1' - (st1·st3 + st0·st4 - st2·st5 + st2·st4 + st1·st5)
3. st2' - (st2·st3 + st1·st4 + st0·st5 + st2·st5)
4. st3' - st6
5. st4' - st7
6. st5' - st8
7. st6' - st9
8. st7' - st10
9. st8' - st11
10. st9' - st12
11. st10' - st13
12. st11' - st14
13. st12' - st15
14. op_stack_pointer' - op_stack_pointer + 3
15. RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊 - 🍉·op_stack_pointer' - 🫒·st15')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 1) - 🫒·st14')
·(🪤 - 🍋·clk - 🍊 - 🍉·(op_stack_pointer' + 2) - 🫒·st13')

Instruction x_invert

In addition to its instruction groups, this instruction has the following constraints.

Description

1. The coefficient of x^0 of multiplying X-Field element on top of the current stack and on top of the next stack is 1.
2. The coefficient of x^1 of multiplying X-Field element on top of the current stack and on top of the next stack is 0.
3. The coefficient of x^2 of multiplying X-Field element on top of the current stack and on top of the next stack is 0.

Polynomials

1. st0·st0' - st2·st1' - st1·st2' - 1
2. st1·st0' + st0·st1' - st2·st2' + st2·st1' + st1·st2'
3. st2·st0' + st1·st1' + st0·st2' + st2·st2'

Instruction xb_mul

In addition to its instruction groups, this instruction has the following constraints.

Description

1. The result of multiplying the top of the stack with the X-Field element's coefficient for x^0 is moved into st0.
2. The result of multiplying the top of the stack with the X-Field element's coefficient for x^1 is moved into st1.
3. The result of multiplying the top of the stack with the X-Field element's coefficient for x^2 is moved into st2.
4. st4 is moved into st3.
5. st5 is moved into st4.
6. st6 is moved into st5.
7. st7 is moved into st6.
8. st8 is moved into st7.
9. st9 is moved into st8.
10. st10 is moved into st9.
11. st11 is moved into st10.
12. st12 is moved into st11.
13. st13 is moved into st12.
14. st14 is moved into st13.
15. st15 is moved into st14.
16. The op stack pointer shrinks by 3.
17. The running product with the Op Stack Table accumulates next row's st15.

Polynomials

1. st0' - st0·st1
2. st1' - st0·st2
3. st2' - st0·st3
4. st3' - st4
5. st4' - st5
6. st5' - stt
7. st6' - st7
8. st7' - st8
9. st8' - st9
10. st9' - st10
11. st10' - st11
12. st11' - st12
13. st12' - st13
14. st13' - st14
15. st14' - st15
16. op_stack_pointer' - op_stack_pointer + 1
17. RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊 - 🍉·op_stack_pointer' - 🫒·st15')

Instruction read_io + n

In addition to its instruction groups, this instruction has the following constraints.

Description

1. If n is 1, the running evaluation for standard input accumulates next row's st0
   else if n is 2, the running evaluation for standard input accumulates next row's st0 and st1
   else if n is 3, the running evaluation for standard input accumulates next row's st0 through st2
   else if n is 4, the running evaluation for standard input accumulates next row's st0 through st3
   else if n is 5, the running evaluation for standard input accumulates next row's st0 through st4.

Polynomials

1. ind_1(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardInput' - 🛏·RunningEvaluationStandardInput - st0')
+ ind_2(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardInput' - 🛏·(🛏·RunningEvaluationStandardInput - st0') - st1')
+ ind_3(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardInput' - 🛏·(🛏·(🛏·RunningEvaluationStandardInput - st0') - st1') - st2')
+ ind_4(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardInput' - 🛏·(🛏·(🛏·(🛏·RunningEvaluationStandardInput - st0') - st1') - st2') - st3')
+ ind_5(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardInput' - 🛏·(🛏·(🛏·(🛏·(🛏·RunningEvaluationStandardInput - st0') - st1') - st2') - st3') - st4')

Instruction write_io + n

In addition to its instruction groups, this instruction has the following constraints.

Description

1. If n is 1, the running evaluation for standard output accumulates st0
   else if n is 2, the running evaluation for standard output accumulates st0 and st1
   else if n is 3, the running evaluation for standard output accumulates st0 through st2
   else if n is 4, the running evaluation for standard output accumulates st0 through st3
   else if n is 5, the running evaluation for standard output accumulates st0 through st4.

Polynomials

1. ind_1(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·RunningEvaluationStandardOutput - st0)
+ ind_2(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·(🧯·RunningEvaluationStandardOutput - st0) - st1)
+ ind_3(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·(🧯·(🧯·RunningEvaluationStandardOutput - st0) - st1) - st2)
+ ind_4(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·(🧯·(🧯·(🧯·RunningEvaluationStandardOutput - st0) - st1) - st2) - st3)
+ ind_5(hv3, hv2, hv1, hv0)·(RunningEvaluationStandardOutput' - 🧯·(🧯·(🧯·(🧯·(🧯·RunningEvaluationStandardOutput - st0) - st1) - st2) - st3) - st4)

Instruction merkle_step

Recall that in a Merkle tree, the indices of left (respectively right) leaves have 0 (respectively 1) as their least significant bit. This motivates the use of a helper variable to hold that least significant bit.

In addition to its instruction groups, this instruction has the following constraints. The two Evaluation Arguments also used for instruction hash guarantee correct transition of the top of the stack.

Description

1. Helper variable hv5 is either 0 or 1.
2. st5 is shifted by 1 bit to the right. In other words, twice st5 in the next row plus hv5 equals st5 in the current row.

Helper variable definitions for merkle_step

1. hv0 through hv4 hold the sibling digest of the node indicated by st5, as read from the interface for non-deterministic input.
2. hv5 holds the result of st5 % 2, the Merkle tree node index's least significant bit, indicating whether it is a left or right node.

Instruction merkle_step_mem

In addition to its instruction groups, this instruction has the following constraints. The two Evaluation Arguments also used for instruction hash guarantee correct transition of the top of the stack. See also merkle_step.

Description

1. Stack element st6 does not change.
2. Stack element st7 is incremented by 5.
3. Helper variable hv5 is either 0 or 1.
4. st5 is shifted by 1 bit to the right. In other words, twice st5 in the next row plus hv5 equals st5 in the current row.
5. The running product with the RAM Table accumulates hv0 through hv4 using the (appropriately adjusted) RAM pointer held in st7.

Helper variable definitions for merkle_step_mem

1. hv0 through hv4 hold the sibling digest of the node indicated by st5, as read from RAM at the address held in st7.
2. hv5 holds the result of st5 % 2, the Merkle tree node index's least significant bit, indicating whether it is a left or right node.

Instruction xx_dot_step

In addition to its instruction groups, this instruction has the following constraints.

Description

1. Store (RAM[st0], RAM[st0+1], RAM[st0+2]) in (hv0, hv1, hv2).
2. Store (RAM[st1], RAM[st1+1], RAM[st1+2]) in (hv3, hv4, hv5).
3. Add (hv0 + hv1·x + hv2·x²) · (hv3 + hv4·x + hv5·x²) into (st2, st3, st4)
4. Increase the pointers: st0 and st1 by 3 each.

Instruction xb_dot_step

In addition to its instruction groups, this instruction has the following constraints.

Description

1. Store RAM[st0] in hv0.
2. Store (RAM[st1], RAM[st1+1], RAM[st1+2]) in (hv1, hv2, hv3).
3. Add hv0 · (hv1 + hv2·x + hv3·x²) into (st1, st2, st3)
4. Increase the pointers: st0 and st1 by 1 and 3, respectively.

Operational Stack Table

The operational stack¹ is where the program stores simple elementary operations, function arguments, and pointers to important objects. There are 16 registers (st0 through st15) that the program can access directly. These registers correspond to the top of the stack. They are recorded in the Processor Table.

The rest of the op stack is stored in a dedicated memory object called “operational stack underflow memory”. It is initially empty. The evolution of the underflow memory is recorded in the Op Stack Table. The sole task of the Op Stack Table is to keep underflow memory immutable. To achieve this, any read or write accesses to the underflow memory are recorded in the Op Stack Table. Read and write accesses to op stack underflow memory are a side effect of shrinking or growing the op stack.

Main Columns

The Op Stack Table consists of 4 columns:

1. the cycle counter clk
2. the shrink stack indicator shrink_stack, corresponding to the processor's instruction bit 1 ib1,
3. the op stack pointer stack_pointer, and
4. the first underflow element first_underflow_element.

Column clk records the processor's execution cycle during which the read or write access happens. The shrink_stack indicator signals whether the underflow memory access is a read or a write: a read corresponds to a shrinking stack is indicated by a 1, a write corresponds to a growing stack and is indicated by a 0. The same column doubles up as a padding indicator, in which case shrink_stack is set to 2. The stack_pointer is the address at which the to-be-read-or-written element resides. Finally, the first_underflow_element is the stack element being transferred from stack register st15 into underflow memory on a write, or the other way around on a read.

A subset Permutation Argument with the Processor Table establishes that the rows recorded in the Op Stack Table are consistent with the processor's part of the op stack.

In order to guarantee memory consistency, the rows of the operational stack table are sorted by stack_pointer first, cycle count clk second. The mechanics are best illustrated by an example. Observe how the malicious manipulation of the Op Stack Underflow Memory, the change of “42” into “99” in cycle 8, is detected: The transition constraints of the Op Stack Table stipulate that if stack_pointer does not change, then the first_underflow_element can only change if the next instruction grows the stack. Consequently, row [4, 0, 8, 42] being followed by row [10, 1, 8, 99] violates the constraints. The shrink stack indicator being correct is guaranteed by the Permutation Argument between Op Stack Table and the Processor Table.

For illustrative purposes only, we use four stack registers st0 through st3 in the example. Triton VM has 16 stack registers, st0 through st15. Furthermore, implied next instructions usually recorded in register “next instruction or argument” nia are omitted for reasons of readability.

Processor's execution trace:

Operational Stack Table:

Auxiliary Columns

The Op Stack Table has 2 auxiliary columns, rppa and ClockJumpDifferenceLookupClientLogDerivative.

1. A Permutation Argument establishes that the rows of the Op Stack Table correspond to the rows of the Processor Table. The running product for this argument is contained in the rppa column.
2. In order to achieve memory consistency, a Lookup Argument shows that all clock jump differences are contained in the clk column of the Processor Table. The logarithmic derivative for this argument is contained in the ClockJumpDifferenceLookupClientLogDerivative column.

Padding

The last row in the Op Stack Table is taken as the padding template row. Should the Op Stack Table be empty, the row (clk, shrink_stack, stack_pointer, first_underflow_element) = (0, 0, 16, 0) is used instead. In the template row, the shrink_stack indicator is set to 2, signifying padding. The template row is inserted below the last row until the desired padded height is reached.

Memory-Consistency

Memory-consistency follows from two more primitive properties:

1. Contiguity of regions of constant memory pointer. Since in Op Stack Table, the stack_pointer can change by at most one per cycle, it is possible to enforce a full sorting using AIR constraints.
2. Correct inner-sorting within contiguous regions. Specifically, the rows within each contiguous region of constant memory pointer should be sorted for clock cycle. This property is established by the clock jump difference Lookup Argument. In a nutshell, every difference of consecutive clock cycles that occurs within one contiguous block of constant memory pointer is shown itself to be a valid clock cycle through a separate cross-table argument.

Arithmetic Intermediate Representation

Let all household items (🪥, 🛁, etc.) be challenges, concretely evaluation points, supplied by the verifier. Let all fruit & vegetables (🥝, 🥥, etc.) be challenges, concretely weights to compress rows, supplied by the verifier. Both types of challenges are X-field elements, i.e., elements of ${\mathbb{F}}_{p^3}$.

Initial Constraints

1. The stack_pointer is the number of available stack registers, i.e., 16.
2. If the row is not a padding row, the running product for the permutation argument with the Processor Table rppa starts off having accumulated the first row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤. Otherwise, it is the Permutation Argument's default initial, i.e., 1.
3. The logarithmic derivative for the clock jump difference lookup ClockJumpDifferenceLookupClientLogDerivative is 0.

Initial Constraints as Polynomials

1. stack_pointer - 16
2. (shrink_stack - 2)·(rppa - (🪤 - 🍋·clk - 🍊·shrink_stack - 🍉·stack_pointer - 🫒·first_underflow_element))
+ (shrink_stack - 0)·(shrink_stack - 1)·(rppa - 1)
3. ClockJumpDifferenceLookupClientLogDerivative

Consistency Constraints

None.

Transition Constraints

1. • the stack_pointer increases by 1, or
   • the stack_pointer does not change AND the first_underflow_element does not change, or
   • the stack_pointer does not change AND the shrink stack indicator shrink_stack in the next row is 0.
2. If thex next row is not a padding row, the running product for the permutation argument with the Processor Table rppa absorbs the next row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤. Otherwise, the running product remains unchanged.
3. If the current row is a padding row, then the next row is a padding row.
4. If the next row is not a padding row and the op stack pointer stack_pointer does not change, then the logarithmic derivative for the clock jump difference lookup ClockJumpDifferenceLookupClientLogDerivative accumulates a factor (clk' - clk) relative to indeterminate 🪞. Otherwise, it remains the unchanged.

Written as Disjunctive Normal Form, the same constraints can be expressed as:

1. The stack_pointer increases by 1 or the stack_pointer does not change.
2. The stack_pointer increases by 1 or the first_underflow_element does not change or the shrink stack indicator shrink_stack in the next row is 0.
3. • The next row is a padding row or rppa has accumulated the next row, and
   • the next row is not a padding row or rppa remains unchanged.
4. The current row is not a padding row or the next row is a padding row.
5. • the stack_pointer changes or the next row is a padding row or the logarithmic derivative accumulates a summand,
   • the stack_pointer remains unchanged or the logarithmic derivative remains unchanged, and
   • the next row is not a padding row or the logarithmic derivative remains unchanged.

Transition Constraints as Polynomials

1. (stack_pointer' - stack_pointer - 1)·(stack_pointer' - stack_pointer)
2. (stack_pointer' - stack_pointer - 1)·(first_underflow_element' - first_underflow_element)·(shrink_stack' - 0)
3. (shrink_stack' - 2)·(rppa' - rppa·(🪤 - 🍋·clk' - 🍊·shrink_stack' - 🍉·stack_pointer' - 🫒first_underflow_element'))
+ (shrink_stack' - 0)·(shrink_stack' - 1)·(rppa' - rppa)
4. (shrink_stack - 0)·(shrink_stack - 1)·(shrink_stack' - 2)
5. (stack_pointer' - stack_pointer - 1)·(shrink_stack' - 2)·((ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative) · (🪞 - clk' + clk) - 1)
+ (stack_pointer' - stack_pointer)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)
+ (shrink_stack' - 0)·(shrink_stack' - 1)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)

Terminal Constraints

None.

Random Access Memory Table

The purpose of the RAM Table is to ensure that the RAM is accessed in a consistent manner. That is, all mutation of RAM happens explicitly through instruction write_mem, and any invocations of instruction read_mem return the values last written.

The fundamental principle is identical to that of the Op Stack Table. The main difference is the absence of a dedicated stack pointer. Instead, op stack element st0 is used as RAM pointer ram_pointer.

If some RAM address is read from before it is written to, the corresponding value is not determined. This is one of interfaces for non-deterministic input in Triton VM. Consecutive reads from any such address always returns the same value (until overwritten via write_mem).

Main Columns

The RAM Table has 7 main columns:

1. the cycle counter clk,
2. the executed instruction_type – 0 for “write”, 1 for “read”, 2 for padding rows,
3. RAM pointer ram_pointer,
4. RAM value ram_value,
5. helper variable "inverse of ram_pointer difference" iord,
6. Bézout coefficient polynomial coefficient 0 bcpc0,
7. Bézout coefficient polynomial coefficient 1 bcpc1,

Column iord helps with detecting a change of ram_pointer across two RAM Table rows. The function of iord is best explained in the context of sorting the RAM Table's rows, which is what the next section is about.

The Bézout coefficient polynomial coefficients bcpc0 and bcpc1 represent the coefficients of polynomials that are needed for the contiguity argument. This argument establishes that all regions of constant ram_pointer are contiguous.

Auxiliary Columns

The RAM Table has 6 auxiliary columns:

1. RunningProductOfRAMP, accumulating next row's ram_pointer as a root whenever ram_pointer changes between two rows,
2. FormalDerivative, the (evaluated) formal derivative of RunningProductOfRAMP,
3. BezoutCoefficient0, the (evaluated) polynomial with main column bcpc0 as coefficients,
4. BezoutCoefficient1, the (evaluated) polynomial with main column bcpc1 as coefficients,
5. RunningProductPermArg, the Permutation Argument with the Processor Table, and
6. ClockJumpDifferenceLookupClientLogDerivative, part of memory consistency.

Columns RunningProductOfRAMP, FormalDerivative, BezoutCoefficient0, and BezoutCoefficient1 are part of the Contiguity Argument.

Sorting Rows

In the Hash Table, the rows are arranged such that they

1. form contiguous regions of ram_pointer, and
2. are sorted by cycle counter clk within each such region.

One way to achieve this is to sort by ram_pointer first, clk second.

Coming back to iord: if the difference between ram_pointer in row $i$ and row $i+1$ is 0, then iord in row $i$ is 0. Otherwise, iord in row $i$ is the multiplicative inverse of the difference between ram_pointer in row $i+1$ and ram_pointer in row $i$. In the last row, there being no next row, iord is 0.

An example of the mechanics can be found below. To increase visual clarity, stack registers holding value “0” are represented by an empty cell. For illustrative purposes only, we use six stack registers st0 through st5 in the example. Triton VM has 16 stack registers, st0 through st15.

Processor Table:

RAM Table:

Padding

The row used for padding the RAM Table is its last row, with the instruction_type set to 2.

If the RAM Table is empty, the all-zero row with the following modifications is used instead:

• instruction_type is set to 2, and
• bcpc1 is set to 1.

This ensures that the Contiguity Argument works correctly in the absence of any actual contiguous RAM pointer region.

The padding row is inserted below the RAM Table until the desired height is reached.

Row Permutation Argument

The permutation argument with the Processor Table establishes that the RAM Table's rows correspond to the Processor Table's sent and received RAM values, at the correct cycle counter and RAM address.

Arithmetic Intermediate Representation

Let all household items (🪥, 🛁, etc.) be challenges, concretely evaluation points, supplied by the verifier. Let all fruit & vegetables (🥝, 🥥, etc.) be challenges, concretely weights to compress rows, supplied by the verifier. Both types of challenges are X-field elements, i.e., elements of ${\mathbb{F}}_{p^3}$.

Initial Constraints

1. The first coefficient of the Bézout coefficient polynomial 0 bcpc0 is 0.
2. The Bézout coefficient 0 bc0 is 0.
3. The Bézout coefficient 1 bc1 is equal to the first coefficient of the Bézout coefficient polynomial bcpc1.
4. The running product polynomial RunningProductOfRAMP starts with 🧼 - ram_pointer.
5. The formal derivative starts with 1.
6. If the first row is not a padding row, the running product for the permutation argument with the Processor Table RunningProductPermArg has absorbed the first row with respect to challenges 🍍, 🍈, 🍎, and 🌽 and indeterminate 🛋.
   Else, the running product for the permutation argument with the Processor Table RunningProductPermArg is 1.
7. The logarithmic derivative for the clock jump difference lookup ClockJumpDifferenceLookupClientLogDerivative is 0.

Initial Constraints as Polynomials

1. bcpc0
2. bc0
3. bc1 - bcpc1
4. RunningProductOfRAMP - 🧼 + ram_pointer
5. FormalDerivative - 1
6. (RunningProductPermArg - 🛋 - 🍍·clk - 🍈·ram_pointer - 🍎·ram_value - 🌽·instruction_type)·(instruction_type - 2)
(RunningProductPermArg - 1)·(instruction_type - 1)·(instruction_type - 0)
7. ClockJumpDifferenceLookupClientLogDerivative

Consistency Constraints

None.

Transition Constraints

1. If the current row is a padding row, then the next row is a padding row.
2. The “inverse of ram_pointer difference” iord is 0 or iord is the inverse of the difference between current and next row's ram_pointer.
3. The ram_pointer changes or iord is the inverse of the difference between current and next row's ram_pointer.
4. The ram_pointer changes or instruction_type is “write” or the ram_value remains unchanged.
5. The bcbp0 changes if and only if the ram_pointer changes.
6. The bcbp1 changes if and only if the ram_pointer changes.
7. If the ram_pointer changes, the RunningProductOfRAMP accumulates next ram_pointer.
   Otherwise, it remains unchanged.
8. If the ram_pointer changes, the FormalDerivative updates under the product rule of differentiation.
   Otherwise, it remains unchanged.
9. If the ram_pointer changes, Bézout coefficient 0 bc0 updates according to the running evaluation rules with respect to bcpc0.
   Otherwise, it remains unchanged.
10. If the ram_pointer changes, Bézout coefficient 1 bc1 updates according to the running evaluation rules with respect to bcpc1.
    Otherwise, it remains unchanged.
11. If the next row is not a padding row, the RunningProductPermArg accumulates the next row.
    Otherwise, it remains unchanged.
12. If the ram_pointer does not change and the next row is not a padding row, the ClockJumpDifferenceLookupClientLogDerivative accumulates the difference of clk.
    Otherwise, it remains unchanged.