//! Writes the proof corpus as Kani harness crates, one per generated program: every graph of
//! `codegen::board::corpus::proof_graphs` (the board generator's corpus, the start screen's
//! microcontroller examples and the e2e firmware fixture) for every board the generator
//! covers, on both executors, each as the firmware flashed to the board would carry it. The crates form
//! one cargo workspace, so `cargo kani --workspace` compiles their shared dependencies once.
//! `tools/kani-programs.sh` runs it, then the proofs, then writes each `proofs.json`.
//!
//! ```text
//! cargo run -p flowrs-core --example program_proofs -- <out dir> <flowRS checkout> [graph...]
//! cargo run -p flowrs-core --example program_proofs -- --compare <committed> <run's> [--subset]
//! ```
//!
//! With graph names, only those corpus graphs are written; FLOWRS_PROOF_BOARDS (board ids,
//! comma-separated) keeps only those boards. It writes `<out>/Cargo.toml` (the
//! workspace), `<out>/<crate>/{Cargo.toml,src/lib.rs,proofs.json}` and `<out>/programs.json`
//! (one entry per program: its id, crate, graph, board, chip, family, target, harness,
//! unwinding bound, and the SHA-256 of its flow module and of its harness). A board that
//! refuses a graph is listed there with the refusal and no crate. `tools/kani_programs.py`
//! makes flowRS's proof table from it (`codegen::proof_table`).

use std::path::{Path, PathBuf};

use flowrs_core::codegen::board::{FirmwareOptions, Harness, corpus, family_of, generate};
use flowrs_core::codegen::mcu::{McuTarget, refusal_message};
use flowrs_core::codegen::proof::{ProgramMeta, flow_text, program_proof};
use serde_json::json;

fn fail(msg: &str) -> ! {
    eprintln!("program_proofs: {msg}");
    std::process::exit(1);
}

fn write(path: &Path, text: &str) {
    if let Some(dir) = path.parent()
        && let Err(e) = std::fs::create_dir_all(dir)
    {
        fail(&format!("{}: {e}", dir.display()));
    }
    if let Err(e) = std::fs::write(path, text) {
        fail(&format!("{}: {e}", path.display()));
    }
}

/// `--compare COMMITTED NEW [--subset]`: hold a run's proof table to the committed one
/// (`codegen::proof_table::compare`); exit 1 on any difference.
fn compare(args: &[String]) -> ! {
    use flowrs_core::codegen::proof_table;
    let read = |p: &str| {
        let text = std::fs::read_to_string(p).unwrap_or_else(|e| fail(&format!("{p}: {e}")));
        proof_table::parse(&text).unwrap_or_else(|e| fail(&format!("{p}: {e}")))
    };
    let (Some(old), Some(new)) = (args.first(), args.get(1)) else {
        fail("usage: program_proofs --compare <committed table> <run's table> [--subset]");
    };
    let (old, new) = (read(old), read(new));
    let why = proof_table::compare(&old, &new, args.iter().any(|a| a == "--subset"));
    for w in &why {
        eprintln!("kani-programs: {w}");
    }
    if why.is_empty() {
        println!(
            "kani-programs: this run agrees with the proof table ({} programs)",
            new.programs.len()
        );
        std::process::exit(0);
    }
    eprintln!(
        "kani-programs: this run differs from the proof table in {} way(s); a whole-corpus run \
         with KANI_PROGRAMS_WRITE=1 rewrites it ({}), for review",
        why.len(),
        proof_table::PATH
    );
    std::process::exit(1);
}

