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 $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 $F_{p}$ , and the transition function gives rise to low-degree transition verification polynomials from the ring of multivariate polynomials over $F_{p}$ .

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.

The name “Oxfoi” comes from the prime's hexadecimal representation 0xffffffff00000001.

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:

Program Memory, from which the VM reads instructions.
Op Stack Memory, which stores the operational stack.
RAM, to which the VM can read and write field elements.
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:

the operational stack registers st0 through st15, and
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. Furthermore, executing instruction recurse requires a non-empty jump stack.

Of course, the machine running Triton VM might have stricter limitations: storing or accessing $(2^{64} - 2^{32} + 1) \cdot 63.99$ bits $\approx 148$ exabytes of data is a non-trivial engineering feat.

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 (*).

Register	Name	Purpose
*`clk`	cycle counter	counts the number of cycles the program has been running for
*`IsPadding`	padding indicator	indicates whether current state is only recorded to improve on STARK's computational runtime
`ip`	instruction pointer	contains the memory address (in Program Memory) of the instruction
`ci`	current instruction register	contains the current instruction
`nia`	next instruction register	contains either the instruction at the next address in Program Memory, or the argument for the current instruction
*`ib0` through `ib6`	instruction bit	decomposition of the instruction's opcode used to keep the AIR degree low
`jsp`	jump stack pointer	contains the memory address (in jump stack memory) of the top of the jump stack
`jso`	jump stack origin	contains the value of the instruction pointer of the last `call`
`jsd`	jump stack destination	contains the argument of the last `call`
`st0` through `st15`	operational stack registers	contain explicit operational stack values
*`op_stack_pointer`	operational stack pointer	the current size of the operational stack
*`hv0` through `hv5`	helper variable registers	helper variables for some arithmetic operations
*`cjd_mul`	clock jump difference lookup multiplicity	multiplicity with which the current `clk` is looked up by the Op Stack Table, RAM Table, and Jump Stack Table

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, divine_sibling, split, and eq, 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	Opcode	old op stack	new op stack	Description
`pop` + `n`	3	e.g., `_ c b a`	e.g., `_`	Pops the `n` top elements from the stack. 1 ⩽ `n` ⩽ 5
`push` + `a`	1	`_`	`_ a`	Pushes `a` onto the stack.
`divine` + `n`	9	e.g., `_`	e.g., `_ b a`	Pushes `n` non-deterministic elements `a` to the stack. Interface for secret input. 1 ⩽ `n` ⩽ 5
`dup` + `i`	17	e.g., `_ e d c b a`	e.g., `_ e d c b a d`	Duplicates the element `i` positions away from the top. 0 ⩽ `i` < 16
`swap` + `i`	25	e.g., `_ e d c b a`	e.g., `_ e a c b d`	Swaps the `i`th stack element with the top of the stack. 0 < `i` < 16

Instruction divine n (together with divine_sibling) 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

Instruction	Opcode	old op stack	new op stack	old `ip`	new `ip`	old jump stack	new jump stack	Description
`halt`	0	`_`	`_`	`ip`	`ip+1`	`_`	`_`	Solves the halting problem (if the instruction is reached). Indicates graceful shutdown of the VM.
`nop`	8	`_`	`_`	`ip`	`ip+1`	`_`	`_`	Do nothing
`skiz`	2	`_ a`	`_`	`ip`	`ip+s`	`_`	`_`	Skip next instruction if `a` is zero. `s` ∈ {1, 2, 3} depends on `a` and whether the next instruction takes an argument.
`call` + `d`	33	`_`	`_`	`ip`	`d`	`_`	`_ (ip+2, d)`	Push `(ip+2,d)` to the jump stack, and jump to absolute address `d`
`return`	16	`_`	`_`	`ip`	`o`	`_ (o, d)`	`_`	Pop one pair off the jump stack and jump to that pair's return address (which is the first element).
`recurse`	24	`_`	`_`	`ip`	`d`	`_ (o, d)`	`_ (o, d)`	Peek at the top pair of the jump stack and jump to that pair's destination address (which is the second element).
`assert`	10	`_ a`	`_`	`ip`	`ip+1`	`_`	`_`	Pops `a` if `a == 1`, else crashes the virtual machine.

Memory Access

Instruction	Opcode	old op stack	new op stack	old RAM	new RAM	Description
`read_mem` + `n`	41	e.g., `_ p+2`	e.g., `_ v2 v1 v0 p-1`	[p: v0, p+1, v1, …]	[p: v0, p+1, v1, …]	Reads consecutive values `vi` from RAM at address `p` and puts them onto the op stack. Decrements RAM pointer (`st0`) by `n`. 1 ⩽ `n` ⩽ 5
`write_mem` + `n`	11	e.g., `_ v2 v1 v0 p`	e.g., `_ p+3`	[]	[p: v0, p+1, v1, …]	Writes op stack's `n` top-most values `vi` to RAM at the address `p+i`, popping the `vi`. Increments RAM pointer (`st0`) by `n`. 1 ⩽ `n` ⩽ 5

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

instruction	old op stack	new op stack	old RAM	new RAM
`read_mem 1`	`_ p`	`_ a p-1`	[p: a]	[p: a]
`read_mem 2`	`_ p+1`	`_ b a p-1`	[p: a, p+1: b]	[p: a, p+1: b]
`read_mem 3`	`_ p+2`	`_ c b a p-1`	[p: a, p+1: b, p+2: c]	[p: a, p+1: b, p+2: c]
`read_mem 4`	`_ p+3`	`_ d c b a p-1`	[p: a, p+1: b, p+2: c, p+3: d]	[p: a, p+1: b, p+2: c, p+3: d]
`read_mem 5`	`_ p+4`	`_ e d c b a p-1`	[p: a, p+1: b, p+2: c, p+3: d, p+4: e]	[p: a, p+1: b, p+2: c, p+3: d, p+4: e]
`write_mem 1`	`_ a p`	`_ p+1`	[]	[p: a]
`write_mem 2`	`_ b a p`	`_ p+2`	[]	[p: a, p+1: b]
`write_mem 3`	`_ c b a p`	`_ p+3`	[]	[p: a, p+1: b, p+2: c]
`write_mem 4`	`_ d c b a p`	`_ p+4`	[]	[p: a, p+1: b, p+2: c, p+3: d]
`write_mem 5`	`_ e d c b a p`	`_ p+5`	[]	[p: a, p+1: b, p+2: c, p+3: d, p+4: e]

Hashing

Instruction	Opcode	old op stack	new op stack	Description
`hash`	18	`_ jihgfedcba`	`_ yxwvu`	Hashes the stack's 10 top-most elements and puts their digest onto the stack, shrinking the stack by 5.
`divine_sibling`	32	`_ i edcba`	e.g., `_ (i div 2) edcba zyxwv`	Helps traversing a Merkle tree during authentication path verification. See extended description below.
`assert_vector`	26	`_ edcba edcba`	`_ edcba`	Assert equality of `st(i)` to `st(i+5)` for `0 <= i < 4`. Crashes the VM if any pair is unequal. Pops the 5 top-most elements.
`sponge_init`	40	`_`	`_`	Initializes (resets) the Sponge's state. Must be the first Sponge instruction executed.
`sponge_absorb`	34	`_ _jihgfedcba`	`_`	Absorbs the stack's ten top-most elements into the Sponge state.
`sponge_squeeze`	48	`_`	`_ zyxwvutsrq`	Squeezes the Sponge and pushes the 10 squeezed elements onto the stack.

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 instruction divine_sibling 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 zyxwv 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 base level. Depending on this least significant bit of i, divine_sibling either

(i = 0 mod 2, i.e., current node is left sibling) lets edcba remain in registers st0 through st4 and puts zyxwv into registers st5 through st9, or
(i = 1 mod 2, i.e., current node is right sibling) moves edcba into registers st5 through st9 and puts zyxwv into registers st0 through st4.

In either case, 6th register i is shifted by 1 bit to the right, i.e., the least-significant bit is dropped, and moved into the 11th register. In conjunction with instruction hash and assert_vector, the instruction divine_sibling allows to efficiently verify a Merkle authentication path.

The instructions sponge_init, sponge_absorb, 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

Instruction	Opcode	old op stack	new op stack	Description
`add`	42	`_ b a`	`_ c`	Computes the sum (`c`) of the top two elements of the stack (`b` and `a`) over the field.
`mul`	50	`_ b a`	`_ c`	Computes the product (`c`) of the top two elements of the stack (`b` and `a`) over the field.
`invert`	56	`_ a`	`_ b`	Computes the multiplicative inverse (over the field) of the top of the stack. Crashes the VM if the top of the stack is 0.
`eq`	58	`_ b a`	`_ (a == b)`	Tests the top two stack elements for equality.

Bitwise Arithmetic on Stack

Instruction	Opcode	old op stack	new op stack	Description
`split`	4	`_ a`	`_ hi lo`	Decomposes the top of the stack into the lower 32 bits and the upper 32 bits.
`lt`	6	`_ b a`	`_ a<b`	“Less than” of the stack's two top-most elements. Crashes the VM if `a` or `b` is not u32.
`and`	14	`_ b a`	`_ a&b`	Bitwise and of the stack's two top-most elements. Crashes the VM if `a` or `b` is not u32.
`xor`	22	`_ b a`	`_ a^b`	Bitwise exclusive or of the stack's two top-most elements. Crashes the VM if `a` or `b` is not u32.
`log_2_floor`	12	`_ a`	`_ ⌊log₂(a)⌋`	The number of bits in `a` minus 1, i.e., $⌊ lo g_{2} a ⌋$ . Crashes the VM if `a` is 0 or not u32.
`pow`	30	`_ e b`	`_ b**e`	The top of the stack to the power of the stack's runner up. Crashes the VM if exponent `e` is not u32.
`div_mod`	20	`_ d n`	`_ q r`	Division with remainder of numerator `n` by denominator `d`. Guarantees the properties `n == q·d + r` and `r < d`. Crashes the VM if `n` or `d` is not u32 or if `d` is 0.
`pop_count`	28	`_ a`	`_ w`	Computes the hamming weight or “population count” of `a`. Crashes the VM if `a` is not u32.

Extension Field Arithmetic on Stack

Instruction	Opcode	old op stack	new op stack	Description
`xxadd`	66	`_ z y x b c a`	`_ w v u`	Adds the two extension field elements encoded by field elements `z y x` and `b c a`.
`xxmul`	74	`_ z y x b c a`	`_ w v u`	Multiplies the two extension field elements encoded by field elements `z y x` and `b c a`.
`xinvert`	64	`_ z y x`	`_ w v u`	Inverts the extension field element encoded by field elements `z y x` in-place. Crashes the VM if the extension field element is 0.
`xbmul`	82	`_ z y x a`	`_ w v u`	Scalar multiplication of the extension field element encoded by field elements `z y x` with field element `a`. Overwrites `z y x` with the result.

Input/Output

Instruction	Opcode	old op stack	new op stack	Description
`read_io` + `n`	49	e.g., `_`	e.g., `_ c b a`	Reads `n` B-Field elements from standard input and pushes them to the stack. 1 ⩽ `n` ⩽ 5
`write_io` + `n`	19	e.g., `_ c b a`	e.g., `_`	Pops `n` elements from the stack and writes them to standard output. 1 ⩽ `n` ⩽ 5

Arithmetization

An arithmetization defines two things:

algebraic execution tables (AETs), and
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.

Base 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., $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 base columns, and make up the base table.

Extension Tables

The entries of a table's columns corresponding to Permutation, Evaluation, and Lookup Arguments are elements from the X-field $F_{p^{3}}$ . These columns are referred to as a table's extension columns, both because the entries are elements of the X-field and because the entries can only be computed using the base tables, through an extension process. Together, these columns are referred to as a table's extension columns, and make up the extension 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^{⌈ l o g_{2} h ⌉}$ .

Arithmetic Intermediate Representation

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

Initial Constraints, defining values in a table's first row,
Consistency Constraints, establishing consistency within any given row,
Transition Constraints, establishing the consistency of two consecutive rows in relation to each other, and
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.

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 $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 $rate$ ¹.

Base Columns

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

Column	Description
`Address`	an instruction's address
`Instruction`	the (opcode of the) instruction
`LookupMultiplicity`	how often an instruction has been executed
*`IndexInChunk`	`Address` modulo the Tip5 $rate$ , which is 10
*`MaxMinusIndexInChunkInv`	the inverse-or-zero of $rate - 1 - IndexInChunk$
*`IsHashInputPadding`	padding indicator for absorbing the program into the Sponge
`IsTablePadding`	padding indicator for rows only required due to the dominating length of some other table

Extension 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 extension 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 $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:

