Degree >2 expression in JALR

[kunxian-xia]

You can reproduce this issue by running the cmd in the feat/guest-example branch

RUST_LOG=info cargo run --release --example fibonacci_elf -- --nocapture  

to see the error msg

thread 'main' panicked at /Users/xkx/GKR/ceno/sumcheck/src/prover_v2.rs:546:26:
not implemented: do not support degree > 3

[kunxian-xia]

I think this bug is triggered by the constraints below.

ceno/ceno_zkvm/src/instructions/riscv/jump/jalr.rs

Lines 74 to 77 in 9dd45db

	circuit_builder.require_zero(
	|| "overflow_0_or_pm1",
	overflow.expr() * (overflow.expr() - 1) * (overflow.expr() + 1),
	)?;

[matthiasgoergens]

Can we add a check for constraint degree as part of the normal tests you get with cargo make tests, please?

[matthiasgoergens]

I think this bug is triggered by the constraints below.

ceno/ceno_zkvm/src/instructions/riscv/jump/jalr.rs

Lines 74 to 77 in 9dd45db

	circuit_builder.require_zero(
	|| "overflow_0_or_pm1",
	overflow.expr() * (overflow.expr() - 1) * (overflow.expr() + 1),
	)?;

Hmm, but that only looks like a cubic expression to me? Are you sure it's that one?

[hero78119]

There are 2 possible quick approach

1. commit one extra column and reduce degree, let say "overflow_tmp" and 2 constrains "req_zero(overflow_tmp - (overflow) * (1-overflow))", "req_zero((overflow +1) * (overflow_tmp))" is sufficient with overall <=3 degree

one extra degree come from 'eq' function

2. resolve/redesign circuit and see whether we can avoid "-1" logic

I think opt 1 is easier with minimal cost, opt 2 is even better

[kunxian-xia]

I think this bug is triggered by the constraints below.

ceno/ceno_zkvm/src/instructions/riscv/jump/jalr.rs

Lines 74 to 77 in 9dd45db

	circuit_builder.require_zero(
	|| "overflow_0_or_pm1",
	overflow.expr() * (overflow.expr() - 1) * (overflow.expr() + 1),
	)?;

Hmm, but that only looks like a cubic expression to me? Are you sure it's that one?

@matthiasgoergens The actual expression that is proved by sumcheck looks like 0 = \sum_b expr(b) * sel(b). Therefore its degree equals to expr.deg() + 1.

[matthiasgoergens]

Thanks, that makes sense.