Open fjarri opened 4 years ago
See the line a = submod(a, p2, m). submod() requires both of its first two arguments to be lower than m, but I am not sure how to prove that a satisfies that.
a = submod(a, p2, m)
submod()
m
a
On the other hand, exhaustive tests with MLUInt{2} pass, so perhaps it's okay?
MLUInt{2}
See the line
a = submod(a, p2, m).submod()requires both of its first two arguments to be lower thanm, but I am not sure how to prove thatasatisfies that.On the other hand, exhaustive tests with
MLUInt{2}pass, so perhaps it's okay?