TypeError in prove_group_implementations.sage #1067
Description
$ sage --version
SageMath version 9.4, Release Date: 2021-08-22
$ sage ./prove_group_implementations.sage
Formula secp256k1_gej_add_var:
Traceback (most recent call last):
File "sage/rings/polynomial/multi_polynomial_libsingular.pyx", line 4680, in sage.rings.polynomial.multi_polynomial_libsingular.MPolynomial_libsingular.reduce (build/cythonized/sage/rings/polynomial/multi_polynomial_libsingular.cpp:36255)
File "sage/structure/parent_old.pyx", line 185, in sage.structure.parent_old.Parent._coerce_c (build/cythonized/sage/structure/parent_old.c:3973)
File "sage/structure/parent.pyx", line 1207, in sage.structure.parent.Parent.coerce (build/cythonized/sage/structure/parent.c:10953)
TypeError: no canonical coercion from Multivariate Polynomial Ring in ax, bx, ay, by, Az, Bz, Ai, Bi over Rational Field to Multivariate Polynomial Ring in ax, bx, ay, by, Az, Bz, Ai, Bi over Integer Ring
During handling of the above exception, another exception occurred:
Traceback (most recent call last):
File "secp256k1/sage/./prove_group_implementations.sage.py", line 300, in <module>
check_symbolic_jacobian_weierstrass("secp256k1_gej_add_var", _sage_const_0 , _sage_const_7 , _sage_const_5 , formula_secp256k1_gej_add_var)
File "<string>", line 255, in check_symbolic_jacobian_weierstrass
File "<string>", line 220, in check_symbolic_function
File "<string>", line 306, in check_symbolic
File "<string>", line 255, in prove_zero
File "<string>", line 230, in prove_nonzero
File "/nix/store/fj99mwys7crk5iifzym7q1m4li9ksknc-python3-3.9.9-env/lib/python3.9/site-packages/sage/rings/polynomial/multi_polynomial_ideal.py", line 4530, in reduce
return f.reduce(gb)
File "sage/rings/polynomial/multi_polynomial_libsingular.pyx", line 4683, in sage.rings.polynomial.multi_polynomial_libsingular.MPolynomial_libsingular.reduce (build/cythonized/sage/rings/polynomial/multi_polynomial_libsingular.cpp:36314)
TypeError: no canonical coercion from Multivariate Polynomial Ring in ax, bx, ay, by, Az, Bz, Ai, Bi over Rational Field to Multivariate Polynomial Ring in ax, bx, ay, by, Az, Bz, Ai, Bi over Integer Ring
For what it's worth, I have only very limited understanding of what the sage script does, but if I change line 230 in group_prover.sage from
for (f, n) in zero.reduce(numerator(allexprs)).factor():
to
for (f, n) in zero.reduce(numerator(allexprs).change_ring(QQ)).factor():
the type error disappears, but running sage ./prove_group_implementations.sage reports failure for secp256k1_gej_add_var (add) and secp256k1_gej_add_zinv_var (add).