bitcoin: update CompactSize Kani proofs
What the developer wrote
Authored by Ismail Daif
bitcoin: update CompactSize Kani proofs
What changed, and why it matters
This commit updates formal verification tests (Kani proofs) for CompactSize encoding. It does not change any production code. The change makes the proofs check that oversized values are correctly rejected, rather than checking round-trips for very large values. There is no indication this fixes a security bug in the actual library.
No action required. This is a test/verification-only change. Reviewers may optionally confirm the Kani proofs pass and that the production CompactSize implementation already rejects oversized values as the proof now expects.
Security signals we found
Formal verification harness update only
No production code changes
No functional behavior change in consensus encoding
No CVE, advisory, or security disclosure referenced
Evidence from the diff
The diff modifies two Kani harnesses in bitcoin/src/consensus/verification.rs. The first harness now constrains its arbitrary u32 input to MAX_COMPACT_SIZE. The second harness is renamed from check_compact_size_large_u64_roundtrip to check_oversized_compact_size_is_rejected and now asserts that values above MAX_COMPACT_SIZE produce ParseError::OversizedCompactSize. No runtime code paths, serialization logic, or error handling behavior in the library are changed.
Changed components
bitcoin/src/consensus/verification.rs (Kani proof tests only)Inspect captured patch +10 / −6
diff --git a/bitcoin/src/consensus/verification.rs b/bitcoin/src/consensus/verification.rs
index d06cf36b..d76859ec 100644
--- a/bitcoin/src/consensus/verification.rs
+++ b/bitcoin/src/consensus/verification.rs
@@ -1,12 +1,14 @@
// SPDX-License-Identifier: CC0-1.0
-use crate::consensus::encode::{ReadExt, WriteExt};
+use crate::consensus::encode::{MAX_COMPACT_SIZE, ReadExt, WriteExt};
+use crate::consensus::{Error, ParseError};
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();
+ kani::assume(x <= MAX_COMPACT_SIZE as u32);
let mut bytes = [0u8; 9];
let mut cursor = Cursor::new(&mut bytes[..]);
cursor.emit_compact_size(x).unwrap();
@@ -17,13 +19,15 @@ fn check_compact_size_roundtrip() {
#[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
+fn check_oversized_compact_size_is_rejected() {
+ let x: u64 = kani::any();
+ kani::assume(x > MAX_COMPACT_SIZE as u64);
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);
+ assert!(matches!(
+ cursor.read_compact_size(),
+ Err(Error::Parse(ParseError::OversizedCompactSize))
+ ));
}
Why this scored 12/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.