This is the supporting material for the paper A Verified Implementation of the Berlekamp–Zassenhaus Factorization Algorithm by Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada. Abstract We formalize the Berlekamp--Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yun's square-free factorization algorithm to integer polynomials, and thus provide an efficient and certified factorization algorithm for arbitrary univariate polynomials. The algorithm first performs factorization in the prime field GF(p) and then performs computations in the ring of integers modulo pk, where both p and k are determined at runtime. Since a natural modeling of these structures via dependent types is not possible in Isabelle/HOL, we formalize the whole algorithm using locales and local type definitions. Through experiments we verify that our algorithm factors polynomials of degree up to 500 within seconds. Formalization The formalization is part of the Archive of Formal Proofs for Isabelle 2018 within the entry The Factorization Algorithm of Berlekamp and Zassenhaus. The following list documents the relationship between the paper and the formalization: Section 1 Introduction Theorem 1 (page 2): factorize_int_poly Section 3 Formalizing Prime Fields Lemma 1 (page 6): coprime_pderiv_imp_square_free Lemma 2 (page 8): square_free_mod_imp_square_free Lemma 3 (page 8): times_MP_Rel Lemma 4 (page 8): degree_mult_eq Lemma 5 (page 8): poly_mod_prime_type.degree_m_mult_eq Lemma 6 (page 8): poly_mod_prime.degree_m_mult_eq Lemma 7 (page 10): gcd_eucl_i Lemma 8 (page 10): finite_field_ops_integer Lemma 9 (page 11): finite_field_ops32 Lemma 10 (page 11): finite_field_ops64 Lemma 11 (page 11): euclidean_ring_ops_poly Lemma 12 (page 11): poly_rel_gcd Lemma 13 (page 12): prime_field_gen.square_free_impl(1) Lemma 14 (page 12): poly_mod_prime.square_free_impl(1) Section 4 Square-Free Factorization of Integer Polynomials Theorem 2 (page 13): square_free_factorization_int Section 5 Square-Free Polynomials in Lemma 15 (page 14): suitable_prime_bz Section 6 Berlekamp's Algorithm Theorem 3 (page 18): berlekamp_monic_factorization Lemma 17 (page 19): degree_divisor1 Lemma 17 (page 19): degree_divisor2 Theorem 4 (page 20): finite_field_factorization Theorem 5 (page 22): finite_field_factorization_int Section 7 Mignotte's Factor Bound Lemma 18 (page 22): factor_bound Lemma 19 (page 24): log_ceiling Section 8 Hensel Lifting Lemma 21 (page 27): hensel_1 Lemma 22 (page 27): unique_hensel_binary Lemma 23 (page 29): hensel_lifting_unique Section 9 Reconstructing True Factors Theorem 6 (page 31): zassenhaus_reconstruction Section 10 Assembled Factorization Algorithm Theorem 7 (page 32): berlekamp_zassenhaus_factorization_irreducible Theorem 8 (page 32): internal_int_poly_factorization_mem Theorem 8 (page 32): internal_int_poly_factorization Experiments One can rerun the experiments as follows: Download and extract the attached file. Inspect the path of the constant binary within the file experiments/Code_Old/Mathematica.hs whether it matches your Mathematica installation. Otherwise you can deactivate the Mathematica experiments by disabling the external factorization in experiments/Experiments/run_experiment.sh. Compile experiments/Code_Old/Main and experiments/Code_New/Main with -O2 Invoke ./experiments/Experiments/run_experiments.sh To turn the raw data into .csv-files and generated the Mathematica-graph, change to the experiments/Experiments directory and invoke ./time_tables_to_mathematica.sh To get the pdf-file, paste the output of the previous command into the first line of the Mathematica-file journal_plot.nb One can also run the experiments disabling some of the optimizations by means of the files Code_New_No_{...}/Main.hs In addition, the files Comparison.xlsx, Profiling.xlsx and Optimization_Table.xlsx contain the exact time for factoring each polynomial, the profiling results and a table comparing the results of each improvement respectively. The Isabelle file Generate_Code.thy also generates the Haskell sources. The following table contains all the experiments of Figure 1 in the article. Polynomial Mathematica Old New poly_100.poly 0.478s 0.194s 0.085s poly_101.poly 0.449s 0.209s 0.095s poly_102.poly 0.475s 0.247s 0.145s poly_103.poly 0.491s 0.171s 0.109s poly_104.poly 0.479s 0.131s 0.096s poly_105.poly 0.492s 0.276s 0.140s poly_106.poly 0.458s 0.148s 0.097s poly_107.poly 0.463s 0.180s 0.107s poly_108.poly 0.472s 0.216s 0.122s poly_109.poly 0.477s 0.154s 0.103s poly_110.poly 0.457s 0.180s 0.119s poly_111.poly 0.465s 0.218s 0.122s poly_112.poly 0.487s 0.217s 0.132s poly_113.poly 0.471s 0.130s 0.084s poly_114.poly 0.465s 0.269s 0.120s poly_115.poly 0.464s 0.243s 0.105s poly_116.poly 0.457s 0.269s 0.122s poly_117.poly 0.476s 0.333s 0.135s poly_118.poly 0.498s 0.220s 0.082s poly_119.poly 0.462s 0.228s 0.134s poly_120.poly 0.449s 0.318s 0.109s poly_121.poly 0.485s 0.271s 0.181s poly_122.poly 0.483s 0.229s 0.108s poly_123.poly 0.465s 0.254s 0.147s poly_124.poly 0.495s 0.278s 0.158s poly_125.poly 0.460s 0.378s 0.157s poly_126.poly 0.480s 0.306s 0.168s poly_127.poly 0.476s 0.328s 0.198s poly_128.poly 0.492s 0.272s 0.144s poly_129.poly 0.464s 0.421s 0.226s poly_130.poly 0.483s 0.267s 0.132s poly_131.poly 0.497s 0.329s 0.158s poly_132.poly 0.471s 0.482s 0.241s poly_133.poly 0.493s &