Processor Table

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

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

Base Columns

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

Extension Columns

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

RunningEvaluationStandardInput for the Evaluation Argument with the input symbols.
RunningEvaluationStandardOutput for the Evaluation Argument with the output symbols.
InstructionLookupClientLogDerivative for the Lookup Argument with the Program Table
RunningProductOpStackTable for the Permutation Argument with the 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 $F_{p^{3}}$ .

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

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

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

Initial Constraints

The cycle counter clk is 0.
The 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 through st15 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 is hash. 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 through ib7 corresponds to the current instruction ci.
The instruction bit ib0 is a bit.
The instruction bit ib1 is a bit.
The instruction bit ib2 is a bit.
The instruction bit ib3 is a bit.
The instruction bit ib4 is a bit.
The instruction bit ib5 is a bit.
The instruction bit ib6 is a bit.
The 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 into previous_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 is read_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 is write_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, or squeeze, 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.
1. If the current instruction is split, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates st0 and st1 in the next row and ci in the current row with respect to challenges 🥜, 🌰, and 🥑, and indeterminate 🧷.
2. If the current instruction is lt, and, xor, or pow, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates st0, st1, and ci in the current row and st0 in the next row with respect to challenges 🥜, 🌰, 🥑, and 🥕, and indeterminate 🧷.
3. If the current instruction is log_2_floor, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates st0 and ci in the current row and st0 in the next row with respect to challenges 🥜, 🥑, and 🥕, and indeterminate 🧷.
4. If the current instruction is div, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates both
  1. st0 in the next row and st1 in the current row as well as the constants opcode(lt) and 1 with respect to challenges 🥜, 🌰, 🥑, and 🥕, and indeterminate 🧷.
  2. st0 in the current row and st1 in the next row as well as opcode(split) with respect to challenges 🥜, 🌰, and 🥑, and indeterminate 🧷.
5. If the current instruction is pop_count, then the logarithmic derivative for the Lookup Argument with the U32 Table accumulates st0 and ci in the current row and st0 in the next row with respect to challenges 🥜, 🥑, and 🥕, and indeterminate 🧷.
6. Else, i.e., if the current instruction is not a u32 instruction, the logarithmic derivative for the Lookup Argument with the U32 Table remains unchanged.
The running sum for the logarithmic derivative of the clock jump difference lookup argument accumulates the next row's clk with the appropriate multiplicity cjd_mul with respect to indeterminate 🪞.

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')
1. split_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0' - 🌰·st1' - 🥑·ci) - 1)
2. + lt_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0') - 1)
3. + and_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0') - 1)
4. + xor_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0') - 1)
5. + pow_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🌰·st1 - 🥑·ci - 🥕·st0') - 1)
6. + log_2_floor_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🥑·ci - 🥕·st0') - 1)
7. + div_deselector·(
  (U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0' - 🌰·st1 - 🥑·opcode(lt) - 🥕·1)·(🧷 - 🥜·st0 - 🌰·st1' - 🥑·opcode(split))
  - (🧷 - 🥜·st0' - 🌰·st1 - 🥑·opcode(lt) - 🥕·1)
  - (🧷 - 🥜·st0 - 🌰·st1' - 🥑·opcode(split))
  )
8. + pop_count_deselector·((U32LookupClientLogDerivative' - U32LookupClientLogDerivative)·(🧷 - 🥜·st0 - 🥑·ci - 🥕·st0') - 1)
9. + (1 - ib2)·(U32LookupClientLogDerivative' - U32LookupClientLogDerivative)
(ClockJumpDifferenceLookupServerLogDerivative' - ClockJumpDifferenceLookupServerLogDerivative)
·(🪞 - clk') - cjd_mul'

Terminal Constraints

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

Terminal Constraints as Polynomials

ci