From 17bacc6fb6e7fb92dcc4f4b5fdeecc3f756d72a3 Mon Sep 17 00:00:00 2001
From: "Tobin C. Harding" <me@tobin.cc>
Date: Tue, 16 Apr 2024 06:14:33 +1000
Subject: [PATCH 1/3] kani: Remove redundant import

`cargo` is reporting a redundant import warning:

 warning: the item `TryInto` is imported redundantly

Remove the import statement from the `verification` module.
---
 units/src/amount.rs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/units/src/amount.rs b/units/src/amount.rs
index 94cfaca3..687b569d 100644
--- a/units/src/amount.rs
+++ b/units/src/amount.rs
@@ -1885,7 +1885,6 @@ pub mod serde {
 #[cfg(kani)]
 mod verification {
     use std::cmp;
-    use std::convert::TryInto;
 
     use super::*;
 

From 5981b15902a444c295a980adb726ae94becf1c1d Mon Sep 17 00:00:00 2001
From: "Tobin C. Harding" <me@tobin.cc>
Date: Tue, 16 Apr 2024 10:03:26 +1000
Subject: [PATCH 2/3] kani: Rename tests

The tests currently include the word "add" but they test addition as
well as subtraction. Elect to keep the multiple assertions per test and
just make the names more general.
---
 units/src/amount.rs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/units/src/amount.rs b/units/src/amount.rs
index 687b569d..cdfbb6b9 100644
--- a/units/src/amount.rs
+++ b/units/src/amount.rs
@@ -1902,7 +1902,7 @@ mod verification {
     // CI it fails, so we need to set it higher.
     #[kani::unwind(4)]
     #[kani::proof]
-    fn u_amount_add_homomorphic() {
+    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
@@ -1932,7 +1932,7 @@ mod verification {
 
     #[kani::unwind(4)]
     #[kani::proof]
-    fn u_amount_add_homomorphic_checked() {
+    fn u_amount_homomorphic_checked() {
         let n1 = kani::any::<u64>();
         let n2 = kani::any::<u64>();
         assert_eq!(
@@ -1947,7 +1947,7 @@ mod verification {
 
     #[kani::unwind(4)]
     #[kani::proof]
-    fn s_amount_add_homomorphic() {
+    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
@@ -1980,7 +1980,7 @@ mod verification {
 
     #[kani::unwind(4)]
     #[kani::proof]
-    fn s_amount_add_homomorphic_checked() {
+    fn s_amount_homomorphic_checked() {
         let n1 = kani::any::<i64>();
         let n2 = kani::any::<i64>();
         assert_eq!(

From 0f0bd91929aa140ec6ba380316407552679cb9cf Mon Sep 17 00:00:00 2001
From: "Tobin C. Harding" <me@tobin.cc>
Date: Tue, 16 Apr 2024 06:54:32 +1000
Subject: [PATCH 3/3] kani: Pin version to 0.48.0

Kani version `0.49.0` came out 10 days ago, its odd that our CI just
broke today but in an attempt to see if its release related pin to the
version before the latest release.
---
 .github/workflows/rust.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml
index 8837d8fc..e3000372 100644
--- a/.github/workflows/rust.yml
+++ b/.github/workflows/rust.yml
@@ -236,4 +236,5 @@ jobs:
       - name: 'Kani build proofs'
         uses: model-checking/kani-github-action@v1.1
         with:
+          kani-version: '0.48.0'
           args: '--only-codegen'