From 132eb6ada309cbf17014f9c6776cff80f1bb4931 Mon Sep 17 00:00:00 2001 From: Matthias Goergens Date: Fri, 25 Oct 2024 14:47:54 +0800 Subject: [PATCH 1/3] Proptest --- Cargo.lock | 91 +++++++++++++++++++ Cargo.toml | 1 + ceno_zkvm/Cargo.toml | 1 + ceno_zkvm/src/instructions/riscv/slti.rs | 19 +++- .../src/instructions/riscv/test_utils.rs | 23 +++++ 5 files changed, 134 insertions(+), 1 deletion(-) diff --git a/Cargo.lock b/Cargo.lock index 923484c8e..7539e0987 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 = "1.3.2" @@ -278,6 +293,7 @@ dependencies = [ "paste", "pprof", "prettytable-rs", + "proptest", "rand", "rand_chacha", "rayon", @@ -700,6 +716,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" @@ -976,6 +998,12 @@ version = "0.2.161" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8e9489c2807c139ffd9c1794f4af0ebe86a828db53ecdc7fea2111d0fed085d1" +[[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" @@ -1198,6 +1226,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "071dfc062690e90b734c0b2273ce72ad0ffa95f0c74596bc250dcfd960262841" dependencies = [ "autocfg", + "libm", ] [[package]] @@ -1439,6 +1468,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 2.6.0", + "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.26.0" @@ -1494,6 +1549,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" @@ -1642,6 +1706,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" @@ -2015,6 +2091,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.13" @@ -2061,6 +2143,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 daa44f156..8aad59e6d 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -37,6 +37,7 @@ plonky2 = "0.2" poseidon = { path = "./poseidon" } pprof = { 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 13f4f2810..c1f89e0fe 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 pprof.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 d88f0336c..433592dca 100644 --- a/ceno_zkvm/src/instructions/riscv/slti.rs +++ b/ceno_zkvm/src/instructions/riscv/slti.rs @@ -139,12 +139,18 @@ mod test { use ceno_emul::{Change, PC_STEP_SIZE, StepRecord, encode_rv32}; use goldilocks::GoldilocksExt2; + use itertools::Itertools; use rand::Rng; + // Not sure. + use multilinear_extensions::mle::IntoMLEs; use super::*; use crate::{ circuit_builder::{CircuitBuilder, ConstraintSystem}, - instructions::Instruction, + instructions::{ + Instruction, + riscv::test_utils::{i32_extra, imm_i}, + }, scheme::mock_prover::{MOCK_PC_START, MockProver}, }; @@ -260,4 +266,15 @@ mod test { MockProver::assert_satisfied_raw(&cb, raw_witin, &[insn_code], None, Some(lkm)); } + + use proptest::{prelude::Strategy, proptest}; + proptest! { + #[test] + fn test_slti_prop( + a in i32_extra(), + b in i32_extra().prop_map(|x| x & 0x7FF), + ) { + verify("random 1", a, b, (a < b) as u32); + } + } } diff --git a/ceno_zkvm/src/instructions/riscv/test_utils.rs b/ceno_zkvm/src/instructions/riscv/test_utils.rs index 416ce628c..45becc3b9 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) @@ -21,3 +27,20 @@ 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) +} From 114cfe12a11b9c0dd144949e025dbd2f7f17eeac Mon Sep 17 00:00:00 2001 From: Matthias Goergens Date: Mon, 2 Dec 2024 18:01:41 +0800 Subject: [PATCH 2/3] Clean up --- ceno_zkvm/src/instructions/riscv/slti.rs | 123 +++++++++--------- .../src/instructions/riscv/test_utils.rs | 11 +- 2 files changed, 68 insertions(+), 66 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/slti.rs b/ceno_zkvm/src/instructions/riscv/slti.rs index 433592dca..7ea9b1675 100644 --- a/ceno_zkvm/src/instructions/riscv/slti.rs +++ b/ceno_zkvm/src/instructions/riscv/slti.rs @@ -139,94 +139,98 @@ mod test { use ceno_emul::{Change, PC_STEP_SIZE, StepRecord, encode_rv32}; use goldilocks::GoldilocksExt2; - use itertools::Itertools; - use rand::Rng; - // Not sure. - use multilinear_extensions::mle::IntoMLEs; + use proptest::proptest; use super::*; use crate::{ circuit_builder::{CircuitBuilder, ConstraintSystem}, instructions::{ Instruction, - riscv::test_utils::{i32_extra, imm_i}, + riscv::test_utils::{i32_extra, imm_extra, immu_extra, u32_extra}, }, scheme::mock_prover::{MOCK_PC_START, MockProver}, }; #[test] fn test_sltiu_true() { - verify::("lt = true, 0 < 1", 0, 1, 1); - verify::("lt = true, 1 < 2", 1, 2, 1); - verify::("lt = true, 10 < 20", 10, 20, 1); - verify::("lt = true, 0 < imm upper boundary", 0, 2047, 1); + let verify = |name, a, imm| verify::(name, a, imm, true); + verify("lt = true, 0 < 1", 0, 1); + verify("lt = true, 1 < 2", 1, 2); + verify("lt = true, 10 < 20", 10, 20); + verify("lt = true, 0 < imm upper boundary", 0, 2047); // negative imm is treated as positive - verify::("lt = true, 0 < u32::MAX-1", 0, -1, 1); - verify::("lt = true, 1 < u32::MAX-1", 1, -1, 1); - verify::("lt = true, 0 < imm lower bondary", 0, -2048, 1); + verify("lt = true, 0 < u32::MAX-1", 0, -1); + verify("lt = true, 1 < u32::MAX-1", 1, -1); + verify("lt = true, 0 < imm lower bondary", 0, -2048); } #[test] fn test_sltiu_false() { - verify::("lt = false, 1 < 0", 1, 0, 0); - verify::("lt = false, 2 < 1", 2, 1, 0); - verify::("lt = false, 100 < 50", 100, 50, 0); - verify::("lt = false, 500 < 100", 500, 100, 0); - verify::("lt = false, 100000 < 2047", 100000, 2047, 0); - verify::("lt = false, 100000 < 0", 100000, 0, 0); - verify::("lt = false, 0 == 0", 0, 0, 0); - verify::("lt = false, 1 == 1", 1, 1, 0); - verify::("lt = false, imm upper bondary", u32::MAX, 2047, 0); + let verify = |name, a, imm| verify::(name, a, imm, false); + verify("lt = false, 1 < 0", 1, 0); + verify("lt = false, 2 < 1", 2, 1); + verify("lt = false, 100 < 50", 100, 50); + verify("lt = false, 500 < 100", 500, 100); + verify("lt = false, 100000 < 2047", 100000, 2047); + verify("lt = false, 100000 < 0", 100000, 0); + verify("lt = false, 0 == 0", 0, 0); + verify("lt = false, 1 == 1", 1, 1); + verify("lt = false, imm upper bondary", u32::MAX, 2047); // negative imm is treated as positive - verify::("lt = false, imm lower bondary", u32::MAX, -2048, 0); + 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)) 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] fn test_slti_true() { - verify::("lt = true, 0 < 1", 0, 1, 1); - verify::("lt = true, 1 < 2", 1, 2, 1); - verify::("lt = true, -1 < 0", -1i32 as u32, 0, 1); - verify::("lt = true, -1 < 1", -1i32 as u32, 1, 1); - verify::("lt = true, -2 < -1", -2i32 as u32, -1, 1); + let verify = |name, a: i32, imm| verify::(name, a as u32, imm, true); + verify("lt = true, 0 < 1", 0, 1); + verify("lt = true, 1 < 2", 1, 2); + verify("lt = true, -1 < 0", -1, 0); + verify("lt = true, -1 < 1", -1, 1); + verify("lt = true, -2 < -1", -2, -1); // -2048 <= imm <= 2047 - verify::("lt = true, imm upper bondary", i32::MIN as u32, 2047, 1); - verify::("lt = true, imm lower bondary", i32::MIN as u32, -2048, 1); + verify("lt = true, imm upper bondary", i32::MIN, 2047); + verify("lt = true, imm lower bondary", i32::MIN, -2048); } #[test] fn test_slti_false() { - verify::("lt = false, 1 < 0", 1, 0, 0); - verify::("lt = false, 2 < 1", 2, 1, 0); - verify::("lt = false, 0 < -1", 0, -1, 0); - verify::("lt = false, 1 < -1", 1, -1, 0); - verify::("lt = false, -1 < -2", -1i32 as u32, -2, 0); - verify::("lt = false, 0 == 0", 0, 0, 0); - verify::("lt = false, 1 == 1", 1, 1, 0); - verify::("lt = false, -1 == -1", -1i32 as u32, -1, 0); + let verify = |name, a: i32, imm| verify::(name, a as u32, imm, false); + verify("lt = false, 1 < 0", 1, 0); + verify("lt = false, 2 < 1", 2, 1); + verify("lt = false, 0 < -1", 0, -1); + verify("lt = false, 1 < -1", 1, -1); + verify("lt = false, -1 < -2", -1, -2); + verify("lt = false, 0 == 0", 0, 0); + verify("lt = false, 1 == 1", 1, 1); + verify("lt = false, -1 == -1", -1, -1); // -2048 <= imm <= 2047 - verify::("lt = false, imm upper bondary", i32::MAX as u32, 2047, 0); - verify::("lt = false, imm lower bondary", i32::MAX as u32, -2048, 0); + verify("lt = false, imm upper bondary", i32::MAX, 2047); + 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) as u32); + 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: u32) { + fn verify(name: &'static str, rs1_read: u32, imm: i32, expected_rd: bool) { + let expected_rd = expected_rd as u32; let mut cs = ConstraintSystem::::new(|| "riscv"); let mut cb = CircuitBuilder::new(&mut cs); @@ -266,15 +270,4 @@ mod test { MockProver::assert_satisfied_raw(&cb, raw_witin, &[insn_code], None, Some(lkm)); } - - use proptest::{prelude::Strategy, proptest}; - proptest! { - #[test] - fn test_slti_prop( - a in i32_extra(), - b in i32_extra().prop_map(|x| x & 0x7FF), - ) { - verify("random 1", a, b, (a < b) as u32); - } - } } diff --git a/ceno_zkvm/src/instructions/riscv/test_utils.rs b/ceno_zkvm/src/instructions/riscv/test_utils.rs index 45becc3b9..973902717 100644 --- a/ceno_zkvm/src/instructions/riscv/test_utils.rs +++ b/ceno_zkvm/src/instructions/riscv/test_utils.rs @@ -20,7 +20,8 @@ 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 { @@ -44,3 +45,11 @@ pub fn u32_extra() -> impl Strategy { 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)) +} From 50237a92781a5e0c679eb20610a71b832dc6b801 Mon Sep 17 00:00:00 2001 From: Matthias Goergens Date: Mon, 9 Dec 2024 11:54:21 +0800 Subject: [PATCH 3/3] Simplify SLTI tests Extracted from https://github.com/scroll-tech/ceno/pull/667 to make that PR smaller and easier to review. --- ceno_zkvm/src/instructions/riscv/slti.rs | 79 +++++++++++++----------- 1 file changed, 42 insertions(+), 37 deletions(-) diff --git a/ceno_zkvm/src/instructions/riscv/slti.rs b/ceno_zkvm/src/instructions/riscv/slti.rs index d88f0336c..76894f7a0 100644 --- a/ceno_zkvm/src/instructions/riscv/slti.rs +++ b/ceno_zkvm/src/instructions/riscv/slti.rs @@ -150,29 +150,31 @@ mod test { #[test] fn test_sltiu_true() { - verify::("lt = true, 0 < 1", 0, 1, 1); - verify::("lt = true, 1 < 2", 1, 2, 1); - verify::("lt = true, 10 < 20", 10, 20, 1); - verify::("lt = true, 0 < imm upper boundary", 0, 2047, 1); + let verify = |name, a, imm| verify::(name, a, imm, true); + verify("lt = true, 0 < 1", 0, 1); + verify("lt = true, 1 < 2", 1, 2); + verify("lt = true, 10 < 20", 10, 20); + verify("lt = true, 0 < imm upper boundary", 0, 2047); // negative imm is treated as positive - verify::("lt = true, 0 < u32::MAX-1", 0, -1, 1); - verify::("lt = true, 1 < u32::MAX-1", 1, -1, 1); - verify::("lt = true, 0 < imm lower bondary", 0, -2048, 1); + verify("lt = true, 0 < u32::MAX-1", 0, -1); + verify("lt = true, 1 < u32::MAX-1", 1, -1); + verify("lt = true, 0 < imm lower bondary", 0, -2048); } #[test] fn test_sltiu_false() { - verify::("lt = false, 1 < 0", 1, 0, 0); - verify::("lt = false, 2 < 1", 2, 1, 0); - verify::("lt = false, 100 < 50", 100, 50, 0); - verify::("lt = false, 500 < 100", 500, 100, 0); - verify::("lt = false, 100000 < 2047", 100000, 2047, 0); - verify::("lt = false, 100000 < 0", 100000, 0, 0); - verify::("lt = false, 0 == 0", 0, 0, 0); - verify::("lt = false, 1 == 1", 1, 1, 0); - verify::("lt = false, imm upper bondary", u32::MAX, 2047, 0); + let verify = |name, a, imm| verify::(name, a, imm, false); + verify("lt = false, 1 < 0", 1, 0); + verify("lt = false, 2 < 1", 2, 1); + verify("lt = false, 100 < 50", 100, 50); + verify("lt = false, 500 < 100", 500, 100); + verify("lt = false, 100000 < 2047", 100000, 2047); + verify("lt = false, 100000 < 0", 100000, 0); + verify("lt = false, 0 == 0", 0, 0); + verify("lt = false, 1 == 1", 1, 1); + verify("lt = false, imm upper bondary", u32::MAX, 2047); // negative imm is treated as positive - verify::("lt = false, imm lower bondary", u32::MAX, -2048, 0); + verify("lt = false, imm lower bondary", u32::MAX, -2048); } #[test] @@ -181,34 +183,36 @@ mod test { let a: u32 = rng.gen::(); let b: i32 = rng.gen_range(-2048..2048); println!("random: {} ("random unsigned comparison", a, b, (a < (b as u32)) as u32); + verify::("random unsigned comparison", a, b, a < (b as u32)); } #[test] fn test_slti_true() { - verify::("lt = true, 0 < 1", 0, 1, 1); - verify::("lt = true, 1 < 2", 1, 2, 1); - verify::("lt = true, -1 < 0", -1i32 as u32, 0, 1); - verify::("lt = true, -1 < 1", -1i32 as u32, 1, 1); - verify::("lt = true, -2 < -1", -2i32 as u32, -1, 1); + let verify = |name, a: i32, imm| verify::(name, a as u32, imm, true); + verify("lt = true, 0 < 1", 0, 1); + verify("lt = true, 1 < 2", 1, 2); + verify("lt = true, -1 < 0", -1, 0); + verify("lt = true, -1 < 1", -1, 1); + verify("lt = true, -2 < -1", -2, -1); // -2048 <= imm <= 2047 - verify::("lt = true, imm upper bondary", i32::MIN as u32, 2047, 1); - verify::("lt = true, imm lower bondary", i32::MIN as u32, -2048, 1); + verify("lt = true, imm upper bondary", i32::MIN, 2047); + verify("lt = true, imm lower bondary", i32::MIN, -2048); } #[test] fn test_slti_false() { - verify::("lt = false, 1 < 0", 1, 0, 0); - verify::("lt = false, 2 < 1", 2, 1, 0); - verify::("lt = false, 0 < -1", 0, -1, 0); - verify::("lt = false, 1 < -1", 1, -1, 0); - verify::("lt = false, -1 < -2", -1i32 as u32, -2, 0); - verify::("lt = false, 0 == 0", 0, 0, 0); - verify::("lt = false, 1 == 1", 1, 1, 0); - verify::("lt = false, -1 == -1", -1i32 as u32, -1, 0); + let verify = |name, a: i32, imm| verify::(name, a as u32, imm, false); + verify("lt = false, 1 < 0", 1, 0); + verify("lt = false, 2 < 1", 2, 1); + verify("lt = false, 0 < -1", 0, -1); + verify("lt = false, 1 < -1", 1, -1); + verify("lt = false, -1 < -2", -1, -2); + verify("lt = false, 0 == 0", 0, 0); + verify("lt = false, 1 == 1", 1, 1); + verify("lt = false, -1 == -1", -1, -1); // -2048 <= imm <= 2047 - verify::("lt = false, imm upper bondary", i32::MAX as u32, 2047, 0); - verify::("lt = false, imm lower bondary", i32::MAX as u32, -2048, 0); + verify("lt = false, imm upper bondary", i32::MAX, 2047); + verify("lt = false, imm lower bondary", i32::MAX, -2048); } #[test] @@ -217,10 +221,11 @@ mod test { let a: i32 = rng.gen(); let b: i32 = rng.gen_range(-2048..2048); println!("random: {} ("random 1", a as u32, b, (a < b) as u32); + verify::("random 1", a as u32, b, a < b); } - fn verify(name: &'static str, rs1_read: u32, imm: i32, expected_rd: u32) { + fn verify(name: &'static str, rs1_read: u32, imm: i32, expected_rd: bool) { + let expected_rd = expected_rd as u32; let mut cs = ConstraintSystem::::new(|| "riscv"); let mut cb = CircuitBuilder::new(&mut cs);