Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL

The Gram–Schmidt orthogonalization (GSO) procedure takes a list of linearly independent vectors \(f_0,\ldots ,f_{m-1}\) from \(\mathbb {R}^n\) or \(\mathbb {Q}^n\) as input, and returns an orthogonal basis \(g_0,\ldots ,g_{m-1}\) for the space that is spanned by the input vectors. The vectors \(g_0,\ldots ,g_{m-1}\) are then referred to as GSO vectors. To be more precise, the GSO is defined by mutual recursion as:An intuition for these definitions is that if we remove from some \(f_i\) the part that is contained in the subspace spanned by \(\{f_0,\ldots ,f_{i-1}\}\), then what remains (the vector \(g_i\)) must be orthogonal to that subspace. The \(\mu _{i,j}\) are the coordinates of \(f_i\) w.r.t. the basis \(\{g_0,\ldots , g_{m-1}\}\) (thus \(\mu _{i,j}=0\) for \(j>i\), since then \(g_j\perp f_i\)).

The GSO vectors have an important property that is relevant for the LLL algorithm, namely they are short in the following sense: for every non-zero integer vector v in the lattice generated by \(f_0,\ldots ,f_{m-1}\), there is some \(g_i\) such that \(|\!|g_i|\!| \le |\!|v|\!|\). Moreover, \(g_0 = f_0\) is an element in the lattice. Hence, if \(g_0\) is a short vector in comparison to the other GSO vectors, then \(g_0\) is a short lattice vector.

The requirement on the \(\mu _{i,j}\) implies that the f-vectors are nearly orthogonal. (If \(|\mu _{i,j}| = 0\) for all \(j< i < m\), then the f-vectors are pairwise orthogonal.)

The connection between a reduced basis and short vectors can now be seen easily: If \(f_0,\ldots ,f_{m-1}\) is reduced, then for any non-zero lattice vector v we haveand thus, \(|\!|f_0|\!| \le \alpha ^{\frac{m-1}{2}} |\!|v|\!|\) shows that \(f_0\) is a short vector which is at most \(\alpha ^{\frac{m-1}{2}}\) longer than the shortest vectors in the lattice.

In a previous formalization [27] of the Gram–Schmidt orthogonalization procedure, the \(\mu \)-values are computed implicitly. Since for the LLL algorithm we need the \(\mu \)-values explicitly, we implement a new version of GSO. Here the dimension n and the input basis are fixed as locale parameters. The are given here as rational vectors, but the implementation is parametric in the type of field.

It is easy to see that these Isabelle functions compute the g-vectors and \(\mu \)-values precisely according to their defining Eq. (1).

Based on this new formal definition of GSO with explicit \(\mu \)-values, it is now easy to formally define a reduced basis. Here, we define a more general notion, which only requires that the first k vectors form a reduced basis.

The LLL algorithm modifies the input \(f_0,\dots ,f_{m-1} \in \mathbb {Z}^n\) until the corresponding GSO is reduced w.r.t. \(\alpha \), while preserving the generated lattice. The approximation factor\(\alpha \) can be chosen arbitrarily as long as \(\alpha > \frac{4}{3}\).¹

In this section, we present a simple implementation of the algorithm given as pseudo-code in Algorithm 1, which mainly corresponds to the LLL algorithm in a textbook [29, Chapters 16.2–16.3] (the textbook fixes \(\alpha = 2\) and \(m = n\)). Here, \(\lfloor x \rceil = \lfloor x + \frac{1}{2}\rfloor \) is the integer nearest to x. Note that whenever \(\mu _{i,j}\) or \(g_i\) are referred to in the pseudo-code, their values are computed (as described in the previous subsection) for the current values of \(f_0,\ldots ,f_{m-1}\).

