A Compositional Natural Semantics and Hoare Logic for Low-Level Languages