Signed Modulo Operator

Stream: Is there code for X?

[Aymeric Fromherz]

Hi! Is there a library/operator for a signed integer modulo operation that would return an integer between [-floor(N/2); floor((N-1)/2)] (assuming we are operating modulo N)?

The operation a % n seems to always return a number in [0; n-1], even when a is negative, while Int.mod seems to return a value between [-n + 1; n - 1].

Thanks!

[Eric Wieser]

docs#toIcoMod

[Aymeric Fromherz]

Thanks!

[Eric Wieser]

Unfortunately it's not computable, but probably it ought to be

[Jireh Loreaux]

I think there's something in std that does this version. Hold on.

[Yaël Dillies]

There's docs#Int.mod, docs#Int.fmod, docs#Int.emod, but not the one Aymeric is looking for.

[Jireh Loreaux]

No, I think it's docs#Int.fmod

[Jireh Loreaux]

(deleted)

[Scott Morrison]

I have some results about bmod (for balanced mod) with this definition. I can put them in Std sooner rather than later if that is useful.

[Scott Morrison]

What are you using it for?

[Aymeric Fromherz]

That'd be very helpful! I'm trying to prove the correctness of a Signed Montgomery Reduction, used in cryptographic code. Section 2.4 of https://eprint.iacr.org/2021/986.pdf gives a good overview of how this is supposed to work (and of the mod^{+,-}operator needed)

[Scott Morrison]

@Aymeric Fromherz https://github.com/leanprover/std4/pull/361