Skip to content

Commit 3026327

Browse files
committed
CBMC: Correct called contracts in verify_pre_hash_internal
For some reason the previous (unrelated) commit caused the verify_pre_hash_internal proof to fail due to extra functions in USE_FUNCTION_CONTRACTS. This commit removes the extra functions. Signed-off-by: Matthias J. Kannwischer <[email protected]>
1 parent 0d691ad commit 3026327

File tree

1 file changed

+1
-8
lines changed
  • proofs/cbmc/crypto_sign_verify_pre_hash_internal

1 file changed

+1
-8
lines changed

proofs/cbmc/crypto_sign_verify_pre_hash_internal/Makefile

Lines changed: 1 addition & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -20,14 +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_internal
23-
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_internal \
24-
$(MLD_NAMESPACE)unpack_pk \
25-
$(MLD_NAMESPACE)unpack_sig \
26-
$(MLD_NAMESPACE)polyvec_matrix_expand \
27-
$(MLD_NAMESPACE)polyvecl_invntt_tomont \
28-
$(MLD_NAMESPACE)polyveck_invntt_tomont \
29-
$(MLD_NAMESPACE)polyveck_sub \
30-
$(MLD_NAMESPACE)polyveck_use_hint
23+
USE_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)verify_internal
3124
USE_FUNCTION_CONTRACTS+=mld_zeroize
3225

3326
APPLY_LOOP_CONTRACTS=on

0 commit comments

Comments
 (0)