Abstraction mechanisms

• Parameterized modules
  • Finite maps, RegFile, Word
  • Can plug in different implementations without invalidating the proof
• Marking definitons as abstract
  • Memory, Addr, and related functions
• Deforestation
  • Alg, Code