//! Solvers for the proof tier ladder (SPEC §4).
//!
//! The two bottom rungs are **real** and report energy with `Estimator`
//! provenance (measured wall time × a default power no host calibrated,
//! [`DEFAULT_ACTIVE_MILLIWATTS`]), but for one case:
//!
//! - [`Propositional`] (T0) → parses a boolean goal and decides validity by
//!   truth-table, in process.
//! - [`Z3Smt`] (T1) → shells out to `z3` on an SMT-LIB2 goal (assert the
//!   negation; `unsat` ⇒ valid). [`Z3Server`] keeps `z3` resident across goals,
//!   and where this host's kernel counts each process's CPU energy live
//!   (macOS), reads each decision off the resident `z3`'s own process tree:
//!   `HwShunt` when the reading saw nothing missing and the operator has
//!   declared that `z3` decides in its own tree, the estimate otherwise (see
//!   [`Z3Server`] for exactly when).
//! - [`LeanVerifier`] → runs Lean and reports what the kernel accepted.
//!
//! The model rungs are stand-ins that gate on `GoalKind` until real backends are
//! wired behind the identical [`Solver`] trait:
//!
//! - [`SmallModel`] (T2) → a distilled in-domain prover.
//! - [`FrontierModel`] (T3) → a frontier reasoning model; the last resort.
//! - [`Automation`] / [`Smt`] → the original `GoalKind`-gated stand-ins, kept for
//!   [`reference_ladder`].
//!
//! **A solver returns `Proved` only when a verifier would accept the artifact —
//! correctness is never traded for energy.** The stand-ins cannot honour that on
//! their own: they check nothing, and their "artifact" is a hash of the goal
//! restated. So the contract is held at the *ladder* level instead, by
//! [`Solver::is_reference_stub`] and the two ladder families described below —
//! a stand-in is a routing fixture, never evidence, and never sits beneath a
//! real rung where the router would escalate into it.

pub mod prop;

use std::io::{BufRead, BufReader, Read, Write};
use std::path::{Path, PathBuf};
use std::process::{Child, Command, Stdio};
use std::sync::{mpsc, Mutex};
use std::time::{Duration, Instant};

use proof_schema::{Attempt, ContentId, Energy, GoalKind, ProofGoal, Solver, Tier, Verdict};
use sandbox_meter::{TreeError, TreeGap, TreeMeter, TreeReading};

/// The active power the wall-time figure assumes, in milliwatts: an
/// order-of-magnitude draw for one busy core (~15 W), documented, not
/// measured on any host.
pub const DEFAULT_ACTIVE_MILLIWATTS: u64 = 15_000;

/// Convert elapsed nanoseconds to microjoules at [`DEFAULT_ACTIVE_MILLIWATTS`].
fn ns_to_uj(ns: u128) -> u64 {
    // mW × ns = 10⁻¹² J = 10⁻⁶ µJ; at 15 W, µJ = ns × 15 / 1000.
    (ns.saturating_mul(DEFAULT_ACTIVE_MILLIWATTS as u128) / 1_000_000) as u64
}

/// The figure for `ns` of solver wall time: [`ns_to_uj`], at least 1 µJ,
/// graded `Estimator`. The power is assumed, not calibrated on this host, so
/// wall time × it is an estimate (the JCP metering ladder's rung 6), never
/// `ModelBased`, which a model earns by its calibration; a hardware interface
/// read live over the work would make it `HwShunt`.
fn wall_time_estimate(ns: u128) -> Energy {
    Energy::estimator(ns_to_uj(ns).max(1))
}

fn proved(goal: &ProofGoal) -> Verdict {
    Verdict::Proved {
        artifact: ContentId::of_bytes(goal.statement.as_bytes()),
    }
}

/// T0 — proof-language automation stand-in. Discharges goals that close by
/// normalization or linear arithmetic.
pub struct Automation;

impl Solver for Automation {
    /// A stand-in: it decides by goal *kind*, never by inspecting the claim.
    fn is_reference_stub(&self) -> bool {
        true
    }
    fn tier(&self) -> Tier {
        Tier::Automation
    }
    fn attempt(&self, goal: &ProofGoal) -> Attempt {
        let verdict = match goal.kind {
            GoalKind::Trivial | GoalKind::Arithmetic => proved(goal),
            _ => Verdict::Unproved,
        };
        Attempt {
            tier: Tier::Automation,
            verdict,
            energy: Energy::estimate_tier(Tier::Automation),
        }
    }
}

/// T1 — SMT / decision-procedure stand-in. Discharges decidable / arithmetic goals.
pub struct Smt;

impl Solver for Smt {
    /// A stand-in: it decides by goal *kind*, never by inspecting the claim.
    fn is_reference_stub(&self) -> bool {
        true
    }
    fn tier(&self) -> Tier {
        Tier::Smt
    }
    fn attempt(&self, goal: &ProofGoal) -> Attempt {
        let verdict = match goal.kind {
            GoalKind::Decidable | GoalKind::Arithmetic => proved(goal),
            _ => Verdict::Unproved,
        };
        Attempt {
            tier: Tier::Smt,
            verdict,
            energy: Energy::estimate_tier(Tier::Smt),
        }
    }
}

/// T2 — a small distilled prover for goals that genuinely need learned search.
pub struct SmallModel;

impl Solver for SmallModel {
    /// A stand-in: it decides by goal *kind*, never by inspecting the claim.
    fn is_reference_stub(&self) -> bool {
        true
    }
    fn tier(&self) -> Tier {
        Tier::SmallModel
    }
    fn attempt(&self, goal: &ProofGoal) -> Attempt {
        let verdict = match goal.kind {
            GoalKind::General => proved(goal),
            _ => Verdict::Unproved,
        };
        Attempt {
            tier: Tier::SmallModel,
            verdict,
            energy: Energy::estimate_tier(Tier::SmallModel),
        }
    }
}

/// T3 — the frontier reasoning model, the last resort.
pub struct FrontierModel;

impl Solver for FrontierModel {
    /// A stand-in: it decides by goal *kind*, never by inspecting the claim.
    fn is_reference_stub(&self) -> bool {
        true
    }
    fn tier(&self) -> Tier {
        Tier::BigModel
    }
    fn attempt(&self, goal: &ProofGoal) -> Attempt {
        Attempt {
            tier: Tier::BigModel,
            verdict: proved(goal),
            energy: Energy::estimate_tier(Tier::BigModel),
        }
    }
}

/// T0 — a **real** propositional decider (no stand-in). Parses the goal and
/// decides validity by truth-table, with energy measured from execution time. A
/// goal beyond propositional logic is refused so the router escalates.
pub struct Propositional;

impl Solver for Propositional {
    fn tier(&self) -> Tier {
        Tier::Automation
    }
    fn attempt(&self, goal: &ProofGoal) -> Attempt {
        let start = Instant::now();
        let verdict = match prop::parse(&goal.statement).and_then(|e| prop::is_valid(&e)) {
            Some(true) => Verdict::Proved {
                artifact: ContentId::of_bytes(goal.statement.as_bytes()),
            },
            _ => Verdict::Unproved,
        };
        Attempt {
            tier: Tier::Automation,
            verdict,
            energy: wall_time_estimate(start.elapsed().as_nanos()),
        }
    }
}

/// The prefix of the end marker that closes z3's output for each script
/// ([`end_marker`]). A goal statement containing it is refused, never run.
const END_MARKER_PREFIX: &str = "@@END@@";

/// A fresh end marker for one script: [`END_MARKER_PREFIX`] and 128 bits no
/// goal can predict, in hex. The bits are two keyed hashes of a counter, under
/// keys std's `RandomState` draws from the operating system's randomness.
///
/// Every script's output is read up to its own marker. A fixed marker let a
/// goal print it (`(echo "@@END@@")`): the read stopped early, the goal's real
/// answer stayed in the pipe, and every later goal on the resident session
/// was read off the answer of the goal before it — a FALSE claim came back
/// proved. A goal cannot print a marker drawn after it was written.
fn end_marker() -> String {
    use std::collections::hash_map::RandomState;
    use std::hash::{BuildHasher, Hasher};
    use std::sync::atomic::{AtomicU64, Ordering};
    static DRAWN: AtomicU64 = AtomicU64::new(0);
    let n = DRAWN.fetch_add(1, Ordering::Relaxed);
    let keys = RandomState::new();
    let word = |lane: u8| {
        let mut h = keys.build_hasher();
        h.write_u64(n);
        h.write_u8(lane);
        h.finish()
    };
    format!("{END_MARKER_PREFIX}{:016x}{:016x}", word(0), word(1))
}

/// The text written to `z3` for a goal: the statement, then this crate's own
/// `(check-sat)`, then the end marker. The answer is the line that
/// `(check-sat)` printed, which is the line just before the marker
/// ([`Reply`]): every command of the statement has run, and printed whatever
/// it prints, before it.
fn framed(statement: &str, marker: &str) -> String {
    format!("{statement}\n(check-sat)\n(echo \"{marker}\")\n")
}

/// `z3`'s answer to this crate's `(check-sat)`.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
enum CheckSat {
    Sat,
    Unsat,
    Unknown,
}

/// What `z3` said of one script, read up to its end marker.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
enum Answer {
    /// A decision: the line before the marker is a verdict, and nothing in
    /// the script's output was an error.
    Verdict(CheckSat),
    /// `z3` answered, but not with a decision: an error anywhere in the
    /// output, or no verdict where this crate's `(check-sat)` answers.
    Undecided,
}

/// The resident session cannot be trusted any more: the script could not be
/// written, or `z3`'s output ended or failed before the marker. The session
/// is retired, never reused.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
struct Broken;

/// `z3`'s output for one script, line by line up to (not including) its end
/// marker.
#[derive(Debug, Default)]
struct Reply {
    error: bool,
    last: Option<String>,
}

impl Reply {
    fn line(&mut self, line: &str) {
        // z3 reports parse and command errors as `(error "...")` on STDOUT,
        // then carries on and answers `(check-sat)` anyway — against the part
        // of the script that parsed, or an empty stack if nothing did. Read as
        // a verdict, "I could not understand the goal" becomes a decision
        // about some other formula; and a refutation is terminal in this
        // cascade, the strongest wrong answer the ladder can give. So any
        // error at all makes the whole script undecided.
        if line.contains("(error") {
            self.error = true;
        }
        self.last = Some(line.trim().to_string());
    }

    /// The answer: the verdict on the line just before the marker, which is
    /// this crate's `(check-sat)`'s, never a verdict-shaped line the goal
    /// printed itself (`(echo "unsat")`) — the first such line was once read
    /// as the answer, and proved a false claim.
    fn answer(&self) -> Answer {
        if self.error {
            return Answer::Undecided;
        }
        match self.last.as_deref() {
            Some("sat") => Answer::Verdict(CheckSat::Sat),
            Some("unsat") => Answer::Verdict(CheckSat::Unsat),
            Some("unknown") => Answer::Verdict(CheckSat::Unknown),
            _ => Answer::Undecided,
        }
    }
}

/// How long `z3` may work on one goal before it gives up on its own: its soft
/// per-query timeout (`-t:`), after which `(check-sat)` answers `unknown` — an
/// undecided goal, which nothing here reads as proved. Measured on the build
/// host: a goal `z3` cannot decide in time answers `unknown` at the limit.
pub const GOAL_TIMEOUT: Duration = Duration::from_secs(60);

/// How long past a goal's timeout a read waits for the goal's end marker
/// before it takes `z3` as wedged. A goal may set `:timeout` itself and so
/// outlast the soft limit; past this deadline the one-shot `z3` is killed and
/// a resident session is broken and replaced, the goal undecided — so no goal
/// can hold the session, and every goal queued behind it, for ever.
pub const GOAL_DEADLINE_GRACE: Duration = Duration::from_secs(5);

