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


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