Skip to content

Commit c6d7c93

Browse files
willieyzhanno-becker
authored andcommitted
Replace FIPS202_NAMESPACE to MLD_NAMESPACE
Signed-off-by: willieyz <[email protected]>
1 parent 5c00492 commit c6d7c93

File tree

45 files changed

+73
-77
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

45 files changed

+73
-77
lines changed

mldsa/mldsa_native.S

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -438,7 +438,6 @@
438438
* Undefine macros from FIPS-202 files
439439
*/
440440
/* mldsa/src/fips202/fips202.h */
441-
#undef FIPS202_NAMESPACE
442441
#undef MLD_FIPS202_FIPS202_H
443442
#undef MLD_KECCAK_LANES
444443
#undef SHA3_256_HASHBYTES

mldsa/mldsa_native.c

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -435,7 +435,6 @@
435435
* Undefine macros from FIPS-202 files
436436
*/
437437
/* mldsa/src/fips202/fips202.h */
438-
#undef FIPS202_NAMESPACE
439438
#undef MLD_FIPS202_FIPS202_H
440439
#undef MLD_KECCAK_LANES
441440
#undef SHA3_256_HASHBYTES

mldsa/src/fips202/fips202.h

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

1213
#define SHAKE128_RATE 168
1314
#define SHAKE256_RATE 136
@@ -17,7 +18,6 @@
1718
#define SHA3_256_HASHBYTES 32
1819
#define SHA3_512_HASHBYTES 64
1920

20-
#define FIPS202_NAMESPACE(s) mldsa_fips202_ref_##s
2121

2222
typedef struct
2323
{
@@ -31,7 +31,7 @@ typedef struct
3131
unsigned int pos;
3232
} mld_shake256ctx;
3333

