Skip to content

Commit 1c4f4d2

Browse files
jakemasUbuntu
jakemas
authored and
Ubuntu
committed
ML-DSA: import x86_64 assembly backend from mldsa-native
Output of: GITHUB_SHA=1b47ba602b3220fb06380840fd516dde4243122e ./importer.sh --force No manual changes — reproducible by running the above command.
1 parent f3b147e commit 1c4f4d2

37 files changed

Lines changed: 10291 additions & 3261 deletions

‎crypto/fipsmodule/ml_dsa/META.yml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
name: mldsa-native
22
source: pq-code-package/mldsa-native.git
3-
branch: main
4-
commit: b61e84f0c73d4ed612ffcaea4282a9d682de3f46
5-
imported-at: 2026-01-16T13:12:01-0800
3+
branch: 1b47ba602b3220fb06380840fd516dde4243122e
4+
commit: 1b47ba602b3220fb06380840fd516dde4243122e
5+
imported-at: 2026-05-14T03:52:22+0000

‎crypto/fipsmodule/ml_dsa/mldsa/.clang-format‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,4 +26,4 @@ Macros:
2626
- __contract__(x)={ void a; void b; void c; void d; void e; void f; } void abcdefghijklmnopqrstuvw()
2727
- __loop__(x)={} do
2828
# Make this artifically long to force line break
29-
- MLK_INTERNAL_API=void abcdefghijklmnopqrstuvwabcdefghijklmnopqrstuvwabcdefg();
29+
- MLD_INTERNAL_API=void abcdefghijklmnopqrstuvwabcdefghijklmnopqrstuvwabcdefg();

‎crypto/fipsmodule/ml_dsa/mldsa/cbmc.h‎

Lines changed: 24 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55

66
#ifndef MLD_CBMC_H
77
#define MLD_CBMC_H
8+
89
/***************************************************
910
* Basic replacements for __CPROVER_XXX contracts
1011
***************************************************/
@@ -16,11 +17,19 @@
1617

1718
#else /* !CBMC */
1819

19-
#include <stdint.h>
2020

2121
#define __contract__(x) x
2222
#define __loop__(x) x
2323

24+
/* Conditionally expand to __VA_ARGS__ depending on MLD_CONFIG_REDUCE_RAM. */
25+
#if defined(MLD_CONFIG_REDUCE_RAM)
26+
#define MLD_IF_REDUCE_RAM(...) __VA_ARGS__
27+
#define MLD_IF_NOT_REDUCE_RAM(...)
28+
#else
29+
#define MLD_IF_REDUCE_RAM(...)
30+
#define MLD_IF_NOT_REDUCE_RAM(...) __VA_ARGS__
31+
#endif
32+
2433
/* https://diffblue.github.io/cbmc/contracts-assigns.html */
2534
#define assigns(...) __CPROVER_assigns(__VA_ARGS__)
2635

@@ -97,7 +106,7 @@
97106
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> (predicate) \
98107
}
99108

