milksad
/
rust-bitcoin-unsafe-fast
14
0
Fork 0
Code Issues Pull Requests Activity

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.
This commit is contained in:
Tobin C. Harding 2024-12-18 09:06:51 +11:00
parent f4069fcd61
commit 50224eecc2
No known key found for this signature in database
GPG Key ID: 40BF9E4C269D6607
1 changed files with 14 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

52
units/src/amount/verification.rs
View File

@ -23,7 +23,12 @@ use super::*;
fn u_amount_homomorphic() {
let n1 = kani::any::<u64>();
let n2 = kani::any::<u64>();
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::<u64>();
let n2 = kani::any::<u64>();
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::<i64>();
let n2 = kani::any::<i64>();
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::<i64>();
let n2 = kani::any::<i64>();
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 },
);
}