Proof of poly_challenge() including contracts #199
Conversation
and proof suppport files. Signed-off-by: Rod Chapman <[email protected]>
|
|
||
| c->coeffs[i] = c->coeffs[j]; | ||
|
|
||
| /* The least-significant bit of signs tells is if we want -1 or +1 */ |
There was a problem hiding this comment.
| /* The least-significant bit of signs tells is if we want -1 or +1 */ | |
| /* The least-significant bit of signs tells us if we want -1 or +1 */ |
| { | ||
| if (pos >= SHAKE256_RATE) | ||
| { | ||
| shake256_squeezeblocks(buf, 1, &state); | ||
| pos = 0; | ||
| } | ||
| j = buf[pos++]; | ||
| } | ||
| while (j > i) /* clang-format mangles layout owing to the contract above */ |
There was a problem hiding this comment.
| while (j > i) /* clang-format mangles layout owing to the contract above */ | |
| while (j > i); /* clang-format mangles layout owing to the contract above */ |
| j = buf[pos++]; | ||
| } | ||
| while (j > i) /* clang-format mangles layout owing to the contract above */ | ||
| ; |
There was a problem hiding this comment.
You can stop clang-format from mangling your code here if you change .clang-format
from
- __loop__(x)={}
to
- __loop__(x)={} do
A little hacky, but it does not seem to have any bad side-effects in mldsa-native and mlkem-native.
While you touching .clang-format already maybe fix the typo in artific(i)ally
| assigns(j, object_whole(buf), state, pos) | ||
| invariant(pos >= 1) | ||
| invariant(pos <= SHAKE256_RATE) | ||
| invariant(array_bound(c->coeffs, 0, MLDSA_N, -1, 2)) |
There was a problem hiding this comment.
Can we remove this invariant since this loop does not change the value of c?
| @@ -5,6 +5,7 @@ | |||
| #ifndef MLD_POLY_H | |||
| #define MLD_POLY_H | |||
|
|
|||
| #include <stdbool.h> | |||
There was a problem hiding this comment.
Do we need booleans here?
|
|
||
| c->coeffs[i] = c->coeffs[j]; | ||
|
|
||
| /* The least-significant bit of signs tells is if we want -1 or +1 */ |
| offset = 2 * (signs & 1); | ||
|
|
||
| b = buf[pos++]; | ||
| } while (b > i); | ||
| /* offset has value 0 or 2 here, so (1 - (int32_t) offset) has | ||
| * value -1 or +1 */ | ||
| c->coeffs[j] = 1 - (int32_t)offset; | ||
|
|
||
| c->coeffs[i] = c->coeffs[b]; | ||
| c->coeffs[b] = 1 - 2 * (signs & 1); | ||
| /* Move to the next bit of signs for next time */ |
There was a problem hiding this comment.
Curious about the deviation from the reference code here
There was a problem hiding this comment.
Agree. We should strive to deviate only if we need to, and if so, leave a comment in the commit message and a /* Reference: ... */ comment.
There was a problem hiding this comment.
The original code mixed unsigned and signed arithmetic and relied on implicit conversions. As a result, CBMC was not able to reason about the range of the resulting expression, leading to a proof failure. As (re-written), it proves fine, it's probably clearer to a human reader what's going on.
Fixes #113
Adds contracts and proof support files for poly_challenge()