Verify AES CoreNI module

cryspen / hacl-packages

The Cryspen HACL Distribution

https://cryspen.com/hacl-packages

Other

15 stars 18 forks source link

Verify AES CoreNI module #448

Closed mamonet closed 9 months ago

mamonet commented 9 months ago

Verifying the part of AES code that utilizes AES intrinsics (currently supported for x86 and ARM). Proofs are supposed to meet the corresponding procedures in Spec.AES module.

Progress regarding this issue is made in this branch https://github.com/mamonet/hacl-star/tree/aes_ctr32

mamonet commented 9 months ago

This issue is completed.