A Formalization of the LLL Basis Reduction Algorithm

In order to factor an integer polynomial f, we may assume a modular factorization of f into several monic factors \(u_i\): modulo m where \(m = p^l\) is some prime power for user-specified l. In Isabelle, we just reuse our verified modular factorization algorithm [1] to obtain the modular factorization of f.

We briefly explain how to compute non-trivial integer polynomial factors h of f based on Lemma 1, as also informally described in the textbook.

Let f be a polynomial of degree n. Let u be any degree-d factor of f modulo m. Now assume that f is reducible, so \(f = f_1 \cdot f_2\) where w.l.o.g., we assume that u divides \(f_1\) modulo m and that . Let the lattice \(L_{u,k}\) be the set of all polynomials of degree below \(d+k\) which are divisible by u modulo m. As , clearly \(f_1 \in L_{u, n - d}\).

In order to instantiate Lemma 1, it now suffices to take g as the polynomial corresponding to any short vector in \(L_{u,k}\): u will divide g modulo m by definition of \(L_{u,k}\) and moreover . The short vector requirement will provide an upper bound to satisfy the assumption .

Here, the first inequality in (4) is the short vector approximation (\(f_1 \in L_{u,k}\)). The second inequality in (4) is Mignotte’s factor bound (\(f_1\) is a factor of f). Finally, Mignotte’s factor bound and (4) are used as approximations of and in (5), respectively.

Hence, if l is chosen large enough so that then all preconditions of Lemma 1 are satisfied, and will be a non-constant factor of f. Since \(f_1\) divides f, also will be a non-constant factor of f. Moreover, the degree of h will be strictly less than n, and so h is a proper factor of f.

In the previous section we have chosen the lattice \(L_{u,k}\) for \(k = n-d\) to find a polynomial h that is a proper factor of f. This has the disadvantage that h is not necessarily irreducible. In contrast, Algorithm 16.22 tries to directly find irreducible factors by iteratively searching for factors w.r.t.  the lattices \(L_{u,k}\) for increasing k from 1 up to \(n - d\).

We do not have the space to present Algorithm 16.22 in detail, but just state that the arguments in the textbook and the provided invariants all look reasonable. Luckily, Isabelle was not so convinced: We got stuck with the goal that the content of the polynomial g corresponding to the short vector is not divisible by the chosen prime p, and this is not necessarily true.

The first problem occurs if the content of g is divisible by p. Consider \(f_1 = x^{12}+x^{10}+x^8+x^5+x^4+1\) and \(f_2 = x\). When trying to factor \(f = f_1 \cdot f_2\), then \(p = 2\) is chosen, and at a certain point the short vector computation is invoked for a modular factor u of degree 9 where \(L_{u,4}\) contains \(f_1\). Since \(f_1\) itself is a shortest vector, \(g = p \cdot f_1\) is a short vector: the approximation quality permits any vector of \(L_{u,4}\) of norm at most . For this valid choice of g, the result of Algorithm 16.22 will be the non-factorization \(f = f_1 \cdot 1\).

We informed the authors of the textbook about this first problem. They admitted the flaw and it is easy to fix.

There is however a second potential problem. If g is even divisible by \(p^l\), then Algorithm 16.22 will again return wrong results. In the formalization we therefore integrate the check into the factorization algorithm⁴, and then this modified version of Algorithm 16.22 is correct.

We could not conclude the question whether the additional check is really required, i.e., whether can ever happen, and just give some indication that the question is non-trivial. For instance, when factoring \(f_1\) above, then \(p^l\) is a number with 124 digits, , so in particular all basis elements of \(L_{u,1}\) will have a norm of at least \(p^l\). Note that \(L_{u,1}\) also does not have quite short vectors: any vector in \(L_{u,1}\) will have norm of at least 111 digits. However, since the approximation factor in this example is only two digits long, the short vector computation must result in a vector whose norm has at most 113 digits, which is not enough for permitting \(p^l\) with its 124 digits as leading coefficient of g.

To verify the factorization algorithm of Sect. 6.1, we formalize the two key facts to relate lattices and factors of polynomials: Lemma 1 and the lattice \(L_{u,k}\).

To prove Lemma 1, we partially follow the textbook, although we do the final reasoning by means of some properties of resultants which were already proved in the previous development of algebraic numbers [14]. We also formalize Hadamard’s inequality, which states that for any square matrix A having rows \(v_i\), then . Essentially, the proof of Lemma 1 consists of showing that the resultant of f and g is 0, and then deduce . We omit the full-detailed proof, the interested reader can see it in the sources.

