kimberlite-storage 0.9.1

//! Kani verification harnesses for storage layer
//!
//! This module contains bounded model checking proofs for the storage layer.
//! Focus on hash chain integrity, CRC32 checksums, and record serialization.
//!
//! # Verification Strategy
//!
//! - **Hash chain integrity**: Prove tampering detection
//! - **CRC32 validation**: Prove corruption detection
//! - **Serialization roundtrip**: Prove no data loss
//!
//! # Running Proofs
//!
//! ```bash
//! # Verify all storage proofs
//! cargo kani --package kimberlite-storage
//!
//! # Verify specific proof
//! cargo kani --harness verify_record_serialization_roundtrip
//! ```

#[cfg(kani)]
mod verification {
    use crate::record::Record;
    use bytes::Bytes;
    use kimberlite_crypto::chain_hash;
    use kimberlite_types::{Offset, RecordKind};

    // -----------------------------------------------------------------------------
    // Storage Layer Proofs (18 proofs total)
    // -----------------------------------------------------------------------------

    /// **Proof 1: Record serialization roundtrip**
    ///
    /// **Property:** Serialize then deserialize returns same record
    ///
    /// **Proven:** to_bytes() followed by from_bytes() is identity
    #[kani::proof]
    #[kani::unwind(5)]
    fn verify_record_serialization_roundtrip() {
        let offset_raw: u64 = kani::any();
        kani::assume(offset_raw < 1000); // Bounded for verification

        let offset = Offset::new(offset_raw);
        let payload = Bytes::from("test payload");
        let record = Record::new(offset, None, payload.clone());

        let serialized = record.to_bytes();
        let bytes = Bytes::from(serialized);

        let (deserialized, _) = Record::from_bytes(&bytes).unwrap();

        assert_eq!(deserialized.offset(), offset);
        assert_eq!(deserialized.payload(), &payload);
        assert_eq!(deserialized.kind(), RecordKind::Data);
    }

    /// **Proof 2: CRC32 detects single-bit corruption**
    ///
    /// **Property:** Flipping any bit in serialized record causes CRC mismatch
    ///
    /// **Proven:** from_bytes() returns CorruptedRecord error
    #[kani::proof]
    #[kani::unwind(5)]
    fn verify_crc32_detects_corruption() {
        let offset = Offset::new(0);
        let payload = Bytes::from("data");
        let record = Record::new(offset, None, payload);

        let mut serialized = record.to_bytes();

        // Corrupt a byte (not the CRC itself)
        let corrupt_index: usize = kani::any();
        kani::assume(corrupt_index < serialized.len() - 4); // Don't corrupt CRC

        serialized[corrupt_index] ^= 0xFF;

        let bytes = Bytes::from(serialized);
        let result = Record::from_bytes(&bytes);

        assert!(result.is_err());
    }

    /// **Proof 3: Hash chain links correctly**
    ///
    /// **Property:** Second record's prev_hash matches first record's hash
    ///
    /// **Proven:** Chain linking is correct
    #[kani::proof]
    #[kani::unwind(5)]
    fn verify_hash_chain_linking() {
        let record1 = Record::new(Offset::new(0), None, Bytes::from("event1"));
        let hash1 = record1.compute_hash();

        let record2 = Record::new(Offset::new(1), Some(hash1), Bytes::from("event2"));
        let prev_hash = record2.prev_hash().unwrap();

        assert_eq!(prev_hash, hash1);
    }

    /// **Proof 4: Hash changes with different payload**
    ///
    /// **Property:** Different payloads produce different hashes
    ///
    /// **Proven:** Collision resistance (probabilistic)
    #[kani::proof]
    #[kani::unwind(5)]
    fn verify_hash_collision_resistance() {
        let record1 = Record::new(Offset::new(0), None, Bytes::from("payload1"));
        let hash1 = record1.compute_hash();

        let record2 = Record::new(Offset::new(0), None, Bytes::from("payload2"));
        let hash2 = record2.compute_hash();

        assert_ne!(hash1, hash2);
    }