34-
#define mld_shake128_init FIPS202_NAMESPACE(shake128_init)
34+
#define mld_shake128_init MLD_NAMESPACE(shake128_init)
3535
/*************************************************
3636
* Name: mld_shake128_init
3737
*
@@ -46,7 +46,7 @@ __contract__(
4646
ensures(state->pos == 0)
4747
);
4848

49-
#define mld_shake128_absorb FIPS202_NAMESPACE(shake128_absorb)
49+
#define mld_shake128_absorb MLD_NAMESPACE(shake128_absorb)
5050
/*************************************************
5151
* Name: mld_shake128_absorb
5252
*
@@ -68,7 +68,7 @@ __contract__(
6868
ensures(state->pos <= SHAKE128_RATE)
6969
);
7070

71-
#define mld_shake128_finalize FIPS202_NAMESPACE(shake128_finalize)
71+
#define mld_shake128_finalize MLD_NAMESPACE(shake128_finalize)
7272
/*************************************************
7373
* Name: mld_shake128_finalize
7474
*
@@ -84,7 +84,7 @@ __contract__(
8484
ensures(state->pos <= SHAKE128_RATE)
8585
);
8686

87-
#define mld_shake128_squeeze FIPS202_NAMESPACE(shake128_squeeze)
87+
#define mld_shake128_squeeze MLD_NAMESPACE(shake128_squeeze)
8888
/*************************************************
8989
* Name: mld_shake128_squeeze
9090
*
@@ -107,7 +107,7 @@ __contract__(
107107
ensures(state->pos <= SHAKE128_RATE)
108108
);
109109

110-
#define mld_shake128_release FIPS202_NAMESPACE(shake128_release)
110+
#define mld_shake128_release MLD_NAMESPACE(shake128_release)
111111
/*************************************************
112112
* Name: mld_shake128_release
113113
*
@@ -121,7 +121,7 @@ __contract__(
121121
assigns(memory_slice(state, sizeof(mld_shake128ctx)))
122122
);
123123

124-
#define mld_shake256_init FIPS202_NAMESPACE(shake256_init)
124+
#define mld_shake256_init MLD_NAMESPACE(shake256_init)
125125
/*************************************************
126126
* Name: mld_shake256_init
127127
*
@@ -136,7 +136,7 @@ __contract__(
136136
ensures(state->pos == 0)
137137
);
138138

139-
#define mld_shake256_absorb FIPS202_NAMESPACE(shake256_absorb)
139+
#define mld_shake256_absorb MLD_NAMESPACE(shake256_absorb)
140140
/*************************************************
141141
* Name: mld_shake256_absorb
142142
*
@@ -158,7 +158,7 @@ __contract__(
158158
ensures(state->pos <= SHAKE256_RATE)
159159
);
160160

161-
#define mld_shake256_finalize FIPS202_NAMESPACE(shake256_finalize)
161+
#define mld_shake256_finalize MLD_NAMESPACE(shake256_finalize)
162162
/*************************************************
163163
* Name: mld_shake256_finalize
164164
*
@@ -174,7 +174,7 @@ __contract__(
174174
ensures(state->pos <= SHAKE256_RATE)
175175
);
176176

177-
#define mld_shake256_squeeze FIPS202_NAMESPACE(shake256_squeeze)
177+
#define mld_shake256_squeeze MLD_NAMESPACE(shake256_squeeze)
178178
/*************************************************
179179
* Name: mld_shake256_squeeze
180180
*
@@ -197,7 +197,7 @@ __contract__(
197197
ensures(state->pos <= SHAKE256_RATE)
198198
);
199199

200-
#define mld_shake256_release FIPS202_NAMESPACE(shake256_release)
200+
#define mld_shake256_release MLD_NAMESPACE(shake256_release)
201201
/*************************************************
202202
* Name: mld_shake256_release
203203
*
@@ -211,7 +211,7 @@ __contract__(
211211
assigns(memory_slice(state, sizeof(mld_shake256ctx)))
212212
);
213213

214-
#define mld_shake256 FIPS202_NAMESPACE(shake256)
214+
#define mld_shake256 MLD_NAMESPACE(shake256)
215215
/*************************************************
216216
* Name: mld_shake256
217217
*

mldsa/src/fips202/fips202x4.h

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ typedef struct
2626
uint64_t ctx[MLD_KECCAK_LANES * MLD_KECCAK_WAY];
2727
} mld_shake256x4ctx;
2828

29-
#define mld_shake128x4_absorb_once FIPS202_NAMESPACE(shake128x4_absorb_once)
29+
#define mld_shake128x4_absorb_once MLD_NAMESPACE(shake128x4_absorb_once)
3030
void mld_shake128x4_absorb_once(mld_shake128x4ctx *state, const uint8_t *in0,
3131
const uint8_t *in1, const uint8_t *in2,
3232
const uint8_t *in3, size_t inlen)
@@ -40,7 +40,7 @@ __contract__(
4040
assigns(object_whole(state))
4141
);
4242

43-
#define mld_shake128x4_squeezeblocks FIPS202_NAMESPACE(shake128x4_squeezeblocks)
43+
#define mld_shake128x4_squeezeblocks MLD_NAMESPACE(shake128x4_squeezeblocks)
4444
void mld_shake128x4_squeezeblocks(uint8_t *out0, uint8_t *out1, uint8_t *out2,
4545
uint8_t *out3, size_t nblocks,
4646
mld_shake128x4ctx *state)
@@ -58,14 +58,14 @@ __contract__(
5858
object_whole(state))
5959
);
6060

61-
#define mld_shake128x4_init FIPS202_NAMESPACE(shake128x4_init)
61+
#define mld_shake128x4_init MLD_NAMESPACE(shake128x4_init)
6262
void mld_shake128x4_init(mld_shake128x4ctx *state);
6363

64-
#define mld_shake128x4_release FIPS202_NAMESPACE(shake128x4_release)
64+
#define mld_shake128x4_release MLD_NAMESPACE(shake128x4_release)
6565
void mld_shake128x4_release(mld_shake128x4ctx *state);
6666

6767

68-
#define mld_shake256x4_absorb_once FIPS202_NAMESPACE(shake256x4_absorb_once)
68+
#define mld_shake256x4_absorb_once MLD_NAMESPACE(shake256x4_absorb_once)
6969
void mld_shake256x4_absorb_once(mld_shake256x4ctx *state, const uint8_t *in0,
7070
const uint8_t *in1, const uint8_t *in2,
7171
const uint8_t *in3, size_t inlen)
@@ -79,7 +79,7 @@ __contract__(
7979
assigns(object_whole(state))
8080
);
8181

82-
#define mld_shake256x4_squeezeblocks FIPS202_NAMESPACE(shake256x4_squeezeblocks)
82+
#define mld_shake256x4_squeezeblocks MLD_NAMESPACE(shake256x4_squeezeblocks)
8383
void mld_shake256x4_squeezeblocks(uint8_t *out0, uint8_t *out1, uint8_t *out2,
8484
uint8_t *out3, size_t nblocks,
8585
mld_shake256x4ctx *state)
@@ -97,10 +97,10 @@ __contract__(
9797
object_whole(state))
9898
);
9999

100-
#define mld_shake256x4_init FIPS202_NAMESPACE(shake256x4_init)
100+
#define mld_shake256x4_init MLD_NAMESPACE(shake256x4_init)
101101
void mld_shake256x4_init(mld_shake256x4ctx *state);
102102

103-
#define mld_shake256x4_release FIPS202_NAMESPACE(shake256x4_release)
103+
#define mld_shake256x4_release MLD_NAMESPACE(shake256x4_release)
104104
void mld_shake256x4_release(mld_shake256x4ctx *state);
105105

106106

mldsa/src/fips202/keccakf1600.h

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -20,8 +20,7 @@
2020
* The struct is only exposed here to allow its construction on the stack.
2121
*/
2222

