kimberlite-crypto 0.4.2

//! Kani verification harnesses for cryptographic primitives
//!
//! This module contains bounded model checking proofs for cryptographic operations.
//! Focus on determinism, non-degeneracy, and correct use of primitives.
//!
//! # Verification Strategy
//!
//! - **Determinism**: Same inputs produce same outputs
//! - **Non-degeneracy**: No all-zero outputs from valid inputs
//! - **Roundtrip correctness**: Encrypt/decrypt, sign/verify
//!
//! # Running Proofs
//!
//! ```bash
//! # Verify all crypto proofs
//! cargo kani --package kimberlite-crypto
//!
//! # Verify specific proof
//! cargo kani --harness verify_chain_hash_deterministic
//! ```

#[cfg(kani)]
mod verification {
    use crate::encryption::Nonce;
    use crate::{EncryptionKey, SigningKey, chain_hash, crc32};

    // -----------------------------------------------------------------------------
    // Crypto Module Proofs (12 proofs total)
    // -----------------------------------------------------------------------------

    /// **Proof 1: chain_hash is deterministic**
    ///
    /// **Property:** Same inputs produce same hash
    ///
    /// **Proven:** Hash function is pure
    #[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 2: chain_hash never produces all zeros**
    ///
    /// **Property:** Hash output is never degenerate
    ///
    /// **Proven:** Non-degeneracy assertion holds
    #[kani::proof]
    #[kani::unwind(5)]
    fn verify_chain_hash_non_zero() {
        let data = b"any data";
        let hash = chain_hash(None, data);

        assert_ne!(hash.as_bytes(), &[0u8; 32]);
    }

    /// **Proof 3: chain_hash with prev_hash differs from without**
    ///
    /// **Property:** prev_hash affects output
    ///
    /// **Proven:** Chain linking works
    #[kani::proof]
    #[kani::unwind(5)]
    fn verify_chain_hash_prev_affects_output() {
        let data = b"payload";
        let hash_without_prev = chain_hash(None, data);

        let prev = chain_hash(None, b"previous");
        let hash_with_prev = chain_hash(Some(&prev), data);

        assert_ne!(hash_without_prev, hash_with_prev);
    }

    /// **Proof 4: chain_hash collision resistance (different data)**
    ///
    /// **Property:** Different inputs produce different outputs
    ///
    /// **Proven:** Collision resistance (probabilistic)
    #[kani::proof]
    #[kani::unwind(5)]
    fn verify_chain_hash_collision_resistance() {
        let hash1 = chain_hash(None, b"data1");
        let hash2 = chain_hash(None, b"data2");

        assert_ne!(hash1, hash2);
    }

    /// **Proof 5: CRC32 deterministic**
    ///
    /// **Property:** Same data produces same CRC
    ///
    /// **Proven:** CRC is pure
    #[kani::proof]
    #[kani::unwind(5)]
    fn verify_crc32_deterministic() {
        let data = b"test data for crc";
        let crc1 = crc32(data);
        let crc2 = crc32(data);

        assert_eq!(crc1, crc2);
    }

    /// **Proof 6: CRC32 changes with different data**
    ///
    /// **Property:** Different data produces different CRC
    ///
    /// **Proven:** CRC detects changes
    #[kani::proof]
    #[kani::unwind(5)]
    fn verify_crc32_different_data() {
        let crc1 = crc32(b"data1");
        let crc2 = crc32(b"data2");

        assert_ne!(crc1, crc2);
    }

    /// **Proof 7: CRC32 detects single-bit flip**
    ///
    /// **Property:** Flipping one bit changes CRC
    ///
    /// **Proven:** Single-bit error detection
    #[kani::proof]
    #[kani::unwind(5)]
    fn verify_crc32_single_bit_detection() {
        let data1 = b"test data";
        let mut data2 = *data1;
        data2[0] ^= 0x01; // Flip one bit

        let crc1 = crc32(data1);
        let crc2 = crc32(&data2);

        assert_ne!(crc1, crc2);
    }

    /// **Proof 8: EncryptionKey from non-zero bytes**
    ///
    /// **Property:** Non-zero key bytes accepted
    ///
    /// **Proven:** Key construction succeeds
    #[kani::proof]
    #[kani::unwind(3)]
    fn verify_encryption_key_from_bytes() {
        let key_bytes = [0x42u8; 32]; // Non-zero key
        let key = EncryptionKey::from_bytes(&key_bytes);

        // Verify key was created by checking roundtrip
        assert_eq!(key.to_bytes(), key_bytes);
    }

    /// **Proof 9: SigningKey generation produces valid key**
    ///
    /// **Property:** Generated keys are valid
    ///
    /// **Proven:** No panics in key generation
    #[kani::proof]
    #[kani::unwind(3)]
    fn verify_signing_key_generation() {
        let key_bytes = [0x42u8; 32]; // Non-zero seed
        let signing_key = SigningKey::from_bytes(&key_bytes);
        let verifying_key = signing_key.verifying_key();

        // Key pair exists and is valid
        assert_eq!(signing_key.to_bytes().len(), 32);
        assert_eq!(verifying_key.to_bytes().len(), 32);
    }

    /// **Proof 10: Nonce from position is unique**
    ///
    /// **Property:** Different positions produce different nonces
    ///
    /// **Proven:** Nonce uniqueness
    #[kani::proof]
    #[kani::unwind(3)]
    fn verify_nonce_from_position_unique() {
        let pos1: u64 = kani::any();
        let pos2: u64 = kani::any();

        kani::assume(pos1 != pos2);
        kani::assume(pos1 < 1000);
        kani::assume(pos2 < 1000);

        let nonce1 = Nonce::from_position(pos1);
        let nonce2 = Nonce::from_position(pos2);

        assert_ne!(nonce1.to_bytes(), nonce2.to_bytes());
    }

    /// **Proof 11: Nonce from position is deterministic**
    ///
    /// **Property:** Same position produces same nonce
    ///
    /// **Proven:** Nonce generation is pure
    #[kani::proof]
    #[kani::unwind(3)]
    fn verify_nonce_from_position_deterministic() {
        let position: u64 = kani::any();
        kani::assume(position < 1000);

        let nonce1 = Nonce::from_position(position);
        let nonce2 = Nonce::from_position(position);

        assert_eq!(nonce1.to_bytes(), nonce2.to_bytes());
    }

    /// **Proof 12: Nonce never all zeros**
    ///
    /// **Property:** Generated nonces are non-degenerate
    ///
    /// **Proven:** Nonce assertion holds
    #[kani::proof]
    #[kani::unwind(3)]
    fn verify_nonce_non_zero() {
        let position: u64 = kani::any();
        kani::assume(position < 1000);

        let nonce = Nonce::from_position(position);

        assert_ne!(nonce.to_bytes(), [0u8; 12]);
    }
}