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

Merge rust-bitcoin/rust-bitcoin#2393: Add kani test and remove TODO 

66352cba98 Add kani test and remove TODO (Tobin C. Harding)

Pull request description:

  Add a kani test to check `div_rem`.

ACKs for top commit:
  Kixunil:
    ACK 66352cba98
  apoelstra:
    ACK 66352cba98

Tree-SHA512: 2cb277e11d9d853f92b12e3c1e93f4a1094466a7aab9a9a8d0883e015b4c0d876678d8147f107155dee11911954e7b3da6ee25e0e67f39f76a4da45b1dbc5307
This commit is contained in:
Andrew Poelstra 2024-01-23 14:28:52 +00:00
parent 44bf326886 66352cba98
commit 8b552c7706
No known key found for this signature in database
GPG Key ID: C588D63CE41B97C1
1 changed files with 9 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
bitcoin/src/pow.rs
View File

@ -1735,7 +1735,6 @@ mod tests {
mod verification { mod verification {
use super::*; use super::*;
// TODO: After we verify div_rem assert x * y / y == x
#[kani::unwind(5)] // mul_u64 loops over 4 64 bit ints so use one more than 4 #[kani::unwind(5)] // mul_u64 loops over 4 64 bit ints so use one more than 4
#[kani::proof] #[kani::proof]
fn check_mul_u64() { fn check_mul_u64() {
@ -1744,4 +1743,13 @@ 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::proof]
fn check_div_rem() {
let x: U256 = kani::any();
let y: U256 = kani::any();
assert_eq!(x * y / y, x);
}
} }