Add bignum_mont{sqr,mul}_p521_neon

This patch adds `bignum_mont{sqr,mul}_p521_neon`.

```
bignum_montsqr_p521             :   114.7 ns each (var  0.2%, corr  0.06) =    8720010 ops/sec
bignum_montsqr_p521_neon        :    83.8 ns each (var  0.4%, corr -0.04) =   11926387 ops/sec
bignum_montmul_p521             :   130.8 ns each (var  0.2%, corr -0.00) =    7644702 ops/sec
bignum_montmul_p521_neon        :   111.4 ns each (var  0.2%, corr  0.04) =    8978421 ops/sec
```

The new subroutine specs are added to specification.txt, and test as well as benchmark are updated.

Modular squaring/multiplication functions are not included in this patch.

This patch also contains the following updates:

- A tactic for showing equivalence of loops is added (the tactic is not used yet).
- Definitions for input state equivalence are canonicalized as `.. /\ (?a. read c1 s = a /\ read c1 s' = a /\ (?b. read c2 s = b /\ read c2 s' = b /\ ( ... )))`
- Minor buggy behaviors in equiv tactics are fixed and performance improvements done

arm/Makefile

@@ -302,8 +302,10 @@ BIGNUM_OBJ = curve25519/bignum_add_p25519.o \
              p521/bignum_mod_p521_9.o \
              p521/bignum_montmul_p521.o \
              p521/bignum_montmul_p521_alt.o \
+             p521/bignum_montmul_p521_neon.o \
              p521/bignum_montsqr_p521.o \
              p521/bignum_montsqr_p521_alt.o \
+             p521/bignum_montsqr_p521_neon.o \
              p521/bignum_mul_p521.o \
              p521/bignum_mul_p521_alt.o \
              p521/bignum_neg_p521.o \

arm/p521/Makefile

@@ -32,8 +32,10 @@ OBJ = bignum_add_p521.o \
       bignum_mod_p521_9.o \
       bignum_montmul_p521.o \
       bignum_montmul_p521_alt.o \
+      bignum_montmul_p521_neon.o \
       bignum_montsqr_p521.o \
       bignum_montsqr_p521_alt.o \
+      bignum_montsqr_p521_neon.o \
       bignum_mul_p521.o \
       bignum_mul_p521_alt.o \
       bignum_neg_p521.o \