Modular Arithmetic Hardware models inevitably need modular arithmetic Common Lisp integers are, by nature, bignums Compiler declarations can suggest 32-bit operations coerce might be a better word Results in efficient 32-bit modular operation ACL2 is faithful to Common Lisp representations Declarations can still be used to suggest 32-bit operations Declarations result in guard conditions that must be proved