fn main() {
    let args: Vec<String> = std::env::args().skip(1).collect();
    if args.first().map(String::as_str) == Some("--compare") {
        compare(&args[1..]);
    }
    if args.len() < 2 {
        fail("usage: program_proofs <out dir> <flowRS checkout> [graph...]");
    }
    let out = PathBuf::from(&args[0]);
    let hal = Path::new(&args[1])
        .join("crates/flowrs-hal")
        .canonicalize()
        .unwrap_or_else(|e| fail(&format!("the flowrs-hal source under {}: {e}", args[1])));
    let only: Vec<&str> = args[2..].iter().map(String::as_str).collect();

    let reg = flowrs_boards::BoardRegistry::with_builtins();
    let wanted: Vec<String> = std::env::var("FLOWRS_PROOF_BOARDS")
        .map(|v| v.split(',').map(|b| b.trim().to_string()).collect())
        .unwrap_or_default();
    let mut boards: Vec<_> = reg
        .boards()
        .iter()
        .filter(|b| family_of(b).is_ok())
        .filter(|b| wanted.is_empty() || wanted.contains(&b.id))
        .collect();
    boards.sort_by(|a, b| a.id.cmp(&b.id));

    let mut members = Vec::new();
    let mut programs = Vec::new();
    for board in boards {
        let Ok((family, table)) = family_of(board) else {
            continue;
        };
        for target in McuTarget::ALL {
            for (name, graph) in corpus::proof_graphs() {
                if !only.is_empty() && !only.contains(&name) {
                    continue;
                }
                let fw = match generate(
                    &graph,
                    target,
                    board,
                    &FirmwareOptions {
                        harness: Harness::Standalone,
                        link: None,
                        twin: false,
                    },
                ) {
                    Ok(fw) => fw,
                    Err(r) => {
                        programs.push(json!({
                            "graph": name,
                            "board": board.id,
                            "target": target.id(),
                            "refused": refusal_message(target, &r),
                        }));
                        continue;
                    }
                };
                // The program the harness proves is the one the firmware carries.
                let flow = flow_text(&fw.lowered.source);
                if !fw.main_rs.contains(&format!("mod flow {{\n{flow}}}\n")) {
                    fail(&format!(
                        "{name} on {} ({}): the firmware's mod flow is not the app's text",
                        board.id,
                        target.id()
                    ));
                }
                let p = program_proof(
                    &fw.lowered,
                    target,
                    &ProgramMeta {
                        board: board.id.clone(),
                        chip: table.regdb.to_string(),
                        family: family.name().to_string(),
                        graph: Some(name.to_string()),
                    },
                );
                if p.flow_sha256 != fw.proof.flow_sha256
                    || p.id != fw.proof.id
                    || p.harness_sha256 != fw.proof.harness_sha256
                {
                    fail(&format!(
                        "{name}: the firmware's proof names another program or harness"
                    ));
                }
                let dir = out.join(&p.crate_name);
                if p.harness.is_some() {
                    let manifest = p.cargo_toml.replace(
                        "\"<your flowRS checkout>/crates/flowrs-hal\"",
                        &format!("{:?}", hal.display().to_string()),
                    );
                    write(&dir.join("Cargo.toml"), &manifest);
                    write(&dir.join("src/lib.rs"), &p.lib_rs);
                    members.push(p.crate_name.clone());
                }
                write(&dir.join("proofs.json"), &p.manifest);
                programs.push(json!({
                    "id": p.id,
                    "crate": p.crate_name,
                    "dir": p.crate_name,
                    "graph": name,
                    "board": board.id,
                    "chip": table.regdb,
                    "family": family.name(),
                    "target": target.id(),
                    "harness": p.harness,
                    "unwind": p.unwind,
                    "flow_sha256": p.flow_sha256,
                    "harness_sha256": p.harness_sha256,
                    "not_provable": p.not_provable,
                }));
            }
        }
    }
    let list = members
        .iter()
        .map(|m| format!("    \"{m}\","))
        .collect::<Vec<_>>()
        .join("\n");
    write(
        &out.join("Cargo.toml"),
        &format!(
            "# The proof corpus as Kani harness crates (flowrs-core's\n\
             # examples/program_proofs.rs); tools/kani-programs.sh proves them.\n\
             [workspace]\nresolver = \"3\"\nmembers = [\n{list}\n]\n"
        ),
    );
    let text = serde_json::to_string_pretty(&programs)
        .unwrap_or_else(|e| fail(&format!("programs.json: {e}")));
    write(&out.join("programs.json"), &(text + "\n"));
    println!(
        "program_proofs: {} programs ({} with a harness) in {}",
        programs.len(),
        members.len(),
        out.display()
    );
}