refreshed C code, after merging properly and bugfix

cryspen · Jul 1, 2024 · f6b0243 · f6b0243
1 parent 69e8c73
commit f6b0243
Show file tree

Hide file tree

Showing 34 changed files with 566 additions and 732 deletions.
diff --git a/libcrux-ml-kem/c/code_gen.txt b/libcrux-ml-kem/c/code_gen.txt
@@ -1,5 +1,5 @@
 This code was generated with the following tools:
-Charon: 23f20c184e51015582b7918ea4f1eb063b28daba
-Eurydice: 30fdb50add4dabaee90051878c166bac8c5ac26a
+Charon: aeeae1d46704810bf498db552a75dff15aa3abcc
+Eurydice: ffeb01ce4cf0646e5cadec836bc042f98b8a16a8
 Karamel: 42a431696cd32d41155d7e484720eb71fd5dc7b1
-F*: a32b316e521fa4f239b610ec8f1d15e78d62cbe8-dirty
+F*: f09228ef9a64ac4ef383ee0e10656ccb612db2ee
diff --git a/libcrux-ml-kem/c/internal/libcrux_core.h b/libcrux-ml-kem/c/internal/libcrux_core.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
   KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: f09228ef KaRaMeL
-  version: 42a43169
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #ifndef __internal_libcrux_core_H

diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #ifndef __internal_libcrux_mlkem_avx2_H

diff --git a/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h b/libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #ifndef __internal_libcrux_mlkem_portable_H

diff --git a/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h b/libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #ifndef __internal_libcrux_sha3_avx2_H

diff --git a/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h b/libcrux-ml-kem/c/internal/libcrux_sha3_internal.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #ifndef __internal_libcrux_sha3_internal_H

diff --git a/libcrux-ml-kem/c/libcrux_core.c b/libcrux-ml-kem/c/libcrux_core.c
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #include "internal/libcrux_core.h"

diff --git a/libcrux-ml-kem/c/libcrux_core.h b/libcrux-ml-kem/c/libcrux_core.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #ifndef __libcrux_core_H
@@ -128,11 +128,11 @@ typedef struct
 #define core_result_Err 1
 
 typedef uint8_t
-    core_result_Result__uint8_t_24size_t__core_array_TryFromSliceError_tags;
+    core_result_Result__uint8_t_32size_t__core_array_TryFromSliceError_tags;
 
 typedef struct
     core_result_Result__uint8_t_8size_t__core_array_TryFromSliceError_s {
-  core_result_Result__uint8_t_24size_t__core_array_TryFromSliceError_tags tag;
+  core_result_Result__uint8_t_32size_t__core_array_TryFromSliceError_tags tag;
   union {
     uint8_t case_Ok[8U];
     core_array_TryFromSliceError case_Err;

diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024.h b/libcrux-ml-kem/c/libcrux_mlkem1024.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #ifndef __libcrux_mlkem1024_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #include "libcrux_mlkem1024_avx2.h"

diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #ifndef __libcrux_mlkem1024_avx2_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.c
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #include "libcrux_mlkem1024_portable.h"

diff --git a/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h b/libcrux-ml-kem/c/libcrux_mlkem1024_portable.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #ifndef __libcrux_mlkem1024_portable_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem512.h b/libcrux-ml-kem/c/libcrux_mlkem512.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #ifndef __libcrux_mlkem512_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.c
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #include "libcrux_mlkem512_avx2.h"

diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem512_avx2.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #ifndef __libcrux_mlkem512_avx2_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_portable.c b/libcrux-ml-kem/c/libcrux_mlkem512_portable.c
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #include "libcrux_mlkem512_portable.h"

diff --git a/libcrux-ml-kem/c/libcrux_mlkem512_portable.h b/libcrux-ml-kem/c/libcrux_mlkem512_portable.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #ifndef __libcrux_mlkem512_portable_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem768.h b/libcrux-ml-kem/c/libcrux_mlkem768.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #ifndef __libcrux_mlkem768_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.c
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #include "libcrux_mlkem768_avx2.h"

diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h b/libcrux-ml-kem/c/libcrux_mlkem768_avx2.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #ifndef __libcrux_mlkem768_avx2_H

diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_portable.c b/libcrux-ml-kem/c/libcrux_mlkem768_portable.c
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #include "libcrux_mlkem768_portable.h"

diff --git a/libcrux-ml-kem/c/libcrux_mlkem768_portable.h b/libcrux-ml-kem/c/libcrux_mlkem768_portable.h
@@ -1,8 +1,8 @@
 /*
   This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
-  KaRaMeL invocation: /home/franziskus/eurydice//eurydice --config ../c.yaml
-  ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F* version: <unknown>
-  KaRaMeL version: 42a43169
+  KaRaMeL invocation: /home/karthik/eurydice/eurydice --config ../c.yaml
+  -funroll-loops 16 ../../libcrux_ml_kem.llbc ../../libcrux_sha3.llbc F*
+  version: f09228ef KaRaMeL version: 42a43169
  */
 
 #ifndef __libcrux_mlkem768_portable_H