Add basic P-521 Jacobian coordinate scalar multiplication

The new function p521_jscalarmul[_alt] is the NIST P-521 analog
of the corresponding P-256 and P-384 functions: it does scalar
multiplication of a point on the P-521 curve, where both input and
output points are in Jacobian representation. But in contrast to
the P-256 and P-284 functions, Montgomery form is *not* used.

This update also fixes a few miscellaneous issues in tests and
improves the specs of some other P-521 functions by fixing the
nominal size parameter in "modular_decode". (It is actually not
semantically relevant, being there to maintain the analog with
"montgomery_decode".)

arm/Makefile

@@ -117,6 +117,8 @@ POINT_OBJ = curve25519/curve25519_ladderstep.o \
             p521/p521_jdouble_alt.o \
             p521/p521_jmixadd.o \
             p521/p521_jmixadd_alt.o \
+            p521/p521_jscalarmul.o \
+            p521/p521_jscalarmul_alt.o \
             secp256k1/secp256k1_jadd.o \
             secp256k1/secp256k1_jadd_alt.o \
             secp256k1/secp256k1_jdouble.o \
@@ -443,6 +445,8 @@ p256/p256_scalarmulbase.correct: proofs/bignum_demont_p256.ml p256/bignum_demont
 p256/p256_scalarmulbase_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/p256_montjmixadd_alt.ml p256/p256_montjmixadd_alt.o proofs/p256_scalarmulbase_alt.ml p256/p256_scalarmulbase_alt.o ; ../tools/run-proof.sh arm p256_scalarmulbase_alt "$(HOLLIGHT)" $@
 p384/p384_montjscalarmul.correct: proofs/p384_montjadd.ml p384/p384_montjadd.o proofs/p384_montjdouble.ml p384/p384_montjdouble.o proofs/p384_montjscalarmul.ml p384/p384_montjscalarmul.o ; ../tools/run-proof.sh arm p384_montjscalarmul "$(HOLLIGHT)" $@
 p384/p384_montjscalarmul_alt.correct: proofs/p384_montjadd_alt.ml p384/p384_montjadd_alt.o proofs/p384_montjdouble_alt.ml p384/p384_montjdouble_alt.o proofs/p384_montjscalarmul_alt.ml p384/p384_montjscalarmul_alt.o ; ../tools/run-proof.sh arm p384_montjscalarmul_alt "$(HOLLIGHT)" $@
+p521/p521_jscalarmul.correct: proofs/bignum_mod_n521_9.ml p521/bignum_mod_n521_9.o proofs/bignum_mod_p521_9.ml p521/bignum_mod_p521_9.o proofs/p521_jadd.ml p521/p521_jadd.o proofs/p521_jdouble.ml p521/p521_jdouble.o proofs/p521_jscalarmul.ml p521/p521_jscalarmul.o ; ../tools/run-proof.sh arm p521_jscalarmul "$(HOLLIGHT)" $@
+p521/p521_jscalarmul_alt.correct: proofs/bignum_mod_n521_9.ml p521/bignum_mod_n521_9.o proofs/bignum_mod_p521_9.ml p521/bignum_mod_p521_9.o proofs/p521_jadd_alt.ml p521/p521_jadd_alt.o proofs/p521_jdouble_alt.ml p521/p521_jdouble_alt.o proofs/p521_jscalarmul_alt.ml p521/p521_jscalarmul_alt.o ; ../tools/run-proof.sh arm p521_jscalarmul_alt "$(HOLLIGHT)" $@
 
 # All other other instances are standalone
 

arm/p521/Makefile

@@ -53,7 +53,9 @@ OBJ = bignum_add_p521.o \
       p521_jdouble.o \
       p521_jdouble_alt.o \
       p521_jmixadd.o \
-      p521_jmixadd_alt.o
+      p521_jmixadd_alt.o \
+      p521_jscalarmul.o \
+      p521_jscalarmul_alt.o
 
 %.o : %.S ; $(CC) -E -I../../include $< | $(GAS) -o $@ -