r"""
Verified polynomial factorization over ZZ
=========================================

Factors a univariate polynomial over Z using verified code.
It calls an external binary called factor_poly_verified that has been generated
from a verified functional implementation of the Berlekamp and Zassenhaus algorithm.
Verification and code generation were done in the Isabelle proof assistant
by  Divasón, Joosten, Thiemann and Yamada.
For details see this article in the Archive of Formal Proofs:
https://www.isa-afp.org/entries/Berlekamp_Zassenhaus.html

The polynomial is passed to factor_poly_verified as a string of the form "[a0,a1,...]"
representing a list of coefficients (in increasing order of degree)
of the polynomial over ZZ. The factorization is returned as a string of the form
"[c, [[a00, a01, ...], e0], [[a10, a11, ...], e1], ...]"
with a leading coefficient c and a list of pairs [factor, exponent],
where each factor is represented by its list of coefficients.

AUTHORS
  Tobias Nipkow and Samuel Lelièvre
  Initial version (2023-10) prepared at Dagstuhl seminar 23401:
    "Automated mathematics: integrating proofs, algorithms and data"
"""

import subprocess

def factor_polynomial_verified(poly):
    r"""
    Return a verified factorization of this univariate polynomial over ZZ

    EXAMPLES::

        sage: x = polygen(ZZ)
        sage: f = 6 * (x^2 + 2*x + 1)
        sage: factor_polynomial_verified(f)
        (6) * (x + 1)^2
        sage: g = x^16 + 4*x^12 - 16*x^11 + 80*x^9 + 2*x^8 + 160*x^7 + 128*x^6 - 160*x^5 + 28*x^4 - 48*x^3 + 128*x^2 - 16*x + 1
        sage: h = x^16 + 4*x^12 + 16*x^11 - 80*x^9 + 2*x^8 - 160*x^7 + 128*x^6 + 160*x^5 + 28*x^4 + 48*x^3 + 128*x^2 + 16*x + 1
        sage: factor_polynomial_verified(g * h)
        (x^16 + 4*x^12 - 16*x^11 + 80*x^9 + 2*x^8 + 160*x^7 + 128*x^6 - 160*x^5 + 28*x^4 - 48*x^3 + 128*x^2 - 16*x + 1) * (x^16 + 4*x^12 + 16*x^11 - 80*x^9 + 2*x^8 - 160*x^7 + 128*x^6 + 160*x^5 + 28*x^4 + 48*x^3 + 128*x^2 + 16*x + 1)
    """

    poly_ring = poly.parent()
    factors_string = subprocess.run(["./factor_polynomial_verified"],
       input=str(poly.list()) + "\n", capture_output=True, text=True).stdout
    # Convert string to sage object using sage_eval
    # Warning: unsafe because the string may contain malicious code injection
    coeff, factors = sage_eval(factors_string)
    return Factorization([(poly_ring(cs), k) for cs,k in factors], unit=coeff)