// SPDX-License-Identifier: MPL-2.0

//! Proof certificate checking
//!
//! Supports verification of proof certificates in multiple formats:
//! - Alethe (from CVC5)
//! - DRAT/LRAT (from SAT solvers)
//! - Lean4 kernel re-checking (lean4checker)
//! - Coq kernel re-checking (coqchk)
//!
//! Certificates provide independent verification of solver results,
//! enabling audit trails and elevating trust levels.

use anyhow::{Context, Result};
use serde::{Deserialize, Serialize};
use std::path::PathBuf;

/// Supported proof certificate formats
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
pub enum CertificateFormat {
    /// Alethe format from CVC5
    Alethe,
    /// DRAT format from SAT solvers
    DRAT,
    /// LRAT format (linear time verification, preferred)
    LRAT,
    /// Lean4 kernel export for lean4checker
    Lean4Kernel,
    /// Coq kernel export for coqchk
    CoqKernel,
    /// TSTP proof format from first-order ATPs (Vampire, E)
    TSTP,
}

/// A proof certificate produced by a solver
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ProofCertificate {
    /// Certificate format
    pub format: CertificateFormat,
    /// Raw certificate content
    pub content: String,
    /// BLAKE3 hash of the certificate content
    pub blake3_hash: String,
    /// Source solver that produced the certificate
    pub source_solver: String,
    /// Whether the certificate has been independently verified
    pub verified: bool,
    /// Path where the certificate is stored (if persisted)
    pub storage_path: Option<PathBuf>,
}

/// Result of certificate verification
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct CertificateVerificationResult {
    /// Whether the certificate is valid
    pub valid: bool,
    /// Verification tool used
    pub checker: String,
    /// Time taken to verify (milliseconds)
    pub time_ms: u64,
    /// Error message if verification failed
    pub error: Option<String>,
    /// Number of proof steps checked
    pub steps_checked: Option<u64>,
}

/// Certificate verifier that checks proof certificates independently
pub struct CertificateVerifier {
    /// Path to drat-trim binary
    drat_trim_path: PathBuf,
    /// Path to lean4checker binary
    #[allow(dead_code)]
    lean4checker_path: PathBuf,
    /// Path to coqchk binary
    #[allow(dead_code)]
    coqchk_path: PathBuf,
    /// Storage directory for certificates
    storage_dir: PathBuf,
}

impl CertificateVerifier {
    /// Create a new certificate verifier
    pub fn new(storage_dir: PathBuf) -> Self {
        Self {
            drat_trim_path: PathBuf::from("drat-trim"),
            lean4checker_path: PathBuf::from("lean4checker"),
            coqchk_path: PathBuf::from("coqchk"),
            storage_dir,
        }
    }

    /// Verify an Alethe certificate (CVC5 proof format)
    pub fn verify_alethe(
        &self,
        certificate: &ProofCertificate,
    ) -> Result<CertificateVerificationResult> {
        let start = std::time::Instant::now();

        // Parse Alethe proof steps
        let steps = self.parse_alethe_steps(&certificate.content)?;
        let mut valid = true;

        // Check each proof step
        for step in &steps {
            if !self.check_alethe_step(step) {
                valid = false;
                break;
            }
        }

        let elapsed = start.elapsed();

        Ok(CertificateVerificationResult {
            valid,
            checker: "echidna-alethe-checker".to_string(),
            time_ms: elapsed.as_millis() as u64,
            error: if valid {
                None
            } else {
                Some("Invalid proof step found".to_string())
            },
            steps_checked: Some(steps.len() as u64),
        })
    }

