In ML-KEM, we need 3 types of compressions and their resp. decompression: Compress_du, Compress_dv, and Compress_1.
Currently Compress_dv is implemented in poly_compress, Compress_du is implemented in polyvec_compress (as it's only
needed for vectors), and Compress_1 is implemented in poly_tomsg.
This is somewhat confusing.
This PR splits up polyvec_compress and polyvec_decompress and hoists out new functions called poly_compress_du and poly_decompress_du.
It also cleans up the naming and CBMC proofs.
It works in the following steps:
[X] Split up polyvec_compress + polyvec_decompress into poly_compress_du, poly_decompress_du
[X] CBMC: State function contract of poly_compress_du, poly_decompress_du
[X] CBMC: Proof polyvec_compress + polyvec_decompress using contract of poly_compress_du+ poly_decompress_dv
[X] Rename poly_{,de}compress to poly_{,de}compress_dv (and adjust CBMC proofs)
[X] Rename polyvec_{,de}compress to polyvec_{,de}compress_du
In preparation of #410.
In ML-KEM, we need 3 types of compressions and their resp. decompression: Compress_du, Compress_dv, and Compress_1.
Currently Compress_dv is implemented in poly_compress, Compress_du is implemented in polyvec_compress (as it's only needed for vectors), and Compress_1 is implemented in poly_tomsg. This is somewhat confusing.
This PR splits up polyvec_compress and polyvec_decompress and hoists out new functions called poly_compress_du and poly_decompress_du.
It also cleans up the naming and CBMC proofs.
It works in the following steps:
poly_compress_du,poly_decompress_dupoly_compress_du,poly_decompress_dupolyvec_compress+polyvec_decompressusing contract ofpoly_compress_du+poly_decompress_dvpoly_{,de}compresstopoly_{,de}compress_dv(and adjust CBMC proofs)polyvec_{,de}compresstopolyvec_{,de}compress_dupoly_compress_du,poly_decompress_du