Design of traces

[matthiasgoergens]

#6

Let's discuss what format we want our traces to be in, and how to record and use them.

As a first step, we will have to capture execution. We can do that as a Vec<State> (with persistent data structures inside State to keep memory usage from becoming O(memory * cycles). That can decouples the dynamic aspect of the execution from the work of converting into a trace proper.

[vivekvpandya]

trace.xlsx

Attaching a trace generated with OlaVM for a Fibonacci program. Mainly it has following columns:

• Value of each registers R0-R8, value of clk, value of pc
• selector to indicate which register has been used as opd0, opd1 and dest
• selector to indicate what is current instruction, i.e is it add,mul,load,store etc.
• value of immediate operand when instruction supports such opd
• some other stuffs

if we go by this design our main(processor) trace will be very large :

• roughly 40+ instruction selector
• 3 * 32 selectors for which register is used for opd1/opd2 and dest
• 32 registers

So above can be roughly 170-180 columns. This feels a large table. Although we can do something similar to https://github.com/zcash/halo2/blob/main/halo2_proofs/src/plonk/circuit/compress_selectors.rs and https://hackmd.io/@daira/SkjDVkLCd
to reduce the number of columns.

[vivekvpandya]

Just to note Triton-VM's trace looks much different compare to OlaVM. Is it because OlaVM is plonk based on Triton is not?

[eightfilms]

I just took a look at their tables and such, they seem to be still relying on lookup tables to link their different traces together. How would being plonk-based change the way their traces are designed?

[vivekvpandya]

PROCESSOR_TRACE

CLK	PC	RAW_INST	OPCODE	RS1	RS2	RD	op_imm	imm_value	s_add	s_sub	s_mul	s_jal	...	s_conditional_branch_taken

Constraints:

CLK: clk is always incremented by 1

next_clk – last_clk -1  == 0

Registers: Except destination registers, all other reg values stay the same between 2 rows.

For reg in 0..31
    (reg - rd) * (next_reg_value - last_reg_value) == 0

Only one opcode selector is enabled

1 - (sum of all s_add, s_sub, ...) == 0

Program counter (PC)

   // NOTE: addition to PC should be chosen to be signed or unsigned based on instruction semantics.
    let increase_by_4 = (1 - (s_JAL + s_jalr) * (next_pc - (last_pc + 4));
    let jal_pc = next_pc - (S_JAL * last_pc + op1_imm * 2);
    let jalr_pc = next_pc - (S_JALR * (last_rs1_value + imm) / 2);
    let conditional_branch_pc = next_pc - ((s_beq + s_bne + s_blt + s_bge + s_bltu + s_bgeu) * ((s_conditional_branch_taken) * (last_pc + imm) + (1 - s_conditional_branch_taken
) *(last_pc + 4))); 

constraints for each opcode except opcodes handled in builtins.

ADD
ADDI
SUB
MUL
JAL
LUI
AUIPC
...

last row should be ECALL 93 (i.e exit system call)?
what to put as padding row? same as ECALL 93?

[matthiasgoergens]

Is putting ecall last just a convention, or does it have to be there?

[matthiasgoergens]

I don't think we necessarily need to have separate ADD and ADDI opcodes:

We could encode an 'addition' instruction that takes both two registers and an immediate operand and adds them all together.

[vivekvpandya]

Good point! For ADD/ADDI we can check following constraint:

     S_ADD * ((1 - op_imm) * (next_rd - (last_rs1 + last_rs2)) + op_imm * (next_rd - (last_rs1 + imm_value))) == 0 

[vivekvpandya]

And perhaps similar check for other instruction which has same smentics and support both R and I type format. This saves some columns. I hope this does not increase degree , for above example degree is 3

[vivekvpandya]

Is putting ecall last just a convention, or does it have to be there?

we can have some instruction internally like END just to represent END of trace. But will need to chose value in field carefully.

[matthiasgoergens]

#121 might help with the traces.