tessellate-core 0.3.0

//! Portable SMT-LIB queries and an opt-in external solver boundary.
//!
//! Exporting does not execute a solver. [`CommandSmtSolver`] is a separate,
//! explicitly constructed adapter that invokes one executable directly (never
//! through a shell), bounds its running time and output, and supports either a
//! strict status-only response or a SAT model that Tess independently replays.

use crate::CompiledProgram;
use crate::analysis::{
    Counterexample, CounterexampleKind, replay_invariant_violation, replay_invariant_witness,
};
use crate::ast::InvariantQuantifier;
use crate::compiler::normalize_name;
use crate::engine::Input;
use crate::source::Span;
use crate::value::Value;
use rust_decimal::Decimal;
use serde::{Deserialize, Serialize};
use std::collections::{BTreeMap, BTreeSet};
use std::error::Error;
use std::ffi::OsString;
use std::fmt;
use std::io::{self, Read, Write};
use std::path::{Path, PathBuf};
use std::process::{Child, Command, Stdio};
use std::sync::mpsc::{self, Receiver};
use std::thread;
use std::time::{Duration, Instant};

/// Current SMT-LIB query contract, including existential witness queries.
pub const SMTLIB_QUERY_SCHEMA_VERSION: &str = "tess.smtlib-query/v2";
/// Current external assessment contract, including validated witnesses.
pub const EXTERNAL_SMT_ASSESSMENT_SCHEMA_VERSION: &str = "tess.external-smt-assessment/v2";
pub const DEFAULT_EXTERNAL_SOLVER_TIMEOUT: Duration = Duration::from_secs(5);
pub const DEFAULT_EXTERNAL_SOLVER_OUTPUT_LIMIT: usize = 64 * 1024;

/// A source location associated with an exported query or symbol.
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub struct SmtSourceLocation {
    pub file: String,
    pub span: Span,
    pub line: usize,
    pub column: usize,
}

/// The portable representation used for one Tess input field.
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
#[serde(tag = "kind", rename_all = "snake_case")]
pub enum SmtSymbolEncoding {
    Bool {
        symbol: String,
    },
    Int {
        symbol: String,
    },
    DecimalMantissaScale {
        mantissa_symbol: String,
        scale_symbol: String,
        canonical_scale: u32,
    },
    EnumIndex {
        symbol: String,
        type_name: String,
        variants: Vec<String>,
    },
}

/// A stable link from a generated SMT symbol to its Tess field.
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub struct SmtSymbol {
    pub binding: String,
    pub entity: String,
    pub field: String,
    pub encoding: SmtSymbolEncoding,
    pub source: SmtSourceLocation,
}

/// Metadata that makes an exported query self-describing.
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub struct SmtLibMetadata {
    pub schema_version: String,
    pub generator: String,
    pub generator_version: String,
    pub logic: String,
    /// The exact SAT target: `invariant_violation` for a universal `assert`, or
    /// `invariant_witness` for `assert some`.
    pub query: String,
}

/// A complete, deterministic SMT-LIB2 `check-sat` query.
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub struct SmtLibQuery {
    pub invariant: String,
    pub source: SmtSourceLocation,
    pub metadata: SmtLibMetadata,
    pub symbols: Vec<SmtSymbol>,
    pub script: String,
}

/// Why an assertion could not be exported.
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
#[serde(tag = "kind", rename_all = "snake_case")]
pub enum SmtLibExportError {
    UnknownInvariant { invariant: String },
    Unsupported { invariant: String, reason: String },
}

impl fmt::Display for SmtLibExportError {
    fn fmt(&self, formatter: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::UnknownInvariant { invariant } => {
                write!(formatter, "unknown assertion `{invariant}`")
            }
            Self::Unsupported { invariant, reason } => {
                write!(
                    formatter,
                    "assertion `{invariant}` cannot be exported: {reason}"
                )
            }
        }
    }
}

impl Error for SmtLibExportError {}

/// Export one compiled assertion as a portable SMT-LIB2 query.
///
/// The supported theory is intentionally the same exact Bool/Int/Decimal/enum
/// fragment used by Tess's embedded solver. Collections, recursive structures,
/// state traces, optional fields, and other unmodelled constructs return
/// [`SmtLibExportError::Unsupported`] instead of receiving an approximation.
///
/// # Errors
///
/// Returns [`SmtLibExportError::UnknownInvariant`] when the name is absent and
/// [`SmtLibExportError::Unsupported`] when the assertion is outside the exact
/// translation fragment.
pub fn export_invariant_smtlib(
    program: &CompiledProgram,
    invariant: &str,
) -> Result<SmtLibQuery, SmtLibExportError> {
    crate::solver::export_invariant_smtlib(program, invariant)
}

/// The only accepted first-order answer to an exported `check-sat` query.
#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum ExternalSolverStatus {
    /// The external process reported that the exported query target has an
    /// assignment. It is not trusted evidence until model import and replay
    /// validate it as either a counterexample or witness.
    Sat,
    /// The external process reported that the exported query target has no
    /// assignment. This remains advisory without an independently checked
    /// proof certificate.
    Unsat,
    /// The external process reported that it did not decide the query.
    Unknown,
}

/// A bounded raw external solver invocation result with no independent trust
/// claim. Use [`CommandSmtSolver::solve_and_replay`] to validate SAT evidence.
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub struct ExternalSolverResult {
    pub backend: String,
    pub status: ExternalSolverStatus,
    pub elapsed_ms: u128,
    /// Diagnostics written by a successful solver process. It is bounded by
    /// the adapter's configured output limit.
    pub stderr: String,
}

/// A scalar returned by `(get-value ...)` for the exported Bool/Int fragment.
///
/// Integers use canonical decimal strings so 96-bit Decimal mantissas remain
/// lossless in JSON implementations that cannot represent them as numbers.
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
#[serde(tag = "kind", rename_all = "snake_case")]
pub enum ExternalModelValue {
    Bool { value: bool },
    Integer { value: String },
}

/// One normalized model assignment, ordered according to the query's symbol
/// table rather than backend-specific model ordering.
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub struct ExternalModelAssignment {
    pub symbol: String,
    pub value: ExternalModelValue,
}

/// The strict, deterministic subset of an external SAT model that Tess can
/// import. Unknown, duplicate, and omitted symbols are rejected.
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub struct ExternalSolverModel {
    pub assignments: Vec<ExternalModelAssignment>,
}

/// Whether an external answer has evidence Tess can independently check.
#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum ExternalSolverTrust {
    /// A concrete violating or satisfying input was replayed through the Tess
    /// evaluator.
    TessReplayValidated,
    /// The answer is reported, but Tess has not independently proved it.
    Advisory,
}

/// The usable conclusion of an external solver assessment.
#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum ExternalSolverAssessmentStatus {
    CounterexampleValidated,
    WitnessValidated,
    SatRejected,
    UnsatAdvisory,
    Unknown,
}

/// A versioned external answer with an explicit trust boundary.
///
/// A validated counterexample or witness combined with
/// [`ExternalSolverTrust::TessReplayValidated`] is independently accepted by
/// Tess. `unsat` remains advisory until a future proof or certificate checker
/// verifies it.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct ExternalSolverAssessment {
    pub schema_version: String,
    pub backend: String,
    pub solver_status: ExternalSolverStatus,
    pub status: ExternalSolverAssessmentStatus,
    pub trust: ExternalSolverTrust,
    pub elapsed_ms: u128,
    pub stderr: String,
    #[serde(skip_serializing_if = "Option::is_none")]
    pub model: Option<ExternalSolverModel>,
    #[serde(skip_serializing_if = "Option::is_none")]
    pub counterexample: Option<Counterexample>,
    #[serde(skip_serializing_if = "Option::is_none")]
    pub reason: Option<String>,
}

impl ExternalSolverAssessment {
    /// Validate the structural trust contract of a serialized assessment.
    ///
    /// This checks the schema version, backend identity, status/trust pairing,
    /// required or forbidden evidence fields, and normalized model assignments.
    /// It does not authenticate where a deserialized DTO came from; callers must
    /// still obtain trusted assessments from [`CommandSmtSolver::solve_and_replay`]
    /// or another authenticated channel.
    ///
    /// # Errors
    ///
    /// Returns a deterministic explanation when fields form an impossible or
    /// internally inconsistent assessment state.
    pub fn validate_consistency(&self) -> Result<(), String> {
        if self.schema_version != EXTERNAL_SMT_ASSESSMENT_SCHEMA_VERSION {
            return Err(format!(
                "unsupported external SMT assessment schema `{}`",
                self.schema_version
            ));
        }
        if self.backend.trim().is_empty() {
            return Err("external SMT assessment backend must not be empty".into());
        }
        match self.status {
            ExternalSolverAssessmentStatus::CounterexampleValidated => {
                require_assessment_state(
                    self,
                    ExternalSolverStatus::Sat,
                    ExternalSolverTrust::TessReplayValidated,
                )?;
                let model = self.model.as_ref().ok_or_else(|| {
                    "a validated counterexample assessment requires a model".to_owned()
                })?;
                validate_external_model(model)?;
                let counterexample = self.counterexample.as_ref().ok_or_else(|| {
                    "a validated counterexample assessment requires a counterexample".to_owned()
                })?;
                if counterexample.kind == CounterexampleKind::Unknown {
                    return Err("an unknown replay cannot be independently validated".into());
                }
                if self.reason.is_some() {
                    return Err(
                        "a validated counterexample assessment must not contain a rejection reason"
                            .into(),
                    );
                }
            }
            ExternalSolverAssessmentStatus::WitnessValidated => {
                require_assessment_state(
                    self,
                    ExternalSolverStatus::Sat,
                    ExternalSolverTrust::TessReplayValidated,
                )?;
                let model = self
                    .model
                    .as_ref()
                    .ok_or_else(|| "a validated witness assessment requires a model".to_owned())?;
                validate_external_model(model)?;
                if self.counterexample.is_some() {
                    return Err(
                        "a validated witness assessment must not contain a counterexample".into(),
                    );
                }
                if self.reason.is_some() {
                    return Err(
                        "a validated witness assessment must not contain a rejection reason".into(),
                    );
                }
            }
            ExternalSolverAssessmentStatus::SatRejected => {
                require_assessment_state(
                    self,
                    ExternalSolverStatus::Sat,
                    ExternalSolverTrust::Advisory,
                )?;
                if let Some(model) = &self.model {
                    validate_external_model(model)?;
                }
                if self.counterexample.is_some() {
                    return Err(
                        "a rejected SAT assessment must not contain a counterexample".into(),
                    );
                }
                require_assessment_reason(self)?;
            }
            ExternalSolverAssessmentStatus::UnsatAdvisory => {
                require_assessment_state(
                    self,
                    ExternalSolverStatus::Unsat,
                    ExternalSolverTrust::Advisory,
                )?;
                require_advisory_without_evidence(self, "UNSAT")?;
            }
            ExternalSolverAssessmentStatus::Unknown => {
                require_assessment_state(
                    self,
                    ExternalSolverStatus::Unknown,
                    ExternalSolverTrust::Advisory,
                )?;
                require_advisory_without_evidence(self, "unknown")?;
            }
        }
        Ok(())
    }

