santh-writ 0.1.1

//! `writ`  -  CPU symbolic execution and exploit witness construction.
//!
//! A writ is a written compulsion of evidence. This crate produces
//! exactly that: given a source→sink path proven by `weir`, it
//! synthesizes a concrete input that drives execution along the path
//! and triggers the attacker constraint at the sink. The output is a
//! Class 1 finding for surgec  -  not "I think there's a SQL injection
//! here" but "here is the curl command that triggers it."
//!
//! `writ` is a wrapper around vyre  -  it consumes vyre IR and weir
//! paths. It is **not** part of the `vyre-*` namespace. The companion
//! GPU-resident wrapper is `scry`, which lives in a separate crate so
//! CPU primitives cannot leak into the GPU code path. See
//! `vyre/VISION.md` "The wrapper namespace and its closed-set rule."
//!
//! ## Architecture
//!
//! Surgec consumes `WitnessProvider` (the trait). Backends register
//! themselves under feature flags:
//!
//! ```text
//! WitnessProvider trait
//!     ↓
//! Z3Backend (cfg(feature = "z3-backend"), the default)
//!     ↓
//! z3 crate → libz3 (system C++ library)
//! ```
//!
//! Future backends (`cvc5`, `bitwuzla`) plug in behind the same trait
//! the same way. The GPU-resident equivalent lives in `scry` and
//! satisfies the same trait while sharing zero implementation code.
//!
//! ## What's implemented today
//!
//! - The `WitnessProvider` trait surface
//! - `WitnessRequest` / `WitnessOutcome` / `ConcreteInput` types
//! - `SinkConstraintKind` enum  -  SQLi / cmd-injection / SSRF / XXE /
//!   path-traversal / deserialization / template-injection (the
//!   sink-payload library is one TOML per kind, parsed at runtime)
//! - Z3 backend skeleton: opens a `z3::Solver`, declares free
//!   variables for path-input bytes, encodes a placeholder constraint,
//!   solves, returns the model
//!
//! ## What's not implemented yet (deliberately, by scope)
//!
//! - Per-language statement→SMT encoders (one per language: C, Python,
//!   JS, Go, Java, Ruby, PHP, Kotlin, Swift, C#). Each is its own
//!   substantial body of work; lands in subsequent sessions.
//! - The full sink-payload TOML library
//! - Concolic fallback for paths longer than the symbolic budget
//! - Input rendering (SMT model → curl command / JSON body / argv)

#![forbid(unsafe_code)]
#![deny(missing_docs)]

/// Identifies which sink class a witness must satisfy. Each kind has
/// a TOML in `rules/sinks/<kind>.toml` declaring the exploit
/// constraint shape (e.g. for SQLi: "the value reaching the sink
/// contains an unquoted SQL operator that escapes the surrounding
/// string literal").
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum SinkConstraintKind {
    /// Untrusted value reaches a SQL `execute` / `query` / `exec` sink.
    SqlInjection,
    /// Untrusted value reaches a shell `system` / `exec` / `popen` sink.
    CommandInjection,
    /// Untrusted URL or host reaches an HTTP-fetch sink.
    Ssrf,
    /// Untrusted XML reaches a parser with external-entity processing.
    Xxe,
    /// Untrusted path reaches a filesystem sink.
    PathTraversal,
    /// Untrusted bytes reach a deserializer that constructs gadget chains.
    Deserialization,
    /// Untrusted value reaches a template renderer.
    TemplateInjection,
    /// Untrusted value reaches a code-evaluation sink (`eval`, `Function`).
    CodeInjection,

    // ── Launch memory-corruption shapes (Class 1, closed-form witness) ──
    /// Attacker bytes reach `strcpy` / `strcat` / equivalent unbounded
    /// copy targeting a stack-resident destination of fixed capacity.
    StackOverflowStrcpy,
    /// Attacker bytes reach `sprintf` / `vsprintf` writing into a
    /// stack-resident destination of fixed capacity (no length arg).
    StackOverflowSprintfUnbounded,
    /// Attacker bytes reach `gets` reading into a stack buffer.
    StackOverflowGets,
    /// Attacker-controlled count multiplied by a struct size wraps
    /// the integer result and produces an undersized allocation.
    HeapOverflowAllocArithWraps,
    /// Attacker-controlled index reaches an indexed store with no
    /// capacity check (`buf[i] = ...` where `i` is unbounded).
    OobWriteUnboundedIndex,
    /// Attacker-controlled bytes flow into a `printf`-class format
    /// argument; a `%n` chain yields an arbitrary-write primitive.
    FormatStringUserControlled,
}

