latticearc 0.6.2

#![deny(unsafe_code)]
#![deny(missing_docs)]

//! Kani model checking proof harnesses for TLS.
//!
//! This module provides proof harnesses for the Kani Rust Verifier to formally
//! verify critical TLS properties. Proofs are executed via `cargo kani`.
//!
//! Properties verified:
//! - Mode selection determinism (same inputs → same mode)
//! - Security level mapping correctness
//! - Configuration validation soundness

use crate::tls::{TlsConfig, TlsMode};

/// Kani verification harness registry.
///
/// Tracks which proof harnesses are available and their verification status.
pub struct KaniProofs {
    /// List of registered proof harness names.
    harnesses: Vec<&'static str>,
}

impl KaniProofs {
    /// Creates a new Kani proof registry with all known harnesses.
    #[must_use]
    pub fn new() -> Self {
        Self {
            harnesses: vec![
                "verify_mode_selection_deterministic",
                "verify_security_level_mapping",
                "verify_config_validation_soundness",
            ],
        }
    }

    /// Get list of registered proof harnesses.
    #[must_use]
    pub fn harnesses(&self) -> &[&'static str] {
        &self.harnesses
    }

    /// Check that mode selection is deterministic:
    /// same TlsMode always produces the same TLS behavior.
    #[must_use]
    pub fn verify_mode_determinism(mode: TlsMode) -> bool {
        let config1 = TlsConfig { mode, ..TlsConfig::default() };
        let config2 = TlsConfig { mode, ..TlsConfig::default() };
        config1.mode == config2.mode
    }

    /// Check that the default config is always Hybrid mode.
    #[must_use]
    pub fn verify_default_is_hybrid() -> bool {
        let config = TlsConfig::default();
        config.mode == TlsMode::Hybrid
    }

    /// Check that config validation accepts valid configs.
    #[must_use]
    pub fn verify_default_validates() -> bool {
        let config = TlsConfig::default();
        config.validate().is_ok()
    }
}

impl Default for KaniProofs {
    fn default() -> Self {
        Self::new()
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_kani_proofs_harness_list_succeeds() {
        let proofs = KaniProofs::new();
        assert_eq!(proofs.harnesses().len(), 3);
        assert!(proofs.harnesses().contains(&"verify_mode_selection_deterministic"));
    }

    #[test]
    fn test_verify_mode_determinism_all_modes_is_deterministic() {
        assert!(KaniProofs::verify_mode_determinism(TlsMode::Classic));
        assert!(KaniProofs::verify_mode_determinism(TlsMode::Hybrid));
        assert!(KaniProofs::verify_mode_determinism(TlsMode::Pq));
    }

    #[test]
    fn test_verify_default_is_hybrid_succeeds() {
        assert!(KaniProofs::verify_default_is_hybrid());
    }

    #[test]
    fn test_verify_default_validates_succeeds() {
        assert!(KaniProofs::verify_default_validates());
    }

    #[test]
    fn test_kani_proofs_default_succeeds() {
        let proofs = KaniProofs::default();
        assert!(!proofs.harnesses().is_empty());
    }
}