Property based testing

.gitignore

@@ -8,3 +8,4 @@ report.json
 table_cache_dev_*
 .DS_Store
 .env
+proptest-regressions/

Cargo.toml

@@ -38,6 +38,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"

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"

ceno_zkvm/src/instructions/riscv.rs

@@ -36,6 +36,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/slti.rs

@@ -138,12 +138,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},
     };
 
@@ -176,13 +179,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::<u32>();
-        let b: i32 = rng.gen_range(-2048..2048);
-        println!("random: {} <? {}", a, b); // For debugging, do not delete.
-        verify::<SltiuOp>("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::<SltiuOp>("random SltiuOp", a, imm as i32, a < imm);
+        }
     }
 
     #[test]
@@ -214,13 +218,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: {} <? {}", a, b); // For debugging, do not delete.
-        verify::<SltiOp>("random 1", a as u32, b, a < b);
+    proptest! {
+        #[test]
+        fn test_slti_prop(
+            a in i32_extra(),
+            imm in imm_extra(12),
+        ) {
+            verify::<SltiOp>("random SltiOp", a as u32, imm, a < imm);
+        }
     }
 
     fn verify<I: RIVInstruction>(name: &'static str, rs1_read: u32, imm: i32, expected_rd: bool) {

ceno_zkvm/src/instructions/riscv/test_utils.rs

@@ -0,0 +1,35 @@
+use proptest::{
+    prelude::any,
+    prop_oneof,
+    strategy::{Just, Strategy},
+};
+
+fn imm_with_max_valid_bits(imm: i32, bits: u32) -> u32 {
+    let shift = 32 - bits;
+    (imm << shift >> shift) as u32
+}
+
+#[allow(clippy::cast_sign_loss)]
+pub fn u32_extra() -> impl Strategy<Value = u32> {
+    prop_oneof![
+        Just(0_u32),
+        Just(1_u32),
+        Just(u32::MAX),
+        any::<u32>(),
+        Just(i32::MIN as u32),
+        Just(i32::MAX as u32),
+    ]
+}
+
+#[allow(clippy::cast_possible_wrap)]
+pub fn i32_extra() -> impl Strategy<Value = i32> {
+    u32_extra().prop_map(|x| x as i32)
+}
+
+pub fn imm_extra(bits: u32) -> impl Strategy<Value = i32> {
+    i32_extra().prop_map(move |x| imm_with_max_valid_bits(x, bits) as i32)
+}
+
+pub fn immu_extra(bits: u32) -> impl Strategy<Value = u32> {
+    i32_extra().prop_map(move |x| imm_with_max_valid_bits(x, bits))
+}