Add unbounded AES-GCM verification.

[andreistefanescu]

Caveats

• llvm_verify_fixpoint_x86 proves partial correctness, that is, the property is verified just for terminating executions of the target x86_64 function
• induction proofs for cryptol functions are in fact proofs just for the inputs on which the function evaluation terminates, for example, \x -> f x == g x means that f x is equal with g x when f x terminates; moreover, the induction principle is applied manually, by using prove_theorem assume_unsat to create a rewrite rule that is then used in it's own proof, after the function f is unfolded.
• saw branch (with submodules): https://github.com/GaloisInc/saw-script/tree/sygus2

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

[andreistefanescu]

I managed to run the entire proof as is, it takes 22 minutes on my M2 Max, memory usage peaked at 97% :-).

[pennyannn]

I tried to reproduce this proof but failed. Specifically, the proofs for assembly aesni_gcm_encrypt and aesni_gcm_decrypt failed. The attached(out.log) is the failure message. The environment is the following:

• AWS-LC-verification commit: https://github.com/pennyannn/aws-lc-verification/tree/yppe/139
• AWS-LC commit: https://github.com/aws/aws-lc/tree/7226be17c2268f5c44cd110dc7e0580903ab9763
• Docker image base: Ubuntu20.04
• Clang version: 10.0.0
• SAW version: https://github.com/pennyannn/saw-script/tree/yppe/sygus2
• Z3 version: 4.8.8
• Yices version: 2.6.2

For compiling SAW:

• Docker image base: Ubuntu20.04
• GHC version: 9.4.8
• Cabal version: 3.10.2.1