We briefly explain the ideas underpinning Algorithm 1: Lines 3–4 work towards satisfying the second requirement for the basis to be reduced (see Definition 1), namely that the \(\mu _{i,j}\) values be small. This is done by “shaving off”, from each \(f_i\), the part that overlaps with some part of an \(f_j\) (with \(j<i\)). This ensures that when the GSO is computed for this new basis, a (norm-wise) significant part of each \(f_i\) does not lie in the subspace spanned by the \(f_j\) with \(j<i\) (as those parts have already been removed in line 4). When a violation of the first requirement for being a reduced basis is detected in line 5, the algorithm attempts to rectify this by performing a swap of the corresponding f-vectors in the next line. Thus, the algorithm continually attempts to fix the basis in such a way that it satisfies both requirements for being reduced, but the fact that it always succeeds, and in polynomial-time, is not obvious at all. For a more detailed explanation of the algorithm itself, we refer to the textbooks [21, 29].

In order to formalize the main parts of Algorithm 1, we first encode it in several functions, which we list and explain below. We are using a locale that fixes the approximation factor \(\alpha \), the dimensions n and m, and the basis \(\textit{fs}_{init}\) of the initial (input) lattice.

The following are some remarks regarding the above code fragments:In this section we only looked at how the algorithms were specified in Isabelle. In the next section we discuss the formal proofs of their soundness.

As mentioned in the previous section, the GSO procedure itself has already been formalized in Isabelle as a function called , in way of proving the existence of Jordan normal forms [27]. That formalization uses an explicit carrier set to enforce that all vectors are of the same dimension. For the current formalization task, the use of a carrier-based vector and matrix library is necessary: encoding dimensions via types [15] is not expressive enough for our application; for instance for a given square matrix of dimension n we need to multiply the determinants of all submatrices that only consider the first i rows and columns for all \(1 \le i \le n\).

Below, we summarize the main result that is formally proved about [27]. For the following code, we open a context assuming common conditions for invoking the Gram–Schmidt procedure, namely that is a list of linearly independent vectors, and that is the GSO of . Here, we also introduce our notion of linear independence for lists of vectors, based on an definition of linear independence for sets from an AFP-entry of H. Lee about vector spaces.

Unfortunately, lemma does not suffice for verifying the LLL algorithm, since it works basically as a black box. By contrast, we need to know how the GSO vectors are computed, that the connection between and can be expressed via a product of matrices, and we need the recursive equations to compute and the \(\mu \)-values. In order to reuse the existing results on , we first show that both definitions are equivalent.

The connection between the f-vectors, g-vectors and the \(\mu \)-values is expressed by the matrix identityby interpreting the \(f_i\)’s and \(g_i\)’s as row vectors.

While there is no conceptual problem in proving the matrix identity (3), there are some conversions of types required. For instance, in lemma , is a list of vectors; in (1), g is a recursively defined function from natural numbers to vectors; and in (3), the list of \(g_i\)’s is seen as a matrix. Consequently, the formalized statement of (3) contains conversions such as and , which convert a function and a list of vectors, respectively, into a matrix. In any case, the overhead is small and very workable; only a few lines of easy conversions are added when required. An alternative approach could be to do everything at the level of matrices [13].

As mentioned in Sect. 3.1, our main use of GSO with regards to the LLL algorithm is that the norm of the shortest GSO vector is a lower bound on the norms of all lattice vectors. While proving this fact requires only a relatively short proof on paper, in the formalization we had to expand the condensed paper-proof into 170 lines of more detailed Isabelle source, plus several auxiliary lemmas. For instance, on paper one easily multiplies two sums (\((\sum \ldots ) \cdot \sum \ldots = \sum \ldots \)) and directly omits quadratically many neutral elements by referring to orthogonality, whereas we first had to prove this auxiliary fact in 34 lines.

With the help of this result it is straight-forward to formalize the reasoning in (2) to obtain the result that the first vector of a reduced basis is a short vector in the lattice.

Finally, we mention the formalization of a key ingredient in reasoning about the LLL algorithm: orthogonal projections. We say \(w \in \mathbb {R}^n\) is a projection of \(v\in \mathbb {R}^n\) into the orthogonal complement of \(S \subseteq \mathbb {R}^n\), or just w is an oc-projection of v and S, if \(v - w\) is in the span of S and w is orthogonal to every element of S:

