CBMC: Proof of poly_ntt()
#371
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
cbmc_ntt
branch
from
2ecb068 to
d6fcd2a
Compare
hanno-becker
force-pushed
the
cbmc_ntt
branch
3 times, most recently
from
5db404b to
fb46e4e
Compare
hanno-becker
force-pushed
the
cbmc_ntt
branch
from
d0ec687 to
62fd65f
Compare
hanno-becker
force-pushed
the
cbmc_ntt
branch
6 times, most recently
from
2e16096 to
04e453c
Compare
mkannwischer
requested changes
Nov 12, 2024
There was a problem hiding this comment.
Nice! Thanks @hanno-becker - this is as readable as it gets now I think. The splitting makes sense.
Small nits.
hanno-becker
force-pushed
the
cbmc_ntt
branch
from
04e453c to
4bf8a98
Compare
hanno-becker
force-pushed
the
cbmc_ntt
branch
from
4bf8a98 to
898c46d
Compare
mkannwischer
approved these changes
Nov 12, 2024
There was a problem hiding this comment.
LGTM - thanks @hanno-becker for integrating my suggestions.
hanno-becker
force-pushed
the
cbmc_ntt
branch
from
898c46d to
c246ad4
Compare
This commit adds a spec and proof for the MLKEM forward NTT. The main difficulty in proving the forward NTT type-safe is to formalize the bounds reasoning showing that the additions and subtractions in the butterflies do not overflow. Luckily, very basic layer-to-layer bounds reasoning is sufficient to achieve an output bound of 8*q, which is enough for reason about the calling code: When moving from layer N to layer N+1, every coefficient is replaced by the addition or subtractio or a layer N coefficient with the result of a Barrett multiplication with a signed canonical twiddle factor. Since such Barrett multiplication always has absolute value < q (this could be improved significantly if we needed to), the absolute bounds increase by at most q. Spelling out the invariants in CBMC is cumbersome and rather verbose. To facilitate, and to keep runtimes down, this commit splits the NTT original NTT code into three functions, one per NTT loop: - The top-level poly_ntt() iterates over the layers, calling ntt_layer() - ntt_layer computes one NTT layer, calling ntt_butterfly_block() for each block of butterflies. - ntt_butterfly_block() actually does the modular arithmetic. While this makes the loop-and-feel of the NTT rather different from what it was, structurally it is almost the same as in the reference implementation. Previously, the NTT code included a runtime check for the tighter bound 5*q for the output of the NTT. The bound and the check are removed in this commit: While they are still true, it is confusing to runtime check for a different value than what we are proving. Instead, a comment is left. Signed-off-by: Hanno Becker <[email protected]>
hanno-becker
force-pushed
the
cbmc_ntt
branch
from
c246ad4 to
77ac5bc
Compare
mkannwischer
added a commit
that referenced
this pull request
Nov 12, 2024
#371 introduced a new macro ARRAY_ABS_BOUND for bounds that are centered around zero. This commit makes use of that macro everywhere. Resolves #379 Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer
added a commit
that referenced
this pull request
Nov 12, 2024
#371 introduced a new ARRAY_ABS_BOUND macro which now has inconsistent naming with ARRAY_IN_BOUNDS. I propose to rename ARRAY_IN_BOUNDS to just ARRAY_BOUND for consistency. This commit renames the function and also moves the array that it operates on to be the first argument Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer
added a commit
that referenced
this pull request
Nov 12, 2024
#371 introduced a new macro ARRAY_ABS_BOUND for bounds that are centered around zero. This commit makes use of that macro everywhere. Resolves #379 Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer
added a commit
that referenced
this pull request
Nov 12, 2024
#371 introduced a new ARRAY_ABS_BOUND macro which now has inconsistent naming with ARRAY_IN_BOUNDS. I propose to rename ARRAY_IN_BOUNDS to just ARRAY_BOUND for consistency. This commit renames the function and also moves the array that it operates on to be the first argument Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer
added a commit
that referenced
this pull request
Nov 12, 2024
#371 introduced a new ARRAY_ABS_BOUND macro which now has inconsistent naming with ARRAY_IN_BOUNDS. I propose to rename ARRAY_IN_BOUNDS to just ARRAY_BOUND for consistency. This commit renames the function and also moves the array that it operates on to be the first argument Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer
added a commit
that referenced
this pull request
Nov 12, 2024
#371 introduced a new macro ARRAY_ABS_BOUND for bounds that are centered around zero. This commit makes use of that macro everywhere. Resolves #379 Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer
added a commit
that referenced
this pull request
Nov 12, 2024
#371 introduced a new ARRAY_ABS_BOUND macro which now has inconsistent naming with ARRAY_IN_BOUNDS. I propose to rename ARRAY_IN_BOUNDS to just ARRAY_BOUND for consistency. This commit renames the function and also moves the array that it operates on to be the first argument Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer
added a commit
that referenced
this pull request
Nov 12, 2024
#371 introduced a new ARRAY_ABS_BOUND macro which now has inconsistent naming with ARRAY_IN_BOUNDS. I propose to rename ARRAY_IN_BOUNDS to just ARRAY_BOUND for consistency. This commit renames the function and also moves the array that it operates on to be the first argument Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer
added a commit
that referenced
this pull request
Nov 12, 2024
#371 introduced a new macro ARRAY_ABS_BOUND for bounds that are centered around zero. This commit makes use of that macro everywhere. Resolves #379 Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer
added a commit
that referenced
this pull request
Nov 12, 2024
#371 introduced a new ARRAY_ABS_BOUND macro which now has inconsistent naming with ARRAY_IN_BOUNDS. I propose to rename ARRAY_IN_BOUNDS to just ARRAY_BOUND for consistency. This commit renames the function and also moves the array that it operates on to be the first argument Signed-off-by: Matthias J. Kannwischer <[email protected]>
hanno-becker
pushed a commit
that referenced
this pull request
Nov 12, 2024
#371 introduced a new macro ARRAY_ABS_BOUND for bounds that are centered around zero. This commit makes use of that macro everywhere. Resolves #379 Signed-off-by: Matthias J. Kannwischer <[email protected]>
hanno-becker
pushed a commit
that referenced
this pull request
Nov 12, 2024
#371 introduced a new ARRAY_ABS_BOUND macro which now has inconsistent naming with ARRAY_IN_BOUNDS. I propose to rename ARRAY_IN_BOUNDS to just ARRAY_BOUND for consistency. This commit renames the function and also moves the array that it operates on to be the first argument Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer
added a commit
that referenced
this pull request
Nov 13, 2024
#371 introduced a new ARRAY_ABS_BOUND macro which now has inconsistent naming with ARRAY_IN_BOUNDS. I propose to rename ARRAY_IN_BOUNDS to just ARRAY_BOUND for consistency. This commit renames the function and also moves the array that it operates on to be the first argument Signed-off-by: Matthias J. Kannwischer <[email protected]>
hanno-becker
pushed a commit
that referenced
this pull request
Nov 13, 2024
#371 introduced a new macro ARRAY_ABS_BOUND for bounds that are centered around zero. This commit makes use of that macro everywhere. Resolves #379 Signed-off-by: Matthias J. Kannwischer <[email protected]>
hanno-becker
pushed a commit
that referenced
this pull request
Nov 13, 2024
#371 introduced a new ARRAY_ABS_BOUND macro which now has inconsistent naming with ARRAY_IN_BOUNDS. I propose to rename ARRAY_IN_BOUNDS to just ARRAY_BOUND for consistency. This commit renames the function and also moves the array that it operates on to be the first argument Signed-off-by: Matthias J. Kannwischer <[email protected]>
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.
No description provided.