use crate::codegen::{self, CodegenError, ExecutionResult, MachineCode};
use crate::emit::{self, EmitError};
use crate::l0_ir::L0Program;
use crate::l1_ir::L1Program;
use crate::parser::{self, ParseError};
use crate::runtime::{InvariantKind, InvariantResult, RuntimeTrace, check_output_determinism, RuntimeEngine};
use crate::translate_validate::{self, VerificationReport};
use crate::verify_l0;
use crate::verify_l1::{self, VerifyError};
use std::collections::HashMap;
use std::fmt;

/// Errors from any stage of the pipeline.
#[derive(Debug)]
pub enum PipelineError {
    Parse(ParseError),
    VerifyL1(VerifyError),
    Emit(EmitError),
    VerifyL0(Vec<verify_l0::L0VerifyError>),
    Codegen(CodegenError),
    TranslationValidation(String),
    Runtime(String),
}

impl fmt::Display for PipelineError {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            PipelineError::Parse(e) => write!(f, "parse: {}", e),
            PipelineError::VerifyL1(e) => write!(f, "L1 verify: {}", e),
            PipelineError::Emit(e) => write!(f, "emit: {}", e),
            PipelineError::VerifyL0(errs) => {
                write!(f, "L0 verify:")?;
                for e in errs {
                    write!(f, " {}", e)?;
                }
                Ok(())
            }
            PipelineError::Codegen(e) => write!(f, "codegen: {}", e),
            PipelineError::TranslationValidation(msg) => write!(f, "translation validation: {}", msg),
            PipelineError::Runtime(msg) => write!(f, "runtime: {}", msg),
        }
    }
}

impl std::error::Error for PipelineError {}

/// All intermediate representations captured during pipeline execution.
pub struct PipelineIR {
    pub l1: L1Program,
    pub l0: L0Program,
    pub machine_code: MachineCode,
}

/// Run the full pipeline: DSL text -> parse -> L1 IR -> verify -> emit L0 IR
/// -> verify -> codegen -> execute.
///
/// Returns both the execution result and captured intermediate representations.
pub fn run(source: &str) -> Result<(ExecutionResult, PipelineIR), PipelineError> {
    // Parse
    let l1 = parser::parse(source).map_err(PipelineError::Parse)?;

    // Verify L1
    verify_l1::verify(&l1).map_err(PipelineError::VerifyL1)?;

    // Emit L0 IR
    let l0 = emit::emit(&l1).map_err(PipelineError::Emit)?;

    // Verify L0
    verify_l0::verify(&l0).map_err(PipelineError::VerifyL0)?;

    // Codegen
    let mc = codegen::codegen(&l0).map_err(PipelineError::Codegen)?;

    // Execute
    let result = codegen::execute(&mc).map_err(PipelineError::Codegen)?;

    let ir = PipelineIR {
        l1,
        l0,
        machine_code: mc,
    };

    Ok((result, ir))
}

/// Dump all intermediate representations for a given DSL input.
/// Returns a human-readable string showing L1 IR, L0 IR, and x86-64 hex.
pub fn dump_ir(source: &str) -> Result<String, PipelineError> {
    let l1 = parser::parse(source).map_err(PipelineError::Parse)?;
    verify_l1::verify(&l1).map_err(PipelineError::VerifyL1)?;
    let l0 = emit::emit(&l1).map_err(PipelineError::Emit)?;
    verify_l0::verify(&l0).map_err(PipelineError::VerifyL0)?;
    let mc = codegen::codegen(&l0).map_err(PipelineError::Codegen)?;

    let mut out = String::new();

    out.push_str("========== L1 IR ==========\n");
    out.push_str(&format!("{}", l1));
    out.push('\n');

    out.push_str("========== L0 IR ==========\n");
    out.push_str(&format!("{}", l0));
    out.push('\n');

    out.push_str("========== x86-64 Machine Code ==========\n");
    out.push_str(&mc.hex_dump());
    out.push('\n');

    Ok(out)
}

