Add bignum_mont{sqr,mul}_p521_neon

[aqjune-aws]

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 included (the tactic is not used in this patch however).
• 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

Issue #, if available:

Description of changes:

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[jargh]

This looks great, thanks! I have checked some details and rerun the proofs; my performance measurements on G2 match the ones quoted, and all the other reorganizations and improvements make good sense.