This requires some alignment information, but presumably makes deductive verification easier (and allows more precise static analysis)