    /// Verify a DRAT/LRAT certificate
    pub fn verify_drat(
        &self,
        certificate: &ProofCertificate,
        cnf_formula: &str,
    ) -> Result<CertificateVerificationResult> {
        let start = std::time::Instant::now();

        // Write CNF and certificate to temp files
        let tmp_dir = std::env::temp_dir();
        let cnf_path = tmp_dir.join("echidna_cnf.dimacs");
        let cert_path = tmp_dir.join("echidna_cert.drat");

        std::fs::write(&cnf_path, cnf_formula)?;
        std::fs::write(&cert_path, &certificate.content)?;

        // Run drat-trim
        let output = std::process::Command::new(&self.drat_trim_path)
            .arg(&cnf_path)
            .arg(&cert_path)
            .output();

        // Clean up temp files
        let _ = std::fs::remove_file(&cnf_path);
        let _ = std::fs::remove_file(&cert_path);

        let elapsed = start.elapsed();

        match output {
            Ok(out) => {
                let stdout = String::from_utf8_lossy(&out.stdout);
                let valid = stdout.contains("VERIFIED") || stdout.contains("s VERIFIED");

                Ok(CertificateVerificationResult {
                    valid,
                    checker: "drat-trim".to_string(),
                    time_ms: elapsed.as_millis() as u64,
                    error: if valid {
                        None
                    } else {
                        Some(stdout.to_string())
                    },
                    steps_checked: None,
                })
            },
            Err(e) => Ok(CertificateVerificationResult {
                valid: false,
                checker: "drat-trim".to_string(),
                time_ms: elapsed.as_millis() as u64,
                error: Some(format!("Failed to run drat-trim: {}", e)),
                steps_checked: None,
            }),
        }
    }

    /// Store a certificate for audit trail
    pub fn store_certificate(
        &self,
        certificate: &mut ProofCertificate,
        proof_id: &str,
    ) -> Result<PathBuf> {
        std::fs::create_dir_all(&self.storage_dir)?;

        let filename = format!("{}_{}.cert", proof_id, certificate.format_extension());
        let path = self.storage_dir.join(&filename);

        std::fs::write(&path, &certificate.content)
            .with_context(|| format!("Failed to store certificate at {}", path.display()))?;

        certificate.storage_path = Some(path.clone());
        Ok(path)
    }

    /// Parse Alethe proof steps (simplified)
    fn parse_alethe_steps(&self, content: &str) -> Result<Vec<AletheStep>> {
        let mut steps = Vec::new();

        for line in content.lines() {
            let line = line.trim();
            if line.is_empty() || line.starts_with(';') {
                continue;
            }

            // Parse step: (step id clause :rule rule_name :premises (p1 p2 ...))
            if line.starts_with("(step") || line.starts_with("(assume") {
                steps.push(AletheStep {
                    raw: line.to_string(),
                    kind: if line.starts_with("(assume") {
                        AletheStepKind::Assume
                    } else {
                        AletheStepKind::Step
                    },
                });
            }
        }

        Ok(steps)
    }

    /// Check a single Alethe proof step (simplified)
    fn check_alethe_step(&self, step: &AletheStep) -> bool {
        // In a full implementation, this would verify the logical
        // correctness of each proof step against the Alethe calculus.
        // For now, we do structural validation.
        match step.kind {
            AletheStepKind::Assume => !step.raw.is_empty(),
            AletheStepKind::Step => step.raw.contains(":rule") && step.raw.starts_with("(step"),
        }
    }
}

impl ProofCertificate {
    /// Create a new proof certificate
    pub fn new(format: CertificateFormat, content: String, source_solver: &str) -> Self {
        let blake3_hash = blake3::hash(content.as_bytes()).to_hex().to_string();

        Self {
            format,
            content,
            blake3_hash,
            source_solver: source_solver.to_string(),
            verified: false,
            storage_path: None,
        }
    }

    /// Get file extension for this certificate format
    pub fn format_extension(&self) -> &str {
        match self.format {
            CertificateFormat::Alethe => "alethe",
            CertificateFormat::DRAT => "drat",
            CertificateFormat::LRAT => "lrat",
            CertificateFormat::Lean4Kernel => "lean4cert",
            CertificateFormat::CoqKernel => "coqcert",
            CertificateFormat::TSTP => "tstp",
        }
    }
}

/// An Alethe proof step
#[derive(Debug)]
struct AletheStep {
    raw: String,
    kind: AletheStepKind,
}