column Address is increased by 1,
column Instruction is set to 0,
column LookupMultiplicity is set to 0,
column IndexInChunk is set to Address mod $rate$ ,
column MaxMinusIndexInChunkInv is set to the inverse-or-zero of $rate - 1 - IndexInChunk$ ,
column IsHashInputPadding is set to 1, and
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}{α - 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 $F_{p^{3}}$ .

Initial Constraints

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

Initial Constraints as Polynomials

Address
IndexInChunk
IsHashInputPadding
InstructionLookupServerLogDerivative
PrepareChunkRunningEvaluation - 🪑 - Instruction
SendChunkRunningEvaluation - 1

Consistency Constraints

The MaxMinusIndexInChunkInv is zero or the inverse of $rate - 1 -$ IndexInChunk.
The IndexInChunk is $rate - 1$ or the MaxMinusIndexInChunkInv is the inverse of $rate - 1 -$ IndexInChunk.
Indicator IsHashInputPadding is either 0 or 1.
Indicator IsTablePadding is either 0 or 1.

Consistency Constraints as Polynomials

(1 - MaxMinusIndexInChunkInv · (rate - 1 - IndexInChunk)) · MaxMinusIndexInChunkInv
(1 - MaxMinusIndexInChunkInv · (rate - 1 - IndexInChunk)) · (rate - 1 - IndexInChunk)
IsHashInputPadding · (IsHashInputPadding - 1)
IsTablePadding · (IsTablePadding - 1)

Transition Constraints

The Address increases by 1.
If the IndexInChunk is not $rate - 1$ , it increases by 1. Else, the IndexInChunk in the next row is 0.
The indicator IsHashInputPadding is 0 or remains unchanged.
The padding indicator IsTablePadding is 0 or remains unchanged.
If IsHashInputPadding is 0 in the current row and 1 in the next row, then Instruction in the next row is 1.
If IsHashInputPadding is 1 in the current row then Instruction in the next row is 0.
If IsHashInputPadding is 1 in the current row and IndexInChunk is $rate - 1$ in the current row then IsTablePadding is 1 in the next row.
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.
If the IndexInChunk in the current row is not $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 🪑.
If the next row is not a padding row and the IndexInChunk in the next row is $rate - 1$ , then SendChunkRunningEvaluation absorbs PrepareChunkRunningEvaluation in the next row with respect to variable 🪣. Otherwise, it remains unchanged.

Transition Constraints as Polynomials

Address' - Address - 1
MaxMinusIndexInChunkInv · (IndexInChunk' - IndexInChunk - 1)
+ (1 - MaxMinusIndexInChunkInv · (rate - 1 - IndexInChunk)) · IndexInChunk'
IsHashInputPadding · (IsHashInputPadding' - IsHashInputPadding)
IsTablePadding · (IsTablePadding' - IsTablePadding)
(IsHashInputPadding - 1) · IsHashInputPadding' · (Instruction' - 1)
IsHashInputPadding · Instruction'
IsHashInputPadding · (1 - MaxMinusIndexInChunkInv · (rate - 1 - IndexInChunk)) · IsTablePadding'
(1 - IsHashInputPadding) · ((InstructionLookupServerLogDerivative' - InstructionLookupServerLogDerivative) · (🪥 - 🥝·Address - 🥥·Instruction - 🫐·Instruction') - LookupMultiplicity)
+ IsHashInputPadding · (InstructionLookupServerLogDerivative' - InstructionLookupServerLogDerivative)
(rate - 1 - IndexInChunk) · (PrepareChunkRunningEvaluation' - 🪑·PrepareChunkRunningEvaluation - Instruction')
+ (1 - MaxMinusIndexInChunkInv · (rate - 1 - IndexInChunk)) · (PrepareChunkRunningEvaluation' - 🪑 - Instruction')
(IsTablePadding' - 1) · (1 - MaxMinusIndexInChunkInv' · (rate - 1 - IndexInChunk')) · (SendChunkRunningEvaluation' - 🪣·SendChunkRunningEvaluation - PrepareChunkRunningEvaluation')
+ (SendChunkRunningEvaluation' - SendChunkRunningEvaluation) · IsTablePadding'
+ (SendChunkRunningEvaluation' - SendChunkRunningEvaluation) · (rate - 1 - IndexInChunk')

Terminal Constraints

The indicator IsHashInputPadding is 1.
The IndexInChunk is $rate - 1$ or the indicator IsTablePadding is 1.

Terminal Constraints as Polynomials

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

See also section 2.5 “Fixed-Length versus Variable-Length” in the Tip5 paper.

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.

Base Columns

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

Extension Columns

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

RunningEvaluationStandardInput for the Evaluation Argument with the input symbols.
RunningEvaluationStandardOutput for the Evaluation Argument with the output symbols.
InstructionLookupClientLogDerivative for the Lookup Argument with the Program Table
RunningProductOpStackTable for the Permutation Argument with the Op Stack Table.
RunningProductRamTable for the Permutation Argument with the RAM Table.
RunningProductJumpStackTable for the Permutation Argument with the Jump Stack Table.
RunningEvaluationHashInput for the Evaluation Argument with the Hash Table for copying the input to the hash function from the processor to the hash coprocessor.
RunningEvaluationHashDigest for the Evaluation Argument with the Hash Table for copying the hash digest from the hash coprocessor to the processor.
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.
U32LookupClientLogDerivative for the Lookup Argument with the U32 Table.
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:

column clk is increased by 1,
column IsPadding is set to 1,
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

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.

Clock Cycle	Current Instruction	st0	…	st15	Running Evaluation “To Hash Table”	Running Evaluation “From Hash Table”
$i - 1$	`foo`	17	…	22	$a$	$b$
$i$	hash	17	…	22	$🚪 \cdot a + \sum_{j} 🧄_{j} \cdot s t_{j}$	$b$
$i + 1$	`bar`	1337	…	22	$🚪 \cdot a + \sum_{j = 0}^{9} 🧄_{j} \cdot s t_{j}$	$🪟 \cdot b + \sum_{j = 0}^{4} 🧄_{j} \cdot s t_{j + 5}$

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

The cycle counter clk is 0.
The instruction pointer ip is 0.
The jump address stack pointer jsp is 0.
The jump address origin jso is 0.
The jump address destination jsd is 0.
The operational stack element st0 is 0.
The operational stack element st1 is 0.
The operational stack element st2 is 0.
The operational stack element st3 is 0.
The operational stack element st4 is 0.
The operational stack element st5 is 0.
The operational stack element st6 is 0.
The operational stack element st7 is 0.
The operational stack element st8 is 0.
The operational stack element st9 is 0.
The operational stack element st10 is 0.
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.
The op_stack_pointer is 16.
RunningEvaluationStandardInput is 1.
RunningEvaluationStandardOutput is 1.
InstructionLookupClientLogDerivative has absorbed the first row with respect to challenges 🥝, 🥥, and 🫐 and indeterminate 🪥.
RunningProductOpStackTable is 1.
RunningProductRamTable has absorbed the first row with respect to challenges 🍍, 🍈, 🍎, and 🌽 and indeterminate 🛋.
RunningProductJumpStackTable has absorbed the first row with respect to challenges 🍇, 🍅, 🍌, 🍏, and 🍐 and indeterminate 🧴.
RunningEvaluationHashInput has absorbed the first row with respect to challenges 🧄₀ through 🧄₉ and indeterminate 🚪 if the current instruction is hash. Otherwise, it is 1.
RunningEvaluationHashDigest is 1.
RunningEvaluationSponge is 1.
U32LookupClientLogDerivative is 0.
ClockJumpDifferenceLookupServerLogDerivative is 0.

Initial Constraints as Polynomials

clk
ip
jsp
jso
jsd
st0
st1
st2
st3
st4
st5
st6
st7
st8
st9
st10
🥬^5 + st11·🥬^4 + st12·🥬^3 + st13·🥬^2 + st14·🥬 + st15 - 🫑
op_stack_pointer - 16
RunningEvaluationStandardInput - 1
RunningEvaluationStandardOutput - 1
InstructionLookupClientLogDerivative · (🪥 - 🥝·ip - 🥥·ci - 🫐·nia) - 1
RunningProductOpStackTable - 1
RunningProductRamTable - (🛋 - 🍍·clk - 🍈·ramp - 🍎·ramv - 🌽·previous_instruction)
RunningProductJumpStackTable - (🧴 - 🍇·clk - 🍅·ci - 🍌·jsp - 🍏·jso - 🍐·jsd)
(ci - opcode(hash))·(RunningEvaluationHashInput - 1)
+ hash_deselector·(RunningEvaluationHashInput - 🚪 - 🧄₀·st0 - 🧄₁·st1 - 🧄₂·st2 - 🧄₃·st3 - 🧄₄·st4 - 🧄₅·st5 - 🧄₆·st6 - 🧄₇·st7 - 🧄₈·st8 - 🧄₉·st9)
RunningEvaluationHashDigest - 1
RunningEvaluationSponge - 1
U32LookupClientLogDerivative
ClockJumpDifferenceLookupServerLogDerivative

Consistency Constraints

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

Consistency Constraints as Polynomials

ci - (2^6·ib6 + 2^5·ib5 + 2^4·ib4 + 2^3·ib3 + 2^2·ib2 + 2^1·ib1 + 2^0·ib0)
ib0·(ib0 - 1)
ib1·(ib1 - 1)
ib2·(ib2 - 1)
ib3·(ib3 - 1)
ib4·(ib4 - 1)
ib5·(ib5 - 1)
ib6·(ib6 - 1)
IsPadding·(IsPadding - 1)
IsPadding·(clk - 1)·ClockJumpDifferenceLookupServerLogDerivative

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.

The cycle counter clk increases by 1.
The padding indicator IsPadding is 0 or remains unchanged.
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.
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 🪞.
The running product for the Jump Stack Table absorbs the next row with respect to challenges 🍇, 🍅, 🍌, 🍏, and 🍐 and indeterminate 🧴.
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 🚪. Otherwise, it remains unchanged.
If the current instruction is hash, the running evaluation “Hash Digest” absorbs the next row with respect to challenges 🧄₀ through 🧄₄ and indeterminate 🪟. Otherwise, it remains unchanged.
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 or sponge_squeeze, then the running evaluation “Sponge” absorbs the current instruction and the next row with respect to challenges 🧅 and 🧄₀ through 🧄₉ and indeterminate 🧽. Otherwise, the running evaluation remains unchanged.
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 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 🧷.
6. 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.

Transition Constraints as Polynomials

clk' - (clk + 1)
IsPadding·(IsPadding' - IsPadding)
(1 - IsPadding') · ((InstructionLookupClientLogDerivative' - InstructionLookupClientLogDerivative) · (🛁 - 🥝·ip' - 🥥·ci' - 🫐·nia') - 1)
+ IsPadding'·(RunningProductInstructionTable' - RunningProductInstructionTable)
(ClockJumpDifferenceLookupServerLogDerivative' - ClockJumpDifferenceLookupServerLogDerivative)
·(🪞 - clk') - cjd_mul'
RunningProductJumpStackTable' - RunningProductJumpStackTable·(🧴 - 🍇·clk' - 🍅·ci' - 🍌·jsp' - 🍏·jso' - 🍐·jsd')
(ci' - opcode(hash))·(RunningEvaluationHashInput' - RunningEvaluationHashInput)
+ hash_deselector'·(RunningEvaluationHashInput' - 🚪·RunningEvaluationHashInput - 🧄₀·st0' - 🧄₁·st1' - 🧄₂·st2' - 🧄₃·st3' - 🧄₄·st4' - 🧄₅·st5' - 🧄₆·st6' - 🧄₇·st7' - 🧄₈·st8' - 🧄₉·st9')
(ci - opcode(hash))·(RunningEvaluationHashDigest' - RunningEvaluationHashDigest)
+ hash_deselector·(RunningEvaluationHashDigest' - 🪟·RunningEvaluationHashDigest - 🧄₀·st5' - 🧄₁·st6' - 🧄₂·st7' - 🧄₃·st8' - 🧄₄·st9')
(ci - opcode(sponge_init))·(ci - opcode(sponge_absorb)·(ci - opcode(sponge_squeeze))·(RunningEvaluationHashDigest' - RunningEvaluationHashDigest)
+ (sponge_init_deselector + sponge_absorb_deselector + sponge_squeeze_deselector)
·(RunningEvaluationSponge' - 🧽·RunningEvaluationSponge - 🧅·ci - 🧄₀·st0' - 🧄₁·st1' - 🧄₂·st2' - 🧄₃·st3' - 🧄₄·st4' - 🧄₅·st5' - 🧄₆·st6' - 🧄₇·st7' - 🧄₈·st8' - 🧄₉·st9')
1. split_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0' - 🌰·st1' - 🥑·ci) - 1)
2. + lt_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0') - 1)
3. + and_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0') - 1)
4. + xor_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0') - 1)
5. + pow_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0') - 1)
6. + log_2_floor_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🥑·ci - 🥕·st0') - 1)
7. + div_mod_deselector·(
  (U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0' - 🌰·st1 - 🥑·opcode(lt) - 🥕·1)·(🧷 - 🥜·st0 - 🌰·st1' - 🥑·opcode(split))
  - (🧷 - 🥜·st0' - 🌰·st1 - 🥑·opcode(lt) - 🥕·1)
  - (🧷 - 🥜·st0 - 🌰·st1' - 🥑·opcode(split))
  )
8. + pop_count_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🥑·ci - 🥕·st0') - 1)
9. + (1 - ib2)·(U32LookupClientLogDerivative' - U32LookupClientLogDerivative)

Terminal Constraints

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

Terminal Constraints as Polynomials

ci

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.

group name	description
`decompose_arg`	instruction's argument held in `nia` is binary decomposed into helper registers `hv0` through `hv3`
`prohibit_illegal_num_words`	constrain the instruction's argument `n` to 1 ⩽ `n` ⩽ 5
`no_io`	the running evaluations for public input & output remain unchanged
`keep_ram`	RAM does not change, i.e., the running product of the Permutation Argument with the RAM Table remains unchanged
`keep_jump_stack`	jump stack does not change, i.e., registers `jsp`, `jso`, and `jsd` do not change
`step_1`	jump stack does not change and instruction pointer `ip` increases by 1
`step_2`	jump stack does not change and instruction pointer `ip` increases by 2
`grow_op_stack`	op stack elements are shifted down by one position, top element of the resulting stack is unconstrained
`grow_op_stack_by_any_of`	op stack elements are shifted down by `n` positions, top `n` elements of the resulting stack are unconstrained, where `n` is the instruction's argument
`unary_operation`	op stack's top-most element is unconstrained, rest of stack remains unchanged
`keep_op_stack`	op stack remains unchanged, i.e., the running product of the Permutation Argument with the Op Stack Table remains unchanged
`binary_operation`	op stack elements starting from `st2` are shifted up by one position, highest two elements of the resulting stack are unconstrained
`shrink_op_stack`	op stack elements starting from `st1` are shifted up by one position
`shrink_op_stack_by_any_of`	op stack elements starting from `stn` are shifted up by one position, where `n` is the instruction's argument

Below figure gives a comprehensive overview over the subset relation between all instruction groups.

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

instruction	`decompose_arg`	`prohibit_illegal_num_words`	`no_io`	`keep_ram`	`keep_jump_stack`	`step_1`	`step_2`	`grow_op_stack`	`grow_op_stack_by_any_of`	`unary_operation`	`keep_op_stack`	`binary_operation`	`shrink_op_stack`	`shrink_op_stack_by_any_of`
`pop` + `n`	x	x	x	x			x							x
`push` + `a`			x	x			x	x
`divine` + `n`	x	x	x	x			x		x
`dup` + `i`	x		x	x			x	x
`swap` + `i`	x		x	x			x
`nop`			x	x		x					x
`skiz`			x	x	x								x
`call` + `d`			x	x							x
`return`			x	x							x
`recurse`			x	x	x						x
`assert`			x	x		x							x
`halt`			x	x		x					x
`read_mem` + `n`	x	x	x				x
`write_mem` + `n`	x	x	x				x
`hash`			x	x		x
`divine_sibling`			x	x		x
`assert_vector`			x	x		x
`sponge_init`			x	x		x
`sponge_absorb`			x	x		x
`sponge_squeeze`			x	x		x
`add`			x	x		x						x
`mul`			x	x		x						x
`invert`			x	x		x				x
`eq`			x	x		x						x
`split`			x	x		x
`lt`			x	x		x						x
`and`			x	x		x						x
`xor`			x	x		x						x
`log_2_floor`			x	x		x				x
`pow`			x	x		x						x
`div_mod`			x	x		x
`pop_count`			x	x		x				x
`xxadd`			x	x		x
`xxmul`			x	x		x
`xinvert`			x	x		x
`xbmul`			x	x		x
`read_io` + `n`	x	x		x			x		x
`write_io` + `n`	x	x		x			x							x

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:

ind_0(hv3, hv2, hv1, hv0) = (1 - hv3)·(1 - hv2)·(1 - hv1)·(1 - hv0)
ind_1(hv3, hv2, hv1, hv0) = (1 - hv3)·(1 - hv2)·(1 - hv1)·hv0
ind_2(hv3, hv2, hv1, hv0) = (1 - hv3)·(1 - hv2)·hv1·(1 - hv0)
ind_3(hv3, hv2, hv1, hv0) = (1 - hv3)·(1 - hv2)·hv1·hv0
ind_4(hv3, hv2, hv1, hv0) = (1 - hv3)·hv2·(1 - hv1)·(1 - hv0)
ind_5(hv3, hv2, hv1, hv0) = (1 - hv3)·hv2·(1 - hv1)·hv0
ind_6(hv3, hv2, hv1, hv0) = (1 - hv3)·hv2·hv1·(1 - hv0)
ind_7(hv3, hv2, hv1, hv0) = (1 - hv3)·hv2·hv1·hv0
ind_8(hv3, hv2, hv1, hv0) = hv3·(1 - hv2)·(1 - hv1)·(1 - hv0)
ind_9(hv3, hv2, hv1, hv0) = hv3·(1 - hv2)·(1 - hv1)·hv0
ind_10(hv3, hv2, hv1, hv0) = hv3·(1 - hv2)·hv1·(1 - hv0)
ind_11(hv3, hv2, hv1, hv0) = hv3·(1 - hv2)·hv1·hv0
ind_12(hv3, hv2, hv1, hv0) = hv3·hv2·(1 - hv1)·(1 - hv0)
ind_13(hv3, hv2, hv1, hv0) = hv3·hv2·(1 - hv1)·hv0
ind_14(hv3, hv2, hv1, hv0) = hv3·hv2·hv1·(1 - hv0)
ind_15(hv3, hv2, hv1, hv0) = hv3·hv2·hv1·hv0

Group `decompose_arg`

Description

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

Polynomials

nia - (8·hv3 + 4·hv2 + 2·hv1 + hv0)
hv0·(hv0 - 1)
hv1·(hv1 - 1)
hv2·(hv2 - 1)
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

The argument is not 0.
The argument is not 6.
The argument is not 7.
The argument is not 8.
The argument is not 9.
The argument is not 10.
The argument is not 11.
The argument is not 12.
The argument is not 13.
The argument is not 14.
The argument is not 15.

Polynomials

ind_0(hv3, hv2, hv1, hv0)
ind_6(hv3, hv2, hv1, hv0)
ind_7(hv3, hv2, hv1, hv0)
ind_8(hv3, hv2, hv1, hv0)
ind_9(hv3, hv2, hv1, hv0)
ind_10(hv3, hv2, hv1, hv0)
ind_11(hv3, hv2, hv1, hv0)
ind_12(hv3, hv2, hv1, hv0)
ind_13(hv3, hv2, hv1, hv0)
ind_14(hv3, hv2, hv1, hv0)
ind_15(hv3, hv2, hv1, hv0)

Group `no_io`

Description

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

Polynomials

RunningEvaluationStandardInput' - RunningEvaluationStandardInput
RunningEvaluationStandardOutput' - RunningEvaluationStandardOutput

Group `keep_ram`

Description

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

Polynomials

RunningProductRamTable' - RunningProductRamTable

Group `keep_jump_stack`

Description

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

Polynomials

jsp' - jsp
jso' - jso
jsd' - jsd

Group `step_1`

Contains all constraints from instruction group keep_jump_stack, and additionally:

Description

The instruction pointer increments by 1.

Polynomials

ip' - (ip + 1)

Group `step_2`

Contains all constraints from instruction group keep_jump_stack, and additionally:

Description

The instruction pointer increments by 2.

Polynomials

ip' - (ip + 2)

Group `grow_op_stack`

Description

The stack element in st0 is moved into st1.
The stack element in st1 is moved into st2.
The stack element in st2 is moved into st3.
The stack element in st3 is moved into st4.
The stack element in st4 is moved into st5.
The stack element in st5 is moved into st6.
The stack element in st6 is moved into st7.
The stack element in st7 is moved into st8.
The stack element in st8 is moved into st9.
The stack element in st9 is moved into st10.
The stack element in st10 is moved into st11.
The stack element in st11 is moved into st12.
The stack element in st12 is moved into st13.
The stack element in st13 is moved into st14.
The stack element in st14 is moved into st15.
The op stack pointer is incremented by 1.
The running product for the Op Stack Table absorbs the current row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤.

Polynomials

st1' - st0
st2' - st1
st3' - st2
st4' - st3
st5' - st4
st6' - st5
st7' - st6
st8' - st7
st9' - st8
st10' - st9
st11' - st10
st12' - st11
st13' - st12
st14' - st13
st15' - st14
op_stack_pointer' - (op_stack_pointer + 1)
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

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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
If n is 1, then the running product with the Op Stack Table accumulates st15.

Group `unary_operation`

Description

The stack element in st1 does not change.
The stack element in st2 does not change.
The stack element in st3 does not change.
The stack element in st4 does not change.
The stack element in st5 does not change.
The stack element in st6 does not change.
The stack element in st7 does not change.
The stack element in st8 does not change.
The stack element in st9 does not change.
The stack element in st10 does not change.
The stack element in st11 does not change.
The stack element in st12 does not change.
The stack element in st13 does not change.
The stack element in st14 does not change.
The stack element in st15 does not change.
The op stack pointer does not change.
The running product for the Op Stack Table remains unchanged.

Polynomials

st1' - st1
st2' - st2
st3' - st3
st4' - st4
st5' - st5
st6' - st6
st7' - st7
st8' - st8
st9' - st9
st10' - st10
st11' - st11
st12' - st12
st13' - st13
st14' - st14
st15' - st15
op_stack_pointer' - op_stack_pointer
RunningProductOpStackTable' - RunningProductOpStackTable

Group `keep_op_stack`

Contains all constraints from instruction group unary_operation, and additionally:

Description

The stack element in st0 does not change.

Polynomials

st0' - st0

Group `binary_operation`

Description

The stack element in st2 is moved into st1.
The stack element in st3 is moved into st2.
The stack element in st4 is moved into st3.
The stack element in st5 is moved into st4.
The stack element in st6 is moved into st5.
The stack element in st7 is moved into st6.
The stack element in st8 is moved into st7.
The stack element in st9 is moved into st8.
The stack element in st10 is moved into st9.
The stack element in st11 is moved into st10.
The stack element in st12 is moved into st11.
The stack element in st13 is moved into st12.
The stack element in st14 is moved into st13.
The stack element in st15 is moved into st14.
The op stack pointer is decremented by 1.
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

st1' - st2
st2' - st3
st3' - st4
st4' - st5
st5' - st6
st6' - st7
st7' - st8
st8' - st9
st9' - st10
st10' - st11
st11' - st12
st12' - st13
st13' - st14
st14' - st15
op_stack_pointer' - (op_stack_pointer - 1)
RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊·ib1 - 🍉·op_stack_pointer' - 🫒·st15')

Group `shrink_op_stack`

Contains all constraints from instruction group binary_operation, and additionally:

Description

The stack element in st1 is moved into st0.

Polynomials

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

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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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

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

Polynomials

st0' - nia

Instruction `divine` + `n`

This instruction is fully constrained by its instruction groups

Instruction `dup` + `i`

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

Description

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

Polynomials

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

Argument i is not 0.
If i is 1, then st0 is moved into st1.
If i is 2, then st0 is moved into st2.
If i is 3, then st0 is moved into st3.
If i is 4, then st0 is moved into st4.
If i is 5, then st0 is moved into st5.
If i is 6, then st0 is moved into st6.
If i is 7, then st0 is moved into st7.
If i is 8, then st0 is moved into st8.
If i is 9, then st0 is moved into st9.
If i is 10, then st0 is moved into st10.
If i is 11, then st0 is moved into st11.
If i is 12, then st0 is moved into st12.
If i is 13, then st0 is moved into st13.
If i is 14, then st0 is moved into st14.
If i is 15, then st0 is moved into st15.
If i is 1, then st1 is moved into st0.
If i is 2, then st2 is moved into st0.
If i is 3, then st3 is moved into st0.
If i is 4, then st4 is moved into st0.
If i is 5, then st5 is moved into st0.
If i is 6, then st6 is moved into st0.
If i is 7, then st7 is moved into st0.
If i is 8, then st8 is moved into st0.
If i is 9, then st9 is moved into st0.
If i is 10, then st10 is moved into st0.
If i is 11, then st11 is moved into st0.
If i is 12, then st12 is moved into st0.
If i is 13, then st13 is moved into st0.
If i is 14, then st14 is moved into st0.
If i is 15, then st15 is moved into st0.
If i is not 1, then st1 does not change.
If i is not 2, then st2 does not change.
If i is not 3, then st3 does not change.
If i is not 4, then st4 does not change.
If i is not 5, then st5 does not change.
If i is not 6, then st6 does not change.
If i is not 7, then st7 does not change.
If i is not 8, then st8 does not change.
If i is not 9, then st9 does not change.
If i is not 10, then st10 does not change.
If i is not 11, then st11 does not change.
If i is not 12, then st12 does not change.
If i is not 13, then st13 does not change.
If i is not 14, then st14 does not change.
If i is not 15, then st15 does not change.
The op stack pointer does not change.
The running product for the Op Stack Table remains unchanged.

Polynomials

ind_0(hv3, hv2, hv1, hv0)
ind_1(hv3, hv2, hv1, hv0)·(st1' - st0)
ind_2(hv3, hv2, hv1, hv0)·(st2' - st0)
ind_3(hv3, hv2, hv1, hv0)·(st3' - st0)
ind_4(hv3, hv2, hv1, hv0)·(st4' - st0)
ind_5(hv3, hv2, hv1, hv0)·(st5' - st0)
ind_6(hv3, hv2, hv1, hv0)·(st6' - st0)
ind_7(hv3, hv2, hv1, hv0)·(st7' - st0)
ind_8(hv3, hv2, hv1, hv0)·(st8' - st0)
ind_9(hv3, hv2, hv1, hv0)·(st9' - st0)
ind_10(hv3, hv2, hv1, hv0)·(st10' - st0)
ind_11(hv3, hv2, hv1, hv0)·(st11' - st0)
ind_12(hv3, hv2, hv1, hv0)·(st12' - st0)
ind_13(hv3, hv2, hv1, hv0)·(st13' - st0)
ind_14(hv3, hv2, hv1, hv0)·(st14' - st0)
ind_15(hv3, hv2, hv1, hv0)·(st15' - 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)
(1 - ind_1(hv3, hv2, hv1, hv0))·(st1' - st1)
(1 - ind_2(hv3, hv2, hv1, hv0))·(st2' - st2)
(1 - ind_3(hv3, hv2, hv1, hv0))·(st3' - st3)
(1 - ind_4(hv3, hv2, hv1, hv0))·(st4' - st4)
(1 - ind_5(hv3, hv2, hv1, hv0))·(st5' - st5)
(1 - ind_6(hv3, hv2, hv1, hv0))·(st6' - st6)
(1 - ind_7(hv3, hv2, hv1, hv0))·(st7' - st7)
(1 - ind_8(hv3, hv2, hv1, hv0))·(st8' - st8)
(1 - ind_9(hv3, hv2, hv1, hv0))·(st9' - st9)
(1 - ind_10(hv3, hv2, hv1, hv0))·(st10' - st10)
(1 - ind_11(hv3, hv2, hv1, hv0))·(st11' - st11)
(1 - ind_12(hv3, hv2, hv1, hv0))·(st12' - st12)
(1 - ind_13(hv3, hv2, hv1, hv0))·(st13' - st13)
(1 - ind_14(hv3, hv2, hv1, hv0))·(st14' - st14)
(1 - ind_15(hv3, hv2, hv1, hv0))·(st15' - st15)
op_stack_pointer' - op_stack_pointer
RunningProductOpStackTable' - RunningProductOpStackTable

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

Helper variable hv1 is the inverse of st0 or 0.
Helper variable hv1 is the inverse of st0 or st0 is 0.
The next instruction nia is decomposed into helper variables hv1 through hv5.
The indicator helper variable hv1 is either 0 or 1. Here, hv1 == 1 means that nia takes an argument.
The helper variable hv2 is either 0 or 1 or 2 or 3.
The helper variable hv3 is either 0 or 1 or 2 or 3.
The helper variable hv4 is either 0 or 1 or 2 or 3.
The helper variable hv5 is either 0 or 1 or 2 or 3.
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:

(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

(st0·hv0 - 1)·hv0
(st0·hv0 - 1)·st0
nia - hv1 - 2·hv2 - 8·hv3 - 32·hv4 - 128·hv5
hv1·(hv1 - 1)
hv2·(hv2 - 1)·(hv2 - 2)·(hv2 - 3)
hv3·(hv3 - 1)·(hv3 - 2)·(hv3 - 3)
hv4·(hv4 - 1)·(hv4 - 2)·(hv4 - 3)
hv5·(hv5 - 1)·(hv5 - 2)·(hv5 - 3)
(ip' - (ip + 1)·st0)
+ ((ip' - (ip + 2))·(st0·hv0 - 1)·(hv1 - 1))
+ ((ip' - (ip + 3))·(st0·hv0 - 1)·hv1)

Helper variable definitions for `skiz`

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

Instruction `call` + `d`

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

Description

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

Polynomials

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

Instruction `return`

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

Description

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

Polynomials

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

Instruction `recurse`

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

Description

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

Polynomials

jsp' - jsp
jso' - jso
jsd' - jsd
ip' - jsd

Instruction `assert`

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

Description

The current top of the stack st0 is 1.

Polynomials

st0 - 1

Instruction `halt`

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

Description

The instruction executed in the following step is instruction halt.

Polynomials

ci' - ci

Instruction `read_mem` + `n`

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

Description

The RAM pointer st0 is decremented by n.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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
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.
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.
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

The RAM pointer st0 is incremented by n.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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

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

Polynomials

st5' - st10
st6' - st11
st7' - st12
st8' - st13
st9' - st14
st10' - st15
op_stack_pointer' - op_stack_pointer + 5
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 `divine_sibling`

Recall that in a Merkle tree, the indices of left (respectively right) leafs have 0 (respectively 1) as their least significant bit. The first two polynomials achieve that helper variable hv0 holds the result of st10 mod 2. The third polynomial sets the new value of st10 to st10 div 2.

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

Description

Helper variable hv0 is either 0 or 1.
If hv0 is 0, then st0 does not change.
If hv0 is 0, then st1 does not change.
If hv0 is 0, then st2 does not change.
If hv0 is 0, then st3 does not change.
If hv0 is 0, then st4 does not change.
If hv0 is 1, then st0 is moved to st5.
If hv0 is 1, then st1 is moved to st6.
If hv0 is 1, then st2 is moved to st7.
If hv0 is 1, then st3 is moved to st8.
If hv0 is 1, then st4 is moved to st9.
st5 is shifted by 1 bit to the right and moved into st10.
st6 is moved into st11
st7 is moved into st12
st8 is moved into st13
st9 is moved into st14
st10 is moved into st15
The op stack pointer grows by 5.
The running product with the Op Stack Table accumulates st11 through st15.

Polynomials

hv0·(hv0 - 1)
(1 - hv0)·(st0' - st0) + hv0·(st5' - st0)
(1 - hv0)·(st1' - st1) + hv0·(st6' - st1)
(1 - hv0)·(st2' - st2) + hv0·(st7' - st2)
(1 - hv0)·(st3' - st3) + hv0·(st8' - st3)
(1 - hv0)·(st4' - st4) + hv0·(st9' - st4)
st10'·2 + hv0 - st5
st11' - st6
st12' - st7
st13' - st8
st14' - st9
st15' - st10
op_stack_pointer' - op_stack_pointer - 5
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)

Helper variable definitions for `divine_sibling`

Since st10 contains the Merkle tree node index,

hv0 holds the result of st10 % 2 (the node index's least significant bit, indicating whether it is a left/right node).

Instruction `assert_vector`

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

Description

st0 is equal to st5.
st1 is equal to st6.
st2 is equal to st7.
st3 is equal to st8.
st4 is equal to st9.
st10 is moved into st5.
st11 is moved into st6.
st12 is moved into st7.
st13 is moved into st8.
st14 is moved into st9.
st15 is moved into st10.
The op stack pointer shrinks by 5.
The running product with the Op Stack Table accumulates next row's st11 through st15.

Polynomials

st5 - st0
st6 - st1
st7 - st2
st8 - st3
st9 - st4
st5' - st10
st6' - st11
st7' - st12
st8' - st13
st9' - st14
st10' - st15
op_stack_pointer' - op_stack_pointer + 5
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

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

Polynomials

st0' - st10
st1' - st11
st2' - st12
st3' - st13
st4' - st14
st5' - st15
op_stack_pointer' - op_stack_pointer + 10
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_squeeze`

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

Description

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

Polynomials

st10' - st0
st11' - st1
st12' - st2
st13' - st3
st14' - st4
st15' - st5
op_stack_pointer' - op_stack_pointer - 10
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

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

Polynomials

st0' - (st0 + st1)

Instruction `mul`

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

Description

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

Polynomials

st0' - st0·st1

Instruction `invert`

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

Description

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

Polynomials

st0'·st0 - 1

Instruction `eq`

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

Description

Helper variable hv0 is the inverse of the difference of the stack's two top-most elements or 0.
Helper variable hv0 is the inverse of the difference of the stack's two top-most elements or the difference is 0.
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

hv0·(hv0·(st1 - st0) - 1)
(st1 - st0)·(hv0·(st1 - st0) - 1)
st0' - (1 - hv0·(st1 - st0))

Helper variable definitions for `eq`

hv0 = inverse(rhs - lhs) if rhs ≠ lhs.
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

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

Polynomials

st0 - (2^32·st1' + st0')
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,

hv0 = (hi - (2^32 - 1)) if lo ≠ 0.
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:

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

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

Description

Numerator is quotient times denominator plus remainder: n == q·d + r.
Stack element st2 does not change.

Polynomials

st0 - st1·st1' - st0'
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 `xxadd`

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

Description

The result of adding st0 to st3 is moved into st0.
The result of adding st1 to st4 is moved into st1.
The result of adding st2 to st5 is moved into st2.
st6 is moved into st3.
st7 is moved into st4.
st8 is moved into st5.
st9 is moved into st6.
st10 is moved into st7.
st11 is moved into st8.
st12 is moved into st9.
st13 is moved into st10.
st14 is moved into st11.
st15 is moved into st12.
The op stack pointer shrinks by 3.
The running product with the Op Stack Table accumulates next row's st13 through st15.

Polynomials

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

Instruction `xxmul`

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

Description

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

Polynomials

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

Instruction `xinvert`

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

Description

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.
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.
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

st0·st0' - st2·st1' - st1·st2' - 1
st1·st0' + st0·st1' - st2·st2' + st2·st1' + st1·st2'
st2·st0' + st1·st1' + st0·st2' + st2·st2'

Instruction `xbmul`

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

Description

The result of multiplying the top of the stack with the X-Field element's coefficient for x^0 is moved into st0.
The result of multiplying the top of the stack with the X-Field element's coefficient for x^1 is moved into st1.
The result of multiplying the top of the stack with the X-Field element's coefficient for x^2 is moved into st2.
st4 is moved into st3.
st5 is moved into st4.
st6 is moved into st5.
st7 is moved into st6.
st8 is moved into st7.
st9 is moved into st8.
st10 is moved into st9.
st11 is moved into st10.
st12 is moved into st11.
st13 is moved into st12.
st14 is moved into st13.
st15 is moved into st14.
The op stack pointer shrinks by 3.
The running product with the Op Stack Table accumulates next row's st15.

Polynomials

st0' - st0·st1
st1' - st0·st2
st2' - st0·st3
st3' - st4
st4' - st5
st5' - stt
st6' - st7
st7' - st8
st8' - st9
st9' - st10
st10' - st11
st11' - st12
st12' - st13
st13' - st14
st14' - st15
op_stack_pointer' - op_stack_pointer + 1
RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk - 🍊 - 🍉·op_stack_pointer' - 🫒·st15')

Instruction `read_io` + `n`

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

Description

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

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

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

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)

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.

Base Columns

The Op Stack Table consists of 4 columns:

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

Clock	Shrink Stack Indicator	Stack Pointer	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:

`clk`	`ci`	`nia`	`st0`	`st1`	`st2`	`st3`	Op Stack Underflow Memory	`op_stack_pointer`
0	push	42	0	0	0	0	[]	4
1	push	43	42	0	0	0	[ 0]	5
2	push	44	43	42	0	0	[ 0, 0]	6
3	push	45	44	43	42	0	[ 0, 0, 0]	7
4	push	46	45	44	43	42	[ 0, 0, 0, 0]	8
5	push	47	46	45	44	43	[42, 0, 0, 0, 0]	9
6	push	48	47	46	45	44	[43, 42, 0, 0, 0, 0]	10
7	nop		48	47	46	45	[44, 43, 42, 0, 0, 0]	11
8	pop		48	47	46	45	[44, 43, 99, 0, 0, 0]	11
9	pop		47	46	45	44	[43, 99, 0, 0, 0, 0]	10
10	pop		46	45	44	43	[99, 0, 0, 0, 0]	9
11	pop		45	44	43	99	[ 0, 0, 0, 0]	8
12	push	77	44	43	99	0	[ 0, 0, 0]	7
13	swap	3	77	44	43	99	[ 0, 0, 0, 0]	8
14	push	78	99	44	43	77	[ 0, 0, 0, 0]	8
15	swap	3	78	99	44	43	[77, 0, 0, 0, 0]	9
16	push	79	43	99	44	78	[77, 0, 0, 0, 0]	9
17	pop		79	43	99	44	[78, 77, 0, 0, 0, 0]	10
18	pop		43	99	44	78	[77, 0, 0, 0, 0]	9
19	pop		99	44	78	77	[ 0, 0, 0, 0]	8
20	pop		44	78	77	0	[ 0, 0, 0]	7
21	pop		78	77	0	0	[ 0, 0]	6
22	pop		77	0	0	0	[ 0]	5
23	halt		0	0	0	0	[]	4

Operational Stack Table:

`clk`	`shrink_stack`	`stack_pointer`	`first_underflow_element`
0	0	4	0
22	1	4	0
1	0	5	0
21	1	5	0
2	0	6	0
20	1	6	0
3	0	7	0
11	1	7	0
12	0	7	0
19	1	7	0
4	0	8	42
10	1	8	99
14	0	8	77
18	1	8	77
5	0	9	43
9	1	9	43
16	0	9	78
17	1	9	78
6	0	10	44
8	1	10	44

Extension Columns

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

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.
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:

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.
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

Initial Constraints

The stack_pointer is the number of available stack registers, i.e., 16.
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.
The logarithmic derivative for the clock jump difference lookup ClockJumpDifferenceLookupClientLogDerivative is 0.

Initial Constraints as Polynomials

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

Consistency Constraints

None.

Transition Constraints

- 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.
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.
If the current row is a padding row, then the next row is a padding row.
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:

The stack_pointer increases by 1 or the stack_pointer does not change.
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.
- 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.
The current row is not a padding row or the next row is a padding row.
- 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

(stack_pointer' - stack_pointer - 1)·(stack_pointer' - stack_pointer)
(stack_pointer' - stack_pointer - 1)·(first_underflow_element' - first_underflow_element)·(shrink_stack' - 0)
(shrink_stack' - 2)·(rppa' - rppa·(🪤 - 🍋·clk' - 🍊·shrink_stack' - 🍉·stack_pointer' - 🫒first_underflow_element'))
+ (shrink_stack' - 0)·(shrink_stack' - 1)·(rppa' - rppa)
(shrink_stack - 0)·(shrink_stack - 1)·(shrink_stack' - 2)
(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.

frequently abbreviated as “Op Stack”

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).

Base Columns

The RAM Table has 7 base columns:

the cycle counter clk,
the executed instruction_type – 0 for “write”, 1 for “read”, 2 for padding rows,
RAM pointer ram_pointer,
RAM value ram_value,
helper variable "inverse of ram_pointer difference" iord,
Bézout coefficient polynomial coefficient 0 bcpc0,
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.

Extension Columns

The RAM Table has 6 extension columns:

RunningProductOfRAMP, accumulating next row's ram_pointer as a root whenever ram_pointer changes between two rows,
FormalDerivative, the (evaluated) formal derivative of RunningProductOfRAMP,
BezoutCoefficient0, the (evaluated) polynomial with base column bcpc0 as coefficients,
BezoutCoefficient1, the (evaluated) polynomial with base column bcpc1 as coefficients,
RunningProductPermArg, the Permutation Argument with the Processor Table, and
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

form contiguous regions of ram_pointer, and
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:

clk	ci	nia	st0	st1	st2	st3	st4	st5
0	push	20
1	push	100	20
2	write_mem	1	100	20
3	pop	1	101
4	push	5
5	push	6	5
6	push	7	6	5
7	push	8	7	6	5
8	push	9	8	7	6	5
9	push	42	9	8	7	6	5
10	write_mem	5	42	9	8	7	6	5
11	pop	1	47
12	push	42
13	read_mem	1	42
14	pop	2	41	9
15	push	45
16	read_mem	3	45
17	pop	4	42	8	7	6
18	push	17
19	push	18	17
20	push	19	18	17
21	push	43	19	18	17
22	write_mem	3	43	19	18	17
23	pop	1	46
24	push	46
25	read_mem	5	46
26	pop	1	41	9	19	18	17	5
27	pop	5	9	19	18	17	5
28	push	42
29	read_mem	1	42
30	pop	2	41	9
31	push	100
32	read_mem	1	100
33	pop	2	99	20
34	halt

RAM Table:

clk	type	pointer	value	iord
10	write	42	9	0
13	read	42	9	0
25	read	42	9	0
29	read	42	9	1
10	write	43	8	0
16	read	43	8	0
22	write	43	19	0
25	read	43	19	1
10	write	44	7	0
16	read	44	7	0
22	write	44	18	0
25	read	44	18	1
10	write	45	6	0
16	read	45	6	0
22	write	45	17	0
25	read	45	17	1
10	write	46	5	0
25	read	46	5	$5 4^{- 1}$
2	write	100	20	0
32	read	100	20	0

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

Initial Constraints

The first coefficient of the Bézout coefficient polynomial 0 bcpc0 is 0.
The Bézout coefficient 0 bc0 is 0.
The Bézout coefficient 1 bc1 is equal to the first coefficient of the Bézout coefficient polynomial bcpc1.
The running product polynomial RunningProductOfRAMP starts with 🧼 - ram_pointer.
The formal derivative starts with 1.
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.
The logarithmic derivative for the clock jump difference lookup ClockJumpDifferenceLookupClientLogDerivative is 0.

Initial Constraints as Polynomials

bcpc0
bc0
bc1 - bcpc1
RunningProductOfRAMP - 🧼 + ram_pointer
FormalDerivative - 1
(RunningProductPermArg - 🛋 - 🍍·clk - 🍈·ram_pointer - 🍎·ram_value - 🌽·previous_instruction)·(instruction_type - 2)
(RunningProductPermArg - 1)·(instruction_type - 1)·(instruction_type - 0)
ClockJumpDifferenceLookupClientLogDerivative

Consistency Constraints

None.

Transition Constraints

If the current row is a padding row, then the next row is a padding row.
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.
The ram_pointer changes or iord is the inverse of the difference between current and next row's ram_pointer.
The ram_pointer changes or instruction_type is “write” or the ram_value remains unchanged.
The bcbp0 changes if and only if the ram_pointer changes.
The bcbp1 changes if and only if the ram_pointer changes.
If the ram_pointer changes, the RunningProductOfRAMP accumulates next ram_pointer.
Otherwise, it remains unchanged.
If the ram_pointer changes, the FormalDerivative updates under the product rule of differentiation.
Otherwise, it remains unchanged.
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.
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.
If the next row is not a padding row, the RunningProductPermArg accumulates the next row.
Otherwise, it remains unchanged.
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.

Transition Constraints as Polynomials

(instruction_type - 0)·(instruction_type - 1)·(instruction_type' - 2)
(iord·(ram_pointer' - ram_pointer) - 1)·iord
(iord·(ram_pointer' - ram_pointer) - 1)·(ram_pointer' - ram_pointer)
(iord·(ram_pointer' - ram_pointer) - 1)·(instruction_type - 0)·(ram_value' - ram_value)
(iord·(ram_pointer' - ram_pointer) - 1)·(bcpc0' - bcpc0)
(iord·(ram_pointer' - ram_pointer) - 1)·(bcpc1' - bcpc1)
(iord·(ram_pointer' - ram_pointer) - 1)·(RunningProductOfRAMP' - RunningProductOfRAMP)
+ (ram_pointer' - ram_pointer)·(RunningProductOfRAMP' - RunningProductOfRAMP·(ram_pointer'-🧼))
(iord·(ram_pointer' - ram_pointer) - 1)·(FormalDerivative' - FormalDerivative)
+ (ram_pointer' - ram_pointer)·(FormalDerivative' - FormalDerivative·(ram_pointer'-🧼) - RunningProductOfRAMP)
(iord·(ram_pointer' - ram_pointer) - 1)·(bc0' - bc0)
+ (ram_pointer' - ram_pointer)·(bc0' - bc0·🧼 - bcpc0')
(iord·(ram_pointer' - ram_pointer) - 1)·(bc1' - bc1)
+ (ram_pointer' - ram_pointer)·(bc1' - bc1·🧼 - bcpc1')
(RunningProductPermArg' - RunningProductPermArg·(🛋 - 🍍·clk' - 🍈·ram_pointer' - 🍎·ram_value' - 🌽·previous_instruction'))·(instruction_type' - 2)
(RunningProductPermArg' - RunningProductPermArg)·(instruction_type - 1)·(instruction_type - 0))
(iord·(ram_pointer' - ram_pointer) - 1)·(instruction_type' - 2)·((ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative) · (🪞 - clk' + clk) - 1)
+ (ram_pointer' - ram_pointer)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)
+ (instruction_type' - 1)·(instruction_type' - 0)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)

Terminal Constraints

The Bézout relation holds between RunningProductOfRAMP, FormalDerivative, bc0, and bc1.

Terminal Constraints as Polynomials

RunningProductOfRAMP·bc0 + FormalDerivative·bc1 - 1

Jump Stack Table

The Jump Stack Memory contains the underflow from the Jump Stack.

Base Columns

The Jump Stack Table consists of 5 columns:

the cycle counter clk
current instruction ci,
the jump stack pointer jsp,
the last jump's origin jso, and
the last jump's destination jsd.

Clock	Current Instruction	Jump Stack Pointer	Jump Stack Origin	Jump Stack Destination
-	-	-	-	-

The rows are sorted by jump stack pointer jsp, then by cycle counter clk. The column jsd contains the destination of stack-extending jump (call) as well as of the no-stack-change jump (recurse); the column jso contains the source of the stack-extending jump (call) or equivalently the destination of the stack-shrinking jump (return).

The AIR for this table guarantees that the return address of a single cell of return address memory can change only if there was a call instruction.

An example program, execution trace, and jump stack table are shown below.

Program:

`address`	`instruction`
`0x00`	`foo`
`0x01`	`bar`
`0x02`	`call`
`0x03`	`0xA0`
`0x04`	`buzz`
`0x05`	`bar`
`0x06`	`call`
`0x07`	`0xB0`
`0x08`	`foo`
`0x09`	`bar`
⋮	⋮
`0xA0`	`buzz`
`0xA1`	`foo`
`0xA2`	`bar`
`0xA3`	`return`
`0xA4`	`foo`
⋮	⋮
`0xB0`	`foo`
`0xB1`	`call`
`0xB2`	`0xC0`
`0xB3`	`return`
`0xB4`	`bazz`
⋮	⋮
`0xC0`	`buzz`
`0xC1`	`foo`
`0xC2`	`bar`
`0xC3`	`return`
`0xC4`	`buzz`

Execution trace:

`clk`	`ip`	`ci`	`nia`	`jsp`	`jso`	`jsd`	jump stack
0	`0x00`	`foo`	`bar`	0	`0x00`	`0x00`	[ ]
1	`0x01`	`bar`	`call`	0	`0x00`	`0x00`	[ ]
2	`0x02`	`call`	`0xA0`	0	`0x00`	`0x00`	[ ]
3	`0xA0`	`buzz`	`foo`	1	`0x04`	`0xA0`	[(`0x04`, `0xA0`)]
4	`0xA1`	`foo`	`bar`	1	`0x04`	`0xA0`	[(`0x04`, `0xA0`)]
5	`0xA2`	`bar`	`return`	1	`0x04`	`0xA0`	[(`0x04`, `0xA0`)]
6	`0xA3`	`return`	`foo`	1	`0x04`	`0xA0`	[(`0x04`, `0xA0`)]
7	`0x04`	`buzz`	`bar`	0	`0x00`	`0x00`	[ ]
8	`0x05`	`bar`	`call`	0	`0x00`	`0x00`	[ ]
9	`0x06`	`call`	`0xB0`	0	`0x00`	`0x00`	[ ]
10	`0xB0`	`foo`	`call`	1	`0x08`	`0xB0`	[(`0x08`, `0xB0`)]
11	`0xB1`	`call`	`0xC0`	1	`0x08`	`0xB0`	[(`0x08`, `0xB0`)]
12	`0xC0`	`buzz`	`foo`	2	`0xB3`	`0xC0`	[(`0x08`, `0xB0`), (`0xB3`, `0xC0`)]
13	`0xC1`	`foo`	`bar`	2	`0xB3`	`0xC0`	[(`0x08`, `0xB0`), (`0xB3`, `0xC0`)]
14	`0xC2`	`bar`	`return`	2	`0xB3`	`0xC0`	[(`0x08`, `0xB0`), (`0xB3`, `0xC0`)]
15	`0xC3`	`return`	`buzz`	2	`0xB3`	`0xC0`	[(`0x08`, `0xB0`), (`0xB3`, `0xC0`)]
16	`0xB3`	`return`	`bazz`	1	`0x08`	`0xB0`	[(`0x08`, `0xB0`)]
17	`0x08`	`foo`	`bar`	0	`0x00`	`0x00`	[ ]

Jump Stack Table:

`clk`	`ci`	`jsp`	`jso`	`jsd`
0	`foo`	0	`0x00`	`0x00`
1	`bar`	0	`0x00`	`0x00`
2	`call`	0	`0x00`	`0x00`
7	`buzz`	0	`0x00`	`0x00`
8	`bar`	0	`0x00`	`0x00`
9	`call`	0	`0x00`	`0x00`
17	`foo`	0	`0x00`	`0x00`
3	`buzz`	1	`0x04`	`0xA0`
4	`foo`	1	`0x04`	`0xA0`
5	`bar`	1	`0x04`	`0xA0`
6	`return`	1	`0x04`	`0xA0`
10	`foo`	1	`0x08`	`0xB0`
11	`call`	1	`0x08`	`0xB0`
16	`return`	1	`0x08`	`0xB0`
12	`buzz`	2	`0xB3`	`0xC0`
13	`foo`	2	`0xB3`	`0xC0`
14	`bar`	2	`0xB3`	`0xC0`
15	`return`	2	`0xB3`	`0xC0`

Extension Columns

The Jump Stack Table has 2 extension columns, rppa and ClockJumpDifferenceLookupClientLogDerivative.

A Permutation Argument establishes that the rows of the Jump Stack Table match with the rows in the Processor Table. The running product for this argument is contained in the rppa column.
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

A padding row is a direct copy of the Jump Stack Table's row with the highest value for column clk, called template row, with the exception of the cycle count column clk. In a padding row, the value of column clk is 1 greater than the value of column clk in the template row. The padding row is inserted right below the template row. These steps are repeated until the desired padded height is reached. In total, above steps ensure that the Permutation Argument between the Jump Stack Table and the Processor Table holds up.

Memory-Consistency

Memory-consistency follows from two more primitive properties:

Contiguity of regions of constant memory pointer. Since the memory pointer for the Jump Stack table, jsp can change by at most one per cycle, it is possible to enforce a full sorting using AIR constraints.
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

Initial Constraints

Cycle count clk is 0.
Jump Stack Pointer jsp is 0.
Jump Stack Origin jso is 0.
Jump Stack Destination jsd is 0.
The running product for the permutation argument with the Processor Table rppa has absorbed the first row with respect to challenges 🍇, 🍅, 🍌, 🍏, and 🍐 and indeterminate 🧴.
The running product of clock jump differences ClockJumpDifferenceLookupClientLogDerivative is 0.

Initial Constraints as Polynomials

clk
jsp
jso
jsd
rppa - (🧴 - 🍇·clk - 🍅·ci - 🍌·jsp - 🍏·jso - 🍐·jsd)
ClockJumpDifferenceLookupClientLogDerivative

Consistency Constraints

None.

Transition Constraints

The jump stack pointer jsp increases by 1, or
(jsp does not change and jso does not change and jsd does not change and the cycle counter clk increases by 1), or
(jsp does not change and jso does not change and jsd does not change and the current instruction ci is call), or
(jsp does not change and the current instruction ci is return).
The running product for the permutation argument rppa absorbs the next row with respect to challenges 🍇, 🍅, 🍌, 🍏, and 🍐 and indeterminate 🧴.
If the jump stack pointer jsp 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 same.

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

The jump stack pointer jsp increases by 1 or the jump stack pointer jsp does not change
The jump stack pointer jsp increases by 1 or the jump stack origin jso does not change or current instruction ci is return
The jump stack pointer jsp increases by 1 or the jump stack destination jsd does not change or current instruction ci is return
The jump stack pointer jsp increases by 1 or the cycle count clk increases by 1 or current instruction ci is call or current instruction ci is return
rppa' - rppa·(🧴 - 🍇·clk' - 🍅·ci' - 🍌·jsp' - 🍏·jso' - 🍐·jsd')
- the jsp changes or the logarithmic derivative accumulates a summand, and
- the jsp does not change or the logarithmic derivative does not change.

Transition Constraints as Polynomials

(jsp' - (jsp + 1))·(jsp' - jsp)
(jsp' - (jsp + 1))·(jso' - jso)·(ci - op_code(return))
(jsp' - (jsp + 1))·(jsd' - jsd)·(ci - op_code(return))
(jsp' - (jsp + 1))·(clk' - (clk + 1))·(ci - op_code(call))·(ci - op_code(return))
clk_di·(jsp' - jsp - 1)·(1 - clk_di·(clk' - clk - one))
(clk' - clk - one)·(jsp' - jsp - 1)·(1 - clk_di·(clk' - clk - one))
rppa' - rppa·(🧴 - 🍇·clk' - 🍅·ci' - 🍌·jsp' - 🍏·jso' - 🍐·jsd')
(jsp' - (jsp + 1))·((ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative) · (🪞 - clk' + clk) - 1)
+ (jsp' - jsp)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)

Terminal Constraints

None.

Hash Table

The instruction hash hashes the Op Stack's 10 top-most elements in one cycle. Similarly, the Sponge instructions sponge_init, sponge_absorb, and sponge_squeeze also all complete in one cycle. The main processor achieves this by using a hash coprocessor. The Hash Table is part of the arithmetization of that coprocessor, the other two parts being the Cascade Table and the Lookup Table. In addition to accelerating these hashing instructions, the Hash Table helps with program attestation by hashing the program.

The arithmetization for instruction hash, the Sponge instructions sponge_init, sponge_absorb, and sponge_squeeze, and for program hashing are quite similar. The main differences are in updates to the state registers between executions of the pseudo-random permutation used in Triton VM, the permutation of Tip5. A summary of the four instructions' mechanics:

Instruction hash
1. sets all the hash coprocessor's rate registers (state_0 through state_9) to equal the processor's stack registers state_0 through state_9,
2. sets all the hash coprocessor's capacity registers (state_10 through state_15) to 1,
3. executes the 5 rounds of the Tip5 permutation,
4. overwrites the processor's stack registers state_0 through state_4 with 0, and
5. overwrites the processor's stack registers state_5 through state_9 with the hash coprocessor's registers state_0 through state_4.
Instruction sponge_init
1. sets all the hash coprocessor's registers (state_0 through state_15) to 0.
Instruction sponge_absorb
1. overwrites the hash coprocessor's rate registers (state_0 through state_9) with the processor's stack registers state_0 through state_9, and
2. executes the 5 rounds of the Tip5 permutation.
Instruction sponge_squeeze
1. overwrites the processor's stack registers state_0 through state_9 with the hash coprocessor's rate registers (state_0 through state_9), and
2. executes the 5 rounds of the Tip5 permutation.

Program hashing happens in the initialization phase of Triton VM. The to-be-executed program has no control over it. Program hashing is mechanically identical to performing instruction sponge_absorb as often as is necessary to hash the entire program. A notable difference is the source of the to-be-absorbed elements: they come from program memory, not the processor (which is not running yet). Once all instructions have been absorbed, the resulting digest is checked against the publicly claimed digest.

Due to the various similar but distinct tasks of the Hash Table, it has an explicit Mode register. The four separate modes are program_hashing, sponge, hash, and pad, and they evolve in that order. Changing the mode is only possible when the permutation has been applied in full, i.e., when the round number is 5. Once mode pad is reached, it is not possible to change the mode anymore. It is not possible to skip mode program_hashing: the program is always hashed. Skipping any or all of the modes sponge, hash, or pad is possible in principle:

if no Sponge instructions are executed, mode sponge will be skipped,
if no hash instruction is executed, mode hash will be skipped, and
if the Hash Table does not require any padding, mode pad will be skipped.

The distinct modes translate into distinct sections in the Hash Table, which are recorded in order: First, the entire Sponge's transition of hashing the program is recorded. Then, the Hash Table records all Sponge instructions in the order the processor executed them. Then, the Hash Table records all hash instructions in the order the processor executed them. Lastly, as many padding rows as necessary are inserted. In total, this separation allows the processor to execute hash instructions without affecting the Sponge's state, and keeps program hashing independent from both.

Note that state_0 through state_3, corresponding to those states that are being split-and-looked-up in the Tip5 permutation, are not stored as a single field element. Instead, four limbs “highest”, “mid high”, “mid low”, and “lowest” are recorded in the Hash Table. This (basically) corresponds to storing the result of $σ (R \cdot state_element)$ . In the Hash Table, the resulting limbs are 16 bit wide, and hence, there are only 4 limbs; the split into 8-bit limbs happens in the Cascade Table. For convenience, this document occasionally refers to those states as if they were a single register. This is an alias for $(2^{48} \cdot state_i_highest_lkin + 2^{32} \cdot state_i_mid_high_lkin + 2^{16} \cdot state_i_mid_low_lkin + state_i_lowest_lkin) \cdot R^{- 1}$ .

Base Columns

The Hash Table has 67 base columns:

The Mode indicator, as described above. It takes value
- $1$ for mode program_hashing,
- $2$ for mode sponge,
- $3$ for mode hash, and
- $0$ for mode pad.
Current instruction CI, holding the instruction the processor is currently executing. This column is only relevant for mode sponge.
Round number indicator round_no, which can be one of ${0, \dots, 5}$ . The Tip5 permutation has 5 rounds, indexed ${0, \dots, 4}$ . The round number 5 indicates that the Tip5 permutation has been applied in full.
16 columns state_i_highest_lkin, state_i_mid_high_lkin, state_i_mid_low_lkin, state_i_lowest_lkin for the to-be-looked-up value of state_0 through state_4, each of which holds one 16-bit wide limb.
16 columns state_i_highest_lkout, state_i_mid_high_lkout, state_i_mid_low_lkout, state_i_lowest_lkout for the looked-up value of state_0 through state_4, each of which holds one 16-bit wide limb.
12 columns state_5 through state_15.
4 columns state_i_inv establishing correct decomposition of state_0_*_lkin through state_3_*_lkin into 16-bit wide limbs.
16 columns constant_i, which hold the round constant for the round indicated by RoundNumber, or 0 if no round with this round number exists.

Extension Columns

The Hash Table has 20 extension columns:

RunningEvaluationReceiveChunk for the Evaluation Argument for copying chunks of size $rate$ from the Program Table. Relevant for program attestation.
RunningEvaluationHashInput for the Evaluation Argument for copying the input to the hash function from the processor to the hash coprocessor,
RunningEvaluationHashDigest for the Evaluation Argument for copying the hash digest from the hash coprocessor to the processor,
RunningEvaluationSponge for the Evaluation Argument 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,
16 columns state_i_limb_LookupClientLogDerivative (for i $\in {0, \dots, 3}$ and limb $\in {$ highest, mid_high, mid_low, lowest $}$ ) establishing correct lookup of the respective limbs in the Cascade Table.

Padding

Each padding row is the all-zero row with the exception of

CI, which is the opcode of instruction hash,
state_i_inv for i $\in {0, \dots, 3}$ , which is $(2^{32} - 1)^{- 1}$ , and
constant_i for i $\in {0, \dots, 15}$ , which is the ith constant for round 0.

Arithmetic Intermediate Representation

Initial Constraints

The Mode is program_hashing.
The round number is 0.
RunningEvaluationReceiveChunk has absorbed the first chunk of instructions with respect to indeterminate 🪣.
RunningEvaluationHashInput is 1.
RunningEvaluationHashDigest is 1.
RunningEvaluationSponge is 1.
For i $\in {0, \dots, 3}$ and limb $\in {$ highest, mid_high, mid_low, lowest $}$ :
state_i_limb_LookupClientLogDerivative has accumulated state_i_limb_lkin and state_i_limb_lkout with respect to challenges 🍒, 🍓 and indeterminate 🧺.

Initial Constraints as Polynomials

Mode - 1
round_no
RunningEvaluationReceiveChunk - 🪣 - (🪑^10 + state_0·🪑^9 + state_1·🪑^8 + state_2·🪑^7 + state_3·🪑^6 + state_4·🪑^5 + state_5·🪑^4 + state_6·🪑^3 + state_7·🪑^2 + state_8·🪑 + state_9)
RunningEvaluationHashInput - 1
RunningEvaluationHashDigest - 1
RunningEvaluationSponge - 1
For i $\in {0, \dots, 3}$ and limb $\in {$ highest, mid_high, mid_low, lowest $}$ :
state_i_limb_LookupClientLogDerivative·(🧺 - 🍒·state_i_limb_lkin - 🍓·state_i_limb_lkout) - 1

Consistency Constraints

The Mode is a valid mode, i.e., $\in {0, \dots, 3}$ .
If the Mode is program_hashing, hash, or pad, then the current instruction is the opcode of hash.
If the Mode is sponge, then the current instruction is a Sponge instruction.
If the Mode is pad, then the round_no is 0.
If the current instruction CI is sponge_init, then the round_no is 0.
For i $\in {10, \dots, 15}$ : If the current instruction CI is sponge_init, then register state_i is 0. (Note: the remaining registers, corresponding to the rate, are guaranteed to be 0 through the Evaluation Argument “Sponge” with the processor.)
For i $\in {10, \dots, 15}$ : If the round number is 0 and the current Mode is hash, then register state_i is 1.
For i $\in {0, \dots, 3}$ : ensure that decomposition of state_i is unique. That is, if both high limbs of state_i are the maximum value, then both low limbs are 0¹. To make the corresponding polynomials low degree, register state_i_inv holds the inverse-or-zero of the re-composed highest two limbs of state_i subtracted from their maximum value. Let state_i_hi_limbs_minus_2_pow_32 be an alias for that difference: state_i_hi_limbs_minus_2_pow_32 $:= 2^{32} - 1 - 2^{16} \cdot$ state_i_highest_lk_in $-$ state_i_mid_high_lk_in.
1. If the two high limbs of state_i are both the maximum possible value, then the two low limbs of state_i are both 0.
2. The state_i_inv is the inverse of state_i_hi_limbs_minus_2_pow_32 or state_i_inv is 0.
3. The state_i_inv is the inverse of state_i_hi_limbs_minus_2_pow_32 or state_i_hi_limbs_minus_2_pow_32 is 0.
The round constants adhere to the specification of Tip5.

Consistency Constraints as Polynomials

(Mode - 0)·(Mode - 1)·(Mode - 2)·(Mode - 3)
(Mode - 2)·(CI - opcode(hash))
(Mode - 0)·(Mode - 1)·(Mode - 3)
·(CI - opcode(sponge_init))·(CI - opcode(sponge_absorb))·(CI - opcode(sponge_squeeze))
(Mode - 1)·(Mode - 2)·(Mode - 3)·(round_no - 0)
(CI - opcode(hash))·(CI - opcode(sponge_absorb))·(CI - opcode(sponge_squeeze))·(round_no - 0)
For i $\in {10, \dots, 15}$ :
·(CI - opcode(hash))·(CI - opcode(sponge_absorb))·(CI - opcode(sponge_squeeze))
·(state_i - 0)
For i $\in {10, \dots, 15}$ :
(round_no - 1)·(round_no - 2)·(round_no - 3)·(round_no - 4)·(round_no - 5)
·(Mode - 0)·(Mode - 1)·(Mode - 2)
·(state_i - 1)
For i $\in {0, \dots, 3}$ : define state_i_hi_limbs_minus_2_pow_32 := 2^32 - 1 - 2^16·state_i_highest_lk_in - state_i_mid_high_lk_in.
1. (1 - state_i_inv · state_i_hi_limbs_minus_2_pow_32)·(2^16·state_i_mid_low_lk_in + state_i_lowest_lk_in)
2. (1 - state_i_inv · state_i_hi_limbs_minus_2_pow_32)·state_i_inv
3. (1 - state_i_inv · state_i_hi_limbs_minus_2_pow_32)·state_i_hi_limbs_minus_2_pow_32

Transition Constraints

If the round_no is 5, then the round_no in the next row is 0.
If the Mode is not pad and the current instruction CI is not sponge_init and the round_no is not 5, then the round_no increments by 1.
If the Mode in the next row is program_hashing and the round_no in the next row is 0, then receive a chunk of instructions with respect to challenges 🪣 and 🪑.
If the Mode changes from program_hashing, then the Evaluation Argument of state_0 through state_4 with respect to indeterminate 🥬 equals the public program digest challenge, 🫑.
If the Mode is program_hashing and the Mode in the next row is sponge, then the current instruction in the next row is sponge_init.
If the round_no is not 5 and the current instruction CI is not sponge_init, then the current instruction does not change.
If the round_no is not 5 and the current instruction CI is not sponge_init, then the Mode does not change.
If the Mode is sponge, then the Mode in the next row is sponge or hash or pad.
If the Mode is hash, then the Mode in the next row is hash or pad.
If the Mode is pad, then the Mode in the next row is pad.
If the round_no in the next row is 0 and the Mode in the next row is either program_hashing or sponge and the instruction in the next row is either sponge_absorb or sponge_init, then the capacity's state registers don't change.
If the round_no in the next row is 0 and the current instruction in the next row is sponge_squeeze, then none of the state registers change.
If the round_no in the next row is 0 and the Mode in the next row is hash, then RunningEvaluationHashInput accumulates the next row with respect to challenges 🧄₀ through 🧄₉ and indeterminate 🚪. Otherwise, it remains unchanged.
If the round_no in the next row is 5 and the Mode in the next row is hash, then RunningEvaluationHashDigest accumulates the next row with respect to challenges 🧄₀ through 🧄₄ and indeterminate 🪟. Otherwise, it remains unchanged.
If the round_no in the next row is 0 and the Mode in the next row is sponge, then RunningEvaluationSponge accumulates the next row with respect to challenges 🧅 and 🧄₀ through 🧄₉ and indeterminate 🧽. Otherwise, it remains unchanged.
For i $\in {0, \dots, 3}$ and limb $\in {$ highest, mid_high, mid_low, lowest $}$ :
If the next round number is not 5 and the mode in the next row is not pad and the current instruction CI in the next row is not sponge_init, then state_i_limb_LookupClientLogDerivative has accumulated state_i_limb_lkin' and state_i_limb_lkout' with respect to challenges 🍒, 🍓 and indeterminate 🧺. Otherwise, state_i_limb_LookupClientLogDerivative remains unchanged.
For r $\in {0, \dots, 4}$ :
If the round_no is r, the state registers adhere to the rules of applying round r of the Tip5 permutation.

Transition Constraints as Polynomials

(round_no - 0)·(round_no - 1)·(round_no - 2)·(round_no - 3)·(round_no - 4)·(round_no' - 0)
(Mode - 0)·(round_no - 5)·(CI - opcode(sponge_init))·(round_no' - round_no - 1)
RunningEvaluationReceiveChunk' - 🪣·RunningEvaluationReceiveChunk - (🪑^10 + state_0·🪑^9 + state_1·🪑^8 + state_2·🪑^7 + state_3·🪑^6 + state_4·🪑^5 + state_5·🪑^4 + state_6·🪑^3 + state_7·🪑^2 + state_8·🪑 + state_9)
(Mode - 0)·(Mode - 2)·(Mode - 3)·(Mode' - 1)·(🥬^5 + state_0·🥬^4 + state_1·🥬^3 + state_2·🥬^2 + state_3·🥬^1 + state_4 - 🫑)
(Mode - 0)·(Mode - 2)·(Mode - 3)·(Mode' - 2)·(CI' - opcode(sponge_init))
(round_no - 5)·(CI - opcode(sponge_init))·(CI' - CI)
(round_no - 5)·(CI - opcode(sponge_init))·(Mode' - Mode)
(Mode - 0)·(Mode - 1)·(Mode - 3)·(Mode' - 0)·(Mode' - 2)·(Mode' - 3)
(Mode - 0)·(Mode - 1)·(Mode - 2)·(Mode' - 0)·(Mode' - 3)
(Mode - 1)·(Mode - 2)·(Mode - 3)·(Mode' - 0)
(round_no' - 1)·(round_no' - 2)·(round_no' - 3)·(round_no' - 4)·(round_no' - 5)
·(Mode' - 3)·(Mode' - 0)
·(CI' - opcode(sponge_init))
·(🧄₁₀·(state_10' - state_10) + 🧄₁₁·(state_11' - state_11) + 🧄₁₂·(state_12' - state_12) + 🧄₁₃·(state_13' - state_13) + 🧄₁₄·(state_14' - state_14) + 🧄₁₅·(state_15' - state_15))
(round_no' - 1)·(round_no' - 2)·(round_no' - 3)·(round_no' - 4)·(round_no' - 5)
·(CI' - opcode(hash))·(CI' - opcode(sponge_init))·(CI' - opcode(sponge_absorb))
·(🧄₀·(state_0' - state_0) + 🧄₁·(state_1' - state_1) + 🧄₂·(state_2' - state_2) + 🧄₃·(state_3' - state_3) + 🧄₄·(state_4' - state_4)
+ 🧄₅·(state_5' - state_5) + 🧄₆·(state_6' - state_6) + 🧄₇·(state_7' - state_7) + 🧄₈·(state_8' - state_8) + 🧄₉·(state_9' - state_9)
+ 🧄₁₀·(state_10' - state_10) + 🧄₁₁·(state_11' - state_11) + 🧄₁₂·(state_12' - state_12) + 🧄₁₃·(state_13' - state_13) + 🧄₁₄·(state_14' - state_14) + 🧄₁₅·(state_15' - state_15))
(round_no' - 0)·(round_no' - 1)·(round_no' - 2)·(round_no' - 3)·(round_no' - 4)
·(RunningEvaluationHashInput' - 🚪·RunningEvaluationHashInput - 🧄₀·state_0' - 🧄₁·state_1' - 🧄₂·state_2' - 🧄₃·state_3' - 🧄₄·state_4' - 🧄₅·state_5' - 🧄₆·state_6' - 🧄₇·state_7' - 🧄₈·state_8' - 🧄₉·state_9')
+ (round_no' - 0)·(RunningEvaluationHashInput' - RunningEvaluationHashInput)
+ (Mode' - 3)·(RunningEvaluationHashInput' - RunningEvaluationHashInput)
(round_no' - 0)·(round_no' - 1)·(round_no' - 2)·(round_no' - 3)·(round_no' - 4)
·(Mode' - 0)·(Mode' - 1)·(Mode' - 2)
·(RunningEvaluationHashDigest' - 🪟·RunningEvaluationHashDigest - 🧄₀·state_0' - 🧄₁·state_1' - 🧄₂·state_2' - 🧄₃·state_3' - 🧄₄·state_4')
+ (round_no' - 5)·(RunningEvaluationHashDigest' - RunningEvaluationHashDigest)
+ (Mode' - 3)·(RunningEvaluationHashDigest' - RunningEvaluationHashDigest)
(round_no' - 1)·(round_no' - 2)·(round_no' - 3)·(round_no' - 4)·(round_no' - 5)
·(CI' - opcode(hash))
·(RunningEvaluationSponge' - 🧽·RunningEvaluationSponge - 🧅·CI' - 🧄₀·state_0' - 🧄₁·state_1' - 🧄₂·state_2' - 🧄₃·state_3' - 🧄₄·state_4' - 🧄₅·state_5' - 🧄₆·state_6' - 🧄₇·state_7' - 🧄₈·state_8' - 🧄₉·state_9')
+ (RunningEvaluationSponge' - RunningEvaluationSponge)·(round_no' - 0)
+ (RunningEvaluationSponge' - RunningEvaluationSponge)·(CI' - opcode(sponge_init))·(CI' - opcode(sponge_absorb))·(CI' - opcode(sponge_squeeze))
For i $\in {0, \dots, 3}$ and limb $\in {$ highest, mid_high, mid_low, lowest $}$ :
(round_no' - 5)·(Mode' - 0)·(CI' - opcode(sponge_init))·((state_i_limb_LookupClientLogDerivative' - state_i_limb_LookupClientLogDerivative)·(🧺 - 🍒·state_i_limb_lkin' - 🍓·state_i_limb_lkout') - 1)
+ (round_no' - 0)·(round_no' - 1)·(round_no' - 2)·(round_no' - 3)·(round_no' - 4)
·(state_i_limb_LookupClientLogDerivative' - state_i_limb_LookupClientLogDerivative)
+ (CI' - opcode(hash))·(CI' - opcode(sponge_absorb))·(CI' - opcode(sponge_squeeze))
·(state_i_limb_LookupClientLogDerivative' - state_i_limb_LookupClientLogDerivative)
The remaining constraints are left as an exercise to the reader. For hints, see the Tip5 paper.

Terminal Constraints

If the Mode is program_hashing, then the Evaluation Argument of state_0 through state_4 with respect to indeterminate 🥬 equals the public program digest challenge, 🫑.
If the Mode is not pad and the current instruction CI is not sponge_init, then the round_no is 5.

Terminal Constraints as Polynomials

🥬^5 + state_0·🥬^4 + state_1·🥬^3 + state_2·🥬^2 + state_3·🥬 + state_4 - 🫑
(Mode - 0)·(CI - opcode(sponge_init))·(round_no - 5)

This is a special property of the Oxfoi prime.

Cascade Table

The Cascade Table helps arithmetizing the lookups necessary for the split-and-lookup S-box used in the Tip5 permutation. The main idea is to allow the Hash Table to look up limbs that are 16 bit wide even though the S-box is defined over limbs that are 8 bit wide. The Cascade Table facilitates the translation of limb widths. For the actual lookup of the 8-bit limbs, the Lookup Table is used. For a more detailed explanation and in-depth analysis, see the Tip5 paper.

Base Columns

The Cascade Table has 6 base columns:

name	description
`IsPadding`	Indicator for padding rows.
`LookInHi`	The more significant bits of the lookup input.
`LookInLo`	The less significant bits of the lookup input.
`LookOutHi`	The more significant bits of the lookup output.
`LookOutLo`	The less significant bits of the lookup output.
`LookupMultiplicity`	The number of times the value is looked up by the Hash Table.

Extension Columns

The Cascade Table has 2 extension columns:

HashTableServerLogDerivative, the (running sum of the) logarithmic derivative for the Lookup Argument with the Hash Table. In every row, the sum accumulates LookupMultiplicity / (🧺 - Combo) where 🧺 is a verifier-supplied challenge and Combo is the weighted sum of LookInHi · 2^8 + LookInLo and LookOutHi · 2^8 + LookOutLo with weights 🍒 and 🍓 supplied by the verifier.
LookupTableClientLogDerivative, the (running sum of the) logarithmic derivative for the Lookup Argument with the Lookup Table. In every row, the sum accumulates the two summands
1. 1 / combo_hi where combo_hi is the verifier-weighted combination of LookInHi and LookOutHi, and
2. 1 / combo_lo where combo_lo is the verifier-weighted combination of LookInLo and LookOutLo.

Padding

Each padding row is the all-zero row with the exception of IsPadding, which is 1.

Arithmetic Intermediate Representation

Initial Constraints

If the first row is not a padding row, then HashTableServerLogDerivative has accumulated the first row with respect to challenges 🍒 and 🍓 and indeterminate 🧺. Else, HashTableServerLogDerivative is 0.
If the first row is not a padding row, then LookupTableClientLogDerivative has accumulated the first row with respect to challenges 🥦 and 🥒 and indeterminate 🪒. Else, LookupTableClientLogDerivative is 0.

Initial Constraints as Polynomials

(1 - IsPadding)·(HashTableServerLogDerivative·(🧺 - 🍒·(2^8·LookInHi + LookInLo) - 🍓·(2^8 · LookOutHi + LookOutLo)) - LookupMultiplicity)
+ IsPadding · HashTableServerLogDerivative
(1 - IsPadding)·(LookupTableClientLogDerivative·(🪒 - 🥦·LookInLo - 🥒·LookOutLo)·(🪒 - 🥦·LookInHi - 🥒·LookOutHi) - 2·🪒 + 🥦·(LookInLo + LookInHi) + 🥒·(LookOutLo + LookOutHi))
+ IsPadding·LookupTableClientLogDerivative

Consistency Constraints

IsPadding is 0 or 1.

Consistency Constraints as Polynomials

IsPadding·(1 - IsPadding)

Transition Constraints

If the current row is a padding row, then the next row is a padding row.
If the next row is not a padding row, then HashTableServerLogDerivative accumulates the next row with respect to challenges 🍒 and 🍓 and indeterminate 🧺. Else, HashTableServerLogDerivative remains unchanged.
If the next row is not a padding row, then LookupTableClientLogDerivative accumulates the next row with respect to challenges 🥦 and 🥒 and indeterminate 🪒. Else, LookupTableClientLogDerivative remains unchanged.

Transition Constraints as Polynomials

IsPadding·(1 - IsPadding')
(1 - IsPadding')·((HashTableServerLogDerivative' - HashTableServerLogDerivative)·(🧺 - 🍒·(2^8·LookInHi' + LookInLo') - 🍓·(2^8 · LookOutHi' + LookOutLo')) - LookupMultiplicity')
+ IsPadding'·(HashTableServerLogDerivative' - HashTableServerLogDerivative)
(1 - IsPadding')·((LookupTableClientLogDerivative' - LookupTableClientLogDerivative)·(🪒 - 🥦·LookInLo' - 🥒·LookOutLo')·(🪒 - 🥦·LookInHi' - 🥒·LookOutHi') - 2·🪒 + 🥦·(LookInLo' + LookInHi') + 🥒·(LookOutLo' + LookOutHi'))
+ IsPadding'·(LookupTableClientLogDerivative' - LookupTableClientLogDerivative)

Terminal Constraints

None.

Lookup Table

The Lookup Table helps arithmetizing the lookups necessary for the split-and-lookup S-box used in the Tip5 permutation. It works in tandem with the Cascade Table. In the language of the Tip5 paper, it is a “narrow lookup table.” This means it is always fully populated, independent of the actual number of lookups.

Correct creation of the Lookup Table is guaranteed through a public-facing Evaluation Argument: after sampling some challenge $X$ , the verifier computes the terminal of the Evaluation Argument over the list of all the expected lookup values with respect to challenge $X$ . The equality of this verifier-supplied terminal against the similarly computed, in-table part of the Evaluation Argument is checked by the Lookup Table's terminal constraint.

Base Columns

The Lookup Table has 4 base columns:

name	description
`IsPadding`	Indicator for padding rows.
`LookIn`	The lookup input.
`LookOut`	The lookup output.
`LookupMultiplicity`	The number of times the value is looked up.

Extension Columns

The Lookup Table has 2 extension columns:

CascadeTableServerLogDerivative, the (running sum of the) logarithmic derivative for the Lookup Argument with the Cascade Table. In every row, accumulates the summand LookupMultiplicity / Combo where Combo is the verifier-weighted combination of LookIn and LookOut.
PublicEvaluationArgument, the running sum for the public evaluation argument of the Lookup Table. In every row, accumulates LookOut.

Padding

Each padding row is the all-zero row with the exception of IsPadding, which is 1.

Arithmetic Intermediate Representation

Initial Constraints

LookIn is 0.
CascadeTableServerLogDerivative has accumulated the first row with respect to challenges 🍒 and 🍓 and indeterminate 🧺.
PublicEvaluationArgument has accumulated the first LookOut with respect to indeterminate 🧹.

Initial Constraints as Polynomials

LookIn
CascadeTableServerLogDerivative·(🧺 - 🍒·LookIn - 🍓·LookOut) - LookupMultiplicity
PublicEvaluationArgument - 🧹 - LookOut

Consistency Constraints

IsPadding is 0 or 1.

Consistency Constraints as Polynomials

IsPadding·(1 - IsPadding)

Transition Constraints

If the current row is a padding row, then the next row is a padding row.
If the next row is not a padding row, LookIn increments by 1. Else, LookIn is 0.
If the next row is not a padding row, CascadeTableServerLogDerivative accumulates the next row with respect to challenges 🍒 and 🍓 and indeterminate 🧺. Else, CascadeTableServerLogDerivative remains unchanged.
If the next row is not a padding row, PublicEvaluationArgument accumulates the next LookOut with respect to indeterminate 🧹. Else, PublicEvaluationArgument remains unchanged.

Transition Constraints as Polynomials

IsPadding·(1 - IsPadding')
((1 - IsPadding')·(LookIn' - LookIn - 1))
+ IsPadding'·LookIn'
(1 - IsPadding')·((CascadeTableServerLogDerivative' - CascadeTableServerLogDerivative)·(🧺 - 🍒·LookIn' - 🍓·LookOut') - LookupMultiplicity')
+ IsPadding'·(CascadeTableServerLogDerivative' - CascadeTableServerLogDerivative)
(1 - IsPadding')·((PublicEvaluationArgument' - PublicEvaluationArgument)·(🧹 - lookup_output'))
+ IsPadding'·(PublicEvaluationArgument' - PublicEvaluationArgument)

Terminal Constraints

PublicEvaluationArgument matches verifier-supplied challenge 🪠.

Terminal Constraints as Polynomials

PublicEvaluationArgument - 🪠

U32 Table

The U32 Operations Table arithmetizes the coprocessor for “difficult” 32-bit unsigned integer operations. The two inputs to the U32 Operations Table are left-hand side (LHS) and right-hand side (RHS), usually corresponding to the processor's st0 and st1, respectively. (For more details see the arithmetization of the specific u32 instructions further below.)

To allow efficient arithmetization, a u32 instruction's result is constructed using multiple rows. The collection of rows arithmetizing the execution of one instruction is called a section. The U32 Table's sections are independent of each other. The processor's current instruction CI is recorded within the section and dictates its arithmetization.

Crucially, the rows of the U32 table are independent of the processor's clock. Hence, the result of the instruction can be transferred into the processor within one clock cycle.

Base Columns

name	description
`CopyFlag`	The row to be copied between processor and u32 coprocessor. Marks the beginning of a section.
`CI`	Current instruction, the instruction the processor is currently executing.
`Bits`	The number of bits that LHS and RHS have already been shifted by.
`BitsMinus33Inv`	The inverse-or-zero of the difference between 33 and `Bits`.
`LHS`	Left-hand side of the operation. Usually corresponds to the processor's `st0`.
`LhsInv`	The inverse-or-zero of LHS. Needed to check whether `LHS` is unequal to 0.
`RHS`	Right-hand side of the operation. Usually corresponds to the processor's `st1`.
`RhsInv`	The inverse-or-zero of RHS. Needed to check whether `RHS` is unequal to 0.
`Result`	The result (or intermediate result) of the instruction requested by the processor.
`LookupMultiplicity`	The number of times the processor has executed the current instruction with the same arguments.

An example U32 Table follows. Some columns are omitted for presentation reasons. All cells in the U32 Table contain elements of the B-field. For clearer illustration of the mechanics, the columns marked “ $_{2}$ ” are presented in base 2, whereas columns marked “ $_{10}$ ” are in the usual base 10.

CopyFlag $_{2}$	CI	Bits $_{10}$	LHS $_{2}$	RHS $_{2}$	Result $_{2}$	Result $_{10}$
1	and	0	11000	11010	11000	24
0	and	1	1100	1101	1100	12
0	and	2	110	110	110	6
0	and	3	11	11	11	3
0	and	4	1	1	1	1
0	and	5	0	0	0	0
1	pow	0	10	101	100000	32
0	pow	1	10	10	100	4
0	pow	2	10	1	10	2
0	pow	3	10	0	1	1
1	log_2_floor	0	100110	0	101	5
0	log_2_floor	1	10011	0	101	5
0	log_2_floor	2	1001	0	101	5
0	log_2_floor	3	100	0	101	5
0	log_2_floor	4	10	0	101	5
0	log_2_floor	5	1	0	101	5
0	log_2_floor	6	0	0	-1	-1
1	lt	0	11111	11011	0	0
0	lt	1	1111	1101	0	0
0	lt	2	111	110	0	0
0	lt	3	11	11	10	2
0	lt	4	1	1	10	2
0	lt	5	0	0	10	2

The AIR verifies the correct update of each consecutive pair of rows. For most instructions, the current least significant bit of both LHS and RHS is eliminated between two consecutive rows. This eliminated bit is used to successively build the required result in the Result column. For instruction pow, only the least significant bit RHS is eliminated, while LHS remains unchanged throughout the section.

There are 6 instructions the U32 Table is “aware” of: split, lt, and, log_2_floor, pow, and pop_count. The instruction split uses the U32 Table for range checking only. Concretely, the U32 Table ensures that the instruction split's resulting “high bits” and “low bits” each fit in a u32. Since the processor does not expect any result from instruction split, the Result must be 0 else the Lookup Argument fails. Similarly, for instructions log_2_floor and pop_count, the processor always sets the RHS to 0.

For instruction xor, the processor requests the computation of the two arguments' and and converts the result using the following equality:

$a xor b = a + b - 2 \cdot (a and b)$

Credit for this trick goes, to the best of our knowledge, to Daniel Lubarov.

For the remaining u32 instruction div_mod, the processor triggers the creation of two sections in the U32 Table:

One section to ensure that the remainder r is smaller than the divisor d. The processor requests the result of lt by setting the U32 Table's CI register to the opcode of lt. This also guarantees that r and d each fit in a u32.
One section to ensure that the quotient q and the numerator n each fit in a u32. The processor needs no result, only the range checking capabilities, like for instruction split. Consequently, the processor sets the U32 Table's CI register to the opcode of split.

If the current instruction is lt, the Result can take on the values 0, 1, or 2, where

0 means LHS >= RHS is definitely known in the current row,
1 means LHS < RHS is definitely known in the current row, and
2 means the result is unknown in the current row. This is only an intermediate result. It can never occur in the first row of a section, i.e., when CopyFlag is 1.

A new row with CopyFlag = 1 can only be inserted if

LHS is 0 or the current instruction is pow, and
RHS is 0.

It is impossible to create a valid proof of correct execution of Triton VM if Bits is 33 in any row.

Extension Columns

The U32 Table has 1 extension column, U32LookupServerLogDerivative. It corresponds to the Lookup Argument with the Processor Table, establishing that whenever the processor executes a u32 instruction, the following holds:

the processor's requested left-hand side is copied into LHS,
the processor's requested right-hand side is copied into RHS,
the processor's requested u32 instruction is copied into CI, and
the result Result is copied to the processor.

Padding

Each padding row is the all-zero row with the exception of

CI, which is the opcode of split, and
BitsMinus33Inv, which is $- 3 3^{- 1}$ .

Additionally, if the U32 Table is non-empty before applying padding, the padding row's columns CI, LHS, LhsInv, and Result are taken from the U32 Table's last row.

Arithmetic Intermediate Representation

Initial Constraints

If the CopyFlag is 0, then U32LookupServerLogDerivative is 0. Otherwise, the U32LookupServerLogDerivative has accumulated the first row with multiplicity LookupMultiplicity and with respect to challenges 🥜, 🌰, 🥑, and 🥕, and indeterminate 🧷.

Initial Constraints as Polynomials

(CopyFlag - 1)·U32LookupServerLogDerivative
+ CopyFlag·(U32LookupServerLogDerivative·(🧷 - 🥜·LHS - 🌰·RHS - 🥑·CI - 🥕·Result) - LookupMultiplicity)

Consistency Constraints

The CopyFlag is 0 or 1.
If CopyFlag is 1, then Bits is 0.
BitsMinus33Inv is the inverse of (Bits - 33).
LhsInv is 0 or the inverse of LHS.
Lhs is 0 or LhsInv is the inverse of LHS.
RhsInv is 0 or the inverse of RHS.
Rhs is 0 or RhsInv is the inverse of RHS.
If CopyFlag is 0 and the current instruction is lt and LHS is 0 and RHS is 0, then Result is 2.
If CopyFlag is 1 and the current instruction is lt and LHS is 0 and RHS is 0, then Result is 0.
If the current instruction is and and LHS is 0 and RHS is 0, then Result is 0.
If the current instruction is pow and RHS is 0, then Result is 1.
If CopyFlag is 0 and the current instruction is log_2_floor and LHS is 0, then Result is -1.
If CopyFlag is 1 and the current instruction is log_2_floor and LHS is 0, the VM crashes.
If CopyFlag is 0 and the current instruction is pop_count and LHS is 0, then Result is 0.
If CopyFlag is 0, then LookupMultiplicity is 0.

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

The CopyFlag is 0 or 1.
CopyFlag is 0 or Bits is 0.
BitsMinus33Inv the inverse of (Bits - 33).
LhsInv is 0 or the inverse of LHS.
Lhs is 0 or LhsInv is the inverse of LHS.
RhsInv is 0 or the inverse of RHS.
Rhs is 0 or RhsInv is the inverse of RHS.
CopyFlag is 1 or CI is the opcode of split, and, pow, log_2_floor, or pop_count or LHS is not 0 or RHS is not 0 or Result is 2.
CopyFlag is 0 or CI is the opcode of split, and, pow, log_2_floor, or pop_count or LHS is not 0 or RHS is not 0 or Result is 0.
CI is the opcode of split, lt, pow, log_2_floor, or pop_count or LHS is not 0 or RHS is not 0 or Result is 0.
CI is the opcode of split, lt, and, log_2_floor, or pop_count or RHS is not 0 or Result is 1.
CopyFlag is 1 or CI is the opcode of split, lt, and, pow, or pop_count or LHS is not 0 or Result is -1.
CopyFlag is 0 or CI is the opcode of split, lt, and, pow, or pop_count or LHS is not 0.
CopyFlag is 1 or CI is the opcode of split, lt, and, pow, or log_2_floor or LHS is not 0 or Result is 0.
CopyFlag is 1 or LookupMultiplicity is 0.

Consistency Constraints as Polynomials

CopyFlag·(CopyFlag - 1)
CopyFlag·Bits
1 - BitsMinus33Inv·(Bits - 33)
LhsInv·(1 - LHS·LhsInv)
LHS·(1 - LHS·LhsInv)
RhsInv·(1 - RHS·RhsInv)
RHS·(1 - RHS·RhsInv)
(CopyFlag - 1)·(CI - opcode(split))·(CI - opcode(and))·(CI - opcode(pow))·(CI - opcode(log_2_floor))·(CI - opcode(pop_count))·(1 - LHS·LhsInv)·(1 - RHS·RhsInv)·(Result - 2)
(CopyFlag - 0)·(CI - opcode(split))·(CI - opcode(and))·(CI - opcode(pow))·(CI - opcode(log_2_floor))·(CI - opcode(pop_count))·(1 - LHS·LhsInv)·(1 - RHS·RhsInv)·(Result - 0)
(CI - opcode(split))·(CI - opcode(lt))·(CI - opcode(pow))·(CI - opcode(log_2_floor))·(CI - opcode(pop_count))·(1 - LHS·LhsInv)·(1 - RHS·RhsInv)·Result
(CI - opcode(split))·(CI - opcode(lt))·(CI - opcode(and))·(CI - opcode(log_2_floor))·(CI - opcode(pop_count))·(1 - RHS·RhsInv)·(Result - 1)
(CopyFlag - 1)·(CI - opcode(split))·(CI - opcode(lt))·(CI - opcode(and))·(CI - opcode(pow))·(CI - opcode(pop_count))·(1 - LHS·LhsInv)·(Result + 1)
CopyFlag·(CI - opcode(split))·(CI - opcode(lt))·(CI - opcode(and))·(CI - opcode(pow))·(CI - opcode(pop_count))·(1 - LHS·LhsInv)
(CopyFlag - 1)·(CI - opcode(split))·(CI - opcode(lt))·(CI - opcode(and))·(CI - opcode(pow))·(CI - opcode(log_2_floor))·(1 - LHS·LhsInv)·(Result - 0)
(CopyFlag - 1)·LookupMultiplicity

Transition Constraints

Even though they are never explicitly represented, it is useful to alias the LHS's and RHS's least significant bit, or “lsb.” Given two consecutive rows, the (current) least significant bit of LHS can be computed by subtracting twice the next row's LHS from the current row's LHS. These aliases, i.e., LhsLsb := LHS - 2·LHS' and RhsLsb := RHS - 2·RHS', are used throughout the following.

If the CopyFlag in the next row is 1 and the current instruction is not pow, then LHS in the current row is 0.
If the CopyFlag in the next row is 1, then RHS in the current row is 0.
If the CopyFlag in the next row is 0, then CI in the next row is CI in the current row.
If the CopyFlag in the next row is 0 and LHS in the current row is unequal to 0 and the current instruction is not pow, then Bits in the next row is Bits in the current row plus 1.
If the CopyFlag in the next row is 0 and RHS in the current row is unequal to 0, then Bits in the next row is Bits in the current row plus 1.
If the CopyFlag in the next row is 0 and the current instruction is not pow, then LhsLsb is either 0 or 1.
If the CopyFlag in the next row is 0, then RhsLsb is either 0 or 1.
If the CopyFlag in the next row is 0 and the current instruction is lt and Result in the next row is 0, then Result in the current row is 0.
If the CopyFlag in the next row is 0 and the current instruction is lt and Result in the next row is 1, then Result in the current row is 1.
If the CopyFlag in the next row is 0 and the current instruction is lt and Result in the next row is 2 and LhsLsb is 0 and RhsLsb is 1, then Result in the current row is 1.
If the CopyFlag in the next row is 0 and the current instruction is lt and Result in the next row is 2 and LhsLsb is 1 and RhsLsb is 0, then Result in the current row is 0.
If the CopyFlag in the next row is 0 and the current instruction is lt and Result in the next row is 2 and LhsLsb is RhsLsb and the CopyFlag in the current row is 0, then Result in the current row is 2.
If the CopyFlag in the next row is 0 and the current instruction is lt and Result in the next row is 2 and LhsLsb is RhsLsb and the CopyFlag in the current row is 1, then Result in the current row is 0.
If the CopyFlag in the next row is 0 and the current instruction is and, then Result in the current row is twice Result in the next row plus the product of LhsLsb and RhsLsb.
If the CopyFlag in the next row is 0 and the current instruction is log_2_floor and LHS in the next row is 0 and LHS in the current row is not 0, then Result in the current row is Bits.
If the CopyFlag in the next row is 0 and the current instruction is log_2_floor and LHS in the next row is not 0, then Result in the current row is Result in the next row.
If the CopyFlag in the next row is 0 and the current instruction is pow, then LHS remains unchanged.
If the CopyFlag in the next row is 0 and the current instruction is pow and RhsLsb in the current row is 0, then Result in the current row is Result in the next row squared.
If the CopyFlag in the next row is 0 and the current instruction is pow and RhsLsb in the current row is 1, then Result in the current row is Result in the next row squared times LHS in the current row.
If the CopyFlag in the next row is 0 and the current instruction is pop_count, then Result in the current row is Result in the next row plus LhsLsb.
If the CopyFlag in the next row is 0, then U32LookupServerLogDerivative in the next row is U32LookupServerLogDerivative in the current row.
If the CopyFlag in the next row is 1, then U32LookupServerLogDerivative in the next row has accumulated the next row with multiplicity LookupMultiplicity and with respect to challenges 🥜, 🌰, 🥑, and 🥕, and indeterminate 🧷.

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

CopyFlag' is 0 or LHS is 0 or CI is the opcode of pow.
CopyFlag' is 0 or RHS is 0.
CopyFlag' is 1 or CI' is CI.
CopyFlag' is 1 or LHS is 0 or CI is the opcode of pow or Bits' is Bits + 1.
CopyFlag' is 1 or RHS is 0 or Bits' is Bits + 1.
CopyFlag' is 1 or CI is the opcode of pow or LhsLsb is 0 or LhsLsb is 1.
CopyFlag' is 1 or RhsLsb is 0 or RhsLsb is 1.
CopyFlag' is 1 or CI is the opcode of split, and, pow, log_2_floor, or pop_count or (Result' is 1 or 2) or Result is 0.
CopyFlag' is 1 or CI is the opcode of split, and, pow, log_2_floor, or pop_count or (Result' is 0 or 2) or Result is 1.
CopyFlag' is 1 or CI is the opcode of split, and, pow, log_2_floor, or pop_count or (Result' is 0 or 1) or LhsLsb is 1 or RhsLsb is 0 or Result is 1.
CopyFlag' is 1 or CI is the opcode of split, and, pow, log_2_floor, or pop_count or (Result' is 0 or 1) or LhsLsb is 0 or RhsLsb is 1 or Result is 0.
CopyFlag' is 1 or CI is the opcode of split, and, pow, log_2_floor, or pop_count or (Result' is 0 or 1) or LhsLsb is unequal to RhsLsb or CopyFlag is 1 or Result is 2.
CopyFlag' is 1 or CI is the opcode of split, and, pow, log_2_floor, or pop_count or (Result' is 0 or 1) or LhsLsb is unequal to RhsLsb or CopyFlag is 0 or Result is 0.
CopyFlag' is 1 or CI is the opcode of split, lt, pow, log_2_floor, or pop_count or Result is twice Result' plus the product of LhsLsb and RhsLsb.
CopyFlag' is 1 or CI is the opcode of split, lt, and, pow, or pop_count or LHS' is not 0 or LHS is 0 or Result is Bits.
CopyFlag' is 1 or CI is the opcode of split, lt, and, pow, or pop_count or LHS' is 0 or Result is Result'.
CopyFlag' is 1 or CI is the opcode of split, lt, and, log_2_floor, or pop_count or LHS' is LHS.
CopyFlag' is 1 or CI is the opcode of split, lt, and, log_2_floor, or pop_count or RhsLsb is 1 or Result is Result' times Result'.
CopyFlag' is 1 or CI is the opcode of split, lt, and, log_2_floor, or pop_count or RhsLsb is 0 or Result is Result' times Result' times LHS.
CopyFlag' is 1 or CI is the opcode of split, lt, and, pow, or log_2_floor or Result is Result' plus LhsLsb.
CopyFlag' is 1 or U32LookupServerLogDerivative' is U32LookupServerLogDerivative.
CopyFlag' is 0 or the difference of U32LookupServerLogDerivative' and U32LookupServerLogDerivative times (🧷 - 🥜·LHS' - 🌰·RHS' - 🥑·CI' - 🥕·Result') is LookupMultiplicity'.

Transition Constraints as Polynomials

(CopyFlag' - 0)·LHS·(CI - opcode(pow))
(CopyFlag' - 0)·RHS
(CopyFlag' - 1)·(CI' - CI)
(CopyFlag' - 1)·LHS·(CI - opcode(pow))·(Bits' - Bits - 1)
(CopyFlag' - 1)·RHS·(Bits' - Bits - 1)
(CopyFlag' - 1)·(CI - opcode(pow))·LhsLsb·(LhsLsb - 1)
(CopyFlag' - 1)·RhsLsb·(RhsLsb - 1)
(CopyFlag' - 1)·(CI - opcode(split))·(CI - opcode(and))·(CI - opcode(pow))·(CI - opcode(log_2_floor))·(CI - opcode(pop_count))·(Result' - 1)·(Result' - 2)·(Result - 0)
(CopyFlag' - 1)·(CI - opcode(split))·(CI - opcode(and))·(CI - opcode(pow))·(CI - opcode(log_2_floor))·(CI - opcode(pop_count))·(Result' - 0)·(Result' - 2)·(Result - 1)
(CopyFlag' - 1)·(CI - opcode(split))·(CI - opcode(and))·(CI - opcode(pow))·(CI - opcode(log_2_floor))·(CI - opcode(pop_count))·(Result' - 0)·(Result' - 1)·(LhsLsb - 1)·(RhsLsb - 0)·(Result - 1)
(CopyFlag' - 1)·(CI - opcode(split))·(CI - opcode(and))·(CI - opcode(pow))·(CI - opcode(log_2_floor))·(CI - opcode(pop_count))·(Result' - 0)·(Result' - 1)·(LhsLsb - 0)·(RhsLsb - 1)·(Result - 0)
(CopyFlag' - 1)·(CI - opcode(split))·(CI - opcode(and))·(CI - opcode(pow))·(CI - opcode(log_2_floor))·(CI - opcode(pop_count))·(Result' - 0)·(Result' - 1)·(1 - LhsLsb - RhsLsb + 2·LhsLsb·RhsLsb)·(CopyFlag - 1)·(Result - 2)
(CopyFlag' - 1)·(CI - opcode(split))·(CI - opcode(and))·(CI - opcode(pow))·(CI - opcode(log_2_floor))·(CI - opcode(pop_count))·(Result' - 0)·(Result' - 1)·(1 - LhsLsb - RhsLsb + 2·LhsLsb·RhsLsb)·(CopyFlag - 0)·(Result - 0)
(CopyFlag' - 1)·(CI - opcode(split))·(CI - opcode(lt))·(CI - opcode(pow))·(CI - opcode(log_2_floor))·(CI - opcode(pop_count))·(Result - 2·Result' - LhsLsb·RhsLsb)
(CopyFlag' - 1)·(CI - opcode(split))·(CI - opcode(lt))·(CI - opcode(and))·(CI - opcode(pow))·(CI - opcode(pop_count))·(1 - LHS'·LhsInv')·LHS·(Result - Bits)
(CopyFlag' - 1)·(CI - opcode(split))·(CI - opcode(lt))·(CI - opcode(and))·(CI - opcode(pow))·(CI - opcode(pop_count))·LHS'·(Result' - Result)
(CopyFlag' - 1)·(CI - opcode(split))·(CI - opcode(lt))·(CI - opcode(and))·(CI - opcode(log_2_floor))·(CI - opcode(pop_count))·(LHS' - LHS)
(CopyFlag' - 1)·(CI - opcode(split))·(CI - opcode(lt))·(CI - opcode(and))·(CI - opcode(log_2_floor))·(CI - opcode(pop_count))·(RhsLsb - 1)·(Result - Result'·Result')
(CopyFlag' - 1)·(CI - opcode(split))·(CI - opcode(lt))·(CI - opcode(and))·(CI - opcode(log_2_floor))·(CI - opcode(pop_count))·(RhsLsb - 0)·(Result - Result'·Result'·LHS)
(CopyFlag' - 1)·(CI - opcode(split))·(CI - opcode(lt))·(CI - opcode(and))·(CI - opcode(pow))·(CI - opcode(log_2_floor))·(Result - Result' - LhsLsb)
(CopyFlag' - 1)·(U32LookupServerLogDerivative' - U32LookupServerLogDerivative)
(CopyFlag' - 0)·((U32LookupServerLogDerivative' - U32LookupServerLogDerivative)·(🧷 - 🥜·LHS - 🌰·RHS - 🥑·CI - 🥕·Result) - LookupMultiplicity')

Terminal Constraints

LHS is 0 or the current instruction is pow.
RHS is 0.

Terminal Constraints as Polynomials

LHS·(CI - opcode(pow))
RHS

Table Linking

Triton VM's tables are linked together using a variety of different cryptographic arguments. The section on arithmetization incorporates all the necessary ingredients by defining the corresponding parts of the Arithmetic Execution Tables and the Arithmetic Intermediate Representation. However, that presentation doesn't make it easy to follow and understand the specific arguments in use. Therefor, the distinct “cross-table” or “table-linking” arguments are presented here in isolation.

Compressing Multiple Elements

Mathematically, all arguments used in Triton VM are about single elements of the finite field $F_{p}$ . In practice, it is very useful to argue about multiple elements. A common trick is to “compress” multiple elements into a single one using random weights. These weights are “supplied by the STARK verifier,” i.e., sampled using the Fiat-Shamir heuristic after the prover has committed to the elements in question. For example, if $a$ , $b$ , and $c$ are to be incorporated into the cryptographic argument, then the prover

commits to $a$ , $b$ , and $c$ ,
samples weights $α$ , $β$ , and $γ$ using the Fiat-Shamir heuristic,
“compresses” the elements in question to $δ = α \cdot a + β \cdot b + γ \cdot c$ , and
uses $δ$ in the cryptographic argument.

In the following, all cryptographic arguments are presented using single field elements. Depending on the use case, this single element represents multiple, “compressed” elements.

Permutation Argument

The Permutation Argument establishes that two lists $A = (a_{0}, \dots, a_{n})$ and $B = (b_{0}, \dots, b_{n})$ are permutations of each other. To achieve this, the lists' elements are interpreted as the roots of polynomials $f_{A} (X)$ and $f_{B} (X)$ , respectively:

$f_{A} (X) f_{B} (X) = i = 0 \prod n X - a_{i} = i = 0 \prod n X - b_{i}$

The two lists $A$ and $B$ are a permutation of each other if and only if the two polynomials $f_{A} (X)$ and $f_{B} (X)$ are identical. By the Schwartz–Zippel lemma, probing the polynomials in a single point $α$ establishes the polynomial identity with high probability.¹

In Triton VM, the Permutation Argument is generally applied to show that the rows of one table appear in some other table without enforcing the rows' order in relation to each other. To establish this, the prover

commits to the base column in question,²
samples a random challenge $α$ through the Fiat-Shamir heuristic,
computes the running product of $f_{A} (α)$ and $f_{B} (α)$ in the respective tables' extension column.

For example, in Table A:

base column A	extension column A: running product
0	$(α - 0)$
1	$(α - 0) (α - 1)$
2	$(α - 0) (α - 1) (α - 2)$
3	$(α - 0) (α - 1) (α - 2) (α - 3)$

And in Table B:

base column B	extension column B: running product
2	$(α - 2)$
1	$(α - 2) (α - 1)$
3	$(α - 2) (α - 1) (α - 3)$
0	$(α - 2) (α - 1) (α - 3) (α - 0)$

It is possible to establish a subset relation by skipping over certain elements when computing the running product. The running product must incorporate the same elements in both tables. Otherwise, the Permutation Argument will fail.

An example of a subset Permutation Argument can be found between the U32 Table and the Processor Table.

This depends on the length $n$ of the lists $A$ and $B$ as well as the field size. For Triton VM, $n < 2^{32}$ . The polynomials $f_{A} (X)$ and $f_{B} (X)$ are evaluated over the extension field with $p^{3} \approx 2^{192}$ elements. The false positive rate is therefore $n /∣ F_{p^{3}} ∣ ⩽ 2^{- 160}$ .

See “Compressing Multiple Elements.”

Evaluation Argument

The Evaluation Argument establishes that two lists $A = (a_{0}, \dots, a_{n})$ and $B = (b_{0}, \dots, b_{n})$ are identical. To achieve this, the lists' elements are interpreted as the coefficients of polynomials $f_{A} (X)$ and $f_{B} (X)$ , respectively:

$f_{A} (X) f_{B} (X) = X^{n + 1} + i = 0 \sum n a_{n - i} X^{i} = X^{n + 1} + i = 0 \sum n b_{n - i} X^{i}$

The two lists $A$ and $B$ are identical if and only if the two polynomials $f_{A} (X)$ and $f_{B} (X)$ are identical. By the Schwartz–Zippel lemma, probing the polynomials in a single point $α$ establishes the polynomial identity with high probability.¹

In Triton VM, the Evaluation Argument is generally used to show that (parts of) some row appear in two tables in the same order. To establish this, the prover

commits to the base column in question,²
samples a random challenge $α$ through the Fiat-Shamir heuristic,
computes the running evaluation of $f_{A} (α)$ and $f_{B} (α)$ in the respective tables' extension column.

For example, in both Table A and B:

base column	extension column: running evaluation
0	$α^{1} + 0 α^{0}$
1	$α^{2} + 0 α^{1} + 1 α^{0}$
2	$α^{3} + 0 α^{2} + 1 α^{1} + 2 α^{0}$
3	$α^{4} + 0 α^{3} + 1 α^{2} + 2 α^{1} + 3 α^{0}$

It is possible to establish a subset relation by skipping over certain elements when computing the running evaluation. The running evaluation must incorporate the same elements in both tables. Otherwise, the Evaluation Argument will fail.

Examples for subset Evaluation Arguments can be found between the Hash Table and the Processor Table.

See “Compressing Multiple Elements.”

Lookup Argument

The Lookup Argument establishes that all elements of list $A = (a_{0}, \dots, a_{ℓ})$ also occur in list $B = (b_{0}, \dots, b_{n})$ . In this context, $A$ contains the values that are being looked up, while $B$ is the lookup table.¹ Both lists $A$ and $B$ may contain duplicates. However, it is inefficient if $B$ does, and is therefor assumed not to.

The example at the end of this section summarizes the necessary computations for the Lookup Argument. The rest of the section derives those computations. The first step is to interpret both lists' elements as the roots of polynomials $f_{A} (X)$ and $f_{B} (X)$ , respectively:

$f_{A} (X) f_{B} (X) = i = 0 \prod ℓ X - a_{i} = i = 0 \prod n X - b_{i}$

By counting the number of occurrences $m_{i}$ of unique elements $a_{i} \in A$ and eliminating duplicates, $f_{A} (X)$ can equivalently be expressed as:

$f_{A} (X) = i = 0 \prod n (X - a_{i})^{m_{i}}$

The next step uses

the formal derivative $f_{A}^{'} (X)$ of $f_{A} (X)$ , and
the multiplicity-weighted formal derivative $f_{B}^{' (m)} (X)$ of $f_{B} (X)$ .

The former is the familiar formal derivative:

$f_{A}^{'} (X) = i = 0 \sum n m_{i} (X - a_{i})^{m_{i} - 1} j \neq = i \prod (X - a_{j})^{m_{j}}$

The multiplicity-weighted formal derivative uses the lookup-multiplicities $m_{i}$ as additional factors:

$f_{B}^{' (m)} (X) = i = 0 \sum n m_{i} j \neq = i \prod (X - b_{j})$

Let $g (X)$ the greatest common divisor of $f_{A} (X)$ and $f_{A}^{'} (X)$ . The polynomial $f_{A} (X) / g (X)$ has the same roots as $f_{A} (X)$ , but all roots have multiplicity 1. This polynomial is identical to $f_{B} (X)$ if and only if all elements in list $A$ also occur in list $B$ .

A similar property holds for the formal derivatives: The polynomial $f_{A}^{'} (x) / g (X)$ is identical to $f_{B}^{' (m)} (X)$ if and only if all elements in list $A$ also occur in list $B$ . By solving for $g (X)$ and equating, the following holds:

$f_{A} (X) \cdot f_{B}^{' (m)} (X) = f_{A}^{'} (X) \cdot f_{B} (X)$

Optimization through Logarithmic Derivatives

The logarithmic derivative of $f (X)$ is defined as $f^{'} (X) / f (X)$ . Furthermore, the equality of monic polynomials $f (X)$ and $g (X)$ is equivalent to the equality of their logarithmic derivatives.² This allows rewriting above equation as:

$\frac{f _{A}^{'} ( X )}{f _{A} ( X )} = \frac{f _{B}^{' (m)} ( X )}{f _{B} ( X )}$

Using logarithmic derivatives for the equality check decreases the computational effort for both prover and verifier. Concretely, instead of four running products – one each for $f_{A}$ , $f_{A}^{'}$ , $f_{B}$ , and $f_{B}^{' (m)}$ – only two logarithmic derivatives are needed. Namely, considering once again list $A$ containing duplicates, above equation can be written as:

$i = 0 \sum ℓ \frac{1}{X - a _{i}} = i = 0 \sum n \frac{m _{i}}{X - b _{i}}$

To compute the sums, the lists $A$ and $B$ are base columns in the two respective tables. Additionally, the lookup multiplicity is recorded explicitly in a base column of the lookup table.

Example

In Table A:

base column A	extension column A: logarithmic derivative
0	$\frac{1}{α - 0}$
2	$\frac{1}{α - 0} + \frac{1}{α - 2}$
2	$\frac{1}{α - 0} + \frac{2}{α - 2}$
1	$\frac{1}{α - 0} + \frac{2}{α - 2} + \frac{1}{α - 1}$
2	$\frac{1}{α - 0} + \frac{3}{α - 2} + \frac{1}{α - 1}$

And in Table B:

base column B	multiplicity	extension column B: logarithmic derivative
0	1	$\frac{1}{α - 0}$
1	1	$\frac{1}{α - 0} + \frac{1}{α - 1}$
2	3	$\frac{1}{α - 0} + \frac{1}{α - 1} + \frac{3}{α - 2}$

It is possible to establish a subset relation by skipping over certain elements when computing the logarithmic derivative. The logarithmic derivative must incorporate the same elements with the same multiplicity in both tables. Otherwise, the Lookup Argument will fail.

An example for a Lookup Argument can be found between the Program Table and the Processor Table.

The lookup table may represent a mapping from one or more “input” elements to one or more “output” elements – see “Compressing Multiple Elements.”

See Lemma 3 in this paper for a proof.

Memory Consistency

Triton has three memory-like units: the RAM, the jump stack, and the op stack. Each such unit has a corresponding table. Memory-consistency is the property that whenever the processor reads a data element from these units, the value that it receives corresponds to the value sent the last time when that cell was written. Memory consistency follows from two intermediate properties.

Contiguity of regions of constant memory pointer. After selecting from each table all the rows with any given memory pointer, the resulting sublist is contiguous, which is to say, there are no gaps and two such sublists can never interleave.
Inner-sorting within contiguous regions. Within each such contiguous region, the rows are sorted in ascending order by clock cycle.

The contiguity of regions of constant memory pointer is established differently for the RAM Table than for the Op Stack or Jump Stack Tables. The Op Stack and Jump Stack Tables enjoy a particular property whereby the memory pointer can only ever increase or decrease by one (or stay the same). As a result, simple AIR constraints can enforce the correct sorting by memory pointer. In contrast, the memory pointer for the RAM Table can jump arbitrarily. As explained in the next section, a Contiguity Argument establishes contiguity.

The correct inner sorting is established the same way for all three memory-like tables. Their respective clock jump differences – differences of clock cycles within regions of constant memory pointer – are shown to be contained in the set of all clock cycles through Lookup Arguments. Under reasonable assumptions about the running time, this fact implies that all clock jumps are directed forwards, as opposed to backwards, which in turn implies that the rows are sorted for clock cycle.

The next sections elaborate on these constructions. A dedicated section shows that these two properties do indeed suffice to prove memory consistency.

Contiguity of Memory-Pointer Regions

Contiguity for Op Stack Table

In each cycle, the memory pointer for the Op Stack Table, op_stack_pointer, can only ever increase by one, remain the same, or decrease by one. As a result, it is easy to enforce that the entire table is sorted for memory pointer using one initial constraint and one transition constraint.

Initial constraint: op_stack_pointer starts with 16¹, so in terms of polynomials the constraint is op_stack_pointer - 16.
Transition constraint: the new op_stack_pointer is either the same as the previous or one larger. The polynomial representation for this constraint is (op_stack_pointer' - op_stack_pointer - 1) · (op_stack_pointer' - op_stack_pointer).

Contiguity for Jump Stack Table

Analogously to the Op Stack Table, the Jump Stack's memory pointer jsp can only ever decrease by one, remain the same, or increase by one, within each cycle. As a result, similar constraints establish that the entire table is sorted for memory pointer.

Initial constraint: jsp starts with zero, so in terms of polynomials the constraint is jsp.
Transition constraint: the new jsp is either the same as the previous or one larger. The polynomial representation for this constraint is (jsp' - jsp - 1) * (jsp' - jsp).

Contiguity for RAM Table

The Contiguity Argument for the RAM table establishes that all RAM pointer regions start with distinct values. It is easy to ignore consecutive duplicates in the list of all RAM pointers using one additional base column. This allows identification of the RAM pointer values at the regions' boundaries, $A$ . The Contiguity Argument then shows that the list $A$ contains no duplicates. For this, it uses Bézout's identity for univariate polynomials. Concretely, the prover shows that for the polynomial $f_{A} (X)$ with all elements of $A$ as roots, i.e., $f_{A} (X) = i = 0 \prod n X - a_{i}$ and its formal derivative $f_{A}^{'} (X)$ , there exist $u (X)$ and $v (X)$ with appropriate degrees such that $u (X) \cdot f_{A} (X) + v (X) \cdot f_{A}^{'} (X) = 1.$ In other words, the Contiguity Argument establishes that the greatest common divisor of $f_{A} (X)$ and $f_{A}^{'} (X)$ is 1. This implies that all roots of $f_{A} (X)$ have multiplicity 1, which holds if and only if there are no duplicate elements in list $A$ .

The following columns and constraints are needed for the Contiguity Argument:

Base column iord and two deterministic transition constraints enable conditioning on a changed memory pointer.
Base columns bcpc0 and bcpc1 and two deterministic transition constraints contain and constrain the symbolic Bézout coefficient polynomials' coefficients.
Extension column rpp is a running product similar to that of a conditioned permutation argument. A randomized transition constraint verifies the correct accumulation of factors for updating this column.
Extension column fd is the formal derivative of rpp. A randomized transition constraint verifies the correct application of the product rule of differentiation to update this column.
Extension columns bc0 and bc1 build up the Bézout coefficient polynomials based on the corresponding base columns, bcpc0 and bcpc1. Two randomized transition constraints enforce the correct build-up of the Bézout coefficient polynomials.
A terminal constraint takes the weighted sum of the running product and the formal derivative, where the weights are the Bézout coefficient polynomials, and equates it to one. This equation asserts the Bézout relation.

The following table illustrates the idea. Columns not needed for establishing memory consistency are not displayed.

`ramp`	`iord`	`bcpc0`	`bcpc1`	`rpp`	`fd`	`bc0`	`bc1`
$a$	0	$0$	$ℓ$	$(X - a)$	$1$	$0$	$ℓ$
$a$	$(b - a)^{- 1}$	$0$	$ℓ$	$(X - a)$	$1$	$0$	$ℓ$
$b$	0	$j$	$m$	$(X - a) (X - b)$	$p (X)$	$j$	$ℓ X + m$
$b$	0	$j$	$m$	$(X - a) (X - b)$	$p (X)$	$j$	$ℓ X + m$
$b$	$(c - b)^{- 1}$	$j$	$m$	$(X - a) (X - b)$	$p (X)$	$j$	$ℓ X + m$
$c$	0	$k$	$n$	$(X - a) (X - b) (X - c)$	$q (X)$	$j X + k$	$ℓ X^{2} + m X + n$
$c$	-	$k$	$n$	$(X - a) (X - b) (X - c)$	$q (X)$	$j X + k$	$ℓ X^{2} + m X + n$

The values contained in the extension columns are undetermined until the verifier's challenge $α$ is known; before that happens it is worthwhile to present the polynomial expressions in $X$ , anticipating the substitution $X \mapsto α$ . The constraints are articulated relative to α.

The inverse of RAMP difference iord takes the inverse of the difference between the current and next ramp values if that difference is non-zero, and zero else. This constraint corresponds to two transition constraint polynomials:

(ramp' - ramp) ⋅ ((ramp' - ramp) ⋅ iord - 1)
iord ⋅ (ramp' - ramp) ⋅ iord - 1)

The running product rpp starts with $X - ramp$ initially, which is enforced by an initial constraint. It accumulates a factor $X - ramp^{'}$ in every pair of rows where ramp ≠ ramp'. This evolution corresponds to one transition constraint: (ramp' - ramp) ⋅ (rpp' - rpp ⋅ (α - ramp')) + (1 - (ramp' - ramp) ⋅ di) ⋅ (rpp' - rp)

Denote by $f_{rp} (X)$ the polynomial that accumulates all factors $X - ramp^{'}$ in every pair of rows where $ramp \neq = ramp^{'}$ .

The column fd contains the “formal derivative” of the running product with respect to $X$ . The formal derivative is initially $1$ , which is enforced by an initial constraint. The transition constraint applies the product rule of differentiation conditioned upon the difference in ramp being nonzero; in other words, if $ramp = ramp^{'}$ then the same value persists; but if $ramp \neq = ramp^{'}$ then $fd$ is mapped as $fd \mapsto fd^{'} = (X - ramp^{'}) \cdot fd + rp .$ This update rule is called the product rule of differentiation because, assuming $ramp^{'} \neq = ramp$ , then $\frac{d rp ^{'}}{d X} = \frac{d ( X - ramp ^{'} ) \cdot rp}{d X} = (X - ramp^{'}) \cdot \frac{d rp}{d X} + \frac{d ( X - ramp ^{'} )}{d X} \cdot rp = (X - ramp^{'}) \cdot fd + rp .$

The transition constraint for fd is (ramp' - ramp) ⋅ (fd' - rp - (α - ramp') ⋅ fd) + (1 - (ramp' - ramp) ⋅ iord) ⋅ (fd' - fd).

The polynomials $f_{bc0} (X)$ and $f_{bc1} (X)$ are the Bézout coefficient polynomials satisfying the relation $f_{bc0} (X) \cdot f_{rp} (X) + f_{bc1} (X) \cdot f_{fd} (X) = g cd (f_{rp} (X), f_{fd} (X)) =! 1 .$ The prover finds $f_{bc0} (X)$ and $f_{bc1} (X)$ as the minimal-degree Bézout coefficients as returned by the extended Euclidean algorithm. Concretely, the degree of $f_{bc0} (X)$ is smaller than the degree of $f_{fd} (X)$ , and the degree of $f_{bc1} (X)$ is smaller than the degree of $f_{rp} (X)$ .

The (scalar) coefficients of the Bézout coefficient polynomials are recorded in base columns bcpc0 and bcpc1, respectively. The transition constraints for these columns enforce that the value in one such column can only change if the memory pointer ramp changes. However, unlike the conditional update rule enforced by the transition constraints of rp and fd, the new value is unconstrained. Concretely, the two transition constraints are:

(1 - (ramp' - ramp) ⋅ iord) ⋅ (bcpc0' - bcpc0)
(1 - (ramp' - ramp) ⋅ iord) ⋅ (bcpc1' - bcpc1)

Additionally, bcpc0 must initially be zero, which is enforced by an initial constraint. This upper-bounds the degrees of the Bézout coefficient polynomials, which are built from base columns bcpc0 and bcpc1. Two transition constraints enforce the correct build-up of the Bézout coefficient polynomials:

(1 - (ramp' - ramp) ⋅ iord) ⋅ (bc0' - bc0) + (ramp' - ramp) ⋅ (bc0' - α ⋅ bc0 - bcpc0')
(1 - (ramp' - ramp) ⋅ iord) ⋅ (bc1' - bc1) + (ramp' - ramp) ⋅ (bc1' - α ⋅ bc1 - bcpc1')

Additionally, bc0 must initially be zero, and bc1 must initially equal bcpc1. This is enforced by initial constraints bc0 and bc1 - bcpc1.

Lastly, the verifier verifies the randomized AIR terminal constraint bc0 ⋅ rpp + bc1 ⋅ fd - 1.

Completeness.

For honest provers, the gcd is guaranteed to be one. As a result, the protocol has perfect completeness. $□$

Soundness.

If the table has at least one non-contiguous region, then $f_{rp} (X)$ and $f_{fd} (X)$ share at least one factor. As a result, no Bézout coefficients $f_{bc0} (X)$ and $f_{bc1} (X)$ can exist such that $f_{bc0} (X) \cdot f_{rp} (X) + f_{bc1} (X) \cdot f_{fd} (X) = 1$ . The verifier therefore probes unequal polynomials of degree at most $2 T - 2$ , where $T$ is the length of the execution trace, which is upper bounded by $2^{32}$ . According to the Schwartz-Zippel lemma, the false positive probability is at most $(2 T - 2) /∣ F ∣$ . $□$

Zero-Knowledge.

Since the contiguity argument is constructed using only AET and AIR, zero-knowledge follows from Triton VM's zk-STNARK engine. $□$

Summary of constraints

We present a summary of all constraints.

Initial

bcpc0
bc0
bc1 - bcpc1
fd - 1
rpp - (α - ramp)

Consistency

None.

Transition

(ramp' - ramp) ⋅ ((ramp' - ramp) ⋅ iord - 1)
iord ⋅ ((ramp' - ramp) ⋅ iord - 1)
(1 - (ramp' - ramp) ⋅ iord) ⋅ (bcpc0' - bcpc0)
(1 - (ramp' - ramp) ⋅ iord) ⋅ (bcpc1' - bcpc1)
(ramp' - ramp) ⋅ (rpp' - rpp ⋅ (α - ramp')) + (1 - (ramp' - ramp) ⋅ iord) ⋅ (rpp' - rpp)
(ramp' - ramp) ⋅ (fd' - rp - (α - ramp') ⋅ fd) + (1 - (ramp' - ramp) ⋅ iord) ⋅ (fd' - fd)
(1 - (ramp' - ramp) ⋅ iord) ⋅ (bc0' - bc0) + (ramp' - ramp) ⋅ (bc0' - α ⋅ bc0 - bcpc0')
(1 - (ramp' - ramp) ⋅ iord) ⋅ (bc1' - bc1) + (ramp' - ramp) ⋅ (bc1' - α ⋅ bc1 - bcpc1')

Terminal

bc0 ⋅ rpp + bc1 ⋅ fd - 1

See data structures and registers for explanations of the specific value 16.

Clock Jump Differences and Inner Sorting

The previous sections show how it is proven that in the Jump Stack, Op Stack, and RAM Tables, the regions of constant memory pointer are contiguous. The next step is to prove that within each contiguous region of constant memory pointer, the rows are sorted for clock cycle. That is the topic of this section.

The problem arises from clock jumps, which describes the phenomenon when the clock cycle increases even though the memory pointer does not change. If arbitrary jumps were allowed, nothing would prevent the cheating prover from using a table where higher rows correspond to later states, giving rise to an exploitable attack. So it must be shown that every clock jump is directed forward and not backward.

Our strategy is to show that the difference, i.e., the next clock cycle minus the current clock cycle, is itself a clock cycle. Recall that the Processor Table's clock cycles run from 0 to $T - 1$ . Therefore, a forward directed clock jump difference is in $F = {1, \dots, T - 1} \subseteq F_{p}$ , whereas a backward directed clock jump's difference is in $B = {- f ∣ f \in F} = {1 - T, \dots, - 1} \subseteq F_{p}$ . No other clock jump difference can occur. If $T ≪ p /2$ , there is no overlap between sets $F$ and $B$ . As a result, in this regime, showing that a clock jump difference is in $F$ guarantees that the jump is forward-directed.

The set of values in the Processor Table's clock cycle column is $F \cup {0}$ . A standard Lookup Argument can show that the clock jump differences are elements of that column. Since all three memory-like tables look up the same property, the Processor Table acts as a single server as opposed to three distinct servers. Concretely, the lookup multiplicities of the three clients, i.e., the memory-like tables, are recorded in a single column cjd_mul. It contains the element-wise sum of the three distinct lookup multiplicities.

Proof of Memory Consistency

Whenever the Processor Table reads a value "from" a memory-like table, this value appears nondeterministically and is unconstrained by the base table AIR constraints. However, there is a permutation argument that links the Processor Table to the memory-like table in question. The construction satisfies memory consistency if it guarantees that whenever a memory cell is read, its value is consistent with the last time that cell was written.

The above is too informal to provide a meaningful proof for. Let's put formal meanings on the proposition and premises, before reducing the former to the latter.

Let $P$ denote the Processor Table and $M$ denote the memory-like table. Both have height $T$ . Both have columns clk, mp, and val. For $P$ the column clk coincides with the index of the row. $P$ has another column ci, which contains the current instruction, which is write, read, or any. Obviously, mp and val are abstract names that depend on the particular memory-like table, just like write, read, and any are abstract instructions that depend on the type of memory being accessed. In the following math notation we use $col$ to denote the column name and $col$ to denote the value that the column might take in a given row.

Definition 1 (contiguity): The memory-like table is contiguous iff all sublists of rows with the same memory pointer mp are contiguous. Specifically, for any given memory pointer $mp$ , there are no rows with a different memory pointer $mp^{'}$ in between rows with memory pointer $mp$ .

$\forall i < j < k \in {0, \dots, T - 1} : mp = △ M [i] [mp] = M [k] [mp] \Rightarrow M [j] [mp] = mp$

Definition 2 (regional sorting): The memory-like table is regionally sorted iff for every contiguous region of constant memory pointer, the clock cycle increases monotonically.

$\forall i < j \in {0, \dots, T - 1} : M [i] [mp] = M [j] [mp] \Rightarrow M [i] [clk] <_{Z} M [j] [clk]$

The symbol $<_{Z}$ denotes the integer less than operator, after lifting the operands from the finite field to the integers.

Definition 3 (memory consistency): A Processor Table $P$ has memory consistency if whenever a memory cell at location $mp$ is read, its value corresponds to the previous time the memory cell at location $mp$ was written. Specifically, there are no writes in between the write and the read, that give the cell a different value.

$\forall k \in {0, \dots, T - 1} : P [k] [ci] = read \Rightarrow ((1) \Rightarrow (2))$

$(1) \exists i \in {0, \dots, k} : P [i] [ci] = write \land P [i + 1] [val] = P [k] [val] \land P [i] [mp] = P [k] [mp]$

$(2) ∄ j \in {i + 1, \dots, k - 1} : P [j] [ci] = write \land P [i] [mp] = P [k] [mp]$

Theorem 1 (memory consistency): Let $P$ be a Processor Table. If there exists a memory-like table $M$ such that

selecting for the columns clk, mp, val, the two tables' lists of rows are permutations of each other; and
$M$ is contiguous and regionally sorted; and
$M$ has no changes in val that coincide with clock jumps;

then $P$ has memory consistency.

Proof. For every memory pointer value $mp$ , select the sublist of rows $P_{mp} = △ {P [k] ∣ P [k] [mp] = mp}$ in order. The way this sublist is constructed guarantees that it coincides with the contiguous region of $M$ where the memory pointer is also $mp$ .

Iteratively apply the following procedure to $P_{mp}$ : remove the bottom-most row if it does not correspond to a row $k$ that constitutes a counter-example to memory consistency. Specifically, let $i$ be the clock cycle of the previous row in $P_{mp}$ .

If $i$ satisfies $(1)$ then by construction it also satisfies $(2)$ . As a result, row $k$ is not part of a counter-example to memory consistency. We can therefore remove the bottom-most row and proceed to the next iteration of the outermost loop.
If $P [i] [ci] \neq = write$ then we can safely ignore this row: if there is no clock jump, then the absence of a $write$ -instruction guarantees that $val$ cannot change; and if there is a clock jump, then by assumption on $M$ , $val$ cannot change. So set $i$ to the clock cycle of the row above it in $P_{mp}$ and proceed to the next iteration of the inner loop. If there are no rows left for $i$ to index, then there is no possible counterexample for $k$ and so remove the bottom-most row of $P_{mp}$ and proceed to the next iteration of the outermost loop.
The case $P [i + 1] [val] \neq = P [k] [val]$ cannot occur because by construction of $i$ , $val$ cannot change.
The case $P [i] [mp] \neq = P [k] [mp]$ cannot occur because the list was constructed by selecting only elements with the same memory pointer.
This list exhausts the possibilities of condition (1).

When $P_{mp}$ consists of only two rows, it can contain no counter-examples. By applying the above procedure, we can reduce every correctly constructed sublist $P_{mp}$ to a list consisting of two rows. Therefore, for every $mp$ , the sublist $P_{mp}$ is free of counter-examples to memory consistency. Equivalently, $P$ is memory consistent. $□$

Program Attestation

“Program attestation” is the notion of cryptographically linking a program to the proof produced by that program's execution. Informally, program attestation allows Triton VM to prove claims of the form:

There exists a program with hash digest X that, given input Y, produces output Z.

Without program attestation, Triton VM would only be able to prove claims of the form:

There exists a program that, given input Y, produces output Z.

The proof system is zero-knowledge with respect to the actual program. That is, the verifier learns nothing about the program of which correct execution is proven, except the program's digest¹. This property is generally desirable, for example to keep a specific machine learning model secret while being able to prove its correct execution. However, it can be equally desirable to reveal the program, for example to allow code auditing. In such cases, the program's source code can be revealed and digest equality can be checked.

As is the case throughout Triton VM, the used hash function is Tip5.

Mechanics

Program attestation is part of initializing Triton VM. That is, control is passed to the to-be-executed program only after the following steps have been performed:

The instructions, located in program memory, are padded. The padding follows Tip5's rules for input of variable length².
The padded instructions are copied to the Hash Table.
The Hash Table computes the program's digest by iterating Tip5 multiple times in Sponge mode.
The program digest is copied to the bottom of the operational stack, i.e., stack elements st11 through st15.

The program digest is part of the generated proof³, and hence public. During proof verification, AIR constraints in the Hash Table establish that the claimed and the computed program digests are identical, and that the digest was computed integrally. This establishes verifiable integrity of the publicly claimed program digest. Below figure visualizes the interplay of tables and public data for proof verification.

Notably, a program has access to the hash digest of itself. This is useful for recursive verification: since the program digest is both part of the proof that is being verified and accessible during execution, the two can be checked for equality at runtime. This way, the recursive verifier can know whether it is actually recursing, or whether it is verifying a proof for some other program. After all, the hash digest of the verifier program cannot be hardcoded into the verifier program, because that would be a circular dependency.

Since hash functions are deterministic, a programmer desiring resistance against enumeration attacks might want to include blinding elements This is easily possible in, for example, dead code, by including instructions like push random_element. The distribution random_element is sampled from and the number of such instructions determine the security level against enumeration attacks.

Padding is one 1 followed by the minimal number of 0’s necessary to make the padded input length a multiple of the $rate$ , which is 10. See also section 2.5 “Fixed-Length versus Variable-Length” in the Tip5 paper.

More specifically, of the claim, which itself is part of the proof.

Index Sampling

Task: given pseudorandomness, sample pseudorandomly $k$ distinct but otherwise uniform indices from the interval $[0 : U)$ . This index sampling task is needed in several locations, not just in the STARK engine. Outside of the VM, this task can be achieved by rejection sampling until the list of collected samples has the requisite size (namely, $k$ ). Inside the VM, we like to avoid variable-length execution paths. This note explains how to do it using non-determinism.

Solution 1: Out-of-Order Divination

We want to sample exactly $k$ unique indices, but the sampler in the VM is allowed to divine counter values.

Outside VM

By rejection sampling until the list of samples has the requisite length I mean something like this:

    function sample_indices(count, upper_bound, randomness):
        list <- []
        counter <- 0
        while length(list) < count:
            integer <- Hash(randomness || counter)
            candidate_index <- integer % upper_bound
            if candidate_index in list:
                continue // reject
            else:
                list <- list || candidate_index
        return list

The loop needs to iterate at least count number of times. It is possible to parallelize this first step by separating the count first iterations from the variable-number follow-ups.

This python-like pseudocode hides important complexity behind the list membership test. To expand this logic, we need sorting and consecutive deduplication.

    function sample_indices(count, upper_bound, randomness):
        list <- []
        counter <- 0
        while length(list) < count:
            integer <- Hash(randomness || counter)
            candidate_index <- integer % upper_bound
            list <- sort(list || candidate_index)
            list.deduplicate()
        return list

Inside VM

In a nutshell, the VM nondeterministically guesses ("divines") the values of the counters out of order, checks that they are within allowed bounds, and then checks that the resulting list of indices is sorted and has no duplicates.

    function sample_indices(count, upper_bound, randomness):
        list <- []
        for i in [0:count):
            counter <- divine()
            assert(counter >= 0)
            assert(counter < count + margin)
            integer <- Hash(randomness || counter)
            index <- integer % upper_bound
            list <- list || index
            if i > 0:
                assert(list[i] < list[i-1])
        return list

The Virtual Machine supplies the right counters through divine(), having observed them from the out-of-VM execution.

The parameter margin should be large enough so that, with overwhelming probability, there is a set of count-many counters in [0:(count+margin)) that map to distinct indices. At the same time, the parameter margin should not be too large as it gives the malicious adversary more flexibility in selecting favorable indices.

Failure Probability

In order for the honest user to fail to find a good counter set, the list [0:(count+margin)) must contain at least margin+1 collisions under x -> Hash(randomness || x) % upper_bound. We continue by modeling this map as uniformly random.

The event margin+1 collisions or more implies that margin+1 samples were drawn from a subset of at most count-1 marked indices. The probability of the implied event is $Pr [# collisions \geq μ + 1] = (\frac{( k - 1 )}{U})^{μ + 1},$ where $U$ denotes upper_bound, $k$ denotes count, and $μ$ denotes margin.

Given the count and the upper_bound, the appropriate value for margin that pushes this failure probability below $2^{- λ}$ is $(\frac{( k - 1 )}{U})^{μ + 1} \leq 2^{- λ}$ $(μ + 1) \cdot lo g_{2} (\frac{( k - 1 )}{U}) \leq - λ$ $μ \geq \frac{- λ}{lo g _{2} ( \frac{( k - 1 )}{U} )} - 1 .$

For a concrete example, set $k = λ = 160$ and $U = 2^{32}$ . Then $μ$ needs to be at least 6.

Security Degradation

Suppose the user is malicous and hopes to conceal his fraud by selecting a set of indices that do not expose it. Suppose that the proportion of subsets of $[0 : U)$ of size $k$ that are suitable for the adversary is $ρ$ . Then clearly with the standard old index sampling method the attacker's success probability is bounded by $ρ \approx 2^{- λ}$ . The question is whether the improved index sampler enables a higher success probability (and if so, how much higher).

The attacker has access to at most $(μ k + μ)$ subsets of $[0 : U)$ of size $k$ . The probability that a given subset is suitable for the attack is $ρ$ , and so:

The probability that one subset is unsuitable for attack is $1 - ρ$ .
The probability that all $(μ k + μ)$ subsets are unsuitable for attack is $(1 - ρ)^{(μ k + μ)}$ . In this step we assume that whether a subset is suitable for attack, is independent from whether different subset is suitable for attack, even if the intersection of the two subsets is nonzero.
The probability that at least one subset is suitable for attack is $1 - (1 - ρ)^{(μ k + μ)}$ .

The binomial formula expands $(1 - ρ)^{(μ k + μ)} = i = 0 \sum (μ k + μ) (- 1)^{i} (i ( μ k + μ )) ρ^{i} .$ We assume that each subsequent term is smaller in absolute value than the previous because $ρ$ dominates. Indeed, plugging the well-known upper bound on the binomial coefficient $(k n) < (\frac{n \cdot e}{k})^{k}$ , we get $(i ( μ k + μ )) < (i ( \frac{( k + μ ) \cdot e}{μ} ) ^{μ}) < ⎝ ⎛ \frac{( \frac{( k + μ ) \cdot e}{μ} ) ^{μ} \cdot e}{i} ⎠ ⎞^{i}$ and the assumption holds already when $(\frac{( k + μ ) \cdot e}{μ})^{μ} < ρ^{- 1}$ . For a concrete example, set $k = 160$ and $μ = 6$ , then the left hand side of this expression is roughly $2^{37.4}$ whereas these parameters target a security level of $λ \approx lo g_{2} ρ^{- 1}$ .

Using this assumption (on the shrinking absolute value of each successive term) we can derive an expression to quantify the security degradation. $Pr [attack] \leq 1 - (1 - ρ)^{(μ k + μ)}$ $= 1 - 1 + ρ \cdot (μ k + μ) - ρ^{2} \cdot (μ k + μ) \cdot (μ k + μ) \cdot \frac{1}{2} + \dots$ $\leq (μ k + μ) \cdot ρ .$

For a concrete example, set $k = 160$ and $μ = 6$ . Then $(μ k + μ) \approx 2^{34.6}$ and so we lose about $33$ bits of security.

Solution 2: Stupid Safety Margin

How about we sample $k + μ$ indices from the start, and use them all no matter what? We only need $k$ for security. The margin parameter $μ$ is chosen such that finding more than $μ$ collisions, which is required to undermine the security guarantee, is cryptographically improbable.

The benefit of this solution is that both the index samplers, i.e., inside and outside the VM, have a simple description. Furthermore, there is no longer a nonzero failure probability for honest users. The drawback is that more work is done than necessary, and the proofs are larger too.

So what is the right value of $μ$ ? It turns out that this probability matches with the correctness error derived for the previous solution. For redundancy this derivation is repeated here.

Sampling $μ + 1$ or more collisions requires hitting a marked subset of at most $k - 1$ indices $μ + 1$ times. The probability of this event is therefore $(\frac{k - 1}{U})^{μ + 1}$ . This probability is smaller than $2^{- λ}$ when $(\frac{k - 1}{U})^{μ + 1} \leq 2^{- λ}$ $(μ + 1) \cdot lo g_{2} (\frac{k - 1}{U}) \leq - λ$ $μ \geq \frac{- λ}{lo g _{2} ( \frac{k - 1}{U} )} - 1 .$

For a concrete example, set $k = λ = 160$ and $U = 2^{32}$ . Then $μ$ needs to be at least 6.

Zero-Integral and Sum-Check

Let $T$ be a table of 1 column and $∣ H ∣$ rows, and let $\hat{f} (X)$ be any polynomial that agrees with $T$ when evaluated on $H = (ο^{i})_{i}$ , where $ο$ is a generator of the subgroup of order $2^{k}$ $H$ . Group theory lets us prove and efficiently verify if $\sum T = 0$ .

Decompose $\hat{f} (X)$ into $\hat{f} (X) = \overset{g}{^} (X) + Z_{H} (X) \cdot \hat{h} (X)$ , where $Z_{H} (X)$ is the zerofier over $H$ , and where $\overset{g}{^} (X)$ has degree at most $∣ H ∣ - 1$ . The table sums to zero if and only if $\overset{g}{^} (X)$ integrates to zero over $H$ because

$h \in H \sum \hat{f} (h) = h \in H \sum (\overset{g}{^} (h) + Z_{H} (h) \cdot \hat{h} (h)) = h \in H \sum \overset{g}{^} (h)$

and this latter proposition is true if and only if the constant term of $\overset{g}{^} (X)$ is zero.

Theorem. $\sum_{h \in H} \hat{f} (h) = 0 \Leftrightarrow X ∣ \overset{g}{^} (X)$ for a subgroup $H \subseteq F^{*}$ of order $2^{k}$ .

$P roo f .$ Let $K$ be a subgroup of $H$ . If $K \neq = {1}$ then $- 1 \in K$ and also $\sum_{k \in K} k = 0$ because the elements of $K$ come in pairs: $k \in K \Leftrightarrow - k \in K$ . Therefore $\sum_{h \in H} h = 0$ .

The map $H \to K, h \mapsto h^{α}$ is a morphism of groups with $∣ H ∣ \geq ∣ K ∣ \geq 1$ . Therefore we have:

$h \in H \sum h^{α} = {∣ H ∣ 0 \Leftarrow α = 0 mod ∣ H ∣ . \Leftarrow α \neq = 0 mod ∣ H ∣ .$

The polynomial $\overset{g}{^} (X)$ has only one term whose exponent is $0 mod ∣ H ∣$ , which is the constant term. $□$

This observation gives rise to the following Polynomial IOP for verifying that a polynomial oracle $[\hat{f} (X)]$ integrates to 0 on a subgroup $H$ of order some power of 2.

Protocol Zero-Integral

Prover computes $\overset{g}{^} (X) \leftarrow \hat{f} (X) mod Z_{H} (X)$ and $\hat{h} (X) \leftarrow \frac{f ^ ( X ) - g ^ ( X )}{Z _{H} ( X )}$ .
Prover computes $\overset{g}{^}^{⋆} (X) = \frac{g ^ ( X )}{X}$ .
Prover sends $\overset{g}{^}^{⋆} (X)$ , of degree at most $∣ H ∣ - 2$ , and $\hat{h} (X)$ , of degree at most $deg (\hat{f} (X)) - ∣ H ∣$ to Verifier.
Verifier queries $[\hat{f} (X)]$ , $[\overset{g}{^}^{⋆} (X)]$ , $[\hat{h} (X)]$ in z \xleftarrow{$} \mathbb{F} and receives $y_{f}, y_{g^{⋆}}, y_{h}$ .
Verifier tests $y_{f} = ? z \cdot y_{g^{⋆}} + y_{h} \cdot Z_{H} (z)$ .

This protocol can be adapted to show instead that a given polynomial oracle integrates to $a \neq = 0$ on the subgroup $H$ , giving rise to the well-known Sum-Check protocol. The adaptation follows from the Verifier's capacity to simulate $[\hat{f}^{⋆} (X)]$ from $[\hat{f} (X)]$ , where $\hat{f}^{⋆} (X) = \hat{f} (X) - \frac{a}{∣ H ∣}$ . This simulated polynomial is useful because

$h \in H \sum \hat{f}^{⋆} (h) = h \in H \sum (\hat{f} (h) - \frac{a}{∣ H ∣}) = a - \frac{a}{H} h \in H \sum 1 = 0 .$

In other words, $\hat{f} (X)$ integrates to $a$ on $H$ iff $\hat{f}^{⋆} (X)$ integrates to $0$ on $H$ , and we already a protocol to establish the latter claim.