Finalize proof of kem_enc_v()

rod-chapman · rod-chapman · commit d488734b5ea2 · 2026-06-17T15:23:51.000+01:00
Signed-off-by: Rod Chapman &lt;rodchap@amazon.com&gt;
diff --git a/mlkem/src/kem.c b/mlkem/src/kem.c
@@ -405,6 +405,7 @@ __contract__(
   requires(memory_no_alias(in, MLKEM_EPP_BYTES))
   requires(memory_no_alias(p, sizeof(mlk_poly)))
   assigns(memory_slice(p, sizeof(mlk_poly)))
+  ensures(array_abs_bound(p->coeffs, 0, MLKEM_N, 16))
 )
 {
   unsigned j;
diff --git a/proofs/cbmc/kem_enc_derand_u/Makefile b/proofs/cbmc/kem_enc_derand_u/Makefile
@@ -23,6 +23,8 @@ CHECK_FUNCTION_CONTRACTS=mlk_enc_derand_u
 USE_FUNCTION_CONTRACTS = mlk_indcpa_enc_u
 USE_FUNCTION_CONTRACTS += mlk_sha3_512
 USE_FUNCTION_CONTRACTS += mlk_polyvec_reduce
+USE_FUNCTION_CONTRACTS += mlk_serialize_epp
+USE_FUNCTION_CONTRACTS += mlk_serialize_polyvec_16le
 USE_FUNCTION_CONTRACTS += mlk_zeroize
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
diff --git a/proofs/cbmc/kem_enc_v/Makefile b/proofs/cbmc/kem_enc_v/Makefile
@@ -24,6 +24,9 @@ USE_FUNCTION_CONTRACTS = mlk_indcpa_enc_v
 USE_FUNCTION_CONTRACTS += mlk_polyvec_frombytes
 USE_FUNCTION_CONTRACTS += mlk_polyvec_reduce
 USE_FUNCTION_CONTRACTS += mlk_polyvec_tobytes
+USE_FUNCTION_CONTRACTS += mlk_deserialize_epp
+USE_FUNCTION_CONTRACTS += mlk_deserialize_polyvec_16le
+USE_FUNCTION_CONTRACTS += mlk_polyvec_mulcache_compute
 USE_FUNCTION_CONTRACTS += mlk_ct_memcmp
 USE_FUNCTION_CONTRACTS += mlk_zeroize
 APPLY_LOOP_CONTRACTS=on

Original file line number	Diff line number	Diff line change
`@@ -405,6 +405,7 @@ __contract__(`
`405`	`405`	`requires(memory_no_alias(in, MLKEM_EPP_BYTES))`
`406`	`406`	`requires(memory_no_alias(p, sizeof(mlk_poly)))`
`407`	`407`	`assigns(memory_slice(p, sizeof(mlk_poly)))`
	`408`	`+ ensures(array_abs_bound(p->coeffs, 0, MLKEM_N, 16))`
`408`	`409`	`)`
`409`	`410`	`{`
`410`	`411`	`unsigned j;`