Add spec and proof for rej_eta #86
Conversation
manastasova
force-pushed
the
mldsa_rej_eta
branch
from
7835504 to
5e81e49
Compare
There was a problem hiding this comment.
I believe that the computation of t0,t1 itself is unsigned; it's only when you convert to signed prior to 2 - t_i and 4 - t_i that you need an explicit cast, as otherwise that subtraction is computed in unsigned. Marking t0,t1 as signed would not check for underflows in t0 = t0 - (205 * t0 >> 10) * 5; and t1 = t1 - (205 * t1 >> 10) * 5;, which we want CBMC to do.
|
@manastasova, should we add you as contributor to mldsa-native? |
|
Yes... Please add Mila as a contributor here, and please add her to the Discord channel. Thanks. |
That would be great! Thanks @mkannwischer! |
I open this PR to add you as a contributor: pq-code-package/tsc#152 The PQCA Discord is open for everyone to join: https://pqca.org/get-involved/ |
It was observed in pq-code-package/mldsa-native#86 that invariant(ctr > 0 ==> array_bound(r, 0, ctr, 0, MLKEM_Q))) can be simplified to invariant(array_bound(r, 0, ctr, 0, MLKEM_Q))) as invariant(array_bound(r, 0, 0, 0, MLKEM_Q))) is just true. This commit simplifies the one place in mlkem-native where we had a similar implicatation. Signed-off-by: Matthias J. Kannwischer <[email protected]>
Signed-off-by: manastasova <[email protected]>
Notes:: - rej_eta is static, thus, CHECK_FUNCTION_CONTRACTS is defined as rej_eta instead of $(MLD_NAMESPACE)rej_eta in the Makefile. - rej_eta is static, thus, additional assumptions, such as requires(len <= MLDSA_N && buflen <= (POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES)) are made. This accelerates the performance of CBMC proofs. Signed-off-by: manastasova <[email protected]>
mkannwischer
force-pushed
the
mldsa_rej_eta
branch
from
519ab9a to
01362e3
Compare
There was a problem hiding this comment.
Thanks @manastasova. LGTM!
I took the liberty to rebase this on top of main.
Change types `uint32_t t0, t1;` to` int32_t t0, t1;` due to potential
overflow in `if (t0 < 9){a[ctr++] = 4 - t0;}` causing cbmc proofs to
fail.
### Issues:
From pq-code-package/mldsa-native#86.
### Description of changes:
The output array is of type `int32_t* a`, thus, `uint32_t` aux values
`t0, t1` cause cbmc proofs to fail due to potential overflow.
### Testing:
`./crypto/crypto_test `
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 license and the ISC license.
4 participants
This PR adds the spec and proof for rej_eta function.
Notes::
rej_etais static, thus,CHECK_FUNCTION_CONTRACTSis defined asrej_etainstead of $(MLD_NAMESPACE)rej_etain theMakefile.rej_etais static, thus, additional assumptions, such asrequires(len <= MLDSA_N && buflen <= (POLY_UNIFORM_ETA_NBLOCKS * STREAM256_BLOCKBYTES))are made. This accelerates the performance of CBMC proofs.Another Note::
uint32_t t0, t1;toint32_t t0, t1;due to potential overflow inif (t0 < 9){a[ctr++] = 4 - t0;}causing cbmc fail.Solves #26.