From 4fb46a4ccfeac9e29cc3a0724b7bf25467274177 Mon Sep 17 00:00:00 2001 From: Bryan Gillespie Date: Fri, 15 Nov 2024 11:31:24 -0700 Subject: [PATCH 01/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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/23] 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