Reproducing ML-KEM-768 Modulus tests

[rod-chapman]

I am having trouble reproducing your "modulus" KATs for ML-KEM-768.

Each line of your input file contains 1184 bytes, which is 384*K+32, as specified in the "Type Check" condition (line 982) of the spec.

BUT... the ByteDecode12 function only works for exact multiples of 384 bytes.

In our official comments to NIST, we wrote:

"Line 984. Similarly, the application of ByteDecode12(EK_Tilde) cannot be correct, since EK_Tilde is 1184 bytes when K = 3, which is not an integer multiple of 384. Perhaps ByteDecode12(EK_Tilde[0:384k]) is intended (as in line 2 of Algorithm 13) so that the final 32 bytes are eliminated?"

Do you draw the same interpretation?

Should I eliminate the final 32 bytes before performing the Modulus Check? Thanks, Rod, AWS

[FiloSottile]

Hello! Those are ML-KEM.Encaps inputs, which are defined as strings of 384k+32 bytes. The extra 32 bytes are the Rho value, which is irrelevant to this specific test, but I believe it’s best to provide test inputs to high level functions when possible.

[rod-chapman]

Similarly, the equality test on line 985 "ek /= ek_tilde" does not make sense if ek is 1184 bytes but ByteEncode12 returns 1152 bytes. Perhaps it should be "ek /= ek_tilde[0:384k]"?

[rod-chapman]

So... I should discard the final 32 bytes of each input, before passing 3*384 bytes to ByteDecode12?

[rod-chapman]

Interesting... of your 780 test cases, I get 772 that report the EK is invalid, and 8 that report that the EK is OK. I assume this is not the expected result?

[FiloSottile]

So... I should discard the final 32 bytes of each input, before passing 3*384 bytes to ByteDecode12?

The intention is that you would pass the whole 384*K+32 bytes to your Encaps implementation, as if they were a public key received from the network.

You are correct that the description of the "Modulus check" at lines 984/985 is incorrect as it should be cutting off the last 32 bytes for the purposes of that check.

[rod-chapman]

Yes... that's what I do... my EK_Is_Valid_For_Encaps() function takes the whole 1184 bytes as its formal parameter, then eliminates the final 32 bytes before calling ByteDecode12.

[FiloSottile]

Interesting... of your 780 test cases, I get 772 that report the EK is invalid, and 8 that report that the EK is OK. I assume this is not the expected result?

Ooooh interesting! They are all supposed to fail, and they do in my code assuming I don't have any bugs in the test.

Which ones pass?

[rod-chapman]

Of the 780 lines in the input file, lines 1, 2, 5, 6, 9, 10, 13 and 780 report that EK is valid. Hmmm...

[FiloSottile]

Yes... that's what I do... my EK_Is_Valid_For_Encaps() function takes the whole 1184 bytes as its formal parameter, then eliminates the final 32 bytes before calling ByteDecode12.

Yeah, to my understanding that is a valid implementation of the Modulus check. (I opted for a different approach, my ByteDecode12 always rejects values >= q, sort of like suggested at line 997.)

[FiloSottile]

Of the 780 lines in the input file, lines 1, 2, 5, 6, 9, 10, 13 and 780 report that EK is valid. Hmmm...

If those are 1-indexed lines, those are the vectors with one of the coefficients == q.

[rod-chapman]

Interesting... looks like I screwed up my constant-time implementation of ModQ...

[rod-chapman]

OK... fixed it... I had a brain-fail at the edge-case of ModQ(3329). Now to see if the proof tools can actually verify it as well...

[rod-chapman]

Done... I have proof of type safety and partial correctness for both ModQ and "*" now, and all your tests pass OK. Thanks for your help.

[FiloSottile]

Awesome! Glad the tests were useful ✨