diff --git a/.github/workflows/integration.yml b/.github/workflows/integration.yml new file mode 100644 index 000000000..598940d22 --- /dev/null +++ b/.github/workflows/integration.yml @@ -0,0 +1,62 @@ +name: Integrations + +on: + merge_group: + pull_request: + types: [synchronize, opened, reopened, ready_for_review] + push: + branches: + - master + +jobs: + skip_check: + runs-on: ubuntu-latest + outputs: + should_skip: ${{ steps.skip_check.outputs.should_skip }} + steps: + - id: skip_check + uses: fkirc/skip-duplicate-actions@v5 + with: + cancel_others: 'true' + concurrent_skipping: 'same_content_newer' + paths_ignore: '["**/README.md"]' + do_not_skip: '["pull_request", "workflow_dispatch", "schedule", "merge_group"]' + + lints: + needs: [skip_check] + if: | + github.event.pull_request.draft == false && + (github.event.action == 'ready_for_review' || needs.skip_check.outputs.should_skip != 'true') + + name: Various lints + timeout-minutes: 30 + runs-on: ubuntu-latest + + strategy: + matrix: + target: [x86_64-unknown-linux-gnu, riscv32im-unknown-none-elf] + # Exclude the riscv32im-unknown-none-elf target + exclude: + - target: riscv32im-unknown-none-elf + + steps: + - uses: actions/checkout@v2 + - name: Cargo cache + uses: actions/cache@v3 + with: + path: | + ~/.cargo/bin/ + ~/.cargo/registry/index/ + ~/.cargo/registry/cache/ + ~/.cargo/git/db/ + target/ + key: integration-${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} + + - name: Run example + uses: actions-rs/cargo@v1 + env: + RAYON_NUM_THREADS: 2 + with: + command: run + args: --package ceno_zkvm --example riscv_add --target ${{ matrix.target }} -- --start 10 --end 11 + diff --git a/.github/workflows/lints.yml b/.github/workflows/lints.yml index be3ee0e67..7215344be 100644 --- a/.github/workflows/lints.yml +++ b/.github/workflows/lints.yml @@ -1,6 +1,5 @@ name: Lints -# We only run these lints on trial-merges of PRs to reduce noise. on: merge_group: pull_request: diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index a1a6b5aba..5a51be8c1 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -1,6 +1,5 @@ name: Tests -# We only run these lints on trial-merges of PRs to reduce noise. on: merge_group: pull_request: diff --git a/Cargo.lock b/Cargo.lock index b69ffa929..3c030bf42 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -57,11 +57,54 @@ version = "0.1.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4b46cbb362ab8752921c97e041f5e366ee6297bd428a31275b9fcf1e380f7299" +[[package]] +name = "anstream" +version = "0.6.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "64e15c1ab1f89faffbf04a634d5e1962e9074f2741eef6d97f3c4e322426d526" +dependencies = [ + "anstyle", + "anstyle-parse", + "anstyle-query", + "anstyle-wincon", + "colorchoice", + "is_terminal_polyfill", + "utf8parse", +] + [[package]] name = "anstyle" -version = "1.0.6" +version = "1.0.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8901269c6307e8d93993578286ac0edf7f195079ffff5ebdeea6a59ffb7e36bc" +checksum = "1bec1de6f59aedf83baf9ff929c98f2ad654b97c9510f4e70cf6f661d49fd5b1" + +[[package]] +name = "anstyle-parse" +version = "0.2.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "eb47de1e80c2b463c735db5b217a0ddc39d612e7ac9e2e96a5aed1f57616c1cb" +dependencies = [ + "utf8parse", +] + +[[package]] +name = "anstyle-query" +version = "1.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6d36fc52c7f6c869915e99412912f22093507da8d9e942ceaf66fe4b7c14422a" +dependencies = [ + "windows-sys 0.52.0", +] + +[[package]] +name = "anstyle-wincon" +version = "3.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5bf74e1b6e971609db8ca7a9ce79fd5768ab6ae46441c572e46cf596f59e57f8" +dependencies = [ + "anstyle", + "windows-sys 0.52.0", +] [[package]] name = "anyhow" @@ -285,6 +328,7 @@ dependencies = [ "ark-std", "ceno_emul", "cfg-if", + "clap", "const_env", "criterion", "ff", @@ -353,21 +397,36 @@ dependencies = [ [[package]] name = "clap" -version = "4.5.4" +version = "4.5.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "90bc066a67923782aa8515dbaea16946c5bcc5addbd668bb80af688e53e548a0" +checksum = "3e5a21b8495e732f1b3c364c9949b201ca7bae518c502c80256c96ad79eaf6ac" dependencies = [ "clap_builder", + "clap_derive", ] [[package]] name = "clap_builder" -version = "4.5.2" +version = "4.5.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ae129e2e766ae0ec03484e609954119f123cc1fe650337e155d03b022f24f7b4" +checksum = "8cf2dd12af7a047ad9d6da2b6b249759a22a7abc0f474c1dae1777afa4b21a73" dependencies = [ + "anstream", "anstyle", "clap_lex", + "strsim", +] + +[[package]] +name = "clap_derive" +version = "4.5.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "501d359d5f3dcaf6ecdeee48833ae73ec6e42723a1e52419c79abf9507eec0a0" +dependencies = [ + "heck 0.5.0", + "proc-macro2", + "quote", + "syn 2.0.49", ] [[package]] @@ -376,6 +435,12 @@ version = "0.7.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "98cc8fbded0c607b7ba9dd60cd98df59af97e84d24e49c8557331cfc26d301ce" +[[package]] +name = "colorchoice" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d3fd119d74b830634cea2a0f58bbd0d54540518a14397557951e79340abc28c0" + [[package]] name = "colored" version = "2.1.0" @@ -853,6 +918,12 @@ version = "0.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8" +[[package]] +name = "heck" +version = "0.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" + [[package]] name = "hermit-abi" version = "0.1.19" @@ -931,6 +1002,12 @@ dependencies = [ "windows-sys 0.52.0", ] +[[package]] +name = "is_terminal_polyfill" +version = "1.70.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7943c866cc5cd64cbc25b2e01621d07fa8eb2a1a23160ee81ce38704e97b8ecf" + [[package]] name = "itertools" version = "0.10.5" @@ -1834,6 +1911,12 @@ version = "0.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9091b6114800a5f2141aee1d1b9d6ca3592ac062dc5decb3764ec5895a47b4eb" +[[package]] +name = "strsim" +version = "0.11.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f" + [[package]] name = "strum" version = "0.25.0" @@ -1852,7 +1935,7 @@ version = "0.25.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "23dc1fa9ac9c169a78ba62f0b841814b7abae11bdd047b9c58f893439e309ea0" dependencies = [ - "heck", + "heck 0.4.1", "proc-macro2", "quote", "rustversion", @@ -1865,7 +1948,7 @@ version = "0.26.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7a3417fc93d76740d974a01654a09777cb500428cc874ca9f45edfe0c4d4cd18" dependencies = [ - "heck", + "heck 0.4.1", "proc-macro2", "quote", "rustversion", @@ -2141,6 +2224,12 @@ dependencies = [ "syn 1.0.109", ] +[[package]] +name = "utf8parse" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821" + [[package]] name = "uuid" version = "1.8.0" diff --git a/ceno_zkvm/Cargo.toml b/ceno_zkvm/Cargo.toml index 387992955..6bc38936b 100644 --- a/ceno_zkvm/Cargo.toml +++ b/ceno_zkvm/Cargo.toml @@ -30,6 +30,7 @@ tracing = "0.1.40" rand = "0.8" thread_local = "1.1.8" generic_static = "0.2.0" +clap = { version = "4.5.17", features = ["derive"] } [dev-dependencies] pprof = { version = "0.13", features = ["flamegraph"]} diff --git a/ceno_zkvm/benches/riscv_add.rs b/ceno_zkvm/benches/riscv_add.rs index aa05b218f..c1bb982f9 100644 --- a/ceno_zkvm/benches/riscv_add.rs +++ b/ceno_zkvm/benches/riscv_add.rs @@ -2,9 +2,10 @@ use std::time::{Duration, Instant}; use ark_std::test_rng; use ceno_zkvm::{ - circuit_builder::{CircuitBuilder, ConstraintSystem}, + self, instructions::{riscv::addsub::AddInstruction, Instruction}, scheme::prover::ZKVMProver, + structs::{ZKVMConstraintSystem, ZKVMFixedTraces}, }; use const_env::from_env; use criterion::*; @@ -62,11 +63,22 @@ fn bench_add(c: &mut Criterion) { RAYON_NUM_THREADS } }; - let mut cs = ConstraintSystem::new(|| "risv_add"); - let mut circuit_builder = CircuitBuilder::::new(&mut cs); - let _ = AddInstruction::construct_circuit(&mut circuit_builder); - let pk = cs.key_gen(None); - let num_witin = pk.get_cs().num_witin; + let mut zkvm_cs = ZKVMConstraintSystem::default(); + let _ = zkvm_cs.register_opcode_circuit::>(); + let mut zkvm_fixed_traces = ZKVMFixedTraces::default(); + zkvm_fixed_traces.register_opcode_circuit::>(&zkvm_cs); + + let pk = zkvm_cs + .clone() + .key_gen(zkvm_fixed_traces) + .expect("keygen failed"); + + let circuit_pk = pk + .circuit_pks + .get(&AddInstruction::::name()) + .unwrap() + .clone(); + let num_witin = circuit_pk.get_cs().num_witin; let prover = ZKVMProver::new(pk); let mut transcript = Transcript::new(b"riscv"); @@ -101,6 +113,7 @@ fn bench_add(c: &mut Criterion) { let timer = Instant::now(); let _ = prover .create_opcode_proof( + &circuit_pk, wits_in, num_instances, max_threads, diff --git a/ceno_zkvm/examples/riscv_add.rs b/ceno_zkvm/examples/riscv_add.rs index 1f9b905b9..773fbcf01 100644 --- a/ceno_zkvm/examples/riscv_add.rs +++ b/ceno_zkvm/examples/riscv_add.rs @@ -2,6 +2,7 @@ use std::time::Instant; use ark_std::test_rng; use ceno_zkvm::{instructions::riscv::addsub::AddInstruction, scheme::prover::ZKVMProver}; +use clap::Parser; use const_env::from_env; use ceno_emul::{ByteAddr, InsnKind::ADD, StepRecord, VMState, CENO_PLATFORM}; @@ -26,6 +27,7 @@ const RAYON_NUM_THREADS: usize = 8; // - x2 is initialized to -1, // - x3 is initialized to loop bound. // we use x4 to hold the acc_sum. +#[allow(clippy::unusual_byte_groupings)] const PROGRAM_ADD_LOOP: [u32; 4] = [ // func7 rs2 rs1 f3 rd opcode 0b_0000000_00100_00001_000_00100_0110011, // add x4, x4, x1 <=> addi x4, x4, 1 @@ -34,7 +36,21 @@ const PROGRAM_ADD_LOOP: [u32; 4] = [ 0b_000000000000_00000_000_00000_1110011, // ecall halt ]; +/// Simple program to greet a person +#[derive(Parser, Debug)] +#[command(version, about, long_about = None)] +struct Args { + /// start round + #[arg(short, long, default_value_t = 8)] + start: u8, + + /// end round + #[arg(short, long, default_value_t = 22)] + end: u8, +} + fn main() { + let args = Args::parse(); type E = GoldilocksExt2; let max_threads = { @@ -90,8 +106,8 @@ fn main() { let prover = ZKVMProver::new(pk); let verifier = ZKVMVerifier::new(vk); - for instance_num_vars in 8..22 { - let num_instances = 1 << instance_num_vars; + for instance_num_vars in args.start..args.end { + let step_loop = 1 << (instance_num_vars - 1); // 1 step in loop contribute to 2 add instance let mut vm = VMState::new(CENO_PLATFORM); let pc_start = ByteAddr(CENO_PLATFORM.pc_start()).waddr(); @@ -99,7 +115,7 @@ fn main() { // vm.x4 += vm.x1 vm.init_register_unsafe(1usize, 1); vm.init_register_unsafe(2usize, u32::MAX); // -1 in two's complement - vm.init_register_unsafe(3usize, num_instances as u32); + vm.init_register_unsafe(3usize, step_loop as u32); for (i, inst) in PROGRAM_ADD_LOOP.iter().enumerate() { vm.init_memory(pc_start + i, *inst); } @@ -133,17 +149,17 @@ fn main() { .create_proof(zkvm_witness, max_threads, &mut transcript, &real_challenges) .expect("create_proof failed"); + println!( + "AddInstruction::create_proof, instance_num_vars = {}, time = {}", + instance_num_vars, + timer.elapsed().as_secs_f64() + ); + let mut transcript = Transcript::new(b"riscv"); assert!( verifier .verify_proof(zkvm_proof, &mut transcript, &real_challenges) .expect("verify proof return with error"), ); - - println!( - "AddInstruction::create_proof, instance_num_vars = {}, time = {}", - instance_num_vars, - timer.elapsed().as_secs_f64() - ); } } diff --git a/ceno_zkvm/src/instructions/riscv/addsub.rs b/ceno_zkvm/src/instructions/riscv/addsub.rs index 670a247d9..2bccb8576 100644 --- a/ceno_zkvm/src/instructions/riscv/addsub.rs +++ b/ceno_zkvm/src/instructions/riscv/addsub.rs @@ -93,12 +93,6 @@ fn add_sub_gadget( let rs2_id = circuit_builder.create_witin(|| "rs2_id")?; let rd_id = circuit_builder.create_witin(|| "rd_id")?; - // TODO remove me, this is just for testing degree > 1 sumcheck in main constraints - circuit_builder.require_zero( - || "test_degree > 1", - rs1_id.expr() * rs1_id.expr() - rs1_id.expr() * rs1_id.expr(), - )?; - let prev_rs1_ts = circuit_builder.create_witin(|| "prev_rs1_ts")?; let prev_rs2_ts = circuit_builder.create_witin(|| "prev_rs2_ts")?; let prev_rd_ts = circuit_builder.create_witin(|| "prev_rd_ts")?; @@ -145,6 +139,87 @@ fn add_sub_gadget( }) } +fn add_sub_assignment( + config: &InstructionConfig, + instance: &mut [MaybeUninit], + lk_multiplicity: &mut LkMultiplicity, + step: &StepRecord, +) -> Result<(), ZKVMError> { + set_val!(instance, config.pc, step.pc().before.0 as u64); + set_val!(instance, config.ts, step.cycle()); + let addend_1 = UIntValue::new_unchecked(step.rs2().unwrap().value); + let rd_prev = UIntValue::new_unchecked(step.rd().unwrap().value.before); + config + .prev_rd_value + .assign_limbs(instance, rd_prev.u16_fields()); + + config + .addend_1 + .assign_limbs(instance, addend_1.u16_fields()); + + if IS_ADD { + // addend_0 + addend_1 = outcome + let addend_0 = UIntValue::new_unchecked(step.rs1().unwrap().value); + config + .addend_0 + .assign_limbs(instance, addend_0.u16_fields()); + let (_, outcome_carries) = addend_0.add(&addend_1, lk_multiplicity, true); + config.outcome.assign_carries( + instance, + outcome_carries + .into_iter() + .map(|carry| E::BaseField::from(carry as u64)) + .collect_vec(), + ); + } else { + // addend_0 = outcome + addend_1 + let outcome = UIntValue::new(step.rd().unwrap().value.after, lk_multiplicity); + config.outcome.assign_limbs(instance, outcome.u16_fields()); + let (_, addend_0_carries) = addend_1.add(&outcome, lk_multiplicity, true); + config.addend_0.assign_carries( + instance, + addend_0_carries + .into_iter() + .map(|carry| E::BaseField::from(carry as u64)) + .collect_vec(), + ); + } + set_val!(instance, config.rs1_id, step.insn().rs1() as u64); + set_val!(instance, config.rs2_id, step.insn().rs2() as u64); + set_val!(instance, config.rd_id, step.insn().rd() as u64); + ExprLtInput { + lhs: step.rs1().unwrap().previous_cycle, + rhs: step.cycle(), + } + .assign(instance, &config.lt_rs1_cfg, lk_multiplicity); + ExprLtInput { + lhs: step.rs2().unwrap().previous_cycle, + rhs: step.cycle() + 1, + } + .assign(instance, &config.lt_rs2_cfg, lk_multiplicity); + ExprLtInput { + lhs: step.rd().unwrap().previous_cycle, + rhs: step.cycle() + 2, + } + .assign(instance, &config.lt_prev_ts_cfg, lk_multiplicity); + set_val!( + instance, + config.prev_rs1_ts, + step.rs1().unwrap().previous_cycle + ); + set_val!( + instance, + config.prev_rs2_ts, + step.rs2().unwrap().previous_cycle + ); + set_val!( + instance, + config.prev_rd_ts, + step.rd().unwrap().previous_cycle + ); + Ok(()) +} + impl Instruction for AddInstruction { // const NAME: &'static str = "ADD"; fn name() -> String { @@ -164,54 +239,7 @@ impl Instruction for AddInstruction { lk_multiplicity: &mut LkMultiplicity, step: &StepRecord, ) -> Result<(), ZKVMError> { - // TODO use fields from step - set_val!(instance, config.pc, 1); - set_val!(instance, config.ts, 3); - let addend_0 = UIntValue::new_unchecked(step.rs1().unwrap().value); - let addend_1 = UIntValue::new_unchecked(step.rs2().unwrap().value); - let rd_prev = UIntValue::new_unchecked(step.rd().unwrap().value.before); - config - .prev_rd_value - .assign_limbs(instance, rd_prev.u16_fields()); - config - .addend_0 - .assign_limbs(instance, addend_0.u16_fields()); - config - .addend_1 - .assign_limbs(instance, addend_1.u16_fields()); - let (_, carries) = addend_0.add(&addend_1, lk_multiplicity, true); - config.outcome.assign_carries( - instance, - carries - .into_iter() - .map(|carry| E::BaseField::from(carry as u64)) - .collect_vec(), - ); - // TODO #167 - set_val!(instance, config.rs1_id, 2); - set_val!(instance, config.rs2_id, 2); - set_val!(instance, config.rd_id, 2); - set_val!(instance, config.prev_rs1_ts, 2); - set_val!(instance, config.prev_rs2_ts, 2); - set_val!(instance, config.prev_rd_ts, 2); - - ExprLtInput { - lhs: 2, // rs1 - rhs: 3, // cur_ts - } - .assign(instance, &config.lt_rs1_cfg); - ExprLtInput { - lhs: 2, // rs2 - rhs: 4, // cur_ts - } - .assign(instance, &config.lt_rs2_cfg); - ExprLtInput { - lhs: 2, // rd - rhs: 5, // cur_ts - } - .assign(instance, &config.lt_prev_ts_cfg); - - Ok(()) + add_sub_assignment::<_, true>(config, instance, lk_multiplicity, step) } } @@ -231,37 +259,10 @@ impl Instruction for SubInstruction { fn assign_instance( config: &Self::InstructionConfig, instance: &mut [MaybeUninit], - _lk_multiplicity: &mut LkMultiplicity, - _step: &StepRecord, + lk_multiplicity: &mut LkMultiplicity, + step: &StepRecord, ) -> Result<(), ZKVMError> { - // TODO use field from step - set_val!(instance, config.pc, _step.pc().before.0 as u64); - set_val!(instance, config.ts, 2); - config.prev_rd_value.wits_in().map(|prev_rd_value| { - set_val!(instance, prev_rd_value[0], 4); - set_val!(instance, prev_rd_value[1], 4); - }); - config.addend_0.wits_in().map(|addend_0| { - set_val!(instance, addend_0[0], 4); - set_val!(instance, addend_0[1], 4); - }); - config.addend_1.wits_in().map(|addend_1| { - set_val!(instance, addend_1[0], 4); - set_val!(instance, addend_1[1], 4); - }); - // TODO #174 - config.outcome.carries.as_ref().map(|carry| { - set_val!(instance, carry[0], 4); - set_val!(instance, carry[1], 0); - }); - // TODO #167 - set_val!(instance, config.rs1_id, 2); - set_val!(instance, config.rs2_id, 2); - set_val!(instance, config.rd_id, 2); - set_val!(instance, config.prev_rs1_ts, 2); - set_val!(instance, config.prev_rs2_ts, 2); - set_val!(instance, config.prev_rd_ts, 2); - Ok(()) + add_sub_assignment::<_, false>(config, instance, lk_multiplicity, step) } } @@ -274,11 +275,11 @@ mod test { use crate::{ circuit_builder::{CircuitBuilder, ConstraintSystem}, - instructions::Instruction, + instructions::{riscv::constants::PC_STEP_SIZE, Instruction}, scheme::mock_prover::MockProver, }; - use super::AddInstruction; + use super::{AddInstruction, SubInstruction}; #[test] #[allow(clippy::option_map_unit_fn)] @@ -300,6 +301,11 @@ mod test { &config, cb.cs.num_witin as usize, vec![StepRecord { + cycle: 3, + pc: Change { + before: 2u32.into(), + after: (2u32 + PC_STEP_SIZE as u32).into(), + }, rs1: Some(ReadOp { addr: 2.into(), value: 11u32, @@ -314,7 +320,7 @@ mod test { addr: 4.into(), value: Change { before: 0u32, - after: 9u32, + after: 11u32.wrapping_add(0xfffffffeu32), }, previous_cycle: 0, }), @@ -355,6 +361,11 @@ mod test { &config, cb.cs.num_witin as usize, vec![StepRecord { + cycle: 3, + pc: Change { + before: 2u32.into(), + after: (2u32 + PC_STEP_SIZE as u32).into(), + }, rs1: Some(ReadOp { addr: 2.into(), value: u32::MAX - 1, @@ -369,7 +380,7 @@ mod test { addr: 4.into(), value: Change { before: 0u32, - after: u32::MAX - 2, + after: (u32::MAX - 1).wrapping_add(u32::MAX - 1), }, previous_cycle: 0, }), @@ -386,7 +397,127 @@ mod test { .into_iter() .map(|v| v.into()) .collect_vec(), - Some([100.into(), 100000.into()]), + None, + ); + } + + #[test] + #[allow(clippy::option_map_unit_fn)] + fn test_opcode_sub() { + let mut cs = ConstraintSystem::::new(|| "riscv"); + let mut cb = CircuitBuilder::new(&mut cs); + let config = cb + .namespace( + || "sub", + |cb| { + let config = SubInstruction::construct_circuit(cb); + Ok(config) + }, + ) + .unwrap() + .unwrap(); + + let (raw_witin, _) = SubInstruction::assign_instances( + &config, + cb.cs.num_witin as usize, + vec![StepRecord { + cycle: 3, + pc: Change { + before: 2u32.into(), + after: (2u32 + PC_STEP_SIZE as u32).into(), + }, + rs1: Some(ReadOp { + addr: 2.into(), + value: 11u32, + previous_cycle: 0, + }), + rs2: Some(ReadOp { + addr: 3.into(), + value: 2u32, + previous_cycle: 0, + }), + rd: Some(WriteOp { + addr: 4.into(), + value: Change { + before: 0u32, + after: 11u32.wrapping_sub(2u32), + }, + previous_cycle: 0, + }), + ..Default::default() + }], + ) + .unwrap(); + + MockProver::assert_satisfied( + &mut cb, + &raw_witin + .de_interleaving() + .into_mles() + .into_iter() + .map(|v| v.into()) + .collect_vec(), + None, + ); + } + + #[test] + #[allow(clippy::option_map_unit_fn)] + fn test_opcode_sub_underflow() { + let mut cs = ConstraintSystem::::new(|| "riscv"); + let mut cb = CircuitBuilder::new(&mut cs); + let config = cb + .namespace( + || "sub", + |cb| { + let config = SubInstruction::construct_circuit(cb); + Ok(config) + }, + ) + .unwrap() + .unwrap(); + + let (raw_witin, _) = SubInstruction::assign_instances( + &config, + cb.cs.num_witin as usize, + vec![StepRecord { + cycle: 3, + pc: Change { + before: 2u32.into(), + after: (2u32 + PC_STEP_SIZE as u32).into(), + }, + rs1: Some(ReadOp { + addr: 2.into(), + value: 3u32, + previous_cycle: 0, + }), + rs2: Some(ReadOp { + addr: 3.into(), + value: 11u32, + previous_cycle: 0, + }), + rd: Some(WriteOp { + addr: 4.into(), + value: Change { + before: 0u32, + after: 3u32.wrapping_sub(11u32), + }, + previous_cycle: 0, + }), + ..Default::default() + }], + ) + .unwrap(); + + MockProver::assert_satisfied( + &mut cb, + &raw_witin + .de_interleaving() + .into_mles() + .into_iter() + .map(|v| v.into()) + .collect_vec(), + None, ); } } diff --git a/ceno_zkvm/src/instructions/riscv/blt.rs b/ceno_zkvm/src/instructions/riscv/blt.rs index da077023b..30f4cc333 100644 --- a/ceno_zkvm/src/instructions/riscv/blt.rs +++ b/ceno_zkvm/src/instructions/riscv/blt.rs @@ -60,6 +60,7 @@ impl BltInput { &self, config: &InstructionConfig, instance: &mut [MaybeUninit], + lk_multiplicity: &mut LkMultiplicity, ) { assert!(!self.lhs_limb8.is_empty() && (self.lhs_limb8.len() == self.rhs_limb8.len())); // TODO: add boundary check for witin @@ -108,12 +109,12 @@ impl BltInput { lhs: self.prev_rs1_ts as u64, rhs: self.ts as u64, } - .assign(instance, &config.lt_rs1_cfg); + .assign(instance, &config.lt_rs1_cfg, lk_multiplicity); ExprLtInput { lhs: self.prev_rs2_ts as u64, rhs: (self.ts + 1) as u64, } - .assign(instance, &config.lt_rs2_cfg); + .assign(instance, &config.lt_rs2_cfg, lk_multiplicity); } pub fn random() -> Self { @@ -223,12 +224,12 @@ impl Instruction for BltInstruction { fn assign_instance( config: &Self::InstructionConfig, instance: &mut [std::mem::MaybeUninit], - _lk_multiplicity: &mut LkMultiplicity, + lk_multiplicity: &mut LkMultiplicity, _step: &ceno_emul::StepRecord, ) -> Result<(), ZKVMError> { // take input from _step let input = BltInput::random(); - input.assign(config, instance); + input.assign(config, instance, lk_multiplicity); Ok(()) } } diff --git a/ceno_zkvm/src/instructions/riscv/config.rs b/ceno_zkvm/src/instructions/riscv/config.rs index 378a1a9b1..2396475cd 100644 --- a/ceno_zkvm/src/instructions/riscv/config.rs +++ b/ceno_zkvm/src/instructions/riscv/config.rs @@ -1,6 +1,6 @@ use std::mem::MaybeUninit; -use crate::{expression::WitIn, set_val, utils::i64_to_base}; +use crate::{expression::WitIn, set_val, utils::i64_to_base, witness::LkMultiplicity}; use goldilocks::SmallField; use itertools::Itertools; @@ -184,7 +184,12 @@ pub struct ExprLtInput { } impl ExprLtInput { - pub fn assign(&self, instance: &mut [MaybeUninit], config: &ExprLtConfig) { + pub fn assign( + &self, + instance: &mut [MaybeUninit], + config: &ExprLtConfig, + lkm: &mut LkMultiplicity, + ) { let is_lt = if let Some(is_lt_wit) = config.is_lt { let is_lt = self.lhs < self.rhs; set_val!(instance, is_lt_wit, is_lt as u64); @@ -197,7 +202,9 @@ impl ExprLtInput { let diff = if is_lt { 1u64 << u32::BITS } else { 0 } + self.lhs - self.rhs; config.diff.iter().enumerate().for_each(|(i, wit)| { // extract the 16 bit limb from diff and assign to instance - set_val!(instance, wit, (diff >> (i * u16::BITS as usize)) & 0xffff); + let val = (diff >> (i * u16::BITS as usize)) & 0xffff; + lkm.assert_ux::<16>(val); + set_val!(instance, wit, val); }); } } diff --git a/ceno_zkvm/src/scheme/mock_prover.rs b/ceno_zkvm/src/scheme/mock_prover.rs index 3b9a8afcc..55386ce8f 100644 --- a/ceno_zkvm/src/scheme/mock_prover.rs +++ b/ceno_zkvm/src/scheme/mock_prover.rs @@ -487,12 +487,11 @@ mod tests { expression::{ToExpr, WitIn}, instructions::riscv::config::{ExprLtConfig, ExprLtInput}, set_val, - witness::RowMajorMatrix, + witness::{LkMultiplicity, RowMajorMatrix}, }; use ff::Field; use goldilocks::{Goldilocks, GoldilocksExt2}; use multilinear_extensions::mle::{IntoMLE, IntoMLEs}; - use rayon::iter::{IndexedParallelIterator, IntoParallelIterator, ParallelIterator}; #[derive(Debug)] #[allow(dead_code)] @@ -649,6 +648,7 @@ mod tests { &self, instance: &mut [MaybeUninit], input: AssertLtCircuitInput, + lk_multiplicity: &mut LkMultiplicity, ) -> Result<(), ZKVMError> { set_val!(instance, self.a, input.a); set_val!(instance, self.b, input.b); @@ -656,7 +656,7 @@ mod tests { lhs: input.a, rhs: input.b, } - .assign(instance, &self.lt_wtns); + .assign(instance, &self.lt_wtns, lk_multiplicity); Ok(()) } @@ -665,14 +665,16 @@ mod tests { &self, num_witin: usize, instances: Vec, + lk_multiplicity: &mut LkMultiplicity, ) -> Result, ZKVMError> { let mut raw_witin = RowMajorMatrix::::new(instances.len(), num_witin); - let raw_witin_iter = raw_witin.par_iter_mut(); + let raw_witin_iter = raw_witin.iter_mut(); raw_witin_iter - .zip_eq(instances.into_par_iter()) - .map(|(instance, input)| self.assign_instance::(instance, input)) - .collect::>()?; + .zip_eq(instances.into_iter()) + .try_for_each(|(instance, input)| { + self.assign_instance::(instance, input, lk_multiplicity) + })?; Ok(raw_witin) } @@ -685,6 +687,7 @@ mod tests { let circuit = AssertLtCircuit::construct_circuit(&mut builder).unwrap(); + let mut lk_multiplicity = LkMultiplicity::default(); let raw_witin = circuit .assign_instances::( builder.cs.num_witin as usize, @@ -692,6 +695,7 @@ mod tests { AssertLtCircuitInput { a: 3, b: 5 }, AssertLtCircuitInput { a: 7, b: 11 }, ], + &mut lk_multiplicity, ) .unwrap(); @@ -713,6 +717,7 @@ mod tests { let mut builder = CircuitBuilder::::new(&mut cs); let circuit = AssertLtCircuit::construct_circuit(&mut builder).unwrap(); + let mut lk_multiplicity = LkMultiplicity::default(); let raw_witin = circuit .assign_instances::( builder.cs.num_witin as usize, @@ -726,6 +731,7 @@ mod tests { b: u32::MAX as u64 - 2, }, ], + &mut lk_multiplicity, ) .unwrap(); @@ -765,6 +771,7 @@ mod tests { &self, instance: &mut [MaybeUninit], input: LtCircuitInput, + lk_multiplicity: &mut LkMultiplicity, ) -> Result<(), ZKVMError> { set_val!(instance, self.a, input.a); set_val!(instance, self.b, input.b); @@ -772,7 +779,7 @@ mod tests { lhs: input.a, rhs: input.b, } - .assign(instance, &self.lt_wtns); + .assign(instance, &self.lt_wtns, lk_multiplicity); Ok(()) } @@ -781,14 +788,16 @@ mod tests { &self, num_witin: usize, instances: Vec, + lk_multiplicity: &mut LkMultiplicity, ) -> Result, ZKVMError> { let mut raw_witin = RowMajorMatrix::::new(instances.len(), num_witin); - let raw_witin_iter = raw_witin.par_iter_mut(); + let raw_witin_iter = raw_witin.iter_mut(); raw_witin_iter - .zip_eq(instances.into_par_iter()) - .map(|(instance, input)| self.assign_instance::(instance, input)) - .collect::>()?; + .zip_eq(instances.into_iter()) + .try_for_each(|(instance, input)| { + self.assign_instance::(instance, input, lk_multiplicity) + })?; Ok(raw_witin) } @@ -801,6 +810,7 @@ mod tests { let circuit = LtCircuit::construct_circuit(&mut builder).unwrap(); + let mut lk_multiplicity = LkMultiplicity::default(); let raw_witin = circuit .assign_instances::( builder.cs.num_witin as usize, @@ -808,6 +818,7 @@ mod tests { LtCircuitInput { a: 3, b: 5 }, LtCircuitInput { a: 7, b: 11 }, ], + &mut lk_multiplicity, ) .unwrap(); @@ -830,6 +841,7 @@ mod tests { let circuit = LtCircuit::construct_circuit(&mut builder).unwrap(); + let mut lk_multiplicity = LkMultiplicity::default(); let raw_witin = circuit .assign_instances::( builder.cs.num_witin as usize, @@ -843,6 +855,7 @@ mod tests { b: u32::MAX as u64 - 5, }, ], + &mut lk_multiplicity, ) .unwrap(); diff --git a/ceno_zkvm/src/structs.rs b/ceno_zkvm/src/structs.rs index c7c136d66..e2bbe0b56 100644 --- a/ceno_zkvm/src/structs.rs +++ b/ceno_zkvm/src/structs.rs @@ -245,7 +245,7 @@ impl ZKVMWitnesses { #[derive(Default)] pub struct ZKVMProvingKey { // pk for opcode and table circuits - pub(crate) circuit_pks: BTreeMap>, + pub circuit_pks: BTreeMap>, } impl ZKVMProvingKey { diff --git a/ceno_zkvm/src/uint.rs b/ceno_zkvm/src/uint.rs index a256cac00..c89aa329b 100644 --- a/ceno_zkvm/src/uint.rs +++ b/ceno_zkvm/src/uint.rs @@ -474,7 +474,6 @@ impl + Copy> UIntValue { mem::size_of::() / u16_bytes }; - #[allow(dead_code)] pub fn new(val: T, lkm: &mut LkMultiplicity) -> Self { let uint = UIntValue:: { val,