Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Document verification status #711

Merged
merged 25 commits into from
Dec 11, 2024
Merged

Document verification status #711

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
52178f6
F* update
karthikbhargavan Dec 4, 2024
18c6c50
f* refresh\
karthikbhargavan Dec 4, 2024
bcca540
bitveveq
karthikbhargavan Dec 4, 2024
933ef33
Merge branch 'dev-review-comments' into dev-verification-status
karthikbhargavan Dec 4, 2024
4ac64bc
status
karthikbhargavan Dec 4, 2024
0d5c258
rlimit
karthikbhargavan Dec 5, 2024
4fe679b
Fix verification
mamonet Dec 6, 2024
0972f98
Fix verification
mamonet Dec 6, 2024
6fe9324
make verification
mamonet Dec 6, 2024
adbf482
fix verification
mamonet Dec 6, 2024
d1a299a
verif status
karthikbhargavan Dec 9, 2024
4d93aa6
Update Makefile
mamonet Dec 10, 2024
c70eb87
Remove AVX2 modules from ADMIT_MODULES
mamonet Dec 10, 2024
2f140ae
Remove admits from vector/avx2.rs
mamonet Dec 10, 2024
ce63901
updated verification status
karthikbhargavan Dec 11, 2024
703cabd
Merge branch 'dev' into dev-verification-status
karthikbhargavan Dec 11, 2024
a197c4d
fmt
karthikbhargavan Dec 11, 2024
d3bc868
c code refresh
karthikbhargavan Dec 11, 2024
b0ff2c5
Put Vector.Rej_sample_table in SLOW_MODULES
mamonet Dec 11, 2024
d1cba65
table for verification status
karthikbhargavan Dec 11, 2024
d8a1a29
linked issue
karthikbhargavan Dec 11, 2024
38cc1db
verif status
karthikbhargavan Dec 11, 2024
578d7f6
raw strings
karthikbhargavan Dec 11, 2024
0953378
raw strings
karthikbhargavan Dec 11, 2024
939e5ea
issue ref
karthikbhargavan Dec 11, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/code_gen.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@ This code was generated with the following revisions:
Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
F*: 5643e656b989aca7629723653a2570c7df6252b9
Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/internal/libcrux_core.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#ifndef __internal_libcrux_core_H
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/internal/libcrux_mlkem_avx2.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#ifndef __internal_libcrux_mlkem_avx2_H
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/internal/libcrux_mlkem_portable.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#ifndef __internal_libcrux_mlkem_portable_H
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/internal/libcrux_sha3_avx2.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#ifndef __internal_libcrux_sha3_avx2_H
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/internal/libcrux_sha3_internal.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#ifndef __internal_libcrux_sha3_internal_H
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/libcrux_core.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#include "internal/libcrux_core.h"
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/libcrux_core.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#ifndef __libcrux_core_H
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/libcrux_mlkem1024.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#ifndef __libcrux_mlkem1024_H
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/libcrux_mlkem1024_avx2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#include "libcrux_mlkem1024_avx2.h"
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/libcrux_mlkem1024_avx2.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#ifndef __libcrux_mlkem1024_avx2_H
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/libcrux_mlkem1024_portable.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#include "libcrux_mlkem1024_portable.h"
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/libcrux_mlkem1024_portable.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#ifndef __libcrux_mlkem1024_portable_H
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/libcrux_mlkem512.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#ifndef __libcrux_mlkem512_H
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/libcrux_mlkem512_avx2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#include "libcrux_mlkem512_avx2.h"
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/libcrux_mlkem512_avx2.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#ifndef __libcrux_mlkem512_avx2_H
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/libcrux_mlkem512_portable.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#include "libcrux_mlkem512_portable.h"
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/libcrux_mlkem512_portable.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#ifndef __libcrux_mlkem512_portable_H
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/libcrux_mlkem768.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#ifndef __libcrux_mlkem768_H
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/libcrux_mlkem768_avx2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#include "libcrux_mlkem768_avx2.h"
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/libcrux_mlkem768_avx2.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#ifndef __libcrux_mlkem768_avx2_H
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/libcrux_mlkem768_portable.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#include "libcrux_mlkem768_portable.h"
Expand Down
4 changes: 2 additions & 2 deletions libcrux-ml-kem/c/libcrux_mlkem768_portable.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
* Charon: 45f5a34f336e35c6cc2253bc90cbdb8d812cefa9
* Eurydice: e2db6e88adc9995ca9d3dedf7fa9bc4095e9ca20
* Karamel: 8c3612018c25889288da6857771be3ad03b75bcd
* F*: 5643e656b989aca7629723653a2570c7df6252b9
* Libcrux: fbef3649fa222b800fc7dcc349855bcd7de48e36
* F*: 8b6fce63ca91b16386d8f76e82ea87a3c109a208
* Libcrux: a197c4d7286246d59e3044d437b3da9119cd5de8
*/

#ifndef __libcrux_mlkem768_portable_H
Expand Down
Loading
Loading