    /// Return the counterexample only when the trust and status markers both
    /// say that Tess replay validated it and the complete DTO is coherent.
    #[must_use]
    pub fn accepted_counterexample(&self) -> Option<&Counterexample> {
        if self.validate_consistency().is_ok()
            && self.status == ExternalSolverAssessmentStatus::CounterexampleValidated
        {
            self.counterexample.as_ref()
        } else {
            None
        }
    }

    /// Return the normalized model only when Tess replay confirmed that it is
    /// a satisfying witness for an `assert some` declaration.
    #[must_use]
    pub fn accepted_witness_model(&self) -> Option<&ExternalSolverModel> {
        if self.validate_consistency().is_ok()
            && self.status == ExternalSolverAssessmentStatus::WitnessValidated
        {
            self.model.as_ref()
        } else {
            None
        }
    }

    #[must_use]
    pub fn independently_validated(&self) -> bool {
        matches!(
            self.status,
            ExternalSolverAssessmentStatus::CounterexampleValidated
                | ExternalSolverAssessmentStatus::WitnessValidated
        ) && self.validate_consistency().is_ok()
    }
}

fn require_assessment_state(
    assessment: &ExternalSolverAssessment,
    solver_status: ExternalSolverStatus,
    trust: ExternalSolverTrust,
) -> Result<(), String> {
    if assessment.solver_status != solver_status {
        return Err(format!(
            "assessment status `{:?}` requires solver status `{:?}`",
            assessment.status, solver_status
        ));
    }
    if assessment.trust != trust {
        return Err(format!(
            "assessment status `{:?}` requires trust `{:?}`",
            assessment.status, trust
        ));
    }
    Ok(())
}

fn require_assessment_reason(assessment: &ExternalSolverAssessment) -> Result<(), String> {
    if assessment
        .reason
        .as_deref()
        .is_none_or(|reason| reason.trim().is_empty())
    {
        return Err("an advisory external SMT assessment requires a non-empty reason".into());
    }
    Ok(())
}

fn require_advisory_without_evidence(
    assessment: &ExternalSolverAssessment,
    label: &str,
) -> Result<(), String> {
    if assessment.model.is_some() || assessment.counterexample.is_some() {
        return Err(format!(
            "an advisory {label} assessment must not contain model or counterexample evidence"
        ));
    }
    require_assessment_reason(assessment)
}

fn validate_external_model(model: &ExternalSolverModel) -> Result<(), String> {
    let mut symbols = BTreeSet::new();
    for assignment in &model.assignments {
        if !is_simple_smt_symbol(&assignment.symbol) {
            return Err(format!(
                "model assignment symbol `{}` is not a safe simple SMT-LIB symbol",
                assignment.symbol
            ));
        }
        if !symbols.insert(&assignment.symbol) {
            return Err(format!(
                "model assignment symbol `{}` is duplicated",
                assignment.symbol
            ));
        }
        if let ExternalModelValue::Integer { value } = &assignment.value {
            let integer = value.parse::<i128>().map_err(|_| {
                format!("model assignment integer `{value}` is out of range or invalid")
            })?;
            if integer.to_string() != *value {
                return Err(format!(
                    "model assignment integer `{value}` is not canonical decimal"
                ));
            }
        }
    }
    Ok(())
}

/// Failure at the process or protocol boundary.
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
#[serde(tag = "kind", rename_all = "snake_case")]
pub enum ExternalSolverError {
    InvalidConfiguration { reason: String },
    Spawn { executable: String, reason: String },
    Io { stream: String, reason: String },
    Timeout { timeout_ms: u128 },
    OutputLimitExceeded { stream: String, limit: usize },
    InvalidUtf8 { stream: String },
    UnsuccessfulExit { code: Option<i32>, stderr: String },
    InvalidStatus { stdout: String },
}

impl fmt::Display for ExternalSolverError {
    fn fmt(&self, formatter: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::InvalidConfiguration { reason } => {
                write!(formatter, "invalid external solver configuration: {reason}")
            }
            Self::Spawn { executable, reason } => {
                write!(formatter, "could not start `{executable}`: {reason}")
            }
            Self::Io { stream, reason } => {
                write!(formatter, "external solver {stream} failed: {reason}")
            }
            Self::Timeout { timeout_ms } => {
                write!(
                    formatter,
                    "external solver exceeded its {timeout_ms} ms timeout"
                )
            }
            Self::OutputLimitExceeded { stream, limit } => write!(
                formatter,
                "external solver {stream} exceeded the {limit}-byte limit"
            ),
            Self::InvalidUtf8 { stream } => {
                write!(formatter, "external solver {stream} was not UTF-8")
            }
            Self::UnsuccessfulExit { code, stderr } => {
                write!(formatter, "external solver exited with {code:?}: {stderr}")
            }
            Self::InvalidStatus { stdout } => write!(
                formatter,
                "external solver returned an invalid check-sat response: {stdout:?}"
            ),
        }
    }
}

impl Error for ExternalSolverError {}

/// An opt-in backend capable of deciding a portable SMT-LIB query.
pub trait SmtLibSolver {
    /// Run one query. Implementations must not interpret `sat` as a replayed
    /// Tess counterexample without independently importing and validating a
    /// model through the core evaluator.
    ///
    /// # Errors
    ///
    /// Returns a process-, resource-, or protocol-specific error without
    /// converting it into a satisfiability result.
    fn solve(&self, query: &SmtLibQuery) -> Result<ExternalSolverResult, ExternalSolverError>;
}

/// A direct-process SMT-LIB adapter with a wall-clock timeout and output cap.
///
/// Arguments are passed to the executable literally; no shell is involved.
/// The query is sent on stdin, and stdout must consist solely of `sat`, `unsat`,
/// or `unknown` plus surrounding ASCII whitespace.
#[derive(Clone, Debug)]
pub struct CommandSmtSolver {
    backend: String,
    executable: PathBuf,
    arguments: Vec<OsString>,
    timeout: Duration,
    output_limit: usize,
}

impl CommandSmtSolver {
    /// Construct an adapter using the documented five-second timeout and a
    /// 64-KiB cap for each output stream.
    ///
    /// # Errors
    ///
    /// Returns [`ExternalSolverError::InvalidConfiguration`] when the backend
    /// name or executable path is empty.
    pub fn new(
        backend: impl Into<String>,
        executable: impl Into<PathBuf>,
    ) -> Result<Self, ExternalSolverError> {
        let backend = backend.into();
        let executable = executable.into();
        if backend.trim().is_empty() {
            return Err(invalid_configuration("backend name must not be empty"));
        }
        if executable.as_os_str().is_empty() {
            return Err(invalid_configuration("executable path must not be empty"));
        }
        Ok(Self {
            backend,
            executable,
            arguments: Vec::new(),
            timeout: DEFAULT_EXTERNAL_SOLVER_TIMEOUT,
            output_limit: DEFAULT_EXTERNAL_SOLVER_OUTPUT_LIMIT,
        })
    }

    #[must_use]
    pub fn arg(mut self, argument: impl Into<OsString>) -> Self {
        self.arguments.push(argument.into());
        self
    }

    #[must_use]
    pub fn args<I, S>(mut self, arguments: I) -> Self
    where
        I: IntoIterator<Item = S>,
        S: Into<OsString>,
    {
        self.arguments.extend(arguments.into_iter().map(Into::into));
        self
    }

    /// Set a finite wall-clock deadline.
    ///
    /// # Errors
    ///
    /// Returns [`ExternalSolverError::InvalidConfiguration`] for a zero or
    /// platform-unrepresentable duration.
    pub fn with_timeout(mut self, timeout: Duration) -> Result<Self, ExternalSolverError> {
        if timeout.is_zero() {
            return Err(invalid_configuration("timeout must be greater than zero"));
        }
        if Instant::now().checked_add(timeout).is_none() {
            return Err(invalid_configuration(
                "timeout is too large for this platform",
            ));
        }
        self.timeout = timeout;
        Ok(self)
    }

    /// Set the maximum retained bytes for each output stream.
    ///
    /// # Errors
    ///
    /// Returns [`ExternalSolverError::InvalidConfiguration`] when `limit` is
    /// zero.
    pub fn with_output_limit(mut self, limit: usize) -> Result<Self, ExternalSolverError> {
        if limit == 0 {
            return Err(invalid_configuration(
                "output limit must be greater than zero",
            ));
        }
        self.output_limit = limit;
        Ok(self)
    }

    #[must_use]
    pub fn backend(&self) -> &str {
        &self.backend
    }

    #[must_use]
    pub fn executable(&self) -> &Path {
        &self.executable
    }

    #[must_use]
    pub const fn timeout(&self) -> Duration {
        self.timeout
    }

    #[must_use]
    pub const fn output_limit(&self) -> usize {
        self.output_limit
    }

