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?