Skip to content

Commit ac76991

Browse files
f15hrmkannwischer
f15hr
authored and
mkannwischer
committed
CBMC: Remove namespacing
Signed-off-by: Liam Fisher <[email protected]>
1 parent d7cb842 commit ac76991

File tree

139 files changed

+1073
-286
lines changed

Some content is hidden

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

139 files changed

+1073
-286
lines changed

‎BIBLIOGRAPHY.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,7 @@ source code and documentation.
3939
- [integration/liboqs/config_x86_64.h](integration/liboqs/config_x86_64.h)
4040
- [mldsa/mldsa_native_config.h](mldsa/mldsa_native_config.h)
4141
- [mldsa/src/sign.c](mldsa/src/sign.c)
42+
- [proofs/cbmc/mldsa_native_config_cbmc.h](proofs/cbmc/mldsa_native_config_cbmc.h)
4243
- [test/configs/break_pct_config.h](test/configs/break_pct_config.h)
4344
- [test/configs/custom_heap_alloc_config.h](test/configs/custom_heap_alloc_config.h)
4445
- [test/configs/custom_memcpy_config.h](test/configs/custom_memcpy_config.h)
@@ -94,6 +95,7 @@ source code and documentation.
9495
- [mldsa/src/rounding.h](mldsa/src/rounding.h)
9596
- [mldsa/src/sign.c](mldsa/src/sign.c)
9697
- [mldsa/src/sign.h](mldsa/src/sign.h)
98+
- [proofs/cbmc/mldsa_native_config_cbmc.h](proofs/cbmc/mldsa_native_config_cbmc.h)
9799
- [test/configs/break_pct_config.h](test/configs/break_pct_config.h)
98100
- [test/configs/custom_memcpy_config.h](test/configs/custom_memcpy_config.h)
99101
- [test/configs/custom_memset_config.h](test/configs/custom_memset_config.h)

‎proofs/cbmc/H/Makefile‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,11 @@ 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=$(MLD_NAMESPACE)shake256_init $(MLD_NAMESPACE)shake256_absorb $(MLD_NAMESPACE)shake256_squeeze $(MLD_NAMESPACE)shake256_finalize $(MLD_NAMESPACE)shake256_release
23+
USE_FUNCTION_CONTRACTS=mld_shake256_init
24+
USE_FUNCTION_CONTRACTS+=mld_shake256_absorb
25+
USE_FUNCTION_CONTRACTS+=mld_shake256_squeeze
26+
USE_FUNCTION_CONTRACTS+=mld_shake256_finalize
27+
USE_FUNCTION_CONTRACTS+=mld_shake256_release
2428
APPLY_LOOP_CONTRACTS=on
2529
USE_DYNAMIC_FRAMES=1
2630

‎proofs/cbmc/Makefile.common‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -555,6 +555,7 @@ ifndef MLD_CONFIG_PARAMETER_SET
555555
$(error MLD_CONFIG_PARAMETER_SET not set)
556556
endif
557557

558+
DEFINES += -DMLD_CONFIG_FILE="\"mldsa_native_config_cbmc.h\""
558559
DEFINES += -DMLD_CONFIG_PARAMETER_SET=$(MLD_CONFIG_PARAMETER_SET)
559560
# Give visibility to all static functions
560561
DEFINES += -Dstatic=

‎proofs/cbmc/Makefile_params.common‎

Lines changed: 0 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -6,16 +6,3 @@ ifndef MLD_CONFIG_PARAMETER_SET
66
endif
77

88
MLD_CONFIG_PARAMETER_SET ?= 65
9-
10-
ifeq ($(MLD_CONFIG_PARAMETER_SET),44)
11-
MLD_NAMESPACE_KL=PQCP_MLDSA_NATIVE_MLDSA44_
12-
MLD_NAMESPACE=PQCP_MLDSA_NATIVE_MLDSA44_
13-
else ifeq ($(MLD_CONFIG_PARAMETER_SET),65)
14-
MLD_NAMESPACE_KL=PQCP_MLDSA_NATIVE_MLDSA65_
15-
MLD_NAMESPACE=PQCP_MLDSA_NATIVE_MLDSA65_
16-
else ifeq ($(MLD_CONFIG_PARAMETER_SET),87)
17-
MLD_NAMESPACE_KL=PQCP_MLDSA_NATIVE_MLDSA87_
18-
MLD_NAMESPACE=PQCP_MLDSA_NATIVE_MLDSA87_
19-
else
20-
$(error Invalid value of MLD_CONFIG_PARAMETER_SET)
21-
endif

