Skip to content

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 added to the state machine.

We denote it by zkPC because it is verified in a zero-knowledge manner.

The zkPC 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.

Figure 7: A state machine with a Program Counter

In addition to the JMPZ(addr), an unconditional jump instruction JMP(addr) is allowed in the zkASM program.

Unlike the JMPZ(addr) instruction, when the state machine executes JMP(addr), it must jump to the line addr, irrespective of what the value of op is.

This is how the JMP(addr) instruction is implemented: A new selector called JMP is added, as a column to the execution trace. And, the Program Counter zkPC now uses the following identity to keep track of the correct line of the assembly program to be executed next;

(Eqn 0*)zkPC=(zkPC+1)+JMP(addr(zkPC+1))

JMP therefore acts as a ‘flag’ where;

  • zkPC=(zkPC+1)+0(addr(zkPC+1))=zkPC+1, if JMP is not activated (i.e., if JMP is 0), or
  • zkPC=(zkPC+1)+1(addr(zkPC+1))=addr, if JMP is activated (i.e., if JMP is 1).

Note that execution continues with the next chronological line of instruction zkPC+1 when JMP is 0, but otherwise proceeds to execute the instruction in line number addr.

The JMPZ(addr) similarly needs a selector to be added as an extra column to the execution trace, call it JMPZ.

Since the JMPZ(addr) instruction is executed only on condition that op is zero, we introduce a flag called isZero, such that; isZero=1 if op = 0, and isZero=0 if op0. This means op and isZero satisfy the following constraint,

(Eqn 1*)isZeroop=0.

Note that op is a field element, and every non-zero element of the prime field Fp has an inverse. That is, op1 exists if and only if op0. The following constraint together with Eqn 1* can be tested to check whether op and isZero are as required,

(Eqn 2*)isZero :=(1opop1)

Since JMPZ=1 only if JMPZ(addr) is the very instruction in the line currently being executed, and zkPC=addr only if isZero=1. It follows that the factor (JMPZisZero) =1 only if both JMPZ =1 and isZero =1 hold true.

Hence, the following constraint enforces the correct sequence of instructions when JMPZ is executed;

(Eqn 3*)zkPC=(zkPC+1)+(JMPZisZero)(addr(zkPC+1))

In order to ascertain correct execution of the JMPZ(addr) instruction, it suffices to check the above three constraints; Eqn 1*, Eqn 2* and Eqn 3*.

Note that op1 is not part of any instruction. The evaluations of op1 therefore have to be included in the execution trace as a committed polynomial, and thus enables checking the first identity, Eqn 1*.

Most importantly, we rename the polynomial op1 as invOp.

All four constraints, Eqn 0*, Eqn 1*, Eqn 2* and Eqn 3* can be merged as follows;

(Eqn 4*)isZero :=(1opop1), isZeroop=0,doJMP:=JPMZisZero+JMP,zkPC=(zkPC+1)+doJMP(addr(zkPC+1))

Define “addr” as an intermediate polynomial,

(Eqn **)addr:=offset,

where offset is provided as part of the jump instructions, JMPZ(addr) and JMP(addr).

We now have the following new columns in the execution trace;

zkPCJMPJMPZinvOpoffset 

With the intermediate definition in Eqn ** , we are preparing the path to expanding the addr 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 “:END” 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 line is less than N1, a step before the last step of the execution trace. That is, before jumping back to the start, with the JMP(start) instruction, the current line is checked with the function “beforeLast()”.

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; start is line 0 and finalWait is line 5.

Figure 8: Ending a Program with a loop

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 3 and a trace size (interpolation size) equal to N = 8.

We show the values corresponding to each step of the execution trace, particularly for,

  • The committed polynomials that form part of the instruction; CONST, offset, JMP, JMPZ, setB, setA, inFREE, inB, inA, zkPC and zkPC.
  • The committed polynomials that are only part of the trace; FREE, A, A, B, B and invOp.
  • The intermediate polynomials Im, which are just intermediate definitions; op, isZero and doJMP.

Step 0: “getAFreeInput()=>A”

Since the instruction here at Step 0 (corresponding to line 0 of the Assembly code) requires a free input 3 to be taken and moved into the registry A. The values of the involved polynomials are therefore;

inFREE=1, FREE=3, setA=1, A=3 and CONST=0.

As a result,

op = inAA + inBB + inFREEFREE + CONST=0A + 0B + 13 + 0 =3

and invOp=31.

Regarding the Program Counter; First note that initially zkPC=0. And, since op=3 and invOp=31, then