To define the lattice \(L_{u,k}\) for a degree d polynomial u and integer k, we define the basis \(v_0,\dots ,v_{k+d-1}\) of the lattice \(L_{u,k}\) such that each \(v_i\) is the \((k+d)\)-dimensional vector corresponding to polynomial \(u(x) \cdot x^i\) if \(i<k\), and to monomial \(m\cdot x^{k+d-i}\) if \(k \le i < k+d\).

We define the basis in Isabelle/HOL as as follows:

Here is a function that transforms a polynomial p into a vector of dimension n with coefficients in the reverse order and completing with zeroes if necessary. We use it to identify an integer polynomial f of degree \(< n\) with its coefficient vector in \(\mathbb {Z}^{n}\). We also define its inverse operation, which transforms a vector into a polynomial, as . denotes the reversed sorted list of natural elements from b to \(a-1\) (with \(b<a\)) and denotes the monomial \(ax^b\). To visualize the definition, for \(u(x) = \sum _{i=0}^d u_i x^i\) we haveand is precisely the basis \((f_1,f_2,f_3)\) of Example 1.

There are some important facts that we must prove about .

The first property is a consequence of obvious facts that the matrix S is upper triangular, and its diagonal entries are non-zero if both u and m are non-zero. Thus, the vectors in are linearly independent.

Now we look at the second property. For one direction, we see the matrix S in (6) as (a generalization of) the Sylvester matrix of polynomial u and constant polynomial m. Then we generalize an existing formalization about Sylvester matrices as follows:

We instantiate by the constant polynomial m. So for every \(c \in \mathbb {Z}^{k+d}\) we getfor some polynomials r and s. As every \(g \in L_{u,k}\) is represented as \(S^{\mathsf T} c\) for some integer coefficient vector \(c \in \mathbb {Z}^{k+d}\), we conclude that every \(g \in L_{u,k}\) is divisible by u modulo m. The other direction requires the use of the division with remainder by the monic polynomial u. Although we closely follow the textbook, the actual formalization of these reasonings requires some more tedious work, namely the connection between the matrix-to-vector multiplication ( ) of Matrix.thy and linear combinations ( ) of HOL-Algebra. The former is naturally described as a summation over lists ( which we define via ), while the latter is set-based . We follow the existing connection between and of the class-based world to the locale-based world, which demands some generalizations of the standard library.

Once those properties are proved, we implement an algorithm for the reconstruction of factors within a context that fixes and :⁵

is a recursive function which receives two parameters: the polynomial that has to be factored and , which is the list of modular factors of the polynomial . computes a short vector (and transforms it into a polynomial) in the lattice generated by a basis for \(L_{u,k}\) and suitable k, that is, . is the list of elements of that divide modulo , and contains the rest of elements of returns the list of irreducible factors of Termination follows from the fact that the degree decreases, that is, in each step the degree of both and is strictly less than the degree of

In order to formally verify the correctness of the reconstruction algorithm for a polynomial we use the following invariants. They consider invocations for every intermediate factor of

Concerning complexity, it is easy to see that if splits into i factors, then invokes the short vector computation for exactly \(i + (i-1)\) times: \(i-1\) invocations are used to split   into the i irreducible factors, and for each of these factors one invocation is required to finally detect irreducibility.

Finally, we combine the new reconstruction algorithm with existing results (the algorithms for computing an appropriate prime p, the corresponding exponent l, the factorization in \(\mathbb {Z}_p[x]\) and its Hensel-lifting to \(\mathbb {Z}_{p^l}[x]\)) presented in the Berlekamp–Zassenhaus development to get a polynomial-time factorization algorithm for square-free and content-free polynomials.

We further combine this algorithm with a pre-processing algorithm of earlier work [1]. This pre-processing splits a polynomial f into \(c \cdot f_1^1 \cdot \ldots \cdot f_k^k\) where c is the content of f which is not further factored. Each \(f_i\) is square-free and content-free, and will then be passed to . The combined algorithm factors arbitrary univariate integer polynomials into its content and a list of irreducible polynomials.

When experimentally comparing our verified LLL-based factorization algorithm with the verified Berlekamp–Zassenhaus factorization algorithm [1] we see no surprises. On the random polynomials from the experiments in [1], Berlekamp–Zassenhaus’s algorithm performs much better: it can factor each polynomial within a minute, whereas the LLL-based algorithm already fails on the smallest example. It is an irreducible polynomial with 100 coefficients where the LLL algorithm was aborted after a day when trying to compute a reduced basis for a lattice of dimension 99 with coefficients having up to 7 763 digits.