CBMC: State (not prove) `poly_invntt_tomont` + Prove `polyvec_ntt` and `polyvec_invntt_tomont`

pq-code-package / mlkem-native

High-assurance, high-performance ML-KEM implementation for mobile, pc, and server targets

Apache License 2.0

11 stars 9 forks source link

Closed mkannwischer closed 1 week ago

mkannwischer commented 1 week ago

This PR:

Proves polyvec_ntt based on the proof of poly_ntt (not that the previous spec missed the pre-condition on the input bounds)
States the contract of poly_invntt_tomont (but does not proof it)
Proves polyvec_invntt_tomont based on the contract of poly_invntt_tomont

Resolves #330 Resolves #378

Based on #371