‎proofs/cbmc/attempt_signature_generation/Makefile‎

Lines changed: 19 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -20,25 +20,25 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
2020
PROJECT_SOURCES += $(SRCDIR)/mldsa/src/sign.c
2121

2222
CHECK_FUNCTION_CONTRACTS=mld_attempt_signature_generation
23-
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_uniform_gamma1 \
24-
$(MLD_NAMESPACE)polyvecl_ntt \
25-
$(MLD_NAMESPACE)polyvec_matrix_pointwise_montgomery \
26-
$(MLD_NAMESPACE)polyveck_reduce \
27-
$(MLD_NAMESPACE)polyveck_invntt_tomont \
28-
$(MLD_NAMESPACE)polyveck_caddq \
29-
$(MLD_NAMESPACE)polyveck_decompose \
30-
$(MLD_NAMESPACE)polyveck_pack_w1 \
31-
mld_H \
32-
$(MLD_NAMESPACE)poly_challenge \
33-
$(MLD_NAMESPACE)poly_ntt \
34-
$(MLD_NAMESPACE)polyveck_pointwise_poly_montgomery \
35-
$(MLD_NAMESPACE)polyveck_sub \
36-
$(MLD_NAMESPACE)polyveck_reduce \
37-
$(MLD_NAMESPACE)polyveck_chknorm \
38-
$(MLD_NAMESPACE)polyveck_add \
39-
$(MLD_NAMESPACE)polyveck_make_hint \
40-
$(MLD_NAMESPACE)pack_sig_c_h \
41-
mld_compute_pack_z
23+
USE_FUNCTION_CONTRACTS=mld_polyvecl_uniform_gamma1
24+
USE_FUNCTION_CONTRACTS+=mld_polyvecl_ntt
25+
USE_FUNCTION_CONTRACTS+=mld_polyvec_matrix_pointwise_montgomery
26+
USE_FUNCTION_CONTRACTS+=mld_polyveck_reduce
27+
USE_FUNCTION_CONTRACTS+=mld_polyveck_invntt_tomont
28+
USE_FUNCTION_CONTRACTS+=mld_polyveck_caddq
29+
USE_FUNCTION_CONTRACTS+=mld_polyveck_decompose
30+
USE_FUNCTION_CONTRACTS+=mld_polyveck_pack_w1
31+
USE_FUNCTION_CONTRACTS+=mld_H
32+
USE_FUNCTION_CONTRACTS+=mld_poly_challenge
33+
USE_FUNCTION_CONTRACTS+=mld_poly_ntt
34+
USE_FUNCTION_CONTRACTS+=mld_polyveck_pointwise_poly_montgomery
35+
USE_FUNCTION_CONTRACTS+=mld_polyveck_sub
36+
USE_FUNCTION_CONTRACTS+=mld_polyveck_reduce
37+
USE_FUNCTION_CONTRACTS+=mld_polyveck_chknorm
38+
USE_FUNCTION_CONTRACTS+=mld_polyveck_add
39+
USE_FUNCTION_CONTRACTS+=mld_polyveck_make_hint
40+
USE_FUNCTION_CONTRACTS+=mld_pack_sig_c_h
41+
USE_FUNCTION_CONTRACTS+=mld_compute_pack_z
4242
USE_FUNCTION_CONTRACTS+=mld_zeroize
4343

4444
APPLY_LOOP_CONTRACTS=on

‎proofs/cbmc/caddq/Makefile‎

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

2222
CHECK_FUNCTION_CONTRACTS=mld_caddq
23-
USE_FUNCTION_CONTRACTS=mld_ct_sel_int32 mld_ct_cmask_neg_i32
23+
USE_FUNCTION_CONTRACTS=mld_ct_sel_int32
24+
USE_FUNCTION_CONTRACTS+=mld_ct_cmask_neg_i32
2425
APPLY_LOOP_CONTRACTS=on
2526
USE_DYNAMIC_FRAMES=1
2627

