Merge remote-tracking branch 'origin/master' into matthias/simplify-c…

…ircuit-builder

.gitignore

@@ -4,3 +4,4 @@ target
 log.txt
 logs/
 table_cache_dev_*
+.DS_Store

Cargo.toml

@@ -26,7 +26,6 @@ version = "0.1.0"
 [workspace.dependencies]
 ark-std = "0.4"
 cfg-if = "1.0"
-const_env = "0.1"
 criterion = { version = "0.5", features = ["html_reports"] }
 crossbeam-channel = "0.5"
 ff = "0.13"

ceno_emul/src/rv32im.rs

@@ -218,28 +218,6 @@ impl DecodedInstruction {
         }
     }
 
-    #[allow(dead_code)]
-    pub fn from_raw(kind: InsnKind, rs1: u32, rs2: u32, rd: u32) -> Self {
-        // limit the range of inputs
-        let rs2 = rs2 & 0x1f; // 5bits mask
-        let rs1 = rs1 & 0x1f;
-        let rd = rd & 0x1f;
-        let func7 = kind.codes().func7;
-        let func3 = kind.codes().func3;
-        let opcode = kind.codes().opcode;
-        let insn = func7 << 25 | rs2 << 20 | rs1 << 15 | func3 << 12 | rd << 7 | opcode;
-        Self {
-            insn,
-            top_bit: func7 | 0x80,
-            func7,
-            rs2,
-            rs1,
-            func3,
-            rd,
-            opcode,
-        }
-    }
-
     pub fn encoded(&self) -> u32 {
         self.insn
     }

ceno_zkvm/Cargo.toml

@@ -36,7 +36,6 @@ thread_local = "1.1"
 [dev-dependencies]
 base64 = "0.22"
 cfg-if.workspace = true
-const_env.workspace = true
 criterion.workspace = true
 pprof.workspace = true
 serde_json.workspace = true

ceno_zkvm/benches/riscv_add.rs

@@ -7,7 +7,6 @@ use ceno_zkvm::{
     scheme::prover::ZKVMProver,
     structs::{ZKVMConstraintSystem, ZKVMFixedTraces},
 };
-use const_env::from_env;
 use criterion::*;
 
 use ceno_zkvm::scheme::constants::MAX_NUM_VARIABLES;
