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 $\text{rate}$ of the Tip5 hash function. Program padding is one 1 followed by the minimal number of 0’s necessary to make the padded input length a multiple of the $\text{rate}$¹.

Main Columns

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

Auxiliary 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 auxiliary 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 $\text{rate}$ (i.e. 10) instructions at a time, after which it is reset and starts absorbing again. The second, SendChunkRunningEvaluation, absorbs one such prepared chunk every 10 instructions.

Padding

A padding row is a copy of the Program Table's last row with the following modifications:

1. column Address is increased by 1,
2. column Instruction is set to 0,
3. column LookupMultiplicity is set to 0,
4. column IndexInChunk is set to Address mod $\text{rate}$,
5. column MaxMinusIndexInChunkInv is set to the inverse-or-zero of $\text{rate}-1-\text{IndexInChunk}$,
6. column IsHashInputPadding is set to 1, and
7. column IsTablePadding is set to 1.

Above procedure is iterated until the necessary number of rows have been added.

A Note on the Instruction Lookup Argument

For almost all table-linking arguments, the initial row contains the argument's initial value after having applied the first update. For example, the initial row for a Lookup Argument usually contains $\frac{x}{\alpha -y}$ for some $x$ and $y$. As an exception, the Program Table's instruction Lookup Argument always records 0 in the initial row.

Recall that the Lookup Argument is not just about the instruction, but also about the instruction's argument if it has one, or the next instruction if it has none. In the Program Table, this argument (or the next instruction) is recorded in the next row from the instruction in question. Therefore, verifying correct application of the logarithmic derivative's update rule requires access to both the current and the next row.

Out of all constraint types, only Transition Constraints have access to more than one row at a time. This implies that the correct application of the first update of the instruction Lookup Argument cannot be verified by an initial constraint. Therefore, the recorded initial value must be independent of the second row.

Consequently, the final value for the Lookup Argument is recorded in the first row just after the program description ends. This row is guaranteed to exist because of the mechanics for program attestation: the program has to be padded with at least one 1 before it is hashed.

Arithmetic Intermediate Representation

Let all household items (🪥, 🛁, etc.) be challenges, concretely evaluation points, supplied by the verifier. Let all fruit & vegetables (🥝, 🥥, etc.) be challenges, concretely weights to compress rows, supplied by the verifier. Both types of challenges are X-field elements, i.e., elements of ${\mathbb{F}}_{p^3}$.

Initial Constraints

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

Initial Constraints as Polynomials

1. Address
2. IndexInChunk
3. IsHashInputPadding
4. InstructionLookupServerLogDerivative
5. PrepareChunkRunningEvaluation - 🪑 - Instruction
6. SendChunkRunningEvaluation - 1

Consistency Constraints

1. The MaxMinusIndexInChunkInv is zero or the inverse of $\text{rate}-1-$ IndexInChunk.
2. The IndexInChunk is $\text{rate}-1$ or the MaxMinusIndexInChunkInv is the inverse of $\text{rate}-1-$ IndexInChunk.
3. Indicator IsHashInputPadding is either 0 or 1.
4. Indicator IsTablePadding is either 0 or 1.

Consistency Constraints as Polynomials

1. (1 - MaxMinusIndexInChunkInv · (rate - 1 - IndexInChunk)) · MaxMinusIndexInChunkInv
2. (1 - MaxMinusIndexInChunkInv · (rate - 1 - IndexInChunk)) · (rate - 1 - IndexInChunk)
3. IsHashInputPadding · (IsHashInputPadding - 1)
4. IsTablePadding · (IsTablePadding - 1)

Transition Constraints

1. The Address increases by 1.
2. If the IndexInChunk is not $\text{rate}-1$, it increases by 1. Else, the IndexInChunk in the next row is 0.
3. The indicator IsHashInputPadding is 0 or remains unchanged.
4. The padding indicator IsTablePadding is 0 or remains unchanged.
5. If IsHashInputPadding is 0 in the current row and 1 in the next row, then Instruction in the next row is 1.
6. If IsHashInputPadding is 1 in the current row then Instruction in the next row is 0.
7. If IsHashInputPadding is 1 in the current row and IndexInChunk is $\text{rate}-1$ in the current row then IsTablePadding is 1 in the next row.
8. 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.
9. If the IndexInChunk in the current row is not $\text{rate}-1$, then PrepareChunkRunningEvaluation absorbs the Instruction in the next row with respect to challenge 🪑. Otherwise, PrepareChunkRunningEvaluation resets and absorbs the Instruction in the next row with respect to challenge 🪑.
10. If the next row is not a padding row and the IndexInChunk in the next row is $\text{rate}-1$, then SendChunkRunningEvaluation absorbs PrepareChunkRunningEvaluation in the next row with respect to variable 🪣. Otherwise, it remains unchanged.

Transition Constraints as Polynomials

1. Address' - Address - 1
2. MaxMinusIndexInChunkInv · (IndexInChunk' - IndexInChunk - 1)
+ (1 - MaxMinusIndexInChunkInv · (rate - 1 - IndexInChunk)) · IndexInChunk'
3. IsHashInputPadding · (IsHashInputPadding' - IsHashInputPadding)
4. IsTablePadding · (IsTablePadding' - IsTablePadding)
5. (IsHashInputPadding - 1) · IsHashInputPadding' · (Instruction' - 1)
6. IsHashInputPadding · Instruction'
7. IsHashInputPadding · (1 - MaxMinusIndexInChunkInv · (rate - 1 - IndexInChunk)) · IsTablePadding'
8. (1 - IsHashInputPadding) · ((InstructionLookupServerLogDerivative' - InstructionLookupServerLogDerivative) · (🪥 - 🥝·Address - 🥥·Instruction - 🫐·Instruction') - LookupMultiplicity)
+ IsHashInputPadding · (InstructionLookupServerLogDerivative' - InstructionLookupServerLogDerivative)
9. (rate - 1 - IndexInChunk) · (PrepareChunkRunningEvaluation' - 🪑·PrepareChunkRunningEvaluation - Instruction')
+ (1 - MaxMinusIndexInChunkInv · (rate - 1 - IndexInChunk)) · (PrepareChunkRunningEvaluation' - 🪑 - Instruction')
10. (IsTablePadding' - 1) · (1 - MaxMinusIndexInChunkInv' · (rate - 1 - IndexInChunk')) · (SendChunkRunningEvaluation' - 🪣·SendChunkRunningEvaluation - PrepareChunkRunningEvaluation')
+ (SendChunkRunningEvaluation' - SendChunkRunningEvaluation) · IsTablePadding'
+ (SendChunkRunningEvaluation' - SendChunkRunningEvaluation) · (rate - 1 - IndexInChunk')
    

Terminal Constraints

1. The indicator IsHashInputPadding is 1.
2. The IndexInChunk is $\text{rate}-1$ or the indicator IsTablePadding is 1.

Terminal Constraints as Polynomials

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