‎proofs/cbmc/check_pct/Makefile‎

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

2222
CHECK_FUNCTION_CONTRACTS=mld_check_pct
23-
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)signature $(MLD_NAMESPACE)verify
23+
USE_FUNCTION_CONTRACTS=mld_signature
24+
USE_FUNCTION_CONTRACTS+=mld_verify
2425
USE_FUNCTION_CONTRACTS+=mld_zeroize
2526
APPLY_LOOP_CONTRACTS=on
2627
USE_DYNAMIC_FRAMES=1

‎proofs/cbmc/compute_pack_z/Makefile‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -20,12 +20,12 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
2020
PROJECT_SOURCES += $(SRCDIR)/mldsa/src/sign.c
2121

2222
CHECK_FUNCTION_CONTRACTS=mld_compute_pack_z
23-
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_pointwise_montgomery \
24-
$(MLD_NAMESPACE)poly_invntt_tomont \
25-
$(MLD_NAMESPACE)poly_add \
26-
$(MLD_NAMESPACE)poly_reduce \
27-
$(MLD_NAMESPACE)poly_chknorm \
28-
$(MLD_NAMESPACE)pack_sig_z
23+
USE_FUNCTION_CONTRACTS=mld_poly_pointwise_montgomery
24+
USE_FUNCTION_CONTRACTS+=mld_poly_invntt_tomont
25+
USE_FUNCTION_CONTRACTS+=mld_poly_add
26+
USE_FUNCTION_CONTRACTS+=mld_poly_reduce
27+
USE_FUNCTION_CONTRACTS+=mld_poly_chknorm
28+
USE_FUNCTION_CONTRACTS+=mld_pack_sig_z
2929
USE_FUNCTION_CONTRACTS+=mld_zeroize
3030

3131
APPLY_LOOP_CONTRACTS=on

‎proofs/cbmc/compute_t0_t1_tr_from_sk_components/Makefile‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -20,16 +20,16 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
2020
PROJECT_SOURCES += $(SRCDIR)/mldsa/src/sign.c
2121

2222
CHECK_FUNCTION_CONTRACTS=mld_compute_t0_t1_tr_from_sk_components
23-
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)shake256
24-
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvec_matrix_expand
25-
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvecl_ntt
26-
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyvec_matrix_pointwise_montgomery
27-
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_reduce
28-
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_invntt_tomont
29-
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_add
30-
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_caddq
31-
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_power2round
32-
USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)pack_pk
23+
USE_FUNCTION_CONTRACTS=mld_shake256
24+
USE_FUNCTION_CONTRACTS+=mld_polyvec_matrix_expand
25+
USE_FUNCTION_CONTRACTS+=mld_polyvecl_ntt
26+
USE_FUNCTION_CONTRACTS+=mld_polyvec_matrix_pointwise_montgomery
27+
USE_FUNCTION_CONTRACTS+=mld_polyveck_reduce
28+
USE_FUNCTION_CONTRACTS+=mld_polyveck_invntt_tomont
29+
USE_FUNCTION_CONTRACTS+=mld_polyveck_add
30+
USE_FUNCTION_CONTRACTS+=mld_polyveck_caddq
31+
USE_FUNCTION_CONTRACTS+=mld_polyveck_power2round
32+
USE_FUNCTION_CONTRACTS+=mld_pack_pk
3333
USE_FUNCTION_CONTRACTS+=mld_zeroize
3434

3535
APPLY_LOOP_CONTRACTS=on

‎proofs/cbmc/ct_abs_i32/Makefile‎

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

2222
CHECK_FUNCTION_CONTRACTS=mld_ct_abs_i32
23-
USE_FUNCTION_CONTRACTS=mld_ct_sel_int32 mld_ct_cmask_neg_i32
23+
USE_FUNCTION_CONTRACTS=mld_ct_sel_int32
24+
USE_FUNCTION_CONTRACTS+=mld_ct_cmask_neg_i32
2425
APPLY_LOOP_CONTRACTS=on
2526
USE_DYNAMIC_FRAMES=1
2627

0 commit comments

Comments
 (0)