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 where is the Oxfoi prime, i.e., .1 This means the registers and memory elements take values from , and the transition function gives rise to low-degree transition verification polynomials from the ring of multivariate polynomials over .
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 pop
, removing the 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:
- RAM, to which the VM can read and write field elements.
- Program Memory, from which the VM reads instructions.
- OpStack Memory, which stores the operational stack.
- Jump Stack Memory, which stores the entire jump stack.
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, “OpStack.”
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
throughst15
, and - the OpStack Underflow Memory.
The motivation and the interplay between the two parts is described and exemplified in arithmetization of the OpStack table.
Random Access Memory
Triton VM has dedicated Random Access Memory.
It can hold up to many base field elements, where is the Oxfoi prime1.
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 that keeps track of return and destination addresses.
This stack changes only when control follows a call
or return
instruction.
Of course, the machine running Triton VM might have stricter limitations: storing or accessing bits TiB 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 |
*PreviousInstruction | previous instruction | holds the opcode of the instruction executed in the previous clock cycle (or 0 if such cycle exists) |
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 ib7 | 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 |
*osp | operational stack pointer | contains the OpStack address of the top of the operational stack |
*osv | operational stack value | contains the (stack) memory value at the given address |
*hv0 through hv6 | helper variable registers | helper variables for some arithmetic operations |
*ramp | RAM pointer | contains an address pointing into the RAM |
*ramv | RAM value | contains the value of the RAM element at the address currently held in ramp |
*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 ib7
.
Stack
The stack is represented by 16 registers called stack registers (st0
– st15
) plus the OpStack Underflow Memory.
The top 16 elements of the OpStack are directly accessible, the remainder of the OpStack, i.e, the part held in OpStack Underflow Memory, is not.
In order to access elements of the OpStack held in OpStack 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. All these elements are initially 0. Trying to run an instruction which would result in a stack of smaller total length than 16 crashes the VM.
The registers osp
and osv
are not directly accessible by the program running in TritonVM.
They exist only to allow efficient arithmetization.
RAM
The registers ramp
and ramv
are not directly accessible by the program running in TritonVM.
They exist only to allow efficient arithmetization.
Helper Variables
Some instructions require helper variables in order to generate an efficient arithmetization.
To this end, there are 7 helper variable registers, labeled hv0
through hv6
.
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 stack_shrinks_and_top_3_unconstrained
and its derivatives, as well as for instructions
dup
,
swap
,
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 guarantee that operational stack underflow cannot happen.
It is used by several instructions through instruction group stack_shrinks_and_top_3_unconstrained
.
The third property allows efficient arithmetization of the running product for the Permutation Argument between Processor Table and U32 Table.
OpStack Manipulation
Instruction | Opcode | old OpStack | new OpStack | Description |
---|---|---|---|---|
pop | 2 | _ a | _ | Pops top element from stack. |
push + a | 1 | _ | _ a | Pushes a onto the stack. |
divine | 8 | _ | _ a | Pushes a non-deterministic element a to the stack. Interface for secret input. |
dup + i | 9 | e.g., _ e d c b a | e.g., _ e d c b a d | Duplicates the element i positions away from the top, assuming 0 <= i < 16 . |
swap + i | 17 | 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, assuming 0 < i < 16 . |
Instruction divine
(together with divine_sibling
) make TritonVM 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
makes some element a
magically appear on the stack.
It is not at all specified what a
is, but generally speaking, a
has to be exactly correct, else execution fails.
Hence, from the perspective of the program, it just non-deterministically guesses the correct value of a
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 value a
was supplied as a secret input.
Control Flow
Instruction | Opcode | old OpStack | new OpStack | old ip | new ip | old JumpStack | new JumpStack | Description |
---|---|---|---|---|---|---|---|---|
nop | 16 | _ | _ | _ | _ + 1 | _ | _ | Do nothing |
skiz | 10 | _ a | _ | _ | _ + 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 | 25 | _ | _ | o | d | _ | _ (o+2, d) | Push (o+2,d) to the jump stack, and jump to absolute address d |
return | 24 | _ | _ | _ | o | _ (o, d) | _ | Pop one pair off the jump stack and jump to that pair's return address (which is the first element). |
recurse | 32 | _ | _ | _ | 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 | 18 | _ a | _ | _ | _ + 1 | _ | _ | Pops a if a == 1 , else crashes the virtual machine. |
halt | 0 | _ | _ | _ | _ + 1 | _ | _ | Solves the halting problem (if the instruction is reached). Indicates graceful shutdown of the VM. |
Memory Access
Instruction | Opcode | old OpStack | new OpStack | old ramv | new ramv | Description |
---|---|---|---|---|---|---|
read_mem | 40 | _ p | _ p v | v | v | Reads value v from RAM at address p and pushes v onto the OpStack. |
write_mem | 26 | _ p v | _ p | _ | v | Writes OpStack's top-most value v to RAM at the address p , popping v . |
Hashing
Instruction | Opcode | old OpStack | new OpStack | Description |
---|---|---|---|---|
hash | 48 | _jihgfedcba | _yxwvu00000 | Overwrites the stack's 10 top-most elements with their hash digest (length 5) and 5 zeros. |
divine_sibling | 56 | _ iedcba***** | e.g., _ (i div 2)edcbazyxwv | Helps traversing a Merkle tree during authentication path verification. See extended description below. |
assert_vector | 64 | _ | _ | Assert equality of st(i) to st(i+5) for 0 <= i < 4 . Crashes the VM if any pair is unequal. |
absorb_init | 72 | _jihgfedcba | _jihgfedcba | Resets the Sponge's state and absorbs the stack's ten top-most elements. |
absorb | 80 | _jihgfedcba | _jihgfedcba | Absorbs the stack's ten top-most elements into the Sponge state. |
squeeze | 88 | _jihgfedcba | _zyxwvutsrq | Squeezes the Sponge, overwriting the stack's ten top-most elements |
The instruction hash
works as follows.
The stack's 10 top-most elements (jihgfedcba
) are reversed and concatenated with six zeros, resulting in abcdefghij000000
.
The permutation xlix
is applied to abcdefghij000000
, resulting in αβγδεζηθικuvwxyz
.
The first five elements of this result, i.e., αβγδε
, are reversed and written to the stack, overwriting st5
through st9
.
The top elements of the stack st0
through st4
are set to zero.
For example, the old stack was _ jihgfedcba
and the new stack is _ εδγβα 00000
.
The instruction divine_sibling
works as follows.
The 11th 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 st5
through st9
, 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) movesedcba
into registersst0
throughst4
and moveszyxwv
into registersst5
throughst9
, or - (
i
= 1 mod 2, i.e., current node is right sibling) does not change registersst5
throughst9
and moveszyxwv
into registersst0
throughst4
.
The 11th element of the operational stack i
is shifted by 1 bit to the right, i.e., the least-significant bit is dropped.
In conjunction with instruction hash
and assert_vector
, the instruction divine_sibling
allows to efficiently verify a Merkle authentication path.
The instructions absorb_init
, absorb
, and squeeze
are the interface for using the permutation xlix
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 absorb_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 OpStack | new OpStack | Description |
---|---|---|---|---|
add | 34 | _ b a | _ c | Computes the sum (c ) of the top two elements of the stack (b and a ) over the field. |
mul | 42 | _ b a | _ c | Computes the product (c ) of the top two elements of the stack (b and a ) over the field. |
invert | 96 | _ 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 | 50 | _ b a | _ (a == b) | Tests the top two stack elements for equality. |
Bitwise Arithmetic on Stack
Instruction | Opcode | old OpStack | new OpStack | 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., . 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 a or b is not u32. The result might be no u32 – care advised. |
div | 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 OpStack | new OpStack | Description |
---|---|---|---|---|
xxadd | 104 | _ z y x b c a | _ z y x w v u | Adds the two extension field elements encoded by field elements z y x and b c a , overwriting the top-most extension field element with the result. |
xxmul | 112 | _ z y x b c a | _ z y x w v u | Multiplies the two extension field elements encoded by field elements z y x and b c a , overwriting the top-most extension field element with the result. |
xinvert | 120 | _ 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 | 58 | _ z y x a | _ w v u | Scalar multiplication of the extension field element encoded by field elements z y x with field element a . Overwrites z y x with the result. |
Input/Output
Instruction | Opcode | old OpStack | new OpStack | Description |
---|---|---|---|---|
read_io | 128 | _ | _ a | Reads a B-Field element from standard input and pushes it to the stack. |
write_io | 66 | _ a | _ | Pops a from the stack and writes it to standard output. |
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., where is the Oxfoi prime, . 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 . 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 of the longest AET determines the padded height for all tables, which is .
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 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 1.
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 , which is 10 |
*MaxMinusIndexInChunkInv | the inverse-or-zero of |
*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 (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 toAddress
mod , - column
MaxMinusIndexInChunkInv
is set to the inverse-or-zero of , - 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 for some and . 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 .
Initial Constraints
- The
Address
is 0. - The
IndexInChunk
is 0. - The indicator
IsHashInputPadding
is 0. - The
InstructionLookupServerLogDerivative
is 0. PrepareChunkRunningEvaluation
has absorbedInstruction
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 ofIndexInChunk
. - The
IndexInChunk
is or theMaxMinusIndexInChunkInv
is the inverse ofIndexInChunk
. - 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 , it increases by 1. Else, theIndexInChunk
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, thenInstruction
in the next row is 1. - If
IsHashInputPadding
is 1 in the current row thenInstruction
in the next row is 0. - If
IsHashInputPadding
is 1 in the current row andIndexInChunk
is in the current row thenIsTablePadding
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 , thenPrepareChunkRunningEvaluation
absorbs theInstruction
in the next row with respect to challenge 🪑. Otherwise,PrepareChunkRunningEvaluation
resets and absorbs theInstruction
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 , thenSendChunkRunningEvaluation
absorbsPrepareChunkRunningEvaluation
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 or the indicatorIsTablePadding
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 TableRunningProductOpStackTable
for the Permutation Argument with the OpStack 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 OpStack Table, the RAM Table, and the JumpStack Table.
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 three memory-like tables.
In fact, all memory-like tables keep looking up clock jump differences in their padding section.
All these clock jumps are guaranteed to have magnitude 1 due to the Permutation Arguments with the respective memory-like tables.
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 .
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” |
---|---|---|---|---|---|---|
foo | 17 | … | 22 | |||
hash | 17 | … | 22 | |||
bar | 1337 | … | 22 |
In order to verify the correctness of RunningEvaluationHashInput
, the corresponding transition constraint needs to conditionally “activate” on row-tuple (, ), where it is conditional on ci_next
(not ci
), and verifies absorption of the next row, i.e., row .
However, in order to verify the correctness of RunningEvaluationHashDigest
, the corresponding transition constraint needs to conditionally “activate” on row-tuple (, ), where it is conditional on ci
(not ci_next
), and verifies absorption of the next row, i.e., row .
Initial Constraints
- The cycle counter
clk
is 0. - The previous instruction
previous_instruction
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
throughst15
with respect to indeterminate 🥬 equals the public part of program digest challenge, 🫑. See program attestation for more details. - The operational stack pointer
osp
is 16. - The operational stack value
osv
is 0. - The RAM pointer
ramp
is 0. RunningEvaluationStandardInput
is 1.RunningEvaluationStandardOutput
is 1.InstructionLookupClientLogDerivative
has absorbed the first row with respect to challenges 🥝, 🥥, and 🫐 and indeterminate 🪥.RunningProductOpStackTable
has absorbed the first row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤.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 ishash
. Otherwise, it is 1.RunningEvaluationHashDigest
is 1.RunningEvaluationSponge
is 1.U32LookupClientLogDerivative
is 0.ClockJumpDifferenceLookupServerLogDerivative
is 0.
Initial Constraints as Polynomials
clk
previous_instruction
ip
jsp
jso
jsd
st0
st1
st2
st3
st4
st5
st6
st7
st8
st9
st10
🥬^5 + st11·🥬^4 + st12·🥬^3 + st13·🥬^2 + st14·🥬 + st15 - 🫑
osp
osv
ramp
RunningEvaluationStandardInput - 1
RunningEvaluationStandardOutput - 1
InstructionLookupClientLogDerivative · (🪥 - 🥝·ip - 🥥·ci - 🫐·nia) - 1
RunningProductOpStackTable - (🪤 - 🍋·clk - 🍊·ib1 - 🍉·osp - 🫒·osv)
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
throughib7
corresponds to the current instructionci
. - 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 instruction bit
ib7
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^7·ib7 + 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)
ib7·(ib7 - 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. - The current instruction
ci
in the current row is copied intoprevious_instruction
in the next row or the next row is a padding row. - The running evaluation for standard input absorbs
st0
of the next row with respect to 🛏 if the current instruction isread_io
, and remains unchanged otherwise. - The running evaluation for standard output absorbs
st0
of the next row with respect to 🧯 if the current instruction in the next row iswrite_io
, and remains unchanged otherwise. - 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 product for the OpStack Table absorbs the next row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤.
- The running product for the RAM Table absorbs the next row with respect to challenges 🍍, 🍈, 🍎, and 🌽 and indeterminate 🛋.
- The running product for the JumpStack 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
absorb_init
,absorb
, orsqueeze
, then the running evaluation “Sponge” absorbs the current instruction and the next row with respect to challenges 🧅 and 🧄₀ through 🧄₉ and indeterminate 🧽. Otherwise, it remains unchanged. -
- If the current instruction is
split
, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulatesst0
andst1
in the next row andci
in the current row with respect to challenges 🥜, 🌰, and 🥑, and indeterminate 🧷. - If the current instruction is
lt
,and
,xor
, orpow
, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulatesst0
,st1
, andci
in the current row andst0
in the next row with respect to challenges 🥜, 🌰, 🥑, and 🥕, and indeterminate 🧷. - If the current instruction is
log_2_floor
, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulatesst0
andci
in the current row andst0
in the next row with respect to challenges 🥜, 🥑, and 🥕, and indeterminate 🧷. - If the current instruction is
div
, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates bothst0
in the next row andst1
in the current row as well as the constantsopcode(lt)
and1
with respect to challenges 🥜, 🌰, 🥑, and 🥕, and indeterminate 🧷.st0
in the current row andst1
in the next row as well asopcode(split)
with respect to challenges 🥜, 🌰, and 🥑, and indeterminate 🧷.
- If the current instruction is
pop_count
, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulatesst0
andci
in the current row andst0
in the next row with respect to challenges 🥜, 🥑, and 🥕, and indeterminate 🧷. - 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.
- If the current instruction is
- The running sum for the logarithmic derivative of the clock jump difference lookup argument accumulates the next row's
clk
with the appropriate multiplicitycjd_mul
with respect to indeterminate 🪞.
Transition Constraints as Polynomials
clk' - (clk + 1)
IsPadding·(IsPadding' - IsPadding)
(1 - IsPadding')·(previous_instruction' - ci)
(ci - opcode(read_io))·(RunningEvaluationStandardInput' - RunningEvaluationStandardInput)
+ read_io_deselector·(RunningEvaluationStandardInput' - 🛏·RunningEvaluationStandardInput - st0')
(ci' - opcode(write_io))·(RunningEvaluationStandardOutput' - RunningEvaluationStandardOutput)
+ write_io_deselector'·(RunningEvaluationStandardOutput' - 🧯·RunningEvaluationStandardOutput - st0')
(1 - IsPadding') · ((InstructionLookupClientLogDerivative' - InstructionLookupClientLogDerivative) · (🛁 - 🥝·ip' - 🥥·ci' - 🫐·nia') - 1)
+ IsPadding'·(RunningProductInstructionTable' - RunningProductInstructionTable)
RunningProductOpStackTable' - RunningProductOpStackTable·(🪤 - 🍋·clk' - 🍊·ib1' - 🍉·osp' - 🫒·osv')
RunningProductRamTable' - RunningProductRamTable·(🛋 - 🍍·clk' - 🍈·ramp' - 🍎·ramv' - 🌽·previous_instruction')
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(absorb_init))·(ci - opcode(absorb)·(ci - opcode(squeeze))·(RunningEvaluationHashDigest' - RunningEvaluationHashDigest)
+ (absorb_init_deselector + absorb_deselector + squeeze_deselector)
·(RunningEvaluationSponge' - 🧽·RunningEvaluationSponge - 🧅·ci - 🧄₀·st0' - 🧄₁·st1' - 🧄₂·st2' - 🧄₃·st3' - 🧄₄·st4' - 🧄₅·st5' - 🧄₆·st6' - 🧄₇·st7' - 🧄₈·st8' - 🧄₉·st9')
-
split_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0' - 🌰·st1' - 🥑·ci) - 1)
+ lt_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0') - 1)
+ and_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0') - 1)
+ xor_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0') - 1)
+ pow_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0') - 1)
+ log_2_floor_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🥑·ci - 🥕·st0') - 1)
+ div_deselector·(
(U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0' - 🌰·st1 - 🥑·opcode(lt) - 🥕·1)·(🧷 - 🥜·st0 - 🌰·st1' - 🥑·opcode(split))
- (🧷 - 🥜·st0' - 🌰·st1 - 🥑·opcode(lt) - 🥕·1)
- (🧷 - 🥜·st0 - 🌰·st1' - 🥑·opcode(split))
)
+ pop_count_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🥑·ci - 🥕·st0') - 1)
+ (1 - ib2)·(U32LookupClientLogDerivative' - U32LookupClientLogDerivative)
(ClockJumpDifferenceLookupServerLogDerivative' - ClockJumpDifferenceLookupServerLogDerivative)
·(🪞 - clk') - cjd_mul'
Terminal Constraints
- In the last row, register “current instruction”
ci
is 0, corresponding to instructionhalt
.
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 |
keep_ram | RAM does not change, i.e.,registers ramp and ramv do not change |
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 |
stack_grows_and_top_2_unconstrained | operational stack elements starting from st1 are shifted down by one position, highest two elements of the resulting stack are unconstrained |
grow_stack | operational stack elements are shifted down by one position, top element of the resulting stack is unconstrained |
stack_remains_and_top_11_unconstrained | operational stack's top 11 elements are unconstrained, rest of stack remains unchanged |
stack_remains_and_top_10_unconstrained | operational stack's top 10 elements are unconstrained, rest of stack remains unchanged |
stack_remains_and_top_3_unconstrained | operational stack's top 3 elements are unconstrained, rest of stack remains unchanged |
unary_operation | operational stack's top-most element is unconstrained, rest of stack remains unchanged |
keep_stack | operational stack remains unchanged |
stack_shrinks_and_top_3_unconstrained | operational stack elements starting from st3 are shifted up by one position, highest three elements of the resulting stack are unconstrained. Needs hv0 |
binary_operation | operational stack elements starting from st2 are shifted up by one position, highest two elements of the resulting stack are unconstrained. Needs hv0 |
shrink_stack | operational stack elements starting from st1 are shifted up by one position. Needs hv0 |
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 | keep_ram | keep_jump_stack | step_1 | step_2 | stack_grows_and_top_2_unconstrained | grow_stack | stack_remains_and_top_11_unconstrained | stack_remains_and_top_10_unconstrained | stack_remains_and_top_3_unconstrained | unary_operation | keep_stack | stack_shrinks_and_top_3_unconstrained | binary_operation | shrink_stack |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
pop | x | x | x | ||||||||||||
push + a | x | x | x | ||||||||||||
divine | x | x | x | ||||||||||||
dup + i | x | x | x | x | |||||||||||
swap + i | x | x | x | ||||||||||||
nop | x | x | x | ||||||||||||
skiz | x | x | x | ||||||||||||
call + d | x | x | |||||||||||||
return | x | x | |||||||||||||
recurse | x | x | x | ||||||||||||
assert | x | x | x | ||||||||||||
halt | x | x | x | ||||||||||||
read_mem | x | x | |||||||||||||
write_mem | x | x | |||||||||||||
hash | x | x | x | ||||||||||||
divine_sibling | x | x | x | ||||||||||||
assert_vector | x | x | x | ||||||||||||
absorb_init | x | x | x | ||||||||||||
absorb | x | x | x | ||||||||||||
squeeze | x | x | x | ||||||||||||
add | x | x | x | ||||||||||||
mul | x | x | x | ||||||||||||
invert | x | x | x | ||||||||||||
eq | x | x | x | ||||||||||||
split | x | x | x | ||||||||||||
lt | x | x | x | ||||||||||||
and | x | x | x | ||||||||||||
xor | x | x | x | ||||||||||||
log_2_floor | x | x | x | ||||||||||||
pow | x | x | x | ||||||||||||
div | x | x | x | ||||||||||||
pop_count | x | x | x | ||||||||||||
xxadd | x | x | x | ||||||||||||
xxmul | x | x | x | ||||||||||||
xinvert | x | x | x | ||||||||||||
xbmul | x | x | x | ||||||||||||
read_io | x | x | x | ||||||||||||
write_io | 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 dup
and swap
, it is beneficial to have polynomials that evaluate to 1 if the instruction's argument i
is a specific value, and to 0 otherwise.
This allows indicating which registers are constraint, and in which way they are, depending on i
.
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 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.
Below, you can find a list of all 16 indicator polynomials.
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 are the 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 keep_ram
Description
- The RAM pointer
ramp
does not change. - The RAM value
ramv
does not change.
Polynomials
ramp' - ramp
ramv' - ramv
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 stack_grows_and_top_2_unconstrained
Description
- The stack element in
st1
is moved intost2
. - The stack element in
st2
is moved intost3
. - The stack element in
st3
is moved intost4
. - The stack element in
st4
is moved intost5
. - The stack element in
st5
is moved intost6
. - The stack element in
st6
is moved intost7
. - The stack element in
st7
is moved intost8
. - The stack element in
st8
is moved intost9
. - The stack element in
st9
is moved intost10
. - The stack element in
st10
is moved intost11
. - The stack element in
st11
is moved intost12
. - The stack element in
st12
is moved intost13
. - The stack element in
st13
is moved intost14
. - The stack element in
st14
is moved intost15
. - The stack element in
st15
is moved to the top of OpStack underflow, i.e.,osv
. - The OpStack pointer is incremented by 1.
Polynomials
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
osv' - st15
osp' - (osp + 1)
Group grow_stack
Contains all constraints from instruction group stack_grows_and_top_2_unconstrained
, and additionally:
Description
- The stack element in
st0
is moved intost1
.
Polynomials
st1' - st0
Group stack_remains_and_top_11_unconstrained
Description
- 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 top of the OpStack underflow, i.e.,
osv
, does not change. - The OpStack pointer does not change.
Polynomials
st11' - st11
st12' - st12
st13' - st13
st14' - st14
st15' - st15
osv' - osv
osp' - osp
Group stack_remains_and_top_10_unconstrained
Contains all constraints from instruction group stack_remains_and_top_11_unconstrained
, and additionally:
Description
- The stack element in
st10
does not change.
Polynomials
st10' - st10
Group stack_remains_and_top_3_unconstrained
Contains all constraints from instruction group stack_remains_and_top_10_unconstrained
, and additionally:
Description
- 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.
Polynomials
st3' - st3
st4' - st4
st5' - st5
st6' - st6
st7' - st7
st8' - st8
st9' - st9
Group unary_operation
Contains all constraints from instruction group stack_remains_and_top_3_unconstrained
, and additionally:
Description
- The stack element in
st1
does not change. - The stack element in
st2
does not change.
Polynomials
st1' - st1
st2' - st2
Group keep_stack
Contains all constraints from instruction group unary_operation
, and additionally:
Description
- The stack element in
st0
does not change.
Polynomials
st0' - st0
Group stack_shrinks_and_top_3_unconstrained
This instruction group requires helper variable hv0
to hold the multiplicative inverse of (osp - 16)
.
In effect, this means that the OpStack pointer can only be decremented if it is not 16, i.e., if OpStack Underflow Memory is not empty.
Since the stack can only change by one element at a time, this prevents stack underflow.
Description
- The stack element in
st4
is moved intost3
. - The stack element in
st5
is moved intost4
. - The stack element in
st6
is moved intost5
. - The stack element in
st7
is moved intost6
. - The stack element in
st8
is moved intost7
. - The stack element in
st9
is moved intost8
. - The stack element in
st10
is moved intost9
. - The stack element in
st11
is moved intost10
. - The stack element in
st12
is moved intost11
. - The stack element in
st13
is moved intost12
. - The stack element in
st14
is moved intost13
. - The stack element in
st15
is moved intost14
. - The stack element at the top of OpStack underflow, i.e.,
osv
, is moved intost15
. - The OpStack pointer is decremented by 1.
- The helper variable register
hv0
holds the inverse of(osp - 16)
.
Polynomials
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' - osv
osp' - (osp - 1)
(osp - 16)·hv0 - 1
Group binary_operation
Contains all constraints from instruction group stack_shrinks_and_top_3_unconstrained
, and additionally:
Description
- The stack element in
st2
is moved intost1
. - The stack element in
st3
is moved intost2
.
Polynomials
st1' - st2
st2' - st3
Group shrink_stack
Contains all constraints from instruction group binary_operation
, and additionally:
Description
- The stack element in
st1
is moved intost0
.
Polynomials
st0' - st1
Instruction-Specific Transition Constraints
Instruction pop
This instruction uses all constraints defined by instruction groups step_1
, shrink_stack
, and keep_ram
.
It has no additional transition constraints.
Instruction push
+ a
This instruction uses all constraints defined by instruction groups step_2
, grow_stack
, and keep_ram
.
Additionally, it defines the following transition constraints.
Description
- The instruction's argument
a
is moved onto the stack.
Polynomials
st0' - nia
Instruction divine
This instruction uses all constraints defined by instruction groups step_2
, grow_stack
, and keep_ram
.
It has no additional transition constraints.
Instruction dup
+ i
This instruction makes use of indicator polynomials. For their definition, please refer to the corresponding section.
This instruction uses all constraints defined by instruction groups decompose_arg
, step_2
, grow_stack
, and keep_ram
.
Additionally, it defines the following transition constraints.
Description
- If
i
is 0, thenst0
is put on top of the stack. - If
i
is 1, thenst1
is put on top of the stack. - If
i
is 2, thenst2
is put on top of the stack. - If
i
is 3, thenst3
is put on top of the stack. - If
i
is 4, thenst4
is put on top of the stack. - If
i
is 5, thenst5
is put on top of the stack. - If
i
is 6, thenst6
is put on top of the stack. - If
i
is 7, thenst7
is put on top of the stack. - If
i
is 8, thenst8
is put on top of the stack. - If
i
is 9, thenst9
is put on top of the stack. - If
i
is 10, thenst10
is put on top of the stack. - If
i
is 11, thenst11
is put on top of the stack. - If
i
is 12, thenst12
is put on top of the stack. - If
i
is 13, thenst13
is put on top of the stack. - If
i
is 14, thenst14
is put on top of the stack. - If
i
is 15, thenst15
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)
Helper variable definitions for dup
+ i
For dup
+ i
, helper variables contain the binary decomposition of i
:
hv0 = i % 2
hv1 = (i >> 1) % 2
hv2 = (i >> 2) % 2
hv3 = (i >> 3) % 2
Instruction swap
+ i
This instruction makes use of indicator polynomials. For their definition, please refer to the corresponding section.
This instruction uses all constraints defined by instruction groups decompose_arg
, step_2
, and keep_ram
.
Additionally, it defines the following transition constraints.
Description
- Argument
i
is not 0. - If
i
is 1, thenst0
is moved intost1
. - If
i
is 2, thenst0
is moved intost2
. - If
i
is 3, thenst0
is moved intost3
. - If
i
is 4, thenst0
is moved intost4
. - If
i
is 5, thenst0
is moved intost5
. - If
i
is 6, thenst0
is moved intost6
. - If
i
is 7, thenst0
is moved intost7
. - If
i
is 8, thenst0
is moved intost8
. - If
i
is 9, thenst0
is moved intost9
. - If
i
is 10, thenst0
is moved intost10
. - If
i
is 11, thenst0
is moved intost11
. - If
i
is 12, thenst0
is moved intost12
. - If
i
is 13, thenst0
is moved intost13
. - If
i
is 14, thenst0
is moved intost14
. - If
i
is 15, thenst0
is moved intost15
. - If
i
is 1, thenst1
is moved intost0
. - If
i
is 2, thenst2
is moved intost0
. - If
i
is 3, thenst3
is moved intost0
. - If
i
is 4, thenst4
is moved intost0
. - If
i
is 5, thenst5
is moved intost0
. - If
i
is 6, thenst6
is moved intost0
. - If
i
is 7, thenst7
is moved intost0
. - If
i
is 8, thenst8
is moved intost0
. - If
i
is 9, thenst9
is moved intost0
. - If
i
is 10, thenst10
is moved intost0
. - If
i
is 11, thenst11
is moved intost0
. - If
i
is 12, thenst12
is moved intost0
. - If
i
is 13, thenst13
is moved intost0
. - If
i
is 14, thenst14
is moved intost0
. - If
i
is 15, thenst15
is moved intost0
. - If
i
is not 1, thenst1
does not change. - If
i
is not 2, thenst2
does not change. - If
i
is not 3, thenst3
does not change. - If
i
is not 4, thenst4
does not change. - If
i
is not 5, thenst5
does not change. - If
i
is not 6, thenst6
does not change. - If
i
is not 7, thenst7
does not change. - If
i
is not 8, thenst8
does not change. - If
i
is not 9, thenst9
does not change. - If
i
is not 10, thenst10
does not change. - If
i
is not 11, thenst11
does not change. - If
i
is not 12, thenst12
does not change. - If
i
is not 13, thenst13
does not change. - If
i
is not 14, thenst14
does not change. - If
i
is not 15, thenst15
does not change. - The top of the OpStack underflow, i.e.,
osv
, does not change. - The OpStack pointer does not change.
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)
osv' - osv
osp' - osp
Helper variable definitions for swap
+ i
For swap
+ i
, helper variables contain the binary decomposition of i
:
hv0 = i % 2
hv1 = (i >> 1) % 2
hv2 = (i >> 2) % 2
hv3 = (i >> 3) % 2
Instruction nop
This instruction uses all constraints defined by instruction groups step_1
, keep_stack
, and keep_ram
.
It has no additional transition constraints.
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 hv1
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.
This instruction uses all constraints defined by instruction groups keep_jump_stack
, shrink_stack
, and keep_ram
.
Additionally, it defines the following transition constraints.
Description
- Helper variable
hv1
is the inverse ofst0
or 0. - Helper variable
hv1
is the inverse ofst0
orst0
is 0. - The next instruction
nia
is decomposed into helper variableshv2
throughhv6
. - The indicator helper variable
hv2
is either 0 or 1. Here,hv2 == 1
means thatnia
takes an argument. - 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. - The helper variable
hv6
is either 0 or 1 or 2 or 3. - If
st0
is non-zero, registerip
is incremented by 1. Ifst0
is 0 andnia
takes no argument, registerip
is incremented by 2. Ifst0
is 0 andnia
takes an argument, registerip
is incremented by 3.
Written as Disjunctive Normal Form, the last constraint can be expressed as:
- (Register
st0
is 0 orip
is incremented by 1), and (st0
has a multiplicative inverse orhv2
is 1 orip
is incremented by 2), and (st0
has a multiplicative inverse orhv2
is 0 orip
is incremented by 3).
Since the three cases are mutually exclusive, the three respective polynomials can be summed up into one.
Polynomials
(st0·hv1 - 1)·hv1
(st0·hv1 - 1)·st0
nia - hv2 - 2·hv3 - 8·hv4 - 32·hv5 - 128·hv6
hv2·(hv2 - 1)
hv3·(hv3 - 1)·(hv3 - 2)·(hv3 - 3)
hv4·(hv4 - 1)·(hv4 - 2)·(hv4 - 3)
hv5·(hv5 - 1)·(hv5 - 2)·(hv5 - 3)
hv6·(hv6 - 1)·(hv6 - 2)·(hv6 - 3)
(ip' - (ip + 1)·st0)
+ ((ip' - (ip + 2))·(st0·hv1 - 1)·(hv2 - 1))
+ ((ip' - (ip + 3))·(st0·hv1 - 1)·hv2)
Helper variable definitions for skiz
hv1 = inverse(st0)
(ifst0 ≠ 0
)hv2 = nia mod 2
hv3 = (nia >> 1) mod 4
hv4 = (nia >> 3) mod 4
hv5 = (nia >> 5) mod 4
hv6 = nia >> 7
Instruction call
+ d
This instruction uses all constraints defined by instruction groups keep_stack
and keep_ram
.
Additionally, it defines the following transition constraints.
Description
- The jump stack pointer
jsp
is incremented by 1. - The jump's origin
jso
is set to the current instruction pointerip
plus 2. - The jump's destination
jsd
is set to the instruction's argumentd
. - The instruction pointer
ip
is set to the instruction's argumentd
.
Polynomials
jsp' - (jsp + 1)
jso' - (ip + 2)
jsd' - nia
ip' - nia
Instruction return
This instruction uses all constraints defined by instruction groups keep_stack
and keep_ram
.
Additionally, it defines the following transition constraints.
Description
- The jump stack pointer
jsp
is decremented by 1. - The instruction pointer
ip
is set to the last call's originjso
.
Polynomials
jsp' - (jsp - 1)
ip' - jso
Instruction recurse
This instruction uses all constraints defined by instruction groups keep_jump_stack
, keep_stack
, and keep_ram
.
Additionally, it defines the following transition 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 destinationjsd
.
Polynomials
jsp' - jsp
jso' - jso
jsd' - jsd
ip' - jsd
Instruction assert
This instruction uses all constraints defined by instruction groups step_1
, shrink_stack
, and keep_ram
.
Additionally, it defines the following transition constraints.
Description
- The current top of the stack
st0
is 1.
Polynomials
st0 - 1
Instruction halt
This instruction uses all constraints defined by instruction groups step_1
, keep_stack
, and keep_ram
.
Additionally, it defines the following transition constraints.
Description
- The instruction executed in the following step is instruction
halt
.
Polynomials
ci' - ci
Instruction read_mem
This instruction uses all constraints defined by instruction groups step_1
and grow_stack
.
Additionally, it defines the following transition constraints.
Description
- The RAM pointer is overwritten with stack element
st0
. - The top of the stack is overwritten with the RAM value.
Polynomials
ramp' - st0
st0' - ramv
Instruction write_mem
This instruction uses all constraints defined by instruction groups step_1
and shrink_stack
.
Additionally, it defines the following transition constraints.
Description
- The RAM pointer is overwritten with stack element
st1
. - The RAM value is overwritten with the top of the stack.
Polynomials
ramp' - st1
ramv' - st0
Instruction hash
This instruction uses all constraints defined by instruction groups step_1
, stack_remains_and_top_10_unconstrained
, and keep_ram
.
It has no additional transition constraints.
Two Evaluation Arguments with the Hash Table guarantee correct transition.
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
.
This instruction uses all constraints defined by instruction groups step_1
, stack_remains_and_top_11_unconstrained
, and keep_ram
.
Additionally, it defines the following transition constraints.
Description
- Helper variable
hv0
is either 0 or 1. - The 11th stack register is shifted by 1 bit to the right.
- If
hv0
is 0, thenst0
does not change. - If
hv0
is 0, thenst1
does not change. - If
hv0
is 0, thenst2
does not change. - If
hv0
is 0, thenst3
does not change. - If
hv0
is 0, thenst4
does not change. - If
hv0
is 1, thenst0
is copied tost5
. - If
hv0
is 1, thenst1
is copied tost6
. - If
hv0
is 1, thenst2
is copied tost7
. - If
hv0
is 1, thenst3
is copied tost8
. - If
hv0
is 1, thenst4
is copied tost9
.
Polynomials
hv0·(hv0 - 1)
st10'·2 + hv0 - st10
(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)
Helper variable definitions for divine_sibling
Since st10
contains the Merkle tree node index,
hv0
holds the result ofst10 % 2
(the node index's least significant bit, indicating whether it is a left/right node).
Instruction assert_vector
This instruction uses all constraints defined by instruction groups step_1
, keep_stack
, and keep_ram
.
Additionally, it defines the following transition constraints.
Description
- Register
st0
is equal tost5
. - Register
st1
is equal tost6
. - Register
st2
is equal tost7
. - Register
st3
is equal tost8
. - Register
st4
is equal tost9
.
Polynomials
st5 - st0
st6 - st1
st7 - st2
st8 - st3
st9 - st4
Instruction absorb_init
This instruction uses all constraints defined by instruction groups step_1
, keep_stack
, and keep_ram
.
Beyond that, this instruction has no transition constraints.
Instead, correct transition is guaranteed by the Hash Table.
Instruction absorb
This instruction uses all constraints defined by instruction groups step_1
, keep_stack
, and keep_ram
.
Beyond that, this instruction has no transition constraints.
Instead, correct transition is guaranteed by the Hash Table.
Instruction squeeze
This instruction uses all constraints defined by instruction groups step_1
, stack_remains_and_top_10_unconstrained
, and keep_ram
.
Beyond that, this instruction has no transition constraints.
Instead, correct transition is guaranteed by the Hash Table.
Instruction add
This instruction uses all constraints defined by instruction groups step_1
, binary_operation
, and keep_ram
.
Additionally, it defines the following transition constraints.
Description
- The sum of the top two stack elements is moved into the top of the stack.
Polynomials
st0' - (st0 + st1)
Instruction mul
This instruction uses all constraints defined by instruction groups step_1
, binary_operation
, and keep_ram
.
Additionally, it defines the following transition constraints.
Description
- The product of the top two stack elements is moved into the top of the stack.
Polynomials
st0' - st0·st1
Instruction invert
This instruction uses all constraints defined by instruction groups step_1
, unary_operation
, and keep_ram
.
Additionally, it defines the following transition constraints.
Description
- The top of the stack's inverse is moved into the top of the stack.
Polynomials
st0'·st0 - 1
Instruction eq
This instruction uses all constraints defined by instruction groups step_1
, binary_operation
, and keep_ram
.
Additionally, it defines the following transition constraints.
Description
- Helper variable
hv1
is the inverse of the difference of the stack's two top-most elements or 0. - Helper variable
hv1
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
hv1·(hv1·(st1 - st0) - 1)
(st1 - st0)·(hv1·(st1 - st0) - 1)
st0' - (1 - hv1·(st1 - st0))
Helper variable definitions for eq
hv1 = inverse(rhs - lhs)
ifrhs - lhs ≠ 0
.hv1 = 0
ifrhs - lhs = 0
.
Instruction split
This instruction uses all constraints defined by instruction groups step_1
, stack_grows_and_top_2_unconstrained
, and keep_ram
.
Additionally, it defines the following transition 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 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))
iflo ≠ 0
.hv0 = 0
iflo = 0
.
Instruction lt
This instruction uses all constraints defined by instruction groups step_1
, binary_operation
, and keep_ram
.
Beyond that, this instruction has no transition constraints.
Instead, correct transition is guaranteed by the U32 Table.
Instruction and
This instruction uses all constraints defined by instruction groups step_1
, binary_operation
, and keep_ram
.
Beyond that, this instruction has no transition constraints.
Instead, correct transition is guaranteed by the U32 Table.
Instruction xor
This instruction uses all constraints defined by instruction groups step_1
, binary_operation
, and keep_ram
.
Beyond that, this instruction has no transition constraints.
Instead, correct transition is guaranteed by the U32 Table.
Instruction log2floor
This instruction uses all constraints defined by instruction groups step_1
, unary_operation
, and keep_ram
.
Beyond that, this instruction has no transition constraints.
Instead, correct transition is guaranteed by the U32 Table.
Instruction pow
This instruction uses all constraints defined by instruction groups step_1
, binary_operation
, and keep_ram
.
Beyond that, this instruction has no transition constraints.
Instead, correct transition is guaranteed by the U32 Table.
Instruction div
This instruction uses all constraints defined by instruction groups step_1
, stack_remains_and_top_3_unconstrained
, and keep_ram
.
Additionally, it defines the following transition constraints.
Recall that instruction div
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 denominatord
, and - all four of
n
,d
,q
, andr
are u32s.
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 uses all constraints defined by instruction groups step_1
, unary_operation
, and keep_ram
.
Beyond that, this instruction has no transition constraints.
Instead, correct transition is guaranteed by the U32 Table.
Instruction xxadd
This instruction uses all constraints defined by instruction groups step_1
, stack_remains_and_top_3_unconstrained
, and keep_ram
.
Additionally, it defines the following transition constraints.
Description
- The result of adding
st0
tost3
is moved intost0
. - The result of adding
st1
tost4
is moved intost1
. - The result of adding
st2
tost5
is moved intost2
.
Polynomials
st0' - (st0 + st3)
st1' - (st1 + st4)
st2' - (st2 + st5)
Instruction xxmul
This instruction uses all constraints defined by instruction groups step_1
, stack_remains_and_top_3_unconstrained
, and keep_ram
.
Additionally, it defines the following transition 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
.
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)
Instruction xinvert
This instruction uses all constraints defined by instruction groups step_1
, stack_remains_and_top_3_unconstrained
, and keep_ram
.
Additionally, it defines the following transition 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
This instruction uses all constraints defined by instruction groups step_1
, stack_shrinks_and_top_3_unconstrained
, and keep_ram
.
Additionally, it defines the following transition 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
.
Polynomials
st0' - st0·st1
st1' - st0·st2
st2' - st0·st3
Instruction read_io
This instruction uses all constraints defined by instruction groups step_1
, grow_stack
, and keep_ram
.
It has no additional transition constraints.
An Evaluation Argument with the list of input symbols guarantees correct transition.
Instruction write_io
This instruction uses all constraints defined by instruction groups step_1
, shrink_stack
, and keep_ram
.
It has no additional transition constraints.
An Evaluation Argument with the list of output symbols guarantees correct transition.
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 operational 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 Operational Stack Table.
Base Columns
The Operational Stack Table consists of 4 columns:
- the cycle counter
clk
- the shrink stack indicator
shrink_stack
- the operational stack value
osv
, and - the operational stack pointer
osp
.
Clock | Shrink Stack Indicator | Op Stack Pointer | Op Stack Value |
---|---|---|---|
- | - | - | - |
Columns clk
, shrink_stack
, osp
, and osv
correspond to columns clk
, ib1
, osp
, and osv
in the Processor Table, respectively.
A Permutation Argument with the Processor Table establishes that, selecting the columns with these labels, the two tables' sets of rows are identical.
In order to guarantee memory consistency, the rows of the operational stack table are sorted by operational stack pointer osp
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 osp
does not change, then osv
can only change if the shrink stack indicator shrink_stack
is set.
Consequently, row [5, push, 9, 42]
being followed by row [_, _, 9, 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.
TritonVM has 16 stack registers, st0
through st15
.
Execution trace:
clk | ci | nia | st0 | st1 | st2 | st3 | Op Stack Underflow Memory | osp | osv |
---|---|---|---|---|---|---|---|---|---|
0 | push | 42 | 0 | 0 | 0 | 0 | [ ] | 4 | 0 |
1 | push | 43 | 42 | 0 | 0 | 0 | [0] | 5 | 0 |
2 | push | 44 | 43 | 42 | 0 | 0 | [0,0] | 6 | 0 |
3 | push | 45 | 44 | 43 | 42 | 0 | [0,0,0] | 7 | 0 |
4 | push | 46 | 45 | 44 | 43 | 42 | [0,0,0,0] | 8 | 0 |
5 | push | 47 | 46 | 45 | 44 | 43 | [42,0,0,0,0] | 9 | 42 |
6 | push | 48 | 47 | 46 | 45 | 44 | [43,42,0,0,0,0] | 10 | 43 |
7 | nop | pop | 48 | 47 | 46 | 45 | [44,43,42,0,0,0,0] | 11 | 44 |
8 | pop | pop | 48 | 47 | 46 | 45 | [44,43,99,0,0,0,0] | 11 | 44 |
9 | pop | pop | 47 | 46 | 45 | 44 | [43,99,0,0,0,0] | 10 | 43 |
10 | pop | pop | 46 | 45 | 44 | 43 | [99,0,0,0,0] | 9 | 99 |
11 | pop | push | 45 | 44 | 43 | 99 | [0,0,0,0] | 8 | 0 |
12 | push | 77 | 44 | 43 | 99 | 0 | [0,0,0] | 7 | 0 |
13 | swap | 4 | 77 | 44 | 43 | 99 | [0,0,0,0] | 8 | 0 |
14 | push | 78 | 99 | 44 | 43 | 77 | [0,0,0,0] | 8 | 0 |
15 | swap | 4 | 78 | 99 | 44 | 43 | [77,0,0,0,0] | 9 | 77 |
16 | push | 79 | 43 | 99 | 44 | 78 | [77,0,0,0,0] | 9 | 77 |
17 | pop | pop | 79 | 43 | 99 | 44 | [78,77,0,0,0,0] | 10 | 78 |
18 | pop | pop | 43 | 99 | 44 | 78 | [77,0,0,0,0] | 9 | 77 |
19 | pop | pop | 99 | 44 | 78 | 77 | [0,0,0,0] | 8 | 0 |
20 | pop | pop | 44 | 78 | 77 | 0 | [0,0,0] | 7 | 0 |
21 | pop | pop | 78 | 77 | 0 | 0 | [0,0] | 6 | 0 |
22 | pop | pop | 77 | 0 | 0 | 0 | [0] | 5 | 0 |
23 | pop | pop | 0 | 0 | 0 | 0 | [ ] | 4 | 0 |
24 | pop | nop | 0 | 0 | 0 | 0 | 💥 | 3 | 0 |
Operational Stack Table:
clk | shrink_stack | (comment) | osp | osv |
---|---|---|---|---|
0 | 0 | (push ) | 4 | 0 |
23 | 1 | (pop ) | 4 | 0 |
1 | 0 | (push ) | 5 | 0 |
22 | 1 | (pop ) | 5 | 0 |
2 | 0 | (push ) | 6 | 0 |
21 | 1 | (pop ) | 6 | 0 |
3 | 0 | (push ) | 7 | 0 |
12 | 0 | (push ) | 7 | 0 |
20 | 1 | (pop ) | 7 | 0 |
4 | 0 | (push ) | 8 | 0 |
11 | 1 | (pop ) | 8 | 0 |
13 | 0 | (swap ) | 8 | 0 |
14 | 0 | (push ) | 8 | 0 |
19 | 1 | (pop ) | 8 | 0 |
5 | 0 | (push ) | 9 | 42 |
10 | 1 | (pop ) | 9 | 99 |
15 | 0 | (swap ) | 9 | 77 |
16 | 0 | (push ) | 9 | 77 |
18 | 1 | (pop ) | 9 | 77 |
6 | 0 | (push ) | 10 | 43 |
9 | 1 | (pop ) | 10 | 43 |
17 | 1 | (pop ) | 10 | 78 |
7 | 0 | (nop ) | 11 | 44 |
8 | 1 | (pop ) | 11 | 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 theClockJumpDifferenceLookupClientLogDerivative
column.
Padding
A padding row is a direct copy of the Op 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 Op 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 Op Stack table,
osp
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
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 .
Initial Constraints
clk
is 0osv
is 0.osp
is the number of available stack registers, i.e., 16.- 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 🪤. - The logarithmic derivative for the clock jump difference lookup
ClockJumpDifferenceLookupClientLogDerivative
is 0.
Initial Constraints as Polynomials
clk
osv
osp - 16
rppa - (🪤 - 🍋·clk - 🍊·ib1 - 🍉·osp - 🫒osv)
ClockJumpDifferenceLookupClientLogDerivative
Consistency Constraints
None.
Transition Constraints
-
- the
osp
increases by 1, or - the
osp
does not change AND theosv
does not change, or - the
osp
does not change AND the shrink stack indicatorshrink_stack
is 1.
- the
- The running product for the permutation argument with the Processor Table
rppa
absorbs the next row with respect to challenges 🍋, 🍊, 🍉, and 🫒 and indeterminate 🪤. - If the op stack pointer
osp
does not change, then the logarithmic derivative for the clock jump difference lookupClockJumpDifferenceLookupClientLogDerivative
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
osp
increases by 1 or theosp
does not change - the
osp
increases by 1 or theosv
does not change or the shrink stack indicatorshrink_stack
is 1
- the
rppa' = rppa·(🪤 - 🍋·clk' - 🍊·ib1' - 🍉·osp' - 🫒osv')
-
- the
osp
changes or the logarithmic derivative accumulates a summand, and - the
osp
does not change or the logarithmic derivative does not change.
- the
Transition Constraints as Polynomials
(osp' - (osp + 1))·(osp' - osp)
(osp' - (osp + 1))·(osv' - osv)·(1 - shrink_stack)
rppa' - rppa·(🪤 - 🍋·clk' - 🍊·ib1' - 🍉·osp' - 🫒osv')
(osp' - (osp + 1))·((ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative) · (🪞 - clk' + clk) - 1)
+ (osp' - osp)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)
Terminal Constraints
None.
Random Access Memory Table
The RAM is accessible through read_mem
and write_mem
commands.
Base Columns
The RAM Table has 7 columns:
- the cycle counter
clk
, - the instruction executed in the previous clock cycle
previous_instruction
, - RAM address pointer
ramp
, - the value of the memory at that address
ramv
, - helper variable
iord
("inverse oframp
difference", but elsewhere also "difference inverse" anddi
for short), - Bézout coefficient polynomial coefficient 0
bcpc0
, - Bézout coefficient polynomial coefficient 1
bcpc1
,
Clock | Previous Instruction | RAM Pointer | RAM Value | Inverse of RAM Pointer Difference | Bézout coefficient polynomial's coefficients 0 | Bézout coefficient polynomial's coefficients 1 |
---|---|---|---|---|---|---|
- | - | - | - | - | - | - |
Columns clk
, previous_instruction
, ramp
, and ramv
correspond to the columns of the same name in the Processor Table.
A permutation argument with the Processor Table establishes that, selecting the columns with these labels, the two tables' sets of rows are identical.
Column iord
helps with detecting a change of ramp
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 ramp
are contiguous.
Extension Columns
The RAM Table has 2 extension columns, rppa
and ClockJumpDifferenceLookupClientLogDerivative
.
- A Permutation Argument establishes that the rows in the RAM Table correspond to the rows of the Processor Table, after selecting for columns
clk
,ramp
,ramv
in both tables. The running product for this argument is contained in therppa
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 theClockJumpDifferenceLookupClientLogDerivative
column.
Sorting Rows
Up to order, the rows of the Hash Table in columns clk
, ramp
, ramv
are identical to the rows in the Processor Table in columns clk
, ramp
, and ramv
.
In the Hash Table, the rows are arranged such that they
- form contiguous regions of
ramp
, and - are sorted by cycle counter
clk
within each such region.
One way to achieve this is to sort by ramp
first, clk
second.
Coming back to iord
:
if the difference between ramp
in row and row is 0, then iord
in row is 0.
Otherwise, iord
in row is the multiplicative inverse of the difference between ramp
in row and ramp
in row .
In the last row, there being no next row, iord
is 0.
An example of the mechanics can be found below.
For reasons of display width, we abbreviate previous_instruction
by pi
.
For illustrative purposes only, we use four stack registers st0
through st3
in the example.
Triton VM has 16 stack registers, st0
through st15
.
Processor Table:
clk | pi | ci | nia | st0 | st1 | st2 | st3 | ramp | ramv |
---|---|---|---|---|---|---|---|---|---|
0 | - | push | 5 | 0 | 0 | 0 | 0 | 0 | 0 |
1 | push | push | 6 | 5 | 0 | 0 | 0 | 0 | 0 |
2 | push | write_mem | pop | 6 | 5 | 0 | 0 | 0 | 0 |
3 | write_mem | pop | push | 5 | 0 | 0 | 0 | 5 | 6 |
4 | pop | push | 15 | 0 | 0 | 0 | 0 | 5 | 6 |
5 | push | push | 16 | 15 | 0 | 0 | 0 | 5 | 6 |
6 | push | write_mem | pop | 16 | 15 | 0 | 0 | 5 | 6 |
7 | write_mem | pop | push | 15 | 0 | 0 | 0 | 15 | 16 |
8 | pop | push | 5 | 0 | 0 | 0 | 0 | 15 | 16 |
9 | push | read_mem | pop | 5 | 0 | 0 | 0 | 15 | 16 |
10 | read_mem | pop | pop | 6 | 5 | 0 | 0 | 5 | 6 |
11 | pop | pop | push | 5 | 0 | 0 | 0 | 5 | 6 |
12 | pop | push | 15 | 0 | 0 | 0 | 0 | 5 | 6 |
13 | push | read_mem | pop | 15 | 0 | 0 | 0 | 5 | 6 |
14 | read_mem | pop | pop | 16 | 15 | 0 | 0 | 15 | 16 |
15 | pop | pop | push | 15 | 0 | 0 | 0 | 15 | 16 |
16 | pop | push | 5 | 0 | 0 | 0 | 0 | 15 | 16 |
17 | push | push | 7 | 5 | 0 | 0 | 0 | 15 | 16 |
18 | push | write_mem | pop | 7 | 5 | 0 | 0 | 15 | 16 |
19 | write_mem | pop | push | 5 | 0 | 0 | 0 | 5 | 7 |
20 | pop | push | 15 | 0 | 0 | 0 | 0 | 5 | 7 |
21 | push | read_mem | push | 15 | 0 | 0 | 0 | 5 | 7 |
22 | read_mem | push | 5 | 16 | 15 | 0 | 0 | 15 | 16 |
23 | push | read_mem | halt | 5 | 16 | 15 | 0 | 15 | 16 |
24 | read_mem | halt | halt | 7 | 5 | 16 | 15 | 5 | 7 |
RAM Table:
clk | pi | ramp | ramv | iord |
---|---|---|---|---|
7 | write_mem | 15 | 16 | 0 |
8 | pop | 15 | 16 | 0 |
9 | push | 15 | 16 | 0 |
14 | read_mem | 15 | 16 | 0 |
15 | pop | 15 | 16 | 0 |
16 | pop | 15 | 16 | 0 |
17 | push | 15 | 16 | 0 |
18 | push | 15 | 16 | 0 |
22 | read_mem | 15 | 16 | 0 |
23 | push | 15 | 16 | -10 |
3 | write_mem | 5 | 6 | 0 |
4 | pop | 5 | 6 | 0 |
5 | push | 5 | 6 | 0 |
6 | push | 5 | 6 | 0 |
10 | read_mem | 5 | 6 | 0 |
11 | pop | 5 | 6 | 0 |
12 | pop | 5 | 6 | 0 |
13 | push | 5 | 6 | 0 |
19 | write_mem | 5 | 7 | 0 |
20 | pop | 5 | 7 | 0 |
21 | push | 5 | 7 | 0 |
24 | read_mem | 5 | 7 | -5 |
0 | - | 0 | 0 | 0 |
1 | push | 0 | 0 | 0 |
2 | push | 0 | 0 | 0 |
Padding
A padding row is a direct copy of the RAM 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.
Finally, the value of column iord
is set to 0 in 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 RAM Table and the Processor Table holds up.
Contiguity Argument
As a stepping stone to proving memory-consistency, it is necessary to prove that all regions of constant ramp
are contiguous. In simpler terms, this condition stipulates that after filtering the rows in the RAM Table for any given ramp
value, the resulting sublist of rows forms a contiguous sublist with no gaps. The contiguity establishes this property. What follows here is a summary of the Contiguity Argument for RAM Consistency.
The contiguity argument is a Randomized AIR without Preprocessing (RAP). In particular, there are 4 extension columns whose values depend on the verifier's challenge :
- The running product polynomial
rpp
, which accumulates a factor in every consecutive pair of rows (including the first) where the current row'sramp
value is different from the previous row'sramp
value. - The formal derivative
fd
, which is updated according to the product rule of differentiation and therefore tracks the formal derivative ofrpp
. - The Bézout coefficient 0
bc0
, which is the evaluation of the polynomial defined by the coefficients ofbcpc0
in . - The Bézout coefficient 1
bc1
, which is the evaluation of the polynomial defined by the coefficients ofbcpc1
in .
The contiguity of regions of constant ramp
is implied by the square-freeness (as a polynomial in ) of rpp
. If rpp
is square-free, then the Bézout relation
holds for any . However, if rp
is not square-free, indicating a malicious prover, then the above relation holds in a negligible fraction of possible 's. Therefore, the AIR enforces the Bézout relation as a terminal boundary constraint.
Inner Sorting
The second stepping stone to proving memory-consistency is to establish that the rows in each region of constant ramp
are correctly sorted for clk
in ascending order. To prove this property, we show that all differences of clk
values difference greater than 1 in consecutive rows with the same ramp
value – the clock jump differences – are contained in the clk
table of the Processor Table. What follows here is a summary of the construction reduced to the RAM Table; the bulk of the logic and constraints that make this argument work is located in the Processor Table. The entirety of this construction is motivated and explained in TIP-0003.
The inner sorting argument requires one extension column cjdrp
, which contains a running product. Specifically, this column accumulates a factor in every pair of consecutive rows where a) the ramp
value is the same, and b) the difference in clk
values minus one is different from zero.
Row Permutation Argument
Selecting for the columns clk
, ramp
, and ramv
, the set of rows of the RAM Table is identical to the set of rows of the Processor Table. This argument requires one extension column, rppa
, short for "running product for Permutation Argument". This column accumulates a factor in every row. In this expression, , , , and are challenges from the verifier.
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 .
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 polynomialbcpc1
. - The running product polynomial
rpp
starts with🧼 - ramp
. - The formal derivative
fd
starts with 1. - 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 logarithmic derivative for the clock jump difference lookup
ClockJumpDifferenceLookupClientLogDerivative
is 0.
Initial Constraints as Polynomials
bcpc0
bc0
bc1 - bcpc1
rpp - 🧼 + ramp
fd - 1
rppa - 🛋 - 🍍·clk - 🍈·ramp - 🍎·ramv - 🌽·previous_instruction
ClockJumpDifferenceLookupClientLogDerivative
Consistency Constraints
None.
Transition Constraints
- If
(ramp - ramp')
is 0, theniord
is 0, elseiord
is the multiplicative inverse of(ramp' - ramp)
. - If the
ramp
does not change andprevious_instruction
in the next row is notwrite_mem
, then the RAM valueramv
does not change. - The Bézout coefficient polynomial coefficients are allowed to change only when the
ramp
changes. - The running product polynomial
rpp
accumulates a factor(🧼 - ramp)
wheneverramp
changes. - The running product for the permutation argument with the Processor Table
rppa
absorbs the next row with respect to challenges 🍍, 🍈, 🍎, and 🌽 and indeterminate 🛋. - If the RAM pointer
ramp
does not change, then the logarithmic derivative for the clock jump difference lookupClockJumpDifferenceLookupClientLogDerivative
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:
iord
is 0 oriord
is the inverse of(ramp' - ramp)
.(ramp' - ramp)
is zero oriord
is the inverse of(ramp' - ramp)
.(ramp' - ramp)
non-zero orprevious_instruction'
isopcode(write_mem)
orramv'
isramv
.bcpc0' - bcpc0
is zero or(ramp' - ramp)
is nonzero.bcpc1' - bcpc1
is zero or(ramp' - ramp)
is nonzero.(ramp' - ramp)
is zero andrpp' = rpp
; or(ramp' - ramp)
is nonzero andrpp' = rpp·(ramp'-🧼))
is zero.- the formal derivative
fd
applies the product rule of differentiation (as necessary). - Bézout coefficient 0 is evaluated correctly.
- Bézout coefficient 1 is evaluated correctly.
rppa' = rppa·(🛋 - 🍍·clk' - 🍈·ramp' - 🍎·ramv' - 🌽·previous_instruction')
-
- the
ramp
changes or the logarithmic derivative accumulates a summand, and - the
ramp
does not change or the logarithmic derivative does not change.
- the
Transition Constraints as Polynomials
iord·(iord·(ramp' - ramp) - 1)
(ramp' - ramp)·(iord·(ramp' - ramp) - 1)
(1 - iord·(ramp' - ramp))·(previous_instruction - opcode(write_mem))·(ramv' - ramv)
(iord·(ramp' - ramp) - 1)·(bcpc0' - bcpc0)
(iord·(ramp' - ramp) - 1)·(bcpc1' - bcpc1)
(iord·(ramp' - ramp) - 1)·(rpp' - rpp) + (ramp' - ramp)·(rpp' - rpp·(ramp'-🧼))
(iord·(ramp' - ramp) - 1)·(fd' - fd) + (ramp' - ramp)·(fd' - fd·(ramp'-🧼) - rpp)
(iord·(ramp' - ramp) - 1)·(bc0' - bc0) + (ramp' - ramp)·(bc0' - bc0·🧼 - bcpc0')
(iord·(ramp' - ramp) - 1)·(bc1' - bc1) + (ramp' - ramp)·(bc1' - bc1·🧼 - bcpc1')
rppa' - rppa·(🛋 - 🍍·clk' - 🍈·ramp' - 🍎·ramv' - 🌽·previous_instruction')
(iord·(ramp' - ramp) - 1)·((ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative) · (🪞 - clk' + clk) - 1)
+ (ramp' - ramp)·(ClockJumpDifferenceLookupClientLogDerivative' - ClockJumpDifferenceLookupClientLogDerivative)
Terminal Constraints
- The Bézout relation holds between
rp
,fd
,bc0
, andbc1
.
Terminal Constraints as Polynomials
rpp·bc0 + fd·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 theClockJumpDifferenceLookupClientLogDerivative
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 JumpStack 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
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 .
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 andjso
does not change andjsd
does not change and the cycle counterclk
increases by 1), or - (
jsp
does not change andjso
does not change andjsd
does not change and the current instructionci
iscall
), or - (
jsp
does not change and the current instructionci
isreturn
). - 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 lookupClockJumpDifferenceLookupClientLogDerivative
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 pointerjsp
does not change - The jump stack pointer
jsp
increases by 1 or the jump stack originjso
does not change or current instructionci
isreturn
- The jump stack pointer
jsp
increases by 1 or the jump stack destinationjsd
does not change or current instructionci
isreturn
- The jump stack pointer
jsp
increases by 1 or the cycle countclk
increases by 1 or current instructionci
iscall
or current instructionci
isreturn
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.
- the
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 OpStack's 10 top-most elements in one cycle.
Similarly, the Sponge instructions absorb_init
, absorb
, and 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 absorb_init
, absorb
, and 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
- sets all the hash coprocessor's rate registers (
state_0
throughstate_9
) to equal the processor's stack registersstate_0
throughstate_9
, - sets all the hash coprocessor's capacity registers (
state_10
throughstate_15
) to 1, - executes the 5 rounds of the Tip5 permutation,
- overwrites the processor's stack registers
state_0
throughstate_4
with 0, and - overwrites the processor's stack registers
state_5
throughstate_9
with the hash coprocessor's registersstate_0
throughstate_4
.
- sets all the hash coprocessor's rate registers (
- Instruction
absorb_init
- sets all the hash coprocessor's rate registers (
state_0
throughstate_9
) to equal the processor's stack registersstate_0
throughstate_9
, - sets all the hash coprocessor's capacity registers (
state_10
throughstate_15
) to 0, and - executes the 5 rounds of the Tip5 permutation.
- sets all the hash coprocessor's rate registers (
- Instruction
absorb
- overwrites the hash coprocessor's rate registers (
state_0
throughstate_9
) with the processor's stack registersstate_0
throughstate_9
, and - executes the 5 rounds of the Tip5 permutation.
- overwrites the hash coprocessor's rate registers (
- Instruction
squeeze
- overwrites the processor's stack registers
state_0
throughstate_9
with the hash coprocessor's rate registers (state_0
throughstate_9
), and - executes the 5 rounds of the Tip5 permutation.
- overwrites the processor's stack registers
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 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, modehash
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 .
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
.
Base Columns
The Hash Table has 67 base columns:
- The
Mode
indicator, as described above. It takes value- for mode
program_hashing
, - for mode
sponge
, - for mode
hash
, and - for mode
pad
.
- for mode
- Current instruction
CI
, holding the instruction the processor is currently executing. This column is only relevant for modesponge
. - Round number indicator
round_no
, which can be one of . The Tip5 permutation has 5 rounds, indexed . 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 ofstate_0
throughstate_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 ofstate_0
throughstate_4
, each of which holds one 16-bit wide limb. - 12 columns
state_5
throughstate_15
. - 4 columns
state_i_inv
establishing correct decomposition ofstate_0_*_lkin
throughstate_3_*_lkin
into 16-bit wide limbs. - 16 columns
constant_i
, which hold the round constant for the round indicated byRoundNumber
, 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 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
(fori
andlimb
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 instructionhash
,state_i_inv
fori
, which is , andconstant_i
fori
, which is thei
th constant for round 0.
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 .
Initial Constraints
- The
Mode
isprogram_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
andlimb
highest
,mid_high
,mid_low
,lowest
:
state_i_limb_LookupClientLogDerivative
has accumulatedstate_i_limb_lkin
andstate_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
andlimb
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., . - If the
Mode
isprogram_hashing
,hash
, orpad
, then the current instruction is the opcode ofhash
. - If the
Mode
issponge
, then the current instruction is a Sponge instruction. - If the
Mode
ispad
, then theround_no
is 0. - For
i
: If the round number is 0 and the currentMode
ishash
, then registerstate_i
is 1. - For
i
: If the round number is 0 and the current instruction isabsorb_init
, then registerstate_i
is 0. - For
i
: ensure that decomposition ofstate_i
is unique. That is, if both high limbs ofstate_i
are the maximum value, then both low limbs are 01. To make the corresponding polynomials low degree, registerstate_i_inv
holds the inverse-or-zero of the re-composed highest two limbs ofstate_i
subtracted from their maximum value. Letstate_i_hi_limbs_minus_2_pow_32
be an alias for that difference:state_i_hi_limbs_minus_2_pow_32
state_i_highest_lk_in
state_i_mid_high_lk_in
.- If the two high limbs of
state_i
are both the maximum possible value, then the two low limbs ofstate_i
are both 0. - The
state_i_inv
is the inverse ofstate_i_hi_limbs_minus_2_pow_32
orstate_i_inv
is 0. - The
state_i_inv
is the inverse ofstate_i_hi_limbs_minus_2_pow_32
orstate_i_hi_limbs_minus_2_pow_32
is 0.
- If the two high limbs of
- 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(absorb_init))·(CI - opcode(absorb))·(CI - opcode(squeeze))
(Mode - 1)·(Mode - 2)·(Mode - 3)·(round_no - 0)
- For
i
:
(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
:
(round_no - 1)·(round_no - 2)·(round_no - 3)·(round_no - 4)·(round_no - 5)
·(CI - opcode(hash))·(CI - opcode(absorb))·(CI - opcode(squeeze))
·(state_i - 0)
- For
i
: definestate_i_hi_limbs_minus_2_pow_32 := 2^32 - 1 - 2^16·state_i_highest_lk_in - state_i_mid_high_lk_in
.(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)
(1 - state_i_inv · state_i_hi_limbs_minus_2_pow_32)·state_i_inv
(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 theround_no
in the next row is 0. - If the
Mode
is notpad
and theround_no
is not 5, then theround_no
increments by 1. - If the
Mode
in the next row isprogram_hashing
and theround_no
in the next row is 0, then receive a chunk of instructions with respect to challenges 🪣 and 🪑. - If the
Mode
changes fromprogram_hashing
, then the Evaluation Argument ofstate_0
throughstate_4
with respect to indeterminate 🥬 equals the public program digest challenge, 🫑. - If the
Mode
isprogram_hashing
and theMode
in the next row issponge
, then the current instructions in the next row isabsorb_init
. - If the
round_no
is not 5, then the current instruction does not change. - If the
round_no
is not 5, then theMode
does not change. - If the
Mode
issponge
, then theMode
in the next row issponge
orhash
orpad
. - If the
Mode
ishash
, then theMode
in the next row ishash
orpad
. - If the
Mode
ispad
, then theMode
in the next row ispad
. - If the
round_no
in the next row is 0 and either (a) theMode
in the next row isprogram_hashing
or (b) theMode
in the next row issponge
and the current instruction in the next row isabsorb
, 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 issqueeze
, then none of the state registers change. - If the
round_no
in the next row is 0 and theMode
in the next row ishash
, thenRunningEvaluationHashInput
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 theMode
in the next row ishash
, thenRunningEvaluationHashDigest
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 theMode
in the next row issponge
, thenRunningEvaluationSponge
accumulates the next row with respect to challenges 🧅 and 🧄₀ through 🧄₉ and indeterminate 🧽. Otherwise, it remains unchanged. - For
i
andlimb
highest
,mid_high
,mid_low
,lowest
:
If the next round number is not 5, thenstate_i_limb_LookupClientLogDerivative
has accumulatedstate_i_limb_lkin'
andstate_i_limb_lkout'
with respect to challenges 🍒, 🍓 and indeterminate 🧺. Otherwise,state_i_limb_LookupClientLogDerivative
remains unchanged. - For
r
:
If theround_no
isr
, thestate
registers adhere to the rules of applying roundr
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)·(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(absorb_init))
(round_no - 5)·(CI' - CI)
(round_no - 5)·(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' - 0)·(Mode' - 3)·(CI' - opcode(hash))·(CI' - opcode(absorb_init))·(CI' - opcode(squeeze))
·(🧄₁₀·(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(absorb_init))·(CI' - opcode(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(absorb_init))·(CI' - opcode(absorb))·(CI' - opcode(squeeze))
- For
i
andlimb
highest
,mid_high
,mid_low
,lowest
:
(round_no - 5)·((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)
- The remaining constraints are left as an exercise to the reader. For hints, see the Tip5 paper.
Terminal Constraints
- If the
Mode
isprogram_hashing
, then the Evaluation Argument ofstate_0
throughstate_4
with respect to indeterminate 🥬 equals the public program digest challenge, 🫑. - If the
Mode
is notpad
, then theround_no
is 5.
Terminal Constraints as Polynomials
🥬^5 + state_0·🥬^4 + state_1·🥬^3 + state_2·🥬^2 + state_3·🥬 + state_4 - 🫑
(Mode - 0)·(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 accumulatesLookupMultiplicity / (🧺 - Combo)
where 🧺 is a verifier-supplied challenge andCombo
is the weighted sum ofLookInHi · 2^8 + LookInLo
andLookOutHi · 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 summands1 / combo_hi
wherecombo_hi
is the verifier-weighted combination ofLookInHi
andLookOutHi
, and1 / combo_lo
wherecombo_lo
is the verifier-weighted combination ofLookInLo
andLookOutLo
.
Padding
Each padding row is the all-zero row with the exception of IsPadding
, which is 1.
Arithmetic Intermediate Representation
Let all household items (🪥, 🛁, etc.) be challenges, concretely evaluation points, supplied by the verifier. Let all fruit & vegetables (🥝, 🥥, etc.) be challenges, concretely weights to compress rows, supplied by the verifier. Both types of challenges are X-field elements, i.e., elements of .
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 , the verifier computes the terminal of the Evaluation Argument over the list of all the expected lookup values with respect to challenge . 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 summandLookupMultiplicity / Combo
whereCombo
is the verifier-weighted combination ofLookIn
andLookOut
.PublicEvaluationArgument
, the running sum for the public evaluation argument of the Lookup Table. In every row, accumulatesLookOut
.
Padding
Each padding row is the all-zero row with the exception of IsPadding
, which is 1.
Arithmetic Intermediate Representation
Let all household items (🪥, 🛁, etc.) be challenges, concretely evaluation points, supplied by the verifier. Let all fruit & vegetables (🥝, 🥥, etc.) be challenges, concretely weights to compress rows, supplied by the verifier. Both types of challenges are X-field elements, i.e., elements of .
Initial Constraints
LookIn
is 0.CascadeTableServerLogDerivative
has accumulated the first row with respect to challenges 🍒 and 🍓 and indeterminate 🧺.PublicEvaluationArgument
has accumulated the firstLookOut
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 nextLookOut
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 “” are presented in base 2, whereas columns marked “” are in the usual base 10.
CopyFlag | CI | Bits | LHS | RHS | Result | Result |
---|---|---|---|---|---|---|
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:
Credit for this trick goes, to the best of our knowledge, to Daniel Lubarov.
For the remaining u32 instruction div
, the processor triggers the creation of two sections in the U32 Table:
- One section to ensure that the remainder
r
is smaller than the divisord
. The processor requests the result oflt
by setting the U32 Table'sCI
register to the opcode oflt
. This also guarantees thatr
andd
each fit in a u32. - One section to ensure that the quotient
q
and the numeratorn
each fit in a u32. The processor needs no result, only the range checking capabilities, like for instructionsplit
. Consequently, the processor sets the U32 Table'sCI
register to the opcode ofsplit
.
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 ispow
, andRHS
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 ofsplit
, andBitsMinus33Inv
, which is .
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
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 .
Initial Constraints
- If the
CopyFlag
is 0, thenU32LookupServerLogDerivative
is 0. Otherwise, theU32LookupServerLogDerivative
has accumulated the first row with multiplicityLookupMultiplicity
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, thenBits
is 0. BitsMinus33Inv
is the inverse of (Bits
- 33).LhsInv
is 0 or the inverse ofLHS
.Lhs
is 0 orLhsInv
is the inverse ofLHS
.RhsInv
is 0 or the inverse ofRHS
.Rhs
is 0 orRhsInv
is the inverse ofRHS
.- If
CopyFlag
is 0 and the current instruction islt
andLHS
is 0 andRHS
is 0, thenResult
is 2. - If
CopyFlag
is 1 and the current instruction islt
andLHS
is 0 andRHS
is 0, thenResult
is 0. - If the current instruction is
and
andLHS
is 0 andRHS
is 0, thenResult
is 0. - If the current instruction is
pow
andRHS
is 0, thenResult
is 1. - If
CopyFlag
is 0 and the current instruction islog_2_floor
andLHS
is 0, thenResult
is -1. - If
CopyFlag
is 1 and the current instruction islog_2_floor
andLHS
is 0, the VM crashes. - If
CopyFlag
is 0 and the current instruction ispop_count
andLHS
is 0, thenResult
is 0. - If
CopyFlag
is 0, thenLookupMultiplicity
is 0.
Written in Disjunctive Normal Form, the same constraints can be expressed as:
- The
CopyFlag
is 0 or 1. CopyFlag
is 0 orBits
is 0.BitsMinus33Inv
the inverse of (Bits
- 33).LhsInv
is 0 or the inverse ofLHS
.Lhs
is 0 orLhsInv
is the inverse ofLHS
.RhsInv
is 0 or the inverse ofRHS
.Rhs
is 0 orRhsInv
is the inverse ofRHS
.CopyFlag
is 1 orCI
is the opcode ofsplit
,and
,pow
,log_2_floor
, orpop_count
orLHS
is not 0 orRHS
is not 0 orResult
is 2.CopyFlag
is 0 orCI
is the opcode ofsplit
,and
,pow
,log_2_floor
, orpop_count
orLHS
is not 0 orRHS
is not 0 orResult
is 0.CI
is the opcode ofsplit
,lt
,pow
,log_2_floor
, orpop_count
orLHS
is not 0 orRHS
is not 0 orResult
is 0.CI
is the opcode ofsplit
,lt
,and
,log_2_floor
, orpop_count
orRHS
is not 0 orResult
is 1.CopyFlag
is 1 orCI
is the opcode ofsplit
,lt
,and
,pow
, orpop_count
orLHS
is not 0 orResult
is -1.CopyFlag
is 0 orCI
is the opcode ofsplit
,lt
,and
,pow
, orpop_count
orLHS
is not 0.CopyFlag
is 1 orCI
is the opcode ofsplit
,lt
,and
,pow
, orlog_2_floor
orLHS
is not 0 orResult
is 0.CopyFlag
is 1 orLookupMultiplicity
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 notpow
, thenLHS
in the current row is 0. - If the
CopyFlag
in the next row is 1, thenRHS
in the current row is 0. - If the
CopyFlag
in the next row is 0, thenCI
in the next row isCI
in the current row. - If the
CopyFlag
in the next row is 0 andLHS
in the current row is unequal to 0 and the current instruction is notpow
, thenBits
in the next row isBits
in the current row plus 1. - If the
CopyFlag
in the next row is 0 andRHS
in the current row is unequal to 0, thenBits
in the next row isBits
in the current row plus 1. - If the
CopyFlag
in the next row is 0 and the current instruction is notpow
, thenLhsLsb
is either 0 or 1. - If the
CopyFlag
in the next row is 0, thenRhsLsb
is either 0 or 1. - If the
CopyFlag
in the next row is 0 and the current instruction islt
andResult
in the next row is 0, thenResult
in the current row is 0. - If the
CopyFlag
in the next row is 0 and the current instruction islt
andResult
in the next row is 1, thenResult
in the current row is 1. - If the
CopyFlag
in the next row is 0 and the current instruction islt
andResult
in the next row is 2 andLhsLsb
is 0 andRhsLsb
is 1, thenResult
in the current row is 1. - If the
CopyFlag
in the next row is 0 and the current instruction islt
andResult
in the next row is 2 andLhsLsb
is 1 andRhsLsb
is 0, thenResult
in the current row is 0. - If the
CopyFlag
in the next row is 0 and the current instruction islt
andResult
in the next row is 2 andLhsLsb
isRhsLsb
and theCopyFlag
in the current row is 0, thenResult
in the current row is 2. - If the
CopyFlag
in the next row is 0 and the current instruction islt
andResult
in the next row is 2 andLhsLsb
isRhsLsb
and theCopyFlag
in the current row is 1, thenResult
in the current row is 0. - If the
CopyFlag
in the next row is 0 and the current instruction isand
, thenResult
in the current row is twiceResult
in the next row plus the product ofLhsLsb
andRhsLsb
. - If the
CopyFlag
in the next row is 0 and the current instruction islog_2_floor
andLHS
in the next row is 0 andLHS
in the current row is not 0, thenResult
in the current row isBits
. - If the
CopyFlag
in the next row is 0 and the current instruction islog_2_floor
andLHS
in the next row is not 0, thenResult
in the current row isResult
in the next row. - If the
CopyFlag
in the next row is 0 and the current instruction ispow
, thenLHS
remains unchanged. - If the
CopyFlag
in the next row is 0 and the current instruction ispow
andRhsLsb
in the current row is 0, thenResult
in the current row isResult
in the next row squared. - If the
CopyFlag
in the next row is 0 and the current instruction ispow
andRhsLsb
in the current row is 1, thenResult
in the current row isResult
in the next row squared timesLHS
in the current row. - If the
CopyFlag
in the next row is 0 and the current instruction ispop_count
, thenResult
in the current row isResult
in the next row plusLhsLsb
. - If the
CopyFlag
in the next row is 0, thenU32LookupServerLogDerivative
in the next row isU32LookupServerLogDerivative
in the current row. - If the
CopyFlag
in the next row is 1, thenU32LookupServerLogDerivative
in the next row has accumulated the next row with multiplicityLookupMultiplicity
and with respect to challenges 🥜, 🌰, 🥑, and 🥕, and indeterminate 🧷.
Written in Disjunctive Normal Form, the same constraints can be expressed as:
CopyFlag
' is 0 orLHS
is 0 orCI
is the opcode ofpow
.CopyFlag
' is 0 orRHS
is 0.CopyFlag
' is 1 orCI
' isCI
.CopyFlag
' is 1 orLHS
is 0 orCI
is the opcode ofpow
orBits
' isBits
+ 1.CopyFlag
' is 1 orRHS
is 0 orBits
' isBits
+ 1.CopyFlag
' is 1 orCI
is the opcode ofpow
orLhsLsb
is 0 orLhsLsb
is 1.CopyFlag
' is 1 orRhsLsb
is 0 orRhsLsb
is 1.CopyFlag
' is 1 orCI
is the opcode ofsplit
,and
,pow
,log_2_floor
, orpop_count
or (Result
' is 1 or 2) orResult
is 0.CopyFlag
' is 1 orCI
is the opcode ofsplit
,and
,pow
,log_2_floor
, orpop_count
or (Result
' is 0 or 2) orResult
is 1.CopyFlag
' is 1 orCI
is the opcode ofsplit
,and
,pow
,log_2_floor
, orpop_count
or (Result
' is 0 or 1) orLhsLsb
is 1 orRhsLsb
is 0 orResult
is 1.CopyFlag
' is 1 orCI
is the opcode ofsplit
,and
,pow
,log_2_floor
, orpop_count
or (Result
' is 0 or 1) orLhsLsb
is 0 orRhsLsb
is 1 orResult
is 0.CopyFlag
' is 1 orCI
is the opcode ofsplit
,and
,pow
,log_2_floor
, orpop_count
or (Result
' is 0 or 1) orLhsLsb
is unequal toRhsLsb
orCopyFlag
is 1 orResult
is 2.CopyFlag
' is 1 orCI
is the opcode ofsplit
,and
,pow
,log_2_floor
, orpop_count
or (Result
' is 0 or 1) orLhsLsb
is unequal toRhsLsb
orCopyFlag
is 0 orResult
is 0.CopyFlag
' is 1 orCI
is the opcode ofsplit
,lt
,pow
,log_2_floor
, orpop_count
orResult
is twiceResult
' plus the product ofLhsLsb
andRhsLsb
.CopyFlag
' is 1 orCI
is the opcode ofsplit
,lt
,and
,pow
, orpop_count
orLHS
' is not 0 orLHS
is 0 orResult
isBits
.CopyFlag
' is 1 orCI
is the opcode ofsplit
,lt
,and
,pow
, orpop_count
orLHS
' is 0 orResult
isResult
'.CopyFlag
' is 1 orCI
is the opcode ofsplit
,lt
,and
,log_2_floor
, orpop_count
orLHS
' isLHS
.CopyFlag
' is 1 orCI
is the opcode ofsplit
,lt
,and
,log_2_floor
, orpop_count
orRhsLsb
is 1 orResult
isResult
' timesResult
'.CopyFlag
' is 1 orCI
is the opcode ofsplit
,lt
,and
,log_2_floor
, orpop_count
orRhsLsb
is 0 orResult
isResult
' timesResult
' timesLHS
.CopyFlag
' is 1 orCI
is the opcode ofsplit
,lt
,and
,pow
, orlog_2_floor
orResult
isResult
' plusLhsLsb
.CopyFlag
' is 1 orU32LookupServerLogDerivative
' isU32LookupServerLogDerivative
.CopyFlag
' is 0 or the difference ofU32LookupServerLogDerivative
' andU32LookupServerLogDerivative
times(🧷 - 🥜·LHS' - 🌰·RHS' - 🥑·CI' - 🥕·Result')
isLookupMultiplicity
'.
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 ispow
.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 . 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 , , and are to be incorporated into the cryptographic argument, then the prover
- commits to , , and ,
- samples weights , , and using the Fiat-Shamir heuristic,
- “compresses” the elements in question to , 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 and are permutations of each other. To achieve this, the lists' elements are interpreted as the roots of polynomials and , respectively:
The two lists and are a permutation of each other if and only if the two polynomials and are identical. By the Schwartz–Zippel lemma, probing the polynomials in a single point establishes the polynomial identity with high probability.1
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,2
- samples a random challenge through the Fiat-Shamir heuristic,
- computes the running product of and in the respective tables' extension column.
For example, in Table A:
base column A | extension column A: running product |
---|---|
0 | |
1 | |
2 | |
3 |
And in Table B:
base column B | extension column B: running product |
---|---|
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 of the lists and as well as the field size. For Triton VM, . The polynomials and are evaluated over the extension field with elements. The false positive rate is therefore .
Evaluation Argument
The Evaluation Argument establishes that two lists and are identical. To achieve this, the lists' elements are interpreted as the coefficients of polynomials and , respectively:
The two lists and are identical if and only if the two polynomials and are identical. By the Schwartz–Zippel lemma, probing the polynomials in a single point establishes the polynomial identity with high probability.1
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,2
- samples a random challenge through the Fiat-Shamir heuristic,
- computes the running evaluation of and in the respective tables' extension column.
For example, in both Table A and B:
base column | extension column: running evaluation |
---|---|
0 | |
1 | |
2 | |
3 |
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.
This depends on the length of the lists and as well as the field size. For Triton VM, . The polynomials and are evaluated over the extension field with elements. The false positive rate is therefore .
Lookup Argument
The Lookup Argument establishes that all elements of list also occur in list . In this context, contains the values that are being looked up, while is the lookup table.1 Both lists and may contain duplicates. However, it is inefficient if 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 and , respectively:
By counting the number of occurrences of unique elements and eliminating duplicates, can equivalently be expressed as:
The next step uses
- the formal derivative of , and
- the multiplicity-weighted formal derivative of .
The former is the familiar formal derivative:
The multiplicity-weighted formal derivative uses the lookup-multiplicities as additional factors:
Let the greatest common divisor of and . The polynomial has the same roots as , but all roots have multiplicity 1. This polynomial is identical to if and only if all elements in list also occur in list .
A similar property holds for the formal derivatives: The polynomial is identical to if and only if all elements in list also occur in list . By solving for and equating, the following holds:
Optimization through Logarithmic Derivatives
The logarithmic derivative of is defined as . Furthermore, the equality of monic polynomials and is equivalent to the equality of their logarithmic derivatives.2 This allows rewriting above equation as:
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 , , , and – only two logarithmic derivatives are needed. Namely, considering once again list containing duplicates, above equation can be written as:
To compute the sums, the lists and 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 | |
2 | |
2 | |
1 | |
2 |
And in Table B:
base column B | multiplicity | extension column B: logarithmic derivative |
---|---|---|
0 | 1 | |
1 | 1 | |
2 | 3 |
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 JumpStack, and the OpStack. 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 OpStack or JumpStack Tables. The OpStack and JumpStack 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 OpStack Table
In each cycle, the memory pointer for the OpStack Table, osp
, 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:
osp
starts with zero, so in terms of polynomials the constraint isosp
. - Transition constraint: the new
osp
is either the same as the previous or one larger. The polynomial representation for this constraint is(osp' - osp - 1) * (osp' - osp)
.
Contiguity for JumpStack Table
Analogously to the OpStack Table, the JumpStack'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 isjsp
. - 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, . The Contiguity Argument then shows that the list contains no duplicates. For this, it uses Bézout's identity for univariate polynomials. Concretely, the prover shows that for the polynomial with all elements of as roots, i.e., and its formal derivative , there exist and with appropriate degrees such that In other words, the Contiguity Argument establishes that the greatest common divisor of and is 1. This implies that all roots of have multiplicity 1, which holds if and only if there are no duplicate elements in list .
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
andbcpc1
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 ofrpp
. A randomized transition constraint verifies the correct application of the product rule of differentiation to update this column. - Extension columns
bc0
andbc1
build up the Bézout coefficient polynomials based on the corresponding base columns,bcpc0
andbcpc1
. 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 |
---|---|---|---|---|---|---|---|
0 | |||||||
0 | |||||||
0 | |||||||
0 | |||||||
- |
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 , anticipating the substitution . 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 initially, which is enforced by an initial constraint.
It accumulates a factor 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 the polynomial that accumulates all factors in every pair of rows where .
The column fd
contains the “formal derivative” of the running product with respect to .
The formal derivative is initially , 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 then the same value persists; but if then is mapped as
This update rule is called the product rule of differentiation because, assuming , then
The transition constraint for fd
is (ramp' - ramp) ⋅ (fd' - rp - (α - ramp') ⋅ fd) + (1 - (ramp' - ramp) ⋅ iord) ⋅ (fd' - fd)
.
The polynomials and are the Bézout coefficient polynomials satisfying the relation The prover finds and as the minimal-degree Bézout coefficients as returned by the extended Euclidean algorithm. Concretely, the degree of is smaller than the degree of , and the degree of is smaller than the degree of .
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 and share at least one factor. As a result, no Bézout coefficients and can exist such that . The verifier therefore probes unequal polynomials of degree at most , where is the length of the execution trace, which is upper bounded by . According to the Schwartz-Zippel lemma, the false positive probability is at most .
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
Clock Jump Differences and Inner Sorting
The previous sections show how it is proven that in the JumpStack, OpStack, 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 . Therefore, a forward directed clock jump difference is in , whereas a backward directed clock jump's difference is in . No other clock jump difference can occur. If , there is no overlap between sets and . As a result, in this regime, showing that a clock jump difference is in guarantees that the jump is forward-directed.
The set of values in the Processor Table's clock cycle column is .
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 denote the Processor Table and denote the memory-like table. Both have height . Both have columns clk
, mp
, and val
. For the column clk
coincides with the index of the row. 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 to denote the column name and 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 , there are no rows with a different memory pointer in between rows with memory pointer .
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.
The symbol denotes the integer less than operator, after lifting the operands from the finite field to the integers.
Definition 3 (memory consistency): A Processor Table has memory consistency if whenever a memory cell at location is read, its value corresponds to the previous time the memory cell at location was written. Specifically, there are no writes in between the write and the read, that give the cell a different value.
Theorem 1 (memory consistency): Let be a Processor Table. If there exists a memory-like table such that
- selecting for the columns
clk
,mp
,val
, the two tables' lists of rows are permutations of each other; and - is contiguous and regionally sorted; and
- has no changes in
val
that coincide with clock jumps;
then has memory consistency.
Proof. For every memory pointer value , select the sublist of rows in order. The way this sublist is constructed guarantees that it coincides with the contiguous region of where the memory pointer is also .
Iteratively apply the following procedure to : remove the bottom-most row if it does not correspond to a row that constitutes a counter-example to memory consistency. Specifically, let be the clock cycle of the previous row in .
- If satisfies then by construction it also satisfies . As a result, row 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 then we can safely ignore this row: if there is no clock jump, then the absence of a -instruction guarantees that cannot change; and if there is a clock jump, then by assumption on , cannot change. So set to the clock cycle of the row above it in and proceed to the next iteration of the inner loop. If there are no rows left for to index, then there is no possible counterexample for and so remove the bottom-most row of and proceed to the next iteration of the outermost loop.
- The case cannot occur because by construction of , cannot change.
- The case 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 consists of only two rows, it can contain no counter-examples. By applying the above procedure, we can reduce every correctly constructed sublist to a list consisting of two rows. Therefore, for every , the sublist is free of counter-examples to memory consistency. Equivalently, 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 digest1. 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 length2.
- 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
throughst15
.
The program digest is part of the generated proof3, 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 , 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 distinct but otherwise uniform indices from the interval . 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, ). 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 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
where denotes upper_bound
, denotes count
, and denotes margin
.
Given the count
and the upper_bound
, the appropriate value for margin
that pushes this failure probability below is
For a concrete example, set and . 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 of size that are suitable for the adversary is . Then clearly with the standard old index sampling method the attacker's success probability is bounded by . 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 subsets of of size . The probability that a given subset is suitable for the attack is , and so:
- The probability that one subset is unsuitable for attack is .
- The probability that all subsets are unsuitable for attack is . 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 .
The binomial formula expands 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 , we get and the assumption holds already when . For a concrete example, set and , then the left hand side of this expression is roughly whereas these parameters target a security level of .
Using this assumption (on the shrinking absolute value of each successive term) we can derive an expression to quantify the security degradation.
For a concrete example, set and . Then and so we lose about bits of security.
Solution 2: Stupid Safety Margin
How about we sample indices from the start, and use them all no matter what? We only need 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 or more collisions requires hitting a marked subset of at most indices times. The probability of this event is therefore . This probability is smaller than when
For a concrete example, set and . Then needs to be at least 6.
Zero-Integral and Sum-Check
Let be a table of 1 column and rows, and let be any polynomial that agrees with when evaluated on , where is a generator of the subgroup of order . Group theory lets us prove and efficiently verify if .
Decompose into , where is the zerofier over , and where has degree at most . The table sums to zero if and only if integrates to zero over because
and this latter proposition is true if and only if the constant term of is zero.
Theorem. for a subgroup of order .
Let be a subgroup of . If then and also because the elements of come in pairs: . Therefore .
The map is a morphism of groups with . Therefore we have:
The polynomial has only one term whose exponent is , which is the constant term.
This observation gives rise to the following Polynomial IOP for verifying that a polynomial oracle integrates to 0 on a subgroup of order some power of 2.
Protocol Zero-Integral
- Prover computes and .
- Prover computes .
- Prover sends , of degree at most , and , of degree at most to Verifier.
- Verifier queries , , in z \xleftarrow{$} \mathbb{F} and receives .
- Verifier tests .
This protocol can be adapted to show instead that a given polynomial oracle integrates to on the subgroup , giving rise to the well-known Sum-Check protocol. The adaptation follows from the Verifier's capacity to simulate from , where . This simulated polynomial is useful because
In other words, integrates to on iff integrates to on , and we already a protocol to establish the latter claim.