Switch to the *_neon functions

[aqjune-aws]

This patch makes the *_neon functions replace their original scalar implementations. This (partially) resolves the divergence between the set of functions supported in Arm and in x86. There are still a few functions that are diverged - bignum_emontredc_8n_cdiff and bignum_copy_row_from_table_* which only exists in Arm - but all other functions are converged into one.

The original scalar functions are moved to the unopt/ directories. Their proofs are merged into the *_neon.ml proofs, which are again renamed to the original *.ml.
All _NEON and _neon suffixes are removed.

Also, this patch applies the NIST P-256 optimized field operations to p256_scalarmulbase which was missing in the past.

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.

[aqjune-aws]

To check that functions are correctly renamed, I ran benchmark with the following script:

suffix=_neon # Enable this line before applying this patch
suffix=  # ... after applying this patch

./benchmark bignum_sqr_8_16${suffix}
./benchmark bignum_mul_8_16${suffix}
./benchmark bignum_ksqr_16_32${suffix}
./benchmark bignum_ksqr_32_64${suffix}
./benchmark bignum_kmul_16_32${suffix}
./benchmark bignum_kmul_32_64${suffix}

./benchmark bignum_emontredc_8n${suffix}

for bits in 256 384 521; do
./benchmark bignum_montmul_p${bits}${suffix}
./benchmark bignum_montsqr_p${bits}${suffix}
done

for rowsz in 8n 16 32; do
./benchmark bignum_copy_row_from_table_${rowsz}${suffix}
done

./benchmark p256_scalarmulbase # Interestingly this performance result did not change much :/