Abstract

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.

BibTeX

@article{Modular_arithmetic_LLL_and_HNF_algorithms-AFP,
  author  = {Ralph Bottesch and Jose Divasón and René Thiemann},
  title   = {Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation},
  journal = {Archive of Formal Proofs},
  month   = mar,
  year    = 2021,
  note    = {\url{https://isa-afp.org/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html},
            Formal proof development},
  ISSN    = {2150-914x},
}