//! The resident `z3`'s decisions read off its own process tree, on a real
//! `z3`. Each test starts a [`Z3Server`] of its own and decides real SMT-LIB
//! goals on it.
//!
//! The oracle shares no code with the meter or the server: the resident
//! `z3`'s `proc_pid_rusage(pid, RUSAGE_INFO_V6)` read into a raw buffer and
//! taken at the SDK's byte offset (energy at 336), read before and after each
//! attempt once `z3` is quiet on the oracle's own terms: no thread on a core
//! or queued (`proc_pidinfo(PROC_PIDTASKINFO)` into a raw buffer,
//! `pti_numrunning` at byte 88) and none in a wait no signal ends (each
//! thread's `pth_run_state`, read raw as well) at two reads 20 ms apart
//! whose energy agrees.
//! A resident `z3` blocked on its next read does not move its count, so
//! between the meter's reads and the oracle's nothing is spent: a decision's
//! reading must EQUAL the oracle's advance across the attempt, to the
//! nanojoule, and the attempt's `HwShunt` figure must be that advance rounded
//! UP to a whole µJ.
//!
//! Every server here but one is declared self-contained
//! ([`Z3Server::declared_self_contained`]): the Homebrew `z3` these tests run
//! is the solver itself, deciding in its own process. The one undeclared
//! server shows that a whole reading is never sealed without it.
//!
//! Without `z3` on `PATH` there is nothing to decide, and each test says so
//! and returns; CI's proof-rs legs install `z3`. The tests log what they saw
//! (`z3 tree meter:`), and run one at a time (a lock) so one test's solver is
//! not loading the host under another's.

#![cfg(all(target_os = "macos", target_arch = "aarch64"))]

use proof_schema::{Energy, GoalKind, ProofGoal, Provenance, Solver, Verdict};
use proof_solvers::{z3_available, Modelled, Z3Server};
use sandbox_meter::{process_energy_status, CounterStatus};
use std::sync::{Mutex, MutexGuard};
use std::time::{Duration, Instant};

static ONE_AT_A_TIME: Mutex<()> = Mutex::new(());

fn alone() -> MutexGuard<'static, ()> {
    ONE_AT_A_TIME.lock().unwrap_or_else(|e| e.into_inner())
}

/// How long the meter may wait for `z3` to go quiet in these tests: far past
/// the production bound, because the host runs at a load of 14 to 260 and a
/// reply's tail can wait that long for a core. A `z3` still running after it
/// is a gap, which fails a test that expects a whole reading: a whole
/// reading is never a stale one.
const TEST_SETTLE: Duration = Duration::from_secs(2);

/// `pid`'s `rusage_info_v6`, raw: `proc_pid_rusage(pid, 6)` into a buffer
/// larger than the struct's 464 bytes, as 64-bit words.
fn oracle_rusage(pid: i32) -> Option<[u64; 64]> {
    let mut buf = [0u64; 64];
    // SAFETY: `buf` is writable and larger than `rusage_info_v6`.
    let rc = unsafe { libc::proc_pid_rusage(pid, 6, buf.as_mut_ptr() as *mut libc::rusage_info_t) };
    (rc == 0).then_some(buf)
}

fn energy_nj(ru: &[u64; 64]) -> u64 {
    ru[336 / 8]
}

/// `pti_numrunning` of `pid`: `proc_pidinfo(pid, PROC_PIDTASKINFO = 4)` into
/// a raw 96-byte buffer, the int32 at byte 88.
fn oracle_running(pid: i32) -> Option<i32> {
    let mut buf = [0u8; 96];
    // SAFETY: `buf` is writable for the 96 bytes passed.
    let n = unsafe { libc::proc_pidinfo(pid, 4, 0, buf.as_mut_ptr().cast(), 96) };
    (n == 96).then(|| i32::from_ne_bytes(buf[88..92].try_into().unwrap()))
}

