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
The
In addition to the
Unlike the
Program Counter constraint related to JMP¶
This is how the
, 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
Program Counter constraint related to JMPZ¶
The
Since the
Note that
Since
Hence, the following constraint enforces the correct sequence of instructions when
In order to ascertain correct execution of the
Note that
Most importantly, we rename the polynomial
Program Counter constraint related to JMP and JMPZ¶
All four constraints,
Define “
where
We now have the following new columns in the execution trace;
With the intermediate definition in
Correct program ending with a loop¶
We have previously resorted to ending our program by repeating the “
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
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;
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
We show the values corresponding to each
- 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
As a result,
and
Regarding the Program Counter; First note that initially
Also, since there are no jumps in the instruction,
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
and
So,
Again, the absence of jumps in the instruction means,
Again, we use Eqn 4 to check whether
Note that,
Since
Here is the execution trace thus far;
Step 2: “: ADD”¶
Here the sum of the registry values
These values yield the following value of
So,
And,
Note that there are no jumps in the instruction, so
In order to verify that
Firstly, check
Then,
The Program Counter therefore moves to the subsequent line of instruction. That is, the next instruction to be executed must the one in
Step 3: “A :JMPZ(finalWait)”¶
According this instruction, the executor has to jump on condition that
As mentioned above, the implicit address label “
Note that,
Consequently,
We use Eqn 4 to check whether
The next value of the Program Counter, according to Eqn 4, is
Step 4: “{beforeLast()} :JMPZ(finalWait)”¶
The
Therefore
Hence according to
Let us use Eqn 4* to check if indeed
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
Similarly,
which means
The absence of unconditional jumps means
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
This means
Since there are no jumps in this step,
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
It ends the execution by setting
Hence,
Therefore
There are no conditional jumps, so
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
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
Note that in cases where the jumps are such that
Publics placed at known steps¶
Regarding the
Notice that, in the above example, the final loop added to Assembly program repeats the values of the registries
So if, for example, the execution result or state machine output is the state of registry
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.