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

f4617e7 kani: Verify no out of bounds for ArrayVec (Tobin C. Harding)
e378cdd kani: Don't bother checking signed to unsigned conversion (Tobin C. Harding)
50224ee 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 f4617e7; successfully ran local tests

Tree-SHA512: dfef05a7bbb5372415efa8acab7f79801aa7326ac298c007b173786f00bcccd0b1b81d327113723c359fb2797895414a586cc3fb86e495476a03fcac02a96899

Author: apoelstra

internals/Cargo.toml

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

internals/src/array_vec.rs

@@ -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);
+        }
+    }
+}

units/src/amount/verification.rs

@@ -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,39 +42,21 @@ 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)]
 #[kani::proof]
 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 },
-    );
 }