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.
The Program Table consists of 7 base columns. Those columns marked with an asterisk (*) are only used for program attestation.
|an instruction's address|
|the (opcode of the) instruction|
|how often an instruction has been executed|
|*||the inverse-or-zero of|
|*||padding indicator for absorbing the program into the Sponge|
|padding indicator for rows only required due to the dominating length of some other table|
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
For sending the padded program to the Hash Table, a combination of two Evaluation Arguments is used.
PrepareChunkRunningEvaluation, absorbs one chunk of (i.e. 10) instructions at a time, after which it is reset and starts absorbing again.
SendChunkRunningEvaluation, absorbs one such prepared chunk every 10 instructions.
A padding row is a copy of the Program Table's last row with the following modifications:
Addressis increased by 1,
Instructionis set to 0,
LookupMultiplicityis set to 0,
IndexInChunkis set to
MaxMinusIndexInChunkInvis set to the inverse-or-zero of ,
IsHashInputPaddingis set to 1, and
IsTablePaddingis set to 1.
Above procedure is iterated until the necessary number of rows have been added.
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.
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 .
- The indicator
Instructionwith respect to challenge 🪑.
PrepareChunkRunningEvaluation - 🪑 - Instruction
SendChunkRunningEvaluation - 1
MaxMinusIndexInChunkInvis zero or the inverse of
IndexInChunkis or the
MaxMinusIndexInChunkInvis the inverse of
IsHashInputPaddingis either 0 or 1.
IsTablePaddingis either 0 or 1.
(1 - MaxMinusIndexInChunkInv · (rate - 1 - IndexInChunk)) · MaxMinusIndexInChunkInv
(1 - MaxMinusIndexInChunkInv · (rate - 1 - IndexInChunk)) · (rate - 1 - IndexInChunk)
IsHashInputPadding · (IsHashInputPadding - 1)
IsTablePadding · (IsTablePadding - 1)
Addressincreases by 1.
- If the
IndexInChunkis not , it increases by 1. Else, the
IndexInChunkin the next row is 0.
- The indicator
IsHashInputPaddingis 0 or remains unchanged.
- The padding indicator
IsTablePaddingis 0 or remains unchanged.
IsHashInputPaddingis 0 in the current row and 1 in the next row, then
Instructionin the next row is 1.
IsHashInputPaddingis 1 in the current row then
Instructionin the next row is 0.
IsHashInputPaddingis 1 in the current row and
IndexInChunkis in the current row then
IsTablePaddingis 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
IndexInChunkin the current row is not , then
Instructionin the next row with respect to challenge 🪑. Otherwise,
PrepareChunkRunningEvaluationresets and absorbs the
Instructionin the next row with respect to challenge 🪑.
- If the next row is not a padding row and the
IndexInChunkin the next row is , then
PrepareChunkRunningEvaluationin the next row with respect to variable 🪣. Otherwise, it remains unchanged.
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')
- The indicator
IndexInChunkis or the indicator
IsHashInputPadding - 1
(rate - 1 - IndexInChunk) · (IsTablePadding - 1)
See also section 2.5 “Fixed-Length versus Variable-Length” in the Tip5 paper.