Verified Translation Between Purely Functional and Imperative Domain Specific Languages in HELIX