/// Whether every thread of `pid` is at rest by its own run state: none on a
/// core or queued (`TH_STATE_RUNNING`, 1) and none in a wait that no signal
/// ends (`TH_STATE_UNINTERRUPTIBLE`, 4: waiting on the disk, the pager or a
/// kernel lock, to run again without anything arriving), the rule the meter
/// settles by. `proc_pidinfo(pid, PROC_PIDLISTTHREADS = 6)` into a raw buffer
/// of 64-bit thread handles, then `proc_pidinfo(pid, PROC_PIDTHREADINFO = 5,
/// handle)` into a raw 112-byte buffer, `pth_run_state` the int32 at byte 24.
/// `None` if the listing fails (an exited process has no task).
fn oracle_at_rest(pid: i32) -> Option<bool> {
    let mut handles = [0u64; 512];
    // SAFETY: `handles` is writable for the bytes passed.
    let n = unsafe { libc::proc_pidinfo(pid, 6, 0, handles.as_mut_ptr().cast(), (handles.len() * 8) as libc::c_int) };
    if n <= 0 {
        return None;
    }
    let n = n as usize / 8;
    assert!(n < handles.len(), "{pid} has more threads than the oracle's buffer holds");
    Some(handles[..n].iter().all(|&handle| {
        let mut buf = [0u8; 112];
        // SAFETY: `buf` is writable for the 112 bytes passed.
        let got = unsafe { libc::proc_pidinfo(pid, 5, handle, buf.as_mut_ptr().cast(), 112) };
        // A thread gone since the listing waits on nothing.
        got != 112 || !matches!(i32::from_ne_bytes(buf[24..28].try_into().unwrap()), 1 | 4)
    }))
}

/// `pid`'s energy count once it is quiet by the oracle's rule: no thread
/// running, queued or in a wait no signal ends at two reads 20 ms apart,
/// with the same energy at both. Panics
/// after 20 s.
fn quiet_energy(pid: i32) -> u64 {
    let deadline = Instant::now() + Duration::from_secs(20);
    loop {
        let first = oracle_rusage(pid).expect("oracle read");
        let before = oracle_running(pid) == Some(0) && oracle_at_rest(pid) == Some(true);
        std::thread::sleep(Duration::from_millis(20));
        let second = oracle_rusage(pid).expect("oracle read");
        let after = oracle_running(pid) == Some(0) && oracle_at_rest(pid) == Some(true);
        if before && after && energy_nj(&first) == energy_nj(&second) {
            return energy_nj(&second);
        }
        assert!(Instant::now() < deadline, "the oracle never saw z3 (pid {pid}) quiet");
    }
}

/// Valid claims, each asserted negated: `unsat`, so proved.
fn theorems() -> Vec<(&'static str, ProofGoal)> {
    let goal = |s: &str| ProofGoal::new(s, "smt2", GoalKind::Decidable);
    vec![
        ("x>0 → x≥0", goal("(declare-const x Int)\n(assert (not (=> (> x 0) (>= x 0))))")),
        ("a+b = b+a", goal("(declare-const a Int)(declare-const b Int)\n(assert (not (= (+ a b) (+ b a))))")),
        (
            "3x = x+x+x (bv32)",
            goal(
                "(declare-const x (_ BitVec 32))\n\
                 (assert (not (= (bvmul x #x00000003) (bvadd x (bvadd x x)))))",
            ),
        ),
    ]
}

/// The server for a test, or `None` (said) when there is no `z3` to decide
/// with. On a host whose per-process counter is not live there is no tree
/// meter, and an attempt keeps the estimate and says why: checked here, so
/// that branch also asserts before the test returns.
fn server(bound: Duration) -> Option<Z3Server> {
    if !z3_available() {
        eprintln!("z3 not installed: no resident z3 to meter");
        return None;
    }
    let server = Z3Server::new().with_settle_bound(bound).declared_self_contained(true);
    let status = process_energy_status();
    if status != CounterStatus::Live {
        assert!(!server.is_tree_metered(), "a tree meter without a live counter ({status:?})");
        let (_, goal) = &theorems()[0];
        let a = server.attempt(goal);
        let acct = server.last_account().expect("an account");
        eprintln!("z3 resident (counter {status:?}): {acct:?}");
        assert_eq!(a.energy, Energy::estimator(acct.modelled_uj));
        assert_eq!(acct.modelled_because, vec![Modelled::NoTreeMeter]);
        return None;
    }
    assert!(server.is_tree_metered(), "the per-process counter is live, yet no tree meter for z3");
    Some(server)
}

