Add prime constraint to inverse function

[marsella]

The mp_mod_inv method in Common/utils.cry is used in several places, but its type signature is not correct; it's only a valid function when the modulus is prime. Cryptol has evolved since that function was first written in 2018, so now I see two options to make it correct:

1. Add a prime p constraint to the function type constraint
2. Replace all uses with the recip and/or /. cryptol-native operators on Z types.

I did a quick review of all the modules that use this and it looks like they do all use it correctly (e.g. with a prime modulus). If we choose option 1, there will be some cascading work to add the prime constraint up the call chain, but that seems worth the precision to me.

That said, if the built-in operations do what I think they do (compute the multiplicative inverse and do modulus-respecting division), we should use those. We might consider improving documentation on those as well, to be explicit about any additional constraints they may have (e.g. does the modulus have to be prime for those operations? I don't know).

• Pick an option to make the inverse function correct
• Propagate it throughout the codebase
• Update any missing documentation / add useful clarifications where necessary