/// Run the full verification pipeline: parse → L1 verify → emit → L0 verify → translate validate → report.
///
/// Returns the verification report containing results from all three validation tools.
pub fn verify_translation(source: &str) -> Result<VerificationReport, PipelineError> {
    // Parse
    let l1 = parser::parse(source).map_err(PipelineError::Parse)?;

    // Verify L1
    verify_l1::verify(&l1).map_err(PipelineError::VerifyL1)?;

    // Emit L0 IR
    let l0 = emit::emit(&l1).map_err(PipelineError::Emit)?;

    // Verify L0
    verify_l0::verify(&l0).map_err(PipelineError::VerifyL0)?;

    // Translation validation
    let report = translate_validate::validate(&l1, &l0);

    if !report.all_passed() {
        return Err(PipelineError::TranslationValidation(format!("{}", report)));
    }

    Ok(report)
}

/// Per-step summary of invariant check results.
#[derive(Debug, Clone)]
pub struct StepInvariantSummary {
    pub step: u64,
    pub checks: Vec<(InvariantKind, InvariantResult)>,
}

/// Comprehensive report from the verified execution pipeline.
#[derive(Debug)]
pub struct VerifiedExecutionReport {
    /// Full runtime execution trace (phase transitions, messages, snapshots, outputs).
    pub trace: RuntimeTrace,
    /// Invariant check results grouped by step.
    pub step_invariants: Vec<StepInvariantSummary>,
    /// Final actor states as (name, fields) pairs.
    pub final_states: Vec<(String, Vec<(String, u64)>)>,
    /// Output values from the program.
    pub outputs: Vec<u64>,
    /// Translation validation report.
    pub verification_report: VerificationReport,
    /// Human-readable summary line.
    pub summary: String,
}

impl fmt::Display for VerifiedExecutionReport {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        writeln!(f, "=== Verified Execution Report ===")?;
        writeln!(f)?;

        // Translation validation summary
        writeln!(f, "-- Translation Validation --")?;
        for result in &self.verification_report.results {
            let status = if result.passed { "PASS" } else { "FAIL" };
            writeln!(f, "  [{}] {}", status, result.tool)?;
        }
        writeln!(f)?;

        // Runtime invariants summary
        writeln!(f, "-- Runtime Invariants --")?;
        let total_checks: usize = self.step_invariants.iter()
            .map(|s| s.checks.len())
            .sum();
        let total_passed: usize = self.step_invariants.iter()
            .flat_map(|s| &s.checks)
            .filter(|(_, r)| *r == InvariantResult::Pass)
            .count();
        writeln!(f, "  {} invariant checks across {} steps: {} passed, {} failed",
            total_checks, self.step_invariants.len(), total_passed, total_checks - total_passed)?;

        // Per-kind summary
        let mut kind_counts: HashMap<InvariantKind, (usize, usize)> = HashMap::new();
        for step in &self.step_invariants {
            for (kind, result) in &step.checks {
                let entry = kind_counts.entry(*kind).or_insert((0, 0));
                entry.0 += 1;
                if *result == InvariantResult::Pass {
                    entry.1 += 1;
                }
            }
        }
        for kind in &[
            InvariantKind::Termination,
            InvariantKind::ActorSerialization,
            InvariantKind::MessageIntegrity,
            InvariantKind::StateIsolation,
            InvariantKind::WindowConsistency,
            InvariantKind::OutputDeterminism,
        ] {
            if let Some((total, passed)) = kind_counts.get(kind) {
                let status = if total == passed { "PASS" } else { "FAIL" };
                writeln!(f, "  [{}] {} ({}/{})", status, kind, passed, total)?;
            }
        }
        writeln!(f)?;

        // Final states
        writeln!(f, "-- Final States --")?;
        for (name, fields) in &self.final_states {
            let flds: Vec<String> = fields.iter().map(|(n, v)| format!("{}={}", n, v)).collect();
            writeln!(f, "  {} {{ {} }}", name, flds.join(", "))?;
        }

