forjar 1.4.2

//! FJ-1401: Convergence proof from arbitrary state.
//!
//! Analyzes config + state to prove that `forjar apply` will converge:
//! 1. All resources have check/apply/state_query scripts (codegen completeness)
//! 2. Check scripts are deterministic (same state → same output)
//! 3. Apply is idempotent (converged state + apply = no change)
//! 4. No circular dependencies in the resource DAG

use crate::core::{codegen, parser, state, types};
use std::path::Path;

/// Prove convergence for a forjar config.
pub(crate) fn cmd_prove(
    file: &Path,
    state_dir: &Path,
    machine_filter: Option<&str>,
    json: bool,
) -> Result<(), String> {
    let config = parser::parse_and_validate(file)?;
    let proofs = collect_proofs(&config, state_dir, machine_filter);

    let all_passed = proofs.iter().all(|p| p.passed);

    if json {
        print_proofs_json(&config, &proofs)?;
    } else {
        print_proofs_text(&config, &proofs);
    }

    if all_passed {
        Ok(())
    } else {
        Err("convergence proof failed: see above".to_string())
    }
}

struct ProofResult {
    name: String,
    passed: bool,
    detail: String,
}

fn collect_proofs(
    config: &types::ForjarConfig,
    state_dir: &Path,
    machine_filter: Option<&str>,
) -> Vec<ProofResult> {
    let proofs = vec![
        prove_codegen_completeness(config, machine_filter),
        prove_dag_acyclicity(config),
        prove_state_coverage(config, state_dir, machine_filter),
        prove_hash_determinism(config, machine_filter),
        prove_idempotency_structure(config, machine_filter),
    ];
    proofs
}

/// Check if a resource's machine matches the filter.
fn machine_matches(resource: &types::Resource, filter: &str) -> bool {
    resource.machine.iter().any(|m| m == filter)
}

fn prove_codegen_completeness(
    config: &types::ForjarConfig,
    machine_filter: Option<&str>,
) -> ProofResult {
    let mut failures = Vec::new();

    for (id, resource) in &config.resources {
        if let Some(filter) = machine_filter {
            if !machine_matches(resource, filter) {
                continue;
            }
        }
        if resource.resource_type == types::ResourceType::Recipe {
            continue;
        }

        if let Err(e) = codegen::check_script(resource) {
            failures.push(format!("{id}: check_script: {e}"));
        }
        if let Err(e) = codegen::apply_script(resource) {
            failures.push(format!("{id}: apply_script: {e}"));
        }
        if let Err(e) = codegen::state_query_script(resource) {
            failures.push(format!("{id}: state_query: {e}"));
        }
    }

    ProofResult {
        name: "codegen-completeness".to_string(),
        passed: failures.is_empty(),
        detail: if failures.is_empty() {
            "all resources produce check/apply/state_query scripts".to_string()
        } else {
            format!("{} failures: {}", failures.len(), failures.join("; "))
        },
    }
}

fn prove_dag_acyclicity(config: &types::ForjarConfig) -> ProofResult {
    let (visited, total) = topo_sort_count(config);
    ProofResult {
        name: "dag-acyclicity".to_string(),
        passed: visited == total,
        detail: if visited == total {
            format!("DAG is acyclic ({total} resources)")
        } else {
            format!("cycle detected: only {visited}/{total} resources reachable")
        },
    }
}

/// Run Kahn's topological sort, return (visited_count, total_count).
fn topo_sort_count(config: &types::ForjarConfig) -> (usize, usize) {
    let mut in_degree: std::collections::HashMap<&str, usize> = config
        .resources
        .keys()
        .map(|k| (k.as_str(), 0usize))
        .collect();

    for (id, resource) in &config.resources {
        for dep in &resource.depends_on {
            if config.resources.contains_key(dep.as_str()) {
                *in_degree.entry(id.as_str()).or_insert(0) += 1;
            }
        }
    }

    let mut queue: Vec<&str> = in_degree
        .iter()
        .filter(|(_, &deg)| deg == 0)
        .map(|(&id, _)| id)
        .collect();
    let mut visited = 0;

    while let Some(node) = queue.pop() {
        visited += 1;
        for (id, resource) in &config.resources {
            if !resource.depends_on.iter().any(|d| d == node) {
                continue;
            }
            if let Some(deg) = in_degree.get_mut(id.as_str()) {
                *deg -= 1;
                if *deg == 0 {
                    queue.push(id.as_str());
                }
            }
        }
    }

    (visited, config.resources.len())
}

