Reformat with bsd style and NO pad-oper otions for compatibility with…

… CBMC contracts (#64) Signed-off-by: Rod Chapman <[email protected]>
pq-code-package · Jun 17, 2024 · 5413c27 · 5413c27
1 parent 3d23dda
commit 5413c27
Show file tree

Hide file tree

Showing 28 changed files with 602 additions and 300 deletions.
diff --git a/.astylerc b/.astylerc
@@ -1,14 +1,13 @@
 # SPDX-License-Identifier: Apache-2.0
---style=google 
+--style=bsd
 --indent=spaces
 --indent-preproc-define
 --indent-preproc-cond
---pad-oper 
---pad-comma 
+--pad-comma
 --pad-header
---align-pointer=name 
---add-braces 
+--align-pointer=name
+--add-braces
 --convert-tabs
---mode=c 
+--mode=c
 --suffix=none
 --lineend=linux
diff --git a/cbmc/proofs/poly_compress/poly_compress_harness.c b/cbmc/proofs/poly_compress/poly_compress_harness.c
@@ -21,7 +21,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
     poly r;
     uint8_t a[KYBER_POLYCOMPRESSEDBYTES];
 

diff --git a/cbmc/proofs/poly_decompress/poly_decompress_harness.c b/cbmc/proofs/poly_decompress/poly_decompress_harness.c
@@ -21,7 +21,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
     poly r;
     uint8_t a[KYBER_POLYCOMPRESSEDBYTES];
 

diff --git a/cbmc/proofs/scalar_compress_q_16/scalar_compress_q_16_harness.c b/cbmc/proofs/scalar_compress_q_16/scalar_compress_q_16_harness.c
@@ -21,7 +21,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
     int32_t u;
 
     /* Contracts for this function are in poly.h */

diff --git a/cbmc/proofs/scalar_compress_q_32/scalar_compress_q_32_harness.c b/cbmc/proofs/scalar_compress_q_32/scalar_compress_q_32_harness.c
@@ -21,7 +21,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
     int32_t u;
 
     /* Contracts for this function are in poly.h */

diff --git a/cbmc/proofs/scalar_decompress_q_16/scalar_decompress_q_16_harness.c b/cbmc/proofs/scalar_decompress_q_16/scalar_decompress_q_16_harness.c
@@ -21,7 +21,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
     // Check that decompression followed by compression is the identity
     uint32_t c0, c1, d;
 

diff --git a/cbmc/proofs/scalar_decompress_q_32/scalar_decompress_q_32_harness.c b/cbmc/proofs/scalar_decompress_q_32/scalar_decompress_q_32_harness.c
@@ -21,7 +21,8 @@
  * @brief Starting point for formal analysis
  *
  */
-void harness(void) {
+void harness(void)
+{
     // Check that decompression followed by compression is the identity
     uint32_t c0, c1, d;
 

diff --git a/fips202/fips202.c b/fips202/fips202.c
@@ -32,22 +32,28 @@
 static void keccak_absorb(uint64_t *s,
                           uint32_t r,
                           const uint8_t *m, size_t mlen,
-                          uint8_t p) {
-    while (mlen >= r) {
+                          uint8_t p)
+{
+    while (mlen >= r)
+    {
         KeccakF1600_StateXORBytes(s, m, 0, r);
         KeccakF1600_StatePermute(s);
         mlen -= r;
         m += r;
     }
 
-    if (mlen > 0) {
+    if (mlen > 0)
+    {
         KeccakF1600_StateXORBytes(s, m, 0, mlen);
     }
 
-    if (mlen == r - 1) {
+    if (mlen == r - 1)
+    {
         p |= 128;
         KeccakF1600_StateXORBytes(s, &p, mlen, 1);
-    } else {
+    }
+    else
+    {
         KeccakF1600_StateXORBytes(s, &p, mlen, 1);
         p = 128;
         KeccakF1600_StateXORBytes(s, &p, r - 1, 1);
@@ -68,8 +74,10 @@ static void keccak_absorb(uint64_t *s,
  **************************************************/
 static void keccak_squeezeblocks(uint8_t *h, size_t nblocks,
                                  uint64_t *s,
-                                 uint32_t r) {
-    while (nblocks > 0) {
+                                 uint32_t r)
+{
+    while (nblocks > 0)
+    {
         KeccakF1600_StatePermute(s);
         KeccakF1600_StateExtractBytes(s, h, 0, r);
         h += r;
@@ -87,10 +95,12 @@ static void keccak_squeezeblocks(uint8_t *h, size_t nblocks,
  *                26th value represents either the number of absorbed bytes
  *                that have not been permuted, or not-yet-squeezed bytes.
  **************************************************/
-static void keccak_inc_init(uint64_t *s_inc) {
+static void keccak_inc_init(uint64_t *s_inc)
+{
     size_t i;
 
-    for (i = 0; i < 25; ++i) {
+    for (i = 0; i < 25; ++i)
+    {
         s_inc[i] = 0;
     }
     s_inc[25] = 0;
@@ -110,9 +120,11 @@ static void keccak_inc_init(uint64_t *s_inc) {
  *              - size_t mlen: length of input in bytes
  **************************************************/
 static void keccak_inc_absorb(uint64_t *s_inc, uint32_t r, const uint8_t *m,
-                              size_t mlen) {
+                              size_t mlen)
+{
     /* Recall that s_inc[25] is the non-absorbed bytes xored into the state */
-    while (mlen + s_inc[25] >= r) {
+    while (mlen + s_inc[25] >= r)
+    {
 
         KeccakF1600_StateXORBytes(s_inc, m, s_inc[25], r - s_inc[25]);
         mlen -= (size_t)(r - s_inc[25]);
@@ -139,13 +151,17 @@ static void keccak_inc_absorb(uint64_t *s_inc, uint32_t r, const uint8_t *m,
  *              - uint8_t p: domain-separation byte for different
  *                                 Keccak-derived functions
  **************************************************/
-static void keccak_inc_finalize(uint64_t *s_inc, uint32_t r, uint8_t p) {
+static void keccak_inc_finalize(uint64_t *s_inc, uint32_t r, uint8_t p)
+{
     /* After keccak_inc_absorb, we are guaranteed that s_inc[25] < r,
        so we can always use one more byte for p in the current state. */
-    if (s_inc[25] == r - 1) {
+    if (s_inc[25] == r - 1)
+    {
         p |= 128;
         KeccakF1600_StateXORBytes(s_inc, &p, s_inc[25], 1);
-    } else {
+    }
+    else
+    {
         KeccakF1600_StateXORBytes(s_inc, &p, s_inc[25], 1);
         p = 128;
         KeccakF1600_StateXORBytes(s_inc, &p, r - 1, 1);
@@ -167,11 +183,15 @@ static void keccak_inc_finalize(uint64_t *s_inc, uint32_t r, uint8_t p) {
  *              - uint32_t r: rate in bytes (e.g., 168 for SHAKE128)
  **************************************************/
 static void keccak_inc_squeeze(uint8_t *h, size_t outlen,
-                               uint64_t *s_inc, uint32_t r) {
+                               uint64_t *s_inc, uint32_t r)
+{
     size_t len;
-    if (outlen < s_inc[25]) {
+    if (outlen < s_inc[25])
+    {
         len = outlen;
-    } else {
+    }
+    else
+    {
         len = s_inc[25];
     }
 
@@ -181,12 +201,16 @@ static void keccak_inc_squeeze(uint8_t *h, size_t outlen,
     s_inc[25] -= len;
 
     /* Then squeeze the remaining necessary blocks */
-    while (outlen > 0) {
+    while (outlen > 0)
+    {
         KeccakF1600_StatePermute(s_inc);
 
-        if (outlen < r) {
+        if (outlen < r)
+        {
             len = outlen;
-        } else {
+        }
+        else
+        {
             len = r;
         }
         KeccakF1600_StateExtractBytes(s_inc, h, 0, len);
@@ -196,19 +220,23 @@ static void keccak_inc_squeeze(uint8_t *h, size_t outlen,
     }
 }
 
-void shake256_inc_init(shake256incctx *state) {
+void shake256_inc_init(shake256incctx *state)
+{
     keccak_inc_init(state->ctx);
 }
 
-void shake256_inc_absorb(shake256incctx *state, const uint8_t *input, size_t inlen) {
+void shake256_inc_absorb(shake256incctx *state, const uint8_t *input, size_t inlen)
+{
     keccak_inc_absorb(state->ctx, SHAKE256_RATE, input, inlen);
 }
 
-void shake256_inc_finalize(shake256incctx *state) {
+void shake256_inc_finalize(shake256incctx *state)
+{
     keccak_inc_finalize(state->ctx, SHAKE256_RATE, 0x1F);
 }
 
-void shake256_inc_squeeze(uint8_t *output, size_t outlen, shake256incctx *state) {
+void shake256_inc_squeeze(uint8_t *output, size_t outlen, shake256incctx *state)
+{
     keccak_inc_squeeze(output, outlen, state->ctx, SHAKE256_RATE);
 }
 
@@ -222,9 +250,11 @@ void shake256_inc_squeeze(uint8_t *output, size_t outlen, shake256incctx *state)
  *              - const uint8_t *input: pointer to input to be absorbed into state
  *              - size_t inlen:         length of input in bytes
  **************************************************/
-void shake128_absorb(shake128ctx *state, const uint8_t *input, size_t inlen) {
+void shake128_absorb(shake128ctx *state, const uint8_t *input, size_t inlen)
+{
     int i;
-    for (i = 0; i < 25; i++) {
+    for (i = 0; i < 25; i++)
+    {
         state->ctx[i] = 0;
     }
 
@@ -242,7 +272,8 @@ void shake128_absorb(shake128ctx *state, const uint8_t *input, size_t inlen) {
  *              - size_t nblocks:      number of blocks to be squeezed (written to output)
  *              - shake128ctx *state:  pointer to in/output Keccak state
  **************************************************/
-void shake128_squeezeblocks(uint8_t *output, size_t nblocks, shake128ctx *state) {
+void shake128_squeezeblocks(uint8_t *output, size_t nblocks, shake128ctx *state)
+{
     keccak_squeezeblocks(output, nblocks, state->ctx, SHAKE128_RATE);
 }
 
@@ -257,7 +288,8 @@ void shake128_squeezeblocks(uint8_t *output, size_t nblocks, shake128ctx *state)
  *              - size_t inlen:         length of input in bytes
  **************************************************/
 void shake256(uint8_t *output, size_t outlen,
-              const uint8_t *input, size_t inlen) {
+              const uint8_t *input, size_t inlen)
+{
     shake256incctx state;
 
     keccak_inc_init(state.ctx);
@@ -279,7 +311,8 @@ void shake256(uint8_t *output, size_t outlen,
  *              - const uint8_t *input: pointer to input
  *              - size_t inlen:         length of input in bytes
  **************************************************/
-void sha3_256(uint8_t *output, const uint8_t *input, size_t inlen) {
+void sha3_256(uint8_t *output, const uint8_t *input, size_t inlen)
+{
     uint64_t ctx[26];
     keccak_inc_init(ctx);
 
@@ -300,7 +333,8 @@ void sha3_256(uint8_t *output, const uint8_t *input, size_t inlen) {
  *              - const uint8_t *input: pointer to input
  *              - size_t inlen:         length of input in bytes
  **************************************************/
-void sha3_512(uint8_t *output, const uint8_t *input, size_t inlen) {
+void sha3_512(uint8_t *output, const uint8_t *input, size_t inlen)
+{
     uint64_t ctx[26];
     keccak_inc_init(ctx);
 

diff --git a/fips202/fips202.h b/fips202/fips202.h
@@ -12,22 +12,26 @@
 #define SHA3_512_RATE 72
 
 // Context for incremental API
-typedef struct {
+typedef struct
+{
     uint64_t ctx[26];
 } shake128incctx;
 
 // Context for non-incremental API
-typedef struct {
+typedef struct
+{
     uint64_t ctx[25];
 } shake128ctx;
 
 // Context for incremental API
-typedef struct {
+typedef struct
+{
     uint64_t ctx[26];
 } shake256incctx;
 
 // Context for non-incremental API
-typedef struct {
+typedef struct
+{
     uint64_t ctx[25];
 } shake256ctx;
 

diff --git a/fips202/keccakf1600.c b/fips202/keccakf1600.c
@@ -14,7 +14,8 @@
 #define NROUNDS 24
 #define ROL(a, offset) ((a << offset) ^ (a >> (64-offset)))
 
-static const uint64_t KeccakF_RoundConstants[NROUNDS] = {
+static const uint64_t KeccakF_RoundConstants[NROUNDS] =
+{
     (uint64_t)0x0000000000000001ULL,
     (uint64_t)0x0000000000008082ULL,
     (uint64_t)0x800000000000808aULL,
@@ -41,21 +42,26 @@ static const uint64_t KeccakF_RoundConstants[NROUNDS] = {
     (uint64_t)0x8000000080008008ULL
 };
 
-void KeccakF1600_StateExtractBytes(uint64_t *state, unsigned char *data, unsigned int offset, unsigned int length) {
+void KeccakF1600_StateExtractBytes(uint64_t *state, unsigned char *data, unsigned int offset, unsigned int length)
+{
     unsigned int i;
-    for (i = 0; i < length; i++) {
+    for (i = 0; i < length; i++)
+    {
         data[i] = state[(offset + i) >> 3] >> (8 * ((offset + i) & 0x07));
     }
 }
 
-void KeccakF1600_StateXORBytes(uint64_t *state, const unsigned char *data, unsigned int offset, unsigned int length) {
+void KeccakF1600_StateXORBytes(uint64_t *state, const unsigned char *data, unsigned int offset, unsigned int length)
+{
     unsigned int i;
-    for (i = 0; i < length; i++) {
+    for (i = 0; i < length; i++)
+    {
         state[(offset + i) >> 3] ^= (uint64_t)data[i] << (8 * ((offset + i) & 0x07));
     }
 }
 
-void KeccakF1600_StatePermute(uint64_t *state) {
+void KeccakF1600_StatePermute(uint64_t *state)
+{
     int round;
 
     uint64_t Aba, Abe, Abi, Abo, Abu;
@@ -98,7 +104,8 @@ void KeccakF1600_StatePermute(uint64_t *state) {
     Aso = state[23];
     Asu = state[24];
 
-    for ( round = 0; round < NROUNDS; round += 2 ) {
+    for ( round = 0; round < NROUNDS; round += 2 )
+    {
         //    prepareTheta
         BCa = Aba ^ Aga ^ Aka ^ Ama ^ Asa;
         BCe = Abe ^ Age ^ Ake ^ Ame ^ Ase;