Skip to content

ML-DSA x86 AVX2 rej_uniform CORRECT proof #401

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jakemas wants to merge 24 commits into
base: main
Choose a base branch
from
Open

ML-DSA x86 AVX2 rej_uniform CORRECT proof #401

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
2b23121
x86: Add VMOVMSKPS, VPMOVZXBD, VZEROUPPER instruction models
jakemas Apr 8, 2026
97f9789
Merge branch 'main' into jakemas/add-x86-vmovmskps-vpmovzxbd-vzeroupper
jakemas Apr 13, 2026
1e19874
Merge branch 'main' into jakemas/add-x86-vmovmskps-vpmovzxbd-vzeroupper
jakemas Apr 15, 2026
02c0dad
Merge branch 'main' into jakemas/add-x86-vmovmskps-vpmovzxbd-vzeroupper
jakemas Apr 16, 2026
7c65f15
Model VZEROUPPER correctly: zero upper bits of ZMM0-ZMM15
jakemas Apr 16, 2026
a062365
Fix VZEROUPPER cosimulation: use YMM writes instead of XMM
Apr 29, 2026
95b1901
Merge branch 'main' into jakemas/add-x86-vmovmskps-vpmovzxbd-vzeroupper
Apr 29, 2026
4c4fe1d
Merge branch 'main' into jakemas/add-x86-vmovmskps-vpmovzxbd-vzeroupper
jakemas Apr 29, 2026
8fcec64
ML-DSA x86 AVX2 rej_uniform CORRECT proof
jakemas May 6, 2026
6a81e1d
Declare mldsa_rej_uniform in s2n-bignum.h + register as x86-only sign…
jakemas May 6, 2026
10d8732
Add SUBROUTINE_CORRECT variants and clean up proof
jakemas May 6, 2026
edab6d0
Register MLDSA_REJ_UNIFORM SUBROUTINE variants in specifications.txt
jakemas May 6, 2026
0ec320e
Add Windows ABI proof for x86 mldsa_rej_uniform
jakemas May 6, 2026
b9871fc
Register MLDSA_REJ_UNIFORM Windows variants in specifications.txt
jakemas May 6, 2026
00c144e
Regenerate AT&T translation of mldsa_rej_uniform.S
jakemas May 6, 2026
bcd2c31
Drop vzeroupper from mldsa_rej_uniform
jakemas May 8, 2026
2c84f35
Merge remote-tracking branch 'upstream/main' into jakemas/mldsa-rej-u…
jakemas May 8, 2026
5b85e45
Add mldsa_rej_uniform test and benchmark entries
May 9, 2026
6414c0f
Merge remote-tracking branch 'upstream/main' into jakemas/mldsa-rej-u…
May 9, 2026
dfcbafd
Prefix mldsa_rej_uniform local labels with L
May 9, 2026
256c05a
Fix mldsa_rej_uniform functionaltest enablement flag
May 9, 2026
e5172fc
Merge branch 'main' into jakemas/mldsa-rej-uniform-x86-proof
jakemas May 13, 2026
6e44de7
Merge branch 'main' into jakemas/mldsa-rej-uniform-x86-proof
jakemas May 15, 2026
fde07c6
x86/mldsa: Add memory safety proof for rej_uniform
jakemas May 30, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
267 changes: 267 additions & 0 deletions benchmarks/benchmark.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -444,6 +444,270 @@ uint8_t mlkem_rej_uniform_table[] =
0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 // 255
};

// Constant lookup table for ML-DSA rejection sampling. Matches the byte-list
// table in x86/proofs/mldsa_rej_uniform_table.ml (256 entries, 8 bytes each =
// 2048 bytes) interpreted as a uint64_t[256] table of VPERMD indices.

