From c11645b7e50578d95816b95db7ef1f649c1d828d Mon Sep 17 00:00:00 2001 From: Andrew Poelstra Date: Sun, 27 Nov 2022 18:08:28 +0000 Subject: [PATCH 1/2] amount: use kani to check some arithmetic properties Kani can't really handle string processing, and appears to be unable to check integer multiplication (for now), but we do several checks for addition and subtraction, and conversion between signedness, that Kani can easily prove. --- bitcoin/src/amount.rs | 142 +++++++++++++++++++++++++++++++++--------- 1 file changed, 113 insertions(+), 29 deletions(-) diff --git a/bitcoin/src/amount.rs b/bitcoin/src/amount.rs index 5b76bfec..5e32ad94 100644 --- a/bitcoin/src/amount.rs +++ b/bitcoin/src/amount.rs @@ -1399,6 +1399,117 @@ pub mod serde { } } +#[cfg(kani)] +mod verification { + use std::cmp; + use std::convert::TryInto; + use super::*; + + // Note regarding the `unwind` parameter: this defines how many iterations + // of loops kani will unwind before handing off to the SMT solver. Basically + // it should be set as low as possible such that Kani still succeeds (doesn't + // return "undecidable"). + // + // There is more info here: https://model-checking.github.io/kani/tutorial-loop-unwinding.html + // + // Unfortunately what it means to "loop" is pretty opaque ... in this case + // there appear to be loops in memcmp, which I guess comes from assert_eq!, + // though I didn't see any failures until I added the to_signed() test. + // Further confusing the issue, a value of 2 works fine on my system, but on + // CI it fails, so we need to set it higher. + #[kani::unwind(4)] + #[kani::proof] + fn u_amount_add_homomorphic() { + let n1 = kani::any::(); + let n2 = kani::any::(); + kani::assume(n1.checked_add(n2).is_some()); // assume we don't overflow in the actual test + assert_eq!(Amount::from_sat(n1) + Amount::from_sat(n2), Amount::from_sat(n1 + n2)); + + let mut amt = Amount::from_sat(n1); + amt += Amount::from_sat(n2); + assert_eq!(amt, Amount::from_sat(n1 + n2)); + + let max = cmp::max(n1, n2); + let min = cmp::min(n1, n2); + assert_eq!(Amount::from_sat(max) - Amount::from_sat(min), Amount::from_sat(max - min)); + + 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(ParseAmountError::TooBig) + }, + ); + } + + #[kani::unwind(4)] + #[kani::proof] + fn u_amount_add_homomorphic_checked() { + let n1 = kani::any::(); + let n2 = kani::any::(); + 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_add_homomorphic() { + let n1 = kani::any::(); + let n2 = kani::any::(); + 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 + assert_eq!(SignedAmount::from_sat(n1) + SignedAmount::from_sat(n2), SignedAmount::from_sat(n1 + n2)); + assert_eq!(SignedAmount::from_sat(n1) - SignedAmount::from_sat(n2), SignedAmount::from_sat(n1 - n2)); + + let mut amt = SignedAmount::from_sat(n1); + amt += SignedAmount::from_sat(n2); + assert_eq!(amt, SignedAmount::from_sat(n1 + n2)); + 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(ParseAmountError::Negative) + }, + ); + } + + #[kani::unwind(4)] + #[kani::proof] + fn s_amount_add_homomorphic_checked() { + let n1 = kani::any::(); + let n2 = kani::any::(); + 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 }, + ); + } +} + #[cfg(test)] mod tests { use core::str::FromStr; @@ -1411,27 +1522,18 @@ mod tests { use super::*; #[test] - fn add_sub_mul_div() { + fn mul_div() { let sat = Amount::from_sat; let ssat = SignedAmount::from_sat; - assert_eq!(sat(15) + sat(15), sat(30)); - assert_eq!(sat(15) - sat(15), sat(0)); assert_eq!(sat(14) * 3, sat(42)); assert_eq!(sat(14) / 2, sat(7)); assert_eq!(sat(14) % 3, sat(2)); - assert_eq!(ssat(15) - ssat(20), ssat(-5)); assert_eq!(ssat(-14) * 3, ssat(-42)); assert_eq!(ssat(-14) / 2, ssat(-7)); assert_eq!(ssat(-14) % 3, ssat(-2)); - let mut b = ssat(-5); - b += ssat(13); - assert_eq!(b, ssat(8)); - b -= ssat(3); - assert_eq!(b, ssat(5)); - b *= 6; - assert_eq!(b, ssat(30)); + let mut b = ssat(30); b /= 3; assert_eq!(b, ssat(10)); b %= 3; @@ -1453,25 +1555,13 @@ mod tests { let sat = Amount::from_sat; let ssat = SignedAmount::from_sat; - assert_eq!(sat(42).checked_add(sat(1)), Some(sat(43))); assert_eq!(SignedAmount::max_value().checked_add(ssat(1)), None); assert_eq!(SignedAmount::min_value().checked_sub(ssat(1)), None); assert_eq!(Amount::max_value().checked_add(sat(1)), None); assert_eq!(Amount::min_value().checked_sub(sat(1)), None); - assert_eq!(sat(5).checked_sub(sat(3)), Some(sat(2))); - assert_eq!(sat(5).checked_sub(sat(6)), None); - assert_eq!(ssat(5).checked_sub(ssat(6)), Some(ssat(-1))); - assert_eq!(sat(5).checked_rem(2), Some(sat(1))); - assert_eq!(sat(5).checked_div(2), Some(sat(2))); // integer division assert_eq!(ssat(-6).checked_div(2), Some(ssat(-3))); - - assert_eq!(ssat(-5).positive_sub(ssat(3)), None); - assert_eq!(ssat(5).positive_sub(ssat(-3)), None); - assert_eq!(ssat(3).positive_sub(ssat(5)), None); - assert_eq!(ssat(3).positive_sub(ssat(3)), Some(ssat(0))); - assert_eq!(ssat(5).positive_sub(ssat(3)), Some(ssat(2))); } #[test] @@ -1781,16 +1871,10 @@ mod tests { assert_eq!(Amount::max_value().to_signed(), Err(E::TooBig)); assert_eq!(ua(i64::max_value() as u64).to_signed(), Ok(sa(i64::max_value()))); - assert_eq!(ua(0).to_signed(), Ok(sa(0))); - assert_eq!(ua(1).to_signed(), Ok(sa(1))); - assert_eq!(ua(1).to_signed(), Ok(sa(1))); assert_eq!(ua(i64::max_value() as u64 + 1).to_signed(), Err(E::TooBig)); - assert_eq!(sa(-1).to_unsigned(), Err(E::Negative)); assert_eq!(sa(i64::max_value()).to_unsigned(), Ok(ua(i64::max_value() as u64))); - assert_eq!(sa(0).to_unsigned().unwrap().to_signed(), Ok(sa(0))); - assert_eq!(sa(1).to_unsigned().unwrap().to_signed(), Ok(sa(1))); assert_eq!( sa(i64::max_value()).to_unsigned().unwrap().to_signed(), Ok(sa(i64::max_value())) From d4bfc3d7b1b793e56c04166d95ccf096fa053f39 Mon Sep 17 00:00:00 2001 From: Andrew Poelstra Date: Sun, 27 Nov 2022 18:09:37 +0000 Subject: [PATCH 2/2] github: add Kani to Github CI --- .github/workflows/kani.yml | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 .github/workflows/kani.yml diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml new file mode 100644 index 00000000..2f53fc71 --- /dev/null +++ b/.github/workflows/kani.yml @@ -0,0 +1,14 @@ +# From https://model-checking.github.io/kani/install-github-ci.html +name: Kani CI +on: + pull_request: + push: +jobs: + run-kani: + runs-on: ubuntu-20.04 + steps: + - name: 'Checkout your code.' + uses: actions/checkout@v3 + + - name: 'Run Kani on your code.' + uses: model-checking/kani-github-action@v0.15