TEST

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

Author: hanno-becker

.github/workflows/all.yml

@@ -36,7 +36,6 @@ jobs:
     permissions:
       contents: 'read'
       id-token: 'write'
-    needs: [ base ]
     uses: ./.github/workflows/cbmc.yml
     secrets: inherit
   oqs_integration:

mlkem/indcpa.c

@@ -228,7 +228,7 @@ void mlk_gen_matrix(mlk_polymat a, const uint8_t seed[MLKEM_SYMBYTES],
      * This call writes across mlk_polyvec boundaries for K=2 and K=3.
      * This is intentional and safe.
      */
-    mlk_poly_rej_uniform_x4(&a[i], seed_ext);
+    mlk_poly_rej_uniform_x4(&a[0][0] + i, seed_ext);
   }
 
   /* For MLKEM_K == 3, sample the last entry individually. */
@@ -249,7 +249,7 @@ void mlk_gen_matrix(mlk_polymat a, const uint8_t seed[MLKEM_SYMBYTES],
       seed_ext[0][MLKEM_SYMBYTES + 1] = x;
     }
 
-    mlk_poly_rej_uniform(&a[i], seed_ext[0]);
+    mlk_poly_rej_uniform(&a[0][0] + i, seed_ext[0]);
     i++;
   }
 
@@ -261,7 +261,10 @@ void mlk_gen_matrix(mlk_polymat a, const uint8_t seed[MLKEM_SYMBYTES],
    */
   for (i = 0; i < MLKEM_K * MLKEM_K; i++)
   {
-    mlk_poly_permute_bitrev_to_custom(a[i].coeffs);
+    for (j = 0; i < MLKEM_K * MLKEM_K; i++)
+    {
+       mlk_poly_permute_bitrev_to_custom(a[i][j].coeffs);
+    }
   }
 
   /* Specification: Partially implements
@@ -288,15 +291,15 @@ void mlk_gen_matrix(mlk_polymat a, const uint8_t seed[MLKEM_SYMBYTES],
  * Specification: Implements [FIPS 203, Section 2.4.7, Eq (2.12), (2.13)]
  *
  **************************************************/
-static void mlk_matvec_mul(mlk_polyvec out, const mlk_polymat a,
+static void mlk_matvec_mul(mlk_polyvec out, mlk_polymat a,
                            const mlk_polyvec v, const mlk_polyvec_mulcache vc)
 __contract__(
   requires(memory_no_alias(out, sizeof(mlk_polyvec)))
   requires(memory_no_alias(a, sizeof(mlk_polymat)))
   requires(memory_no_alias(v, sizeof(mlk_polyvec)))
   requires(memory_no_alias(vc, sizeof(mlk_polyvec_mulcache)))
-  requires(forall(k0, 0, MLKEM_K * MLKEM_K,
-      array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
+  requires(forall(k0, 0, MLKEM_K, forall(k4, 0, MLKEM_K,
+    array_bound(a[k0][k4].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))))
   requires(forall(k1, 0, MLKEM_K,
      array_abs_bound(v[k1].coeffs, 0, MLKEM_N, MLK_NTT_BOUND)))
   requires(forall(k2, 0, MLKEM_K,
@@ -313,7 +316,7 @@ __contract__(
     invariant(forall(k, 0, i,
       array_abs_bound(out[k].coeffs, 0, MLKEM_N, INT16_MAX/2))))
   {
-    mlk_polyvec_basemul_acc_montgomery_cached(&out[i], &a[MLKEM_K * i], v, vc);
+    mlk_polyvec_basemul_acc_montgomery_cached(&out[i], a[i], v, vc);
   }
 }
 

mlkem/indcpa.h

@@ -36,8 +36,8 @@ __contract__(
   requires(memory_no_alias(seed, MLKEM_SYMBYTES))
   requires(transposed == 0 || transposed == 1)
   assigns(object_whole(a))
-  ensures(forall(x, 0, MLKEM_K * MLKEM_K,
-    array_bound(a[x].coeffs, 0, MLKEM_N, 0, MLKEM_Q)))
+  ensures(forall(x, 0, MLKEM_K, forall(y, 0, MLKEM_K,
+    array_bound(a[x][y].coeffs, 0, MLKEM_N, 0, MLKEM_Q))))
 );
 
 #define mlk_indcpa_keypair_derand MLK_NAMESPACE_K(indcpa_keypair_derand)

mlkem/poly_k.h

@@ -20,7 +20,7 @@
 /* End of level namespacing */
 
 typedef mlk_poly mlk_polyvec[MLKEM_K];
-typedef mlk_poly mlk_polymat[MLKEM_K * MLKEM_K];
+typedef mlk_poly mlk_polymat[MLKEM_K][MLKEM_K];
 typedef mlk_poly_mulcache mlk_polyvec_mulcache[MLKEM_K];
 
 #define mlk_poly_compress_du MLK_NAMESPACE_K(poly_compress_du)

proofs/cbmc/matvec_mul/Makefile

@@ -11,6 +11,7 @@ PROOF_UID = mlk_matvec_mul
 
 DEFINES +=
 INCLUDES +=
+#UNWINDSET += matvec_mul.0:4
 
 REMOVE_FUNCTION_BODY +=
 

proofs/cbmc/matvec_mul/matvec_mul_harness.c

@@ -6,12 +6,13 @@
 #include "poly_k.h"
 
 #define mlk_matvec_mul MLK_NAMESPACE(matvec_mul)
-void mlk_matvec_mul(mlk_polyvec out, const mlk_polymat a, mlk_polyvec const v,
+void mlk_matvec_mul(mlk_polyvec out, mlk_polymat a, mlk_polyvec const v,
                     mlk_polyvec_mulcache const vc);
 
 void harness(void)
 {
-  mlk_poly *out, *a, *v;
+  mlk_poly *out, *v;
+  mlk_poly (*a)[MLKEM_K];
   mlk_poly_mulcache *vc;
   mlk_matvec_mul(out, a, v, vc);
 }