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

Merge rust-bitcoin/rust-bitcoin#2464: Remove broken kani test 

7e1ba7895f Remove broken kani test (Tobin C. Harding)

Pull request description:

  This test is failing. I do not want to dive back into kani right now, just remove it.

  This is what I originally did in #2454 but changed directions and tried to fix it. Running kani test takes ages and I'd need to dig back to refresh my memory to work with kani. I don't have the motivation to do that at the moment. Just remove the test.

  FTR I added the test recently without fulling thinking it through and it has never passed so we are not loosing any coverage. Doing this was the original mistake I should not have made.

ACKs for top commit:
  Kixunil:
    ACK 7e1ba7895f
  apoelstra:
    ACK 7e1ba7895f

Tree-SHA512: cb76807173b637be9d5ce790b015e711ca76add95ce0f0acfdc56947c075f57ea89774c09c4314dbc89086dcf7a8e21053552bfae805fd5dc9c91051cd53c468
This commit is contained in:
Andrew Poelstra 2024-02-12 14:08:02 +00:00
parent 4523034ba3 7e1ba7895f
commit 9bdac92e1a
No known key found for this signature in database
GPG Key ID: C588D63CE41B97C1
1 changed files with 0 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
bitcoin/src/pow.rs
View File

@ -1746,14 +1746,4 @@ mod verification {
let _ = x.mul_u64(y); let _ = x.mul_u64(y);
} }
#[kani::unwind(5)] // Same as above.
#[kani::proof]
fn check_div_rem() {
let x: 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);
}
} }