//! flowRS's proof table (`codegen::proof_table`, `data/program-proofs.json`) is the proof
//! corpus as the generator writes it today: every program, by its two digests, refused where
//! the generator refuses, run by the pinned Kani. A generator change that alters any program's
//! `mod flow` (or its harness, or what a board refuses) fails here until the build host proves
//! the corpus again (`KANI_PROGRAMS_WRITE=1 tools/kani-programs.sh`), so no stale "proved" can
//! stand in the table; and an export's record names the program it is about.

use flowrs_core::codegen::board::{FirmwareOptions, Harness, corpus, family_of, generate};
use flowrs_core::codegen::mcu::{McuTarget, refusal_message};
use flowrs_core::codegen::proof::{self, KANI_PIN, ProgramMeta, Record, program_proof};
use flowrs_core::codegen::proof_table::{self, Entry};
use std::collections::BTreeMap;

const AGAIN: &str = "the proof table is stale: on the build host, run \
     `KANI_PROGRAMS_WRITE=1 tools/kani-programs.sh` and commit crates/flowrs-core/data/program-proofs.json";

/// (graph, board, target).
type Key = (String, String, String);
/// (id, flow SHA-256, harness SHA-256).
type Generated = (String, String, String);

/// Every program of the proof corpus, as `examples/program_proofs.rs` generates it for
/// `tools/kani-programs.sh`: (graph, board, target) -> Ok((id, flow, harness)) or the refusal.
fn generated() -> BTreeMap<Key, Result<Generated, String>> {
    let reg = flowrs_boards::BoardRegistry::with_builtins();
    let mut out = BTreeMap::new();
    for board in reg.boards() {
        let Ok((family, table)) = family_of(board) else {
            continue;
        };
        for target in McuTarget::ALL {
            for (name, graph) in corpus::proof_graphs() {
                let key = (name.to_string(), board.id.clone(), target.id().to_string());
                let fw = generate(
                    &graph,
                    target,
                    board,
                    &FirmwareOptions {
                        harness: Harness::Standalone,
                        link: None,
                        twin: false,
                    },
                );
                let v = match fw {
                    Err(r) => Err(refusal_message(target, &r)),
                    Ok(fw) => {
                        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()),
                            },
                        );
                        // What the export ships names the same program and harness.
                        assert_eq!(p.flow_sha256, fw.proof.flow_sha256, "{key:?}");
                        assert_eq!(p.harness_sha256, fw.proof.harness_sha256, "{key:?}");
                        Ok((
                            p.id,
                            p.flow_sha256,
                            p.harness_sha256.expect("a corpus program has a harness"),
                        ))
                    }
                };
                out.insert(key, v);
            }
        }
    }
    out
}

#[test]
#[ignore = "compares flowRS's proof scripts, which are not in this snapshot"]
fn the_table_reads_and_was_run_by_the_pinned_kani() {
    let t = proof_table::table().expect("data/program-proofs.json is a proof table");
    assert_eq!(t.schema, proof_table::SCHEMA);
    assert!(proof_table::pinned(t), "{:?}: {AGAIN}", t.kani);
    assert_eq!(t.run.by, "tools/kani-programs.sh");
    assert!(!t.run.at.is_empty() && !t.run.host.is_empty());
    // tools/kani-env.sh pins the same Kani the code holds a result to.
    let env = std::fs::read_to_string(
        std::path::Path::new(env!("CARGO_MANIFEST_DIR")).join("../../tools/kani-env.sh"),
    )
    .unwrap();
    assert!(
        env.lines().any(|l| l == format!("KANI_PIN={KANI_PIN}")),
        "tools/kani-env.sh does not pin Kani {KANI_PIN}"
    );
}

