Consistently use mld_assert instead of cassert #365
Conversation
|
What happens when an mld_assert() contains a forall quantifier or something else that isn't executable? |
|
@rod-chapman We have so far managed to avoid that. |
You can make use of |
mkannwischer
force-pushed
the
mld_assert
branch
2 times, most recently
from
1649e77 to
b4ac310
Compare
mldsa/polyvec.c
Outdated
| cassert(j == MLDSA_L); | ||
| cassert(t >= -(int64_t)MLDSA_L * (MLDSA_Q - 1) * (MLD_NTT_BOUND - 1)); | ||
| cassert(t <= (int64_t)MLDSA_L * (MLDSA_Q - 1) * (MLD_NTT_BOUND - 1)); | ||
| mld_assert(j == MLDSA_L); |
There was a problem hiding this comment.
@mkannwischer Can we use this opportunity to check if we actually need those asserts?
There was a problem hiding this comment.
While assertions like these might not be strictly needed for Z3 to prove everything, they sometimes serve as documentation for a new human reader. Imagine someone from (say) TrailOfBits looking at this code for the first time ... such assertions are a chance for the developer to say "Dear reader, here's something important that has to True at this point in the program that might not be obvious..."
Please consider the human reader in evaluating the merits of these cases.
There was a problem hiding this comment.
I agree in principle, but here were merely restate the loop invariant which is just a few lines above.
There was a problem hiding this comment.
Removing all casserts to check if the CI is still happy.
| @@ -17,20 +18,20 @@ void mld_decompose(int32_t *a0, int32_t *a1, int32_t a) | |||
| { | |||
| *a1 = (a + 127) >> 7; | |||
| /* We know a >= 0 and a < MLDSA_Q, so... */ | |||
| cassert(*a1 >= 0 && *a1 <= 65472); | |||
|
Note that updates in main have introduced additional casserts. Those should be changed to mld_assert (or removed as well). |
hanno-becker
force-pushed
the
mld_assert
branch
3 times, most recently
from
5a3689b to
5c43700
Compare
cassert turns into a CBMC proof assertion inside of CBMC proofs, but it turns into a no-op otherwise. mld_assert behaves the save inside of CBMC proofs, but also turns into a run-time assertion in debug builds. Signed-off-by: Matthias J. Kannwischer <[email protected]> Signed-off-by: Hanno Becker <[email protected]>
mld_montgomery_reduce() so far had two CBMC specs with varying input/output bounds. However, it appears that the weak version is not necessary and can be removed. Signed-off-by: Hanno Becker <[email protected]>
cassert turns into a CBMC proof assertion inside of CBMC proofs, but it turns into a no-op otherwise.
mld_assert behaves the save inside of CBMC proofs, but also turns into a run-time assertion in debug builds.