isZero :=(1opop1)=(1331)=0. 

Also, since there are no jumps in the instruction, JMP=0 and JMPZ=0, and therefore zkPC=zkPC+1.

We use Eqn 4* to check whether zkPC=zkPC+1=0+1=1.

First, note that,

doJMP:=JPMZisZero+JMP=00+0=0.

This means, according to Eqn 4,

zkPC=(zkPC+1)+doJMP(addr(zkPC+1))=(0+1)+0(addr(0+1))=0+1=1.

Step 1: “−3=>B, −3=>B”

In this step, a constant CONST=3 is moved into the B registry. Hence setB=1, B=3, but inB=0, inA=0 and inFREE=0. This yields,

op= inAA + inBB + inFREEFREE + CONST = 0A + 0B + 0FREE +(3)=3

and invOp=(3)1.

So, isZero :=(1opop1)=(1(3)(3)1)=0.

Again, the absence of jumps in the instruction means, JMP=0 and JMPZ=0. And therefore zkPC=zkPC+1.

Again, we use Eqn 4 to check whether zkPC=zkPC+1=1+1=2.

Note that,

doJMP:=JPMZisZero+JMP=00+0=0.

Since zkPC=1, the next value of the Program Counter (according to Eqn 4*) must therefore be,

zkPC=(zkPC+1)+doJMP(addr(zkPC+1))=(1+1)+0(addr(1+1))=2.

Here is the execution trace thus far;

stepinstructionsCONSToffsetJMPJMPZsetBsetAinFREEinBinAzkPCzkPC0getAFreeInput()=>A 0000011000113=>B    30001000012
opisZerodoJMPFREEAABBinvOp 30030300 3130003303 (3)1

Step 2: “: ADD”

Here the sum of the registry values A=3 and B=3 is computed, and the result is moved into the registry A. That is, A=3+(3)=0 and setA=1. Also, inA=1 , inB=1 and inFREE=0.

These values yield the following value of op,

op =inAA+inBB+inFREEFREE+CONST=13+1(3)+0FREE+0=0.

So, invOp is set to a randomly chosen non-zero α in Fp , used to pass the identities related to isZero.

And, isZero:=(1opinvOp)=(10α)=1.

Note that there are no jumps in the instruction, so JMP=0 and JMPZ=0. And therefore zkPC=zkPC+1.

In order to verify that zkPC=zkPC+1=2+1=3, we use the constraints given as Eqn 4* above.

Firstly, check doJMP as follows,

doJMP := JPMZisZero+JMP =01 + 0 = 0.

Then,

zkPC=(zkPC+1)+doJMP(addr(zkPC+1))=(2+1)+0(addr(2+1))=3.

The Program Counter therefore moves to the subsequent line of instruction. That is, the next instruction to be executed must the one in line 3 of the Assembly code.

Step 3: “A :JMPZ(finalWait)”

According this instruction, the executor has to jump on condition that A is 0, otherwise there is no jump. The polynomials immediately involved in this instruction are inA and JMPZ. Therefore, inA=1 and JMPZ=1.

As mentioned above, the implicit address label “finalWait” is computed by the Assembly compiler, and in this example, that address is line 5. That is, offset=5. It follows that zkPC=5.

Note that, inB=0 , inFREE=0 and CONST=0. Therefore,

op=inAA+inBB+inFREEFREE+CONST=10+0(3)+0FREE+0=0.

Consequently, isZero:=(1opinvOp)=(10)=1. And since there are no unconditional jumps, JMP=0.

We use Eqn 4 to check whether zkPC=5. Note that,

doJMP:=JPMZisZero+JMP=11+0=1.

The next value of the Program Counter, according to Eqn 4, is

zkPC=(zkPC+1)+doJMP(addr(zkPC+1))=(3+1)+1(5(3+1))=4+(54)=5.

Step 4: “{beforeLast()} :JMPZ(finalWait)”

The beforeLast() 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 4 and not 6, then the executor returns a zero. And thus, inFREE=1 and JMPZ=1 but inA=0, inB=0, FREE=0 and CONST=0. Consequently,

op=inAA+inBB+inFREEFREE+CONST=0A+0B+10+0=0.

Therefore isZero:=(1opinvOp)=(10α)=1.

Hence according to JMPZ(finalWait), a jump is executed. This means the executor must jump to the offset=5 address, as computed by the Assembly compiler. It follows that zkPC must be 5.