uint8_t mldsa_rej_uniform_table[] =
{
0, 0, 0, 0, 0, 0, 0, 0, // 0
0, 0, 0, 0, 0, 0, 0, 0, // 1
1, 0, 0, 0, 0, 0, 0, 0, // 2
0, 1, 0, 0, 0, 0, 0, 0, // 3
2, 0, 0, 0, 0, 0, 0, 0, // 4
0, 2, 0, 0, 0, 0, 0, 0, // 5
1, 2, 0, 0, 0, 0, 0, 0, // 6
0, 1, 2, 0, 0, 0, 0, 0, // 7
3, 0, 0, 0, 0, 0, 0, 0, // 8
0, 3, 0, 0, 0, 0, 0, 0, // 9
1, 3, 0, 0, 0, 0, 0, 0, // 10
0, 1, 3, 0, 0, 0, 0, 0, // 11
2, 3, 0, 0, 0, 0, 0, 0, // 12
0, 2, 3, 0, 0, 0, 0, 0, // 13
1, 2, 3, 0, 0, 0, 0, 0, // 14
0, 1, 2, 3, 0, 0, 0, 0, // 15
4, 0, 0, 0, 0, 0, 0, 0, // 16
0, 4, 0, 0, 0, 0, 0, 0, // 17
1, 4, 0, 0, 0, 0, 0, 0, // 18
0, 1, 4, 0, 0, 0, 0, 0, // 19
2, 4, 0, 0, 0, 0, 0, 0, // 20
0, 2, 4, 0, 0, 0, 0, 0, // 21
1, 2, 4, 0, 0, 0, 0, 0, // 22
0, 1, 2, 4, 0, 0, 0, 0, // 23
3, 4, 0, 0, 0, 0, 0, 0, // 24
0, 3, 4, 0, 0, 0, 0, 0, // 25
1, 3, 4, 0, 0, 0, 0, 0, // 26
0, 1, 3, 4, 0, 0, 0, 0, // 27
2, 3, 4, 0, 0, 0, 0, 0, // 28
0, 2, 3, 4, 0, 0, 0, 0, // 29
1, 2, 3, 4, 0, 0, 0, 0, // 30
0, 1, 2, 3, 4, 0, 0, 0, // 31
5, 0, 0, 0, 0, 0, 0, 0, // 32
0, 5, 0, 0, 0, 0, 0, 0, // 33
1, 5, 0, 0, 0, 0, 0, 0, // 34
0, 1, 5, 0, 0, 0, 0, 0, // 35
2, 5, 0, 0, 0, 0, 0, 0, // 36
0, 2, 5, 0, 0, 0, 0, 0, // 37
1, 2, 5, 0, 0, 0, 0, 0, // 38
0, 1, 2, 5, 0, 0, 0, 0, // 39
3, 5, 0, 0, 0, 0, 0, 0, // 40
0, 3, 5, 0, 0, 0, 0, 0, // 41
1, 3, 5, 0, 0, 0, 0, 0, // 42
0, 1, 3, 5, 0, 0, 0, 0, // 43
2, 3, 5, 0, 0, 0, 0, 0, // 44
0, 2, 3, 5, 0, 0, 0, 0, // 45
1, 2, 3, 5, 0, 0, 0, 0, // 46
0, 1, 2, 3, 5, 0, 0, 0, // 47
4, 5, 0, 0, 0, 0, 0, 0, // 48
0, 4, 5, 0, 0, 0, 0, 0, // 49
1, 4, 5, 0, 0, 0, 0, 0, // 50
0, 1, 4, 5, 0, 0, 0, 0, // 51
2, 4, 5, 0, 0, 0, 0, 0, // 52
0, 2, 4, 5, 0, 0, 0, 0, // 53
1, 2, 4, 5, 0, 0, 0, 0, // 54
0, 1, 2, 4, 5, 0, 0, 0, // 55
3, 4, 5, 0, 0, 0, 0, 0, // 56
0, 3, 4, 5, 0, 0, 0, 0, // 57
1, 3, 4, 5, 0, 0, 0, 0, // 58
0, 1, 3, 4, 5, 0, 0, 0, // 59
2, 3, 4, 5, 0, 0, 0, 0, // 60
0, 2, 3, 4, 5, 0, 0, 0, // 61
1, 2, 3, 4, 5, 0, 0, 0, // 62
0, 1, 2, 3, 4, 5, 0, 0, // 63
6, 0, 0, 0, 0, 0, 0, 0, // 64
0, 6, 0, 0, 0, 0, 0, 0, // 65
1, 6, 0, 0, 0, 0, 0, 0, // 66
0, 1, 6, 0, 0, 0, 0, 0, // 67
2, 6, 0, 0, 0, 0, 0, 0, // 68
0, 2, 6, 0, 0, 0, 0, 0, // 69
1, 2, 6, 0, 0, 0, 0, 0, // 70
0, 1, 2, 6, 0, 0, 0, 0, // 71
3, 6, 0, 0, 0, 0, 0, 0, // 72
0, 3, 6, 0, 0, 0, 0, 0, // 73
1, 3, 6, 0, 0, 0, 0, 0, // 74
0, 1, 3, 6, 0, 0, 0, 0, // 75
2, 3, 6, 0, 0, 0, 0, 0, // 76
0, 2, 3, 6, 0, 0, 0, 0, // 77
1, 2, 3, 6, 0, 0, 0, 0, // 78
0, 1, 2, 3, 6, 0, 0, 0, // 79
4, 6, 0, 0, 0, 0, 0, 0, // 80
0, 4, 6, 0, 0, 0, 0, 0, // 81
1, 4, 6, 0, 0, 0, 0, 0, // 82
0, 1, 4, 6, 0, 0, 0, 0, // 83
2, 4, 6, 0, 0, 0, 0, 0, // 84
0, 2, 4, 6, 0, 0, 0, 0, // 85
1, 2, 4, 6, 0, 0, 0, 0, // 86
0, 1, 2, 4, 6, 0, 0, 0, // 87
3, 4, 6, 0, 0, 0, 0, 0, // 88
0, 3, 4, 6, 0, 0, 0, 0, // 89
1, 3, 4, 6, 0, 0, 0, 0, // 90
0, 1, 3, 4, 6, 0, 0, 0, // 91
2, 3, 4, 6, 0, 0, 0, 0, // 92
0, 2, 3, 4, 6, 0, 0, 0, // 93
1, 2, 3, 4, 6, 0, 0, 0, // 94
0, 1, 2, 3, 4, 6, 0, 0, // 95
5, 6, 0, 0, 0, 0, 0, 0, // 96
0, 5, 6, 0, 0, 0, 0, 0, // 97
1, 5, 6, 0, 0, 0, 0, 0, // 98
0, 1, 5, 6, 0, 0, 0, 0, // 99
2, 5, 6, 0, 0, 0, 0, 0, // 100
0, 2, 5, 6, 0, 0, 0, 0, // 101
1, 2, 5, 6, 0, 0, 0, 0, // 102
0, 1, 2, 5, 6, 0, 0, 0, // 103
3, 5, 6, 0, 0, 0, 0, 0, // 104
0, 3, 5, 6, 0, 0, 0, 0, // 105
1, 3, 5, 6, 0, 0, 0, 0, // 106
0, 1, 3, 5, 6, 0, 0, 0, // 107
2, 3, 5, 6, 0, 0, 0, 0, // 108
0, 2, 3, 5, 6, 0, 0, 0, // 109
1, 2, 3, 5, 6, 0, 0, 0, // 110
0, 1, 2, 3, 5, 6, 0, 0, // 111
4, 5, 6, 0, 0, 0, 0, 0, // 112
0, 4, 5, 6, 0, 0, 0, 0, // 113
1, 4, 5, 6, 0, 0, 0, 0, // 114
0, 1, 4, 5, 6, 0, 0, 0, // 115
2, 4, 5, 6, 0, 0, 0, 0, // 116
0, 2, 4, 5, 6, 0, 0, 0, // 117
1, 2, 4, 5, 6, 0, 0, 0, // 118
0, 1, 2, 4, 5, 6, 0, 0, // 119
3, 4, 5, 6, 0, 0, 0, 0, // 120
0, 3, 4, 5, 6, 0, 0, 0, // 121
1, 3, 4, 5, 6, 0, 0, 0, // 122
0, 1, 3, 4, 5, 6, 0, 0, // 123
2, 3, 4, 5, 6, 0, 0, 0, // 124
0, 2, 3, 4, 5, 6, 0, 0, // 125
1, 2, 3, 4, 5, 6, 0, 0, // 126
0, 1, 2, 3, 4, 5, 6, 0, // 127
7, 0, 0, 0, 0, 0, 0, 0, // 128
0, 7, 0, 0, 0, 0, 0, 0, // 129
1, 7, 0, 0, 0, 0, 0, 0, // 130
0, 1, 7, 0, 0, 0, 0, 0, // 131
2, 7, 0, 0, 0, 0, 0, 0, // 132
0, 2, 7, 0, 0, 0, 0, 0, // 133
1, 2, 7, 0, 0, 0, 0, 0, // 134
0, 1, 2, 7, 0, 0, 0, 0, // 135
3, 7, 0, 0, 0, 0, 0, 0, // 136
0, 3, 7, 0, 0, 0, 0, 0, // 137
1, 3, 7, 0, 0, 0, 0, 0, // 138
0, 1, 3, 7, 0, 0, 0, 0, // 139
2, 3, 7, 0, 0, 0, 0, 0, // 140
0, 2, 3, 7, 0, 0, 0, 0, // 141
1, 2, 3, 7, 0, 0, 0, 0, // 142
0, 1, 2, 3, 7, 0, 0, 0, // 143
4, 7, 0, 0, 0, 0, 0, 0, // 144
0, 4, 7, 0, 0, 0, 0, 0, // 145
1, 4, 7, 0, 0, 0, 0, 0, // 146
0, 1, 4, 7, 0, 0, 0, 0, // 147
2, 4, 7, 0, 0, 0, 0, 0, // 148
0, 2, 4, 7, 0, 0, 0, 0, // 149
1, 2, 4, 7, 0, 0, 0, 0, // 150
0, 1, 2, 4, 7, 0, 0, 0, // 151
3, 4, 7, 0, 0, 0, 0, 0, // 152
0, 3, 4, 7, 0, 0, 0, 0, // 153
1, 3, 4, 7, 0, 0, 0, 0, // 154
0, 1, 3, 4, 7, 0, 0, 0, // 155
2, 3, 4, 7, 0, 0, 0, 0, // 156
0, 2, 3, 4, 7, 0, 0, 0, // 157
1, 2, 3, 4, 7, 0, 0, 0, // 158
0, 1, 2, 3, 4, 7, 0, 0, // 159
5, 7, 0, 0, 0, 0, 0, 0, // 160
0, 5, 7, 0, 0, 0, 0, 0, // 161
1, 5, 7, 0, 0, 0, 0, 0, // 162
0, 1, 5, 7, 0, 0, 0, 0, // 163
2, 5, 7, 0, 0, 0, 0, 0, // 164
0, 2, 5, 7, 0, 0, 0, 0, // 165
1, 2, 5, 7, 0, 0, 0, 0, // 166
0, 1, 2, 5, 7, 0, 0, 0, // 167
3, 5, 7, 0, 0, 0, 0, 0, // 168
0, 3, 5, 7, 0, 0, 0, 0, // 169
1, 3, 5, 7, 0, 0, 0, 0, // 170
0, 1, 3, 5, 7, 0, 0, 0, // 171
2, 3, 5, 7, 0, 0, 0, 0, // 172
0, 2, 3, 5, 7, 0, 0, 0, // 173
1, 2, 3, 5, 7, 0, 0, 0, // 174
0, 1, 2, 3, 5, 7, 0, 0, // 175
4, 5, 7, 0, 0, 0, 0, 0, // 176
0, 4, 5, 7, 0, 0, 0, 0, // 177
1, 4, 5, 7, 0, 0, 0, 0, // 178
0, 1, 4, 5, 7, 0, 0, 0, // 179
2, 4, 5, 7, 0, 0, 0, 0, // 180
0, 2, 4, 5, 7, 0, 0, 0, // 181
1, 2, 4, 5, 7, 0, 0, 0, // 182
0, 1, 2, 4, 5, 7, 0, 0, // 183
3, 4, 5, 7, 0, 0, 0, 0, // 184
0, 3, 4, 5, 7, 0, 0, 0, // 185
1, 3, 4, 5, 7, 0, 0, 0, // 186
0, 1, 3, 4, 5, 7, 0, 0, // 187
2, 3, 4, 5, 7, 0, 0, 0, // 188
0, 2, 3, 4, 5, 7, 0, 0, // 189
1, 2, 3, 4, 5, 7, 0, 0, // 190
0, 1, 2, 3, 4, 5, 7, 0, // 191
6, 7, 0, 0, 0, 0, 0, 0, // 192
0, 6, 7, 0, 0, 0, 0, 0, // 193
1, 6, 7, 0, 0, 0, 0, 0, // 194
0, 1, 6, 7, 0, 0, 0, 0, // 195
2, 6, 7, 0, 0, 0, 0, 0, // 196
0, 2, 6, 7, 0, 0, 0, 0, // 197
1, 2, 6, 7, 0, 0, 0, 0, // 198
0, 1, 2, 6, 7, 0, 0, 0, // 199
3, 6, 7, 0, 0, 0, 0, 0, // 200
0, 3, 6, 7, 0, 0, 0, 0, // 201
1, 3, 6, 7, 0, 0, 0, 0, // 202
0, 1, 3, 6, 7, 0, 0, 0, // 203
2, 3, 6, 7, 0, 0, 0, 0, // 204
0, 2, 3, 6, 7, 0, 0, 0, // 205
1, 2, 3, 6, 7, 0, 0, 0, // 206
0, 1, 2, 3, 6, 7, 0, 0, // 207
4, 6, 7, 0, 0, 0, 0, 0, // 208
0, 4, 6, 7, 0, 0, 0, 0, // 209
1, 4, 6, 7, 0, 0, 0, 0, // 210
0, 1, 4, 6, 7, 0, 0, 0, // 211
2, 4, 6, 7, 0, 0, 0, 0, // 212
0, 2, 4, 6, 7, 0, 0, 0, // 213
1, 2, 4, 6, 7, 0, 0, 0, // 214
0, 1, 2, 4, 6, 7, 0, 0, // 215
3, 4, 6, 7, 0, 0, 0, 0, // 216
0, 3, 4, 6, 7, 0, 0, 0, // 217
1, 3, 4, 6, 7, 0, 0, 0, // 218
0, 1, 3, 4, 6, 7, 0, 0, // 219
2, 3, 4, 6, 7, 0, 0, 0, // 220
0, 2, 3, 4, 6, 7, 0, 0, // 221
1, 2, 3, 4, 6, 7, 0, 0, // 222
0, 1, 2, 3, 4, 6, 7, 0, // 223
5, 6, 7, 0, 0, 0, 0, 0, // 224
0, 5, 6, 7, 0, 0, 0, 0, // 225
1, 5, 6, 7, 0, 0, 0, 0, // 226
0, 1, 5, 6, 7, 0, 0, 0, // 227
2, 5, 6, 7, 0, 0, 0, 0, // 228
0, 2, 5, 6, 7, 0, 0, 0, // 229
1, 2, 5, 6, 7, 0, 0, 0, // 230
0, 1, 2, 5, 6, 7, 0, 0, // 231
3, 5, 6, 7, 0, 0, 0, 0, // 232
0, 3, 5, 6, 7, 0, 0, 0, // 233
1, 3, 5, 6, 7, 0, 0, 0, // 234
0, 1, 3, 5, 6, 7, 0, 0, // 235
2, 3, 5, 6, 7, 0, 0, 0, // 236
0, 2, 3, 5, 6, 7, 0, 0, // 237
1, 2, 3, 5, 6, 7, 0, 0, // 238
0, 1, 2, 3, 5, 6, 7, 0, // 239
4, 5, 6, 7, 0, 0, 0, 0, // 240
0, 4, 5, 6, 7, 0, 0, 0, // 241
1, 4, 5, 6, 7, 0, 0, 0, // 242
0, 1, 4, 5, 6, 7, 0, 0, // 243
2, 4, 5, 6, 7, 0, 0, 0, // 244
0, 2, 4, 5, 6, 7, 0, 0, // 245
1, 2, 4, 5, 6, 7, 0, 0, // 246
0, 1, 2, 4, 5, 6, 7, 0, // 247
3, 4, 5, 6, 7, 0, 0, 0, // 248
0, 3, 4, 5, 6, 7, 0, 0, // 249
1, 3, 4, 5, 6, 7, 0, 0, // 250
0, 1, 3, 4, 5, 6, 7, 0, // 251
2, 3, 4, 5, 6, 7, 0, 0, // 252
0, 2, 3, 4, 5, 6, 7, 0, // 253
1, 2, 3, 4, 5, 6, 7, 0, // 254
0, 1, 2, 3, 4, 5, 6, 7 // 255
};