Returning to the GSO procedure, we prove that \(g_j\) is the unique oc-projection of \(f_j\) and \(\{f_0,\dots ,f_{j-1}\}\). Hence, \(g_j\) is uniquely determined in terms of \(f_j\) and the span of \(\{f_0,\dots ,f_{j-1}\}\). Put differently, we obtain the same \(g_j\) even if we modify some of the first j input vectors of the GSO: only the span of these vectors must be preserved. This result is in particular important for proving that only \(g_{i-1}\) and \(g_i\) can change in Line 6 of Algorithm 1, since for any other \(g_j\), neither \(f_j\) nor the set \(\{f_0,\dots ,f_{j-1}\}\) is changed by a swap of \(f_{i-1}\) and \(f_i\).

In this subsection we give an overview of the formal proof that Algorithm 1 terminates on valid inputs, with an output that has the desired properties.

In order to prove the correctness of the algorithm, we define an invariant, which is simply a set of conditions that the current state must satisfy throughout the entire execution of the algorithm. For example, we require that the lattice generated by the original input vectors \(f_0,\ldots ,f_{m-1}\) be maintained throughout the execution of the algorithm. Intuitively this is obvious, since the basis is only changed in lines 4 and 6, and swapping two basis vectors or adding a multiple of one basis vector to another will not change the resulting lattice. Nevertheless, the formalization of these facts required 170 lines of Isabelle code.

In the following Isabelle statements we write as a short form of , i.e., the Isabelle expression for the predicate w.r.t. \(\alpha \), considering the first vectors, within the locale with an . Similarly, we write and when we are referring to the \(\mu \)-values and the GSO vectors corresponding to the basis .

The key correctness property of the LLL algorithm is then given by the following lemma, which states that the invariant is preserved in the while-loop of Algorithm 1 ( and in the definition above refer to the variables with the same name in the main loop of the algorithm). Specifically, the lemma states that if the current state (the current pair ), prior to the execution of an instruction, satisfies the invariant, then so does the resulting state after the instruction. It also states a decrease in a measure, which will be defined below, to indicate how far the algorithm is from completing the computation—this is used to prove that the algorithm terminates.

Using Lemma , one can prove the following crucial properties of the LLL algorithm. Both the fact that the algorithm terminates and the fact that the invariant is maintained throughout its execution, are non-trivial to prove, as both proofs require equations that determine how the GSO will change through the modification of \(f_0,\ldots ,f_{m-1}\) in lines 4 and 6. Specifically, we formally prove that the GSO remains unchanged in lines 3–4, that a swap of \(f_{i-1}\) and \(f_i\) will at most change \(g_{i-1}\) and \(g_i\), and we provide an explicit formula for calculating the new values of \(g_{i-1}\) and \(g_i\) after a swap. In these proofs we require the recursive definition of the GSO as well as the characterization via oc-projections.

In the remainder of this section, we provide details on the termination argument. The measure that is used for proving termination is defined below using Gramian determinants, a generalization of determinants which also works for non-square matrices. The definition of the measure is also the point where the condition \(\alpha > \frac{4}{3}\) becomes important: it ensures that the base \(\frac{4\alpha }{4 + \alpha }\) of the logarithm is strictly greater than 1.²

In the definition, the matrix is the submatrix of corresponding to the first elements of . Note that the measure is defined in terms of the variables  and . However, for lines 3–4 we only proved that and the GSO remain unchanged. Hence the following lemma is important: it implies that the measure can also be defined purely from and the GSO of , and that the measure will be positive.

Having defined a suitable measure, we sketch the termination proof: The value of the Gramian determinant for parameter \(k \ne i\) stays identical when swapping \(f_i\) and \(f_{i-1}\), since it just corresponds to an exchange of two rows, which will not modify the absolute value of the determinant. The Gramian determinant for parameter \(k = i\) can be shown to decrease, by using the first statement of lemma , the explicit formula for the new value of \(g_{i-1}\), the condition \(|\!|g_{i-1}|\!|^2 > \alpha \cdot |\!|g_i|\!|^2\), and the fact that \(|\mu _{i,i-1}| \le \frac{1}{2}\).

