PrimeEC::ec_mult can produce incorrect results

[weaversa]

Cryptol> :m PrimeEC
Loading module Cryptol
Loading module PrimeEC
PrimeEC> ec_mult`{13} 3 {x = 0, y = 0, z = 1}
{x = 0, y = 13, z = 1}
PrimeEC> :t ec_mult`{13}
ec_mult`{13} : Z 13 -> ProjectivePoint 13 -> ProjectivePoint 13
PrimeEC> ec_mult`{13} 3 {x = 0, y = 0, z = 1} : ProjectivePoint 13
{x = 0, y = 13, z = 1}
PrimeEC> {x = 0, y = 13, z = 1} : ProjectivePoint 13
[error] at <interactive>:334:13--334:15:
  • Unsolvable constraint:
      13 >= 14
        arising from
        use of literal or demoted expression
        at <interactive>:334:13--334:15

This is very strange behavior.

[yav]

The elements of ProjectivePair 13 are supposed to be Z 13, and 13 is clearly not a valid value of this type, so the first answer is incorrect. I am not sure if it is just missing a reduction, or the algorithm is incorrect, we'll need to investigate this. The code implementing it is here:

cryptol/src/Cryptol/PrimeEC.hs

Line 290 in 4afba5f

ec_mult :: PrimeModulus -> Integer -> ProjectivePoint -> ProjectivePoint

[RyanGlScott]

Using the :sat command produces different results:

PrimeEC> :set prover=w4-z3
PrimeEC> :sat \x -> ec_mult`{13} 3 {x = 0, y = 0, z = 1} == x
[Warning] Uninterpreted functions used to represent Prime ECC operations.
Satisfiable
(\x -> ec_mult`{13} 3 {x = 0, y = 0, z = 1} == x)
  {x = 0, y = 0, z = 0}
  = True
(Total Elapsed Time: 0.030s, using "Z3")

PrimeEC> :set prover=w4-yices
PrimeEC> :sat \x -> ec_mult`{13} 3 {x = 0, y = 0, z = 1} == x
[Warning] Uninterpreted functions used to represent Prime ECC operations.
Satisfiable
(\x -> ec_mult`{13} 3 {x = 0, y = 0, z = 1} == x)
  {x = 2, y = 8, z = 11}
  = True
(Total Elapsed Time: 0.004s, using "Yices")

[weaversa]

@RyanGlScott That's because the function isn't symbolically executed, but rather uninterpreted. So, the SMT solver can say whatever it likes.

[mccleeary-galois]

https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=e1b05e600bfcdeecf8555bc9948483c5fbbdd478

Adding this for an easy link for the source paper of the code in question.