santh-writ 0.1.1

CPU symbolic execution + exploit witness construction. Takes a weir-produced source→sink path and returns a concrete input that drives execution to the sink. Z3-backed.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47

# writ  -  CPU symbolic execution + exploit witness construction

> **Internal Santh tooling.** `writ` is the symbolic-execution backend for
> surgec and depends on workspace-internal crates (`weir`, `vyre`). It is not
> published to crates.io and has no supported use outside the Santh workspace.

`writ` upgrades a Class 2 finding (path proven by `weir`) into a Class 1 finding (concrete exploit input that triggers the path). Z3-backed today; future backends (`cvc5`, `bitwuzla`) plug in behind the same `WitnessProvider` trait.

## Architecture

```
weir::Path  +  SinkConstraintKind   →   WitnessRequest
                                        ↓
                                   WitnessProvider
                                        ↓
                          ┌─────────────┴─────────────┐
                          ↓                           ↓
                   writ::Z3Backend            scry::GpuBackend (future)
                   (CPU, libz3)               (GPU, vyre-native research)
                          ↓                           ↓
                   ConcreteInput               ConcreteInput
                          ↓                           ↓
                          └─────── Class 1 finding ───┘
```

`writ` is the **CPU** wrapper. The GPU equivalent (`scry`) lives in a separate crate so CPU primitives never leak into GPU code paths. Both satisfy the same trait; surgec is backend-agnostic.

## Status

- ✅ `WitnessProvider` trait surface
- ✅ `WitnessRequest` / `WitnessOutcome` / `ConcreteInput` types
- ✅ `SinkConstraintKind` enum (8 launch sink classes)
- ✅ `Z3Backend` plumbing  -  opens solver, sets time budget
- ⏳ Per-language statement→SMT encoders (one per language; lands in subsequent sessions)
- ⏳ Sink-payload TOML library (one TOML per `SinkConstraintKind`)
- ⏳ Input rendering (SMT model → curl command / argv / file content)
- ⏳ Concolic fallback for paths exceeding the symbolic budget

Until the encoders land, `Z3Backend::witness` returns `Unsupported(...)` for every request. That is the truthful answer: the SMT plumbing is wired, the encoders are not. Surgec consults the outcome and keeps the Class 2 finding; future encoder additions upgrade existing paths to Class 1 without any rule changes.

## Why CPU first

The library is real and ships in days, not quarters. GPU symbolic execution (`scry`) is a multi-quarter research project. We launch on `writ`; `scry` is a moat-extension that arrives later without changing the surface surgec consumes.

## License

MIT  -  same as the rest of the Santh workspace.