What the developer wrote
Authored by Alkamal01
Add Kani proof for VarInt round-trip
What changed, and why it matters
This commit only adds two automated formal-verification test cases (Kani proofs) that check Bitcoin's variable-length integer encoding round-trips correctly. It does not change any production code, fix a bug, or introduce a security-relevant behavior change. There is no indication of a vulnerability or security patch.
No security action required. Treat as normal test/verification infrastructure addition.
Security signals we found
No strong security signals were identified.
Evidence from the diff
The commit creates bitcoin/src/consensus/verification.rs containing two Kani harnesses: check_compact_size_roundtrip for arbitrary u32 values and check_compact_size_large_u64_roundtrip for u64 values greater than 0xFFFFFFFF. Both call emit_compact_size and read_compact_size via Cursor-backed buffers and assert equality. The module is conditionally compiled only under #[cfg(kani)]. No runtime code is modified.
Changed components
bitcoin/src/consensus/verification.rs (new test-only Kani verification module)Inspect captured patch +31 / −0
diff --git a/bitcoin/src/consensus/mod.rs b/bitcoin/src/consensus/mod.rs
index dbfa9c4d..a7e16c03 100644
--- a/bitcoin/src/consensus/mod.rs
+++ b/bitcoin/src/consensus/mod.rs
@@ -7,6 +7,8 @@
pub mod encode;
mod error;
+#[cfg(kani)]
+mod verification;
#[cfg(feature = "serde")]
pub mod serde;
diff --git a/bitcoin/src/consensus/verification.rs b/bitcoin/src/consensus/verification.rs
new file mode 100644
index 00000000..d06cf36b
--- /dev/null
+++ b/bitcoin/src/consensus/verification.rs
@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: CC0-1.0
+
+use crate::consensus::encode::{ReadExt, WriteExt};
+use crate::io::Cursor;
+
+#[kani::unwind(10)] // Unwind recursion for read/write operations
+#[kani::proof]
+fn check_compact_size_roundtrip() {
+ let x: u32 = kani::any();
+ let mut bytes = [0u8; 9];
+ let mut cursor = Cursor::new(&mut bytes[..]);
+ cursor.emit_compact_size(x).unwrap();
+ cursor.set_position(0);
+ let y = cursor.read_compact_size().unwrap();
+ assert_eq!(u64::from(x), y);
+}
+
+#[kani::unwind(10)]
+#[kani::proof]
+fn check_compact_size_large_u64_roundtrip() {
+ let x: u64 = kani::any();
+ kani::assume(x > 0xFFFFFFFF); // Force 9-byte encoding
+ let mut bytes = [0u8; 9];
+ let mut cursor = Cursor::new(&mut bytes[..]);
+ cursor.emit_compact_size(x).unwrap();
+ cursor.set_position(0);
+ let y = cursor.read_compact_size().unwrap();
+ assert_eq!(x, y);
+}
Why this scored 15/100
Community notes
Notes can correct, qualify, or add evidence to the AI analysis. Every note shown here has been validated by a human moderator.
The AI analysis stands alone for now. Submit a note if you can add evidence or important context.