//! `flowrsc prove` on real exports, with a stand-in `cargo` that plays Kani: it answers
//! `cargo kani --version` and `cargo fetch --locked`, and for `cargo kani` writes Kani's JSON
//! export for the harness it is asked for, as told (proved, a cover not reached, a check
//! failed), then holds on, sleeps or allocates as told. So the runner's whole path is run here
//! (the record, the budget, the contract) without Kani; the real Kani runs it on the build host
//! (`flowrsc prove` on an export, and `tools/kani-programs.sh` on the corpus).
#![cfg(unix)]

use std::os::unix::fs::PermissionsExt;
use std::path::{Path, PathBuf};

use flowrs_appshell::export::{self, FirmwareOptions};
use flowrs_appshell::form::{self, Status};
use flowrs_cli::prove::{self, Options, Stopped, judge, verdict};
use flowrs_connect::ScaffoldFile;
use flowrs_core::codegen::mcu::McuTarget;
use flowrs_core::codegen::proof::{KANI_INSTALL, KANI_PIN, Record};

const FAKE: &str = r#"#!/bin/bash
# A stand-in for cargo that plays Kani; its instructions are files beside it.
D="$(cd "$(dirname "$0")" && pwd)"
if [ "$1 ${2:-}" = "kani --version" ]; then
  [ -f "$D/no-kani" ] && { echo "error: no such command: kani" >&2; exit 101; }
  echo "Kani Rust Verifier $(cat "$D/version" 2>/dev/null || echo 0.68.0) (cargo plugin)"
  exit 0
fi
if [ "$1 ${2:-}" = "fetch --locked" ]; then exit 0; fi
[ "$1" = kani ] || exit 1
echo "$@" > "$D/invoked"
pwd > "$D/cwd"
h=""; j=""; prev=""
for a in "$@"; do
  [ "$prev" = "--harness" ] && h="$a"
  [ "$prev" = "--export-json" ] && j="$a"
  prev="$a"
done
result=$(cat "$D/result" 2>/dev/null || echo proved)
first=Success; second=Satisfied; status=Success
[ "$result" = failed ] && { first=Failure; status=Failure; }
[ "$result" = uncovered ] && second=Unsatisfiable
cat > "$j" <<EOF
{"tools": {"kani": "0.68.0", "cbmc": "6.11.0 (stand-in)", "rustc": "rustc (stand-in)"},
 "error_details": [{"harness_id": "$h", "has_errors": false}],
 "verification_results": {"summary": {}, "results": [{"harness_id": "$h", "status": "$status", "duration_ms": 1234,
  "checks": [
   {"status": "$first", "description": "attempt to add with overflow", "category": "arithmetic_overflow"},
   {"status": "Success", "description": "index out of bounds: the length is less than or equal to the given index", "category": "assertion"},
   {"status": "Unreachable", "description": "unreachable code", "category": "unreachable"},
   {"status": "Satisfied", "description": "a pass runs to its end", "category": "cover"},
   {"status": "$second", "description": "a pass fails, into the safe state", "category": "cover"}
  ]}]}}
EOF
[ -f "$D/sleep" ] && sleep "$(cat "$D/sleep")"
[ -f "$D/alloc" ] && perl -e '$x = "a" x (300 * 1024 * 1024); sleep 30'
exit 0
"#;

/// A firmware graph flowRS's proof table does not hold (the e2e fixture with one more output),
/// so its export ships its harness not run.
fn not_in_the_table() -> String {
    let root = Path::new(env!("CARGO_MANIFEST_DIR")).join("../..");
    let mcu_io = std::fs::read_to_string(root.join("e2e/fixtures/firmware/mcu_io.fdsl")).unwrap();
    format!("{mcu_io}let n9 = embedded.gpio.digital_out {{ pin: 12 }};\n")
}

struct Bench {
    _tmp: tempfile::TempDir,
    dir: PathBuf,
    fake: PathBuf,
}