/// `z3`'s arguments for a goal limit of `timeout`: SMT-LIB on stdin, and the
/// soft per-query timeout in milliseconds.
fn z3_args(timeout: Duration) -> [String; 3] {
    ["-in".into(), "-smt2".into(), format!("-t:{}", timeout.as_millis().max(1))]
}

/// `input` on a one-shot `z3` limited to `timeout` a goal: its stdout, or
/// `None` if `z3` could not be run or did not finish by the deadline
/// (`timeout` plus [`GOAL_DEADLINE_GRACE`]), in which case it is killed.
fn run_one_shot(input: &str, timeout: Duration) -> Option<String> {
    let child = Command::new("z3")
        .args(z3_args(timeout))
        .stdin(Stdio::piped())
        .stdout(Stdio::piped())
        .stderr(Stdio::null())
        .spawn()
        .ok()?;
    output_within(child, input, timeout.saturating_add(GOAL_DEADLINE_GRACE))
}

/// `input` written to `child`'s stdin, which is then closed, and all of its
/// stdout once it closes that: `None` if it does not by `deadline`, and the
/// child is killed. The child is reaped either way.
///
/// Both ends are on threads of their own. `z3` reads its input only as it
/// gets to each command, so a goal with a `(check-sat)` of its own and more
/// than a pipe's worth of text after it holds a write on the calling thread
/// for as long as that check runs — past any deadline the read keeps.
fn output_within(mut child: Child, input: &str, deadline: Duration) -> Option<String> {
    let reap = |child: &mut Child| {
        let _ = child.kill();
        let _ = child.wait();
    };
    let (Some(mut stdin), Some(mut stdout)) = (child.stdin.take(), child.stdout.take()) else {
        reap(&mut child);
        return None;
    };
    let input = input.to_owned();
    // Ends when the input is written, or the child stops reading it (it
    // exited, or was killed here).
    std::thread::spawn(move || {
        let _ = stdin.write_all(input.as_bytes());
    });
    let (tx, rx) = mpsc::channel();
    std::thread::spawn(move || {
        let mut out = Vec::new();
        let _ = stdout.read_to_end(&mut out);
        let _ = tx.send(String::from_utf8_lossy(&out).into_owned());
    });
    match rx.recv_timeout(deadline) {
        Ok(out) => {
            let _ = child.wait();
            Some(out)
        }
        Err(_) => {
            reap(&mut child);
            None
        }
    }
}

/// Read `lines` up to `marker` into a [`Reply`]: `None` if the marker never
/// came (`z3` ended first).
fn reply_until<'a>(lines: &mut impl Iterator<Item = &'a str>, marker: &str) -> Option<Reply> {
    let mut reply = Reply::default();
    for line in lines {
        if line.trim() == marker {
            return Some(reply);
        }
        reply.line(line);
    }
    None
}

/// Run a one-shot `z3` on an SMT-LIB2 script (piped over stdin) and return
/// the answer to this crate's `(check-sat)`. `None` if `z3` is absent, the
/// script errored, or no verdict came — the router reads that as "escalate",
/// never as proof.
fn run_z3(script: &str) -> Option<CheckSat> {
    let marker = end_marker();
    let out = run_one_shot(&framed(script, &marker), GOAL_TIMEOUT)?;
    match reply_until(&mut out.lines(), &marker)?.answer() {
        Answer::Verdict(v) => Some(v),
        Answer::Undecided => None,
    }
}

/// Fetch the counter-model for a refuted goal: re-run `z3` with `(get-model)`
/// appended so the witness assignment is captured for the `Refuted` verdict.
/// Best-effort — returns an empty string if `z3` declines a model (some goals
/// are `sat` without a printable model). Only called on the refutation path,
/// which is terminal, so the extra spawn costs nothing on the proved path.
/// A `sat` answer becomes a refutation only when z3 can actually produce a
/// counter-model. An empty or absent model is not evidence of falsehood — most
/// often it means nothing was asserted — and since a refutation halts the
/// cascade as a final decision, an unsubstantiated one is worse than no answer.
fn refutation_or_undecided(script: &str) -> Verdict {
    let cm = z3_counter_model(script).unwrap_or_default();
    // A model with no assignments in it: "(", ")", whitespace, and nothing else.
    let substantive = cm.chars().any(|c| !matches!(c, '(' | ')' | ' ' | '\n' | '\t' | '\r'));
    if substantive {
        Verdict::Refuted { counter_model: cm }
    } else {
        Verdict::Unproved
    }
}

/// The model `z3` gives for `script`, framed like every other script: this
/// run must itself answer `sat` to this crate's `(check-sat)` with no error,
/// and the model is the output of the `(get-model)` after it, between two
/// fresh markers — never text the goal printed. `None` otherwise.
fn z3_counter_model(script: &str) -> Option<String> {
    let (decided, modelled) = (end_marker(), end_marker());
    let input = format!("{}(get-model)\n(echo \"{modelled}\")\n", framed(script, &decided));
    let out = run_one_shot(&input, GOAL_TIMEOUT)?;
    let mut lines = out.lines();
    if reply_until(&mut lines, &decided)?.answer() != Answer::Verdict(CheckSat::Sat) {
        return None;
    }
    let mut model = Vec::new();
    for line in lines {
        if line.trim() == modelled {
            return Some(model.join("\n").trim().to_string());
        }
        if line.contains("(error") {
            return None;
        }
        model.push(line.trim_end());
    }
    None
}

/// T1 — a **real** SMT backend that shells out to `z3`. The goal's statement is
/// an SMT-LIB2 script asserting the *negation* of the claim; `unsat` ⇒ the
/// claim is valid — a genuine decision by a trusted procedure. `sat` is a real
/// counter-model (refuse); `unknown`/missing `z3` escalates. Energy is measured
/// from the solver's wall time.
pub struct Z3Smt;

impl Solver for Z3Smt {
    fn tier(&self) -> Tier {
        Tier::Smt
    }
    fn attempt(&self, goal: &ProofGoal) -> Attempt {
        let start = Instant::now();
        // The same shape guard the resident session applies. One-shot `z3` was
        // missing it, so prose reached the solver and came back "refuted".
        let outcome = if admit(&goal.statement).is_some() {
            run_z3(&goal.statement)
        } else {
            None
        };
        let verdict = match outcome {
            Some(CheckSat::Unsat) => Verdict::Proved {
                artifact: ContentId::of_bytes(goal.statement.as_bytes()),
            },
            // `sat` = the negated claim is satisfiable = the claim is FALSE. A
            // decision, not a failure to decide — surface the witness and let
            // the router halt rather than escalate a disproof.
            //
            // But only where a witness actually exists: a script that asserts
            // nothing is trivially satisfiable, and `sat` from an empty
            // assertion stack means "no constraints", not "here is a
            // counter-example". A disproof is terminal, so it must carry
            // evidence or it is not a disproof.
            Some(CheckSat::Sat) => refutation_or_undecided(&goal.statement),
            _ => Verdict::Unproved,
        };
        Attempt {
            tier: Tier::Smt,
            verdict,
            energy: wall_time_estimate(start.elapsed().as_nanos()),
        }
    }
}

/// A long-lived `z3 -in` process that decides many goals across one startup —
/// the fix for the per-spawn startup tax. Each goal is isolated with `(reset)`
/// and framed like a one-shot script ([`framed`]): this crate's own
/// `(check-sat)`, then a fresh, unpredictable end marker ([`end_marker`]).
///
/// `(reset)` clears assertions and declarations but NOT options: `z3` keeps
/// every `set-option` across it, so one goal's `:rlimit` or `:timeout` would
/// reach every goal after it. A session is therefore retired — killed and
/// replaced — after a goal that sets an option, and after any goal it did not
/// answer cleanly ([`Z3Server`]).
///
/// A goal is limited twice: `z3`'s own soft timeout gives `unknown` at the
/// limit, and the read gives up [`GOAL_DEADLINE_GRACE`] past it, for a goal
/// that set its own `:timeout` or a `z3` that does not stop. The session's
/// stdin is written and its stdout read on threads of their own, so that
/// neither a write `z3` is not taking nor a read it is not answering can
/// hold a goal past that deadline (see [`output_within`]).
struct Z3Session {
    child: Child,
    /// Scripts for `z3`'s stdin, to the session's writer thread.
    scripts: mpsc::Sender<String>,
    /// `z3`'s stdout, a line at a time, from the session's reader thread.
    lines: mpsc::Receiver<String>,
    /// How long one goal's read waits for its end marker: the soft timeout
    /// plus [`GOAL_DEADLINE_GRACE`].
    deadline: Duration,
}

/// The `z3` a resident session runs: the first `z3` on `PATH`, as a spawn by
/// name finds it, with symlinks resolved — the file the kernel executes. The
/// session is started from this path, so the path recorded is the binary
/// that ran.
fn resolve_z3() -> Option<PathBuf> {
    let name = if cfg!(windows) { "z3.exe" } else { "z3" };
    std::env::split_paths(&std::env::var_os("PATH")?)
        .map(|dir| dir.join(name))
        .find(|p| is_executable(p))
        .and_then(|p| p.canonicalize().ok())
}

fn is_executable(p: &Path) -> bool {
    #[cfg(unix)]
    {
        use std::os::unix::fs::PermissionsExt;
        p.metadata().is_ok_and(|m| m.is_file() && m.permissions().mode() & 0o111 != 0)
    }
    #[cfg(not(unix))]
    {
        p.is_file()
    }
}

impl Z3Session {
    /// A session on `z3`, each goal limited to `timeout` (see [`Z3Session`]).
    fn spawn(z3: &Path, timeout: Duration) -> Option<Self> {
        let mut child = Command::new(z3)
            .args(z3_args(timeout))
            .stdin(Stdio::piped())
            .stdout(Stdio::piped())
            .stderr(Stdio::null())
            .spawn()
            .ok()?;
        let (Some(mut stdin), Some(stdout)) = (child.stdin.take(), child.stdout.take()) else {
            let _ = child.kill();
            let _ = child.wait();
            return None;
        };
        let (scripts, to_write) = mpsc::channel::<String>();
        // Ends when the session is dropped, or a write fails: `z3` exited or
        // was killed. A session whose writer has ended is broken.
        std::thread::spawn(move || {
            for script in to_write {
                if stdin.write_all(script.as_bytes()).and_then(|()| stdin.flush()).is_err() {
                    break;
                }
            }
        });
        let (tx, lines) = mpsc::channel();
        // Ends when `z3` closes its stdout: when the session is dropped (and
        // `z3` killed), or `z3` exits.
        std::thread::spawn(move || {
            for line in BufReader::new(stdout).lines() {
                let Ok(line) = line else { break };
                if tx.send(line).is_err() {
                    break;
                }
            }
        });
        Some(Self { child, scripts, lines, deadline: timeout.saturating_add(GOAL_DEADLINE_GRACE) })
    }

    /// The resident `z3`'s pid. It names this `z3` for as long as the session
    /// lives: the session holds the [`Child`] unreaped until it is dropped.
    fn pid(&self) -> u32 {
        self.child.id()
    }

    /// Decide one script (the caller has [`admit`]ted it): reset, write it
    /// framed, and read up to this script's own marker. [`Broken`] when `z3`
    /// ended, or the marker did not come by the session's deadline: the
    /// caller retires the session, so nothing late reaches the next goal.
    fn decide(&mut self, script: &str) -> Result<Answer, Broken> {
        let marker = end_marker();
        let until = Instant::now() + self.deadline;
        self.scripts.send(format!("(reset)\n{}", framed(script, &marker))).map_err(|_| Broken)?;
        let mut reply = Reply::default();
        loop {
            let line = self.lines.recv_timeout(until.saturating_duration_since(Instant::now())).map_err(|_| Broken)?;
            if line.trim() == marker {
                return Ok(reply.answer());
            }
            reply.line(&line);
        }
    }
}

