// SPDX-License-Identifier: MPL-2.0
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
//! End-to-End Verification Module
//!
//! This module provides runtime verification that the FFI layer
//! correctly implements the semantics proven in the formal proofs.
//!
//! # Verification Approach
//!
//! Each theorem from the proofs is encoded as a property test:
//! 1. Set up initial filesystem state matching proof preconditions
//! 2. Execute the operation
//! 3. Verify the postcondition matches the proof's claim
//!
//! # Theorem Coverage
//!
//! Isabelle and Mizar were archived unchecked on 2026-11-09 (`archive/proofs/`)
//! and are not counted here.
//!
//! | Theorem | Coq | Lean4 | Agda | Z3 |
//! |---------|-----|-------|------|----|
//! | mkdir_rmdir_reversible | ✓ | ✓ | ✓ | ✓ |
//! | create_delete_reversible | ✓ | ✓ | ✓ | ✓ |
//! | write_file_reversible | ✓ | ✗ | ✓ | — |
//! | copy_preserves_source | ✓ | ✗ | ✓ | A |
//! | move_reversible | ✓ | ✗ | ✓ | A |
//! | obliterate_irreversible | ✓ | ✗ | ✓ | A |
//!
//! ✓: the proof builds in that system (the Lean and Coq statements are not yet
//! compared one by one with the Agda source). ✗: the Lean library
//! (`FileContentOperations`, `CopyMoveOperations`, `RMOOperations`) does not
//! build on the pinned toolchain, so CI does not check it. A: the Z3 query runs
//! over asserted axioms (PROOF-POLICY §5 `ASSUMED`). —: no Z3 encoding.
//! Per-obligation status: `EXPLAINME.adoc#proof-ledger`.

use crate::{FfiConfig, FfiContext, FfiResult};
use std::path::PathBuf;

/// Verification result with proof reference
#[derive(Debug)]
pub struct VerificationResult {
    /// Name of the theorem being verified
    pub theorem: String,
    /// Whether the verification passed
    pub passed: bool,
    /// Locations of formal proofs
    pub proof_locations: Vec<String>,
    /// Error message if failed
    pub error: Option<String>,
}

impl VerificationResult {
    fn success(theorem: &str, locations: Vec<&str>) -> Self {
        Self {
            theorem: theorem.to_string(),
            passed: true,
            proof_locations: locations.into_iter().map(String::from).collect(),
            error: None,
        }
    }

    fn failure(theorem: &str, locations: Vec<&str>, error: String) -> Self {
        Self {
            theorem: theorem.to_string(),
            passed: false,
            proof_locations: locations.into_iter().map(String::from).collect(),
            error: Some(error),
        }
    }
}

/// Verification suite for FFI operations
pub struct VerificationSuite {
    sandbox: PathBuf,
}

impl VerificationSuite {
    /// Create a new verification suite with a temporary sandbox
    pub fn new() -> FfiResult<Self> {
        let sandbox = std::env::temp_dir().join(format!("vsh_verify_{}", std::process::id()));
        std::fs::create_dir_all(&sandbox)?;
        Ok(Self { sandbox })
    }

    /// Create a fresh FFI context for testing
    fn fresh_context(&self) -> FfiResult<FfiContext> {
        FfiContext::new(FfiConfig {
            sandbox_root: self.sandbox.clone(),
            audit_enabled: false,
            audit_path: None,
            strict_preconditions: true,
            rmo_passes: 1, // Fast for testing
        })
    }

    /// Clean up the sandbox after a test
    fn cleanup(&self) -> FfiResult<()> {
        if self.sandbox.exists() {
            std::fs::remove_dir_all(&self.sandbox)?;
            std::fs::create_dir_all(&self.sandbox)?;
        }
        Ok(())
    }

    /// Run all verifications
    pub fn run_all(&self) -> FfiResult<Vec<VerificationResult>> {
        let mut results = Vec::new();

        results.push(self.verify_mkdir_rmdir_reversible()?);
        results.push(self.verify_create_delete_reversible()?);
        results.push(self.verify_write_file_reversible()?);
        results.push(self.verify_copy_preserves_source()?);
        results.push(self.verify_move_reversible()?);
        results.push(self.verify_operation_independence()?);

        Ok(results)
    }

