Pre-conditions can often be transformed into premises of the post-condition. While largely equivalent, this can lead to slightly stronger theorems: For example, if an NTT zeta table is fixed in the pre-condition, we have no guarantee of memory-safety if corrupted constants are passed. If instead, the values of the zeta pointer are constrained only in the post-condition, then the safety spec entails that even with a corrupted constant table, safety (albeit not correctness, of course) is retained.
Task:
- Audit the mlkem-native and mldsa-native for the use of this specification pattern
- Agree on a set of preconditions for which there is added value in expressing them as premises of the post-condition
- Adjust all specifications and proofs as needed
Pre-conditions can often be transformed into premises of the post-condition. While largely equivalent, this can lead to slightly stronger theorems: For example, if an NTT zeta table is fixed in the pre-condition, we have no guarantee of memory-safety if corrupted constants are passed. If instead, the values of the zeta pointer are constrained only in the post-condition, then the safety spec entails that even with a corrupted constant table, safety (albeit not correctness, of course) is retained.
Task: