Two Algorithms Based on Modular Arithmetic: Lattice Basis Reduction and Hermite Normal Form Computation

Ralph Bottesch, Jose Divasón 🌐 and René Thiemann 📧

March 12, 2021

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We verify two algorithms for which modular arithmetic plays an essential role: Storjohann's variant of the LLL lattice basis reduction algorithm and Kopparty's algorithm for computing the Hermite normal form of a matrix. To do this, we also formalize some facts about the modulo operation with symmetric range. Our implementations are based on the original papers, but are otherwise efficient. For basis reduction we formalize two versions: one that includes all of the optimizations/heuristics from Storjohann's paper, and one excluding a heuristic that we observed to often decrease efficiency. We also provide a fast, self-contained certifier for basis reduction, based on the efficient Hermite normal form algorithm.


BSD License


Session Modular_arithmetic_LLL_and_HNF_algorithms