circuit under-constraint in opcode-level bugs

Summary

Credited to Shankara Pailoor and Veridise https://github.com/scroll-tech/ceno/issues/883#issuecomment-4165050346

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):
https://github.com/scroll-tech/ceno/blob/e33cca0738ac6e9dba1266c50ddad7d8ef8a7515/ceno_zkvm/src/instructions/riscv/shift/shift_circuit.rs#L74

However, the actual constraint enforcing outflow is implemented differently:

https://github.com/scroll-tech/ceno/blob/e33cca0738ac6e9dba1266c50ddad7d8ef8a7515/ceno_zkvm/src/instructions/riscv/shift/shift_circuit.rs#L87-L93

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:
https://github.com/scroll-tech/ceno/blob/e33cca0738ac6e9dba1266c50ddad7d8ef8a7515/ceno_zkvm/src/instructions/riscv/mulh/mulh_circuit_v2.rs#L82

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:

https://github.com/scroll-tech/ceno/blob/e33cca0738ac6e9dba1266c50ddad7d8ef8a7515/ceno_zkvm/src/instructions/riscv/ecall/keccak.rs#L94-L98

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.

https://github.com/scroll-tech/ceno/blob/e33cca0738ac6e9dba1266c50ddad7d8ef8a7515/ceno_zkvm/src/instructions/riscv/shift/shift_circuit_v2.rs#L47-L49

However caller also missed range check
https://github.com/scroll-tech/ceno/blob/e33cca0738ac6e9dba1266c50ddad7d8ef8a7515/ceno_zkvm/src/instructions/riscv/shift/shift_circuit_v2.rs#L295-L296

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:
https://github.com/scroll-tech/ceno/blob/e33cca0738ac6e9dba1266c50ddad7d8ef8a7515/ceno_zkvm/src/instructions/riscv/mulh/mulh_circuit_v2.rs#L82

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.