Skip to content

Commit

Permalink
Merge pull request #522 from pq-code-package/cbmc_custom_order
Browse files Browse the repository at this point in the history 
CBMC: Add custom reordering loop into CBMC scope
  • Loading branch information
@hanno-becker
hanno-becker authored Dec 13, 2024
2 parents 440e7b0 + 8e72c85 commit e3fa106
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 5 deletions.
6 changes: 3 additions & 3 deletions cbmc/proofs/gen_matrix/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,13 +13,13 @@ DEFINES +=
INCLUDES +=

REMOVE_FUNCTION_BODY +=
UNWINDSET += $(MLKEM_NAMESPACE)gen_matrix.0:4 $(MLKEM_NAMESPACE)gen_matrix.1:4 $(MLKEM_NAMESPACE)gen_matrix.2:4
UNWINDSET += $(MLKEM_NAMESPACE)gen_matrix.0:4 $(MLKEM_NAMESPACE)gen_matrix.1:4 $(MLKEM_NAMESPACE)gen_matrix.2:4 $(MLKEM_NAMESPACE)gen_matrix.3:4 $(MLKEM_NAMESPACE)gen_matrix.4:4

PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROJECT_SOURCES += $(SRCDIR)/mlkem/indcpa.c

CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)gen_matrix
USE_FUNCTION_CONTRACTS=gen_matrix_entry gen_matrix_entry_x4
USE_FUNCTION_CONTRACTS=gen_matrix_entry gen_matrix_entry_x4 poly_permute_bitrev_to_custom
APPLY_LOOP_CONTRACTS=on
USE_DYNAMIC_FRAMES=1

Expand All @@ -36,7 +36,7 @@ FUNCTION_NAME = $(MLKEM_NAMESPACE)gen_matrix
# EXPENSIVE = true

# This function is large enough to need...
CBMC_OBJECT_BITS = 8
CBMC_OBJECT_BITS = 10

# If you require access to a file-local ("static") function or object to conduct
# your proof, set the following (and do not include the original source file
Expand Down
13 changes: 11 additions & 2 deletions mlkem/indcpa.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -250,6 +250,17 @@ __contract__(
xof_release(&state);
}

#if !defined(MLKEM_USE_NATIVE_NTT_CUSTOM_ORDER)
STATIC_INLINE_TESTABLE
void poly_permute_bitrev_to_custom(poly *data)
__contract__(
/* We don't specify that this should be a permutation, but only
* that it does not change the bound established at the end of gen_matrix. */
requires(memory_no_alias(data, sizeof(poly)))
requires(array_bound(data->coeffs, 0, MLKEM_N - 1, 0, MLKEM_Q - 1))
assigns(memory_slice(data, sizeof(poly)))
ensures(array_bound(data->coeffs, 0, MLKEM_N - 1, 0, MLKEM_Q - 1))) { ((void)data); }
#endif /* MLKEM_USE_NATIVE_NTT_CUSTOM_ORDER */

/* Not static for benchmarking */
void gen_matrix(polyvec *a, const uint8_t seed[MLKEM_SYMBYTES], int transposed)
Expand Down Expand Up @@ -330,7 +341,6 @@ void gen_matrix(polyvec *a, const uint8_t seed[MLKEM_SYMBYTES], int transposed)
cassert(i == MLKEM_K * MLKEM_K,
"gen_matrix: failed to generate whole matrix");

#if defined(MLKEM_USE_NATIVE_NTT_CUSTOM_ORDER)
/*
* The public matrix is generated in NTT domain. If the native backend
* uses a custom order in NTT domain, permute A accordingly.
Expand All @@ -342,7 +352,6 @@ void gen_matrix(polyvec *a, const uint8_t seed[MLKEM_SYMBYTES], int transposed)
poly_permute_bitrev_to_custom(&a[i].vec[j]);
}
}
#endif /* MLKEM_USE_NATIVE_NTT_CUSTOM_ORDER */
}

