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

Merge rust-bitcoin/rust-bitcoin#3782: A couple of kani fixes 

f4617e71f5 kani: Verify no out of bounds for ArrayVec (Tobin C. Harding)
e378cdd8fa kani: Don't bother checking signed to unsigned conversion (Tobin C. Harding)
50224eecc2 kani: Don't overflow the tests (Tobin C. Harding)

Pull request description:

  PR does two things because a recent upgrade of `kani` broke our setup. I'm not sure why it just showed up.

  We fix the verification for `amount` types which recently broke because of `MAX_MONEY` changes and then we add a verification function to `internals` because build fails and one fix is to just add something.

  - Patch 1: units: Assumes correct values
  - Patch 2: units: Removes a stale check now that MAX_MONEY is being used for MAX
  - Patch 3: Add verification to `internals::ArrayVec`.

ACKs for top commit:
  apoelstra:
    ACK f4617e71f5fd074000d1e3a9376644c744210562; successfully ran local tests

Tree-SHA512: dfef05a7bbb5372415efa8acab7f79801aa7326ac298c007b173786f00bcccd0b1b81d327113723c359fb2797895414a586cc3fb86e495476a03fcac02a96899
This commit is contained in:
merge-script 2024-12-19 02:18:07 +00:00
parent ebe43b6f87 f4617e71f5
commit 9cb302e477
No known key found for this signature in database
GPG Key ID: C588D63CE41B97C1
3 changed files with 57 additions and 57 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
internals/Cargo.toml
View File

@ -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)'] }

42
internals/src/array_vec.rs
View File

@ -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::<u32>();
let elements = (n & 0x0F) as usize; // Just use 4 bits.
let val = kani::any::<u32>();
let mut v = ArrayVec::<u32, CAP>::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::<u32>();
let mut v = ArrayVec::<u32, CAP>::new();
for _ in 0..elements {
v.push(val);
}
for i in 0..elements {
assert_eq!(v[i], val);
}
}
}

70
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);
@ -37,30 +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)]
#[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)]
@ -68,8 +49,14 @@ fn u_amount_homomorphic_checked() {
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)
@ -85,33 +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 })
},
);
}
#[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 },
);
}