#[test]
fn the_table_is_the_proof_corpus_the_generator_writes_today() {
    let t = proof_table::table().expect("a proof table");
    let table: BTreeMap<(String, String, String), &Entry> = t
        .programs
        .iter()
        .map(|e| ((e.graph.clone(), e.board.clone(), e.target.clone()), e))
        .collect();
    assert_eq!(table.len(), t.programs.len(), "a program listed twice");
    let now = generated();
    let mut wrong = Vec::new();
    for (key, want) in &now {
        let Some(e) = table.get(key) else {
            wrong.push(format!("{key:?}: not in the table"));
            continue;
        };
        match want {
            Err(why) => {
                if e.status != "refused" || e.reason.as_deref() != Some(why.as_str()) {
                    wrong.push(format!(
                        "{key:?}: refused ({why}), the table says {} {:?}",
                        e.status, e.reason
                    ));
                }
            }
            Ok((id, flow, harness)) => {
                if e.status == "refused" {
                    wrong.push(format!("{key:?}: generated now, refused in the table"));
                } else if e.id.as_deref() != Some(id.as_str())
                    || e.flow_sha256.as_deref() != Some(flow.as_str())
                    || e.harness_sha256.as_deref() != Some(harness.as_str())
                {
                    wrong.push(format!(
                        "{key:?}: now {id} (flow {}, harness {}), the table proved {:?} (flow \
                         {:?}, harness {:?})",
                        &flow[..12],
                        &harness[..12],
                        e.id,
                        e.flow_sha256,
                        e.harness_sha256
                    ));
                }
            }
        }
    }
    for key in table.keys() {
        if !now.contains_key(key) {
            wrong.push(format!("{key:?}: in the table, no longer generated"));
        }
    }
    assert!(wrong.is_empty(), "{AGAIN}:\n  {}", wrong.join("\n  "));
    // The corpus has programs on every covered board, and the SparkFun Thing Plus's UART
    // programs are generated (its UART is in flowrs-boards, from SparkFun's schematic).
    for board in [
        "nucleo_f401re",
        "nucleo_g071rb",
        "rpi_pico",
        "feather_rp2040",
        "sparkfun_thing_plus_rp2040",
    ] {
        for g in [
            "uart.read",
            "uart.write (echo)",
            "spi.transfer",
            "i2c.write",
            "mcuio (all but PWM)",
        ] {
            for target in McuTarget::ALL {
                let k = (g.to_string(), board.to_string(), target.id().to_string());
                assert!(matches!(now.get(&k), Some(Ok(_))), "{k:?} is refused");
            }
        }
    }
}

#[test]
fn every_program_with_a_harness_has_a_result_and_a_proved_one_has_both_covers() {
    let t = proof_table::table().expect("a proof table");
    for e in &t.programs {
        let n = format!("{} on {} ({})", e.graph, e.board, e.target);
        if e.status == "refused" {
            assert!(e.reason.is_some() && e.flow_sha256.is_none(), "{n}");
            continue;
        }
        assert!(
            ["proved", "failed", "not_proved", "budget_exceeded"].contains(&e.status.as_str()),
            "{n}: {}",
            e.status
        );
        if e.status == "proved" {
            let c = e.checks.expect("a proved program's checks");
            let v = e.covers.expect("a proved program's covers");
            assert!(c.failed == 0 && c.undetermined == 0, "{n}: {c:?}");
            assert!(v.total >= 2 && v.satisfied == v.total, "{n}: {v:?}");
            assert!(e.reason.is_none(), "{n}");
        }
    }
}

/// An export ships the table's result for its program, and only for its program: the record a
/// firmware's `proof/proofs.json` carries is the manifest with the result filled in, and a
/// manifest of another program (or another harness) is never filled.
#[test]
fn a_program_the_table_proved_ships_its_result_and_no_other_program_inherits_it() {
    let reg = flowrs_boards::BoardRegistry::with_builtins();
    let (_, graph) = corpus::proof_graphs()
        .into_iter()
        .find(|(n, _)| *n == "uart.write (echo)")
        .unwrap();
    let opts = FirmwareOptions {
        harness: Harness::Standalone,
        link: None,
        twin: false,
    };
    let fw = generate(&graph, McuTarget::Rtic, reg.get("rpi_pico").unwrap(), &opts).unwrap();
    let shipped = Record::parse(&fw.proof.proofs_json()).unwrap();
    let h = &shipped.harnesses[0];
    assert_eq!(h.status, "proved", "{h:?}");
    assert_eq!(shipped.program.flow_sha256, fw.proof.flow_sha256);
    assert_eq!(h.harness_sha256, fw.proof.harness_sha256);
    assert_eq!(
        shipped.kani.as_ref().unwrap().version.as_deref(),
        Some(KANI_PIN)
    );
    let run = shipped.run.as_ref().unwrap();
    assert_eq!(run["by"], "tools/kani-programs.sh");
    assert_eq!(run["table"], proof_table::PATH);
    assert_eq!(run["as"], "uart.write (echo)");
    // The files the export writes carry exactly that record.
    let files = fw.proof.files();
    assert_eq!(
        files.iter().map(|f| f.0.as_str()).collect::<Vec<_>>(),
        ["proof/Cargo.toml", "proof/src/lib.rs", "proof/proofs.json"]
    );
    assert_eq!(files[2].1, fw.proof.proofs_json());
    assert_eq!(
        proof::sha256_hex(&files[1].1),
        h.harness_sha256.clone().unwrap()
    );

    // The same graph with one more node is another program: nothing is filled in.
    let mut other = graph.clone();
    let n = other.add_node("embedded.gpio.digital_out", 0.0, 0.0);
    other
        .get_node_mut(n)
        .unwrap()
        .properties
        .insert("pin".into(), "21".into());
    let fw2 = generate(&other, McuTarget::Rtic, reg.get("rpi_pico").unwrap(), &opts).unwrap();
    assert_ne!(fw2.proof.flow_sha256, fw.proof.flow_sha256);
    let r2 = Record::parse(&fw2.proof.proofs_json()).unwrap();
    assert_eq!(r2.harnesses[0].status, "not_run");
    assert!(r2.kani.is_none() && r2.run.is_none());
    // A table entry is never filled into a manifest whose digests are not its own.
    let (entry, table) = proof_table::lookup(
        &fw.proof.flow_sha256,
        fw.proof.harness_sha256.as_deref().unwrap(),
    )
    .unwrap();
    assert!(proof_table::fill(&fw2.proof.manifest, entry, table).is_none());
    // Nor is one found by the flow alone: a harness that differs (here, one cover dropped)
    // has another digest.
    let edited = fw
        .proof
        .lib_rs
        .replace("kani::cover!(r.is_err()", "let _ = (r.is_err()");
    assert!(proof_table::lookup(&fw.proof.flow_sha256, &proof::sha256_hex(&edited)).is_none());
}

