Skip to content

Commit

Permalink
Recognise UInt::from_exprs_unchecked can't fail (#486)
Browse files Browse the repository at this point in the history
  • Loading branch information
matthiasgoergens authored Oct 28, 2024
1 parent e949246 commit 81b5745
Show file tree
Hide file tree
Showing 7 changed files with 16 additions and 24 deletions.
4 changes: 1 addition & 3 deletions ceno_zkvm/src/gadgets/signed_ext.rs
Original file line number Diff line number Diff line change
Expand Up @@ -68,9 +68,7 @@ impl SignedExtendConfig {
16 => val,
_ => unreachable!("unsupported N_BITS = {}", self.n_bits),
};

// it's safe to unwrap as `UInt::from_exprs_unchecked` never return error
UInt::from_exprs_unchecked(vec![limb0, self.msb.expr() * 0xffff]).unwrap()
UInt::from_exprs_unchecked(vec![limb0, self.msb.expr() * 0xffff])
}

pub fn assign_instance<E: ExtensionField>(
Expand Down
15 changes: 5 additions & 10 deletions ceno_zkvm/src/instructions/riscv/memory/load.rs
Original file line number Diff line number Diff line change
Expand Up @@ -155,8 +155,7 @@ impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for LoadInstruction<E,
UInt::from_exprs_unchecked(vec![
target_limb.as_ref().map(|limb| limb.expr()).unwrap(),
Expression::ZERO,
])
.unwrap(),
]),
)
}
InsnKind::LB => {
Expand All @@ -167,14 +166,10 @@ impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for LoadInstruction<E,

(Some(signed_extend_config), rd_written)
}
InsnKind::LBU => {
(
None,
// it's safe to unwrap as `UInt::from_exprs_unchecked` never return error
UInt::from_exprs_unchecked(vec![target_byte_expr.unwrap(), Expression::ZERO])
.unwrap(),
)
}
InsnKind::LBU => (
None,
UInt::from_exprs_unchecked(vec![target_byte_expr.unwrap(), Expression::ZERO]),
),
_ => unreachable!("Unsupported instruction kind {:?}", I::INST_KIND),
};

Expand Down
2 changes: 1 addition & 1 deletion ceno_zkvm/src/instructions/riscv/slt.rs
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ impl<E: ExtensionField> Instruction<E> for SltInstruction<E> {
let rs2_read = UInt::new_unchecked(|| "rs2_read", cb)?;

let lt = SignedLtConfig::construct_circuit(cb, || "rs1 < rs2", &rs1_read, &rs2_read)?;
let rd_written = UInt::from_exprs_unchecked(vec![lt.expr()])?;
let rd_written = UInt::from_exprs_unchecked(vec![lt.expr()]);

let r_insn = RInstructionConfig::<E>::construct_circuit(
cb,
Expand Down
2 changes: 1 addition & 1 deletion ceno_zkvm/src/instructions/riscv/slti.rs
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,7 @@ impl<E: ExtensionField> Instruction<E> for SltiInstruction<E> {
imm.expr(),
UINT_LIMBS,
)?;
let rd_written = UInt::from_exprs_unchecked(vec![lt.expr()])?;
let rd_written = UInt::from_exprs_unchecked(vec![lt.expr()]);

let i_insn = IInstructionConfig::<E>::construct_circuit(
cb,
Expand Down
2 changes: 1 addition & 1 deletion ceno_zkvm/src/instructions/riscv/sltu.rs
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for ArithInstruction<E
rs2_read.value(),
UINT_LIMBS,
)?;
let rd_written = UInt::from_exprs_unchecked(vec![lt.expr()])?;
let rd_written = UInt::from_exprs_unchecked(vec![lt.expr()]);

let r_insn = RInstructionConfig::<E>::construct_circuit(
circuit_builder,
Expand Down
13 changes: 6 additions & 7 deletions ceno_zkvm/src/uint.rs
Original file line number Diff line number Diff line change
Expand Up @@ -302,7 +302,7 @@ impl<const M: usize, const C: usize, E: ExtensionField> UIntLimbs<M, C, E> {
.unwrap()
})
.collect_vec();
UIntLimbs::<M, C, E>::from_exprs_unchecked(combined_limbs)
Ok(UIntLimbs::<M, C, E>::from_exprs_unchecked(combined_limbs))
}

pub fn to_u8_limbs(
Expand Down Expand Up @@ -345,8 +345,8 @@ impl<const M: usize, const C: usize, E: ExtensionField> UIntLimbs<M, C, E> {
UIntLimbs::<M, 8, E>::create_witin_from_exprs(circuit_builder, split_limbs)
}

pub fn from_exprs_unchecked(expr_limbs: Vec<Expression<E>>) -> Result<Self, ZKVMError> {
let n = Self {
pub fn from_exprs_unchecked(expr_limbs: Vec<Expression<E>>) -> Self {
Self {
limbs: UintLimb::Expression(
expr_limbs
.into_iter()
Expand All @@ -356,8 +356,7 @@ impl<const M: usize, const C: usize, E: ExtensionField> UIntLimbs<M, C, E> {
),
carries: None,
carries_auxiliary_lt_config: None,
};
Ok(n)
}
}

/// If current limbs are Expression, this function will create witIn and replace the limbs
Expand Down Expand Up @@ -523,8 +522,8 @@ impl<const M: usize, const C: usize, E: ExtensionField> UIntLimbs<M, C, E> {
let mut self_lo = self.expr();
let self_hi = self_lo.split_off(self_lo.len() / 2);
Ok((
UIntLimbs::from_exprs_unchecked(self_lo)?,
UIntLimbs::from_exprs_unchecked(self_hi)?,
UIntLimbs::from_exprs_unchecked(self_lo),
UIntLimbs::from_exprs_unchecked(self_hi),
))
}

Expand Down
2 changes: 1 addition & 1 deletion ceno_zkvm/src/uint/arithmetic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -241,7 +241,7 @@ impl<const M: usize, const C: usize, E: ExtensionField> UIntLimbs<M, C, E> {
mul_hi
} else {
// lo limb
UIntLimbs::from_exprs_unchecked(mul.expr())?
UIntLimbs::from_exprs_unchecked(mul.expr())
};
let add = cb.namespace(
|| "add",
Expand Down

0 comments on commit 81b5745

Please sign in to comment.