From 50224eecc242ddc4d67f76b0c5e28f7120b6e961 Mon Sep 17 00:00:00 2001 From: "Tobin C. Harding" Date: Wed, 18 Dec 2024 09:06:51 +1100 Subject: [PATCH 1/3] kani: Don't overflow the tests Amount add and sub now enforce the MAX_MONEY invariant when doing addition and subtraction. We need to tell kani to assume we don't overflow before doing actual tests. Note also that `ops::Add` calls through to `checked_add` and `ops::Sub` calls through to `checked_sub` so separate kani tests for these are unnecessary. --- units/src/amount/verification.rs | 52 +++++++++----------------------- 1 file changed, 14 insertions(+), 38 deletions(-) diff --git a/units/src/amount/verification.rs b/units/src/amount/verification.rs index 0310e19e9..76f26ec0d 100644 --- a/units/src/amount/verification.rs +++ b/units/src/amount/verification.rs @@ -23,7 +23,12 @@ use super::*; fn u_amount_homomorphic() { let n1 = kani::any::(); let n2 = kani::any::(); - kani::assume(n1.checked_add(n2).is_some()); // assume we don't overflow in the actual test + // Assume we don't overflow in the actual tests. + kani::assume(n1.checked_add(n2).is_some()); // Adding u64s doesn't overflow. + let a1 = Amount::from_sat(n1); // TODO: If from_sat enforces invariant assume this `is_ok()`. + let a2 = Amount::from_sat(n2); + kani::assume(a1.checked_add(a2).is_some()); // Adding amounts doesn't overflow. + assert_eq!(Amount::from_sat(n1) + Amount::from_sat(n2), Amount::from_sat(n1 + n2)); let mut amt = Amount::from_sat(n1); @@ -48,28 +53,19 @@ fn u_amount_homomorphic() { ); } -#[kani::unwind(4)] -#[kani::proof] -fn u_amount_homomorphic_checked() { - let n1 = kani::any::(); - let n2 = kani::any::(); - assert_eq!( - Amount::from_sat(n1).checked_add(Amount::from_sat(n2)), - n1.checked_add(n2).map(Amount::from_sat), - ); - assert_eq!( - Amount::from_sat(n1).checked_sub(Amount::from_sat(n2)), - n1.checked_sub(n2).map(Amount::from_sat), - ); -} - #[kani::unwind(4)] #[kani::proof] fn s_amount_homomorphic() { let n1 = kani::any::(); let n2 = kani::any::(); - kani::assume(n1.checked_add(n2).is_some()); // assume we don't overflow in the actual test - kani::assume(n1.checked_sub(n2).is_some()); // assume we don't overflow in the actual test + // Assume we don't overflow in the actual tests. + kani::assume(n1.checked_add(n2).is_some()); // Adding i64s doesn't overflow. + kani::assume(n1.checked_sub(n2).is_some()); // Subbing i64s doesn't overflow. + let a1 = SignedAmount::from_sat(n1); // TODO: If from_sat enforces invariant assume this `is_ok()`. + let a2 = SignedAmount::from_sat(n2); + kani::assume(a1.checked_add(a2).is_some()); // Adding amounts doesn't overflow. + kani::assume(a1.checked_sub(a2).is_some()); // Subbing amounts doesn't overflow. + assert_eq!( SignedAmount::from_sat(n1) + SignedAmount::from_sat(n2), SignedAmount::from_sat(n1 + n2) @@ -95,23 +91,3 @@ fn s_amount_homomorphic() { }, ); } - -#[kani::unwind(4)] -#[kani::proof] -fn s_amount_homomorphic_checked() { - let n1 = kani::any::(); - let n2 = kani::any::(); - assert_eq!( - SignedAmount::from_sat(n1).checked_add(SignedAmount::from_sat(n2)), - n1.checked_add(n2).map(SignedAmount::from_sat), - ); - assert_eq!( - SignedAmount::from_sat(n1).checked_sub(SignedAmount::from_sat(n2)), - n1.checked_sub(n2).map(SignedAmount::from_sat), - ); - - assert_eq!( - SignedAmount::from_sat(n1).positive_sub(SignedAmount::from_sat(n2)), - if n1 >= 0 && n2 >= 0 && n1 >= n2 { Some(SignedAmount::from_sat(n1 - n2)) } else { None }, - ); -} From e378cdd8fa340469b8c9b046ea6d6f0dd4e04414 Mon Sep 17 00:00:00 2001 From: "Tobin C. Harding" Date: Wed, 18 Dec 2024 09:36:54 +1100 Subject: [PATCH 2/3] kani: Don't bother checking signed to unsigned conversion Now that we use MAX_MONEY a signed amount always fits in an unsigned amount. --- units/src/amount/verification.rs | 18 ------------------ 1 file changed, 18 deletions(-) diff --git a/units/src/amount/verification.rs b/units/src/amount/verification.rs index 76f26ec0d..ae970e186 100644 --- a/units/src/amount/verification.rs +++ b/units/src/amount/verification.rs @@ -42,15 +42,6 @@ fn u_amount_homomorphic() { let mut amt = Amount::from_sat(max); amt -= Amount::from_sat(min); assert_eq!(amt, Amount::from_sat(max - min)); - - assert_eq!( - Amount::from_sat(n1).to_signed(), - if n1 <= i64::MAX as u64 { - Ok(SignedAmount::from_sat(n1.try_into().unwrap())) - } else { - Err(OutOfRangeError::too_big(true)) - }, - ); } #[kani::unwind(4)] @@ -81,13 +72,4 @@ fn s_amount_homomorphic() { let mut amt = SignedAmount::from_sat(n1); amt -= SignedAmount::from_sat(n2); assert_eq!(amt, SignedAmount::from_sat(n1 - n2)); - - assert_eq!( - SignedAmount::from_sat(n1).to_unsigned(), - if n1 >= 0 { - Ok(Amount::from_sat(n1.try_into().unwrap())) - } else { - Err(OutOfRangeError { is_signed: false, is_greater_than_max: false }) - }, - ); } From f4617e71f5fd074000d1e3a9376644c744210562 Mon Sep 17 00:00:00 2001 From: "Tobin C. Harding" Date: Thu, 19 Dec 2024 08:59:12 +1100 Subject: [PATCH 3/3] kani: Verify no out of bounds for ArrayVec I'm not super confident that I know exactly what kani does but I believe this test verifies that the `ArrayVec` can add and access elements less than capacity and upto capacity. --- internals/Cargo.toml | 2 +- internals/src/array_vec.rs | 42 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 43 insertions(+), 1 deletion(-) diff --git a/internals/Cargo.toml b/internals/Cargo.toml index 0b9b6c252..12a5daa1d 100644 --- a/internals/Cargo.toml +++ b/internals/Cargo.toml @@ -35,4 +35,4 @@ all-features = true rustdoc-args = ["--cfg", "docsrs"] [lints.rust] -unexpected_cfgs = { level = "deny" } +unexpected_cfgs = { level = "deny", check-cfg = ['cfg(kani)'] } diff --git a/internals/src/array_vec.rs b/internals/src/array_vec.rs index 49fca83d8..24003e14b 100644 --- a/internals/src/array_vec.rs +++ b/internals/src/array_vec.rs @@ -188,3 +188,45 @@ mod tests { av.extend_from_slice(b"abc"); } } + +#[cfg(kani)] +mod verification { + use super::*; + + #[kani::unwind(16)] // One greater than 15 (max number of elements). + #[kani::proof] + fn no_out_of_bounds_less_than_cap() { + const CAP: usize = 32; + let n = kani::any::(); + let elements = (n & 0x0F) as usize; // Just use 4 bits. + + let val = kani::any::(); + + let mut v = ArrayVec::::new(); + for _ in 0..elements { + v.push(val); + } + + for i in 0..elements { + assert_eq!(v[i], val); + } + } + + #[kani::unwind(16)] // One grater than 15. + #[kani::proof] + fn no_out_of_bounds_upto_cap() { + const CAP: usize = 15; + let elements = CAP; + + let val = kani::any::(); + + let mut v = ArrayVec::::new(); + for _ in 0..elements { + v.push(val); + } + + for i in 0..elements { + assert_eq!(v[i], val); + } + } +}