# BACKLOG - writ
Hand-verified findings (Claude deep review 2026-07-13). Format: number | affected files | problem | acceptance criteria.
DONE 2026-07-14 | dedup | high | `try_trivial_witness` (the crate's single sink-kind -> witness dispatcher) has ZERO callers repo-wide; the sole consumer `surge/surgec/src/scan/findings/proof_assembly.rs:219-247` re-implements the exact same match by calling the individual `writ::*_witness` fns directly, so there are two divergent dispatch tables for the same mapping. | PARTIAL: try_trivial_witness now HAS a caller (Z3Backend::witness routes Class-1 shapes through it, see z3_backend.rs:59), so the "zero callers" half is resolved. The remaining half (surgec still re-implements the match rather than calling try_trivial_witness) needs a surgec refactor to build a WitnessRequest+ShapeParams from the Finding (surgec passes DEFAULT_CAPACITY directly to individual fns today). Left open for that surgec-side unification. | status=done | TURNKEY MAPPING (derived 2026-07-14 by reading proof_assembly.rs:215-250 - do this in a focused surgec pass with surgec's heavy/CUDA build loaded, since it changes exploit-witness generation): surgec's `SinkClass` -> writ's `SinkConstraintKind` + `ShapeParams`: StackOverflowStrcpy->StackOverflowStrcpy+StackOverflow{dst_capacity:DEFAULT_CAPACITY}; StackOverflowSprintf->StackOverflowSprintfUnbounded+StackOverflow{DEFAULT_CAPACITY}; Gets->StackOverflowGets+StackOverflow{DEFAULT_CAPACITY}; FormatString->FormatStringUserControlled (no params); HeapOverflowAllocArithWraps->HeapOverflowAllocArithWraps+AllocArithWraps{DEFAULT_STRUCT_SIZE,DEFAULT_PTR_WIDTH}; **HeapOverflowOffByOne->HeapOverflowAllocArithWraps+AllocArithWraps{struct_size:2,DEFAULT_PTR_WIDTH}** (surgec's off-by-one trick: struct_size=1 returns None so it uses 2); **OobWriteIndex AND OobReadIndex both->OobWriteUnboundedIndex+OobWriteIndex{DEFAULT_CAPACITY,signed:false,DEFAULT_INDEX_WIDTH=4}** (read reuses the write payload; ASan signature differs, bytes identical). CAVEAT that makes this non-trivial: writ's try_trivial_witness returns a full writ::ConcreteInput, but surgec's fn takes `raw` from the individual *_witness fns and re-wraps it in its OWN ConcreteInput{...} with extra context - confirm whether surgec's ConcreteInput == writ::ConcreteInput (re-export) or a distinct type before rerouting, and preserve surgec's post-wrap fields. writ's SinkConstraintKind must already expose all these variants (it does: Strcpy/SprintfUnbounded/Gets/AllocArithWraps/OobWriteUnboundedIndex/FormatStringUserControlled) - note there is NO dedicated OffByOne/OobRead variant, they intentionally fold onto AllocArithWraps/OobWrite, so the mapping lives on the surgec side. | FIXED: added `writ::classify_primitive` as the ONE-PLACE owner of the sink-kind/primitive dispatch table (with default `ShapeParams`). `surgec/src/scan/findings/proof_assembly.rs` now delegates to `writ::classify_primitive` instead of re-implementing the same `if/else` chain. `surgec` `cargo check` and `cargo test --lib sink_kind_from_primitive_delegates_to_writ` pass (CARGO_EXIT=0).
src/z3_backend.rs:63 | perf | medium | `Z3Backend::witness` constructs a `z3::Config`, `z3::Context`, `z3::Solver`, `z3::Params` and calls `solver.push()` on EVERY call, then discards all of it and unconditionally returns `Unsupported` — the solver is never queried. Expensive C++ allocation for a guaranteed no-op. | FIXED: witness() no longer builds any z3 Config/Context/Solver/Params. It routes Class-1 shapes through try_trivial_witness (see :59) and otherwise computes only the adapter string for the Unsupported message. Solver construction is deferred to when a real encoder dispatch exists. | status=done
src/z3_backend.rs:59 | capability | medium | `Z3Backend::witness` never consults `try_trivial_witness`, so a caller holding only the `WitnessProvider` trait object gets `Unsupported` even for `StackOverflowStrcpy`/`Gets`/`FormatString` shapes that HAVE working closed-form witnesses. The implemented Class-1 surface is unreachable through the trait. | FIXED: witness() now begins with `if let Some(concrete) = crate::try_trivial_witness(request) { return WitnessOutcome::Witnessed(concrete); }`, so all Class-1 closed-form shapes are reachable through the trait object; solver-required shapes still fall through to Unsupported. | status=done
src/sink_payloads.rs:103 | bug | medium | `stack_overflow_witness`: `let total_len = dst_capacity + CANARY_PADDING;` then `vec![b'A'; total_len]` with NO overflow/size guard. A large `dst_capacity` wraps in release (silent short witness) or panics in debug, then can OOM. Sibling `alloc_arith_wraps_witness` explicitly guards this exact class (lines 226, 270). | FIXED: stack_overflow_witness / sprintf_unbounded_witness / gets_witness now return Option<ConcreteInput>; use checked_add(CANARY_PADDING) and reject total_len > MAX_WITNESS_BYTES (64 MiB — beyond any real stack buffer). try_trivial_witness call sites drop the Some() wrappers; surgec proof_assembly.rs adds `?` (already returns Option; DEFAULT_CAPACITY=64 always succeeds so behavior unchanged). Proving test stack_overflow_witness_refuses_capacity_that_overflows_or_exceeds_cap (usize::MAX, cap boundary). | status=done
VERIFICATION NOTE 2026-07-13: writ has no clean standalone build (it inherits root workspace.package + vyre workspace-deps but is intentionally not a root member — see root Cargo.toml lines 30-35, blocked on the vyre-tree fold). Verified my changes via the SURGE workspace instead (it consumes writ as a path-dep): `cargo check -p writ` exit 0; `cargo test -p writ --lib --test sink_payloads_extended` = 20 + 12 passed (all new proving tests green); z3_backend compiles under `--features writ/z3-backend`. surgec proof_assembly.rs `?` change: correct by construction (fn already returns Option and uses `?` on sibling calls; DEFAULT_CAPACITY=64 always succeeds); full `cargo check -p surgec` OOM-killed sccache/rustc on heavy GPU deps (spirv/hexf-parse) — an env memory limit, not a compile error in the change. The earlier root-Cargo.toml workspace.exclude attempt was REVERTED (it broke writ's `workspace=true` inheritance); root Cargo.toml is unchanged.
src/sink_payloads.rs:127 | dedup | medium | `gets_witness` hardcodes the literal `dst_capacity + 16` in its `render` string instead of reusing `CANARY_PADDING`; the bytes come from `stack_overflow_witness` (which uses the const). If `CANARY_PADDING` changes, the byte length and the render command silently disagree. | FIXED: CANARY_PADDING hoisted to a single module-scope const (ONE-PLACE); gets_witness/stack_overflow_witness/sprintf_unbounded_witness all reference it. gets_witness render now uses `dst_capacity + CANARY_PADDING`. Proving test gets_witness_render_matches_stack_overflow_bytes ties render count to bytes.len() across capacities incl 0/1. | status=done
src/sink_payloads.rs:166 | test-gap | medium | `sprintf_unbounded_witness` render pipes `python3 ... stdout.write("A"*N) | xargs -I{} ./victim '{}'`; no test asserts the render is a valid shell command or that bytes length == dst_capacity+16. Existing tests likely assert only shape. | FIXED: proving test sprintf_unbounded_render_byte_count_matches_bytes asserts bytes.len()==dst_capacity+CANARY_PADDING AND render contains the exact `"A" * {total}` count across capacities [0,1,64,4096] incl boundaries. | status=done
src/z3_backend.rs:66 | bug | low | `solver.push()` is called with no matching `pop()` and the solver is immediately dropped — dead call that signals a scope that never materializes. | FIXED: entire solver/params/push block removed with the :63 rewrite; witness() no longer touches z3 at all until an encoder dispatch exists. | status=done
DONE 2026-07-14 Cargo.toml:29 | deps | low | `z3 = { version = "0.12", optional = true }` — z3 crate 0.12 is behind current (0.13+ line exists with updated libz3 bindings). Verify against `cargo outdated`; a bump may be needed before the encoders land. | FIXED: bumped `z3` from `0.12` to `0.13` in `libs/symbolic/writ/Cargo.toml`. `cargo +1.92.0 check -p writ` in the `surge/` workspace OK; `cargo +1.92.0 test -p writ --lib --test sink_payloads_extended` 32 passed (CARGO_EXIT=0); `cargo +1.92.0 check -p surgec` OK. | status=done