100-
#define exists(qvar, qvar_lb, qvar_ub, predicate) \
109+
#define exists(qvar, qvar_lb, qvar_ub, predicate) \
101110
__CPROVER_exists \
102111
{ \
103112
unsigned qvar; \
@@ -121,30 +130,30 @@
121130
{ \
122131
unsigned qvar; \
123132
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \
124-
(((int)(value_lb) <= ((array_var)[(qvar)])) && \
125-
(((array_var)[(qvar)]) < (int)(value_ub))) \
133+
(((int)(value_lb) <= ((array_var)[(qvar)])) && \
134+
(((array_var)[(qvar)]) < (int)(value_ub))) \
126135
}
127136

128137
#define array_bound(array_var, qvar_lb, qvar_ub, value_lb, value_ub) \
129-
array_bound_core(CBMC_CONCAT(_cbmc_idx, __COUNTER__), (qvar_lb), \
138+
array_bound_core(CBMC_CONCAT(_cbmc_idx, __COUNTER__), (qvar_lb), \
130139
(qvar_ub), (array_var), (value_lb), (value_ub))
131140

132-
#define array_unchanged_core(qvar, qvar_lb, qvar_ub, array_var) \
133-
__CPROVER_forall \
134-
{ \
135-
unsigned qvar; \
136-
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \
141+
#define array_unchanged_core(qvar, qvar_lb, qvar_ub, array_var) \
142+
__CPROVER_forall \
143+
{ \
144+
unsigned qvar; \
145+
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \
137146
((array_var)[(qvar)]) == (old(* (int32_t (*)[(qvar_ub)])(array_var)))[(qvar)] \
138147
}
139148

140149
#define array_unchanged(array_var, N) \
141150
array_unchanged_core(CBMC_CONCAT(_cbmc_idx, __COUNTER__), 0, (N), (array_var))
142151

143-
#define array_unchanged_u64_core(qvar, qvar_lb, qvar_ub, array_var) \
144-
__CPROVER_forall \
145-
{ \
146-
unsigned qvar; \
147-
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \
152+
#define array_unchanged_u64_core(qvar, qvar_lb, qvar_ub, array_var) \
153+
__CPROVER_forall \
154+
{ \
155+
unsigned qvar; \
156+
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \
148157
((array_var)[(qvar)]) == (old(* (uint64_t (*)[(qvar_ub)])(array_var)))[(qvar)] \
149158
}
150159

‎crypto/fipsmodule/ml_dsa/mldsa/common.h‎

Lines changed: 39 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,11 @@
66
#ifndef MLD_COMMON_H
77
#define MLD_COMMON_H
88

9+
#ifndef __ASSEMBLER__
10+
#include <stdint.h>
11+
#endif
12+
13+
914
#define MLD_BUILD_INTERNAL
1015

1116
#if defined(MLD_CONFIG_FILE)
@@ -21,8 +26,12 @@
2126
* this can be overwritten by the user, e.g. for single-CU builds. */
2227
#if !defined(MLD_CONFIG_INTERNAL_API_QUALIFIER)
2328
#define MLD_INTERNAL_API
29+
#define MLD_INTERNAL_DATA_DECLARATION extern
30+
#define MLD_INTERNAL_DATA_DEFINITION
2431
#else
2532
#define MLD_INTERNAL_API MLD_CONFIG_INTERNAL_API_QUALIFIER
33+
#define MLD_INTERNAL_DATA_DECLARATION MLD_CONFIG_INTERNAL_API_QUALIFIER
34+
#define MLD_INTERNAL_DATA_DEFINITION MLD_CONFIG_INTERNAL_API_QUALIFIER
2635
#endif
2736

2837
#if !defined(MLD_CONFIG_EXTERNAL_API_QUALIFIER)
@@ -77,8 +86,24 @@
7786
*/
7887
#if defined(MLD_SYS_X86_64)
7988
#define MLD_ASM_FN_SYMBOL(sym) MLD_ASM_NAMESPACE(sym) : MLD_CET_ENDBR
80-
#else
89+
#elif defined(MLD_SYS_ARMV81M_MVE)
90+
/* clang-format off */
91+
#define MLD_ASM_FN_SYMBOL(sym) \
92+
.type MLD_ASM_NAMESPACE(sym), %function; \
93+
MLD_ASM_NAMESPACE(sym) :
94+
/* clang-format on */
95+
#else /* !MLD_SYS_X86_64 && MLD_SYS_ARMV81M_MVE */
8196
#define MLD_ASM_FN_SYMBOL(sym) MLD_ASM_NAMESPACE(sym) :
97+
#endif /* !MLD_SYS_X86_64 && !MLD_SYS_ARMV81M_MVE */
98+
99+
/*
100+
* Output the size of an assembly function.
101+
*/
102+
#if defined(__ELF__)
103+
#define MLD_ASM_FN_SIZE(sym) \
104+
.size MLD_ASM_NAMESPACE(sym), .- MLD_ASM_NAMESPACE(sym)
105+
#else
106+
#define MLD_ASM_FN_SIZE(sym)
82107
#endif
83108

84109
/* We aim to simplify the user's life by supporting builds where
@@ -107,6 +132,14 @@
107132
#error Bad configuration: MLD_CONFIG_NO_RANDOMIZED_API is incompatible with MLD_CONFIG_KEYGEN_PCT as the current PCT implementation requires crypto_sign_signature()
108133
#endif
109134

135+
#if defined(MLD_CONFIG_NO_SIGN_API) && defined(MLD_CONFIG_KEYGEN_PCT)
136+
#error Bad configuration: MLD_CONFIG_NO_SIGN_API is incompatible with MLD_CONFIG_KEYGEN_PCT as the current PCT implementation requires crypto_sign_signature()
137+
#endif
138+
139+
#if defined(MLD_CONFIG_NO_VERIFY_API) && defined(MLD_CONFIG_KEYGEN_PCT)
140+
#error Bad configuration: MLD_CONFIG_NO_VERIFY_API is incompatible with MLD_CONFIG_KEYGEN_PCT as the current PCT implementation requires crypto_sign_verify()
141+
#endif
142+
110143
#if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH)
111144
#include MLD_CONFIG_ARITH_BACKEND_FILE
112145
/* Include to enforce consistency of API and implementation,
@@ -269,20 +302,6 @@
269302

270303
#endif /* MLD_CONFIG_CUSTOM_ALLOC_FREE */
271304

272-
/*
273-
* We are facing severe CBMC performance issues when using unions.
274-
* As a temporary workaround, we use unions only when MLD_CONFIG_REDUCE_RAM is
275-
* set.
276-
* TODO: Remove the workaround once
277-
* https://github.com/diffblue/cbmc/issues/8813
278-
* is resolved
279-
*/
280-
#if defined(MLD_CONFIG_REDUCE_RAM)
281-
#define MLK_UNION_OR_STRUCT union
282-
#else
283-
#define MLK_UNION_OR_STRUCT struct
284-
#endif
285-
286305
/****************************** Error codes ***********************************/
287306

288307
/* Generic failure condition */
@@ -293,6 +312,11 @@
293312
/* An rng failure occured. Might be due to insufficient entropy or
294313
* system misconfiguration. */
295314
#define MLD_ERR_RNG_FAIL -3
315+
/* The signing rejection-sampling loop exceeded
316+
* MLD_CONFIG_MAX_SIGNING_ATTEMPTS iterations without producing a valid
317+
* signature. With a FIPS 204 Appendix C compliant bound (>= 814) this
318+
* has probability < 2^-256. */
319+
#define MLD_ERR_SIGN_ATTEMPTS_EXHAUSTED -4
296320

297321

298322
#endif /* !__ASSEMBLER__ */

0 commit comments

Comments
 (0)