cpp-to-dafny-translator
Installation
SKILL.md
C++ → Dafny Translator
This is a delta over → python-to-dafny-translator — the Dafny target is the same; the source is harder. C++ brings three problems Python doesn't: fixed-width integers (overflow), pointers (aliasing), and manual memory (lifetime).
The C++-specific impedance mismatch
| C++ has | Dafny needs | Translation |
|---|---|---|
int32_t, uint64_t — wraps |
bv32, bv64 — modular; or int — unbounded |
Choose: proving no-overflow → int + ensures in-range. Modeling actual wrap → bv. |
T* pointer |
array<T> + index, or class ref |
Decompose: a pointer is (base array, offset). Verify offset in bounds. |
T& ref |
inout param or direct object access |
Dafny params are value by default — use class fields for mutation |
new/delete |
new (garbage-collected, no delete) |
Drop delete. If use-after-free is the property you're proving, you need a ghost lifetime tracker. |
Pointer arithmetic p + n |
a, i+n on the (array, index) pair |
Stays in bounds? That's a proof obligation. |
reinterpret_cast |
Nothing | Refuse. If the algorithm relies on type punning, Dafny is the wrong tool. |
| Templates | Generics <T> |
Usually direct; constraints become T extends Trait |
std::vector<T> |
seq<T> (value semantics) or array<T> (ref) |
seq if you're not mutating through aliases |
| Undefined behavior | Dafny has none | Every UB in C++ becomes a requires clause — that's the point |