Commit 97f5c6c8 by nipkow

new entry LLL_Basis_Reduction

parent 41f8c8c84179
 ... ... @@ -6497,3 +6497,24 @@ abstract = criterion, a general framework for refutational theorem proving, and soundness and completeness of an abstract first-order prover. [LLL_Basis_Reduction] title = A verified LLL algorithm author = Jose Divasón , Sebastiaan Joosten , René Thiemann , Akihisa Yamada<> topic = Computer Science/Algorithms, Mathematics/Algebra date = 2018-02-02 notify = jose.divason@unirioja.es, s.j.c.joosten@utwente.nl, rene.thiemann@uibk.ac.at, ayamada@trs.cm.is.nagoya-u.ac.jp abstract = The Lenstra-Lenstra-Lovász 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.
This diff is collapsed.
This diff is collapsed.
 (* Authors: Jose Divasón Sebastiaan Joosten René Thiemann Akihisa Yamada License: BSD *) section \List representation\ theory List_Representation imports Main begin lemma rev_take_Suc: assumes j: "j < length xs" shows "rev (take (Suc j) xs) = xs ! j # rev (take j xs)" proof - from j have xs: "xs = take j xs @ xs ! j # drop (Suc j) xs" by (rule id_take_nth_drop) show ?thesis unfolding arg_cong[OF xs, of "\ xs. rev (take (Suc j) xs)"] by (simp add: min_def) qed type_synonym 'a list_repr = "'a list \ 'a list" definition list_repr :: "nat \ 'a list_repr \ 'a list \ bool" where "list_repr i ba xs = (i \ length xs \ fst ba = rev (take i xs) \ snd ba = drop i xs)" definition of_list_repr :: "'a list_repr \ 'a list" where "of_list_repr ba = (rev (fst ba) @ snd ba)" lemma of_list_repr: "list_repr i ba xs \ of_list_repr ba = xs" unfolding of_list_repr_def list_repr_def by auto definition get_nth_i :: "'a list_repr \ 'a" where "get_nth_i ba = hd (snd ba)" definition get_nth_im1 :: "'a list_repr \ 'a" where "get_nth_im1 ba = hd (fst ba)" lemma get_nth_i: "list_repr i ba xs \ i < length xs \ get_nth_i ba = xs ! i" unfolding list_repr_def get_nth_i_def by (auto simp: hd_drop_conv_nth) lemma get_nth_im1: "list_repr i ba xs \ i \ 0 \ get_nth_im1 ba = xs ! (i - 1)" unfolding list_repr_def get_nth_im1_def by (cases i, auto simp: rev_take_Suc) definition update_i :: "'a list_repr \ 'a \ 'a list_repr" where "update_i ba x = (fst ba, x # tl (snd ba))" lemma Cons_tl_drop_update: "i < length xs \ x # tl (drop i xs) = drop i (xs[i := x])" proof (induct i arbitrary: xs) case (0 xs) thus ?case by (cases xs, auto) next case (Suc i xs) thus ?case by (cases xs, auto) qed lemma update_i: "list_repr i ba xs \ i < length xs \ list_repr i (update_i ba x) (xs [i := x])" unfolding update_i_def list_repr_def by (auto simp: Cons_tl_drop_update) definition update_im1 :: "'a list_repr \ 'a \ 'a list_repr" where "update_im1 ba x = (x # tl (fst ba), snd ba)" lemma update_im1: "list_repr i ba xs \ i \ 0 \ list_repr i (update_im1 ba x) (xs [i - 1 := x])" unfolding update_im1_def list_repr_def by (cases i, auto simp: rev_take_Suc) lemma tl_drop_Suc: "tl (drop i xs) = drop (Suc i) xs" proof (induct i arbitrary: xs) case (0 xs) thus ?case by (cases xs, auto) next case (Suc i xs) thus ?case by (cases xs, auto) qed definition inc_i :: "'a list_repr \ 'a list_repr" where "inc_i ba = (case ba of (b,a) \ (hd a # b, tl a))" lemma inc_i: "list_repr i ba xs \ i < length xs \ list_repr (Suc i) (inc_i ba) xs" unfolding list_repr_def inc_i_def by (cases ba, auto simp: rev_take_Suc hd_drop_conv_nth tl_drop_Suc) definition dec_i :: "'a list_repr \ 'a list_repr" where "dec_i ba = (case ba of (b,a) \ (tl b, hd b # a))" lemma dec_i: "list_repr i ba xs \ i \ 0 \ list_repr (i - 1) (dec_i ba) xs" unfolding list_repr_def dec_i_def by (cases ba; cases i, auto simp: rev_take_Suc hd_drop_conv_nth Cons_nth_drop_Suc) lemma dec_i_Suc: "list_repr (Suc i) ba xs \ list_repr i (dec_i ba) xs" using dec_i[of "Suc i" ba xs] by auto end \ No newline at end of file
This diff is collapsed.
This diff is collapsed.
 chapter AFP session LLL_Basis_Reduction (AFP) = Berlekamp_Zassenhaus + description {* LLL Algorithm *} options [timeout = 600] sessions Algebraic_Numbers Perron_Frobenius theories [document = false] theories List_Representation Norms Missing_Lemmas Vector_Lattice_Locale Gram_Schmidt_2 LLL document_files "root.tex" "root.bib"
 @book{MCA, author = {Gathen, Joachim von zur and Gerhard, J\"urgen}, title = {Modern Computer Algebra}, year = {2003}, edition = {2nd}, publisher = {Cambridge University Press}, address = {New York, NY, USA}, } @article{LLL, title = {Factoring polynomials with rational coefficients}, author = {A. K. Lenstra and H. W. Lenstra and L. Lov{\'a}sz}, journal = {Mathematische Annalen}, year = {1982}, volume = {261}, pages = {515--534}, } @inproceedings{ThiemannY16, Author = {Ren{\'e} Thiemann and Akihisa Yamada}, Booktitle = {CPP~2016}, Opeditor = {Jeremy Avigad and Adam Chlipala}, Pages = {88--99}, Publisher = {ACM}, Title = {Formalizing {J}ordan normal forms in {I}sabelle/{HOL}}, Year = 2016}
 \documentclass[11pt,a4paper]{article} \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{Jose Divas\'on \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. \end{itemize} Regarding the complexity of the LLL algorithm, we did not include a formal statement which would have required an instrumentation of the algorithm by some instruction counter. However, from the termination proof of our Isabelle implementation of the LLL algorithm, one can easily infer a polynomial bound on the number of arithmetic operations. 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:
 ... ... @@ -205,6 +205,7 @@ List-Infinite List_Interleaving List_Update Lifting_Definition_Option LLL_Basis_Reduction LocalLexing Locally-Nameless-Sigma LOFT ... ...
 ... ... @@ -81,7 +81,7 @@
Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at) René Thiemann
... ...
 ... ... @@ -84,9 +84,9 @@ Authors:
René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at), Akihisa Yamada (akihisa /dot/ yamada /at/ uibk /dot/ ac /dot/ at) and Sebastiaan Joosten (sebastiaan /dot/ joosten /at/ uibk /dot/ ac /dot/ at) René Thiemann, Akihisa Yamada and Sebastiaan Joosten
Berlekamp_Zassenhaus, Show, Sturm_Sequences
Used by: Linear_Recurrences, Perron_Frobenius
Linear_Recurrences, LLL_Basis_Reduction, Perron_Frobenius
... ... @@ -135,7 +135,7 @@ To this end, we mechanized several results on resultants, which also required us ... ...
 ... ... @@ -90,10 +90,10 @@ Authors:
Jose Divasón, Sebastiaan Joosten (sebastiaan /dot/ joosten /at/ uibk /dot/ ac /dot/ at), René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at) and Akihisa Yamada (akihisa /dot/ yamada /at/ uibk /dot/ ac /dot/ at) Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada
Efficient-Mergesort, Polynomial_Factorization, Polynomial_Interpolation, Show, Subresultants
Used by: Algebraic_Numbers, Probabilistic_While
Algebraic_Numbers, LLL_Basis_Reduction, Probabilistic_While
... ... @@ -150,7 +150,7 @@ local type definitions. ... ...
 ... ... @@ -81,7 +81,7 @@
Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at) René Thiemann
... ...
 ... ... @@ -86,7 +86,7 @@ Author:
René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at) René Thiemann
... ...
 ... ... @@ -87,7 +87,7 @@
Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at) René Thiemann