Merge branch 'master' into feat/load_mem

ceno_emul/src/platform.rs

@@ -36,14 +36,15 @@ impl Platform {
     }
 
     pub const fn ram_end(&self) -> Addr {
-        if cfg!(feature = "forbid_overflow") {
-            // (1<<11) - 1 == 0x7ff is the largest positive 'immediate'
-            // offset we can have in memory instructions.
-            // So if we stay away from it, we are safe.
-            u32::MAX - 0x7FF
-        } else {
-            0xFFFF_FFFF
-        }
+        0xFFFF_FFFF
+            - if cfg!(feature = "forbid_overflow") {
+                // (1<<11) - 1 == 0x7ff is the largest positive 'immediate'
+                // offset we can have in memory instructions.
+                // So if we stay away from it, we are safe.
+                0x7FF
+            } else {
+                0
+            }
     }
 
     pub fn is_ram(&self, addr: Addr) -> bool {

ceno_zkvm/src/gadgets/is_lt.rs

@@ -1,15 +1,17 @@
 use std::{fmt::Display, mem::MaybeUninit};
 
-use ceno_emul::SWord;
+use ceno_emul::{SWord, Word};
 use ff_ext::ExtensionField;
 use goldilocks::SmallField;
 use itertools::izip;
 
 use crate::{
+    Value,
     chip_handler::utils::power_sequence,
     circuit_builder::CircuitBuilder,
     error::ZKVMError,
     expression::{Expression, ToExpr, WitIn},
+    instructions::riscv::constants::{UINT_LIMBS, UInt},
     set_val,
     witness::LkMultiplicity,
 };
@@ -192,9 +194,9 @@ impl InnerLtConfig {
         rhs: SWord,
     ) -> Result<(), ZKVMError> {
         let diff = if lhs < rhs {
-            Self::range(self.diff.len()) - (rhs - lhs) as u64
+            Self::range(self.diff.len()) - lhs.abs_diff(rhs) as u64
         } else {
-            (lhs - rhs) as u64
+            lhs.abs_diff(rhs) as u64
         };
         self.diff.iter().enumerate().for_each(|(i, wit)| {
             // extract the 16 bit limb from diff and assign to instance
@@ -214,3 +216,174 @@ pub fn cal_lt_diff(is_lt: bool, max_num_u16_limbs: usize, lhs: u64, rhs: u64) ->
     } + lhs
         - rhs)
 }
+
+#[derive(Debug)]
+pub struct AssertSignedLtConfig {
+    config: InnerSignedLtConfig,
+}
+
+impl AssertSignedLtConfig {
+    pub fn construct_circuit<
+        E: ExtensionField,
+        NR: Into<String> + Display + Clone,
+        N: FnOnce() -> NR,
+    >(
+        cb: &mut CircuitBuilder<E>,
+        name_fn: N,
+        lhs: &UInt<E>,
+        rhs: &UInt<E>,
+    ) -> Result<Self, ZKVMError> {
+        cb.namespace(
+            || "assert_signed_lt",
+            |cb| {
+                let name = name_fn();
+                let config =
+                    InnerSignedLtConfig::construct_circuit(cb, name, lhs, rhs, Expression::ONE)?;
+                Ok(Self { config })
+            },
+        )
+    }
+
+    pub fn assign_instance<E: ExtensionField>(
+        &self,
+        instance: &mut [MaybeUninit<E::BaseField>],
+        lkm: &mut LkMultiplicity,
+        lhs: SWord,
+        rhs: SWord,
+    ) -> Result<(), ZKVMError> {
+        self.config.assign_instance::<E>(instance, lkm, lhs, rhs)?;
+        Ok(())
+    }
+}
+
+#[derive(Debug)]
+pub struct SignedLtConfig {
+    is_lt: WitIn,
+    config: InnerSignedLtConfig,
+}
+
+impl SignedLtConfig {
+    pub fn expr<E: ExtensionField>(&self) -> Expression<E> {
+        self.is_lt.expr()
+    }
+
+    pub fn construct_circuit<
+        E: ExtensionField,
+        NR: Into<String> + Display + Clone,
+        N: FnOnce() -> NR,
+    >(
+        cb: &mut CircuitBuilder<E>,
+        name_fn: N,
+        lhs: &UInt<E>,
+        rhs: &UInt<E>,
+    ) -> Result<Self, ZKVMError> {
+        cb.namespace(
+            || "is_signed_lt",
+            |cb| {
+                let name = name_fn();
+                let is_lt = cb.create_witin(|| format!("{name} is_signed_lt witin"))?;
+                cb.assert_bit(|| "is_lt_bit", is_lt.expr())?;
+                let config =
+                    InnerSignedLtConfig::construct_circuit(cb, name, lhs, rhs, is_lt.expr())?;
+
+                Ok(SignedLtConfig { is_lt, config })
+            },
+        )
+    }
+
+    pub fn assign_instance<E: ExtensionField>(
+        &self,
+        instance: &mut [MaybeUninit<E::BaseField>],
+        lkm: &mut LkMultiplicity,
+        lhs: SWord,
+        rhs: SWord,
+    ) -> Result<(), ZKVMError> {
+        set_val!(instance, self.is_lt, (lhs < rhs) as u64);
+        self.config
+            .assign_instance::<E>(instance, lkm, lhs as SWord, rhs as SWord)?;
+        Ok(())
+    }
+}
+
+#[derive(Debug)]
+struct InnerSignedLtConfig {
+    is_lhs_neg: IsLtConfig,
+    is_rhs_neg: IsLtConfig,
+    config: InnerLtConfig,
+}
+
+impl InnerSignedLtConfig {
+    pub fn construct_circuit<E: ExtensionField, NR: Into<String> + Display + Clone>(
+        cb: &mut CircuitBuilder<E>,
+        name: NR,
+        lhs: &UInt<E>,
+        rhs: &UInt<E>,
+        is_lt_expr: Expression<E>,
+    ) -> Result<Self, ZKVMError> {
+        let max_signed_limb_expr: Expression<_> = ((1 << (UInt::<E>::LIMB_BITS - 1)) - 1).into();
+        // Extract the sign bit.
+        let is_lhs_neg = IsLtConfig::construct_circuit(
+            cb,
+            || "lhs_msb",
+            max_signed_limb_expr.clone(),
+            lhs.limbs.iter().last().unwrap().expr(), // msb limb
+            1,
+        )?;
+        let is_rhs_neg = IsLtConfig::construct_circuit(
+            cb,
+            || "rhs_msb",
+            max_signed_limb_expr,
+            rhs.limbs.iter().last().unwrap().expr(), // msb limb
+            1,
+        )?;
+
+        // Convert two's complement representation into field arithmetic.
+        // Example: 0xFFFF_FFFF = 2^32 - 1  -->  shift  -->  -1
+        let neg_shift = -Expression::Constant((1_u64 << 32).into());
+        let lhs_value = lhs.value() + is_lhs_neg.expr() * neg_shift.clone();
+        let rhs_value = rhs.value() + is_rhs_neg.expr() * neg_shift;
+
+        let config = InnerLtConfig::construct_circuit(
+            cb,
+            format!("{name} (lhs < rhs)"),
+            lhs_value,
+            rhs_value,
+            is_lt_expr,
+            UINT_LIMBS,
+        )?;
+
+        Ok(Self {
+            is_lhs_neg,
+            is_rhs_neg,
+            config,
+        })
+    }
+
+    pub fn assign_instance<E: ExtensionField>(
+        &self,
+        instance: &mut [MaybeUninit<E::BaseField>],
+        lkm: &mut LkMultiplicity,
+        lhs: SWord,
+        rhs: SWord,
+    ) -> Result<(), ZKVMError> {
+        let max_signed_limb = (1u64 << (UInt::<E>::LIMB_BITS - 1)) - 1;
+        let lhs_value = Value::new_unchecked(lhs as Word);
+        let rhs_value = Value::new_unchecked(rhs as Word);
+        self.is_lhs_neg.assign_instance(
+            instance,
+            lkm,
+            max_signed_limb,
+            *lhs_value.limbs.last().unwrap() as u64,
+        )?;
+        self.is_rhs_neg.assign_instance(
+            instance,
+            lkm,
+            max_signed_limb,
+            *rhs_value.limbs.last().unwrap() as u64,
+        )?;
+
+        self.config
+            .assign_instance_signed(instance, lkm, lhs, rhs)?;
+        Ok(())
+    }
+}

ceno_zkvm/src/gadgets/mod.rs

@@ -2,5 +2,7 @@ mod div;
 mod is_lt;
 mod is_zero;
 pub use div::DivConfig;
-pub use is_lt::{AssertLTConfig, InnerLtConfig, IsLtConfig, cal_lt_diff};
+pub use is_lt::{
+    AssertLTConfig, AssertSignedLtConfig, InnerLtConfig, IsLtConfig, SignedLtConfig, cal_lt_diff,
+};
 pub use is_zero::{IsEqualConfig, IsZeroConfig};

ceno_zkvm/src/instructions/riscv.rs

@@ -16,6 +16,7 @@ pub mod logic_imm;
 pub mod mulh;
 pub mod shift;
 pub mod shift_imm;
+pub mod slt;
 pub mod sltu;
 
 mod b_insn;

ceno_zkvm/src/instructions/riscv/branch/blt.rs

@@ -7,11 +7,10 @@ use crate::{
     circuit_builder::CircuitBuilder,
     error::ZKVMError,
     expression::Expression,
+    gadgets::SignedLtConfig,
     instructions::{
         Instruction,
-        riscv::{
-            RIVInstruction, b_insn::BInstructionConfig, config::SignedLtConfig, constants::UInt,
-        },
+        riscv::{RIVInstruction, b_insn::BInstructionConfig, constants::UInt},
     },
     witness::LkMultiplicity,
 };