    /// Ask for a SAT model and replay it through the regular Tess evaluator.
    ///
    /// The adapter first performs a status-only `check-sat` request. Only
    /// after a `sat` answer does it run the same query again with a bounded
    /// `(get-value ...)` request. Both processes share one wall-clock deadline.
    /// A parsed model is accepted only when it evaluates to a concrete
    /// violation (universal `assert`) or non-vacuous witness (`assert some`) of
    /// the assertion named by `query.invariant` in `program`. `unsat` is always
    /// returned as advisory.
    ///
    /// # Errors
    ///
    /// Returns the same process, resource, and UTF-8 errors as [`Self::solve`].
    /// A syntactically invalid or incomplete SAT model is a structured
    /// [`ExternalSolverAssessmentStatus::SatRejected`] result, not trusted
    /// evidence and not a process error.
    pub fn solve_and_replay(
        &self,
        program: &CompiledProgram,
        query: &SmtLibQuery,
    ) -> Result<ExternalSolverAssessment, ExternalSolverError> {
        let started = Instant::now();
        let deadline = started
            .checked_add(self.timeout)
            .ok_or_else(|| invalid_configuration("timeout is too large for this platform"))?;
        let initial = self.invoke(&query.script, deadline)?;
        let solver_status = parse_solver_status(&initial.stdout)?;
        match solver_status {
            ExternalSolverStatus::Unsat => Ok(advisory_assessment(
                self,
                solver_status,
                ExternalSolverAssessmentStatus::UnsatAdvisory,
                started,
                initial.stderr,
                "external unsat has no independently verified proof certificate",
            )),
            ExternalSolverStatus::Unknown => Ok(advisory_assessment(
                self,
                solver_status,
                ExternalSolverAssessmentStatus::Unknown,
                started,
                initial.stderr,
                "external solver returned unknown",
            )),
            ExternalSolverStatus::Sat => {
                let requested_symbols = requested_model_symbols(query);
                let requested_symbols = match requested_symbols {
                    Ok(symbols) => symbols,
                    Err(reason) => {
                        return Ok(rejected_sat_assessment(
                            self,
                            started,
                            initial.stderr,
                            None,
                            reason,
                        ));
                    }
                };
                let (model, stderr) = if requested_symbols.is_empty() {
                    (
                        ExternalSolverModel {
                            assignments: Vec::new(),
                        },
                        initial.stderr,
                    )
                } else {
                    let model_script = script_with_model_request(&query.script, &requested_symbols);
                    let model_output = self.invoke(&model_script, deadline)?;
                    let stderr = merge_bounded_diagnostics(
                        &initial.stderr,
                        &model_output.stderr,
                        self.output_limit,
                    )?;
                    let model =
                        match parse_sat_model_response(&model_output.stdout, &requested_symbols) {
                            Ok(model) => model,
                            Err(reason) => {
                                return Ok(rejected_sat_assessment(
                                    self, started, stderr, None, reason,
                                ));
                            }
                        };
                    (model, stderr)
                };
                let input = match model_to_input(program, query, &model) {
                    Ok(input) => input,
                    Err(reason) => {
                        return Ok(rejected_sat_assessment(
                            self,
                            started,
                            stderr,
                            Some(model),
                            reason,
                        ));
                    }
                };
                let quantifier = match query_quantifier(program, query) {
                    Ok(quantifier) => quantifier,
                    Err(reason) => {
                        return Ok(rejected_sat_assessment(
                            self,
                            started,
                            stderr,
                            Some(model),
                            reason,
                        ));
                    }
                };
                let violation_replay = (quantifier == InvariantQuantifier::All)
                    .then(|| replay_invariant_violation(program, &query.invariant, &input));
                match (quantifier, violation_replay) {
                    (InvariantQuantifier::All, Some(Ok(Some(counterexample))))
                        if counterexample.kind != CounterexampleKind::Unknown =>
                    {
                        Ok(ExternalSolverAssessment {
                            schema_version: EXTERNAL_SMT_ASSESSMENT_SCHEMA_VERSION.into(),
                            backend: self.backend.clone(),
                            solver_status,
                            status: ExternalSolverAssessmentStatus::CounterexampleValidated,
                            trust: ExternalSolverTrust::TessReplayValidated,
                            elapsed_ms: started.elapsed().as_millis(),
                            stderr,
                            model: Some(model),
                            counterexample: Some(counterexample),
                            reason: None,
                        })
                    }
                    (InvariantQuantifier::All, Some(Ok(Some(counterexample)))) => {
                        Ok(rejected_sat_assessment(
                            self,
                            started,
                            stderr,
                            Some(model),
                            format!(
                                "Tess replay needed additional input: {}",
                                counterexample.reason
                            ),
                        ))
                    }
                    (InvariantQuantifier::All, Some(Ok(None))) => Ok(rejected_sat_assessment(
                        self,
                        started,
                        stderr,
                        Some(model),
                        "the imported assignment does not violate the assertion",
                    )),
                    (InvariantQuantifier::Some, None) => {
                        match replay_invariant_witness(program, &query.invariant, &input) {
                            Ok(()) => Ok(ExternalSolverAssessment {
                                schema_version: EXTERNAL_SMT_ASSESSMENT_SCHEMA_VERSION.into(),
                                backend: self.backend.clone(),
                                solver_status,
                                status: ExternalSolverAssessmentStatus::WitnessValidated,
                                trust: ExternalSolverTrust::TessReplayValidated,
                                elapsed_ms: started.elapsed().as_millis(),
                                stderr,
                                model: Some(model),
                                counterexample: None,
                                reason: None,
                            }),
                            Err(reason) => Ok(rejected_sat_assessment(
                                self,
                                started,
                                stderr,
                                Some(model),
                                format!(
                                    "the imported assignment does not satisfy the assertion: {reason}"
                                ),
                            )),
                        }
                    }
                    (InvariantQuantifier::All, Some(Err(reason))) => Ok(rejected_sat_assessment(
                        self,
                        started,
                        stderr,
                        Some(model),
                        reason,
                    )),
                    (InvariantQuantifier::All, None) | (InvariantQuantifier::Some, Some(_)) => {
                        unreachable!(
                            "quantifier-specific replay selection must match the assertion"
                        )
                    }
                }
            }
        }
    }

    fn invoke(
        &self,
        script: &str,
        deadline: Instant,
    ) -> Result<CommandOutput, ExternalSolverError> {
        if Instant::now() >= deadline {
            return Err(timeout_error(self.timeout));
        }
        let mut child = Command::new(&self.executable)
            .args(&self.arguments)
            .stdin(Stdio::piped())
            .stdout(Stdio::piped())
            .stderr(Stdio::piped())
            .spawn()
            .map_err(|error| ExternalSolverError::Spawn {
                executable: self.executable.to_string_lossy().into_owned(),
                reason: error.to_string(),
            })?;

        let Some(stdin) = child.stdin.take() else {
            terminate_child(&mut child);
            return Err(io_error("stdin", "not piped"));
        };
        let Some(stdout) = child.stdout.take() else {
            terminate_child(&mut child);
            return Err(io_error("stdout", "not piped"));
        };
        let Some(stderr) = child.stderr.take() else {
            terminate_child(&mut child);
            return Err(io_error("stderr", "not piped"));
        };

        let input = script.as_bytes().to_vec();
        let output_limit = self.output_limit;
        let stdin_result = spawn_io(move || write_input(stdin, &input));
        let stdout_result = spawn_io(move || read_bounded(stdout, output_limit));
        let stderr_result = spawn_io(move || read_bounded(stderr, output_limit));

        let status = loop {
            match child.try_wait() {
                Ok(Some(status)) => break status,
                Ok(None) if Instant::now() >= deadline => {
                    terminate_child(&mut child);
                    return Err(timeout_error(self.timeout));
                }
                Ok(None) => thread::sleep(poll_interval(deadline)),
                Err(error) => {
                    terminate_child(&mut child);
                    return Err(io_error("process", error));
                }
            }
        };

        receive_io(stdin_result, deadline, self.timeout, "stdin")?
            .map_err(|error| io_error("stdin", error))?;
        let stdout = receive_io(stdout_result, deadline, self.timeout, "stdout")?
            .map_err(|error| io_error("stdout", error))?;
        let stderr = receive_io(stderr_result, deadline, self.timeout, "stderr")?
            .map_err(|error| io_error("stderr", error))?;
        let stdout = bounded_utf8(stdout, "stdout", self.output_limit)?;
        let stderr = bounded_utf8(stderr, "stderr", self.output_limit)?;

        if !status.success() {
            return Err(ExternalSolverError::UnsuccessfulExit {
                code: status.code(),
                stderr,
            });
        }
        Ok(CommandOutput { stdout, stderr })
    }
}

impl SmtLibSolver for CommandSmtSolver {
    fn solve(&self, query: &SmtLibQuery) -> Result<ExternalSolverResult, ExternalSolverError> {
        let started = Instant::now();
        let deadline = started
            .checked_add(self.timeout)
            .ok_or_else(|| invalid_configuration("timeout is too large for this platform"))?;
        let output = self.invoke(&query.script, deadline)?;
        let solver_status = parse_solver_status(&output.stdout)?;
        Ok(ExternalSolverResult {
            backend: self.backend.clone(),
            status: solver_status,
            elapsed_ms: started.elapsed().as_millis(),
            stderr: output.stderr,
        })
    }
}

#[derive(Debug)]
struct CommandOutput {
    stdout: String,
    stderr: String,
}

fn advisory_assessment(
    solver: &CommandSmtSolver,
    solver_status: ExternalSolverStatus,
    status: ExternalSolverAssessmentStatus,
    started: Instant,
    stderr: String,
    reason: impl Into<String>,
) -> ExternalSolverAssessment {
    ExternalSolverAssessment {
        schema_version: EXTERNAL_SMT_ASSESSMENT_SCHEMA_VERSION.into(),
        backend: solver.backend.clone(),
        solver_status,
        status,
        trust: ExternalSolverTrust::Advisory,
        elapsed_ms: started.elapsed().as_millis(),
        stderr,
        model: None,
        counterexample: None,
        reason: Some(reason.into()),
    }
}

fn rejected_sat_assessment(
    solver: &CommandSmtSolver,
    started: Instant,
    stderr: String,
    model: Option<ExternalSolverModel>,
    reason: impl Into<String>,
) -> ExternalSolverAssessment {
    ExternalSolverAssessment {
        schema_version: EXTERNAL_SMT_ASSESSMENT_SCHEMA_VERSION.into(),
        backend: solver.backend.clone(),
        solver_status: ExternalSolverStatus::Sat,
        status: ExternalSolverAssessmentStatus::SatRejected,
        trust: ExternalSolverTrust::Advisory,
        elapsed_ms: started.elapsed().as_millis(),
        stderr,
        model,
        counterexample: None,
        reason: Some(reason.into()),
    }
}

fn merge_bounded_diagnostics(
    first: &str,
    second: &str,
    limit: usize,
) -> Result<String, ExternalSolverError> {
    let separator = usize::from(!first.is_empty() && !second.is_empty());
    let length = first
        .len()
        .checked_add(second.len())
        .and_then(|length| length.checked_add(separator));
    if length.is_none_or(|length| length > limit) {
        return Err(ExternalSolverError::OutputLimitExceeded {
            stream: "combined stderr".into(),
            limit,
        });
    }
    match (first.is_empty(), second.is_empty()) {
        (true, _) => Ok(second.to_owned()),
        (_, true) => Ok(first.to_owned()),
        (false, false) => Ok(format!("{first}\n{second}")),
    }
}

fn requested_model_symbols(query: &SmtLibQuery) -> Result<Vec<String>, String> {
    let mut symbols = Vec::new();
    let mut seen = BTreeSet::new();
    for symbol in &query.symbols {
        let names: Vec<&str> = match &symbol.encoding {
            SmtSymbolEncoding::Bool { symbol }
            | SmtSymbolEncoding::Int { symbol }
            | SmtSymbolEncoding::EnumIndex { symbol, .. } => vec![symbol],
            SmtSymbolEncoding::DecimalMantissaScale {
                mantissa_symbol,
                scale_symbol,
                ..
            } => vec![mantissa_symbol, scale_symbol],
        };
        for name in names {
            if !is_simple_smt_symbol(name) {
                return Err(format!(
                    "query model symbol `{name}` is not a safe simple SMT-LIB symbol"
                ));
            }
            if !seen.insert(name.to_owned()) {
                return Err(format!("query model symbol `{name}` is duplicated"));
            }
            symbols.push(name.to_owned());
        }
    }
    Ok(symbols)
}

fn is_simple_smt_symbol(symbol: &str) -> bool {
    let mut characters = symbol.chars();
    let Some(first) = characters.next() else {
        return false;
    };
    let punctuation = |character: char| {
        matches!(
            character,
            '~' | '!'
                | '@'
                | '$'
                | '%'
                | '^'
                | '&'
                | '*'
                | '_'
                | '-'
                | '+'
                | '='
                | '<'
                | '>'
                | '.'
                | '?'
                | '/'
        )
    };
    (first.is_ascii_alphabetic() || punctuation(first))
        && characters.all(|character| character.is_ascii_alphanumeric() || punctuation(character))
}

fn script_with_model_request(script: &str, symbols: &[String]) -> String {
    let mut output = String::from("(set-option :produce-models true)\n");
    output.push_str(script);
    if !output.ends_with('\n') {
        output.push('\n');
    }
    output.push_str("(get-value (");
    output.push_str(&symbols.join(" "));
    output.push_str("))\n");
    output
}

