Title: Logics for low-level code and proof-preserving program transformations