23-
#define mld_keccakf1600_extract_bytes \
24-
FIPS202_NAMESPACE(keccakf1600_extract_bytes)
23+
#define mld_keccakf1600_extract_bytes MLD_NAMESPACE(keccakf1600_extract_bytes)
2524
void mld_keccakf1600_extract_bytes(uint64_t *state, unsigned char *data,
2625
unsigned offset, unsigned length)
2726
__contract__(
@@ -32,7 +31,7 @@ __contract__(
3231
assigns(memory_slice(data, length))
3332
);
3433

35-
#define mld_keccakf1600_xor_bytes FIPS202_NAMESPACE(keccakf1600_xor_bytes)
34+
#define mld_keccakf1600_xor_bytes MLD_NAMESPACE(keccakf1600_xor_bytes)
3635
void mld_keccakf1600_xor_bytes(uint64_t *state, const unsigned char *data,
3736
unsigned offset, unsigned length)
3837
__contract__(
@@ -44,7 +43,7 @@ __contract__(
4443
);
4544

4645
#define mld_keccakf1600x4_extract_bytes \
47-
FIPS202_NAMESPACE(keccakf1600x4_extract_bytes)
46+
MLD_NAMESPACE(keccakf1600x4_extract_bytes)
4847
void mld_keccakf1600x4_extract_bytes(uint64_t *state, unsigned char *data0,
4948
unsigned char *data1, unsigned char *data2,
5049
unsigned char *data3, unsigned offset,
@@ -63,7 +62,7 @@ __contract__(
6362
assigns(memory_slice(data3, length))
6463
);
6564

66-
#define mld_keccakf1600x4_xor_bytes FIPS202_NAMESPACE(keccakf1600x4_xor_bytes)
65+
#define mld_keccakf1600x4_xor_bytes MLD_NAMESPACE(keccakf1600x4_xor_bytes)
6766
void mld_keccakf1600x4_xor_bytes(uint64_t *state, const unsigned char *data0,
6867
const unsigned char *data1,
6968
const unsigned char *data2,
@@ -84,14 +83,14 @@ __contract__(
8483
assigns(memory_slice(state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY))
8584
);
8685

87-
#define mld_keccakf1600x4_permute FIPS202_NAMESPACE(keccakf1600x4_permute)
86+
#define mld_keccakf1600x4_permute MLD_NAMESPACE(keccakf1600x4_permute)
8887
void mld_keccakf1600x4_permute(uint64_t *state)
8988
__contract__(
9089
requires(memory_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY))
9190
assigns(memory_slice(state, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY))
9291
);
9392

94-
#define mld_keccakf1600_permute FIPS202_NAMESPACE(keccakf1600_permute)
93+
#define mld_keccakf1600_permute MLD_NAMESPACE(keccakf1600_permute)
9594
void mld_keccakf1600_permute(uint64_t *state)
9695
__contract__(
9796
requires(memory_no_alias(state, sizeof(uint64_t) * MLD_KECCAK_LANES))

proofs/cbmc/H/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/src/sign.c
2121

2222
CHECK_FUNCTION_CONTRACTS=mld_H
23-
USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256_init $(FIPS202_NAMESPACE)shake256_absorb $(FIPS202_NAMESPACE)shake256_squeeze $(FIPS202_NAMESPACE)shake256_finalize $(FIPS202_NAMESPACE)shake256_release
23+
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)shake256_init $(MLD_NAMESPACE)shake256_absorb $(MLD_NAMESPACE)shake256_squeeze $(MLD_NAMESPACE)shake256_finalize $(MLD_NAMESPACE)shake256_release
2424
APPLY_LOOP_CONTRACTS=on
2525
USE_DYNAMIC_FRAMES=1
2626

proofs/cbmc/Makefile_params.common

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,6 @@ ifndef MLD_CONFIG_PARAMETER_SET
66
endif
77

88
MLD_CONFIG_PARAMETER_SET ?= 65
9-
FIPS202_NAMESPACE = mldsa_fips202_ref_
109

1110
ifeq ($(MLD_CONFIG_PARAMETER_SET),44)
1211
MLD_NAMESPACE_KL=PQCP_MLDSA_NATIVE_MLDSA44_

proofs/cbmc/crypto_sign_keypair_internal/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/src/sign.c
2121

2222
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)keypair_internal
23-
USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256
23+
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)shake256
2424
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvec_matrix_expand
2525
USE_FUNCTION_CONTRACTS+=mld_sample_s1_s2
2626
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvecl_ntt

proofs/cbmc/crypto_sign_signature_pre_hash_shake256/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/src/sign.c
2121

2222
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)signature_pre_hash_shake256
23-
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)signature_pre_hash_internal $(FIPS202_NAMESPACE)shake256
23+
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)signature_pre_hash_internal $(MLD_NAMESPACE)shake256
2424

2525
APPLY_LOOP_CONTRACTS=on
2626
USE_DYNAMIC_FRAMES=1

proofs/cbmc/crypto_sign_verify_pre_hash_shake256/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/src/sign.c
2121

2222
CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_pre_hash_shake256
23-
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_pre_hash_internal $(FIPS202_NAMESPACE)shake256
23+
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_pre_hash_internal $(MLD_NAMESPACE)shake256
2424

2525
APPLY_LOOP_CONTRACTS=on
2626
USE_DYNAMIC_FRAMES=1

0 commit comments

Comments
 (0)