### 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.

### License

BSD License

### Topics

- Computer science/Algorithms/Mathematical

### Session Modular_arithmetic_LLL_and_HNF_algorithms

- Matrix_Change_Row
- Signed_Modulo
- Storjohann_Mod_Operation
- Storjohann
- Storjohann_Impl
- Uniqueness_Hermite
- Uniqueness_Hermite_JNF
- HNF_Mod_Det_Algorithm
- HNF_Mod_Det_Soundness
- LLL_Certification_via_HNF

### Depends on

- Hermite Normal Form
- Matrices, Jordan Normal Forms, and Spectral Radius Theory
- A verified LLL algorithm
- Haskell’s Show Class in Isabelle/HOL
- A verified algorithm for computing the Smith normal form of a matrix

## Cite

×

Modular_arithmetic_LLL_and_HNF_algorithms-AFP

    @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   = {March},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Mar 14, 2021 : Isabelle2021