/// Each resident decision of a proved goal is read whole off `z3`'s tree
/// and sealed `HwShunt`: the reading equals the oracle's advance across the
/// attempt to the nanojoule, and the attempt's figure is that advance
/// rounded up to the µJ.
#[test]
fn a_resident_decision_is_hwshunt_and_equals_the_oracle() {
    let _one = alone();
    let Some(server) = server(TEST_SETTLE) else { return };
    let pid = server.pid().expect("a resident z3") as i32;
    for rep in 0..4 {
        for (name, goal) in theorems() {
            let before = quiet_energy(pid);
            let a = server.attempt(&goal);
            let after = quiet_energy(pid);
            let oracle = after - before;
            let acct = server.last_account().expect("an account of the attempt");
            let r = acct.reading.clone().expect("a span was opened").expect("a reading");
            eprintln!(
                "z3 tree meter: {name} rep {rep}: {} nJ over {:?}, oracle {oracle} nJ, sealed {:?}, work {:?}, overhead {:?}, gaps {:?}",
                r.cpu_nj, r.pids, a.energy, acct.work, acct.overhead, r.gaps
            );
            assert!(a.verdict.is_proved(), "{name}: {:?}", a.verdict);
            assert!(r.is_whole(), "{name}: the resident z3 was not read whole: {:?}", r.gaps);
            assert_eq!(r.pids, vec![pid as u32], "{name}: z3 is a single process");
            assert_eq!(r.cpu_nj, oracle, "{name}: the reading is not the oracle's advance");
            assert!(acct.modelled_because.is_empty(), "{name}: {:?}", acct.modelled_because);
            assert_eq!(a.energy, Energy::measured(oracle.div_ceil(1_000)), "{name}");
            assert_eq!(a.energy.provenance, Provenance::HwShunt);
            assert!(a.energy.check_provenance().is_ok());
        }
    }
}

/// A refuted goal: the resident `z3` decides `sat`, and a one-shot `z3`,
/// outside the resident tree, fetches the counter-model. The span read the
/// resident decision alone — exactly the oracle's advance on the resident
/// `z3`, no other process in it — and the attempt keeps the wall-time
/// estimate for the whole attempt, saying why.
#[test]
fn a_refuted_goal_keeps_the_estimate_because_its_counter_model_ran_outside_the_tree() {
    let _one = alone();
    let Some(server) = server(TEST_SETTLE) else { return };
    let pid = server.pid().expect("a resident z3") as i32;
    let not_thm = ProofGoal::new("(declare-const x Int)\n(assert (not (> x 0)))", "smt2", GoalKind::Decidable);
    for rep in 0..3 {
        let before = quiet_energy(pid);
        let a = server.attempt(&not_thm);
        let after = quiet_energy(pid);
        let oracle = after - before;
        let acct = server.last_account().expect("an account of the attempt");
        let r = acct.reading.clone().expect("a span was opened").expect("a reading");
        eprintln!(
            "z3 tree meter: refuted rep {rep}: resident {} nJ over {:?}, oracle {oracle} nJ, sealed {:?}, work {:?}, because {:?}",
            r.cpu_nj, r.pids, a.energy, acct.work, acct.modelled_because
        );
        assert!(matches!(a.verdict, Verdict::Refuted { .. }), "{:?}", a.verdict);
        assert_eq!(acct.modelled_because, vec![Modelled::CounterModelOutsideTree]);
        assert_eq!(a.energy, Energy::estimator(acct.modelled_uj));
        assert_eq!(a.energy.provenance, Provenance::Estimator);
        assert!(r.is_whole(), "{:?}", r.gaps);
        assert_eq!(r.pids, vec![pid as u32], "the one-shot z3 is not in the resident tree");
        assert_eq!(r.cpu_nj, oracle, "the span is the resident decision alone");
    }
}