In order to obtain a full integer-only implementation of the LLL algorithm, we also require such an implementation of the Gram–Schmidt orthogonalization. For this, we mainly follow [12], where a GSO-algorithm using only operations in an abstract integral domain is given. We implemented this algorithm for the integers and proved the main soundness results following [12].

The correctness of Algorithm 2 hinges on two properties: that the calculated \(\tilde{\mu }_{i,j}\) are equal to \(d_{j + 1}\mu _{i,j}\), and that it is sound to use integer division in line 6 of the algorithm (in other words, that the intermediate values computed at every step of the algorithm are integers). We prove these two statements in Isabelle by starting out with a more abstract version of the algorithm, which we then refine to the one above. Specifically, we first define the relevant quantities as follows:

Here \(\tilde{\mu }\) is not computed recursively, and represents the value of \(\sigma \) at the beginning of the l-th iteration of the innermost loop, i.e., is the value of \(\sigma \) after executing line 4. We remark that the type of (the range of) \(\tilde{\mu }\) and of \(\sigma \) is , rather than ; this is why we can use general division for fields (/) in the above function definition, rather than integer division ( ). The advantage of letting and return rational numbers is that we can proceed to prove all of the equations and lemmas from [12] while focusing only on the underlying mathematics, without having to worry about non-exact division. For example, from the definition above we can easily show the following characterization.

This lemma is needed to prove one of the two statements that are crucial for the correctness of the algorithm, namely that the computation of \(\tilde{\mu }\) in lines 2 and 7 is correct (recall the identities \(d_0 = 1\) and \(d_j = \tilde{\mu }_{j-1,j-1}\) for \(j > 0\)).

To prove that the above quantities are integers, we first show \(d_i g_{i}\in {\mathbb {Z}}^n\). For this, we prove that \(g_i\) can be written as a sum involving only the f vectors, namely, that \(g_i = f_i - \sum _{j< i} \mu _{i,j}g_j = f_i - \sum _{j < i} \kappa _{i,j} f_j\). Two sets of vectors \(f_0,\ldots ,f_{i-1}\) and \(g_0,\ldots ,g_{i-1}\) span by construction the same space and both are linearly independent. The \(\kappa _{i,j}\) are therefore simply the coordinates of \(\sum _{j < i} \mu _{i,j}g_j\) in the basis \(f_0,\ldots ,f_{i-1}\). Now, since the f vectors are integer-valued, it suffices to show that \(d_i \kappa _{i,j} \in {\mathbb {Z}}\), in order to get \(d_i g_{i} \in {\mathbb {Z}}^n\). To prove the former, observe that each \(g_i\) is orthogonal to every \(f_l\) with \(l < i\) and therefore \(0 = f_l \bullet g_i = f_l \bullet f_i - \sum _{j < i} \kappa _{i,j}(f_l \bullet f_j)\). Thus, the \(\kappa _{i,j}\) form a solution to a system of linear equations:The coefficient matrix A on the left-hand side where \(A_{i,j} = f_i \bullet f_j\) is exactly the Gramian matrix of and . By an application of Cramer’s lemma,³ we deduce:The matrix , which is obtained from by replacing its -th column by , contains only inner products of the f vectors as entries and these are integers. Then the determinant is also an integer and \(d_i \kappa _{i,j} \in \mathbb {Z}\).

Since \(\mu _{i,j}=\frac{f_i \bullet g_j}{|\!|g_j|\!|^2}\) and \(\frac{d_{j+1}}{d_j} = |\!|g_j|\!|^2\), the theorem from the introduction of this section, stating that \(\tilde{\mu }_{i,j} = d_{j+1} \mu _{i,j}\in {\mathbb {Z}}\), is easily deduced from the fact that \(d_i g_{i} \in {\mathbb {Z}}^n\).

