Verify high-level AES-CTR32 functions for NI and BitSlice

cryspen / hacl-packages

The Cryspen HACL Distribution

https://cryspen.com/hacl-packages

Other

13 stars 18 forks source link

Verify high-level AES-CTR32 functions for NI and BitSlice #451

Closed mamonet closed 3 months ago

mamonet commented 5 months ago

Provide proofs for the functions that are implemented the following modules Hacl.AES_128.CTR32.NI Hacl.AES_128.CTR32.BitSlice Hacl.AES_256.CTR32.NI Hacl.AES_256.CTR32.BitSlice

mamonet commented 3 months ago

Completed! https://github.com/hacl-star/hacl-star/pull/919