    /// Verify: rmdir(mkdir(path, fs)) = fs
    ///
    /// Coq: proofs/coq/filesystem_model.v
    /// ```coq
    /// Theorem mkdir_rmdir_reversible : forall path fs,
    ///   mkdir_precondition path fs ->
    ///   rmdir path (mkdir path fs) = fs.
    /// ```
    pub fn verify_mkdir_rmdir_reversible(&self) -> FfiResult<VerificationResult> {
        self.cleanup()?;
        let mut ctx = self.fresh_context()?;

        let locations = vec![
            "proofs/coq/filesystem_model.v",
            "proofs/lean4/FilesystemModel.lean",
            "proofs/agda/FilesystemModel.agda",
            "proofs/z3/filesystem_operations.smt2",
        ];

        // Initial state: path does not exist
        let test_path = "verify_mkdir";
        let full_path = self.sandbox.join(test_path);

        if full_path.exists() {
            return Ok(VerificationResult::failure(
                "mkdir_rmdir_reversible",
                locations,
                "Precondition failed: path already exists".into(),
            ));
        }

        // Apply: mkdir
        ctx.mkdir(test_path)?;
        if !full_path.exists() {
            return Ok(VerificationResult::failure(
                "mkdir_rmdir_reversible",
                locations,
                "mkdir failed to create directory".into(),
            ));
        }

        // Apply inverse: rmdir
        ctx.rmdir(test_path)?;

        // Verify: fs = original fs (path does not exist)
        if full_path.exists() {
            return Ok(VerificationResult::failure(
                "mkdir_rmdir_reversible",
                locations,
                "rmdir failed to restore original state".into(),
            ));
        }

        Ok(VerificationResult::success("mkdir_rmdir_reversible", locations))
    }

    /// Verify: delete_file(create_file(path, fs)) = fs
    pub fn verify_create_delete_reversible(&self) -> FfiResult<VerificationResult> {
        self.cleanup()?;
        let mut ctx = self.fresh_context()?;

        let locations = vec![
            "proofs/coq/file_operations.v",
            "proofs/lean4/FileOperations.lean",
            "proofs/agda/FileOperations.agda",
            "proofs/z3/filesystem_operations.smt2",
        ];

        let test_path = "verify_create.txt";
        let full_path = self.sandbox.join(test_path);

        if full_path.exists() {
            return Ok(VerificationResult::failure(
                "create_delete_reversible",
                locations,
                "Precondition failed: path already exists".into(),
            ));
        }

        // Apply: create_file
        ctx.create_file(test_path)?;
        if !full_path.exists() {
            return Ok(VerificationResult::failure(
                "create_delete_reversible",
                locations,
                "create_file failed to create file".into(),
            ));
        }

        // Apply inverse: delete_file
        ctx.delete_file(test_path)?;

        if full_path.exists() {
            return Ok(VerificationResult::failure(
                "create_delete_reversible",
                locations,
                "delete_file failed to restore original state".into(),
            ));
        }

        Ok(VerificationResult::success("create_delete_reversible", locations))
    }

    /// Verify: write(path, old, write(path, new, fs)) = fs
    pub fn verify_write_file_reversible(&self) -> FfiResult<VerificationResult> {
        self.cleanup()?;
        let mut ctx = self.fresh_context()?;

        let locations = vec![
            "proofs/coq/file_content_operations.v",
        ];

        let test_path = "verify_write.txt";
        let _full_path = self.sandbox.join(test_path);

        // Create file with initial content
        ctx.create_file(test_path)?;
        let old_content = b"original content";
        ctx.write_file(test_path, old_content)?;

        // Verify initial state
        let content = ctx.read_file(test_path)?;
        if content != old_content {
            return Ok(VerificationResult::failure(
                "write_file_reversible",
                locations,
                "Initial write failed".into(),
            ));
        }

        // Apply: write new content, capture old
        let new_content = b"new content";
        let captured_old = ctx.write_file(test_path, new_content)?;

        // Verify old was captured correctly
        if captured_old != old_content {
            return Ok(VerificationResult::failure(
                "write_file_reversible",
                locations,
                format!("Old content not captured correctly: {:?} != {:?}",
                    captured_old, old_content),
            ));
        }

        // Apply inverse: write old content back
        ctx.write_file(test_path, &captured_old)?;

        // Verify: fs = original fs
        let final_content = ctx.read_file(test_path)?;
        if final_content != old_content {
            return Ok(VerificationResult::failure(
                "write_file_reversible",
                locations,
                "write_file inverse failed to restore original state".into(),
            ));
        }

        Ok(VerificationResult::success("write_file_reversible", locations))
    }

