Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Feat/Opcode Circuits for DIV, REM, and REMU opcodes #596

Open
wants to merge 25 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 10 commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
4fb46a4
Move `Signed` gadget from MULH opcode to `gadgets` submodule
Nov 15, 2024
2812c12
Extend DIVU gadget implementation to support REMU/DIV/REM opcodes
Nov 17, 2024
6919ece
Format updates
Dec 6, 2024
754a75d
Merge branch 'master' into bg/div-rem-remu-opcodes
Dec 6, 2024
b9be2fc
A few DIV opcode circuit fixes, documentation, and vm integration
Dec 7, 2024
22bc22a
Rename `divu.rs` to `div.rs` and add check for Goldilocks field
Dec 7, 2024
4c11b43
Small reformatting and doc improvements
Dec 7, 2024
277fd77
Merge branch 'master' into bg/div-rem-remu-opcodes
Dec 7, 2024
36c2af4
Formatting fix
Dec 10, 2024
3e7931b
Fix a couple of missed changes in rv32im.rs needed for new opcodes
Dec 10, 2024
7821de4
Fix bug in signed remainder construction
Dec 11, 2024
23e6421
Small comment fixes
Dec 11, 2024
eb0a117
Update UInt assignment in DIV opcodes to use assign_value function
Dec 11, 2024
92d44d5
Replace constants using UInt BIT_WIDTH with hard-coded values in DIV …
Dec 11, 2024
4425c13
Change unnecessary generic constant with hard-coded value for readabi…
Dec 11, 2024
0158e01
Merge branch 'master' into bg/div-rem-remu-opcodes
Dec 11, 2024
54bf10c
Change Signed circuit to use bit shift directly on expression
Dec 11, 2024
92bce79
Small updates based on PR comments
Dec 11, 2024
8317a28
Fix assignment to remainder_nonnegative in DIV/REM opcodes circuit
Dec 11, 2024
0c3f5ed
Simplify syntax for a few Expression definitions
Dec 11, 2024
41e3e19
Remove a few unnecessary type annotations
Dec 11, 2024
137964a
Use built-in arithmetic calls for unsigned quotient/remainder computa…
Dec 11, 2024
0f71c30
Simplify variables in signed DIV/REM assignment by shadowing unsigned…
Dec 11, 2024
124d623
Use parameter for limb size in SignedExtendConfig rather than hard-co…
Dec 11, 2024
833dbca
Revise Signed val construction to use relevant UInt utility function
Dec 11, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions ceno_zkvm/src/gadgets/is_lt.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ use crate::{

use super::SignedExtendConfig;

// TODO rename to AssertLtConfig (LT -> Lt) to fit naming conventions
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See #731

#[derive(Debug, Clone)]
pub struct AssertLTConfig(InnerLtConfig);

Expand Down
2 changes: 2 additions & 0 deletions ceno_zkvm/src/gadgets/mod.rs
Original file line number Diff line number Diff line change
@@ -1,11 +1,13 @@
mod div;
mod is_lt;
mod is_zero;
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::Signed;
pub use signed_ext::SignedExtendConfig;
57 changes: 57 additions & 0 deletions ceno_zkvm/src/gadgets/signed.rs
Original file line number Diff line number Diff line change
@@ -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.
bgillesp marked this conversation as resolved.
Show resolved Hide resolved
pub struct Signed<E: ExtensionField> {
pub is_negative: SignedExtendConfig<E>,
val: Expression<E>,
}

impl<E: ExtensionField> Signed<E> {
pub fn construct_circuit<NR: Into<String> + Display + Clone, N: FnOnce() -> NR>(
cb: &mut CircuitBuilder<E>,
name_fn: N,
unsigned_val: &UInt<E>,
) -> Result<Self, ZKVMError> {
cb.namespace(name_fn, |cb| {
let is_negative = unsigned_val.is_negative(cb)?;
let val = unsigned_val.value() - (1u64 << BIT_WIDTH) * is_negative.expr();
bgillesp marked this conversation as resolved.
Show resolved Hide resolved
bgillesp marked this conversation as resolved.
Show resolved Hide resolved

Ok(Self { is_negative, val })
})
}

pub fn assign_instance(
&self,
instance: &mut [MaybeUninit<E::BaseField>],
lkm: &mut LkMultiplicity,
val: &Value<u32>,
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Will it be better to use i32? Callers could assign i32::MAX + 1, and this could cause unexpeced result If the type isu32.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this might be a nontrivial change to implement -- the Value type seems to lean into the design of an "unsigned integer register" which can be interpreted as signed as desired, but not by default. In particular, the generic type T for Value<T> is currently constrained to Into<u64> + From<u32>, so u32 and u64 values are first-class citizens, but things break when I try to make it an i32. The gadget is really designed to provide a signed interpretation to an unsigned register value anyway, so I think that's why I originally chose the u32 representation. Okay if we leave it as is for now?

) -> Result<i32, ZKVMError> {
self.is_negative.assign_instance(
instance,
lkm,
*val.as_u16_limbs().last().unwrap() as u64,
)?;
let signed_val = val.as_u32() as i32;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See #732

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just reviewed #732, will make the change here once it's merged into master.


Ok(signed_val)
}

pub fn expr(&self) -> Expression<E> {
self.val.clone()
}
}
9 changes: 7 additions & 2 deletions ceno_zkvm/src/gadgets/signed_ext.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,11 +9,16 @@ use crate::{
use ff_ext::ExtensionField;
bgillesp marked this conversation as resolved.
Show resolved Hide resolved
use std::{marker::PhantomData, mem::MaybeUninit};

/// Extract the most significant bit from an expression previously constrained
/// to an 8- or 16-bit length.
bgillesp marked this conversation as resolved.
Show resolved Hide resolved
///
/// Uses 1 `WitIn` value to store the bit, one `assert_bit` constraint, and one
/// `u8` or `u16` table lookup.
#[derive(Debug)]
pub struct SignedExtendConfig<E> {
/// 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<E>,
Expand Down
2 changes: 1 addition & 1 deletion ceno_zkvm/src/instructions/riscv.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
Loading