search

leanprover / LNSym

Armv8 Native Code Symbolic Simulator in Lean
Apache License 2.0
62 stars 18 forks source link

Work towards the GCM GMult functional correctness proof #225

Closed shigoel closed 4 weeks ago

shigoel commented 1 month ago

Description:

Some work towards proving the functional correctness of GCM Gmult.

Summary of changes:

  1. Removed h : esize > 0 from the ShiftInfo structure.
  2. Added a dsimproc for AdvSIMDExpandImm. Cleaned up other dsimprocs.
  3. Defined GCMGmultV8_alt, an alternative GCM GMult definition that does not traffic in lists.
  4. Massaged the functional correctness goal a bit.

Testing:

What tests have been run? Did make all succeed for your changes? Was conformance testing successful on an Aarch64 machine?

Yes

License:

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