/*************************************************
Expand Down

18 comments on commit e3fa106

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Arm Cortex-A76 (Raspberry Pi 5) benchmarks

Benchmark suite Current: e3fa106 Previous: 440e7b0 Ratio
ML-KEM-512 keypair 29185 cycles 29185 cycles 1
ML-KEM-512 encaps 35550 cycles 35559 cycles 1.00
ML-KEM-512 decaps 46096 cycles 46103 cycles 1.00
ML-KEM-768 keypair 49233 cycles 49233 cycles 1
ML-KEM-768 encaps 55388 cycles 55387 cycles 1.00
ML-KEM-768 decaps 70237 cycles 70234 cycles 1.00
ML-KEM-1024 keypair 72230 cycles 72224 cycles 1.00
ML-KEM-1024 encaps 81141 cycles 81138 cycles 1.00
ML-KEM-1024 decaps 100875 cycles 100873 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Intel Xeon 4th gen (c7i)

Benchmark suite Current: e3fa106 Previous: 440e7b0 Ratio
ML-KEM-512 keypair 13512 cycles 13510 cycles 1.00
ML-KEM-512 encaps 17301 cycles 17493 cycles 0.99
ML-KEM-512 decaps 22817 cycles 22800 cycles 1.00
ML-KEM-768 keypair 22532 cycles 22518 cycles 1.00
ML-KEM-768 encaps 24473 cycles 24483 cycles 1.00
ML-KEM-768 decaps 32630 cycles 32498 cycles 1.00
ML-KEM-1024 keypair 31462 cycles 31363 cycles 1.00
ML-KEM-1024 encaps 34979 cycles 34901 cycles 1.00
ML-KEM-1024 decaps 45821 cycles 45693 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

AMD EPYC 3rd gen (c6a)

Benchmark suite Current: e3fa106 Previous: 440e7b0 Ratio
ML-KEM-512 keypair 18132 cycles 18127 cycles 1.00
ML-KEM-512 encaps 23180 cycles 23196 cycles 1.00
ML-KEM-512 decaps 30506 cycles 30512 cycles 1.00
ML-KEM-768 keypair 31075 cycles 31103 cycles 1.00
ML-KEM-768 encaps 34160 cycles 34231 cycles 1.00
ML-KEM-768 decaps 44728 cycles 44840 cycles 1.00
ML-KEM-1024 keypair 44641 cycles 44596 cycles 1.00
ML-KEM-1024 encaps 49913 cycles 50021 cycles 1.00
ML-KEM-1024 decaps 64361 cycles 64457 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

AMD EPYC 4th gen (c7a)

Benchmark suite Current: e3fa106 Previous: 440e7b0 Ratio
ML-KEM-512 keypair 15080 cycles 15070 cycles 1.00
ML-KEM-512 encaps 19671 cycles 19652 cycles 1.00
ML-KEM-512 decaps 26309 cycles 26305 cycles 1.00
ML-KEM-768 keypair 25619 cycles 25611 cycles 1.00
ML-KEM-768 encaps 28169 cycles 28165 cycles 1.00
ML-KEM-768 decaps 37849 cycles 37858 cycles 1.00
ML-KEM-1024 keypair 35611 cycles 35696 cycles 1.00
ML-KEM-1024 encaps 40962 cycles 40972 cycles 1.00
ML-KEM-1024 decaps 54509 cycles 54502 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Intel Xeon 3rd gen (c6i)

Benchmark suite Current: e3fa106 Previous: 440e7b0 Ratio
ML-KEM-512 keypair 20325 cycles 20326 cycles 1.00
ML-KEM-512 encaps 26995 cycles 27019 cycles 1.00
ML-KEM-512 decaps 35812 cycles 35841 cycles 1.00
ML-KEM-768 keypair 34899 cycles 34895 cycles 1.00
ML-KEM-768 encaps 38185 cycles 38183 cycles 1.00
ML-KEM-768 decaps 50917 cycles 50912 cycles 1.00
ML-KEM-1024 keypair 47948 cycles 47950 cycles 1.00
ML-KEM-1024 encaps 54101 cycles 54118 cycles 1.00
ML-KEM-1024 decaps 71680 cycles 71700 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Intel Xeon 4th gen (c7i) (no-opt)

Benchmark suite Current: e3fa106 Previous: 440e7b0 Ratio
ML-KEM-512 keypair 34839 cycles 34826 cycles 1.00
ML-KEM-512 encaps 44977 cycles 45050 cycles 1.00
ML-KEM-512 decaps 58856 cycles 58955 cycles 1.00
ML-KEM-768 keypair 59143 cycles 59210 cycles 1.00
ML-KEM-768 encaps 71798 cycles 71850 cycles 1.00
ML-KEM-768 decaps 89222 cycles 89401 cycles 1.00
ML-KEM-1024 keypair 87543 cycles 87585 cycles 1.00
ML-KEM-1024 encaps 104656 cycles 104666 cycles 1.00
ML-KEM-1024 decaps 127605 cycles 127661 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graviton3

Benchmark suite Current: e3fa106 Previous: 440e7b0 Ratio
ML-KEM-512 keypair 18992 cycles 18992 cycles 1
ML-KEM-512 encaps 23578 cycles 23578 cycles 1
ML-KEM-512 decaps 30753 cycles 30756 cycles 1.00
ML-KEM-768 keypair 32242 cycles 32251 cycles 1.00
ML-KEM-768 encaps 35717 cycles 35713 cycles 1.00
ML-KEM-768 decaps 45885 cycles 45888 cycles 1.00
ML-KEM-1024 keypair 46845 cycles 46846 cycles 1.00
ML-KEM-1024 encaps 52631 cycles 52630 cycles 1.00
ML-KEM-1024 decaps 66483 cycles 66483 cycles 1

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graviton4

Benchmark suite Current: e3fa106 Previous: 440e7b0 Ratio
ML-KEM-512 keypair 18199 cycles 18204 cycles 1.00
ML-KEM-512 encaps 22234 cycles 22234 cycles 1
ML-KEM-512 decaps 28992 cycles 28991 cycles 1.00
ML-KEM-768 keypair 30683 cycles 30681 cycles 1.00
ML-KEM-768 encaps 33732 cycles 33737 cycles 1.00
ML-KEM-768 decaps 43312 cycles 43314 cycles 1.00
ML-KEM-1024 keypair 44368 cycles 44369 cycles 1.00
ML-KEM-1024 encaps 49789 cycles 49790 cycles 1.00
ML-KEM-1024 decaps 62847 cycles 62857 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Arm Cortex-A55 (Snapdragon 888) benchmarks

Benchmark suite Current: e3fa106 Previous: e7721c6 Ratio
ML-KEM-512 keypair 57894 cycles 57912 cycles 1.00
ML-KEM-512 encaps 65189 cycles 65405 cycles 1.00
ML-KEM-512 decaps 83747 cycles 83799 cycles 1.00
ML-KEM-768 keypair 98166 cycles 98061 cycles 1.00
ML-KEM-768 encaps 109235 cycles 109994 cycles 0.99
ML-KEM-768 decaps 135575 cycles 135640 cycles 1.00
ML-KEM-1024 keypair 148737 cycles 149124 cycles 1.00
ML-KEM-1024 encaps 164910 cycles 165109 cycles 1.00
ML-KEM-1024 decaps 200052 cycles 201025 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

AMD EPYC 4th gen (c7a) (no-opt)

Benchmark suite Current: e3fa106 Previous: 440e7b0 Ratio
ML-KEM-512 keypair 45729 cycles 45727 cycles 1.00
ML-KEM-512 encaps 56869 cycles 56864 cycles 1.00
ML-KEM-512 decaps 76267 cycles 76245 cycles 1.00
ML-KEM-768 keypair 74519 cycles 74538 cycles 1.00
ML-KEM-768 encaps 88597 cycles 88639 cycles 1.00
ML-KEM-768 decaps 114415 cycles 114404 cycles 1.00
ML-KEM-1024 keypair 109402 cycles 109385 cycles 1.00
ML-KEM-1024 encaps 127250 cycles 127274 cycles 1.00
ML-KEM-1024 decaps 159963 cycles 159967 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

AMD EPYC 3rd gen (c6a) (no-opt)

Benchmark suite Current: e3fa106 Previous: 440e7b0 Ratio
ML-KEM-512 keypair 52167 cycles 52177 cycles 1.00
ML-KEM-512 encaps 65779 cycles 65780 cycles 1.00
ML-KEM-512 decaps 88379 cycles 88380 cycles 1.00
ML-KEM-768 keypair 84807 cycles 84766 cycles 1.00
ML-KEM-768 encaps 101826 cycles 101459 cycles 1.00
ML-KEM-768 decaps 132072 cycles 132087 cycles 1.00
ML-KEM-1024 keypair 124443 cycles 124204 cycles 1.00
ML-KEM-1024 encaps 145779 cycles 145970 cycles 1.00
ML-KEM-1024 decaps 183760 cycles 183995 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Intel Xeon 3rd gen (c6i) (no-opt)

Benchmark suite Current: e3fa106 Previous: 440e7b0 Ratio
ML-KEM-512 keypair 56575 cycles 56558 cycles 1.00
ML-KEM-512 encaps 69439 cycles 69474 cycles 1.00
ML-KEM-512 decaps 91359 cycles 91366 cycles 1.00
ML-KEM-768 keypair 91839 cycles 91880 cycles 1.00
ML-KEM-768 encaps 107800 cycles 107832 cycles 1.00
ML-KEM-768 decaps 136349 cycles 136375 cycles 1.00
ML-KEM-1024 keypair 134753 cycles 134838 cycles 1.00
ML-KEM-1024 encaps 155231 cycles 155280 cycles 1.00
ML-KEM-1024 decaps 191530 cycles 191743 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graviton2

Benchmark suite Current: e3fa106 Previous: 440e7b0 Ratio
ML-KEM-512 keypair 29194 cycles 29196 cycles 1.00
ML-KEM-512 encaps 35566 cycles 35568 cycles 1.00
ML-KEM-512 decaps 46110 cycles 46112 cycles 1.00
ML-KEM-768 keypair 49246 cycles 49232 cycles 1.00
ML-KEM-768 encaps 55426 cycles 55401 cycles 1.00
ML-KEM-768 decaps 70242 cycles 70219 cycles 1.00
ML-KEM-1024 keypair 72348 cycles 72357 cycles 1.00
ML-KEM-1024 encaps 81167 cycles 81164 cycles 1.00
ML-KEM-1024 decaps 100837 cycles 100836 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graviton4 (no-opt)

Benchmark suite Current: e3fa106 Previous: 440e7b0 Ratio
ML-KEM-512 keypair 41990 cycles 41947 cycles 1.00
ML-KEM-512 encaps 50164 cycles 50164 cycles 1
ML-KEM-512 decaps 66051 cycles 66050 cycles 1.00
ML-KEM-768 keypair 69061 cycles 69049 cycles 1.00
ML-KEM-768 encaps 79765 cycles 79761 cycles 1.00
ML-KEM-768 decaps 101020 cycles 101015 cycles 1.00
ML-KEM-1024 keypair 102210 cycles 102226 cycles 1.00
ML-KEM-1024 encaps 117192 cycles 117206 cycles 1.00
ML-KEM-1024 decaps 143733 cycles 143688 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graviton3 (no-opt)

Benchmark suite Current: e3fa106 Previous: 440e7b0 Ratio
ML-KEM-512 keypair 45389 cycles 45389 cycles 1
ML-KEM-512 encaps 54218 cycles 54216 cycles 1.00
ML-KEM-512 decaps 71153 cycles 71147 cycles 1.00
ML-KEM-768 keypair 74830 cycles 74831 cycles 1.00
ML-KEM-768 encaps 86068 cycles 86063 cycles 1.00
ML-KEM-768 decaps 108813 cycles 108812 cycles 1.00
ML-KEM-1024 keypair 111115 cycles 111133 cycles 1.00
ML-KEM-1024 encaps 125941 cycles 125936 cycles 1.00
ML-KEM-1024 decaps 154648 cycles 154627 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graviton2 (no-opt)

Benchmark suite Current: e3fa106 Previous: 440e7b0 Ratio
ML-KEM-512 keypair 71257 cycles 71260 cycles 1.00
ML-KEM-512 encaps 85058 cycles 85055 cycles 1.00
ML-KEM-512 decaps 112744 cycles 112742 cycles 1.00
ML-KEM-768 keypair 117500 cycles 117683 cycles 1.00
ML-KEM-768 encaps 135232 cycles 135339 cycles 1.00
ML-KEM-768 decaps 171827 cycles 171986 cycles 1.00
ML-KEM-1024 keypair 173673 cycles 173861 cycles 1.00
ML-KEM-1024 encaps 196101 cycles 196221 cycles 1.00
ML-KEM-1024 decaps 242390 cycles 242317 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Arm Cortex-A72 (Raspberry Pi 4) benchmarks

Benchmark suite Current: e3fa106 Previous: 440e7b0 Ratio
ML-KEM-512 keypair 51439 cycles 52194 cycles 0.99
ML-KEM-512 encaps 58366 cycles 58706 cycles 0.99
ML-KEM-512 decaps 75079 cycles 75108 cycles 1.00
ML-KEM-768 keypair 88407 cycles 87962 cycles 1.01
ML-KEM-768 encaps 96577 cycles 96851 cycles 1.00
ML-KEM-768 decaps 119583 cycles 120000 cycles 1.00
ML-KEM-1024 keypair 132066 cycles 131870 cycles 1.00
ML-KEM-1024 encaps 145290 cycles 145065 cycles 1.00
ML-KEM-1024 decaps 175891 cycles 175792 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Bananapi bpi-f3 benchmarks

Benchmark suite Current: e3fa106 Previous: e7721c6 Ratio
ML-KEM-512 keypair 335058 cycles 335053 cycles 1.00
ML-KEM-512 encaps 445599 cycles 445713 cycles 1.00
ML-KEM-512 decaps 593790 cycles 593801 cycles 1.00
ML-KEM-768 keypair 556096 cycles 556004 cycles 1.00
ML-KEM-768 encaps 698032 cycles 697746 cycles 1.00
ML-KEM-768 decaps 890321 cycles 889371 cycles 1.00
ML-KEM-1024 keypair 821323 cycles 821627 cycles 1.00
ML-KEM-1024 encaps 998267 cycles 998284 cycles 1.00
ML-KEM-1024 decaps 1230270 cycles 1230464 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

Please sign in to comment.