[touisteur]

From experience with these kinds of specs, one might be better off clearly stating things that are left to the compiler implementation (and thus should have no impact -?-on the verifiability of the spec).