search

pq-code-package / mlkem-native

High-assurance, high-performance ML-KEM implementation for mobile, pc, and server targets
https://pq-code-package.github.io/mlkem-native/dev/bench/
Apache License 2.0
11 stars 9 forks source link

CBMC Proof of indcpa_dec() #384

Closed rod-chapman closed 1 week ago

rod-chapman commented 1 week ago

Adds contracts and proof artefacts for

unpack_ciphertext() (local function within indcpa.c) and indcpa_dec()

All tests OK All proofs OK lint OK

rod-chapman commented 1 week ago

OK...I will squash and amend the commit message