In our formalization we generalized the above proof so that we are also able to show that \(d_l(f_i - \sum _{j<l}\mu _{i,j} g_j)\) is integer-valued (note that the sum only goes up to l, not i). This generalization is necessary to prove that all \(\sigma \) values are integers.

Having proved the desired properties of the abstract version of Algorithm 2, we make the connection with an actual implementation on integers that computes the values of \(\tilde{\mu }\) recursively using integer division.

Note that these functions only use integer arithmetic and therefore return a value of type . We then show that the new functions are equal to the ones defined previously. Here, is a function that converts a number of type into the corresponding number of type . For notational convenience, the indices of are shifted by one with respect to the indices of .

We then replace the repeated calls of \(\tilde{\mu }_{\mathbb {Z}}\) by saving already computed values in an array for fast access. Furthermore, we rewrite \(\sigma _\mathbb {Z}\) in a tail-recursive form, which completes the integer implementation of the algorithm for computing \(\tilde{\mu }\).

Note that Algorithm 2 so far only computes the \(\tilde{\mu }\)-matrix. For completeness, we also formalize and verify an algorithm that computes the integer-valued multiples \(\tilde{g_i} = d_ig_i\) of the GSO-vectors. Again, we first define the algorithm using rational numbers, then prove that all intermediate values are in fact integers, and finally refine the algorithm to an optimized and executable version that solely uses integer operations. A pseudo-code description is provided in the appendix as Algorithm 3.

We can now describe the formalization of an integer-only implementation of the LLL algorithm. For the version of the algorithm described in Sect. 3, we assumed that the GSO vectors and \(\mu \)-values are recomputed whenever the integer vectors f are changed. This made it easier to formalize the soundness proof, but as an implementation it would result in a severe computational overhead. Here we therefore assume that the algorithm keeps track of the required values and updates them whenever f is changed. This requires an extension of the soundness proof, since we now need to show that each change made to a value is consistent with what we would get if it were recomputed for the current value of f.

The version of the algorithm described in this section only stores f, the \(\tilde{\mu }\)-matrix, and the d-values, which, by lemma  , are all integer values or integer vectors [25]. This integer representation will be the basis for our verified integer implementation of the LLL algorithm. To prove its soundness, we proceed similarly as for the GSO procedure: First we provide an implementation which still operates on rational numbers and uses field-division, then we use lemma  to implement and prove the soundness of an equivalent but efficient algorithm which only operates on integers.

The main additional difficulty in the soundness proof of the reduction algorithm is that we are now required to explicitly state and prove the effect of each computation that results in a value update. We illustrate this problem with lemma  (Sect. 4.2). The statement of this lemma only speaks about the effect, w.r.t. the invariant, of executing one while-loop iteration of Algorithm 1, but it does not provide results on how to update the \(\tilde{\mu }\)-values and the d-values. In order to prove such facts, we added several computation lemmas of the following form, which precisely specify how the values of interest are updated when performing a swap of \(f_i\) and \(f_{i-1}\), or when performing an update \(f_i {:=} f_i - c \cdot f_j\). The newly computed values of and are marked with a sign after the identifier.

The computation lemma allows us to implement this part of the algorithm for various representations, i.e., the full lemma contains local updates for f, g, \(\mu \), and d. Moreover, the lemma has actually been used to prove the soundness of the abstract algorithm: the precise description of the \(\mu \)-values allows us to easily establish the invariant in step 4 of Algorithm 1: if \(c = \lfloor \mu _{i,j} \rceil \), then the new \(\mu _{i,j}\)-value will be small afterwards and only the \(\mu _{i,j_0}\)-entries with \(j_0 \le j\) can change.

Whereas the computation lemmas such as the one above mainly speak about rational numbers and vectors, we further derive similar computation lemmas for the integer values \(\tilde{\mu }\) and d, in such a way that the new values can be calculated based solely on the previous integer values of f, \(\tilde{\mu }\), and d. At this point, we also replace field divisions by integer divisions; the corresponding soundness proofs heavily rely upon Lemma  . As an example, the computation lemma for the swap operation of \(f_{k-1}\) and \(f_k\) provides the following equality for d, and a more complex one for the update of \(\tilde{\mu }\).⁴

