libcrux icon indicating copy to clipboard operation
libcrux copied to clipboard

Published 20 hours ago • verified publisher icon cryspen

A more complete spec of ML-KEM

Open karthikbhargavan opened this issue 1 year ago • 2 comments

This PR fills out some of the functions of the ML-KEM spec that had not been previously specified and does a general clean up of the spec in prep for the proofs.

karthikbhargavan avatar Aug 11 '24 22:08 karthikbhargavan

This is blocked on ind_cca decap breaking CI. We need to debug this.

karthikbhargavan avatar Aug 14 '24 11:08 karthikbhargavan

This now relies on https://github.com/hacspec/hax/pull/854

karthikbhargavan avatar Aug 16 '24 23:08 karthikbhargavan

Fixed decap using https://github.com/hacspec/hax/pull/854

karthikbhargavan avatar Aug 17 '24 14:08 karthikbhargavan

Should we merge this, now https://github.com/hacspec/hax/pull/856 is in (aka unsize are gone)?

W95Psp avatar Aug 20 '24 06:08 W95Psp