I have never really used it.
If I need to do it, I may try something as follows:
Say, ptr_get reads a value of type T from a given pointer:
extern
fun ptr_get{l:addr} (pf: !T @ l | p: ptr(l)): T
If I need to make sure that the given pointer is well-aligned, I can use the following
interface for ptr_get:
extern
fun ptr_get{l:addr} (pf: !T @ l, pf2: is_aligned(l) | p: ptr(l)): T
where is_aligned is an abstract prop:
absprop is_aligned (l:addr).
Run-time checks can be added to get a proof for the 'is_aligned' predicate.