Remove NTT_BOUND_NATIVE and INVNTT_BOUND_NATIVE #645
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
hanno-becker
force-pushed
the
bound_native
branch
3 times, most recently
from
dcec93e to
3ead8ca
Compare
The numeric macros NTT_BOUND_NATIVE and INVNTT_BOUND_NATIVE could be used by backends to specify an output bound for the forward and inverse NTT. We would then use STATIC_ASSERT's to check that those backend-specific bounds would imply the bounds (NTT_BOUND and INVNTT_BOUND) that the CBMC proofs work against. The added value of NTT_BOUND_NATIVE and INVNTT_BOUND_NATIVE is questionable. In the end, what we care about is that the native NTT and invNTT adhere to the bounds that CBMC relies on. Any strengthening of the bounds may be good to know, but is otherwise an unnecessary complication of the code. This commit removes NTT_BOUND_NATIVE and INVNTT_BOUND_NATIVE and uses the contractual bounds NTT_BOUND and INVNT_BOUND in their place. Similarly, INVNTT_BOUND_REF is removed, which is finer bound for the reference invNTT. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
We conduct some basic static sanity checks on the values of NTT_BOUND and INVNTT_BOUND. Previously, those checks were done using a `STATIC_ASSERT` macro. The `STATIC_ASSERT` macro was otherwise not used. This commit rewrites said bounds checks using plain `#if ...`. It therefore eliminates the need for `STATIC_ASSERT`, which is removed. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
hanno-becker
force-pushed
the
bound_native
branch
from
3ead8ca to
1f08487
Compare
Those assertions are already checked by CBMC. Repeating them does not add value but impedes readability. Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>
mkannwischer
approved these changes
Jan 13, 2025
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The numeric macros NTT_BOUND_NATIVE and INVNTT_BOUND_NATIVE could be used by backends to specify an output bound for the forward and inverse NTT. We would then use STATIC_ASSERT's to check that those backend-specific bounds would imply the bounds (NTT_BOUND and INVNTT_BOUND) that the CBMC proofs work against.
The added value of NTT_BOUND_NATIVE and INVNTT_BOUND_NATIVE is questionable. In the end, what we care about is that the native NTT and invNTT adhere to the bounds that CBMC relies on. Any strengthening of the bounds may be good to know, but is otherwise an unnecessary complication of the code.
This commit removes NTT_BOUND_NATIVE and INVNTT_BOUND_NATIVE and uses the contractual bounds NTT_BOUND and INVNT_BOUND in their place.
Also, remove the need for
STATIC_ASSERTby rewriting its use using a plain#if.