Coq embedding of Rosette’s solver aided language inspired by smten.
Factors proof into two parts with SpaceSearch ADT as the interface between the two.
- Coq proof (interactive) - can use induction, coinduction, higher order, etc.
- Rosette proof (automatic) - limited to first order.
- verifying RockSalt against STOKE
- verifying Bagpipe