//! Phase 121: Parity verification between shadow and existing router
//!
//! ## Responsibility
//!
//! - Compare exit contracts and writes between shadow and existing paths
//! - Log mismatches in dev mode
//! - Fail-fast in strict mode with `freeze_with_hint`
//!
//! ## Comparison Strategy (Minimal & Robust)
//!
//! - Compare structural contracts (exits, writes)
//! - Do NOT compare actual values (too fragile)
//! - Focus on "did we extract the same information?"

use crate::mir::control_tree::step_tree_contract_box::StepTreeContract;
use std::collections::BTreeSet;

/// Mismatch classification
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum MismatchKind {
    /// Exit contract mismatch
    ExitMismatch,
    /// Writes contract mismatch
    WritesMismatch,
    /// Unsupported kind (should not happen for if-only)
    UnsupportedKind,
}

impl MismatchKind {
    /// Get human-readable description
    pub fn description(&self) -> &'static str {
        match self {
            MismatchKind::ExitMismatch => "exit contract mismatch",
            MismatchKind::WritesMismatch => "writes contract mismatch",
            MismatchKind::UnsupportedKind => "unsupported pattern for parity check",
        }
    }
}

/// Result of parity check
#[derive(Debug, Clone)]
pub struct ShadowParityResult {
    /// Whether parity check passed
    pub ok: bool,
    /// Mismatch kind if not ok
    pub mismatch_kind: Option<MismatchKind>,
    /// Hint for debugging (must be non-empty if not ok)
    pub hint: Option<String>,
}

impl ShadowParityResult {
    /// Create successful parity result
    pub fn ok() -> Self {
        Self {
            ok: true,
            mismatch_kind: None,
            hint: None,
        }
    }

    /// Create failed parity result with hint
    pub fn mismatch(kind: MismatchKind, hint: String) -> Self {
        assert!(!hint.is_empty(), "hint must not be empty for mismatch");
        Self {
            ok: false,
            mismatch_kind: Some(kind),
            hint: Some(hint),
        }
    }
}

/// Compare exit contracts between shadow and existing path
///
/// ## Contract
///
/// - Input: Two `StepTreeContract` instances (shadow vs existing)
/// - Compares `exits` field (BTreeSet for deterministic ordering)
/// - Returns mismatch with specific hint if different
pub fn compare_exit_contracts(
    shadow: &StepTreeContract,
    existing: &StepTreeContract,
) -> ShadowParityResult {
    if shadow.exits != existing.exits {
        let hint = format!(
            "exit mismatch: shadow={:?}, existing={:?}",
            shadow.exits, existing.exits
        );
        return ShadowParityResult::mismatch(MismatchKind::ExitMismatch, hint);
    }
    ShadowParityResult::ok()
}

/// Compare writes contracts between shadow and existing path
///
/// ## Contract
///
/// - Input: Two `StepTreeContract` instances (shadow vs existing)
/// - Compares `writes` field (BTreeSet for deterministic ordering)
/// - Returns mismatch with specific hint if different
pub fn compare_writes_contracts(
    shadow: &StepTreeContract,
    existing: &StepTreeContract,
) -> ShadowParityResult {
    if shadow.writes != existing.writes {
        let hint = format!(
            "writes mismatch: shadow={:?}, existing={:?}",
            shadow.writes, existing.writes
        );
        return ShadowParityResult::mismatch(MismatchKind::WritesMismatch, hint);
    }
    ShadowParityResult::ok()
}

/// Full parity check (exits + writes)
///
/// ## Contract
///
/// - Combines exit and writes checks
/// - Returns first mismatch found
/// - Returns ok only if all checks pass
pub fn check_full_parity(
    shadow: &StepTreeContract,
    existing: &StepTreeContract,
) -> ShadowParityResult {
    // Check exits first
    let exit_result = compare_exit_contracts(shadow, existing);
    if !exit_result.ok {
        return exit_result;
    }

    // Check writes second
    let writes_result = compare_writes_contracts(shadow, existing);
    if !writes_result.ok {
        return writes_result;
    }

    ShadowParityResult::ok()
}

