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

Fix broken kani test 

We can only multiply numbers that do not overflow. Also inhibit div by
zero.
This commit is contained in:
Tobin C. Harding 2024-02-06 14:40:07 +11:00
parent a3c4194c3f
commit 47569302fc
No known key found for this signature in database
GPG Key ID: 40BF9E4C269D6607
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
bitcoin/src/pow.rs
View File

@ -1742,11 +1742,12 @@ mod verification {
let _ = x.mul_u64(y); let _ = x.mul_u64(y);
} }
#[kani::unwind(5)] // I can't remember exactly why we need this. #[kani::unwind(5)] // Same as above.
#[kani::proof] #[kani::proof]
fn check_div_rem() { fn check_div_rem() {
let x: U256 = kani::any(); let x: U256 = kani::any();
let y: U256 = kani::any(); let y: U256 = kani::any();
kani::assume(x < U256::from(u128::MAX) && y < U256::from(u128::MAX) && y != U256::ZERO);
assert_eq!(x * y / y, x); assert_eq!(x * y / y, x);
} }