ML-KEM: Improve compression and byte conversion functions #161
Conversation
Replaces tick marks with explicit denotations of what dimension the input and output are.
Changes implementation details of BytesToBits and BitsToBytes
| | ell == 0 => [] | ||
| | ell > 0 => join [[ b8ij where | ||
| // Step 4. Taking the last bit is the same as modding by 2. | ||
| b8ij = Ci' ! 0 |
There was a problem hiding this comment.
note: I intend to refer this to the mod2IsFinalBit property I added in #160.
There was a problem hiding this comment.
Caught this on this PR, but the ML-KEM proofs currently require z3 v4.13+. This is what is installed by default with brew install cryptol but it is not what we ship with what4 solvers as that is v4.8.14. Adding a ticket to ensure we do :check-docstring against multiple z3 versions. We should also consider adding support to be able to set z3 version.
Going to cut some tickets for CI related tasks from this and also try and figure out which properties are actually causing the problem. |
Looking at the spec I agree that this is not super clear on endianness here. I am happy with how this looks right now. |
There was a problem hiding this comment.
LGTM, opened up a separate issue #166 for the issue uncovered during review of this.
Closes #144 (assuming that #160 has already been merged).
This has two parts:
For the second part, I am honestly kind of confused. I thought the endianness was wrong but I tried rewriting it multiple times to make it look more like the spec and it seems correct. The KATs pass and all the internal properties pass. If anyone discerns something weird I'm doing with bit ordering I would love feedback.