impl Bench {
    fn new(target: McuTarget) -> Bench {
        let tmp = tempfile::tempdir().unwrap();
        let dir = tmp.path().join("export");
        let done = export::firmware_document(
            &not_in_the_table(),
            Some("other.fdsl"),
            &FirmwareOptions {
                name: None,
                board: "nucleo_f401re".into(),
                target,
            },
            None,
        )
        .unwrap();
        export::write(&done.scaffold, &dir).unwrap();
        let fake_dir = tmp.path().join("fake");
        std::fs::create_dir_all(&fake_dir).unwrap();
        let fake = fake_dir.join("cargo");
        std::fs::write(&fake, FAKE).unwrap();
        std::fs::set_permissions(&fake, std::fs::Permissions::from_mode(0o755)).unwrap();
        Bench {
            _tmp: tmp,
            dir,
            fake,
        }
    }

    fn tell(&self, file: &str, what: &str) {
        std::fs::write(self.fake.parent().unwrap().join(file), what).unwrap();
    }

    fn invoked(&self) -> bool {
        self.fake.parent().unwrap().join("invoked").exists()
    }

    fn opts(&self) -> Options {
        let mut o = Options::new(
            &self.dir,
            prove::DEFAULT_MEM_GB,
            prove::DEFAULT_TIMEOUT_S,
            None,
        );
        o.cargo.clone_from(&self.fake);
        o
    }

    fn run(&self, o: &Options) -> (i32, String, String) {
        let (mut out, mut err) = (Vec::new(), Vec::new());
        let code = prove::prove(o, &mut out, &mut err);
        (
            code,
            String::from_utf8(out).unwrap(),
            String::from_utf8(err).unwrap(),
        )
    }

    fn read(&self, rel: &str) -> String {
        std::fs::read_to_string(self.dir.join(rel)).unwrap()
    }

    fn record(&self) -> Record {
        Record::parse(&self.read("proof/proofs.json")).unwrap()
    }

    /// The export's files row 13 is computed from, as they are now.
    fn files(&self) -> Vec<ScaffoldFile> {
        [
            form::FILE,
            "src/main.rs",
            form::PROOF_RECORD,
            form::PROOF_HARNESS,
        ]
        .into_iter()
        .map(|p| ScaffoldFile {
            path: p.into(),
            contents: self.read(p),
        })
        .collect()
    }

    fn row(&self) -> form::Property {
        form::validate_export(&self.files())
            .unwrap_or_else(|e| panic!("{e:?}"))
            .property("no_panic_proof")
            .unwrap()
            .clone()
    }
}

#[test]
fn an_export_of_another_program_ships_its_harness_not_run() {
    let b = Bench::new(McuTarget::Rtic);
    let r = b.record();
    assert_eq!(r.harnesses[0].status, "not_run");
    assert!(r.kani.is_none() && r.run.is_none());
    let row = b.row();
    assert_eq!(row.status, Status::NotYet);
    assert!(row.reason.contains("flowrsc prove"), "{}", row.reason);
    // The README says how to prove it, with the runner's own budget and the pinned Kani.
    let readme = b.read("README.md");
    assert!(readme.contains("## Prove it"), "{readme}");
    assert!(readme.contains("flowrsc prove ."));
    assert!(readme.contains(KANI_INSTALL));
    assert!(readme.contains(&format!(
        "{} GB and {} s by default",
        prove::DEFAULT_MEM_GB,
        prove::DEFAULT_TIMEOUT_S
    )));
    for a in &r.assumptions {
        assert!(readme.contains(&a[..20]), "{a}");
    }
    // The harness is a member of the project's workspace, on the vendored flowrs-hal, which
    // carries the modules a build under Kani compiles (its own proofs), or it would not build.
    assert!(b.read("Cargo.toml").contains("members = [\"proof\"]"));
    assert!(
        b.read("proof/Cargo.toml")
            .contains("path = \"../vendor/flowrs-hal\"")
    );
    for f in [
        "vendor/flowrs-hal/src/rt/proofs.rs",
        "vendor/flowrs-hal/src/can/proofs.rs",
    ] {
        assert!(b.dir.join(f).exists(), "no {f}");
    }
}

