cipherrun 0.3.0

// Kani Proof Harnesses for Certificate Parsing
//
// These proofs verify that X.509 certificate parsing utility functions
// handle arbitrary input safely without panics or buffer overflows.

/// Proof: Expiry countdown calculation handles all date differences
///
/// Verifies that the duration calculation for certificate expiry
/// does not overflow or panic.
#[cfg(kani)]
#[kani::proof]
fn proof_expiry_duration_calculation() {
    let total_days: u32 = kani::any();
    kani::assume(total_days <= 365 * 100); // Up to 100 years

    // Simulate calculate_duration_parts logic
    let years = total_days / 365;
    let remaining_days = total_days % 365;
    let months = remaining_days / 30;
    let final_days = remaining_days % 30;

    // Verify invariants
    // Note: months can be 0-12 (364/30 = 12.13...) so we use < 13
    kani::assert(months < 13, "Months should be 0-12");
    kani::assert(final_days < 30, "Days should be 0-29");

    // Verify we can reconstruct approximately
    let reconstructed = years * 365 + months * 30 + final_days;
    let diff = if reconstructed >= total_days {
        reconstructed - total_days
    } else {
        total_days - reconstructed
    };
    kani::assert(
        diff < 13, // Allow for month length variance
        "Reconstruction should be close"
    );
}

/// Proof: Certificate fingerprint hex formatting
///
/// Verifies that SHA256 fingerprint formatting doesn't panic.
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(33)]
fn proof_fingerprint_hex_formatting() {
    // SHA256 produces 32 bytes
    let mut digest: [u8; 32] = [0u8; 32];
    let mut i: u8 = 0;
    while i < 32 {
        digest[i as usize] = kani::any();
        i = i.saturating_add(1);
    }

    // Format as colon-separated hex string
    let mut pair_count: u8 = 0;
    let mut j: u8 = 0;
    while j < 32 {
        let b = digest[j as usize];
        let high = (b >> 4) & 0x0F;
        let low = b & 0x0F;

        // Convert to hex chars
        let high_char = if high < 10 {
            (b'0' + high) as char
        } else {
            (b'A' + high - 10) as char
        };
        let low_char = if low < 10 {
            (b'0' + low) as char
        } else {
            (b'A' + low - 10) as char
        };

        let _ = (high_char, low_char);
        pair_count = pair_count.saturating_add(1);
        j = j.saturating_add(1);
    }

    // Verify we get 32 parts
    kani::assert(pair_count == 32, "Should have 32 hex pairs");
}

/// Proof: Base64 pin length calculation
///
/// Verifies that Base64 encoding length calculation is correct.
#[cfg(kani)]
#[kani::proof]
fn proof_base64_pin_length() {
    // SHA256 hash is 32 bytes
    let hash_len: u8 = 32;

    // Base64 encoding: 4 chars for every 3 bytes, rounded up, plus padding
    let base64_len = ((hash_len + 2) / 3) * 4;

    kani::assert(base64_len == 44, "Base64 SHA256 should be 44 characters");
}

/// Proof: Serial number hex conversion
///
/// Verifies that converting certificate serial numbers to hex doesn't panic.
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(21)]
fn proof_serial_number_hex_conversion() {
    // Serial numbers can be up to 20 bytes
    let len: u8 = kani::any();
    kani::assume(len > 0 && len <= 20);

    let mut serial_bytes: [u8; 20] = [0u8; 20];
    let mut i: u8 = 0;
    while i < len {
        serial_bytes[i as usize] = kani::any();
        i = i.saturating_add(1);
    }

    // Convert to hex string
    let mut hex_len: u8 = 0;
    let mut j: u8 = 0;
    while j < len {
        // Safe hex conversion (two chars per byte)
        let b = serial_bytes[j as usize];
        let high = (b >> 4) & 0x0F;
        let low = b & 0x0F;
        let _ = (high, low);
        hex_len = hex_len.saturating_add(2);
        j = j.saturating_add(1);
    }

    kani::assert(hex_len == (len.saturating_mul(2)), "Hex string should be 2x byte length");
}

