Trying to add an Fstar interface for Hacl SIMD Sha3.

cryspen · Dec 6, 2023 · d6ecfa0 · d6ecfa0
1 parent 697d323
commit d6ecfa0
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 0 deletions.
diff --git a/proofs/fstar/extraction/Libcrux.Hacl.Sha3.Simd256.fsti b/proofs/fstar/extraction/Libcrux.Hacl.Sha3.Simd256.fsti
@@ -0,0 +1,6 @@
+module Libcrux.Hacl.Sha3.Simd256
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Rust_primitives
+open Core
+
+val shake128 (v_LEN: usize) (payload0: t_Slice u8) (payload1: t_Slice u8) (payload2: t_Slice u8) (payload3: t_Slice u8): ((t_Array u8 v_LEN) & (t_Array u8 v_LEN) & (t_Array u8 v_LEN) & (t_Array u8 v_LEN))
diff --git a/proofs/fstar/extraction/Makefile b/proofs/fstar/extraction/Makefile
@@ -52,6 +52,7 @@ VERIFIED = \
 	Libcrux.Kem.fst \
 	Libcrux.Kem.Kyber.Constants.fst \
 	Libcrux.Digest.fsti \
+	Libcrux.Hacl.Sha3.Simd256.fsti \
 	Libcrux.Kem.Kyber.Hash_functions.fst \
 	Libcrux.Kem.Kyber.Kyber768.fst \
 	Libcrux.Kem.Kyber.Kyber1024.fst \