Module align 

SMT lowering for the Align safety property.

This module reduces:

Align(p, T)

to the common SMT obligation:

Aligned { place: p, align: align_of(T) }

The common model then proves the obligation by asking whether the path facts plus the negated alignment goal are satisfiable.

Functions

check 🔒

Check Align by lowering it to SmtObligation::Aligned.

check_for_checkpoint 🔒

Check Align at a return checkpoint for struct invariant verification.