#[test]
fn a_run_that_proves_this_program_makes_its_row_live() {
    for target in McuTarget::ALL {
        let b = Bench::new(target);
        let readme_before = b.read("README.md");
        let (code, out, err) = b.run(&b.opts());
        assert_eq!(code, 0, "{out}\n{err}");
        let r = b.record();
        let h = &r.harnesses[0];
        assert_eq!(h.status, "proved");
        assert_eq!(h.covers.unwrap().satisfied, 2);
        assert_eq!(h.checks.unwrap().unreachable, 1);
        assert_eq!(r.kani.as_ref().unwrap().version.as_deref(), Some(KANI_PIN));
        let run = r.run.as_ref().unwrap();
        assert_eq!(run["by"], "flowrsc prove");
        assert_eq!(h.budget.unwrap().mem_gb, Some(prove::DEFAULT_MEM_GB));
        // Kani ran in proof/, on exactly the harness the record names, within its limit.
        let invoked = std::fs::read_to_string(b.fake.parent().unwrap().join("invoked")).unwrap();
        assert!(invoked.contains(&format!("--harness {} --exact", h.name.as_deref().unwrap())));
        assert!(invoked.contains("-Z restrict-vtable"), "{invoked}");
        // The corpus's arguments, every one: codegen::proof::KANI_ARGS.
        assert!(
            invoked.contains(&flowrs_core::codegen::proof::KANI_ARGS.join(" ")),
            "{invoked}"
        );
        assert!(invoked.contains("--no-overflow-checks"), "{invoked}");
        // Kani runs in proof/: the JSON's path it is handed is absolute, so it lands where
        // prove reads it whatever directory prove was given.
        assert!(invoked.contains("--export-json /"), "{invoked}");
        assert!(invoked.contains(&format!("--harness-timeout {}s", prove::DEFAULT_TIMEOUT_S)));
        let cwd = std::fs::read_to_string(b.fake.parent().unwrap().join("cwd")).unwrap();
        assert!(cwd.trim_end().ends_with("export/proof"), "{cwd}");
        // Row 13 is live, the contract holds to the files, the README's section follows it.
        let row = b.row();
        assert_eq!(row.status, Status::Live, "{}", row.reason);
        assert!(
            row.reason.contains("Run by flowrsc prove"),
            "{}",
            row.reason
        );
        let c = form::validate(&b.read(form::FILE)).unwrap();
        let readme = b.read("README.md");
        assert_ne!(readme, readme_before);
        assert!(readme.contains(&form::readme_section(&c)));
        // It says what it proved and what it assumes.
        assert!(out.contains("result: proved"), "{out}");
        for a in &r.assumptions {
            assert!(out.contains(a.as_str()), "{a}");
        }
        assert!(out.contains("FORM.json row 13 (no panic): live"), "{out}");
    }
}

#[test]
fn a_run_past_its_wall_clock_is_never_proved() {
    let b = Bench::new(McuTarget::Rtic);
    // Kani wrote "proved", then the run went on past its wall clock.
    b.tell("sleep", "30");
    let mut o = b.opts();
    o.wall_s = 2;
    let start = std::time::Instant::now();
    let (code, out, err) = b.run(&o);
    assert!(start.elapsed().as_secs() < 20, "the run was not stopped");
    assert_eq!(code, 1, "{out}\n{err}");
    let h = &b.record().harnesses[0];
    assert_eq!(h.status, "budget_exceeded");
    assert!(h.reason.as_deref().unwrap().contains("wall clock"), "{h:?}");
    let row = b.row();
    assert_eq!(row.status, Status::NotYet);
    assert!(row.reason.contains("budget"), "{}", row.reason);
}

#[test]
fn a_run_past_its_memory_is_never_proved() {
    let b = Bench::new(McuTarget::Embassy);
    b.tell("alloc", "");
    let mut o = b.opts();
    o.total_kib = 50 * 1024;
    let (code, out, err) = b.run(&o);
    assert_eq!(code, 1, "{out}\n{err}");
    let h = &b.record().harnesses[0];
    assert_eq!(h.status, "budget_exceeded", "{h:?}");
    assert!(h.reason.as_deref().unwrap().starts_with("memory"), "{h:?}");
    assert_eq!(b.row().status, Status::NotYet);
}

