Skip to main content

cachekit_core/
byte_storage.rs

1//! LZ4 compression and xxHash3 checksums for raw byte storage.
2//!
3//! Provides integrity-protected byte storage with security validation:
4//! - 512MB size limits for decompression bomb protection
5//! - 1000x max compression ratio enforcement
6//! - xxHash3-64 checksums for corruption detection
7
8#[cfg(feature = "compression")]
9use lz4_flex;
10use serde::{Deserialize, Serialize};
11use thiserror::Error;
12
13/// Error types for ByteStorage operations
14#[derive(Debug, Error, Clone, PartialEq)]
15pub enum ByteStorageError {
16    #[error("input exceeds maximum size")]
17    InputTooLarge,
18
19    #[error("decompression ratio exceeds safety limit")]
20    DecompressionBomb,
21
22    #[error("integrity check failed")]
23    ChecksumMismatch,
24
25    #[error("compression failed")]
26    CompressionFailed,
27
28    #[error("decompression failed")]
29    DecompressionFailed,
30
31    #[error("size validation failed")]
32    SizeValidationFailed,
33
34    #[error("serialization failed: {0}")]
35    SerializationFailed(String),
36
37    #[error("deserialization failed: {0}")]
38    DeserializationFailed(String),
39}
40
41// Security constants - Production-safe limits
42const MAX_UNCOMPRESSED_SIZE: usize = 512 * 1024 * 1024; // 512MB limit
43const MAX_COMPRESSED_SIZE: usize = 512 * 1024 * 1024; // 512MB limit
44/// Maximum allowed compression ratio (1000:1)
45/// Uses u64 for integer-only arithmetic to prevent floating-point precision bypass attacks
46const MAX_COMPRESSION_RATIO: u64 = 1000;
47
48/// Storage envelope for raw byte storage
49/// Contains compressed data with integrity checking
50#[derive(Serialize, Deserialize)]
51pub struct StorageEnvelope {
52    /// Compressed payload data
53    ///
54    /// Serialized as msgpack `bin` (protocol 1.1, `envelope-bin-encoding.md`).
55    /// Scope is strictly this field: `checksum` stays array-of-ints by
56    /// normative exclusion (crypto-adjacent surface — MUST NOT flip).
57    #[serde(with = "serde_bytes")]
58    pub compressed_data: Vec<u8>,
59    /// xxHash3-64 checksum for integrity (8 bytes)
60    pub checksum: [u8; 8],
61    /// Original size for validation
62    pub original_size: u32,
63    /// Format identifier (e.g., "msgpack")
64    pub format: String,
65}
66
67impl StorageEnvelope {
68    /// Create new envelope with data compression and checksum.
69    ///
70    /// Takes the input by shared slice: it is only compressed and hashed (both
71    /// borrow), never retained, so there is no reason to own it. Avoids a
72    /// full-payload copy (up to `MAX_UNCOMPRESSED_SIZE`) on the write path.
73    #[cfg(all(feature = "compression", feature = "checksum"))]
74    pub fn new(data: &[u8], format: String) -> Result<Self, ByteStorageError> {
75        // Security: Check input size before compression
76        if data.len() > MAX_UNCOMPRESSED_SIZE {
77            return Err(ByteStorageError::InputTooLarge);
78        }
79
80        let original_size = data.len() as u32;
81
82        // Compress with LZ4
83        let compressed_data = lz4_flex::compress(data);
84
85        // Security: Check compressed size
86        if compressed_data.len() > MAX_COMPRESSED_SIZE {
87            return Err(ByteStorageError::InputTooLarge);
88        }
89
90        // Single canonical xxHash3-64 definition (see crate::checksum)
91        let checksum = crate::checksum::checksum(data);
92
93        Ok(StorageEnvelope {
94            compressed_data,
95            checksum,
96            original_size,
97            format,
98        })
99    }
100
101    /// Extract and validate data from envelope
102    #[cfg(all(feature = "compression", feature = "checksum"))]
103    pub fn extract(&self) -> Result<Vec<u8>, ByteStorageError> {
104        // Unit tests only: the allocation probe's positive control.
105        #[cfg(test)]
106        crate::read_allocation_probe::reserve_first_control(
107            &self.compressed_data,
108            self.original_size,
109        );
110
111        check_decompression_bound(self.compressed_data.len(), self.original_size)?;
112
113        // Decompress (with validated sizes)
114        let decompressed = lz4_flex::decompress(&self.compressed_data, self.original_size as usize)
115            .map_err(|_| ByteStorageError::DecompressionFailed)?;
116
117        // Verify checksum (checksum validation happens AFTER decompression to prevent processing corrupted data)
118        // false -> ChecksumMismatch (preserve the error variant; verify_checksum returns bool)
119        if !crate::checksum::verify_checksum(&decompressed, &self.checksum) {
120            return Err(ByteStorageError::ChecksumMismatch);
121        }
122
123        // Verify size (final safety check)
124        if decompressed.len() != self.original_size as usize {
125            return Err(ByteStorageError::SizeValidationFailed);
126        }
127
128        Ok(decompressed)
129    }
130}
131
132/// Decompression bound, checked by `extract` before it allocates the output.
133///
134/// A separate function so the Kani proofs verify the predicate `extract`
135/// actually runs, not a restatement of it.
136#[cfg(all(feature = "compression", feature = "checksum"))]
137fn check_decompression_bound(
138    compressed_len: usize,
139    original_size: u32,
140) -> Result<(), ByteStorageError> {
141    // Size caps first
142    if compressed_len > MAX_COMPRESSED_SIZE {
143        return Err(ByteStorageError::InputTooLarge);
144    }
145
146    if original_size as usize > MAX_UNCOMPRESSED_SIZE {
147        return Err(ByteStorageError::InputTooLarge);
148    }
149
150    // Security: Check compression ratio for decompression bomb protection
151    // Uses integer arithmetic to prevent floating-point precision bypass attacks
152    let compressed_size = compressed_len as u64;
153
154    // Step 1: Zero-length compressed data is always a bomb
155    if compressed_size == 0 {
156        return Err(ByteStorageError::DecompressionBomb);
157    }
158
159    // Step 2: Checked multiplication - overflow = bomb (fail-safe)
160    let max_allowed_original = MAX_COMPRESSION_RATIO
161        .checked_mul(compressed_size)
162        .ok_or(ByteStorageError::DecompressionBomb)?;
163
164    // Step 3: Compare original_size against computed maximum
165    if (original_size as u64) > max_allowed_original {
166        return Err(ByteStorageError::DecompressionBomb);
167    }
168
169    Ok(())
170}
171
172/// Raw byte storage engine (pure Rust core)
173/// Simple store/retrieve interface with no type awareness
174pub struct ByteStorage {
175    default_format: String,
176}
177
178impl ByteStorage {
179    /// Create new ByteStorage instance
180    pub fn new(default_format: Option<String>) -> Self {
181        ByteStorage {
182            default_format: default_format.unwrap_or_else(|| "msgpack".to_string()),
183        }
184    }
185
186    /// Store arbitrary bytes with compression and checksums
187    ///
188    /// Returns serialized StorageEnvelope bytes
189    #[cfg(all(feature = "compression", feature = "checksum", feature = "messagepack"))]
190    pub fn store(&self, data: &[u8], format: Option<String>) -> Result<Vec<u8>, ByteStorageError> {
191        // Security: Check input size before processing
192        if data.len() > MAX_UNCOMPRESSED_SIZE {
193            return Err(ByteStorageError::InputTooLarge);
194        }
195
196        let format = format.unwrap_or_else(|| self.default_format.clone());
197
198        let envelope = StorageEnvelope::new(data, format)?;
199
200        // Serialize envelope with MessagePack
201        let envelope_bytes = rmp_serde::to_vec(&envelope)
202            .map_err(|e| ByteStorageError::SerializationFailed(e.to_string()))?;
203
204        // Security: Final check on serialized envelope size
205        if envelope_bytes.len() > MAX_COMPRESSED_SIZE {
206            return Err(ByteStorageError::InputTooLarge);
207        }
208
209        Ok(envelope_bytes)
210    }
211
212    /// Retrieve and validate stored bytes
213    ///
214    /// Returns (original_data, format_identifier)
215    ///
216    /// # Errors
217    ///
218    /// `envelope_bytes` is untrusted. Before it is decoded, a structural
219    /// pre-scan bounds its nesting depth and rejects any header that declares
220    /// more than the input can back (protocol Retrieve Flow, step 2). A
221    /// pre-scan rejection is `DeserializationFailed` whose message starts with
222    /// `decode pre-scan: `, the same variant as any other bytes that do not
223    /// decode as a `StorageEnvelope`.
224    #[cfg(all(feature = "compression", feature = "checksum", feature = "messagepack"))]
225    pub fn retrieve(&self, envelope_bytes: &[u8]) -> Result<(Vec<u8>, String), ByteStorageError> {
226        // Security: Check envelope size before deserializing
227        if envelope_bytes.len() > MAX_COMPRESSED_SIZE {
228            return Err(ByteStorageError::InputTooLarge);
229        }
230
231        let envelope = decode_envelope(envelope_bytes)?;
232
233        // Extract and validate data (all security checks happen inside extract())
234        let data = envelope.extract()?;
235
236        Ok((data, envelope.format))
237    }
238
239    /// Get compression ratio for given data
240    #[cfg(feature = "compression")]
241    pub fn estimate_compression(&self, data: &[u8]) -> Result<f64, ByteStorageError> {
242        // Security: Check size before compression
243        if data.len() > MAX_UNCOMPRESSED_SIZE {
244            return Err(ByteStorageError::InputTooLarge);
245        }
246
247        let compressed = lz4_flex::compress(data);
248
249        Ok(data.len() as f64 / compressed.len() as f64)
250    }
251
252    /// Validate an envelope by fully extracting it and discarding the result
253    ///
254    /// This runs `StorageEnvelope::extract`, so it decompresses the payload and
255    /// allocates up to the decompression bound. It is not a cheap structural
256    /// pre-screen for untrusted envelopes.
257    #[cfg(all(feature = "compression", feature = "checksum", feature = "messagepack"))]
258    pub fn validate(&self, envelope_bytes: &[u8]) -> bool {
259        // Security: Check size before validating
260        if envelope_bytes.len() > MAX_COMPRESSED_SIZE {
261            return false; // Invalid due to size limit
262        }
263
264        match decode_envelope(envelope_bytes) {
265            Ok(envelope) => envelope.extract().is_ok(),
266            Err(_) => false,
267        }
268    }
269
270    /// Get security limits
271    pub fn max_uncompressed_size(&self) -> usize {
272        MAX_UNCOMPRESSED_SIZE
273    }
274
275    pub fn max_compressed_size(&self) -> usize {
276        MAX_COMPRESSED_SIZE
277    }
278
279    pub fn max_compression_ratio(&self) -> u64 {
280        MAX_COMPRESSION_RATIO
281    }
282}
283
284impl Default for ByteStorage {
285    fn default() -> Self {
286        Self::new(None)
287    }
288}
289
290/// Decode untrusted envelope bytes: structural pre-scan first, then the typed
291/// decode. Serde's derive skips an unknown map key with `IgnoredAny`, which
292/// recurses, so the depth bound has to hold before `rmp_serde` sees the bytes.
293#[cfg(all(feature = "compression", feature = "checksum", feature = "messagepack"))]
294fn decode_envelope(envelope_bytes: &[u8]) -> Result<StorageEnvelope, ByteStorageError> {
295    // Nesting bound for the envelope decode. The protocol requires 32..=1024;
296    // 100 matches cachekit-rs and cachekit-ts. A legitimate envelope nests 2 deep.
297    const MAX_DEPTH: usize = 100;
298    crate::check_msgpack_structure(envelope_bytes, MAX_DEPTH).map_err(|what| {
299        ByteStorageError::DeserializationFailed(format!("decode pre-scan: {what}"))
300    })?;
301    rmp_serde::from_slice(envelope_bytes)
302        .map_err(|e| ByteStorageError::DeserializationFailed(e.to_string()))
303}
304
305#[cfg(all(
306    test,
307    feature = "compression",
308    feature = "checksum",
309    feature = "messagepack"
310))]
311mod tests {
312    use super::*;
313
314    #[test]
315    fn envelope_embeds_canonical_checksum() {
316        let data = b"DRY-guard payload";
317        let envelope = StorageEnvelope::new(data, "test".to_string()).unwrap();
318        assert_eq!(envelope.checksum, crate::checksum::checksum(data));
319    }
320
321    #[test]
322    fn test_storage_envelope_roundtrip() {
323        let data = b"Hello, World! This is test data for compression.".to_vec();
324        let envelope = StorageEnvelope::new(&data, "test".to_string()).unwrap();
325        let extracted = envelope.extract().unwrap();
326        assert_eq!(data, extracted);
327    }
328
329    #[test]
330    fn test_compression_works() {
331        let data = b"aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa".to_vec(); // Highly compressible
332        let envelope = StorageEnvelope::new(&data, "test".to_string()).unwrap();
333        assert!(envelope.compressed_data.len() < data.len());
334    }
335
336    #[test]
337    fn test_checksum_validation() {
338        let mut envelope = StorageEnvelope::new(b"test", "test".to_string()).unwrap();
339        // Corrupt the checksum
340        envelope.checksum[0] = !envelope.checksum[0];
341        // Fail-open guard: the DRY refactor must still surface the specific
342        // ChecksumMismatch variant (not silently succeed on a flipped checksum).
343        assert!(matches!(
344            envelope.extract(),
345            Err(ByteStorageError::ChecksumMismatch)
346        ));
347    }
348
349    #[test]
350    fn test_raw_persistence_roundtrip() {
351        let storage = ByteStorage::new(None);
352        let test_data = b"test data for persistence";
353
354        let stored = storage.store(test_data, None).unwrap();
355        let (retrieved_data, format) = storage.retrieve(&stored).unwrap();
356        assert_eq!(test_data, retrieved_data.as_slice());
357        assert_eq!("msgpack", format);
358    }
359
360    #[test]
361    fn test_size_limits_input() {
362        let storage = ByteStorage::new(None);
363
364        // Create data larger than MAX_UNCOMPRESSED_SIZE (512MB)
365        let large_data = vec![0u8; MAX_UNCOMPRESSED_SIZE + 1];
366
367        let result = storage.store(&large_data, None);
368        assert!(matches!(result, Err(ByteStorageError::InputTooLarge)));
369    }
370
371    #[test]
372    fn test_size_limits_envelope() {
373        // Create data exactly at the limit
374        let max_data = vec![0u8; MAX_UNCOMPRESSED_SIZE];
375        let envelope_result = StorageEnvelope::new(&max_data, "test".to_string());
376
377        // Should succeed at exactly the limit
378        assert!(envelope_result.is_ok());
379    }
380
381    #[test]
382    fn test_compression_ratio_bomb_protection() {
383        // Simulate a decompression bomb scenario
384        let malicious_envelope = StorageEnvelope {
385            compressed_data: vec![0u8; 1000], // Small compressed size
386            checksum: [0u8; 8],               // Fake checksum
387            original_size: 200 * 1024 * 1024, // Claims 200MB original (200x expansion)
388            format: "test".to_string(),
389        };
390
391        let result = malicious_envelope.extract();
392        assert!(matches!(result, Err(ByteStorageError::DecompressionBomb)));
393    }
394
395    // ============================================================================
396    // Decompression Bomb Edge Case Tests (Task 6.1)
397    // ============================================================================
398
399    #[test]
400    fn test_decompression_bomb_zero_compressed_size() {
401        // WHY: Empty compressed data claiming non-zero original is always a bomb
402        let malicious_envelope = StorageEnvelope {
403            compressed_data: vec![], // Zero compressed size
404            checksum: [0u8; 8],
405            original_size: 1000, // Claims 1KB original
406            format: "test".to_string(),
407        };
408
409        let result = malicious_envelope.extract();
410        assert!(
411            matches!(result, Err(ByteStorageError::DecompressionBomb)),
412            "Zero compressed size should be rejected as decompression bomb"
413        );
414    }
415
416    #[test]
417    fn test_decompression_bomb_extreme_ratio() {
418        // WHY: Test extreme ratio that exceeds 1000:1
419        // compressed_size=1, original_size=2000 → 2000:1 ratio exceeds limit
420        // Note: u32::MAX would be caught by InputTooLarge first (> MAX_UNCOMPRESSED_SIZE)
421        let malicious_envelope = StorageEnvelope {
422            compressed_data: vec![0u8; 1], // 1 byte compressed
423            checksum: [0u8; 8],
424            original_size: 2000, // 2000:1 ratio (exceeds 1000:1 limit)
425            format: "test".to_string(),
426        };
427
428        let result = malicious_envelope.extract();
429        assert!(
430            matches!(result, Err(ByteStorageError::DecompressionBomb)),
431            "Extreme ratio should be rejected as bomb: {:?}",
432            result
433        );
434    }
435
436    #[test]
437    fn test_decompression_u32_max_original_size() {
438        // WHY: u32::MAX original_size exceeds MAX_UNCOMPRESSED_SIZE
439        // Should fail with InputTooLarge, not DecompressionBomb
440        // This validates the check order (size limits before ratio)
441        let malicious_envelope = StorageEnvelope {
442            compressed_data: vec![0u8; 1000],
443            checksum: [0u8; 8],
444            original_size: u32::MAX, // ~4GB exceeds 512MB limit
445            format: "test".to_string(),
446        };
447
448        let result = malicious_envelope.extract();
449        assert!(
450            matches!(result, Err(ByteStorageError::InputTooLarge)),
451            "u32::MAX should be rejected as InputTooLarge (exceeds 512MB limit): {:?}",
452            result
453        );
454    }
455
456    #[test]
457    fn test_decompression_exactly_at_threshold() {
458        // WHY: Exactly 1000:1 ratio should be accepted (pass ratio check)
459        // The test verifies the ratio check passes - subsequent failures are expected
460        // (invalid LZ4 data will fail at decompression or checksum)
461        let envelope = StorageEnvelope {
462            compressed_data: vec![0u8; 100], // 100 bytes compressed (not valid LZ4)
463            checksum: [0u8; 8],
464            original_size: 100_000, // 100KB = exactly 1000:1 ratio
465            format: "test".to_string(),
466        };
467
468        let result = envelope.extract();
469        // KEY: Should NOT fail with DecompressionBomb (ratio check should pass)
470        // Will fail with DecompressionFailed, ChecksumMismatch, or SizeValidationFailed
471        assert!(
472            !matches!(result, Err(ByteStorageError::DecompressionBomb)),
473            "Exactly 1000:1 ratio should pass bomb check: {:?}",
474            result
475        );
476        assert!(
477            result.is_err(),
478            "Invalid data should still fail after ratio check"
479        );
480    }
481
482    #[test]
483    fn test_decompression_just_over_threshold() {
484        // WHY: 1001:1 ratio should be rejected
485        let malicious_envelope = StorageEnvelope {
486            compressed_data: vec![0u8; 100], // 100 bytes compressed
487            checksum: [0u8; 8],
488            original_size: 100_001, // 100.001KB = 1000.01:1 ratio (just over)
489            format: "test".to_string(),
490        };
491
492        let result = malicious_envelope.extract();
493        assert!(
494            matches!(result, Err(ByteStorageError::DecompressionBomb)),
495            "Just over 1000:1 ratio should be rejected as bomb"
496        );
497    }
498
499    #[test]
500    fn test_decompression_bomb_integer_boundary() {
501        // WHY: Test near u64 overflow boundary
502        // MAX_COMPRESSION_RATIO (1000) * compressed_size must not overflow
503        // u64::MAX / 1000 ≈ 18,446,744,073,709,551 is max safe compressed_size
504        // But we're constrained by MAX_COMPRESSED_SIZE (512MB), so overflow is unlikely
505        // This test verifies the check works at realistic boundary
506
507        let envelope = StorageEnvelope {
508            compressed_data: vec![0u8; 1_000_000], // 1MB compressed
509            checksum: [0u8; 8],
510            original_size: 1_000_000_000, // 1GB = exactly 1000:1 ratio
511            format: "test".to_string(),
512        };
513
514        // Should fail due to size limit (1GB > MAX_UNCOMPRESSED_SIZE)
515        let result = envelope.extract();
516        assert!(
517            matches!(result, Err(ByteStorageError::InputTooLarge)),
518            "Should fail size check before ratio check: {:?}",
519            result
520        );
521    }
522
523    #[test]
524    fn test_extract_rejects_oversized_compressed_data() {
525        // WHY: only the compressed-length cap rejects this envelope. original_size
526        // is under its cap and the ratio is far below 1000:1, and retrieve's
527        // envelope-length check is bypassed by calling extract directly.
528        let envelope = StorageEnvelope {
529            compressed_data: vec![0u8; MAX_COMPRESSED_SIZE + 1],
530            checksum: [0u8; 8],
531            original_size: 1,
532            format: "test".to_string(),
533        };
534
535        assert_eq!(envelope.extract(), Err(ByteStorageError::InputTooLarge));
536    }
537
538    #[test]
539    fn test_envelope_size_validation() {
540        let storage = ByteStorage::new(None);
541
542        // Create oversized envelope bytes
543        let oversized_envelope = vec![0u8; MAX_COMPRESSED_SIZE + 1];
544
545        let result = storage.retrieve(&oversized_envelope);
546        assert!(matches!(result, Err(ByteStorageError::InputTooLarge)));
547    }
548
549    #[test]
550    fn test_security_limits_getters() {
551        let storage = ByteStorage::new(None);
552
553        assert_eq!(storage.max_uncompressed_size(), MAX_UNCOMPRESSED_SIZE);
554        assert_eq!(storage.max_compressed_size(), MAX_COMPRESSED_SIZE);
555        assert_eq!(storage.max_compression_ratio(), 1000u64);
556    }
557
558    #[test]
559    fn test_compression_estimate_security() {
560        let storage = ByteStorage::new(None);
561
562        // Test with oversized data
563        let large_data = vec![0u8; MAX_UNCOMPRESSED_SIZE + 1];
564        let result = storage.estimate_compression(&large_data);
565        assert!(matches!(result, Err(ByteStorageError::InputTooLarge)));
566    }
567
568    #[test]
569    fn test_validate_security() {
570        let storage = ByteStorage::new(None);
571
572        // Test with oversized envelope
573        let large_envelope = vec![0u8; MAX_COMPRESSED_SIZE + 1];
574        let result = storage.validate(&large_envelope);
575        assert!(!result); // Should be invalid due to size
576    }
577
578    #[test]
579    fn test_edge_case_exactly_at_limits() {
580        // Test data exactly at 512MB
581        let storage = ByteStorage::new(None);
582        let max_size_data = vec![1u8; MAX_UNCOMPRESSED_SIZE]; // Fill with 1s to ensure it's compressible
583
584        // Should succeed at exactly the limit
585        let result = storage.store(&max_size_data, None);
586        assert!(result.is_ok());
587    }
588
589    #[test]
590    fn test_zero_size_edge_case() {
591        let storage = ByteStorage::new(None);
592        let empty_data = vec![];
593
594        let stored = storage.store(&empty_data, None).unwrap();
595        let (retrieved_data, format) = storage.retrieve(&stored).unwrap();
596        assert_eq!(empty_data, retrieved_data);
597        assert_eq!("msgpack", format);
598    }
599}
600
601// Kani Formal Verification Proofs
602// These proofs use bounded model checking to verify critical security properties
603// Bounded to complete within 10 minutes as per specification requirements
604#[cfg(kani)]
605mod kani_proofs {
606    use super::*;
607
608    /// Verify checksum integrity (corruption detection)
609    /// Property: Any single-bit checksum corruption is always detected
610    #[kani::proof]
611    #[kani::unwind(10)] // Need 8+ for memcmp of 8-byte xxHash3-64 checksum
612    fn verify_checksum_detects_corruption() {
613        // Create symbolic checksum (xxHash3-64 produces 8 bytes)
614        let checksum_a: [u8; 8] = kani::any();
615        let mut checksum_b = checksum_a;
616
617        // Flip exactly one bit
618        let byte_index: usize = kani::any();
619        let bit_index: usize = kani::any();
620        kani::assume(byte_index < 8);
621        kani::assume(bit_index < 8);
622
623        checksum_b[byte_index] ^= 1 << bit_index;
624
625        // Property: Corrupted checksum must differ from original
626        assert_ne!(checksum_a, checksum_b);
627    }
628
629    // The size/ratio proofs pin the limits as literals instead of reading the
630    // constants, so changing a constant or inverting a comparison in
631    // `check_decompression_bound` fails a proof.
632    const PINNED_MAX_COMPRESSED: u64 = 512 * 1024 * 1024;
633    const PINNED_MAX_UNCOMPRESSED: u64 = 512 * 1024 * 1024;
634    const PINNED_MAX_RATIO: u64 = 1000;
635
636    /// Verify the size caps of the decompression bound
637    /// Property: `InputTooLarge` exactly when either size exceeds 512 MiB, for
638    /// every (compressed length, original_size) pair
639    #[kani::proof]
640    fn verify_decompression_bound_size_caps() {
641        let compressed_len: usize = kani::any();
642        let original_size: u32 = kani::any();
643
644        let over_cap = compressed_len as u64 > PINNED_MAX_COMPRESSED
645            || original_size as u64 > PINNED_MAX_UNCOMPRESSED;
646        let result = check_decompression_bound(compressed_len, original_size);
647
648        assert_eq!(
649            over_cap,
650            matches!(result, Err(ByteStorageError::InputTooLarge))
651        );
652    }
653
654    /// Verify the ratio limit of the decompression bound
655    /// Property: with both sizes within their caps, `DecompressionBomb` exactly
656    /// when the compressed length is zero or the ratio exceeds 1000:1, else Ok
657    #[kani::proof]
658    fn verify_decompression_bound_ratio() {
659        let compressed_len: usize = kani::any();
660        let original_size: u32 = kani::any();
661        kani::assume(compressed_len as u64 <= PINNED_MAX_COMPRESSED);
662        kani::assume(original_size as u64 <= PINNED_MAX_UNCOMPRESSED);
663
664        let is_bomb =
665            compressed_len == 0 || original_size as u64 > PINNED_MAX_RATIO * compressed_len as u64;
666        let result = check_decompression_bound(compressed_len, original_size);
667
668        if is_bomb {
669            assert!(matches!(result, Err(ByteStorageError::DecompressionBomb)));
670        } else {
671            assert!(result.is_ok());
672        }
673    }
674}