Let us use Eqn 4* to check if indeed zkPC=5. We first note that, there are no unconditional jumps, so JMP=0. And,

doJMP:=JPMZisZero+JMP=11+0=1.

The next value of the Program Counter is given by,

zkPC=(zkPC+1)+doJMP(addr(zkPC+1))=(5+1)+1(5(5+1))=6+(56)=5.

The execution trace is currently as follows,

stepinstructionsCONSToffsetJMPJMPZsetBsetAinFREEinBinAzkPCzkPC0getAFreeInput()=>A0000011000113=>B   300010000122:ADD 000001011233A:JMPZ(finalWait)050100001354{beforeLast()}:JMPZ(finalWait)05010010055
opisZerodoJMPFREEAABBinvOp 30030300 3130003303 (3)1 0100303 3 α 0110003 3 α 0110003 3α

Step 5: “{beforeLast()} :JMPZ(finalWait)”

As seen in Step 4, the beforeLast() function checks if the execution trace is currently at Step 6. Since the current step is 5 and not 6, the executor returns a zero.

Similarly, inFREE=1 and JMPZ=1 but inA=0, inB=0, FREE=0 and CONST=0. As a result,

op=inAA+inBB+inFREEFREE+CONST=0A+0B+10+0=0,

which means FREE=0 and isZero :=(1opinvOp) =(10α)=1. So, again JMPZ(finalWait) gets executed.

The absence of unconditional jumps means JMP=0, while JMPZ=1. Since offset=5, the Program Counter, zkPC, must in the next step be 5.

We verify this by first checking:

doJMP:=JPMZisZero+JMP=11+0=1,

and use Eqn 4,

zkPC=(zkPC+1)+doJMP(addr(zkPC+1))=(5+1)+1(5(5+1))=6+(56)=5.

Step 6: “{beforeLast()} :JMPZ(finalWait)”

In this case, the current step is the last but one step. That is, the beforeLast() function holds true, and hence the executor must return a 1. So, inFREE=1 and JMPZ=1 while inA=0, inB=0 and CONST=0. Then,

op=inAA+inBB+inFREEFREE+CONST=0A+0B+11+0=1.

This means FREE=1 and isZero :=(1opinvOp) =(111)=0. And, this time JMPZ(finalWait) is not executed, implying the next Program Counter, zkPC=zkPC+1.

Since there are no jumps in this step, JMP=0 and JMPZ=0, yielding

doJMP:=JPMZisZero+JMP=01+0=0,

and with a quick verification using Eqn 4*, we obtain

zkPC=(zkPC+1)+doJMP(addr(zkPC+1))=(5+1)+0(addr(5+1))=6.

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 8 in this example).

It ends the execution by setting A and B to zero, and jumps to start, which is line 0. And thus, zkPC must be 0.

Hence, setA=1, setB=1 and JMP=1 but inFREE=0, inA=0, inB=0 and CONST=0. Consequently,

op=inAA+inBB+inFREEFREE+CONST=00+0(3)+01+0=0.

Therefore isZero:=(1opinvOp)=(10α)=1.

There are no conditional jumps, so JMPZ=0. Then, as a consequence of this,

doJMP:=JPMZisZero+JMP=01+1=1.

The constraint in Eqn 4* verifies the next value of the Program Counter as follows,

zkPC=(zkPC+1)+doJMP(addr(zkPC+1)) = (6+1) + 1(0(6+1)) = 0.

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 A, B and zkPC to zero causes the execution trace to attain cyclicity.

See the complete execution trace below,

stepinstructionsCONSToffsetJMPJMPZsetBsetAinFREEinBinAzkPCzkPC0getAFreeInput()=>A0000011000113=>B   300010000122:ADD 000001011233A:JMPZ(finalWait)050100001354{beforeLast()}:JMPZ(finalWait)050100100555{beforeLast()}:JMPZ(finalWait)050100100556{beforeLast()}:JMPZ(finalWait)0501001005670=>A,B  :JMP(start)00101100060
opisZerodoJMPFREEAABBinvOp 30030300 3130003303 (3)1 0100303 3 α 0110003 3 α 0110003 3α 0110003 3 α 1001003 3 1 0110003 0α

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 A, 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 offset 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., zkPC2N1 where 2N1 is the degree of the state machine polynomials.

Publics placed at known steps

Regarding the publics, 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 A and B until they are reset to Step 0.

So if, for example, the execution result or state machine output is the state of registry A at the end of all the instructions, we will find this value at A(N1).

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 update: January 17, 2024
Authors: avenbreaks