#[derive(Clone, Debug, PartialEq, Eq)]
enum SExpression {
    Atom(String),
    List(Vec<SExpression>),
}

struct SExpressionParser<'a> {
    input: &'a [u8],
    position: usize,
    nodes: usize,
}

impl<'a> SExpressionParser<'a> {
    fn new(input: &'a str) -> Result<Self, String> {
        if !input.is_ascii() {
            return Err("external model response must be ASCII".into());
        }
        Ok(Self {
            input: input.as_bytes(),
            position: 0,
            nodes: 0,
        })
    }

    fn parse_all(mut self) -> Result<Vec<SExpression>, String> {
        let mut expressions = Vec::new();
        self.skip_trivia();
        while self.position < self.input.len() {
            expressions.push(self.parse_expression(0)?);
            self.skip_trivia();
        }
        Ok(expressions)
    }

    fn parse_expression(&mut self, depth: usize) -> Result<SExpression, String> {
        const MAX_MODEL_DEPTH: usize = 16;
        const MAX_MODEL_NODES: usize = 4_096;
        if depth > MAX_MODEL_DEPTH {
            return Err("external model nesting is too deep".into());
        }
        self.nodes += 1;
        if self.nodes > MAX_MODEL_NODES {
            return Err("external model contains too many expressions".into());
        }
        self.skip_trivia();
        match self.input.get(self.position).copied() {
            Some(b'(') => {
                self.position += 1;
                let mut values = Vec::new();
                loop {
                    self.skip_trivia();
                    match self.input.get(self.position).copied() {
                        Some(b')') => {
                            self.position += 1;
                            return Ok(SExpression::List(values));
                        }
                        None => return Err("external model has an unclosed list".into()),
                        _ => values.push(self.parse_expression(depth + 1)?),
                    }
                }
            }
            Some(b')') => Err("external model has an unexpected `)`".into()),
            Some(b'\"' | b'|') => {
                Err("external model strings and quoted symbols are not supported".into())
            }
            Some(_) => self.parse_atom(),
            None => Err("external model ended unexpectedly".into()),
        }
    }

    fn parse_atom(&mut self) -> Result<SExpression, String> {
        let start = self.position;
        while let Some(byte) = self.input.get(self.position).copied() {
            if byte.is_ascii_whitespace() || matches!(byte, b'(' | b')' | b';') {
                break;
            }
            self.position += 1;
        }
        if self.position == start {
            return Err("external model contains an empty atom".into());
        }
        let atom = std::str::from_utf8(&self.input[start..self.position])
            .map_err(|_| "external model atom was not UTF-8")?;
        Ok(SExpression::Atom(atom.to_owned()))
    }

    fn skip_trivia(&mut self) {
        loop {
            while self
                .input
                .get(self.position)
                .is_some_and(u8::is_ascii_whitespace)
            {
                self.position += 1;
            }
            if self.input.get(self.position) != Some(&b';') {
                return;
            }
            while self
                .input
                .get(self.position)
                .is_some_and(|byte| *byte != b'\n')
            {
                self.position += 1;
            }
        }
    }
}

fn parse_sat_model_response(
    stdout: &str,
    requested_symbols: &[String],
) -> Result<ExternalSolverModel, String> {
    let expressions = SExpressionParser::new(stdout)?.parse_all()?;
    let [SExpression::Atom(status), SExpression::List(pairs)] = expressions.as_slice() else {
        return Err("external model response must contain `sat` followed by one value list".into());
    };
    if status != "sat" {
        return Err(format!(
            "external model request returned `{status}` instead of `sat`"
        ));
    }
    let requested = requested_symbols.iter().cloned().collect::<BTreeSet<_>>();
    let mut parsed = BTreeMap::new();
    for pair in pairs {
        let SExpression::List(parts) = pair else {
            return Err("external model assignment must be a two-item list".into());
        };
        let [SExpression::Atom(symbol), value] = parts.as_slice() else {
            return Err("external model assignment must be a two-item list".into());
        };
        if !requested.contains(symbol) {
            return Err(format!("external model returned unknown symbol `{symbol}`"));
        }
        let value = parse_external_model_value(value)?;
        if parsed.insert(symbol.clone(), value).is_some() {
            return Err(format!("external model repeated symbol `{symbol}`"));
        }
    }
    let mut assignments = Vec::with_capacity(requested_symbols.len());
    for symbol in requested_symbols {
        let value = parsed
            .remove(symbol)
            .ok_or_else(|| format!("external model omitted symbol `{symbol}`"))?;
        assignments.push(ExternalModelAssignment {
            symbol: symbol.clone(),
            value,
        });
    }
    Ok(ExternalSolverModel { assignments })
}

fn parse_external_model_value(expression: &SExpression) -> Result<ExternalModelValue, String> {
    match expression {
        SExpression::Atom(value) if value == "true" => Ok(ExternalModelValue::Bool { value: true }),
        SExpression::Atom(value) if value == "false" => {
            Ok(ExternalModelValue::Bool { value: false })
        }
        SExpression::Atom(value) => parse_external_integer(value),
        SExpression::List(parts) => match parts.as_slice() {
            [SExpression::Atom(operator), SExpression::Atom(magnitude)] if operator == "-" => {
                if magnitude.starts_with('+') || magnitude.starts_with('-') {
                    return Err("external model has an invalid negative integer".into());
                }
                parse_external_integer(&format!("-{magnitude}"))
            }
            _ => Err("external model value is outside the Bool/Int fragment".into()),
        },
    }
}

fn parse_external_integer(value: &str) -> Result<ExternalModelValue, String> {
    let parsed = value
        .parse::<i128>()
        .map_err(|_| format!("external model integer `{value}` is out of range or invalid"))?;
    Ok(ExternalModelValue::Integer {
        value: parsed.to_string(),
    })
}

fn model_to_input(
    program: &CompiledProgram,
    query: &SmtLibQuery,
    model: &ExternalSolverModel,
) -> Result<Input, String> {
    let invariant = program
        .invariant(&query.invariant)
        .ok_or_else(|| format!("unknown assertion `{}`", query.invariant))?;
    let mut values = BTreeMap::new();
    for assignment in &model.assignments {
        values.insert(assignment.symbol.as_str(), &assignment.value);
    }

    let mut bindings = BTreeMap::<String, (String, BTreeMap<String, Value>)>::new();
    for variable in &invariant.variables {
        let binding = normalize_name(&variable.name.value);
        if bindings
            .insert(binding, (variable.ty.value.clone(), BTreeMap::new()))
            .is_some()
        {
            return Err("assertion contains duplicate normalized bindings".into());
        }
    }

    for symbol in &query.symbols {
        let binding_name = normalize_name(&symbol.binding);
        let Some((entity_name, fields)) = bindings.get_mut(&binding_name) else {
            return Err(format!(
                "query field `{}.{}` references a non-assertion binding",
                symbol.binding, symbol.field
            ));
        };
        if normalize_name(entity_name) != normalize_name(&symbol.entity) {
            return Err(format!(
                "query binding `{}` claims record `{}` instead of `{entity_name}`",
                symbol.binding, symbol.entity
            ));
        }
        let field = program.field(entity_name, &symbol.field).ok_or_else(|| {
            format!(
                "query references unknown field `{entity_name}.{}`",
                symbol.field
            )
        })?;
        let value = decode_external_field_value(&symbol.encoding, &values)?;
        let field_name = normalize_name(&field.name.value);
        if fields.insert(field_name.clone(), value).is_some() {
            return Err(format!(
                "query repeats field `{}.{field_name}`",
                symbol.binding
            ));
        }
    }

    let mut input = Input::new();
    for variable in &invariant.variables {
        let binding = normalize_name(&variable.name.value);
        let (entity, fields) = bindings
            .remove(&binding)
            .ok_or_else(|| format!("query omitted assertion binding `{binding}`"))?;
        input.insert(&variable.name.value, entity, fields);
    }
    let diagnostics = input.validate(program);
    if !diagnostics.is_empty() {
        return Err(diagnostics
            .iter()
            .map(|diagnostic| diagnostic.message.as_str())
            .collect::<Vec<_>>()
            .join("; "));
    }
    Ok(input)
}

fn query_quantifier(
    program: &CompiledProgram,
    query: &SmtLibQuery,
) -> Result<InvariantQuantifier, String> {
    let invariant = program
        .invariant(&query.invariant)
        .ok_or_else(|| format!("unknown assertion `{}`", query.invariant))?;
    if query.metadata.schema_version != SMTLIB_QUERY_SCHEMA_VERSION {
        return Err(format!(
            "unsupported SMT-LIB query schema `{}`",
            query.metadata.schema_version
        ));
    }
    let expected_query = match invariant.quantifier {
        InvariantQuantifier::All => "invariant_violation",
        InvariantQuantifier::Some => "invariant_witness",
    };
    if query.metadata.query != expected_query {
        return Err(format!(
            "query kind `{}` does not match the assertion's `{expected_query}` semantics",
            query.metadata.query
        ));
    }
    Ok(invariant.quantifier)
}

fn decode_external_field_value(
    encoding: &SmtSymbolEncoding,
    values: &BTreeMap<&str, &ExternalModelValue>,
) -> Result<Value, String> {
    match encoding {
        SmtSymbolEncoding::Bool { symbol } => match values.get(symbol.as_str()) {
            Some(ExternalModelValue::Bool { value }) => Ok(Value::Bool(*value)),
            Some(_) => Err(format!("external model symbol `{symbol}` is not Bool")),
            None => Err(format!("external model omitted symbol `{symbol}`")),
        },
        SmtSymbolEncoding::Int { symbol } => {
            let integer = external_integer(values, symbol)?;
            let integer = i64::try_from(integer)
                .map_err(|_| format!("external model Int `{symbol}` is outside i64"))?;
            Ok(Value::Int(integer))
        }
        SmtSymbolEncoding::DecimalMantissaScale {
            mantissa_symbol,
            scale_symbol,
            ..
        } => {
            let mantissa = external_integer(values, mantissa_symbol)?;
            let scale = external_integer(values, scale_symbol)?;
            let scale = u32::try_from(scale)
                .ok()
                .filter(|scale| *scale <= Decimal::MAX_SCALE)
                .ok_or_else(|| {
                    format!("external model Decimal scale `{scale_symbol}` is outside 0..28")
                })?;
            let decimal = Decimal::try_from_i128_with_scale(mantissa, scale)
                .map_err(|error| format!("external model Decimal is not representable: {error}"))?;
            Ok(Value::decimal(decimal))
        }
        SmtSymbolEncoding::EnumIndex {
            symbol,
            type_name,
            variants,
        } => {
            let index = external_integer(values, symbol)?;
            let index = usize::try_from(index)
                .ok()
                .filter(|index| *index < variants.len())
                .ok_or_else(|| format!("external model enum index `{symbol}` is out of range"))?;
            Ok(Value::Enum {
                type_name: type_name.clone(),
                variant: variants[index].clone(),
            })
        }
    }
}