impl Drop for Z3Session {
    fn drop(&mut self) {
        let _ = self.child.kill();
        let _ = self.child.wait();
    }
}

/// What the shape guard ([`admit`]) found in a script it admitted.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
struct Admitted {
    /// The script sets a solver option, which `z3` keeps across `(reset)`:
    /// the resident session that runs it is retired after it.
    sets_option: bool,
}

/// The shape guard on every script written to `z3`, resident or one-shot. A
/// script is admitted only when it is a sequence of whole SMT-LIB commands
/// that cannot take over the framing around it; anything else is refused
/// without touching `z3` (undecided), so no goal can desync, wedge or end the
/// long-lived process. Refused:
///
/// - a statement containing the end marker's prefix ([`END_MARKER_PREFIX`]);
/// - anything but whole parenthesized commands at the top level: an atom
///   there, an unbalanced parenthesis, no command at all, or a string literal
///   or quoted symbol left open — an open one swallows this crate's
///   `(check-sat)` and marker, and the read never ends. Parentheses inside
///   strings, quoted symbols and comments are not counted;
/// - a command that ends `z3` (`exit`) or reads a file (`include`);
/// - a `set-option` of an output channel (`:regular-output-channel`,
///   `:diagnostic-output-channel`), which sends `z3`'s answers — and the
///   marker — elsewhere, and keeps them there across `(reset)`.
///
/// Command names are read as `z3` reads them: `|exit|` is `exit`.
fn admit(statement: &str) -> Option<Admitted> {
    if statement.contains(END_MARKER_PREFIX) {
        return None;
    }
    let b = statement.as_bytes();
    let mut i = 0;
    let mut depth: u32 = 0;
    let mut commands = 0u32;
    let mut sets_option = false;
    // The next token is a command's name / a `set-option`'s keyword.
    let (mut want_head, mut want_option) = (false, false);
    while i < b.len() {
        let token: &str = match b[i] {
            b' ' | b'\t' | b'\n' | b'\r' => {
                i += 1;
                continue;
            }
            b';' => {
                while i < b.len() && b[i] != b'\n' {
                    i += 1;
                }
                continue;
            }
            b'(' => {
                if want_head {
                    return None;
                }
                if depth == 0 {
                    want_head = true;
                    commands += 1;
                }
                want_option = false;
                depth += 1;
                i += 1;
                continue;
            }
            b')' => {
                if depth == 0 || want_head {
                    return None;
                }
                want_option = false;
                depth -= 1;
                i += 1;
                continue;
            }
            b'"' => {
                // A string literal; `""` inside it is an escaped quote.
                i += 1;
                loop {
                    match b.get(i) {
                        None => return None,
                        Some(b'"') if b.get(i + 1) == Some(&b'"') => i += 2,
                        Some(b'"') => break,
                        Some(_) => i += 1,
                    }
                }
                i += 1;
                if depth == 0 || want_head {
                    return None;
                }
                want_option = false;
                continue;
            }
            b'|' => {
                // A quoted symbol: no escapes, ends at the next `|`.
                let start = i + 1;
                i = start;
                while i < b.len() && b[i] != b'|' {
                    i += 1;
                }
                if i >= b.len() {
                    return None;
                }
                i += 1;
                &statement[start..i - 1]
            }
            _ => {
                let start = i;
                while i < b.len() && !matches!(b[i], b' ' | b'\t' | b'\n' | b'\r' | b'(' | b')' | b'"' | b'|' | b';') {
                    i += 1;
                }
                &statement[start..i]
            }
        };
        if depth == 0 {
            return None;
        }
        if want_head {
            want_head = false;
            match token {
                "exit" | "include" => return None,
                "set-option" => {
                    sets_option = true;
                    want_option = true;
                }
                _ => {}
            }
        } else if want_option {
            want_option = false;
            if token.contains("output-channel") {
                return None;
            }
        }
    }
    (depth == 0 && commands > 0).then_some(Admitted { sets_option })
}

/// T1 — `z3` kept **resident** across goals. Same decision semantics as
/// [`Z3Smt`], but the per-goal energy excludes process startup — and, where
/// this host can read it, is the resident `z3`'s own energy.
///
/// **Isolation.** Every goal passes the shape guard (`admit`) before it is
/// written, and is read up to an end marker drawn fresh for it, so no goal's
/// output can be read as another's. The session is retired — its `z3` killed
/// and reaped, a new one started (with a new meter) — after a goal that sets
/// an option (`z3` keeps options across `(reset)`), after any goal it did not
/// answer with a clean verdict (an error, or no verdict where this crate's
/// `(check-sat)` answers), and whenever it breaks (the script cannot be
/// written, or `z3`'s output ends before the marker). Each goal is therefore
/// decided as a fresh `z3` would decide it. The new session is started after
/// the attempt's span has stopped; its startup is in the attempt's overhead,
/// never in its figure.
///
/// **Metering.** Each decision is written to the resident `z3` and its
/// verdict read back; the work runs in that process while this thread waits,
/// so this process's own energy count would read the waiting. Where the
/// host's kernel counts each process's CPU energy live
/// ([`sandbox_meter::TreeMeter`]: macOS, where its liveness probe passed), the
/// decision is read off the resident `z3`'s own process tree instead — the
/// CPU energy the kernel attributes to `z3`'s threads (and any descendant's)
/// from just before the script is written to just after the verdict's end
/// marker is read, each end walked until the tree is quiet (up to the
/// settle bound, [`Z3Server::with_settle_bound`]). A session's meter is built
/// when the session starts: the first one in a process pays the counter's
/// liveness probe, about 300 ms of CPU on the constructing thread, so the
/// first goal does not.
///
/// The attempt's figure is that reading, `HwShunt` ([`Energy::measured`]),
/// rounded UP to a whole µJ (a reading of 1 to 999 nJ is 1 µJ, never a
/// measured zero), only when **both** hold:
///
/// 1. **Nothing was seen missing from the tree.** The reading has no gap
///    ([`TreeReading::is_whole`]): every member read and quiet at both ends,
///    no descendant reaped or exited in the span, no GPU client held, no
///    in-process Neural Engine memory — and no gap of any kind the meter
///    reports now or comes to report.
/// 2. **There is nothing outside the tree to miss, on the operator's
///    declaration.** A tree reading cannot see work its process hands to
///    another (a system service, a server, a solver in a container, a VM or
///    on another host): that is charged to the other process. A `z3` on
///    `PATH` that forwards each goal elsewhere reads whole — only the
///    forwarding client is in the tree — and would be sealed far short of
///    the decision. This crate cannot tell: it names `z3` by `PATH`, and
///    spawning it says nothing about what answers to that name. So, as
///    jcp-gateway seals an upstream's reading and sandbox-proof a local
///    engine's only on its operator's declaration that it delegates
///    nothing, a reading here is sealed only on the operator's declaration
///    that the `z3` it runs — the binary at [`Z3EnergyAccount::z3`], the
///    first on `PATH` with symlinks resolved — decides each goal in its own
///    process tree ([`Z3Server::declared_self_contained`]; proof-cli reads
///    `PROOF_Z3_SELF_CONTAINED=1`). Undeclared, the default, a whole reading
///    keeps the wall-time estimate ([`Modelled::NotDeclaredSelfContained`]).
///    Condition 1 still applies to every reading, so a declared `z3` that
///    forked or used the GPU is graded down by its gaps.
///
/// Otherwise the attempt keeps the figure it always had — the solver's wall
/// time × the crate's default power ([`DEFAULT_ACTIVE_MILLIWATTS`], ~15 W,
/// which no host calibrated), an estimate, [`Energy::estimator`] — and never
/// seals the reading: [`Energy`] has no coverage field, so a reading of part
/// of the decision sealed as `HwShunt` would claim the whole. The estimate is
/// the figure when:
///
/// - the reading has a gap ([`Modelled::Gaps`]: it is short of the tree's
///   energy, or with a member still running at the start may hold a little
///   from before the span);
/// - the reading was taken, but the `z3` is not declared self-contained
///   ([`Modelled::NotDeclaredSelfContained`]);
/// - the span gave no reading ([`Modelled::NoReading`]: `z3` gone, or its
///   count not advanced);
/// - there is no tree meter ([`Modelled::NoTreeMeter`]: off macOS, or the
///   per-process counter is not live here);
/// - the goal never reached `z3` ([`Modelled::NotRun`]: refused by the shape
///   guard, or no session);
/// - the goal was refuted ([`Modelled::CounterModelOutsideTree`]): the
///   counter-model is fetched by a ONE-SHOT `z3`, a child of this process,
///   not of the resident one, so it is outside the tree. Its span is never
///   opened over it — the tree span covers the resident decision alone — and
///   its work is in the attempt's figure only through the estimate, which
///   then covers the whole attempt: the resident decision and the one-shot
///   run.
///
/// Why each attempt was graded as it was is kept beside it, not on the wire:
/// [`Z3Server::last_account`].
///
/// **Cost.** The span adds two things to each goal's latency, at each end.
/// The tree is walked until it is quiet: `z3` blocks on its next read as
/// soon as it has written the end marker, so on a quiet host that is a few
/// walks of one process (tens of µs each), and on a loaded one up to the
/// settle bound, after which a reading still unsettled is a gap (the
/// estimate). And the GPU clients are read from the I/O Registry — before the
/// start walk and after the stop walk, outside the settle bound — which
/// takes about a millisecond on the hosts measured and has been seen at
/// tens of milliseconds under heavy load. Together, on a loaded development
/// host at the production bound, that has come to a few milliseconds for a
/// typical goal, several at the 90th percentile and tens at worst; the test
/// `the_production_settle_bound_grades_every_attempt_consistently` logs the
/// figures on the host it runs on. The estimate times the solver's work
/// alone — the resident decision and, when it runs, the one-shot `z3` —
/// never the meter's walks or reads, nor a retired session's replacement
/// starting after the span.
pub struct Z3Server {
    /// The resident session and its meter: `None` when `z3` could not be
    /// started.
    resident: Mutex<Option<Resident>>,
    /// The settle bound each session's meter is built with; `None`: the
    /// meter's default.
    settle_bound: Option<Duration>,
    /// How long each session's `z3` may work on one goal
    /// ([`Z3Server::with_goal_timeout`]; default [`GOAL_TIMEOUT`]).
    goal_timeout: Duration,
    /// The operator's declaration that the `z3` it runs decides each goal in
    /// its own process tree ([`Z3Server::declared_self_contained`]).
    self_contained: bool,
    /// How the last attempt's energy was obtained.
    last: Mutex<Option<Z3EnergyAccount>>,
}

/// A resident session and the tree meter of its `z3`, retired together.
struct Resident {
    session: Z3Session,
    /// The binary the session was started from ([`resolve_z3`]).
    z3: PathBuf,
    /// The resident `z3`'s tree meter: `None` off macOS, or where the
    /// per-process counter is not live.
    meter: Option<TreeMeter>,
}

impl Resident {
    /// Start a session on the `z3` on `PATH` and, where this host can read
    /// it, its meter.
    fn start(settle_bound: Option<Duration>, goal_timeout: Duration) -> Option<Self> {
        let z3 = resolve_z3()?;
        let session = Z3Session::spawn(&z3, goal_timeout)?;
        let meter = TreeMeter::for_process(session.pid()).map(|m| match settle_bound {
            Some(bound) => m.with_settle_bound(bound),
            None => m,
        });
        Some(Self { session, z3, meter })
    }
}

