Merge pull request #458 from pq-code-package/cbmc_formatting

CBMC: Make CBMC annotations more readable

.clang-format

@@ -1,8 +1,6 @@
 # SPDX-License-Identifier: Apache-2.0
 #
-# clang-format style file for MLKEM-C
-#
-# This is based on the style for for AWS-LC
+# clang-format style file for mlkem-native
 #
 BasedOnStyle: Google
 MaxEmptyLinesToKeep: 3
@@ -17,4 +15,8 @@ IncludeBlocks: Preserve
 
 # Designate CBMC contracts/macros that appear in .h files
 # as "attributes" so they don't get increasingly indented line after line
-AttributeMacros: ['REQUIRES', 'ENSURES', 'ASSIGNS', 'INVARIANT']
+BreakBeforeBraces: Allman
+WhitespaceSensitiveMacros: ['__contract__', '__loop__' ]
+Macros:
+ - __contract__(x)={} void foo()
+ - __loop__(x)={}

cbmc/proofs/barrett_reduce/barrett_reduce_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   int16_t a;
   int16_t r;
 

cbmc/proofs/basemul_cached/basemul_cached_harness.c

@@ -23,7 +23,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   int16_t *a, *b, *r, b_cached;
 
   basemul_cached(r, a, b, b_cached);

cbmc/proofs/cmov/cmov_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   uint8_t *x, *y;
   size_t len;
   uint8_t b;

cbmc/proofs/cmov_int16/cmov_int16_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   uint16_t b;
   int16_t *r, v;
 

cbmc/proofs/crypto_kem_dec/crypto_kem_dec_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   uint8_t *a, *b, *c;
   crypto_kem_dec(a, b, c);
 }

cbmc/proofs/crypto_kem_enc/crypto_kem_enc_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   uint8_t *a, *b, *c;
   crypto_kem_enc(a, b, c);
 }

cbmc/proofs/crypto_kem_enc_derand/crypto_kem_enc_derand_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   uint8_t *a, *b, *c, *d;
   crypto_kem_enc_derand(a, b, c, d);
 }

cbmc/proofs/crypto_kem_keypair/crypto_kem_keypair_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   uint8_t *a, *b;
   crypto_kem_keypair(a, b);
 }

cbmc/proofs/crypto_kem_keypair_derand/crypto_kem_keypair_derand_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   uint8_t *a, *b, *c;
   crypto_kem_keypair_derand(a, b, c);
 }

cbmc/proofs/fqmul/fqmul_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   int16_t a, b, r;
 
   r = fqmul(a, b);

cbmc/proofs/gen_matrix/gen_matrix_harness.c

@@ -23,7 +23,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   polyvec *a;
   uint8_t *seed;
   int transposed;

cbmc/proofs/gen_matrix_entry/gen_matrix_entry_harness.c

@@ -26,7 +26,8 @@ void gen_matrix_entry(poly *entry, uint8_t seed[MLKEM_SYMBYTES + 16]);
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   poly *out;
   uint8_t *seed;
   gen_matrix_entry(out, seed);

cbmc/proofs/gen_matrix_entry_x4/gen_matrix_entry_x4_harness.c

@@ -26,7 +26,8 @@ void gen_matrix_entry_x4(poly vec[4], uint8_t *seed[4]);
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   poly out[4];
   uint8_t *seed[4];
   gen_matrix_entry_x4(out, seed);

cbmc/proofs/indcpa_dec/indcpa_dec_harness.c

@@ -23,7 +23,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   uint8_t *m, *c, *sk;
   indcpa_dec(m, c, sk);
 }

cbmc/proofs/indcpa_enc/indcpa_enc_harness.c

@@ -23,7 +23,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   uint8_t *a, *b, *c, *d;
   indcpa_enc(a, b, c, d);
 }