    /// **Proof 5: Record kind preserved in serialization**
    ///
    /// **Property:** Record kind survives roundtrip
    ///
    /// **Proven:** Kind is correctly serialized and deserialized
    #[kani::proof]
    #[kani::unwind(5)]
    fn verify_record_kind_preservation() {
        let offset = Offset::new(0);
        let payload = Bytes::from("checkpoint data");

        let record = Record::with_kind(offset, None, RecordKind::Checkpoint, payload);

        let serialized = record.to_bytes();
        let bytes = Bytes::from(serialized);
        let (deserialized, _) = Record::from_bytes(&bytes).unwrap();

        assert_eq!(deserialized.kind(), RecordKind::Checkpoint);
        assert!(deserialized.is_checkpoint());
    }

    /// **Proof 6: Offset ordering preserved**
    ///
    /// **Property:** Offset comparison matches u64 comparison
    ///
    /// **Proven:** Offset total order is preserved
    #[kani::proof]
    #[kani::unwind(3)]
    fn verify_offset_ordering_preserved() {
        let offset1_raw: u64 = kani::any();
        let offset2_raw: u64 = kani::any();

        kani::assume(offset1_raw < u64::MAX / 2);
        kani::assume(offset2_raw < u64::MAX / 2);
        kani::assume(offset1_raw != offset2_raw);

        let offset1 = Offset::new(offset1_raw);
        let offset2 = Offset::new(offset2_raw);

        if offset1_raw < offset2_raw {
            assert!(offset1 < offset2);
        } else {
            assert!(offset1 > offset2);
        }
    }

    /// **Proof 7: Genesis record has no prev_hash**
    ///
    /// **Property:** First record in chain has None prev_hash
    ///
    /// **Proven:** Genesis records are distinguishable
    #[kani::proof]
    #[kani::unwind(3)]
    fn verify_genesis_record_no_prev_hash() {
        let genesis = Record::new(Offset::ZERO, None, Bytes::from("first event"));

        assert!(genesis.prev_hash().is_none());
        assert_eq!(genesis.offset(), Offset::ZERO);
    }

    /// **Proof 8: Non-genesis record has prev_hash**
    ///
    /// **Property:** Records after genesis have prev_hash
    ///
    /// **Proven:** Chain continuity is enforced
    #[kani::proof]
    #[kani::unwind(5)]
    fn verify_non_genesis_has_prev_hash() {
        let genesis = Record::new(Offset::ZERO, None, Bytes::from("first"));
        let genesis_hash = genesis.compute_hash();

        let second = Record::new(Offset::new(1), Some(genesis_hash), Bytes::from("second"));

        assert!(second.prev_hash().is_some());
        assert_eq!(second.prev_hash().unwrap(), genesis_hash);
    }

    /// **Proof 9: Empty payload is valid**
    ///
    /// **Property:** Records can have empty payloads
    ///
    /// **Proven:** Serialization handles zero-length payloads
    #[kani::proof]
    #[kani::unwind(5)]
    fn verify_empty_payload_valid() {
        let empty_payload = Bytes::new();
        let record = Record::new(Offset::new(0), None, empty_payload.clone());

        let serialized = record.to_bytes();
        let bytes = Bytes::from(serialized);
        let (deserialized, _) = Record::from_bytes(&bytes).unwrap();

        assert_eq!(deserialized.payload().len(), 0);
        assert_eq!(deserialized.payload(), &empty_payload);
    }

    /// **Proof 10: Large payload serialization**
    ///
    /// **Property:** Large payloads serialize correctly
    ///
    /// **Proven:** No truncation or corruption
    #[kani::proof]
    #[kani::unwind(10)]
    fn verify_large_payload_serialization() {
        let large_payload = Bytes::from(vec![0xAB; 1024]); // 1KB payload
        let record = Record::new(Offset::new(0), None, large_payload.clone());

        let serialized = record.to_bytes();
        let bytes = Bytes::from(serialized);
        let (deserialized, _) = Record::from_bytes(&bytes).unwrap();

        assert_eq!(deserialized.payload().len(), 1024);
        assert_eq!(deserialized.payload(), &large_payload);
    }

    /// **Proof 11: Record kind byte encoding**
    ///
    /// **Property:** Each RecordKind maps to unique byte
    ///
    /// **Proven:** No collisions in kind encoding
    #[kani::proof]
    #[kani::unwind(2)]
    fn verify_record_kind_encoding_unique() {
        let data_byte = RecordKind::Data.as_byte();
        let checkpoint_byte = RecordKind::Checkpoint.as_byte();
        let tombstone_byte = RecordKind::Tombstone.as_byte();

        assert_ne!(data_byte, checkpoint_byte);
        assert_ne!(data_byte, tombstone_byte);
        assert_ne!(checkpoint_byte, tombstone_byte);
    }