        // Outputs
        if !self.outputs.is_empty() {
            writeln!(f, "  outputs: {:?}", self.outputs)?;
        }
        writeln!(f)?;

        writeln!(f, "-- Summary --")?;
        writeln!(f, "  {}", self.summary)?;

        Ok(())
    }
}

/// Run the full verified execution pipeline: parse → L1 verify → emit → L0 verify
/// → translation validation → runtime execution with all invariants → report.
pub fn run_verified(source: &str) -> Result<VerifiedExecutionReport, PipelineError> {
    // Parse
    let l1 = parser::parse(source).map_err(PipelineError::Parse)?;

    // Verify L1
    verify_l1::verify(&l1).map_err(PipelineError::VerifyL1)?;

    // Emit L0 IR
    let l0 = emit::emit(&l1).map_err(PipelineError::Emit)?;

    // Verify L0
    verify_l0::verify(&l0).map_err(PipelineError::VerifyL0)?;

    // Translation validation
    let verification_report = translate_validate::validate(&l1, &l0);
    if !verification_report.all_passed() {
        return Err(PipelineError::TranslationValidation(format!("{}", verification_report)));
    }

    // Runtime execution with invariants
    let mut engine = RuntimeEngine::new(&l1);
    let trace = engine.run_with_invariants(true)
        .map_err(|e| PipelineError::Runtime(e.message))?;

    // Output determinism: run a second time and compare
    let mut engine2 = RuntimeEngine::new(&l1);
    let trace2 = engine2.run_with_invariants(false)
        .map_err(|e| PipelineError::Runtime(e.message))?;
    let determinism_result = check_output_determinism(&trace, &trace2);

    // Build step invariant summaries
    let mut step_invariants: Vec<StepInvariantSummary> = Vec::new();
    for check in &trace.invariant_checks {
        let step_summary = step_invariants.iter_mut()
            .find(|s| s.step == check.step);
        match step_summary {
            Some(s) => s.checks.push((check.kind, check.result.clone())),
            None => step_invariants.push(StepInvariantSummary {
                step: check.step,
                checks: vec![(check.kind, check.result.clone())],
            }),
        }
    }

    // Add output determinism to the last step's checks
    if let Some(last) = step_invariants.last_mut() {
        last.checks.push((InvariantKind::OutputDeterminism, determinism_result.clone()));
    }

    // Final states
    let final_states: Vec<(String, Vec<(String, u64)>)> = trace.final_actor_states.iter()
        .map(|snap| (snap.actor_name.clone(), snap.fields.clone()))
        .collect();

    let outputs = trace.all_outputs.clone();

    // Build summary
    let total_checks: usize = step_invariants.iter().map(|s| s.checks.len()).sum();
    let all_invariants_passed = step_invariants.iter()
        .flat_map(|s| &s.checks)
        .all(|(_, r)| *r == InvariantResult::Pass);
    let all_translation_passed = verification_report.all_passed();

    let summary = if all_invariants_passed && all_translation_passed {
        format!(
            "all {} invariant checks passed across {} steps; translation validation passed",
            total_checks, trace.steps.len()
        )
    } else {
        let failed: Vec<String> = step_invariants.iter()
            .flat_map(|s| &s.checks)
            .filter(|(_, r)| *r != InvariantResult::Pass)
            .map(|(k, r)| match r {
                InvariantResult::Fail(msg) => format!("{}: {}", k, msg),
                InvariantResult::Pass => unreachable!(),
            })
            .collect();
        format!("FAILURES: {}", failed.join("; "))
    };

    Ok(VerifiedExecutionReport {
        trace,
        step_invariants,
        final_states,
        outputs,
        verification_report,
        summary,
    })
}

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

    #[test]
    fn counter_end_to_end() {
        let source = include_str!("../examples/counter.l1");
        let (result, _ir) = run(source).expect("counter pipeline should succeed");
        let count = result.read_u64("counter_state", 0).expect("should read counter_state");
        assert_eq!(count, 5, "counter should be 5 after 5 steps");
    }

    #[test]
    fn window_end_to_end() {
        let source = include_str!("../examples/window.l1");
        let (result, _ir) = run(source).expect("window pipeline should succeed");
        let total = result.read_u64("accumulator_state", 0).expect("should read accumulator_state");
        assert_eq!(total, 30, "total should be 30 after 3 steps of Add(10)");
        let observed = result.read_output_values();
        assert_eq!(observed, vec![10, 20, 30], "observed values should be [10, 20, 30]");
    }

    #[test]
    fn counter_ir_dump() {
        let source = include_str!("../examples/counter.l1");
        let dump = dump_ir(source).expect("dump should succeed");
        assert!(dump.contains("========== L1 IR =========="));
        assert!(dump.contains("========== L0 IR =========="));
        assert!(dump.contains("========== x86-64 Machine Code =========="));
        assert!(dump.contains("actor counter"));
        assert!(dump.contains("=== Regions ==="));
        assert!(dump.contains("counter_state"));
    }

    #[test]
    fn window_ir_dump() {
        let source = include_str!("../examples/window.l1");
        let dump = dump_ir(source).expect("dump should succeed");
        assert!(dump.contains("========== L1 IR =========="));
        assert!(dump.contains("accumulator"));
        assert!(dump.contains("output"));
    }

    #[test]
    fn counter_test_vector_full_pipeline() {
        // Full test vector: DSL source -> L1 IR -> L0 IR -> x86-64 -> result
        let source = include_str!("../examples/counter.l1");
        let (result, ir) = run(source).expect("pipeline should succeed");

        // 1. DSL source is the counter.l1 file (inlined via include_str!)
        assert!(source.contains("actor counter"));
        assert!(source.contains("on Increment(amount: u64)"));
        assert!(source.contains("steps: 5"));

        // 2. Expected L1 IR text
        let l1_text = format!("{}", ir.l1);
        assert!(l1_text.contains("actor counter {"));
        assert!(l1_text.contains("count: u64 = 0"));
        assert!(l1_text.contains("window count_view : (count) readers(display)"));
        assert!(l1_text.contains("on Increment(amount: u64) { count = (count + amount) }"));
        assert!(l1_text.contains("leaf ticker {"));
        assert!(l1_text.contains("forward(counter, Increment(1))"));
        assert!(l1_text.contains("leaf display {"));
        assert!(l1_text.contains("pipeline main { ticker -> counter -> display }"));
        assert!(l1_text.contains("steps: 5"));

        // 3. Expected L0 IR text
        let l0_text = format!("{}", ir.l0);
        assert!(l0_text.contains("=== Regions ==="));
        assert!(l0_text.contains("region counter_state : 8 bytes, rw, state"));
        assert!(l0_text.contains("queue"));
        assert!(l0_text.contains("region step_counter : 8 bytes, rw, control"));
        assert!(l0_text.contains("=== Blocks ==="));
        assert!(l0_text.contains("entry:"));
        assert!(l0_text.contains("loop_check:"));
        assert!(l0_text.contains("step:"));
        assert!(l0_text.contains("exit:"));
        assert!(l0_text.contains("load.64"));
        assert!(l0_text.contains("store.64"));
        assert!(l0_text.contains("cmp.lt"));
        assert!(l0_text.contains("branch"));
        assert!(l0_text.contains("queue_push"));
        assert!(l0_text.contains("queue_pop"));
        assert!(l0_text.contains("terminate"));

        // 4. Expected x86-64 bytes (non-empty hex string)
        let hex = ir.machine_code.hex_dump();
        assert!(!hex.is_empty(), "machine code should not be empty");
        // Verify it ends with ret (c3) preceded by the epilogue pops
        assert!(hex.contains("c3"), "machine code should contain ret instruction");

        // 5. Expected execution result
        let count = result.read_u64("counter_state", 0).unwrap();
        assert_eq!(count, 5, "counter should equal step count (5)");
    }

    #[test]
    fn window_test_vector_full_pipeline() {
        // Full test vector: DSL source -> L1 IR -> L0 IR -> x86-64 -> result
        let source = include_str!("../examples/window.l1");
        let (result, ir) = run(source).expect("pipeline should succeed");

        // 1. DSL source
        assert!(source.contains("actor accumulator"));
        assert!(source.contains("on Add(value: u64)"));
        assert!(source.contains("steps: 3"));

        // 2. Expected L1 IR text
        let l1_text = format!("{}", ir.l1);
        assert!(l1_text.contains("actor accumulator {"));
        assert!(l1_text.contains("total: u64 = 0"));
        assert!(l1_text.contains("window total_view : (total) readers(observe)"));
        assert!(l1_text.contains("on Add(value: u64) { total = (total + value) }"));
        assert!(l1_text.contains("leaf source {"));
        assert!(l1_text.contains("forward(accumulator, Add(10))"));
        assert!(l1_text.contains("leaf observe {"));
        assert!(l1_text.contains("emit(total)"));
        assert!(l1_text.contains("pipeline main { source -> accumulator -> observe }"));
        assert!(l1_text.contains("steps: 3"));

        // 3. Expected L0 IR text
        let l0_text = format!("{}", ir.l0);
        assert!(l0_text.contains("region accumulator_state : 8 bytes, rw, state"));
        assert!(l0_text.contains("region output :"));
        assert!(l0_text.contains("output"));
        assert!(l0_text.contains("entry:"));
        assert!(l0_text.contains("queue_push output"));

        // 4. x86-64 bytes
        let hex = ir.machine_code.hex_dump();
        assert!(!hex.is_empty());
        assert!(hex.contains("c3"));

        // 5. Expected execution result
        let total = result.read_u64("accumulator_state", 0).unwrap();
        assert_eq!(total, 30, "total should be 30");
        let observed = result.read_output_values();
        assert_eq!(observed, vec![10, 20, 30], "observed values should be [10, 20, 30]");
    }

    #[test]
    fn pipeline_error_on_invalid_input() {
        let result = run("invalid garbage input");
        assert!(result.is_err());
    }

    #[test]
    fn verify_translation_counter() {
        let source = include_str!("../examples/counter.l1");
        let report = verify_translation(source).expect("counter verification should pass");
        assert!(report.all_passed());
        assert_eq!(report.results.len(), 3);
    }

    #[test]
    fn verify_translation_window() {
        let source = include_str!("../examples/window.l1");
        let report = verify_translation(source).expect("window verification should pass");
        assert!(report.all_passed());
    }

    #[test]
    fn verify_translation_product() {
        let source = include_str!("../examples/product.l1");
        let report = verify_translation(source).expect("product verification should pass");
        assert!(report.all_passed());
    }

    #[test]
    fn verify_translation_invalid_input() {
        let result = verify_translation("invalid garbage");
        assert!(result.is_err());
    }

    // ── Stage 4: Verified Execution Pipeline Tests ──────────────

    #[test]
    fn run_verified_counter_all_invariants_pass() {
        let source = include_str!("../examples/counter.l1");
        let report = run_verified(source).expect("run_verified should succeed for counter");

        // All six invariant kinds should be present
        let all_kinds: std::collections::HashSet<_> = report.step_invariants.iter()
            .flat_map(|s| s.checks.iter().map(|(k, _)| *k))
            .collect();
        assert!(all_kinds.contains(&crate::runtime::InvariantKind::Termination));
        assert!(all_kinds.contains(&crate::runtime::InvariantKind::ActorSerialization));
        assert!(all_kinds.contains(&crate::runtime::InvariantKind::MessageIntegrity));
        assert!(all_kinds.contains(&crate::runtime::InvariantKind::StateIsolation));
        assert!(all_kinds.contains(&crate::runtime::InvariantKind::WindowConsistency));
        assert!(all_kinds.contains(&crate::runtime::InvariantKind::OutputDeterminism));

        // All should pass
        let all_pass = report.step_invariants.iter()
            .flat_map(|s| &s.checks)
            .all(|(_, r)| *r == crate::runtime::InvariantResult::Pass);
        assert!(all_pass, "all invariants should pass for counter");

        // Final state should match
        assert_eq!(report.final_states.len(), 1);
        assert_eq!(report.final_states[0].0, "counter");
        assert_eq!(report.final_states[0].1, vec![("count".to_string(), 5)]);

        // Summary should be positive
        assert!(report.summary.contains("passed"), "summary should indicate success: {}", report.summary);
    }

    #[test]
    fn run_verified_window_all_invariants_pass() {
        let source = include_str!("../examples/window.l1");
        let report = run_verified(source).expect("run_verified should succeed for window");

        let all_pass = report.step_invariants.iter()
            .flat_map(|s| &s.checks)
            .all(|(_, r)| *r == crate::runtime::InvariantResult::Pass);
        assert!(all_pass, "all invariants should pass for window");

        assert_eq!(report.outputs, vec![10, 20, 30]);
        assert!(report.summary.contains("passed"));
    }

    #[test]
    fn run_verified_product_all_invariants_pass() {
        let source = include_str!("../examples/product.l1");
        let report = run_verified(source).expect("run_verified should succeed for product");

        let all_pass = report.step_invariants.iter()
            .flat_map(|s| &s.checks)
            .all(|(_, r)| *r == crate::runtime::InvariantResult::Pass);
        assert!(all_pass, "all invariants should pass for product");

        assert_eq!(report.outputs, vec![21, 42, 63, 84]);
    }

    #[test]
    fn run_verified_report_final_states_match_jit() {
        let source = include_str!("../examples/counter.l1");
        let report = run_verified(source).expect("run_verified should succeed");
        let (jit_result, _) = run(source).expect("JIT should succeed");

        let jit_count = jit_result.read_u64("counter_state", 0).unwrap();
        let verified_count = report.final_states[0].1.iter()
            .find(|(n, _)| n == "count").unwrap().1;
        assert_eq!(verified_count, jit_count, "verified and JIT final states must agree");
    }

    #[test]
    fn run_verified_report_final_states_match_interpreter() {
        let source = include_str!("../examples/window.l1");
        let report = run_verified(source).expect("run_verified should succeed");
        let program = crate::parser::parse(source).unwrap();
        let interp_trace = crate::interpret_l1::interpret(&program).unwrap();

        let verified_total = report.final_states[0].1.iter()
            .find(|(n, _)| n == "total").unwrap().1;
        let interp_total = interp_trace.final_actor_states[0].fields.iter()
            .find(|(n, _)| n == "total").unwrap().1;
        assert_eq!(verified_total, interp_total, "verified and interpreter final states must agree");
        assert_eq!(report.outputs, interp_trace.all_outputs, "verified and interpreter outputs must agree");
    }

    #[test]
    fn run_verified_report_contains_translation_validation() {
        let source = include_str!("../examples/counter.l1");
        let report = run_verified(source).expect("run_verified should succeed");

        assert_eq!(report.verification_report.results.len(), 3, "should have 3 translation validation tool results");
        assert!(report.verification_report.all_passed());
    }

    #[test]
    fn run_verified_report_display_is_readable() {
        let source = include_str!("../examples/counter.l1");
        let report = run_verified(source).expect("run_verified should succeed");
        let text = format!("{}", report);

        assert!(text.contains("Verified Execution Report"));
        assert!(text.contains("Translation Validation"));
        assert!(text.contains("Runtime Invariants"));
        assert!(text.contains("Final States"));
        assert!(text.contains("Summary"));
        assert!(text.contains("counter"));
        assert!(text.contains("count=5"));
    }

    #[test]
    fn run_verified_invalid_input() {
        let result = run_verified("invalid garbage");
        assert!(result.is_err());
    }

    // ── Stage 5: Cross-Validation and Negative Testing ──────────

    // --- Mutated L0 IR tests: corrupt emitted L0, verify translation validation catches it ---

    fn emit_l0_for(source: &str) -> (crate::l1_ir::L1Program, crate::l0_ir::L0Program) {
        let l1 = crate::parser::parse(source).expect("parse");
        crate::verify_l1::verify(&l1).expect("verify L1");
        let l0 = crate::emit::emit(&l1).expect("emit");
        crate::verify_l0::verify(&l0).expect("verify L0");
        (l1, l0)
    }

    #[test]
    fn mutated_l0_counter_add_to_sub_caught() {
        let source = include_str!("../examples/counter.l1");
        let (l1, mut l0) = emit_l0_for(source);

        // Corrupt: change Add to Sub in the step block
        let step = l0.blocks.iter_mut().find(|b| b.name == "step").unwrap();
        let mut mutated = false;
        for op in step.ops.iter_mut() {
            if let crate::l0_ir::Op::Arith { kind, .. } = op {
                if *kind == crate::l0_ir::ArithKind::Add {
                    *kind = crate::l0_ir::ArithKind::Sub;
                    mutated = true;
                    break;
                }
            }
        }
        assert!(mutated, "should have found an Add to corrupt");

        let report = crate::translate_validate::validate(&l1, &l0);
        let trace_result = report.results.iter()
            .find(|r| r.tool == crate::translate_validate::ToolName::TraceEquivalence)
            .unwrap();
        assert!(!trace_result.passed, "trace checker should catch Add→Sub corruption");
    }

    #[test]
    fn mutated_l0_window_add_to_sub_caught() {
        let source = include_str!("../examples/window.l1");
        let (l1, mut l0) = emit_l0_for(source);

        let step = l0.blocks.iter_mut().find(|b| b.name == "step").unwrap();
        for op in step.ops.iter_mut() {
            if let crate::l0_ir::Op::Arith { kind, .. } = op {
                if *kind == crate::l0_ir::ArithKind::Add {
                    *kind = crate::l0_ir::ArithKind::Sub;
                    break;
                }
            }
        }

        let report = crate::translate_validate::validate(&l1, &l0);
        assert!(!report.all_passed(), "should catch Add→Sub mutation in window example");
    }

    #[test]
    fn mutated_l0_product_add_to_mul_caught() {
        let source = include_str!("../examples/product.l1");
        let (l1, mut l0) = emit_l0_for(source);

        // Product uses Add for count and Mul for total — corrupt the Mul to Add
        let step = l0.blocks.iter_mut().find(|b| b.name == "step").unwrap();
        let mut mutated = false;
        for op in step.ops.iter_mut() {
            if let crate::l0_ir::Op::Arith { kind, .. } = op {
                if *kind == crate::l0_ir::ArithKind::Mul {
                    *kind = crate::l0_ir::ArithKind::Add;
                    mutated = true;
                    break;
                }
            }
        }
        assert!(mutated, "should have found a Mul to corrupt");

        let report = crate::translate_validate::validate(&l1, &l0);
        assert!(!report.all_passed(), "should catch Mul→Add mutation in product example");
    }

    #[test]
    fn mutated_l0_remove_queue_pop_caught() {
        let source = include_str!("../examples/counter.l1");
        let (l1, mut l0) = emit_l0_for(source);

        // Remove all queue_pop ops from step block
        let step = l0.blocks.iter_mut().find(|b| b.name == "step").unwrap();
        let before = step.ops.len();
        step.ops.retain(|op| !matches!(op, crate::l0_ir::Op::QueuePop { .. }));
        assert!(step.ops.len() < before, "should have removed queue_pop ops");

        let report = crate::translate_validate::validate(&l1, &l0);
        // Structural checker should catch missing queue_pop
        let structural = report.results.iter()
            .find(|r| r.tool == crate::translate_validate::ToolName::StructuralCorrespondence)
            .unwrap();
        assert!(!structural.passed, "structural checker should catch missing queue_pop");
    }

    #[test]
    fn mutated_l0_wrong_loop_limit_caught() {
        let source = include_str!("../examples/counter.l1");
        let (l1, mut l0) = emit_l0_for(source);

        // Change the loop limit from 5 to 3
        let loop_check = l0.blocks.iter_mut().find(|b| b.name == "loop_check").unwrap();
        for op in loop_check.ops.iter_mut() {
            if let crate::l0_ir::Op::LoadImm { value, .. } = op {
                if *value == 5 {
                    *value = 3;
                    break;
                }
            }
        }

        let report = crate::translate_validate::validate(&l1, &l0);
        // Both trace checker (wrong final state) and BMC (wrong loop limit) should catch this
        assert!(!report.all_passed(), "should catch wrong loop limit");
    }

    #[test]
    fn mutated_l0_remove_state_region_caught() {
        let source = include_str!("../examples/window.l1");
        let (l1, mut l0) = emit_l0_for(source);

        l0.regions.retain(|r| r.name != "accumulator_state");

        let report = crate::translate_validate::validate(&l1, &l0);
        let structural = report.results.iter()
            .find(|r| r.tool == crate::translate_validate::ToolName::StructuralCorrespondence)
            .unwrap();
        assert!(!structural.passed, "structural checker should catch missing state region");
    }

    // --- Round-trip agreement: three-way cross-validation for all examples ---

    fn three_way_agreement(source: &str, actor_name: &str, region_name: &str) {
        // 1. JIT pipeline
        let (jit_result, _) = run(source).expect("JIT pipeline should succeed");

        // 2. Verified runtime
        let report = run_verified(source).expect("verified pipeline should succeed");

        // 3. L1 interpreter
        let program = crate::parser::parse(source).unwrap();
        let interp_trace = crate::interpret_l1::interpret(&program).unwrap();

        // Compare final actor states
        let verified_fields = &report.final_states.iter()
            .find(|(n, _)| n == actor_name).unwrap().1;
        let interp_fields = &interp_trace.final_actor_states.iter()
            .find(|s| s.actor_name == actor_name).unwrap().fields;

        // Verified == Interpreter
        assert_eq!(verified_fields, interp_fields,
            "verified runtime and interpreter must agree on {} final state", actor_name);

        // Verified == JIT (compare each field)
        let mut jit_offset = 0usize;
        for (name, verified_val) in verified_fields {
            let jit_val = jit_result.read_u64(region_name, jit_offset)
                .unwrap_or_else(|| panic!("JIT should have field {} at offset {}", name, jit_offset));
            assert_eq!(*verified_val, jit_val,
                "verified runtime and JIT must agree on {}.{}", actor_name, name);
            jit_offset += 8;
        }

        // Compare outputs
        assert_eq!(report.outputs, interp_trace.all_outputs,
            "verified and interpreter outputs must agree");
        let jit_outputs = jit_result.read_output_values();
        assert_eq!(report.outputs, jit_outputs,
            "verified and JIT outputs must agree");
    }

    #[test]
    fn round_trip_counter_three_way_agreement() {
        three_way_agreement(
            include_str!("../examples/counter.l1"),
            "counter", "counter_state",
        );
    }

    #[test]
    fn round_trip_window_three_way_agreement() {
        three_way_agreement(
            include_str!("../examples/window.l1"),
            "accumulator", "accumulator_state",
        );
    }

    #[test]
    fn round_trip_product_three_way_agreement() {
        three_way_agreement(
            include_str!("../examples/product.l1"),
            "ledger", "ledger_state",
        );
    }
}