fn external_integer(
    values: &BTreeMap<&str, &ExternalModelValue>,
    symbol: &str,
) -> Result<i128, String> {
    match values.get(symbol) {
        Some(ExternalModelValue::Integer { value }) => value
            .parse::<i128>()
            .map_err(|_| format!("external model integer `{symbol}` is invalid")),
        Some(_) => Err(format!("external model symbol `{symbol}` is not Int")),
        None => Err(format!("external model omitted symbol `{symbol}`")),
    }
}

type IoReceiver<T> = Receiver<io::Result<T>>;

#[derive(Debug)]
struct BoundedOutput {
    bytes: Vec<u8>,
    exceeded: bool,
}

fn spawn_io<T, F>(operation: F) -> IoReceiver<T>
where
    T: Send + 'static,
    F: FnOnce() -> io::Result<T> + Send + 'static,
{
    let (sender, receiver) = mpsc::sync_channel(1);
    thread::spawn(move || {
        let _ = sender.send(operation());
    });
    receiver
}

fn write_input(mut stdin: impl Write, input: &[u8]) -> io::Result<()> {
    stdin.write_all(input)?;
    stdin.flush()
}

fn read_bounded(mut stream: impl Read, limit: usize) -> io::Result<BoundedOutput> {
    let mut bytes = Vec::with_capacity(limit.min(8 * 1024));
    let mut buffer = [0_u8; 8 * 1024];
    let mut exceeded = false;
    loop {
        let count = stream.read(&mut buffer)?;
        if count == 0 {
            break;
        }
        let remaining = limit.saturating_sub(bytes.len());
        bytes.extend_from_slice(&buffer[..count.min(remaining)]);
        exceeded |= count > remaining;
    }
    Ok(BoundedOutput { bytes, exceeded })
}

fn receive_io<T>(
    receiver: IoReceiver<T>,
    deadline: Instant,
    timeout: Duration,
    stream: &'static str,
) -> Result<io::Result<T>, ExternalSolverError> {
    let remaining = deadline.saturating_duration_since(Instant::now());
    if remaining.is_zero() {
        return Err(timeout_error(timeout));
    }
    receiver
        .recv_timeout(remaining)
        .map_err(|error| match error {
            mpsc::RecvTimeoutError::Timeout => timeout_error(timeout),
            mpsc::RecvTimeoutError::Disconnected => io_error(stream, "worker disconnected"),
        })
}

fn bounded_utf8(
    output: BoundedOutput,
    stream: &'static str,
    limit: usize,
) -> Result<String, ExternalSolverError> {
    if output.exceeded {
        return Err(ExternalSolverError::OutputLimitExceeded {
            stream: stream.into(),
            limit,
        });
    }
    String::from_utf8(output.bytes).map_err(|_| ExternalSolverError::InvalidUtf8 {
        stream: stream.into(),
    })
}

fn parse_solver_status(stdout: &str) -> Result<ExternalSolverStatus, ExternalSolverError> {
    match stdout.trim_matches(|character: char| character.is_ascii_whitespace()) {
        "sat" => Ok(ExternalSolverStatus::Sat),
        "unsat" => Ok(ExternalSolverStatus::Unsat),
        "unknown" => Ok(ExternalSolverStatus::Unknown),
        _ => Err(ExternalSolverError::InvalidStatus {
            stdout: stdout.to_owned(),
        }),
    }
}

fn poll_interval(deadline: Instant) -> Duration {
    deadline
        .saturating_duration_since(Instant::now())
        .min(Duration::from_millis(5))
}

fn invalid_configuration(reason: impl fmt::Display) -> ExternalSolverError {
    ExternalSolverError::InvalidConfiguration {
        reason: reason.to_string(),
    }
}

fn io_error(stream: &'static str, reason: impl fmt::Display) -> ExternalSolverError {
    ExternalSolverError::Io {
        stream: stream.into(),
        reason: reason.to_string(),
    }
}

fn timeout_error(timeout: Duration) -> ExternalSolverError {
    ExternalSolverError::Timeout {
        timeout_ms: timeout.as_millis(),
    }
}