After having proved all the updates for \(\tilde{\mu }\) and d when changing f, we implemented all the other expressions in Algorithm 1, e.g., \(\lfloor \mu _{i,j} \rceil \), based on these integer values.

Finally, we plug everything together to obtain an efficient executable LLL algorithm—- —-that uses solely integer operations. It has the same structure as Algorithm 1 and therefore we are able to prove that the integer algorithm is a valid implementation of Algorithm 1, only the internal computations being different. The following lemma resides in the locale , but takes the locale parameters \(\alpha \) and as explicit arguments, since we define it outside the locale as required by Isabelle’s code-generator [14].

We also explain here the optimization of the algorithm, that was mentioned in Sect. 3.2: Whenever the variable i is decreased in one iteration of the main loop, the next loop iteration does not invoke lines 3–4 of Algorithm 1. Recall that these lines have the purpose of obtaining small \(\mu _{i,j}\)-values. However, when decreasing i, the \(\mu _{i,j}\)-values are already small. This can be deduced from the invariant of the previous iteration in combination with the computation lemmas for a swap.

In the appendix, Algorithm 5 shows a pseudo-code of .

The computational cost of each of the basic arithmetic operations on integers (\(+\), −, \(\times \), \(\div \)) is obviously upper-bounded by a polynomial in the size of the largest operand. We are therefore interested in bounding the sizes of the various intermediate values that are computed throughout the execution of the algorithm. This is not a trivial task as already apparent in Examples 1 and 2, where we see that even the initial GSO computation can produce large numbers.

Our task is to formally derive bounds on \(f_i\), \({\tilde{\mu }}_{i,j}\), \(d_k\) and \(g_i\), as well as on the auxiliary values computed by Algorithm 2. Although the implementation of Algorithm 2 computes neither \(g_i\) nor \({\tilde{g}}_i\) throughout its execution, the proof of an upper bound on \(\tilde{\mu }_{i,j}\) uses an upper bound on \(g_i\).

Whereas the bounds for \(g_i\) will be valid throughout the whole execution of the algorithm, the bounds for the \(f_i\) depend on whether we are inside or outside the for-loop in lines 3–4 of Algorithm 1.

To formally verify bounds on the above values, we first define a stronger LLL-invariant which includes the conditions and and prove that it is indeed satisfied throughout the execution of the algorithm. Here, we define N as the maximum squared norm of the initial f-vectors.

Note that does not enforce a bound on the \({\tilde{\mu }}_{i,j}\), since such a bound can be derived from the bounds on f, g, and the Gramian determinants.

Based on the invariant, we first formally prove the bound \(|\mu _{i,j}|^2 \le d_j \cdot |\!|f_i|\!|^2\) by closely following the proof from [29, Chapter 16]. It uses Cauchy’s inequality, which is a part of our vector library. The bound \(d_k \le N^k\) on the Gramian determinant can be directly derived from the Lemma and .

The previous two bounds clearly give an upper-bound on \(\tilde{\mu }_{i,j} = d_{j+1}\mu _{i,j}\) in terms of N. Bounds on the intermediate values of \(\sigma \) in Algorithm 2 are obtained via lemma in Sect. 5.1. Finally, we show that all integer values x during the computing stay polynomial in n, m, and M, where M is the maximal absolute value within the initial f-vectors, satisfying \(N \le M^2 \cdot n\).

In this subsection we give an overview of the formal proof that our LLL implementation not only terminates on valid inputs, but does so after executing a number of arithmetic operations that is bounded by a polynomial in the size of the input.

The first step towards reasoning about the complexity is to extend the algorithm by annotating and collecting costs. In our cost model, we only count the number of arithmetic operations. To integrate this model formally, we use a lightweight approach that is similar to [11, 22]. It has the advantage of being easy to integrate on top of our formalization obtained so far, hence we did not try to incorporate alternative ways to track costs, e.g., via type systems [19].We illustrate our approach using an example: corresponds to lines 3–7 of Algorithm 2.

