From 4fb46a4ccfeac9e29cc3a0724b7bf25467274177 Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Fri, 15 Nov 2024 11:31:24 -0700 Subject: [PATCH 01/37] Move `Signed` gadget from MULH opcode to `gadgets` submodule --- ceno_zkvm/src/gadgets/mod.rs | 2 + ceno_zkvm/src/gadgets/signed.rs | 57 ++++++++++++++++++++++++ ceno_zkvm/src/gadgets/signed_ext.rs | 9 +++- ceno_zkvm/src/instructions/riscv/mulh.rs | 54 ++-------------------- 4 files changed, 70 insertions(+), 52 deletions(-) create mode 100644 ceno_zkvm/src/gadgets/signed.rs diff --git a/ceno_zkvm/src/gadgets/mod.rs b/ceno_zkvm/src/gadgets/mod.rs index 60846581e..4e41801f0 100644 --- a/ceno_zkvm/src/gadgets/mod.rs +++ b/ceno_zkvm/src/gadgets/mod.rs @@ -2,6 +2,7 @@ mod div; mod is_lt; mod is_zero; mod signed_ext; +mod signed; pub use div::DivConfig; pub use is_lt::{ @@ -9,3 +10,4 @@ pub use is_lt::{ }; pub use is_zero::{IsEqualConfig, IsZeroConfig}; pub use signed_ext::SignedExtendConfig; +pub use signed::Signed; diff --git a/ceno_zkvm/src/gadgets/signed.rs b/ceno_zkvm/src/gadgets/signed.rs new file mode 100644 index 000000000..8de3ea745 --- /dev/null +++ b/ceno_zkvm/src/gadgets/signed.rs @@ -0,0 +1,57 @@ +use std::{fmt::Display, mem::MaybeUninit}; + +use ff_ext::ExtensionField; + +use crate::{ + Value, + circuit_builder::CircuitBuilder, + error::ZKVMError, + expression::Expression, + instructions::riscv::constants::{BIT_WIDTH, UInt}, + witness::LkMultiplicity, +}; + +use super::SignedExtendConfig; + +/// Interprets a `UInt` value as a 2s-complement signed value. +/// +/// Uses 1 `WitIn` to represent the MSB 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.value() - (1u64 << BIT_WIDTH) * is_negative.expr(); + + Ok(Self { is_negative, val }) + }) + } + + pub fn assign_instance( + &self, + instance: &mut [MaybeUninit], + lkm: &mut LkMultiplicity, + val: &Value, + ) -> Result { + self.is_negative.assign_instance( + instance, + lkm, + *val.as_u16_limbs().last().unwrap() as u64, + )?; + let signed_val = val.as_u32() as i32; + + Ok(signed_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 d1dc8ed62..cedabac4e 100644 --- a/ceno_zkvm/src/gadgets/signed_ext.rs +++ b/ceno_zkvm/src/gadgets/signed_ext.rs @@ -9,11 +9,16 @@ use crate::{ use ff_ext::ExtensionField; use std::{marker::PhantomData, mem::MaybeUninit}; +/// 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, diff --git a/ceno_zkvm/src/instructions/riscv/mulh.rs b/ceno_zkvm/src/instructions/riscv/mulh.rs index be467de8d..b740327c2 100644 --- a/ceno_zkvm/src/instructions/riscv/mulh.rs +++ b/ceno_zkvm/src/instructions/riscv/mulh.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,14 +88,11 @@ use crate::{ circuit_builder::CircuitBuilder, error::ZKVMError, expression::Expression, - gadgets::{IsEqualConfig, SignedExtendConfig}, + gadgets::{IsEqualConfig, Signed}, instructions::{ - Instruction, riscv::{ - RIVInstruction, - constants::{BIT_WIDTH, UInt}, - r_insn::RInstructionConfig, - }, + constants::{UInt, BIT_WIDTH}, r_insn::RInstructionConfig, RIVInstruction + }, Instruction }, uint::Value, utils::i64_to_base, @@ -349,49 +346,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 [MaybeUninit], - lkm: &mut LkMultiplicity, - val: &Value, - ) -> Result { - self.is_negative.assign_instance( - instance, - lkm, - *val.as_u16_limbs().last().unwrap() as u64, - )?; - let signed_val = val.as_u32() as i32; - - Ok(signed_val) - } - - pub fn expr(&self) -> Expression { - self.val.clone() - } -} - #[cfg(test)] mod test { use ceno_emul::{Change, StepRecord, encode_rv32}; From 2812c129c67d4342a06fd06dd4653cfbd1ef3887 Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Sun, 17 Nov 2024 13:21:21 -0700 Subject: [PATCH 02/37] Extend DIVU gadget implementation to support REMU/DIV/REM opcodes --- ceno_zkvm/src/gadgets/is_lt.rs | 1 + ceno_zkvm/src/instructions/riscv/divu.rs | 362 +++++++++++++++++------ 2 files changed, 279 insertions(+), 84 deletions(-) diff --git a/ceno_zkvm/src/gadgets/is_lt.rs b/ceno_zkvm/src/gadgets/is_lt.rs index 3885b7257..8a5ca6a65 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/instructions/riscv/divu.rs b/ceno_zkvm/src/instructions/riscv/divu.rs index 8d25f583f..4ca6063c5 100644 --- a/ceno_zkvm/src/instructions/riscv/divu.rs +++ b/ceno_zkvm/src/instructions/riscv/divu.rs @@ -1,35 +1,43 @@ use ceno_emul::{InsnKind, StepRecord}; use ff_ext::ExtensionField; +use goldilocks::SmallField; use super::{ - RIVInstruction, - constants::{UINT_LIMBS, UInt}, - dummy::DummyInstruction, - r_insn::RInstructionConfig, + constants::{UInt, BIT_WIDTH, UINT_LIMBS}, dummy::DummyInstruction, r_insn::RInstructionConfig, RIVInstruction }; use crate::{ - circuit_builder::CircuitBuilder, - error::ZKVMError, - expression::Expression, - gadgets::{IsLtConfig, IsZeroConfig}, - instructions::Instruction, - uint::Value, - witness::LkMultiplicity, + circuit_builder::CircuitBuilder, error::ZKVMError, expression::{Expression, ToExpr, WitIn}, gadgets::{AssertLTConfig, IsEqualConfig, IsLtConfig, IsZeroConfig, Signed}, instructions::Instruction, set_val, uint::Value, witness::LkMultiplicity }; use core::mem::MaybeUninit; 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, + negative_division: WitIn, + is_dividend_max_negative: IsEqualConfig, + is_divisor_minus_one: IsEqualConfig, + is_signed_overflow: WitIn, + quotient_signed: Signed, + remainder_signed: Signed, + remainder_nonnegative: AssertLTConfig, + }, } pub struct ArithInstruction(PhantomData<(E, I)>); @@ -58,113 +66,299 @@ impl RIVInstruction for RemuOp { } pub type RemuDummy = DummyInstruction; // TODO: implement RemuInstruction. +// dividend and divisor are always rs1 and rs2 respectively, this can be uniform +// unsigned values are as represented by UInts +// signed values should be interpreted as such (extra data in internal enum?) +// might be able to factor out all sign operations to the end + 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(); + // quotient = dividend / divisor + remainder + // => dividend = divisor * quotient + remainder + let dividend = UInt::new_unchecked(|| "dividend", cb)?; // 32-bit value from rs1 + let divisor = UInt::new_unchecked(|| "divisor", cb)?; // 32-bit value from rs2 + let quotient = UInt::new(|| "quotient", cb)?; + let remainder = UInt::new(|| "remainder", cb)?; + + // rem_e and div_e are expressions verified to be nonnegative, which + // must be validated as either 0 <= rem_e < div_e, or div_e == 0 with + // appropriate divide by zero outputs + let (internal_config, rem_e, div_e) = match I::INST_KIND { + InsnKind::DIVU | InsnKind::REMU => { + (InternalDivRem::Unsigned, remainder.value(), divisor.value()) + }, + + InsnKind::ADD | InsnKind::REM => { + let dividend_signed: Signed = Signed::construct_circuit(cb, || "dividend_signed", ÷nd)?; + let divisor_signed: Signed = Signed::construct_circuit(cb, || "divisor_signed", &divisor)?; + + // quotient and remainder can be interpreted as non-positive + // values when exactly one of dividend and divisor is negative + let neg_div_expr: Expression = { + let a_neg = dividend_signed.is_negative.expr(); + let b_neg = divisor_signed.is_negative.expr(); + // a_neg * (1 - b_neg) + (1 - a_neg) * b_neg + (a_neg.clone() + b_neg.clone()) - (Expression::::from(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(), + (1u64 << (BIT_WIDTH - 1)).into() + )?; + let is_divisor_minus_one = IsEqualConfig::construct_circuit( + cb, + || "is_divisor_minus_one", + divisor.value(), + ((1u64 << BIT_WIDTH) - 1).into() + )?; + let is_signed_overflow = cb.flatten_expr( + || "signed_division_overflow", + is_dividend_max_negative.expr() * is_divisor_minus_one.expr() + )?; + + let quotient_signed: Signed = Signed::construct_circuit(cb, || "quotient_signed", "ient)?; + let remainder_signed: Signed = Signed::construct_circuit(cb, || "remainder_signed", "ient)?; + + // For signed integer overflow, dividend side of division + // relation is set to a different value, +2^31, corresponding + // to the dividend we would need to satisfy the division + // relation with the required output quotient -2^31 and + // remainder 0 with the overflow divisor -1. The two distinct + // possibilities are handled with `condition_require_equal` + 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, +2^31 + (1u64 << (BIT_WIDTH - 1)).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::ONE - Expression::::from(2)*negative_division.expr()) * remainder_signed.expr(); + let divisor_pos_orientation = (Expression::ONE - Expression::::from(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, + negative_division, + is_dividend_max_negative, + is_divisor_minus_one, + is_signed_overflow, + quotient_signed, + remainder_signed, + remainder_nonnegative, + }, + remainder_pos_orientation, + divisor_pos_orientation) + } + + _ => unreachable!("Unsupported instruction kind"), + }; + + // For signed division overflow, dividend = -2^31, and divisor = -1, so + // that we would require quotient = 2^31 which is too large for signed + // 32-bit values. In this case, quotient and remainder must be set to + // -2^31 and 0 respectively. This is assured by the constraints + // + // 2^31 = divisor * quotient + remainder + // 0 <= remainder < divisor (positive) or divisor < remainder <= 0 (negative) + // + // The second condition is the same whether or not overflow occurs, and + // the first condition is only different from the usual value in the + // left side of the equality, which can be controlled by a conditional + // equality constraint. + // + // cb.condition_require_equal( + // || "division_signed_overflow", + // is_signed_overflow.expr(), + // div_rhs, + // (1u64 << (UInt::::TOTAL_BITS - 1)).into(), + // dividend.value(), + // ); + + 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(), + || "quotient_zero_division", + is_divisor_zero.expr(), + quotient.value(), ((1u64 << UInt::::TOTAL_BITS) - 1).into(), - outcome_value, + 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(), - UINT_LIMBS, + || "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, 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(), )?; + 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, }) } + // TODO rewrite assign_instance fn assign_instance( config: &Self::InstructionConfig, instance: &mut [MaybeUninit], lkm: &mut LkMultiplicity, step: &StepRecord, ) -> Result<(), ZKVMError> { - let rs1 = step.rs1().unwrap().value; - let rs2 = step.rs2().unwrap().value; - let rd = step.rd().unwrap().value.after; + // 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); + + config.dividend.assign_limbs(instance, dividend_v.as_u16_limbs()); + config.divisor.assign_limbs(instance, divisor_v.as_u16_limbs()); + + let (quotient, remainder) = match &config.internal_config { + InternalDivRem::Unsigned => { + if divisor == 0 { + (u32::MAX, dividend) + } else { + (dividend / divisor, dividend % divisor) + } + }, + InternalDivRem::Signed{ .. } => { + let dividend_s = dividend as i32; + let divisor_s = divisor as i32; + + let (quotient_s, remainder_s) = if divisor_s == 0 { + (-1i32, dividend_s) + } else { + // these correctly handle signed division overflow + (dividend_s.wrapping_div(divisor_s), dividend_s.wrapping_rem(divisor_s)) + }; + + (quotient_s as u32, remainder_s as u32) + } + }; - // dividend = divisor * outcome + r - let divisor = Value::new_unchecked(rs2); - let outcome = Value::new(rd, lkm); + let quotient_v = Value::new(quotient, lkm); + let remainder_v = Value::new(remainder, lkm); + + config.quotient.assign_limbs(instance, quotient_v.as_u16_limbs()); + config.remainder.assign_limbs(instance, remainder_v.as_u16_limbs()); + + 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_s = dividend as i32; + let divisor_s = divisor as i32; + let remainder_s = remainder as i32; + + dividend_signed.assign_instance(instance, lkm, ÷nd_v)?; + divisor_signed.assign_instance(instance, lkm, &divisor_v)?; + + let negative_division_b = (dividend_s < 0) ^ (divisor_s < 0); + set_val!(instance, negative_division, negative_division_b as u64); + + is_dividend_max_negative.assign_instance(instance, (dividend as u64).into(), ((i32::MIN as u32) as u64).into())?; + is_divisor_minus_one.assign_instance(instance, (divisor as u64).into(), ((-1i32 as u32) as u64).into())?; + + let signed_div_overflow_b = dividend_s == i32::MIN && divisor_s == -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 remainder_pos_orientation = if negative_division_b { -(remainder_s as i64) } else { remainder_s as i64 }; + let divisor_pos_orientation = if divisor_s < 0 { -(divisor_s as i64) } else { divisor_s as i64 }; + + remainder_nonnegative.assign_instance(instance, lkm, + ::MODULUS_U64.wrapping_add_signed(-1), + ::MODULUS_U64.wrapping_add_signed(remainder_pos_orientation))?; + + (remainder_pos_orientation as u32, divisor_pos_orientation as u32) + }, + }; - let r = Value::new(if rs2 == 0 { 0 } else { rs1 % rs2 }, lkm); + config.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)?; - // 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()); - - let (dividend, inter_mul_value) = divisor.mul_add(&outcome, &r, lkm, true); - config - .inter_mul_value - .assign_mul_outcome(instance, lkm, &inter_mul_value)?; - - 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())?; Ok(()) } } +// TODO Tests + #[cfg(test)] mod test { @@ -230,7 +424,7 @@ mod test { ); config - .outcome + .test .require_equal(|| "assert_outcome", &mut cb, &expected_rd_written) .unwrap(); From 6919ece09c7185a03cecc4900ad274fcbd500d53 Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Fri, 6 Dec 2024 13:36:02 -0700 Subject: [PATCH 03/37] Format updates --- ceno_zkvm/src/gadgets/mod.rs | 4 +- ceno_zkvm/src/instructions/riscv/divu.rs | 183 +++++++++++++++-------- ceno_zkvm/src/instructions/riscv/mulh.rs | 7 +- 3 files changed, 131 insertions(+), 63 deletions(-) diff --git a/ceno_zkvm/src/gadgets/mod.rs b/ceno_zkvm/src/gadgets/mod.rs index 4e41801f0..989fb479e 100644 --- a/ceno_zkvm/src/gadgets/mod.rs +++ b/ceno_zkvm/src/gadgets/mod.rs @@ -1,13 +1,13 @@ mod div; mod is_lt; mod is_zero; -mod signed_ext; mod signed; +mod signed_ext; pub use div::DivConfig; pub use is_lt::{ AssertLTConfig, AssertSignedLtConfig, InnerLtConfig, IsLtConfig, SignedLtConfig, cal_lt_diff, }; pub use is_zero::{IsEqualConfig, IsZeroConfig}; -pub use signed_ext::SignedExtendConfig; pub use signed::Signed; +pub use signed_ext::SignedExtendConfig; diff --git a/ceno_zkvm/src/instructions/riscv/divu.rs b/ceno_zkvm/src/instructions/riscv/divu.rs index 4ca6063c5..0346c50c7 100644 --- a/ceno_zkvm/src/instructions/riscv/divu.rs +++ b/ceno_zkvm/src/instructions/riscv/divu.rs @@ -3,10 +3,20 @@ use ff_ext::ExtensionField; use goldilocks::SmallField; use super::{ - constants::{UInt, BIT_WIDTH, UINT_LIMBS}, dummy::DummyInstruction, r_insn::RInstructionConfig, RIVInstruction + RIVInstruction, + constants::{BIT_WIDTH, UINT_LIMBS, UInt}, + dummy::DummyInstruction, + r_insn::RInstructionConfig, }; use crate::{ - circuit_builder::CircuitBuilder, error::ZKVMError, expression::{Expression, ToExpr, WitIn}, gadgets::{AssertLTConfig, IsEqualConfig, IsLtConfig, IsZeroConfig, Signed}, instructions::Instruction, set_val, uint::Value, witness::LkMultiplicity + circuit_builder::CircuitBuilder, + error::ZKVMError, + expression::{Expression, ToExpr, WitIn}, + gadgets::{AssertLTConfig, IsEqualConfig, IsLtConfig, IsZeroConfig, Signed}, + instructions::Instruction, + set_val, + uint::Value, + witness::LkMultiplicity, }; use core::mem::MaybeUninit; use std::marker::PhantomData; @@ -71,6 +81,10 @@ pub type RemuDummy = DummyInstruction; // TODO: implement RemuInst // signed values should be interpreted as such (extra data in internal enum?) // might be able to factor out all sign operations to the end +// TODO detailed documentation for signed case +// TODO assess whether any optimizations are possible for getting just one of +// quotient or remainder + impl Instruction for ArithInstruction { type InstructionConfig = DivRemConfig; @@ -92,11 +106,13 @@ impl Instruction for ArithInstruction { (InternalDivRem::Unsigned, remainder.value(), divisor.value()) - }, + } InsnKind::ADD | InsnKind::REM => { - let dividend_signed: Signed = Signed::construct_circuit(cb, || "dividend_signed", ÷nd)?; - let divisor_signed: Signed = Signed::construct_circuit(cb, || "divisor_signed", &divisor)?; + let dividend_signed: Signed = + Signed::construct_circuit(cb, || "dividend_signed", ÷nd)?; + let divisor_signed: Signed = + Signed::construct_circuit(cb, || "divisor_signed", &divisor)?; // quotient and remainder can be interpreted as non-positive // values when exactly one of dividend and divisor is negative @@ -113,21 +129,23 @@ impl Instruction for ArithInstruction = Signed::construct_circuit(cb, || "quotient_signed", "ient)?; - let remainder_signed: Signed = Signed::construct_circuit(cb, || "remainder_signed", "ient)?; + let quotient_signed: Signed = + Signed::construct_circuit(cb, || "quotient_signed", "ient)?; + let remainder_signed: Signed = + Signed::construct_circuit(cb, || "remainder_signed", "ient)?; // For signed integer overflow, dividend side of division // relation is set to a different value, +2^31, corresponding @@ -135,42 +153,50 @@ impl Instruction for ArithInstruction::from(2)*negative_division.expr()) * remainder_signed.expr(); - let divisor_pos_orientation = (Expression::ONE - Expression::::from(2)*divisor_signed.is_negative.expr()) * divisor_signed.expr(); + let remainder_pos_orientation = (Expression::ONE + - Expression::::from(2) * negative_division.expr()) + * remainder_signed.expr(); + let divisor_pos_orientation = (Expression::ONE + - Expression::::from(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 + UINT_LIMBS, )?; - (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, - }, - remainder_pos_orientation, - divisor_pos_orientation) + ( + 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, + }, + remainder_pos_orientation, + divisor_pos_orientation, + ) } _ => unreachable!("Unsupported instruction kind"), @@ -188,7 +214,7 @@ impl Instruction for ArithInstruction Instruction for ArithInstruction Instruction for ArithInstruction Instruction for ArithInstruction { quotient.register_expr() }, - InsnKind::REMU | InsnKind::REM => { remainder.register_expr() }, + InsnKind::DIVU | InsnKind::DIV => quotient.register_expr(), + InsnKind::REMU | InsnKind::REM => remainder.register_expr(), _ => unreachable!("Unsupported instruction kind"), }; let r_insn = RInstructionConfig::::construct_circuit( @@ -256,7 +283,6 @@ impl Instruction for ArithInstruction], @@ -270,8 +296,12 @@ impl Instruction for ArithInstruction { @@ -280,8 +310,8 @@ impl Instruction for ArithInstruction { + } + InternalDivRem::Signed { .. } => { let dividend_s = dividend as i32; let divisor_s = divisor as i32; @@ -289,7 +319,10 @@ impl Instruction for ArithInstruction Instruction for ArithInstruction { - (remainder, divisor) - } - InternalDivRem::Signed { + InternalDivRem::Unsigned => (remainder, divisor), + InternalDivRem::Signed { dividend_signed, divisor_signed, negative_division, @@ -315,8 +350,8 @@ impl Instruction for ArithInstruction - { + remainder_nonnegative, + } => { let dividend_s = dividend as i32; let divisor_s = divisor as i32; let remainder_s = remainder as i32; @@ -327,8 +362,16 @@ impl Instruction for ArithInstruction Instruction for ArithInstruction::MODULUS_U64.wrapping_add_signed(-1), - ::MODULUS_U64.wrapping_add_signed(remainder_pos_orientation))?; + ::MODULUS_U64 + .wrapping_add_signed(remainder_pos_orientation), + )?; - (remainder_pos_orientation as u32, divisor_pos_orientation as u32) - }, + ( + remainder_pos_orientation as u32, + divisor_pos_orientation as u32, + ) + } }; - config.is_divisor_zero.assign_instance(instance, (divisor as u64).into())?; + config + .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.is_remainder_lt_divisor.assign_instance( + instance, + lkm, + rem_pos as u64, + div_pos as u64, + )?; config.r_insn.assign_instance(instance, lkm, step)?; @@ -424,7 +489,7 @@ mod test { ); config - .test + .quotient .require_equal(|| "assert_outcome", &mut cb, &expected_rd_written) .unwrap(); @@ -456,7 +521,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/mulh.rs b/ceno_zkvm/src/instructions/riscv/mulh.rs index b740327c2..c60cc4377 100644 --- a/ceno_zkvm/src/instructions/riscv/mulh.rs +++ b/ceno_zkvm/src/instructions/riscv/mulh.rs @@ -90,9 +90,12 @@ use crate::{ expression::Expression, gadgets::{IsEqualConfig, Signed}, instructions::{ + Instruction, riscv::{ - constants::{UInt, BIT_WIDTH}, r_insn::RInstructionConfig, RIVInstruction - }, Instruction + RIVInstruction, + constants::{BIT_WIDTH, UInt}, + r_insn::RInstructionConfig, + }, }, uint::Value, utils::i64_to_base, From b9be2fc9ca5f13157baf673889be89387d601638 Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Sat, 7 Dec 2024 12:15:55 -0700 Subject: [PATCH 04/37] A few DIV opcode circuit fixes, documentation, and vm integration --- ceno_zkvm/src/instructions/riscv/divu.rs | 188 +++++++++++++-------- ceno_zkvm/src/instructions/riscv/rv32im.rs | 45 +++-- 2 files changed, 141 insertions(+), 92 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/divu.rs b/ceno_zkvm/src/instructions/riscv/divu.rs index 0346c50c7..b1551e8a4 100644 --- a/ceno_zkvm/src/instructions/riscv/divu.rs +++ b/ceno_zkvm/src/instructions/riscv/divu.rs @@ -5,7 +5,6 @@ use goldilocks::SmallField; use super::{ RIVInstruction, constants::{BIT_WIDTH, UINT_LIMBS, UInt}, - dummy::DummyInstruction, r_insn::RInstructionConfig, }; use crate::{ @@ -50,40 +49,96 @@ enum InternalDivRem { }, } +/// 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. Of particular note 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. 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. - -// dividend and divisor are always rs1 and rs2 respectively, this can be uniform -// unsigned values are as represented by UInts -// signed values should be interpreted as such (extra data in internal enum?) -// might be able to factor out all sign operations to the end - -// TODO detailed documentation for signed case -// TODO assess whether any optimizations are possible for getting just one of -// quotient or remainder +pub type DivInstruction = ArithInstruction; impl Instruction for ArithInstruction { type InstructionConfig = DivRemConfig; @@ -100,15 +155,21 @@ impl Instruction for ArithInstruction { + cb.require_equal( + || "unsigned_division_relation", + dividend.value(), + divisor.value() * quotient.value() + remainder.value(), + )?; + (InternalDivRem::Unsigned, remainder.value(), divisor.value()) } - InsnKind::ADD | InsnKind::REM => { + InsnKind::DIV | InsnKind::REM => { let dividend_signed: Signed = Signed::construct_circuit(cb, || "dividend_signed", ÷nd)?; let divisor_signed: Signed = @@ -124,7 +185,12 @@ impl Instruction for ArithInstruction = + Signed::construct_circuit(cb, || "quotient_signed", "ient)?; + let remainder_signed: Signed = + Signed::construct_circuit(cb, || "remainder_signed", "ient)?; + + // check for signed division overflow: i32::MIN / -1 let is_dividend_max_negative = IsEqualConfig::construct_circuit( cb, || "is_dividend_max_negative", @@ -142,24 +208,29 @@ impl Instruction for ArithInstruction = - Signed::construct_circuit(cb, || "quotient_signed", "ient)?; - let remainder_signed: Signed = - Signed::construct_circuit(cb, || "remainder_signed", "ient)?; - - // For signed integer overflow, dividend side of division - // relation is set to a different value, +2^31, corresponding - // to the dividend we would need to satisfy the division - // relation with the required output quotient -2^31 and - // remainder 0 with the overflow divisor -1. The two distinct - // possibilities are handled with `condition_require_equal` + // 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, +2^31 + // overflow replacement dividend value, +2^31 (1u64 << (BIT_WIDTH - 1)).into(), dividend_signed.expr(), )?; @@ -202,32 +273,11 @@ impl Instruction for ArithInstruction unreachable!("Unsupported instruction kind"), }; - // For signed division overflow, dividend = -2^31, and divisor = -1, so - // that we would require quotient = 2^31 which is too large for signed - // 32-bit values. In this case, quotient and remainder must be set to - // -2^31 and 0 respectively. This is assured by the constraints - // - // 2^31 = divisor * quotient + remainder - // 0 <= remainder < divisor (positive) or divisor < remainder <= 0 (negative) - // - // The second condition is the same whether or not overflow occurs, and - // the first condition is only different from the usual value in the - // left side of the equality, which can be controlled by a conditional - // equality constraint. - // - // cb.condition_require_equal( - // || "division_signed_overflow", - // is_signed_overflow.expr(), - // div_rhs, - // (1u64 << (UInt::::TOTAL_BITS - 1)).into(), - // dividend.value(), - // ); - 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 + // unsigned and signed cases, representing 2^32-1 and -1 respectively. cb.condition_require_equal( || "quotient_zero_division", is_divisor_zero.expr(), @@ -239,7 +289,7 @@ impl Instruction for ArithInstruction Instruction for ArithInstruction quotient.register_expr(), InsnKind::REMU | InsnKind::REM => remainder.register_expr(), @@ -440,7 +492,7 @@ mod test { circuit_builder::{CircuitBuilder, ConstraintSystem}, instructions::{ Instruction, - riscv::{constants::UInt, divu::DivUInstruction}, + riscv::{constants::UInt, divu::DivuInstruction}, }, scheme::mock_prover::{MOCK_PC_START, MockProver}, }; @@ -457,7 +509,7 @@ mod test { let config = cb .namespace( || format!("divu_({name})"), - |cb| Ok(DivUInstruction::construct_circuit(cb)), + |cb| Ok(DivuInstruction::construct_circuit(cb)), ) .unwrap() .unwrap(); @@ -471,7 +523,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, diff --git a/ceno_zkvm/src/instructions/riscv/rv32im.rs b/ceno_zkvm/src/instructions/riscv/rv32im.rs index b11cbfee5..be43abacf 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, }, - divu::DivUInstruction, + divu::{DivuInstruction, RemuInstruction, DivInstruction, RemInstruction}, logic::{AndInstruction, OrInstruction, XorInstruction}, logic_imm::{AndiInstruction, OriInstruction, XoriInstruction}, mul::MulhuInstruction, @@ -27,7 +27,6 @@ use ceno_emul::{ InsnKind::{self, *}, Platform, StepRecord, }; -use divu::{DivDummy, RemDummy, RemuDummy}; use ecall::EcallDummy; use ff_ext::ExtensionField; use itertools::Itertools; @@ -64,7 +63,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, @@ -133,7 +135,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::>(); @@ -200,6 +205,9 @@ impl Rv32imConfig { mulhsu_config, mulhu_config, divu_config, + remu_config, + div_config, + rem_config, // alu with imm addi_config, andi_config, @@ -266,7 +274,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); @@ -372,7 +383,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, divu_config); + assign_opcode!(DIV, DivInstruction, divu_config); + assign_opcode!(REM, RemInstruction, divu_config); // alu with imm assign_opcode!(ADDI, AddiInstruction, addi_config); assign_opcode!(ANDI, AndiInstruction, andi_config); @@ -444,23 +458,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( @@ -468,9 +471,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); } @@ -492,9 +492,6 @@ impl DummyExtraConfig { }; } - assign_opcode!(DIV, DivDummy, div_config); - assign_opcode!(REM, RemDummy, rem_config); - assign_opcode!(REMU, RemuDummy, remu_config); assign_opcode!(EANY, EcallDummy, ecall_config); let _ = steps.remove(&(INVALID as usize)); From 22bc22a9b25711c328d7b3a3c7031f355ca5fa9d Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Sat, 7 Dec 2024 12:26:56 -0700 Subject: [PATCH 05/37] Rename `divu.rs` to `div.rs` and add check for Goldilocks field --- ceno_zkvm/src/instructions/riscv.rs | 2 +- .../instructions/riscv/{divu.rs => div.rs} | 144 +++++++++--------- ceno_zkvm/src/instructions/riscv/rv32im.rs | 2 +- 3 files changed, 78 insertions(+), 70 deletions(-) rename ceno_zkvm/src/instructions/riscv/{divu.rs => div.rs} (84%) diff --git a/ceno_zkvm/src/instructions/riscv.rs b/ceno_zkvm/src/instructions/riscv.rs index 0c8272846..de0dfc771 100644 --- a/ceno_zkvm/src/instructions/riscv.rs +++ b/ceno_zkvm/src/instructions/riscv.rs @@ -11,7 +11,7 @@ pub mod arith_imm; pub mod branch; pub mod config; pub mod constants; -pub mod divu; +pub mod div; pub mod dummy; pub mod ecall; pub mod jump; diff --git a/ceno_zkvm/src/instructions/riscv/divu.rs b/ceno_zkvm/src/instructions/riscv/div.rs similarity index 84% rename from ceno_zkvm/src/instructions/riscv/divu.rs rename to ceno_zkvm/src/instructions/riscv/div.rs index b1551e8a4..2c6e13508 100644 --- a/ceno_zkvm/src/instructions/riscv/divu.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -1,3 +1,72 @@ +//! 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_ext::ExtensionField; use goldilocks::SmallField; @@ -49,71 +118,6 @@ enum InternalDivRem { }, } -/// 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. Of particular note 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. pub struct ArithInstruction(PhantomData<(E, I)>); pub struct DivuOp; @@ -148,8 +152,12 @@ impl Instruction for ArithInstruction) -> Result { - // quotient = dividend / divisor + remainder - // => dividend = divisor * quotient + remainder + // 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); + let dividend = UInt::new_unchecked(|| "dividend", cb)?; // 32-bit value from rs1 let divisor = UInt::new_unchecked(|| "divisor", cb)?; // 32-bit value from rs2 let quotient = UInt::new(|| "quotient", cb)?; @@ -492,7 +500,7 @@ mod test { circuit_builder::{CircuitBuilder, ConstraintSystem}, instructions::{ Instruction, - riscv::{constants::UInt, divu::DivuInstruction}, + riscv::{constants::UInt, div::DivuInstruction}, }, scheme::mock_prover::{MOCK_PC_START, MockProver}, }; diff --git a/ceno_zkvm/src/instructions/riscv/rv32im.rs b/ceno_zkvm/src/instructions/riscv/rv32im.rs index be43abacf..53ee269b9 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, }, - divu::{DivuInstruction, RemuInstruction, DivInstruction, RemInstruction}, + div::{DivuInstruction, RemuInstruction, DivInstruction, RemInstruction}, logic::{AndInstruction, OrInstruction, XorInstruction}, logic_imm::{AndiInstruction, OriInstruction, XoriInstruction}, mul::MulhuInstruction, From 4c11b43115e824d7e2bdbb7bb78591a21415d7a7 Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Sat, 7 Dec 2024 13:12:15 -0700 Subject: [PATCH 06/37] Small reformatting and doc improvements --- ceno_zkvm/src/instructions/riscv/div.rs | 33 ++++++++++++++----------- 1 file changed, 18 insertions(+), 15 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index 2c6e13508..a81c4af3a 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -108,12 +108,12 @@ enum InternalDivRem { 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, - quotient_signed: Signed, - remainder_signed: Signed, remainder_nonnegative: AssertLTConfig, }, } @@ -157,15 +157,19 @@ impl Instruction for ArithInstruction::TOTAL_BITS, u32::BITS as usize); assert_eq!(E::BaseField::MODULUS_U64, goldilocks::MODULUS); - + let dividend = UInt::new_unchecked(|| "dividend", cb)?; // 32-bit value from rs1 let divisor = UInt::new_unchecked(|| "divisor", cb)?; // 32-bit value from rs2 let quotient = UInt::new(|| "quotient", cb)?; let remainder = UInt::new(|| "remainder", cb)?; - // `rem_e` and `div_e` are expressions verified to be nonnegative, which - // must be validated as either 0 <= rem_e < div_e, or div_e == 0 with - // appropriate divide by zero outputs + // `rem_e` and `div_e` are expressions representing the remainder and + // divisor from the signed or unsigned division operation, with signs + // renormalized 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( @@ -182,8 +186,12 @@ impl Instruction for ArithInstruction = Signed::construct_circuit(cb, || "divisor_signed", &divisor)?; + let quotient_signed: Signed = + Signed::construct_circuit(cb, || "quotient_signed", "ient)?; + let remainder_signed: Signed = + Signed::construct_circuit(cb, || "remainder_signed", "ient)?; - // quotient and remainder can be interpreted as non-positive + // The quotient and remainder can be interpreted as non-positive // values when exactly one of dividend and divisor is negative let neg_div_expr: Expression = { let a_neg = dividend_signed.is_negative.expr(); @@ -193,12 +201,7 @@ impl Instruction for ArithInstruction = - Signed::construct_circuit(cb, || "quotient_signed", "ient)?; - let remainder_signed: Signed = - Signed::construct_circuit(cb, || "remainder_signed", "ient)?; - - // check for signed division overflow: i32::MIN / -1 + // Check for signed division overflow: i32::MIN / -1 let is_dividend_max_negative = IsEqualConfig::construct_circuit( cb, || "is_dividend_max_negative", @@ -265,12 +268,12 @@ impl Instruction for ArithInstruction Date: Tue, 10 Dec 2024 09:38:36 -0700 Subject: [PATCH 07/37] Formatting fix --- ceno_zkvm/src/instructions/riscv/rv32im.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ceno_zkvm/src/instructions/riscv/rv32im.rs b/ceno_zkvm/src/instructions/riscv/rv32im.rs index 53ee269b9..c2c308d7e 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, RemuInstruction, DivInstruction, RemInstruction}, + div::{DivInstruction, DivuInstruction, RemInstruction, RemuInstruction}, logic::{AndInstruction, OrInstruction, XorInstruction}, logic_imm::{AndiInstruction, OriInstruction, XoriInstruction}, mul::MulhuInstruction, From 3e7931b3e9a45d054a48f0e8d093bef847e44184 Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Tue, 10 Dec 2024 10:10:48 -0700 Subject: [PATCH 08/37] Fix a couple of missed changes in rv32im.rs needed for new opcodes --- ceno_zkvm/src/instructions/riscv/rv32im.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/rv32im.rs b/ceno_zkvm/src/instructions/riscv/rv32im.rs index c2c308d7e..dd3f559c4 100644 --- a/ceno_zkvm/src/instructions/riscv/rv32im.rs +++ b/ceno_zkvm/src/instructions/riscv/rv32im.rs @@ -384,9 +384,9 @@ impl Rv32imConfig { assign_opcode!(MULHSU, MulhsuInstruction, mulhsu_config); assign_opcode!(MULHU, MulhuInstruction, mulhu_config); assign_opcode!(DIVU, DivuInstruction, divu_config); - assign_opcode!(REMU, RemuInstruction, divu_config); - assign_opcode!(DIV, DivInstruction, divu_config); - assign_opcode!(REM, RemInstruction, 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); @@ -425,7 +425,7 @@ impl Rv32imConfig { assert_eq!( all_records.keys().cloned().collect::>(), // these are opcodes that haven't been implemented - [INVALID, DIV, REM, REMU, EANY] + [INVALID, EANY] .into_iter() .map(|insn_kind| insn_kind as usize) .collect::>(), From 7821de4c7e1781eba04cc311843aa388cf0d7643 Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Wed, 11 Dec 2024 07:39:31 -0700 Subject: [PATCH 09/37] Fix bug in signed remainder construction --- ceno_zkvm/src/instructions/riscv/div.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index a81c4af3a..757c98467 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -189,7 +189,7 @@ impl Instruction for ArithInstruction = Signed::construct_circuit(cb, || "quotient_signed", "ient)?; let remainder_signed: Signed = - Signed::construct_circuit(cb, || "remainder_signed", "ient)?; + 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 From 23e6421cd04d95d1cc1678f7f1f8abda3e7ef32f Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Wed, 11 Dec 2024 07:57:55 -0700 Subject: [PATCH 10/37] Small comment fixes --- ceno_zkvm/src/gadgets/signed.rs | 2 +- ceno_zkvm/src/gadgets/signed_ext.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/ceno_zkvm/src/gadgets/signed.rs b/ceno_zkvm/src/gadgets/signed.rs index 8de3ea745..9d7e8c413 100644 --- a/ceno_zkvm/src/gadgets/signed.rs +++ b/ceno_zkvm/src/gadgets/signed.rs @@ -15,7 +15,7 @@ use super::SignedExtendConfig; /// Interprets a `UInt` value as a 2s-complement signed value. /// -/// Uses 1 `WitIn` to represent the MSB of the value. +/// Uses 1 `WitIn` to represent the most sigificant bit of the value. pub struct Signed { pub is_negative: SignedExtendConfig, val: Expression, diff --git a/ceno_zkvm/src/gadgets/signed_ext.rs b/ceno_zkvm/src/gadgets/signed_ext.rs index cedabac4e..2fee03f38 100644 --- a/ceno_zkvm/src/gadgets/signed_ext.rs +++ b/ceno_zkvm/src/gadgets/signed_ext.rs @@ -10,7 +10,7 @@ use ff_ext::ExtensionField; use std::{marker::PhantomData, mem::MaybeUninit}; /// Extract the most significant bit from an expression previously constrained -/// to an 8- or 16-bit length. +/// 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. From eb0a117bcb5c365cb19f5535ec7d1f7253a4075e Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Wed, 11 Dec 2024 08:10:54 -0700 Subject: [PATCH 11/37] Update UInt assignment in DIV opcodes to use assign_value function --- ceno_zkvm/src/instructions/riscv/div.rs | 27 ++++++++++++------------- 1 file changed, 13 insertions(+), 14 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index 757c98467..79cc1ee59 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -359,13 +359,6 @@ impl Instruction for ArithInstruction { if divisor == 0 { @@ -395,13 +388,6 @@ impl Instruction for ArithInstruction (remainder, divisor), InternalDivRem::Signed { @@ -468,6 +454,19 @@ impl Instruction for ArithInstruction Date: Wed, 11 Dec 2024 08:17:07 -0700 Subject: [PATCH 12/37] Replace constants using UInt BIT_WIDTH with hard-coded values in DIV opcodes The current implementation tries to be generic over different UInt widths, but the circuit design soundness relies on specifically using 32-bit registers in the Goldilocks field, so it doesn't make sense to sacrifice readability for unused generality here. --- ceno_zkvm/src/instructions/riscv/div.rs | 24 ++++++++---------------- 1 file changed, 8 insertions(+), 16 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index 79cc1ee59..2481a7c12 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -73,7 +73,7 @@ use goldilocks::SmallField; use super::{ RIVInstruction, - constants::{BIT_WIDTH, UINT_LIMBS, UInt}, + constants::{UINT_LIMBS, UInt}, r_insn::RInstructionConfig, }; use crate::{ @@ -206,13 +206,13 @@ impl Instruction for ArithInstruction Instruction for ArithInstruction Instruction for ArithInstruction Date: Wed, 11 Dec 2024 08:31:17 -0700 Subject: [PATCH 13/37] Change unnecessary generic constant with hard-coded value for readability --- ceno_zkvm/src/instructions/riscv/div.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index 2481a7c12..3ea6af8dc 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -293,7 +293,7 @@ impl Instruction for ArithInstruction::TOTAL_BITS) - 1).into(), + u32::MAX.into(), quotient.value(), )?; From 54bf10c4a3d444156610ff3cfcd16b7029956def Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Wed, 11 Dec 2024 09:09:22 -0700 Subject: [PATCH 14/37] Change Signed circuit to use bit shift directly on expression --- ceno_zkvm/src/gadgets/signed.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ceno_zkvm/src/gadgets/signed.rs b/ceno_zkvm/src/gadgets/signed.rs index 9d7e8c413..d582868f8 100644 --- a/ceno_zkvm/src/gadgets/signed.rs +++ b/ceno_zkvm/src/gadgets/signed.rs @@ -29,7 +29,7 @@ impl Signed { ) -> 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(); + let val = unsigned_val.value() - (is_negative.expr() << BIT_WIDTH); Ok(Self { is_negative, val }) }) From 92bce79345cf585680939d60aff616a07d7ee93d Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Wed, 11 Dec 2024 09:39:22 -0700 Subject: [PATCH 15/37] Small updates based on PR comments --- ceno_zkvm/src/instructions/riscv/div.rs | 29 ++++++++++--------------- 1 file changed, 12 insertions(+), 17 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index 3ea6af8dc..807a237c2 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -158,14 +158,16 @@ impl Instruction for ArithInstruction::TOTAL_BITS, u32::BITS as usize); assert_eq!(E::BaseField::MODULUS_U64, goldilocks::MODULUS); - let dividend = UInt::new_unchecked(|| "dividend", cb)?; // 32-bit value from rs1 - let divisor = UInt::new_unchecked(|| "divisor", cb)?; // 32-bit value from rs2 + // 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 - // renormalized to be nonnegative, so that correct values must satisfy + // 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 @@ -196,8 +198,7 @@ impl Instruction for ArithInstruction = { let a_neg = dividend_signed.is_negative.expr(); let b_neg = divisor_signed.is_negative.expr(); - // a_neg * (1 - b_neg) + (1 - a_neg) * b_neg - (a_neg.clone() + b_neg.clone()) - (Expression::::from(2) * a_neg * b_neg) + &a_neg * (1 - &b_neg) + (1 - &a_neg) * &b_neg }; let negative_division = cb.flatten_expr(|| "neg_division", neg_div_expr)?; @@ -414,12 +415,12 @@ impl Instruction for ArithInstruction Instruction for ArithInstruction Date: Wed, 11 Dec 2024 10:05:18 -0700 Subject: [PATCH 16/37] Fix assignment to remainder_nonnegative in DIV/REM opcodes circuit --- ceno_zkvm/src/instructions/riscv/div.rs | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index 807a237c2..c589e722b 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -68,8 +68,9 @@ //! 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::SmallField; +use goldilocks::{Goldilocks, SmallField}; use super::{ RIVInstruction, @@ -84,6 +85,7 @@ use crate::{ instructions::Instruction, set_val, uint::Value, + utils::i64_to_base, witness::LkMultiplicity, }; use core::mem::MaybeUninit; @@ -437,9 +439,8 @@ impl Instruction for ArithInstruction::MODULUS_U64.wrapping_add_signed(-1), - ::MODULUS_U64 - .wrapping_add_signed(remainder_pos_orientation), + (-Goldilocks::ONE).to_canonical_u64(), + i64_to_base::(remainder_pos_orientation).to_canonical_u64(), )?; ( From 0c3f5edbd492c4a7da6f9c52ed7e810063a9d330 Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Wed, 11 Dec 2024 10:16:46 -0700 Subject: [PATCH 17/37] Simplify syntax for a few Expression definitions --- ceno_zkvm/src/instructions/riscv/div.rs | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index c589e722b..47987e6d4 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -252,12 +252,10 @@ impl Instruction for ArithInstruction::from(2) * negative_division.expr()) - * remainder_signed.expr(); - let divisor_pos_orientation = (Expression::ONE - - Expression::::from(2) * divisor_signed.is_negative.expr()) - * divisor_signed.expr(); + 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, From 41e3e19476883ef0b43a9473975cc68ec434f0b0 Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Wed, 11 Dec 2024 10:21:37 -0700 Subject: [PATCH 18/37] Remove a few unnecessary type annotations --- ceno_zkvm/src/instructions/riscv/div.rs | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index 47987e6d4..4532ac470 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -186,18 +186,17 @@ impl Instruction for ArithInstruction { - let dividend_signed: Signed = + let dividend_signed = Signed::construct_circuit(cb, || "dividend_signed", ÷nd)?; - let divisor_signed: Signed = - Signed::construct_circuit(cb, || "divisor_signed", &divisor)?; - let quotient_signed: Signed = + let divisor_signed = Signed::construct_circuit(cb, || "divisor_signed", &divisor)?; + let quotient_signed = Signed::construct_circuit(cb, || "quotient_signed", "ient)?; - let remainder_signed: Signed = + 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: Expression = { + let neg_div_expr = { let a_neg = dividend_signed.is_negative.expr(); let b_neg = divisor_signed.is_negative.expr(); &a_neg * (1 - &b_neg) + (1 - &a_neg) * &b_neg From 137964a8625fe80f83c7f0efb204239a4dac9f9c Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Wed, 11 Dec 2024 10:31:48 -0700 Subject: [PATCH 19/37] Use built-in arithmetic calls for unsigned quotient/remainder computation --- ceno_zkvm/src/instructions/riscv/div.rs | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index 4532ac470..e1c3b610e 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -360,13 +360,10 @@ impl Instruction for ArithInstruction { - if divisor == 0 { - (u32::MAX, dividend) - } else { - (dividend / divisor, dividend % divisor) - } - } + InternalDivRem::Unsigned => ( + dividend.checked_div(divisor).unwrap_or(u32::MAX), + dividend.checked_rem(divisor).unwrap_or(dividend), + ), InternalDivRem::Signed { .. } => { let dividend_s = dividend as i32; let divisor_s = divisor as i32; From 0f71c30a9c781b8cb905bea93628dc83097672a3 Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Wed, 11 Dec 2024 10:42:16 -0700 Subject: [PATCH 20/37] Simplify variables in signed DIV/REM assignment by shadowing unsigned versions --- ceno_zkvm/src/instructions/riscv/div.rs | 32 ++++++++++++------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index e1c3b610e..9a0da7aca 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -365,20 +365,20 @@ impl Instruction for ArithInstruction { - let dividend_s = dividend as i32; - let divisor_s = divisor as i32; + let dividend = dividend as i32; + let divisor = divisor as i32; - let (quotient_s, remainder_s) = if divisor_s == 0 { - (-1i32, dividend_s) + let (quotient, remainder) = if divisor == 0 { + (-1i32, dividend) } else { // these correctly handle signed division overflow ( - dividend_s.wrapping_div(divisor_s), - dividend_s.wrapping_rem(divisor_s), + dividend.wrapping_div(divisor), + dividend.wrapping_rem(divisor), ) }; - (quotient_s as u32, remainder_s as u32) + (quotient as u32, remainder as u32) } }; @@ -398,28 +398,28 @@ impl Instruction for ArithInstruction { - let dividend_s = dividend as i32; - let divisor_s = divisor as i32; - let remainder_s = remainder as i32; + 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_s < 0) ^ (divisor_s < 0); + 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 u64).into(), + (dividend as u32 as u64).into(), (i32::MIN as u32 as u64).into(), )?; is_divisor_minus_one.assign_instance( instance, - (divisor as u64).into(), + (divisor as u32 as u64).into(), (-1i32 as u32 as u64).into(), )?; - let signed_div_overflow_b = dividend_s == i32::MIN && divisor_s == -1i32; + 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)?; @@ -427,8 +427,8 @@ impl Instruction for ArithInstruction Date: Wed, 11 Dec 2024 10:51:14 -0700 Subject: [PATCH 21/37] Use parameter for limb size in SignedExtendConfig rather than hard-coded value The current assumption of the circuit design is that n_bits has to be 8 or 16, so this change will better flag violations of this assumption if we end up changing the base limb size to 32 bits. --- ceno_zkvm/src/gadgets/signed_ext.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ceno_zkvm/src/gadgets/signed_ext.rs b/ceno_zkvm/src/gadgets/signed_ext.rs index 2fee03f38..55981999b 100644 --- a/ceno_zkvm/src/gadgets/signed_ext.rs +++ b/ceno_zkvm/src/gadgets/signed_ext.rs @@ -2,7 +2,7 @@ use crate::{ circuit_builder::CircuitBuilder, error::ZKVMError, expression::{Expression, ToExpr, WitIn}, - instructions::riscv::constants::UInt, + instructions::riscv::constants::{UInt, LIMB_BITS}, set_val, witness::LkMultiplicity, }; @@ -29,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( From 833dbca01cf50fe353a03b68e4bc0ffae19a4ec0 Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Wed, 11 Dec 2024 10:55:59 -0700 Subject: [PATCH 22/37] Revise Signed val construction to use relevant UInt utility function --- ceno_zkvm/src/gadgets/signed.rs | 10 +++------- ceno_zkvm/src/gadgets/signed_ext.rs | 2 +- 2 files changed, 4 insertions(+), 8 deletions(-) diff --git a/ceno_zkvm/src/gadgets/signed.rs b/ceno_zkvm/src/gadgets/signed.rs index d582868f8..425a3d1ae 100644 --- a/ceno_zkvm/src/gadgets/signed.rs +++ b/ceno_zkvm/src/gadgets/signed.rs @@ -3,12 +3,8 @@ use std::{fmt::Display, mem::MaybeUninit}; use ff_ext::ExtensionField; use crate::{ - Value, - circuit_builder::CircuitBuilder, - error::ZKVMError, - expression::Expression, - instructions::riscv::constants::{BIT_WIDTH, UInt}, - witness::LkMultiplicity, + Value, circuit_builder::CircuitBuilder, error::ZKVMError, expression::Expression, + instructions::riscv::constants::UInt, witness::LkMultiplicity, }; use super::SignedExtendConfig; @@ -29,7 +25,7 @@ impl Signed { ) -> Result { cb.namespace(name_fn, |cb| { let is_negative = unsigned_val.is_negative(cb)?; - let val = unsigned_val.value() - (is_negative.expr() << BIT_WIDTH); + let val = unsigned_val.to_field_expr(is_negative.expr()); Ok(Self { is_negative, val }) }) diff --git a/ceno_zkvm/src/gadgets/signed_ext.rs b/ceno_zkvm/src/gadgets/signed_ext.rs index 55981999b..8656be716 100644 --- a/ceno_zkvm/src/gadgets/signed_ext.rs +++ b/ceno_zkvm/src/gadgets/signed_ext.rs @@ -2,7 +2,7 @@ use crate::{ circuit_builder::CircuitBuilder, error::ZKVMError, expression::{Expression, ToExpr, WitIn}, - instructions::riscv::constants::{UInt, LIMB_BITS}, + instructions::riscv::constants::{LIMB_BITS, UInt}, set_val, witness::LkMultiplicity, }; From e719763c09c8472f5d364775806d2da6b9c6b85c Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Fri, 13 Dec 2024 10:32:49 -0700 Subject: [PATCH 23/37] Change way that expression for `neg_div_expr` is written --- ceno_zkvm/src/instructions/riscv/div.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index 5437ed913..d7ed7ca31 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -198,7 +198,8 @@ impl Instruction for ArithInstruction Date: Mon, 16 Dec 2024 11:46:50 +0200 Subject: [PATCH 24/37] basic unit test + (as u32) change + signed LT --- ceno_zkvm/src/gadgets/is_lt.rs | 11 +++ ceno_zkvm/src/instructions/riscv/div.rs | 105 ++++++++++++++++++++++-- 2 files changed, 110 insertions(+), 6 deletions(-) diff --git a/ceno_zkvm/src/gadgets/is_lt.rs b/ceno_zkvm/src/gadgets/is_lt.rs index 8a5ca6a65..509409f20 100644 --- a/ceno_zkvm/src/gadgets/is_lt.rs +++ b/ceno_zkvm/src/gadgets/is_lt.rs @@ -61,6 +61,17 @@ impl AssertLTConfig { self.0.assign_instance(instance, lkm, lhs, rhs)?; Ok(()) } + + pub fn assign_instance_signed( + &self, + instance: &mut [MaybeUninit], + lkm: &mut LkMultiplicity, + lhs: i32, + rhs: i32, + ) -> Result<(), ZKVMError> { + self.0.assign_instance_signed(instance, lkm, lhs, rhs)?; + Ok(()) + } } #[derive(Debug, Clone)] diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index 9a0da7aca..445bebb08 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -208,13 +208,13 @@ impl Instruction for ArithInstruction Instruction for ArithInstruction(remainder_pos_orientation).to_canonical_u64(), + -1i32, + remainder_pos_orientation, )?; ( @@ -577,4 +579,95 @@ mod test { verify("random", a, b, a / b, true); } } + + mod div { + use crate::{ + Value, + circuit_builder::{CircuitBuilder, ConstraintSystem}, + instructions::{ + Instruction, + riscv::{ + constants::UInt, + div::{DivInstruction, DivuInstruction}, + }, + }, + scheme::mock_prover::{MOCK_PC_START, MockProver}, + }; + use ceno_emul::{Change, InsnKind, StepRecord, Word, encode_rv32}; + use goldilocks::GoldilocksExt2; + use itertools::Itertools; + use multilinear_extensions::mle::IntoMLEs; + use rand::Rng; + fn verify(name: &'static str, dividend: i32, divisor: i32, exp_outcome: i32, is_ok: bool) { + let mut cs = ConstraintSystem::::new(|| "riscv"); + let mut cb = CircuitBuilder::new(&mut cs); + let config = cb + .namespace( + || format!("div_({name})"), + |cb| Ok(DivInstruction::construct_circuit(cb)), + ) + .unwrap() + .unwrap(); + let outcome = if divisor == 0 { + -1i32 + } else if dividend == i32::MIN && divisor == -1 { + i32::MAX + } else { + dividend / divisor + }; + let insn_code = encode_rv32(InsnKind::DIV, 2, 3, 4, 0); + // values assignment + let (raw_witin, lkm) = + DivInstruction::assign_instances(&config, cb.cs.num_witin as usize, vec![ + StepRecord::new_r_instruction( + 3, + MOCK_PC_START, + insn_code, + dividend as u32, + divisor as u32, + Change::new(0, outcome as u32), + 0, + ), + ]) + .unwrap(); + let expected_rd_written = UInt::from_const_unchecked( + Value::new_unchecked(exp_outcome as u32) + .as_u16_limbs() + .to_vec(), + ); + config + .quotient + .require_equal(|| "assert_outcome", &mut cb, &expected_rd_written) + .unwrap(); + let expected_errors: &[_] = if is_ok { &[] } else { &[name] }; + MockProver::assert_with_expected_errors( + &cb, + &raw_witin + .de_interleaving() + .into_mles() + .into_iter() + .map(|v| v.into()) + .collect_vec(), + &[insn_code], + expected_errors, + None, + Some(lkm), + ); + } + #[test] + fn test_opcode_div() { + verify("basic", 10, 2, 5, true); + // verify("dividend < divisor", 10, 11, 0, true); + // verify("remainder", 11, 2, 5, true); + // verify("i32::MAX", i32::MAX, i32::MAX, 1, true); + // verify("div u32::MAX", 3, i32::MAX, 0, true); + // verify("i32::MAX div by 2", i32::MAX, 2, i32::MAX / 2, true); + // verify("mul with carries", 1202729773, 171818539, 7, true); + // verify("div by zero", 10, 0, -1, true); + } + #[test] + fn test_opcode_div_unsatisfied() { + verify("assert_outcome", 10, 2, 3, false); + } + } } From e0defad73e39016b874af80ec22e732261f92057 Mon Sep 17 00:00:00 2001 From: Mihai Date: Tue, 17 Dec 2024 13:13:47 +0200 Subject: [PATCH 25/37] extend test cases --- ceno_zkvm/src/instructions/riscv/div.rs | 34 ++++++++++++++++--------- 1 file changed, 22 insertions(+), 12 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index 445bebb08..92600f806 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -573,10 +573,12 @@ mod test { #[test] fn test_opcode_divu_random() { - let mut rng = rand::thread_rng(); - let a: u32 = rng.gen(); - let b: u32 = rng.gen_range(1..u32::MAX); - verify("random", a, b, a / b, true); + for i in 0..100 { + let mut rng = rand::thread_rng(); + let a: u32 = rng.gen(); + let b: u32 = rng.gen_range(1..u32::MAX); + verify("random", a, b, a / b, true); + } } } @@ -611,7 +613,7 @@ mod test { let outcome = if divisor == 0 { -1i32 } else if dividend == i32::MIN && divisor == -1 { - i32::MAX + i32::MIN } else { dividend / divisor }; @@ -635,6 +637,7 @@ mod test { .as_u16_limbs() .to_vec(), ); + config .quotient .require_equal(|| "assert_outcome", &mut cb, &expected_rd_written) @@ -657,13 +660,20 @@ mod test { #[test] fn test_opcode_div() { verify("basic", 10, 2, 5, true); - // verify("dividend < divisor", 10, 11, 0, true); - // verify("remainder", 11, 2, 5, true); - // verify("i32::MAX", i32::MAX, i32::MAX, 1, true); - // verify("div u32::MAX", 3, i32::MAX, 0, true); - // verify("i32::MAX div by 2", i32::MAX, 2, i32::MAX / 2, true); - // verify("mul with carries", 1202729773, 171818539, 7, true); - // verify("div by zero", 10, 0, -1, true); + verify("dividend < divisor", 10, 11, 0, true); + verify("non-zero remainder", 11, 2, 5, true); + verify("i32::MAX", i32::MAX, i32::MAX, 1, true); + verify("div u32::MAX", 7801, i32::MAX, 0, true); + verify("i32::MAX div by 2", i32::MAX, 2, i32::MAX / 2, true); + verify("mul with carries", 1202729773, 171818539, 7, true); + verify("div by zero", 10, 0, -1, true); + verify( + "i32::MIN div -1 (overflow case)", + i32::MIN, + -1, + i32::MIN, + true, + ); } #[test] fn test_opcode_div_unsatisfied() { From 89e85f8f6a336b7e3821c8d45b8d222c5c5266b3 Mon Sep 17 00:00:00 2001 From: Mihai Date: Tue, 17 Dec 2024 13:29:30 +0200 Subject: [PATCH 26/37] brute force some cases --- ceno_zkvm/src/instructions/riscv/div.rs | 41 +++++++++++++++++++++++-- 1 file changed, 38 insertions(+), 3 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index 92600f806..ed37f20ea 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -427,7 +427,7 @@ impl Instruction for ArithInstruction::new(|| "riscv"); let mut cb = CircuitBuilder::new(&mut cs); let config = cb @@ -676,7 +676,42 @@ mod test { ); } #[test] - fn test_opcode_div_unsatisfied() { + fn test_batch_div() { + let interesting = [ + i32::MIN, + i32::MAX, + 0, + -1, + 1, + 2, + 3, + 4, + 5, + 6, + 10, + (1 << 10), + (1 << 20), + // 1000, + // 10000000, + // 123456, + // 1234, + i32::MAX / 2, + i32::MIN / 2, + i32::MIN + 1, + i32::MAX - 1, + ]; + + for dividend in interesting { + for divisor in interesting { + let exp_outcome = if divisor == 0 { + -1i32 + } else { + dividend.wrapping_div(divisor) + }; + let name = format!("{}, {}, {}", dividend, divisor, exp_outcome); + verify(&name, dividend, divisor, exp_outcome, true); + } + } verify("assert_outcome", 10, 2, 3, false); } } From 2ca9a8322f243d7fbe5cb636117b270df387bd43 Mon Sep 17 00:00:00 2001 From: Mihai Date: Tue, 17 Dec 2024 15:39:07 +0200 Subject: [PATCH 27/37] change to remainder sign --- ceno_zkvm/src/instructions/riscv/div.rs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index ed37f20ea..4b3f88e91 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -252,7 +252,7 @@ impl Instruction for ArithInstruction = - (1 - 2 * negative_division.expr()) * remainder_signed.expr(); + (1 - 2 * dividend_signed.is_negative.expr()) * remainder_signed.expr(); let divisor_pos_orientation = (1 - 2 * divisor_signed.is_negative.expr()) * divisor_signed.expr(); @@ -429,7 +429,8 @@ impl Instruction for ArithInstruction Date: Tue, 17 Dec 2024 18:12:59 +0200 Subject: [PATCH 28/37] stash --- ceno_zkvm/src/instructions/riscv/div.rs | 81 ++++++++++++++----------- 1 file changed, 46 insertions(+), 35 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index 4b3f88e91..cb2916991 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -429,7 +429,7 @@ impl Instruction for ArithInstruction::new(|| "riscv"); let mut cb = CircuitBuilder::new(&mut cs); let config = cb @@ -508,6 +511,8 @@ mod test { ) .unwrap() .unwrap(); + let duration = start.elapsed(); + println!("Time elapsed in construct_circuit() is: {:?}", duration); let outcome = if divisor == 0 { u32::MAX @@ -541,6 +546,7 @@ mod test { .unwrap(); let expected_errors: &[_] = if is_ok { &[] } else { &[name] }; + let start = Instant::now(); MockProver::assert_with_expected_errors( &cb, &raw_witin @@ -554,6 +560,11 @@ mod test { None, Some(lkm), ); + let duration = start.elapsed(); + println!( + "Time elapsed in assert_with_expected_errors() is: {:?}", + duration + ); } #[test] fn test_opcode_divu() { @@ -601,7 +612,15 @@ mod test { use itertools::Itertools; use multilinear_extensions::mle::IntoMLEs; use rand::Rng; - fn verify(name: &str, dividend: i32, divisor: i32, exp_outcome: i32, is_ok: bool) { + use std::time::Instant; + fn verify( + name: &str, + dividend: i32, + divisor: i32, + exp_outcome: i32, + exp_remainder: i32, + is_ok: bool, + ) { let mut cs = ConstraintSystem::::new(|| "riscv"); let mut cb = CircuitBuilder::new(&mut cs); let config = cb @@ -660,60 +679,52 @@ mod test { } #[test] fn test_opcode_div() { - verify("basic", 10, 2, 5, true); - verify("dividend < divisor", 10, 11, 0, true); - verify("non-zero remainder", 11, 2, 5, true); - verify("i32::MAX", i32::MAX, i32::MAX, 1, true); - verify("div u32::MAX", 7801, i32::MAX, 0, true); - verify("i32::MAX div by 2", i32::MAX, 2, i32::MAX / 2, true); - verify("mul with carries", 1202729773, 171818539, 7, true); - verify("div by zero", 10, 0, -1, true); + verify("basic", 10, 2, 5, 0, true); + verify("dividend < divisor", 10, 11, 0, 0, true); + verify("non-zero remainder", 11, 2, 5, 0, true); + verify("i32::MAX", i32::MAX, i32::MAX, 1, 0, true); + verify("div u32::MAX", 7801, i32::MAX, 0, 0, true); + verify("i32::MAX div by 2", i32::MAX, 2, i32::MAX / 2, 0, true); + verify("mul with carries", 1202729773, 171818539, 7, 0, true); + verify("div by zero", 10, 0, -1, 0, true); verify( "i32::MIN div -1 (overflow case)", i32::MIN, -1, i32::MIN, + 0, true, ); } #[test] - fn test_batch_div() { - let interesting = [ + fn test_div_edges() { + let interesting_values = [ i32::MIN, i32::MAX, - 0, - -1, - 1, - 2, - 3, - 4, - 5, - 6, - 10, - (1 << 10), - (1 << 20), - // 1000, - // 10000000, - // 123456, - // 1234, i32::MAX / 2, i32::MIN / 2, i32::MIN + 1, i32::MAX - 1, + 0, + -1, + 1, + 2, ]; - for dividend in interesting { - for divisor in interesting { - let exp_outcome = if divisor == 0 { - -1i32 + for dividend in interesting_values { + for divisor in interesting_values { + let (exp_quotient, exp_remainder) = if divisor == 0 { + (-1i32, 0) } else { - dividend.wrapping_div(divisor) + ( + dividend.wrapping_div(divisor), + dividend.wrapping_rem(divisor), + ) }; - let name = format!("{}, {}, {}", dividend, divisor, exp_outcome); - verify(&name, dividend, divisor, exp_outcome, true); + let name = format!("expects {} / {}, = {}", dividend, divisor, exp_quotient); + verify(&name, dividend, divisor, exp_quotient, exp_remainder, true); } } - verify("assert_outcome", 10, 2, 3, false); } } } From 6d87fc0f3f00b0a55478a81e3b8595b2dc3be66c Mon Sep 17 00:00:00 2001 From: Mihai Date: Wed, 18 Dec 2024 10:35:35 +0200 Subject: [PATCH 29/37] refactor verify --- ceno_zkvm/src/instructions/riscv/div.rs | 160 ++++++++++++++---------- 1 file changed, 92 insertions(+), 68 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index 5558fb6d2..cb044329c 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -84,7 +84,7 @@ use crate::{ gadgets::{AssertLtConfig, IsEqualConfig, IsLtConfig, IsZeroConfig, Signed}, instructions::Instruction, set_val, - uint::Value, + uint::{UIntLimbs, Value}, utils::i64_to_base, witness::LkMultiplicity, }; @@ -111,7 +111,6 @@ enum InternalDivRem { 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, @@ -193,15 +192,6 @@ impl Instruction for ArithInstruction Instruction for ArithInstruction Instruction for ArithInstruction Instruction for ArithInstruction Instruction for ArithInstruction +where + Self: Instruction, +{ + fn output(config: Self::InstructionConfig) -> UInt; + fn correct(dividend: i32, divisor: i32) -> i32; +} + +impl TestOutput for DivInstruction { + fn output(config: DivRemConfig) -> UInt { + config.quotient + } + fn correct(dividend: i32, divisor: i32) -> i32 { + if divisor == 0 { + -1i32 + } else { + dividend.wrapping_div(divisor) + } + } +} + +impl TestOutput for RemInstruction { + fn output(config: DivRemConfig) -> UInt { + config.remainder + } + fn correct(dividend: i32, divisor: i32) -> i32 { + if divisor == 0 { + 0 + } else { + dividend.wrapping_rem(divisor) + } + } +} + // TODO Tests #[cfg(test)] @@ -599,23 +618,24 @@ mod test { Instruction, riscv::{ constants::UInt, - div::{DivInstruction, DivuInstruction}, + div::{DivInstruction, DivuInstruction, RemInstruction, TestOutput}, }, }, scheme::mock_prover::{MOCK_PC_START, MockProver}, }; use ceno_emul::{Change, InsnKind, StepRecord, Word, encode_rv32}; + use ff_ext::ExtensionField; use goldilocks::GoldilocksExt2; use itertools::Itertools; use multilinear_extensions::mle::IntoMLEs; use rand::Rng; use std::time::Instant; - fn verify( + + fn verify + TestOutput>( name: &str, dividend: i32, divisor: i32, exp_outcome: i32, - exp_remainder: i32, is_ok: bool, ) { let mut cs = ConstraintSystem::::new(|| "riscv"); @@ -623,42 +643,35 @@ mod test { let config = cb .namespace( || format!("div_({name})"), - |cb| Ok(DivInstruction::construct_circuit(cb)), + |cb| Ok(Insn::construct_circuit(cb)), ) .unwrap() .unwrap(); - let outcome = if divisor == 0 { - -1i32 - } else if dividend == i32::MIN && divisor == -1 { - i32::MIN - } else { - dividend / divisor - }; + let outcome = Insn::correct(dividend, divisor); let insn_code = encode_rv32(InsnKind::DIV, 2, 3, 4, 0); // values assignment - let (raw_witin, lkm) = - DivInstruction::assign_instances(&config, cb.cs.num_witin as usize, vec![ - StepRecord::new_r_instruction( - 3, - MOCK_PC_START, - insn_code, - dividend as u32, - divisor as u32, - Change::new(0, outcome as u32), - 0, - ), - ]) - .unwrap(); + let (raw_witin, lkm) = Insn::assign_instances(&config, cb.cs.num_witin as usize, vec![ + StepRecord::new_r_instruction( + 3, + MOCK_PC_START, + insn_code, + dividend as u32, + divisor as u32, + Change::new(0, outcome as u32), + 0, + ), + ]) + .unwrap(); let expected_rd_written = UInt::from_const_unchecked( Value::new_unchecked(exp_outcome as u32) .as_u16_limbs() .to_vec(), ); - config - .quotient + Insn::output(config) .require_equal(|| "assert_outcome", &mut cb, &expected_rd_written) .unwrap(); + let expected_errors: &[_] = if is_ok { &[] } else { &[name] }; MockProver::assert_with_expected_errors( &cb, @@ -673,27 +686,45 @@ mod test { Some(lkm), ); } + + type Div = DivInstruction; + type Rem = RemInstruction; #[test] - fn test_opcode_div() { - verify("basic", 10, 2, 5, 0, true); - verify("dividend < divisor", 10, 11, 0, 0, true); - verify("non-zero remainder", 11, 2, 5, 0, true); - verify("i32::MAX", i32::MAX, i32::MAX, 1, 0, true); - verify("div u32::MAX", 7801, i32::MAX, 0, 0, true); - verify("i32::MAX div by 2", i32::MAX, 2, i32::MAX / 2, 0, true); - verify("mul with carries", 1202729773, 171818539, 7, 0, true); - verify("div by zero", 10, 0, -1, 0, true); - verify( - "i32::MIN div -1 (overflow case)", - i32::MIN, - -1, - i32::MIN, - 0, + fn test_divrem() { + let test_cases = [ + ("basic", 10, 2), + ("dividend < divisor", 10, 11), + ("non-zero remainder", 11, 2), + ("i32::MAX", i32::MAX, i32::MAX), + ("div u32::MAX", 7801, i32::MAX), + ("i32::MAX div by 2", i32::MAX, 2), + ("mul with carries", 1202729773, 171818539), + ("div by zero", 10, 0), + ("i32::MIN div -1 (overflow case)", i32::MIN, -1), + ]; + + for (name, dividend, divisor) in test_cases.into_iter() { + verify_positive::
(name, dividend, divisor); + verify_positive::(name, dividend, divisor); + } + } + + fn verify_positive + TestOutput>( + name: &str, + dividend: i32, + divisor: i32, + ) { + verify::( + name, + dividend, + divisor, + Insn::correct(dividend, divisor), true, ); } + #[test] - fn test_div_edges() { + fn test_divrem_edges() { let interesting_values = [ i32::MIN, i32::MAX, @@ -709,16 +740,9 @@ mod test { for dividend in interesting_values { for divisor in interesting_values { - let (exp_quotient, exp_remainder) = if divisor == 0 { - (-1i32, 0) - } else { - ( - dividend.wrapping_div(divisor), - dividend.wrapping_rem(divisor), - ) - }; - let name = format!("expects {} / {}, = {}", dividend, divisor, exp_quotient); - verify(&name, dividend, divisor, exp_quotient, exp_remainder, true); + let name = format!("dividend = {}, divisor = {}", dividend, divisor); + verify_positive::
(&name, dividend, divisor); + verify_positive::(&name, dividend, divisor); } } } From f66ac9b692313f58f4830d6df4bfdb45cda84e90 Mon Sep 17 00:00:00 2001 From: Mihai Date: Wed, 18 Dec 2024 10:55:15 +0200 Subject: [PATCH 30/37] include rem tests --- ceno_zkvm/src/instructions/riscv/div.rs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index cb044329c..ec265fc0b 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -459,6 +459,7 @@ where { fn output(config: Self::InstructionConfig) -> UInt; fn correct(dividend: i32, divisor: i32) -> i32; + const INSN_KIND: InsnKind; } impl TestOutput for DivInstruction { @@ -472,6 +473,7 @@ impl TestOutput for DivInstruction { dividend.wrapping_div(divisor) } } + const INSN_KIND: InsnKind = InsnKind::DIV; } impl TestOutput for RemInstruction { @@ -480,11 +482,12 @@ impl TestOutput for RemInstruction { } fn correct(dividend: i32, divisor: i32) -> i32 { if divisor == 0 { - 0 + dividend } else { dividend.wrapping_rem(divisor) } } + const INSN_KIND: InsnKind = InsnKind::REM; } // TODO Tests @@ -617,6 +620,7 @@ mod test { instructions::{ Instruction, riscv::{ + arith::ArithConfig, constants::UInt, div::{DivInstruction, DivuInstruction, RemInstruction, TestOutput}, }, @@ -642,13 +646,13 @@ mod test { let mut cb = CircuitBuilder::new(&mut cs); let config = cb .namespace( - || format!("div_({name})"), + || format!("{}_({})", Insn::name(), name), |cb| Ok(Insn::construct_circuit(cb)), ) .unwrap() .unwrap(); let outcome = Insn::correct(dividend, divisor); - let insn_code = encode_rv32(InsnKind::DIV, 2, 3, 4, 0); + let insn_code = encode_rv32(Insn::INSN_KIND, 2, 3, 4, 0); // values assignment let (raw_witin, lkm) = Insn::assign_instances(&config, cb.cs.num_witin as usize, vec![ StepRecord::new_r_instruction( From f0128aa1d14b49fecf98462255004afcfda0003f Mon Sep 17 00:00:00 2001 From: Mihai Date: Wed, 18 Dec 2024 11:54:12 +0200 Subject: [PATCH 31/37] progress on tests --- ceno_zkvm/src/instructions/riscv/div.rs | 321 +++++++++++------------- 1 file changed, 153 insertions(+), 168 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index ec265fc0b..875b5bd0c 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -453,16 +453,22 @@ impl Instruction for ArithInstruction +trait TestInstance where Self: Instruction, { + type NumType: Copy; + fn as_u32(val: Self::NumType) -> u32; fn output(config: Self::InstructionConfig) -> UInt; - fn correct(dividend: i32, divisor: i32) -> i32; + fn correct(dividend: Self::NumType, divisor: Self::NumType) -> Self::NumType; const INSN_KIND: InsnKind; } -impl TestOutput for DivInstruction { +impl TestInstance for DivInstruction { + type NumType = i32; + fn as_u32(val: Self::NumType) -> u32 { + val as u32 + } fn output(config: DivRemConfig) -> UInt { config.quotient } @@ -476,7 +482,11 @@ impl TestOutput for DivInstruction { const INSN_KIND: InsnKind = InsnKind::DIV; } -impl TestOutput for RemInstruction { +impl TestInstance for RemInstruction { + type NumType = i32; + fn as_u32(val: Self::NumType) -> u32 { + val as u32 + } fn output(config: DivRemConfig) -> UInt { config.remainder } @@ -490,129 +500,46 @@ impl TestOutput for RemInstruction { const INSN_KIND: InsnKind = InsnKind::REM; } -// TODO Tests - -#[cfg(test)] -mod test { - - mod divu { - - use std::time::Instant; - - use ceno_emul::{Change, InsnKind, StepRecord, Word, encode_rv32}; - use goldilocks::GoldilocksExt2; - use itertools::Itertools; - use rand::Rng; - - use crate::{ - Value, - circuit_builder::{CircuitBuilder, ConstraintSystem}, - instructions::{ - Instruction, - riscv::{constants::UInt, div::DivuInstruction}, - }, - scheme::mock_prover::{MOCK_PC_START, MockProver}, - }; - - fn verify( - name: &'static str, - dividend: Word, - divisor: Word, - exp_outcome: Word, - is_ok: bool, - ) { - let start = Instant::now(); - let mut cs = ConstraintSystem::::new(|| "riscv"); - let mut cb = CircuitBuilder::new(&mut cs); - let config = cb - .namespace( - || format!("divu_({name})"), - |cb| Ok(DivuInstruction::construct_circuit(cb)), - ) - .unwrap() - .unwrap(); - let duration = start.elapsed(); - println!("Time elapsed in construct_circuit() is: {:?}", duration); - - let outcome = if divisor == 0 { - u32::MAX - } else { - dividend / divisor - }; - - 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![ - StepRecord::new_r_instruction( - 3, - MOCK_PC_START, - insn_code, - dividend, - divisor, - Change::new(0, outcome), - 0, - ), - ]) - .unwrap(); - - let expected_rd_written = UInt::from_const_unchecked( - Value::new_unchecked(exp_outcome).as_u16_limbs().to_vec(), - ); - - config - .quotient - .require_equal(|| "assert_outcome", &mut cb, &expected_rd_written) - .unwrap(); - - let expected_errors: &[_] = if is_ok { &[] } else { &[name] }; - let start = Instant::now(); - MockProver::assert_with_expected_errors( - &cb, - &raw_witin - .into_mles() - .into_iter() - .map(|v| v.into()) - .collect_vec(), - &[insn_code], - expected_errors, - None, - Some(lkm), - ); - let duration = start.elapsed(); - println!( - "Time elapsed in assert_with_expected_errors() is: {:?}", - duration - ); - } - #[test] - fn test_opcode_divu() { - verify("basic", 10, 2, 5, true); - verify("dividend > divisor", 10, 11, 0, true); - verify("remainder", 11, 2, 5, true); - verify("u32::MAX", u32::MAX, u32::MAX, 1, true); - verify("div u32::MAX", 3, u32::MAX, 0, true); - verify("u32::MAX div by 2", u32::MAX, 2, u32::MAX / 2, true); - verify("mul with carries", 1202729773, 171818539, 7, true); - verify("div by zero", 10, 0, u32::MAX, true); - } - - #[test] - fn test_opcode_divu_unsatisfied() { - verify("assert_outcome", 10, 2, 3, false); +impl TestInstance for DivuInstruction { + type NumType = u32; + fn as_u32(val: Self::NumType) -> u32 { + val as u32 + } + fn output(config: DivRemConfig) -> UInt { + config.quotient + } + fn correct(dividend: u32, divisor: u32) -> u32 { + if divisor == 0 { + u32::MAX + } else { + dividend / divisor } + } + const INSN_KIND: InsnKind = InsnKind::DIVU; +} - #[test] - fn test_opcode_divu_random() { - for i in 0..1 { - let mut rng = rand::thread_rng(); - let a: u32 = rng.gen(); - let b: u32 = rng.gen_range(1..u32::MAX); - verify("random", a, b, a / b, true); - } +impl TestInstance for RemuInstruction { + type NumType = u32; + fn as_u32(val: Self::NumType) -> u32 { + val as u32 + } + fn output(config: DivRemConfig) -> UInt { + config.remainder + } + fn correct(dividend: u32, divisor: u32) -> u32 { + if divisor == 0 { + dividend + } else { + dividend % divisor } } + const INSN_KIND: InsnKind = InsnKind::REMU; +} +// TODO Tests + +#[cfg(test)] +mod test { mod div { use crate::{ Value, @@ -622,7 +549,10 @@ mod test { riscv::{ arith::ArithConfig, constants::UInt, - div::{DivInstruction, DivuInstruction, RemInstruction, TestOutput}, + div::{ + DivInstruction, DivuInstruction, RemInstruction, RemuInstruction, + TestInstance, + }, }, }, scheme::mock_prover::{MOCK_PC_START, MockProver}, @@ -632,14 +562,17 @@ mod test { use goldilocks::GoldilocksExt2; use itertools::Itertools; use multilinear_extensions::mle::IntoMLEs; + use num_traits::Num; use rand::Rng; use std::time::Instant; - fn verify + TestOutput>( + type GE = GoldilocksExt2; + + fn verify + TestInstance>( name: &str, - dividend: i32, - divisor: i32, - exp_outcome: i32, + dividend: >::NumType, + divisor: >::NumType, + exp_outcome: >::NumType, is_ok: bool, ) { let mut cs = ConstraintSystem::::new(|| "riscv"); @@ -659,15 +592,15 @@ mod test { 3, MOCK_PC_START, insn_code, - dividend as u32, - divisor as u32, - Change::new(0, outcome as u32), + Insn::as_u32(dividend), + Insn::as_u32(divisor), + Change::new(0, Insn::as_u32(outcome)), 0, ), ]) .unwrap(); let expected_rd_written = UInt::from_const_unchecked( - Value::new_unchecked(exp_outcome as u32) + Value::new_unchecked(Insn::as_u32(exp_outcome)) .as_u16_limbs() .to_vec(), ); @@ -691,32 +624,11 @@ mod test { ); } - type Div = DivInstruction; - type Rem = RemInstruction; - #[test] - fn test_divrem() { - let test_cases = [ - ("basic", 10, 2), - ("dividend < divisor", 10, 11), - ("non-zero remainder", 11, 2), - ("i32::MAX", i32::MAX, i32::MAX), - ("div u32::MAX", 7801, i32::MAX), - ("i32::MAX div by 2", i32::MAX, 2), - ("mul with carries", 1202729773, 171818539), - ("div by zero", 10, 0), - ("i32::MIN div -1 (overflow case)", i32::MIN, -1), - ]; - - for (name, dividend, divisor) in test_cases.into_iter() { - verify_positive::
(name, dividend, divisor); - verify_positive::(name, dividend, divisor); - } - } - - fn verify_positive + TestOutput>( + // shortcut to verify given pair produces correct output + fn verify_positive + TestInstance>( name: &str, - dividend: i32, - divisor: i32, + dividend: >::NumType, + divisor: >::NumType, ) { verify::( name, @@ -727,21 +639,83 @@ mod test { ); } + // Test unsigned opcodes + type Divu = DivuInstruction; + type Remu = RemuInstruction; + #[test] - fn test_divrem_edges() { - let interesting_values = [ - i32::MIN, - i32::MAX, - i32::MAX / 2, - i32::MIN / 2, - i32::MIN + 1, - i32::MAX - 1, - 0, - -1, - 1, - 2, + fn test_divrem_unsigned_handmade() { + let test_cases = [ + ("10 / 2", 10, 2), + ("10 / 11", 10, 11), + ("11 / 2", 11, 2), + ("large values 1", 1234 * 5678 * 100, 1234), + ("large values 2", 1202729773, 171818539), ]; + for (name, dividend, divisor) in test_cases.into_iter() { + verify_positive::(name, dividend, divisor); + verify_positive::(name, dividend, divisor); + } + } + + #[test] + fn test_divrem_unsigned_edges() { + let interesting_values = [u32::MAX, u32::MAX - 1, 0, 1, 2]; + + for dividend in interesting_values { + for divisor in interesting_values { + let name = format!("dividend = {}, divisor = {}", dividend, divisor); + verify_positive::(&name, dividend, divisor); + verify_positive::(&name, dividend, divisor); + } + } + } + + #[test] + fn test_divrem_unsigned_unsatisfied() { + verify::("assert_outcome", 10, 2, 3, false); + } + + #[test] + fn test_divrem_unsigned_random() { + for _ in 0..10 { + let mut rng = rand::thread_rng(); + let dividend: u32 = rng.gen(); + let divisor: u32 = rng.gen(); + let name = format!("random: dividend = {}, divisor = {}", dividend, divisor); + verify_positive::(&name, dividend, divisor); + verify_positive::(&name, dividend, divisor); + } + } + + // Test signed opcodes + type Div = DivInstruction; + type Rem = RemInstruction; + + #[test] + fn test_divrem_signed_handmade() { + let test_cases = [ + ("10 / 2", 10, 2), + ("10 / 11", 10, 11), + ("11 / 2", 11, 2), + ("-10 / 3", -10, 3), + ("-10 / -3", -10, -3), + ("large values 1", -1234 * 5678 * 100, 5678), + ("large values 2", 1234 * 5678 * 100, 1234), + ("large values 3", 1202729773, 171818539), + ]; + + for (name, dividend, divisor) in test_cases.into_iter() { + verify_positive::
(name, dividend, divisor); + verify_positive::(name, dividend, divisor); + } + } + + #[test] + fn test_divrem_signed_edges() { + let interesting_values = [i32::MIN, i32::MAX, i32::MIN + 1, i32::MAX - 1, 0, -1, 1, 2]; + for dividend in interesting_values { for divisor in interesting_values { let name = format!("dividend = {}, divisor = {}", dividend, divisor); @@ -750,5 +724,16 @@ mod test { } } } + #[test] + fn test_divrem_signed_random() { + for _ in 0..10 { + let mut rng = rand::thread_rng(); + let dividend: i32 = rng.gen(); + let divisor: i32 = rng.gen(); + let name = format!("random: dividend = {}, divisor = {}", dividend, divisor); + verify_positive::
(&name, dividend, divisor); + verify_positive::(&name, dividend, divisor); + } + } } } From 326a623f8f64fe51d95eef1eb6e67413b8d97217 Mon Sep 17 00:00:00 2001 From: Mihai Date: Wed, 18 Dec 2024 11:56:06 +0200 Subject: [PATCH 32/37] clean-up --- ceno_zkvm/src/gadgets/signed.rs | 2 +- ceno_zkvm/src/instructions/riscv/div.rs | 498 ++++++++++++------------ 2 files changed, 246 insertions(+), 254 deletions(-) diff --git a/ceno_zkvm/src/gadgets/signed.rs b/ceno_zkvm/src/gadgets/signed.rs index cc1a1e70f..320787240 100644 --- a/ceno_zkvm/src/gadgets/signed.rs +++ b/ceno_zkvm/src/gadgets/signed.rs @@ -1,4 +1,4 @@ -use std::{fmt::Display, mem::MaybeUninit}; +use std::fmt::Display; use ff_ext::ExtensionField; diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index 875b5bd0c..866c15618 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -68,9 +68,8 @@ //! 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 goldilocks::SmallField; use super::{ RIVInstruction, @@ -84,8 +83,7 @@ use crate::{ gadgets::{AssertLtConfig, IsEqualConfig, IsLtConfig, IsZeroConfig, Signed}, instructions::Instruction, set_val, - uint::{UIntLimbs, Value}, - utils::i64_to_base, + uint::Value, witness::LkMultiplicity, }; use std::marker::PhantomData; @@ -453,287 +451,281 @@ impl Instruction for ArithInstruction -where - Self: Instruction, -{ - type NumType: Copy; - fn as_u32(val: Self::NumType) -> u32; - fn output(config: Self::InstructionConfig) -> UInt; - fn correct(dividend: Self::NumType, divisor: Self::NumType) -> Self::NumType; - const INSN_KIND: InsnKind; -} +#[cfg(test)] +mod test { -impl TestInstance for DivInstruction { - type NumType = i32; - fn as_u32(val: Self::NumType) -> u32 { - val as u32 - } - fn output(config: DivRemConfig) -> UInt { - config.quotient - } - fn correct(dividend: i32, divisor: i32) -> i32 { - if divisor == 0 { - -1i32 - } else { - dividend.wrapping_div(divisor) - } + use super::DivRemConfig; + use crate::{ + Value, + circuit_builder::{CircuitBuilder, ConstraintSystem}, + instructions::{ + Instruction, + riscv::{ + constants::UInt, + div::{DivInstruction, DivuInstruction, RemInstruction, RemuInstruction}, + }, + }, + scheme::mock_prover::{MOCK_PC_START, MockProver}, + }; + use ceno_emul::{Change, InsnKind, StepRecord, encode_rv32}; + use ff_ext::ExtensionField; + use goldilocks::GoldilocksExt2 as GE; + use itertools::Itertools; + use rand::Rng; + + // unifies DIV/REM/DIVU/REMU interface for testing purposes + trait TestInstance + where + Self: Instruction, + { + // type the instruction works with (i32 or u32) + type NumType: Copy; + // conv to register necessary due to lack of native "as" trait + fn as_u32(val: Self::NumType) -> u32; + // designates output value of the circuit that is under scrutiny + fn output(config: Self::InstructionConfig) -> UInt; + // the correct/expected value for given parameters + fn correct(dividend: Self::NumType, divisor: Self::NumType) -> Self::NumType; + const INSN_KIND: InsnKind; } - const INSN_KIND: InsnKind = InsnKind::DIV; -} -impl TestInstance for RemInstruction { - type NumType = i32; - fn as_u32(val: Self::NumType) -> u32 { - val as u32 - } - fn output(config: DivRemConfig) -> UInt { - config.remainder - } - fn correct(dividend: i32, divisor: i32) -> i32 { - if divisor == 0 { - dividend - } else { - dividend.wrapping_rem(divisor) + impl TestInstance for DivInstruction { + type NumType = i32; + fn as_u32(val: Self::NumType) -> u32 { + val as u32 + } + fn output(config: DivRemConfig) -> UInt { + config.quotient + } + fn correct(dividend: i32, divisor: i32) -> i32 { + if divisor == 0 { + -1i32 + } else { + dividend.wrapping_div(divisor) + } } + const INSN_KIND: InsnKind = InsnKind::DIV; } - const INSN_KIND: InsnKind = InsnKind::REM; -} -impl TestInstance for DivuInstruction { - type NumType = u32; - fn as_u32(val: Self::NumType) -> u32 { - val as u32 - } - fn output(config: DivRemConfig) -> UInt { - config.quotient - } - fn correct(dividend: u32, divisor: u32) -> u32 { - if divisor == 0 { - u32::MAX - } else { - dividend / divisor + impl TestInstance for RemInstruction { + type NumType = i32; + fn as_u32(val: Self::NumType) -> u32 { + val as u32 } + fn output(config: DivRemConfig) -> UInt { + config.remainder + } + fn correct(dividend: i32, divisor: i32) -> i32 { + if divisor == 0 { + dividend + } else { + dividend.wrapping_rem(divisor) + } + } + const INSN_KIND: InsnKind = InsnKind::REM; } - const INSN_KIND: InsnKind = InsnKind::DIVU; -} -impl TestInstance for RemuInstruction { - type NumType = u32; - fn as_u32(val: Self::NumType) -> u32 { - val as u32 - } - fn output(config: DivRemConfig) -> UInt { - config.remainder - } - fn correct(dividend: u32, divisor: u32) -> u32 { - if divisor == 0 { - dividend - } else { - dividend % divisor + impl TestInstance for DivuInstruction { + type NumType = u32; + fn as_u32(val: Self::NumType) -> u32 { + val } + fn output(config: DivRemConfig) -> UInt { + config.quotient + } + fn correct(dividend: u32, divisor: u32) -> u32 { + if divisor == 0 { + u32::MAX + } else { + dividend / divisor + } + } + const INSN_KIND: InsnKind = InsnKind::DIVU; } - const INSN_KIND: InsnKind = InsnKind::REMU; -} -// TODO Tests - -#[cfg(test)] -mod test { - mod div { - use crate::{ - Value, - circuit_builder::{CircuitBuilder, ConstraintSystem}, - instructions::{ - Instruction, - riscv::{ - arith::ArithConfig, - constants::UInt, - div::{ - DivInstruction, DivuInstruction, RemInstruction, RemuInstruction, - TestInstance, - }, - }, - }, - scheme::mock_prover::{MOCK_PC_START, MockProver}, - }; - use ceno_emul::{Change, InsnKind, StepRecord, Word, encode_rv32}; - use ff_ext::ExtensionField; - use goldilocks::GoldilocksExt2; - use itertools::Itertools; - use multilinear_extensions::mle::IntoMLEs; - use num_traits::Num; - use rand::Rng; - use std::time::Instant; - - type GE = GoldilocksExt2; - - fn verify + TestInstance>( - name: &str, - dividend: >::NumType, - divisor: >::NumType, - exp_outcome: >::NumType, - is_ok: bool, - ) { - let mut cs = ConstraintSystem::::new(|| "riscv"); - let mut cb = CircuitBuilder::new(&mut cs); - let config = cb - .namespace( - || format!("{}_({})", Insn::name(), name), - |cb| Ok(Insn::construct_circuit(cb)), - ) - .unwrap() - .unwrap(); - let outcome = Insn::correct(dividend, divisor); - let insn_code = encode_rv32(Insn::INSN_KIND, 2, 3, 4, 0); - // values assignment - let (raw_witin, lkm) = Insn::assign_instances(&config, cb.cs.num_witin as usize, vec![ - StepRecord::new_r_instruction( - 3, - MOCK_PC_START, - insn_code, - Insn::as_u32(dividend), - Insn::as_u32(divisor), - Change::new(0, Insn::as_u32(outcome)), - 0, - ), - ]) - .unwrap(); - let expected_rd_written = UInt::from_const_unchecked( - Value::new_unchecked(Insn::as_u32(exp_outcome)) - .as_u16_limbs() - .to_vec(), - ); - - Insn::output(config) - .require_equal(|| "assert_outcome", &mut cb, &expected_rd_written) - .unwrap(); - - let expected_errors: &[_] = if is_ok { &[] } else { &[name] }; - MockProver::assert_with_expected_errors( - &cb, - &raw_witin - .into_mles() - .into_iter() - .map(|v| v.into()) - .collect_vec(), - &[insn_code], - expected_errors, - None, - Some(lkm), - ); + impl TestInstance for RemuInstruction { + type NumType = u32; + fn as_u32(val: Self::NumType) -> u32 { + val } - - // shortcut to verify given pair produces correct output - fn verify_positive + TestInstance>( - name: &str, - dividend: >::NumType, - divisor: >::NumType, - ) { - verify::( - name, - dividend, - divisor, - Insn::correct(dividend, divisor), - true, - ); + fn output(config: DivRemConfig) -> UInt { + config.remainder } - - // Test unsigned opcodes - type Divu = DivuInstruction; - type Remu = RemuInstruction; - - #[test] - fn test_divrem_unsigned_handmade() { - let test_cases = [ - ("10 / 2", 10, 2), - ("10 / 11", 10, 11), - ("11 / 2", 11, 2), - ("large values 1", 1234 * 5678 * 100, 1234), - ("large values 2", 1202729773, 171818539), - ]; - - for (name, dividend, divisor) in test_cases.into_iter() { - verify_positive::(name, dividend, divisor); - verify_positive::(name, dividend, divisor); + fn correct(dividend: u32, divisor: u32) -> u32 { + if divisor == 0 { + dividend + } else { + dividend % divisor } } + const INSN_KIND: InsnKind = InsnKind::REMU; + } - #[test] - fn test_divrem_unsigned_edges() { - let interesting_values = [u32::MAX, u32::MAX - 1, 0, 1, 2]; + fn verify + TestInstance>( + name: &str, + dividend: >::NumType, + divisor: >::NumType, + exp_outcome: >::NumType, + is_ok: bool, + ) { + let mut cs = ConstraintSystem::::new(|| "riscv"); + let mut cb = CircuitBuilder::new(&mut cs); + let config = cb + .namespace( + || format!("{}_({})", Insn::name(), name), + |cb| Ok(Insn::construct_circuit(cb)), + ) + .unwrap() + .unwrap(); + let outcome = Insn::correct(dividend, divisor); + let insn_code = encode_rv32(Insn::INSN_KIND, 2, 3, 4, 0); + // values assignment + let (raw_witin, lkm) = Insn::assign_instances(&config, cb.cs.num_witin as usize, vec![ + StepRecord::new_r_instruction( + 3, + MOCK_PC_START, + insn_code, + Insn::as_u32(dividend), + Insn::as_u32(divisor), + Change::new(0, Insn::as_u32(outcome)), + 0, + ), + ]) + .unwrap(); + let expected_rd_written = UInt::from_const_unchecked( + Value::new_unchecked(Insn::as_u32(exp_outcome)) + .as_u16_limbs() + .to_vec(), + ); + + Insn::output(config) + .require_equal(|| "assert_outcome", &mut cb, &expected_rd_written) + .unwrap(); - for dividend in interesting_values { - for divisor in interesting_values { - let name = format!("dividend = {}, divisor = {}", dividend, divisor); - verify_positive::(&name, dividend, divisor); - verify_positive::(&name, dividend, divisor); - } - } - } + let expected_errors: &[_] = if is_ok { &[] } else { &[name] }; + MockProver::assert_with_expected_errors( + &cb, + &raw_witin + .into_mles() + .into_iter() + .map(|v| v.into()) + .collect_vec(), + &[insn_code], + expected_errors, + None, + Some(lkm), + ); + } + + // shortcut to verify given pair produces correct output + fn verify_positive + TestInstance>( + name: &str, + dividend: >::NumType, + divisor: >::NumType, + ) { + verify::( + name, + dividend, + divisor, + Insn::correct(dividend, divisor), + true, + ); + } - #[test] - fn test_divrem_unsigned_unsatisfied() { - verify::("assert_outcome", 10, 2, 3, false); + // Test unsigned opcodes + type Divu = DivuInstruction; + type Remu = RemuInstruction; + + #[test] + fn test_divrem_unsigned_handmade() { + let test_cases = [ + ("10 / 2", 10, 2), + ("10 / 11", 10, 11), + ("11 / 2", 11, 2), + ("large values 1", 1234 * 5678 * 100, 1234), + ("large values 2", 1202729773, 171818539), + ]; + + for (name, dividend, divisor) in test_cases.into_iter() { + verify_positive::(name, dividend, divisor); + verify_positive::(name, dividend, divisor); } + } - #[test] - fn test_divrem_unsigned_random() { - for _ in 0..10 { - let mut rng = rand::thread_rng(); - let dividend: u32 = rng.gen(); - let divisor: u32 = rng.gen(); - let name = format!("random: dividend = {}, divisor = {}", dividend, divisor); + #[test] + fn test_divrem_unsigned_edges() { + let interesting_values = [u32::MAX, u32::MAX - 1, 0, 1, 2]; + + for dividend in interesting_values { + for divisor in interesting_values { + let name = format!("dividend = {}, divisor = {}", dividend, divisor); verify_positive::(&name, dividend, divisor); verify_positive::(&name, dividend, divisor); } } + } - // Test signed opcodes - type Div = DivInstruction; - type Rem = RemInstruction; - - #[test] - fn test_divrem_signed_handmade() { - let test_cases = [ - ("10 / 2", 10, 2), - ("10 / 11", 10, 11), - ("11 / 2", 11, 2), - ("-10 / 3", -10, 3), - ("-10 / -3", -10, -3), - ("large values 1", -1234 * 5678 * 100, 5678), - ("large values 2", 1234 * 5678 * 100, 1234), - ("large values 3", 1202729773, 171818539), - ]; - - for (name, dividend, divisor) in test_cases.into_iter() { - verify_positive::
(name, dividend, divisor); - verify_positive::(name, dividend, divisor); - } - } + #[test] + fn test_divrem_unsigned_unsatisfied() { + verify::("assert_outcome", 10, 2, 3, false); + } - #[test] - fn test_divrem_signed_edges() { - let interesting_values = [i32::MIN, i32::MAX, i32::MIN + 1, i32::MAX - 1, 0, -1, 1, 2]; + #[test] + fn test_divrem_unsigned_random() { + for _ in 0..10 { + let mut rng = rand::thread_rng(); + let dividend: u32 = rng.gen(); + let divisor: u32 = rng.gen(); + let name = format!("random: dividend = {}, divisor = {}", dividend, divisor); + verify_positive::(&name, dividend, divisor); + verify_positive::(&name, dividend, divisor); + } + } - for dividend in interesting_values { - for divisor in interesting_values { - let name = format!("dividend = {}, divisor = {}", dividend, divisor); - verify_positive::
(&name, dividend, divisor); - verify_positive::(&name, dividend, divisor); - } - } + // Test signed opcodes + type Div = DivInstruction; + type Rem = RemInstruction; + + #[test] + fn test_divrem_signed_handmade() { + let test_cases = [ + ("10 / 2", 10, 2), + ("10 / 11", 10, 11), + ("11 / 2", 11, 2), + ("-10 / 3", -10, 3), + ("-10 / -3", -10, -3), + ("large values 1", -1234 * 5678 * 100, 5678), + ("large values 2", 1234 * 5678 * 100, 1234), + ("large values 3", 1202729773, 171818539), + ]; + + for (name, dividend, divisor) in test_cases.into_iter() { + verify_positive::
(name, dividend, divisor); + verify_positive::(name, dividend, divisor); } - #[test] - fn test_divrem_signed_random() { - for _ in 0..10 { - let mut rng = rand::thread_rng(); - let dividend: i32 = rng.gen(); - let divisor: i32 = rng.gen(); - let name = format!("random: dividend = {}, divisor = {}", dividend, divisor); + } + + #[test] + fn test_divrem_signed_edges() { + let interesting_values = [i32::MIN, i32::MAX, i32::MIN + 1, i32::MAX - 1, 0, -1, 1, 2]; + + for dividend in interesting_values { + for divisor in interesting_values { + let name = format!("dividend = {}, divisor = {}", dividend, divisor); verify_positive::
(&name, dividend, divisor); verify_positive::(&name, dividend, divisor); } } } + #[test] + fn test_divrem_signed_random() { + for _ in 0..10 { + let mut rng = rand::thread_rng(); + let dividend: i32 = rng.gen(); + let divisor: i32 = rng.gen(); + let name = format!("random: dividend = {}, divisor = {}", dividend, divisor); + verify_positive::
(&name, dividend, divisor); + verify_positive::(&name, dividend, divisor); + } + } } From 3eade8b50a37829085b3ddb0f645ab6eb0ae5990 Mon Sep 17 00:00:00 2001 From: Mihai Date: Wed, 18 Dec 2024 12:12:31 +0200 Subject: [PATCH 33/37] add docs TODO --- ceno_zkvm/src/instructions/riscv/div.rs | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index 866c15618..b942969ec 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -41,15 +41,9 @@ //! //! `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 -//! +//! when `dividend` is negative, `quotient` and `remainder` are negative, we +//! need +//! TODO: finish this part of the docs //! `-|divisor| < remainder <= 0` (5) //! //! To handle these variations of the remainder inequalities in a uniform From f72e8294c2265a4453d1945daba378448fa15e57 Mon Sep 17 00:00:00 2001 From: Mihai Date: Wed, 18 Dec 2024 19:36:50 +0200 Subject: [PATCH 34/37] change back to assign_instance --- ceno_zkvm/src/instructions/riscv/div.rs | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index b942969ec..67c143dd4 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -62,8 +62,9 @@ //! 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::SmallField; +use goldilocks::{Goldilocks, SmallField}; use super::{ RIVInstruction, @@ -78,6 +79,7 @@ use crate::{ instructions::Instruction, set_val, uint::Value, + utils::i64_to_base, witness::LkMultiplicity, }; use std::marker::PhantomData; @@ -349,6 +351,7 @@ impl Instruction for ArithInstruction remainder == i32::MIN (-1i32, dividend) } else { // these correctly handle signed division overflow @@ -405,15 +408,17 @@ impl Instruction for ArithInstruction(remainder_pos_orientation).to_canonical_u64(), )?; ( From d2c7b6922bdca56be259ebe872b2752870d513c3 Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Fri, 20 Dec 2024 21:51:25 -0700 Subject: [PATCH 35/37] Integrate DIV/REM assignment with updated interface for AssertLtConfig --- ceno_zkvm/src/gadgets/is_lt.rs | 7 +++---- ceno_zkvm/src/instructions/riscv/div.rs | 15 ++++----------- 2 files changed, 7 insertions(+), 15 deletions(-) diff --git a/ceno_zkvm/src/gadgets/is_lt.rs b/ceno_zkvm/src/gadgets/is_lt.rs index 4c85f213e..45e4d8cf7 100644 --- a/ceno_zkvm/src/gadgets/is_lt.rs +++ b/ceno_zkvm/src/gadgets/is_lt.rs @@ -19,7 +19,6 @@ use crate::{ use super::SignedExtendConfig; -// TODO rename to AssertLtConfig (LT -> Lt) to fit naming conventions #[derive(Debug, Clone)] pub struct AssertLtConfig(InnerLtConfig); @@ -67,10 +66,10 @@ impl AssertLtConfig { &self, instance: &mut [F], lkm: &mut LkMultiplicity, - lhs: i32, - rhs: i32, + lhs: i64, + rhs: i64, ) -> Result<(), ZKVMError> { - self.0.assign_instance_signed(instance, lkm, lhs, rhs)?; + self.0.assign_instance_i64(instance, lkm, lhs, rhs)?; Ok(()) } } diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index 67c143dd4..c3f75ff84 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -62,9 +62,8 @@ //! 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 goldilocks::SmallField; use super::{ RIVInstruction, @@ -79,7 +78,6 @@ use crate::{ instructions::Instruction, set_val, uint::Value, - utils::i64_to_base, witness::LkMultiplicity, }; use std::marker::PhantomData; @@ -405,20 +403,15 @@ impl Instruction for ArithInstruction(remainder_pos_orientation).to_canonical_u64(), + -1, + remainder_pos_orientation, )?; ( From 84b636a93206fa7aa3cd7eb8f58af8e85c566295 Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Fri, 20 Dec 2024 22:30:02 -0700 Subject: [PATCH 36/37] Update comments based on PR feedback and for remainder sign bug fix --- ceno_zkvm/src/instructions/riscv/div.rs | 63 +++++++++++++------------ 1 file changed, 32 insertions(+), 31 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index c3f75ff84..9b29a4154 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -16,13 +16,16 @@ //! //! 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. +//! ambiguity due to modular field arithmetic -- more specifically, `dividend` +//! and `divisor` are taken from RISC-V registers, so are constrained to 32-bit +//! unsigned or signed values, and `quotient` and `remainder` values are +//! explicitly constrained to 32 bits by the checked UInt construction. //! //! 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). +//! or `-1` in the signed 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 @@ -41,25 +44,23 @@ //! //! `0 <= remainder < divisor` (3) //! -//! when `dividend` is negative, `quotient` and `remainder` are negative, we -//! need -//! TODO: finish this part of the docs -//! `-|divisor| < remainder <= 0` (5) +//! For signed inputs the situation is slightly more complicated, as `remainder` +//! and `divisor` may be either positive or negative. To handle sign +//! variations for the remainder inequality 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). The correct sign +//! normalization is to take the absolute value of `divisor`, and to multiply +//! `remainder` by the sign of `dividend` since these two values are required +//! to have matching signs. //! -//! 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. +//! For the special case of signed division overflow, the inequality condition +//! (3) still holds for the remainder and divisor after normalizing signs in +//! this way (specifically: `0 <= 0 < 1`), so no special treatment is needed. +//! In the division by 0 case, since `divisor` is `0`, the inequality cannot be +//! satisfied. To address this case, 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_ext::ExtensionField; @@ -204,10 +205,10 @@ impl Instruction for ArithInstruction Instruction for ArithInstruction = (1 - 2 * dividend_signed.is_negative.expr()) * remainder_signed.expr(); let divisor_pos_orientation = @@ -277,10 +279,9 @@ impl Instruction for ArithInstruction Date: Fri, 20 Dec 2024 22:39:45 -0700 Subject: [PATCH 37/37] Change a few config variable names for clarity --- ceno_zkvm/src/instructions/riscv/div.rs | 26 ++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/div.rs b/ceno_zkvm/src/instructions/riscv/div.rs index 9b29a4154..daa7bc000 100644 --- a/ceno_zkvm/src/instructions/riscv/div.rs +++ b/ceno_zkvm/src/instructions/riscv/div.rs @@ -104,8 +104,8 @@ enum InternalDivRem { divisor_signed: Signed, quotient_signed: Signed, remainder_signed: Signed, - is_dividend_max_negative: IsEqualConfig, - is_divisor_minus_one: IsEqualConfig, + is_dividend_signed_min: IsEqualConfig, + is_divisor_neg_one: IsEqualConfig, is_signed_overflow: WitIn, remainder_nonnegative: AssertLtConfig, }, @@ -186,21 +186,21 @@ impl Instruction for ArithInstruction Instruction for ArithInstruction Instruction for ArithInstruction Instruction for ArithInstruction