Fix formal verification failure in AWS-LC PR 1101

[pennyannn]

AWS-LC PR: aws/aws-lc#1101
Ticket: V964947909

Changes from AWS-LC PR:

1. EC_RAW_POINT is renamed to EC_JACOBIAN.
2. A new parameter Htable is added to the aesni_gcm_en[de]decrypt functions. The assembly now directly refers to Htable instead of locating Htable with respect to Xip with some offset.

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

[nebeid]

My understanding is that for point 1, EC_JACOBIAN change is accepted by the tests and they continue to pass.
But for point 2, there are changes in the proofs, but the AES-GCM tests were still failing so they were disabled. Is my understanding correct?

[pennyannn]

My understanding is that for point 1, EC_JACOBIAN change is accepted by the tests and they continue to pass. But for point 2, there are changes in the proofs, but the AES-GCM tests were still failing so they were disabled. Is my understanding correct?

Yes. Exactly right. The EC proofs now work with the new name EC_JACOBIAN. The AES-GCM proofs are updated to fit with the changes but they are currently crashing because of the lack of feature in SAW (Though I won't know for sure if the changes are correct until I am able to run the proofs. Maybe I can revert the changes back to what they used to be if you prefer. In principal it shouldn't matter because the proofs are disabled anyways). So I disabled them in the shell scripts.

[Update]
Per @apetcher-amazon's request, I've reverted the changes in the AES-GCM proofs and added a comment on the AWS-LC commit that the old proof works on.