TypeError in prove_group_implementations.sage #1067

issue jonasnick opened this issue on January 30, 2022

jonasnick commented at 8:38 PM on January 30, 2022: contributor

$ 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():

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).

sipa commented at 8:41 PM on January 30, 2022: contributor

Hmm, it works for me, in Sage 9.2.
real-or-random referenced this in commit e108d0039c on Jan 31, 2022
real-or-random cross-referenced this on Jan 31, 2022 from issue sage: Fix incompatibility with sage 9.4 by real-or-random

jonasnick commented at 4:58 PM on January 31, 2022: contributor

@sipa Just to be clear, that means that you do not see the following failures in the output?

Formula secp256k1_gej_add_var:
  add:
    branch 4: FAIL, <map object at 0x7f417d48b820> fails (assuming )
...
Formula secp256k1_gej_add_zinv_var:
  add:
    branch 4: FAIL, <map object at 0x7f417d67d420> fails (assuming )
...

sipa commented at 5:01 PM on January 31, 2022: contributor

My output as of commit d8a246324650c3df8d54d133a8ac3c1b857a7a4e (master):

$ sage --version; sage prove_group_implementations.sage 
SageMath version 9.2, Release Date: 2020-10-24
Formula secp256k1_gej_add_var:
  add:
    branch 4: OK
  double:
    branch 2: OK
  add_opposite:
    branch 3: OK
  add_infinite_a:
    branch 0: OK
  add_infinite_b:
    branch 1: OK
  add_infinite_ab:
    branch 0: OK

Formula secp256k1_gej_add_ge_var:
  add:
    branch 4: OK (assuming Bz - 1 = 0 [b.z=1])
  double:
    branch 2: OK (assuming Bz - 1 = 0 [b.z=1])
  add_opposite:
    branch 3: OK (assuming Bz - 1 = 0 [b.z=1])
  add_infinite_a:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1])
  add_infinite_b:
    branch 1: OK (assuming Bz - 1 = 0 [b.z=1])
  add_infinite_ab:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1])

Formula secp256k1_gej_add_zinv_var:
  add:
    branch 4: OK
  double:
    branch 2: OK
  add_opposite:
    branch 3: OK
  add_infinite_a:
    branch 1: OK
  add_infinite_b:
    branch 0: OK
  add_infinite_ab:
    branch 0: OK

Formula secp256k1_gej_add_ge:
  add:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
    branch 2: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
    branch 3: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  double:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  add_opposite:
    branch 9: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  add_infinite_a:
    branch 4: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
    branch 6: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
    branch 7: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
    branch 13: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  add_infinite_b:
  add_infinite_ab:

Formula secp256k1_gej_add_ge_old [should fail]:
  add:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
    branch 2: FAIL, ['finite_point', 'on_curve', 'colinear_1', 'colinear_2', 'colinear_3'] fails (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  double:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  add_opposite:
    branch 2: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  add_infinite_a:
    branch 1: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  add_infinite_b:
  add_infinite_ab:

My output as of eb86372d5d411ccf200a3add49111d9c197d7dce (#1068):

$ sage --version; sage prove_group_implementations.sage 
SageMath version 9.2, Release Date: 2020-10-24
Formula secp256k1_gej_add_var:
  add:
    branch 4: OK
  double:
    branch 2: OK
  add_opposite:
    branch 3: OK
  add_infinite_a:
    branch 0: OK
  add_infinite_b:
    branch 1: OK
  add_infinite_ab:
    branch 0: OK

Formula secp256k1_gej_add_ge_var:
  add:
    branch 4: OK (assuming Bz - 1 = 0 [b.z=1])
  double:
    branch 2: OK (assuming Bz - 1 = 0 [b.z=1])
  add_opposite:
    branch 3: OK (assuming Bz - 1 = 0 [b.z=1])
  add_infinite_a:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1])
  add_infinite_b:
    branch 1: OK (assuming Bz - 1 = 0 [b.z=1])
  add_infinite_ab:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1])

Formula secp256k1_gej_add_zinv_var:
  add:
    branch 4: OK
  double:
    branch 2: OK
  add_opposite:
    branch 3: OK
  add_infinite_a:
    branch 1: OK
  add_infinite_b:
    branch 0: OK
  add_infinite_ab:
    branch 0: OK

Formula secp256k1_gej_add_ge:
  add:
    branch 0: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
    branch 2: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
    branch 3: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
  double:
    branch 0: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
  add_opposite:
    branch 9: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
  add_infinite_a:
    branch 4: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
    branch 6: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
    branch 7: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
    branch 13: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
  add_infinite_b:
  add_infinite_ab:

