Add contract-based proofs for compression functions

- scalar_compress_q_16
- scalar_compress_q_32
- poly_compress

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

cbmc/proofs/Makefile.common

@@ -517,6 +517,7 @@ COMMA :=,
 CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS)
 
 # --object_bits is removed in goto-cc 6.0.0
+# COMPILE_FLAGS += --object-bits $(CBMC_OBJECT_BITS)
 
 DEFINES += -DCBMC=1
 DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS)

cbmc/proofs/poly_compress/Makefile

@@ -19,12 +19,15 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c
 
-# UNWINDSET += $(KYBER_NAMESPACE)poly_compress.0:9
-# UNWINDSET += $(KYBER_NAMESPACE)poly_compress.1:33
+CHECK_FUNCTION_CONTRACTS=$(KYBER_NAMESPACE)poly_compress
+USE_FUNCTION_CONTRACTS = $(KYBER_NAMESPACE)scalar_compress_q_16 $(KYBER_NAMESPACE)scalar_compress_q_32 $(KYBER_NAMESPACE)scalar_signed_to_unsigned_q_16
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+CBMCFLAGS=--smt2
 
 FUNCTION_NAME = $(KYBER_NAMESPACE)poly_compress
 
-USE_FUNCTION_CONTRACTS = $(KYBER_NAMESPACE)scalar_compress_q_16 $(KYBER_NAMESPACE)scalar_compress_q_32
 # If this proof is found to consume huge amounts of RAM, you can set the
 # EXPENSIVE variable. With new enough versions of the proof tools, this will
 # restrict the number of EXPENSIVE CBMC jobs running at once. See the

cbmc/proofs/poly_compress/poly_compress_harness.c

@@ -26,9 +26,5 @@ void harness(void)
     poly r;
     uint8_t a[KYBER_POLYCOMPRESSEDBYTES];
 
-    __CPROVER_assume(__CPROVER_forall
-    {
-        unsigned i; (i < KYBER_N) ==> ( -KYBER_Q <= r.coeffs[i] && r.coeffs[i] < KYBER_Q )
-    });
     poly_compress(a, &r);
 }

mlkem/poly.c

@@ -27,11 +27,14 @@ uint32_t scalar_compress_q_16(int32_t u)
 
     /* This multiply will exceed UINT32_MAX and wrap around */
     /* for large values of u. This is expected and required */
+    #ifdef CBMC
 #pragma CPROVER check push
 #pragma CPROVER check disable "unsigned-overflow"
+    #endif
     d0 *=  80635;
+    #ifdef CBMC
 #pragma CPROVER check pop
-
+    #endif
     d0 >>= 28;
     d0 &=  0xF;
     return d0;
@@ -66,11 +69,14 @@ uint32_t scalar_compress_q_32(int32_t u)
 
     /* This multiply will exceed UINT32_MAX and wrap around */
     /* for large values of u. This is expected and required */
+    #ifdef CBMC
 #pragma CPROVER check push
 #pragma CPROVER check disable "unsigned-overflow"
+    #endif
     d0 *=  40318;
+    #ifdef CBMC
 #pragma CPROVER check pop
-
+    #endif
     d0 >>= 27;
     d0 &=  0x1f;
     return d0;
