Add P-256 Montgomery-Jacobian scalar multiplication operation

The new function p256_montjscalarmul[_alt] is analogous to the
existing p256_scalarmul[_alt], doing scalar multiplication n * P for a
point P on the NIST P-256 curve and a scalar n. This variant, however,
uses the Jacobian representation for both input and output points,
with the coordinates in Montgomery form. As such, it is approximately
the same as the "middle" of p256_scalarmul, excluding the mappings
from and back to affine form; it may make a more convenient
building-block for other operations.

arm/Makefile

@@ -97,6 +97,8 @@ POINT_OBJ = curve25519/curve25519_ladderstep.o \
             p256/p256_montjdouble_alt.o \
             p256/p256_montjmixadd.o \
             p256/p256_montjmixadd_alt.o \
+            p256/p256_montjscalarmul.o \
+            p256/p256_montjscalarmul_alt.o \
             p256/p256_scalarmul.o \
             p256/p256_scalarmul_alt.o \
             p256/p256_scalarmulbase.o \
@@ -413,6 +415,8 @@ curve25519/edwards25519_scalarmulbase_alt.correct: curve25519/bignum_inv_p25519.
 curve25519/edwards25519_scalarmuldouble.correct: curve25519/bignum_inv_p25519.o proofs/edwards25519_scalarmuldouble.ml curve25519/edwards25519_scalarmuldouble.o ; ../tools/run-proof.sh arm edwards25519_scalarmuldouble "$(HOLLIGHT)" $@
 curve25519/edwards25519_scalarmuldouble_alt.correct: curve25519/bignum_inv_p25519.o proofs/edwards25519_scalarmuldouble_alt.ml curve25519/edwards25519_scalarmuldouble_alt.o ; ../tools/run-proof.sh arm edwards25519_scalarmuldouble_alt "$(HOLLIGHT)" $@
 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 ; ../tools/run-proof.sh arm bignum_modexp "$(HOLLIGHT)" $@
+p256/p256_montjscalarmul.correct: proofs/p256_montjadd.ml p256/p256_montjadd.o proofs/p256_montjdouble.ml p256/p256_montjdouble.o proofs/p256_montjscalarmul.ml p256/p256_montjscalarmul.o ; ../tools/run-proof.sh arm p256_montjscalarmul "$(HOLLIGHT)" $@
+p256/p256_montjscalarmul_alt.correct: proofs/p256_montjadd_alt.ml p256/p256_montjadd_alt.o proofs/p256_montjdouble_alt.ml p256/p256_montjdouble_alt.o proofs/p256_montjscalarmul_alt.ml p256/p256_montjscalarmul_alt.o ; ../tools/run-proof.sh arm p256_montjscalarmul_alt "$(HOLLIGHT)" $@
 p256/p256_scalarmul.correct: proofs/bignum_demont_p256.ml p256/bignum_demont_p256.o proofs/bignum_inv_p256.ml p256/bignum_inv_p256.o proofs/bignum_montmul_p256.ml p256/bignum_montmul_p256.o proofs/bignum_montsqr_p256.ml p256/bignum_montsqr_p256.o proofs/bignum_tomont_p256.ml p256/bignum_tomont_p256.o proofs/p256_montjadd.ml p256/p256_montjadd.o proofs/p256_montjdouble.ml p256/p256_montjdouble.o proofs/p256_montjmixadd.ml p256/p256_montjmixadd.o proofs/p256_scalarmul.ml p256/p256_scalarmul.o ; ../tools/run-proof.sh arm p256_scalarmul "$(HOLLIGHT)" $@
 p256/p256_scalarmul_alt.correct: proofs/bignum_demont_p256.ml p256/bignum_demont_p256.o proofs/bignum_inv_p256.ml p256/bignum_inv_p256.o proofs/bignum_montmul_p256_alt.ml p256/bignum_montmul_p256_alt.o proofs/bignum_montsqr_p256_alt.ml p256/bignum_montsqr_p256_alt.o proofs/bignum_tomont_p256.ml p256/bignum_tomont_p256.o proofs/p256_montjadd_alt.ml p256/p256_montjadd_alt.o proofs/p256_montjdouble_alt.ml p256/p256_montjdouble_alt.o proofs/p256_montjmixadd_alt.ml p256/p256_montjmixadd_alt.o proofs/p256_scalarmul_alt.ml p256/p256_scalarmul_alt.o ; ../tools/run-proof.sh arm p256_scalarmul_alt "$(HOLLIGHT)" $@
 p256/p256_scalarmulbase.correct: proofs/bignum_demont_p256.ml p256/bignum_demont_p256.o proofs/bignum_inv_p256.ml p256/bignum_inv_p256.o proofs/bignum_montmul_p256.ml p256/bignum_montmul_p256.o proofs/bignum_montsqr_p256.ml p256/bignum_montsqr_p256.o proofs/p256_montjmixadd.ml p256/p256_montjmixadd.o proofs/p256_scalarmulbase.ml p256/p256_scalarmulbase.o ; ../tools/run-proof.sh arm p256_scalarmulbase "$(HOLLIGHT)" $@

arm/p256/Makefile

@@ -54,6 +54,8 @@ OBJ = bignum_add_p256.o \
       p256_montjdouble_alt.o \
       p256_montjmixadd.o \
       p256_montjmixadd_alt.o \
+      p256_montjscalarmul.o \
+      p256_montjscalarmul_alt.o \
       p256_scalarmul.o \
       p256_scalarmul_alt.o \
       p256_scalarmulbase.o \