circuit under-constraint in opcode-level bugs

[hero78119]

Summary

Credited to Shankara Pailoor and Veridise #883 (comment)

cite to original report ceno bugs

This issue highlights several soundness bugs and constraint inconsistencies identified across multiple opcode circuits. These issues may allow a malicious prover to satisfy constraints while violating intended semantic bounds.

---

v1 in Goldilocks Circuit: Missing Outflow Range Assumption

Issue

There is a general pattern in opcode circuits that rely on inflow/outflow-style constraints. These implicitly assume that outflow ∈ [0, 2^32).

Reference (assumption):

ceno/ceno_zkvm/src/instructions/riscv/shift/shift_circuit.rs

Line 74 in e33cca0

// 32 + 31. 31. 31 + 32. 32. (Bit widths)

However, the actual constraint enforcing outflow is implemented differently:

ceno/ceno_zkvm/src/instructions/riscv/shift/shift_circuit.rs

Lines 87 to 93 in e33cca0

	let assert_lt_config = AssertLtConfig::construct_circuit(
	circuit_builder,
	|| "outflow < pow2_rs2_low5",
	outflow.expr(),
	pow2_rs2_low5.expr(),
	UINT_LIMBS * LIMB_BITS,
	)?;

This does not guarantee that outflow ≥ 0 or that it is bounded within [0, 2^32).

Impact

A malicious prover can set:

• outflow ≥ 2^32

while still satisfying the constraint by compensating with a small positive pow2_rs2_low5.

This breaks the intended soundness assumption.

---

v2 in BabyBear circuit: Limb Multiplication Overflow

Issue

In the BabyBear field, special care is required when multiplying limbs that may exceed u16.

Example:

ceno/ceno_zkvm/src/instructions/riscv/mulh/mulh_circuit_v2.rs

Line 82 in e33cca0

carry_low[i] = carry_divide.expr() * (expected_limb - rd_low[i].expr());

This constraint can be interpreted as:

carry_low[i] * 2^16 = limb - rd_low[i]

Problem

• carry_low[i] can be up to 18 bits
• LHS becomes up to 2^(18+16) bits, exceeding the BabyBear field modulus

Impact

• The RHS is no longer canonical in the field
• Multiple values can satisfy the equation
• This introduces ambiguity in rd_low[i], leading to multiple valid witness assignments

---

Incorrect RW Flag in ECALL

Issue

All ECALL argument 0 (arg0) are marked as read-write = true generically:

ceno/ceno_zkvm/src/instructions/riscv/ecall/keccak.rs

Lines 94 to 98 in e33cca0

	let state_ptr = OpFixedRS::<_, { Platform::reg_arg0() }, true>::construct_circuit(
	cb,
	state_ptr_value.uint_unaligned().register_expr(),
	vm_state.ts,
	)?;

Impact

This allows unintended mutation of the pointer value.

A malicious prover can:

• Manipulate arg0
• Redirect it to arbitrary memory locations after the operation

This breaks memory safety assumptions.

---

missing u8 range check for opcode not leverage lookup

Issue

There are based config which assume external range check has done by caller
e.g.

ceno/ceno_zkvm/src/instructions/riscv/shift/shift_circuit_v2.rs

Lines 47 to 49 in e33cca0

	a: [Expression<E>; NUM_LIMBS],
	b: [Expression<E>; NUM_LIMBS],
	c: [Expression<E>; NUM_LIMBS],

However caller also missed range check

ceno/ceno_zkvm/src/instructions/riscv/shift/shift_circuit_v2.rs

Lines 295 to 296 in e33cca0

	let rs1_read = UInt8::new_unchecked(|| "rs1_read", circuit_builder)?;
	let rs2_read = UInt8::new_unchecked(|| "rs2_read", circuit_builder)?;

Impact

Missing u8 lookup range check lead to non-canonical decomposition of a 16 bits number, which malicious could change opcode behaviours

Issue

In the BabyBear field, special care is required when multiplying limbs that may exceed u16.

Example:

ceno/ceno_zkvm/src/instructions/riscv/mulh/mulh_circuit_v2.rs

Line 82 in e33cca0

carry_low[i] = carry_divide.expr() * (expected_limb - rd_low[i].expr());

This constraint can be interpreted as:

carry_low[i] * 2^16 = limb - rd_low[i]

Problem

• carry_low[i] can be up to 18 bits
• LHS becomes up to 2^(18+16) bits, exceeding the BabyBear field modulus

Impact

• The RHS is no longer canonical in the field
• Multiple values can satisfy the equation
• This introduces ambiguity in rd_low[i], leading to multiple valid witness assignments

---

Conclusion

These issues collectively introduce soundness risks:

• Missing range constraints
• Field overflow leading to non-uniqueness
• Incorrect memory access permissions

Each should be addressed to restore constraint correctness and prevent adversarial witness construction.