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