0$ sage --version
1SageMath version 9.4, Release Date: 2021-08-22
2$ sage ./prove_group_implementations.sage
3Formula secp256k1_gej_add_var:
4Traceback (most recent call last):
5 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)
6 File "sage/structure/parent_old.pyx", line 185, in sage.structure.parent_old.Parent._coerce_c (build/cythonized/sage/structure/parent_old.c:3973)
7 File "sage/structure/parent.pyx", line 1207, in sage.structure.parent.Parent.coerce (build/cythonized/sage/structure/parent.c:10953)
8TypeError: 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
9
10During handling of the above exception, another exception occurred:
11
12Traceback (most recent call last):
13 File "secp256k1/sage/./prove_group_implementations.sage.py", line 300, in <module>
14 check_symbolic_jacobian_weierstrass("secp256k1_gej_add_var", _sage_const_0 , _sage_const_7 , _sage_const_5 , formula_secp256k1_gej_add_var)
15 File "<string>", line 255, in check_symbolic_jacobian_weierstrass
16 File "<string>", line 220, in check_symbolic_function
17 File "<string>", line 306, in check_symbolic
18 File "<string>", line 255, in prove_zero
19 File "<string>", line 230, in prove_nonzero
20 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
21 return f.reduce(gb)
22 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)
23TypeError: 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
0for (f, n) in zero.reduce(numerator(allexprs)).factor():
to
0for (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).