fn prove_state_coverage(
    config: &types::ForjarConfig,
    state_dir: &Path,
    machine_filter: Option<&str>,
) -> ProofResult {
    let mut total = 0;
    let mut covered = 0;

    for (id, resource) in &config.resources {
        if let Some(filter) = machine_filter {
            if !machine_matches(resource, filter) {
                continue;
            }
        }
        if resource.resource_type == types::ResourceType::Recipe {
            continue;
        }

        total += 1;

        for machine in resource.machine.iter() {
            if let Ok(Some(lock)) = state::load_lock(state_dir, machine) {
                if lock.resources.contains_key(id) {
                    covered += 1;
                    break;
                }
            }
        }
    }

    let pct = if total > 0 {
        (covered * 100) / total
    } else {
        100
    };

    ProofResult {
        name: "state-coverage".to_string(),
        passed: true, // Informational, not a hard failure
        detail: format!("{covered}/{total} resources have state entries ({pct}%)"),
    }
}

fn prove_hash_determinism(
    config: &types::ForjarConfig,
    machine_filter: Option<&str>,
) -> ProofResult {
    let mut tested = 0;
    let mut failures = Vec::new();

    for (id, resource) in &config.resources {
        if let Some(filter) = machine_filter {
            if !machine_matches(resource, filter) {
                continue;
            }
        }
        if resource.resource_type == types::ResourceType::Recipe {
            continue;
        }

        if let (Ok(s1), Ok(s2)) = (
            codegen::state_query_script(resource),
            codegen::state_query_script(resource),
        ) {
            tested += 1;
            if s1 != s2 {
                failures.push(id.to_string());
            }
        }
    }

    ProofResult {
        name: "hash-determinism".to_string(),
        passed: failures.is_empty(),
        detail: if failures.is_empty() {
            format!("{tested} resources: state_query scripts are deterministic")
        } else {
            format!(
                "{} non-deterministic: {}",
                failures.len(),
                failures.join(", ")
            )
        },
    }
}

fn prove_idempotency_structure(
    config: &types::ForjarConfig,
    machine_filter: Option<&str>,
) -> ProofResult {
    let mut tested = 0;
    let mut pipefail_count = 0;

    for (_id, resource) in &config.resources {
        if let Some(filter) = machine_filter {
            if !machine_matches(resource, filter) {
                continue;
            }
        }
        if resource.resource_type == types::ResourceType::Recipe {
            continue;
        }

        if let Ok(script) = codegen::apply_script(resource) {
            tested += 1;
            if script.contains("set -euo pipefail") {
                pipefail_count += 1;
            }
        }
    }

    let pct = if tested > 0 {
        (pipefail_count * 100) / tested
    } else {
        100
    };

    ProofResult {
        name: "idempotency-structure".to_string(),
        passed: pct >= 80,
        detail: format!("{pipefail_count}/{tested} apply scripts use set -euo pipefail ({pct}%)"),
    }
}

fn print_proofs_json(config: &types::ForjarConfig, proofs: &[ProofResult]) -> Result<(), String> {
    let results: Vec<serde_json::Value> = proofs
        .iter()
        .map(|p| {
            serde_json::json!({
                "proof": p.name,
                "passed": p.passed,
                "detail": p.detail,
            })
        })
        .collect();

    let all_passed = proofs.iter().all(|p| p.passed);
    let doc = serde_json::json!({
        "config": config.name,
        "convergenceProven": all_passed,
        "proofs": results,
    });

    let output = serde_json::to_string_pretty(&doc).map_err(|e| format!("JSON error: {e}"))?;
    println!("{output}");
    Ok(())
}

fn print_proofs_text(config: &types::ForjarConfig, proofs: &[ProofResult]) {
    println!("Convergence Proof: {}", config.name);
    println!("{:-<72}", "");
    for p in proofs {
        let status = if p.passed { "PASS" } else { "FAIL" };
        println!("[{status}] {}: {}", p.name, p.detail);
    }
    println!("{:-<72}", "");
    let passed = proofs.iter().filter(|p| p.passed).count();
    let total = proofs.len();
    println!("{passed}/{total} proofs passed");
}