/// Phase 122: Verify Normalized JoinModule structure
///
/// ## Contract
///
/// - Checks function count, continuation count, tail-call form, env args
/// - Does NOT check actual execution (RC comparison is optional)
/// - Returns mismatch with hint if structure is invalid
pub fn verify_normalized_structure(
    module: &crate::mir::join_ir::JoinModule,
    expected_env_fields: usize,
) -> ShadowParityResult {
    use crate::mir::join_ir::JoinIrPhase;

    // Check phase
    if !module.is_normalized() {
        let hint = format!(
            "module phase is not Normalized: {:?}",
            module.phase
        );
        return ShadowParityResult::mismatch(MismatchKind::UnsupportedKind, hint);
    }

    // Check function count (Phase 122 minimal: 1 main function)
    if module.functions.is_empty() {
        let hint = "no functions in module".to_string();
        return ShadowParityResult::mismatch(MismatchKind::UnsupportedKind, hint);
    }

    // Check entry point
    if module.entry.is_none() {
        let hint = "no entry point in module".to_string();
        return ShadowParityResult::mismatch(MismatchKind::UnsupportedKind, hint);
    }

    // Check main function exists
    let entry_id = module.entry.unwrap();
    let main_func = module.functions.get(&entry_id);
    if main_func.is_none() {
        let hint = format!("entry function {:?} not found", entry_id);
        return ShadowParityResult::mismatch(MismatchKind::UnsupportedKind, hint);
    }

    // Check env args count (Phase 122: writes only)
    let main_func = main_func.unwrap();
    if main_func.params.len() != expected_env_fields {
        let hint = format!(
            "env args mismatch: expected {}, got {}",
            expected_env_fields,
            main_func.params.len()
        );
        return ShadowParityResult::mismatch(MismatchKind::UnsupportedKind, hint);
    }

    ShadowParityResult::ok()
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::mir::control_tree::step_tree::ExitKind;

    fn make_contract(exits: Vec<ExitKind>, writes: Vec<&str>) -> StepTreeContract {
        StepTreeContract {
            exits: exits.into_iter().collect(),
            writes: writes.into_iter().map(String::from).collect(),
            required_caps: Default::default(),
            cond_sig: Default::default(),
        }
    }

    #[test]
    fn test_exit_parity_match() {
        let c1 = make_contract(vec![ExitKind::Return], vec!["x"]);
        let c2 = make_contract(vec![ExitKind::Return], vec!["x"]);
        let result = compare_exit_contracts(&c1, &c2);
        assert!(result.ok);
    }

    #[test]
    fn test_exit_parity_mismatch() {
        let c1 = make_contract(vec![ExitKind::Return], vec!["x"]);
        let c2 = make_contract(vec![ExitKind::Break], vec!["x"]);
        let result = compare_exit_contracts(&c1, &c2);
        assert!(!result.ok);
        assert_eq!(result.mismatch_kind, Some(MismatchKind::ExitMismatch));
        assert!(result.hint.is_some());
    }

    #[test]
    fn test_writes_parity_match() {
        let c1 = make_contract(vec![ExitKind::Return], vec!["x", "y"]);
        let c2 = make_contract(vec![ExitKind::Return], vec!["x", "y"]);
        let result = compare_writes_contracts(&c1, &c2);
        assert!(result.ok);
    }

    #[test]
    fn test_writes_parity_mismatch() {
        let c1 = make_contract(vec![ExitKind::Return], vec!["x"]);
        let c2 = make_contract(vec![ExitKind::Return], vec!["x", "y"]);
        let result = compare_writes_contracts(&c1, &c2);
        assert!(!result.ok);
        assert_eq!(result.mismatch_kind, Some(MismatchKind::WritesMismatch));
        assert!(result.hint.is_some());
    }

    #[test]
    fn test_full_parity_ok() {
        let c1 = make_contract(vec![ExitKind::Return], vec!["x"]);
        let c2 = make_contract(vec![ExitKind::Return], vec!["x"]);
        let result = check_full_parity(&c1, &c2);
        assert!(result.ok);
    }

    #[test]
    fn test_full_parity_exit_mismatch() {
        let c1 = make_contract(vec![ExitKind::Return], vec!["x"]);
        let c2 = make_contract(vec![ExitKind::Break], vec!["x"]);
        let result = check_full_parity(&c1, &c2);
        assert!(!result.ok);
        assert_eq!(result.mismatch_kind, Some(MismatchKind::ExitMismatch));
    }

    #[test]
    fn test_full_parity_writes_mismatch() {
        let c1 = make_contract(vec![ExitKind::Return], vec!["x"]);
        let c2 = make_contract(vec![ExitKind::Return], vec!["x", "y"]);
        let result = check_full_parity(&c1, &c2);
        assert!(!result.ok);
        assert_eq!(result.mismatch_kind, Some(MismatchKind::WritesMismatch));
    }
}