\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{xspace}


% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}


\newcommand\isafor{\textsf{IsaFoR}}
\newcommand\ceta{\textsf{Ce\kern-.18emT\kern-.18emA}}
\newcommand\rats{\mathbb{Q}}
\newcommand\ints{\mathbb{Z}}
\newcommand\reals{\mathbb{R}}
\newcommand\complex{\mathbb{C}}

\newcommand\GFpp[1]{\ensuremath{\text{GF}(#1)}}
\newcommand\GFp{\GFpp{p}}
\newcommand\ring[1][p^k]{\ensuremath{\ints/{#1}\ints}\xspace}
\newcommand\tint{\isa{int}}
\newcommand\tlist{\isa{list}}
\newcommand\tpoly{\isa{poly}}
\newcommand\tto{\Rightarrow}
\newcommand\sqfree{\isa{square\_free}\xspace}
\newcommand\norm[1]{|\!|#1|\!|}
\newcommand\sqnorm[1]{\norm{#1}^2}
\newcommand\lemma{\isakeyword{lemma}\xspace}
\newcommand\assumes{\isakeyword{assumes}\xspace}
\newcommand\idegree{\isa{degree}}
\newcommand\iand{\isakeyword{and}\xspace}
\newcommand\shows{\isakeyword{shows}}
\newcommand\bz{\isa{berlekamp\_zassenhaus\_factorization}\xspace}
\newcommand\fs{\mathit{fs}}
\newcommand\listprod{\isa{prod\_list}}
\newcommand\set{\isa{set}}
\newcommand\irred{\isa{irreducible}}
\newcommand\rTH[1]{Theorem~\ref{#1}}
\newcommand\base[1]{(#1_0,\ldots,#1_{n-1})}
\newcommand\Base[2][m]{{#2}_0,\ldots,{#2}_{#1-1}}

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}

\newtheorem{theorem}{Theorem}

\begin{document}

\title{A verified LLL algorithm\footnote{Supported by FWF (Austrian Science Fund) project Y757.
Jose Divas\'on is partially funded by the
Spanish project MTM2017-88804-P.}}
\author{Ralph Bottesch \and
  Jose Divas\'on \and
  Maximilian Haslbeck \and
  Sebastiaan Joosten \and
  Ren\'e Thiemann \and
  Akihisa Yamada}
\maketitle


\begin{abstract}
The Lenstra\textendash{}Lenstra\textendash{}Lov\'asz basis reduction algorithm, 
also known as LLL algorithm, is an algorithm 
to find a basis with short, nearly orthogonal vectors of an integer lattice. 
Thereby, it can also be seen as an approximation to solve the shortest vector problem (SVP), 
which is an NP-hard problem, where the approximation
quality solely depends on the dimension of the lattice, but not the lattice itself. 
The algorithm also possesses many applications in diverse fields of computer science, 
from cryptanalysis to number theory, but it is specially well-known 
since it was used to implement the first polynomial-time algorithm to factor polynomials.
In this work we present the first mechanized soundness proof of the LLL algorithm to compute 
short vectors in lattices. The formalization follows a textbook by von~zur~Gathen and Gerhard~\cite{MCA}.
\end{abstract}

\tableofcontents

\section{Introduction}

The LLL basis reduction algorithm by Lenstra, Lenstra and Lov\'asz~\cite{LLL} is a remarkable algorithm with 
numerous applications in diverse fields. For instance, it can be used for 
finding the minimal polynomial of an algebraic number given to a good enough approximation, for finding integer
relations, for integer programming and even for breaking knapsack based cryptographic protocols.
Its most famous application is a polynomial-time algorithm to factor integer polynomials.
Moreover, the LLL algorithm is used as part of the best known polynomial factorization algorithm 
that is used in today's computer algebra systems.

In this work we implement it in Isabelle/HOL and fully formalize the correctness of the implementation.
The algorithm is parametric by some $\alpha > \frac43$, and given $\isa{fs}$ a list of 
$m$-linearly independent vectors $\Base {\isa{fs}} \in \ints^n$, it computes a short vector whose norm is at most $\alpha^{\frac{m-1}2}$ larger 
than the norm of any nonzero vector in the lattice generated by the vectors of the list $\isa{fs}$.
The soundness theorem follows.

\begin{theorem}[Soundness of LLL algorithm]
\label{thm:LLL}
\begin{align*}
&\lemma\ short\_vector:\\
&\assumes\ \alpha \geq 4 / 3\\
&\iand\ lin\_indpt\_list\ (RAT\ fs)\\
&\iand\ short\_vector\ \alpha\ fs = v\\
&\iand\ length\ fs = m\\
&\iand\ m \neq 0\\
&\shows\ v \in lattice\_of\ fs - \{0_v\;\isa n\}\\
&\iand\ h \in lattice\_of\ fs - \{0_v\;\isa n\} \longrightarrow \sqnorm{\isa v} \leq \alpha^{\isa m-1} \cdot \sqnorm{\isa{h}}
\end{align*}
\end{theorem}

To this end, we have performed the following tasks:
\begin{itemize}
 \item We firstly have to improve some AFP entries, as well as generalize several concepts from the standard library.
 \item We have to develop a library about norms of vectors and their properties.
 \item We formalize the Gram--Schmidt orthogonalization 
      procedure, which is a crucial sub-routine of the LLL algorithm. 
      Indeed, we already formalized this procedure in Isabelle as a function \isa{gram\_schmidt} when proving
      the existence of Jordan normal forms \cite{ThiemannY16}. 
      Unfortunately, lemma \isa{gram\_schmidt} does not suffice for verifying the LLL algorithm and we have had to extend such a formalization. 
  \item We prove the termination of the algorithm and its soundness.
  \item We prove polynomial runtime complexity by showing that there is a polynomial bound
      on the required number of arithmetic operations. Moreover, we formally prove that the representation size 
      of the numbers
      that occur during the executation stays polynomial.
\end{itemize}

To our knowledge, this is the first formalization of the LLL algorithm in any theorem prover.


% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
