From 8e9c2d2bd37c147014a61dadd2fed5f385a55492 Mon Sep 17 00:00:00 2001 From: "sm.wu" Date: Mon, 20 Oct 2025 16:16:48 +0800 Subject: [PATCH] chores: mock_proving non-static ram type --- .github/workflows/lints.yml | 2 + Cargo.lock | 16 ++--- ceno_zkvm/src/scheme/mock_prover.rs | 91 +++++++++++++++++++++++++--- gkr_iop/src/circuit_builder.rs | 94 ++++++++++++++++++++++++----- 4 files changed, 169 insertions(+), 34 deletions(-) diff --git a/.github/workflows/lints.yml b/.github/workflows/lints.yml index 29ff53880..8c08a3662 100644 --- a/.github/workflows/lints.yml +++ b/.github/workflows/lints.yml @@ -66,3 +66,5 @@ jobs: run: taplo --version || cargo install taplo-cli - name: Run taplo run: taplo fmt --check --diff + - name: Ensure Cargo.lock not modified by build + run: git diff --exit-code Cargo.lock diff --git a/Cargo.lock b/Cargo.lock index d3cb607be..c837a88ee 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -939,7 +939,7 @@ dependencies = [ [[package]] name = "ceno_crypto_primitives" version = "0.1.0" -source = "git+https://github.com/scroll-tech/ceno#4a9dff21fd408e93c21edb6e874a09b0171b0c8b" +source = "git+https://github.com/scroll-tech/ceno#050108047aad24101fcb010da4e7d29e9d72678a" dependencies = [ "ceno_syscall 0.1.0 (git+https://github.com/scroll-tech/ceno)", "elliptic-curve", @@ -1013,7 +1013,7 @@ version = "0.1.0" [[package]] name = "ceno_syscall" version = "0.1.0" -source = "git+https://github.com/scroll-tech/ceno#4a9dff21fd408e93c21edb6e874a09b0171b0c8b" +source = "git+https://github.com/scroll-tech/ceno#050108047aad24101fcb010da4e7d29e9d72678a" [[package]] name = "ceno_zkvm" @@ -1851,7 +1851,7 @@ dependencies = [ "ceno_syscall 0.1.0", "getrandom 0.3.2", "rand 0.8.5", - "revm-precompile 28.1.0", + "revm-precompile 28.1.1", "rkyv", "substrate-bn 0.6.0 (registry+https://github.com/rust-lang/crates.io-index)", "substrate-bn 0.6.0 (git+https://github.com/scroll-tech/bn?branch=ceno)", @@ -3874,9 +3874,9 @@ dependencies = [ [[package]] name = "revm-precompile" -version = "28.1.0" +version = "28.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "176169b39beb1f57b11f2ea3900c404b8498a56dfd8394e66f4d24f66cea368e" +checksum = "e57aadd7a2087705f653b5aaacc8ad4f8e851f5d330661e3f4c43b5475bbceae" dependencies = [ "ark-bls12-381", "ark-bn254", @@ -3888,7 +3888,7 @@ dependencies = [ "cfg-if", "k256 0.13.4 (registry+https://github.com/rust-lang/crates.io-index)", "p256", - "revm-primitives 21.0.0", + "revm-primitives 21.0.1", "ripemd", "sha2 0.10.9", ] @@ -3907,9 +3907,9 @@ dependencies = [ [[package]] name = "revm-primitives" -version = "21.0.0" +version = "21.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "38271b8b85f00154bdcf9f2ab0a3ec7a8100377d2c7a0d8eb23e19389b42c795" +checksum = "536f30e24c3c2bf0d3d7d20fa9cf99b93040ed0f021fd9301c78cddb0dacda13" dependencies = [ "alloy-primitives", "num_enum 0.7.4", diff --git a/ceno_zkvm/src/scheme/mock_prover.rs b/ceno_zkvm/src/scheme/mock_prover.rs index 028f844a6..911649e12 100644 --- a/ceno_zkvm/src/scheme/mock_prover.rs +++ b/ceno_zkvm/src/scheme/mock_prover.rs @@ -1147,7 +1147,7 @@ Hints: .into() }; - for ((w_rlc_expr, annotation), _) in (cs + for ((w_rlc_expr, annotation), (ram_type_expr, _)) in (cs .w_expressions .iter() .chain(cs.w_table_expressions.iter().map(|expr| &expr.expr))) @@ -1157,8 +1157,19 @@ Hints: .chain(cs.w_table_expressions_namespace_map.iter()), ) .zip_eq(cs.w_ram_types.iter()) - .filter(|((_, _), (ram_type, _))| *ram_type == $ram_type) { + let ram_type_mle = wit_infer_by_expr( + ram_type_expr, + cs.num_witin, + cs.num_structural_witin, + cs.num_fixed as WitnessId, + fixed, + witness, + structural_witness, + &pi_mles, + &challenges, + ); + let ram_type_vec = ram_type_mle.get_ext_field_vec(); let write_rlc_records = wit_infer_by_expr( w_rlc_expr, cs.num_witin, @@ -1170,13 +1181,32 @@ Hints: &pi_mles, &challenges, ); + let w_selector_vec = w_selector.get_base_field_vec(); let write_rlc_records = - filter_mle_by_selector_mle(write_rlc_records, w_selector.clone()); + filter_mle_by_predicate(write_rlc_records, |i, _v| { + ram_type_vec[i] == E::from_canonical_u32($ram_type as u32) + && w_selector_vec[i] == E::BaseField::ONE + }); + if write_rlc_records.is_empty() { + continue; + } let mut records = vec![]; + let mut writes_within_expr_dedup = HashSet::new(); for (row, record_rlc) in enumerate(write_rlc_records) { // TODO: report error - assert_eq!(writes.insert(record_rlc), true); + assert_eq!( + writes_within_expr_dedup.insert(record_rlc), + true, + "within expression write duplicated on RAMType {:?}", + $ram_type + ); + assert_eq!( + writes.insert(record_rlc), + true, + "crossing-chip write duplicated on RAMType {:?}", + $ram_type + ); records.push((record_rlc, row)); } writes_grp_by_annotations @@ -1212,7 +1242,7 @@ Hints: ) .into() }; - for ((r_rlc_expr, annotation), (_, r_exprs)) in (cs + for ((r_rlc_expr, annotation), (ram_type_expr, r_exprs)) in (cs .r_expressions .iter() .chain(cs.r_table_expressions.iter().map(|expr| &expr.expr))) @@ -1222,8 +1252,19 @@ Hints: .chain(cs.r_table_expressions_namespace_map.iter()), ) .zip_eq(cs.r_ram_types.iter()) - .filter(|((_, _), (ram_type, _))| *ram_type == $ram_type) { + let ram_type_mle = wit_infer_by_expr( + ram_type_expr, + cs.num_witin, + cs.num_structural_witin, + cs.num_fixed as WitnessId, + fixed, + witness, + structural_witness, + &pi_mles, + &challenges, + ); + let ram_type_vec = ram_type_mle.get_ext_field_vec(); let read_records = wit_infer_by_expr( r_rlc_expr, cs.num_witin, @@ -1235,8 +1276,14 @@ Hints: &pi_mles, &challenges, ); - let read_records = - filter_mle_by_selector_mle(read_records, r_selector.clone()); + let r_selector_vec = r_selector.get_base_field_vec(); + let read_records = filter_mle_by_predicate(read_records, |i, _v| { + ram_type_vec[i] == E::from_canonical_u32($ram_type as u32) + && r_selector_vec[i] == E::BaseField::ONE + }); + if read_records.is_empty() { + continue; + } if $ram_type == RAMType::GlobalState { // r_exprs = [GlobalState, pc, timestamp] @@ -1269,9 +1316,21 @@ Hints: }; let mut records = vec![]; + let mut reads_within_expr_dedup = HashSet::new(); for (row, record) in enumerate(read_records) { // TODO: return error - assert_eq!(reads.insert(record), true); + assert_eq!( + reads_within_expr_dedup.insert(record), + true, + "within expression read duplicated on RAMType {:?}", + $ram_type + ); + assert_eq!( + reads.insert(record), + true, + "crossing-chip read duplicated on RAMType {:?}", + $ram_type + ); records.push((record, row)); } reads_grp_by_annotations @@ -1467,6 +1526,19 @@ fn print_errors( } } +fn filter_mle_by_predicate(target_mle: ArcMultilinearExtension, mut predicate: F) -> Vec +where + E: ExtensionField, + F: FnMut(usize, &E) -> bool, +{ + target_mle + .get_ext_field_vec() + .iter() + .enumerate() + .filter_map(|(i, v)| if predicate(i, v) { Some(*v) } else { None }) + .collect_vec() +} + fn filter_mle_by_selector_mle( target_mle: ArcMultilinearExtension, selector: ArcMultilinearExtension, @@ -1487,7 +1559,6 @@ fn filter_mle_by_selector_mle( #[cfg(test)] mod tests { - use super::*; use crate::{ ROMType, diff --git a/gkr_iop/src/circuit_builder.rs b/gkr_iop/src/circuit_builder.rs index e4129bfe8..395b9e6c9 100644 --- a/gkr_iop/src/circuit_builder.rs +++ b/gkr_iop/src/circuit_builder.rs @@ -108,14 +108,14 @@ pub struct ConstraintSystem { pub r_expressions_namespace_map: Vec, // for each read expression we store its ram type and original value before doing RLC // the original value will be used for debugging - pub r_ram_types: Vec<(RAMType, Vec>)>, + pub r_ram_types: Vec<(Expression, Vec>)>, pub w_selector: Option>, pub w_expressions: Vec>, pub w_expressions_namespace_map: Vec, // for each write expression we store its ram type and original value before doing RLC // the original value will be used for debugging - pub w_ram_types: Vec<(RAMType, Vec>)>, + pub w_ram_types: Vec<(Expression, Vec>)>, /// init/final ram expression pub r_table_expressions: Vec>, @@ -329,12 +329,27 @@ impl ConstraintSystem { N: FnOnce() -> NR, { let rlc_record = self.rlc_chip_record(record.clone()); - assert_eq!( - rlc_record.degree(), - 1, - "rlc record degree {} != 1", - rlc_record.degree() - ); + self.r_table_rlc_record( + name_fn, + (ram_type as u64).into(), + table_spec, + record, + rlc_record, + ) + } + + pub fn r_table_rlc_record( + &mut self, + name_fn: N, + ram_type: Expression, + table_spec: SetTableSpec, + record: Vec>, + rlc_record: Expression, + ) -> Result<(), CircuitBuilderError> + where + NR: Into, + N: FnOnce() -> NR, + { self.r_table_expressions.push(SetTableExpression { expr: rlc_record, table_spec, @@ -358,12 +373,27 @@ impl ConstraintSystem { N: FnOnce() -> NR, { let rlc_record = self.rlc_chip_record(record.clone()); - assert_eq!( - rlc_record.degree(), - 1, - "rlc record degree {} != 1", - rlc_record.degree() - ); + self.w_table_rlc_record( + name_fn, + (ram_type as u64).into(), + table_spec, + record, + rlc_record, + ) + } + + pub fn w_table_rlc_record( + &mut self, + name_fn: N, + ram_type: Expression, + table_spec: SetTableSpec, + record: Vec>, + rlc_record: Expression, + ) -> Result<(), CircuitBuilderError> + where + NR: Into, + N: FnOnce() -> NR, + { self.w_table_expressions.push(SetTableExpression { expr: rlc_record, table_spec, @@ -387,7 +417,7 @@ impl ConstraintSystem { self.r_expressions_namespace_map.push(path); // Since r_expression is RLC(record) and when we're debugging // it's helpful to recover the value of record itself. - self.r_ram_types.push((ram_type, record)); + self.r_ram_types.push(((ram_type as u64).into(), record)); Ok(()) } @@ -401,7 +431,7 @@ impl ConstraintSystem { self.w_expressions.push(rlc_record); let path = self.ns.compute_path(name_fn().into()); self.w_expressions_namespace_map.push(path); - self.w_ram_types.push((ram_type, record)); + self.w_ram_types.push(((ram_type as u64).into(), record)); Ok(()) } @@ -579,6 +609,22 @@ impl<'a, E: ExtensionField> CircuitBuilder<'a, E> { .r_table_record(name_fn, ram_type, table_spec, record) } + pub fn r_table_rlc_record( + &mut self, + name_fn: N, + ram_type: Expression, + table_spec: SetTableSpec, + record: Vec>, + rlc_record: Expression, + ) -> Result<(), CircuitBuilderError> + where + NR: Into, + N: FnOnce() -> NR, + { + self.cs + .r_table_rlc_record(name_fn, ram_type, table_spec, record, rlc_record) + } + pub fn w_table_record( &mut self, name_fn: N, @@ -594,6 +640,22 @@ impl<'a, E: ExtensionField> CircuitBuilder<'a, E> { .w_table_record(name_fn, ram_type, table_spec, record) } + pub fn w_table_rlc_record( + &mut self, + name_fn: N, + ram_type: Expression, + table_spec: SetTableSpec, + record: Vec>, + rlc_record: Expression, + ) -> Result<(), CircuitBuilderError> + where + NR: Into, + N: FnOnce() -> NR, + { + self.cs + .w_table_rlc_record(name_fn, ram_type, table_spec, record, rlc_record) + } + pub fn read_record( &mut self, name_fn: N,