libcrux icon indicating copy to clipboard operation
libcrux copied to clipboard

Published 20 hours ago • verified publisher icon cryspen

Make ML-KEM serialize.rs panic-free

Open mamonet opened this issue 1 year ago • 3 comments

This patch adds pre-conditions and workaround assumptions to serialize.rs to make Libcrux_ml_kem.Serialize.fst verifiable. It also adds Libcrux_ml_kem.Serialize.fst to PANIC_FREE category in ML-KEM Makefile.

mamonet avatar Jul 18 '24 17:07 mamonet

I turn this PR to draft until we get rid of all the assumes. The next PRs will focus on Vector modules as it seems to be less affected by issues that require inline assumptions.

mamonet avatar Jul 19 '24 16:07 mamonet

@mamonet What's the state here? This looks stale. Do you want to close it?

franziskuskiefer avatar Aug 06 '24 07:08 franziskuskiefer

The changes are still relative. However, this PR depends on https://github.com/hacspec/hax/issues/605 to remove assumes.

mamonet avatar Aug 06 '24 08:08 mamonet

I will close this PR because it's now part of https://github.com/cryspen/libcrux/pull/488

mamonet avatar Aug 25 '24 13:08 mamonet