/// Why a [`Z3Server`] attempt's figure is the wall-time estimate (`Estimator`)
/// rather than a reading of the resident `z3`'s tree. An attempt can have
/// several.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Modelled {
    /// The goal never reached the resident `z3`: the shape guard refused it,
    /// or there is no session (`z3` absent). Nothing ran that could be read.
    NotRun,
    /// This host has no tree meter for the resident `z3`: not macOS, or the
    /// kernel's per-process CPU energy counter is not live here.
    NoTreeMeter,
    /// The span over the decision gave no reading at all: `z3` gone or
    /// unreadable at an end, or its count did not advance.
    NoReading(TreeError),
    /// The reading saw part of the tree's energy missing (or, for a member
    /// still running at the start, possibly some from before the span): a
    /// partial figure, never sealed as the decision's.
    Gaps(Vec<TreeGap>),
    /// A reading was taken, but the operator has not declared that the `z3`
    /// it runs decides in its own process tree
    /// ([`Z3Server::declared_self_contained`]). Work handed outside the tree
    /// — to a solver in a container, a VM or on another host — is charged
    /// to the process that does it, so no reading of the tree can show it,
    /// and a forwarding `z3` reads whole.
    NotDeclaredSelfContained,
    /// The goal was refuted, and its counter-model fetched by a one-shot `z3`
    /// outside the resident tree, which no span read.
    CounterModelOutsideTree,
}

/// How one [`Z3Server`] attempt's energy was obtained: the figure the attempt
/// reported, the reading it was graded from, and why the estimate was kept
/// where it was. The gateway's plaintext account, in-process: the attempt's figure
/// and its provenance are what travels; this says why.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct Z3EnergyAccount {
    /// The attempt's figure, exactly as [`Attempt::energy`] reported it.
    pub energy: Energy,
    /// The resident `z3`'s tree reading over the decision, when a span was
    /// opened: `None` when the goal never reached `z3` or there is no meter.
    pub reading: Option<Result<TreeReading, TreeError>>,
    /// Empty when the figure is the reading; otherwise every reason the
    /// estimate was kept.
    pub modelled_because: Vec<Modelled>,
    /// The estimate, µJ: the solver's wall time (the resident decision, and
    /// the one-shot `z3` when it ran) × the crate's default power
    /// ([`DEFAULT_ACTIVE_MILLIWATTS`]), at least 1. The attempt's figure,
    /// graded `Estimator`, whenever `modelled_because` is not empty.
    pub modelled_uj: u64,
    /// The solver's own wall time: what `modelled_uj` is computed from.
    pub work: Duration,
    /// The attempt's wall time beyond `work`: the meter's settling at both
    /// ends of the span, and the rest of the attempt's bookkeeping. The
    /// latency the metering adds to the goal.
    pub overhead: Duration,
    /// The binary of the resident `z3` the goal was written to: the absolute
    /// path its session was started from (the first `z3` on `PATH`, symlinks
    /// resolved). What an operator's declaration is about. `None` when the
    /// goal reached no session.
    pub z3: Option<PathBuf>,
}

/// Grade a [`Z3Server`] attempt's energy. `reading`: the resident tree's span
/// over the decision, `None` when no span was opened; `ran`: the goal reached
/// the resident `z3`; `self_contained`: the operator's declaration;
/// `one_shot`: a one-shot `z3` fetched a counter-model outside the tree;
/// `modelled_uj`: the wall-time estimate.
///
/// `HwShunt` only for a reading with no gap at all, of a decision that ran
/// entirely in the tree, of a `z3` declared self-contained; otherwise the
/// wall-time estimate, `Estimator`, with every reason. Pure, so its tests drive every case without a
/// process.
fn grade_attempt(
    reading: Option<&Result<TreeReading, TreeError>>,
    ran: bool,
    self_contained: bool,
    one_shot: bool,
    modelled_uj: u64,
) -> (Energy, Vec<Modelled>) {
    let mut because: Vec<Modelled> = Vec::new();
    if !ran {
        because.push(Modelled::NotRun);
    }
    match reading {
        Some(Ok(r)) => {
            if !r.is_whole() {
                because.push(Modelled::Gaps(r.gaps.clone()));
            }
            if !self_contained {
                because.push(Modelled::NotDeclaredSelfContained);
            }
        }
        Some(Err(e)) => because.push(Modelled::NoReading(e.clone())),
        None if ran => because.push(Modelled::NoTreeMeter),
        None => {}
    }
    if one_shot {
        because.push(Modelled::CounterModelOutsideTree);
    }
    match reading {
        Some(Ok(r)) if because.is_empty() => (Energy::measured(r.cpu_nj.div_ceil(1_000)), because),
        _ => (Energy::estimator(modelled_uj.max(1)), because),
    }
}

impl Z3Server {
    /// Start the resident `z3` and, where this host can read it, its tree
    /// meter (the first one in a process pays the counter's liveness probe:
    /// see [`Z3Server`]).
    pub fn new() -> Self {
        Self {
            resident: Mutex::new(Resident::start(None, GOAL_TIMEOUT)),
            settle_bound: None,
            goal_timeout: GOAL_TIMEOUT,
            self_contained: false,
            last: Mutex::new(None),
        }
    }

    /// The same server, its tree meter waiting up to `bound` at each end of
    /// a decision for the resident `z3` to go quiet (default
    /// [`sandbox_meter::probe::SETTLE_BOUND`]). A `z3` still running when it
    /// runs out is a gap, so that decision keeps the wall-time estimate; a
    /// longer bound trades latency on a loaded host for fewer of those. It
    /// holds for every session the server starts.
    pub fn with_settle_bound(mut self, bound: Duration) -> Self {
        self.settle_bound = Some(bound);
        if let Ok(Some(r)) = self.resident.get_mut() {
            r.meter = r.meter.take().map(|m| m.with_settle_bound(bound));
        }
        self
    }

    /// The same server, each goal limited to `timeout` of `z3`'s work
    /// (default [`GOAL_TIMEOUT`]): `z3` answers `unknown` at the limit, an
    /// undecided goal; a goal that outlasts it by [`GOAL_DEADLINE_GRACE`]
    /// (it set its own `:timeout`) breaks the session, which is replaced. The
    /// resident session is restarted under the new limit, and every session
    /// the server starts keeps it.
    pub fn with_goal_timeout(mut self, timeout: Duration) -> Self {
        self.goal_timeout = timeout;
        if let Ok(r) = self.resident.get_mut() {
            *r = Resident::start(self.settle_bound, timeout);
        }
        self
    }

    /// The same server, on its operator's declaration that the `z3` it runs
    /// — the binary at [`Z3EnergyAccount::z3`] — decides each goal in its
    /// own process tree, handing no work to any other process: no container,
    /// VM, service or remote solver. A whole reading of a decision is sealed
    /// `HwShunt` only with it. Only the operator can make it: this crate
    /// names `z3` by `PATH`, and whatever answers to that name is what runs.
    /// Undeclared (the default), every decision keeps the wall-time estimate
    /// ([`Modelled::NotDeclaredSelfContained`]). proof-cli reads it from
    /// `PROOF_Z3_SELF_CONTAINED=1`.
    pub fn declared_self_contained(mut self, declared: bool) -> Self {
        self.self_contained = declared;
        self
    }

    /// The resident `z3`'s pid, while there is a session. A retired session's
    /// replacement has a new one.
    pub fn pid(&self) -> Option<u32> {
        self.resident.lock().ok()?.as_ref().map(|r| r.session.pid())
    }

    /// Whether decisions are read off the resident `z3`'s tree: a session,
    /// and a live per-process counter on this host.
    pub fn is_tree_metered(&self) -> bool {
        self.resident.lock().is_ok_and(|g| g.as_ref().is_some_and(|r| r.meter.is_some()))
    }

    /// How the last attempt's energy was obtained ([`Z3EnergyAccount`]).
    pub fn last_account(&self) -> Option<Z3EnergyAccount> {
        self.last.lock().ok()?.clone()
    }
}

impl Default for Z3Server {
    fn default() -> Self {
        Self::new()
    }
}

impl Solver for Z3Server {
    fn tier(&self) -> Tier {
        Tier::Smt
    }
    fn attempt(&self, goal: &ProofGoal) -> Attempt {
        let start = Instant::now();
        let mut work = Duration::ZERO;
        let mut reading: Option<Result<TreeReading, TreeError>> = None;
        let mut ran = false;
        let mut z3: Option<PathBuf> = None;
        let outcome = admit(&goal.statement).and_then(|script| {
            let mut g = self.resident.lock().ok()?;
            let r = g.as_mut()?;
            ran = true;
            z3 = Some(r.z3.clone());
            let session = &mut r.session;
            // The span is the resident decision and nothing else: opened
            // just before the script is written, stopped once the end
            // marker is read.
            let mut decide = || {
                let t = Instant::now();
                let v = session.decide(&goal.statement);
                work += t.elapsed();
                v
            };
            let answer = match &r.meter {
                Some(m) => {
                    let (v, rd) = m.measure(decide);
                    reading = Some(rd);
                    v
                }
                None => decide(),
            };
            // Retire the session unless it answered cleanly and holds no
            // option of this goal's: the next goal must meet a fresh `z3`.
            if script.sets_option || !matches!(answer, Ok(Answer::Verdict(_))) {
                *g = None;
                *g = Resident::start(self.settle_bound, self.goal_timeout);
            }
            match answer {
                Ok(Answer::Verdict(v)) => Some(v),
                Ok(Answer::Undecided) | Err(Broken) => None,
            }
        });
        let mut one_shot = false;
        let verdict = match outcome {
            Some(CheckSat::Unsat) => Verdict::Proved {
                artifact: ContentId::of_bytes(goal.statement.as_bytes()),
            },
            // `sat` ⇒ refuted. The resident session decided it; fetch the
            // witness with a one-shot `z3` (the refutation path is terminal, so
            // the extra spawn never touches the hot proved path). That `z3` is
            // not in the resident tree, and runs after its span has stopped.
            Some(CheckSat::Sat) => {
                one_shot = true;
                let t = Instant::now();
                let v = refutation_or_undecided(&goal.statement);
                work += t.elapsed();
                v
            }
            _ => Verdict::Unproved,
        };
        let modelled_uj = ns_to_uj(work.as_nanos()).max(1);
        let (energy, modelled_because) =
            grade_attempt(reading.as_ref(), ran, self.self_contained, one_shot, modelled_uj);
        if let Ok(mut last) = self.last.lock() {
            *last = Some(Z3EnergyAccount {
                energy,
                reading,
                modelled_because,
                modelled_uj,
                work,
                overhead: start.elapsed().saturating_sub(work),
                z3,
            });
        }
        Attempt {
            tier: Tier::Smt,
            verdict,
            energy,
        }
    }
}

/// **Lean 4 verifier backend** — the real proof-assistant rung, the SOTA
/// verifier substrate (Lean + Mathlib is what AlphaProof/Aristotle/Axiom build
/// on). It runs the `lean` typechecker on a goal whose `statement` *is* a
/// complete Lean theorem-with-proof and reports what Lean actually decided:
///
/// - typechecks (exit 0, no `error:`, no `sorry`) → `Proved` (Lean *is* the
///   verifier that makes `Proved` meaningful — the trust root, not a model).
/// - Lean's `decide` reports the proposition is false → `Refuted` (a decision,
///   carrying Lean's message as the counter-model witness — the cascade halts).
/// - any other failure, or `lean` not installed → `Unproved` (this rung did not
///   close it; the cascade escalates). Check [`LeanVerifier::available`] to skip
///   the rung when the toolchain is absent.
///
/// The goal→Lean encoding is the caller's (`context` carries the dialect, e.g.
/// `"lean4"`); the backend only attempts goals whose context names Lean. Energy
/// is `Estimator` (wall time × the crate's default power), like the z3 rung.
pub struct LeanVerifier {
    tier: Tier,
    lean_bin: String,
}

