warp-types¶
Linear typestate for GPU warp divergence: compile-time prevention of shuffle-from-inactive-lane bugs.
Status: v0.3.2 on crates.io. Nelson-Oppen SMT combination (QF_UFBV) shipped.
Repository: github.com/modelmiser/warp-types
What it is¶
A Rust type system that makes GPU divergence bugs into compile errors. When a warp diverges (some lanes take one branch, others take the other), shuffles and reductions become unsafe — reading from an inactive lane is undefined behavior. warp-types encodes the divergence state in the type system so the compiler rejects these bugs before they reach the GPU.
Blog posts¶
- Intervals Collapse to Points — what happens to formal verification when the hardware is deterministic
- Neither Theory Alone — an SMT solver with one theory is a SAT solver with opinions. Add a second theory and you need a protocol for disagreement
- One Oracle, Four Products — a SAT solver answers one question: is this set of clauses satisfiable? Four crates — the solver itself, a bounded model checker, an SMT solver, and a property-directed reachability engine — are built on that question, each posing it differently