#[test]
fn an_unreached_cover_or_a_counterexample_is_not_a_proof() {
    for (result, status, why) in [
        ("uncovered", "not_proved", "vacuous"),
        ("failed", "failed", "attempt to add with overflow"),
    ] {
        let b = Bench::new(McuTarget::Rtic);
        b.tell("result", result);
        let (code, out, err) = b.run(&b.opts());
        assert_eq!(code, 1, "{out}\n{err}");
        let h = &b.record().harnesses[0];
        assert_eq!(h.status, status);
        assert!(h.reason.as_deref().unwrap().contains(why), "{h:?}");
        assert_eq!(b.row().status, Status::NotYet, "{result}");
    }
}

#[test]
fn without_the_pinned_kani_it_says_how_to_install_it_and_runs_nothing() {
    for (tell, says) in [("no-kani", "not installed"), ("version", "Kani 0.67.0")] {
        let b = Bench::new(McuTarget::Rtic);
        b.tell(tell, "0.67.0");
        let before = b.read("proof/proofs.json");
        let (code, _, err) = b.run(&b.opts());
        assert_eq!(code, 2, "{err}");
        assert!(err.contains(says), "{err}");
        assert!(err.contains(KANI_INSTALL), "{err}");
        assert!(!b.invoked());
        assert_eq!(b.read("proof/proofs.json"), before);
    }
}

#[test]
fn a_harness_that_is_not_the_records_is_refused_before_anything_runs() {
    let b = Bench::new(McuTarget::Rtic);
    let lib = b
        .read("proof/src/lib.rs")
        .replace("kani::cover!(r.is_err()", "let _ = (r.is_err()");
    std::fs::write(b.dir.join("proof/src/lib.rs"), lib).unwrap();
    let (code, _, err) = b.run(&b.opts());
    assert_eq!(code, 1, "{err}");
    assert!(err.contains("not the harness the record names"), "{err}");
    assert!(!b.invoked());
}

/// A program that speaks a typed link: its loops are bounded by elapsed time, so no harness can
/// prove it; `prove` says why and runs nothing, and its row says the same.
#[test]
fn a_program_no_harness_can_prove_says_why_and_is_never_run() {
    use flowrs_core::codegen::link::{LinkChannel, LinkEnd, LinkPlan, WireTy};
    use flowrs_core::codegen::mcu::{Options as Lower, lower_with};
    use flowrs_core::codegen::proof::{ProgramMeta, program_proof};
    let b = Bench::new(McuTarget::Rtic);
    let mut g = flowrs_core::graph::ir::Graph::new();
    let adc = g.add_node("embedded.adc", 0.0, 0.0);
    let plan = LinkPlan {
        uart: 0,
        baud: 1_000_000,
        timeout_ms: 10_000,
        cdc: false,
        order: None,
        channels: vec![LinkChannel {
            id: 1,
            name: "raw".into(),
            ty: WireTy::U16,
            end: LinkEnd::Send {
                node: adc,
                port: "raw".into(),
            },
            iface: None,
            fragments: 1,
            stamped: false,
        }],
    };
    let l = lower_with(
        &g,
        McuTarget::Rtic,
        &Lower {
            probes: false,
            board: None,
            link: Some(&plan),
        },
    )
    .unwrap();
    let p = program_proof(
        &l,
        McuTarget::Rtic,
        &ProgramMeta {
            board: "nucleo_f401re".into(),
            chip: "stm32f401re".into(),
            family: "STM32F4".into(),
            graph: None,
        },
    );
    assert!(p.harness.is_none());
    std::fs::write(b.dir.join("proof/proofs.json"), &p.manifest).unwrap();
    // The export's contract, recomputed for that record, as an exporter of it would write it.
    let mut c = form::validate(&b.read(form::FILE)).unwrap();
    form::reassess_no_panic(&mut c, &b.files());
    std::fs::write(b.dir.join(form::FILE), c.to_json()).unwrap();
    let row = b.row();
    assert_eq!(row.status, Status::NotYet);
    assert!(
        row.reason.contains("no harness can prove"),
        "{}",
        row.reason
    );
    let (code, out, err) = b.run(&b.opts());
    assert_eq!(code, 1, "{out}\n{err}");
    assert!(out.contains("cannot be proved"), "{out}");
    assert!(out.contains("clock"), "{out}");
    assert!(!out.contains("result: proved"));
    assert!(!b.invoked());
}

