Switch edwards25519 operations to divstep-based modular inverse

This replaces the inlined variant of "bignum_modinv" with code from
"bignum_inv_p25519" in all "edwards25519_scalarmul*" functions.
Again, there are consequential changes related to the slightly
different amount of temporary storage needed by bignum_inv_p25519.

arm/Makefile

@@ -379,10 +379,10 @@ curve25519/curve25519_x25519base.correct: curve25519/bignum_inv_p25519.o proofs/
 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) >$@
-curve25519/edwards25519_scalarmuldouble_alt.correct: generic/bignum_modinv.o proofs/edwards25519_scalarmuldouble_alt.ml curve25519/edwards25519_scalarmuldouble_alt.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/edwards25519_scalarmuldouble_alt.ml";;') | $(HOLLIGHT) 2>&1) >$@
+curve25519/edwards25519_scalarmulbase.correct: curve25519/bignum_inv_p25519.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: curve25519/bignum_inv_p25519.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: curve25519/bignum_inv_p25519.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) >$@
+curve25519/edwards25519_scalarmuldouble_alt.correct: curve25519/bignum_inv_p25519.o proofs/edwards25519_scalarmuldouble_alt.ml curve25519/edwards25519_scalarmuldouble_alt.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/edwards25519_scalarmuldouble_alt.ml";;') | $(HOLLIGHT) 2>&1) >$@
 generic/bignum_modexp.correct: generic/bignum_amontifier.correct generic/bignum_amontmul.correct generic/bignum_demont.correct generic/bignum_mux.correct proofs/bignum_modexp.ml generic/bignum_modexp.o ; (cd ..; (echo 'loadt "arm/proofs/base.ml";;'; echo 'loadt "arm/proofs/bignum_modexp.ml";;') | $(HOLLIGHT) 2>&1) >$@
 
 # All other other instances are standalone