// Wrappers round the functions to call uniformly

void call_bignum_add__4_4(void) repeat(bignum_add(4,b0,4,b1,4,b2))
Expand Down Expand Up @@ -1112,6 +1376,7 @@ void call_mldsa_pointwise_acc_l4(void) repeat(mldsa_pointwise_acc_l4_x86((int32_
void call_mldsa_pointwise_acc_l5(void) repeat(mldsa_pointwise_acc_l5_x86((int32_t*)b0,(const int32_t*)b1,(const int32_t*)b2,mldsa_avx2_qdata))
void call_mldsa_pointwise_acc_l7(void) repeat(mldsa_pointwise_acc_l7_x86((int32_t*)b0,(const int32_t*)b1,(const int32_t*)b2,mldsa_avx2_qdata))
void call_mldsa_reduce(void) repeat(mldsa_reduce((int32_t*)b0))
void call_mldsa_rej_uniform(void) repeat(mldsa_rej_uniform((int32_t*)b0,(uint8_t*)b1,(const uint64_t*)mldsa_rej_uniform_table))

void call_mlkem_frombytes(void) repeat(mlkem_frombytes((uint16_t*)b0,(int8_t*)b1))
void call_mlkem_intt(void) repeat(mlkem_intt_x86((int16_t*)b0,(int16_t*)b1))
Expand Down Expand Up @@ -1156,6 +1421,7 @@ void call_mldsa_pointwise_acc_l4(void) repeat(mldsa_pointwise_acc_l4((int32_t*)b
void call_mldsa_pointwise_acc_l5(void) repeat(mldsa_pointwise_acc_l5((int32_t*)b0,(const int32_t*)b1,(const int32_t*)b2))
void call_mldsa_pointwise_acc_l7(void) repeat(mldsa_pointwise_acc_l7((int32_t*)b0,(const int32_t*)b1,(const int32_t*)b2))
void call_mldsa_reduce(void) {}
void call_mldsa_rej_uniform(void) {}

void call_bignum_copy_row_from_table_8n__32_16(void) \
repeat(bignum_copy_row_from_table_8n(b0,b1,32,16,0))
Expand Down Expand Up @@ -1630,6 +1896,7 @@ int main(int argc, char *argv[])
timingtest(all,"mldsa_pointwise_acc_l5",call_mldsa_pointwise_acc_l5);
timingtest(all,"mldsa_pointwise_acc_l7",call_mldsa_pointwise_acc_l7);
timingtest(!arm,"mldsa_reduce",call_mldsa_reduce);
timingtest(!arm,"mldsa_rej_uniform",call_mldsa_rej_uniform);
timingtest(bmi,"p256_montjadd",call_p256_montjadd);
timingtest(all,"p256_montjadd_alt",call_p256_montjadd_alt);
timingtest(bmi,"p256_montjdouble",call_p256_montjdouble);
Expand Down
7 changes: 7 additions & 0 deletions include/s2n-bignum-c89.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1013,6 +1013,13 @@ extern void mldsa_ntt(int32_t a[256], const int32_t zetas[624]);
/* Input a[256] (signed 32-bit words); output a[256] (signed 32-bit words) */
extern void mldsa_nttunpack(int32_t a[256]);

/* Uniform rejection sampling for ML-DSA: extract 23-bit coefficients from */
/* 3-byte-packed input, keeping only those strictly less than q = 8380417. */
/* Returns the number of accepted coefficients (at most 256). */
/* Inputs buf[840] (uint8_t), table[256] (uint64_t lookup table); */
/* output r[256] (int32_t). */
extern uint32_t mldsa_rej_uniform(int32_t r[256], const uint8_t buf[840], const uint64_t table[256]);

/* Pointwise multiplication of polynomials in NTT domain (Montgomery form) for ML-DSA */
/* Inputs a[256], b[256] (signed 32-bit words); output r[256] (signed 32-bit words) */
extern void mldsa_pointwise(int32_t r[256], const int32_t a[256], const int32_t b[256]);
Expand Down
7 changes: 7 additions & 0 deletions include/s2n-bignum.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1018,6 +1018,13 @@ extern void mldsa_ntt(int32_t a[S2N_BIGNUM_STATIC 256], const int32_t zetas[S2N_
// Input a[256] (signed 32-bit words); output a[256] (signed 32-bit words)
extern void mldsa_nttunpack(int32_t a[S2N_BIGNUM_STATIC 256]);

// Uniform rejection sampling for ML-DSA: extract 23-bit coefficients from
// 3-byte-packed input, keeping only those strictly less than q = 8380417.
// Returns the number of accepted coefficients (at most 256).
// Inputs buf[840] (uint8_t), table[256] (uint64_t lookup table);
// output r[256] (int32_t).
extern uint32_t mldsa_rej_uniform(int32_t r[S2N_BIGNUM_STATIC 256], const uint8_t buf[S2N_BIGNUM_STATIC 840], const uint64_t table[S2N_BIGNUM_STATIC 256]);

// Pointwise multiplication of polynomials in NTT domain (Montgomery form) for ML-DSA
// Inputs a[256], b[256] (signed 32-bit words); output r[256] (signed 32-bit words)
extern void mldsa_pointwise(int32_t r[S2N_BIGNUM_STATIC 256], const int32_t a[S2N_BIGNUM_STATIC 256], const int32_t b[S2N_BIGNUM_STATIC 256]);
Expand Down
Loading