Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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.
- Loading branch information