diff --git a/Cargo.lock b/Cargo.lock index d84685eb4..8174773aa 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -162,6 +162,21 @@ version = "0.22.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "72b3254f16251a8381aa12e40e3c4d2f0199f8c6508fbecb9d91f575e0fbb8c6" +[[package]] +name = "bit-set" +version = "0.5.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0700ddab506f33b20a03b13996eccd309a48e5ff77d0d95926aa0210fb4e95f1" +dependencies = [ + "bit-vec", +] + +[[package]] +name = "bit-vec" +version = "0.6.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "349f9b6a179ed607305526ca489b34ad0a41aed5f7980fa90eb03160b69598fb" + [[package]] name = "bitflags" version = "2.6.0" @@ -272,6 +287,7 @@ dependencies = [ "paste", "pprof2", "prettytable-rs", + "proptest", "rand", "rand_chacha", "rayon", @@ -694,6 +710,12 @@ dependencies = [ "static_assertions", ] +[[package]] +name = "fnv" +version = "1.0.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1" + [[package]] name = "funty" version = "2.0.0" @@ -970,6 +992,12 @@ version = "0.2.167" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "09d6582e104315a817dff97f75133544b2e094ee22447d2acf4a74e189ba06fc" +[[package]] +name = "libm" +version = "0.2.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8355be11b20d696c8f18f6cc018c4e372165b1fa8126cef092399c9951984ffa" + [[package]] name = "libredox" version = "0.1.3" @@ -1192,6 +1220,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "071dfc062690e90b734c0b2273ce72ad0ffa95f0c74596bc250dcfd960262841" dependencies = [ "autocfg", + "libm", ] [[package]] @@ -1433,6 +1462,32 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "proptest" +version = "1.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b4c2511913b88df1637da85cc8d96ec8e43a3f8bb8ccb71ee1ac240d6f3df58d" +dependencies = [ + "bit-set", + "bit-vec", + "bitflags", + "lazy_static", + "num-traits", + "rand", + "rand_chacha", + "rand_xorshift", + "regex-syntax 0.8.5", + "rusty-fork", + "tempfile", + "unarray", +] + +[[package]] +name = "quick-error" +version = "1.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1d01941d82fa2ab50be1e79e6714289dd7cde78eba4c074bc5a4374f650dfe0" + [[package]] name = "quick-xml" version = "0.37.1" @@ -1488,6 +1543,15 @@ dependencies = [ "getrandom", ] +[[package]] +name = "rand_xorshift" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d25bf25ec5ae4a3f1b92f929810509a2f53d7dca2f50b794ff57e3face536c8f" +dependencies = [ + "rand_core", +] + [[package]] name = "rayon" version = "1.10.0" @@ -1636,6 +1700,18 @@ version = "1.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0e819f2bc632f285be6d7cd36e25940d45b2391dd6d9b939e79de557f7014248" +[[package]] +name = "rusty-fork" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cb3dcc6e454c328bb824492db107ab7c0ae8fcffe4ad210136ef014458c1bc4f" +dependencies = [ + "fnv", + "quick-error", + "tempfile", + "wait-timeout", +] + [[package]] name = "ryu" version = "1.0.18" @@ -2030,6 +2106,12 @@ dependencies = [ "static_assertions", ] +[[package]] +name = "unarray" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "eaea85b334db583fe3274d12b4cd1880032beab409c0d774be044d4480ab9a94" + [[package]] name = "unicode-ident" version = "1.0.14" @@ -2076,6 +2158,15 @@ version = "0.9.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" +[[package]] +name = "wait-timeout" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9f200f5b12eb75f8c1ed65abd4b2db8a6e1b138a20de009dacee265a2498f3f6" +dependencies = [ + "libc", +] + [[package]] name = "walkdir" version = "2.5.0" diff --git a/Cargo.toml b/Cargo.toml index 1ee0b66ef..926941472 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -37,6 +37,7 @@ plonky2 = "0.2" poseidon = { path = "./poseidon" } pprof2 = { version = "0.13", features = ["flamegraph"] } prettytable-rs = "^0.10" +proptest = "1" rand = "0.8" rand_chacha = { version = "0.3", features = ["serde1"] } rand_core = "0.6" diff --git a/ceno_zkvm/Cargo.toml b/ceno_zkvm/Cargo.toml index 4bb427eb9..c72c5c8db 100644 --- a/ceno_zkvm/Cargo.toml +++ b/ceno_zkvm/Cargo.toml @@ -47,6 +47,7 @@ thread_local = "1.1" cfg-if.workspace = true criterion.workspace = true pprof2.workspace = true +proptest.workspace = true [build-dependencies] glob = "0.3" diff --git a/ceno_zkvm/src/instructions/riscv/slti.rs b/ceno_zkvm/src/instructions/riscv/slti.rs index 76894f7a0..7ea9b1675 100644 --- a/ceno_zkvm/src/instructions/riscv/slti.rs +++ b/ceno_zkvm/src/instructions/riscv/slti.rs @@ -139,12 +139,15 @@ mod test { use ceno_emul::{Change, PC_STEP_SIZE, StepRecord, encode_rv32}; use goldilocks::GoldilocksExt2; - use rand::Rng; + use proptest::proptest; use super::*; use crate::{ circuit_builder::{CircuitBuilder, ConstraintSystem}, - instructions::Instruction, + instructions::{ + Instruction, + riscv::test_utils::{i32_extra, imm_extra, immu_extra, u32_extra}, + }, scheme::mock_prover::{MOCK_PC_START, MockProver}, }; @@ -177,13 +180,14 @@ mod test { verify("lt = false, imm lower bondary", u32::MAX, -2048); } - #[test] - fn test_sltiu_random() { - let mut rng = rand::thread_rng(); - let a: u32 = rng.gen::(); - let b: i32 = rng.gen_range(-2048..2048); - println!("random: {} ("random unsigned comparison", a, b, a < (b as u32)); + proptest! { + #[test] + fn test_sltiu_prop( + a in u32_extra(), + imm in immu_extra(12), + ) { + verify::("random SltiuOp", a, imm as i32, a < imm); + } } #[test] @@ -215,13 +219,14 @@ mod test { verify("lt = false, imm lower bondary", i32::MAX, -2048); } - #[test] - fn test_slti_random() { - let mut rng = rand::thread_rng(); - let a: i32 = rng.gen(); - let b: i32 = rng.gen_range(-2048..2048); - println!("random: {} ("random 1", a as u32, b, a < b); + proptest! { + #[test] + fn test_slti_prop( + a in i32_extra(), + imm in imm_extra(12), + ) { + verify::("random SltiOp", a as u32, imm, a < imm); + } } fn verify(name: &'static str, rs1_read: u32, imm: i32, expected_rd: bool) { diff --git a/ceno_zkvm/src/instructions/riscv/test_utils.rs b/ceno_zkvm/src/instructions/riscv/test_utils.rs index 416ce628c..973902717 100644 --- a/ceno_zkvm/src/instructions/riscv/test_utils.rs +++ b/ceno_zkvm/src/instructions/riscv/test_utils.rs @@ -1,3 +1,9 @@ +use proptest::{ + prelude::any, + prop_oneof, + strategy::{Just, Strategy}, +}; + pub fn imm_b(imm: i32) -> u32 { // imm is 13 bits in B-type imm_with_max_valid_bits(imm, 13) @@ -14,10 +20,36 @@ pub fn imm_j(imm: i32) -> u32 { } fn imm_with_max_valid_bits(imm: i32, bits: u32) -> u32 { - imm as u32 & !(u32::MAX << bits) + let shift = 32 - bits; + (imm << shift >> shift) as u32 } pub fn imm_u(imm: u32) -> u32 { // valid imm is imm[12:31] in U-type imm << 12 } + +#[allow(clippy::cast_sign_loss)] +pub fn u32_extra() -> impl Strategy { + prop_oneof![ + Just(0_u32), + Just(1_u32), + Just(u32::MAX), + any::(), + Just(i32::MIN as u32), + Just(i32::MAX as u32), + ] +} + +#[allow(clippy::cast_possible_wrap)] +pub fn i32_extra() -> impl Strategy { + u32_extra().prop_map(|x| x as i32) +} + +pub fn imm_extra(bits: u32) -> impl Strategy { + i32_extra().prop_map(move |x| imm_with_max_valid_bits(x, bits) as i32) +} + +pub fn immu_extra(bits: u32) -> impl Strategy { + i32_extra().prop_map(move |x| imm_with_max_valid_bits(x, bits)) +}