diff --git a/ceno_zkvm/src/gadgets/is_lt.rs b/ceno_zkvm/src/gadgets/is_lt.rs index c9dedaa03..06ecc4f46 100644 --- a/ceno_zkvm/src/gadgets/is_lt.rs +++ b/ceno_zkvm/src/gadgets/is_lt.rs @@ -18,6 +18,7 @@ use crate::{ use super::SignedExtendConfig; +// TODO rename to AssertLtConfig (LT -> Lt) to fit naming conventions #[derive(Debug, Clone)] pub struct AssertLtConfig(InnerLtConfig); diff --git a/ceno_zkvm/src/gadgets/mod.rs b/ceno_zkvm/src/gadgets/mod.rs index 0f21b3ce2..3ea9ff41d 100644 --- a/ceno_zkvm/src/gadgets/mod.rs +++ b/ceno_zkvm/src/gadgets/mod.rs @@ -1,6 +1,7 @@ mod div; mod is_lt; mod is_zero; +mod signed; mod signed_ext; pub use div::DivConfig; @@ -8,4 +9,5 @@ pub use is_lt::{ AssertLtConfig, AssertSignedLtConfig, InnerLtConfig, IsLtConfig, SignedLtConfig, cal_lt_diff, }; pub use is_zero::{IsEqualConfig, IsZeroConfig}; +pub use signed::Signed; pub use signed_ext::SignedExtendConfig; diff --git a/ceno_zkvm/src/gadgets/signed.rs b/ceno_zkvm/src/gadgets/signed.rs new file mode 100644 index 000000000..520be32c0 --- /dev/null +++ b/ceno_zkvm/src/gadgets/signed.rs @@ -0,0 +1,51 @@ +use std::fmt::Display; + +use ff_ext::ExtensionField; + +use crate::{ + Value, circuit_builder::CircuitBuilder, error::ZKVMError, expression::Expression, + instructions::riscv::constants::UInt, witness::LkMultiplicity, +}; + +use super::SignedExtendConfig; + +/// Interprets a `UInt` value as a 2s-complement signed value. +/// +/// Uses 1 `WitIn` to represent the most sigificant bit of the value. +pub struct Signed { + pub is_negative: SignedExtendConfig, + val: Expression, +} + +impl Signed { + pub fn construct_circuit + Display + Clone, N: FnOnce() -> NR>( + cb: &mut CircuitBuilder, + name_fn: N, + unsigned_val: &UInt, + ) -> Result { + cb.namespace(name_fn, |cb| { + let is_negative = unsigned_val.is_negative(cb)?; + let val = unsigned_val.to_field_expr(is_negative.expr()); + + Ok(Self { is_negative, val }) + }) + } + + pub fn assign_instance( + &self, + instance: &mut [::BaseField], + lkm: &mut LkMultiplicity, + val: &Value, + ) -> Result { + self.is_negative.assign_instance( + instance, + lkm, + *val.as_u16_limbs().last().unwrap() as u64, + )?; + Ok(i32::from(val)) + } + + pub fn expr(&self) -> Expression { + self.val.clone() + } +} diff --git a/ceno_zkvm/src/gadgets/signed_ext.rs b/ceno_zkvm/src/gadgets/signed_ext.rs index 3b6757bc3..0ee17208c 100644 --- a/ceno_zkvm/src/gadgets/signed_ext.rs +++ b/ceno_zkvm/src/gadgets/signed_ext.rs @@ -2,18 +2,23 @@ use crate::{ circuit_builder::CircuitBuilder, error::ZKVMError, expression::{Expression, ToExpr, WitIn}, - instructions::riscv::constants::UInt, + instructions::riscv::constants::{LIMB_BITS, UInt}, set_val, witness::LkMultiplicity, }; use ff_ext::ExtensionField; use std::marker::PhantomData; +/// Extract the most significant bit from an expression previously constrained +/// to an 8 or 16-bit length. +/// +/// Uses 1 `WitIn` value to store the bit, one `assert_bit` constraint, and one +/// `u8` or `u16` table lookup. #[derive(Debug)] pub struct SignedExtendConfig { - /// most significant bit + /// Most significant bit msb: WitIn, - /// number of bits contained in the value + /// Number of bits of the represented value n_bits: usize, _marker: PhantomData, @@ -24,7 +29,7 @@ impl SignedExtendConfig { cb: &mut CircuitBuilder, val: Expression, ) -> Result { - Self::construct_circuit(cb, 16, val) + Self::construct_circuit(cb, LIMB_BITS, val) } pub fn construct_byte( diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index f162478fa..d7ed7ca31 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -1,123 +1,348 @@ +//! Circuit implementations for DIVU, REMU, DIV, and REM RISC-V opcodes +//! +//! The signed and unsigned division and remainder opcodes are handled by +//! simulating the division algorithm expression: +//! +//! `dividend = divisor * quotient + remainder` (1) +//! +//! where `remainder` is constrained to be between 0 and the divisor in a way +//! that suitably respects signed values, except for the case of division by 0. +//! Of particular note for this implememntation is the fact that in the +//! Goldilocks field, the right hand side of (1) does not wrap around under +//! modular arithmetic for either unsigned or signed 32-bit range-checked +//! values of `divisor`, `quotient`, and `remainder`, taking values between `0` +//! and `2^64 - 2^32` in the unsigned case, and between `-2^62` and `2^62 + +//! 2^31 - 1` in the signed case. +//! +//! This means that in either the unsigned or the signed setting, equation +//! (1) can be checked directly using native field expressions without +//! ambiguity due to modular field arithmetic. +//! +//! The remainder of the complexity of this circuit comes about because of two +//! edge cases in the opcodes: division by zero, and signed division overflow. +//! For division by zero, equation (1) still holds, but an extra constraint is +//! imposed on the value of `quotient` to be `u32::MAX` in the unsigned case, +//! or `-1` in the unsigned case (the 32-bit vector with all 1s for both). +//! +//! Signed division overflow occurs when `dividend` is set to `i32::MIN +//! = -2^31`, and `divisor` is set to `-1`. In this case, the natural value of +//! `quotient` is `2^31`, but this value cannot be properly represented as a +//! signed 32-bit integer, so an error output must be enforced with `quotient = +//! i32::MIN`, and `remainder = 0`. In this one case, the proper RISC-V values +//! for `dividend`, `divisor`, `quotient`, and `remainder` do not satisfy the +//! division algorithm expression (1), so the proper values of `quotient` and +//! `remainder` can be enforced by instead imposing the variant constraint +//! +//! `2^31 = divisor * quotient + remainder` (2) +//! +//! Once (1) or (2) is appropriately satisfied, an inequality condition is +//! imposed on remainder, which varies depending on signs of the inputs. In +//! the case of unsigned inputs, this is just +//! +//! `0 <= remainder < divisor` (3) +//! +//! for signed inputs, the inequality is a little more complicated: for +//! `dividend` and `divisor` with the same sign, quotient and remainder are +//! non-negative, and we require +//! +//! `0 <= remainder < |divisor|` (4) +//! +//! When `dividend` and `divisor` have different signs, `quotient` and +//! `remainder` are non-positive values, and we instead require +//! +//! `-|divisor| < remainder <= 0` (5) +//! +//! To handle these variations of the remainder inequalities in a uniform +//! manner, we derive expressions representing the "positively oriented" values +//! with signs set so that the inequalities are always of the form (3). Note +//! that it is not enough to just take absolute values, as this would allow +//! values with an incorrect sign, e.g. for 10 divided by -6, one could witness +//! `10 = -6 * 2 + 2` instead of the correct expression `10 = -6 * 1 - 4`. +//! +//! The inequality condition (5) is properly satisfied by `divisor` and the +//! appropriate value of `remainder` in the case of signed division overflow, +//! so no special treatment is needed in this case. On the other hand, these +//! inequalities cannot be satisfied when `divisor` is `0`, so we require that +//! exactly one of `remainder < divisor` and `divisor = 0` holds. +//! Specifically, since these conditions are expressed as 0/1-valued booleans, +//! we require just that the sum of these booleans is equal to 1. + use ceno_emul::{InsnKind, StepRecord}; +use ff::Field; use ff_ext::ExtensionField; +use goldilocks::{Goldilocks, SmallField}; use super::{ RIVInstruction, constants::{UINT_LIMBS, UInt}, - dummy::DummyInstruction, r_insn::RInstructionConfig, }; use crate::{ circuit_builder::CircuitBuilder, error::ZKVMError, - expression::Expression, - gadgets::{IsLtConfig, IsZeroConfig}, + expression::{Expression, ToExpr, WitIn}, + gadgets::{AssertLtConfig, IsEqualConfig, IsLtConfig, IsZeroConfig, Signed}, instructions::Instruction, + set_val, uint::Value, + utils::i64_to_base, witness::LkMultiplicity, }; use std::marker::PhantomData; -pub struct ArithConfig { - r_insn: RInstructionConfig, +pub struct DivRemConfig { + dividend: UInt, // rs1_read + divisor: UInt, // rs2_read + quotient: UInt, + remainder: UInt, - dividend: UInt, - divisor: UInt, - pub(crate) outcome: UInt, + internal_config: InternalDivRem, - remainder: UInt, - inter_mul_value: UInt, - is_zero: IsZeroConfig, - pub remainder_lt: IsLtConfig, + is_divisor_zero: IsZeroConfig, + is_remainder_lt_divisor: IsLtConfig, + + r_insn: RInstructionConfig, +} + +enum InternalDivRem { + Unsigned, + Signed { + dividend_signed: Signed, + divisor_signed: Signed, + quotient_signed: Signed, + remainder_signed: Signed, + negative_division: WitIn, + is_dividend_max_negative: IsEqualConfig, + is_divisor_minus_one: IsEqualConfig, + is_signed_overflow: WitIn, + remainder_nonnegative: AssertLtConfig, + }, } pub struct ArithInstruction(PhantomData<(E, I)>); -pub struct DivOp; -impl RIVInstruction for DivOp { - const INST_KIND: InsnKind = InsnKind::DIV; +pub struct DivuOp; +impl RIVInstruction for DivuOp { + const INST_KIND: InsnKind = InsnKind::DIVU; } -pub type DivDummy = DummyInstruction; // TODO: implement DivInstruction. +pub type DivuInstruction = ArithInstruction; -pub struct DivUOp; -impl RIVInstruction for DivUOp { - const INST_KIND: InsnKind = InsnKind::DIVU; +pub struct RemuOp; +impl RIVInstruction for RemuOp { + const INST_KIND: InsnKind = InsnKind::REMU; } -pub type DivUInstruction = ArithInstruction; +pub type RemuInstruction = ArithInstruction; pub struct RemOp; impl RIVInstruction for RemOp { const INST_KIND: InsnKind = InsnKind::REM; } -pub type RemDummy = DummyInstruction; // TODO: implement RemInstruction. +pub type RemInstruction = ArithInstruction; -pub struct RemuOp; -impl RIVInstruction for RemuOp { - const INST_KIND: InsnKind = InsnKind::REMU; +pub struct DivOp; +impl RIVInstruction for DivOp { + const INST_KIND: InsnKind = InsnKind::DIV; } -pub type RemuDummy = DummyInstruction; // TODO: implement RemuInstruction. +pub type DivInstruction = ArithInstruction; impl Instruction for ArithInstruction { - type InstructionConfig = ArithConfig; + type InstructionConfig = DivRemConfig; fn name() -> String { format!("{:?}", I::INST_KIND) } fn construct_circuit(cb: &mut CircuitBuilder) -> Result { - // outcome = dividend / divisor + remainder => dividend = divisor * outcome + r - let mut divisor = UInt::new_unchecked(|| "divisor", cb)?; - let mut outcome = UInt::new(|| "outcome", cb)?; - let r = UInt::new(|| "remainder", cb)?; - let (dividend, inter_mul_value) = - divisor.mul_add(|| "divisor * outcome + r", cb, &mut outcome, &r, true)?; - - // div by zero check - let is_zero = - IsZeroConfig::construct_circuit(cb, || "divisor_zero_check", divisor.value())?; - let outcome_value = outcome.value(); + // The soundness analysis for these constraints is only valid for + // 32-bit registers represented over the Goldilocks field, so verify + // these parameters + assert_eq!(UInt::::TOTAL_BITS, u32::BITS as usize); + assert_eq!(E::BaseField::MODULUS_U64, goldilocks::MODULUS); + + // 32-bit value from rs1 + let dividend = UInt::new_unchecked(|| "dividend", cb)?; + // 32-bit value from rs2 + let divisor = UInt::new_unchecked(|| "divisor", cb)?; + let quotient = UInt::new(|| "quotient", cb)?; + let remainder = UInt::new(|| "remainder", cb)?; + + // `rem_e` and `div_e` are expressions representing the remainder and + // divisor from the signed or unsigned division operation, with signs + // normalized to be nonnegative, so that correct values must satisfy + // either `0 <= rem_e < div_e` or `div_e == 0`. The `rem_e` value + // should be constrained to be nonnegative before being returned from + // this block, while the checks `rem_e < div_e` or `div_e == 0` are + // done later. + let (internal_config, rem_e, div_e) = match I::INST_KIND { + InsnKind::DIVU | InsnKind::REMU => { + cb.require_equal( + || "unsigned_division_relation", + dividend.value(), + divisor.value() * quotient.value() + remainder.value(), + )?; + + (InternalDivRem::Unsigned, remainder.value(), divisor.value()) + } + + InsnKind::DIV | InsnKind::REM => { + let dividend_signed = + Signed::construct_circuit(cb, || "dividend_signed", ÷nd)?; + let divisor_signed = Signed::construct_circuit(cb, || "divisor_signed", &divisor)?; + let quotient_signed = + Signed::construct_circuit(cb, || "quotient_signed", "ient)?; + let remainder_signed = + Signed::construct_circuit(cb, || "remainder_signed", &remainder)?; + + // The quotient and remainder can be interpreted as non-positive + // values when exactly one of dividend and divisor is negative + let neg_div_expr = { + let a_neg = dividend_signed.is_negative.expr(); + let b_neg = divisor_signed.is_negative.expr(); + // a_neg xor b_neg + &a_neg + &b_neg - 2 * a_neg * b_neg + }; + let negative_division = cb.flatten_expr(|| "neg_division", neg_div_expr)?; + + // Check for signed division overflow: i32::MIN / -1 + let is_dividend_max_negative = IsEqualConfig::construct_circuit( + cb, + || "is_dividend_max_negative", + dividend.value(), + i32::MIN.into(), + )?; + let is_divisor_minus_one = IsEqualConfig::construct_circuit( + cb, + || "is_divisor_minus_one", + divisor.value(), + (-1i32).into(), + )?; + let is_signed_overflow = cb.flatten_expr( + || "signed_division_overflow", + is_dividend_max_negative.expr() * is_divisor_minus_one.expr(), + )?; + + // For signed division overflow, dividend = -2^31 and divisor + // = -1, so that quotient = 2^31 would be required for proper + // arithmetic, which is too large for signed 32-bit values. In + // this case, quotient and remainder are required to be set to + // -2^31 and 0 respectively. These values are assured by the + // constraints + // + // 2^31 = divisor * quotient + remainder + // 0 <= |remainder| < |divisor| + // + // The second condition is the same inequality as required when + // there is no overflow, so no special handling is needed. The + // first condition is only different from the proper value in + // the left side of the equality, which can be controlled by a + // conditional equality constraint using fixed dividend value + // +2^31 in the signed overflow case. + let div_rel_expr = + quotient_signed.expr() * divisor_signed.expr() + remainder_signed.expr(); + cb.condition_require_equal( + || "signed_division_relation", + is_signed_overflow.expr(), + div_rel_expr, + // overflow replacement dividend value, +2^31 + (1u64 << 31).into(), + dividend_signed.expr(), + )?; + + // Check required inequalities for remainder value; change sign + // for remainder and divisor so that checked inequality is the + // usual unsigned one, 0 <= remainder < divisor + let remainder_pos_orientation: Expression = + (1 - 2 * negative_division.expr()) * remainder_signed.expr(); + let divisor_pos_orientation = + (1 - 2 * divisor_signed.is_negative.expr()) * divisor_signed.expr(); + + let remainder_nonnegative = AssertLtConfig::construct_circuit( + cb, + || "oriented_remainder_nonnegative", + (-1).into(), + remainder_pos_orientation.clone(), + UINT_LIMBS, + )?; + + ( + InternalDivRem::Signed { + dividend_signed, + divisor_signed, + quotient_signed, + remainder_signed, + negative_division, + is_dividend_max_negative, + is_divisor_minus_one, + is_signed_overflow, + remainder_nonnegative, + }, + remainder_pos_orientation, + divisor_pos_orientation, + ) + } + + _ => unreachable!("Unsupported instruction kind"), + }; + + let is_divisor_zero = + IsZeroConfig::construct_circuit(cb, || "is_divisor_zero", divisor.value())?; + + // For zero division, quotient must be the "all ones" register for both + // unsigned and signed cases, representing 2^32-1 and -1 respectively. cb.condition_require_equal( - || "outcome_is_zero", - is_zero.expr(), - outcome_value.clone(), - ((1u64 << UInt::::TOTAL_BITS) - 1).into(), - outcome_value, + || "quotient_zero_division", + is_divisor_zero.expr(), + quotient.value(), + u32::MAX.into(), + quotient.value(), )?; - // remainder should be less than divisor if divisor != 0. - let lt = IsLtConfig::construct_circuit( + // Check whether the (suitably oriented) remainder is less than the + // (suitably oriented) divisor, where "suitably oriented" is subtle for + // the signed case, involving both signs and the constraints used for + // signed division overflow. + let is_remainder_lt_divisor = IsLtConfig::construct_circuit( cb, - || "remainder < divisor?", - r.value(), - divisor.value(), + || "is_remainder_lt_divisor", + rem_e, + div_e, UINT_LIMBS, )?; - // When divisor is zero, remainder is -1 implies "remainder > divisor" aka. lt.expr() == 0 - // otherwise lt.expr() == 1 + // When divisor is nonzero, (nonnegative) remainder must be less than + // divisor, but when divisor is zero, remainder can't be less than + // divisor; so require that exactly one of these is true, i.e. sum of + // bit expressions is equal to 1. cb.require_equal( - || "remainder < divisor when non-zero divisor", - is_zero.expr() + lt.expr(), - Expression::ONE, + || "remainder < divisor iff divisor nonzero", + is_divisor_zero.expr() + is_remainder_lt_divisor.expr(), + 1.into(), )?; + // TODO determine whether any optimizations are possible for getting + // just one of quotient or remainder + let rd_written_e = match I::INST_KIND { + InsnKind::DIVU | InsnKind::DIV => quotient.register_expr(), + InsnKind::REMU | InsnKind::REM => remainder.register_expr(), + _ => unreachable!("Unsupported instruction kind"), + }; let r_insn = RInstructionConfig::::construct_circuit( cb, I::INST_KIND, dividend.register_expr(), divisor.register_expr(), - outcome.register_expr(), + rd_written_e, )?; - Ok(ArithConfig { - r_insn, + Ok(DivRemConfig { dividend, divisor, - outcome, - remainder: r, - inter_mul_value, - is_zero, - remainder_lt: lt, + quotient, + remainder, + internal_config, + is_divisor_zero, + is_remainder_lt_divisor, + r_insn, }) } @@ -127,43 +352,122 @@ impl Instruction for ArithInstruction Result<(), ZKVMError> { - let rs1 = step.rs1().unwrap().value; - let rs2 = step.rs2().unwrap().value; - let rd = step.rd().unwrap().value.after; - - // dividend = divisor * outcome + r - let divisor = Value::new_unchecked(rs2); - let outcome = Value::new(rd, lkm); + // dividend = quotient * divisor + remainder + let dividend = step.rs1().unwrap().value; + let divisor = step.rs2().unwrap().value; + + let dividend_v = Value::new_unchecked(dividend); + let divisor_v = Value::new_unchecked(divisor); + + let (quotient, remainder) = match &config.internal_config { + InternalDivRem::Unsigned => ( + dividend.checked_div(divisor).unwrap_or(u32::MAX), + dividend.checked_rem(divisor).unwrap_or(dividend), + ), + InternalDivRem::Signed { .. } => { + let dividend = dividend as i32; + let divisor = divisor as i32; + + let (quotient, remainder) = if divisor == 0 { + (-1i32, dividend) + } else { + // these correctly handle signed division overflow + ( + dividend.wrapping_div(divisor), + dividend.wrapping_rem(divisor), + ) + }; + + (quotient as u32, remainder as u32) + } + }; - let r = Value::new(if rs2 == 0 { 0 } else { rs1 % rs2 }, lkm); + let quotient_v = Value::new(quotient, lkm); + let remainder_v = Value::new(remainder, lkm); + + let (rem_pos, div_pos) = match &config.internal_config { + InternalDivRem::Unsigned => (remainder, divisor), + InternalDivRem::Signed { + dividend_signed, + divisor_signed, + negative_division, + is_dividend_max_negative, + is_divisor_minus_one, + is_signed_overflow, + quotient_signed, + remainder_signed, + remainder_nonnegative, + } => { + let dividend = dividend as i32; + let divisor = divisor as i32; + let remainder = remainder as i32; + + dividend_signed.assign_instance(instance, lkm, ÷nd_v)?; + divisor_signed.assign_instance(instance, lkm, &divisor_v)?; + + let negative_division_b = (dividend < 0) ^ (divisor < 0); + set_val!(instance, negative_division, negative_division_b as u64); + + is_dividend_max_negative.assign_instance( + instance, + (dividend as u32 as u64).into(), + (i32::MIN as u32 as u64).into(), + )?; + is_divisor_minus_one.assign_instance( + instance, + (divisor as u32 as u64).into(), + (-1i32 as u32 as u64).into(), + )?; + + let signed_div_overflow_b = dividend == i32::MIN && divisor == -1i32; + set_val!(instance, is_signed_overflow, signed_div_overflow_b as u64); + + quotient_signed.assign_instance(instance, lkm, "ient_v)?; + remainder_signed.assign_instance(instance, lkm, &remainder_v)?; + + let negate_if = |b: bool, x: i32| if b { -(x as i64) } else { x as i64 }; + + let remainder_pos_orientation = negate_if(negative_division_b, remainder); + let divisor_pos_orientation = negate_if(divisor < 0, divisor); + + remainder_nonnegative.assign_instance( + instance, + lkm, + (-Goldilocks::ONE).to_canonical_u64(), + i64_to_base::(remainder_pos_orientation).to_canonical_u64(), + )?; + + ( + remainder_pos_orientation as u32, + divisor_pos_orientation as u32, + ) + } + }; - // assignment - config.r_insn.assign_instance(instance, lkm, step)?; - config - .divisor - .assign_limbs(instance, divisor.as_u16_limbs()); - config - .outcome - .assign_limbs(instance, outcome.as_u16_limbs()); + config.dividend.assign_value(instance, dividend_v); + config.divisor.assign_value(instance, divisor_v); + config.quotient.assign_value(instance, quotient_v); + config.remainder.assign_value(instance, remainder_v); - let (dividend, inter_mul_value) = divisor.mul_add(&outcome, &r, lkm, true); config - .inter_mul_value - .assign_mul_outcome(instance, lkm, &inter_mul_value)?; + .is_divisor_zero + .assign_instance(instance, (divisor as u64).into())?; + + config.is_remainder_lt_divisor.assign_instance( + instance, + lkm, + rem_pos as u64, + div_pos as u64, + )?; - config.dividend.assign_add_outcome(instance, ÷nd); - config.remainder.assign_limbs(instance, r.as_u16_limbs()); - config - .is_zero - .assign_instance(instance, divisor.as_u64().into())?; - config - .remainder_lt - .assign_instance(instance, lkm, r.as_u64(), divisor.as_u64())?; + config.r_insn.assign_instance(instance, lkm, step)?; Ok(()) } } +// TODO Tests + #[cfg(test)] mod test { @@ -179,7 +483,7 @@ mod test { circuit_builder::{CircuitBuilder, ConstraintSystem}, instructions::{ Instruction, - riscv::{constants::UInt, div::DivUInstruction}, + riscv::{constants::UInt, div::DivuInstruction}, }, scheme::mock_prover::{MOCK_PC_START, MockProver}, }; @@ -196,7 +500,7 @@ mod test { let config = cb .namespace( || format!("divu_({name})"), - |cb| Ok(DivUInstruction::construct_circuit(cb)), + |cb| Ok(DivuInstruction::construct_circuit(cb)), ) .unwrap() .unwrap(); @@ -210,7 +514,7 @@ mod test { let insn_code = encode_rv32(InsnKind::DIVU, 2, 3, 4, 0); // values assignment let (raw_witin, lkm) = - DivUInstruction::assign_instances(&config, cb.cs.num_witin as usize, vec![ + DivuInstruction::assign_instances(&config, cb.cs.num_witin as usize, vec![ StepRecord::new_r_instruction( 3, MOCK_PC_START, @@ -228,7 +532,7 @@ mod test { ); config - .outcome + .quotient .require_equal(|| "assert_outcome", &mut cb, &expected_rd_written) .unwrap(); @@ -259,7 +563,7 @@ mod test { } #[test] - fn test_opcode_divu_unstatisfied() { + fn test_opcode_divu_unsatisfied() { verify("assert_outcome", 10, 2, 3, false); } diff --git a/ceno_zkvm/src/instructions/riscv/mul.rs b/ceno_zkvm/src/instructions/riscv/mul.rs index 2214c437b..e98a5e8bb 100644 --- a/ceno_zkvm/src/instructions/riscv/mul.rs +++ b/ceno_zkvm/src/instructions/riscv/mul.rs @@ -78,7 +78,7 @@ //! the high limb uniquely represent the product values for unsigned/unsigned //! and signed/unsigned products. -use std::{fmt::Display, marker::PhantomData}; +use std::marker::PhantomData; use ceno_emul::{InsnKind, StepRecord}; use ff_ext::ExtensionField; @@ -88,7 +88,7 @@ use crate::{ circuit_builder::CircuitBuilder, error::ZKVMError, expression::Expression, - gadgets::{IsEqualConfig, SignedExtendConfig}, + gadgets::{IsEqualConfig, Signed}, instructions::{ Instruction, riscv::{ @@ -398,47 +398,6 @@ impl Instruction for MulhInstructionBas } } -/// Transform a value represented as a `UInt` into a `WitIn` containing its -/// corresponding signed value, interpreting the bits as a 2s-complement -/// encoding. Gadget allocates 2 `WitIn` values in total. -struct Signed { - pub is_negative: SignedExtendConfig, - val: Expression, -} - -impl Signed { - pub fn construct_circuit + Display + Clone, N: FnOnce() -> NR>( - cb: &mut CircuitBuilder, - name_fn: N, - unsigned_val: &UInt, - ) -> Result { - cb.namespace(name_fn, |cb| { - let is_negative = unsigned_val.is_negative(cb)?; - let val = unsigned_val.value() - (1u64 << BIT_WIDTH) * is_negative.expr(); - - Ok(Self { is_negative, val }) - }) - } - - pub fn assign_instance( - &self, - instance: &mut [E::BaseField], - lkm: &mut LkMultiplicity, - val: &Value, - ) -> Result { - self.is_negative.assign_instance( - instance, - lkm, - *val.as_u16_limbs().last().unwrap() as u64, - )?; - Ok(i32::from(val)) - } - - pub fn expr(&self) -> Expression { - self.val.clone() - } -} - #[cfg(test)] mod test { use ceno_emul::{Change, StepRecord, encode_rv32}; diff --git a/ceno_zkvm/src/instructions/riscv/rv32im.rs b/ceno_zkvm/src/instructions/riscv/rv32im.rs index a00d2c7e4..5d19255d7 100644 --- a/ceno_zkvm/src/instructions/riscv/rv32im.rs +++ b/ceno_zkvm/src/instructions/riscv/rv32im.rs @@ -7,7 +7,7 @@ use crate::{ branch::{ BeqInstruction, BgeInstruction, BgeuInstruction, BltInstruction, BneInstruction, }, - div::DivUInstruction, + div::{DivInstruction, DivuInstruction, RemInstruction, RemuInstruction}, logic::{AndInstruction, OrInstruction, XorInstruction}, logic_imm::{AndiInstruction, OriInstruction, XoriInstruction}, mul::MulhuInstruction, @@ -27,7 +27,6 @@ use ceno_emul::{ InsnKind::{self, *}, Platform, StepRecord, }; -use div::{DivDummy, RemDummy, RemuDummy}; use ecall::EcallDummy; use ff_ext::ExtensionField; use itertools::Itertools; @@ -61,7 +60,10 @@ pub struct Rv32imConfig { pub mulh_config: as Instruction>::InstructionConfig, pub mulhsu_config: as Instruction>::InstructionConfig, pub mulhu_config: as Instruction>::InstructionConfig, - pub divu_config: as Instruction>::InstructionConfig, + pub divu_config: as Instruction>::InstructionConfig, + pub remu_config: as Instruction>::InstructionConfig, + pub div_config: as Instruction>::InstructionConfig, + pub rem_config: as Instruction>::InstructionConfig, // ALU with imm pub addi_config: as Instruction>::InstructionConfig, @@ -128,7 +130,10 @@ impl Rv32imConfig { let mulh_config = cs.register_opcode_circuit::>(); let mulhsu_config = cs.register_opcode_circuit::>(); let mulhu_config = cs.register_opcode_circuit::>(); - let divu_config = cs.register_opcode_circuit::>(); + let divu_config = cs.register_opcode_circuit::>(); + let remu_config = cs.register_opcode_circuit::>(); + let div_config = cs.register_opcode_circuit::>(); + let rem_config = cs.register_opcode_circuit::>(); // alu with imm opcodes let addi_config = cs.register_opcode_circuit::>(); @@ -193,6 +198,9 @@ impl Rv32imConfig { mulhsu_config, mulhu_config, divu_config, + remu_config, + div_config, + rem_config, // alu with imm addi_config, andi_config, @@ -257,7 +265,10 @@ impl Rv32imConfig { fixed.register_opcode_circuit::>(cs); fixed.register_opcode_circuit::>(cs); fixed.register_opcode_circuit::>(cs); - fixed.register_opcode_circuit::>(cs); + fixed.register_opcode_circuit::>(cs); + fixed.register_opcode_circuit::>(cs); + fixed.register_opcode_circuit::>(cs); + fixed.register_opcode_circuit::>(cs); // alu with imm fixed.register_opcode_circuit::>(cs); fixed.register_opcode_circuit::>(cs); @@ -360,7 +371,10 @@ impl Rv32imConfig { assign_opcode!(MULH, MulhInstruction, mulh_config); assign_opcode!(MULHSU, MulhsuInstruction, mulhsu_config); assign_opcode!(MULHU, MulhuInstruction, mulhu_config); - assign_opcode!(DIVU, DivUInstruction, divu_config); + assign_opcode!(DIVU, DivuInstruction, divu_config); + assign_opcode!(REMU, RemuInstruction, remu_config); + assign_opcode!(DIV, DivInstruction, div_config); + assign_opcode!(REM, RemInstruction, rem_config); // alu with imm assign_opcode!(ADDI, AddiInstruction, addi_config); assign_opcode!(ANDI, AndiInstruction, andi_config); @@ -397,9 +411,7 @@ impl Rv32imConfig { assert_eq!( all_records.keys().cloned().collect::>(), // these are opcodes that haven't been implemented - [INVALID, DIV, REM, REMU, ECALL] - .into_iter() - .collect::>(), + [INVALID, ECALL].into_iter().collect::>(), ); Ok(GroupedSteps(all_records)) } @@ -429,23 +441,12 @@ pub struct GroupedSteps(BTreeMap>); /// Fake version of what is missing in Rv32imConfig, for some tests. pub struct DummyExtraConfig { ecall_config: as Instruction>::InstructionConfig, - div_config: as Instruction>::InstructionConfig, - rem_config: as Instruction>::InstructionConfig, - remu_config: as Instruction>::InstructionConfig, } impl DummyExtraConfig { pub fn construct_circuits(cs: &mut ZKVMConstraintSystem) -> Self { - let div_config = cs.register_opcode_circuit::>(); - let rem_config = cs.register_opcode_circuit::>(); - let remu_config = cs.register_opcode_circuit::>(); let ecall_config = cs.register_opcode_circuit::>(); - Self { - div_config, - rem_config, - remu_config, - ecall_config, - } + Self { ecall_config } } pub fn generate_fixed_traces( @@ -453,9 +454,6 @@ impl DummyExtraConfig { cs: &ZKVMConstraintSystem, fixed: &mut ZKVMFixedTraces, ) { - fixed.register_opcode_circuit::>(cs); - fixed.register_opcode_circuit::>(cs); - fixed.register_opcode_circuit::>(cs); fixed.register_opcode_circuit::>(cs); } @@ -477,9 +475,6 @@ impl DummyExtraConfig { }; } - assign_opcode!(DIV, DivDummy, div_config); - assign_opcode!(REM, RemDummy, rem_config); - assign_opcode!(REMU, RemuDummy, remu_config); assign_opcode!(ECALL, EcallDummy, ecall_config); let _ = steps.remove(&INVALID);