/// Proof: Key size extraction handles all algorithm types
///
/// Verifies that key size extraction logic handles edge cases.
#[cfg(kani)]
#[kani::proof]
fn proof_key_size_extraction() {
    // Use index to select key type
    let key_type_idx: u8 = kani::any();
    kani::assume(key_type_idx < 3);

    let raw_size: usize = kani::any();
    kani::assume(raw_size <= 16384); // Max reasonable key size in bits

    let key_size: Option<usize> = match key_type_idx {
        0 => Some(raw_size), // RSA
        1 => Some(raw_size), // EC
        _ => None,           // Unknown
    };

    // Verify result is valid
    if let Some(size) = key_size {
        kani::assert(size <= 16384, "Key size should be bounded");
    }
}

/// Proof: EV OID string comparison is safe
///
/// Verifies that OID comparison for EV certificate detection is safe.
#[cfg(kani)]
#[kani::proof]
fn proof_ev_oid_comparison() {
    // Simulate OID string matching
    const EV_OIDS: &[&str] = &[
        "2.16.840.1.114412.2.1",
        "1.3.6.1.4.1.6449.1.2.1.5.1",
        "1.3.6.1.4.1.4146.1.1",
        "2.23.140.1.1",
    ];

    // Select a test OID without formatting to avoid heap use in proofs.
    let idx: u8 = kani::any();
    let test_oid: &str = if (idx as usize) < EV_OIDS.len() {
        EV_OIDS[idx as usize]
    } else {
        "1.2.3.4"
    };

    // Check if matches any EV OID
    let mut is_ev = false;
    let mut i: u8 = 0;
    while i < EV_OIDS.len() as u8 {
        if test_oid == EV_OIDS[i as usize] {
            is_ev = true;
            break;
        }
        i = i.saturating_add(1);
    }

    // Just verify we got a result
    let _ = is_ev;
}

/// Proof: SAN (Subject Alternative Name) extraction bounds
///
/// Verifies that SAN extraction handles arbitrary counts safely.
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(11)]
fn proof_san_extraction_bounds() {
    let san_count: u8 = kani::any();
    kani::assume(san_count <= 10); // Bound for tractability

    let mut sans_count: u8 = 0;
    let mut i: u8 = 0;

    while i < san_count {
        // Simulate adding SAN entries
        let san_type: u8 = kani::any();

        match san_type & 0x03 {
            0 => {
                // DNS name
                let _ = i;
                sans_count = sans_count.saturating_add(1);
            }
            1 => {
                // IP address
                let ip: [u8; 4] = [kani::any(), kani::any(), kani::any(), kani::any()];
                let _ = ip;
                sans_count = sans_count.saturating_add(1);
            }
            _ => {
                // Other - skip
            }
        }
        i = i.saturating_add(1);
    }

    kani::assert(sans_count <= san_count, "SANs should not exceed count");
}

/// Proof: Certificate chain size calculation
///
/// Verifies that chain size calculation doesn't overflow.
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(11)]
fn proof_chain_size_calculation() {
    let cert_count: u8 = kani::any();
    kani::assume(cert_count > 0 && cert_count <= 10);

    let mut total_size: u64 = 0;
    let mut i: u8 = 0;

    while i < cert_count {
        let cert_size: u64 = kani::any();
        kani::assume(cert_size <= 65535); // Max reasonable cert size

        total_size = total_size.saturating_add(cert_size);
        i = i.saturating_add(1);
    }

    let bound = (cert_count as u64) * 65535;
    kani::assert(total_size <= bound, "Total should be bounded");
}

/// Proof: Key usage flags extraction
///
/// Verifies that extracting key usage flags is safe.
#[cfg(kani)]
#[kani::proof]
fn proof_key_usage_extraction() {
    // Simulate key usage bitmap
    let usage_bits: u16 = kani::any();

    let b0 = (usage_bits & 0x0001 != 0) as u8;
    let b1 = (usage_bits & 0x0004 != 0) as u8;
    let b2 = (usage_bits & 0x0020 != 0) as u8;
    let b3 = (usage_bits & 0x0040 != 0) as u8;

    let count = b0.saturating_add(b1).saturating_add(b2).saturating_add(b3);
    kani::assert(count <= 4, "At most 4 usages in this test");
}

/// Proof: CT timestamp extension detection
///
/// Verifies that Certificate Transparency detection is safe.
#[cfg(kani)]
#[kani::proof]
fn proof_ct_extension_detection() {
    let has_sct: bool = kani::any();

    let ct_status: &str = if has_sct {
        "Yes (certificate)"
    } else {
        "No"
    };

    kani::assert(!ct_status.is_empty(), "CT status should not be empty");
}