static LEAN_TMP_COUNTER: std::sync::atomic::AtomicU64 = std::sync::atomic::AtomicU64::new(0);

impl Default for LeanVerifier {
    fn default() -> Self {
        Self::new()
    }
}

impl LeanVerifier {
    /// A Lean verifier invoking `lean`, declared at the automation tier (Lean's
    /// `decide`/`rfl`/`omega` are deterministic decision procedures; a
    /// Mathlib-heavy proof can be re-tiered with [`LeanVerifier::at_tier`]).
    pub fn new() -> Self {
        Self { tier: Tier::Automation, lean_bin: "lean".into() }
    }

    /// Place this verifier at a specific tier on the ladder.
    pub fn at_tier(mut self, tier: Tier) -> Self {
        self.tier = tier;
        self
    }

    /// Use a specific `lean` binary (e.g. a `lake env lean` wrapper for a
    /// Mathlib project).
    pub fn with_bin(mut self, bin: impl Into<String>) -> Self {
        self.lean_bin = bin.into();
        self
    }

    /// Whether `lean` is reachable on this host.
    pub fn available(&self) -> bool {
        Command::new(&self.lean_bin)
            .arg("--version")
            .output()
            .map(|o| o.status.success())
            .unwrap_or(false)
    }

    fn targets_lean(goal: &ProofGoal) -> bool {
        goal.context.to_ascii_lowercase().contains("lean")
    }

    /// Run `lean` on `source`; returns `(typechecks, combined_output)`.
    fn run(&self, source: &str) -> std::io::Result<(bool, String)> {
        let path = std::env::temp_dir().join(format!(
            "proof-lean-{}-{}.lean",
            std::process::id(),
            LEAN_TMP_COUNTER.fetch_add(1, std::sync::atomic::Ordering::SeqCst)
        ));
        std::fs::write(&path, source)?;
        let result = Command::new(&self.lean_bin).arg(&path).output();
        let _ = std::fs::remove_file(&path);
        let out = result?;
        let mut combined = String::from_utf8_lossy(&out.stderr).into_owned();
        combined.push_str(&String::from_utf8_lossy(&out.stdout));
        // A real proof: clean exit, no error, and no `sorry` escape hatch.
        let ok = out.status.success()
            && !combined.contains("error:")
            && !combined.contains("sorry");
        Ok((ok, combined))
    }
}

impl Solver for LeanVerifier {
    fn tier(&self) -> Tier {
        self.tier
    }

    fn attempt(&self, goal: &ProofGoal) -> Attempt {
        // Not a Lean-dialect goal → this rung is inapplicable.
        if !Self::targets_lean(goal) {
            return Attempt {
                tier: self.tier,
                verdict: Verdict::Unproved,
                energy: Energy::estimate_tier(self.tier),
            };
        }
        let started = Instant::now();
        let verdict = match self.run(&goal.statement) {
            Ok((true, _)) => Verdict::Proved {
                artifact: ContentId::of_bytes(goal.statement.as_bytes()),
            },
            Ok((false, out)) => {
                // `decide` deciding the proposition false is a refutation, not a
                // mere failed proof — a decision the cascade must not escalate.
                if out.contains("proved that the proposition") && out.contains("is false") {
                    let witness = out.lines().find(|l| l.contains("error:")).unwrap_or("").trim();
                    Verdict::Refuted { counter_model: witness.to_string() }
                } else {
                    Verdict::Unproved
                }
            }
            // `lean` missing or a spawn failure: this rung simply didn't close it.
            Err(_) => Verdict::Unproved,
        };
        Attempt {
            tier: self.tier,
            verdict,
            energy: Energy::estimator(ns_to_uj(started.elapsed().as_nanos())),
        }
    }
}

// ── Two families of ladder, and why they must not be mixed ──────────────
//
// A ladder's verdict is only as sound as its weakest rung, because the router
// escalates until something says `Proved` and then stops. Put a fabricating
// stand-in below a real rung and the ladder proves *everything*: the real rungs
// decline, the stand-in obliges, and the cascade reports success.
//
// That is not hypothetical — it shipped twice. The first instance was a
// refutation escalated into a proof (fixed by `Verdict::Refuted` halting the
// router). The second was this one: with `z3` absent, `Z3Smt` returned
// `Unproved`, the router escalated, and `FrontierModel` — which proves any goal
// unconditionally — closed the goal at T3. Every goal on a machine without `z3`
// came back proved, at ~50 J of imaginary energy.
//
// So the families are kept apart by construction and checked by
// `ladder_is_sound`:
//
//   * **real** — no rung is a reference stand-in. Exhausting the ladder
//     yields `Unproved`, which is the honest answer to "nothing here could
//     decide this". An absent tool must produce a weaker claim, never a
//     stronger one.
//   * **reference** — stand-ins that gate on `GoalKind`. Total by design, which
//     is what makes routing and receipt vectors deterministic. Sound as a
//     fixture, never as evidence.

/// The pure stand-in ladder, cheapest-first — every rung a `GoalKind`-gated
/// model, used by conformance to exercise routing deterministically.
///
/// **Fixture only.** No rung here checks anything: `Proved` carries a hash of
/// the goal restated, and [`FrontierModel`] closes *any* goal. Use it to pin
/// routing and receipt encoding, never to decide whether something is true.
pub fn reference_ladder() -> Vec<Box<dyn Solver>> {
    vec![
        Box::new(Automation),
        Box::new(Smt),
        Box::new(SmallModel),
        Box::new(FrontierModel),
    ]
}

/// The reference ladder with a real propositional decider at T0.
///
/// **Fixture only**, like [`reference_ladder`]: T0 is real, but the rungs above
/// it are stand-ins, so the ladder is still total and its verdict still is not
/// evidence. Renamed from `real_t0_ladder` — a mixed ladder under a `real_`
/// name is exactly the confusion that produced the fabrication bug.
pub fn reference_ladder_with_real_t0() -> Vec<Box<dyn Solver>> {
    vec![
        Box::new(Propositional),
        Box::new(Smt),
        Box::new(SmallModel),
        Box::new(FrontierModel),
    ]
}

/// The real ladder: the propositional decider (T0) and `z3` (T1) — every rung a
/// decision procedure, so a `Proved` verdict is backed by something a verifier
/// would accept.
///
/// There is no T2/T3 rung because no real one exists yet. When a model backend
/// lands behind the same [`Solver`] trait and can emit a checkable artifact, it
/// joins here; until then the ladder ends at T1 and unreachable goals come back
/// `Unproved`. **A missing rung must never be papered over with a stand-in** —
/// that converts "we could not decide" into "we decided", which is the one
/// error a proof system may not make.
///
/// With `z3` absent this ladder decides only propositional goals and returns
/// `Unproved` for the rest. That is the intended behaviour: see
/// [`z3_available`] to report the reduced reach honestly rather than hide it.
pub fn real_ladder() -> Vec<Box<dyn Solver>> {
    vec![Box::new(Propositional), Box::new(Z3Smt)]
}

/// Like [`real_ladder`] but with `z3` kept resident at T1, on its
/// operator's declaration (`self_contained`) or without it
/// ([`Z3Server::declared_self_contained`]): undeclared, no T1 decision is
/// sealed as a hardware reading.
pub fn resident_z3_ladder(self_contained: bool) -> Vec<Box<dyn Solver>> {
    vec![
        Box::new(Propositional),
        Box::new(Z3Server::new().declared_self_contained(self_contained)),
    ]
}

/// Whether a working `z3` is on PATH — lets callers/tests adapt honestly.
pub fn z3_available() -> bool {
    Command::new("z3")
        .arg("--version")
        .stdout(Stdio::null())
        .stderr(Stdio::null())
        .status()
        .map(|s| s.success())
        .unwrap_or(false)
}

#[cfg(test)]
mod tests {
    use super::*;

    /// Every rung of a ladder that calls itself real must be a decision
    /// procedure. This is the structural guard: the fabrication bug was a
    /// stand-in sitting where the router could escalate into it, and a shape
    /// test catches that at compile-and-test time rather than in an audit.
    #[test]
    fn ladder_is_sound() {
        for (name, ladder) in [
            ("real_ladder", real_ladder()),
            ("resident_z3_ladder", resident_z3_ladder(false)),
            ("resident_z3_ladder declared", resident_z3_ladder(true)),
        ] {
            assert!(!ladder.is_empty(), "{name}: a real ladder needs a rung");
            for rung in &ladder {
                assert!(
                    !rung.is_reference_stub(),
                    "{name}: rung {:?} is not a decision procedure — a stand-in \
                     here lets the router escalate a failure into a fabricated proof",
                    rung.tier()
                );
            }
        }

        // `is_reference_stub` defaults to `false`, so a stand-in that forgets to
        // override it would pass the loop above unnoticed. Pin the exact tiers
        // too: adding any rung to a real ladder trips this even if the new rung
        // lies about what it is. Update these deliberately when a real T2/T3
        // backend actually lands.
        assert_eq!(
            real_ladder().iter().map(|r| r.tier()).collect::<Vec<_>>(),
            vec![Tier::Automation, Tier::Smt],
            "real_ladder membership changed — is the new rung a decision procedure?"
        );
        assert_eq!(
            resident_z3_ladder(false)
                .iter()
                .map(|r| r.tier())
                .collect::<Vec<_>>(),
            vec![Tier::Automation, Tier::Smt],
            "resident_z3_ladder membership changed — is the new rung a decision procedure?"
        );

        // And the fixture ladders are honestly declared as such, so the marker
        // means something in both directions.
        assert!(
            reference_ladder()
                .iter()
                .all(|r| r.is_reference_stub()),
            "reference_ladder must be entirely stand-ins"
        );
        assert!(
            reference_ladder_with_real_t0()
                .iter()
                .filter(|r| r.is_reference_stub())
                .count()
                == 3,
            "reference_ladder_with_real_t0 is one real rung under three stand-ins"
        );
    }

    /// The regression itself, driven through the real router.
    ///
    /// A goal no decision procedure can discharge must come back `Unproved`.
    /// Before the fix this returned **Proved, closed by `BigModel`, at ~50 J** —
    /// on any machine without `z3`, every goal did. The energy figure was as
    /// invented as the proof.
    ///
    /// Holds with or without `z3` on PATH: `z3` cannot parse prose, so it
    /// declines either way, which is what makes this a stable assertion rather
    /// than one that changes meaning with the runner image.
    #[test]
    fn ladder_never_fabricates_a_proof_when_a_rung_is_absent() {
        use proof_cascade::{ProofCache, Router};

        let unreachable = ProofGoal::new(
            "every even integer > 2 is the sum of two primes",
            "lean4",
            GoalKind::Hard,
        );

        let mut cache = ProofCache::default();
        let out = Router::new(real_ladder()).prove(&unreachable, &mut cache);

        assert!(
            !out.proved,
            "a goal no decision procedure decided came back proved, closed by {:?}",
            out.closed_by
        );
        assert!(
            out.closed_by.is_none(),
            "nothing may close a goal it did not decide (closed_by = {:?})",
            out.closed_by
        );
        assert!(
            !out.attempts.iter().any(|a| a.proved),
            "no rung may report success here"
        );
        // No model rung may even be on this ladder to be escalated into.
        assert!(
            !out.attempts
                .iter()
                .any(|a| matches!(a.tier, Tier::SmallModel | Tier::BigModel)),
            "a model stand-in ran on the real ladder"
        );
    }

