Introduce common coeff_signed_to_unsigned function in poly.c #53
Conversation
mlkem/poly.c
Outdated
| int32_t factor = (r < 0); // 1 if r < 0; 0 if r >= 0 | ||
| r = r + (factor * KYBER_Q); |
There was a problem hiding this comment.
I think it's not unlikely that a compiler would introduce a branch here. One way to thwart this is by calculating r and r + KYBER_q and having a safe_cond_select() stub which, based on either (a) a mask that's 0 or -1, or (b) an int that's 0 or 1, picks one of the two arguments. This function would itself be a C stub that's ideally replaced by ASM.
There was a problem hiding this comment.
Agreed - we need a translation unit of safe constant-time functions like cond_select() and others. Disagree about the third parameter - it's a Boolean not a bleedin' Integer!
There was a problem hiding this comment.
The multiplication factor*KYBER_Q you want will disappear when compiler optimize it.
https://godbolt.org/z/xaY39sdWr
So the compiler see our intentions and convert to:
r += (c >> 15) & KYBER_Q or r += (c >> 31) & KYBER_Q.
On other platform like AVR it's a branch condition.
I think the new style and the old style are equivalent in the eye of compiler.
There was a problem hiding this comment.
The semantics of the >> operator on a signed, negative integer is implementation-defined (see WG14 N2310 6.5.7(5) for example), so I prefer not to use it. Strictly speaking, the use of >> here defies verification with CBMC.
|
@rod-chapman You need DCO's for the CI to be happy. Running the other checks now. |
|
What's a DCO? |
|
Hi @rod-chapman , Thanks for the PR. the DCO is agreement to contribute, so it needs your signature. |
rod-chapman
force-pushed
the
poly_compress_contracts
branch
from
c22d9c1 to
4c53ce5
Compare
|
OK... I have rebase my commits with --sign-off and pushed. Does that look better? |
|
@rod-chapman Yes, all good. |
|
@rod-chapman Can you rebase your PR on |
rod-chapman
force-pushed
the
poly_compress_contracts
branch
from
4c53ce5 to
328f920
Compare
|
@rod-chapman Linting fails (check the formatting of |
|
@rod-chapman CBMC seems to be failing, can you have a look? Also, can you rebase on |
rod-chapman
force-pushed
the
poly_compress_contracts
branch
2 times, most recently
from
3e23577 to
06ce2a8
Compare
|
@rod-chapman , can you do the honor, test the "update with rebase" button after #71 landed ? |
|
Seemed to work OK! |
Signed-off-by: Hanno Becker <[email protected]>
|
It looks like this PR needs manual rebase after https://github.com/pq-code-package/mlkem-c-aarch64/pull/67 was merged separately. |
hanno-becker
force-pushed
the
poly_compress_contracts
branch
from
4aa85e0 to
e939eaf
Compare
|
I think this branch and PR are dead and subsumed by #67. Work on other functions can begin afresh. |
- scalar_compress_q_16 - scalar_compress_q_32 - poly_compress Signed-off-by: Rod Chapman <[email protected]> Signed-off-by: Hanno Becker <[email protected]>
hanno-becker
force-pushed
the
poly_compress_contracts
branch
from
e939eaf to
fdecdb2
Compare
|
This PR did also introduce a loop-invariant based proof of @rod-chapman Where would I find human-readable descriptions of the failure here? Can you reproduce the issue locally? |
Signed-off-by: Rod Chapman <[email protected]>
…rmal parameter r. Uses array indexing instead. Signed-off-by: Rod Chapman <[email protected]>
Signed-off-by: Rod Chapman <[email protected]>
2. Remove commented-out line in body of poly_compress() Signed-off-by: Rod Chapman <[email protected]>
Signed-off-by: Rod Chapman <[email protected]>
1. Introduce common num_blocks constant to avoid repetition of "KYBER_N / 8" 2. Add explanatory comment on switch from pointer arithmetic to array indexing in assignment to r[] 3. Introduce loop invariants for the KYBER_K=4 branch of the code. Signed-off-by: Rod Chapman <[email protected]>
…ed in a later PR Signed-off-by: Rod Chapman <[email protected]>
This PR introduces a common "coeff_signed_to_unsigned()" function in poly.c, its contracts and verification thereof using CBMC. This function reduces repetition of the same idiom in poly.c and simplifies the calling code in poly_compress() and other functions.
Additionally, this PR adds contract-based proof of scalar_compress_q_16 and scalar_compress_q_32