//! The exhaustive differential check described in `PROOF.md`.
//!
//! This is separate from `tests/differential.rs` because it is a different
//! kind of claim. That runner asks whether a handful of hand-written cases
//! agree; this one enumerates *entire input domains* — every two-byte input
//! to the decoder, every two-byte input to the encoder, every single byte
//! through `encode_str` and `HexDisplay` — and compares the complete output
//! of both programs byte for byte.
//!
//! The driver in `proof/main.rs` references base16ct's own module files in
//! place, so this cannot drift from what `tests/cases/026-base16ct-crate/`
//! transpiles.

use std::fs;
use std::io::Write as _;
use std::path::{Path, PathBuf};
use std::process::{Command, Stdio};

const RUSTNIM: &str = env!("CARGO_BIN_EXE_rustnim");

fn find_nim() -> PathBuf {
    if let Ok(p) = std::env::var("RUSTNIM_NIM") {
        return PathBuf::from(p);
    }
    let mut dir: Option<&Path> = Some(Path::new(env!("CARGO_MANIFEST_DIR")));
    while let Some(d) = dir {
        let c = d.join(".nim-toolchain/bin/nim");
        if c.is_file() {
            return c;
        }
        dir = d.parent();
    }
    panic!("no .nim-toolchain/bin/nim found; set RUSTNIM_NIM");
}

fn sh(cmd: &mut Command, what: &str) -> Vec<u8> {
    let out = cmd
        .stdout(Stdio::piped())
        .stderr(Stdio::piped())
        .output()
        .unwrap_or_else(|e| panic!("{what}: spawn: {e}"));
    if !out.status.success() {
        let mut msg = String::from_utf8_lossy(&out.stderr).into_owned();
        if msg.trim().is_empty() {
            msg = String::from_utf8_lossy(&out.stdout).into_owned();
        }
        panic!("{what} failed ({:?}):\n{}", out.status.code(), tail(&msg));
    }
    out.stdout
}

fn tail(s: &str) -> String {
    let v: Vec<&str> = s.trim_end().lines().collect();
    v[v.len().saturating_sub(25)..].join("\n")
}

/// Report the first differing line, and how many lines differ in total.
fn first_difference(a: &[u8], b: &[u8]) -> String {
    let (sa, sb) = (String::from_utf8_lossy(a), String::from_utf8_lossy(b));
    let (la, lb): (Vec<_>, Vec<_>) = (sa.lines().collect(), sb.lines().collect());
    let mut first = None;
    let mut count = 0usize;
    for i in 0..la.len().max(lb.len()) {
        if la.get(i) != lb.get(i) {
            count += 1;
            if first.is_none() {
                first = Some(i);
            }
        }
    }
    match first {
        None => format!("{} vs {} bytes, but every line matches", a.len(), b.len()),
        Some(i) => format!(
            "{count} line(s) differ; first at line {}:\n  rustc: {:?}\n  nim  : {:?}",
            i + 1,
            la.get(i),
            lb.get(i)
        ),
    }
}

#[test]
fn base16ct_is_byte_identical_over_the_enumerated_domains() {
    let root = Path::new(env!("CARGO_MANIFEST_DIR"));
    let work = root.join("tests/.work/proof");
    let _ = fs::remove_dir_all(&work);
    fs::create_dir_all(&work).unwrap();

    let driver = root.join("proof/main.rs");
    let crate_dir = root.join("tests/cases/026-base16ct-crate");
    let mut modules: Vec<PathBuf> = fs::read_dir(&crate_dir)
        .unwrap()
        .filter_map(|e| e.ok().map(|e| e.path()))
        .filter(|p| {
            p.extension().is_some_and(|x| x == "rs")
                && p.file_name().is_some_and(|f| f != "main.rs")
        })
        .collect();
    modules.sort();
    assert!(
        modules.len() == 5,
        "expected base16ct's five module files, found {:?}",
        modules
    );

    // -- rustc: the oracle.
    let rs_bin = work.join("rs");
    sh(
        Command::new("rustc")
            .arg("--edition=2021")
            .arg("--cfg")
            .arg("feature=\"alloc\"")
            .arg("-A")
            .arg("warnings")
            .arg(&driver)
            .arg("-o")
            .arg(&rs_bin)
            .env("TMPDIR", &work),
        "rustc",
    );
    let expected = sh(&mut Command::new(&rs_bin).env("TMPDIR", &work), "the Rust binary");

    // -- rustnim, then Nim.
    let nim_src = work.join("proof.nim");
    let mut t = Command::new(RUSTNIM);
    t.arg(&driver);
    for m in &modules {
        t.arg(m);
    }
    t.arg("--cfg")
        .arg("feature=alloc")
        .arg("-o")
        .arg(&nim_src)
        .env("TMPDIR", &work);
    sh(&mut t, "rustnim");

    let meta = fs::metadata(&nim_src).expect("rustnim wrote no output file");
    assert!(meta.len() > 0, "rustnim wrote an empty output file");

    let nim_bin = work.join("nim");
    sh(
        Command::new(find_nim())
            .arg("c")
            .arg("--hints:off")
            .arg("--warnings:off")
            .arg("--colors:off")
            .arg(format!("--nimcache:{}", work.join("cache").display()))
            .arg(format!("-o:{}", nim_bin.display()))
            .arg(&nim_src)
            .env("TMPDIR", &work),
        "nim c",
    );
    let actual = sh(&mut Command::new(&nim_bin).env("TMPDIR", &work), "the Nim binary");

    // The output must be substantial: an empty or truncated run agreeing with
    // an empty or truncated run would otherwise read as success, which is the
    // exact failure this project exists to avoid.
    let lines = expected.iter().filter(|b| **b == b'\n').count();
    assert!(
        lines > 150_000 && expected.ends_with(b"done\n"),
        "the oracle did not run to completion: {lines} lines, {} bytes",
        expected.len()
    );

    assert!(
        expected == actual,
        "outputs differ.\n{}",
        first_difference(&expected, &actual)
    );

    let _ = writeln!(
        std::io::stderr(),
        "proof: {} cases, {} bytes of output, byte-identical",
        lines,
        expected.len()
    );
}