Add bignum_mont{sqr,mul}_p256_neon for Arm

This patch adds `bignum_mont{sqr,mul}_p256_neon` functions.

These are vectorized and instruction-rescheduled versions of `bignum_mont{sqr,mul}_p256`.
They are verified using the equivalence checking tactics.

A new bash script `tools/external/slothy.sh` is added to help reproduce the optimized output.
The 'intermediate' functions of the two functions are written as comments in the two assembly files.

Additionally,
- A new instruction `umull2` is formalized add added to the simulator in order to verify the new functions.
- Old `*_neon` functions' proofs are refactored a bit.

arm/Makefile

@@ -244,8 +244,10 @@ BIGNUM_OBJ = curve25519/bignum_add_p25519.o \
  p256/bignum_mod_p256_4.o \
  p256/bignum_montmul_p256.o \
  p256/bignum_montmul_p256_alt.o \
+ p256/bignum_montmul_p256_neon.o \
  p256/bignum_montsqr_p256.o \
  p256/bignum_montsqr_p256_alt.o \
+ p256/bignum_montsqr_p256_neon.o \
  p256/bignum_mux_4.o \
  p256/bignum_neg_p256.o \
  p256/bignum_nonzero_4.o \

arm/allowed_asm

@@ -24,6 +24,7 @@
 : lsr$
 : madd$
 : mov$
+: movi$
 : movk$
 : mul$
 : mvn$
@@ -33,14 +34,23 @@
 : ngcs$
 : orr$
 : ret$
+: rev64$
 : sbc$
 : sbcs$
+: shl$
 : stp$
 : str$
 : strb$
 : sub$
 : subs$
 : tst$
+: uaddlp$
+: umlal$
 : umulh$
 : umull$
+: umull2$
+: usra$
+: uzp1$
+: uzp2$
+: xtn$
 : $

arm/p256/Makefile

@@ -35,8 +35,10 @@ OBJ = bignum_add_p256.o \
  bignum_mod_p256_4.o \
  bignum_montmul_p256.o \
  bignum_montmul_p256_alt.o \
+ bignum_montmul_p256_neon.o \
  bignum_montsqr_p256.o \
  bignum_montsqr_p256_alt.o \
+ bignum_montsqr_p256_neon.o \
  bignum_mux_4.o \
  bignum_neg_p256.o \
  bignum_nonzero_4.o \