Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation

Ralph Bottesch, Jose Divasón, René Thiemann
Archive of Formal Proofs 2021.

AFP entry

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},
}