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 (19x faster than Blake3)
7
8use crate::metrics::OperationMetrics;
9#[cfg(feature = "compression")]
10use lz4_flex;
11use serde::{Deserialize, Serialize};
12use std::sync::{Arc, Mutex};
13#[cfg(not(target_arch = "wasm32"))]
14use std::time::Instant;
15use thiserror::Error;
16
17/// Error types for ByteStorage operations
18#[derive(Debug, Error, Clone, PartialEq)]
19pub enum ByteStorageError {
20    #[error("input exceeds maximum size")]
21    InputTooLarge,
22
23    #[error("decompression ratio exceeds safety limit")]
24    DecompressionBomb,
25
26    #[error("integrity check failed")]
27    ChecksumMismatch,
28
29    #[error("compression failed")]
30    CompressionFailed,
31
32    #[error("decompression failed")]
33    DecompressionFailed,
34
35    #[error("size validation failed")]
36    SizeValidationFailed,
37
38    #[error("serialization failed: {0}")]
39    SerializationFailed(String),
40
41    #[error("deserialization failed: {0}")]
42    DeserializationFailed(String),
43}
44
45// Security constants - Production-safe limits
46const MAX_UNCOMPRESSED_SIZE: usize = 512 * 1024 * 1024; // 512MB limit
47const MAX_COMPRESSED_SIZE: usize = 512 * 1024 * 1024; // 512MB limit
48/// Maximum allowed compression ratio (1000:1)
49/// Uses u64 for integer-only arithmetic to prevent floating-point precision bypass attacks
50const MAX_COMPRESSION_RATIO: u64 = 1000;
51
52/// Storage envelope for raw byte storage
53/// Contains compressed data with integrity checking
54#[derive(Serialize, Deserialize)]
55pub struct StorageEnvelope {
56    /// Compressed payload data
57    pub compressed_data: Vec<u8>,
58    /// xxHash3-64 checksum for integrity (8 bytes)
59    pub checksum: [u8; 8],
60    /// Original size for validation
61    pub original_size: u32,
62    /// Format identifier (e.g., "msgpack")
63    pub format: String,
64}
65
66impl StorageEnvelope {
67    /// Create new envelope with data compression and checksum.
68    ///
69    /// Takes the input by shared slice: it is only compressed and hashed (both
70    /// borrow), never retained, so there is no reason to own it. Avoids a
71    /// full-payload copy (up to `MAX_UNCOMPRESSED_SIZE`) on the write path.
72    #[cfg(all(feature = "compression", feature = "checksum"))]
73    pub fn new(data: &[u8], format: String) -> Result<Self, ByteStorageError> {
74        // Security: Check input size before compression
75        if data.len() > MAX_UNCOMPRESSED_SIZE {
76            return Err(ByteStorageError::InputTooLarge);
77        }
78
79        let original_size = data.len() as u32;
80
81        // Compress with LZ4
82        let compressed_data = lz4_flex::compress(data);
83
84        // Security: Check compressed size
85        if compressed_data.len() > MAX_COMPRESSED_SIZE {
86            return Err(ByteStorageError::InputTooLarge);
87        }
88
89        // Single canonical xxHash3-64 definition (see crate::checksum)
90        let checksum = crate::checksum::checksum(data);
91
92        Ok(StorageEnvelope {
93            compressed_data,
94            checksum,
95            original_size,
96            format,
97        })
98    }
99
100    /// Extract and validate data from envelope
101    #[cfg(all(feature = "compression", feature = "checksum"))]
102    pub fn extract(&self) -> Result<Vec<u8>, ByteStorageError> {
103        // Security: Validate envelope structure first
104        if self.compressed_data.len() > MAX_COMPRESSED_SIZE {
105            return Err(ByteStorageError::InputTooLarge);
106        }
107
108        if self.original_size as usize > MAX_UNCOMPRESSED_SIZE {
109            return Err(ByteStorageError::InputTooLarge);
110        }
111
112        // Security: Check compression ratio for decompression bomb protection
113        // Uses integer arithmetic to prevent floating-point precision bypass attacks
114        let compressed_size = self.compressed_data.len() as u64;
115
116        // Step 1: Zero check - empty compressed data with non-zero original is a bomb
117        if compressed_size == 0 {
118            return Err(ByteStorageError::DecompressionBomb);
119        }
120
121        // Step 2: Checked multiplication - overflow = bomb (fail-safe)
122        let max_allowed_original = MAX_COMPRESSION_RATIO
123            .checked_mul(compressed_size)
124            .ok_or(ByteStorageError::DecompressionBomb)?;
125
126        // Step 3: Compare original_size against computed maximum
127        if (self.original_size as u64) > max_allowed_original {
128            return Err(ByteStorageError::DecompressionBomb);
129        }
130
131        // Decompress (with validated sizes)
132        let decompressed = lz4_flex::decompress(&self.compressed_data, self.original_size as usize)
133            .map_err(|_| ByteStorageError::DecompressionFailed)?;
134
135        // Verify checksum (checksum validation happens AFTER decompression to prevent processing corrupted data)
136        // false -> ChecksumMismatch (preserve the error variant; verify_checksum returns bool)
137        if !crate::checksum::verify_checksum(&decompressed, &self.checksum) {
138            return Err(ByteStorageError::ChecksumMismatch);
139        }
140
141        // Verify size (final safety check)
142        if decompressed.len() != self.original_size as usize {
143            return Err(ByteStorageError::SizeValidationFailed);
144        }
145
146        Ok(decompressed)
147    }
148}
149
150/// Raw byte storage engine (pure Rust core)
151/// Simple store/retrieve interface with no type awareness
152pub struct ByteStorage {
153    default_format: String,
154    /// Last operation metrics (interior mutability for observability)
155    last_metrics: Arc<Mutex<OperationMetrics>>,
156}
157
158impl ByteStorage {
159    /// Create new ByteStorage instance
160    pub fn new(default_format: Option<String>) -> Self {
161        ByteStorage {
162            default_format: default_format.unwrap_or_else(|| "msgpack".to_string()),
163            last_metrics: Arc::new(Mutex::new(OperationMetrics::new())),
164        }
165    }
166
167    /// Store arbitrary bytes with compression and checksums
168    ///
169    /// Returns serialized StorageEnvelope bytes
170    #[cfg(all(feature = "compression", feature = "checksum", feature = "messagepack"))]
171    pub fn store(&self, data: &[u8], format: Option<String>) -> Result<Vec<u8>, ByteStorageError> {
172        // Security: Check input size before processing
173        if data.len() > MAX_UNCOMPRESSED_SIZE {
174            return Err(ByteStorageError::InputTooLarge);
175        }
176
177        let format = format.unwrap_or_else(|| self.default_format.clone());
178
179        // Time compression operation (wasm32: Instant unavailable, use 0)
180        #[cfg(not(target_arch = "wasm32"))]
181        let compression_start = Instant::now();
182        let original_size = data.len();
183
184        let envelope = StorageEnvelope::new(data, format)?;
185
186        #[cfg(not(target_arch = "wasm32"))]
187        let compression_micros = compression_start.elapsed().as_micros() as u64;
188        #[cfg(target_arch = "wasm32")]
189        let compression_micros = 0u64;
190        let compressed_size = envelope.compressed_data.len();
191
192        // Serialize envelope with MessagePack
193        let envelope_bytes = rmp_serde::to_vec(&envelope)
194            .map_err(|e| ByteStorageError::SerializationFailed(e.to_string()))?;
195
196        // Security: Final check on serialized envelope size
197        if envelope_bytes.len() > MAX_COMPRESSED_SIZE {
198            return Err(ByteStorageError::InputTooLarge);
199        }
200
201        // Update metrics for observability
202        if let Ok(mut metrics) = self.last_metrics.lock() {
203            *metrics = OperationMetrics::new().with_compression(
204                compression_micros,
205                original_size,
206                compressed_size,
207            );
208        }
209
210        Ok(envelope_bytes)
211    }
212
213    /// Retrieve and validate stored bytes
214    ///
215    /// Returns (original_data, format_identifier)
216    #[cfg(all(feature = "compression", feature = "checksum", feature = "messagepack"))]
217    pub fn retrieve(&self, envelope_bytes: &[u8]) -> Result<(Vec<u8>, String), ByteStorageError> {
218        // Security: Check envelope size before deserializing
219        if envelope_bytes.len() > MAX_COMPRESSED_SIZE {
220            return Err(ByteStorageError::InputTooLarge);
221        }
222
223        // Deserialize envelope
224        let envelope: StorageEnvelope = rmp_serde::from_slice(envelope_bytes)
225            .map_err(|e| ByteStorageError::DeserializationFailed(e.to_string()))?;
226
227        // Time decompression and checksum operations (wasm32: Instant unavailable, use 0)
228        #[cfg(not(target_arch = "wasm32"))]
229        let decompress_start = Instant::now();
230
231        // Extract and validate data (all security checks happen inside extract())
232        let data = envelope.extract()?;
233
234        #[cfg(not(target_arch = "wasm32"))]
235        let decompress_micros = decompress_start.elapsed().as_micros() as u64;
236        #[cfg(target_arch = "wasm32")]
237        let decompress_micros = 0u64;
238
239        // Calculate compression ratio from stored metadata
240        let compressed_size = envelope.compressed_data.len();
241        let original_size = envelope.original_size as usize;
242
243        // Update metrics for observability
244        if let Ok(mut metrics) = self.last_metrics.lock() {
245            *metrics = OperationMetrics::new().with_compression(
246                decompress_micros,
247                original_size,
248                compressed_size,
249            );
250        }
251
252        Ok((data, envelope.format))
253    }
254
255    /// Get compression ratio for given data
256    #[cfg(feature = "compression")]
257    pub fn estimate_compression(&self, data: &[u8]) -> Result<f64, ByteStorageError> {
258        // Security: Check size before compression
259        if data.len() > MAX_UNCOMPRESSED_SIZE {
260            return Err(ByteStorageError::InputTooLarge);
261        }
262
263        let compressed = lz4_flex::compress(data);
264
265        Ok(data.len() as f64 / compressed.len() as f64)
266    }
267
268    /// Validate envelope without extracting data
269    #[cfg(all(feature = "compression", feature = "checksum", feature = "messagepack"))]
270    pub fn validate(&self, envelope_bytes: &[u8]) -> bool {
271        // Security: Check size before validating
272        if envelope_bytes.len() > MAX_COMPRESSED_SIZE {
273            return false; // Invalid due to size limit
274        }
275
276        match rmp_serde::from_slice::<StorageEnvelope>(envelope_bytes) {
277            Ok(envelope) => envelope.extract().is_ok(),
278            Err(_) => false,
279        }
280    }
281
282    /// Get metrics from last operation
283    ///
284    /// Returns a snapshot of metrics from the most recent store() or retrieve() call
285    pub fn get_last_metrics(&self) -> OperationMetrics {
286        self.last_metrics
287            .lock()
288            .map(|metrics| metrics.clone())
289            .unwrap_or_else(|_| OperationMetrics::new())
290    }
291
292    /// Get security limits
293    pub fn max_uncompressed_size(&self) -> usize {
294        MAX_UNCOMPRESSED_SIZE
295    }
296
297    pub fn max_compressed_size(&self) -> usize {
298        MAX_COMPRESSED_SIZE
299    }
300
301    pub fn max_compression_ratio(&self) -> u64 {
302        MAX_COMPRESSION_RATIO
303    }
304}
305
306impl Default for ByteStorage {
307    fn default() -> Self {
308        Self::new(None)
309    }
310}
311
312#[cfg(all(
313    test,
314    feature = "compression",
315    feature = "checksum",
316    feature = "messagepack"
317))]
318mod tests {
319    use super::*;
320
321    #[test]
322    fn envelope_embeds_canonical_checksum() {
323        let data = b"DRY-guard payload";
324        let envelope = StorageEnvelope::new(data, "test".to_string()).unwrap();
325        assert_eq!(envelope.checksum, crate::checksum::checksum(data));
326    }
327
328    #[test]
329    fn test_storage_envelope_roundtrip() {
330        let data = b"Hello, World! This is test data for compression.".to_vec();
331        let envelope = StorageEnvelope::new(&data, "test".to_string()).unwrap();
332        let extracted = envelope.extract().unwrap();
333        assert_eq!(data, extracted);
334    }
335
336    #[test]
337    fn test_compression_works() {
338        let data = b"aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa".to_vec(); // Highly compressible
339        let envelope = StorageEnvelope::new(&data, "test".to_string()).unwrap();
340        assert!(envelope.compressed_data.len() < data.len());
341    }
342
343    #[test]
344    fn test_checksum_validation() {
345        let mut envelope = StorageEnvelope::new(b"test", "test".to_string()).unwrap();
346        // Corrupt the checksum
347        envelope.checksum[0] = !envelope.checksum[0];
348        // Fail-open guard: the DRY refactor must still surface the specific
349        // ChecksumMismatch variant (not silently succeed on a flipped checksum).
350        assert!(matches!(
351            envelope.extract(),
352            Err(ByteStorageError::ChecksumMismatch)
353        ));
354    }
355
356    #[test]
357    fn test_raw_persistence_roundtrip() {
358        let storage = ByteStorage::new(None);
359        let test_data = b"test data for persistence";
360
361        let stored = storage.store(test_data, None).unwrap();
362        let (retrieved_data, format) = storage.retrieve(&stored).unwrap();
363        assert_eq!(test_data, retrieved_data.as_slice());
364        assert_eq!("msgpack", format);
365    }
366
367    #[test]
368    fn test_size_limits_input() {
369        let storage = ByteStorage::new(None);
370
371        // Create data larger than MAX_UNCOMPRESSED_SIZE (512MB)
372        let large_data = vec![0u8; MAX_UNCOMPRESSED_SIZE + 1];
373
374        let result = storage.store(&large_data, None);
375        assert!(matches!(result, Err(ByteStorageError::InputTooLarge)));
376    }
377
378    #[test]
379    fn test_size_limits_envelope() {
380        // Create data exactly at the limit
381        let max_data = vec![0u8; MAX_UNCOMPRESSED_SIZE];
382        let envelope_result = StorageEnvelope::new(&max_data, "test".to_string());
383
384        // Should succeed at exactly the limit
385        assert!(envelope_result.is_ok());
386    }
387
388    #[test]
389    fn test_compression_ratio_bomb_protection() {
390        // Simulate a decompression bomb scenario
391        let malicious_envelope = StorageEnvelope {
392            compressed_data: vec![0u8; 1000], // Small compressed size
393            checksum: [0u8; 8],               // Fake checksum
394            original_size: 200 * 1024 * 1024, // Claims 200MB original (200x expansion)
395            format: "test".to_string(),
396        };
397
398        let result = malicious_envelope.extract();
399        assert!(matches!(result, Err(ByteStorageError::DecompressionBomb)));
400    }
401
402    // ============================================================================
403    // Decompression Bomb Edge Case Tests (Task 6.1)
404    // ============================================================================
405
406    #[test]
407    fn test_decompression_bomb_zero_compressed_size() {
408        // WHY: Empty compressed data claiming non-zero original is always a bomb
409        let malicious_envelope = StorageEnvelope {
410            compressed_data: vec![], // Zero compressed size
411            checksum: [0u8; 8],
412            original_size: 1000, // Claims 1KB original
413            format: "test".to_string(),
414        };
415
416        let result = malicious_envelope.extract();
417        assert!(
418            matches!(result, Err(ByteStorageError::DecompressionBomb)),
419            "Zero compressed size should be rejected as decompression bomb"
420        );
421    }
422
423    #[test]
424    fn test_decompression_bomb_extreme_ratio() {
425        // WHY: Test extreme ratio that exceeds 1000:1
426        // compressed_size=1, original_size=2000 → 2000:1 ratio exceeds limit
427        // Note: u32::MAX would be caught by InputTooLarge first (> MAX_UNCOMPRESSED_SIZE)
428        let malicious_envelope = StorageEnvelope {
429            compressed_data: vec![0u8; 1], // 1 byte compressed
430            checksum: [0u8; 8],
431            original_size: 2000, // 2000:1 ratio (exceeds 1000:1 limit)
432            format: "test".to_string(),
433        };
434
435        let result = malicious_envelope.extract();
436        assert!(
437            matches!(result, Err(ByteStorageError::DecompressionBomb)),
438            "Extreme ratio should be rejected as bomb: {:?}",
439            result
440        );
441    }
442
443    #[test]
444    fn test_decompression_u32_max_original_size() {
445        // WHY: u32::MAX original_size exceeds MAX_UNCOMPRESSED_SIZE
446        // Should fail with InputTooLarge, not DecompressionBomb
447        // This validates the check order (size limits before ratio)
448        let malicious_envelope = StorageEnvelope {
449            compressed_data: vec![0u8; 1000],
450            checksum: [0u8; 8],
451            original_size: u32::MAX, // ~4GB exceeds 512MB limit
452            format: "test".to_string(),
453        };
454
455        let result = malicious_envelope.extract();
456        assert!(
457            matches!(result, Err(ByteStorageError::InputTooLarge)),
458            "u32::MAX should be rejected as InputTooLarge (exceeds 512MB limit): {:?}",
459            result
460        );
461    }
462
463    #[test]
464    fn test_decompression_exactly_at_threshold() {
465        // WHY: Exactly 1000:1 ratio should be accepted (pass ratio check)
466        // The test verifies the ratio check passes - subsequent failures are expected
467        // (invalid LZ4 data will fail at decompression or checksum)
468        let envelope = StorageEnvelope {
469            compressed_data: vec![0u8; 100], // 100 bytes compressed (not valid LZ4)
470            checksum: [0u8; 8],
471            original_size: 100_000, // 100KB = exactly 1000:1 ratio
472            format: "test".to_string(),
473        };
474
475        let result = envelope.extract();
476        // KEY: Should NOT fail with DecompressionBomb (ratio check should pass)
477        // Will fail with DecompressionFailed, ChecksumMismatch, or SizeValidationFailed
478        assert!(
479            !matches!(result, Err(ByteStorageError::DecompressionBomb)),
480            "Exactly 1000:1 ratio should pass bomb check: {:?}",
481            result
482        );
483        assert!(
484            result.is_err(),
485            "Invalid data should still fail after ratio check"
486        );
487    }
488
489    #[test]
490    fn test_decompression_just_over_threshold() {
491        // WHY: 1001:1 ratio should be rejected
492        let malicious_envelope = StorageEnvelope {
493            compressed_data: vec![0u8; 100], // 100 bytes compressed
494            checksum: [0u8; 8],
495            original_size: 100_001, // 100.001KB = 1000.01:1 ratio (just over)
496            format: "test".to_string(),
497        };
498
499        let result = malicious_envelope.extract();
500        assert!(
501            matches!(result, Err(ByteStorageError::DecompressionBomb)),
502            "Just over 1000:1 ratio should be rejected as bomb"
503        );
504    }
505
506    #[test]
507    fn test_decompression_bomb_integer_boundary() {
508        // WHY: Test near u64 overflow boundary
509        // MAX_COMPRESSION_RATIO (1000) * compressed_size must not overflow
510        // u64::MAX / 1000 ≈ 18,446,744,073,709,551 is max safe compressed_size
511        // But we're constrained by MAX_COMPRESSED_SIZE (512MB), so overflow is unlikely
512        // This test verifies the check works at realistic boundary
513
514        let envelope = StorageEnvelope {
515            compressed_data: vec![0u8; 1_000_000], // 1MB compressed
516            checksum: [0u8; 8],
517            original_size: 1_000_000_000, // 1GB = exactly 1000:1 ratio
518            format: "test".to_string(),
519        };
520
521        // Should fail due to size limit (1GB > MAX_UNCOMPRESSED_SIZE)
522        let result = envelope.extract();
523        assert!(
524            matches!(result, Err(ByteStorageError::InputTooLarge)),
525            "Should fail size check before ratio check: {:?}",
526            result
527        );
528    }
529
530    #[test]
531    fn test_envelope_size_validation() {
532        let storage = ByteStorage::new(None);
533
534        // Create oversized envelope bytes
535        let oversized_envelope = vec![0u8; MAX_COMPRESSED_SIZE + 1];
536
537        let result = storage.retrieve(&oversized_envelope);
538        assert!(matches!(result, Err(ByteStorageError::InputTooLarge)));
539    }
540
541    #[test]
542    fn test_security_limits_getters() {
543        let storage = ByteStorage::new(None);
544
545        assert_eq!(storage.max_uncompressed_size(), MAX_UNCOMPRESSED_SIZE);
546        assert_eq!(storage.max_compressed_size(), MAX_COMPRESSED_SIZE);
547        assert_eq!(storage.max_compression_ratio(), 1000u64);
548    }
549
550    #[test]
551    fn test_compression_estimate_security() {
552        let storage = ByteStorage::new(None);
553
554        // Test with oversized data
555        let large_data = vec![0u8; MAX_UNCOMPRESSED_SIZE + 1];
556        let result = storage.estimate_compression(&large_data);
557        assert!(matches!(result, Err(ByteStorageError::InputTooLarge)));
558    }
559
560    #[test]
561    fn test_validate_security() {
562        let storage = ByteStorage::new(None);
563
564        // Test with oversized envelope
565        let large_envelope = vec![0u8; MAX_COMPRESSED_SIZE + 1];
566        let result = storage.validate(&large_envelope);
567        assert!(!result); // Should be invalid due to size
568    }
569
570    #[test]
571    fn test_edge_case_exactly_at_limits() {
572        // Test data exactly at 512MB
573        let storage = ByteStorage::new(None);
574        let max_size_data = vec![1u8; MAX_UNCOMPRESSED_SIZE]; // Fill with 1s to ensure it's compressible
575
576        // Should succeed at exactly the limit
577        let result = storage.store(&max_size_data, None);
578        assert!(result.is_ok());
579    }
580
581    #[test]
582    fn test_zero_size_edge_case() {
583        let storage = ByteStorage::new(None);
584        let empty_data = vec![];
585
586        let stored = storage.store(&empty_data, None).unwrap();
587        let (retrieved_data, format) = storage.retrieve(&stored).unwrap();
588        assert_eq!(empty_data, retrieved_data);
589        assert_eq!("msgpack", format);
590    }
591
592    #[test]
593    fn test_metrics_collection_on_store() {
594        let storage = ByteStorage::new(None);
595        let test_data = b"aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa".to_vec(); // Compressible
596
597        // Store data
598        storage.store(&test_data, None).unwrap();
599        let metrics = storage.get_last_metrics();
600
601        // Verify metrics were collected
602        assert!(metrics.compression_ratio > 0.0); // Should have valid compression ratio
603    }
604
605    #[test]
606    fn test_metrics_collection_on_retrieve() {
607        let storage = ByteStorage::new(None);
608        let test_data = b"test data for retrieval metrics";
609
610        // Store then retrieve
611        let stored = storage.store(test_data, None).unwrap();
612        storage.retrieve(&stored).unwrap();
613        let metrics = storage.get_last_metrics();
614
615        // Verify retrieve metrics were collected
616        assert!(metrics.compression_ratio > 0.0); // Should have valid ratio
617    }
618}
619
620// Kani Formal Verification Proofs
621// These proofs use bounded model checking to verify critical security properties
622// Bounded to complete within 10 minutes as per specification requirements
623#[cfg(kani)]
624mod kani_proofs {
625    use super::*;
626
627    /// Verify checksum integrity (corruption detection)
628    /// Property: Any single-bit checksum corruption is always detected
629    #[kani::proof]
630    #[kani::unwind(10)] // Need 8+ for memcmp of 8-byte xxHash3-64 checksum
631    fn verify_checksum_detects_corruption() {
632        // Create symbolic checksum (xxHash3-64 produces 8 bytes)
633        let checksum_a: [u8; 8] = kani::any();
634        let mut checksum_b = checksum_a;
635
636        // Flip exactly one bit
637        let byte_index: usize = kani::any();
638        let bit_index: usize = kani::any();
639        kani::assume(byte_index < 8);
640        kani::assume(bit_index < 8);
641
642        checksum_b[byte_index] ^= 1 << bit_index;
643
644        // Property: Corrupted checksum must differ from original
645        assert_ne!(checksum_a, checksum_b);
646    }
647
648    /// Verify decompression bomb protection (compression ratio limits)
649    /// Property: Malicious compression ratios exceeding 1000x are always rejected
650    /// Uses integer arithmetic to match production implementation
651    #[kani::proof]
652    #[kani::unwind(3)]
653    fn verify_decompression_bomb_protection() {
654        // Symbolic envelope parameters
655        let compressed_size: u64 = kani::any();
656        let original_size: u64 = kani::any();
657
658        // Constrain to reasonable test ranges
659        kani::assume(compressed_size > 0 && compressed_size <= 1000);
660        kani::assume(original_size > 0);
661
662        // Simulate the 3-step check from StorageEnvelope::extract()
663        // Step 1: Zero check already covered by assume
664        // Step 2: Checked multiplication
665        let max_allowed = MAX_COMPRESSION_RATIO.checked_mul(compressed_size);
666
667        // Property: If original_size exceeds max_allowed, extraction must fail
668        if let Some(max) = max_allowed {
669            let would_reject = original_size > max;
670            let exceeds_ratio = original_size > MAX_COMPRESSION_RATIO * compressed_size;
671            assert_eq!(would_reject, exceeds_ratio);
672        } else {
673            // Overflow case: always reject (fail-safe)
674            assert!(true); // Overflow is always rejected
675        }
676    }
677
678    /// Verify size limit enforcement on input
679    /// Property: Inputs exceeding MAX_UNCOMPRESSED_SIZE are always rejected
680    #[kani::proof]
681    #[kani::unwind(3)]
682    fn verify_input_size_limits() {
683        let size: usize = kani::any();
684
685        // Test boundary conditions around the limit
686        kani::assume(size <= MAX_UNCOMPRESSED_SIZE + 100);
687
688        // Property: Size check logic is correct
689        let exceeds_limit = size > MAX_UNCOMPRESSED_SIZE;
690        let should_reject = size > MAX_UNCOMPRESSED_SIZE;
691
692        assert_eq!(exceeds_limit, should_reject);
693    }
694
695    /// Verify size limit enforcement on compressed data
696    /// Property: Compressed data exceeding MAX_COMPRESSED_SIZE is rejected
697    #[kani::proof]
698    #[kani::unwind(3)]
699    fn verify_compressed_size_limits() {
700        let compressed_size: usize = kani::any();
701
702        // Test boundary conditions
703        kani::assume(compressed_size <= MAX_COMPRESSED_SIZE + 100);
704
705        // Property: Size check logic is correct
706        let exceeds_limit = compressed_size > MAX_COMPRESSED_SIZE;
707        let should_reject = compressed_size > MAX_COMPRESSED_SIZE;
708
709        assert_eq!(exceeds_limit, should_reject);
710    }
711
712    /// Verify compression ratio calculation is safe (integer arithmetic)
713    /// Property: Ratio check never panics and correctly identifies bombs
714    #[kani::proof]
715    #[kani::unwind(3)]
716    fn verify_compression_ratio_calculation_safety() {
717        let original_size: u64 = kani::any();
718        let compressed_size: u64 = kani::any();
719
720        // Constrain to prevent division by zero and keep ranges manageable
721        kani::assume(compressed_size > 0);
722        kani::assume(compressed_size <= 10000);
723        kani::assume(original_size <= 100_000_000); // 100MB max for test
724
725        // Property 1: checked_mul never panics (it returns None on overflow)
726        let result = MAX_COMPRESSION_RATIO.checked_mul(compressed_size);
727
728        // Property 2: If multiplication succeeds, comparison is valid
729        if let Some(max_allowed) = result {
730            // The check `original_size > max_allowed` is always safe
731            let is_bomb = original_size > max_allowed;
732
733            // Verify equivalence: is_bomb == (original_size > 1000 * compressed_size)
734            // This holds when no overflow occurred
735            if original_size <= max_allowed {
736                assert!(!is_bomb);
737            } else {
738                assert!(is_bomb);
739            }
740        }
741
742        // Property 3: Zero compressed_size is handled by separate check (not tested here)
743    }
744}
cachekit_core/byte_storage.rs

cachekit_core/
byte_storage.rs