The function is a typical example of cost-annotated function and works as follows: One part invokes sub-algorithms or makes a recursive call and extracts the cost by pattern matching on pairs ( and ), the other part does some local operations and manually annotates the costs for them ( ). Finally, the pair of the computed result and the total cost is returned. For all cost functions we prove that is the value returned by the corresponding function.

To formally prove an upper bound on the cumulative cost of a run of the entire algorithm, we use the fact that was defined as the logarithm of a product of Gramian determinants, together with the bound \(d_k \le N^k \le (Mn)^{2k} \le (Mn)^{2m}\) from the previous subsection (where M was the maximum absolute value in the input vectors). This easily gives the desired polynomial bound:

The common structure of a modern factorization algorithm for square-free primitive polynomials in \(\mathbb {Z}[x]\) is as follows: In a previous work [7], we formalized the Berlekamp–Zassenhaus algorithm, which follows the structure presented above, where step 4 runs in exponential time. The use of the LLL algorithm allows us to derive a polynomial-time algorithm for the reconstruction phase.⁷ In order to reconstruct the factors in \(\mathbb {Z}[x]\) of a polynomial f, by steps 1–3 we compute a modular factorization of f into several monic factors \(u_i\): modulo m where \(m = p^l\) is some prime power given in step 1.

The intuitive idea underlying why lattices and short vectors can be used to factor polynomials follows. We want to determine a non-trivial factor h of f which shares a common modular factor u, i.e., both h and f are divided by u modulo \(p^l\). This means that h belongs to a certain lattice. The condition that h is a factor of f means that the coefficients of h are relatively small. So, we must look for a small element (a short vector) in that lattice, which can be done by means of the LLL algorithm. This allows us to determine h.

More concretely, the key is the following lemma.

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 that \(f = f_1 \cdot f_2\), where w.l.o.g. we may assume that u divides \(f_1\) modulo m and that . Let \(L_{u,k}\) be the lattice 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,n-d}\): u divides g modulo m by definition of \(L_{u,n-d}\) and moreover . The short vector requirement provides an upper bound to satisfy the assumption .The first inequality in (5) is the short vector approximation (\(f_1 \in L_{u,n-d}\)). The second inequality in (5) is Mignotte’s factor bound (\(f_1\) is a factor of f). Mignotte’s factor bound and (5) are used in (6) as approximations of \(|\!|f_1|\!|\) and \(|\!|g|\!|\), respectively. Hence, if l is chosen such that \(m = p^l > |\!|f|\!|^{2(n-1)} \cdot 2^{5(n - 1)^2/2}\), then all preconditions of Lemma 1 are satisfied, and is a non-constant factor of f. Since \(f_1\) divides f, also is a non-constant factor of f. Moreover, the degree of h is strictly less than n, and so h is a proper factor of f.

Here we present the formalization of two items that are essential for relating 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 [16]. We also formalize Hadamard’s inequality, which states that for any square matrix A having rows \(v_i\) we have . Essentially, the proof of Lemma 1 consists of showing that the resultant of f and g is 0, and then deduce . We omit the detailed proof; a formalized version can be found in the sources.

To define the lattice \(L_{u,k}\) for a degree-d polynomial u and integer k, we give a 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 the monomial \(m\cdot x^{k+d-i}\) if \(k \le i < k+d\).

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

Here, denotes the list of natural numbers descending from \(a-1\) to b (with \(a>b\)), denotes the monomial \(ax^b\), and 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 .

To visualize the definition, for \(u(x) = \sum _{i=0}^d u_i x^i\) we haveand is precisely the basis \((f_0,f_1,f_2)\) of Example 1.

There are some important facts that we must prove about .The first property is a consequence of the obvious fact that the matrix S in (7) is upper triangular, and that its diagonal entries are non-zero if both u and m are non-zero. Thus, the vectors in ukm are linearly independent.

Next, we look at the second property. For one direction, we see the matrix S as (a generalization of) the Sylvester matrix of the 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 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-times-vector multiplication of Matrix.thy (denoted by in the formalization) and linear combinations ( ) of HOL-Algebra.

