2.7. Key Insight: Macros as Verified Abstractions

From the paper: "Such definitions really shine when proving correctness of machine code programs using our separation logic framework, as we can give derived Hoare-style proof rules for the macros."

The assembler isn't just about generating bytes—it's about building verified building blocks that compose with proofs.