Update SHA proof for "moving AArch64/X86_64 dispatching to C" changes

[pennyannn]

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

AWS-LC PR: aws/aws-lc#1625
Ticket: V1417594860

The AWS-LC PR refactors existing SHA2 code to move AArch86/x86_64 dispatching code from within the assembly to within the C. In doing so, assembly function names are changed in the following way:

1. For x86_64, the sha512_block_data_order routine is now called sha512_block_data_order_avx
2. For AArch64, the sha512_block_data_order routine is now called sha512_block_data_order_nohw (for Graviton2) and sha512_block_armv8 routine is now called sha512_block_data_order_hw (for Graviton3)

While working on the fix, I solved a problem in the proof of EVP_DigestFinal. Previously, the proof fails for SHA512 because the LLVM optimization introduces pointer comparisons, which is an undefined behaviour in SAW (see GaloisInc/saw-script#1308). SAW produces the error:
"Comparison of pointers from different allocations"

In this fix, we use SAW feature enable_lax_pointer_ordering to allow pointer comparison introduced by LLVM optimization. In addition, this proof requires defining an override for CRYPTO_bswap8 for the version that uses __builtin_bswap64:

static inline uint64_t CRYPTO_bswap8(uint64_t x) {
  return __builtin_bswap64(x);
}

[robdockins]

Seems reasonable to me, modulo a couple of minor questions.