Jolt defines a few virtual instructions that are not part of RISC-V:
[x] ASSERT_LTU
[x] ASSERT_LTE
[x] ASSERT_EQ
[x] ADVICE
[ ] MOVE
It also defines a virtual set of registers used by the virtual instructions:
[x] v_q, v_r, v_qy
Since virtual instructions don't correspond to the original program, Jolt mentions having two program counters, one to keep track of the RISCV PC, and the other to keep track of all instructions (including virtual ones).
I believe we should also implement the virtual instructions in the emulator. We could do the following:
Take the source program (as a list of instructions) and transform it to another program with the virtual instructions (by replacing div, rem, etc. by their virtual code)
While doing 1, build a map (in the form of a table) from original PC to virtual PC
The emulator will now work on the extended program and will have pc and pc_virt. Each non-virtual instruction increments both pc and pc_virt, and virtual instructions only increment pc_virt.
To fetch instructions we use pc with the mapping we built in point 2, to obtain the instruction from the extended program.
See Jolt 6.1
Jolt defines a few virtual instructions that are not part of RISC-V:
It also defines a virtual set of registers used by the virtual instructions:
Since virtual instructions don't correspond to the original program, Jolt mentions having two program counters, one to keep track of the RISCV PC, and the other to keep track of all instructions (including virtual ones).
I believe we should also implement the virtual instructions in the emulator. We could do the following:
pcandpc_virt. Each non-virtual instruction increments bothpcandpc_virt, and virtual instructions only incrementpc_virt.pcwith the mapping we built in point 2, to obtain the instruction from the extended program.