Refresh with latest code from Karthik

cryspen · Apr 18, 2024 · 4e9c96a · 4e9c96a
1 parent e18be45
commit 4e9c96a
Show file tree

Hide file tree

Showing 8 changed files with 72 additions and 36 deletions.
diff --git a/libcrux/include/Eurydice.h b/libcrux/include/Eurydice.h
@@ -1,8 +1,8 @@
 /* 
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc
-  F* version: 13bd96aa
-  KaRaMeL version: 9926c187
+  F* version: c990b3ca
+  KaRaMeL version: c27466aa
  */
 
 #ifndef __Eurydice_H

diff --git a/libcrux/include/core.h b/libcrux/include/core.h
@@ -1,8 +1,8 @@
 /* 
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc
-  F* version: 13bd96aa
-  KaRaMeL version: 9926c187
+  F* version: c990b3ca
+  KaRaMeL version: c27466aa
  */
 
 #ifndef __core_H

diff --git a/libcrux/include/internal/core.h b/libcrux/include/internal/core.h
@@ -1,8 +1,8 @@
 /* 
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc
-  F* version: 13bd96aa
-  KaRaMeL version: 9926c187
+  F* version: c990b3ca
+  KaRaMeL version: c27466aa
  */
 
 #ifndef __internal_core_H

diff --git a/libcrux/include/internal/libcrux_kyber.h b/libcrux/include/internal/libcrux_kyber.h
@@ -1,8 +1,8 @@
 /* 
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc
-  F* version: 13bd96aa
-  KaRaMeL version: 9926c187
+  F* version: c990b3ca
+  KaRaMeL version: c27466aa
  */
 
 #ifndef __internal_libcrux_kyber_H

diff --git a/libcrux/include/libcrux_digest.h b/libcrux/include/libcrux_digest.h
@@ -1,8 +1,8 @@
 /* 
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc
-  F* version: 13bd96aa
-  KaRaMeL version: 9926c187
+  F* version: c990b3ca
+  KaRaMeL version: c27466aa
  */
 
 #ifndef __libcrux_digest_H

diff --git a/libcrux/include/libcrux_kyber.h b/libcrux/include/libcrux_kyber.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config
-  ../../kyber-c.yaml ../libcrux_kyber.llbc F* version: 13bd96aa KaRaMeL version:
-  9926c187
+  ../../kyber-c.yaml ../libcrux_kyber.llbc F* version: c990b3ca KaRaMeL version:
+  c27466aa
  */
 
 #ifndef __libcrux_kyber_H
@@ -142,7 +142,7 @@ void libcrux_kyber_kyber768_decapsulate(uint8_t (*secret_key)[2400U],
 void libcrux_kyber_kyber768_decapsulate_unpacked(
   int32_t (*secret_as_ntt)[256U],
   int32_t (*t_as_ntt)[256U],
-  int32_t (*A_transpose)[3U][256U],
+  int32_t (*a_transpose)[3U][256U],
   Eurydice_slice implicit_rejection_value,
   Eurydice_slice ind_cpa_public_key_hash,
   uint8_t (*ciphertext)[1088U],

diff --git a/libcrux/src/core.c b/libcrux/src/core.c
@@ -1,8 +1,8 @@
 /* 
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config ../../kyber-c.yaml ../libcrux_kyber.llbc
-  F* version: 13bd96aa
-  KaRaMeL version: 9926c187
+  F* version: c990b3ca
+  KaRaMeL version: c27466aa
  */
 
 #include "internal/core.h"

diff --git a/libcrux/src/libcrux_kyber.c b/libcrux/src/libcrux_kyber.c
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /Users/jonathan/Code/eurydice/eurydice --config
-  ../../kyber-c.yaml ../libcrux_kyber.llbc F* version: 13bd96aa KaRaMeL version:
-  9926c187
+  ../../kyber-c.yaml ../libcrux_kyber.llbc F* version: c990b3ca KaRaMeL version:
+  c27466aa
  */
 
 #include "internal/libcrux_kyber.h"
@@ -2224,23 +2224,59 @@ generate_keypair_unpacked___3size_t_1184size_t_1152size_t_2size_t_128size_t(
       }
     }
   }
