Skip to content

Commit b945b53

Browse files
mkannwischermkannwischer
committed
Inline reduce.c
After the constant-time hardening has been applied, we can simply inline all functions. This should dramatically improve non-LTO performance. Signed-off-by: Matthias J. Kannwischer <[email protected]>
1 parent 7250ed3 commit b945b53

File tree

11 files changed

+82
-97
lines changed

11 files changed

+82
-97
lines changed

‎mldsa/reduce.c‎

Lines changed: 0 additions & 76 deletions
This file was deleted.

‎mldsa/reduce.h‎

Lines changed: 70 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@
88
#include <stdint.h>
99
#include "cbmc.h"
1010
#include "common.h"
11+
#include "ct.h"
1112

1213
#define MONT -4186625 /* 2^32 % MLDSA_Q */
1314

@@ -24,7 +25,35 @@
2425
#define MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX ((int64_t)INT32_MIN * -MLDSA_Q)
2526

2627

27-
#define mld_montgomery_reduce MLD_NAMESPACE(montgomery_reduce)
28+
29+
/*************************************************
30+
* Name: mld_cast_uint32_to_int32
31+
*
32+
* Description: Cast uint32 value to int32
33+
*
34+
* Returns:
35+
* input x in 0 .. 2^31-1: returns value unchanged
36+
* input x in 2^31 .. 2^32-1: returns (x - 2^32)
37+
**************************************************/
38+
#ifdef CBMC
39+
#pragma CPROVER check push
40+
#pragma CPROVER check disable "conversion"
41+
#endif
42+
static MLD_INLINE int32_t mld_cast_uint32_to_int32(uint32_t x)
43+
{
44+
/*
45+
* PORTABILITY: This relies on uint32_t -> int32_t
46+
* being implemented as the inverse of int32_t -> uint32_t,
47+
* which is implementation-defined (C99 6.3.1.3 (3))
48+
* CBMC (correctly) fails to prove this conversion is OK,
49+
* so we have to suppress that check here
50+
*/
51+
return (int32_t)x;
52+
}
53+
#ifdef CBMC
54+
#pragma CPROVER check pop
55+
#endif
56+
2857
/*************************************************
2958
* Name: mld_montgomery_reduce
3059
*
@@ -46,17 +75,39 @@
4675
*
4776
* Returns r.
4877
**************************************************/
49-
int32_t mld_montgomery_reduce(int64_t a)
78+
static MLD_INLINE int32_t mld_montgomery_reduce(int64_t a)
5079
__contract__(
5180
requires(a >= -MONTGOMERY_REDUCE_DOMAIN_MAX && a <= MONTGOMERY_REDUCE_DOMAIN_MAX)
5281
ensures(return_value >= INT32_MIN && return_value < REDUCE32_DOMAIN_MAX)
5382

5483
/* Special case - for stronger input bounds, we can ensure stronger bounds on the output */
5584
ensures((a >= -MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX && a < MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX) ==>
5685
(return_value > -MLDSA_Q && return_value < MLDSA_Q))
57-
);
86+
)
87+
{
88+
/* check-magic: 58728449 == unsigned_mod(pow(MLDSA_Q, -1, 2^32), 2^32) */
89+
const uint64_t QINV = 58728449;
90+
91+
/* Compute a*q^{-1} mod 2^32 in unsigned representatives */
92+
const uint32_t a_reduced = a & UINT32_MAX;
93+
const uint32_t a_inverted = (a_reduced * QINV) & UINT32_MAX;
94+
95+
/* Lift to signed canonical representative mod 2^32. */
96+
const int32_t t = mld_cast_uint32_to_int32(a_inverted);
97+
98+
int64_t r;
99+
100+
r = a - ((int64_t)t * MLDSA_Q);
101+
102+
/*
103+
* PORTABILITY: Right-shift on a signed integer is, strictly-speaking,
104+
* implementation-defined for negative left argument. Here,
105+
* we assume it's sign-preserving "arithmetic" shift right. (C99 6.5.7 (5))
106+
*/
107+
r = r >> 32;
108+
return (int32_t)r;
109+
}
58110

59-
#define mld_reduce32 MLD_NAMESPACE(reduce32)
60111
/*************************************************
61112
* Name: mld_reduce32
62113
*
@@ -68,14 +119,21 @@ __contract__(
68119
*
69120
* Returns r.
70121
**************************************************/
71-
int32_t mld_reduce32(int32_t a)
122+
static MLD_INLINE int32_t mld_reduce32(int32_t a)
72123
__contract__(
73124
requires(a <= REDUCE32_DOMAIN_MAX)
74125
ensures(return_value >= -REDUCE32_RANGE_MAX)
75126
ensures(return_value < REDUCE32_RANGE_MAX)
76-
);
127+
)
128+
{
129+
int32_t t;
130+
131+
t = (a + (1 << 22)) >> 23;
132+
t = a - t * MLDSA_Q;
133+
cassert((t - a) % MLDSA_Q == 0);
134+
return t;
135+
}
77136

