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 28 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 10 commits
Commits
Show all changes
28 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
5947d99
Merge branch 'master' into bg/div-rem-remu-opcodes
Dec 12, 2024
19647e0
Merge branch 'master' into bg/div-rem-remu-opcodes
Dec 13, 2024
e719763
Change way that expression for `neg_div_expr` is written
Dec 13, 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
matthiasgoergens marked this conversation as resolved.
Show resolved Hide resolved
Copy link
Collaborator

Choose a reason for hiding this comment

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

Suggested change
// TODO rename to AssertLtConfig (LT -> Lt) to fit naming conventions

#[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>,
matthiasgoergens marked this conversation as resolved.
Show resolved Hide resolved
) -> 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;
bgillesp marked this conversation as resolved.
Show resolved Hide resolved

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