//! 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;
/// 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 Err(freeze_with_hint) if structure is invalid
pub fn verify_normalized_structure(
    module: &crate::mir::join_ir::JoinModule,
    expected_env_fields: usize,
) -> Result<(), String> {
    use crate::mir::join_ir::{JoinFuncId, JoinInst};
    use crate::mir::join_ir::lowering::error_tags;

    // Check phase
    if !module.is_normalized() {
        return Err(error_tags::freeze_with_hint(
            "phase129/join_k/not_normalized",
            &format!("module phase is not Normalized: {:?}", module.phase),
            "ensure the shadow lowering marks module as Normalized",
        ));
    }

    if module.functions.is_empty() {
        return Err(error_tags::freeze_with_hint(
            "phase129/join_k/no_functions",
            "no functions in module",
            "ensure the shadow lowering emits at least the entry function",
        ));
    }

    // Check entry point
    let entry_id = module.entry.ok_or_else(|| {
        error_tags::freeze_with_hint(
            "phase129/join_k/no_entry",
            "no entry point in module",
            "ensure the shadow lowering sets JoinModule.entry",
        )
    })?;

    // Check entry function exists
    let entry_func = module.functions.get(&entry_id).ok_or_else(|| {
        error_tags::freeze_with_hint(
            "phase129/join_k/entry_missing",
            &format!("entry function {:?} not found", entry_id),
            "ensure the emitted module includes the entry function id",
        )
    })?;

    // Env layout: writes + inputs (SSOT)
    if entry_func.params.len() != expected_env_fields {
        return Err(error_tags::freeze_with_hint(
            "phase129/join_k/env_arity_mismatch",
            &format!(
                "env args mismatch: expected {}, got {}",
                expected_env_fields,
                entry_func.params.len()
            ),
            "ensure env params are built from (writes + inputs) SSOT",
        ));
    }

    // All functions in this shadow module must share the same env param arity.
    for (fid, func) in &module.functions {
        if func.params.len() != expected_env_fields {
            return Err(error_tags::freeze_with_hint(
                "phase129/join_k/env_arity_mismatch",
                &format!(
                    "env args mismatch in {:?}: expected {}, got {}",
                    fid,
                    expected_env_fields,
                    func.params.len()
                ),
                "ensure all continuations share the same env layout (writes + inputs)",
            ));
        }
    }

    // PHI prohibition (Phase 129-B scope): no IfMerge/NestedIfMerge in shadow output.
    for (fid, func) in &module.functions {
        for inst in &func.body {
            if matches!(inst, JoinInst::IfMerge { .. } | JoinInst::NestedIfMerge { .. }) {
                return Err(error_tags::freeze_with_hint(
                    "phase129/join_k/phi_forbidden",
                    &format!("PHI-like merge instruction found in {:?}", fid),
                    "Phase 129-B join_k path forbids IfMerge/NestedIfMerge; use join_k tailcall merge instead",
                ));
            }
        }
    }

    // Detect join_k tailcall form (if present) and validate it.
    fn tailcall_target(func: &crate::mir::join_ir::JoinFunction) -> Option<(JoinFuncId, usize)> {
        match func.body.last()? {
            JoinInst::Call {
                func,
                args,
                k_next: None,
                dst: None,
            } => Some((*func, args.len())),
            _ => None,
        }
    }

    let mut tailcall_targets: Vec<(JoinFuncId, usize)> = Vec::new();
    for func in module.functions.values() {
        if let Some((target, argc)) = tailcall_target(func) {
            tailcall_targets.push((target, argc));
        }
    }

    if tailcall_targets.is_empty() {
        return Ok(());
    }

    // join_k merge should have at least two branch continuations tailcalling the same target.
    if tailcall_targets.len() < 2 {
        return Err(error_tags::freeze_with_hint(
            "phase129/join_k/tailcall_count",
            &format!(
                "join_k tailcall form requires >=2 tailcalls, got {}",
                tailcall_targets.len()
            ),
            "ensure both then/else branches tailcall join_k as the last instruction",
        ));
    }

    let first_target = tailcall_targets[0].0;
    for (target, argc) in &tailcall_targets {
        if *target != first_target {
            return Err(error_tags::freeze_with_hint(
                "phase129/join_k/tailcall_target_mismatch",
                "tailcalls do not target a single join_k function",
                "ensure then/else both tailcall the same join_k function id",
            ));
        }
        if *argc != expected_env_fields {
            return Err(error_tags::freeze_with_hint(
                "phase129/join_k/tailcall_arg_arity_mismatch",
                &format!(
                    "tailcall env arg count mismatch: expected {}, got {}",
                    expected_env_fields, argc
                ),
                "ensure join_k is called with the full env fields list (writes + inputs)",
            ));
        }
    }

    let join_k_func = module.functions.get(&first_target).ok_or_else(|| {
        error_tags::freeze_with_hint(
            "phase129/join_k/join_k_missing",
            "tailcall target join_k function not found in module",
            "ensure join_k is registered in JoinModule.functions",
        )
    })?;

    match join_k_func.body.last() {
        Some(JoinInst::Ret { value: Some(_) }) => Ok(()),
        _ => Err(error_tags::freeze_with_hint(
            "phase129/join_k/join_k_not_ret",
            "join_k must end with Ret(Some(value))",
            "ensure join_k returns the merged env variable and has no post-if continuation in Phase 129-B",
        )),
    }
}

#[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(),
            reads: Default::default(), // Phase 124
            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));
    }
}