@@ -130,35 +136,44 @@ uint16_t scalar_signed_to_unsigned_q_16 (int16_t c)
 **************************************************/
 void poly_compress(uint8_t r[KYBER_POLYCOMPRESSEDBYTES], const poly *a)
 {
-    unsigned int i, j;
-    uint8_t t[8];
+    uint8_t t[8] = { 0 };
 
     #if (KYBER_POLYCOMPRESSEDBYTES == 128)
-    for (i = 0; i < KYBER_N / 8; i++)
-        __CPROVER_assigns(i, j, t, r)
-        /* Stronger loop invariant here TBD */
-    {
-        for (j = 0; j < 8; j++)
-            __CPROVER_assigns(j, t)
-            /* Stronger loop invariant here TBD */
+    for (size_t i = 0; i < KYBER_N / 8; i++)
+        __CPROVER_assigns(i, __CPROVER_object_whole(t), __CPROVER_object_whole(r))
+        __CPROVER_loop_invariant(i <= KYBER_N)
+        __CPROVER_decreases(32 - i) {
+        for (size_t j = 0; j < 8; j++)
+// *INDENT-OFF*
+            __CPROVER_assigns(j, __CPROVER_object_whole(t))
+            __CPROVER_loop_invariant(i <= KYBER_N)
+            __CPROVER_loop_invariant(j <= 8)
+            __CPROVER_loop_invariant(__CPROVER_forall { size_t k2; (0 <= k2 && k2 < j) ==> (t[k2] >= 0 && t[k2] < 16) })
+            __CPROVER_decreases(8 - j)
+// *INDENT-ON*
         {
             // map to positive standard representatives
             // REF-CHANGE: Hoist signed-to-unsigned conversion into separate function
-            int32_t u = (int32_t) scalar_signed_to_unsigned_q_16(a->coeffs[8 * i + j]);
+            int32_t u;
+            u = (int32_t) scalar_signed_to_unsigned_q_16(a->coeffs[8 * i + j]);
             // REF-CHANGE: Hoist scalar compression into separate function
             t[j] = scalar_compress_q_16(u);
         }
 
+        __CPROVER_assert(t[0] < 16, "UB on t[0]");
+        __CPROVER_assert(t[1] < 16, "UB on t[1]");
+        __CPROVER_assert((t[0] | (t[1] << 4)) <= 255, "Range of t");
+
         r[0] = t[0] | (t[1] << 4);
         r[1] = t[2] | (t[3] << 4);
         r[2] = t[4] | (t[5] << 4);
         r[3] = t[6] | (t[7] << 4);
         r += 4;
     }
     #elif (KYBER_POLYCOMPRESSEDBYTES == 160)
-    for (i = 0; i < KYBER_N / 8; i++)
+    for (size_t i = 0; i < KYBER_N / 8; i++)
     {
-        for (j = 0; j < 8; j++)
+        for (size_t j = 0; j < 8; j++)
         {
             // map to positive standard representatives
             // REF-CHANGE: Hoist signed-to-unsigned conversion into separate function

mlkem/poly.h

@@ -2,6 +2,7 @@
 #ifndef POLY_H
 #define POLY_H
 
+#include <stddef.h>
 #include <stdint.h>
 #include "params.h"
 #include "cbmc.h"
@@ -57,7 +58,16 @@ __CPROVER_ensures(__CPROVER_return_value == (int32_t) c + (((int32_t) c < 0) * K
 /* *INDENT-ON* */
 
 #define poly_compress KYBER_NAMESPACE(poly_compress)
-void poly_compress(uint8_t r[KYBER_POLYCOMPRESSEDBYTES], const poly *a);
+void poly_compress(uint8_t r[KYBER_POLYCOMPRESSEDBYTES], const poly *a)
+/* *INDENT-OFF* */
+__CPROVER_requires(r != NULL)
+__CPROVER_requires(__CPROVER_is_fresh(r, KYBER_POLYCOMPRESSEDBYTES))
+__CPROVER_requires(a != NULL)
+__CPROVER_requires(__CPROVER_is_fresh(a, sizeof(poly)))
+__CPROVER_requires(__CPROVER_forall { unsigned k; (k < KYBER_N) ==> ( -KYBER_Q <= a->coeffs[k] && a->coeffs[k] < KYBER_Q ) })
+__CPROVER_assigns(__CPROVER_object_whole(r));
+/* *INDENT-ON* */
+
 
 #define poly_decompress KYBER_NAMESPACE(poly_decompress)
 void poly_decompress(poly *r, const uint8_t a[KYBER_POLYCOMPRESSEDBYTES]);