/// Kind of Alethe proof step
#[derive(Debug)]
enum AletheStepKind {
    Assume,
    Step,
}

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

    #[test]
    fn test_certificate_creation() {
        let cert = ProofCertificate::new(
            CertificateFormat::Alethe,
            "(assume a1 (= x y))\n(step s1 (cl (= y x)) :rule eq_symmetric :premises (a1))"
                .to_string(),
            "cvc5",
        );

        assert_eq!(cert.format, CertificateFormat::Alethe);
        assert!(!cert.blake3_hash.is_empty());
        assert!(!cert.verified);
        assert_eq!(cert.source_solver, "cvc5");
    }

    #[test]
    fn test_alethe_verification_valid() {
        let verifier = CertificateVerifier::new(std::env::temp_dir().join("echidna_certs_test"));

        let cert = ProofCertificate::new(
            CertificateFormat::Alethe,
            "(assume a1 (= x y))\n(step s1 (cl (= y x)) :rule eq_symmetric :premises (a1))"
                .to_string(),
            "cvc5",
        );

        let result = verifier.verify_alethe(&cert).unwrap();
        assert!(result.valid);
        assert_eq!(result.steps_checked, Some(2));
    }

    #[test]
    fn test_invalid_certificate_rejected() {
        let verifier = CertificateVerifier::new(std::env::temp_dir().join("echidna_certs_test"));

        // Step without :rule is invalid
        let cert = ProofCertificate::new(
            CertificateFormat::Alethe,
            "(step s1 (cl (= y x)))".to_string(),
            "cvc5",
        );

        let result = verifier.verify_alethe(&cert).unwrap();
        assert!(!result.valid);
    }

    #[test]
    fn test_certificate_hash_consistency() {
        let cert1 =
            ProofCertificate::new(CertificateFormat::DRAT, "1 2 3 0\n".to_string(), "minisat");
        let cert2 =
            ProofCertificate::new(CertificateFormat::DRAT, "1 2 3 0\n".to_string(), "minisat");

        assert_eq!(cert1.blake3_hash, cert2.blake3_hash);
    }

    #[test]
    fn test_format_extension() {
        assert_eq!(
            ProofCertificate::new(CertificateFormat::Alethe, String::new(), "test")
                .format_extension(),
            "alethe"
        );
        assert_eq!(
            ProofCertificate::new(CertificateFormat::LRAT, String::new(), "test")
                .format_extension(),
            "lrat"
        );
    }

    #[test]
    fn test_format_extension_drat() {
        assert_eq!(
            ProofCertificate::new(CertificateFormat::DRAT, String::new(), "test")
                .format_extension(),
            "drat"
        );
    }

    #[test]
    fn test_format_extension_tstp() {
        assert_eq!(
            ProofCertificate::new(CertificateFormat::TSTP, String::new(), "test")
                .format_extension(),
            "tstp"
        );
    }

    #[test]
    fn test_certificate_hash_different_content() {
        let cert1 =
            ProofCertificate::new(CertificateFormat::DRAT, "1 2 3 0\n".to_string(), "minisat");
        let cert2 =
            ProofCertificate::new(CertificateFormat::DRAT, "4 5 6 0\n".to_string(), "minisat");

        assert_ne!(cert1.blake3_hash, cert2.blake3_hash);
    }

    #[test]
    fn test_certificate_not_verified_by_default() {
        let cert = ProofCertificate::new(
            CertificateFormat::Alethe,
            "test content".to_string(),
            "cvc5",
        );
        assert!(!cert.verified);
        assert!(cert.storage_path.is_none());
    }

    #[test]
    fn test_certificate_format_serialization() {
        let json = serde_json::to_string(&CertificateFormat::Alethe).unwrap();
        assert!(json.contains("Alethe"));

        let deserialized: CertificateFormat = serde_json::from_str(&json).unwrap();
        assert_eq!(deserialized, CertificateFormat::Alethe);
    }

    #[test]
    fn test_verification_result_serialization() {
        let result = CertificateVerificationResult {
            valid: true,
            checker: "drat-trim".to_string(),
            time_ms: 100,
            error: None,
            steps_checked: Some(42),
        };

        let json = serde_json::to_string(&result).unwrap();
        let deserialized: CertificateVerificationResult = serde_json::from_str(&json).unwrap();
        assert!(deserialized.valid);
        assert_eq!(deserialized.steps_checked, Some(42));
    }
}