Correct proof Makefiles and harnesses for dir structure and name-spaceing.

Signed-off-by: Rod Chapman <[email protected]>

Author: rod-chapman

proofs/cbmc/pointwise_sum_of_products/Makefile

@@ -17,9 +17,9 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c
 
-CHECK_FUNCTION_CONTRACTS=mld_pointwise_sum_of_products
+CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)mld_pointwise_sum_of_products
 USE_FUNCTION_CONTRACTS=
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1

proofs/cbmc/pointwise_sum_of_products/pointwise_sum_of_products_harness.c

@@ -3,6 +3,8 @@
 
 #include "polyvec.h"
 
+#define mld_pointwise_sum_of_products \
+  MLD_NAMESPACE_KL(mld_pointwise_sum_of_products)
 int64_t mld_pointwise_sum_of_products(const mld_polyvecl *u,
                                       const mld_polyvecl *v, unsigned int i);
 

proofs/cbmc/poly_uniform_eta/Makefile

@@ -17,15 +17,15 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROJECT_SOURCES += $(SRCDIR)/mldsa/poly_kl.c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform_eta
 USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256_init
 USE_FUNCTION_CONTRACTS+=$(FIPS202_NAMESPACE)shake256_absorb
 USE_FUNCTION_CONTRACTS+=$(FIPS202_NAMESPACE)shake256_finalize
 USE_FUNCTION_CONTRACTS+=$(FIPS202_NAMESPACE)shake256_squeeze
 USE_FUNCTION_CONTRACTS+=mld_rej_eta
-USE_FUNCTION_CONTRACTS+=$(FIPS202_NAMESPACE)shake256_release 
+USE_FUNCTION_CONTRACTS+=$(FIPS202_NAMESPACE)shake256_release
 USE_FUNCTION_CONTRACTS+=mld_zeroize
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1

proofs/cbmc/poly_uniform_eta/poly_uniform_eta_harness.c

@@ -1,7 +1,7 @@
 // Copyright (c) The mldsa-native project authors
 // SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 
-#include "poly.h"
+#include "poly_kl.h"
 
 void harness(void)
 {

proofs/cbmc/polyvec_matrix_expand_serial/Makefile

@@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvec_matrix_expand
 USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform

proofs/cbmc/polyveck_add_error/Makefile

@@ -17,7 +17,7 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyveck_add_error
 USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_add

proofs/cbmc/polyvecl_pointwise_acc_montgomery/Makefile

@@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_pointwise_acc_montgomery
-USE_FUNCTION_CONTRACTS=mld_montgomery_reduce mld_pointwise_sum_of_products
+USE_FUNCTION_CONTRACTS=mld_montgomery_reduce $(MLD_NAMESPACE)mld_pointwise_sum_of_products
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 

proofs/cbmc/polyvecl_uniform_gamma1_serial/Makefile

@@ -18,7 +18,7 @@ REMOVE_FUNCTION_BODY +=
 UNWINDSET += $(MLD_NAMESPACE)polyvecl_uniform_gamma1.0:7 # Largest value of MLDSA_L
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROJECT_SOURCES += $(SRCDIR)/mldsa/polyvec.c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/polyvec.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)polyvecl_uniform_gamma1
 USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform_gamma1

proofs/cbmc/sample_s1_s2_serial/Makefile

@@ -18,7 +18,7 @@ UNWINDSET += mld_sample_s1_s2.0:7 # Largest value of MLDSA_L
 UNWINDSET += mld_sample_s1_s2.1:8 # Largest value of MLDSA_K
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/sign.c
 
 CHECK_FUNCTION_CONTRACTS=mld_sample_s1_s2
 USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_uniform_eta