Property based testing

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"

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/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::<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]
@@ -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: {} <? {}", 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

@@ -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<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))
+}