Modular Arithmetic : Solutions JEM1 solution : dual mode Define a +<32> operator ACL2 : logical implementation satisfies guards GCL : "under-the-hood" replacement of +<32> Optimal solution : ACL2 support Have ACL2 provide built-in pre-optimized modular operators