#[test]
fn the_watcher_stops_a_solver_or_a_run_past_its_cap() {
    // pid ppid rss(KiB) command
    let ps = "\
1 0 100 /sbin/launchd
500 1 1000 /bin/bash ./cargo kani
501 500 2000 /usr/bin/kani-driver
502 501 9000000 /opt/kani/bin/cbmc --json-ui x.out
503 501 300 /opt/kani/bin/goto-instrument y.out
900 1 99999999 /usr/bin/cbmc somebody-elses.out
";
    // The solver past its 8 GB cap (9,000,000 KiB is 8.6 GB): stopped, as the solver's.
    let (total, solver, stop) = judge(ps, 500, 8 * 1024 * 1024, 12 * 1024 * 1024);
    assert_eq!(solver, 9_000_000);
    assert_eq!(total, 1000 + 2000 + 9_000_000 + 300);
    assert!(
        matches!(stop, Some(Stopped::Solver { kib: 9_000_000, .. })),
        "{stop:?}"
    );
    // Under its cap but the run as a whole past its own.
    let (_, _, stop) = judge(ps, 500, 10 * 1024 * 1024, 8 * 1024 * 1024);
    assert!(matches!(stop, Some(Stopped::Run { .. })), "{stop:?}");
    // Within both: nothing stopped. Another run's solver (pid 900) is not this run's.
    let (_, _, stop) = judge(ps, 500, 10 * 1024 * 1024, 12 * 1024 * 1024);
    assert_eq!(stop, None);
}

#[test]
fn a_stopped_run_is_budget_exceeded_whatever_kani_wrote() {
    let proved = serde_json::json!({
        "verification_results": {"results": [{
            "harness_id": "proof::p", "status": "Success", "duration_ms": 10,
            "checks": [
                {"status": "Success", "description": "x", "category": "assertion"},
                {"status": "Satisfied", "description": "a", "category": "cover"},
                {"status": "Satisfied", "description": "b", "category": "cover"}
            ]
        }]}
    });
    assert_eq!(
        verdict(Some(&proved), "proof::p", None, 600).status,
        "proved"
    );
    for s in [
        Stopped::Solver {
            kib: 9 << 20,
            cap_kib: 8 << 20,
        },
        Stopped::Run {
            kib: 13 << 20,
            cap_kib: 12 << 20,
        },
        Stopped::Wall { secs: 1500 },
    ] {
        let v = verdict(Some(&proved), "proof::p", Some(s), 600);
        assert_eq!(v.status, "budget_exceeded", "{s:?}");
    }
    // Kani's own time limit, and no result at all.
    let timeout = serde_json::json!({
        "error_details": [{"harness_id": "proof::p", "exit_status": "timeout"}],
        "verification_results": {"results": [{"harness_id": "proof::p", "status": "Failure", "checks": []}]}
    });
    let v = verdict(Some(&timeout), "proof::p", None, 600);
    assert_eq!(v.status, "budget_exceeded");
    assert!(v.reason.unwrap().contains("600 s"));
    assert_eq!(verdict(None, "proof::p", None, 600).status, "not_proved");
    assert_eq!(
        verdict(Some(&proved), "proof::q", None, 600).status,
        "not_proved"
    );
    // An unwinding assertion is a loop past its bound, not a proof.
    let unwound = serde_json::json!({
        "verification_results": {"results": [{
            "harness_id": "proof::p", "status": "Failure",
            "checks": [
                {"status": "Failure", "description": "unwinding assertion loop 0", "category": "unwind"},
                {"status": "Satisfied", "description": "a", "category": "cover"}
            ]
        }]}
    });
    let v = verdict(Some(&unwound), "proof::p", None, 600);
    assert_eq!(v.status, "not_proved");
    assert!(v.reason.unwrap().contains("unwinding"));
}