/// Per-shape parameters that the trivial-encoder needs from the rule's
/// path-bound variables. Surgec populates this from `weir`'s slot
/// extraction at proof-assembly time. None for shapes that don't take
/// shape-specific parameters.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum ShapeParams {
    /// Stack-overflow shapes (strcpy / sprintf / gets) take a single
    /// destination capacity in bytes. The witness emits a payload of
    /// `dst_capacity + canary_padding` bytes to clobber the saved
    /// frame pointer + return address.
    StackOverflow {
        /// Destination buffer's static capacity in bytes (i.e.
        /// `sizeof(dst)` from the rule's path-bound variable).
        dst_capacity: usize,
    },
    /// Heap-overflow alloc-arith-wraps shape. `struct_size` is the
    /// per-element size used as the multiplicand; `ptr_width_bytes`
    /// distinguishes 32-bit from 64-bit pointer arches (each wraps
    /// at a different threshold).
    AllocArithWraps {
        /// Per-element struct size used as the multiplicand in
        /// `count * struct_size`.
        struct_size: usize,
        /// Pointer-width of the target architecture in bytes
        /// (4 for 32-bit, 8 for 64-bit). Determines the modulus
        /// at which the multiplication wraps.
        ptr_width_bytes: usize,
    },
    /// OOB-write shape. `capacity` is the array length; `signed` is
    /// true when the index variable is signed (negative-index
    /// variant); `index_width_bytes` is the width of the index slot
    /// in the sink's ABI (commonly 4 for `int` / 8 for `size_t` /
    /// `ssize_t`). On 64-bit Linux a `size_t` index slot reads 8
    /// bytes; emitting only 4 bytes would leave the upper word
    /// uninitialized and yield the wrong index.
    OobWriteIndex {
        /// Static array length the indexed store believes it has.
        capacity: usize,
        /// `true` if the index variable's type is signed (`int`,
        /// `ssize_t`); `false` for unsigned indices. Signed indices
        /// admit the negative-index variant.
        signed: bool,
        /// Width of the index slot in bytes (4 for `int` /
        /// `unsigned`, 8 for `size_t` / `ssize_t` on 64-bit Linux).
        /// The witness encodes the index as a little-endian integer
        /// of this exact width.
        index_width_bytes: usize,
    },
}

/// A request to synthesize an exploit witness. Built by surgec from a
/// weir path + a rule's declared sink kind.
#[derive(Debug, Clone)]
pub struct WitnessRequest {
    /// The path source location, addressed by file + byte offset.
    pub source: PathLocation,
    /// The path sink location.
    pub sink: PathLocation,
    /// The intermediate statements weir traversed to connect source to sink.
    /// Each entry is a serialized vyre `Node` describing one statement
    /// (assignment, branch, call, etc.) along with the language adapter
    /// that produced it. Encoders dispatch on the adapter.
    pub statements: Vec<PathStatement>,
    /// Which exploit class the witness must satisfy at the sink.
    pub sink_kind: SinkConstraintKind,
    /// Optional per-shape parameters extracted from the rule's
    /// bound variables (e.g., destination capacity for stack-overflow
    /// shapes). The trivial encoders consume these directly.
    pub shape_params: Option<ShapeParams>,
}

/// One statement on a weir path.
#[derive(Debug, Clone)]
pub struct PathStatement {
    /// Source-language adapter id (e.g. `"py-3.11"`, `"c-c11"`).
    pub adapter: String,
    /// Serialized vyre IR for this statement. Encoders parse and lower.
    pub vyre_node: Vec<u8>,
    /// Source location for traceback in the witness output.
    pub location: PathLocation,
}

/// File + byte-range location.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct PathLocation {
    /// Repository-relative file path.
    pub file: String,
    /// Starting byte offset.
    pub byte_start: u32,
    /// Ending byte offset.
    pub byte_end: u32,
}

/// The output of a successful witness construction.
#[derive(Debug, Clone)]
pub struct ConcreteInput {
    /// Bytes the user can feed to the program to trigger the path.
    /// For HTTP entrypoints this is a fully-formed request body.
    /// For CLI entrypoints, an argv joined by `\0`.
    /// For file-input entrypoints, the file contents.
    pub bytes: Vec<u8>,
    /// Human-renderable form (curl command, repro script).
    pub render: String,
    /// Which entrypoint kind this input is shaped for.
    pub entrypoint_kind: EntrypointKind,
}

/// Categorizes how the input is delivered to the program.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum EntrypointKind {
    /// HTTP request body / query string / header.
    Http,
    /// CLI argv.
    Cli,
    /// File contents read by the program.
    File,
    /// Environment variable.
    EnvVar,
    /// RPC call body (gRPC, JSON-RPC).
    Rpc,
}

/// Outcome of a witness attempt.
#[derive(Debug, Clone)]
pub enum WitnessOutcome {
    /// Witness constructed. Ship as Class 1 finding.
    Witnessed(ConcreteInput),
    /// SMT solver returned UNSAT  -  no input drives this exact path with
    /// the requested sink constraint. The Class 2 path proof is still
    /// valid; this just means no Class 1 upgrade is available.
    Unsat,
    /// Path contains constructs the encoder doesn't yet support.
    /// Surgec keeps the Class 2 finding; a future encoder upgrade may
    /// upgrade this same path to Class 1 without rule changes.
    Unsupported(String),
    /// The solver hit a budget limit (time / memory). Path remains
    /// Class 2; concolic fallback may upgrade in a separate pass.
    BudgetExhausted,
}

/// The trait surgec consumes. Both `writ` (CPU/Z3) and `scry` (GPU/
/// vyre-native) implement this  -  surgec is backend-agnostic.
pub trait WitnessProvider: Send + Sync {
    /// Attempt to construct a concrete input that drives execution
    /// along the path and triggers the sink constraint.
    fn witness(&self, request: &WitnessRequest) -> WitnessOutcome;

    /// Identifier for this backend. Logged in finding metadata so
    /// users can audit which provider produced each witness.
    fn backend_id(&self) -> &'static str;
}

/// Per-sink-class trivial witness encoders. Ships the closed-form
/// witnesses for stack-overflow / gets / format-string shapes  - 
/// shapes whose witness is mechanically derivable from path-bound
/// variables without an SMT solver. Other sink kinds route through
/// the Z3 backend.
pub mod sink_payloads;
pub use sink_payloads::{
    alloc_arith_wraps_witness, classify_primitive, format_string_witness, gets_witness,
    oob_write_index_witness, sprintf_unbounded_witness, stack_overflow_witness,
    try_trivial_witness,
};

#[cfg(feature = "z3-backend")]
pub mod z3_backend;
#[cfg(feature = "z3-backend")]
pub use z3_backend::Z3Backend;