#[test]
fn flow_of_finds_the_module_the_firmware_carries() {
    let reg = flowrs_boards::BoardRegistry::with_builtins();
    for (name, graph) in corpus::proof_graphs() {
        for target in McuTarget::ALL {
            let Ok(fw) = generate(
                &graph,
                target,
                reg.get("nucleo_f401re").unwrap(),
                &FirmwareOptions {
                    harness: Harness::Standalone,
                    link: None,
                    twin: false,
                },
            ) else {
                continue;
            };
            let flow = proof::flow_text(&fw.lowered.source);
            assert_eq!(proof::flow_of(&fw.main_rs), Some(flow.as_str()), "{name}");
            assert_eq!(
                proof::flow_of(&fw.proof.lib_rs),
                Some(flow.as_str()),
                "{name}"
            );
            assert_eq!(proof::sha256_hex(&flow), fw.proof.flow_sha256, "{name}");
        }
    }
    assert_eq!(proof::flow_of("no module here"), None);
    assert_eq!(proof::flow_of("mod flow {\n    fn a() {}\n"), None);
    assert_eq!(
        proof::flow_of("// x\nmod flow {\n    fn a() {}\n}\nmod b {\n}\n"),
        Some("    fn a() {}\n")
    );
}

/// The e2e suite's document of the corpus's `digital_in+not` (`e2e/fixtures/firmware/
/// in_not_out.flowrs`, which `e2e/proofcarry.spec.js` opens in the editor) is that program, as
/// the table proved it, on every board and executor: the Code view shows it proved.
#[test]
fn the_e2e_document_of_a_corpus_graph_is_a_program_the_table_proved() {
    let text = include_str!("../../../e2e/fixtures/firmware/in_not_out.flowrs");
    let graph = flowrs_core::graph::document::load(text).unwrap();
    let reg = flowrs_boards::BoardRegistry::with_builtins();
    for board in ["nucleo_f401re", "rpi_pico"] {
        for target in McuTarget::ALL {
            let fw = generate(
                &graph,
                target,
                reg.get(board).unwrap(),
                &FirmwareOptions {
                    harness: Harness::Standalone,
                    link: None,
                    twin: false,
                },
            )
            .unwrap();
            let r = Record::parse(&fw.proof.proofs_json()).unwrap();
            assert_eq!(r.harnesses[0].status, "proved", "{board} {}", target.id());
            assert_eq!(r.run.unwrap()["as"], "digital_in+not");
        }
    }
}

