Add kani test and remove TODO

Add a kani test to check `div_rem`.
tcharding · Jan 23, 2024 · 66352cb · 66352cb
1 parent d08d3ef
commit 66352cb
Showing 1 changed file with 9 additions and 1 deletion.
diff --git a/bitcoin/src/pow.rs b/bitcoin/src/pow.rs
@@ -1735,7 +1735,6 @@ mod tests {
 mod verification {
     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::proof]
     fn check_mul_u64() {
@@ -1744,4 +1743,13 @@ mod verification {
 
         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);
+    }
 }