Merge pull request #280 from pq-code-package/cbmc-poly_add-polyveck_add-polyvecl_add

CBMC and refactor: Change poly_add and vector-variants and add proof

Author: mkannwischer

mldsa/poly.c

@@ -50,20 +50,20 @@ void poly_caddq(poly *a)
 
   mld_assert_bound(a->coeffs, MLDSA_N, 0, MLDSA_Q);
 }
-
-void poly_add(poly *c, const poly *a, const poly *b)
+/* Reference: We use destructive version (output=first input) to avoid
+ *            reasoning about aliasing in the CBMC specification */
+void poly_add(poly *r, const poly *b)
 {
   unsigned int i;
-
   for (i = 0; i < MLDSA_N; ++i)
   __loop__(
-    invariant(i <= MLDSA_N)
-    invariant(forall(k1, 0, i, c->coeffs[k1] == a->coeffs[k1] + b->coeffs[k1])))
+      invariant(i <= MLDSA_N)
+      invariant(forall(k0, i, MLDSA_N, r->coeffs[k0] == loop_entry(*r).coeffs[k0]))
+      invariant(forall(k1, 0, i, r->coeffs[k1] == loop_entry(*r).coeffs[k1] + b->coeffs[k1]))
+    )
   {
-    c->coeffs[i] = a->coeffs[i] + b->coeffs[i];
+    r->coeffs[i] = r->coeffs[i] + b->coeffs[i];
   }
-
-  cassert(forall(k, 0, MLDSA_N, c->coeffs[k] == a->coeffs[k] + b->coeffs[k]));
 }
 
 void poly_sub(poly *c, const poly *a, const poly *b)

mldsa/poly.h

@@ -57,18 +57,23 @@ __contract__(
  *
  * Description: Add polynomials. No modular reduction is performed.
  *
- * Arguments:   - poly *c: pointer to output polynomial
- *              - const poly *a: pointer to first summand
- *              - const poly *b: pointer to second summand
+ * Arguments: - r: Pointer to input-output polynomial to be added to.
+ *            - b: Pointer to input polynomial that should be added
+ *                 to r. Must be disjoint from r.
  **************************************************/
-void poly_add(poly *c, const poly *a, const poly *b)
+
+/*
+ * NOTE: The reference implementation uses a 3-argument poly_add.
+ * We specialize to the accumulator form to avoid reasoning about aliasing.
+ */
+void poly_add(poly *r, const poly *b)
 __contract__(
-  requires(memory_no_alias(c, sizeof(poly)))
-  requires(memory_no_alias(a, sizeof(poly)))
   requires(memory_no_alias(b, sizeof(poly)))
-  requires(forall(k0, 0, MLDSA_N, (int64_t) a->coeffs[k0] + b->coeffs[k0] <= INT32_MAX))
-  requires(forall(k1, 0, MLDSA_N, (int64_t) a->coeffs[k1] + b->coeffs[k1] >= INT32_MIN))
-  assigns(memory_slice(c, sizeof(poly)))
+  requires(memory_no_alias(r, sizeof(poly)))
+  requires(forall(k0, 0, MLDSA_N, (int64_t) r->coeffs[k0] + b->coeffs[k0] <= INT32_MAX))
+  requires(forall(k1, 0, MLDSA_N, (int64_t) r->coeffs[k1] + b->coeffs[k1] >= INT32_MIN))
+  assigns(memory_slice(r, sizeof(poly)))
+  ensures(forall(k, 0, MLDSA_N, r->coeffs[k] == old(*r).coeffs[k] + b->coeffs[k]))
 );
 
 #define poly_sub MLD_NAMESPACE(poly_sub)

mldsa/polyvec.c

@@ -162,20 +162,24 @@ void polyvecl_reduce(polyvecl *v)
   }
 }
 