Formula secp256k1_gej_add_ge_old [should fail]:
  add:
    branch 0: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
    branch 2: FAIL, ['finite_point', 'on_curve', 'colinear_1', 'colinear_2', 'colinear_3'] fails (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
  double:
    branch 0: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
  add_opposite:
    branch 2: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
  add_infinite_a:
    branch 1: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
  add_infinite_b:
  add_infinite_ab:

siv2r commented at 10:32 AM on February 1, 2022: contributor

The branch 4 of gej_add_var and gej_add_zinv_var fails on SageMath version 9.4, Release Date: 2021-08-22

<details> <summary> Output on sage v9.4 </summary>

sage: load("prove_group_implementations.sage")                                            
Formula secp256k1_gej_add_var:
  add:
    branch 4: FAIL, <map object at 0x7fdf43f902b0> fails (assuming )
  double:
    branch 2: OK
  add_opposite:
    branch 3: OK
  add_infinite_a:
    branch 0: OK
  add_infinite_b:
    branch 1: OK
  add_infinite_ab:
    branch 0: OK

Formula secp256k1_gej_add_ge_var:
  add:
    branch 4: OK (assuming Bz - 1 = 0 [b.z=1])
  double:
    branch 2: OK (assuming Bz - 1 = 0 [b.z=1])
  add_opposite:
    branch 3: OK (assuming Bz - 1 = 0 [b.z=1])
  add_infinite_a:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1])
  add_infinite_b:
    branch 1: OK (assuming Bz - 1 = 0 [b.z=1])
  add_infinite_ab:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1])

Formula secp256k1_gej_add_zinv_var:
  add:
    branch 4: FAIL, <map object at 0x7fdf443faac0> fails (assuming )
  double:
    branch 2: OK
  add_opposite:
    branch 3: OK
  add_infinite_a:
    branch 1: OK
  add_infinite_b:
    branch 0: OK
  add_infinite_ab:
    branch 0: OK

Formula secp256k1_gej_add_ge:
  add:
    branch 0: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
    branch 2: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
    branch 3: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
  double:
    branch 0: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
  add_opposite:
    branch 9: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
  add_infinite_a:
    branch 4: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
    branch 6: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
    branch 7: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
    branch 13: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
  add_infinite_b:
  add_infinite_ab:

Formula secp256k1_gej_add_ge_old [should fail]:
  add:
    branch 0: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
    branch 2: FAIL, ['finite_point', 'on_curve', 'colinear_1', 'colinear_2', 'colinear_3'] fails (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
  double:
    branch 0: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
  add_opposite:
    branch 2: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
  add_infinite_a:
    branch 1: OK (assuming Bi = 0 [b_finite], Bz - 1 = 0 [b.z=1])
  add_infinite_b:
  add_infinite_ab:

</details>

But there was no TypeError in my case. I used CoCalc to run the sage scripts.

On running, sage ./prove_group_implementations.sage for sage v9.0 (on my local machine) there are no errors (with or without the change_ring workaround).

<details> <summary> Output on sage v9.0 </summary>

$ sage --version;sage ./prove_group_implementations.sage
SageMath version 9.0, Release Date: 2020-01-01
Formula secp256k1_gej_add_var:
  add:
    branch 4: OK
  double:
    branch 2: OK
  add_opposite:
    branch 3: OK
  add_infinite_a:
    branch 0: OK
  add_infinite_b:
    branch 1: OK
  add_infinite_ab:
    branch 0: OK

Formula secp256k1_gej_add_ge_var:
  add:
    branch 4: OK (assuming Bz - 1 = 0 [b.z=1])
  double:
    branch 2: OK (assuming Bz - 1 = 0 [b.z=1])
  add_opposite:
    branch 3: OK (assuming Bz - 1 = 0 [b.z=1])
  add_infinite_a:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1])
  add_infinite_b:
    branch 1: OK (assuming Bz - 1 = 0 [b.z=1])
  add_infinite_ab:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1])

Formula secp256k1_gej_add_zinv_var:
  add:
    branch 4: OK
  double:
    branch 2: OK
  add_opposite:
    branch 3: OK
  add_infinite_a:
    branch 1: OK
  add_infinite_b:
    branch 0: OK
  add_infinite_ab:
    branch 0: OK

Formula secp256k1_gej_add_ge:
  add:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
    branch 2: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
    branch 3: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  double:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  add_opposite:
    branch 9: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  add_infinite_a:
    branch 4: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
    branch 6: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
    branch 7: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
    branch 13: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  add_infinite_b:
  add_infinite_ab:

Formula secp256k1_gej_add_ge_old [should fail]:
  add:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
    branch 2: FAIL, ['finite_point', 'on_curve', 'colinear_1', 'colinear_2', 'colinear_3'] fails (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  double:
    branch 0: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  add_opposite:
    branch 2: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  add_infinite_a:
    branch 1: OK (assuming Bz - 1 = 0 [b.z=1], Bi = 0 [b_finite])
  add_infinite_b:
  add_infinite_ab:

</details>

jonasnick closed this on Feb 5, 2022
dderjoel referenced this in commit 9a3a468ff4 on May 23, 2023
matteonardelli referenced this in commit a84443afca on Jun 16, 2023

Contributors

jonasnick

sipa

siv2r

Linked (view graph)

#1068 sage: Fix incompatibility with sage 9.4