cbmc/proofs/indcpa_keypair_derand/indcpa_keypair_derand_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   uint8_t *a, *b, *c;
   indcpa_keypair_derand(a, b, c);
 }

cbmc/proofs/invntt_layer/invntt_layer_harness.c

@@ -23,7 +23,8 @@ void invntt_layer(int16_t *p, int len, int layer);
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   int16_t *a;
   int len, layer;
   invntt_layer(a, len, layer);

cbmc/proofs/matvec_mul/matvec_mul_harness.c

@@ -26,7 +26,8 @@ void matvec_mul(polyvec *out, polyvec const *a, polyvec const *v,
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   polyvec *out, *a, *v;
   polyvec_mulcache *vc;
   matvec_mul(out, a, v, vc);

cbmc/proofs/montgomery_reduce/montgomery_reduce_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   int32_t a;
   int16_t r;
 

cbmc/proofs/ntt_butterfly_block/ntt_butterfly_block_harness.c

@@ -18,7 +18,8 @@ void ntt_butterfly_block(int16_t *r, int16_t root, int start, int len,
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   int16_t *r, root;
   int start, stride, bound;
   ntt_butterfly_block(r, root, start, stride, bound);

cbmc/proofs/ntt_layer/ntt_layer_harness.c

@@ -23,7 +23,8 @@ void ntt_layer(int16_t *p, int len, int layer);
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   int16_t *a;
   int len, layer;
   ntt_layer(a, len, layer);

cbmc/proofs/poly_add/poly_add_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   poly *r, *b;
   poly_add(r, b);
 }

cbmc/proofs/poly_basemul_montgomery_cached/poly_basemul_montgomery_cached_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   poly *r, *a, *b;
   poly_mulcache *b_cached;
 

cbmc/proofs/poly_cbd_eta1/poly_cbd_eta1_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   uint8_t *buf;
   poly *a;
 

cbmc/proofs/poly_cbd_eta2/poly_cbd_eta2_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   uint8_t *buf;
   poly *a;
 

cbmc/proofs/poly_compress_du/poly_compress_du_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   poly *r;
   uint8_t *a;
 

cbmc/proofs/poly_compress_dv/poly_compress_dv_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   poly *r;
   uint8_t *a;
 

cbmc/proofs/poly_decompress_du/poly_decompress_du_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   poly *r;
   uint8_t *a;
 

cbmc/proofs/poly_decompress_dv/poly_decompress_dv_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   poly *r;
   uint8_t *a;
 

cbmc/proofs/poly_frombytes/poly_frombytes_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   poly *a;
   uint8_t *r;
 

cbmc/proofs/poly_frommsg/poly_frommsg_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   poly *a;
   uint8_t *msg;
 

cbmc/proofs/poly_getnoise_eta1122_4x/poly_getnoise_eta1122_4x_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   uint8_t *seed;
   poly *r0, *r1, *r2, *r3;
   uint8_t nonce0, nonce1, nonce2, nonce3;

cbmc/proofs/poly_getnoise_eta1_4x/poly_getnoise_eta1_4x_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   uint8_t *seed;
   poly *r0, *r1, *r2, *r3;
   uint8_t nonce0, nonce1, nonce2, nonce3;

cbmc/proofs/poly_getnoise_eta2/poly_getnoise_eta2_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   uint8_t *seed;
   poly *r;
   uint8_t nonce;

cbmc/proofs/poly_invntt_tomont/poly_invntt_tomont_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   poly *p;
   poly_invntt_tomont(p);
 }

cbmc/proofs/poly_mulcache_compute/poly_mulcache_compute_harness.c

@@ -23,7 +23,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   poly_mulcache *x;
   poly *a;
 

cbmc/proofs/poly_ntt/poly_ntt_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   poly *a;
   poly_ntt(a);
 }

cbmc/proofs/poly_reduce/poly_reduce_harness.c

@@ -22,7 +22,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
   poly *a;
 
   /* Contracts for this function are in poly.h */