Switch curve25519 operations to divstep-based modular inverse

This replaces the inlined variant of "bignum_modinv" with code from
"bignum_inv_p25519" in all "curve25519_" functions returning an affine
point and hence using modular inverse. There are also a few
consequential changes related to the slightly different amount of
temporary storage needed by this function.

arm/Makefile

@@ -371,14 +371,14 @@ PROOFS = $(OBJ:.o=.correct)
 
 # Cases where a proof uses other proofs for lemmas and/or subroutines
 
-curve25519/curve25519_x25519.correct: generic/bignum_modinv.o proofs/curve25519_x25519.ml curve25519/curve25519_x25519.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/curve25519_x25519.ml";;') | $(HOLLIGHT) 2>&1) >$@
-curve25519/curve25519_x25519_alt.correct: generic/bignum_modinv.o proofs/curve25519_x25519_alt.ml curve25519/curve25519_x25519_alt.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/curve25519_x25519_alt.ml";;') | $(HOLLIGHT) 2>&1) >$@
-curve25519/curve25519_x25519_byte.correct: generic/bignum_modinv.o proofs/curve25519_x25519_byte.ml curve25519/curve25519_x25519_byte.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/curve25519_x25519_byte.ml";;') | $(HOLLIGHT) 2>&1) >$@
-curve25519/curve25519_x25519_byte_alt.correct: generic/bignum_modinv.o proofs/curve25519_x25519_byte_alt.ml curve25519/curve25519_x25519_byte_alt.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/curve25519_x25519_byte_alt.ml";;') | $(HOLLIGHT) 2>&1) >$@
-curve25519/curve25519_x25519base.correct: generic/bignum_modinv.o proofs/curve25519_x25519base.ml curve25519/curve25519_x25519base.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/curve25519_x25519base.ml";;') | $(HOLLIGHT) 2>&1) >$@
-curve25519/curve25519_x25519base_alt.correct: generic/bignum_modinv.o proofs/curve25519_x25519base_alt.ml curve25519/curve25519_x25519base_alt.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/curve25519_x25519base_alt.ml";;') | $(HOLLIGHT) 2>&1) >$@
-curve25519/curve25519_x25519base_byte.correct: generic/bignum_modinv.o proofs/curve25519_x25519base_byte.ml curve25519/curve25519_x25519base_byte.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/curve25519_x25519base_byte.ml";;') | $(HOLLIGHT) 2>&1) >$@
-curve25519/curve25519_x25519base_byte_alt.correct: generic/bignum_modinv.o proofs/curve25519_x25519base_byte_alt.ml curve25519/curve25519_x25519base_byte_alt.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/curve25519_x25519base_byte_alt.ml";;') | $(HOLLIGHT) 2>&1) >$@
+curve25519/curve25519_x25519.correct: curve25519/bignum_inv_p25519.o proofs/curve25519_x25519.ml curve25519/curve25519_x25519.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/curve25519_x25519.ml";;') | $(HOLLIGHT) 2>&1) >$@
+curve25519/curve25519_x25519_alt.correct: curve25519/bignum_inv_p25519.o proofs/curve25519_x25519_alt.ml curve25519/curve25519_x25519_alt.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/curve25519_x25519_alt.ml";;') | $(HOLLIGHT) 2>&1) >$@
+curve25519/curve25519_x25519_byte.correct: curve25519/bignum_inv_p25519.o proofs/curve25519_x25519_byte.ml curve25519/curve25519_x25519_byte.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/curve25519_x25519_byte.ml";;') | $(HOLLIGHT) 2>&1) >$@
+curve25519/curve25519_x25519_byte_alt.correct: curve25519/bignum_inv_p25519.o proofs/curve25519_x25519_byte_alt.ml curve25519/curve25519_x25519_byte_alt.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/curve25519_x25519_byte_alt.ml";;') | $(HOLLIGHT) 2>&1) >$@
+curve25519/curve25519_x25519base.correct: curve25519/bignum_inv_p25519.o proofs/curve25519_x25519base.ml curve25519/curve25519_x25519base.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/curve25519_x25519base.ml";;') | $(HOLLIGHT) 2>&1) >$@
+curve25519/curve25519_x25519base_alt.correct: curve25519/bignum_inv_p25519.o proofs/curve25519_x25519base_alt.ml curve25519/curve25519_x25519base_alt.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/curve25519_x25519base_alt.ml";;') | $(HOLLIGHT) 2>&1) >$@
+curve25519/curve25519_x25519base_byte.correct: curve25519/bignum_inv_p25519.o proofs/curve25519_x25519base_byte.ml curve25519/curve25519_x25519base_byte.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/curve25519_x25519base_byte.ml";;') | $(HOLLIGHT) 2>&1) >$@
+curve25519/curve25519_x25519base_byte_alt.correct: curve25519/bignum_inv_p25519.o proofs/curve25519_x25519base_byte_alt.ml curve25519/curve25519_x25519base_byte_alt.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/curve25519_x25519base_byte_alt.ml";;') | $(HOLLIGHT) 2>&1) >$@
 curve25519/edwards25519_scalarmulbase.correct: generic/bignum_modinv.o proofs/edwards25519_scalarmulbase.ml curve25519/edwards25519_scalarmulbase.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/edwards25519_scalarmulbase.ml";;') | $(HOLLIGHT) 2>&1) >$@
 curve25519/edwards25519_scalarmulbase_alt.correct: generic/bignum_modinv.o proofs/edwards25519_scalarmulbase_alt.ml curve25519/edwards25519_scalarmulbase_alt.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/edwards25519_scalarmulbase_alt.ml";;') | $(HOLLIGHT) 2>&1) >$@
 curve25519/edwards25519_scalarmuldouble.correct: generic/bignum_modinv.o proofs/edwards25519_scalarmuldouble.ml curve25519/edwards25519_scalarmuldouble.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/edwards25519_scalarmuldouble.ml";;') | $(HOLLIGHT) 2>&1) >$@