Program Counter
## Checking sequence of instructions In order to keep track of which line of the program is currently being executed, a new registry called "program counter" is
Checking sequence of instructions
In order to keep track of which line of the program is currently being executed, a new registry called "program counter" is added to the state machine.
We denote it by because it is verified in a zero-knowledge manner.
The is therefore a new column of the execution trace and it contains, at each clock, the line in the zkASM program of the instruction being executed.

In addition to the , an unconditional jump instruction is allowed in the zkASM program.
Unlike the instruction, when the state machine executes , it must jump to the line , irrespective of what the value of is.
Program counter constraint related to JMP
This is how the instruction is implemented: A new selector called is added, as a column to the execution trace. And, the program counter now uses the following identity to keep track of the correct line of the assembly program to be executed next;
therefore acts as a 'flag' where;
- , if is not activated (i.e., if is ), or
- , if is activated (i.e., if is ).
Note that execution continues with the next chronological line of instruction when is , but otherwise proceeds to execute the instruction in line number .
Program counter constraint related to JMPZ
The similarly needs a selector to be added as an extra column to the execution trace, call it .
Since the instruction is executed only on condition that is zero, we introduce a flag called , such that; if , and if . This means and satisfy the following constraint,
Note that is a field element, and every non-zero element of the prime field has an inverse. That is, exists if and only if . The following constraint together with can be tested to check whether and are as required,
Since only if is the very instruction in the line currently being executed, and only if . It follows that the factor only if both and hold true.
Hence, the following constraint enforces the correct sequence of instructions when is executed;
In order to ascertain correct execution of the instruction, it suffices to check the above three constraints; , and .
Note that is not part of any instruction. The evaluations of therefore have to be included in the execution trace as a committed polynomial, and thus enables checking the first identity, .
Most importantly, we rename the polynomial as .
Program counter constraint related to JMP and JMPZ
All four constraints, , , and can be merged as follows;
Define "" as an intermediate polynomial,
where is provided as part of the jump instructions, and .
We now have the following new columns in the execution trace:
With the intermediate definition in , we are preparing the path to expanding the definition, for example, to include other sources (apart from instructions) from which to get the destination address in jumps.
Correct program ending with a loop
We have previously resorted to ending our program by repeating the "" instruction. This was not the best solution.
To properly finish our programs, we need to ensure that the execution trace generated from the assembly is cyclic.
We therefore utilise a loop while the current is less than , a step before the last step of the execution trace. That is, before jumping back to the start, with the instruction, the current is checked with the function "".
So, we query the executor for when the execution trace is at its last but one row, with the following line of code,
$beforeLast() :JMPZ(finalWait);The assembly program uses labels instead of explicit line numbers, hence conforming to how assembly programs are typically written. Labels are convenient because with them, the assembly compiler can take care of computing actual line numbers. For instance, as in Figure 8 below; is line and is line .