    /// The reference ladder is *total* — it closes every goal, including the one
    /// above that no real solver can touch. That totality is exactly why it is
    /// useful for pinning routing determinism and exactly why it must never sit
    /// under a real rung. Kept as a test so the property is asserted rather than
    /// assumed by the ladder-family split.
    #[test]
    fn reference_ladder_is_total_which_is_why_it_is_fixture_only() {
        use proof_cascade::{ProofCache, Router};

        let unreachable = ProofGoal::new(
            "every even integer > 2 is the sum of two primes",
            "lean4",
            GoalKind::Hard,
        );
        let mut cache = ProofCache::default();
        let out = Router::new(reference_ladder()).prove(&unreachable, &mut cache);

        assert!(
            out.proved,
            "the stand-in ladder closes everything by design"
        );
        assert_eq!(out.closed_by, Some(Tier::BigModel));
    }

    #[test]
    fn each_rung_reaches_its_kind() {
        let triv = ProofGoal::new("x = x", "lean4", GoalKind::Trivial);
        assert!(Automation.attempt(&triv).verdict.is_proved());
        let dec = ProofGoal::new("decidable thing", "lean4", GoalKind::Decidable);
        assert!(!Automation.attempt(&dec).verdict.is_proved());
        assert!(Smt.attempt(&dec).verdict.is_proved());
        let gen = ProofGoal::new("needs search", "lean4", GoalKind::General);
        assert!(SmallModel.attempt(&gen).verdict.is_proved());
        let hard = ProofGoal::new("research conjecture", "lean4", GoalKind::Hard);
        assert!(FrontierModel.attempt(&hard).verdict.is_proved());
        assert_eq!(reference_ladder().len(), 4);
    }

    #[test]
    fn real_t0_proves_tautologies_and_refuses_the_rest() {
        let taut = ProofGoal::new("a | ~a", "prop", GoalKind::Trivial);
        let a = Propositional.attempt(&taut);
        assert!(a.verdict.is_proved());
        assert!(a.energy.measured_uj.is_none()); // Estimator: no hardware shunt
        assert!(a.energy.uj() >= 1);
        assert!(!Propositional
            .attempt(&ProofGoal::new("a -> b", "prop", GoalKind::Trivial))
            .verdict
            .is_proved());
        assert!(!Propositional
            .attempt(&ProofGoal::new("∀ n, n+0 = n", "lean4", GoalKind::General))
            .verdict
            .is_proved());
        assert_eq!(reference_ladder_with_real_t0().len(), 4);
    }

    /// Every rung that prices its attempt by wall time × the crate's default
    /// power grades the figure `Estimator`, never `ModelBased`: no host
    /// calibrated that power, so the figure is a constant scaled by time, an
    /// estimate. Holds whether or not the work decided anything, and whether
    /// or not the tool was there to run.
    #[test]
    fn a_wall_time_figure_at_the_default_power_is_an_estimate() {
        let e = wall_time_estimate(4_000_000);
        assert_eq!(e, Energy::estimator(60_000), "4 ms at the default 15 W is 60,000 µJ, an estimate");
        assert_eq!(wall_time_estimate(0), Energy::estimator(1), "a figure for work that ran is at least 1 µJ");
        assert_eq!(ns_to_uj(1_000_000_000), DEFAULT_ACTIVE_MILLIWATTS * 1_000, "1 s at the default power, in µJ");

        let smt = ProofGoal::new("(declare-const x Int)\n(assert (not (> x 0)))", "smt2", GoalKind::Decidable);
        let lean = ProofGoal::new("example : 1 + 1 = 2 := by decide", "lean4", GoalKind::Arithmetic);
        let absent_lean = LeanVerifier::new().with_bin("/nonexistent/proof-solvers-test/lean");
        for (name, a) in [
            ("T0 proved", Propositional.attempt(&ProofGoal::new("a | ~a", "prop", GoalKind::Trivial))),
            ("T0 refused", Propositional.attempt(&ProofGoal::new("a -> b", "prop", GoalKind::Trivial))),
            ("one-shot z3", Z3Smt.attempt(&smt)),
            ("lean absent", absent_lean.attempt(&lean)),
        ] {
            assert_eq!(a.energy.provenance, proof_schema::Provenance::Estimator, "{name}: {:?}", a.energy);
            assert_eq!(a.energy.measured_uj, None, "{name}: {:?}", a.energy);
            a.energy.check_provenance().unwrap();
        }
    }

    #[test]
    fn z3_decides_real_smt_goals_when_available() {
        let valid = ProofGoal::new(
            "(declare-const x Int)\n(assert (not (=> (> x 0) (>= x 0))))",
            "smt2",
            GoalKind::Decidable,
        );
        let a = Z3Smt.attempt(&valid);
        assert_eq!(real_ladder().len(), 2); // decision procedures only
        if z3_available() {
            assert!(a.verdict.is_proved());
            assert!(a.energy.uj() >= 1);
            let not_thm = ProofGoal::new(
                "(declare-const x Int)\n(assert (not (> x 0)))",
                "smt2",
                GoalKind::Decidable,
            );
            assert!(!Z3Smt.attempt(&not_thm).verdict.is_proved());
        } else {
            assert!(!a.verdict.is_proved());
        }
    }

    #[test]
    fn lean_verifies_proves_refutes_and_skips_non_lean() {
        let lean = LeanVerifier::new();
        // A non-Lean goal is inapplicable regardless of toolchain.
        let smt = ProofGoal::new("(assert true)", "smt2", GoalKind::Decidable);
        assert!(!lean.attempt(&smt).verdict.is_proved());

        if !lean.available() {
            eprintln!("lean not installed — skipping the live verification smoke");
            return;
        }
        // A real, checkable Lean proof → Proved (Lean is the verifier).
        let ok = ProofGoal::new("example : 1 + 1 = 2 := by decide", "lean4", GoalKind::Arithmetic);
        let a = lean.attempt(&ok);
        assert!(a.verdict.is_proved(), "valid lean proof must verify");
        assert!(a.energy.uj() >= 1);

        // `decide` deciding the proposition false → Refuted (a decision).
        let f = ProofGoal::new("example : 1 + 1 = 3 := by decide", "lean4", GoalKind::Arithmetic);
        assert!(lean.attempt(&f).verdict.is_refuted(), "decide-false must refute");

        // A failing-but-not-decided-false proof → Unproved.
        let u = ProofGoal::new("example : 2 + 2 = 5 := rfl", "lean4", GoalKind::Arithmetic);
        assert_eq!(lean.attempt(&u).verdict, Verdict::Unproved);

        // The `sorry` escape hatch must NOT count as proved.
        let s = ProofGoal::new("example (p : Prop) : p := by sorry", "lean4", GoalKind::General);
        assert!(!lean.attempt(&s).verdict.is_proved(), "sorry is not a proof");
    }

    #[test]
    fn resident_z3_decides_many_goals_on_one_session() {
        let server = Z3Server::new();
        let thm = ProofGoal::new(
            "(declare-const x Int)\n(assert (not (=> (> x 0) (>= x 0))))",
            "smt2",
            GoalKind::Decidable,
        );
        let comm = ProofGoal::new(
            "(declare-const a Int)(declare-const b Int)\n(assert (not (= (+ a b) (+ b a))))",
            "smt2",
            GoalKind::Decidable,
        );
        let prose = ProofGoal::new("∃ continuous f with property P", "lean4", GoalKind::General);
        assert!(!server.attempt(&prose).verdict.is_proved());
        if z3_available() {
            assert!(server.attempt(&thm).verdict.is_proved());
            assert!(server.attempt(&comm).verdict.is_proved());
            assert!(server.attempt(&thm).verdict.is_proved()); // still healthy after prose
        }
        assert_eq!(resident_z3_ladder(false).len(), 2); // decision procedures only
        assert!(admit("(assert (> x 0))").is_some());
        assert!(admit("∃ continuous f").is_none());
        assert!(admit("(unbalanced").is_none());
    }

    fn smt(s: &str) -> ProofGoal {
        ProofGoal::new(s, "smt2", GoalKind::Decidable)
    }

    /// Valid, asserted negated: `unsat`, so proved.
    const VALID_X: &str = "(declare-const x Int)(assert (not (= x x)))";
    const VALID_BV: &str = "(declare-const x (_ BitVec 32))\n\
                            (assert (not (= (bvmul x #x00000003) (bvadd x (bvadd x x)))))";
    /// FALSE (`y > 0` for every `y`), asserted negated: `sat`, so refuted.
    const FALSE_Y: &str = "(declare-const y Int)(assert (not (> y 0)))";

