santh-writ 0.1.1

//! Z3-backed `WitnessProvider` implementation.
//!
//! This module is the wiring between the language-neutral
//! `WitnessRequest` and the Z3 SMT solver. Per-language statement
//! encoders live in `writ::encode::<lang>` (forthcoming, one file per
//! language). Today this module exposes the backend struct and the
//! solver setup; encoders register themselves via `inventory` once
//! they exist.
//!
//! ## Why this is intentionally minimal today
//!
//! Real Class 1 witness production requires per-language statement→SMT
//! encoders, each a non-trivial body of work (the AST shape varies per
//! language, the type system varies, the standard-library effect
//! summaries vary). The right move is to wire the SMT plumbing now so
//! later sessions can grow encoders without reshaping the trait
//! surface, not to fake an encoder that only handles two statement
//! kinds.
//!
//! Until per-language encoders land, `Z3Backend::witness` returns
//! `Unsupported` for every request. That is the truthful answer:
//! we have the SMT plumbing but not the encoders. This is not a
//! stub  -  surgec consults the outcome and keeps the Class 2 finding;
//! when an encoder lands the same path becomes Class 1.

use crate::{WitnessOutcome, WitnessProvider, WitnessRequest};

/// Z3-backed witness provider. Default backend; surgec can swap it for
/// any other `WitnessProvider` (future `cvc5_backend`, future
/// `scry::GpuBackend`).
pub struct Z3Backend {
    /// SMT solver budget in milliseconds. Path-symbolic solving is
    /// usually milliseconds; we cap to avoid runaway on pathological
    /// path constraints.
    pub timeout_ms: u32,
}

impl Z3Backend {
    /// Construct with default 5-second per-witness budget.
    #[must_use]
    pub fn new() -> Self {
        Self { timeout_ms: 5_000 }
    }

    /// Construct with an explicit per-witness time budget.
    #[must_use]
    pub fn with_timeout(timeout_ms: u32) -> Self {
        Self { timeout_ms }
    }
}

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

impl WitnessProvider for Z3Backend {
    fn witness(&self, request: &WitnessRequest) -> WitnessOutcome {
        // Class-1 shapes (stack overflow / gets / sprintf / format string /
        // alloc-arith / oob-write) have closed-form witnesses that need no
        // solver. Route them through the trivial encoder first so a caller
        // holding only the `WitnessProvider` trait object can reach the
        // implemented Class-1 surface instead of always getting `Unsupported`.
        if let Some(concrete) = crate::try_trivial_witness(request) {
            return WitnessOutcome::Witnessed(concrete);
        }

        // Solver-required shapes (SQLi / command injection / SSRF / ...) need
        // per-language statement→SMT encoders that have not landed yet. We do
        // NOT construct a `z3::Context`/`Solver` here: it would be built with
        // C++ allocation and immediately discarded on every call for a
        // guaranteed no-op. The `timeout_ms` budget is applied once the encoder
        // dispatch that actually queries the solver exists.
        let adapter = request
            .statements
            .first()
            .map(|s| s.adapter.as_str())
            .unwrap_or("<empty path>");

        WitnessOutcome::Unsupported(format!(
            "writ::z3_backend has no encoder registered for adapter `{adapter}`. \
             Per-language encoders land in subsequent sessions; the path remains \
             Class 2 with full proof bundle."
        ))
    }

    fn backend_id(&self) -> &'static str {
        "writ-z3"
    }
}