Once the key results, namely Lemma 1 and properties about the lattice \(L_{u,k}\), are proved, we implement an algorithm for the reconstruction of factors within a context that fixes and . The simplified definition looks as follows.

is a recursive function which receives two parameters: the polynomial that has to be factored, and 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, . We collect the elements of that divide modulo into the list , and the rest into . 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 for each invocation of , where is an intermediate non-constant factor of . Here some properties are formulated solely via , so they are trivially invariant, and then corresponding properties are derived locally for by using that is a factor of . Concerning complexity, it is easy to see that if a polynomial splits into i factors, then invokes the short vector computation \(i + (i-1)\) times: \(i-1\) invocations are used to split the polynomial 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 presented in the Berlekamp–Zassenhaus development to get a polynomial-time factorization algorithm for square-free and primitive polynomials.

We further combine this algorithm with a pre-processing algorithm also from our earlier work [7]. 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 (see Sect. 2). Each \(f_i\) is primitive and square-free, and will then be passed to . The combined algorithm factors arbitrary univariate integer polynomials into its content and a list of irreducible polynomials.

The Berlekamp–Zassenhaus algorithm has worst-case exponential complexity, e.g., exhibited on Swinnerton–Dyer polynomials. Still it is a practical algorithm, since it has polynomial average complexity [5], and this average complexity is smaller than the complexity of the LLL-based algorithm, cf. [29, Ch. 15 and 16]. Therefore, it is no surprise that our verified Berlekamp–Zassenhaus algorithm [7] significantly outperforms the verified LLL-based factorization algorithm on random polynomials, as it factors, within one minute, polynomials that the LLL-based algorithm fails to factor within any reasonable amount of time.

In the previous section we have chosen the lattice \(L_{u,k}\) for \(k = n-d\), in order to find a polynomial h that is a proper factor of f. This has the disadvantage that h is not necessarily irreducible. By contrast, Algorithm 16.22 from the textbook 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\).

The max-norm of a polynomial \(f(x) = \sum _{i=0}^n c_i x^i\) is defined to be \(|\!|f|\!|_\infty = \max \{|c_0|,\dots ,|c_n|\}\), the 1-norm is \(|\!|f|\!|_1=\sum _{i=0}^{n} |c_i|\) and is the primitive part of f, i.e., the quotient of the polynomial f by its content.

Let us note that Algorithm 16.22 also follows the common structure of a modern factorization algorithm; indeed, the reconstruction phase corresponds to steps 5-13. Once again, the idea behind this reconstruction phase is to find irreducible factors via Lemma 1 and short vectors in the lattice \(L_{u,k}\). However, this part of the algorithm (concretely, the inner loop presented at step 8) can return erroneous calculations, and some modifications are required to make it sound.

The textbook proposes the following invariants to the reconstruction phase:While the arguments given in the textbook and the provided invariants all look reasonable, the attempt to formalize them in Isabelle runs into obstacles when one tries to prove that the content of the polynomial g in step 9 is not divisible by the chosen prime p. In fact, 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 in step 9 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\).

The authors of the textbook agreed that this problem can occur. The flaw itself is easily fixed by modifying step 10 toA potential second problem revealed by our formalization work, is that if g is divisible not only by p but also by \(p^l\), Algorithm 16.22 will still return a wrong result (even with step 10 modified). Therefore, we modify the condition in step 12 of the factorization algorithm and additionally demand , and then prove that the resulting algorithm is sound. Unlike the first problem, we did not establish whether or not this second problem can actually occur.

Regarding to the implementation, apart from the required modifications to make Algorithm 16.22 sound, we also integrate some changes and optimizations:The interested reader can explore the implementation and the soundness proof of the modified algorithm in the file Factorization_Algorithm_16_22.thy of our AFP entry [9]. The file Modern_Computer_Algebra_Problem.thy in the same entry shows some examples of erroneous outputs of the textbook algorithm. A pseudo-code version of the fixed algorithm is detailed in the appendix as Algorithm 4.