[Super Issue] Ceno-ZKVM V2

[hero78119]

This is a super issue to track relevant sub issues of zkVM tasks.

• skeleton: circuit_builder + expression framework for main constraints circuit construction

• prover & verifier framework

  • prover: main constraint sel witness infer + sumcheck
  • prover: tower constraint read/write witness infer + sumcheck
  • prover: tower constraint lookup witness infer + sumcheck
  • verifier: tower constraint verification
  • verifier: main/sel constraint verification
  • optimization: devirgo style 2 stage sumcheck #103
  • degree > 1 main constraint sumcheck #107
  • stablize framework first version #102
  • zkVM framework benchmark #100
  • zkVM codebase documentation #101
  • implement batched opcodes constraint system & prover/verifier #96
  • zkvm witness generation #177
  • zkVM ConstraintSystem & proving/verifying key & namespace #151

• opcode util function

  • refactor UInt to adopt new expression design #97
  • register machine bytecode lookup #104
  • MockProver to improve debugging ability #105

• opcode (rv32im)

  • rtype

    • add
    • sub #131
    • riscv opcode mul implemetation #98
    • MULHU #130
    • DIVU #132
    • xor: bitwise XOR #121
    • and #133
    • or #134
    • SLTU #135
    • sll: shift left logical by register #123
    • SRL #282
    • slt #382
    • mulh #390
    • sra #495
    • MULHSU #510
    • div #588
    • rem #589
    • remu #590

  • itype

    • addi #186
    • srli: shift right logical by immediate #122
    • andi #361
    • xori #362
    • ori #363
    • slli #364
    • srai #365
    • sltiu #366
    • slti #367

  • btype

    • BEQ #136
    • BNE #137
    • BLTU #138
    • BGEU #139
    • blt: branch to pc + sext(imm) if (int)rs1 < (int)rs2_ #99
    • bge #383

  • jtype

    • jal: Jump and link #124
    • JALR #140

  • utype

    • AUIPC #141

  • memory

    • load/store word: lw/sw #120
    • LBU #283
    • SB #284
    • lb #384
    • sh #385
    • lh #386
    • lhu #387

  • ecall

    • ecall/halt #125

• tables

  • add range table circuit #109
  • add program table circuit #110
  • byte table (AND / OR / XOR / LT) #202
  • dummy padding table #150
  • program data table #389

• init / finalize

  • memory init / finalize #126
  • cpu state init / finalize #127

• multivariate polynomial commitment (mpcs)

  • integrate mpcs for polynomial commitment/opening #112
  • include mpcs in prover's & verifier's workflow #168
  • migrate plonky2-fri optimization
    • optimize batch_commit method #118
    • optimize batch_prove method #119
  • formalize setup phase for prover/verifier key and pre-commitment polynomial

• precompiles

  • frontend design for precompiles #591

• e2e test

  • riscv emulator to generate trace #111
  • riscv cross-compiler toolchain integration #179
    • Fibonacci program in riscv and zkVM #353

• soundnessc & audit

  • circuit debugging tool: inspect under-constraints
  • formal verification tool integration

• snarked verifier

[kunxian-xia]

The number of execution traces running the following Fibonacci program (compiled by SP1 rust toolchain) is around 12.5M (12587994).

Fibonacci rust program computing $2^{20}$-th fibonacci number

pub fn main() {
    // Compute the n'th fibonacci number, using normal Rust code.
    let mut a = 0_u32;
    let mut b = 1_u32;
    let n = 1 << 20_u32;
    for _ in 0..n {
        let mut c = a + b;
        c %= 7919; // Modulus to prevent overflow.
        a = b;
        b = c;
    }

    sp1_zkvm::io::commit(&a);
    sp1_zkvm::io::commit(&b);
}

And we report the instruction / syscall counts here.

instruction	type	count
BNE	Branching	1048598
BLTU	Branching	25
BEQ	Branching	20
BGEU	Branching	13
BLT	Branching	1
ADD	ALU	5243955
SUB	ALU	2097163
MUL	ALU	1048578
MULHU	ALU	1048576
SRL	ALU	2097844
XOR	ALU	706
OR	ALU	687
SLL	ALU	676
AND	ALU	240
SLTU	ALU	7
DIVU	ALU	1
LW	Memory	363
SW	Memory	337
LBU	Memory	102
SB	Memory	21
JALR	Control Flow	33
AUIPC	Control Flow	20
JAL	Control Flow	9
Ecall + Halt	Ecall	1
Ecall + Commit	Ecall	8
Ecall + Commit_deferred_proofs	Ecall	8

[kunxian-xia]

The table below lists opcodes that occur in the execution of several example programs.

• ✅: means that opcode occurs in the execution.
• ❌: means that opcode does not occur in the execution.

category	instruction	fibonacci	rsa	regex	ssz-withdrawal	tendermint light client
ALU	add	✅	✅	✅	✅	✅
	sub	✅	✅	✅	✅	✅
	and	✅	✅	✅	✅	✅
	or	✅	✅	✅	✅	✅
	xor	✅	✅	✅	✅	✅
	sll	✅	✅	✅	✅	✅
	srl	✅	✅	✅	✅	✅
	sra	✅	✅	✅	❌	✅
	slt	❌	✅	✅	❌	✅
	sltu	✅	✅	✅	✅	✅
ALU (M extension)	mul	✅	✅	✅	✅	✅
	mulhu	❌	✅	✅	✅	✅
	mulh	✅	❌	❌	❌	✅
	mulhsu	❌	❌	❌	❌	❌
	div	❌	❌	❌	❌	❌
	divu	❌	✅	❌	✅	✅
	rem	❌	❌	❌	❌	❌
	remu	❌	❌	❌	❌	❌
Branch	beq	✅	✅	✅	✅	✅
	bltu	✅	✅	✅	✅	✅
	bne	✅	✅	✅	✅	✅
	bgeu	✅	✅	✅	✅	✅
	blt	❌	✅	✅	✅	✅
	bge	❌	✅	✅	✅	✅
Memory Access	sw	✅	✅	✅	✅	✅
	lw	✅	✅	✅	✅	✅
	sb	✅	✅	✅	✅	✅
	lb	❌	✅	✅	✅	✅
	lbu	✅	✅	✅	✅	✅
	sh	❌	✅	✅	❌	✅
	lh	❌	✅	✅	❌	✅
	lhu	❌	✅	✅	❌	✅
Jump	jal	✅	✅	✅	✅	✅
	jalr	✅	✅	✅	✅	✅
U-type	auipc	✅	✅	✅	✅	✅
	lui	❌	❌	❌	❌	❌
syscall	ecall/halt	✅	✅	✅	✅	✅

[hero78119]

circuit statistics
#585 (comment)