fn terminate_child(child: &mut Child) {
    let _ = child.kill();
    let _ = child.wait();
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::SourceFile;
    use std::ffi::{OsStr, OsString};

    fn compile_text(source: &str) -> CompiledProgram {
        let output = crate::compile_source(SourceFile::new("export.tes", source));
        assert!(
            !output.has_errors(),
            "{}",
            output
                .diagnostics
                .iter()
                .map(|diagnostic| diagnostic.message.as_str())
                .collect::<Vec<_>>()
                .join("; ")
        );
        output.program.expect("compiled SMT-LIB fixture")
    }

    fn query(script: &str) -> SmtLibQuery {
        SmtLibQuery {
            invariant: "example".into(),
            source: SmtSourceLocation {
                file: "example.tes".into(),
                span: Span::new(0, 1),
                line: 1,
                column: 1,
            },
            metadata: SmtLibMetadata {
                schema_version: SMTLIB_QUERY_SCHEMA_VERSION.into(),
                generator: "tess".into(),
                generator_version: env!("CARGO_PKG_VERSION").into(),
                logic: "QF_LIA".into(),
                query: "invariant_violation".into(),
            },
            symbols: Vec::new(),
            script: script.into(),
        }
    }

    fn replay_fixture() -> (CompiledProgram, SmtLibQuery) {
        let program = compile_text(
            r"mod Replay
enum Choice:
    A
    B

record E:
    enabled: Bool
    count: Int 0..10
    amount: Decimal 0.0..2.0
    choice: Choice

dec d(e E) -> Choice

policy::replay @replay policy:
    Matching inputs produce A.

    rule only(e E):
        e.enabled and e.count > 5 and e.amount > 1.0 and e.choice = A => d(e) = A

assert total(e E):
    d(e)
",
        );
        let query = export_invariant_smtlib(&program, "total").unwrap();
        (program, query)
    }

    fn violating_model(query: &SmtLibQuery) -> String {
        violating_model_with(query, &BTreeMap::new())
    }

    fn violating_model_with(query: &SmtLibQuery, overrides: &BTreeMap<String, String>) -> String {
        let mut assignments = Vec::new();
        for symbol in &query.symbols {
            match &symbol.encoding {
                SmtSymbolEncoding::Bool { symbol } => {
                    let value = overrides.get(symbol).map_or("false", String::as_str);
                    assignments.push(format!("({symbol} {value})"));
                }
                SmtSymbolEncoding::Int { symbol } => {
                    let value = overrides.get(symbol).map_or("2", String::as_str);
                    assignments.push(format!("({symbol} {value})"));
                }
                SmtSymbolEncoding::DecimalMantissaScale {
                    mantissa_symbol,
                    scale_symbol,
                    ..
                } => {
                    let mantissa = overrides.get(mantissa_symbol).map_or("15", String::as_str);
                    let scale = overrides.get(scale_symbol).map_or("1", String::as_str);
                    assignments.push(format!("({mantissa_symbol} {mantissa})"));
                    assignments.push(format!("({scale_symbol} {scale})"));
                }
                SmtSymbolEncoding::EnumIndex { symbol, .. } => {
                    let value = overrides.get(symbol).map_or("1", String::as_str);
                    assignments.push(format!("({symbol} {value})"));
                }
            }
        }
        format!("sat\n({})\n", assignments.join(" "))
    }

    fn primary_encoding_symbol(encoding: &SmtSymbolEncoding) -> &str {
        match encoding {
            SmtSymbolEncoding::Bool { symbol }
            | SmtSymbolEncoding::Int { symbol }
            | SmtSymbolEncoding::EnumIndex { symbol, .. } => symbol,
            SmtSymbolEncoding::DecimalMantissaScale {
                mantissa_symbol, ..
            } => mantissa_symbol,
        }
    }

    fn primary_encoding_symbol_mut(encoding: &mut SmtSymbolEncoding) -> &mut String {
        match encoding {
            SmtSymbolEncoding::Bool { symbol }
            | SmtSymbolEncoding::Int { symbol }
            | SmtSymbolEncoding::EnumIndex { symbol, .. } => symbol,
            SmtSymbolEncoding::DecimalMantissaScale {
                mantissa_symbol, ..
            } => mantissa_symbol,
        }
    }

    fn coherent_assessment() -> ExternalSolverAssessment {
        ExternalSolverAssessment {
            schema_version: EXTERNAL_SMT_ASSESSMENT_SCHEMA_VERSION.into(),
            backend: "test".into(),
            solver_status: ExternalSolverStatus::Sat,
            status: ExternalSolverAssessmentStatus::CounterexampleValidated,
            trust: ExternalSolverTrust::TessReplayValidated,
            elapsed_ms: 1,
            stderr: String::new(),
            model: Some(ExternalSolverModel {
                assignments: vec![ExternalModelAssignment {
                    symbol: "v0".into(),
                    value: ExternalModelValue::Integer { value: "0".into() },
                }],
            }),
            counterexample: Some(Counterexample {
                invariant: "total".into(),
                kind: CounterexampleKind::Undefined,
                input: Input::new(),
                reason: "no candidate".into(),
                evaluation: None,
            }),
            reason: None,
        }
    }

    fn satisfying_model(query: &SmtLibQuery) -> String {
        let mut assignments = Vec::new();
        for symbol in &query.symbols {
            match &symbol.encoding {
                SmtSymbolEncoding::Bool { symbol } => {
                    assignments.push(format!("({symbol} true)"));
                }
                SmtSymbolEncoding::Int { symbol } => {
                    assignments.push(format!("({symbol} 6)"));
                }
                SmtSymbolEncoding::DecimalMantissaScale {
                    mantissa_symbol,
                    scale_symbol,
                    ..
                } => {
                    assignments.push(format!("({mantissa_symbol} 15)"));
                    assignments.push(format!("({scale_symbol} 1)"));
                }
                SmtSymbolEncoding::EnumIndex { symbol, .. } => {
                    assignments.push(format!("({symbol} 0)"));
                }
            }
        }
        format!("sat\n({})\n", assignments.join(" "))
    }

    #[cfg(unix)]
    fn fake_model_solver(model_response: impl Into<OsString>) -> CommandSmtSolver {
        CommandSmtSolver::new("fake", "/bin/sh").unwrap().args([
            OsString::from("-c"),
            OsString::from(
                "input=$(cat); case \"$input\" in *'(get-value ('*) printf '%s' \"$1\";; *) printf sat;; esac",
            ),
            OsString::from("tess-fake-solver"),
            model_response.into(),
        ])
    }

    #[cfg(unix)]
    fn assert_fake_sat_rejected(
        program: &CompiledProgram,
        query: &SmtLibQuery,
        model_response: impl Into<OsString>,
        reason_fragment: &str,
    ) -> ExternalSolverAssessment {
        let assessment = fake_model_solver(model_response)
            .solve_and_replay(program, query)
            .unwrap();
        assert_eq!(
            assessment.status,
            ExternalSolverAssessmentStatus::SatRejected
        );
        assert_eq!(assessment.trust, ExternalSolverTrust::Advisory);
        assert!(assessment.validate_consistency().is_ok());
        assert!(!assessment.independently_validated());
        assert!(assessment.accepted_counterexample().is_none());
        assert!(
            assessment
                .reason
                .as_deref()
                .is_some_and(|reason| reason.contains(reason_fragment)),
            "{:?}",
            assessment.reason
        );
        assessment
    }

    #[test]
    fn status_parser_accepts_only_one_standard_token() {
        assert_eq!(
            parse_solver_status("sat").unwrap(),
            ExternalSolverStatus::Sat
        );
        assert_eq!(
            parse_solver_status(" \nunsat\t").unwrap(),
            ExternalSolverStatus::Unsat
        );
        assert_eq!(
            parse_solver_status("unknown\n").unwrap(),
            ExternalSolverStatus::Unknown
        );
        for invalid in ["", "SAT", "sat unknown", "sat\n(model)", "; note\nsat"] {
            assert!(matches!(
                parse_solver_status(invalid),
                Err(ExternalSolverError::InvalidStatus { .. })
            ));
        }
    }

    #[test]
    fn model_parser_normalizes_order_and_rejects_incomplete_models() {
        let symbols = vec!["v0".to_owned(), "v1".to_owned()];
        let model = parse_sat_model_response("sat\n((v1 (- 2)) (v0 true))", &symbols).unwrap();
        assert_eq!(
            model.assignments,
            vec![
                ExternalModelAssignment {
                    symbol: "v0".into(),
                    value: ExternalModelValue::Bool { value: true },
                },
                ExternalModelAssignment {
                    symbol: "v1".into(),
                    value: ExternalModelValue::Integer { value: "-2".into() },
                },
            ]
        );
        assert!(parse_sat_model_response("sat\n((v0 true))", &symbols).is_err());
        assert!(parse_sat_model_response("sat\n((v0 true) (extra 1))", &symbols).is_err());
        assert!(parse_sat_model_response("sat\n((v0 true) (v0 false))", &symbols).is_err());
    }

    #[test]
    fn model_parser_enforces_text_depth_and_node_boundaries() {
        assert!(SExpressionParser::new("sat\n((v0 café))").is_err());
        assert!(parse_sat_model_response("sat\n((|v0| 1))", &["v0".into()]).is_err());
        assert!(parse_sat_model_response("sat\n((v0 \"1\"))", &["v0".into()]).is_err());

        let at_depth_limit = format!("{}x{}", "(".repeat(16), ")".repeat(16));
        assert!(
            SExpressionParser::new(&at_depth_limit)
                .unwrap()
                .parse_all()
                .is_ok()
        );
        let beyond_depth_limit = format!("{}x{}", "(".repeat(17), ")".repeat(17));
        assert!(
            SExpressionParser::new(&beyond_depth_limit)
                .unwrap()
                .parse_all()
                .is_err()
        );

        let at_node_limit = format!("({})", vec!["x"; 4_095].join(" "));
        assert!(
            SExpressionParser::new(&at_node_limit)
                .unwrap()
                .parse_all()
                .is_ok()
        );
        let beyond_node_limit = format!("({})", vec!["x"; 4_096].join(" "));
        assert!(
            SExpressionParser::new(&beyond_node_limit)
                .unwrap()
                .parse_all()
                .is_err()
        );
    }

    #[test]
    fn inconsistent_deserialized_assessments_never_become_trusted() {
        let valid = coherent_assessment();
        assert!(valid.validate_consistency().is_ok());
        assert!(valid.independently_validated());
        assert!(valid.accepted_counterexample().is_some());

        let mut unsupported_schema = coherent_assessment();
        unsupported_schema.schema_version = "unsupported".into();
        assert!(unsupported_schema.validate_consistency().is_err());
        assert!(!unsupported_schema.independently_validated());

        let base = serde_json::to_value(&valid).unwrap();
        let mutations = [
            ("solver_status", serde_json::json!("unsat")),
            ("status", serde_json::json!("sat_rejected")),
            ("trust", serde_json::json!("advisory")),
            ("model", serde_json::Value::Null),
            ("counterexample", serde_json::Value::Null),
            ("reason", serde_json::json!("rejected")),
        ];
        for (field, value) in mutations {
            let mut serialized = base.clone();
            if value.is_null() {
                serialized.as_object_mut().unwrap().remove(field);
            } else {
                serialized[field] = value;
            }
            let assessment: ExternalSolverAssessment = serde_json::from_value(serialized).unwrap();
            assert!(assessment.validate_consistency().is_err(), "{field}");
            assert!(!assessment.independently_validated(), "{field}");
            assert!(assessment.accepted_counterexample().is_none(), "{field}");
        }

        let mut unknown_counterexample = base.clone();
        unknown_counterexample["counterexample"]["kind"] = serde_json::json!("unknown");
        let assessment: ExternalSolverAssessment =
            serde_json::from_value(unknown_counterexample).unwrap();
        assert!(assessment.validate_consistency().is_err());
        assert!(!assessment.independently_validated());

        let mut malformed_status = base;
        malformed_status["status"] = serde_json::json!("trusted");
        assert!(serde_json::from_value::<ExternalSolverAssessment>(malformed_status).is_err());
    }

    #[test]
    fn query_replay_requires_the_current_schema() {
        let (program, mut query) = replay_fixture();
        query.metadata.schema_version = "unsupported".into();
        assert!(
            query_quantifier(&program, &query)
                .unwrap_err()
                .contains("unsupported SMT-LIB query schema")
        );
    }

    #[test]
    fn assessment_validation_rejects_malformed_models_and_advisory_evidence() {
        for assignments in [
            vec![
                ExternalModelAssignment {
                    symbol: "v0".into(),
                    value: ExternalModelValue::Integer { value: "0".into() },
                },
                ExternalModelAssignment {
                    symbol: "v0".into(),
                    value: ExternalModelValue::Integer { value: "1".into() },
                },
            ],
            vec![ExternalModelAssignment {
                symbol: "bad symbol".into(),
                value: ExternalModelValue::Integer { value: "0".into() },
            }],
            vec![ExternalModelAssignment {
                symbol: "v0".into(),
                value: ExternalModelValue::Integer { value: "00".into() },
            }],
            vec![ExternalModelAssignment {
                symbol: "v0".into(),
                value: ExternalModelValue::Integer {
                    value: "170141183460469231731687303715884105728".into(),
                },
            }],
        ] {
            let mut assessment = coherent_assessment();
            assessment.model = Some(ExternalSolverModel { assignments });
            assert!(assessment.validate_consistency().is_err());
            assert!(!assessment.independently_validated());
            assert!(assessment.accepted_counterexample().is_none());
        }

        let mut advisory = coherent_assessment();
        advisory.solver_status = ExternalSolverStatus::Unsat;
        advisory.status = ExternalSolverAssessmentStatus::UnsatAdvisory;
        advisory.trust = ExternalSolverTrust::Advisory;
        advisory.reason = Some("no checked proof".into());
        assert!(advisory.validate_consistency().is_err());
        advisory.model = None;
        advisory.counterexample = None;
        assert!(advisory.validate_consistency().is_ok());
        advisory.reason = Some("  ".into());
        assert!(advisory.validate_consistency().is_err());
    }

    #[test]
    fn configuration_rejects_unbounded_values() {
        assert!(CommandSmtSolver::new("", "solver").is_err());
        assert!(CommandSmtSolver::new("solver", "").is_err());
        let solver = CommandSmtSolver::new("solver", "solver").unwrap();
        assert!(solver.clone().with_timeout(Duration::ZERO).is_err());
        assert!(solver.with_output_limit(0).is_err());
    }

    #[test]
    fn exporter_is_deterministic_and_records_symbol_sources() {
        let program = compile_text(
            r"mod Export
enum Result:
    Low
    High

record E:
    x: Int 0..10
    enabled: Bool

dec d(e E) -> Result

policy::result @result policy:
    Inputs are divided into Low and High results.

    rule low(e E):
        e.enabled and e.x < 5 => d(e) = Low

    rule high(e E):
        not e.enabled or e.x > 5 => d(e) = High

assert total(e E):
    d(e)
",
        );
        let first = export_invariant_smtlib(&program, "total").unwrap();
        let second = export_invariant_smtlib(&program, "total").unwrap();
        assert_eq!(first, second);
        let json = serde_json::to_string(&first).unwrap();
        assert_eq!(serde_json::from_str::<SmtLibQuery>(&json).unwrap(), first);
        assert_eq!(first.metadata.schema_version, SMTLIB_QUERY_SCHEMA_VERSION);
        assert_eq!(first.metadata.logic, "QF_LIA");
        assert_eq!(first.metadata.query, "invariant_violation");
        assert!(first.script.contains("(set-logic QF_LIA)"));
        assert!(first.script.contains("(check-sat)"));
        assert!(
            first
                .script
                .contains("; symbol: v0 -> e.x (E.x) @ export.tes:7:5")
        );
        assert_eq!(first.symbols.len(), 2);
        assert!(matches!(
            first.symbols[0].encoding,
            SmtSymbolEncoding::Int { ref symbol } if symbol == "v0"
        ));
        assert!(matches!(
            first.symbols[1].encoding,
            SmtSymbolEncoding::Bool { ref symbol } if symbol == "v1"
        ));
        assert!(first.symbols.iter().all(|symbol| {
            symbol.binding == "e"
                && symbol.entity == "E"
                && symbol.source.file == "export.tes"
                && symbol.source.column == 5
        }));
        assert_eq!(
            first
                .symbols
                .iter()
                .map(|symbol| symbol.source.line)
                .collect::<Vec<_>>(),
            [7, 8]
        );

        let solver = z3::Solver::new();
        solver.from_string(first.script.clone());
        assert_eq!(solver.check(), z3::SatResult::Sat);
        assert!(matches!(
            export_invariant_smtlib(&program, "missing"),
            Err(SmtLibExportError::UnknownInvariant { invariant }) if invariant == "missing"
        ));
    }

    #[test]
    fn exporter_uses_existential_witness_semantics_without_vacuous_implication() {
        let cardinality = compile_text(
            r"mod Export
enum Result:
    Yes

record E:
    x: Int 0..2

dec d(e E) -> Result

policy::yes @yes policy:
    One produces Yes.

    rule yes(e E):
        e.x = 1 => d(e) = Yes

assert some reachable(e E):
    d(e)
",
        );
        let query = export_invariant_smtlib(&cardinality, "reachable").unwrap();
        assert_eq!(query.metadata.query, "invariant_witness");
        assert!(
            query
                .script
                .contains("; semantics: sat means assertion witness")
        );
        let solver = z3::Solver::new();
        solver.from_string(query.script);
        assert_eq!(solver.check(), z3::SatResult::Sat);

        let non_vacuous = compile_text(
            r"mod Export
enum Result:
    No

record E:
    x: Int 0..1

dec d(e E) -> Result

policy::false_premise @false premise:
    Only zero produces No.

    rule only_false_premise(e E):
        e.x = 0 => d(e) = No

assert some reachable(e E):
    e.x > 0 => d(e) = No
",
        );
        let query = export_invariant_smtlib(&non_vacuous, "reachable").unwrap();
        let solver = z3::Solver::new();
        solver.from_string(query.script);
        assert_eq!(solver.check(), z3::SatResult::Unsat);
    }

    #[test]
    fn exporter_supports_existential_decimal_nonlinear_witnesses() {
        let program = compile_text(
            r"mod Export
enum Result:
    Yes

record E:
    left: Decimal 0.0..2.0
    right: Decimal 0.0..2.0

dec d(e E) -> Result

policy::product @product policy:
    A product of two produces Yes.

    rule product(e E):
        e.left * e.right = 2.0 => d(e) = Yes

assert some reachable(e E):
    d(e)
",
        );
        let query = export_invariant_smtlib(&program, "reachable").unwrap();
        assert_eq!(query.metadata.query, "invariant_witness");
        assert_eq!(query.metadata.logic, "QF_NIA");
        let solver = z3::Solver::new();
        solver.from_string(query.script);
        assert_eq!(solver.check(), z3::SatResult::Sat);
    }

    #[test]
    fn exporter_marks_nonlinear_queries_and_rejects_unsupported_theories() {
        let nonlinear = compile_text(
            r"mod Export
enum Result:
    Any

record E:
    left: Decimal 0.0..2.0
    right: Decimal 0.0..2.0

dec d(e E) -> Result

policy::nonlinear @nonlinear policy:
    Nonnegative products produce Any.

    rule any(e E):
        e.left * e.right >= 0 => d(e) = Any

assert total(e E):
    d(e)
",
        );
        let query = export_invariant_smtlib(&nonlinear, "total").unwrap();
        assert_eq!(query.metadata.logic, "QF_NIA");
        assert!(query.script.contains("(set-logic QF_NIA)"));
        assert!(matches!(
            query.symbols[0].encoding,
            SmtSymbolEncoding::DecimalMantissaScale { .. }
        ));

        let unsupported = compile_text(
            r#"mod Export
enum Result:
    Any

record E:
    label: String

dec d(e E) -> Result

policy::string @string policy:
    The yes label produces Any.

    rule any(e E):
        e.label = "yes" => d(e) = Any

assert total(e E):
    d(e)
"#,
        );
        let error = export_invariant_smtlib(&unsupported, "total").unwrap_err();
        assert!(matches!(
            error,
            SmtLibExportError::Unsupported { ref reason, .. }
                if reason.contains("outside the solver arithmetic fragment")
        ));
    }

    #[cfg(unix)]
    #[test]
    fn command_adapter_passes_query_on_stdin_and_arguments_literally() {
        let solver = CommandSmtSolver::new("test", "/bin/sh").unwrap().args([
            OsStr::new("-c"),
            OsStr::new("read line; test \"$line\" = sentinel; printf unsat"),
        ]);
        let result = solver.solve(&query("sentinel\n")).unwrap();
        assert_eq!(result.status, ExternalSolverStatus::Unsat);
    }

    #[cfg(unix)]
    #[test]
    fn command_adapter_times_out_and_rejects_extra_output() {
        let slow = CommandSmtSolver::new("slow", "/bin/sh")
            .unwrap()
            .args([OsStr::new("-c"), OsStr::new("while :; do :; done")])
            .with_timeout(Duration::from_millis(20))
            .unwrap();
        assert!(matches!(
            slow.solve(&query("(check-sat)\n")),
            Err(ExternalSolverError::Timeout { .. })
        ));

        let noisy = CommandSmtSolver::new("noisy", "/bin/sh").unwrap().args([
            OsStr::new("-c"),
            OsStr::new("cat >/dev/null; printf 'sat\\n(model)'"),
        ]);
        assert!(matches!(
            noisy.solve(&query("(check-sat)\n")),
            Err(ExternalSolverError::InvalidStatus { .. })
        ));
    }

    #[cfg(unix)]
    #[test]
    fn command_adapter_enforces_output_limit() {
        let solver = CommandSmtSolver::new("noisy", "/bin/sh")
            .unwrap()
            .args([
                OsStr::new("-c"),
                OsStr::new("cat >/dev/null; printf 123456"),
            ])
            .with_output_limit(3)
            .unwrap();
        assert!(matches!(
            solver.solve(&query("(check-sat)\n")),
            Err(ExternalSolverError::OutputLimitExceeded { .. })
        ));
    }

    #[cfg(unix)]
    #[test]
    fn command_adapter_reports_spawn_exit_utf8_and_stderr_failures() {
        let missing =
            CommandSmtSolver::new("missing", "/definitely/not/a/real/tess-external-solver")
                .unwrap();
        assert!(matches!(
            missing.solve(&query("(check-sat)\n")),
            Err(ExternalSolverError::Spawn { .. })
        ));

        let failed = CommandSmtSolver::new("failed", "/bin/sh").unwrap().args([
            OsStr::new("-c"),
            OsStr::new("cat >/dev/null; printf 'solver failed' >&2; exit 7"),
        ]);
        assert!(matches!(
            failed.solve(&query("(check-sat)\n")),
            Err(ExternalSolverError::UnsuccessfulExit {
                code: Some(7),
                ref stderr,
            }) if stderr == "solver failed"
        ));

        let invalid_stdout = CommandSmtSolver::new("invalid-stdout", "/bin/sh")
            .unwrap()
            .args([
                OsStr::new("-c"),
                OsStr::new("cat >/dev/null; printf '\\377'"),
            ]);
        assert!(matches!(
            invalid_stdout.solve(&query("(check-sat)\n")),
            Err(ExternalSolverError::InvalidUtf8 { ref stream }) if stream == "stdout"
        ));

        let invalid_stderr = CommandSmtSolver::new("invalid-stderr", "/bin/sh")
            .unwrap()
            .args([
                OsStr::new("-c"),
                OsStr::new("cat >/dev/null; printf sat; printf '\\377' >&2"),
            ]);
        assert!(matches!(
            invalid_stderr.solve(&query("(check-sat)\n")),
            Err(ExternalSolverError::InvalidUtf8 { ref stream }) if stream == "stderr"
        ));

        let noisy_stderr = CommandSmtSolver::new("noisy-stderr", "/bin/sh")
            .unwrap()
            .args([
                OsStr::new("-c"),
                OsStr::new("cat >/dev/null; printf sat; printf 123456 >&2"),
            ])
            .with_output_limit(3)
            .unwrap();
        assert!(matches!(
            noisy_stderr.solve(&query("(check-sat)\n")),
            Err(ExternalSolverError::OutputLimitExceeded { ref stream, .. })
                if stream == "stderr"
        ));
    }

    #[cfg(unix)]
    #[test]
    fn unsafe_and_duplicate_query_symbols_are_advisory_rejections() {
        let (program, baseline) = replay_fixture();

        let malformed =
            assert_fake_sat_rejected(&program, &baseline, "sat\n()\n", "omitted symbol");
        assert!(malformed.model.is_none());

        let mut unsafe_query = baseline.clone();
        *primary_encoding_symbol_mut(&mut unsafe_query.symbols[0].encoding) = "bad symbol".into();
        assert_fake_sat_rejected(
            &program,
            &unsafe_query,
            violating_model(&unsafe_query),
            "not a safe simple SMT-LIB symbol",
        );

        let mut duplicate_query = baseline.clone();
        let duplicated = primary_encoding_symbol(&duplicate_query.symbols[0].encoding).to_owned();
        *primary_encoding_symbol_mut(&mut duplicate_query.symbols[1].encoding) = duplicated;
        assert_fake_sat_rejected(
            &program,
            &duplicate_query,
            violating_model(&duplicate_query),
            "is duplicated",
        );
    }

    #[cfg(unix)]
    #[test]
    fn query_metadata_and_field_type_mismatches_never_validate() {
        let (program, baseline) = replay_fixture();

        let mut unknown_invariant = baseline.clone();
        unknown_invariant.invariant = "missing".into();
        assert_fake_sat_rejected(
            &program,
            &unknown_invariant,
            violating_model(&unknown_invariant),
            "unknown assertion",
        );

        let mut wrong_binding = baseline.clone();
        wrong_binding.symbols[0].binding = "other".into();
        assert_fake_sat_rejected(
            &program,
            &wrong_binding,
            violating_model(&wrong_binding),
            "non-assertion binding",
        );

        let mut wrong_entity = baseline.clone();
        wrong_entity.symbols[0].entity = "Other".into();
        assert_fake_sat_rejected(
            &program,
            &wrong_entity,
            violating_model(&wrong_entity),
            "claims record",
        );

        let mut wrong_field = baseline.clone();
        wrong_field.symbols[0].field = "missing".into();
        assert_fake_sat_rejected(
            &program,
            &wrong_field,
            violating_model(&wrong_field),
            "unknown field",
        );

        let mut wrong_type = baseline.clone();
        let enabled = wrong_type
            .symbols
            .iter_mut()
            .find(|symbol| symbol.field == "enabled")
            .unwrap();
        let symbol = primary_encoding_symbol(&enabled.encoding).to_owned();
        enabled.encoding = SmtSymbolEncoding::Int { symbol };
        assert_fake_sat_rejected(
            &program,
            &wrong_type,
            violating_model(&wrong_type),
            "expected Bool",
        );
    }

    #[cfg(unix)]
    #[test]
    fn external_model_numeric_and_enum_bounds_are_rejected() {
        let (program, query) = replay_fixture();
        let mut cases = Vec::<(String, String, &str)>::new();
        for symbol in &query.symbols {
            match &symbol.encoding {
                SmtSymbolEncoding::Int { symbol } => {
                    cases.push((symbol.clone(), "9223372036854775808".into(), "outside i64"));
                }
                SmtSymbolEncoding::DecimalMantissaScale {
                    mantissa_symbol,
                    scale_symbol,
                    ..
                } => {
                    cases.push((
                        mantissa_symbol.clone(),
                        "79228162514264337593543950336".into(),
                        "not representable",
                    ));
                    cases.push((scale_symbol.clone(), "29".into(), "outside 0..28"));
                }
                SmtSymbolEncoding::EnumIndex {
                    symbol, variants, ..
                } => cases.push((symbol.clone(), variants.len().to_string(), "enum index")),
                SmtSymbolEncoding::Bool { .. } => {}
            }
        }
        assert_eq!(cases.len(), 4);
        for (symbol, value, reason) in cases {
            let overrides = BTreeMap::from([(symbol, value)]);
            assert_fake_sat_rejected(
                &program,
                &query,
                violating_model_with(&query, &overrides),
                reason,
            );
        }
    }

    #[cfg(unix)]
    #[test]
    fn incomplete_query_that_replays_as_unknown_is_not_trusted() {
        let (program, mut query) = replay_fixture();
        query.symbols.retain(|symbol| symbol.field != "enabled");
        assert_fake_sat_rejected(
            &program,
            &query,
            satisfying_model(&query),
            "needed additional input",
        );
    }

    #[cfg(unix)]
    #[test]
    fn sat_model_is_accepted_only_after_tess_replay() {
        let (program, query) = replay_fixture();
        let solver = fake_model_solver(violating_model(&query));
        let assessment = solver.solve_and_replay(&program, &query).unwrap();

        assert_eq!(
            assessment.status,
            ExternalSolverAssessmentStatus::CounterexampleValidated
        );
        assert_eq!(assessment.trust, ExternalSolverTrust::TessReplayValidated);
        assert!(assessment.independently_validated());
        let counterexample = assessment.accepted_counterexample().unwrap();
        assert_eq!(counterexample.kind, CounterexampleKind::Undefined);
        let fields = &counterexample.input.bindings["e"].fields;
        assert_eq!(fields["enabled"], Value::Bool(false));
        assert_eq!(fields["count"], Value::Int(2));
        assert_eq!(fields["amount"], Value::decimal(Decimal::new(15, 1)));
        assert_eq!(
            fields["choice"],
            Value::Enum {
                type_name: "Choice".into(),
                variant: "B".into(),
            }
        );
        let encoded = serde_json::to_string(&assessment).unwrap();
        let decoded: ExternalSolverAssessment = serde_json::from_str(&encoded).unwrap();
        assert_eq!(decoded.status, assessment.status);
        assert_eq!(decoded.model, assessment.model);
        assert_eq!(
            decoded.model.unwrap().assignments,
            assessment.model.unwrap().assignments
        );
    }

    #[cfg(unix)]
    #[test]
    fn existential_sat_model_is_accepted_only_after_witness_replay() {
        let program = compile_text(
            r"mod Replay
enum Result:
    Yes

record E:
    x: Int 0..2

dec d(e E) -> Result

policy::yes @yes policy:
    One produces Yes.

    rule yes(e E):
        e.x = 1 => d(e) = Yes

assert some reachable(e E):
    d(e)
",
        );
        let query = export_invariant_smtlib(&program, "reachable").unwrap();
        let symbol = primary_encoding_symbol(&query.symbols[0].encoding).to_owned();

        let valid_model = format!("sat\n(({symbol} 1))\n");
        let assessment = fake_model_solver(valid_model)
            .solve_and_replay(&program, &query)
            .unwrap();
        assert_eq!(
            assessment.status,
            ExternalSolverAssessmentStatus::WitnessValidated
        );
        assert_eq!(assessment.trust, ExternalSolverTrust::TessReplayValidated);
        assert!(assessment.independently_validated());
        assert!(assessment.accepted_counterexample().is_none());
        assert!(assessment.accepted_witness_model().is_some());
        assert!(assessment.counterexample.is_none());
        assert!(assessment.reason.is_none());

        let invalid_model = format!("sat\n(({symbol} 0))\n");
        let rejected = fake_model_solver(invalid_model)
            .solve_and_replay(&program, &query)
            .unwrap();
        assert_eq!(rejected.status, ExternalSolverAssessmentStatus::SatRejected);
        assert!(!rejected.independently_validated());
        assert!(rejected.accepted_witness_model().is_none());
        assert!(
            rejected
                .reason
                .as_deref()
                .is_some_and(|reason| reason.contains("does not satisfy"))
        );

        let mut mismatched = query;
        mismatched.metadata.query = "invariant_violation".into();
        let mismatch = fake_model_solver(format!("sat\n(({symbol} 1))\n"))
            .solve_and_replay(&program, &mismatched)
            .unwrap();
        assert_eq!(mismatch.status, ExternalSolverAssessmentStatus::SatRejected);
        assert!(
            mismatch
                .reason
                .as_deref()
                .is_some_and(|reason| reason.contains("does not match"))
        );

        let unsat = CommandSmtSolver::new("fake", "/bin/sh")
            .unwrap()
            .args([OsStr::new("-c"), OsStr::new("cat >/dev/null; printf unsat")])
            .solve_and_replay(&program, &mismatched)
            .unwrap();
        assert_eq!(unsat.status, ExternalSolverAssessmentStatus::UnsatAdvisory);
        assert_eq!(unsat.trust, ExternalSolverTrust::Advisory);
        assert!(!unsat.independently_validated());
        assert!(unsat.accepted_witness_model().is_none());
    }

    #[cfg(unix)]
    #[test]
    fn existential_implication_replay_rejects_a_false_premise_model() {
        let program = compile_text(
            r"mod Replay
enum Result:
    No

record E:
    x: Int 0..1

dec d(e E) -> Result

policy::false_premise @false premise:
    Only zero produces No.

    rule only_false_premise(e E):
        e.x = 0 => d(e) = No

assert some reachable(e E):
    e.x > 0 => d(e) = No
",
        );
        let query = export_invariant_smtlib(&program, "reachable").unwrap();
        let symbol = primary_encoding_symbol(&query.symbols[0].encoding);
        let assessment = fake_model_solver(format!("sat\n(({symbol} 0))\n"))
            .solve_and_replay(&program, &query)
            .unwrap();
        assert_eq!(
            assessment.status,
            ExternalSolverAssessmentStatus::SatRejected
        );
        assert!(
            assessment
                .reason
                .as_deref()
                .is_some_and(|reason| reason.contains("premise is false"))
        );
    }

    #[test]
    fn witness_assessment_consistency_requires_only_normalized_model_evidence() {
        let mut assessment = coherent_assessment();
        assessment.status = ExternalSolverAssessmentStatus::WitnessValidated;
        assessment.counterexample = None;
        assert!(assessment.validate_consistency().is_ok());
        assert!(assessment.independently_validated());
        assert!(assessment.accepted_witness_model().is_some());
        assert!(assessment.accepted_counterexample().is_none());

        assessment.model = None;
        assert!(assessment.validate_consistency().is_err());
        assert!(assessment.accepted_witness_model().is_none());

        assessment = coherent_assessment();
        assessment.status = ExternalSolverAssessmentStatus::WitnessValidated;
        assert!(assessment.validate_consistency().is_err());
        assessment.counterexample = None;
        assessment.reason = Some("not coherent".into());
        assert!(assessment.validate_consistency().is_err());
        assessment.reason = None;
        assessment.trust = ExternalSolverTrust::Advisory;
        assert!(assessment.validate_consistency().is_err());
    }

    #[cfg(unix)]
    #[test]
    fn sat_model_that_does_not_violate_the_invariant_is_rejected() {
        let (program, query) = replay_fixture();
        let solver = fake_model_solver(satisfying_model(&query));
        let assessment = solver.solve_and_replay(&program, &query).unwrap();

        assert_eq!(
            assessment.status,
            ExternalSolverAssessmentStatus::SatRejected
        );
        assert_eq!(assessment.trust, ExternalSolverTrust::Advisory);
        assert!(!assessment.independently_validated());
        assert!(assessment.accepted_counterexample().is_none());
        assert!(
            assessment
                .reason
                .as_deref()
                .unwrap()
                .contains("does not violate")
        );
    }

    #[cfg(unix)]
    #[test]
    fn unsat_and_unknown_are_advisory_and_do_not_request_models() {
        let (program, query) = replay_fixture();
        let solver = CommandSmtSolver::new("fake", "/bin/sh").unwrap().args([
            OsStr::new("-c"),
            OsStr::new(
                "input=$(cat); case \"$input\" in *'(get-value ('*) exit 9;; *) printf unsat;; esac",
            ),
        ]);
        let assessment = solver.solve_and_replay(&program, &query).unwrap();
        assert_eq!(
            assessment.status,
            ExternalSolverAssessmentStatus::UnsatAdvisory
        );
        assert_eq!(assessment.trust, ExternalSolverTrust::Advisory);
        assert!(!assessment.independently_validated());
        assert!(assessment.model.is_none());
        assert!(assessment.counterexample.is_none());
        assert!(assessment.validate_consistency().is_ok());

        let unknown = CommandSmtSolver::new("fake", "/bin/sh").unwrap().args([
            OsStr::new("-c"),
            OsStr::new(
                "input=$(cat); case \"$input\" in *'(get-value ('*) exit 9;; *) printf unknown;; esac",
            ),
        ]);
        let assessment = unknown.solve_and_replay(&program, &query).unwrap();
        assert_eq!(assessment.status, ExternalSolverAssessmentStatus::Unknown);
        assert_eq!(assessment.solver_status, ExternalSolverStatus::Unknown);
        assert_eq!(assessment.trust, ExternalSolverTrust::Advisory);
        assert!(assessment.validate_consistency().is_ok());
        assert!(!assessment.independently_validated());
        assert!(assessment.model.is_none());
        assert!(assessment.counterexample.is_none());
    }

    #[cfg(unix)]
    #[test]
    fn constant_sat_query_replays_without_an_empty_get_value_request() {
        let program = compile_text(
            r"mod Constant
enum Choice:
    A

dec d() -> Choice

assert total():
    d()
",
        );
        let query = export_invariant_smtlib(&program, "total").unwrap();
        assert!(query.symbols.is_empty());
        let solver = CommandSmtSolver::new("fake", "/bin/sh").unwrap().args([
            OsStr::new("-c"),
            OsStr::new(
                "input=$(cat); case \"$input\" in *'(get-value ('*) exit 9;; *) printf sat;; esac",
            ),
        ]);
        let assessment = solver.solve_and_replay(&program, &query).unwrap();
        assert_eq!(
            assessment.status,
            ExternalSolverAssessmentStatus::CounterexampleValidated
        );
        assert!(assessment.model.unwrap().assignments.is_empty());
    }

    #[cfg(unix)]
    #[test]
    fn replay_model_request_shares_timeout_and_output_limits() {
        let (program, query) = replay_fixture();
        let model = violating_model(&query);
        let slow = CommandSmtSolver::new("slow-model", "/bin/sh")
            .unwrap()
            .args([
                OsString::from("-c"),
                OsString::from(
                    "input=$(cat); sleep 0.25; case \"$input\" in *'(get-value ('*) printf '%s' \"$1\";; *) printf sat;; esac",
                ),
                OsString::from("tess-shared-deadline"),
                OsString::from(&model),
            ])
            .with_timeout(Duration::from_millis(400))
            .unwrap();
        assert!(matches!(
            slow.solve_and_replay(&program, &query),
            Err(ExternalSolverError::Timeout { .. })
        ));

        let noisy = CommandSmtSolver::new("noisy-model", "/bin/sh")
            .unwrap()
            .args([
                OsStr::new("-c"),
                OsStr::new(
                    "input=$(cat); case \"$input\" in *'(get-value ('*) printf 'sat\\n12345678901234567890';; *) printf sat;; esac",
                ),
            ])
            .with_output_limit(8)
            .unwrap();
        assert!(matches!(
            noisy.solve_and_replay(&program, &query),
            Err(ExternalSolverError::OutputLimitExceeded { .. })
        ));

        let limit = model.len() + 20;
        let diagnostic = "x".repeat(limit / 2 + 1);
        let combined = CommandSmtSolver::new("combined-stderr", "/bin/sh")
            .unwrap()
            .args([
                OsString::from("-c"),
                OsString::from(
                    "input=$(cat); case \"$input\" in *'(get-value ('*) printf '%s' \"$1\"; printf '%s' \"$3\" >&2;; *) printf sat; printf '%s' \"$2\" >&2;; esac",
                ),
                OsString::from("tess-combined-stderr"),
                OsString::from(model),
                OsString::from(&diagnostic),
                OsString::from(diagnostic),
            ])
            .with_output_limit(limit)
            .unwrap();
        assert!(matches!(
            combined.solve_and_replay(&program, &query),
            Err(ExternalSolverError::OutputLimitExceeded { ref stream, .. })
                if stream == "combined stderr"
        ));
    }
}