    /// Verify: copy(src, dst, fs) preserves src unchanged
    pub fn verify_copy_preserves_source(&self) -> FfiResult<VerificationResult> {
        self.cleanup()?;
        let mut ctx = self.fresh_context()?;

        let locations = vec![
            "proofs/z3/copy_move_operations.smt2",
            "proofs/lean4/CopyMoveOperations.lean",
            "proofs/agda/CopyMoveOperations.agda",
        ];

        let src_path = "verify_copy_src.txt";
        let dst_path = "verify_copy_dst.txt";

        // Create source file with content
        let src_content = b"source file content";
        ctx.create_file(src_path)?;
        ctx.write_file(src_path, src_content)?;

        // Verify source content
        let src_before = ctx.read_file(src_path)?;

        // Apply: copy
        ctx.copy_file(src_path, dst_path)?;

        // Verify: source unchanged
        let src_after = ctx.read_file(src_path)?;
        if src_before != src_after {
            return Ok(VerificationResult::failure(
                "copy_preserves_source",
                locations,
                "Source file modified by copy operation".into(),
            ));
        }

        // Verify: destination has same content
        let dst_content = ctx.read_file(dst_path)?;
        if dst_content != src_content {
            return Ok(VerificationResult::failure(
                "copy_preserves_source",
                locations,
                "Destination content differs from source".into(),
            ));
        }

        Ok(VerificationResult::success("copy_preserves_source", locations))
    }

    /// Verify: move(dst, src, move(src, dst, fs)) = fs
    pub fn verify_move_reversible(&self) -> FfiResult<VerificationResult> {
        self.cleanup()?;
        let mut ctx = self.fresh_context()?;

        let locations = vec![
            "proofs/z3/copy_move_operations.smt2",
            "proofs/lean4/CopyMoveOperations.lean",
            "proofs/agda/CopyMoveOperations.agda",
        ];

        let src_path = "verify_move_src.txt";
        let dst_path = "verify_move_dst.txt";
        let src_full = self.sandbox.join(src_path);
        let dst_full = self.sandbox.join(dst_path);

        // Create source file with content
        let content = b"move test content";
        ctx.create_file(src_path)?;
        ctx.write_file(src_path, content)?;

        // Initial state: src exists, dst does not
        if !src_full.exists() || dst_full.exists() {
            return Ok(VerificationResult::failure(
                "move_reversible",
                locations,
                "Precondition failed".into(),
            ));
        }

        // Apply: move src -> dst
        ctx.move_path(src_path, dst_path)?;

        // State after move: src does not exist, dst exists
        if src_full.exists() || !dst_full.exists() {
            return Ok(VerificationResult::failure(
                "move_reversible",
                locations,
                "Move failed".into(),
            ));
        }

        // Apply inverse: move dst -> src
        ctx.move_path(dst_path, src_path)?;

        // Verify: fs = original fs
        if !src_full.exists() || dst_full.exists() {
            return Ok(VerificationResult::failure(
                "move_reversible",
                locations,
                "Move inverse failed to restore original state".into(),
            ));
        }

        // Verify content preserved
        let final_content = ctx.read_file(src_path)?;
        if final_content != content {
            return Ok(VerificationResult::failure(
                "move_reversible",
                locations,
                "Content not preserved through move/reverse".into(),
            ));
        }

        Ok(VerificationResult::success("move_reversible", locations))
    }

    /// Verify: operations on different paths don't interfere
    pub fn verify_operation_independence(&self) -> FfiResult<VerificationResult> {
        self.cleanup()?;
        let mut ctx = self.fresh_context()?;

        let locations = vec![
            "proofs/coq/filesystem_model.v",
            "proofs/lean4/FilesystemModel.lean",
            "proofs/agda/FilesystemModel.agda",
        ];

        // Create two separate files
        let path1 = "independent1.txt";
        let path2 = "independent2.txt";
        let content1 = b"content 1";
        let content2 = b"content 2";

        ctx.create_file(path1)?;
        ctx.write_file(path1, content1)?;

        ctx.create_file(path2)?;
        ctx.write_file(path2, content2)?;

        // Modify path1
        ctx.write_file(path1, b"modified content 1")?;

        // Verify path2 unchanged (independence)
        let path2_content = ctx.read_file(path2)?;
        if path2_content != content2 {
            return Ok(VerificationResult::failure(
                "operation_independence",
                locations,
                "Operation on path1 affected path2".into(),
            ));
        }

        Ok(VerificationResult::success("operation_independence", locations))
    }
}

impl Drop for VerificationSuite {
    fn drop(&mut self) {
        // Clean up sandbox on drop
        let _ = std::fs::remove_dir_all(&self.sandbox);
    }
}

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

    #[test]
    fn test_verification_suite() {
        let suite = VerificationSuite::new().unwrap();
        let results = suite.run_all().unwrap();

        for result in &results {
            if !result.passed {
                panic!("Verification failed: {} - {:?}", result.theorem, result.error);
            }
            println!("✓ {} verified against {} systems",
                result.theorem,
                result.proof_locations.len()
            );
        }

        assert!(results.iter().all(|r| r.passed));
    }
}