    /// `f` on a thread of its own, its value if it returns within `limit`. A
    /// goal that wedges the resident session would hang the test run, so a
    /// hang is a failure here rather than a stuck suite.
    fn within<T: Send + 'static>(limit: Duration, f: impl FnOnce() -> T + Send + 'static) -> T {
        let (tx, rx) = std::sync::mpsc::channel();
        std::thread::spawn(move || {
            let _ = tx.send(f());
        });
        rx.recv_timeout(limit).expect("the attempt did not return: the z3 session is wedged")
    }

    /// A goal that prints the session's end marker must not shift every
    /// later verdict by one. With a fixed marker it did: the FALSE claim
    /// after it was read off the previous goal's `unsat` and sealed proved.
    /// A marker-shaped statement is refused (undecided), and the goals
    /// after it are decided on their own output.
    #[test]
    fn an_injected_end_marker_never_desyncs_the_resident_session() {
        if !z3_available() {
            eprintln!("z3 not installed: no resident session to desync");
            return;
        }
        let server = Z3Server::new();
        let a = server.attempt(&smt(&format!("(echo \"@@END@@\"){VALID_X}")));
        let b = server.attempt(&smt(FALSE_Y));
        let c = server.attempt(&smt(VALID_X));
        assert!(!b.verdict.is_proved(), "a FALSE claim came back proved: {:?}", b.verdict);
        assert!(b.verdict.is_refuted(), "the false claim is refuted on its own output: {:?}", b.verdict);
        assert!(c.verdict.is_proved(), "{:?}", c.verdict);
        assert_eq!(a.verdict, Verdict::Unproved, "a marker-shaped goal is refused, never decided");
    }

    /// Below the refusal: the marker is fresh and unpredictable per goal, so
    /// even a script that prints the old fixed marker (or anything else)
    /// cannot end a read early. Driven on the session itself.
    #[test]
    fn the_session_marker_is_fresh_per_goal() {
        if !z3_available() {
            eprintln!("z3 not installed: no session");
            return;
        }
        let mut s = Z3Session::spawn(&resolve_z3().expect("z3 on PATH"), GOAL_TIMEOUT).expect("a z3 session");
        let injected = format!("(echo \"@@END@@\")(echo \"unsat\"){FALSE_Y}");
        assert_eq!(s.decide(&injected), Ok(Answer::Verdict(CheckSat::Sat)));
        assert_eq!(s.decide(FALSE_Y), Ok(Answer::Verdict(CheckSat::Sat)));
        assert_eq!(s.decide(VALID_X), Ok(Answer::Verdict(CheckSat::Unsat)));
        assert_ne!(end_marker(), end_marker());
        assert!(end_marker().starts_with(END_MARKER_PREFIX));
    }

    /// A goal can print a verdict-shaped line itself. The one-shot rung read
    /// the FIRST such line, so `(echo "unsat")` before a false claim proved
    /// it. The answer is the line this crate's own `(check-sat)` printed,
    /// just before the end marker, on both rungs.
    #[test]
    fn an_echoed_verdict_is_never_read_as_the_answer() {
        if !z3_available() {
            eprintln!("z3 not installed");
            return;
        }
        let spoof = smt(&format!("(echo \"unsat\"){FALSE_Y}"));
        let one_shot = Z3Smt.attempt(&spoof);
        assert!(!one_shot.verdict.is_proved(), "one-shot proved a FALSE claim: {:?}", one_shot.verdict);
        let resident = Z3Server::new().attempt(&spoof);
        assert!(!resident.verdict.is_proved(), "resident proved a FALSE claim: {:?}", resident.verdict);
        // And a goal ending in its own `(check-sat)` and more output.
        let tail = smt(&format!("{FALSE_Y}(check-sat)(echo \"unsat\")"));
        assert!(!Z3Smt.attempt(&tail).verdict.is_proved());
        assert!(!Z3Server::new().attempt(&tail).verdict.is_proved());
    }

    /// z3 reports an error and carries on, answering `(check-sat)` over the
    /// part that parsed. One-shot read that as undecided; the resident rung
    /// read the `sat` of the partial stack and came back REFUTED with a
    /// model. An error anywhere is undecided on both rungs.
    #[test]
    fn a_goal_that_errors_is_undecided_on_both_rungs() {
        if !z3_available() {
            eprintln!("z3 not installed");
            return;
        }
        let err = smt("(declare-const x Int)(assert (> x 0))(assert (bogus x))");
        assert_eq!(Z3Smt.attempt(&err).verdict, Verdict::Unproved);
        let server = Z3Server::new();
        assert_eq!(server.attempt(&err).verdict, Verdict::Unproved);
        // The session goes on deciding after it.
        assert!(server.attempt(&smt(VALID_BV)).verdict.is_proved());
        assert!(server.attempt(&smt(FALSE_Y)).verdict.is_refuted());
    }

    /// z3 keeps `set-option` across `(reset)`: a goal's options reached
    /// every later goal on the resident session (`:rlimit 1` turned the next
    /// valid claim `unknown`). A goal that sets an option is decided, and
    /// its session is retired after it.
    #[test]
    fn a_goal_option_never_reaches_the_next_goal() {
        if !z3_available() {
            eprintln!("z3 not installed");
            return;
        }
        let server = Z3Server::new();
        let before = server.pid();
        let _ = server.attempt(&smt(&format!("(set-option :rlimit 1){VALID_X}")));
        assert_ne!(server.pid(), before, "the session that ran a set-option goal was kept");
        let next = server.attempt(&smt(VALID_BV));
        assert!(next.verdict.is_proved(), "the previous goal's option reached this one: {:?}", next.verdict);
    }

    /// A session that breaks (here: its `z3` killed) is replaced, not reused:
    /// the attempt that found it broken is undecided, the next is decided on
    /// a fresh `z3`.
    #[test]
    fn a_broken_session_is_replaced() {
        if !z3_available() {
            eprintln!("z3 not installed");
            return;
        }
        let server = Z3Server::new();
        let pid = server.pid().expect("a resident z3");
        let killed = Command::new("kill").args(["-9", &pid.to_string()]).status().expect("kill");
        assert!(killed.success());
        std::thread::sleep(Duration::from_millis(50));
        assert_eq!(server.attempt(&smt(VALID_X)).verdict, Verdict::Unproved);
        assert_ne!(server.pid(), Some(pid), "the broken session was kept");
        assert!(server.attempt(&smt(VALID_X)).verdict.is_proved());
    }

    /// A goal `z3` cannot decide in seconds: two 32-bit factors of a 64-bit
    /// semiprime (3220908563 × 3999525389). Satisfiable, so it never proves
    /// anything; on the build host `z3` gives up on it at a 3 s limit and has
    /// not decided it at 20 s.
    const HARD: &str = "(declare-const x (_ BitVec 64))(declare-const y (_ BitVec 64))\
                        (assert (bvugt x #x0000000000000001))(assert (bvugt y #x0000000000000001))\
                        (assert (bvult x #x0000000100000000))(assert (bvult y #x0000000100000000))\
                        (assert (= (bvmul x y) #xb2c66ec4438f80f7))";
    /// A goal can lift `z3`'s own limit for itself: with this in front, [`HARD`]
    /// runs until something stops it.
    const NO_LIMIT: &str = "(set-option :timeout 4294967295)";
    /// The goal limit the tests run at.
    const SHORT: Duration = Duration::from_millis(300);

    /// Whether `pid` names a live process.
    fn alive(pid: u32) -> bool {
        Command::new("kill").args(["-0", &pid.to_string()]).stderr(Stdio::null()).status().is_ok_and(|s| s.success())
    }

    /// `z3`'s soft limit: a goal it cannot decide in time answers `unknown`
    /// — undecided, never proved — and the session goes on deciding.
    #[test]
    fn a_goal_past_its_limit_is_unknown_and_the_session_decides_on() {
        if !z3_available() {
            eprintln!("z3 not installed");
            return;
        }
        let (hard, after) = within(Duration::from_secs(60), || {
            let mut s = Z3Session::spawn(&resolve_z3().expect("z3 on PATH"), SHORT).expect("a z3 session");
            (s.decide(HARD), s.decide(VALID_X))
        });
        assert_eq!(hard, Ok(Answer::Verdict(CheckSat::Unknown)), "z3 gave up at the limit and said so");
        assert_eq!(after, Ok(Answer::Verdict(CheckSat::Unsat)));
    }

    /// A goal that lifts the soft limit for itself is cut off at the read
    /// deadline: the session is broken (the caller retires it) and its `z3`
    /// is gone once it is dropped. Without the deadline this read never
    /// returned, and held the resident session from every goal after it.
    #[test]
    fn a_goal_that_lifts_its_limit_is_cut_off_at_the_deadline() {
        if !z3_available() {
            eprintln!("z3 not installed");
            return;
        }
        let (answer, took, pid) = within(Duration::from_secs(60), || {
            let mut s = Z3Session::spawn(&resolve_z3().expect("z3 on PATH"), SHORT).expect("a z3 session");
            let pid = s.pid();
            let t = Instant::now();
            let answer = s.decide(&format!("{NO_LIMIT}{HARD}"));
            (answer, t.elapsed(), pid)
        });
        assert_eq!(answer, Err(Broken));
        assert!(took >= SHORT + GOAL_DEADLINE_GRACE, "cut off before its deadline: {took:?}");
        assert!(!alive(pid), "the z3 of a dropped session is still running");
    }

    /// The write is under the deadline too. `z3` reads its input as it gets
    /// to each command, so a goal running a `(check-sat)` of its own, with
    /// more than a pipe's worth after it, is not read past that check: a
    /// write on the calling thread waited on it for as long as it ran.
    #[test]
    fn a_goal_too_long_to_write_is_cut_off_at_the_deadline() {
        if !z3_available() {
            eprintln!("z3 not installed");
            return;
        }
        let goal = format!("{NO_LIMIT}{HARD}(check-sat){}", "(assert true)".repeat(1 << 15));
        let (answer, pid) = within(Duration::from_secs(60), move || {
            let mut s = Z3Session::spawn(&resolve_z3().expect("z3 on PATH"), SHORT).expect("a z3 session");
            let pid = s.pid();
            (s.decide(&goal), pid)
        });
        assert_eq!(answer, Err(Broken));
        assert!(!alive(pid), "the z3 of a dropped session is still running");
    }

    /// The one-shot `z3` is under the same deadline, on both ends, and is
    /// killed at it.
    #[test]
    fn a_one_shot_z3_is_killed_at_the_deadline() {
        if !z3_available() {
            eprintln!("z3 not installed");
            return;
        }
        for goal in [format!("{NO_LIMIT}{HARD}"), format!("{NO_LIMIT}{HARD}(check-sat){}", "(assert true)".repeat(1 << 15))] {
            let (out, took, pid) = within(Duration::from_secs(60), move || {
                let child = Command::new(resolve_z3().expect("z3 on PATH"))
                    .args(z3_args(SHORT))
                    .stdin(Stdio::piped())
                    .stdout(Stdio::piped())
                    .stderr(Stdio::null())
                    .spawn()
                    .expect("spawn z3");
                let pid = child.id();
                let t = Instant::now();
                let out = output_within(child, &framed(&goal, &end_marker()), SHORT + GOAL_DEADLINE_GRACE);
                (out, t.elapsed(), pid)
            });
            assert_eq!(out, None);
            assert!(took >= SHORT + GOAL_DEADLINE_GRACE, "cut off before its deadline: {took:?}");
            assert!(!alive(pid), "the one-shot z3 outlived its deadline");
        }
        // And within its limit it answers, as it always has.
        let out = run_one_shot(&framed(HARD, "@@END@@limit"), SHORT).expect("z3 answers at its soft limit");
        assert_eq!(reply_until(&mut out.lines(), "@@END@@limit").map(|r| r.answer()), Some(Answer::Verdict(CheckSat::Unknown)));
    }

    /// Through the server: an undecided goal is unproved, a goal past the
    /// deadline breaks its session, which is replaced, and the server goes
    /// on proving.
    #[test]
    fn the_server_keeps_its_goal_limit_across_sessions() {
        if !z3_available() {
            eprintln!("z3 not installed");
            return;
        }
        // Under the default limit, so that a session which lost the short one
        // (a 60 s HARD) fails here rather than passing slowly.
        let (unknown, kept, lifted, replaced, after) = within(GOAL_TIMEOUT - Duration::from_secs(15), || {
            let server = Z3Server::new().with_goal_timeout(SHORT);
            let first = server.pid();
            let unknown = server.attempt(&smt(HARD)).verdict;
            let kept = server.pid() == first;
            let lifted = server.attempt(&smt(&format!("{NO_LIMIT}{HARD}"))).verdict;
            let replaced = server.pid() != first;
            // The replacement keeps the limit: it gives up on HARD in time.
            let again = server.attempt(&smt(HARD)).verdict;
            assert_eq!(again, Verdict::Unproved);
            (unknown, kept, lifted, replaced, server.attempt(&smt(VALID_X)).verdict)
        });
        assert_eq!(unknown, Verdict::Unproved);
        assert!(kept, "an unknown is a clean answer: the session is kept");
        assert_eq!(lifted, Verdict::Unproved);
        assert!(replaced, "the session cut off at its deadline was kept");
        assert!(after.is_proved(), "{after:?}");
    }

    /// Goals that would wedge the session — leave a string or quoted symbol
    /// open (swallowing the marker), send z3's answers elsewhere, end z3,
    /// or read a file — are refused at once, and the session decides on.
    #[test]
    fn a_goal_that_would_wedge_the_session_is_refused_at_once() {
        if !z3_available() {
            eprintln!("z3 not installed");
            return;
        }
        let verdicts = within(Duration::from_secs(60), || {
            let server = Z3Server::new();
            let mut out = Vec::new();
            for wedge in [
                format!("{VALID_X}(echo \"x)"),
                format!("{VALID_X}(declare-const |a) Int)"),
                format!("(set-option :regular-output-channel \"/dev/null\"){VALID_X}"),
                format!("(|set-option| :diagnostic-output-channel \"/dev/null\"){VALID_X}"),
                format!("{VALID_X}(exit)"),
                format!("{VALID_X}(|exit|)"),
                format!("(include \"/dev/null\"){VALID_X}"),
            ] {
                out.push((wedge.clone(), server.attempt(&smt(&wedge)).verdict, Z3Smt.attempt(&smt(&wedge)).verdict));
            }
            out.push(("after".into(), server.attempt(&smt(VALID_X)).verdict, Verdict::Unproved));
            out
        });
        let (last, rest) = verdicts.split_last().expect("verdicts");
        for (goal, resident, one_shot) in rest {
            assert_eq!(resident, &Verdict::Unproved, "{goal}");
            assert_eq!(one_shot, &Verdict::Unproved, "{goal}");
        }
        assert!(last.1.is_proved(), "the session decides on after the refusals: {:?}", last.1);
    }

    /// The shape guard, case by case, without `z3`.
    #[test]
    fn the_shape_guard_admits_whole_commands_only() {
        let admitted = |s: &str| admit(s).is_some();
        // Whole commands, with parentheses inside strings, quoted symbols and
        // comments not counted, and `""` an escaped quote.
        assert!(admitted(VALID_X));
        assert!(admitted("(declare-const |a (b| Int)(assert (= |a (b| |a (b|))"));
        assert!(admitted("(echo \"(\")(echo \"say \"\"hi\"\" )\")"));
        assert!(admitted("; a comment ) with ( parens\n(assert true) ; trailing comment"));
        assert_eq!(admit("(set-option :rlimit 1)(assert true)"), Some(Admitted { sets_option: true }));
        assert_eq!(admit("(|set-option| :timeout 5)"), Some(Admitted { sets_option: true }));
        assert_eq!(admit(VALID_X), Some(Admitted { sets_option: false }));
        // Refused.
        for s in [
            "",
            "   ; only a comment",
            "∃ continuous f",
            "(assert true) stray",
            "\"top-level string\"",
            "(assert true))(",
            "(assert (> x 0)",
            "()",
            "((assert true))",
            "(echo \"x)",
            "(declare-const |a) Int)",
            "(echo \"@@END@@\")",
            "(declare-const @@END@@x Int)",
            "(exit)",
            "(|exit|)",
            "(include \"goal.smt2\")",
            "(set-option :regular-output-channel \"/dev/null\")",
            "(set-option ; sneaky\n :diagnostic-output-channel \"x\")",
        ] {
            assert!(!admitted(s), "admitted {s:?}");
        }
    }

    /// The answer is the line just before the marker, and only when no
    /// line of the output is an error.
    #[test]
    fn the_answer_is_the_line_before_the_marker_with_no_error() {
        let answer = |lines: &[&str]| {
            let mut r = Reply::default();
            for l in lines {
                r.line(l);
            }
            r.answer()
        };
        assert_eq!(answer(&["unsat"]), Answer::Verdict(CheckSat::Unsat));
        assert_eq!(answer(&["unsat", "sat\n"]), Answer::Verdict(CheckSat::Sat));
        assert_eq!(answer(&["sat", "unknown"]), Answer::Verdict(CheckSat::Unknown));
        assert_eq!(answer(&["unsat", "x"]), Answer::Undecided, "a verdict before other output is the goal's");
        assert_eq!(answer(&[]), Answer::Undecided);
        assert_eq!(answer(&["(error \"line 1: unknown constant\")", "sat"]), Answer::Undecided);
        assert_eq!(answer(&["unsat", "(error \"oops\")", "unsat"]), Answer::Undecided);
    }

    /// A reading of the resident tree, as the meter would give it.
    fn reading(cpu_nj: u64, gaps: Vec<TreeGap>) -> TreeReading {
        TreeReading {
            cpu_uj: cpu_nj.div_ceil(1_000),
            cpu_nj,
            processes: 1,
            pids: vec![4242],
            wall: Duration::from_millis(3),
            gaps,
        }
    }

    /// The one case a Z3Server attempt is a hardware reading: a span over a
    /// decision that ran entirely in the resident tree, with nothing seen
    /// missing. Its figure is the reading's nanojoules rounded UP to the
    /// attempt's microjoule, so a reading is never sealed as a measured zero.
    #[test]
    fn a_whole_reading_of_a_resident_decision_is_hwshunt_rounded_up() {
        for (nj, uj) in [(2_345_001, 2_346), (2_345_000, 2_345), (1, 1), (999, 1)] {
            let r: Result<TreeReading, TreeError> = Ok(reading(nj, Vec::new()));
            let (e, because) = grade_attempt(Some(&r), true, true, false, 77);
            assert_eq!(e, Energy::measured(uj), "{nj} nJ");
            assert!(because.is_empty(), "{because:?}");
            assert!(e.check_provenance().is_ok());
        }
    }

    /// Every gap the meter can report grades the attempt down to the estimate,
    /// and the reading is never sealed: Energy has no coverage field, so a
    /// partial reading as `HwShunt` would claim the whole decision. This
    /// includes the gap that can put energy from BEFORE the span into the
    /// figure (`Unsettled` at the start), and the GPU and Neural Engine gaps
    /// a CPU reading cannot cover.
    #[test]
    fn a_reading_with_any_gap_keeps_the_estimate() {
        use sandbox_meter::SpanEnd;
        let gaps = [
            TreeGap::Unreadable { pid: 7, errno: 1, end: SpanEnd::Stop },
            TreeGap::Unlisted { pid: 7, errno: 1, end: SpanEnd::Start },
            TreeGap::Unsettled { pid: 4242, end: SpanEnd::Start },
            TreeGap::Unsettled { pid: 4242, end: SpanEnd::Stop },
            TreeGap::Changing { end: SpanEnd::Stop },
            TreeGap::PredatesSpan { pid: 7 },
            TreeGap::Gone { pid: 7 },
            TreeGap::EnergyWentBack { pid: 4242 },
            TreeGap::ReapedDescendant { pid: 4242, cpu: Duration::from_millis(2) },
            TreeGap::Exited { pid: 4242 },
            TreeGap::Gpu { ns: 5_000 },
            TreeGap::GpuUnknown { pid: None },
            TreeGap::GpuUnknown { pid: Some(4242) },
            TreeGap::NeuralEngine { pid: 4242, bytes: 1 << 20 },
        ];
        for gap in gaps {
            let r: Result<TreeReading, TreeError> = Ok(reading(5_000_000, vec![gap.clone()]));
            let (e, because) = grade_attempt(Some(&r), true, true, false, 77);
            assert_eq!(e, Energy::estimator(77), "{gap:?} was sealed as the reading");
            assert_eq!(because, vec![Modelled::Gaps(vec![gap])]);
        }
    }

    /// No reading, no meter, nothing run: the estimate, each with its
    /// reason. And a refuted goal, whose counter-model a one-shot `z3`
    /// fetched outside the resident tree, keeps the estimate for the whole
    /// attempt even when the resident decision's reading was whole: the
    /// one-shot run is in no span, and a reading of the decision alone
    /// sealed as `HwShunt` would claim the attempt.
    #[test]
    fn an_attempt_with_no_whole_reading_of_all_its_work_keeps_the_estimate() {
        let gone: Result<TreeReading, TreeError> = Err(TreeError::RootGone { pid: 4242 });
        let (e, because) = grade_attempt(Some(&gone), true, true, false, 12);
        assert_eq!((e, because), (Energy::estimator(12), vec![Modelled::NoReading(TreeError::RootGone { pid: 4242 })]));

        let (e, because) = grade_attempt(None, true, true, false, 12);
        assert_eq!((e, because), (Energy::estimator(12), vec![Modelled::NoTreeMeter]));

        let (e, because) = grade_attempt(None, false, true, false, 0);
        assert_eq!((e, because), (Energy::estimator(1), vec![Modelled::NotRun]), "the estimate is at least 1 µJ");

        let whole: Result<TreeReading, TreeError> = Ok(reading(3_000_000, Vec::new()));
        let (e, because) = grade_attempt(Some(&whole), true, true, true, 900);
        assert_eq!((e, because), (Energy::estimator(900), vec![Modelled::CounterModelOutsideTree]));

        // Both reasons, when both hold.
        let gapped: Result<TreeReading, TreeError> = Ok(reading(3_000_000, vec![TreeGap::Gone { pid: 9 }]));
        let (e, because) = grade_attempt(Some(&gapped), true, true, true, 900);
        assert_eq!(e, Energy::estimator(900));
        assert_eq!(because, vec![Modelled::Gaps(vec![TreeGap::Gone { pid: 9 }]), Modelled::CounterModelOutsideTree]);
    }

    /// Without the operator's declaration a reading — even a whole one — is
    /// never sealed: the tree cannot show work its `z3` hands elsewhere. The
    /// reason rides beside any other; with no reading there is nothing the
    /// declaration would change, and it is not given as a reason.
    #[test]
    fn an_undeclared_z3_keeps_the_estimate_for_any_reading() {
        let whole: Result<TreeReading, TreeError> = Ok(reading(5_000_000, Vec::new()));
        let (e, because) = grade_attempt(Some(&whole), true, false, false, 77);
        assert_eq!((e, because), (Energy::estimator(77), vec![Modelled::NotDeclaredSelfContained]));

        let gapped: Result<TreeReading, TreeError> = Ok(reading(5_000_000, vec![TreeGap::Gone { pid: 9 }]));
        let (e, because) = grade_attempt(Some(&gapped), true, false, true, 77);
        assert_eq!(e, Energy::estimator(77));
        assert_eq!(
            because,
            vec![
                Modelled::Gaps(vec![TreeGap::Gone { pid: 9 }]),
                Modelled::NotDeclaredSelfContained,
                Modelled::CounterModelOutsideTree
            ]
        );

        let gone: Result<TreeReading, TreeError> = Err(TreeError::RootGone { pid: 4242 });
        assert_eq!(grade_attempt(Some(&gone), true, false, false, 12).1, vec![Modelled::NoReading(TreeError::RootGone { pid: 4242 })]);
        assert_eq!(grade_attempt(None, true, false, false, 12).1, vec![Modelled::NoTreeMeter]);
    }

    /// The account names the binary the goal was written to: absolute,
    /// symlinks resolved, and the one a spawn by name finds on `PATH` (the
    /// shell's own lookup is the oracle). The default server is undeclared.
    #[cfg(unix)]
    #[test]
    fn the_account_names_the_z3_binary_that_ran() {
        if !z3_available() {
            eprintln!("z3 not installed");
            return;
        }
        let server = Z3Server::new();
        assert!(server.attempt(&smt(VALID_X)).verdict.is_proved());
        let acct = server.last_account().expect("an account");
        let z3 = acct.z3.expect("the account names the z3 it ran");
        let shell = Command::new("sh").args(["-c", "command -v z3"]).output().expect("sh");
        let found = PathBuf::from(String::from_utf8_lossy(&shell.stdout).trim()).canonicalize().expect("canonical");
        assert!(z3.is_absolute(), "{z3:?}");
        assert_eq!(z3, found);
        if acct.reading.as_ref().is_some_and(Result::is_ok) {
            assert!(acct.modelled_because.contains(&Modelled::NotDeclaredSelfContained), "{:?}", acct.modelled_because);
        }
        // A goal refused before any session is reached names none.
        let _ = server.attempt(&smt("(exit)"));
        assert_eq!(server.last_account().expect("an account").z3, None);
    }

    /// Off macOS there is no per-process energy counter, so no tree meter:
    /// every attempt that reaches `z3` keeps the estimate and says why.
    #[cfg(not(target_os = "macos"))]
    #[test]
    fn off_macos_a_resident_decision_keeps_the_estimate_and_says_why() {
        // Declared, so the one reason is the missing meter.
        let server = Z3Server::new().declared_self_contained(true);
        assert!(!server.is_tree_metered());
        if !z3_available() {
            eprintln!("z3 not installed: the resident session is absent, nothing to decide");
            return;
        }
        let thm = ProofGoal::new("(declare-const x Int)\n(assert (not (=> (> x 0) (>= x 0))))", "smt2", GoalKind::Decidable);
        let a = server.attempt(&thm);
        assert!(a.verdict.is_proved());
        let acct = server.last_account().expect("an account of the attempt");
        eprintln!("z3 resident (no tree meter): {acct:?}");
        assert_eq!(a.energy, Energy::estimator(acct.modelled_uj));
        assert_eq!(acct.modelled_because, vec![Modelled::NoTreeMeter]);
        assert_eq!(acct.reading, None);
    }
}