Commentary on the execution trace
The intention here to give a step-by-step commentary on the execution trace for the Assembly code in Figure 8 above, for a free input equal to and a trace size (interpolation size) equal to .
We show the values corresponding to each of the execution trace, particularly for,
- The committed polynomials that form part of the instruction; , , , , , , , , , and .
- The committed polynomials that are only part of the trace; , , , , and .
- The intermediate polynomials , which are just intermediate definitions; , and .
Step 0: "getAFreeInput()=>A"
Since the instruction here at (corresponding to of the Assembly code) requires a free input to be taken and moved into the registry . The values of the involved polynomials are therefore;
As a result,
and .
Regarding the program counter, first note that initially . And, since and , then
Also, since there are no jumps in the instruction, and , and therefore .
We use Eqn 4* to check whether .
First, note that,
This means, according to Eqn 4,
Step 1: "-3=>B, -3=>B"
In this step, a constant is moved into the registry. Hence , , but , and . This yields,
and .
So, .
Again, the absence of jumps in the instruction means, and . And therefore .
Again, we use Eqn 4 to check whether .
Note that,
Since , the next value of the program counter (according to Eqn 4*) must therefore be,
Here is the execution trace thus far;
Step 2: ": ADD"
Here the sum of the registry values and is computed, and the result is moved into the registry . That is, and . Also, , and .
These values yield the following value of ,
So, is set to a randomly chosen non-zero in , used to pass the identities related to .
And, .
Note that there are no jumps in the instruction, so and . And therefore .
In order to verify that , we use the constraints given as Eqn 4* above.
Firstly, check as follows,
Then,
The program counter therefore moves to the subsequent line of instruction. That is, the next instruction to be executed must the one in of the Assembly code.
Step 3: "A :JMPZ(finalWait)"
According this instruction, the executor has to jump on condition that is , otherwise there is no jump. The polynomials immediately involved in this instruction are and . Therefore, and .
As mentioned above, the implicit address label "" is computed by the Assembly compiler, and in this example, that address is . That is, . It follows that .
Note that, , and . Therefore,
Consequently, . And since there are no unconditional jumps, .
We use Eqn 4 to check whether . Note that,
The next value of the program counter, according to Eqn 4, is
Step 4: {beforeLast()} :JMPZ(finalWait)
The function, which keeps track of the number of steps being executed, reads the current step-number as a free input. Since the execution trace is currently at step and not , then the executor returns a zero. And thus, and but , , and . Consequently,
Therefore .
Hence according to , a jump is executed. This means the executor must jump to the address, as computed by the Assembly compiler. It follows that must be .
Let us use Eqn 4* to check if indeed . We first note that, there are no unconditional jumps, so . And,
The next value of the program counter is given by,
The execution trace is currently as follows,
Step 5: {beforeLast()} :JMPZ(finalWait)
As seen in Step 4, the function checks if the execution trace is currently at Step 6. Since the current step is and not , the executor returns a zero.
Similarly, and but , , and . As a result,
which means and . So, again gets executed.
The absence of unconditional jumps means , while . Since , the program counter, , must in the next step be .
We verify this by first checking:
and use Eqn 4,
Step 6: {beforeLast()} :JMPZ(finalWait)
In this case, the current step is the last but one step. That is, the function holds true, and hence the executor must return a . So, and while , and . Then,
This means and . And, this time is not executed, implying the next program counter, .
Since there are no jumps in this step, and , yielding
and with a quick verification using Eqn 4*, we obtain
Step 7: "0=>A,B :JMP(start)"
The aim with this instruction is to complete the execution trace such that it is of the correct size (which is in this example).
It ends the execution by setting and to zero, and jumps to , which is line . And thus, must be .
Hence, , and but , , and . Consequently,
Therefore .
There are no conditional jumps, so . Then, as a consequence of this,
The constraint in Eqn 4* verifies the next value of the program counter as follows,
This instruction, as the last step the Assembly program, achieves two things; Firstly, the program ends correctly with the specified size of the execution trace. Secondly, resetting , and to zero causes the execution trace to attain cyclicity.
See the complete execution trace below,
In conclusion, our Assembly program uses jumps to create a loop in its execution. That is, at the right point of the execution, when the registry values of interest have been attained, the executor retains these values until the execution trace is in the last but one row. This way, the result of the computations can be reflected in the last position of the registry , in the last row of the execution trace, which is the output of the mFibonacci state machine.
Note that in cases where the jumps are such that is one of the previous addresses, the length of the execution trace can turn out to be much bigger than the final value of the program counter. i.e., where is the degree of the state machine polynomials.
Publics placed at known steps
Regarding the , it is best to place these at specific and known steps.
Notice that, in the above example, the final loop added to Assembly program repeats the values of the registries and until they are reset to Step .
So if, for example, the execution result or state machine output is the state of registry at the end of all the instructions, we find this value at .
This is important for verification purposes, because then, we need only add the proper boundary constraint in the PIL, referencing a specific step in the execution trace.
Last updated on
Plookup
The main state machine executor sends various instructions to the secondary state machines within the zkProver. Although secondary state machines specialize in
Commitment Scheme
The framework for the proof-verification system of our mFibonacci state machine is that of a _polynomial commitment scheme_. The mechanism for proving correctne