/// The production settle bound, on this host as it is: what the metering
/// adds to a goal's latency, and how often a decision is read whole. Every
/// attempt is graded consistently either way — a whole reading `HwShunt` at
/// its rounded-up figure, a gapped one the estimate with its gaps — and the
/// numbers are logged for the record rather than asserted, because they
/// depend on the host's load.
#[test]
fn the_production_settle_bound_grades_every_attempt_consistently() {
    let _one = alone();
    let Some(server) = server(sandbox_meter::probe::SETTLE_BOUND) else { return };
    let mut overheads: Vec<Duration> = Vec::new();
    let mut works: Vec<Duration> = Vec::new();
    let (mut whole, mut gapped) = (0, 0);
    for _ in 0..10 {
        for (name, goal) in theorems() {
            let a = server.attempt(&goal);
            assert!(a.verdict.is_proved(), "{name}");
            let acct = server.last_account().expect("an account of the attempt");
            let r = acct.reading.clone().expect("a span was opened").expect("a reading");
            if r.is_whole() {
                whole += 1;
                assert_eq!(a.energy, Energy::measured(r.cpu_nj.div_ceil(1_000)), "{name}");
                assert!(acct.modelled_because.is_empty());
            } else {
                gapped += 1;
                assert_eq!(a.energy, Energy::estimator(acct.modelled_uj), "{name}: {:?}", r.gaps);
                assert_eq!(acct.modelled_because, vec![Modelled::Gaps(r.gaps.clone())]);
            }
            overheads.push(acct.overhead);
            works.push(acct.work);
        }
    }
    overheads.sort_unstable();
    works.sort_unstable();
    let n = overheads.len();
    eprintln!(
        "z3 tree meter: production bound {:?}: {whole} whole, {gapped} gapped of {n}; overhead per goal median {:?} p90 {:?} max {:?}; solver work median {:?} max {:?}",
        sandbox_meter::probe::SETTLE_BOUND,
        overheads[n / 2],
        overheads[n * 9 / 10],
        overheads[n - 1],
        works[n / 2],
        works[n - 1]
    );
}

/// Through the cascade: an SMT goal fails the T0 propositional decider (its
/// figure the wall-time estimate) and is proved by the resident `z3` (read
/// whole, `HwShunt`). The goal's headline cost sums both, so it is sealed
/// `Estimator`, never as a hardware reading of a total that holds an
/// estimate; the T1 attempt's own record keeps its hardware grade.
#[test]
fn a_cascade_total_holding_modelled_waste_is_not_sealed_as_hardware() {
    use proof_cascade::{ProofCache, Router};
    use proof_solvers::Propositional;
    let _one = alone();
    let Some(server) = server(TEST_SETTLE) else { return };
    let router = Router::new(vec![Box::new(Propositional), Box::new(server)]);
    let (_, goal) = &theorems()[1];
    let r = router.prove(goal, &mut ProofCache::new());
    eprintln!(
        "z3 tree meter: cascade: total {} uj ({} wasted) sealed {:?}, attempts {:?}",
        r.total_uj, r.wasted_uj, r.provenance, r.attempts
    );
    assert!(r.proved);
    let grades: Vec<Provenance> = r.attempts.iter().map(|a| a.provenance).collect();
    assert_eq!(grades, vec![Provenance::Estimator, Provenance::HwShunt]);
    assert_eq!(r.provenance, Provenance::Estimator);
}

/// Without its operator's declaration, a resident decision read whole off
/// `z3`'s tree is NOT sealed as hardware. The tree cannot show work handed
/// outside it: a `z3` on `PATH` that forwards each goal to a solver in a
/// container or on another host reads whole here (only the forwarding
/// client is in the tree) while the decision's energy is charged elsewhere.
#[test]
fn an_undeclared_resident_decision_keeps_the_estimate() {
    let _one = alone();
    if !z3_available() || process_energy_status() != CounterStatus::Live {
        eprintln!("no z3, or no live per-process counter: nothing to seal either way");
        return;
    }
    let server = Z3Server::new().with_settle_bound(TEST_SETTLE);
    for (name, goal) in theorems() {
        let a = server.attempt(&goal);
        assert!(a.verdict.is_proved(), "{name}");
        let acct = server.last_account().expect("an account of the attempt");
        eprintln!("z3 tree meter: undeclared {name}: sealed {:?}, because {:?}", a.energy, acct.modelled_because);
        assert_eq!(a.energy.provenance, Provenance::Estimator, "{name}: an undeclared z3 was sealed as hardware");
        assert_eq!(a.energy, Energy::estimator(acct.modelled_uj), "{name}");
        let r = acct.reading.clone().expect("a span was opened").expect("a reading");
        let mut want = if r.is_whole() { Vec::new() } else { vec![Modelled::Gaps(r.gaps.clone())] };
        want.push(Modelled::NotDeclaredSelfContained);
        assert_eq!(acct.modelled_because, want, "{name}");
        assert!(acct.z3.as_ref().is_some_and(|p| p.is_absolute()), "{name}: {:?}", acct.z3);
    }
}