78-
#define mld_caddq MLD_NAMESPACE(caddq)
79137
/*************************************************
80138
* Name: mld_caddq
81139
*
@@ -85,14 +143,17 @@ __contract__(
85143
*
86144
* Returns r.
87145
**************************************************/
88-
int32_t mld_caddq(int32_t a)
146+
static MLD_INLINE int32_t mld_caddq(int32_t a)
89147
__contract__(
90148
requires(a > -MLDSA_Q)
91149
requires(a < MLDSA_Q)
92150
ensures(return_value >= 0)
93151
ensures(return_value < MLDSA_Q)
94152
ensures(return_value == (a >= 0) ? a : (a + MLDSA_Q))
95-
);
153+
)
154+
{
155+
return mld_ct_sel_int32(a + MLDSA_Q, a, mld_ct_cmask_neg_i32(a));
156+
}
96157

97158

98159
#endif /* !MLD_REDUCE_H */

‎proofs/cbmc/caddq/Makefile‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,9 +17,9 @@ REMOVE_FUNCTION_BODY +=
1717
UNWINDSET +=
1818

1919
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
20-
PROJECT_SOURCES += $(SRCDIR)/mldsa/reduce.c
20+
PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c
2121

22-
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)caddq
22+
CHECK_FUNCTION_CONTRACTS=mld_caddq
2323
USE_FUNCTION_CONTRACTS=mld_ct_sel_int32 mld_ct_cmask_neg_i32
2424
APPLY_LOOP_CONTRACTS=on
2525
USE_DYNAMIC_FRAMES=1

‎proofs/cbmc/fqmul/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY +=
1717
UNWINDSET +=
1818

1919
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
20-
PROJECT_SOURCES += $(SRCDIR)/mldsa/ntt.c $(SRCDIR)/mldsa/reduce.c
20+
PROJECT_SOURCES += $(SRCDIR)/mldsa/ntt.c
2121

2222
CHECK_FUNCTION_CONTRACTS=mld_fqmul
2323
USE_FUNCTION_CONTRACTS=

‎proofs/cbmc/fqscale/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY +=
1717
UNWINDSET +=
1818

1919
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
20-
PROJECT_SOURCES += $(SRCDIR)/mldsa/ntt.c $(SRCDIR)/mldsa/reduce.c
20+
PROJECT_SOURCES += $(SRCDIR)/mldsa/ntt.c
2121

2222
CHECK_FUNCTION_CONTRACTS=mld_fqscale
2323
USE_FUNCTION_CONTRACTS=

‎proofs/cbmc/montgomery_reduce/Makefile‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,9 +17,9 @@ REMOVE_FUNCTION_BODY +=
1717
UNWINDSET +=
1818

1919
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
20-
PROJECT_SOURCES += $(SRCDIR)/mldsa/reduce.c
20+
PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c
2121

22-
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)montgomery_reduce
22+
CHECK_FUNCTION_CONTRACTS=mld_montgomery_reduce
2323
USE_FUNCTION_CONTRACTS=
2424
APPLY_LOOP_CONTRACTS=on
2525
USE_DYNAMIC_FRAMES=1

‎proofs/cbmc/poly_caddq/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
2020
PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c
2121

2222
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_caddq
23-
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)caddq
23+
USE_FUNCTION_CONTRACTS=mld_caddq
2424
APPLY_LOOP_CONTRACTS=on
2525
USE_DYNAMIC_FRAMES=1
2626

‎proofs/cbmc/poly_pointwise_montgomery/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
2020
PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c
2121

2222
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_pointwise_montgomery
23-
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)montgomery_reduce
23+
USE_FUNCTION_CONTRACTS=mld_montgomery_reduce
2424
APPLY_LOOP_CONTRACTS=on
2525
USE_DYNAMIC_FRAMES=1
2626

‎proofs/cbmc/poly_reduce/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
2020
PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c
2121

2222
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_reduce
23-
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)reduce32
23+
USE_FUNCTION_CONTRACTS=mld_reduce32
2424
APPLY_LOOP_CONTRACTS=on
2525
USE_DYNAMIC_FRAMES=1
2626

‎proofs/cbmc/polyvecl_pointwise_acc_montgomery/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
2020
PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c
2121

2222
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_pointwise_acc_montgomery
23-
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)montgomery_reduce
23+
USE_FUNCTION_CONTRACTS=mld_montgomery_reduce
2424
APPLY_LOOP_CONTRACTS=on
2525
USE_DYNAMIC_FRAMES=1
2626

0 commit comments

Comments
 (0)