-void polyvecl_add(polyvecl *w, const polyvecl *u, const polyvecl *v)
+/* Reference: We use destructive version (output=first input) to avoid
+ *            reasoning about aliasing in the CBMC specification */
+void polyvecl_add(polyvecl *u, const polyvecl *v)
 {
   unsigned int i;
 
   for (i = 0; i < MLDSA_L; ++i)
   __loop__(
-    invariant(i <= MLDSA_L))
+    invariant(i <= MLDSA_L)
+    invariant(forall(k0, i, MLDSA_L, 
+              forall(k1, 0, MLDSA_N, u->vec[k0].coeffs[k1] == loop_entry(*u).vec[k0].coeffs[k1]))))
   {
-    poly t;
-    poly_add(&t, &u->vec[i], &v->vec[i]);
+    poly tmp = u->vec[i];
+    poly_add(&tmp, &v->vec[i]);
     /* Full struct assignment from local variables to simplify proof */
     /* TODO: eliminate once CBMC resolves
      * https://github.com/diffblue/cbmc/issues/8617 */
-    w->vec[i] = t;
+    u->vec[i] = tmp;
   }
 }
 
@@ -323,20 +327,24 @@ void polyveck_caddq(polyveck *v)
   }
 }
 
-void polyveck_add(polyveck *w, const polyveck *u, const polyveck *v)
+/* Reference: We use destructive version (output=first input) to avoid
+ *            reasoning about aliasing in the CBMC specification */
+void polyveck_add(polyveck *u, const polyveck *v)
 {
   unsigned int i;
 
   for (i = 0; i < MLDSA_K; ++i)
   __loop__(
-    invariant(i <= MLDSA_K))
+    invariant(i <= MLDSA_K)
+    invariant(forall(k0, i, MLDSA_K, 
+             forall(k1, 0, MLDSA_N, u->vec[k0].coeffs[k1] == loop_entry(*u).vec[k0].coeffs[k1]))))
   {
-    poly t;
-    poly_add(&t, &u->vec[i], &v->vec[i]);
+    poly tmp = u->vec[i];
+    poly_add(&tmp, &v->vec[i]);
     /* Full struct assignment from local variables to simplify proof */
     /* TODO: eliminate once CBMC resolves
      * https://github.com/diffblue/cbmc/issues/8617 */
-    w->vec[i] = t;
+    u->vec[i] = tmp;
   }
 }
 

mldsa/polyvec.h