-  int32_t uu____9[3U][256U];
-  memcpy(uu____9, secret_as_ntt, (size_t)3U * sizeof(int32_t[256U]));
-  int32_t uu____10[3U][256U];
-  memcpy(uu____10, t_as_ntt, (size_t)3U * sizeof(int32_t[256U]));
-  int32_t uu____11[3U][3U][256U];
-  memcpy(uu____11, a_transpose, (size_t)3U * sizeof(int32_t[3U][256U]));
+  int32_t a_matrix[3U][3U][256U];
+  memcpy(a_matrix, a_transpose, (size_t)3U * sizeof(int32_t[3U][256U]));
+  core_ops_range_Range__size_t iter1 =
+    core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I___into_iter(
+      ((core_ops_range_Range__size_t){ .start = (size_t)0U,
+                                       .end = (size_t)3U }),
+      core_ops_range_Range__size_t,
+      core_ops_range_Range__size_t);
+  while (true) {
+    core_option_Option__size_t uu____9 =
+      core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___3__next(
+        &iter1, size_t, core_option_Option__size_t);
+    if (uu____9.tag == core_option_None) {
+      break;
+    } else {
+      size_t i = uu____9.f0;
+      core_ops_range_Range__size_t iter =
+        core_iter_traits_collect___core__iter__traits__collect__IntoIterator_for_I___into_iter(
+          ((core_ops_range_Range__size_t){ .start = (size_t)0U,
+                                           .end = (size_t)3U }),
+          core_ops_range_Range__size_t,
+          core_ops_range_Range__size_t);
+      while (true) {
+        core_option_Option__size_t uu____10 =
+          core_iter_range___core__iter__traits__iterator__Iterator_for_core__ops__range__Range_A___3__next(
+            &iter, size_t, core_option_Option__size_t);
+        if (uu____10.tag == core_option_None) {
+          break;
+        } else {
+          size_t j = uu____10.f0;
+          memcpy(
+            a_matrix[i][j], a_transpose[j][i], (size_t)256U * sizeof(int32_t));
+        }
+      }
+    }
+  }
+  int32_t uu____11[3U][256U];
+  memcpy(uu____11, secret_as_ntt, (size_t)3U * sizeof(int32_t[256U]));
+  int32_t uu____12[3U][256U];
+  memcpy(uu____12, t_as_ntt, (size_t)3U * sizeof(int32_t[256U]));
+  int32_t uu____13[3U][3U][256U];
+  memcpy(uu____13, a_matrix, (size_t)3U * sizeof(int32_t[3U][256U]));
   __libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__3size_t_
-    uu____12;
-  memcpy(uu____12.fst, uu____9, (size_t)3U * sizeof(int32_t[256U]));
-  memcpy(uu____12.snd, uu____10, (size_t)3U * sizeof(int32_t[256U]));
-  memcpy(uu____12.thd, uu____11, (size_t)3U * sizeof(int32_t[3U][256U]));
-  uint8_t uu____13[1184U];
-  memcpy(uu____13, public_key_serialized, (size_t)1184U * sizeof(uint8_t));
+    uu____14;
+  memcpy(uu____14.fst, uu____11, (size_t)3U * sizeof(int32_t[256U]));
+  memcpy(uu____14.snd, uu____12, (size_t)3U * sizeof(int32_t[256U]));
+  memcpy(uu____14.thd, uu____13, (size_t)3U * sizeof(int32_t[3U][256U]));
+  uint8_t uu____15[1184U];
+  memcpy(uu____15, public_key_serialized, (size_t)1184U * sizeof(uint8_t));
   __libcrux_kyber_arithmetic_PolynomialRingElement_3size_t____libcrux_kyber_arithmetic_PolynomialRingElement_3size_t____libcrux_kyber_arithmetic_PolynomialRingElement_3size_t__3size_t__uint8_t_1184size_t_
     lit;
-  lit.fst = uu____12;
-  memcpy(lit.snd, uu____13, (size_t)1184U * sizeof(uint8_t));
+  lit.fst = uu____14;
+  memcpy(lit.snd, uu____15, (size_t)1184U * sizeof(uint8_t));
   return lit;
 }
 
@@ -3285,12 +3321,12 @@ encrypt___3size_t_1088size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320
     t_as_ntt);
   Eurydice_slice seed = Eurydice_slice_subslice_from(
     public_key, (size_t)1152U, uint8_t, size_t, Eurydice_slice);
-  int32_t A_transpose[3U][3U][256U];
+  int32_t a_transpose[3U][3U][256U];
   uint8_t ret0[34U];
   into_padded_array___34size_t(seed, ret0);
-  sample_matrix_A___3size_t(ret0, false, A_transpose);
+  sample_matrix_A___3size_t(ret0, false, a_transpose);
   int32_t(*uu____0)[256U] = t_as_ntt;
-  int32_t(*uu____1)[3U][256U] = A_transpose;
+  int32_t(*uu____1)[3U][256U] = a_transpose;
   uint8_t uu____2[32U];
   memcpy(uu____2, message, (size_t)32U * sizeof(uint8_t));
   uint8_t ret1[1088U];
@@ -3856,7 +3892,7 @@ void
 libcrux_kyber_kyber768_decapsulate_unpacked(
   int32_t (*secret_as_ntt)[256U],
   int32_t (*t_as_ntt)[256U],
-  int32_t (*A_transpose)[3U][256U],
+  int32_t (*a_transpose)[3U][256U],
   Eurydice_slice implicit_rejection_value,
   Eurydice_slice ind_cpa_public_key_hash,
   uint8_t (*ciphertext)[1088U],
@@ -3866,7 +3902,7 @@ libcrux_kyber_kyber768_decapsulate_unpacked(
   decapsulate_unpacked___3size_t_2400size_t_1152size_t_1184size_t_1088size_t_1152size_t_960size_t_128size_t_10size_t_4size_t_320size_t_2size_t_128size_t_2size_t_128size_t_1120size_t(
     secret_as_ntt,
     t_as_ntt,
-    A_transpose,
+    a_transpose,
     implicit_rejection_value,
     ind_cpa_public_key_hash,
     ciphertext,