@@ -37,31 +36,9 @@ cfg_if::cfg_if! {
 criterion_main!(op_add);
 
 const NUM_SAMPLES: usize = 10;
-#[from_env]
-const RAYON_NUM_THREADS: usize = 8;
 
 fn bench_add(c: &mut Criterion) {
     type Pcs = BasefoldDefault<E>;
-    let max_threads = {
-        if !RAYON_NUM_THREADS.is_power_of_two() {
-            #[cfg(not(feature = "non_pow2_rayon_thread"))]
-            {
-                panic!(
-                    "add --features non_pow2_rayon_thread to enable unsafe feature which support non pow of 2 rayon thread pool"
-                );
-            }
-
-            #[cfg(feature = "non_pow2_rayon_thread")]
-            {
-                use sumcheck::{local_thread_pool::create_local_pool_once, util::ceil_log2};
-                let max_thread_id = 1 << ceil_log2(RAYON_NUM_THREADS);
-                create_local_pool_once(1 << ceil_log2(RAYON_NUM_THREADS), true);
-                max_thread_id
-            }
-        } else {
-            RAYON_NUM_THREADS
-        }
-    };
     let mut zkvm_cs = ZKVMConstraintSystem::default();
     let _ = zkvm_cs.register_opcode_circuit::<AddInstruction<E>>();
     let mut zkvm_fixed_traces = ZKVMFixedTraces::default();
@@ -128,7 +105,6 @@ fn bench_add(c: &mut Criterion) {
                                 commit,
                                 &[],
                                 num_instances,
-                                max_threads,
                                 &mut transcript,
                                 &challenges,
                             )

ceno_zkvm/examples/riscv_opcodes.rs

@@ -8,7 +8,6 @@ use ceno_zkvm::{
     tables::{MemFinalRecord, ProgramTableCircuit, initial_memory, initial_registers},
 };
 use clap::Parser;
-use const_env::from_env;
 
 use ceno_emul::{
     ByteAddr, CENO_PLATFORM, EmuContext,
@@ -28,9 +27,6 @@ use tracing_flame::FlameLayer;
 use tracing_subscriber::{EnvFilter, Registry, fmt, layer::SubscriberExt};
 use transcript::Transcript;
 
-#[from_env]
-const RAYON_NUM_THREADS: usize = 8;
-
 const PROGRAM_SIZE: usize = 512;
 // For now, we assume registers
 //  - x0 is not touched,
@@ -80,27 +76,6 @@ fn main() {
     type E = GoldilocksExt2;
     type Pcs = Basefold<GoldilocksExt2, BasefoldRSParams, ChaCha8Rng>;
 
-    let max_threads = {
-        if !RAYON_NUM_THREADS.is_power_of_two() {
-            #[cfg(not(feature = "non_pow2_rayon_thread"))]
-            {
-                panic!(
-                    "add --features non_pow2_rayon_thread to enable unsafe feature which support non pow of 2 rayon thread pool"
-                );
-            }
-
-            #[cfg(feature = "non_pow2_rayon_thread")]
-            {
-                use sumcheck::{local_thread_pool::create_local_pool_once, util::ceil_log2};
-                let max_thread_id = 1 << ceil_log2(RAYON_NUM_THREADS);
-                create_local_pool_once(1 << ceil_log2(RAYON_NUM_THREADS), true);
-                max_thread_id
-            }
-        } else {
-            RAYON_NUM_THREADS
-        }
-    };
-
     let (flame_layer, _guard) = FlameLayer::with_file("./tracing.folded").unwrap();
     let subscriber = Registry::default()
         .with(
@@ -237,7 +212,7 @@ fn main() {
 
         let transcript = Transcript::new(b"riscv");
         let mut zkvm_proof = prover
-            .create_proof(zkvm_witness, pi, max_threads, transcript)
+            .create_proof(zkvm_witness, pi, transcript)
             .expect("create_proof failed");
 
         println!(

ceno_zkvm/src/chip_handler/general.rs

@@ -157,7 +157,10 @@ impl<'a, E: ExtensionField> CircuitBuilder<'a, E> {
     where
         Name: Into<String>,
     {
-        self.namespace("require_equal", |cb| cb.cs.require_zero(name, a - b))
+        self.namespace("require_equal", |cb| {
+            cb.cs
+                .require_zero(name, a.to_monomial_form() - b.to_monomial_form())
+        })
     }
 
     pub fn require_one<Name>(&mut self, name: Name, expr: Expression<E>) -> Result<(), ZKVMError>

ceno_zkvm/src/expression.rs

@@ -634,22 +634,6 @@ impl WitIn {
     }
 }
 
-#[macro_export]
-/// this is to avoid non-monomial expression
-macro_rules! create_witin_from_expr {
-    // Handle the case for a single expression
-    ($name:expr, $builder:expr, $debug:expr, $e:expr) => {
-        WitIn::from_expr($name, $builder, $e, $debug)
-    };
-    // Recursively handle multiple expressions and create a flat tuple with error handling
-    ($name:expr, $builder:expr, $debug:expr, $e:expr, $($rest:expr),+) => {
-        {
-            // Return a Result tuple, handling errors
-            Ok::<_, ZKVMError>((WitIn::from_expr($name, $builder, $e, $debug)?, $(WitIn::from_expr($name, $builder, $rest)?),*))
-        }
-    };
-}
-
 pub trait ToExpr<E: ExtensionField> {
     type Output;
     fn expr(&self) -> Self::Output;
@@ -752,7 +736,9 @@ pub mod fmt {
     ) -> String {
         match expression {
             Expression::WitIn(wit_in) => {
-                wtns.push(*wit_in);
+                if !wtns.contains(wit_in) {
+                    wtns.push(*wit_in);
+                }
                 format!("WitIn({})", wit_in)
             }
             Expression::Challenge(id, pow, scaler, offset) => {

ceno_zkvm/src/gadgets/is_lt.rs

@@ -93,11 +93,23 @@ impl IsLtConfig {
         lhs: u64,
         rhs: u64,
     ) -> Result<(), ZKVMError> {
-        let is_lt = lhs < rhs;
-        set_val!(instance, self.is_lt, is_lt as u64);
+        set_val!(instance, self.is_lt, (lhs < rhs) as u64);
         self.config.assign_instance(instance, lkm, lhs, rhs)?;
         Ok(())
     }
+
+    pub fn assign_instance_signed<F: SmallField>(
+        &self,
+        instance: &mut [MaybeUninit<F>],
+        lkm: &mut LkMultiplicity,
+        lhs: SWord,
+        rhs: SWord,
+    ) -> Result<(), ZKVMError> {
+        set_val!(instance, self.is_lt, (lhs < rhs) as u64);
+        self.config
+            .assign_instance_signed(instance, lkm, lhs, rhs)?;
+        Ok(())
+    }
 }
 
 #[derive(Debug, Clone)]
@@ -301,12 +313,9 @@ impl InnerSignedLtConfig {
             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;
-
+        // Convert to field arithmetic.
+        let lhs_value = lhs.to_field_expr(is_lhs_neg.expr());
+        let rhs_value = rhs.to_field_expr(is_rhs_neg.expr());
         let config = InnerLtConfig::construct_circuit(
             cb,
             format!("{name} (lhs < rhs)"),

ceno_zkvm/src/instructions/riscv.rs

@@ -17,6 +17,7 @@ pub mod mulh;
 pub mod shift;
 pub mod shift_imm;
 pub mod slt;
+pub mod slti;
 pub mod sltu;
 
 mod b_insn;
@@ -33,6 +34,8 @@ mod memory;
 mod s_insn;
 #[cfg(test)]
 mod test;
+#[cfg(test)]
+mod test_utils;
 
 pub trait RIVInstruction {
     const INST_KIND: InsnKind;

ceno_zkvm/src/instructions/riscv/arith_imm.rs

@@ -88,21 +88,12 @@ mod test {
 
     use crate::{
         circuit_builder::{CircuitBuilder, ConstraintSystem},
-        instructions::Instruction,
+        instructions::{Instruction, riscv::test_utils::imm_i},
         scheme::mock_prover::{MOCK_PC_START, MockProver},
     };
 
     use super::AddiInstruction;
 
-    fn imm(imm: i32) -> u32 {
-        // imm is 12 bits in B-type
-        const IMM_MAX: i32 = 2i32.pow(12);
-        if imm.is_negative() {
-            (IMM_MAX + imm) as u32
-        } else {
-            imm as u32
-        }
-    }
     #[test]
     fn test_opcode_addi() {
         let mut cs = ConstraintSystem::<GoldilocksExt2>::new("riscv");
@@ -115,7 +106,7 @@ mod test {
             .unwrap()
             .unwrap();
 
-        let insn_code = encode_rv32(InsnKind::ADDI, 2, 0, 4, imm(3));
+        let insn_code = encode_rv32(InsnKind::ADDI, 2, 0, 4, imm_i(3));
         let (raw_witin, lkm) = AddiInstruction::<GoldilocksExt2>::assign_instances(
             &config,
             cb.cs.num_witin as usize,
@@ -156,7 +147,7 @@ mod test {
             .unwrap()
             .unwrap();
 
-        let insn_code = encode_rv32(InsnKind::ADDI, 2, 0, 4, imm(-3));
+        let insn_code = encode_rv32(InsnKind::ADDI, 2, 0, 4, imm_i(-3));
         let (raw_witin, lkm) = AddiInstruction::<GoldilocksExt2>::assign_instances(
             &config,
             cb.cs.num_witin as usize,