Formalizing Coppersmith's Method

We formalize Coppersmith's method, an algorithm for finding small (in magnitude) roots of univariate integer polynomials mod M. Coppersmith's method has important applications in cryptography and is used in various attacks on the RSA algorithm for public-key cryptography. We also formalize a related (more lightweight) result with slightly weaker bounds; we split out the generic mathematical results underlying both this lightweight result and Coppersmith's method into a dedicated locale, which could be used to prove other "Coppersmith-like" results. Our work builds on the existing formalization of the Lenstra–Lenstra–Lovász (LLL) algorithm for lattice basis reduction, and our formalization adds a determinant bound on the length of the short vector produced by the LLL algorithm.