How to use Montgomery arithmetic for elliptic curves (FIAT cryptography)

Question

Let us consider the source code for curve P-256 from BoringSSL. This source code can be found here. This source code uses the FIAT generated implementation for field arithmetic. This implementation can be found here. In the source generated by FIAT can be found functions for doing multiplications and additions modulo a prime (the prime from curve P-256). These functions operate on numbers in the Montgomery domain. In the p256_32.h, the function fiat_p256_from_montgomery translates a field element out of the Montgomery domain. The problem is that there is no function that translates a field element into Montgomery domain.

For example, I want to implement point doubling on curve P-256. The inputs will be a 32-byte number that represents x-coordinate and a 32-byte number that represent y-coordinate. If I want for example to square the x-coordinate I cannot use the function fiat_p256_square (provided by the FIAT generated source) because my 32-byte number isn't in the Montogomery domain. I could implement a function that translates a field element into the Montgomery domain but I find it odd that such a function is not already implemented (since this appears a critical function).

Can anybody explain to me what's the catch here? Do I really have to implement a function that translates a field element into the Montgomery domain or did I miss something?

Answer 1

fiat_p256_mul with the constant R2 value for the p-256 prime given the chosen Montgomery bit size so 256 which must be precomputed and defined somewhere. Unless the had special optimization for multiplication by a constant which they do not, then there is no reason for a to Momtgomery function beyond merely a wrapper to embed the constant for convenience.