/// The e2e suite's document of the frame DSP firmware (`e2e/fixtures/firmware/mcu_dsp.flowrs`,
/// which `e2e/mcu-dsp.spec.js` opens) is the exported fixture `mcu_dsp.fdsl`'s program, as the
/// table proved it, on the STM32F4 and the STM32G0 boards and the Pico, both executors.
#[test]
fn the_e2e_document_of_the_frame_dsp_firmware_is_a_program_the_table_proved() {
    let text = include_str!("../../../e2e/fixtures/firmware/mcu_dsp.flowrs");
    let graph = flowrs_core::graph::document::load(text).unwrap();
    let reg = flowrs_boards::BoardRegistry::with_builtins();
    for board in ["nucleo_f401re", "nucleo_g071rb", "rpi_pico"] {
        for target in McuTarget::ALL {
            let fw = generate(
                &graph,
                target,
                reg.get(board).unwrap(),
                &FirmwareOptions {
                    harness: Harness::Standalone,
                    link: None,
                    twin: false,
                },
            )
            .unwrap_or_else(|r| panic!("{board} {}: {r:?}", target.id()));
            let r = Record::parse(&fw.proof.proofs_json()).unwrap();
            assert_eq!(r.harnesses[0].status, "proved", "{board} {}", target.id());
            assert_eq!(r.run.unwrap()["as"], "e2e: mcu_dsp.fdsl");
        }
    }
}

/// An edit of a table's entry `usize`.
type Edit = fn(&mut proof_table::Table, usize);

/// A run's table is held to the committed one in what a result is (the gate's
/// `tools/kani-programs.sh`): a status, a check count, a cover, a digest, a program more or
/// fewer, or another Kani is a difference; time and peak memory are the run's own.
#[test]
fn a_run_that_departs_from_the_table_is_told_apart() {
    let t = proof_table::table().unwrap().clone();
    assert!(proof_table::compare(&t, &t, false).is_empty());
    let first_proved = t
        .programs
        .iter()
        .position(|e| e.status == "proved")
        .unwrap();
    let edits: [(&str, Edit); 9] = [
        ("status", |t, i| {
            t.programs[i].status = "budget_exceeded".into()
        }),
        ("checks", |t, i| {
            t.programs[i].checks.as_mut().unwrap().passed -= 1;
        }),
        ("covers", |t, i| {
            t.programs[i].covers.as_mut().unwrap().satisfied -= 1;
        }),
        ("flow_sha256", |t, i| {
            t.programs[i].flow_sha256 = Some("0".repeat(64));
        }),
        ("harness_sha256", |t, i| {
            t.programs[i].harness_sha256 = Some("0".repeat(64));
        }),
        ("reason", |t, i| t.programs[i].reason = Some("x".into())),
        ("unwind", |t, i| t.programs[i].unwind = Some(1)),
        ("Kani", |t, _| t.kani.version = Some("0.67.0".into())),
        ("not in the table", |t, i| {
            let mut e = t.programs[i].clone();
            e.graph.push_str(" (again)");
            t.programs.push(e);
        }),
    ];
    for (what, edit) in edits {
        let mut run = t.clone();
        edit(&mut run, first_proved);
        let why = proof_table::compare(&t, &run, false);
        assert!(why.iter().any(|w| w.contains(what)), "{what}: {why:?}");
    }
    // A program missing from a whole run is a difference; from a run of some graphs it is not.
    let mut part = t.clone();
    part.programs.remove(first_proved);
    assert!(!proof_table::compare(&t, &part, false).is_empty());
    assert!(proof_table::compare(&t, &part, true).is_empty());
    // Time and peak memory are the run's own.
    let mut slower = t.clone();
    slower.programs[first_proved].time_s = Some(1e6);
    slower.programs[first_proved].peak_mem_gb = Some(99.0);
    slower.run.wall_s = Some(1e6);
    assert!(proof_table::compare(&t, &slower, false).is_empty());
}

/// The corpus and an export are proved with the same arguments: tools/kani-programs.sh's
/// `ARGS` (the corpus and the canary) is `codegen::proof::KANI_ARGS`, which `flowrsc prove`
/// passes too, and the script runs the canary before the corpus.
#[test]
#[ignore = "compares flowRS's proof scripts, which are not in this snapshot"]
fn the_corpus_the_canary_and_flowrsc_prove_run_kani_with_the_same_arguments() {
    let script = std::fs::read_to_string(
        std::path::Path::new(env!("CARGO_MANIFEST_DIR")).join("../../tools/kani-programs.sh"),
    )
    .unwrap();
    let args = script
        .lines()
        .find(|l| l.starts_with("ARGS=("))
        .expect("tools/kani-programs.sh sets ARGS");
    assert_eq!(args, format!("ARGS=({})", proof::KANI_ARGS.join(" ")));
    let canary = script
        .find("cargo kani \"${ARGS[@]}\")")
        .expect("the canary runs with ARGS");
    let corpus = script
        .find("cargo kani --workspace \"${ARGS[@]}\")")
        .expect("the corpus runs with ARGS");
    assert!(canary < corpus, "the canary runs first");
    assert!(proof::KANI_ARGS.contains(&"--no-overflow-checks"));
    assert!(proof::KANI_ARGS.contains(&"restrict-vtable"));
}