@@ -67,20 +67,18 @@ __contract__(
  * Description: Add vectors of polynomials of length MLDSA_L.
  *              No modular reduction is performed.
  *
- * Arguments:   - polyvecl *w: pointer to output vector
- *              - const polyvecl *u: pointer to first summand
- *              - const polyvecl *v: pointer to second summand
+ * Arguments:   - polyveck *u: pointer to input-output vector of polynomials to
+ *              be added to
+ *              - const polyveck *v: pointer to second input vector of
+ *              polynomials
  **************************************************/
-void polyvecl_add(polyvecl *w, const polyvecl *u, const polyvecl *v)
+void polyvecl_add(polyvecl *u, const polyvecl *v)
 __contract__(
-  requires(memory_no_alias(w, sizeof(polyvecl)))
   requires(memory_no_alias(u, sizeof(polyvecl)))
   requires(memory_no_alias(v, sizeof(polyvecl)))
-  requires(forall(k0, 0, MLDSA_L,
-    forall(k1, 0, MLDSA_N, (int64_t) u->vec[k0].coeffs[k1] + v->vec[k0].coeffs[k1] <= INT32_MAX)))
-  requires(forall(k2, 0, MLDSA_L,
-    forall(k3, 0, MLDSA_N, (int64_t) u->vec[k2].coeffs[k3] + v->vec[k2].coeffs[k3] >= INT32_MIN)))
-  assigns(memory_slice(w, sizeof(polyvecl)))
+  requires(forall(k0, 0, MLDSA_L, forall(k1, 0, MLDSA_N, (int64_t) u->vec[k0].coeffs[k1] + v->vec[k0].coeffs[k1] <= INT32_MAX)))
+  requires(forall(k2, 0, MLDSA_L, forall(k3, 0, MLDSA_N, (int64_t) u->vec[k2].coeffs[k3] + v->vec[k2].coeffs[k3] >= INT32_MIN)))
+  assigns(object_whole(u))
 );
 
 #define polyvecl_ntt MLD_NAMESPACE(polyvecl_ntt)
@@ -242,20 +240,18 @@ __contract__(
  * Description: Add vectors of polynomials of length MLDSA_K.
  *              No modular reduction is performed.
  *
- * Arguments:   - polyveck *w: pointer to output vector
- *              - const polyveck *u: pointer to first summand
- *              - const polyveck *v: pointer to second summand
+ * Arguments:   - polyveck *u: pointer to input-output vector of polynomials to
+ *              be added to
+ *              - const polyveck *v: pointer to second input vector of
+ *              polynomials
  **************************************************/
-void polyveck_add(polyveck *w, const polyveck *u, const polyveck *v)
+void polyveck_add(polyveck *u, const polyveck *v)
 __contract__(
-  requires(memory_no_alias(w, sizeof(polyveck)))
   requires(memory_no_alias(u, sizeof(polyveck)))
   requires(memory_no_alias(v, sizeof(polyveck)))
-  requires(forall(k0, 0, MLDSA_K,
-    forall(k1, 0, MLDSA_N, (int64_t) u->vec[k0].coeffs[k1] + v->vec[k0].coeffs[k1] <= INT32_MAX)))
-  requires(forall(k2, 0, MLDSA_K,
-    forall(k3, 0, MLDSA_N, (int64_t) u->vec[k2].coeffs[k3] + v->vec[k2].coeffs[k3] >= INT32_MIN)))
-  assigns(memory_slice(w, sizeof(polyveck)))
+  requires(forall(k0, 0, MLDSA_K, forall(k1, 0, MLDSA_N, (int64_t) u->vec[k0].coeffs[k1] + v->vec[k0].coeffs[k1] <= INT32_MAX)))
+  requires(forall(k2, 0, MLDSA_K, forall(k3, 0, MLDSA_N, (int64_t) u->vec[k2].coeffs[k3] + v->vec[k2].coeffs[k3] >= INT32_MIN)))
+  assigns(object_whole(u))
 );
 
 #define polyveck_sub MLD_NAMESPACE(polyveck_sub)

mldsa/sign.c

@@ -71,7 +71,7 @@ int crypto_sign_keypair_internal(uint8_t *pk, uint8_t *sk,
   polyveck_invntt_tomont(&t1);
 
   /* Add error vector s2 */
-  polyveck_add(&t1, &t1, &s2);
+  polyveck_add(&t1, &s2);
 
   /* Extract t1 and write public key */
   polyveck_caddq(&t1);
@@ -179,7 +179,7 @@ int crypto_sign_signature_internal(uint8_t *sig, size_t *siglen,
     /* Compute z, reject if it reveals secret */
     polyvecl_pointwise_poly_montgomery(&z, &cp, &s1);
     polyvecl_invntt_tomont(&z);
-    polyvecl_add(&z, &z, &y);
+    polyvecl_add(&z, &y);
     polyvecl_reduce(&z);
     if (polyvecl_chknorm(&z, MLDSA_GAMMA1 - MLDSA_BETA))
     {
@@ -209,7 +209,7 @@ int crypto_sign_signature_internal(uint8_t *sig, size_t *siglen,
       continue;
     }
 
-    polyveck_add(&w0, &w0, &h);
+    polyveck_add(&w0, &h);
     n = polyveck_make_hint(&h, &w0, &w1);
     if (n > MLDSA_OMEGA)
     {

proofs/cbmc/poly_add/poly_add_harness.c

@@ -5,6 +5,6 @@
 
 void harness(void)
 {
-  poly *c, *a, *b;
-  poly_add(c, a, b);
+  poly *r, *b;
+  poly_add(r, b);
 }

proofs/cbmc/polyveck_add/polyveck_add_harness.c

@@ -5,6 +5,6 @@
 
 void harness(void)
 {
-  polyveck *a, *b, *c;
-  polyveck_add(a, b, c);
+  polyveck *r, *b;
+  polyveck_add(r, b);
 }

proofs/cbmc/polyvecl_add/polyvecl_add_harness.c

@@ -5,6 +5,6 @@
 
 void harness(void)
 {
-  polyvecl *a, *b, *c;
-  polyvecl_add(a, b, c);
+  polyvecl *r, *b;
+  polyvecl_add(r, b);
 }