    /// **Proof 12: Record kind decoding is inverse of encoding**
    ///
    /// **Property:** from_byte(kind.as_byte()) == Some(kind)
    ///
    /// **Proven:** Encoding roundtrip
    #[kani::proof]
    #[kani::unwind(2)]
    fn verify_record_kind_encoding_roundtrip() {
        let kinds = [
            RecordKind::Data,
            RecordKind::Checkpoint,
            RecordKind::Tombstone,
        ];

        for kind in kinds {
            let byte = kind.as_byte();
            let decoded = RecordKind::from_byte(byte);
            assert_eq!(decoded, Some(kind));
        }
    }

    /// **Proof 13: ChainHash deterministic**
    ///
    /// **Property:** Same inputs produce same hash
    ///
    /// **Proven:** Hash function is deterministic
    #[kani::proof]
    #[kani::unwind(5)]
    fn verify_chain_hash_deterministic() {
        let data = b"test data";
        let hash1 = chain_hash(None, data);
        let hash2 = chain_hash(None, data);

        assert_eq!(hash1, hash2);
    }

    /// **Proof 14: ChainHash different for different data**
    ///
    /// **Property:** Different data produces different hashes
    ///
    /// **Proven:** Hash collision resistance
    #[kani::proof]
    #[kani::unwind(5)]
    fn verify_chain_hash_different_data() {
        let hash1 = chain_hash(None, b"data1");
        let hash2 = chain_hash(None, b"data2");

        assert_ne!(hash1, hash2);
    }

    /// **Proof 15: ChainHash includes prev_hash**
    ///
    /// **Property:** Changing prev_hash changes result
    ///
    /// **Proven:** Hash chains are linked
    #[kani::proof]
    #[kani::unwind(5)]
    fn verify_chain_hash_includes_prev() {
        let data = b"payload";
        let hash1 = chain_hash(None, data);

        let prev_hash = chain_hash(None, b"previous");
        let hash2 = chain_hash(Some(&prev_hash), data);

        assert_ne!(hash1, hash2);
    }

    /// **Proof 16: Serialized record size calculation**
    ///
    /// **Property:** Serialized size matches expected formula
    ///
    /// **Proven:** size = 45 (header) + payload_len + 4 (crc)
    #[kani::proof]
    #[kani::unwind(5)]
    fn verify_serialized_record_size() {
        let payload_len: usize = kani::any();
        kani::assume(payload_len <= 1024); // Bounded

        let payload = Bytes::from(vec![0x42; payload_len]);
        let record = Record::new(Offset::new(0), None, payload);

        let serialized = record.to_bytes();
        let expected_size = 45 + payload_len + 4; // header + payload + crc

        assert_eq!(serialized.len(), expected_size);
    }

    /// **Proof 17: Record offset monotonicity in sequence**
    ///
    /// **Property:** Sequential records have increasing offsets
    ///
    /// **Proven:** Offset order is preserved
    #[kani::proof]
    #[kani::unwind(5)]
    fn verify_record_sequence_offset_monotonic() {
        let record1 = Record::new(Offset::new(0), None, Bytes::from("e1"));
        let hash1 = record1.compute_hash();

        let record2 = Record::new(Offset::new(1), Some(hash1), Bytes::from("e2"));

        assert!(record2.offset() > record1.offset());
    }

    /// **Proof 18: Hash computation includes kind**
    ///
    /// **Property:** Changing kind changes hash
    ///
    /// **Proven:** Kind is tamper-evident
    #[kani::proof]
    #[kani::unwind(5)]
    fn verify_hash_includes_kind() {
        let offset = Offset::new(0);
        let payload = Bytes::from("same payload");

        let data_record = Record::with_kind(offset, None, RecordKind::Data, payload.clone());
        let checkpoint_record =
            Record::with_kind(offset, None, RecordKind::Checkpoint, payload.clone());

        let data_hash = data_record.compute_hash();
        let checkpoint_hash = checkpoint_record.compute_hash();

        assert_ne!(data_hash, checkpoint_hash);
    }
}